# File Impl.ML

    (*  Title:      HOL/IOA/NTP/Impl.ML
        ID:         $Id: Impl.ML,v 1.21 2005/09/03 14:50:24 wenzelm Exp $
        Author:     Tobias Nipkow & Konrad Slind

    The implementation --- Invariants.
    *)

    Addsimps [Let_def, le_SucI];

    val impl_ioas =
      [impl_def,
       sender_ioa_def,
       receiver_ioa_def,
       srch_ioa_thm RS eq_reflection,
       rsch_ioa_thm RS eq_reflection];

    val transitions = [sender_trans_def, receiver_trans_def,
                       srch_trans_def, rsch_trans_def];

    Addsimps [ioa_triple_proj, starts_of_par, trans_of_par4,
              in_sender_asig, in_receiver_asig, in_srch_asig,
              in_rsch_asig];
    Addcongs [let_weak_cong];

    Goal
      "fst(x) = sen(x)            & \
    \  fst(snd(x)) = rec(x)       & \
    \  fst(snd(snd(x))) = srch(x) & \
    \  snd(snd(snd(x))) = rsch(x)";
    by (simp_tac (simpset() addsimps
                 [sen_def,rec_def,srch_def,rsch_def]) 1);
    Addsimps [result()];

    Goal "a:actions(sender_asig)   \
    \            | a:actions(receiver_asig) \
    \            | a:actions(srch_asig)     \
    \            | a:actions(rsch_asig)";
      by (induct_tac "a" 1);
      by (ALLGOALS (Simp_tac));
    Addsimps [result()];

    Delsimps [split_paired_All];

    (* Three Simp_sets in different sizes
    ----------------------------------------------

    1) simpset() does not unfold the transition relations
    2) ss unfolds transition relations
    3) renname_ss unfolds transitions and the abstract channel *)

    val ss = (simpset() addsimps transitions);
    val rename_ss = (ss addsimps unfold_renaming);

    val tac     = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]);
    val tac_ren = asm_simp_tac (rename_ss addcongs [conj_cong] addsplits [split_if]);

    (* INVARIANT 1 *)

    Goalw impl_ioas "invariant impl_ioa inv1";
    by (rtac invariantI 1);
    by (asm_full_simp_tac (simpset()
       addsimps [inv1_def, hdr_sum_def, srcvd_def,
                 ssent_def, rsent_def,rrcvd_def]) 1);

    by (simp_tac (simpset() delsimps [trans_of_par4]
                    addsimps [imp_conjR,inv1_def]) 1);

    (* Split proof in two *)
    by (rtac conjI 1);

    (* First half *)
    by (asm_full_simp_tac (simpset() addsimps [thm "Impl.inv1_def"]
                                     delsplits [split_if]) 1);
    by (rtac action.induct 1);

    by (EVERY1[tac, tac, tac, tac]);
    by (tac 1);
    by (tac_ren 1);

    (* 5 + 1 *)

    by (tac 1);
    by (tac_ren 1);

    (* 4 + 1 *)
    by (EVERY1[tac, tac, tac, tac]);

    (* Now the other half *)
    by (asm_full_simp_tac (simpset() addsimps [thm "Impl.inv1_def"]
                                     delsplits [split_if]) 1);
    by (rtac action.induct 1);
    by (EVERY1[tac, tac]);

    (* detour 1 *)
    by (tac 1);
    by (tac_ren 1);
    by (rtac impI 1);
    by (REPEAT (etac conjE 1));
    by (asm_simp_tac (simpset() addsimps [hdr_sum_def, Multiset.count_def,
                                          Multiset.countm_nonempty_def]
                                addsplits [split_if]) 1);
    (* detour 2 *)
    by (tac 1);
    by (tac_ren 1);
    by (rtac impI 1);
    by (REPEAT (etac conjE 1));
    by (asm_full_simp_tac (simpset() addsimps [thm "Impl.hdr_sum_def",
                                             Multiset.count_def,
                                             Multiset.countm_nonempty_def,
                                             Multiset.delm_nonempty_def]
                                     addsplits [split_if]) 1);
    by (rtac allI 1);
    by (rtac conjI 1);
    by (rtac impI 1);
    by (hyp_subst_tac 1);
    by (rtac (pred_suc RS iffD1) 1);
    by (dtac less_le_trans 1);
    by (cut_facts_tac [rewrite_rule[thm "Packet.hdr_def"]
                       eq_packet_imp_eq_hdr RS countm_props] 1);;
    by (assume_tac 1);
    by (assume_tac 1);

    by (rtac (countm_done_delm RS mp RS sym) 1);
    by (rtac refl 1);
    by (asm_simp_tac (simpset() addsimps [Multiset.count_def]) 1);

    by (rtac impI 1);
    by (asm_full_simp_tac (simpset() addsimps [neg_flip]) 1);
    by (hyp_subst_tac 1);
    by (rtac countm_spurious_delm 1);
    by (Simp_tac 1);

    by (EVERY1[tac, tac, tac, tac, tac, tac]);

    qed "inv1";

    (* INVARIANT 2 *)

    Goal "invariant impl_ioa inv2";

      by (rtac invariantI1 1);
      (* Base case *)
      by (asm_full_simp_tac (simpset() addsimps (inv2_def ::
                              (receiver_projections
                               @ sender_projections @ impl_ioas)))
          1);

      by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
      by (induct_tac "a" 1);

      (* 10 cases. First 4 are simple, since state doesn't change *)

    val tac2 = asm_full_simp_tac (ss addsimps [inv2_def]);

      (* 10 - 7 *)
      by (EVERY1[tac2,tac2,tac2,tac2]);
      (* 6 *)
      by (forward_tac [rewrite_rule [thm "Impl.inv1_def"]
                                   (inv1 RS invariantE) RS conjunct1] 1);
      (* 6 - 5 *)
      by (EVERY1[tac2,tac2]);

      (* 4 *)
      by (forward_tac [rewrite_rule [thm "Impl.inv1_def"]
                                    (inv1 RS invariantE) RS conjunct1] 1);
      by (tac2 1);

      (* 3 *)
      by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE)] 1);

      by (tac2 1);
      by (fold_tac [rewrite_rule [thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")]);
      by (arith_tac 1);

      (* 2 *)
      by (tac2 1);
      by (forward_tac [rewrite_rule [thm "Impl.inv1_def"]
                                   (inv1 RS invariantE) RS conjunct1] 1);
      by (strip_tac 1);
      by (REPEAT (etac conjE 1));
      by (Asm_full_simp_tac 1);

      (* 1 *)
      by (tac2 1);
      by (forward_tac [rewrite_rule [thm "Impl.inv1_def"]
                                   (inv1 RS invariantE) RS conjunct2] 1);
      by (strip_tac 1);
      by (REPEAT (etac conjE 1));
      by (fold_tac  [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")]);
      by (Asm_full_simp_tac 1);
    qed "inv2";

    (* INVARIANT 3 *)

    Goal "invariant impl_ioa inv3";

      by (rtac invariantI 1);
      (* Base case *)
      by (asm_full_simp_tac (simpset() addsimps
                        (thm "Impl.inv3_def" :: (receiver_projections
                                           @ sender_projections @ impl_ioas))) 1);

      by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
      by (induct_tac "a" 1);

    val tac3 = asm_full_simp_tac (ss addsimps [inv3_def]);

      (* 10 - 8 *)

      by (EVERY1[tac3,tac3,tac3]);

      by (tac_ren 1);
      by (strip_tac  1 THEN REPEAT (etac conjE 1));
      by (hyp_subst_tac 1);
      by (etac exE 1);
      by (Asm_full_simp_tac 1);

      (* 7 *)
      by (tac3 1);
      by (tac_ren 1);
      by (Force_tac 1);

      (* 6 - 3 *)

      by (EVERY1[tac3,tac3,tac3,tac3]);

      (* 2 *)
      by (asm_full_simp_tac ss 1);
      by (simp_tac (simpset() addsimps [inv3_def]) 1);
      by (strip_tac  1 THEN REPEAT (etac conjE 1));
      by (rtac (imp_disjL RS iffD1) 1);
      by (rtac impI 1);
      by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1);
      by (Asm_full_simp_tac 1);
      by (REPEAT (etac conjE 1));
      by (res_inst_tac [("j","count (ssent(sen s)) (~sbit(sen s))"),
                        ("k","count (rsent(rec s)) (sbit(sen s))")] le_trans 1);
      by (forward_tac [rewrite_rule [inv1_def]
                                    (inv1 RS invariantE) RS conjunct2] 1);
      by (asm_full_simp_tac (simpset() addsimps
                             [hdr_sum_def, Multiset.count_def]) 1);
      by (rtac add_le_mono 1);
      by (rtac countm_props 1);
      by (Simp_tac 1);
      by (rtac countm_props 1);
      by (Simp_tac 1);
      by (assume_tac 1);

      (* 1 *)
      by (tac3 1);
      by (strip_tac  1 THEN REPEAT (etac conjE 1));
      by (rtac (imp_disjL RS iffD1) 1);
      by (rtac impI 1);
      by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1);
      by (Asm_full_simp_tac 1);
    qed "inv3";

    (* INVARIANT 4 *)

    Goal "invariant impl_ioa inv4";

      by (rtac invariantI 1);
      (* Base case *)
      by (asm_full_simp_tac (simpset() addsimps
                        (thm "Impl.inv4_def" :: (receiver_projections
                                           @ sender_projections @ impl_ioas))) 1);

      by (asm_simp_tac (simpset() addsimps impl_ioas delsplits [split_if]) 1);
      by (induct_tac "a" 1);

    val tac4 =  asm_full_simp_tac (ss addsimps [inv4_def]);

      (* 10 - 2 *)

      by (EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]);

     (* 2 b *)

      by (strip_tac  1 THEN REPEAT (etac conjE 1));
      by (forward_tac [rewrite_rule [thm "Impl.inv2_def"]
                                   (inv2 RS invariantE)] 1);
      by (Asm_full_simp_tac 1);

      (* 1 *)
      by (tac4 1);
      by (strip_tac  1 THEN REPEAT (etac conjE 1));
      by (rtac ccontr 1);
      by (forward_tac [rewrite_rule [thm "Impl.inv2_def"]
                                   (inv2 RS invariantE)] 1);
      by (forward_tac [rewrite_rule [thm "Impl.inv3_def"]
                                   (inv3 RS invariantE)] 1);
      by (Asm_full_simp_tac 1);
      by (eres_inst_tac [("x","m")] allE 1);
      by (Asm_full_simp_tac 1);
    qed "inv4";

    (* rebind them *)

    val inv1 = rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE);
    val inv2 = rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE);
    val inv3 = rewrite_rule [thm "Impl.inv3_def"] (inv3 RS invariantE);
    val inv4 = rewrite_rule [thm "Impl.inv4_def"] (inv4 RS invariantE);