--- a/src/HOL/Arith.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/Arith.ML Fri Oct 23 20:44:34 1998 +0200
@@ -212,10 +212,10 @@
(*needs !!k for add_ac to work*)
Goal "!!k:: nat. [| k<l; m+l = k+n |] ==> m<n";
-by (auto_tac (claset(),
+by (force_tac (claset(),
simpset() delsimps [add_Suc_right]
addsimps [less_iff_Suc_add,
- add_Suc_right RS sym] @ add_ac));
+ add_Suc_right RS sym] @ add_ac) 1);
qed "less_add_eq_less";
--- a/src/HOL/Induct/Multiset.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/Induct/Multiset.ML Fri Oct 23 20:44:34 1998 +0200
@@ -266,8 +266,6 @@
Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
be finite_induct 1;
by(Auto_tac);
-by(asm_full_simp_tac
- (simpset() delsimps [setsum_0] addsimps [setsum_0 RS sym]) 1);
val lemma = result();
Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
--- a/src/HOL/Integ/IntDef.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/Integ/IntDef.ML Fri Oct 23 20:44:34 1998 +0200
@@ -470,7 +470,7 @@
by (asm_full_simp_tac
(simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
-by (auto_tac (claset(), simpset() addsimps add_ac));
+by (ALLGOALS (force_tac (claset(), simpset() addsimps add_ac)));
qed "zless_linear";
Goal "!!w::int. (w ~= z) = (w<z | z<w)";
--- a/src/HOL/Lambda/ListOrder.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/Lambda/ListOrder.ML Fri Oct 23 20:44:34 1998 +0200
@@ -43,6 +43,7 @@
"(ys,xs) : step1 r & vs=us | ys=xs & (vs,us) : step1 r \
\ ==> (ys@vs,xs@us) : step1 r";
by (Auto_tac);
+ by (Blast_tac 1);
by (blast_tac (claset() addIs [append_eq_appendI]) 1);
qed "append_step1I";
--- a/src/HOL/Lex/RegExp2NA.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/Lex/RegExp2NA.ML Fri Oct 23 20:44:34 1998 +0200
@@ -84,13 +84,13 @@
Goal
"!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
by (induct_tac "w" 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
qed_spec_mp "lift_True_over_steps_union";
Goal
"!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
by (induct_tac "w" 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
qed_spec_mp "lift_False_over_steps_union";
AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
@@ -177,7 +177,7 @@
Goal
"!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
by (induct_tac "w" 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
qed_spec_mp "False_steps_conc";
AddIffs [False_steps_conc];
--- a/src/HOL/Lex/RegExp2NAe.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML Fri Oct 23 20:44:34 1998 +0200
@@ -137,13 +137,15 @@
Goal
"!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
by (induct_tac "w" 1);
-by Auto_tac;
+ by Auto_tac;
+by (Force_tac 1);
qed_spec_mp "lift_True_over_steps_union";
Goal
"!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
by (induct_tac "w" 1);
-by Auto_tac;
+ by Auto_tac;
+by (Force_tac 1);
qed_spec_mp "lift_False_over_steps_union";
AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
--- a/src/HOL/List.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/List.ML Fri Oct 23 20:44:34 1998 +0200
@@ -862,8 +862,8 @@
qed_spec_mp "start_le_sum";
Goal "n : set ns ==> n <= foldl op+ 0 ns";
-by (auto_tac (claset() addIs [start_le_sum],
- simpset() addsimps [in_set_conv_decomp]));
+by (force_tac (claset() addIs [start_le_sum],
+ simpset() addsimps [in_set_conv_decomp]) 1);
qed "elem_le_sum";
Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
--- a/src/HOL/Real/PNat.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/Real/PNat.ML Fri Oct 23 20:44:34 1998 +0200
@@ -294,8 +294,8 @@
Goalw [pnat_less_def]
"!! (z1::nat). z1 < z2 ==> ? z3. z1 + Rep_pnat z3 = z2";
by (dtac less_imp_add_positive 1);
-by (auto_tac (claset() addSIs [Abs_pnat_inverse],
- simpset() addsimps [Collect_pnat_gt_0]));
+by (force_tac (claset() addSIs [Abs_pnat_inverse],
+ simpset() addsimps [Collect_pnat_gt_0]) 1);
qed "lemma_less_ex_sum_Rep_pnat";
--- a/src/HOL/UNITY/Client.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/UNITY/Client.ML Fri Oct 23 20:44:34 1998 +0200
@@ -119,10 +119,12 @@
by (Clarify_tac 1);
by (dtac (impOfSubs increasing_length) 1);
by (invariant_tac 1);
-by (Force_tac 1);
+ by (Force_tac 1);
by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
-by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
-by (force_tac (claset(),
+by Auto_tac;
+ by (TRYALL (dtac localTo_imp_equals THEN' atac));
+ by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
+by (force_tac (claset() addD2 ("x",localTo_imp_equals),
simpset() addsimps [increasing_def, Acts_Join, stable_def,
constrains_def]) 1);
val lemma1 = result();
@@ -136,20 +138,27 @@
by (rtac guaranteesI 1);
by (Clarify_tac 1);
by (rtac Stable_transient_reachable_LeadsTo 1);
-by (res_inst_tac [("k", "k")] transient_lemma 2);
-by (rtac stable_imp_Stable 1);
-by (dtac (impOfSubs increasing_length) 1);
-by (force_tac (claset(),
- simpset() addsimps [increasing_def,
+ by (res_inst_tac [("k", "k")] transient_lemma 2);
+ by (rtac stable_imp_Stable 1);
+ by (dtac (impOfSubs increasing_length) 1);
+ by (force_tac (claset(),
+ simpset() addsimps [increasing_def,
stable_def, constrains_def]) 1);
(** LEVEL 7 **)
-(* Invariant (Cli_prg Join G)
- (- {s. k < length (giv s)} Un {s. k < length (rel s)} Un
- {s. length (giv s) = Suc k &
- length (rel s) = k & ask s ! k <= giv s ! k})
+(*
+ 1. !!G. [| Cli_prg Join G : invariant giv_meets_ask;
+ Cli_prg Join G : ask localTo Cli_prg;
+ Cli_prg Join G : increasing giv;
+ Cli_prg Join G : rel localTo Cli_prg |]
+ ==> reachable (Cli_prg Join G)
+ <= - {s. k < length (giv s)} Un {s. k < length (rel s)} Un
+ {s. length (giv s) = Suc k &
+ length (rel s) = k & ask s ! k <= giv s ! k}
+x
*)
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
-by (Blast_tac 1);
+ by (Blast_tac 1);
by (auto_tac (claset() addSDs [invariant_includes_reachable],
simpset() addsimps [giv_meets_ask_def]));
+by (ALLGOALS Force_tac);
qed "client_correct";
--- a/src/HOL/UNITY/Lift.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML Fri Oct 23 20:44:34 1998 +0200
@@ -304,8 +304,8 @@
i.e. the trivial disjunction, leading to an asymmetrical proof.*)
Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
by (asm_simp_tac (simpset() addsimps metric_simps) 1);
-by (auto_tac (claset() delrules [impCE] addEs [impCE],
- simpset() addsimps conj_comms));
+by (force_tac (claset() delrules [impCE] addEs [impCE],
+ simpset() addsimps conj_comms) 1);
qed "E_thm16c";
--- a/src/HOL/UNITY/NSP_Bad.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML Fri Oct 23 20:44:34 1998 +0200
@@ -77,7 +77,7 @@
Goal "s : reachable Nprg ==> (Key (priK A) : parts (spies s)) = (A : bad)";
by (etac reachable.induct 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
qed "Spy_see_priK";
Addsimps [Spy_see_priK];
--- a/src/HOL/UNITY/Reach.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML Fri Oct 23 20:44:34 1998 +0200
@@ -52,6 +52,7 @@
Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
"FP Rprg <= fixedpoint";
by Auto_tac;
+by (dtac bspec 1 THEN atac 1);
by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
by (dtac fun_cong 1);
by Auto_tac;
@@ -77,7 +78,8 @@
by (simp_tac (simpset() addsimps
([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def])) 1);
by Auto_tac;
-by (rtac fun_upd_idem 1);
+ by (ALLGOALS (dtac bspec THEN' atac));
+ by (rtac fun_upd_idem 1);
by (auto_tac (claset(),simpset() addsimps [fun_upd_idem_iff]));
qed "Compl_fixedpoint";
--- a/src/ZF/Integ/Int.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/ZF/Integ/Int.ML Fri Oct 23 20:44:34 1998 +0200
@@ -172,7 +172,7 @@
qed "zmagnitude_int_of";
Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
-by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
+by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1);
qed "zmagnitude_zminus_int_of";
Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
--- a/src/ZF/Resid/Residuals.ML Fri Oct 23 20:36:21 1998 +0200
+++ b/src/ZF/Resid/Residuals.ML Fri Oct 23 20:44:34 1998 +0200
@@ -154,7 +154,7 @@
Goal "u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
by (etac Scomp.induct 1);
-by Auto_tac;
+by (ALLGOALS Force_tac);
qed_spec_mp "residuals_preserve_comp";