# HG changeset patch
# User oheimb
# Date 909168274 -7200
# Node ID 27a2b36efd95011709cf31627e75590d6143799d
# Parent  0ad476dabbc6073870e73c0f9d09f276bf135d59
corrected auto_tac (applications of unsafe wrappers)

diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/Arith.ML
--- 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";
 
 
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/Induct/Multiset.ML
--- 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";
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/Integ/IntDef.ML
--- 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)";
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/Lambda/ListOrder.ML
--- 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";
 
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/Lex/RegExp2NA.ML
--- 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];
 
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/Lex/RegExp2NAe.ML
--- 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];
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/List.ML
--- 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))";
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/Real/PNat.ML
--- 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";
 
 
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/UNITY/Client.ML
--- 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";
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/UNITY/Lift.ML
--- 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";
 
 
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/UNITY/NSP_Bad.ML
--- 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];
 
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/HOL/UNITY/Reach.ML
--- 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";
 
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/ZF/Integ/Int.ML
--- 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];
diff -r 0ad476dabbc6 -r 27a2b36efd95 src/ZF/Resid/Residuals.ML
--- 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";