# HG changeset patch # User wenzelm # Date 936693658 -7200 # Node ID 23e090051cb8cbb3f85f45f6902bfed7d7943637 # Parent 1e5585fd36324bb979fae1cdd569415744722ce5 isatool expandshort; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/KerberosIV.ML --- a/src/HOL/Auth/KerberosIV.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/KerberosIV.ML Tue Sep 07 10:40:58 1999 +0200 @@ -148,10 +148,10 @@ fun parts_induct_tac i = etac kerberos.induct i THEN REPEAT (FIRSTGOAL analz_mono_contra_tac) THEN - forward_tac [K3_msg_in_parts_spies] (i+4) THEN - forward_tac [K5_msg_in_parts_spies] (i+6) THEN - forward_tac [Oops_parts_spies1] (i+8) THEN - forward_tac [Oops_parts_spies2] (i+9) THEN + ftac K3_msg_in_parts_spies (i+4) THEN + ftac K5_msg_in_parts_spies (i+6) THEN + ftac Oops_parts_spies1 (i+8) THEN + ftac Oops_parts_spies2 (i+9) THEN prove_simple_subgoals_tac 1; @@ -247,7 +247,7 @@ \ : parts (spies evs);\ \ evs : kerberos |] \ \ ==> AuthKey : AuthKeys evs"; -by (forward_tac [A_trusts_AuthTicket] 1); +by (ftac A_trusts_AuthTicket 1); by (assume_tac 1); by (simp_tac (simpset() addsimps [AuthKeys_def]) 1); by (Blast_tac 1); @@ -497,7 +497,7 @@ "[| Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, tt, X |}) \ \ : set evs; \ \ evs : kerberos |] ==> KeyCryptKey AuthKey ServKey evs"; -by (forward_tac [Says_Tgs_message_form] 1); +by (ftac Says_Tgs_message_form 1); by (assume_tac 1); by (Blast_tac 1); qed "KeyCryptKeyI"; @@ -643,10 +643,10 @@ val analz_sees_tac = EVERY [REPEAT (FIRSTGOAL analz_mono_contra_tac), - forward_tac [Oops_range_spies2] 10, - forward_tac [Oops_range_spies1] 9, - forward_tac [Says_tgs_message_form] 7, - forward_tac [Says_kas_message_form] 5, + ftac Oops_range_spies2 10, + ftac Oops_range_spies1 9, + ftac Says_tgs_message_form 7, + ftac Says_kas_message_form 5, REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE] ORELSE' hyp_subst_tac)]; @@ -700,14 +700,14 @@ (*Oops 2*) by (case_tac "Key ServKey : analz (spies evsO2)" 2); by (ALLGOALS Asm_full_simp_tac); -by (forward_tac [analz_mono_KK] 2 +by (ftac analz_mono_KK 2 THEN assume_tac 2 THEN assume_tac 2); -by (forward_tac [analz_cut] 2 THEN assume_tac 2); +by (ftac analz_cut 2 THEN assume_tac 2); by (blast_tac (claset() addDs [analz_cut, impOfSubs analz_mono]) 2); by (dres_inst_tac [("x","SK")] spec 2); by (dres_inst_tac [("x","insert ServKey KK")] spec 2); -by (forward_tac [Says_Tgs_message_form] 2 THEN assume_tac 2); +by (ftac Says_Tgs_message_form 2 THEN assume_tac 2); by (Clarify_tac 2); by (forward_tac [Says_imp_spies RS parts.Inj RS parts.Body RS parts.Snd RS parts.Snd RS parts.Snd] 2); @@ -732,7 +732,7 @@ \ SesKey ~: range shrK |] \ \ ==> Key K : analz (insert (Key SesKey) (spies evs)) = \ \ (K = SesKey | Key K : analz (spies evs))"; -by (forward_tac [AuthKeys_are_not_KeyCryptKey] 1 THEN assume_tac 1); +by (ftac AuthKeys_are_not_KeyCryptKey 1 THEN assume_tac 1); by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); qed "analz_insert_freshK1"; @@ -742,7 +742,7 @@ Goal "[| evs : kerberos; ServKey ~: (AuthKeys evs); ServKey ~: range shrK|]\ \ ==> Key K : analz (insert (Key ServKey) (spies evs)) = \ \ (K = ServKey | Key K : analz (spies evs))"; -by (forward_tac [not_AuthKeys_not_KeyCryptKey] 1 +by (ftac not_AuthKeys_not_KeyCryptKey 1 THEN assume_tac 1 THEN assume_tac 1); by (asm_full_simp_tac (analz_image_freshK_ss addsimps [Key_analz_image_Key]) 1); @@ -837,7 +837,7 @@ \ ~ ExpirAuth Tk evs; \ \ A ~: bad; evs : kerberos |] \ \ ==> Key AuthKey ~: analz (spies evs)"; -by (forward_tac [Says_Kas_message_form] 1 THEN assume_tac 1); +by (ftac Says_Kas_message_form 1 THEN assume_tac 1); by (blast_tac (claset() addSDs [lemma]) 1); qed "Confidentiality_Kas"; @@ -890,7 +890,7 @@ Key_unique_SesKey] addIs [less_SucI]) 3); (** Level 12 **) (*Oops1*) -by (forward_tac [Says_Kas_message_form] 2); +by (ftac Says_Kas_message_form 2); by (assume_tac 2); by (blast_tac (claset() addDs [analz_insert_freshK3, Says_Kas_message_form, Says_Tgs_message_form] @@ -917,7 +917,7 @@ \ ~ ExpirServ Tt evs; \ \ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos |] \ \ ==> Key ServKey ~: analz (spies evs)"; -by (forward_tac [Says_Tgs_message_form] 1 THEN assume_tac 1); +by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); by (blast_tac (claset() addDs [lemma]) 1); qed "Confidentiality_Tgs1"; @@ -953,7 +953,7 @@ \ evs : kerberos |] \ \==> Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Tt, ServTicket|})\ \ : set evs"; -by (forward_tac [Says_Kas_message_form] 1 THEN assume_tac 1); +by (ftac Says_Kas_message_form 1 THEN assume_tac 1); by (etac rev_mp 1); by (etac rev_mp 1); by (etac rev_mp 1); @@ -1055,9 +1055,9 @@ \ & Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, \ \ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \ \ : set evs"; -by (forward_tac [B_trusts_ServKey] 1); +by (ftac B_trusts_ServKey 1); by (etac exE 4); -by (forward_tac [K4_imp_K2] 4); +by (ftac K4_imp_K2 4); by (Blast_tac 5); by (ALLGOALS assume_tac); qed "B_trusts_ServTicket"; @@ -1073,9 +1073,9 @@ \ Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|}|}) \ \ : set evs \ \ & ServLife + Tt <= AuthLife + Tk)"; -by (forward_tac [B_trusts_ServKey] 1); +by (ftac B_trusts_ServKey 1); by (etac exE 4); -by (forward_tac [K4_imp_K2_refined] 4); +by (ftac K4_imp_K2_refined 4); by (Blast_tac 5); by (ALLGOALS assume_tac); qed "B_trusts_ServTicket_refined"; @@ -1096,12 +1096,12 @@ \ ~ ExpirServ Tt evs; ~ ExpirAuth Tk evs; \ \ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos |] \ \ ==> Key ServKey ~: analz (spies evs)"; -by (forward_tac [A_trusts_AuthKey] 1); -by (forward_tac [Confidentiality_Kas] 3); -by (forward_tac [B_trusts_ServTicket] 6); +by (ftac A_trusts_AuthKey 1); +by (ftac Confidentiality_Kas 3); +by (ftac B_trusts_ServTicket 6); by (etac exE 9); by (etac exE 9); -by (forward_tac [Says_Kas_message_form] 9); +by (ftac Says_Kas_message_form 9); by (blast_tac (claset() addDs [A_trusts_K4, unique_ServKeys, unique_AuthKeys, Confidentiality_Tgs2]) 10); @@ -1143,7 +1143,7 @@ \ ~ ExpirAuth Tk evs; A ~: bad; evs : kerberos |] \ \==>Says Tgs A (Crypt AuthKey {|Key ServKey, Agent B, Number Tt, ServTicket|})\ \ : set evs"; -by (forward_tac [A_trusts_AuthKey] 1 THEN assume_tac 1 THEN assume_tac 1); +by (ftac A_trusts_AuthKey 1 THEN assume_tac 1 THEN assume_tac 1); by (blast_tac (claset() addDs [Confidentiality_Auth_A, A_trusts_K4_bis]) 1); qed "A_trusts_ServKey"; (*Note: requires a temporal check*) @@ -1170,8 +1170,8 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (etac kerberos.induct 1); -by (forward_tac [Says_ticket_in_parts_spies] 5); -by (forward_tac [Says_ticket_in_parts_spies] 7); +by (ftac Says_ticket_in_parts_spies 5); +by (ftac Says_ticket_in_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); by (Fake_parts_insert_tac 1); @@ -1198,8 +1198,8 @@ \ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos |] \ \ ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\ \ Crypt ServKey {|Agent A, Number Ta|} |} : set evs"; -by (forward_tac [Confidentiality_B] 1); -by (forward_tac [B_trusts_ServKey] 9); +by (ftac Confidentiality_B 1); +by (ftac B_trusts_ServKey 9); by (etac exE 12); by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] addSIs [Says_Auth]) 12); @@ -1214,8 +1214,8 @@ \ B ~= Tgs; A ~: bad; B ~: bad; evs : kerberos |] \ \ ==> Says A B {|Crypt (shrK B) {|Agent A, Agent B, Key ServKey, Number Tt|},\ \ Crypt ServKey {|Agent A, Number Ta2|} |} : set evs"; -by (forward_tac [Confidentiality_B_refined] 1); -by (forward_tac [B_trusts_ServKey] 6); +by (ftac Confidentiality_B_refined 1); +by (ftac B_trusts_ServKey 6); by (etac exE 9); by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] addSIs [Says_Auth]) 9); @@ -1235,14 +1235,14 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (etac kerberos.induct 1); -by (forward_tac [Says_ticket_in_parts_spies] 5); -by (forward_tac [Says_ticket_in_parts_spies] 7); +by (ftac Says_ticket_in_parts_spies 5); +by (ftac Says_ticket_in_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS Asm_simp_tac); by (Fake_parts_insert_tac 1); by (force_tac (claset() addSDs [Crypt_imp_keysFor], simpset()) 1); by (Clarify_tac 1); -by (forward_tac [Says_Tgs_message_form] 1 THEN assume_tac 1); +by (ftac Says_Tgs_message_form 1 THEN assume_tac 1); by (Clarify_tac 1); (*PROOF FAILED if omitted*) by (blast_tac (claset() addDs [unique_CryptKey] addEs spies_partsEs) 1); qed "Says_K6"; @@ -1269,13 +1269,13 @@ \ ~ ExpirAuth Tk evs; ~ ExpirServ Tt evs; \ \ A ~: bad; B ~: bad; B ~= Tgs; evs : kerberos |] \ \ ==> Says B A (Crypt ServKey (Number Ta)) : set evs"; -by (forward_tac [A_trusts_AuthKey] 1); -by (forward_tac [Says_Kas_message_form] 3); -by (forward_tac [Confidentiality_Kas] 4); -by (forward_tac [K4_trustworthy] 7); +by (ftac A_trusts_AuthKey 1); +by (ftac Says_Kas_message_form 3); +by (ftac Confidentiality_Kas 4); +by (ftac K4_trustworthy 7); by (Blast_tac 8); by (etac exE 9); -by (forward_tac [K4_imp_K2] 9); +by (ftac K4_imp_K2 9); by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj, Key_unique_SesKey] addSIs [Says_K6] addSEs [Confidentiality_Tgs1 RSN (2,rev_notE)]) 10); @@ -1298,8 +1298,8 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (etac kerberos.induct 1); -by (forward_tac [Says_ticket_in_parts_spies] 5); -by (forward_tac [Says_ticket_in_parts_spies] 7); +by (ftac Says_ticket_in_parts_spies 5); +by (ftac Says_ticket_in_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); by (Fake_parts_insert_tac 1); @@ -1399,8 +1399,8 @@ by (etac rev_mp 1); by (etac rev_mp 1); by (etac kerberos.induct 1); -by (forward_tac [Says_ticket_in_parts_spies] 5); -by (forward_tac [Says_ticket_in_parts_spies] 7); +by (ftac Says_ticket_in_parts_spies 5); +by (ftac Says_ticket_in_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS Asm_simp_tac); by (Clarify_tac 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/Kerberos_BAN.ML --- a/src/HOL/Auth/Kerberos_BAN.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/Kerberos_BAN.ML Tue Sep 07 10:40:58 1999 +0200 @@ -53,8 +53,8 @@ (*For proving the easier theorems about X ~: parts (spies evs).*) fun parts_induct_tac i = etac kerberos_ban.induct i THEN - forward_tac [Oops_parts_spies] (i+6) THEN - forward_tac [Kb3_msg_in_parts_spies] (i+4) THEN + ftac Oops_parts_spies (i+6) THEN + ftac Kb3_msg_in_parts_spies (i+4) THEN prove_simple_subgoals_tac i; @@ -160,8 +160,8 @@ (*For proofs involving analz.*) val analz_spies_tac = - forward_tac [Says_Server_message_form] 7 THEN - forward_tac [Says_S_message_form] 5 THEN + ftac Says_Server_message_form 7 THEN + ftac Says_S_message_form 5 THEN REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); @@ -266,7 +266,7 @@ \ ~ Expired T evs; \ \ A ~: bad; B ~: bad; evs : kerberos_ban \ \ |] ==> Key K ~: analz (spies evs)"; -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); +by (ftac Says_Server_message_form 1 THEN assume_tac 1); by (blast_tac (claset() addIs [lemma2]) 1); qed "Confidentiality_S"; @@ -304,9 +304,9 @@ \ Crypt K (Number Ta) : parts (spies evs) --> \ \ Says B A (Crypt K (Number Ta)) : set evs"; by (etac kerberos_ban.induct 1); -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); +by (ftac Says_S_message_form 5 THEN assume_tac 5); by (dtac Kb3_msg_in_parts_spies 5); -by (forward_tac [Oops_parts_spies] 7); +by (ftac Oops_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); (**LEVEL 6**) @@ -349,9 +349,9 @@ \ Says A B {|X, Crypt K {|Agent A, Number Ta|}|} \ \ : set evs"; by (etac kerberos_ban.induct 1); -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); -by (forward_tac [Kb3_msg_in_parts_spies] 5); -by (forward_tac [Oops_parts_spies] 7); +by (ftac Says_S_message_form 5 THEN assume_tac 5); +by (ftac Kb3_msg_in_parts_spies 5); +by (ftac Oops_parts_spies 7); by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); (**LEVEL 6**) diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/NS_Shared.ML Tue Sep 07 10:40:58 1999 +0200 @@ -50,8 +50,8 @@ fun parts_induct_tac i = EVERY [etac ns_shared.induct i, REPEAT (FIRSTGOAL analz_mono_contra_tac), - forward_tac [Oops_parts_spies] (i+7), - forward_tac [NS3_msg_in_parts_spies] (i+4), + ftac Oops_parts_spies (i+7), + ftac NS3_msg_in_parts_spies (i+4), prove_simple_subgoals_tac i]; @@ -140,8 +140,8 @@ (*For proofs involving analz.*) val analz_spies_tac = - forward_tac [Says_Server_message_form] 8 THEN - forward_tac [Says_S_message_form] 5 THEN + ftac Says_Server_message_form 8 THEN + ftac Says_S_message_form 5 THEN REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE] ORELSE' hyp_subst_tac); @@ -263,7 +263,7 @@ \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : ns_shared \ \ |] ==> Key K ~: analz (spies evs)"; -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); +by (ftac Says_Server_message_form 1 THEN assume_tac 1); by (blast_tac (claset() delrules [notI] addIs [lemma2]) 1); qed "Spy_not_see_encrypted_key"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Tue Sep 07 10:40:58 1999 +0200 @@ -70,9 +70,9 @@ (*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_induct_tac i = etac otway.induct i THEN - forward_tac [Oops_parts_knows_Spy] (i+7) THEN - forward_tac [OR4_parts_knows_Spy] (i+6) THEN - forward_tac [OR2_parts_knows_Spy] (i+4) THEN + ftac Oops_parts_knows_Spy (i+7) THEN + ftac OR4_parts_knows_Spy (i+6) THEN + ftac OR2_parts_knows_Spy (i+4) THEN prove_simple_subgoals_tac i; @@ -130,7 +130,7 @@ val analz_knows_Spy_tac = dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN - forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN + ftac Says_Server_message_form 8 THEN assume_tac 8 THEN REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); @@ -327,7 +327,7 @@ \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ \ ==> Key K ~: analz (knows Spy evs)"; -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); +by (ftac Says_Server_message_form 1 THEN assume_tac 1); by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/OtwayRees_AN.ML Tue Sep 07 10:40:58 1999 +0200 @@ -63,8 +63,8 @@ (*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_induct_tac i = etac otway.induct i THEN - forward_tac [Oops_parts_knows_Spy] (i+7) THEN - forward_tac [OR4_parts_knows_Spy] (i+6) THEN + ftac Oops_parts_knows_Spy (i+7) THEN + ftac OR4_parts_knows_Spy (i+6) THEN prove_simple_subgoals_tac i; @@ -123,7 +123,7 @@ (*For proofs involving analz.*) val analz_knows_Spy_tac = dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN - forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN + ftac Says_Server_message_form 8 THEN assume_tac 8 THEN REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); @@ -261,7 +261,7 @@ \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ \ ==> Key K ~: analz (knows Spy evs)"; -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); +by (ftac Says_Server_message_form 1 THEN assume_tac 1); by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Tue Sep 07 10:40:58 1999 +0200 @@ -74,9 +74,9 @@ (*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_induct_tac i = etac otway.induct i THEN - forward_tac [Oops_parts_knows_Spy] (i+7) THEN - forward_tac [OR4_parts_knows_Spy] (i+6) THEN - forward_tac [OR2_parts_knows_Spy] (i+4) THEN + ftac Oops_parts_knows_Spy (i+7) THEN + ftac OR4_parts_knows_Spy (i+6) THEN + ftac OR2_parts_knows_Spy (i+4) THEN prove_simple_subgoals_tac i; @@ -134,7 +134,7 @@ val analz_knows_Spy_tac = dtac OR2_analz_knows_Spy 5 THEN assume_tac 5 THEN dtac OR4_analz_knows_Spy 7 THEN assume_tac 7 THEN - forward_tac [Says_Server_message_form] 8 THEN assume_tac 8 THEN + ftac Says_Server_message_form 8 THEN assume_tac 8 THEN REPEAT ((eresolve_tac [exE, conjE] ORELSE' hyp_subst_tac) 8); @@ -229,7 +229,7 @@ \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : otway |] \ \ ==> Key K ~: analz (knows Spy evs)"; -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); +by (ftac Says_Server_message_form 1 THEN assume_tac 1); by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/Recur.ML --- a/src/HOL/Auth/Recur.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/Recur.ML Tue Sep 07 10:40:58 1999 +0200 @@ -112,9 +112,9 @@ (*For proving the easier theorems about X ~: parts (spies evs).*) fun parts_induct_tac i = EVERY [etac recur.induct i, - forward_tac [RA4_parts_spies] (i+5), - forward_tac [respond_imp_responses] (i+4), - forward_tac [RA2_parts_spies] (i+3), + ftac RA4_parts_spies (i+5), + ftac respond_imp_responses (i+4), + ftac RA2_parts_spies (i+3), prove_simple_subgoals_tac i]; @@ -175,7 +175,7 @@ (*For proofs involving analz.*) val analz_spies_tac = dtac RA2_analz_spies 4 THEN - forward_tac [respond_imp_responses] 5 THEN + ftac respond_imp_responses 5 THEN dtac RA4_analz_spies 6; @@ -354,8 +354,8 @@ \ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \ \ Key K ~: analz (insert RB (spies evs))"; by (etac respond.induct 1); -by (forward_tac [respond_imp_responses] 2); -by (forward_tac [respond_imp_not_used] 2); +by (ftac respond_imp_responses 2); +by (ftac respond_imp_not_used 2); by (ALLGOALS (*6 seconds*) (asm_simp_tac (analz_image_freshK_ss diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/WooLam.ML --- a/src/HOL/Auth/WooLam.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/WooLam.ML Tue Sep 07 10:40:58 1999 +0200 @@ -39,7 +39,7 @@ (*For proving the easier theorems about X ~: parts (spies evs) *) fun parts_induct_tac i = etac woolam.induct i THEN - forward_tac [WL4_parts_spies] (i+5) THEN + ftac WL4_parts_spies (i+5) THEN prove_simple_subgoals_tac 1; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/Yahalom.ML Tue Sep 07 10:40:58 1999 +0200 @@ -38,7 +38,7 @@ AddDs [Gets_imp_knows_Spy RS parts.Inj]; fun g_not_bad_tac s = - forward_tac [Gets_imp_Says] THEN' assume_tac THEN' not_bad_tac s; + ftac Gets_imp_Says THEN' assume_tac THEN' not_bad_tac s; (**** Inductive proofs about yahalom ****) @@ -65,8 +65,8 @@ (*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_knows_Spy_tac i = EVERY - [forward_tac [YM4_Key_parts_knows_Spy] (i+7), - forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6), + [ftac YM4_Key_parts_knows_Spy (i+7), + ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6), prove_simple_subgoals_tac i]; (*Induction for regularity theorems. If induction formula has the form @@ -132,7 +132,7 @@ (*For proofs involving analz.*) val analz_knows_Spy_tac = - forward_tac [YM4_analz_knows_Spy] 7 THEN assume_tac 7; + ftac YM4_analz_knows_Spy 7 THEN assume_tac 7; (**** The following is to prove theorems of the form @@ -512,7 +512,7 @@ by (g_not_bad_tac "Aa" 1); by (dtac (Gets_imp_knows_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1 THEN assume_tac 1); -by (forward_tac [Says_Server_imp_YM2] 3); +by (ftac Says_Server_imp_YM2 3); by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); (* use Says_unique_NB to identify message components: Aa=A, Ba=B*) by (blast_tac (claset() addDs [Says_unique_NB, @@ -520,7 +520,7 @@ (** LEVEL 13 **) (*Oops case: if the nonce is betrayed now, show that the Oops event is covered by the quantified Oops assumption.*) -by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1); +by (ftac Says_Server_imp_YM2 1 THEN assume_tac 1); by (expand_case_tac "NB = NBa" 1); (*If NB=NBa then all other components of the Oops message agree*) by (blast_tac (claset() addDs [Says_unique_NB]) 1); @@ -550,12 +550,12 @@ \ Nonce NA, Nonce NB|}, \ \ Crypt (shrK B) {|Agent A, Key K|}|} \ \ : set evs"; -by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); +by (ftac Spy_not_see_NB 1 THEN REPEAT (assume_tac 1)); by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1 THEN dtac B_trusts_YM4_shrK 1); by (dtac B_trusts_YM4_newK 3); by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); -by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1); +by (ftac Says_Server_imp_YM2 1 THEN assume_tac 1); by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1)); by (blast_tac (claset() addDs [Says_unique_NB]) 1); qed "B_trusts_YM4"; @@ -650,7 +650,7 @@ \ (ALL NA k. Notes Spy {|Nonce NA, Nonce NB, k|} ~: set evs); \ \ A ~: bad; B ~: bad; evs : yahalom |] \ \ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; -by (forward_tac [B_trusts_YM4] 1); +by (ftac B_trusts_YM4 1); by (REPEAT_FIRST (eresolve_tac [asm_rl, spec])); by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1); by (rtac A_Said_YM3_lemma 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/Yahalom2.ML --- a/src/HOL/Auth/Yahalom2.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/Yahalom2.ML Tue Sep 07 10:40:58 1999 +0200 @@ -64,8 +64,8 @@ (*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_knows_Spy_tac i = EVERY - [forward_tac [YM4_Key_parts_knows_Spy] (i+7), - forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6), + [ftac YM4_Key_parts_knows_Spy (i+7), + ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6), prove_simple_subgoals_tac i]; (*Induction for regularity theorems. If induction formula has the form @@ -130,7 +130,7 @@ (*For proofs involving analz.*) val analz_knows_Spy_tac = dtac YM4_analz_knows_Spy 7 THEN assume_tac 7 THEN - forward_tac [Says_Server_message_form] 8 THEN + ftac Says_Server_message_form 8 THEN assume_tac 8 THEN REPEAT ((etac conjE ORELSE' hyp_subst_tac) 8); @@ -228,7 +228,7 @@ \ Notes Spy {|na, nb, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : yahalom |] \ \ ==> Key K ~: analz (knows Spy evs)"; -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); +by (ftac Says_Server_message_form 1 THEN assume_tac 1); by (blast_tac (claset() addSEs [lemma]) 1); qed "Spy_not_see_encrypted_key"; @@ -372,7 +372,7 @@ by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); (*yes: delete a useless induction hypothesis; apply unicity of session keys*) by (thin_tac "?P-->?Q" 1); -by (forward_tac [Gets_imp_Says] 1 THEN assume_tac 1); +by (ftac Gets_imp_Says 1 THEN assume_tac 1); by (not_bad_tac "Aa" 1); by (blast_tac (claset() addSDs [A_trusts_YM3, B_trusts_YM4_shrK] addDs [unique_session_keys]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Auth/Yahalom_Bad.ML --- a/src/HOL/Auth/Yahalom_Bad.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Auth/Yahalom_Bad.ML Tue Sep 07 10:40:58 1999 +0200 @@ -35,7 +35,7 @@ AddDs [Gets_imp_knows_Spy RS parts.Inj]; fun g_not_bad_tac s = - forward_tac [Gets_imp_Says] THEN' assume_tac THEN' not_bad_tac s; + ftac Gets_imp_Says THEN' assume_tac THEN' not_bad_tac s; (**** Inductive proofs about yahalom ****) @@ -55,7 +55,7 @@ (*For proving the easier theorems about X ~: parts (knows Spy evs).*) fun parts_knows_Spy_tac i = EVERY - [forward_tac [YM4_parts_knows_Spy] (i+6), assume_tac (i+6), + [ftac YM4_parts_knows_Spy (i+6), assume_tac (i+6), prove_simple_subgoals_tac i]; (*Induction for regularity theorems. If induction formula has the form @@ -107,7 +107,7 @@ (*For proofs involving analz.*) val analz_knows_Spy_tac = - forward_tac [YM4_analz_knows_Spy] 7 THEN assume_tac 7; + ftac YM4_analz_knows_Spy 7 THEN assume_tac 7; (**** The following is to prove theorems of the form @@ -291,7 +291,7 @@ by (dtac B_trusts_YM4_newK 3); by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); by (etac Spy_not_see_encrypted_key 1 THEN REPEAT (assume_tac 1)); -by (forward_tac [unique_session_keys] 1 THEN REPEAT (assume_tac 1)); +by (ftac unique_session_keys 1 THEN REPEAT (assume_tac 1)); by (blast_tac (claset() addDs []) 1); qed "B_trusts_YM4"; @@ -348,7 +348,7 @@ \ : set evs; \ \ A ~: bad; B ~: bad; evs : yahalom |] \ \ ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs"; -by (forward_tac [B_trusts_YM4] 1); +by (ftac B_trusts_YM4 1); by (REPEAT_FIRST assume_tac); by (etac (Gets_imp_knows_Spy RS parts.Inj RS MPair_parts) 1 THEN assume_tac 1); by (Clarify_tac 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Divides.ML --- a/src/HOL/Divides.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Divides.ML Tue Sep 07 10:40:58 1999 +0200 @@ -438,14 +438,14 @@ AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2]; Goal "k dvd (n + k) = k dvd (n::nat)"; -br iffI 1; -be dvd_add 2; -br dvd_refl 2; +by (rtac iffI 1); +by (etac dvd_add 2); +by (rtac dvd_refl 2); by (subgoal_tac "n = (n+k)-k" 1); by (Simp_tac 2); -be ssubst 1; -be dvd_diff 1; -br dvd_refl 1; +by (etac ssubst 1); +by (etac dvd_diff 1); +by (rtac dvd_refl 1); qed "dvd_reduce"; Goalw [dvd_def] "[| f dvd m; f dvd n; 0 f dvd (m mod n)"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Finite.ML --- a/src/HOL/Finite.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Finite.ML Tue Sep 07 10:40:58 1999 +0200 @@ -341,7 +341,7 @@ by (Auto_tac); by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1); by (Auto_tac); -by (forward_tac [cardR_SucD] 1); +by (ftac cardR_SucD 1); by (Blast_tac 1); val lemma = result(); @@ -628,7 +628,7 @@ by (res_inst_tac [("A1", "Aa-{xb}"), ("f1","f")] (finite_imp_foldSet RS exE) 1); by (blast_tac (claset() addIs [foldSet_imp_finite, finite_Diff]) 1); -by (forward_tac [Diff1_foldSet] 1 THEN assume_tac 1); +by (ftac Diff1_foldSet 1 THEN assume_tac 1); by (subgoal_tac "ya = f xb x" 1); by (Blast_tac 2); by (subgoal_tac "(Ab - {xa}, x) : foldSet f e" 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Hoare/Arith2.ML --- a/src/HOL/Hoare/Arith2.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Hoare/Arith2.ML Tue Sep 07 10:40:58 1999 +0200 @@ -36,7 +36,7 @@ (*** gcd ***) Goalw [gcd_def] "0 n = gcd n n"; -by (forward_tac [cd_nnn] 1); +by (ftac cd_nnn 1); by (rtac (select_equality RS sym) 1); by (blast_tac (claset() addDs [cd_le]) 1); by (blast_tac (claset() addIs [le_anti_sym] addDs [cd_le]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/IOA/IOA.ML --- a/src/HOL/IOA/IOA.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/IOA/IOA.ML Tue Sep 07 10:40:58 1999 +0200 @@ -70,7 +70,7 @@ by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1); by (etac disjE 1); by (Asm_simp_tac 1); - by (forward_tac [less_not_sym] 1); + by (ftac less_not_sym 1); by (asm_simp_tac (simpset() addsimps [less_not_refl2,less_Suc_eq]) 1); qed "reachable_n"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/IOA/Solve.ML --- a/src/HOL/IOA/Solve.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/IOA/Solve.ML Tue Sep 07 10:40:58 1999 +0200 @@ -29,7 +29,7 @@ by (asm_simp_tac (simpset() addsimps [mk_trace_def,filter_oseq_idemp])1); (* Use lemma *) - by (forward_tac [states_of_exec_reachable] 1); + by (ftac states_of_exec_reachable 1); (* Now show that it's an execution *) by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Induct/LFilter.ML --- a/src/HOL/Induct/LFilter.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Induct/LFilter.ML Tue Sep 07 10:40:58 1999 +0200 @@ -47,7 +47,7 @@ \ !!x l'. [| (l, LCons x l') : findRel p; p x |] ==> Q \ \ |] ==> Q"; by (rtac (major RS DomainE) 1); -by (forward_tac [findRel_imp_LCons] 1); +by (ftac findRel_imp_LCons 1); by (REPEAT (eresolve_tac [exE,conjE] 1)); by (hyp_subst_tac 1); by (REPEAT (ares_tac prems 1)); @@ -331,7 +331,7 @@ by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3); by (Asm_simp_tac 2); by (etac Domain_findRelE 1); -by (forward_tac [lmap_LCons_findRel] 1); +by (ftac lmap_LCons_findRel 1); by (Clarify_tac 1); by (Asm_simp_tac 1); qed "lfilter_lmap"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Induct/Multiset.ML --- a/src/HOL/Induct/Multiset.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Induct/Multiset.ML Tue Sep 07 10:40:58 1999 +0200 @@ -307,7 +307,7 @@ by (rtac ext 1); by (Force_tac 1); by (Clarify_tac 1); -by (forward_tac [setsum_SucD] 1); +by (ftac setsum_SucD 1); by (assume_tac 1); by (Clarify_tac 1); by (rename_tac "a" 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Induct/Mutil.ML --- a/src/HOL/Induct/Mutil.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Induct/Mutil.ML Tue Sep 07 10:40:58 1999 +0200 @@ -103,7 +103,7 @@ by (res_inst_tac [("k1", "i+j")] (mod2_cases RS disjE) 1); by (REPEAT_FIRST assume_tac); (*Four similar cases: case (i+j) mod 2 = b, 2#-b, ...*) -by(auto_tac (claset(), simpset() addsimps [less_Suc_eq, mod_Suc])); +by (auto_tac (claset(), simpset() addsimps [less_Suc_eq, mod_Suc])); qed "domino_singleton"; Goal "d:domino ==> finite d"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Integ/IntDiv.ML --- a/src/HOL/Integ/IntDiv.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Integ/IntDiv.ML Tue Sep 07 10:40:58 1999 +0200 @@ -360,7 +360,7 @@ qed "self_quotient"; Goal "[| quorem((a,a),(q,r)); a ~= (#0::int) |] ==> r = #0"; -by (forward_tac [self_quotient] 1); +by (ftac self_quotient 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [quorem_def]) 1); qed "self_remainder"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/MiniML/Instance.ML --- a/src/HOL/MiniML/Instance.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/MiniML/Instance.ML Tue Sep 07 10:40:58 1999 +0200 @@ -127,7 +127,7 @@ by (simp_tac (simpset() addsimps [le_type_scheme_def2]) 1); by (rtac iffI 1); by (etac exE 1); -by (forward_tac [bound_scheme_inst_type] 1); +by (ftac bound_scheme_inst_type 1); by (etac exE 1); by (rtac exI 1); by (rtac mk_scheme_injective 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/MiniML/W.ML --- a/src/HOL/MiniML/W.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/MiniML/W.ML Tue Sep 07 10:40:58 1999 +0200 @@ -211,7 +211,7 @@ by (asm_full_simp_tac (simpset() addsimps [rotate_Some,o_def]) 1); by (dtac W_var_geD 1); by (dtac W_var_geD 1); -by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); +by ( (ftac less_le_trans 1) THEN (assume_tac 1) ); by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, less_le_trans,less_not_refl2,subsetD] @@ -220,7 +220,7 @@ by (Asm_full_simp_tac 1); by (dtac (sym RS W_var_geD) 1); by (dtac (sym RS W_var_geD) 1); -by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); +by ( (ftac less_le_trans 1) THEN (assume_tac 1) ); by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, free_tv_app_subst_te RS subsetD,free_tv_app_subst_scheme_list RS subsetD, less_le_trans,subsetD] @@ -296,11 +296,11 @@ by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1); by (asm_full_simp_tac (simpset() addsimps [subst_comp_scheme_list RS sym,o_def,has_type_cl_sub,eq_sym_conv]) 1); by (rtac (has_type_cl_sub RS spec) 1); -by (forward_tac [new_tv_W] 1); +by (ftac new_tv_W 1); by (assume_tac 1); by (dtac conjunct1 1); by (dtac conjunct1 1); -by (forward_tac [new_tv_subst_scheme_list] 1); +by (ftac new_tv_subst_scheme_list 1); by (rtac new_scheme_list_le 1); by (rtac W_var_ge 1); by (assume_tac 1); @@ -340,11 +340,11 @@ by (dres_inst_tac [("x","t")] spec 2); by (dres_inst_tac [("x","n2")] spec 2); by (dres_inst_tac [("x","m2")] spec 2); -by (forward_tac [new_tv_W] 2); +by (ftac new_tv_W 2); by (assume_tac 2); by (dtac conjunct1 2); by (dtac conjunct1 2); -by (forward_tac [new_tv_subst_scheme_list] 2); +by (ftac new_tv_subst_scheme_list 2); by (rtac new_scheme_list_le 2); by (rtac W_var_ge 2); by (assume_tac 2); @@ -442,7 +442,7 @@ new_tv_not_free_tv,new_tv_le]) 3); by (case_tac "na:free_tv Sa" 2); (* n1 ~: free_tv S1 *) -by (forward_tac [not_free_impl_id] 3); +by (ftac not_free_impl_id 3); by (Asm_simp_tac 3); (* na : free_tv Sa *) by (dres_inst_tac [("A1","$ S A")] (subst_comp_scheme_list RSN (2,trans)) 2); @@ -456,7 +456,7 @@ by (rtac eq_free_eq_subst_te 2); by (strip_tac 2); by (subgoal_tac "nb ~= ma" 2); -by ((forward_tac [new_tv_W] 3) THEN (atac 3)); +by ((ftac new_tv_W 3) THEN (atac 3)); by (etac conjE 3); by (dtac new_tv_subst_scheme_list 3); by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 3); @@ -467,7 +467,7 @@ by (rtac eq_free_eq_subst_te 2); by (strip_tac 2 ); by (subgoal_tac "na ~= ma" 2); -by ((forward_tac [new_tv_W] 3) THEN (atac 3)); +by ((ftac new_tv_W 3) THEN (atac 3)); by (etac conjE 3); by (dtac (sym RS W_var_geD) 3); by (fast_tac (HOL_cs addDs [new_scheme_list_le,new_tv_subst_scheme_list,new_tv_W,new_tv_not_free_tv]) 3); @@ -502,7 +502,7 @@ by (rtac eq_free_eq_subst_scheme_list 1); by ( safe_tac HOL_cs ); by (subgoal_tac "ma ~= na" 1); -by ((forward_tac [new_tv_W] 2) THEN (atac 2)); +by ((ftac new_tv_W 2) THEN (atac 2)); by (etac conjE 2); by (dtac new_tv_subst_scheme_list 2); by (fast_tac (HOL_cs addIs [new_scheme_list_le] addDs [sym RS W_var_geD]) 2); @@ -542,7 +542,7 @@ by (Simp_tac 1); by (rtac gen_bound_typ_instance 1); by (dtac mp 1); -by (forward_tac [new_tv_compatible_W] 1); +by (ftac new_tv_compatible_W 1); by (rtac sym 1); by (assume_tac 1); by (fast_tac (claset() addDs [new_tv_compatible_gen,new_tv_subst_scheme_list,new_tv_W]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Real/Hyperreal/Filter.ML --- a/src/HOL/Real/Hyperreal/Filter.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Real/Hyperreal/Filter.ML Tue Sep 07 10:40:58 1999 +0200 @@ -274,7 +274,7 @@ by (dres_inst_tac [("A","xa")] mem_FiltersetD3 2 THEN assume_tac 2); by (Blast_tac 2); by (dtac lemma_empty_Int_subset_Compl 1); -by (EVERY1[forward_tac [mem_Filterset_disjI], assume_tac, Fast_tac]); +by (EVERY1[ftac mem_Filterset_disjI , assume_tac, Fast_tac]); by (dtac mem_FiltersetD3 1 THEN assume_tac 1); by (dres_inst_tac [("x","f")] spec 1); by (Blast_tac 1); @@ -387,7 +387,7 @@ Goalw [Ultrafilter_def,FreeUltrafilter_def] "[| ~finite(UNIV :: 'a set); (U :: 'a set set): FreeUltrafilter UNIV\ \ |] ==> {X. finite(- X)} <= U"; -by (forward_tac [cofinite_Filter] 1); +by (ftac cofinite_Filter 1); by (Step_tac 1); by (forw_inst_tac [("X","- x :: 'a set")] not_finite_UNIV_Compl 1); by (assume_tac 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Real/Hyperreal/HyperDef.ML --- a/src/HOL/Real/Hyperreal/HyperDef.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Real/Hyperreal/HyperDef.ML Tue Sep 07 10:40:58 1999 +0200 @@ -1096,7 +1096,7 @@ by (dtac (hypreal_minus_zero_less_iff RS iffD2) 2); by (dres_inst_tac [("R2.0","-x")] hypreal_less_trans 2); by (Auto_tac ); -by (forward_tac [hypreal_add_order] 1 THEN assume_tac 1); +by (ftac hypreal_add_order 1 THEN assume_tac 1); by (dres_inst_tac [("C","-x"),("B","x + x")] hypreal_add_less_mono1 1); by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); qed "hypreal_gt_zero_iff"; @@ -1318,7 +1318,7 @@ qed "hypreal_hrinv_gt_zero"; Goal "x < 0hr ==> hrinv x < 0hr"; -by (forward_tac [hypreal_not_refl2] 1); +by (ftac hypreal_not_refl2 1); by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1); by (dtac (hypreal_minus_hrinv RS sym) 1); @@ -1394,13 +1394,13 @@ (* TODO: remove redundant 0hr < x *) Goal "[| 0hr < r; 0hr < x; r < x |] ==> hrinv x < hrinv r"; -by (forward_tac [hypreal_hrinv_gt_zero] 1); +by (ftac hypreal_hrinv_gt_zero 1); by (forw_inst_tac [("x","x")] hypreal_hrinv_gt_zero 1); by (forw_inst_tac [("x","r"),("z","hrinv r")] hypreal_mult_less_mono1 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS not_sym RS hypreal_mult_hrinv]) 1); -by (forward_tac [hypreal_hrinv_gt_zero] 1); +by (ftac hypreal_hrinv_gt_zero 1); by (forw_inst_tac [("x","1hr"),("z","hrinv x")] hypreal_mult_less_mono2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [hypreal_not_refl2 RS diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Real/Hyperreal/Zorn.ML --- a/src/HOL/Real/Hyperreal/Zorn.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Real/Hyperreal/Zorn.ML Tue Sep 07 10:40:58 1999 +0200 @@ -177,7 +177,7 @@ Goal "c: chain S - maxchain S ==> \ \ succ S c ~= c"; -by (forward_tac [succI3] 1); +by (ftac succI3 1); by (Asm_simp_tac 1); by (rtac select_not_equals 1); by (assume_tac 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Real/PReal.ML --- a/src/HOL/Real/PReal.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Real/PReal.ML Tue Sep 07 10:40:58 1999 +0200 @@ -247,7 +247,7 @@ Goal "!y: {w. ? x: Rep_preal R. ? y: Rep_preal S. w = x + y}. \ \ !z. z < y --> z : {w. ? x:Rep_preal R. ? y:Rep_preal S. w = x + y}"; by Auto_tac; -by (forward_tac [prat_mult_qinv_less_1] 1); +by (ftac prat_mult_qinv_less_1 1); by (forw_inst_tac [("x","x"),("q2.0","prat_of_pnat (Abs_pnat 1)")] prat_mult_less2_mono1 1); by (forw_inst_tac [("x","ya"),("q2.0","prat_of_pnat (Abs_pnat 1)")] @@ -658,7 +658,7 @@ by (etac prat_lessE 1); by (cut_inst_tac [("R","A"),("x","Q3")] lemma_gleason9_34 1); by (dtac sym 1 THEN Auto_tac ); -by (forward_tac [not_in_preal_ub] 1); +by (ftac not_in_preal_ub 1); by (dres_inst_tac [("x","xa + Q3")] bspec 1 THEN assume_tac 1); by (dtac prat_add_right_less_cancel 1); by (dres_inst_tac [("x","qinv(xa)*Q3")] prat_mult_less2_mono1 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Real/RComplete.ML --- a/src/HOL/Real/RComplete.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Real/RComplete.ML Tue Sep 07 10:40:58 1999 +0200 @@ -28,7 +28,7 @@ by (blast_tac (claset() addDs [bspec, real_gt_zero_preal_Ex RS iffD1]) 1); by Auto_tac; by (dtac bspec 1 THEN assume_tac 1); -by (forward_tac [bspec] 1 THEN assume_tac 1); +by (ftac bspec 1 THEN assume_tac 1); by (dtac real_less_trans 1 THEN assume_tac 1); by (dtac (real_gt_zero_preal_Ex RS iffD1) 1 THEN etac exE 1); by (res_inst_tac [("x","ya")] exI 1); @@ -49,22 +49,22 @@ by (res_inst_tac [("x","real_of_preal (psup({w. real_of_preal w : P}))")] exI 1); by Auto_tac; -by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac); +by (ftac real_sup_lemma2 1 THEN Auto_tac); by (case_tac "0r < ya" 1); by (dtac (real_gt_zero_preal_Ex RS iffD1) 1); by (dtac real_less_all_real2 2); by Auto_tac; by (rtac (preal_complete RS spec RS iffD1) 1); by Auto_tac; -by (forward_tac [real_gt_preal_preal_Ex] 1); +by (ftac real_gt_preal_preal_Ex 1); by Auto_tac; (* second part *) by (rtac (real_sup_lemma1 RS iffD2) 1 THEN assume_tac 1); by (case_tac "0r < ya" 1); by (auto_tac (claset() addSDs [real_less_all_real2, real_gt_zero_preal_Ex RS iffD1],simpset())); -by (forward_tac [real_sup_lemma2] 2 THEN Auto_tac); -by (forward_tac [real_sup_lemma2] 1 THEN Auto_tac); +by (ftac real_sup_lemma2 2 THEN Auto_tac); +by (ftac real_sup_lemma2 1 THEN Auto_tac); by (rtac (preal_complete RS spec RS iffD2 RS bexE) 1); by (Blast_tac 3); by (Blast_tac 1); @@ -77,7 +77,7 @@ -------------------------------------------------------*) Goal "[| isLub R S x; isLub R S y |] ==> x = (y::real)"; -by (forward_tac [isLub_isUb] 1); +by (ftac isLub_isUb 1); by (forw_inst_tac [("x","y")] isLub_isUb 1); by (blast_tac (claset() addSIs [real_le_anti_sym] addSDs [isLub_le_isUb]) 1); @@ -105,12 +105,12 @@ by (auto_tac (claset(), simpset() addsimps [real_of_preal_le_iff])); by (rtac preal_psup_leI2a 1); by (forw_inst_tac [("y","real_of_preal ya")] setleD 1 THEN assume_tac 1); -by (forward_tac [real_ge_preal_preal_Ex] 1); +by (ftac real_ge_preal_preal_Ex 1); by (Step_tac 1); by (res_inst_tac [("x","y")] exI 1); by (blast_tac (claset() addSDs [setleD] addIs [real_of_preal_le_iff RS iffD1]) 1); by (forw_inst_tac [("x","x")] bspec 1 THEN assume_tac 1); -by (forward_tac [isUbD2] 1); +by (ftac isUbD2 1); by (dtac (real_gt_zero_preal_Ex RS iffD1) 1); by (auto_tac (claset() addSDs [isUbD, real_ge_preal_preal_Ex], simpset() addsimps [real_of_preal_le_iff])); @@ -188,12 +188,12 @@ by (Step_tac 1); by (res_inst_tac [("R1.0","x"),("R2.0","y")] real_linear_less2 1); by (stac lemma_le_swap2 1); -by (forward_tac [isLubD2] 1 THEN assume_tac 2); +by (ftac isLubD2 1 THEN assume_tac 2); by (Step_tac 1); by (Blast_tac 1); by (dtac lemma_real_complete1 1 THEN REPEAT(assume_tac 1)); by (stac lemma_le_swap2 1); -by (forward_tac [isLubD2] 1 THEN assume_tac 2); +by (ftac isLubD2 1 THEN assume_tac 2); by (Blast_tac 1); by (rtac lemma_real_complete2b 1); by (etac real_less_imp_le 2); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Real/RealDef.ML --- a/src/HOL/Real/RealDef.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Real/RealDef.ML Tue Sep 07 10:40:58 1999 +0200 @@ -498,7 +498,7 @@ qed "real_mult_inv_left_ex"; Goalw [rinv_def] "x ~= 0r ==> rinv(x)*x = 1r"; -by (forward_tac [real_mult_inv_left_ex] 1); +by (ftac real_mult_inv_left_ex 1); by (Step_tac 1); by (rtac selectI2 1); by Auto_tac; @@ -531,7 +531,7 @@ qed "real_mult_right_cancel_ccontr"; Goalw [rinv_def] "x ~= 0r ==> rinv(x) ~= 0r"; -by (forward_tac [real_mult_inv_left_ex] 1); +by (ftac real_mult_inv_left_ex 1); by (etac exE 1); by (rtac selectI2 1); by (auto_tac (claset(), diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Real/RealOrd.ML --- a/src/HOL/Real/RealOrd.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Real/RealOrd.ML Tue Sep 07 10:40:58 1999 +0200 @@ -353,7 +353,7 @@ qed "real_rinv_gt_zero"; Goal "x < 0r ==> rinv x < 0r"; -by (forward_tac [real_not_refl2] 1); +by (ftac real_not_refl2 1); by (dtac (real_minus_zero_less_iff RS iffD2) 1); by (rtac (real_minus_zero_less_iff RS iffD1) 1); by (dtac (real_minus_rinv RS sym) 1); @@ -608,14 +608,14 @@ qed "real_of_posnat_rinv_eq_iff"; Goal "[| 0r < r; r < x |] ==> rinv x < rinv r"; -by (forward_tac [real_less_trans] 1 THEN assume_tac 1); -by (forward_tac [real_rinv_gt_zero] 1); +by (ftac real_less_trans 1 THEN assume_tac 1); +by (ftac real_rinv_gt_zero 1); by (forw_inst_tac [("x","x")] real_rinv_gt_zero 1); by (forw_inst_tac [("x","r"),("z","rinv r")] real_mult_less_mono1 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS not_sym RS real_mult_inv_right]) 1); -by (forward_tac [real_rinv_gt_zero] 1); +by (ftac real_rinv_gt_zero 1); by (forw_inst_tac [("x","1r"),("z","rinv x")] real_mult_less_mono2 1); by (assume_tac 1); by (asm_full_simp_tac (simpset() addsimps [real_not_refl2 RS @@ -704,7 +704,7 @@ Addsimps [real_mult_eq_self_zero2]; Goal "[| 0r <= x*y; 0r < x |] ==> 0r <= y"; -by (forward_tac [real_rinv_gt_zero] 1); +by (ftac real_rinv_gt_zero 1); by (dres_inst_tac [("x","rinv x")] real_less_le_mult_order 1); by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2); by (auto_tac (claset(), diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Set.ML --- a/src/HOL/Set.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Set.ML Tue Sep 07 10:40:58 1999 +0200 @@ -466,7 +466,7 @@ Goal "A <= insert x B ==> A <= B & x ~: A | (? B'. A = insert x B' & B' <= B)"; by (case_tac "x:A" 1); by (Fast_tac 2); -br disjI2 1; +by (rtac disjI2 1); by (res_inst_tac [("x","A-{x}")] exI 1); by (Fast_tac 1); qed "subset_insertD"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Subst/UTerm.ML --- a/src/HOL/Subst/UTerm.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Subst/UTerm.ML Tue Sep 07 10:40:58 1999 +0200 @@ -39,7 +39,7 @@ Goal "finite(vars_of M)"; by (induct_tac"M" 1); by (ALLGOALS Simp_tac); -by (forward_tac [finite_UnI] 1); +by (ftac finite_UnI 1); by (assume_tac 1); by (Asm_simp_tac 1); val finite_vars_of = result(); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Tue Sep 07 10:40:58 1999 +0200 @@ -570,7 +570,7 @@ [rtac iffI 1, REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2, dresolve_tac rep_congs 1, dtac box_equals 1, - REPEAT (resolve_tac rep_thms 1), rewrite_goals_tac [o_def], + REPEAT (resolve_tac rep_thms 1), rewtac o_def, REPEAT (eresolve_tac inj_thms 1), REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1, eresolve_tac inj_thms 1, atac 1]))]) @@ -634,7 +634,7 @@ EVERY (map (fn (prem, r) => (EVERY [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1), simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1, - DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewrite_goals_tac [o_def], + DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def, rtac allI 1, dtac FunsD 1, etac CollectD 1]))])) (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/UNITY/Channel.ML --- a/src/HOL/UNITY/Channel.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/UNITY/Channel.ML Tue Sep 07 10:40:58 1999 +0200 @@ -51,7 +51,7 @@ Goal "!!y::nat. F : (UNIV-{{}}) leadsTo {s. y ~: s}"; by (rtac (lemma RS leadsTo_weaken_R) 1); by (Clarify_tac 1); -by (forward_tac [minSet_nonempty] 1); +by (ftac minSet_nonempty 1); by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least], simpset())); qed "Channel_progress"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/UNITY/Extend.ML --- a/src/HOL/UNITY/Extend.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/UNITY/Extend.ML Tue Sep 07 10:40:58 1999 +0200 @@ -29,7 +29,7 @@ val [surj,prem] = Goalw [inv_def] "[| surj h; !! x y. g (h(x,y)) = x |] ==> fst (inv h z) = g z"; by (res_inst_tac [("y1", "z")] (surj RS surjD RS exE) 1); -br selectI2 1; +by (rtac selectI2 1); by (dres_inst_tac [("f", "g")] arg_cong 2); by (auto_tac (claset(), simpset() addsimps [prem])); qed "fst_inv_equalityI"; @@ -200,9 +200,9 @@ Goalw [project_set_def, project_act_def] "Domain (project_act h act) = project_set h (Domain act)"; -auto(); +by Auto_tac; by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1); -auto(); +by Auto_tac; qed "Domain_project_act"; Addsimps [extend_act_Id, project_act_Id]; @@ -562,8 +562,8 @@ Goal "F : transient (extend_set h A) ==> project h F : transient A"; by (auto_tac (claset(), simpset() addsimps [transient_def, Domain_project_act])); -br bexI 1; -ba 2; +by (rtac bexI 1); +by (assume_tac 2); by (full_simp_tac (simpset() addsimps [extend_set_def, project_set_def, project_act_def]) 1); by (Blast_tac 1); @@ -577,8 +577,8 @@ \ ==> F : transient (extend_set h A)"; by (auto_tac (claset(), simpset() addsimps [transient_def, Domain_project_act])); -br bexI 1; -ba 2; +by (rtac bexI 1); +by (assume_tac 2); by Auto_tac; by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1); by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/UNITY/GenPrefix.ML --- a/src/HOL/UNITY/GenPrefix.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/UNITY/GenPrefix.ML Tue Sep 07 10:40:58 1999 +0200 @@ -136,7 +136,7 @@ Goal "[| reflexive r; (xs,ys) : genPrefix r |] \ \ ==> (xs@zs, take (length xs) ys @ zs) : genPrefix r"; by (etac genPrefix.induct 1); -by (forward_tac [genPrefix_length_le] 3); +by (ftac genPrefix_length_le 3); by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_is_0_eq RS iffD2]))); qed "genPrefix_take_append"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/UNITY/Lift_prog.ML --- a/src/HOL/UNITY/Lift_prog.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/UNITY/Lift_prog.ML Tue Sep 07 10:40:58 1999 +0200 @@ -507,7 +507,7 @@ Goal "fst (inv (lift_map i) g) = g i"; -br (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1; +by (rtac (good_map_lift_map RS good_map_is_surj RS fst_inv_equalityI) 1); by (auto_tac (claset(), simpset() addsimps [lift_map_def])); qed "fst_inv_lift_map"; Addsimps [fst_inv_lift_map]; @@ -520,34 +520,34 @@ Goalw [drop_set_def, project_set_def, lift_map_def] "drop_set i A = project_set (lift_map i) A"; -auto(); -br image_eqI 2; -br exI 1; +by Auto_tac; +by (rtac image_eqI 2); +by (rtac exI 1); by (stac (refl RS fun_upd_idem) 1); -auto(); +by Auto_tac; qed "drop_set_correct"; Goal "lift_act i = extend_act (lift_map i)"; -br ext 1; +by (rtac ext 1); by Auto_tac; by (forward_tac [good_map_lift_map RS export extend_act_D] 2); -by(Full_simp_tac 2); -bws [extend_act_def, lift_map_def]; +by (Full_simp_tac 2); +by (rewrite_goals_tac [extend_act_def, lift_map_def]); by Auto_tac; -br bexI 1; -ba 2; -auto(); -br exI 1; -auto(); +by (rtac bexI 1); +by (assume_tac 2); +by Auto_tac; +by (rtac exI 1); +by Auto_tac; qed "lift_act_correct"; Goal "drop_act i = project_act (lift_map i)"; -br ext 1; -bws [project_act_def, drop_act_def, lift_map_def]; +by (rtac ext 1); +by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]); by Auto_tac; -br image_eqI 2; +by (rtac image_eqI 2); by (REPEAT (rtac exI 1 ORELSE stac (refl RS fun_upd_idem) 1)); -auto(); +by Auto_tac; qed "drop_act_correct"; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/W0/I.ML --- a/src/HOL/W0/I.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/W0/I.ML Tue Sep 07 10:40:58 1999 +0200 @@ -63,7 +63,7 @@ by (etac exE 1); by (etac conjE 1); by (etac impE 1); - by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); + by ((ftac new_tv_subst_tel 1) THEN (atac 1)); by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] addss simpset()) 1); @@ -78,7 +78,7 @@ by (etac exE 1); by (etac conjE 1); by (etac impE 1); - by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); + by ((ftac new_tv_subst_tel 1) THEN (atac 1)); by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] addss simpset()) 1); @@ -90,7 +90,7 @@ by (etac exE 1); by (etac conjE 1); by (etac impE 1); - by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); + by ((ftac new_tv_subst_tel 1) THEN (atac 1)); by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); by (fast_tac (HOL_cs addDs [sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] addss simpset()) 1); @@ -102,7 +102,7 @@ (** LEVEL 70 **) by (subgoal_tac "new_tv n2 s & new_tv n2 r & new_tv n2 ra" 1); by (asm_full_simp_tac (simpset() addsimps [new_tv_subst]) 1); -by ((forward_tac [new_tv_subst_tel] 1) THEN (atac 1)); +by ((ftac new_tv_subst_tel 1) THEN (atac 1)); by ((dres_inst_tac [("a","$ s a")] new_tv_W 1) THEN (atac 1)); by (safe_tac HOL_cs); by (best_tac (HOL_cs addDs[sym RS W_var_geD,new_tv_subst_le,new_tv_list_le] diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/W0/W.ML --- a/src/HOL/W0/W.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/W0/W.ML Tue Sep 07 10:40:58 1999 +0200 @@ -189,7 +189,7 @@ by (asm_full_simp_tac (simpset() addsimps [rotate_Ok,o_def]) 1); by (dtac W_var_geD 1); by (dtac W_var_geD 1); -by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); +by ( (ftac less_le_trans 1) THEN (assume_tac 1) ); (** LEVEL 33 **) by (fast_tac (HOL_cs addDs [free_tv_comp_subst RS subsetD,sym RS mgu_free, codD,free_tv_app_subst_te RS subsetD,free_tv_app_subst_tel RS subsetD, @@ -199,7 +199,7 @@ by (Asm_full_simp_tac 1); by (dtac (sym RS W_var_geD) 1); by (dtac (sym RS W_var_geD) 1); -by ( (forward_tac [less_le_trans] 1) THEN (assume_tac 1) ); +by ( (ftac less_le_trans 1) THEN (assume_tac 1) ); by (fast_tac (HOL_cs addDs [mgu_free, codD,free_tv_subst_var RS subsetD, free_tv_app_subst_te RS subsetD, free_tv_app_subst_tel RS subsetD, @@ -269,7 +269,7 @@ (** LEVEL 35 **) by (case_tac "na:free_tv sa" 2); (* na ~: free_tv sa *) -by (forward_tac [not_free_impl_id] 3); +by (ftac not_free_impl_id 3); by (Asm_simp_tac 3); (* na : free_tv sa *) by (dres_inst_tac [("ts1","$ s a")] (subst_comp_tel RSN (2,trans)) 2); @@ -284,7 +284,7 @@ by (rtac eq_free_eq_subst_te 2); by (strip_tac 2); by (subgoal_tac "nb ~= ma" 2); -by ((forward_tac [new_tv_W] 3) THEN (atac 3)); +by ((ftac new_tv_W 3) THEN (atac 3)); by (etac conjE 3); by (dtac new_tv_subst_tel 3); by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 3); @@ -297,7 +297,7 @@ by (rtac eq_free_eq_subst_te 2); by (strip_tac 2 ); by (subgoal_tac "na ~= ma" 2); -by ((forward_tac [new_tv_W] 3) THEN (atac 3)); +by ((ftac new_tv_W 3) THEN (atac 3)); by (etac conjE 3); by (dtac (sym RS W_var_geD) 3); by (fast_tac (HOL_cs addDs [new_tv_list_le,new_tv_subst_tel,new_tv_W,new_tv_not_free_tv]) 3); @@ -331,7 +331,7 @@ by (rtac eq_free_eq_subst_tel 1); by ( safe_tac HOL_cs ); by (subgoal_tac "ma ~= na" 1); -by ((forward_tac [new_tv_W] 2) THEN (atac 2)); +by ((ftac new_tv_W 2) THEN (atac 2)); by (etac conjE 2); by (dtac new_tv_subst_tel 2); by (fast_tac (HOL_cs addIs [new_tv_list_le] addDs [sym RS W_var_geD]) 2); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/WF.ML --- a/src/HOL/WF.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/WF.ML Tue Sep 07 10:40:58 1999 +0200 @@ -326,8 +326,8 @@ by (rtac impI 1); by (res_inst_tac [("a1","a")] (th RS ssubst) 1); by (assume_tac 1); -by (forward_tac [wf_trancl] 1); -by (forward_tac [r_into_trancl] 1); +by (ftac wf_trancl 1); +by (ftac r_into_trancl 1); by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1); by (rtac H_cong2 1); (*expose the equality of cuts*) by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/ex/MT.ML --- a/src/HOL/ex/MT.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/ex/MT.ML Tue Sep 07 10:40:58 1999 +0200 @@ -639,7 +639,7 @@ by (dtac elab_fix_elim 1); by (safe_tac HOL_cs); (*Do a single unfolding of cl*) -by ((forward_tac [ssubst] 1) THEN (assume_tac 2)); +by ((ftac ssubst 1) THEN (assume_tac 2)); by (rtac hasty_rel_clos_coind 1); by (etac elab_fn 1); by (asm_simp_tac (simpset() addsimps [ve_dom_owr, te_dom_owr]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOL/ex/Tarski.ML --- a/src/HOL/ex/Tarski.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOL/ex/Tarski.ML Tue Sep 07 10:40:58 1999 +0200 @@ -486,7 +486,7 @@ by (etac ssubst 1); by (Simp_tac 1); by (rtac conjI 1); -by (forward_tac [fixfE2] 1); +by (ftac fixfE2 1); by (etac ssubst 1); by (rtac reflE 1); by (rtac CompleteLatticeE11 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/Cont.ML --- a/src/HOLCF/Cont.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOLCF/Cont.ML Tue Sep 07 10:40:58 1999 +0200 @@ -675,7 +675,7 @@ by ( atac 1); by (rtac contlubI 1); by (strip_tac 1); -by (forward_tac [chfin2finch] 1); +by (ftac chfin2finch 1); by (rtac antisym_less 1); by ( force_tac (HOL_cs addIs [is_ub_thelub,ch2ch_monofun], HOL_ss addsimps [finite_chain_def,maxinch_is_thelub]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/IOA/NTP/Correctness.ML --- a/src/HOLCF/IOA/NTP/Correctness.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOLCF/IOA/NTP/Correctness.ML Tue Sep 07 10:40:58 1999 +0200 @@ -79,19 +79,19 @@ by (induct_tac "a" 1); by (ALLGOALS (asm_simp_tac ss')); -by (forward_tac [inv4] 1); +by (ftac inv4 1); by (Force_tac 1); -by (forward_tac [inv4] 1); -by (forward_tac [inv2] 1); +by (ftac inv4 1); +by (ftac inv2 1); by (etac disjE 1); by (Asm_simp_tac 1); by (Force_tac 1); -by (forward_tac [inv2] 1); +by (ftac inv2 1); by (etac disjE 1); -by (forward_tac [inv3] 1); +by (ftac inv3 1); by (case_tac "sq(sen(s))=[]" 1); by (asm_full_simp_tac ss' 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/IOA/meta_theory/Abstraction.ML --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML Tue Sep 07 10:40:58 1999 +0200 @@ -410,7 +410,7 @@ "[| temp_strengthening P Q h |]\ \ ==> temp_strengthening ([] P) ([] Q) h"; by (clarify_tac set_cs 1); -by (forward_tac [ex2seq_tsuffix] 1); +by (ftac ex2seq_tsuffix 1); by (clarify_tac set_cs 1); by (dres_inst_tac [("h","h")] cex_absSeq_tsuffix 1); by (asm_full_simp_tac (simpset() addsimps [ex2seq_abs_cex])1); diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/IOA/meta_theory/CompoTraces.ML --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Tue Sep 07 10:40:58 1999 +0200 @@ -483,8 +483,8 @@ by (safe_tac set_cs); (* Case a:A, a:B *) -by (forward_tac [divide_Seq] 1); -by (forward_tac [divide_Seq] 1); +by (ftac divide_Seq 1); +by (ftac divide_Seq 1); back(); by (REPEAT (etac conjE 1)); (* filtering internals of A in schA and of B in schB is nil *) @@ -501,7 +501,7 @@ ForallTL,ForallDropwhile]) 1); (* Case a:A, a~:B *) -by (forward_tac [divide_Seq] 1); +by (ftac divide_Seq 1); by (REPEAT (etac conjE 1)); (* filtering internals of A is nil *) by (asm_full_simp_tac (simpset() addsimps @@ -513,7 +513,7 @@ ForallTL,ForallDropwhile]) 1); (* Case a:B, a~:A *) -by (forward_tac [divide_Seq] 1); +by (ftac divide_Seq 1); by (REPEAT (etac conjE 1)); (* filtering internals of A is nil *) by (asm_full_simp_tac (simpset() addsimps diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/IOA/meta_theory/Deadlock.ML --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML Tue Sep 07 10:40:58 1999 +0200 @@ -14,7 +14,7 @@ \ ==> Filter (%x. x:act A)`sch @@ a>>nil : schedules A"; by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1); by (safe_tac set_cs); -by (forward_tac [inp_is_act] 1); +by (ftac inp_is_act 1); by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); by (pair_tac "ex" 1); ren "s ex" 1; @@ -25,7 +25,7 @@ by (assume_tac 2); by (etac FiniteFilter 2); (* subgoal 1 *) -by (forward_tac [exists_laststate] 1); +by (ftac exists_laststate 1); by (etac allE 1); by (etac exE 1); (* using input-enabledness *) diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/IOA/meta_theory/RefMappings.ML --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Tue Sep 07 10:40:58 1999 +0200 @@ -93,7 +93,7 @@ by (dtac sym 1); by (Asm_full_simp_tac 1); by (REPEAT (hyp_subst_tac 1)); -by (forward_tac [reachable_rename] 1); +by (ftac reachable_rename 1); by (Asm_full_simp_tac 1); (* x is output *) by (etac exE 1); @@ -102,10 +102,10 @@ by (dtac sym 1); by (Asm_full_simp_tac 1); by (REPEAT (hyp_subst_tac 1)); -by (forward_tac [reachable_rename] 1); +by (ftac reachable_rename 1); by (Asm_full_simp_tac 1); (* x is internal *) -by (forward_tac [reachable_rename] 1); +by (ftac reachable_rename 1); by Auto_tac; qed"rename_through_pmap"; Addsplits [split_if]; Addcongs [if_weak_cong]; diff -r 1e5585fd3632 -r 23e090051cb8 src/HOLCF/Sprod2.ML --- a/src/HOLCF/Sprod2.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/HOLCF/Sprod2.ML Tue Sep 07 10:40:58 1999 +0200 @@ -47,7 +47,7 @@ (strip_tac 1), (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), - (forward_tac [notUU_I] 1), + (ftac notUU_I 1), (atac 1), (REPEAT(asm_simp_tac(Sprod0_ss addsimps[inst_sprod_po,refl_less,minimal]) 1)) @@ -59,7 +59,7 @@ (strip_tac 1), (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1), (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1), - (forward_tac [notUU_I] 1), + (ftac notUU_I 1), (atac 1), (REPEAT(asm_simp_tac(Sprod0_ss addsimps[inst_sprod_po,refl_less,minimal]) 1)) diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/AC15_WO6.ML --- a/src/ZF/AC/AC15_WO6.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/AC15_WO6.ML Tue Sep 07 10:40:58 1999 +0200 @@ -24,7 +24,7 @@ \ ALL x GG ` v <= x"; -by (forward_tac [the_in_MM_subset] 1); -by (forward_tac [in_LL_eq_Int] 1); +by (ftac the_in_MM_subset 1); +by (ftac in_LL_eq_Int 1); by (force_tac (claset() addEs [equalityE], simpset()) 1); qed "GG_subset"; @@ -612,7 +612,7 @@ by (cut_facts_tac [lemma2] 1); by (REPEAT (eresolve_tac [exE, conjE] 1)); by (eres_inst_tac [("x","A Un y")] allE 1); -by (forward_tac [infinite_Un] 1 THEN (mp_tac 1)); +by (ftac infinite_Un 1 THEN (mp_tac 1)); by (etac zero_lt_natE 1); by (assume_tac 1); by (Clarify_tac 1); by (DEPTH_SOLVE (ares_tac [export conclusion] 1)); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/AC16_lemmas.ML --- a/src/ZF/AC/AC16_lemmas.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/AC16_lemmas.ML Tue Sep 07 10:40:58 1999 +0200 @@ -137,7 +137,7 @@ by (fast_tac (claset() addSEs [Diff_sing_eqpoll, Diff_sing_eqpoll RS eqpoll_succ_imp_not_empty]) 1); by (resolve_tac [Union_eq_Un RSN (2, subst_elem)] 1 THEN (assume_tac 2)); -by (forward_tac [bspec] 1 THEN (assume_tac 1)); +by (ftac bspec 1 THEN (assume_tac 1)); by (dresolve_tac [Diff_subset RS subsetD RSN (2, bspec)] 1 THEN (assume_tac 1)); by (dtac Un_Ord_disj 1 THEN (assume_tac 1)); by (etac DiffE 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/AC2_AC6.ML --- a/src/ZF/AC/AC2_AC6.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/AC2_AC6.ML Tue Sep 07 10:40:58 1999 +0200 @@ -138,7 +138,7 @@ by (rtac ballI 1); by (rtac apply_equality 1 THEN (assume_tac 2)); by (etac domainE 1); -by (forward_tac [range_type] 1 THEN (assume_tac 1)); +by (ftac range_type 1 THEN (assume_tac 1)); by (fast_tac (claset() addDs [apply_equality]) 1); qed "AC4_AC5"; @@ -164,7 +164,7 @@ Goal "[| EX f: A->C. P(f,domain(f)); A=B |] ==> EX f: B->C. P(f,B)"; by (etac bexE 1); -by (forward_tac [domain_of_fun] 1); +by (ftac domain_of_fun 1); by (Fast_tac 1); val lemma3 = result(); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/AC_Equiv.ML --- a/src/ZF/AC/AC_Equiv.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/AC_Equiv.ML Tue Sep 07 10:40:58 1999 +0200 @@ -36,8 +36,8 @@ goal Cardinal.thy "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m"; by (rtac not_emptyE 1 THEN (assume_tac 1)); -by (forward_tac [singleton_subsetI] 1); -by (forward_tac [subsetD] 1 THEN (assume_tac 1)); +by (ftac singleton_subsetI 1); +by (ftac subsetD 1 THEN (assume_tac 1)); by (res_inst_tac [("A2","A")] (Diff_sing_lepoll RSN (2, subset_imp_lepoll RS lepoll_trans)) 1 THEN (REPEAT (assume_tac 2))); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/DC.ML --- a/src/ZF/AC/DC.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/DC.ML Tue Sep 07 10:40:58 1999 +0200 @@ -214,7 +214,7 @@ by (etac conjE 1); by (resolve_tac [eqpoll_succ_imp_not_empty RS not_emptyE] 1 THEN (assume_tac 1)); -by (forward_tac [Diff_sing_eqpoll] 1 THEN (assume_tac 1)); +by (ftac Diff_sing_eqpoll 1 THEN (assume_tac 1)); by (etac allE 1); by (etac impE 1); by (Fast_tac 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/DC_lemmas.ML --- a/src/ZF/AC/DC_lemmas.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/DC_lemmas.ML Tue Sep 07 10:40:58 1999 +0200 @@ -97,7 +97,7 @@ qed "restrict_eq_imp_val_eq"; Goal "[| domain(f)=A; f:B->C |] ==> f:A->C"; -by (forward_tac [domain_of_fun] 1); +by (ftac domain_of_fun 1); by (Fast_tac 1); qed "domain_eq_imp_fun_type"; diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/HH.ML --- a/src/ZF/AC/HH.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/HH.ML Tue Sep 07 10:40:58 1999 +0200 @@ -186,7 +186,7 @@ Goal "[| f : (Pow(x)-{0}) -> {{z}. z:x}; \ \ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}"; by (dtac less_Least_subset_x 1); -by (forward_tac [HH_subset_imp_eq] 1); +by (ftac HH_subset_imp_eq 1); by (dtac apply_type 1); by (resolve_tac [Diff_subset RS PowI RS DiffI] 1); by (fast_tac diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/WO1_WO7.ML --- a/src/ZF/AC/WO1_WO7.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/WO1_WO7.ML Tue Sep 07 10:40:58 1999 +0200 @@ -72,7 +72,7 @@ by (REPEAT (resolve_tac [allI,impI] 1)); by (REPEAT (eresolve_tac [allE,exE] 1)); by (REPEAT (ares_tac [exI,conjI,notI] 1)); -by (forward_tac [well_ord_converse_Memrel] 1 THEN (assume_tac 1)); +by (ftac well_ord_converse_Memrel 1 THEN (assume_tac 1)); by (forward_tac [Ord_ordertype RS converse_Memrel_not_well_ord] 1); by (contr_tac 2); by (fast_tac (empty_cs addSEs [ordertype_ord_iso RS ord_iso_is_bij RS diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/WO2_AC16.ML --- a/src/ZF/AC/WO2_AC16.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/WO2_AC16.ML Tue Sep 07 10:40:58 1999 +0200 @@ -404,7 +404,7 @@ THEN (assume_tac 1)); by (forward_tac [subsetD RS Diff_sing_lepoll] 1 THEN REPEAT (assume_tac 1)); -by (forward_tac [lepoll_Diff_sing] 1); +by (ftac lepoll_Diff_sing 1); by (REPEAT (eresolve_tac [allE, impE] 1)); by (rtac conjI 1); by (Fast_tac 2); @@ -443,7 +443,7 @@ by (eresolve_tac [dbl_Diff_eqpoll RS ex_subset_eqpoll RS bexE] 1 THEN REPEAT (assume_tac 1)); by (etac Card_is_Ord 1); -by (forward_tac [Un_in_Collect] 2 THEN REPEAT (assume_tac 2)); +by (ftac Un_in_Collect 2 THEN REPEAT (assume_tac 2)); by (etac CollectE 4); by (rtac bexI 4); by (rtac CollectI 5); @@ -521,7 +521,7 @@ \ (ALL x \ \ (EX! Y. Y:recfunAC16(f, fa, b, a) & fa ` x <= Y))"; by (etac lt_induct 1); -by (forward_tac [lt_Ord] 1); +by (ftac lt_Ord 1); by (etac Ord_cases 1); (* case 0 *) by (asm_simp_tac (simpset() addsimps [recfunAC16_0]) 1); @@ -568,7 +568,7 @@ by (etac imageE 1); by (dresolve_tac [prem3 RS Limit_is_Ord RSN (2, ltI) RS (prem3 RS Limit_has_succ)] 1); -by (forward_tac [prem1] 1); +by (ftac prem1 1); by (etac conjE 1); (** LEVEL 10 **) by (dresolve_tac [leI RS succ_leE RSN (2, ospec)] 1 THEN (assume_tac 1)); @@ -585,8 +585,8 @@ by (dresolve_tac [prem4 RS subsetD] 2 THEN (assume_tac 2)); (** LEVEL 20 **) by (fast_tac FOL_cs 2); -by (forward_tac [prem1] 1); -by (forward_tac [succ_leE] 1); +by (ftac prem1 1); +by (ftac succ_leE 1); by (dresolve_tac [prem4 RS subsetD] 1 THEN (assume_tac 1)); by (etac conjE 1); (** LEVEL 25 **) @@ -604,11 +604,11 @@ Goalw [AC16_def] "[| WO2; 0 AC16(k #+ m,k)"; by (rtac allI 1); by (rtac impI 1); -by (forward_tac [WO2_infinite_subsets_eqpoll_X] 1 +by (ftac WO2_infinite_subsets_eqpoll_X 1 THEN (REPEAT (assume_tac 1))); by (forw_inst_tac [("n","k #+ m")] (WO2_infinite_subsets_eqpoll_X) 1 THEN (REPEAT (ares_tac [add_type] 1))); -by (forward_tac [WO2_imp_ex_Card] 1); +by (ftac WO2_imp_ex_Card 1); by (REPEAT (eresolve_tac [exE,conjE] 1)); by (dresolve_tac [eqpoll_trans RS eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1 THEN (assume_tac 1)); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/AC/WO6_WO1.ML --- a/src/ZF/AC/WO6_WO1.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/AC/WO6_WO1.ML Tue Sep 07 10:40:58 1999 +0200 @@ -453,7 +453,7 @@ by (dtac WO6_imp_NN_not_empty 1); by (eresolve_tac [Un_subset_iff RS iffD1 RS conjE] 1); by (eres_inst_tac [("A","NN(y)")] not_emptyE 1); -by (forward_tac [y_well_ord] 1); +by (ftac y_well_ord 1); by (fast_tac (claset() addEs [well_ord_subset]) 2); by (fast_tac (claset() addSIs [lemma3] addSDs [NN_y_0] addSEs [not_emptyE]) 1); qed "WO6_imp_WO1"; diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/Arith.ML --- a/src/ZF/Arith.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Arith.ML Tue Sep 07 10:40:58 1999 +0200 @@ -200,7 +200,7 @@ (*Addition is the inverse of subtraction*) Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m"; -by (forward_tac [lt_nat_in_nat] 1); +by (ftac lt_nat_in_nat 1); by (etac nat_succI 1); by (etac rev_mp 1); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); @@ -208,14 +208,14 @@ qed "add_diff_inverse"; Goal "[| n le m; m:nat |] ==> (m#-n) #+ n = m"; -by (forward_tac [lt_nat_in_nat] 1); +by (ftac lt_nat_in_nat 1); by (etac nat_succI 1); by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1); qed "add_diff_inverse2"; (*Proof is IDENTICAL to that above*) Goal "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)"; -by (forward_tac [lt_nat_in_nat] 1); +by (ftac lt_nat_in_nat 1); by (etac nat_succI 1); by (etac rev_mp 1); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); @@ -272,7 +272,7 @@ (*** Remainder ***) Goal "[| 0 m #- n < m"; -by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); by (etac rev_mp 1); by (etac rev_mp 1); by (res_inst_tac [("m","m"),("n","n")] diff_induct 1); @@ -299,7 +299,7 @@ qed "mod_less"; Goal "[| 0 m mod n = (m#-n) mod n"; -by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); by (rtac (mod_def RS def_transrec RS trans) 1); by (asm_simp_tac div_ss 1); qed "mod_geq"; @@ -321,7 +321,7 @@ qed "div_less"; Goal "[| 0 m div n = succ((m#-n) div n)"; -by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1); +by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1); by (rtac (div_def RS def_transrec RS trans) 1); by (asm_simp_tac div_ss 1); qed "div_geq"; @@ -408,7 +408,7 @@ (*strict, in 1st argument; proof is by rule induction on 'less than'*) Goal "[| i i#+k < j#+k"; -by (forward_tac [lt_nat_in_nat] 1); +by (ftac lt_nat_in_nat 1); by (assume_tac 1); by (etac succ_lt_induct 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI]))); @@ -453,7 +453,7 @@ (*** Monotonicity of Multiplication ***) Goal "[| i le j; j:nat; k:nat |] ==> i#*k le j#*k"; -by (forward_tac [lt_nat_in_nat] 1); +by (ftac lt_nat_in_nat 1); by (induct_tac "k" 2); by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono]))); qed "mult_le_mono1"; @@ -471,7 +471,7 @@ (*strict, in 1st argument; proof is by induction on k>0*) Goal "[| i k#*i < k#*j"; by (etac zero_lt_natE 1); -by (forward_tac [lt_nat_in_nat] 2); +by (ftac lt_nat_in_nat 2); by (ALLGOALS Asm_simp_tac); by (induct_tac "x" 1); by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono]))); @@ -534,7 +534,7 @@ qed "add_le_elim1"; Goal "[| m EX k: nat. n = succ(m#+k)"; -by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1); +by (ftac lt_nat_in_nat 1 THEN assume_tac 1); by (etac rev_mp 1); by (induct_tac "n" 1); by (ALLGOALS (simp_tac (simpset() addsimps [le_iff]))); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/Cardinal.ML --- a/src/ZF/Cardinal.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Cardinal.ML Tue Sep 07 10:40:58 1999 +0200 @@ -650,7 +650,7 @@ qed "Diff_sing_eqpoll"; Goal "[| A lepoll 1; a:A |] ==> A = {a}"; -by (forward_tac [Diff_sing_lepoll] 1); +by (ftac Diff_sing_lepoll 1); by (assume_tac 1); by (dtac lepoll_0_is_0 1); by (blast_tac (claset() addEs [equalityE]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/CardinalArith.ML Tue Sep 07 10:40:58 1999 +0200 @@ -357,7 +357,7 @@ (*Kunen's Lemma 10.11*) Goalw [InfCard_def] "InfCard(K) ==> Limit(K)"; by (etac conjE 1); -by (forward_tac [Card_is_Ord] 1); +by (ftac Card_is_Ord 1); by (rtac (ltI RS non_succ_LimitI) 1); by (etac ([asm_rl, nat_0I] MRS (le_imp_subset RS subsetD)) 1); by (safe_tac (claset() addSDs [Limit_nat RS Limit_le_succD])); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/Coind/MT.ML --- a/src/ZF/Coind/MT.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Coind/MT.ML Tue Sep 07 10:40:58 1999 +0200 @@ -46,7 +46,7 @@ \ :HasTyRel"; by (etac elab_fixE 1); by Safe_tac; -by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]); +by (EVERY [ftac subst 1,atac 2,rtac htr_closCI 1]); by clean_tac; by (rtac ve_owrI 1); by clean_tac; diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/Coind/Map.ML --- a/src/ZF/Coind/Map.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Coind/Map.ML Tue Sep 07 10:40:58 1999 +0200 @@ -134,7 +134,7 @@ Goalw [PMap_def] "[| m:PMap(A,B); a:domain(m) |] ==> map_app(m,a):B"; -by (forward_tac [tmap_app_notempty] 1); +by (ftac tmap_app_notempty 1); by (assume_tac 1); by (dtac tmap_appI 1); by (assume_tac 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/IMP/Equiv.ML --- a/src/ZF/IMP/Equiv.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/IMP/Equiv.ML Tue Sep 07 10:40:58 1999 +0200 @@ -79,7 +79,7 @@ (* while *) by Safe_tac; by (ALLGOALS Asm_full_simp_tac); -by (EVERY1 [forward_tac [Gamma_bnd_mono], etac induct, atac]); +by (EVERY1 [ftac Gamma_bnd_mono , etac induct, atac]); by (rewtac Gamma_def); by Safe_tac; by (EVERY1 [dtac bspec, atac]); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/Order.ML --- a/src/ZF/Order.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Order.ML Tue Sep 07 10:40:58 1999 +0200 @@ -374,8 +374,8 @@ (*Simple consequence of Lemma 6.1*) Goal "[| well_ord(A,r); f : ord_iso(pred(A,a,r), r, pred(A,c,r), r); \ \ a:A; c:A |] ==> a=c"; -by (forward_tac [well_ord_is_trans_on] 1); -by (forward_tac [well_ord_is_linear] 1); +by (ftac well_ord_is_trans_on 1); +by (ftac well_ord_is_linear 1); by (linear_case_tac 1); by (dtac ord_iso_sym 1); (*two symmetric cases*) @@ -422,7 +422,7 @@ by (Asm_simp_tac 1); by (rtac well_ord_iso_pred_eq 1); by (REPEAT_SOME assume_tac); -by (forward_tac [ord_iso_restrict_pred] 1 THEN +by (ftac ord_iso_restrict_pred 1 THEN REPEAT1 (eresolve_tac [asm_rl, predI] 1)); by (asm_full_simp_tac (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); @@ -437,11 +437,11 @@ Goal "[| well_ord(A,r); \ \ f: ord_iso(A,r, B,s); g: ord_iso(A,r, B,s); y: A |] \ \ ==> ~ : s"; -by (forward_tac [well_ord_iso_subset_lemma] 1); +by (ftac well_ord_iso_subset_lemma 1); by (res_inst_tac [("f","converse(f)"), ("g","g")] ord_iso_trans 1); by (REPEAT_FIRST (ares_tac [subset_refl, ord_iso_sym])); by Safe_tac; -by (forward_tac [ord_iso_converse] 1); +by (ftac ord_iso_converse 1); by (EVERY (map (blast_tac bij_apply_cs) [1,1,1])); by (asm_full_simp_tac bij_inverse_ss 1); qed "well_ord_iso_unique_lemma"; @@ -535,7 +535,7 @@ (*Harder case: : r*) by (forward_tac [ord_iso_is_bij RS bij_is_fun RS apply_type] 1 THEN REPEAT1 (eresolve_tac [asm_rl, predI, predE] 1)); -by (forward_tac [ord_iso_restrict_pred] 1 THEN +by (ftac ord_iso_restrict_pred 1 THEN REPEAT1 (eresolve_tac [asm_rl, predI] 1)); by (asm_full_simp_tac (simpset() addsimps [well_ord_is_trans_on, trans_pred_pred_eq]) 1); @@ -546,7 +546,7 @@ Goal "[| well_ord(A,r); well_ord(B,s) |] ==> \ \ domain(ord_iso_map(A,r,B,s)) = A | \ \ (EX x:A. domain(ord_iso_map(A,r,B,s)) = pred(A,x,r))"; -by (forward_tac [well_ord_is_wf] 1); +by (ftac well_ord_is_wf 1); by (rewrite_goals_tac [wf_on_def, wf_def]); by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1); by Safe_tac; diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/OrderType.ML --- a/src/ZF/OrderType.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/OrderType.ML Tue Sep 07 10:40:58 1999 +0200 @@ -39,7 +39,7 @@ qed "pred_Memrel"; Goal "[| j R"; -by (forward_tac [lt_pred_Memrel] 1); +by (ftac lt_pred_Memrel 1); by (etac ltE 1); by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN assume_tac 3 THEN assume_tac 1); @@ -167,7 +167,7 @@ Goal "[| f: ord_iso(A,r,B,s); well_ord(B,s) |] ==> \ \ ordertype(A,r) = ordertype(B,s)"; -by (forward_tac [well_ord_ord_iso] 1 THEN assume_tac 1); +by (ftac well_ord_ord_iso 1 THEN assume_tac 1); by (rtac Ord_iso_implies_eq 1 THEN REPEAT (etac Ord_ordertype 1)); by (deepen_tac (claset() addIs [ord_iso_trans, ord_iso_sym] @@ -535,8 +535,8 @@ qed "oadd_le_self2"; Goal "[| k le j; Ord(i) |] ==> k++i le j++i"; -by (forward_tac [lt_Ord] 1); -by (forward_tac [le_Ord2] 1); +by (ftac lt_Ord 1); +by (ftac le_Ord2 1); by (etac trans_induct3 1); by (Asm_simp_tac 1); by (asm_simp_tac (simpset() addsimps [oadd_succ, succ_le_iff]) 1); @@ -818,8 +818,8 @@ qed "omult_le_self"; Goal "[| k le j; Ord(i) |] ==> k**i le j**i"; -by (forward_tac [lt_Ord] 1); -by (forward_tac [le_Ord2] 1); +by (ftac lt_Ord 1); +by (ftac le_Ord2 1); by (etac trans_induct3 1); by (asm_simp_tac (simpset() addsimps [le_refl, Ord_0]) 1); by (asm_simp_tac (simpset() addsimps [omult_succ, oadd_le_mono]) 1); @@ -856,7 +856,7 @@ qed "omult_lt_mono"; Goal "[| Ord(i); 0 i le j**i"; -by (forward_tac [lt_Ord2] 1); +by (ftac lt_Ord2 1); by (eres_inst_tac [("i","i")] trans_induct3 1); by (asm_simp_tac (simpset() addsimps [omult_0, Ord_0 RS le_refl]) 1); by (asm_simp_tac (simpset() addsimps [omult_succ, succ_le_iff]) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/Resid/Confluence.ML --- a/src/ZF/Resid/Confluence.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Resid/Confluence.ML Tue Sep 07 10:40:58 1999 +0200 @@ -38,7 +38,7 @@ Goalw [confluence_def] "confluence(Spar_red1)"; by (Clarify_tac 1); -by (forward_tac [simulation] 1); +by (ftac simulation 1); by (forw_inst_tac [("n","z")] simulation 1); by (Clarify_tac 1); by (forw_inst_tac [("v","va")] paving 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/Resid/Substitution.ML --- a/src/ZF/Resid/Substitution.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Resid/Substitution.ML Tue Sep 07 10:40:58 1999 +0200 @@ -131,7 +131,7 @@ by (ALLGOALS Asm_simp_tac); by Safe_tac; by (case_tac "n < xa" 1); -by ((forward_tac [lt_trans2] 1) THEN (assume_tac 1)); +by ((ftac lt_trans2 1) THEN (assume_tac 1)); by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [lift_rec_Var, leI]))); qed "lift_lift_rec"; @@ -176,7 +176,7 @@ by (excluded_middle_tac "n < x" 1); by (Asm_full_simp_tac 1); by (eres_inst_tac [("i","x")] leE 1); -by (forward_tac [lt_trans1] 1 THEN assume_tac 1); +by (ftac lt_trans1 1 THEN assume_tac 1); by (ALLGOALS(asm_simp_tac (simpset() addsimps [succ_pred,leI,gt_pred]))); by (asm_full_simp_tac (simpset() addsimps [leI]) 1); @@ -218,7 +218,7 @@ by (eres_inst_tac [("j","n")] leE 1); by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); by (asm_simp_tac (simpset() addsimps [subst_rec_lift_rec]) 1); -by (forward_tac [lt_trans2] 1 THEN assume_tac 1); +by (ftac lt_trans2 1 THEN assume_tac 1); by (asm_simp_tac (simpset() addsimps [gt_pred]) 1); qed "subst_rec_subst_rec"; diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/Zorn.ML --- a/src/ZF/Zorn.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/Zorn.ML Tue Sep 07 10:40:58 1999 +0200 @@ -300,7 +300,7 @@ by (Blast_tac 2); (*Now prove the well_foundedness goal*) by (rtac wf_onI 1); -by (forward_tac [well_ord_TFin_lemma] 1 THEN assume_tac 1); +by (ftac well_ord_TFin_lemma 1 THEN assume_tac 1); by (dres_inst_tac [("x","Inter(Z)")] bspec 1 THEN assume_tac 1); by (Blast_tac 1); qed "well_ord_TFin"; diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/ex/Primrec.ML --- a/src/ZF/ex/Primrec.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/ex/Primrec.ML Tue Sep 07 10:40:58 1999 +0200 @@ -75,7 +75,7 @@ (*PROPERTY A 5, monotonicity for < *) Goal "[| j ack(i,j) < ack(i,k)"; -by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1); +by (ftac lt_nat_in_nat 1 THEN assume_tac 1); by (etac succ_lt_induct 1); by (assume_tac 1); by (rtac lt_trans 2); @@ -106,7 +106,7 @@ (*PROPERTY A 7, monotonicity for < *) Goal "[| i ack(i,k) < ack(j,k)"; -by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1); +by (ftac lt_nat_in_nat 1 THEN assume_tac 1); by (etac succ_lt_induct 1); by (assume_tac 1); by (rtac lt_trans 2); @@ -227,7 +227,7 @@ \ f`l < ack(kf, list_add(l))}) \ \ |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l < ack(k, list_add(l))"; by (Asm_simp_tac 1); -by (forward_tac [list_CollectD] 1); +by (ftac list_CollectD 1); by (etac (COMP_map_lemma RS bexE) 1); by (rtac (ballI RS bexI) 1); by (etac (bspec RS lt_trans) 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/ex/Term.ML --- a/src/ZF/ex/Term.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/ex/Term.ML Tue Sep 07 10:40:58 1999 +0200 @@ -93,7 +93,7 @@ \ ==> d(x, zs, r): C(Apply(x,zs)) \ \ |] ==> term_rec(t,d) : C(t)"; by (rtac (major RS term.induct) 1); -by (forward_tac [list_CollectD] 1); +by (ftac list_CollectD 1); by (stac term_rec 1); by (REPEAT (ares_tac prems 1)); by (etac list.induct 1); diff -r 1e5585fd3632 -r 23e090051cb8 src/ZF/func.ML --- a/src/ZF/func.ML Mon Sep 06 22:12:08 1999 +0200 +++ b/src/ZF/func.ML Tue Sep 07 10:40:58 1999 +0200 @@ -89,7 +89,7 @@ qed "apply_0"; Goal "[| f: Pi(A,B); c: f |] ==> EX x:A. c = "; -by (forward_tac [fun_is_rel] 1); +by (ftac fun_is_rel 1); by (blast_tac (claset() addDs [apply_equality]) 1); qed "Pi_memberD"; @@ -112,7 +112,7 @@ qed "apply_funtype"; Goal "f: Pi(A,B) ==> : f <-> a:A & f`a = b"; -by (forward_tac [fun_is_rel] 1); +by (ftac fun_is_rel 1); by (blast_tac (claset() addSIs [apply_Pair, apply_equality]) 1); qed "apply_iff";