--- a/src/HOL/Lambda/ListBeta.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOL/Lambda/ListBeta.ML Mon Sep 21 23:17:28 1998 +0200
@@ -7,16 +7,15 @@
Goal
"v -> v' ==> !rs. v = (Var n)$$rs --> (? ss. rs => ss & v' = (Var n)$$ss)";
by (etac beta.induct 1);
-by (Asm_full_simp_tac 1);
-by (rtac allI 1);
-by (res_inst_tac [("xs","rs")] rev_exhaust 1);
-by (Asm_full_simp_tac 1);
-by (force_tac (claset() addIs [append_step1I],simpset()) 1);
-by (rtac allI 1);
-by (res_inst_tac [("xs","rs")] rev_exhaust 1);
-by (Asm_full_simp_tac 1);
-by (force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
-by (Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (rtac allI 1);
+ by (res_inst_tac [("xs","rs")] rev_exhaust 1);
+ by (Asm_full_simp_tac 1);
+ by (force_tac (claset() addIs [append_step1I],simpset()) 1);
+ by (rtac allI 1);
+ by (res_inst_tac [("xs","rs")] rev_exhaust 1);
+ by (Asm_full_simp_tac 1);
+ by (mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3);
val lemma = result();
Goal "(Var n)$$rs -> v ==> (? ss. rs => ss & v = (Var n)$$ss)";
@@ -52,8 +51,7 @@
by (split_asm_tac [split_if_asm] 1);
by (Asm_full_simp_tac 1);
by (Blast_tac 1);
- by (force_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 1);
-by (Asm_full_simp_tac 1);
+ by (mk_auto_tac (claset() addIs [disjI2 RS append_step1I],simpset()) 0 3);
val lemma = result();
val major::prems =
--- a/src/HOL/Lambda/ListOrder.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOL/Lambda/ListOrder.ML Mon Sep 21 23:17:28 1998 +0200
@@ -43,7 +43,6 @@
"(ys,xs) : step1 r & vs=us | ys=xs & (vs,us) : step1 r \
\ ==> (ys@vs,xs@us) : step1 r";
by (Auto_tac);
-by (Force_tac 1);
by (blast_tac (claset() addIs [append_eq_appendI]) 1);
qed "append_step1I";
--- a/src/HOL/Lex/RegExp2NA.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOL/Lex/RegExp2NA.ML Mon Sep 21 23:17:28 1998 +0200
@@ -235,8 +235,8 @@
\ (? r. (p,r) : steps L u & fin L r & \
\ (? s. (start R,s) : step R a & \
\ (? t. (s,t) : steps R v & q = False#t)))))";
-by(fast_tac (claset() addDs [True_steps_concD]
- addIs [True_True_steps_concI] addss simpset()) 1);
+by(force_tac (claset() addDs [True_steps_concD]
+ addIs [True_True_steps_concI],simpset()) 1);
qed "True_steps_conc";
(** starting from the start **)
@@ -439,7 +439,7 @@
by(Simp_tac 1);
by(Blast_tac 1);
by(Blast_tac 1);
-by(Auto_tac);
+by(Force_tac 1);
qed "accepts_star";
(***** Correctness of r2n *****)
--- a/src/HOL/TLA/Buffer/Buffer.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.ML Mon Sep 21 23:17:28 1998 +0200
@@ -28,7 +28,7 @@
(* Enabling condition for dequeue -- NOT NEEDED *)
Goalw [temp_rewrite Deq_visible]
"!!q. base_var <ic,q,oc> ==> $Enabled (<Deq ic q oc>_<ic,q,oc>) .= ($q .~= .[])";
-by (auto_tac (claset() addSEs [base_enabled,enabledE], simpset() addsimps [Deq_def]));
+by (force_tac (claset() addSEs [base_enabled,enabledE], simpset() addsimps [Deq_def]) 1);
qed "Deq_enabled";
(* For the left-to-right implication, we don't need the base variable stuff *)
--- a/src/HOL/TLA/Buffer/DBuffer.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.ML Mon Sep 21 23:17:28 1998 +0200
@@ -48,8 +48,8 @@
Goal "$Enabled (<DBPass>_<inp,mid,out,q1,q2>) .= ($q1 .~= .[])";
by (rewtac (action_rewrite DBPass_visible));
by (cut_facts_tac [DB_base] 1);
-by (auto_tac (db_css addSEs2 [base_enabled,enabledE]
- addsimps2 [angle_def,DBPass_def,Deq_def]));
+by (force_tac (db_css addSEs2 [base_enabled,enabledE]
+ addsimps2 [angle_def,DBPass_def,Deq_def]) 1);
qed "DBPass_enabled";
@@ -115,5 +115,5 @@
(*** Main theorem ***)
Goalw [DBuffer_def,Buffer_def,IBuffer_def] "DBuffer .-> Buffer inp out";
-by (auto_tac (db_css addSIs2 (map temp_mp [eexI,DBInit,DB_step_simulation RS STL4,DBFair])));
+by (ALLGOALS (force_tac (db_css addSIs2 (map temp_mp [eexI,DBInit,DB_step_simulation RS STL4,DBFair]))));
qed "DBuffer_impl_Buffer";
--- a/src/HOL/TLA/Inc/Inc.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOL/TLA/Inc/Inc.ML Mon Sep 21 23:17:28 1998 +0200
@@ -230,20 +230,19 @@
(* Now assemble the bits and pieces to prove that Psi is fair. *)
-qed_goal "Fair_M1_lemma" Inc.thy
- "[](PsiInv .& [(N1 .| N2)]_<x,y,sem,pc1,pc2>) \
+goal Inc.thy "[](PsiInv .& [(N1 .| N2)]_<x,y,sem,pc1,pc2>) \
\ .& SF(N1)_<x,y,sem,pc1,pc2> .& [] SF(N2)_<x,y,sem,pc1,pc2> \
-\ .-> SF(M1)_<x,y>"
- (fn _ => [res_inst_tac [("B","beta1"),("P","$pc1 .= #b")] SF2 1,
- (* the action premises are simple *)
- SELECT_GOAL (auto_tac (Inc_css addsimps2 [angle_def,M1_def,beta1_def])) 1,
- SELECT_GOAL (auto_tac (Inc_css addsimps2 angle_def::Psi_defs)) 1,
- SELECT_GOAL (auto_tac (Inc_css addSEs2 [action_mp N1_enabled_at_b])) 1,
- (* temporal premise: use previous lemmas and simple TL *)
- auto_tac (Inc_css addSIs2 DmdStable::(map temp_mp [N1_live,Stuck_at_b])
- addEs2 [STL4E]
- addsimps2 [square_def])
- ]);
+\ .-> SF(M1)_<x,y>";
+by (res_inst_tac [("B","beta1"),("P","$pc1 .= #b")] SF2 1);
+
+(* the action premises are simple *)
+ by (force_tac (Inc_css addsimps2 [angle_def,M1_def,beta1_def]) 1);
+ by (force_tac (Inc_css addsimps2 angle_def::Psi_defs) 1);
+ by (force_tac (Inc_css addSEs2 [action_mp N1_enabled_at_b]) 1);
+(* temporal premise: use previous lemmas and simple TL *)
+by (force_tac (Inc_css addSIs2 DmdStable::(map temp_mp [N1_live,Stuck_at_b])
+ addEs2 [STL4E] addsimps2 [square_def]) 1);
+qed "Fair_M1_lemma";
qed_goal "Fair_M1" Inc.thy "Psi .-> WF(M1)_<x,y>"
(fn _ => [auto_tac (Inc_css addSIs2 SFImplWF::(map temp_mp [Fair_M1_lemma, PsiInv])
--- a/src/HOL/TLA/Memory/Memory.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOL/TLA/Memory/Memory.ML Mon Sep 21 23:17:28 1998 +0200
@@ -26,8 +26,8 @@
(* 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])]);
+ (K [force_tac (temp_css addsimps2 ([square_def,UNext_def] @
+ RM_temp_defs @ UM_temp_defs) addSEs2 [STL4E]) 1]);
(* The memory spec implies the memory invariant *)
qed_goal "MemoryInvariant" Memory.thy
@@ -129,11 +129,9 @@
"($(rs@p) .= #NotAResult) .& (RALL l. $(MemInv mm l)) \
\ .& $(Enabled (Read ch mm rs p .| (REX l. Write ch mm rs p l))) \
\ .-> $(Enabled (<RNext ch mm rs p>_<rtrner ch @ p, rs@p>))"
- (fn _ => [auto_tac
- (action_css addsimps2 [RNext_def,angle_def]
- addSEs2 [enabled_mono2]
- addEs2[action_conjimpE ReadResult,action_impE WriteResult])
- ]);
+ (K [force_tac (action_css addsimps2 [RNext_def,angle_def]
+ addSEs2 [enabled_mono2]
+ addEs2[action_conjimpE ReadResult,action_impE WriteResult]) 1]);
(* Combine previous lemmas: the memory can make a visible step if there is an
--- a/src/HOL/TLA/TLA.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOL/TLA/TLA.ML Mon Sep 21 23:17:28 1998 +0200
@@ -464,9 +464,8 @@
(* Generalization of INV1 *)
qed_goalw "StableBox" TLA.thy [stable_def]
"!!sigma. (sigma |= stable P) ==> (sigma |= [](Init P .-> []P))"
- (fn _ => [etac dup_boxE 1,
- auto_tac (temp_css addsimps2 [stable_def] addEs2 [STL4E, INV1I])
- ]);
+ (K [etac dup_boxE 1,
+ force_tac (temp_css addsimps2 [stable_def] addEs2 [STL4E, INV1I]) 1]);
(* useful for WF2 / SF2 *)
qed_goal "DmdStable" TLA.thy
@@ -616,10 +615,9 @@
*)
qed_goalw "leadsto_SF" TLA.thy [SF_def]
"!!sigma. (sigma |= $(Enabled(<A>_v)) ~> <A>_v) ==> sigma |= SF(A)_v"
- (fn _ => [step_tac temp_cs 1,
+ (K [REPEAT(step_tac temp_cs 1),
rtac leadsto_infinite 1,
- ALLGOALS atac
- ]);
+ ALLGOALS atac]);
bind_thm("leadsto_WF", leadsto_SF RS SFImplWF);
--- a/src/HOLCF/IMP/Denotational.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.ML Mon Sep 21 23:17:28 1998 +0200
@@ -31,8 +31,8 @@
Goal "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
by (induct_tac "c" 1);
by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
- by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
- by (fast_tac ((HOL_cs addSIs evalc.intrs) addss simpset()) 1);
+ by (Force_tac 1);
+ by (Force_tac 1);
by (Simp_tac 1);
by (fast_tac ((HOL_cs addIs evalc.intrs) addss simpset()) 1);
by (Simp_tac 1);
--- a/src/Provers/clasimp.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/Provers/clasimp.ML Mon Sep 21 23:17:28 1998 +0200
@@ -85,7 +85,7 @@
fun cs addSss ss = cs addSaltern ("safe_asm_full_simp_tac",
CHANGED o Simplifier.safe_asm_full_simp_tac ss);
fun cs addss ss = cs addbefore ("asm_full_simp_tac",
- Simplifier.asm_full_simp_tac ss);
+ CHANGED o Simplifier.asm_full_simp_tac ss);
(* tacticals *)
@@ -108,17 +108,15 @@
(* a variant of depth_tac that avoids interference of the simplifier
with dup_step_tac when they are combined by auto_tac *)
-fun nodup_depth_tac cs m i state =
- SELECT_GOAL
- (Classical.appWrappers cs
- (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
- (Classical.safe_step_tac cs i)) THEN_ELSE
- (DEPTH_SOLVE (nodup_depth_tac cs m i),
- Classical.inst0_step_tac cs i APPEND
- COND (K(m=0)) no_tac
- ((Classical.instp_step_tac cs i APPEND Classical.step_tac cs i)
- THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i)))) 1)
- i state;
+fun nodup_depth_tac cs m i state = CHANGED (SELECT_GOAL
+ (REPEAT_DETERM1 (COND (has_fewer_prems 1) no_tac
+ (Classical.safe_step_tac cs 1))
+ THEN_ELSE (DEPTH_SOLVE (nodup_depth_tac cs m 1),
+ Classical.appWrappers cs (fn i => Classical.inst0_step_tac cs i APPEND
+ COND (K(m=0)) no_tac
+ ((Classical.instp_step_tac cs i APPEND Classical.step_tac cs i)
+ THEN DEPTH_SOLVE (nodup_depth_tac cs (m-1) i))) 1))
+ i) state;
(*Designed to be idempotent, except if best_tac instantiates variables
in some of the subgoals*)
@@ -129,7 +127,7 @@
ORELSE'
nodup_depth_tac cs' n; (*slower but more general*)
in EVERY [ALLGOALS (Simplifier.asm_full_simp_tac ss),
- TRY (Classical.safe_tac cs'),
+ TRY (Classical.safe_tac cs),
REPEAT (FIRSTGOAL maintac),
TRY (Classical.safe_tac (cs addSss ss)),
prune_params_tac]
--- a/src/ZF/Perm.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/ZF/Perm.ML Mon Sep 21 23:17:28 1998 +0200
@@ -544,8 +544,8 @@
Goalw [inj_def]
"[| f: inj(A,B); a~:A; b~:B |] ==> \
\ cons(<a,b>,f) : inj(cons(a,A), cons(b,B))";
-by (fast_tac (claset() addIs [apply_type]
- addss (simpset() addsimps [fun_extend, fun_extend_apply2,
- fun_extend_apply1])) 1);
+by (force_tac (claset() addIs [apply_type],
+ simpset() addsimps [fun_extend, fun_extend_apply2,
+ fun_extend_apply1]) 1);
qed "inj_extend";
--- a/src/ZF/ex/Integ.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/ZF/ex/Integ.ML Mon Sep 21 23:17:28 1998 +0200
@@ -144,8 +144,7 @@
by Safe_tac;
by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
-by (fast_tac (claset() addss
- (simpset() addsimps [add_le_self2 RS le_imp_not_lt])) 1);
+by (force_tac (claset(), simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
qed "not_znegative_znat";
Addsimps [not_znegative_znat];
--- a/src/ZF/ex/Limit.ML Mon Sep 21 23:16:25 1998 +0200
+++ b/src/ZF/ex/Limit.ML Mon Sep 21 23:17:28 1998 +0200
@@ -860,9 +860,9 @@
by (Asm_full_simp_tac 3);
by (rtac matrix_chainI 1);
by (Asm_simp_tac 1);
-by (Asm_simp_tac 2);
-by (fast_tac (claset() addDs [chain_in RS cf_cont,
- chain_cf RSN(2,cont_chain)]
+by (Asm_simp_tac 2);
+by (dtac (chain_in RS cf_cont) 1 THEN atac 1);
+by (fast_tac (claset() addDs [chain_cf RSN(2,cont_chain)]
addss simpset()) 1);
by (rtac chain_cf 1);
by (REPEAT (ares_tac [cont_fun RS apply_type, chain_in RS cf_cont,