--- a/src/HOLCF/IOA/NTP/Impl.ML Sat Sep 03 16:49:48 2005 +0200
+++ b/src/HOLCF/IOA/NTP/Impl.ML Sat Sep 03 16:50:22 2005 +0200
@@ -9,18 +9,16 @@
Addsimps [Let_def, le_SucI];
-open Abschannel Impl;
-
val impl_ioas =
- [Impl.impl_def,
- Sender.sender_ioa_def,
- Receiver.receiver_ioa_def,
+ [impl_def,
+ sender_ioa_def,
+ receiver_ioa_def,
srch_ioa_thm RS eq_reflection,
rsch_ioa_thm RS eq_reflection];
-val transitions = [Sender.sender_trans_def, Receiver.receiver_trans_def,
+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,
@@ -47,15 +45,15 @@
Delsimps [split_paired_All];
-(* Three Simp_sets in different sizes
+(* Three Simp_sets in different sizes
----------------------------------------------
-1) simpset() does not unfold the transition relations
-2) ss unfolds transition relations
+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 ss = (simpset() addsimps transitions);
val rename_ss = (ss addsimps unfold_renaming);
val tac = asm_simp_tac (ss addcongs [conj_cong] addsplits [split_if]);
@@ -68,19 +66,19 @@
Goalw impl_ioas "invariant impl_ioa inv1";
by (rtac invariantI 1);
by (asm_full_simp_tac (simpset()
- addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
- Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
+ 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);
+by (rtac conjI 1);
(* First half *)
-by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
+by (asm_full_simp_tac (simpset() addsimps [thm "Impl.inv1_def"]
delsplits [split_if]) 1);
-by (rtac Action.action.induct 1);
+by (rtac action.induct 1);
by (EVERY1[tac, tac, tac, tac]);
by (tac 1);
@@ -96,9 +94,9 @@
(* Now the other half *)
-by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]
+by (asm_full_simp_tac (simpset() addsimps [thm "Impl.inv1_def"]
delsplits [split_if]) 1);
-by (rtac Action.action.induct 1);
+by (rtac action.induct 1);
by (EVERY1[tac, tac]);
(* detour 1 *)
@@ -114,7 +112,7 @@
by (tac_ren 1);
by (rtac impI 1);
by (REPEAT (etac conjE 1));
-by (asm_full_simp_tac (simpset() addsimps [Impl.hdr_sum_def,
+by (asm_full_simp_tac (simpset() addsimps [thm "Impl.hdr_sum_def",
Multiset.count_def,
Multiset.countm_nonempty_def,
Multiset.delm_nonempty_def]
@@ -125,7 +123,7 @@
by (hyp_subst_tac 1);
by (rtac (pred_suc RS iffD1) 1);
by (dtac less_le_trans 1);
-by (cut_facts_tac [rewrite_rule[Packet.hdr_def]
+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);
@@ -150,10 +148,10 @@
Goal "invariant impl_ioa inv2";
- by (rtac invariantI1 1);
+ by (rtac invariantI1 1);
(* Base case *)
by (asm_full_simp_tac (simpset() addsimps (inv2_def ::
- (receiver_projections
+ (receiver_projections
@ sender_projections @ impl_ioas)))
1);
@@ -167,26 +165,26 @@
(* 10 - 7 *)
by (EVERY1[tac2,tac2,tac2,tac2]);
(* 6 *)
- by (forward_tac [rewrite_rule [Impl.inv1_def]
+ 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 [Impl.inv1_def]
+ by (forward_tac [rewrite_rule [thm "Impl.inv1_def"]
(inv1 RS invariantE) RS conjunct1] 1);
by (tac2 1);
(* 3 *)
- by (forward_tac [rewrite_rule [Impl.inv1_def] (inv1 RS invariantE)] 1);
+ by (forward_tac [rewrite_rule [thm "Impl.inv1_def"] (inv1 RS invariantE)] 1);
by (tac2 1);
- by (fold_tac [rewrite_rule [Packet.hdr_def]Impl.hdr_sum_def]);
+ 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 [Impl.inv1_def]
+ by (forward_tac [rewrite_rule [thm "Impl.inv1_def"]
(inv1 RS invariantE) RS conjunct1] 1);
by (strip_tac 1);
by (REPEAT (etac conjE 1));
@@ -194,11 +192,11 @@
(* 1 *)
by (tac2 1);
- by (forward_tac [rewrite_rule [Impl.inv1_def]
+ 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[Packet.hdr_def]Impl.hdr_sum_def]);
+ by (fold_tac [rewrite_rule[thm "Packet.hdr_def"] (thm "Impl.hdr_sum_def")]);
by (Asm_full_simp_tac 1);
qed "inv2";
@@ -207,10 +205,10 @@
Goal "invariant impl_ioa inv3";
- by (rtac invariantI 1);
+ by (rtac invariantI 1);
(* Base case *)
- by (asm_full_simp_tac (simpset() addsimps
- (Impl.inv3_def :: (receiver_projections
+ 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);
@@ -221,7 +219,7 @@
(* 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);
@@ -231,7 +229,7 @@
(* 7 *)
by (tac3 1);
by (tac_ren 1);
- by (Force_tac 1);
+ by (Force_tac 1);
(* 6 - 3 *)
@@ -243,7 +241,7 @@
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 [Impl.inv2_def] (inv2 RS invariantE)] 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))"),
@@ -264,7 +262,7 @@
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 [Impl.inv2_def] (inv2 RS invariantE)] 1);
+ by (forward_tac [rewrite_rule [thm "Impl.inv2_def"] (inv2 RS invariantE)] 1);
by (Asm_full_simp_tac 1);
qed "inv3";
@@ -273,10 +271,10 @@
Goal "invariant impl_ioa inv4";
- by (rtac invariantI 1);
+ by (rtac invariantI 1);
(* Base case *)
- by (asm_full_simp_tac (simpset() addsimps
- (Impl.inv4_def :: (receiver_projections
+ 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);
@@ -291,7 +289,7 @@
(* 2 b *)
by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by (forward_tac [rewrite_rule [Impl.inv2_def]
+ by (forward_tac [rewrite_rule [thm "Impl.inv2_def"]
(inv2 RS invariantE)] 1);
by (Asm_full_simp_tac 1);
@@ -299,9 +297,9 @@
by (tac4 1);
by (strip_tac 1 THEN REPEAT (etac conjE 1));
by (rtac ccontr 1);
- by (forward_tac [rewrite_rule [Impl.inv2_def]
+ by (forward_tac [rewrite_rule [thm "Impl.inv2_def"]
(inv2 RS invariantE)] 1);
- by (forward_tac [rewrite_rule [Impl.inv3_def]
+ 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);
@@ -311,7 +309,7 @@
(* rebind them *)
-val inv1 = rewrite_rule [Impl.inv1_def] (inv1 RS invariantE);
-val inv2 = rewrite_rule [Impl.inv2_def] (inv2 RS invariantE);
-val inv3 = rewrite_rule [Impl.inv3_def] (inv3 RS invariantE);
-val inv4 = rewrite_rule [Impl.inv4_def] (inv4 RS invariantE);
+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);