--- 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".
--- 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<n then ex1 i \
\ else (if i=n then Some a else None), \
\ %i. if i<Suc n then ex2 i else t)")] bexI 1);
- by (res_inst_tac [("x","Suc(n)")] exI 1);
+ by (res_inst_tac [("x","Suc n")] exI 1);
by (Simp_tac 1);
by (Asm_full_simp_tac 1);
- by (REPEAT(rtac allI 1));
+ by (rtac allI 1);
by (res_inst_tac [("m","na"),("n","n")] (make_elim less_linear) 1);
by (etac disjE 1);
by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
@@ -78,8 +79,8 @@
\ !!s t a. [|reachable A s; P(s)|] ==> (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);
--- 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);
--- 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];
--- 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 <rtrner ch @ p, rs@p> ==> \
\ $(Calling ch p) .& ($(rs@p) .~= #NotAResult) \
\ .-> $(Enabled (<MemReturn ch rs p>_<rtrner ch @ p, rs@p>))"
- (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 <rtrner ch @ p, mm@l, rs@p>) ==> \
-\ ($(rs@p) .= #NotAResult) .& $(Calling ch p) .& (RALL l. $(MemInv mm l)) \
-\ .-> $(Enabled (<RNext ch mm rs p>_<rtrner ch @ p, rs@p>))"
- (fn _ => [auto_tac (action_css addsimps2 [enabled_disj]
+"!!p. (ALL l. base_var <rtrner ch @ p, mm@l, rs@p>) ==> \
+\ ($(rs@p) .= #NotAResult) .& $(Calling ch p) .& (RALL l. $(MemInv mm l)) \
+\ .-> $(Enabled (<RNext ch mm rs p>_<rtrner ch @ p, rs@p>))" (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 ]);