corrected auto_tac (applications of unsafe wrappers)
authoroheimb
Fri Oct 23 20:44:34 1998 +0200 (1998-10-23)
changeset 575827a2b36efd95
parent 5757 0ad476dabbc6
child 5759 bf5d9e5b8cdf
corrected auto_tac (applications of unsafe wrappers)
src/HOL/Arith.ML
src/HOL/Induct/Multiset.ML
src/HOL/Integ/IntDef.ML
src/HOL/Lambda/ListOrder.ML
src/HOL/Lex/RegExp2NA.ML
src/HOL/Lex/RegExp2NAe.ML
src/HOL/List.ML
src/HOL/Real/PNat.ML
src/HOL/UNITY/Client.ML
src/HOL/UNITY/Lift.ML
src/HOL/UNITY/NSP_Bad.ML
src/HOL/UNITY/Reach.ML
src/ZF/Integ/Int.ML
src/ZF/Resid/Residuals.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Oct 23 20:36:21 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Oct 23 20:44:34 1998 +0200
     1.3 @@ -212,10 +212,10 @@
     1.4  
     1.5  (*needs !!k for add_ac to work*)
     1.6  Goal "!!k:: nat. [| k<l;  m+l = k+n |] ==> m<n";
     1.7 -by (auto_tac (claset(),
     1.8 +by (force_tac (claset(),
     1.9  	      simpset() delsimps [add_Suc_right]
    1.10  	                addsimps [less_iff_Suc_add,
    1.11 -				  add_Suc_right RS sym] @ add_ac));
    1.12 +				  add_Suc_right RS sym] @ add_ac) 1);
    1.13  qed "less_add_eq_less";
    1.14  
    1.15  
     2.1 --- a/src/HOL/Induct/Multiset.ML	Fri Oct 23 20:36:21 1998 +0200
     2.2 +++ b/src/HOL/Induct/Multiset.ML	Fri Oct 23 20:44:34 1998 +0200
     2.3 @@ -266,8 +266,6 @@
     2.4  Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
     2.5  be finite_induct 1;
     2.6  by(Auto_tac);
     2.7 -by(asm_full_simp_tac
     2.8 -    (simpset() delsimps [setsum_0] addsimps [setsum_0 RS sym]) 1);
     2.9  val lemma = result();
    2.10  
    2.11  Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
     3.1 --- a/src/HOL/Integ/IntDef.ML	Fri Oct 23 20:36:21 1998 +0200
     3.2 +++ b/src/HOL/Integ/IntDef.ML	Fri Oct 23 20:44:34 1998 +0200
     3.3 @@ -470,7 +470,7 @@
     3.4  by (asm_full_simp_tac
     3.5      (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
     3.6  by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
     3.7 -by (auto_tac (claset(), simpset() addsimps add_ac));
     3.8 +by (ALLGOALS (force_tac (claset(), simpset() addsimps add_ac)));
     3.9  qed "zless_linear";
    3.10  
    3.11  Goal "!!w::int. (w ~= z) = (w<z | z<w)";
     4.1 --- a/src/HOL/Lambda/ListOrder.ML	Fri Oct 23 20:36:21 1998 +0200
     4.2 +++ b/src/HOL/Lambda/ListOrder.ML	Fri Oct 23 20:44:34 1998 +0200
     4.3 @@ -43,6 +43,7 @@
     4.4   "(ys,xs) : step1 r & vs=us | ys=xs & (vs,us) : step1 r \
     4.5  \ ==> (ys@vs,xs@us) : step1 r";
     4.6  by (Auto_tac);
     4.7 + by (Blast_tac 1);
     4.8  by (blast_tac (claset() addIs [append_eq_appendI]) 1);
     4.9  qed "append_step1I";
    4.10  
     5.1 --- a/src/HOL/Lex/RegExp2NA.ML	Fri Oct 23 20:36:21 1998 +0200
     5.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Fri Oct 23 20:44:34 1998 +0200
     5.3 @@ -84,13 +84,13 @@
     5.4  Goal
     5.5   "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
     5.6  by (induct_tac "w" 1);
     5.7 -by Auto_tac;
     5.8 +by (ALLGOALS Force_tac);
     5.9  qed_spec_mp "lift_True_over_steps_union";
    5.10  
    5.11  Goal 
    5.12   "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
    5.13  by (induct_tac "w" 1);
    5.14 -by Auto_tac;
    5.15 +by (ALLGOALS Force_tac);
    5.16  qed_spec_mp "lift_False_over_steps_union";
    5.17  
    5.18  AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
    5.19 @@ -177,7 +177,7 @@
    5.20  Goal
    5.21   "!p. (False#p,q): steps (conc L R) w = (? r. q=False#r & (p,r): steps R w)";
    5.22  by (induct_tac "w" 1);
    5.23 -by Auto_tac;
    5.24 +by (ALLGOALS Force_tac);
    5.25  qed_spec_mp "False_steps_conc";
    5.26  AddIffs [False_steps_conc];
    5.27  
     6.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Fri Oct 23 20:36:21 1998 +0200
     6.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Fri Oct 23 20:44:34 1998 +0200
     6.3 @@ -137,13 +137,15 @@
     6.4  Goal
     6.5   "!p. (True#p,q):steps (union L R) w = (? r. q = True # r & (p,r):steps L w)";
     6.6  by (induct_tac "w" 1);
     6.7 -by Auto_tac;
     6.8 + by Auto_tac;
     6.9 +by (Force_tac 1);
    6.10  qed_spec_mp "lift_True_over_steps_union";
    6.11  
    6.12  Goal 
    6.13   "!p. (False#p,q):steps (union L R) w = (? r. q = False#r & (p,r):steps R w)";
    6.14  by (induct_tac "w" 1);
    6.15 -by Auto_tac;
    6.16 + by Auto_tac;
    6.17 +by (Force_tac 1);
    6.18  qed_spec_mp "lift_False_over_steps_union";
    6.19  
    6.20  AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
     7.1 --- a/src/HOL/List.ML	Fri Oct 23 20:36:21 1998 +0200
     7.2 +++ b/src/HOL/List.ML	Fri Oct 23 20:44:34 1998 +0200
     7.3 @@ -862,8 +862,8 @@
     7.4  qed_spec_mp "start_le_sum";
     7.5  
     7.6  Goal "n : set ns ==> n <= foldl op+ 0 ns";
     7.7 -by (auto_tac (claset() addIs [start_le_sum],
     7.8 -             simpset() addsimps [in_set_conv_decomp]));
     7.9 +by (force_tac (claset() addIs [start_le_sum],
    7.10 +              simpset() addsimps [in_set_conv_decomp]) 1);
    7.11  qed "elem_le_sum";
    7.12  
    7.13  Goal "!m. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))";
     8.1 --- a/src/HOL/Real/PNat.ML	Fri Oct 23 20:36:21 1998 +0200
     8.2 +++ b/src/HOL/Real/PNat.ML	Fri Oct 23 20:44:34 1998 +0200
     8.3 @@ -294,8 +294,8 @@
     8.4  Goalw [pnat_less_def]
     8.5       "!! (z1::nat). z1 < z2  ==> ? z3. z1 + Rep_pnat z3 = z2";
     8.6  by (dtac less_imp_add_positive 1);
     8.7 -by (auto_tac (claset() addSIs [Abs_pnat_inverse],
     8.8 -	      simpset() addsimps [Collect_pnat_gt_0]));
     8.9 +by (force_tac (claset() addSIs [Abs_pnat_inverse],
    8.10 +	       simpset() addsimps [Collect_pnat_gt_0]) 1);
    8.11  qed "lemma_less_ex_sum_Rep_pnat";
    8.12  
    8.13  
     9.1 --- a/src/HOL/UNITY/Client.ML	Fri Oct 23 20:36:21 1998 +0200
     9.2 +++ b/src/HOL/UNITY/Client.ML	Fri Oct 23 20:44:34 1998 +0200
     9.3 @@ -119,10 +119,12 @@
     9.4  by (Clarify_tac 1);
     9.5  by (dtac (impOfSubs increasing_length) 1);
     9.6  by (invariant_tac 1);
     9.7 -by (Force_tac 1);
     9.8 + by (Force_tac 1);
     9.9  by (dtac (Acts_Cli_Join_eq RS iffD1) 1);
    9.10 -by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
    9.11 -by (force_tac (claset(),
    9.12 +by Auto_tac;
    9.13 + by (TRYALL (dtac localTo_imp_equals THEN' atac));
    9.14 +     by (auto_tac (claset() addD2 ("x",localTo_imp_equals), simpset()));
    9.15 +by (force_tac (claset() addD2 ("x",localTo_imp_equals),
    9.16  	       simpset() addsimps [increasing_def, Acts_Join, stable_def, 
    9.17  				   constrains_def]) 1);
    9.18  val lemma1 = result();
    9.19 @@ -136,20 +138,27 @@
    9.20  by (rtac guaranteesI 1);
    9.21  by (Clarify_tac 1);
    9.22  by (rtac Stable_transient_reachable_LeadsTo 1);
    9.23 -by (res_inst_tac [("k", "k")] transient_lemma 2);
    9.24 -by (rtac stable_imp_Stable 1);
    9.25 -by (dtac (impOfSubs increasing_length) 1);
    9.26 -by (force_tac (claset(),
    9.27 -	       simpset() addsimps [increasing_def, 
    9.28 +  by (res_inst_tac [("k", "k")] transient_lemma 2);
    9.29 + by (rtac stable_imp_Stable 1);
    9.30 + by (dtac (impOfSubs increasing_length) 1);
    9.31 + by (force_tac (claset(),
    9.32 + 	        simpset() addsimps [increasing_def, 
    9.33  				   stable_def, constrains_def]) 1);
    9.34  (** LEVEL 7 **)
    9.35 -(*         Invariant (Cli_prg Join G)
    9.36 -              (- {s. k < length (giv s)} Un {s. k < length (rel s)} Un
    9.37 -               {s. length (giv s) = Suc k &
    9.38 -                   length (rel s) = k & ask s ! k <= giv s ! k})
    9.39 +(*
    9.40 + 1. !!G. [| Cli_prg Join G : invariant giv_meets_ask;
    9.41 +            Cli_prg Join G : ask localTo Cli_prg;
    9.42 +            Cli_prg Join G : increasing giv;
    9.43 +            Cli_prg Join G : rel localTo Cli_prg |]
    9.44 +         ==> reachable (Cli_prg Join G)
    9.45 +             <= - {s. k < length (giv s)} Un {s. k < length (rel s)} Un
    9.46 +                {s. length (giv s) = Suc k &
    9.47 +                    length (rel s) = k & ask s ! k <= giv s ! k}
    9.48 +x
    9.49  *)
    9.50  by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
    9.51 -by (Blast_tac 1);
    9.52 + by (Blast_tac 1);
    9.53  by (auto_tac (claset() addSDs [invariant_includes_reachable],
    9.54  	      simpset() addsimps [giv_meets_ask_def]));
    9.55 +by (ALLGOALS Force_tac);
    9.56  qed "client_correct";
    10.1 --- a/src/HOL/UNITY/Lift.ML	Fri Oct 23 20:36:21 1998 +0200
    10.2 +++ b/src/HOL/UNITY/Lift.ML	Fri Oct 23 20:44:34 1998 +0200
    10.3 @@ -304,8 +304,8 @@
    10.4    i.e. the trivial disjunction, leading to an asymmetrical proof.*)
    10.5  Goal "#0<N ==> Req n Int {s. metric n s = N} <= goingup Un goingdown";
    10.6  by (asm_simp_tac (simpset() addsimps metric_simps) 1);
    10.7 -by (auto_tac (claset() delrules [impCE] addEs [impCE], 
    10.8 -	      simpset() addsimps conj_comms));
    10.9 +by (force_tac (claset() delrules [impCE] addEs [impCE], 
   10.10 +	      simpset() addsimps conj_comms) 1);
   10.11  qed "E_thm16c";
   10.12  
   10.13  
    11.1 --- a/src/HOL/UNITY/NSP_Bad.ML	Fri Oct 23 20:36:21 1998 +0200
    11.2 +++ b/src/HOL/UNITY/NSP_Bad.ML	Fri Oct 23 20:44:34 1998 +0200
    11.3 @@ -77,7 +77,7 @@
    11.4  
    11.5  Goal "s : reachable Nprg ==> (Key (priK A) : parts (spies s)) = (A : bad)";
    11.6  by (etac reachable.induct 1);
    11.7 -by Auto_tac;
    11.8 +by (ALLGOALS Force_tac);
    11.9  qed "Spy_see_priK";
   11.10  Addsimps [Spy_see_priK];
   11.11  
    12.1 --- a/src/HOL/UNITY/Reach.ML	Fri Oct 23 20:36:21 1998 +0200
    12.2 +++ b/src/HOL/UNITY/Reach.ML	Fri Oct 23 20:44:34 1998 +0200
    12.3 @@ -52,6 +52,7 @@
    12.4  Goalw [FP_def, fixedpoint_def, stable_def, constrains_def, Rprg_def]
    12.5       "FP Rprg <= fixedpoint";
    12.6  by Auto_tac;
    12.7 +by (dtac bspec 1 THEN atac 1);
    12.8  by (asm_full_simp_tac (simpset() addsimps [Image_singleton, image_iff]) 1);
    12.9  by (dtac fun_cong 1);
   12.10  by Auto_tac;
   12.11 @@ -77,7 +78,8 @@
   12.12  by (simp_tac (simpset() addsimps
   12.13  	      ([Compl_FP, UN_UN_flatten, FP_fixedpoint RS sym, Rprg_def])) 1);
   12.14  by Auto_tac;
   12.15 -by (rtac fun_upd_idem 1);
   12.16 + by (ALLGOALS (dtac bspec THEN' atac));
   12.17 + by (rtac fun_upd_idem 1);
   12.18   by (auto_tac (claset(),simpset() addsimps [fun_upd_idem_iff]));
   12.19  qed "Compl_fixedpoint";
   12.20  
    13.1 --- a/src/ZF/Integ/Int.ML	Fri Oct 23 20:36:21 1998 +0200
    13.2 +++ b/src/ZF/Integ/Int.ML	Fri Oct 23 20:44:34 1998 +0200
    13.3 @@ -172,7 +172,7 @@
    13.4  qed "zmagnitude_int_of";
    13.5  
    13.6  Goalw [zmagnitude_def] "n: nat ==> zmagnitude($~ $# n) = n";
    13.7 -by (auto_tac(claset() addDs [not_znegative_imp_zero], simpset()));
    13.8 +by (force_tac(claset() addDs [not_znegative_imp_zero], simpset())1);
    13.9  qed "zmagnitude_zminus_int_of";
   13.10  
   13.11  Addsimps [zmagnitude_int_of, zmagnitude_zminus_int_of];
    14.1 --- a/src/ZF/Resid/Residuals.ML	Fri Oct 23 20:36:21 1998 +0200
    14.2 +++ b/src/ZF/Resid/Residuals.ML	Fri Oct 23 20:44:34 1998 +0200
    14.3 @@ -154,7 +154,7 @@
    14.4  
    14.5  Goal "u~v ==> ALL w. u~w --> v~w --> regular(w) --> (u|>w) ~ (v|>w)";
    14.6  by (etac Scomp.induct 1);
    14.7 -by Auto_tac;
    14.8 +by (ALLGOALS Force_tac);
    14.9  qed_spec_mp "residuals_preserve_comp";
   14.10  
   14.11