# HG changeset patch # User paulson # Date 882954150 -3600 # Node ID b3e5857d8d99ecaa28fa60e8c50697225e374939 # Parent fbdc87f8ac7e3e81f585329c7f6218a0ba4e5439 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort diff -r fbdc87f8ac7e -r b3e5857d8d99 src/FOL/simpdata.ML --- 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; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/Event.ML --- 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)"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/Message.ML --- 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]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/NS_Public.ML --- 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]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/NS_Public_Bad.ML --- 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); (* diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/NS_Shared.ML --- 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(); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/OtwayRees.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/OtwayRees_AN.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/OtwayRees_Bad.ML --- 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)]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/Public.ML --- 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]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/Recur.ML --- 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. diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/Shared.ML --- 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' & \ diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/TLS.ML --- 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)]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/WooLam.ML --- 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]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/Yahalom.ML --- 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)]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Auth/Yahalom2.ML --- 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)]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Divides.ML --- 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]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Finite.ML --- 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); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/IMP/Denotation.ML --- 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); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/IMP/Transition.ML --- 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-> t --> -c-> t)"; by (etac evalc1.induct 1); -by (Auto_tac()); +by Auto_tac; qed_spec_mp "FB_lemma3"; val [major] = goal Transition.thy diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/IOA/Solve.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Induct/Exp.ML --- 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)); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Induct/LFilter.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Induct/LList.ML --- 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); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Induct/Mutil.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Integ/Integ.ML --- 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 *) diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Option.ML --- 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]); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Quot/HQUOT.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Quot/NPAIR.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/Set.ML --- 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} 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*) diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/TLA/Action.ML --- 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] "(.~ _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 diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/TLA/Buffer/DBuffer.ML --- 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 (_) .= ($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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/TLA/Inc/Inc.ML --- 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 diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/TLA/Memory/MIlive.ML --- 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]_ .& $(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 |= []<>(_(c p))" 1, eres_inst_tac [("P","_(c p)")] EnsuresInfinite 1, atac 1, diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/TLA/Memory/MemoryImplementation.ML --- 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]_))" - (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]) diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/TLA/ROOT.ML --- 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 = (); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/TLA/TLA.ML --- 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(_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(_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(_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 |= <>_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(_v))" 1, SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1, @@ -805,7 +806,7 @@ \ [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(_g))) .-> <>[]P |] \ \ ==> []N .& WF(A)_f .& []F .-> WF(M)_g" (fn [prem1,prem2,prem3,prem4] - => [Auto_tac(), + => [Auto_tac, case_tac "sigma |= <>[]$Enabled(_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 .& []<>_f)" 1, rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1, eres_inst_tac [("F","[]N .& []P .& []<>_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","<>_f"),("G","[]P")] BoxDmd 1, atac 1, eres_inst_tac [("F","[]<>_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(_g))) .-> <>[]P |] \ \ ==> []N .& SF(A)_f .& []F .-> SF(M)_g" (fn [prem1,prem2,prem3,prem4] - => [Auto_tac(), + => [Auto_tac, case_tac "sigma |= []<>$Enabled(_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 .& []<>_f)" 1, rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1, eres_inst_tac [("F","[]N .& []P .& []<>_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","<>_f"),("G","[]P")] BoxDmd 1, atac 1, eres_inst_tac [("F","[]<>_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()) ]); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/equalities.ML --- 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]; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/ex/Recdef.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOL/simpdata.ML --- 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; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/Fix.ML --- 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 ]); (* ------------------------------------------------------------------------ *) diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/ABP/Correctness.ML --- 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(); diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/Automata.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/CompoScheds.ML --- 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; *) diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/CompoTraces.ML --- 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 diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/Compositionality.ML --- 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 diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/RefMappings.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/Seq.ML --- 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< nil=x"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/Sequence.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/ShortExecutions.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/IOA/meta_theory/Traces.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/Lift.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/Lift3.ML --- 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)"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/HOLCF/Tr.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/ZF/CardinalArith.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/ZF/Coind/MT.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/ZF/Perm.ML --- 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] diff -r fbdc87f8ac7e -r b3e5857d8d99 src/ZF/QPair.ML --- 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) ==> = 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 = --> R(c(x,y)))"; -by (Auto_tac()); +by Auto_tac; qed "expand_qsplit"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/ZF/Sum.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/ZF/ex/Limit.ML --- 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"; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/ZF/ex/misc.ML --- 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", "%.{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."; diff -r fbdc87f8ac7e -r b3e5857d8d99 src/ZF/pair.ML --- 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) ==> = 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 = --> R(c(x,y)))"; -by (Auto_tac()); +by Auto_tac; qed "expand_split";