--- 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);
--- 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**)
--- 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";
--- 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";
--- 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";
--- 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";
--- 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
--- 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;
--- 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);
--- 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);
--- 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);
--- 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<n |] ==> f dvd (m mod n)";
--- 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);
--- 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 ==> 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);
--- 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";
--- 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);
--- 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";
--- 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);
--- 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";
--- 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";
--- 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);
--- 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);
--- 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);
--- 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
--- 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);
--- 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);
--- 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);
--- 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(),
--- 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(),
--- 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";
--- 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();
--- 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))))]);
--- 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";
--- 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);
--- 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";
--- 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";
--- 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]
--- 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);
--- 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);
--- 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);
--- 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);
--- 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);
--- 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);
--- 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);
--- 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
--- 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 *)
--- 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];
--- 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))
--- 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<LEAST x. HH(f,A,x)={A}. HH(f,A,x) lepoll m";
by (rtac oallI 1);
by (dresolve_tac [ltD RS less_Least_subset_x] 1);
-by (forward_tac [HH_subset_imp_eq] 1);
+by (ftac HH_subset_imp_eq 1);
by (etac ssubst 1);
by (fast_tac (claset() addIs [prem RS ballE]
addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1);
--- a/src/ZF/AC/AC16_WO4.ML Mon Sep 06 22:12:08 1999 +0200
+++ b/src/ZF/AC/AC16_WO4.ML Tue Sep 07 10:40:58 1999 +0200
@@ -394,7 +394,7 @@
by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1);
by (EVERY (map Blast_tac [4,3,2,1]));
by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
-by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1));
+by (ftac cons_cons_in 1 THEN REPEAT (assume_tac 1));
by (etac ex1_two_eq 1);
by (REPEAT (blast_tac
(claset() addDs [s_subset RS subsetD, in_s_imp_u_in]) 1));
@@ -481,8 +481,8 @@
qed "the_in_MM_subset";
Goalw [GG_def] "v : LL ==> 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));
--- 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);
--- 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();
--- 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)));
--- 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);
--- 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";
--- 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
--- 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
--- 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<a. x < b | (EX Y:recfunAC16(f, fa, b, a). fa ` x <= Y) --> \
\ (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<m; k:nat; m:nat |] ==> 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));
--- 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";
--- 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<n; n le m; m:nat |] ==> 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<n; n le m; m:nat |] ==> 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<n; n le m; m:nat |] ==> 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<j; j:nat; k:nat |] ==> 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<j; 0<k; j:nat; k:nat |] ==> 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<n; n: nat |] ==> 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])));
--- 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);
--- 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]));
--- 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 @@
\ <cl,t>: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;
--- 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);
--- 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]);
--- 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 |] \
\ ==> ~ <g`y, f`y> : 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: <a, xa>: 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;
--- 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<i; f: ord_iso(i,Memrel(i),j,Memrel(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<j |] ==> 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);
--- 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);
--- 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";
--- 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";
--- 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<k; i:nat; k:nat |] ==> 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<j; j:nat; k:nat |] ==> 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);
--- 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);
--- 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 = <x,f`x>";
-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) ==> <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";