--- a/src/HOLCF/IOA/NTP/Impl.ML Sat May 27 19:49:36 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,315 +0,0 @@
-(* Title: HOL/IOA/NTP/Impl.ML
- ID: $Id$
- 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);