# HG changeset patch # User oheimb # Date 893427519 -7200 # Node ID ee3317896a4734ccd5062f5b54ea7a03ba473b89 # Parent a0b8f56ecb9e7473de22e7e4c2f06ad6346b81e1 improved split_all_tac significantly diff -r a0b8f56ecb9e -r ee3317896a47 NEWS --- a/NEWS Fri Apr 24 16:16:29 1998 +0200 +++ b/NEWS Fri Apr 24 16:18:39 1998 +0200 @@ -33,7 +33,9 @@ * added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset() * New directory HOL/UNITY: Chandy and Misra's UNITY formalism -* split_all_tac is now much faster and fails if there is nothing to split +* split_all_tac is now much faster and fails if there is nothing to split. + Existing (fragile) proofs may require adaption because the order and the names + of the automatically generated variables have changed. split_all_tac has moved within claset() from usafe wrappers to safe wrappers, which means that !!-bound variables are splitted much more aggressively. If this splitting is not appropriate, use delSWrapper "split_all_tac". diff -r a0b8f56ecb9e -r ee3317896a47 src/HOL/IOA/IOA.ML --- a/src/HOL/IOA/IOA.ML Fri Apr 24 16:16:29 1998 +0200 +++ b/src/HOL/IOA/IOA.ML Fri Apr 24 16:18:39 1998 +0200 @@ -55,15 +55,16 @@ goalw IOA.thy (reachable_def::exec_rws) "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t"; by (asm_full_simp_tac (simpset() delsimps bex_simps) 1); - by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac))); - by (rename_tac "n ex1 ex2 a1 a4 a5 a2 a3" 1); + by (split_all_tac 1); + by (Safe_tac); + by (rename_tac "ex1 ex2 n" 1); by (res_inst_tac [("x","(%i. if i (s,a,t): trans_of(A) --> P(t) |] \ \ ==> invariant A P"; by (rewrite_goals_tac(reachable_def::Let_def::exec_rws)); - by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac))); - by (rename_tac "n ex1 ex2" 1); + by (Safe_tac); + by (rename_tac "ex1 ex2 n" 1); by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1); by (Asm_full_simp_tac 1); by (nat_ind_tac "n" 1); diff -r a0b8f56ecb9e -r ee3317896a47 src/HOL/IOA/Solve.ML --- a/src/HOL/IOA/Solve.ML Fri Apr 24 16:16:29 1998 +0200 +++ b/src/HOL/IOA/Solve.ML Fri Apr 24 16:18:39 1998 +0200 @@ -15,8 +15,8 @@ \ is_weak_pmap f C A |] ==> traces(C) <= traces(A)"; by (simp_tac(simpset() addsimps [has_trace_def])1); - by (safe_tac (claset() addSaltern ("split_all_tac", split_all_tac))); - by (rename_tac "f ex1 ex2" 1); + by (Safe_tac); + by (rename_tac "ex1 ex2" 1); (* choose same trace, therefore same NF *) by (res_inst_tac[("x","mk_trace C ex1")] exI 1); diff -r a0b8f56ecb9e -r ee3317896a47 src/HOL/Prod.ML --- a/src/HOL/Prod.ML Fri Apr 24 16:16:29 1998 +0200 +++ b/src/HOL/Prod.ML Fri Apr 24 16:18:39 1998 +0200 @@ -57,66 +57,55 @@ fun pair_tac s = EVERY' [res_inst_tac [("p",s)] PairE, hyp_subst_tac, K prune_params_tac]; +(* Do not add as rewrite rule: invalidates some proofs in IMP *) +goal Prod.thy "p = (fst(p),snd(p))"; +by (pair_tac "p" 1); +by (Asm_simp_tac 1); +qed "surjective_pairing"; + +val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [ + rtac exI 1, rtac exI 1, rtac surjective_pairing 1]); +Addsimps [surj_pair]; + +(* lemmas for splitting paired `!!' *) +local + val lemma1 = prove_goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))" + (fn prems => [resolve_tac prems 1]); + + val psig = sign_of Prod.thy; + val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop"; + val PeqP = reflexive(read_cterm psig ("P", pT)); + val psplit = zero_var_indexes(read_instantiate [("p","x")] + surjective_pairing RS eq_reflection); + val adhoc = combination PeqP psplit; + val lemma = prove_goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x" + (fn prems => [rewtac adhoc, resolve_tac prems 1]); + val lemma2 = prove_goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)" + (fn prems => [rtac lemma 1, resolve_tac prems 1]); +in + val split_paired_all = equal_intr lemma1 lemma2 +end; +bind_thm("split_paired_all", split_paired_all); +(* +Addsimps [split_paired_all] does not work with simplifier +because it also affects premises in congrence rules, +where is can lead to premises of the form !!a b. ... = ?P(a,b) +which cannot be solved by reflexivity. +*) + (* replace parameters of product type by individual component parameters *) local fun is_pair (_,Type("*",_)) = true | is_pair _ = false; - fun ptac x = res_inst_tac [("p",x)] PairE; - fun find_pair_params prem = - let val params = Logic.strip_params prem - in if exists is_pair params - then let val params = rev(rename_wrt_term prem params) - (*as they are printed*) - in filter is_pair params end - else [] - end; + fun exists_paired_all prem = exists is_pair (Logic.strip_params prem); + val split_tac = full_simp_tac (HOL_basic_ss addsimps [split_paired_all]); in -val split_all_tac = REPEAT1 o SUBGOAL (fn (prem,i) => - let val params = find_pair_params prem in - if params = [] then no_tac - else EVERY'[EVERY' (map (ptac o fst) params), - REPEAT o hyp_subst_tac, - K prune_params_tac] i end) +val split_all_tac = SUBGOAL (fn (prem,i) => + if exists_paired_all prem then split_tac i else no_tac); end; -(*claset_ref() := claset() addbefore ("split_all_tac", TRY o split_all_tac);*) - claset_ref() := claset() addSWrapper ("split_all_tac", - fn tac2 => split_all_tac ORELSE' tac2); - -(*** lemmas for splitting paired `!!' -Does not work with simplifier because it also affects premises in -congrence rules, where is can lead to premises of the form -!!a b. ... = ?P(a,b) -which cannot be solved by reflexivity. - -val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))"; -by (rtac prem 1); -val lemma1 = result(); - -local - val psig = sign_of Prod.thy; - val pT = Sign.read_typ (psig, K None) "?'a*?'b=>prop"; - val PeqP = reflexive(read_cterm psig ("P", pT)); - val psplit = zero_var_indexes(read_instantiate [("p","x")] - surjective_pairing RS eq_reflection) -in -val adhoc = combination PeqP psplit -end; - - -val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x"; -by (rewtac adhoc); -by (rtac prem 1); -val lemma = result(); - -val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)"; -by (rtac lemma 1); -by (rtac prem 1); -val lemma2 = result(); - -bind_thm("split_paired_all", equal_intr lemma1 lemma2); -Addsimps [split_paired_all]; -***) +claset_ref() := claset() addSWrapper ("split_all_tac", + fn tac2 => split_all_tac ORELSE' tac2); goal Prod.thy "(!x. P x) = (!a b. P(a,b))"; by (Fast_tac 1); @@ -134,9 +123,14 @@ qed "split"; Addsimps [split]; -goal Prod.thy "(s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; -by (res_inst_tac[("p","s")] PairE 1); -by (res_inst_tac[("p","t")] PairE 1); +goal Prod.thy "split Pair p = p"; +by (pair_tac "p" 1); +by (Simp_tac 1); +qed "split_Pair"; +(*unused: val surjective_pairing2 = split_Pair RS sym;*) + +goal Prod.thy "!!s t. (s=t) = (fst(s)=fst(t) & snd(s)=snd(t))"; +by (split_all_tac 1); by (Asm_simp_tac 1); qed "Pair_fst_snd_eq"; @@ -145,21 +139,6 @@ "p=q ==> split c p = split c q" (fn [prem] => [rtac (prem RS arg_cong) 1]); -(* Do not add as rewrite rule: invalidates some proofs in IMP *) -goal Prod.thy "p = (fst(p),snd(p))"; -by (res_inst_tac [("p","p")] PairE 1); -by (Asm_simp_tac 1); -qed "surjective_pairing"; - -goal Prod.thy "p = split (%x y.(x,y)) p"; -by (res_inst_tac [("p","p")] PairE 1); -by (Asm_simp_tac 1); -qed "surjective_pairing2"; - -val surj_pair = prove_goal Prod.thy "? x y. z = (x, y)" (K [ - rtac exI 1, rtac exI 1, rtac surjective_pairing 1]); -Addsimps [surj_pair]; - qed_goal "split_eta" Prod.thy "(%(x,y). f(x,y)) = f" (K [rtac ext 1, split_all_tac 1, rtac split 1]); @@ -264,13 +243,13 @@ goal Prod.thy "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))"; by (rtac ext 1); -by (res_inst_tac [("p","x")] PairE 1); +by (pair_tac "x" 1); by (Asm_simp_tac 1); qed "prod_fun_compose"; goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)"; by (rtac ext 1); -by (res_inst_tac [("p","z")] PairE 1); +by (pair_tac "z" 1); by (Asm_simp_tac 1); qed "prod_fun_ident"; Addsimps [prod_fun_ident]; diff -r a0b8f56ecb9e -r ee3317896a47 src/HOL/TLA/Memory/Memory.ML --- a/src/HOL/TLA/Memory/Memory.ML Fri Apr 24 16:16:29 1998 +0200 +++ b/src/HOL/TLA/Memory/Memory.ML Fri Apr 24 16:18:39 1998 +0200 @@ -21,39 +21,40 @@ (* Make sure the simpset accepts non-boolean simplifications *) simpset_ref() := simpset() setmksimps ((mksimps mksimps_pairs) o maybe_unlift); -(* -------------------- Proofs -------------------------------------------------- *) +(* -------------------- Proofs ---------------------------------------------- *) (* The reliable memory is an implementation of the unreliable one *) qed_goal "ReliableImplementsUnReliable" Memory.thy "IRSpec ch mm rs .-> IUSpec ch mm rs" - (fn _ => [auto_tac (temp_css addsimps2 ([square_def,UNext_def] @ RM_temp_defs @ UM_temp_defs) - addSEs2 [STL4E]) - ]); + (fn _ => [auto_tac (temp_css addsimps2 ([square_def,UNext_def] @ + RM_temp_defs @ UM_temp_defs) addSEs2 [STL4E])]); (* The memory spec implies the memory invariant *) qed_goal "MemoryInvariant" Memory.thy "(MSpec ch mm rs l) .-> []($(MemInv mm l))" - (fn _ => [ auto_inv_tac (simpset() addsimps RM_temp_defs @ MP_simps @ RM_action_defs) 1 ]); + (fn _ => [ auto_inv_tac (simpset() addsimps RM_temp_defs @ + MP_simps @ RM_action_defs) 1 ]); (* The invariant is trivial for non-locations *) qed_goal "NonMemLocInvariant" Memory.thy ".~ #(MemLoc l) .-> []($MemInv mm l)" - (fn _ => [ auto_tac (temp_css addsimps2 [MemInv_def] addSIs2 [necT RS tempD]) ]); + (K [ auto_tac (temp_css addsimps2 [MemInv_def] addSIs2 [necT RS tempD]) ]); qed_goal "MemoryInvariantAll" Memory.thy "((RALL l. #(MemLoc l) .-> MSpec ch mm rs l)) .-> (RALL l. []($MemInv mm l))" - (fn _ => [step_tac temp_cs 1, - case_tac "MemLoc l" 1, - auto_tac (temp_css addSEs2 (map temp_mp [MemoryInvariant,NonMemLocInvariant])) - ]); + (K [step_tac temp_cs 1, + case_tac "MemLoc l" 1, + auto_tac (temp_css addSEs2 (map temp_mp [MemoryInvariant, + NonMemLocInvariant]))]); -(* The memory engages in an action for process p only if there is an unanswered call from p. +(* The memory engages in an action for process p only if there is an + unanswered call from p. We need this only for the reliable memory. *) qed_goal "Memoryidle" Memory.thy ".~ $(Calling ch p) .-> .~ RNext ch mm rs p" - (fn _ => [ auto_tac (action_css addsimps2 (RM_action_defs @ [Return_def])) ]); + (K [ auto_tac (action_css addsimps2 (RM_action_defs @ [Return_def])) ]); bind_thm("MemoryidleI", action_mp Memoryidle); bind_thm("MemoryidleE", action_impE Memoryidle); @@ -69,8 +70,8 @@ "!!p. base_var ==> \ \ $(Calling ch p) .& ($(rs@p) .~= #NotAResult) \ \ .-> $(Enabled (_))" - (fn _ => [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1, - action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def]) + (K [action_simp_tac (simpset()) [MemReturn_change RSN (2,enabled_mono)] [] 1, + action_simp_tac (simpset() addsimps [MemReturn_def,Return_def,rtrner_def]) [] [base_enabled,Pair_inject] 1 ]); @@ -79,7 +80,7 @@ \ $(Calling ch p) .& (arg[$(ch@p)] .= #(Inl (read,l))) \ \ .-> $(Enabled (ReadInner ch mm rs p l))" (fn _ => [Action_simp_tac 1, - (* unlift before applying case_tac: case_split_thm expects boolean conclusion *) +(* unlift before applying case_tac: case_split_thm expects boolean conclusion *) case_tac "MemLoc l" 1, ALLGOALS (action_simp_tac @@ -94,9 +95,8 @@ \ .-> $(Enabled (WriteInner ch mm rs p l v))" (fn _ => [Action_simp_tac 1, case_tac "MemLoc l & MemVal v" 1, - ALLGOALS - (action_simp_tac - (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def, + ALLGOALS (action_simp_tac + (simpset() addsimps [WriteInner_def,GoodWrite_def,BadWrite_def, WrRequest_def] delsimps [disj_not1]) [] [base_enabled,Pair_inject]) ]); @@ -114,7 +114,7 @@ "(Write ch mm rs p l) .-> (rs@p)$ .~= #NotAResult" (fn _ => [auto_tac (claset(), simpset() addsimps (MP_simps @ - [Write_def,WriteInner_def,GoodWrite_def,BadWrite_def])) + [Write_def,WriteInner_def,GoodWrite_def,BadWrite_def])) ]); qed_goal "ReturnNotReadWrite" Memory.thy @@ -122,7 +122,7 @@ \ .-> .~(Read ch mm rs p) .& (RALL l. .~(Write ch mm rs p l))" (fn _ => [auto_tac (action_css addsimps2 [MemReturn_def] - addSEs2 [action_impE WriteResult,action_conjimpE ReadResult]) + addSEs2 [action_impE WriteResult,action_conjimpE ReadResult]) ]); qed_goal "RWRNext_enabled" Memory.thy @@ -132,7 +132,7 @@ (fn _ => [auto_tac (action_css addsimps2 [RNext_def,angle_def] addSEs2 [enabled_mono2] - addEs2 [action_conjimpE ReadResult,action_impE WriteResult]) + addEs2[action_conjimpE ReadResult,action_impE WriteResult]) ]); @@ -140,21 +140,21 @@ outstanding call for which no result has been produced. *) qed_goal "RNext_enabled" Memory.thy - "!!p. (ALL l. base_var ) ==> \ -\ ($(rs@p) .= #NotAResult) .& $(Calling ch p) .& (RALL l. $(MemInv mm l)) \ -\ .-> $(Enabled (_))" - (fn _ => [auto_tac (action_css addsimps2 [enabled_disj] +"!!p. (ALL l. base_var ) ==> \ +\ ($(rs@p) .= #NotAResult) .& $(Calling ch p) .& (RALL l. $(MemInv mm l)) \ +\ .-> $(Enabled (_))" (K [ + auto_tac (action_css addsimps2 [enabled_disj] addSIs2 [action_mp RWRNext_enabled]), res_inst_tac [("s","arg(ch s p)")] sumE 1, - action_simp_tac (simpset() addsimps [Read_def,enabled_ex,base_pair]) - [action_mp ReadInner_enabled,exI] [] 1, - split_all_tac 1, Rd.induct_tac "xa" 1, + action_simp_tac (simpset()addsimps[Read_def,enabled_ex,base_pair]) + [action_mp ReadInner_enabled,exI] [] 1, + split_all_tac 1, rename_tac "a b" 1, Rd.induct_tac "a" 1, (* introduce a trivial subgoal to solve flex-flex constraint?! *) - subgoal_tac "y = snd(xa,y)" 1, - TRYALL Simp_tac, (* solves "read" case *) + subgoal_tac "b = snd(a,b)" 1, + TRYALL Simp_tac, (* solves "read" case *) etac swap 1, - action_simp_tac (simpset() addsimps [Write_def,enabled_ex,base_pair]) + action_simp_tac (simpset()addsimps[Write_def,enabled_ex,base_pair]) [action_mp WriteInner_enabled,exI] [] 1, - split_all_tac 1, Wr.induct_tac "x" 1, - subgoal_tac "(xa = fst(snd(x,xa,y))) & (y = snd(snd(x,xa,y)))" 1, + split_all_tac 1, rename_tac "a aa b" 1, Wr.induct_tac "a" 1, + subgoal_tac "(aa = fst(snd(a,aa,b))) & (b = snd(snd(a,aa,b)))" 1, ALLGOALS Simp_tac ]);