--- a/src/FOL/simpdata.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/FOL/simpdata.ML Wed Dec 24 10:02:30 1997 +0100
@@ -362,14 +362,25 @@
fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
-fun auto_tac (cs,ss) =
+
+fun mk_auto_tac (cs, ss) m n =
let val cs' = cs addss ss
- in EVERY [TRY (safe_tac cs'),
- REPEAT (FIRSTGOAL (fast_tac cs')),
+ val bdt = Blast.depth_tac cs m;
+ fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s =>
+ (warning ("Blast_tac: " ^ s); Seq.empty);
+ val maintac =
+ blast_depth_tac (*fast but can't use addss*)
+ ORELSE'
+ depth_tac cs' n; (*slower but general*)
+ in EVERY [ALLGOALS (asm_full_simp_tac ss),
+ TRY (safe_tac cs'),
+ REPEAT (FIRSTGOAL maintac),
TRY (safe_tac (cs addSss ss)),
prune_params_tac]
end;
-fun Auto_tac () = auto_tac (claset(), simpset());
+fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
-fun auto () = by (Auto_tac ());
+fun Auto_tac st = auto_tac (claset(), simpset()) st;
+
+fun auto () = by Auto_tac;
--- a/src/HOL/Auth/Event.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/Event.ML Wed Dec 24 10:02:30 1997 +0100
@@ -27,7 +27,7 @@
\ ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
\ (ALL A X. ev = Notes A X --> P(nf A X)))";
by (induct_tac "ev" 1);
-by (Auto_tac());
+by Auto_tac;
qed "expand_event_case";
goal thy "spies (Says A B X # evs) = insert X (spies evs)";
--- a/src/HOL/Auth/Message.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/Message.ML Wed Dec 24 10:02:30 1997 +0100
@@ -20,15 +20,15 @@
(*Equations hold because constructors are injective; cannot prove for all f*)
goal thy "(Friend x : Friend``A) = (x:A)";
-by (Auto_tac());
+by Auto_tac;
qed "Friend_image_eq";
goal thy "(Key x : Key``A) = (x:A)";
-by (Auto_tac());
+by Auto_tac;
qed "Key_image_eq";
goal thy "(Nonce x ~: Key``A)";
-by (Auto_tac());
+by Auto_tac;
qed "Nonce_Key_image_eq";
Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
@@ -90,7 +90,7 @@
goalw thy [keysFor_def]
"keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
-by (Auto_tac());
+by Auto_tac;
qed "keysFor_insert_Crypt";
Addsimps [keysFor_empty, keysFor_Un, keysFor_UN,
@@ -101,7 +101,7 @@
keysFor_UN RS equalityD1 RS subsetD RS UN_E];
goalw thy [keysFor_def] "keysFor (Key``E) = {}";
-by (Auto_tac ());
+by Auto_tac;
qed "keysFor_image_Key";
Addsimps [keysFor_image_Key];
@@ -235,7 +235,7 @@
goal thy "!!H. [| Y: parts (insert X G); X: parts H |] \
\ ==> Y: parts (G Un H)";
by (etac parts_trans 1);
-by (Auto_tac());
+by Auto_tac;
qed "parts_cut";
goal thy "!!H. X: parts H ==> parts (insert X H) = parts H";
@@ -279,7 +279,7 @@
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac parts.induct 1);
-by (Auto_tac());
+by Auto_tac;
by (etac parts.induct 1);
by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
qed "parts_insert_Crypt";
@@ -289,7 +289,7 @@
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac parts.induct 1);
-by (Auto_tac());
+by Auto_tac;
by (etac parts.induct 1);
by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd])));
qed "parts_insert_MPair";
@@ -300,9 +300,9 @@
goal thy "parts (Key``N) = Key``N";
-by (Auto_tac());
+by Auto_tac;
by (etac parts.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed "parts_image_Key";
Addsimps [parts_image_Key];
@@ -359,9 +359,9 @@
Addsimps [parts_analz];
goal thy "analz (parts H) = parts H";
-by (Auto_tac());
+by Auto_tac;
by (etac analz.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed "analz_parts";
Addsimps [analz_parts];
@@ -427,7 +427,7 @@
by (rtac equalityI 1);
by (rtac subsetI 1);
by (etac analz.induct 1);
-by (Auto_tac());
+by Auto_tac;
by (etac analz.induct 1);
by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd])));
qed "analz_insert_MPair";
@@ -450,9 +450,9 @@
goal thy "!!H. Key (invKey K) : analz H ==> \
\ insert (Crypt K X) (analz (insert X H)) <= \
\ analz (insert (Crypt K X) H)";
-by (Auto_tac());
+by Auto_tac;
by (eres_inst_tac [("za","x")] analz.induct 1);
-by (Auto_tac());
+by Auto_tac;
by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
val lemma2 = result();
@@ -484,14 +484,14 @@
\ insert (Crypt K X) (analz (insert X H))";
by (rtac subsetI 1);
by (etac analz.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed "analz_insert_Crypt_subset";
goal thy "analz (Key``N) = Key``N";
-by (Auto_tac());
+by Auto_tac;
by (etac analz.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed "analz_image_Key";
Addsimps [analz_image_Key];
@@ -808,7 +808,7 @@
qed "MPair_eq_HPair";
goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
-by (Auto_tac());
+by Auto_tac;
qed "HPair_eq_MPair";
AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
--- a/src/HOL/Auth/NS_Public.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/NS_Public.ML Wed Dec 24 10:02:30 1997 +0100
@@ -36,7 +36,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
by (etac ns_public.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
@@ -66,7 +66,7 @@
goal thy
"!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
-by (Auto_tac());
+by Auto_tac;
qed "Spy_analz_priK";
Addsimps [Spy_analz_priK];
--- a/src/HOL/Auth/NS_Public_Bad.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/NS_Public_Bad.ML Wed Dec 24 10:02:30 1997 +0100
@@ -33,7 +33,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
by (etac ns_public.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
@@ -286,7 +286,7 @@
(*NS3: unicity of NB identifies A and NA, but not B*)
by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
-by (Auto_tac());
+by Auto_tac;
by (rename_tac "C B' evs3" 1);
(*
--- a/src/HOL/Auth/NS_Shared.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/NS_Shared.ML Wed Dec 24 10:02:30 1997 +0100
@@ -45,7 +45,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
by (etac ns_shared.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
@@ -84,7 +84,7 @@
goal thy
"!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
-by (Auto_tac());
+by Auto_tac;
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
@@ -124,7 +124,7 @@
\ K' = shrK A";
by (etac rev_mp 1);
by (etac ns_shared.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed "Says_Server_message_form";
@@ -193,7 +193,7 @@
by (blast_tac (claset() addSEs partsEs
addDs [impOfSubs parts_insert_subset_Un]) 1);
(*Base, NS4 and NS5*)
-by (Auto_tac());
+by Auto_tac;
result();
--- a/src/HOL/Auth/OtwayRees.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees.ML Wed Dec 24 10:02:30 1997 +0100
@@ -39,7 +39,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
@@ -49,13 +49,13 @@
goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
\ ==> X : analz (spies evs)";
-bd (Says_imp_spies RS analz.Inj) 1;
+by (dtac (Says_imp_spies RS analz.Inj) 1);
by (Blast_tac 1);
qed "OR2_analz_spies";
goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
\ ==> X : analz (spies evs)";
-bd (Says_imp_spies RS analz.Inj) 1;
+by (dtac (Says_imp_spies RS analz.Inj) 1);
by (Blast_tac 1);
qed "OR4_analz_spies";
--- a/src/HOL/Auth/OtwayRees_AN.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_AN.ML Wed Dec 24 10:02:30 1997 +0100
@@ -39,7 +39,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
@@ -49,7 +49,7 @@
goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
\ X : analz (spies evs)";
-bd (Says_imp_spies RS analz.Inj) 1;
+by (dtac (Says_imp_spies RS analz.Inj) 1);
by (Blast_tac 1);
qed "OR4_analz_spies";
--- a/src/HOL/Auth/OtwayRees_Bad.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.ML Wed Dec 24 10:02:30 1997 +0100
@@ -38,7 +38,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
by (etac otway.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
--- a/src/HOL/Auth/Public.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/Public.ML Wed Dec 24 10:02:30 1997 +0100
@@ -38,16 +38,16 @@
(** "Image" equations that hold for injective functions **)
goal thy "(invKey x : invKey``A) = (x:A)";
-by (Auto_tac());
+by Auto_tac;
qed "invKey_image_eq";
(*holds because invKey is injective*)
goal thy "(pubK x : pubK``A) = (x:A)";
-by (Auto_tac());
+by Auto_tac;
qed "pubK_image_eq";
goal thy "(priK x ~: pubK``A)";
-by (Auto_tac());
+by Auto_tac;
qed "priK_pubK_image_eq";
Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
@@ -67,7 +67,7 @@
(*Agents see their own private keys!*)
goal thy "Key (priK A) : initState A";
by (induct_tac "A" 1);
-by (Auto_tac());
+by Auto_tac;
qed "priK_in_initState";
AddIffs [priK_in_initState];
@@ -114,7 +114,7 @@
goal thy "Nonce N ~: parts (initState B)";
by (induct_tac "B" 1);
-by (Auto_tac ());
+by Auto_tac;
qed "Nonce_notin_initState";
AddIffs [Nonce_notin_initState];
--- a/src/HOL/Auth/Recur.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/Recur.ML Wed Dec 24 10:02:30 1997 +0100
@@ -77,7 +77,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
by (etac recur.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
@@ -175,7 +175,7 @@
\ ==> K : range shrK";
by (etac rev_mp 1);
by (etac (respond_imp_responses RS responses.induct) 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "Key_in_keysFor_parts";
@@ -358,7 +358,7 @@
\ ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
by (etac recur.induct 1);
by (etac (respond.induct) 5);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "Says_Server_not";
AddSEs [Says_Server_not RSN (2,rev_notE)];
@@ -479,7 +479,7 @@
\ ==> Hash {|Key (shrK B), M|} : parts H";
by (etac rev_mp 1);
by (etac (respond_imp_responses RS responses.induct) 1);
-by (Auto_tac());
+by Auto_tac;
qed "Hash_in_parts_respond";
(*Only RA1 or RA2 can have caused such a part of a message to appear.
--- a/src/HOL/Auth/Shared.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/Shared.ML Wed Dec 24 10:02:30 1997 +0100
@@ -24,7 +24,7 @@
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
by (induct_tac "C" 1);
-by (Auto_tac ());
+by Auto_tac;
qed "keysFor_parts_initState";
Addsimps [keysFor_parts_initState];
@@ -70,7 +70,7 @@
(*Agents see their own shared keys!*)
goal thy "Key (shrK A) : initState A";
by (induct_tac "A" 1);
-by (Auto_tac());
+by Auto_tac;
qed "shrK_in_initState";
AddIffs [shrK_in_initState];
@@ -97,7 +97,7 @@
goal thy "Nonce N ~: parts (initState B)";
by (induct_tac "B" 1);
-by (Auto_tac ());
+by Auto_tac;
qed "Nonce_notin_initState";
AddIffs [Nonce_notin_initState];
@@ -169,7 +169,7 @@
by (etac exE 1);
by (cut_inst_tac [("evs","evs'")]
(Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
-by (Auto_tac());
+by Auto_tac;
qed "Key_supply2";
goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
--- a/src/HOL/Auth/TLS.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/TLS.ML Wed Dec 24 10:02:30 1997 +0100
@@ -130,7 +130,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
by (etac tls.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
--- a/src/HOL/Auth/WooLam.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/WooLam.ML Wed Dec 24 10:02:30 1997 +0100
@@ -37,7 +37,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs";
by (etac woolam.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
@@ -72,7 +72,7 @@
goal thy
"!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
-by (Auto_tac());
+by Auto_tac;
qed "Spy_analz_shrK";
Addsimps [Spy_analz_shrK];
--- a/src/HOL/Auth/Yahalom.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/Yahalom.ML Wed Dec 24 10:02:30 1997 +0100
@@ -34,7 +34,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
by (etac yahalom.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
--- a/src/HOL/Auth/Yahalom2.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML Wed Dec 24 10:02:30 1997 +0100
@@ -34,7 +34,7 @@
(*Nobody sends themselves messages*)
goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
by (etac yahalom.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "not_Says_to_self";
Addsimps [not_Says_to_self];
AddSEs [not_Says_to_self RSN (2, rev_notE)];
--- a/src/HOL/Divides.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Divides.ML Wed Dec 24 10:02:30 1997 +0100
@@ -244,7 +244,7 @@
goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)";
by (subgoal_tac "m mod 2 < 2" 1);
by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
-by (Auto_tac());
+by Auto_tac;
qed "mod2_gr_0";
Addsimps [mod2_gr_0];
--- a/src/HOL/Finite.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Finite.ML Wed Dec 24 10:02:30 1997 +0100
@@ -192,7 +192,7 @@
by (simp_tac (simpset() addsplits [expand_split]) 1);
by (etac finite_imageI 1);
by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1);
-by (Auto_tac());
+by Auto_tac;
by (rtac bexI 1);
by (assume_tac 2);
by (Simp_tac 1);
--- a/src/HOL/IMP/Denotation.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/IMP/Denotation.ML Wed Dec 24 10:02:30 1997 +0100
@@ -29,7 +29,7 @@
(* start with rule induction *)
by (etac evalc.induct 1);
-by (Auto_tac());
+by Auto_tac;
(* while *)
by (rewtac Gamma_def);
by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
--- a/src/HOL/IMP/Transition.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/IMP/Transition.ML Wed Dec 24 10:02:30 1997 +0100
@@ -193,7 +193,7 @@
goal Transition.thy
"!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
by (etac evalc1.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "FB_lemma3";
val [major] = goal Transition.thy
--- a/src/HOL/IOA/Solve.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/IOA/Solve.ML Wed Dec 24 10:02:30 1997 +0100
@@ -205,5 +205,5 @@
by (rtac impI 1);
by (etac conjE 1);
by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
-by (Auto_tac());
+by Auto_tac;
qed"rename_through_pmap";
--- a/src/HOL/Induct/Exp.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Induct/Exp.ML Wed Dec 24 10:02:30 1997 +0100
@@ -109,7 +109,7 @@
(*This theorem says that "WHILE TRUE DO c" cannot terminate*)
goal thy "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
by (etac exec.induct 1);
-by (Auto_tac());
+by Auto_tac;
bind_thm ("while_true_E", refl RSN (2, result() RS mp));
--- a/src/HOL/Induct/LFilter.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Induct/LFilter.ML Wed Dec 24 10:02:30 1997 +0100
@@ -190,7 +190,7 @@
(*Cases: p x is true or false*)
by (rtac (lfilter_cases RS disjE) 1);
by (etac ssubst 1);
-by (Auto_tac());
+by Auto_tac;
qed "lfilter_idem";
@@ -211,7 +211,7 @@
\ ==> (l, LCons x l') : findRel q --> ~ p x \
\ --> l' : Domain (findRel (%x. p x & q x))";
by (etac findRel.induct 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "findRel_not_conj_Domain";
@@ -229,9 +229,9 @@
by (etac findRel.induct 1);
by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
addIs [findRel_conj]) 1);
-by (Auto_tac());
+by Auto_tac;
by (dtac (sym RS lfilter_eq_LCons) 1);
-by (Auto_tac());
+by Auto_tac;
by (dtac spec 1);
by (dtac (refl RS rev_mp) 1);
by (blast_tac (claset() addIs [findRel_conj2]) 1);
@@ -303,7 +303,7 @@
\ (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
by (stac (lmap_def RS def_llist_corec) 1);
by (res_inst_tac [("l", "l")] llistE 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "lmap_eq_LCons";
--- a/src/HOL/Induct/LList.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Induct/LList.ML Wed Dec 24 10:02:30 1997 +0100
@@ -652,7 +652,7 @@
(*Surprisingly hard to prove. Used with lfilter*)
goalw thy [llistD_Fun_def, prod_fun_def]
"!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
-by (Auto_tac());
+by Auto_tac;
by (rtac image_eqI 1);
by (fast_tac (claset() addss (simpset())) 1);
by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1);
--- a/src/HOL/Induct/Mutil.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Induct/Mutil.ML Wed Dec 24 10:02:30 1997 +0100
@@ -53,7 +53,7 @@
\ {(i, n+n), (i, Suc(n+n))}" 1);
by (Blast_tac 2);
by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
-by (Auto_tac());
+by Auto_tac;
qed "dominoes_tile_row";
goal thy "(below m) Times below(n+n) : tiling domino";
--- a/src/HOL/Integ/Integ.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Integ/Integ.ML Wed Dec 24 10:02:30 1997 +0100
@@ -847,7 +847,7 @@
negative_eq_positive, not_znat_zless_negative];
goalw Integ.thy [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
- by (Auto_tac());
+ by Auto_tac;
qed "znegative_less_0";
goalw Integ.thy [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
@@ -868,7 +868,7 @@
by (dtac zle_imp_zless_or_eq 1);
by (etac disjE 1);
by (dtac zless_eq_zadd_Suc 1);
- by (Auto_tac());
+ by Auto_tac;
qed "not_znegativeD";
(* a case theorem distinguishing positive and negative int *)
--- a/src/HOL/Option.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Option.ML Wed Dec 24 10:02:30 1997 +0100
@@ -8,7 +8,7 @@
open Option;
qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
- (K [option.induct_tac "x" 1, Auto_tac()]);
+ (K [option.induct_tac "x" 1, Auto_tac]);
section "case analysis in premises";
@@ -31,7 +31,7 @@
res_inst_tac [("opt","x")] optionE 1,
forward_tac prems 1,
forward_tac prems 3,
- Auto_tac()]);
+ Auto_tac]);
fun option_case_tac i = EVERY [
etac option_caseE i,
hyp_subst_tac (i+1),
@@ -56,4 +56,4 @@
val option_map_SomeD = prove_goalw thy [option_map_def]
"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
optionE_tac "x" 1,
- Auto_tac()]);
+ Auto_tac]);
--- a/src/HOL/Quot/HQUOT.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Quot/HQUOT.ML Wed Dec 24 10:02:30 1997 +0100
@@ -82,14 +82,14 @@
by (cut_facts_tac prems 1);
by (rtac notI 1);
by (dtac per_class_eqE 1);
-by (Auto_tac());
+by Auto_tac;
qed "per_class_neqI";
val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>";
by (cut_facts_tac prems 1);
by (rtac notI 1);
by (dtac er_class_eqE 1);
-by (Auto_tac());
+by Auto_tac;
qed "er_class_neqI";
val prems = goal thy "<[x]>~=<[y]>==>~x===y";
--- a/src/HOL/Quot/NPAIR.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Quot/NPAIR.ML Wed Dec 24 10:02:30 1997 +0100
@@ -7,13 +7,13 @@
open NPAIR;
goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
-by (Auto_tac());
+by Auto_tac;
qed "rep_abs_NP";
Addsimps [rep_abs_NP];
val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
by (cut_facts_tac prems 1);
-by (Auto_tac());
+by Auto_tac;
qed "per_sym_NP";
--- a/src/HOL/Set.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Set.ML Wed Dec 24 10:02:30 1997 +0100
@@ -470,7 +470,7 @@
(*The order of the premises presupposes that A is rigid; b may be flexible*)
goal Set.thy "!!b. [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))";
-by (Auto_tac());
+by Auto_tac;
qed "UN_I";
val major::prems = goalw Set.thy [UNION_def]
@@ -494,7 +494,7 @@
section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
goalw Set.thy [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
-by (Auto_tac());
+by Auto_tac;
qed "INT_iff";
Addsimps [INT_iff];
@@ -505,7 +505,7 @@
qed "INT_I";
goal Set.thy "!!b. [| b : (INT x:A. B(x)); a:A |] ==> b: B(a)";
-by (Auto_tac());
+by Auto_tac;
qed "INT_D";
(*"Classical" elimination -- by the Excluded Middle on a:A *)
@@ -537,7 +537,7 @@
(*The order of the premises presupposes that C is rigid; A may be flexible*)
goal Set.thy "!!X. [| X:C; A:X |] ==> A : Union(C)";
-by (Auto_tac());
+by Auto_tac;
qed "UnionI";
val major::prems = goalw Set.thy [Union_def]
@@ -566,7 +566,7 @@
(*A "destruct" rule -- every X in C contains A as an element, but
A:X can hold when X:C does not! This rule is analogous to "spec". *)
goal Set.thy "!!X. [| A : Inter(C); X:C |] ==> A:X";
-by (Auto_tac());
+by Auto_tac;
qed "InterD";
(*"Classical" elimination rule -- does not require proving X:C *)
@@ -672,7 +672,7 @@
goalw Set.thy [psubset_def]
"!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
-by (Auto_tac());
+by Auto_tac;
qed "psubset_insertD";
bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
--- a/src/HOL/Subst/Subst.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Subst/Subst.ML Wed Dec 24 10:02:30 1997 +0100
@@ -181,7 +181,7 @@
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff])));
by (Blast_tac 2);
by (safe_tac (claset() addSIs [exI, vars_var_iff RS iffD1 RS sym]));
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp "Var_intro";
goal Subst.thy
--- a/src/HOL/Sum.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/Sum.ML Wed Dec 24 10:02:30 1997 +0100
@@ -149,7 +149,7 @@
goal Sum.thy "R(sum_case f g s) = \
\ ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
by (res_inst_tac [("s","s")] sumE 1);
-by (Auto_tac());
+by Auto_tac;
qed "expand_sum_case";
(*Prevents simplification of f and g: much faster*)
--- a/src/HOL/TLA/Action.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/Action.ML Wed Dec 24 10:02:30 1997 +0100
@@ -219,17 +219,17 @@
qed_goalw "idle_squareI" Action.thy [square_def]
"!!s t. ([[s,t]] |= unchanged v) ==> ([[s,t]] |= [A]_v)"
- (fn _ => [ Auto_tac() ]);
+ (fn _ => [ Auto_tac ]);
qed_goalw "busy_squareI" Action.thy [square_def]
"!!s t. ([[s,t]] |= A) ==> ([[s,t]] |= [A]_v)"
- (fn _ => [ Auto_tac() ]);
+ (fn _ => [ Auto_tac ]);
qed_goalw "square_simulation" Action.thy [square_def]
"[| unchanged f .& .~B .-> unchanged g; \
\ A .& .~unchanged g .-> B \
\ |] ==> [A]_f .-> [B]_g"
- (fn [p1,p2] => [Auto_tac(),
+ (fn [p1,p2] => [Auto_tac,
etac (action_conjimpE p2) 1,
etac swap 3, etac (action_conjimpE p1) 3,
ALLGOALS atac
@@ -237,11 +237,11 @@
qed_goalw "not_square" Action.thy [square_def,angle_def]
"(.~ [A]_v) .= <.~A>_v"
- (fn _ => [ Auto_tac() ]);
+ (fn _ => [ Auto_tac ]);
qed_goalw "not_angle" Action.thy [square_def,angle_def]
"(.~ <A>_v) .= [.~A]_v"
- (fn _ => [ Auto_tac() ]);
+ (fn _ => [ Auto_tac ]);
(* ============================== Facts about ENABLED ============================== *)
@@ -278,22 +278,22 @@
qed_goal "enabled_disj1" Action.thy
"!!s. (Enabled F) s ==> (Enabled (F .| G)) s"
- (fn _ => [etac enabled_mono 1, Auto_tac()
+ (fn _ => [etac enabled_mono 1, Auto_tac
]);
qed_goal "enabled_disj2" Action.thy
"!!s. (Enabled G) s ==> (Enabled (F .| G)) s"
- (fn _ => [etac enabled_mono 1, Auto_tac()
+ (fn _ => [etac enabled_mono 1, Auto_tac
]);
qed_goal "enabled_conj1" Action.thy
"!!s. (Enabled (F .& G)) s ==> (Enabled F) s"
- (fn _ => [etac enabled_mono 1, Auto_tac()
+ (fn _ => [etac enabled_mono 1, Auto_tac
]);
qed_goal "enabled_conj2" Action.thy
"!!s. (Enabled (F .& G)) s ==> (Enabled G) s"
- (fn _ => [etac enabled_mono 1, Auto_tac()
+ (fn _ => [etac enabled_mono 1, Auto_tac
]);
qed_goal "enabled_conjE" Action.thy
--- a/src/HOL/TLA/Buffer/DBuffer.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/Buffer/DBuffer.ML Wed Dec 24 10:02:30 1997 +0100
@@ -37,8 +37,8 @@
goal DBuffer.thy "$Enabled (<DBDeq>_<inp,mid,out,q1,q2>) .= ($q2 .~= .[])";
by (rewtac (action_rewrite DBDeq_visible));
by (cut_facts_tac [DB_base] 1);
-by (auto_tac (db_css addSEs2 [base_enabled,enabledE]
- addsimps2 [angle_def,DBDeq_def,Deq_def]));
+by (old_auto_tac (db_css addSEs2 [base_enabled,enabledE]
+ addsimps2 [angle_def,DBDeq_def,Deq_def]));
qed "DBDeq_enabled";
goal DBuffer.thy "<DBPass>_<inp,mid,out,q1,q2> .= DBPass";
--- a/src/HOL/TLA/Inc/Inc.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/Inc/Inc.ML Wed Dec 24 10:02:30 1997 +0100
@@ -171,7 +171,7 @@
(fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N2_leadsto_a) RSN(2,leadsto_init)]),
rewrite_goals_tac (Init_def::action_rews),
pcount.induct_tac "pc2 (fst_st sigma)" 1,
- Auto_tac()
+ Auto_tac
]);
(* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
@@ -217,7 +217,7 @@
(fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N1_leadsto_b) RSN(2,leadsto_init)]),
rewrite_goals_tac (Init_def::action_rews),
pcount.induct_tac "pc1 (fst_st sigma)" 1,
- Auto_tac()
+ Auto_tac
]);
qed_goal "N1_enabled_at_b" Inc.thy
--- a/src/HOL/TLA/Memory/MIlive.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/Memory/MIlive.ML Wed Dec 24 10:02:30 1997 +0100
@@ -286,7 +286,7 @@
"[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& $(ImpInv rmhist p)) \
\ .& SF(MClkReply memCh crCh cst p)_(c p) .& []<>($(S6 rmhist p)) \
\ .-> []<>($(S1 rmhist p))"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1,
eres_inst_tac [("P","<MClkReply memCh crCh cst p>_(c p)")]
EnsuresInfinite 1, atac 1,
--- a/src/HOL/TLA/Memory/MemoryImplementation.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.ML Wed Dec 24 10:02:30 1997 +0100
@@ -77,7 +77,7 @@
"Init(RALL p. $(ImpInit p)) .& [](RALL p. ImpNext p) \
\ .-> (EEX rmhist. Init(RALL p. $(HInit rmhist p)) \
\ .& [](RALL p. [HNext rmhist p]_<c p, r p, m p, rmhist@p>))"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
rtac historyI 1, TRYALL atac,
action_simp_tac (simpset() addsimps [HInit_def]) [] [] 1,
res_inst_tac [("x","p")] fun_cong 1, atac 1,
@@ -87,7 +87,7 @@
qed_goal "History" MemoryImplementation.thy
"Implementation .-> (EEX rmhist. Hist rmhist)"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
rtac ((temp_mp HistoryLemma) RS eex_mono) 1,
SELECT_GOAL
(auto_tac (MI_css
@@ -609,7 +609,7 @@
action_simp_tac (simpset() addsimps [ImpNext_def])
[] [S4EnvUnchE,S4ClerkUnchE,S4RPCUnchE] 1,
TRYALL (action_simp_tac (simpset() addsimps [square_def]) [] [S4WriteE]),
- Auto_tac()
+ Auto_tac
]);
qed_goal "Step2_2" MemoryImplementation.thy
@@ -664,7 +664,7 @@
(* The main theorem: introduce hiding and eliminate history variable. *)
qed_goal "Implementation" MemoryImplementation.thy
"Implementation .-> USpec memCh"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
forward_tac [temp_mp History] 1,
auto_tac (MI_css addsimps2 [USpec_def]
addIs2 (map temp_mp [eexI, Impl_IUSpec])
--- a/src/HOL/TLA/ROOT.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/ROOT.ML Wed Dec 24 10:02:30 1997 +0100
@@ -14,6 +14,16 @@
reset global_names;
+(*FIXME: the old auto_tac is sometimes needed!*)
+fun old_auto_tac (cs,ss) =
+ let val cs' = cs addss ss
+ in EVERY [TRY (safe_tac cs'),
+ REPEAT (FIRSTGOAL (fast_tac cs')),
+ TRY (safe_tac (cs addSss ss)),
+ prune_params_tac]
+ end;
+
+
use_thy "TLA";
val TLA_build_completed = ();
--- a/src/HOL/TLA/TLA.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/TLA/TLA.ML Wed Dec 24 10:02:30 1997 +0100
@@ -135,7 +135,7 @@
(* ------------------------ STL4 ------------------------------------------- *)
qed_goal "STL4" TLA.thy "(F .-> G) ==> ([]F .-> []G)"
- (fn [prem] => [Auto_tac(),
+ (fn [prem] => [Auto_tac,
rtac ((temp_mp normalT) RS mp) 1,
REPEAT (ares_tac [prem, necT RS tempD] 1)
]);
@@ -163,7 +163,7 @@
(* ------------------------ STL5 ------------------------------------------- *)
qed_goal "STL5" TLA.thy "([]F .& []G) .= ([](F .& G))"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
subgoal_tac "sigma |= [](G .-> (F .& G))" 1,
etac ((temp_mp normalT) RS mp) 1, atac 1,
ALLGOALS (fast_tac (temp_cs addSEs [STL4E]))
@@ -238,7 +238,7 @@
qed_goalw "DmdImpl2" TLA.thy [dmd_def]
"!!sigma. [| (sigma |= <>F); (sigma |= [](F .-> G)) |] ==> (sigma |= <>G)"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
etac notE 1,
merge_box_tac 1,
fast_tac (temp_cs addSEs [STL4E]) 1
@@ -256,7 +256,7 @@
(* ------------------------ STL6 ------------------------------------------- *)
(* Used in the proof of STL6, but useful in itself. *)
qed_goalw "BoxDmdT" TLA.thy [dmd_def] "[]F .& <>G .-> <>([]F .& G)"
- (fn _ => [ Auto_tac(),
+ (fn _ => [ Auto_tac,
etac dup_boxE 1,
merge_box_tac 1,
etac swap 1,
@@ -265,7 +265,7 @@
(* weaker than BoxDmd, but more polymorphic (and often just right) *)
qed_goalw "BoxDmdT2" TLA.thy [dmd_def] "<>F .& []G .-> <>(F .& G)"
- (fn _ => [ Auto_tac(),
+ (fn _ => [ Auto_tac,
merge_box_tac 1,
fast_tac (temp_cs addSEs [notE,STL4E]) 1
]);
@@ -278,7 +278,7 @@
etac DmdImplE 1, rtac BoxDmdT 1,
(* the second subgoal needs commutativity of .&, which complicates the proof *)
etac DmdImplE 1,
- Auto_tac(),
+ Auto_tac,
etac (temp_conjimpE BoxDmdT) 1, atac 1, etac thin_rl 1,
fast_tac (temp_cs addSEs [DmdImplE]) 1
]);
@@ -347,10 +347,10 @@
section "Further rewrites";
qed_goalw "NotBox" TLA.thy [dmd_def] "(.~[]F) .= (<>.~F)"
- (fn _ => [ Auto_tac() ]);
+ (fn _ => [ Auto_tac ]);
qed_goalw "NotDmd" TLA.thy [dmd_def] "(.~<>F) .= ([].~F)"
- (fn _ => [ Auto_tac () ]);
+ (fn _ => [ Auto_tac ]);
(* These are not by default included in temp_css, because they could be harmful,
e.g. []F .& .~[]F becomes []F .& <>.~F !! *)
@@ -363,7 +363,7 @@
rtac ccontr 1,
subgoal_tac "sigma |= <>[][]F .& <>[].~[]F" 1,
etac thin_rl 1,
- Auto_tac(),
+ Auto_tac,
etac (temp_conjimpE STL6) 1, atac 1,
Asm_full_simp_tac 1,
ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps))
@@ -382,18 +382,19 @@
(fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]);
qed_goal "DBImplBD" TLA.thy "<>[](F::temporal) .-> []<>F"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
rtac ccontr 1,
- auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
+ old_auto_tac (temp_css addsimps2 more_temp_simps
+ addEs2 [temp_conjimpE STL6])
]);
(* Although the script is the same, the derivation isn't polymorphic and doesn't
work for other types of formulas (uses STL2).
*)
qed_goal "DBImplBDAct" TLA.thy "<>[](A::action) .-> []<>A"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
rtac ccontr 1,
- auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
+ old_auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
]);
qed_goal "BoxDmdDmdBox" TLA.thy
@@ -420,7 +421,7 @@
(* Auxiliary lemma allows priming of boxed actions *)
qed_goal "BoxPrime" TLA.thy "[]P .-> [](P .& P`)"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
etac dup_boxE 1,
auto_tac (temp_css addsimps2 [boxact_def]
addSIs2 [STL2bD_pr] addSEs2 [STL4E])
@@ -517,7 +518,7 @@
]);
qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
etac notE 1,
SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps)
addIs2 [INV1I] addEs2 [STL4E])) 1,
@@ -533,7 +534,7 @@
(* The "=>" part of the following is a little intricate. *)
qed_goal "InfinitePrime" TLA.thy "([]<>$P) .= ([]<>P$)"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
rtac classical 1,
rtac (temp_mp DBImplBDAct) 1,
subgoal_tac "sigma |= <>[]$P" 1,
@@ -592,7 +593,7 @@
qed_goalw "streett_leadsto" TLA.thy [leadsto]
"([]<>P .-> []<>Q) .= (<>(P ~> Q))"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
asm_full_simp_tac (simpset() addsimps boxact_def::more_temp_simps) 1,
SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E]
addsimps2 Init_simps)) 1,
@@ -725,26 +726,26 @@
\ P .& N .-> $(Enabled(<A>_v)) |] \
\ ==> []N .& WF(A)_v .-> (P ~> Q)"
(fn [prem1,prem2,prem3]
- => [auto_tac (temp_css addSDs2 [BoxWFI]),
- etac STL4Edup 1, atac 1,
- Auto_tac(),
- subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
- auto_tac (temp_css addSDs2 [unless]),
- etac (temp_conjimpE INV1) 1, atac 1,
- merge_box_tac 1,
- rtac STL2D 1,
- rtac EnsuresInfinite 1, atac 2,
- SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_alt])) 1,
- atac 2,
- subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
- merge_box_tac 1,
- SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
- SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
- (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
- fast_tac (action_cs addSIs [action_mp prem2]) 1,
- fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
- fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
- ]);
+ => [auto_tac (temp_css addSDs2 [BoxWFI]),
+ etac STL4Edup 1, atac 1,
+ Auto_tac,
+ subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
+ auto_tac (temp_css addSDs2 [unless]),
+ etac (temp_conjimpE INV1) 1, atac 1,
+ merge_box_tac 1,
+ rtac STL2D 1,
+ rtac EnsuresInfinite 1, atac 2,
+ SELECT_GOAL (old_auto_tac (temp_css addsimps2 [WF_alt])) 1,
+ atac 2,
+ subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
+ merge_box_tac 1,
+ SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
+ SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
+ (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
+ fast_tac (action_cs addSIs [action_mp prem2]) 1,
+ fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
+ fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
+ ]);
(* Sometimes easier to use; designed for action B rather than state predicate Q *)
qed_goalw "WF_leadsto" TLA.thy [leadsto]
@@ -755,7 +756,7 @@
(fn [prem1,prem2,prem3]
=> [auto_tac (temp_css addSDs2 [BoxWFI]),
etac STL4Edup 1, atac 1,
- Auto_tac(),
+ Auto_tac,
subgoal_tac "sigmaa |= <><A>_v" 1,
SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1,
rtac classical 1,
@@ -779,14 +780,14 @@
eres_inst_tac [("F","F")] dup_boxE 1,
merge_temp_box_tac 1,
etac STL4Edup 1, atac 1,
- Auto_tac(),
+ Auto_tac,
subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
auto_tac (temp_css addSDs2 [unless]),
etac (temp_conjimpE INV1) 1, atac 1,
merge_act_box_tac 1,
rtac STL2D 1,
rtac EnsuresInfinite 1, atac 2,
- SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_alt])) 1,
+ SELECT_GOAL (old_auto_tac (temp_css addsimps2 [SF_alt])) 1,
atac 2,
subgoal_tac "sigmaa |= []<>$(Enabled(<A>_v))" 1,
SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
@@ -805,7 +806,7 @@
\ [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(<M>_g))) .-> <>[]P |] \
\ ==> []N .& WF(A)_f .& []F .-> WF(M)_g"
(fn [prem1,prem2,prem3,prem4]
- => [Auto_tac(),
+ => [Auto_tac,
case_tac "sigma |= <>[]$Enabled(<M>_g)" 1,
SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
case_tac "sigma |= <>[][.~B]_f" 1,
@@ -819,7 +820,7 @@
subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
- SELECT_GOAL (Auto_tac()) 1,
+ SELECT_GOAL Auto_tac 1,
dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
merge_act_box_tac 1,
etac InfImpl 1, atac 1,
@@ -827,7 +828,7 @@
etac BoxDmd 1,
dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
- SELECT_GOAL (Auto_tac ()) 1,
+ SELECT_GOAL Auto_tac 1,
rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1,
fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1,
etac (temp_conjimpE STL6) 1, atac 1,
@@ -857,7 +858,7 @@
\ [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>($(Enabled(<M>_g))) .-> <>[]P |] \
\ ==> []N .& SF(A)_f .& []F .-> SF(M)_g"
(fn [prem1,prem2,prem3,prem4]
- => [Auto_tac(),
+ => [Auto_tac,
case_tac "sigma |= []<>$Enabled(<M>_g)" 1,
SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
case_tac "sigma |= <>[][.~B]_f" 1,
@@ -871,7 +872,7 @@
subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
- SELECT_GOAL (Auto_tac()) 1,
+ SELECT_GOAL Auto_tac 1,
dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
merge_act_box_tac 1,
etac InfImpl 1, atac 1,
@@ -879,7 +880,7 @@
etac BoxDmd 1,
dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
- SELECT_GOAL (Auto_tac ()) 1,
+ SELECT_GOAL Auto_tac 1,
rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1,
fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1,
dtac BoxSFI 1,
@@ -915,7 +916,7 @@
subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1,
cut_facts_tac prems 1,
etac STL4Edup 1, atac 1,
- Auto_tac(), etac swap 1, atac 1,
+ Auto_tac, etac swap 1, atac 1,
rtac dup_dmdD 1,
etac DmdImpl2 1, atac 1,
subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1,
@@ -943,7 +944,7 @@
(* If r is well-founded, state function v cannot decrease forever *)
qed_goal "wf_not_box_decrease" TLA.thy
"!!r. wf r ==> [][ {[v$, $v]} .: #r ]_v .-> <>[][#False]_v"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
subgoal_tac "ALL x. (sigma |= [](Init($v .= #x) .-> <>[][#False]_v))" 1,
etac allE 1,
dtac STL2D 1,
@@ -968,7 +969,7 @@
dres_inst_tac [("P", "$v .= #xa")] (temp_mp BoxPrime) 1,
SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1,
SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1,
- auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
+ old_auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
]);
(* "wf ?r ==> <>[][{[?v$, $?v]} .: #?r]_?v .-> <>[][#False]_?v" *)
@@ -980,14 +981,14 @@
*)
qed_goal "wf_box_dmd_decrease" TLA.thy
"wf r ==> []<>({[v$, $v]} .: #r) .-> []<><.~({[v$, $v]} .: #r)>_v"
- (fn [prem] => [Auto_tac(),
+ (fn [prem] => [Auto_tac,
rtac ccontr 1,
asm_full_simp_tac
(simpset() addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
dtac BoxDmdDmdBox 1, atac 1,
subgoal_tac "sigma |= []<>((#False)::action)" 1,
- SELECT_GOAL (Auto_tac()) 1,
+ SELECT_GOAL Auto_tac 1,
etac STL4E 1,
rtac DmdImpl 1,
auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl])
@@ -998,12 +999,12 @@
*)
qed_goal "nat_box_dmd_decrease" TLA.thy
"!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)"
- (fn _ => [Auto_tac(),
+ (fn _ => [Auto_tac,
subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1,
etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1,
rtac nat_less_cases 1,
- Auto_tac(),
+ Auto_tac,
rtac (temp_mp wf_box_dmd_decrease) 1,
auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset())
]);
--- a/src/HOL/equalities.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/equalities.ML Wed Dec 24 10:02:30 1997 +0100
@@ -603,7 +603,7 @@
AddIffs [all_not_in_conv];
goalw thy [Pow_def] "Pow {} = {{}}";
-by (Auto_tac());
+by Auto_tac;
qed "Pow_empty";
Addsimps [Pow_empty];
--- a/src/HOL/ex/Recdef.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/ex/Recdef.ML Wed Dec 24 10:02:30 1997 +0100
@@ -24,7 +24,7 @@
goal thy "g x < Suc x";
by (res_inst_tac [("u","x")] g.induct 1);
-by (Auto_tac());
+by Auto_tac;
by (trans_tac 1);
qed "g_terminates";
--- a/src/HOL/simpdata.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOL/simpdata.ML Wed Dec 24 10:02:30 1997 +0100
@@ -471,14 +471,24 @@
fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
-fun auto_tac (cs,ss) =
+fun mk_auto_tac (cs, ss) m n =
let val cs' = cs addss ss
- in EVERY [TRY (safe_tac cs'),
- REPEAT (FIRSTGOAL (fast_tac cs')),
+ val bdt = Blast.depth_tac cs m;
+ fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s =>
+ (warning ("Blast_tac: " ^ s); Seq.empty);
+ val maintac =
+ blast_depth_tac (*fast but can't use addss*)
+ ORELSE'
+ depth_tac cs' n; (*slower but general*)
+ in EVERY [ALLGOALS (asm_full_simp_tac ss),
+ TRY (safe_tac cs'),
+ REPEAT (FIRSTGOAL maintac),
TRY (safe_tac (cs addSss ss)),
prune_params_tac]
end;
-fun Auto_tac () = auto_tac (claset(), simpset());
+fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
-fun auto () = by (Auto_tac ());
+fun Auto_tac st = auto_tac (claset(), simpset()) st;
+
+fun auto () = by Auto_tac;
--- a/src/HOLCF/Fix.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/Fix.ML Wed Dec 24 10:02:30 1997 +0100
@@ -414,7 +414,7 @@
(cut_facts_tac prems 1),
(rtac trans 1),
(stac unfold 1),
- (Auto_tac ())
+ Auto_tac
]);
(* ------------------------------------------------------------------------ *)
--- a/src/HOLCF/IOA/ABP/Correctness.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Wed Dec 24 10:02:30 1997 +0100
@@ -159,7 +159,7 @@
by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
by (Step_tac 1);
by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
-by (Auto_tac());
+by (Auto_tac);
val reduce_tl =result();
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Wed Dec 24 10:02:30 1997 +0100
@@ -112,7 +112,7 @@
goal thy"compatible A B = compatible B A";
by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1);
-by (Auto_tac());
+by Auto_tac;
qed"compat_commute";
goalw thy [externals_def,actions_def,compatible_def]
@@ -289,7 +289,7 @@
by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
restrict_asig_def]) 1);
-by (Auto_tac());
+by Auto_tac;
qed"acts_restrict";
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
@@ -414,10 +414,11 @@
goalw thy [is_trans_of_def,restrict_def,restrict_asig_def]
"!!A. is_trans_of A ==> is_trans_of (rename A f)";
-by (asm_full_simp_tac (simpset() addsimps [actions_def,trans_of_def,
- asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,
- asig_of_def,rename_def,rename_set_def]) 1);
-by (Auto_tac());
+by (asm_full_simp_tac
+ (simpset() addsimps [actions_def,trans_of_def, asig_internals_def,
+ asig_outputs_def,asig_inputs_def,externals_def,
+ asig_of_def,rename_def,rename_set_def]) 1);
+by (Blast_tac 1);
qed"is_trans_of_rename";
goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|] \
@@ -426,7 +427,7 @@
asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
asig_inputs_def,actions_def,is_asig_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
-by (Auto_tac());
+by Auto_tac;
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"is_asig_of_par";
@@ -434,7 +435,7 @@
asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def]
"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
by (Asm_full_simp_tac 1);
-by (Auto_tac());
+by Auto_tac;
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"is_asig_of_restrict";
@@ -442,7 +443,7 @@
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
-by (Auto_tac());
+by Auto_tac;
by (dres_inst_tac [("s","Some xb")] sym 1);
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
@@ -466,7 +467,7 @@
"!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
outputs_of_par,actions_of_par]) 1);
-by (Auto_tac());
+by Auto_tac;
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"compatible_par";
@@ -475,7 +476,7 @@
"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
outputs_of_par,actions_of_par]) 1);
-by (Auto_tac());
+by Auto_tac;
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"compatible_par2";
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Wed Dec 24 10:02:30 1997 +0100
@@ -115,7 +115,7 @@
by (simp_tac (simpset() addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
-by (Auto_tac());
+by Auto_tac;
qed"mkex_cons_1";
goal thy "!!x.[| x~:act A; x:act B |] \
@@ -124,7 +124,7 @@
by (simp_tac (simpset() addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
-by (Auto_tac());
+by Auto_tac;
qed"mkex_cons_2";
goal thy "!!x.[| x:act A; x:act B |] \
@@ -133,7 +133,7 @@
by (simp_tac (simpset() addsimps [mkex_def]
setloop (split_tac [expand_if]) ) 1);
by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
-by (Auto_tac());
+by Auto_tac;
qed"mkex_cons_3";
Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
@@ -364,7 +364,7 @@
by (Seq_induct_tac "x" [] 1);
by (Seq_case_simp_tac "y" 2);
by (pair_tac "a" 1);
-by (Auto_tac());
+by Auto_tac;
*)
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed Dec 24 10:02:30 1997 +0100
@@ -170,7 +170,7 @@
by (rtac (Forall_Conc_impl RS mp) 1);
by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
(* a~:A,a~:B *)
-by (Auto_tac());
+by Auto_tac;
qed"ForallAorB_mksch1";
bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
@@ -395,12 +395,12 @@
\ y = z @@ mksch A B`tr`a`b\
\ --> Finite tr";
by (etac Seq_Finite_ind 1);
-by (Auto_tac());
+by Auto_tac;
by (Seq_case_simp_tac "tr" 1);
(* tr = UU *)
by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1);
(* tr = nil *)
-by (Auto_tac());
+by Auto_tac;
(* tr = Conc *)
ren "s ss" 1;
@@ -419,7 +419,7 @@
by (Seq_case_simp_tac "tr" 1);
(* tr = UU *)
by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
-by (Auto_tac());
+by Auto_tac;
(* tr = nil ok *)
(* tr = Conc *)
by (Seq_case_simp_tac "z" 1);
@@ -452,19 +452,19 @@
goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))";
by (Seq_case_simp_tac "y" 1);
-by (Auto_tac());
+by Auto_tac;
qed"Conc_Conc_eq";
goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU";
by (etac Seq_Finite_ind 1);
by (Seq_case_simp_tac "x" 1);
by (Seq_case_simp_tac "x" 1);
-by (Auto_tac());
+by Auto_tac;
qed"FiniteConcUU1";
goal thy "~ Finite ((x::'a Seq)@@UU)";
by (rtac (FiniteConcUU1 COMP rev_contrapos) 1);
-by (Auto_tac());
+by Auto_tac;
qed"FiniteConcUU";
finiteR_mksch
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Wed Dec 24 10:02:30 1997 +0100
@@ -9,7 +9,7 @@
goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
-by (Auto_tac());
+by Auto_tac;
qed"compatibility_consequence3";
@@ -29,7 +29,7 @@
or even better A||B= B||A, FIX *)
goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
-by (Auto_tac());
+by Auto_tac;
qed"compatibility_consequence4";
goal thy
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Wed Dec 24 10:02:30 1997 +0100
@@ -136,7 +136,7 @@
by (rtac impI 1);
by (etac conjE 1);
by (forward_tac [reachable_rename] 1);
-by (Auto_tac());
+by Auto_tac;
qed"rename_through_pmap";
--- a/src/HOLCF/IOA/meta_theory/Seq.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML Wed Dec 24 10:02:30 1997 +0100
@@ -320,7 +320,7 @@
"!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
by (rtac iffI 1);
by (etac (hd seq.injects) 1);
-by (Auto_tac());
+by Auto_tac;
qed"scons_inject_eq";
goal thy "!!x. nil<<x ==> nil=x";
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Wed Dec 24 10:02:30 1997 +0100
@@ -432,7 +432,7 @@
by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
by (rtac refl 1);
by (rtac (FiniteConc_1 RS mp) 1);
-by (Auto_tac());
+by Auto_tac;
qed"FiniteConc";
Addsimps [FiniteConc];
@@ -448,13 +448,13 @@
by (Seq_case_simp_tac "t" 1);
by (Asm_full_simp_tac 1);
(* main case *)
-by (Auto_tac());
+by Auto_tac;
by (Seq_case_simp_tac "t" 1);
by (Asm_full_simp_tac 1);
qed"FiniteMap2";
goal thy "Finite (Map f`s) = Finite s";
-by (Auto_tac());
+by Auto_tac;
by (etac (FiniteMap2 RS spec RS mp) 1);
by (rtac refl 1);
by (etac FiniteMap1 1);
@@ -482,9 +482,9 @@
by (etac conjE 1);
by (etac nil_less_is_nil 1);
(* main case *)
-by (Auto_tac());
+by Auto_tac;
by (Seq_case_simp_tac "y" 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp"Finite_flat";
@@ -499,7 +499,7 @@
by (eres_inst_tac [("x","j")] allE 1);
by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1);
(* Generates a contradiction in subgoal 3 *)
-by (Auto_tac());
+by Auto_tac;
qed"adm_Finite";
Addsimps [adm_Finite];
@@ -530,12 +530,12 @@
(* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
goal thy "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
by (Seq_case_simp_tac "x" 1);
-by (Auto_tac());
+by Auto_tac;
qed"nil_is_Conc";
goal thy "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
by (Seq_case_simp_tac "x" 1);
-by (Auto_tac());
+by Auto_tac;
qed"nil_is_Conc2";
@@ -642,14 +642,14 @@
by (strip_tac 1);
by (Seq_case_simp_tac "sa" 1);
by (Asm_full_simp_tac 1);
-by (Auto_tac());
+by Auto_tac;
qed"Forall_prefix";
bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
-by (Auto_tac());
+by Auto_tac;
qed"Forall_postfixclosed";
@@ -728,7 +728,7 @@
\ (Forall (%x. ~P x) ys & ~Finite ys)";
by (rtac conjI 1);
by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
-by (Auto_tac());
+by Auto_tac;
by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1);
qed"FilternPUUForallP";
@@ -737,14 +737,14 @@
\ ==> Filter P`ys = nil";
by (etac ForallnPFilterPnil 1);
by (etac ForallPForallQ 1);
-by (Auto_tac());
+by Auto_tac;
qed"ForallQFilterPnil";
goal thy "!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|] \
\ ==> Filter P`ys = UU ";
by (etac ForallnPFilterPUU 1);
by (etac ForallPForallQ 1);
-by (Auto_tac());
+by Auto_tac;
qed"ForallQFilterPUU";
@@ -762,7 +762,7 @@
goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
by (rtac ForallPForallQ 1);
by (rtac ForallPTakewhileP 1);
-by (Auto_tac());
+by Auto_tac;
qed"ForallPTakewhileQ";
@@ -771,7 +771,7 @@
by (etac ForallnPFilterPnil 1);
by (rtac ForallPForallQ 1);
by (rtac ForallPTakewhileP 1);
-by (Auto_tac());
+by Auto_tac;
qed"FilterPTakewhileQnil";
goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
@@ -779,7 +779,7 @@
by (rtac ForallPFilterPid 1);
by (rtac ForallPForallQ 1);
by (rtac ForallPTakewhileP 1);
-by (Auto_tac());
+by Auto_tac;
qed"FilterPTakewhileQid";
Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
@@ -864,14 +864,15 @@
by (safe_tac set_cs);
by (res_inst_tac [("x","x")] exI 1);
by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
-by (Auto_tac());
+by Auto_tac;
qed"divide_Seq2";
goal thy "!! y. ~Forall P y \
\ ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
by (cut_inst_tac [] divide_Seq2 1);
-by (Auto_tac());
+(*Auto_tac no longer proves it*)
+by (REPEAT (fast_tac (claset() addss (simpset())) 1));
qed"divide_Seq3";
Addsimps [FilterPQ,FilterConc,Conc_cong];
@@ -885,7 +886,7 @@
goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
by (rtac iffI 1);
by (resolve_tac seq.take_lemmas 1);
-by (Auto_tac());
+by Auto_tac;
qed"seq_take_lemma";
goal thy
@@ -894,9 +895,9 @@
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
by (res_inst_tac [("n","n")] natE 1);
-by (Auto_tac());
+by Auto_tac;
by (res_inst_tac [("n","n")] natE 1);
-by (Auto_tac());
+by Auto_tac;
qed"take_reduction1";
@@ -916,9 +917,9 @@
by (Seq_induct_tac "x" [] 1);
by (strip_tac 1);
by (res_inst_tac [("n","n")] natE 1);
-by (Auto_tac());
+by Auto_tac;
by (res_inst_tac [("n","n")] natE 1);
-by (Auto_tac());
+by Auto_tac;
qed"take_reduction_less1";
@@ -949,7 +950,7 @@
goal thy "(!n. seq_take n`x << seq_take n`x') = (x << x')";
by (rtac iffI 1);
by (rtac take_lemma_less1 1);
-by (Auto_tac());
+by Auto_tac;
by (etac monofun_cfun_arg 1);
qed"take_lemma_less";
@@ -973,7 +974,7 @@
by (case_tac "Forall Q x" 1);
by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
by (resolve_tac seq.take_lemmas 1);
-by (Auto_tac());
+by Auto_tac;
qed"take_lemma_principle2";
@@ -1190,8 +1191,9 @@
goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
-by (res_inst_tac [("A1","%x. True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
-by (Auto_tac());
+by (res_inst_tac [("A1","%x. True"), ("x1","x")]
+ (take_lemma_in_eq_out RS mp) 1);
+by Auto_tac;
qed"MapConc_takelemma";
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Wed Dec 24 10:02:30 1997 +0100
@@ -106,7 +106,7 @@
ForallQFilterPUU]) 1);
(* main case *)
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
-by (Auto_tac());
+by Auto_tac;
qed"FilterCut";
@@ -124,7 +124,7 @@
(* main case *)
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
by (rtac take_reduction 1);
-by (Auto_tac());
+by Auto_tac;
qed"Cut_idemp";
@@ -148,7 +148,7 @@
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc,
ForallMap,FiniteMap1,o_def]) 1);
by (rtac take_reduction 1);
-by (Auto_tac());
+by Auto_tac;
qed"MapCut";
@@ -174,7 +174,7 @@
by (asm_full_simp_tac (simpset() addsimps [Cut_Cons]) 1);
by (rtac take_reduction_less 1);
(* auto makes also reasoning about Finiteness of parts of s ! *)
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp"Cut_prefixcl_nFinite";
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Wed Dec 24 10:02:30 1997 +0100
@@ -179,7 +179,7 @@
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
by (pair_tac "x" 1);
by (rtac (execfrag_in_sig RS spec RS mp) 1);
-by (Auto_tac());
+by Auto_tac;
qed"exec_in_sig";
goalw thy [schedules_def,has_schedule_def]
@@ -213,7 +213,7 @@
by (strip_tac 1);
by (Seq_case_simp_tac "xa" 1);
by (pair_tac "a" 1);
-by (Auto_tac());
+by Auto_tac;
qed"execfrag_prefixclosed";
bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
@@ -226,6 +226,6 @@
by (strip_tac 1);
by (Seq_case_simp_tac "s" 1);
by (pair_tac "a" 1);
-by (Auto_tac());
+by Auto_tac;
qed_spec_mp"exec_prefix2closed";
--- a/src/HOLCF/Lift.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/Lift.ML Wed Dec 24 10:02:30 1997 +0100
@@ -40,7 +40,7 @@
back();
by (safe_tac set_cs);
by (rtac cont_flift1_not_arg 1);
-by (Auto_tac());
+by Auto_tac;
by (rtac cont_flift1_arg 1);
qed"cont_flift1_arg_and_not_arg";
--- a/src/HOLCF/Lift3.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/Lift3.ML Wed Dec 24 10:02:30 1997 +0100
@@ -148,7 +148,7 @@
goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
by (rtac cont2cont_CF1L 1);
by (REPEAT (resolve_tac cont_lemmas1 1));
-by (Auto_tac());
+by Auto_tac;
qed"cont_fapp_app";
goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
--- a/src/HOLCF/Tr.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/HOLCF/Tr.ML Wed Dec 24 10:02:30 1997 +0100
@@ -115,17 +115,17 @@
"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)";
by (rtac iffI 1);
by (res_inst_tac [("p","t")] trE 1);
-by (Auto_tac());
+by Auto_tac;
by (res_inst_tac [("p","t")] trE 1);
-by (Auto_tac());
+by Auto_tac;
qed"andalso_or";
goal thy "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
by (rtac iffI 1);
by (res_inst_tac [("p","t")] trE 1);
-by (Auto_tac());
+by Auto_tac;
by (res_inst_tac [("p","t")] trE 1);
-by (Auto_tac());
+by Auto_tac;
qed"andalso_and";
goal thy "(Def x ~=FF)= x";
--- a/src/ZF/CardinalArith.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/CardinalArith.ML Wed Dec 24 10:02:30 1997 +0100
@@ -806,7 +806,7 @@
goal CardinalArith.thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
by (rtac eqpoll_trans 1);
by (resolve_tac [well_ord_radd RS well_ord_cardinal_eqpoll RS eqpoll_sym] 1);
-by (REPEAT (eresolve_tac [nat_implies_well_ord] 1));
+by (REPEAT (etac nat_implies_well_ord 1));
by (asm_simp_tac (simpset()
addsimps [nat_cadd_eq_add RS sym, cadd_def, eqpoll_refl]) 1);
qed "nat_sum_eqpoll_sum";
--- a/src/ZF/Coind/MT.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/Coind/MT.ML Wed Dec 24 10:02:30 1997 +0100
@@ -79,7 +79,7 @@
by (excluded_middle_tac "f=y" 1);
by (rtac UnI1 2);
by (rtac UnI2 1);
-by (Auto_tac());
+by Auto_tac;
qed "consistency_fix";
--- a/src/ZF/Perm.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/Perm.ML Wed Dec 24 10:02:30 1997 +0100
@@ -431,7 +431,7 @@
by (Asm_full_simp_tac 1);
by (rtac fun_extension 1);
by (REPEAT (ares_tac [comp_fun, lam_type] 1));
-by (Auto_tac());
+by Auto_tac;
qed "comp_eq_id_iff";
goalw Perm.thy [bij_def]
--- a/src/ZF/QPair.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/QPair.ML Wed Dec 24 10:02:30 1997 +0100
@@ -110,14 +110,14 @@
qed_goal "qfst_type" thy
"!!p. p:QSigma(A,B) ==> qfst(p) : A"
- (fn _=> [ Auto_tac() ]);
+ (fn _=> [ Auto_tac ]);
qed_goal "qsnd_type" thy
"!!p. p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
- (fn _=> [ Auto_tac() ]);
+ (fn _=> [ Auto_tac ]);
goal thy "!!a A B. a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
-by (Auto_tac());
+by Auto_tac;
qed "QPair_qfst_qsnd_eq";
@@ -142,7 +142,7 @@
goalw thy [qsplit_def]
"!!u. u: A<*>B ==> \
\ R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
-by (Auto_tac());
+by Auto_tac;
qed "expand_qsplit";
--- a/src/ZF/Sum.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/Sum.ML Wed Dec 24 10:02:30 1997 +0100
@@ -156,7 +156,7 @@
\ R(case(c,d,u)) <-> \
\ ((ALL x:A. u = Inl(x) --> R(c(x))) & \
\ (ALL y:B. u = Inr(y) --> R(d(y))))";
-by (Auto_tac());
+by Auto_tac;
qed "expand_case";
val major::prems = goal Sum.thy
@@ -172,7 +172,7 @@
"!!z. z: A+B ==> \
\ case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \
\ case(%x. c(c'(x)), %y. d(d'(y)), z)";
-by (Auto_tac());
+by Auto_tac;
qed "case_case";
--- a/src/ZF/ex/Limit.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/ex/Limit.ML Wed Dec 24 10:02:30 1997 +0100
@@ -49,8 +49,8 @@
val [po,xy,yz,x,y,z] = goalw Limit.thy [po_def]
"[|po(D); rel(D,x,y); rel(D,y,z); x:set(D); \
\ y:set(D); z:set(D)|] ==> rel(D,x,z)";
-br (po RS conjunct2 RS conjunct1 RS bspec RS bspec
- RS bspec RS mp RS mp) 1;
+by (rtac (po RS conjunct2 RS conjunct1 RS bspec RS bspec
+ RS bspec RS mp RS mp) 1);
by (rtac x 1);
by (rtac y 1);
by (rtac z 1);
@@ -126,8 +126,8 @@
val prems = goal Limit.thy
"[|islub(D,X,x); n:nat|] ==> rel(D,X`n,x)";
-br (rewrite_rule[islub_def,isub_def](hd prems) RS conjunct1
- RS conjunct2 RS bspec) 1;
+by (rtac (rewrite_rule[islub_def,isub_def](hd prems) RS conjunct1
+ RS conjunct2 RS bspec) 1);
by (resolve_tac prems 1);
qed "islub_ub";
--- a/src/ZF/ex/misc.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/ex/misc.ML Wed Dec 24 10:02:30 1997 +0100
@@ -155,7 +155,8 @@
\ : bij(Pow(A+B), Pow(A)*Pow(B))";
by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")]
lam_bijective 1);
-by (Auto_tac());
-val Pow_bij = result();
+(*Auto_tac no longer proves it*)
+by (REPEAT (fast_tac (claset() addss (simpset())) 1));
+qed "Pow_bij";
writeln"Reached end of file.";
--- a/src/ZF/pair.ML Tue Dec 23 11:56:09 1997 +0100
+++ b/src/ZF/pair.ML Wed Dec 24 10:02:30 1997 +0100
@@ -118,14 +118,14 @@
Addsimps [fst_conv,snd_conv];
qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
- (fn _=> [ Auto_tac() ]);
+ (fn _=> [ Auto_tac ]);
qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
- (fn _=> [ Auto_tac() ]);
+ (fn _=> [ Auto_tac ]);
qed_goal "Pair_fst_snd_eq" ZF.thy
"!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
- (fn _=> [ Auto_tac() ]);
+ (fn _=> [ Auto_tac ]);
(*** Eliminator - split ***)
@@ -148,7 +148,7 @@
goalw ZF.thy [split_def]
"!!u. u: A*B ==> \
\ R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
-by (Auto_tac());
+by Auto_tac;
qed "expand_split";