# HG changeset patch # User paulson # Date 931434151 -7200 # Node ID 4957978b6f9e00336342ec850f3eae8a8d256a1b # Parent 4ab8e31a842152de843848e44afbb03f9b5d97f2 tidied proofs to cope with default if_weak_cong diff -r 4ab8e31a8421 -r 4957978b6f9e src/HOL/IOA/Solve.ML --- a/src/HOL/IOA/Solve.ML Thu Jul 08 13:38:41 1999 +0200 +++ b/src/HOL/IOA/Solve.ML Thu Jul 08 13:42:31 1999 +0200 @@ -73,13 +73,13 @@ \ (fst ex), \ \ %i. fst (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) - by (Simp_tac 1); - by (fast_tac (claset() delSWrapper"split_all_tac")1); + by (Force_tac 1); (* projected execution is indeed an execution *) by (asm_full_simp_tac - (simpset() addsimps [executions_def,is_execution_fragment_def, - par_def,starts_of_def,trans_of_def,filter_oseq_def] - addsplits [option.split]) 1); + (simpset() delcongs [if_weak_cong] + addsimps [executions_def,is_execution_fragment_def, + par_def,starts_of_def,trans_of_def,filter_oseq_def] + addsplits [option.split]) 1); qed"comp1_reachable"; @@ -93,23 +93,25 @@ \ (fst ex), \ \ %i. snd (snd ex i))")] bexI 1); (* fst(s) is in projected execution *) - by (Simp_tac 1); - by (fast_tac (claset() delSWrapper"split_all_tac")1); + by (Force_tac 1); (* projected execution is indeed an execution *) by (asm_full_simp_tac - (simpset() addsimps [executions_def,is_execution_fragment_def, - par_def,starts_of_def,trans_of_def,filter_oseq_def] - addsplits [option.split]) 1); + (simpset() delcongs [if_weak_cong] + addsimps [executions_def,is_execution_fragment_def, + par_def,starts_of_def,trans_of_def,filter_oseq_def] + addsplits [option.split]) 1); qed"comp2_reachable"; -Delsplits [split_if]; +Delsplits [split_if]; Delcongs [if_weak_cong]; -(* Composition of possibility-mappings *) -Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \ -\ externals(asig_of(A1))=externals(asig_of(C1)) &\ -\ is_weak_pmap g C2 A2 & \ -\ externals(asig_of(A2))=externals(asig_of(C2)) & \ -\ compat_ioas C1 C2 & compat_ioas A1 A2 |] \ +(* THIS THEOREM IS NEVER USED (lcp) + Composition of possibility-mappings *) +Goalw [is_weak_pmap_def] + "[| is_weak_pmap f C1 A1; \ +\ externals(asig_of(A1))=externals(asig_of(C1));\ +\ is_weak_pmap g C2 A2; \ +\ externals(asig_of(A2))=externals(asig_of(C2)); \ +\ compat_ioas C1 C2; compat_ioas A1 A2 |] \ \ ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)"; by (rtac conjI 1); (* start_states *) @@ -117,7 +119,6 @@ (* transitions *) by (REPEAT (rtac allI 1)); by (rtac imp_conj_lemma 1); -by (REPEAT(etac conjE 1)); by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1); by (simp_tac (simpset() addsimps [par_def]) 1); by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1); @@ -144,8 +145,8 @@ by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong] addsplits [split_if]) 1); by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN - asm_full_simp_tac(simpset() addsimps[comp1_reachable, - comp2_reachable])1)); + asm_full_simp_tac(simpset() addsimps[comp1_reachable, + comp2_reachable])1)); qed"fxg_is_weak_pmap_of_product_IOA"; @@ -210,3 +211,4 @@ qed"rename_through_pmap"; Addsplits [split_if]; +Addcongs [if_weak_cong]; diff -r 4ab8e31a8421 -r 4957978b6f9e src/HOL/UNITY/Lift.ML --- a/src/HOL/UNITY/Lift.ML Thu Jul 08 13:38:41 1999 +0200 +++ b/src/HOL/UNITY/Lift.ML Thu Jul 08 13:42:31 1999 +0200 @@ -32,8 +32,12 @@ val mov_metric4 = read_instantiate_sg (sign_of thy) [("P", "(?x <= metric ?n ?s)")] rev_mp; +val mov_metric5 = read_instantiate_sg (sign_of thy) + [("P", "?x ~= metric ?n ?s")] rev_mp; + (*The order in which they are applied seems to be critical...*) -val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4]; +val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4, + mov_metric5]; val metric_simps = [metric_def, vimage_def]; @@ -302,12 +306,15 @@ by Auto_tac; qed "E_thm11"; +val metric_tac = REPEAT (FIRSTGOAL (eresolve_tac mov_metrics)) + THEN auto_tac (claset(), simpset() addsimps metric_simps); + (*lem_lift_3_5*) Goal "Lift : (moving Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ \ LeadsTo (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s})"; by (ensures_tac "request_act" 1); -by (auto_tac (claset(), simpset() addsimps metric_simps)); +by metric_tac; qed "E_thm13"; (*lem_lift_3_6*) @@ -316,15 +323,14 @@ \ (stopped Int Req n Int {s. metric n s = N} Int {s. floor s : req s}) \ \ LeadsTo (opened Int Req n Int {s. metric n s = N})"; by (ensures_tac "open_act" 1); -by (REPEAT_FIRST (eresolve_tac mov_metrics)); -by (auto_tac (claset(), simpset() addsimps metric_simps)); +by metric_tac; qed "E_thm14"; (*lem_lift_3_7*) Goal "Lift : (opened Int Req n Int {s. metric n s = N}) \ \ LeadsTo (closed Int Req n Int {s. metric n s = N})"; by (ensures_tac "close_act" 1); -by (auto_tac (claset(), simpset() addsimps metric_simps)); +by metric_tac; qed "E_thm15"; @@ -339,11 +345,10 @@ qed "lift_3_Req"; - (*Now we observe that our integer metric is really a natural number*) Goal "Lift : Always {s. #0 <= metric n s}"; by (rtac (bounded RS Always_weaken) 1); -by (auto_tac (claset(), simpset() addsimps metric_simps)); +by metric_tac; qed "Always_nonneg"; val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken; diff -r 4ab8e31a8421 -r 4957978b6f9e src/HOL/ex/Fib.ML --- a/src/HOL/ex/Fib.ML Thu Jul 08 13:38:41 1999 +0200 +++ b/src/HOL/ex/Fib.ML Thu Jul 08 13:42:31 1999 +0200 @@ -53,8 +53,8 @@ (*Concrete Mathematics, page 278: Cassini's identity*) Goal "fib (Suc (Suc n)) * fib n = \ -\ (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \ -\ else Suc (fib(Suc n) * fib(Suc n)))"; +\ (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \ +\ else Suc (fib(Suc n) * fib(Suc n)))"; by (res_inst_tac [("u","n")] fib.induct 1); by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3); by (stac (read_instantiate [("x", "Suc(Suc ?n)")] fib_Suc_Suc) 3); @@ -63,11 +63,10 @@ by (ALLGOALS (*using [fib_Suc_Suc] here results in a longer proof!*) (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, mod_less, mod_Suc]))); -by (ALLGOALS - (asm_full_simp_tac - (simpset() addsimps add_ac @ mult_ac @ - [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, - mod_less, mod_Suc]))); +by (asm_full_simp_tac + (simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2, + mod_less, mod_Suc]) 2); +by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [fib_Suc_Suc]))); qed "fib_Cassini"; diff -r 4ab8e31a8421 -r 4957978b6f9e src/HOLCF/IOA/ABP/Correctness.ML --- 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) diff -r 4ab8e31a8421 -r 4957978b6f9e src/HOLCF/IOA/NTP/Correctness.ML --- a/src/HOLCF/IOA/NTP/Correctness.ML Thu Jul 08 13:38:41 1999 +0200 +++ b/src/HOLCF/IOA/NTP/Correctness.ML Thu Jul 08 13:42:31 1999 +0200 @@ -64,13 +64,13 @@ Receiver.rbit_def, Receiver.rq_def, Receiver.rsending_def]; - (* Proof of correctness *) Goalw [Spec.ioa_def, is_weak_ref_map_def] "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) \ \ spec_ioa"; -by (simp_tac (simpset() delsplits [split_if] addsimps - [Correctness.hom_def, cancel_restrict, externals_lemma]) 1); +by (simp_tac (simpset() delcongs [if_weak_cong] delsplits [split_if] + addsimps [Correctness.hom_def, cancel_restrict, + externals_lemma]) 1); by (rtac conjI 1); by (simp_tac ss' 1); by (asm_simp_tac (simpset() addsimps sels) 1); @@ -78,25 +78,16 @@ by (rtac imp_conj_lemma 1); (* from lemmas.ML *) by (induct_tac "a" 1); -by (asm_simp_tac (ss' addsplits [split_if]) 1); +by (ALLGOALS (asm_simp_tac ss')); by (forward_tac [inv4] 1); -by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); -by (simp_tac ss' 1); -by (simp_tac ss' 1); -by (simp_tac ss' 1); -by (simp_tac ss' 1); -by (simp_tac ss' 1); -by (simp_tac ss' 1); -by (simp_tac ss' 1); +by (Force_tac 1); -by (asm_simp_tac ss' 1); by (forward_tac [inv4] 1); by (forward_tac [inv2] 1); by (etac disjE 1); by (Asm_simp_tac 1); -by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); +by (Force_tac 1); -by (asm_simp_tac ss' 1); by (forward_tac [inv2] 1); by (etac disjE 1); @@ -104,14 +95,14 @@ by (case_tac "sq(sen(s))=[]" 1); by (asm_full_simp_tac ss' 1); -by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1); +by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); by (case_tac "m = hd(sq(sen(s)))" 1); -by (fast_tac (claset() addss (simpset() addsimps [neq_Nil_conv])) 1); +by (Force_tac 1); by (Asm_full_simp_tac 1); -by (fast_tac (claset() addSDs [add_leD1 RS leD]) 1); +by (blast_tac (claset() addSDs [add_leD1 RS leD]) 1); by (Asm_full_simp_tac 1); qed"ntp_correct"; diff -r 4ab8e31a8421 -r 4957978b6f9e src/HOLCF/IOA/meta_theory/RefMappings.ML --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Jul 08 13:38:41 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Thu Jul 08 13:42:31 1999 +0200 @@ -67,9 +67,10 @@ by (fast_tac (claset() addDs prems) 1); val lemma = result(); -Delsplits [split_if]; -Goal "[| is_weak_ref_map f C A |]\ -\ ==> (is_weak_ref_map f (rename C g) (rename A g))"; +Delsplits [split_if]; Delcongs [if_weak_cong]; + +Goal "[| is_weak_ref_map f C A |] \ +\ ==> (is_weak_ref_map f (rename C g) (rename A g))"; by (asm_full_simp_tac (simpset() addsimps [is_weak_ref_map_def]) 1); by (rtac conjI 1); (* 1: start states *) @@ -104,12 +105,9 @@ by (forward_tac [reachable_rename] 1); by (Asm_full_simp_tac 1); (* x is internal *) -by (simp_tac (simpset() addcongs [conj_cong]) 1); -by (rtac impI 1); -by (etac conjE 1); by (forward_tac [reachable_rename] 1); by Auto_tac; qed"rename_through_pmap"; -Addsplits [split_if]; +Addsplits [split_if]; Addcongs [if_weak_cong];