tidied proofs to cope with default if_weak_cong
authorpaulson
Thu Jul 08 13:42:31 1999 +0200 (1999-07-08)
changeset 69164957978b6f9e
parent 6915 4ab8e31a8421
child 6917 eba301caceea
tidied proofs to cope with default if_weak_cong
src/HOL/IOA/Solve.ML
src/HOL/UNITY/Lift.ML
src/HOL/ex/Fib.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/NTP/Correctness.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
     1.1 --- a/src/HOL/IOA/Solve.ML	Thu Jul 08 13:38:41 1999 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Thu Jul 08 13:42:31 1999 +0200
     1.3 @@ -73,13 +73,13 @@
     1.4  \                (fst ex),                                                \
     1.5  \    %i. fst (snd ex i))")]  bexI 1);
     1.6  (* fst(s) is in projected execution *)
     1.7 - by (Simp_tac 1);
     1.8 - by (fast_tac (claset() delSWrapper"split_all_tac")1);
     1.9 + by (Force_tac 1);
    1.10  (* projected execution is indeed an execution *)
    1.11  by (asm_full_simp_tac
    1.12 -      (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.13 -                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.14 -                addsplits [option.split]) 1);
    1.15 +      (simpset() delcongs [if_weak_cong]
    1.16 +		 addsimps [executions_def,is_execution_fragment_def,
    1.17 +			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.18 +                 addsplits [option.split]) 1);
    1.19  qed"comp1_reachable";
    1.20  
    1.21  
    1.22 @@ -93,23 +93,25 @@
    1.23  \                (fst ex),                                                \
    1.24  \    %i. snd (snd ex i))")]  bexI 1);
    1.25  (* fst(s) is in projected execution *)
    1.26 - by (Simp_tac 1);
    1.27 - by (fast_tac (claset() delSWrapper"split_all_tac")1);
    1.28 + by (Force_tac 1);
    1.29  (* projected execution is indeed an execution *)
    1.30  by (asm_full_simp_tac
    1.31 -      (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.32 -                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.33 -                addsplits [option.split]) 1);
    1.34 +      (simpset() delcongs [if_weak_cong]
    1.35 +		 addsimps [executions_def,is_execution_fragment_def,
    1.36 +			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.37 +                 addsplits [option.split]) 1);
    1.38  qed"comp2_reachable";
    1.39  
    1.40 -Delsplits [split_if];
    1.41 +Delsplits [split_if]; Delcongs [if_weak_cong];
    1.42  
    1.43 -(* Composition of possibility-mappings *)
    1.44 -Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \
    1.45 -\               externals(asig_of(A1))=externals(asig_of(C1)) &\
    1.46 -\               is_weak_pmap g C2 A2 &  \
    1.47 -\               externals(asig_of(A2))=externals(asig_of(C2)) & \
    1.48 -\               compat_ioas C1 C2 & compat_ioas A1 A2  |]     \
    1.49 +(* THIS THEOREM IS NEVER USED (lcp)
    1.50 +   Composition of possibility-mappings *)
    1.51 +Goalw [is_weak_pmap_def]
    1.52 +     "[| is_weak_pmap f C1 A1; \
    1.53 +\        externals(asig_of(A1))=externals(asig_of(C1));\
    1.54 +\        is_weak_pmap g C2 A2;  \
    1.55 +\        externals(asig_of(A2))=externals(asig_of(C2)); \
    1.56 +\        compat_ioas C1 C2; compat_ioas A1 A2  |]     \
    1.57  \  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
    1.58   by (rtac conjI 1);
    1.59  (* start_states *)
    1.60 @@ -117,7 +119,6 @@
    1.61  (* transitions *)
    1.62  by (REPEAT (rtac allI 1));
    1.63  by (rtac imp_conj_lemma 1);
    1.64 -by (REPEAT(etac conjE 1));
    1.65  by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
    1.66  by (simp_tac (simpset() addsimps [par_def]) 1);
    1.67  by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
    1.68 @@ -144,8 +145,8 @@
    1.69  by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
    1.70                   addsplits [split_if]) 1);
    1.71  by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    1.72 -        asm_full_simp_tac(simpset() addsimps[comp1_reachable,
    1.73 -                                      comp2_reachable])1));
    1.74 +	   asm_full_simp_tac(simpset() addsimps[comp1_reachable,
    1.75 +						comp2_reachable])1));
    1.76  qed"fxg_is_weak_pmap_of_product_IOA";
    1.77  
    1.78  
    1.79 @@ -210,3 +211,4 @@
    1.80  qed"rename_through_pmap";
    1.81  
    1.82  Addsplits [split_if];
    1.83 +Addcongs  [if_weak_cong];
     2.1 --- a/src/HOL/UNITY/Lift.ML	Thu Jul 08 13:38:41 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Lift.ML	Thu Jul 08 13:42:31 1999 +0200
     2.3 @@ -32,8 +32,12 @@
     2.4  val mov_metric4 = read_instantiate_sg (sign_of thy) 
     2.5                     [("P", "(?x <= metric ?n ?s)")] rev_mp;
     2.6  
     2.7 +val mov_metric5 = read_instantiate_sg (sign_of thy) 
     2.8 +                   [("P", "?x ~= metric ?n ?s")] rev_mp;
     2.9 +
    2.10  (*The order in which they are applied seems to be critical...*)
    2.11 -val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4];
    2.12 +val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4,
    2.13 +		   mov_metric5];
    2.14  
    2.15  val metric_simps = [metric_def, vimage_def];
    2.16  
    2.17 @@ -302,12 +306,15 @@
    2.18  by Auto_tac;
    2.19  qed "E_thm11";
    2.20  
    2.21 +val metric_tac = REPEAT (FIRSTGOAL (eresolve_tac mov_metrics))
    2.22 +                 THEN auto_tac (claset(), simpset() addsimps metric_simps);
    2.23 +
    2.24  (*lem_lift_3_5*)
    2.25  Goal
    2.26    "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
    2.27  \ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})";
    2.28  by (ensures_tac "request_act" 1);
    2.29 -by (auto_tac (claset(), simpset() addsimps metric_simps));
    2.30 +by metric_tac;
    2.31  qed "E_thm13";
    2.32  
    2.33  (*lem_lift_3_6*)
    2.34 @@ -316,15 +323,14 @@
    2.35  \       (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \
    2.36  \       LeadsTo (opened Int Req n Int {s. metric n s = N})";
    2.37  by (ensures_tac "open_act" 1);
    2.38 -by (REPEAT_FIRST (eresolve_tac mov_metrics));
    2.39 -by (auto_tac (claset(), simpset() addsimps metric_simps));
    2.40 +by metric_tac;
    2.41  qed "E_thm14";
    2.42  
    2.43  (*lem_lift_3_7*)
    2.44  Goal "Lift : (opened Int Req n Int {s. metric n s = N})  \
    2.45  \            LeadsTo (closed Int Req n Int {s. metric n s = N})";
    2.46  by (ensures_tac "close_act" 1);
    2.47 -by (auto_tac (claset(), simpset() addsimps metric_simps));
    2.48 +by metric_tac;
    2.49  qed "E_thm15";
    2.50  
    2.51  
    2.52 @@ -339,11 +345,10 @@
    2.53  qed "lift_3_Req";
    2.54  
    2.55  
    2.56 -
    2.57  (*Now we observe that our integer metric is really a natural number*)
    2.58  Goal "Lift : Always {s. #0 <= metric n s}";
    2.59  by (rtac (bounded RS Always_weaken) 1);
    2.60 -by (auto_tac (claset(), simpset() addsimps metric_simps));
    2.61 +by metric_tac;
    2.62  qed "Always_nonneg";
    2.63  
    2.64  val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken;
     3.1 --- a/src/HOL/ex/Fib.ML	Thu Jul 08 13:38:41 1999 +0200
     3.2 +++ b/src/HOL/ex/Fib.ML	Thu Jul 08 13:42:31 1999 +0200
     3.3 @@ -53,8 +53,8 @@
     3.4  
     3.5  (*Concrete Mathematics, page 278: Cassini's identity*)
     3.6  Goal "fib (Suc (Suc n)) * fib n = \
     3.7 -\              (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \
     3.8 -\                              else Suc (fib(Suc n) * fib(Suc n)))";
     3.9 +\     (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \
    3.10 +\                     else Suc (fib(Suc n) * fib(Suc n)))";
    3.11  by (res_inst_tac [("u","n")] fib.induct 1);
    3.12  by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3);
    3.13  by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3);
    3.14 @@ -63,11 +63,10 @@
    3.15  by (ALLGOALS  (*using [fib_Suc_Suc] here results in a longer proof!*)
    3.16      (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
    3.17  				       mod_less, mod_Suc])));
    3.18 -by (ALLGOALS
    3.19 -    (asm_full_simp_tac
    3.20 -     (simpset() addsimps add_ac @ mult_ac @
    3.21 -			 [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
    3.22 -			  mod_less, mod_Suc])));
    3.23 +by (asm_full_simp_tac
    3.24 +     (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, 
    3.25 +			  mod_less, mod_Suc]) 2);
    3.26 +by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [fib_Suc_Suc])));
    3.27  qed "fib_Cassini";
    3.28  
    3.29  
     4.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Thu Jul 08 13:38:41 1999 +0200
     4.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Thu Jul 08 13:42:31 1999 +0200
     4.3 @@ -33,8 +33,6 @@
     4.4                 asig_projections @ set_lemmas;
     4.5  Addsimps hom_ioas;
     4.6  
     4.7 -Addsimps [reduce_Nil,reduce_Cons];
     4.8 -
     4.9  
    4.10  
    4.11  (* auxiliary function *)
    4.12 @@ -43,70 +41,27 @@
    4.13  (* lemmas about reduce *)
    4.14  
    4.15  Goal "(reduce(l)=[]) = (l=[])";  
    4.16 - by (rtac iffI 1);
    4.17 - by (subgoal_tac "(l~=[]) --> (reduce(l)~=[])" 1);
    4.18 - by (Fast_tac 1); 
    4.19 - by (induct_tac "l" 1);
    4.20 - by (Simp_tac 1);
    4.21 - by (Simp_tac 1);
    4.22 - by (rtac (list.split RS iffD2) 1);
    4.23 - by (Asm_full_simp_tac 1);
    4.24 - by (REPEAT (rtac allI 1)); 
    4.25 - by (rtac impI 1); 
    4.26 - by (hyp_subst_tac 1);
    4.27 - by (stac split_if 1);
    4.28 - by (Asm_full_simp_tac 1);
    4.29 - by (Asm_full_simp_tac 1);
    4.30 +by (induct_tac "l" 1);
    4.31 +by (auto_tac (claset(), simpset() addsplits [list.split]));
    4.32  val l_iff_red_nil = result();
    4.33  
    4.34  Goal "s~=[] --> hd(s)=hd(reduce(s))";
    4.35  by (induct_tac "s" 1);
    4.36 -by (Simp_tac 1);
    4.37 -by (case_tac "list =[]" 1);
    4.38 -by (Asm_full_simp_tac 1);
    4.39 -(* main case *)
    4.40 -by (rotate 1 1);
    4.41 -by (asm_full_simp_tac list_ss 1);
    4.42 -by (Simp_tac 1);
    4.43 -by (rtac (list.split RS iffD2) 1);
    4.44 -by (asm_full_simp_tac list_ss 1);
    4.45 -by (REPEAT (rtac allI 1)); 
    4.46 - by (rtac impI 1); 
    4.47 -by (stac split_if 1);
    4.48 -by (REPEAT(hyp_subst_tac 1));
    4.49 -by (etac subst 1);
    4.50 -by (Simp_tac 1);
    4.51 +by (auto_tac (claset(), simpset() addsplits [list.split]));
    4.52  qed"hd_is_reduce_hd";
    4.53  
    4.54  (* to be used in the following Lemma *)
    4.55  Goal "l~=[] --> reverse(reduce(l))~=[]";
    4.56  by (induct_tac "l" 1);
    4.57 -by (Simp_tac 1);
    4.58 -by (case_tac "list =[]" 1);
    4.59 -by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
    4.60 -(* main case *)
    4.61 -by (rotate 1 1);
    4.62 -by (Asm_full_simp_tac 1);
    4.63 -by (cut_inst_tac [("l","list")] cons_not_nil 1); 
    4.64 -by (Asm_full_simp_tac 1);
    4.65 -by (REPEAT (etac exE 1));
    4.66 -by (Asm_simp_tac 1);
    4.67 -by (stac split_if 1);
    4.68 -by (hyp_subst_tac 1);
    4.69 -by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1); 
    4.70 -qed"rev_red_not_nil";
    4.71 +by (auto_tac (claset(), simpset() addsplits [list.split]));
    4.72 +qed_spec_mp "rev_red_not_nil";
    4.73  
    4.74  (* shows applicability of the induction hypothesis of the following Lemma 1 *)
    4.75 -Goal "!!l.[| l~=[] |] ==>   \
    4.76 -\   hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
    4.77 +Goal "l~=[] ==> hd(reverse(reduce(a#l))) = hd(reverse(reduce(l)))";
    4.78   by (Simp_tac 1);
    4.79 - by (rtac (list.split RS iffD2) 1);
    4.80 - by (asm_full_simp_tac list_ss 1);
    4.81 - by (REPEAT (rtac allI 1)); 
    4.82 - by (rtac impI 1); 
    4.83 - by (stac split_if 1);
    4.84 - by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
    4.85 -                          (rev_red_not_nil RS mp)])  1);
    4.86 + by (asm_full_simp_tac (list_ss addsplits [list.split]
    4.87 +                                addsimps [reverse_Cons,hd_append,
    4.88 +					  rev_red_not_nil])  1);
    4.89  qed"last_ind_on_first";
    4.90  
    4.91  val impl_ss = simpset() delsimps [reduce_Cons];
    4.92 @@ -145,21 +100,14 @@
    4.93  
    4.94  
    4.95  (* Main Lemma 2 for R_pkt in showing that reduce is refinement *)
    4.96 -Goal 
    4.97 -  "!! s. [| s~=[] |] ==>  \
    4.98 +Goal "s~=[] ==>  \
    4.99  \    if hd(s)=hd(tl(s)) & tl(s)~=[] then    \
   4.100  \      reduce(tl(s))=reduce(s) else      \
   4.101  \      reduce(tl(s))=tl(reduce(s))"; 
   4.102  by (cut_inst_tac [("l","s")] cons_not_nil 1);
   4.103  by (Asm_full_simp_tac 1);
   4.104  by (REPEAT (etac exE 1));
   4.105 -by (Asm_full_simp_tac 1);
   4.106 -by (stac split_if 1);
   4.107 -by (rtac conjI 1);
   4.108 -by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
   4.109 -by (Step_tac 1);
   4.110 -by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
   4.111 -by (Auto_tac);
   4.112 +by (auto_tac (claset(), simpset() addsplits [list.split]));
   4.113  val reduce_tl =result();
   4.114  
   4.115  
   4.116 @@ -167,16 +115,17 @@
   4.117            C h a n n e l   A b s t r a c t i o n
   4.118   *******************************************************************)
   4.119  
   4.120 -Delsplits [split_if];
   4.121 -Goal 
   4.122 -      "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
   4.123 +Delsplits [split_if]; 
   4.124 +
   4.125 +Goal "is_weak_ref_map reduce ch_ioa ch_fin_ioa";
   4.126  by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   4.127  (* ---------------- main-part ------------------- *)
   4.128  by (REPEAT (rtac allI 1));
   4.129  by (rtac imp_conj_lemma 1);
   4.130  by (induct_tac "a" 1);
   4.131  (* ----------------- 2 cases ---------------------*)
   4.132 -by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
   4.133 +by (ALLGOALS (simp_tac (simpset() delcongs [if_weak_cong]
   4.134 +				  addsimps [externals_def])));
   4.135  (* fst case --------------------------------------*)
   4.136   by (rtac impI 1);
   4.137   by (rtac disjI2 1);
   4.138 @@ -194,14 +143,14 @@
   4.139  by (etac reduce_tl 1);
   4.140  qed"channel_abstraction";
   4.141  
   4.142 -Goal 
   4.143 -      "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
   4.144 +Addsplits [split_if]; 
   4.145 +
   4.146 +Goal "is_weak_ref_map reduce srch_ioa srch_fin_ioa";
   4.147  by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
   4.148   srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
   4.149  qed"sender_abstraction";
   4.150  
   4.151 -Goal 
   4.152 -      "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
   4.153 +Goal "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa";
   4.154  by (simp_tac (list_ss addsimps [srch_fin_ioa_def,rsch_fin_ioa_def,
   4.155   srch_ioa_def,rsch_ioa_def,rename_through_pmap,channel_abstraction]) 1);
   4.156  qed"receiver_abstraction";
   4.157 @@ -209,52 +158,34 @@
   4.158  
   4.159  (* 3 thms that do not hold generally! The lucky restriction here is 
   4.160     the absence of internal actions. *)
   4.161 -Goal 
   4.162 -      "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
   4.163 +Goal "is_weak_ref_map (%id. id) sender_ioa sender_ioa";
   4.164  by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   4.165 -by (TRY(
   4.166 -   (rtac conjI 1) THEN
   4.167 -(* start states *)
   4.168 -   (Fast_tac 1)));
   4.169  (* main-part *)
   4.170  by (REPEAT (rtac allI 1));
   4.171 -by (rtac imp_conj_lemma 1);
   4.172  by (induct_tac "a" 1);
   4.173  (* 7 cases *)
   4.174 -by (ALLGOALS (simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
   4.175 +by (ALLGOALS (simp_tac (simpset() addsimps [externals_def])));
   4.176  qed"sender_unchanged";
   4.177  
   4.178  (* 2 copies of before *)
   4.179 -Goal 
   4.180 -      "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
   4.181 +Goal "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa";
   4.182  by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   4.183 -by (TRY(
   4.184 -   (rtac conjI 1) THEN
   4.185 - (* start states *)
   4.186 -   (Fast_tac 1)));
   4.187  (* main-part *)
   4.188  by (REPEAT (rtac allI 1));
   4.189 -by (rtac imp_conj_lemma 1);
   4.190  by (induct_tac "a" 1);
   4.191  (* 7 cases *)
   4.192 -by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
   4.193 +by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
   4.194  qed"receiver_unchanged";
   4.195  
   4.196 -Goal 
   4.197 -      "is_weak_ref_map (%id. id) env_ioa env_ioa";
   4.198 +Goal "is_weak_ref_map (%id. id) env_ioa env_ioa";
   4.199  by (simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
   4.200 -by (TRY(
   4.201 -   (rtac conjI 1) THEN
   4.202 -(* start states *)
   4.203 -   (Fast_tac 1)));
   4.204  (* main-part *)
   4.205  by (REPEAT (rtac allI 1));
   4.206 -by (rtac imp_conj_lemma 1);
   4.207  by (induct_tac "a" 1);
   4.208  (* 7 cases *)
   4.209 -by (ALLGOALS(simp_tac (simpset() addsimps [externals_def] addsplits [split_if])));
   4.210 +by (ALLGOALS(simp_tac (simpset() addsimps [externals_def])));
   4.211  qed"env_unchanged";
   4.212 -Addsplits [split_if];
   4.213 +
   4.214  
   4.215  Goal "compatible srch_ioa rsch_ioa"; 
   4.216  by (simp_tac (simpset() addsimps [compatible_def,Int_def,empty_def]) 1);
   4.217 @@ -335,8 +266,7 @@
   4.218  
   4.219  
   4.220  (* lemmata about externals of channels *)
   4.221 -Goal 
   4.222 - "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &  \
   4.223 +Goal "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &  \
   4.224  \ externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))";
   4.225     by (simp_tac (simpset() addsimps [externals_def]) 1);
   4.226  val ext_single_ch = result();
   4.227 @@ -363,8 +293,7 @@
   4.228  (* FIX: this proof should be done with compositionality on trace level, not on 
   4.229          weak_ref_map level, as done here with fxg_is_weak_ref_map_of_product_IOA 
   4.230  
   4.231 -Goal 
   4.232 -     "is_weak_ref_map  abs  system_ioa  system_fin_ioa";
   4.233 +Goal "is_weak_ref_map  abs  system_ioa  system_fin_ioa";
   4.234  
   4.235  by (simp_tac (impl_ss delsimps ([srch_ioa_def, rsch_ioa_def, srch_fin_ioa_def,
   4.236                                   rsch_fin_ioa_def] @ env_ioas @ impl_ioas)
     5.1 --- a/src/HOLCF/IOA/NTP/Correctness.ML	Thu Jul 08 13:38:41 1999 +0200
     5.2 +++ b/src/HOLCF/IOA/NTP/Correctness.ML	Thu Jul 08 13:42:31 1999 +0200
     5.3 @@ -64,13 +64,13 @@
     5.4              Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def];
     5.5  
     5.6  
     5.7 -
     5.8  (* Proof of correctness *)
     5.9  Goalw [Spec.ioa_def, is_weak_ref_map_def]
    5.10    "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig))  \
    5.11  \                  spec_ioa";
    5.12 -by (simp_tac (simpset() delsplits [split_if] addsimps 
    5.13 -    [Correctness.hom_def, cancel_restrict, externals_lemma]) 1);
    5.14 +by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if] 
    5.15 + 	                addsimps [Correctness.hom_def, cancel_restrict, 
    5.16 +				  externals_lemma]) 1);
    5.17  by (rtac conjI 1);
    5.18   by (simp_tac ss' 1);
    5.19   by (asm_simp_tac (simpset() addsimps sels) 1);
    5.20 @@ -78,25 +78,16 @@
    5.21  by (rtac imp_conj_lemma 1);   (* from lemmas.ML *)
    5.22  
    5.23  by (induct_tac "a"  1);
    5.24 -by (asm_simp_tac (ss' addsplits [split_if]) 1);
    5.25 +by (ALLGOALS (asm_simp_tac ss'));
    5.26  by (forward_tac [inv4] 1);
    5.27 -by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
    5.28 -by (simp_tac ss' 1);
    5.29 -by (simp_tac ss' 1);
    5.30 -by (simp_tac ss' 1);
    5.31 -by (simp_tac ss' 1);
    5.32 -by (simp_tac ss' 1);
    5.33 -by (simp_tac ss' 1);
    5.34 -by (simp_tac ss' 1);
    5.35 +by (Force_tac 1);
    5.36  
    5.37 -by (asm_simp_tac ss' 1);
    5.38  by (forward_tac [inv4] 1);
    5.39  by (forward_tac [inv2] 1);
    5.40  by (etac disjE 1);
    5.41  by (Asm_simp_tac 1);
    5.42 -by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
    5.43 +by (Force_tac 1);
    5.44  
    5.45 -by (asm_simp_tac ss' 1);
    5.46  by (forward_tac [inv2] 1);
    5.47  by (etac disjE 1);
    5.48  
    5.49 @@ -104,14 +95,14 @@
    5.50  by (case_tac "sq(sen(s))=[]" 1);
    5.51  
    5.52  by (asm_full_simp_tac ss' 1);
    5.53 -by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
    5.54 +by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1);
    5.55  
    5.56  by (case_tac "m = hd(sq(sen(s)))" 1);
    5.57  
    5.58 -by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1);
    5.59 +by (Force_tac 1);
    5.60  
    5.61  by (Asm_full_simp_tac 1);
    5.62 -by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1);
    5.63 +by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1);
    5.64  
    5.65  by (Asm_full_simp_tac 1);
    5.66  qed"ntp_correct";
     6.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Thu Jul 08 13:38:41 1999 +0200
     6.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Thu Jul 08 13:42:31 1999 +0200
     6.3 @@ -67,9 +67,10 @@
     6.4    by (fast_tac (claset() addDs prems) 1);
     6.5  val lemma = result();
     6.6  
     6.7 -Delsplits [split_if];
     6.8 -Goal "[| is_weak_ref_map f C A |]\
     6.9 -\                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
    6.10 +Delsplits [split_if]; Delcongs [if_weak_cong];
    6.11 +
    6.12 +Goal "[| is_weak_ref_map f C A |] \
    6.13 +\     ==> (is_weak_ref_map f (rename C g) (rename A g))";
    6.14  by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1);
    6.15  by (rtac conjI 1);
    6.16  (* 1: start states *)
    6.17 @@ -104,12 +105,9 @@
    6.18  by (forward_tac  [reachable_rename] 1);
    6.19  by (Asm_full_simp_tac 1);
    6.20  (* x is internal *)
    6.21 -by (simp_tac (simpset() addcongs [conj_cong]) 1);
    6.22 -by (rtac impI 1);
    6.23 -by (etac conjE 1);
    6.24  by (forward_tac  [reachable_rename] 1);
    6.25  by Auto_tac;
    6.26  qed"rename_through_pmap";
    6.27 -Addsplits [split_if];
    6.28 +Addsplits [split_if]; Addcongs [if_weak_cong];
    6.29  
    6.30