--- a/src/HOLCF/IOA/ABP/Correctness.ML Thu Jul 08 13:38:41 1999 +0200
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Thu Jul 08 13:42:31 1999 +0200
@@ -33,8 +33,6 @@
asig_projections @ set_lemmas;
Addsimps hom_ioas;
-Addsimps [reduce_Nil,reduce_Cons];
-
(* auxiliary function *)
@@ -43,70 +41,27 @@
(* lemmas about reduce *)
Goal "(reduce(l)=[]) = (l=[])";
- by (rtac iffI 1);
- by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
- by (Fast_tac 1);
- by (induct_tac "l" 1);
- by (Simp_tac 1);
- by (Simp_tac 1);
- by (rtac (list.split RS iffD2) 1);
- by (Asm_full_simp_tac 1);
- by (REPEAT (rtac allI 1));
- by (rtac impI 1);
- by (hyp_subst_tac 1);
- by (stac split_if 1);
- by (Asm_full_simp_tac 1);
- by (Asm_full_simp_tac 1);
+by (induct_tac "l" 1);
+by (auto_tac (claset(), simpset() addsplits [list.split]));
val l_iff_red_nil = result();
Goal "s~=[] --> hd(s)=hd(reduce(s))";
by (induct_tac "s" 1);
-by (Simp_tac 1);
-by (case_tac "list =[]" 1);
-by (Asm_full_simp_tac 1);
-(* main case *)
-by (rotate 1 1);
-by (asm_full_simp_tac list_ss 1);
-by (Simp_tac 1);
-by (rtac (list.split RS iffD2) 1);
-by (asm_full_simp_tac list_ss 1);
-by (REPEAT (rtac allI 1));
- by (rtac impI 1);
-by (stac split_if 1);
-by (REPEAT(hyp_subst_tac 1));
-by (etac subst 1);
-by (Simp_tac 1);
+by (auto_tac (claset(), simpset() addsplits [list.split]));
qed"hd_is_reduce_hd";
(* to be used in the following Lemma *)
Goal "l~=[] --> reverse(reduce(l))~=[]";
by (induct_tac "l" 1);
-by (Simp_tac 1);
-by (case_tac "list =[]" 1);
-by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
-(* main case *)
-by (rotate 1 1);
-by (Asm_full_simp_tac 1);
-by (cut_inst_tac [("l","list")] cons_not_nil 1);
-by (Asm_full_simp_tac 1);
-by (REPEAT (etac exE 1));
-by (Asm_simp_tac 1);
-by (stac split_if 1);
-by (hyp_subst_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
-qed"rev_red_not_nil";
+by (auto_tac (claset(), simpset() addsplits [list.split]));
+qed_spec_mp "rev_red_not_nil";
(* shows applicability of the induction hypothesis of the following Lemma 1 *)
-Goal "!!l.[| l~=[] |] ==> \
-\ hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
+Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
by (Simp_tac 1);
- by (rtac (list.split RS iffD2) 1);
- by (asm_full_simp_tac list_ss 1);
- by (REPEAT (rtac allI 1));
- by (rtac impI 1);
- by (stac split_if 1);
- by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
- (rev_red_not_nil RS mp)]) 1);
+ by (asm_full_simp_tac (list_ss addsplits [list.split]
+ addsimps [reverse_Cons,hd_append,
+ rev_red_not_nil]) 1);
qed"last_ind_on_first";
val impl_ss = simpset() delsimps [reduce_Cons];
@@ -145,21 +100,14 @@
(* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
-Goal
- "!! s. [| s~=[] |] ==> \
+Goal "s~=[] ==> \
\ if hd(s)=hd(tl(s)) & tl(s)~=[] then \
\ reduce(tl(s))=reduce(s) else \
\ reduce(tl(s))=tl(reduce(s))";
by (cut_inst_tac [("l","s")] cons_not_nil 1);
by (Asm_full_simp_tac 1);
by (REPEAT (etac exE 1));
-by (Asm_full_simp_tac 1);
-by (stac split_if 1);
-by (rtac conjI 1);
-by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
-by (Step_tac 1);
-by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
-by (Auto_tac);
+by (auto_tac (claset(), simpset() addsplits [list.split]));
val reduce_tl =result();
@@ -167,16 +115,17 @@
C h a n n e l A b s t r a c t i o n
*******************************************************************)
-Delsplits [split_if];
-Goal
- "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
+Delsplits [split_if];
+
+Goal "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
(* ---------------- main-part ------------------- *)
by (REPEAT (rtac allI 1));
by (rtac imp_conj_lemma 1);
by (induct_tac "a" 1);
(* ----------------- 2 cases ---------------------*)
-by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
+by (ALLGOALS (simp_tac (simpset() delcongs [if_weak_cong]
+ addsimps [externals_def])));
(* fst case --------------------------------------*)
by (rtac impI 1);
by (rtac disjI2 1);
@@ -194,14 +143,14 @@
by (etac reduce_tl 1);
qed"channel_abstraction";
-Goal
- "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
+Addsplits [split_if];
+
+Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
qed"sender_abstraction";
-Goal
- "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
+Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
qed"receiver_abstraction";
@@ -209,52 +158,34 @@
(* 3 thms that do not hold generally! The lucky restriction here is
the absence of internal actions. *)
-Goal
- "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
+Goal "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
-(* start states *)
- (Fast_tac 1)));
(* main-part *)
by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
by (induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
+by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
qed"sender_unchanged";
(* 2 copies of before *)
-Goal
- "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
+Goal "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
- (* start states *)
- (Fast_tac 1)));
(* main-part *)
by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
by (induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
+by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
qed"receiver_unchanged";
-Goal
- "is_weak_ref_map (%id. id) env_ioa env_ioa";
+Goal "is_weak_ref_map (%id. id) env_ioa env_ioa";
by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
-by (TRY(
- (rtac conjI 1) THEN
-(* start states *)
- (Fast_tac 1)));
(* main-part *)
by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
by (induct_tac "a" 1);
(* 7 cases *)
-by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
+by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
qed"env_unchanged";
-Addsplits [split_if];
+
Goal "compatible srch_ioa rsch_ioa";
by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
@@ -335,8 +266,7 @@
(* lemmata about externals of channels *)
-Goal
- "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & \
+Goal "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) & \
\ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
by (simp_tac (simpset() addsimps [externals_def]) 1);
val ext_single_ch = result();
@@ -363,8 +293,7 @@
(* FIX: this proof should be done with compositionality on trace level, not on
weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA
-Goal
- "is_weak_ref_map abs system_ioa system_fin_ioa";
+Goal "is_weak_ref_map abs system_ioa system_fin_ioa";
by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
rsch_fin_ioa_def] @ env_ioas @ impl_ioas)