--- a/src/HOL/IMP/Transition.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/IMP/Transition.ML Wed Aug 30 16:29:21 2000 +0200
@@ -93,7 +93,7 @@
(* WHILE, induction on the length of the computation *)
by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);
by (res_inst_tac [("x","s")] spec 1);
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
by (strip_tac 1);
by (etac rel_pow_E2 1);
by (Asm_full_simp_tac 1);
@@ -214,7 +214,7 @@
qed_spec_mp "comp_decomp_lemma";
Goal "!c s t. (c,s) -n-> (SKIP,t) --> <c,s> -c-> t";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
by (Clarify_tac 1);
by (etac rel_pow_E2 1);
by (asm_full_simp_tac (simpset() addsimps evalc.intrs) 1);
--- a/src/HOL/Induct/LList.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Induct/LList.ML Wed Aug 30 16:29:21 2000 +0200
@@ -128,7 +128,7 @@
qed "LListD_unfold";
Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
-by (res_inst_tac [("n", "k")] less_induct 1);
+by (induct_thm_tac less_induct "k" 1);
by (safe_tac (claset() delrules [equalityI]));
by (etac LListD.elim 1);
by (safe_tac (claset() delrules [equalityI]));
@@ -287,7 +287,7 @@
by (rtac (ntrunc_equality RS ext) 1);
by (rename_tac "x k" 1);
by (res_inst_tac [("x", "x")] spec 1);
-by (res_inst_tac [("n", "k")] less_induct 1);
+by (induct_thm_tac less_induct "k" 1);
by (rename_tac "n" 1);
by (rtac allI 1);
by (rename_tac "y" 1);
--- a/src/HOL/Induct/Multiset.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Induct/Multiset.ML Wed Aug 30 16:29:21 2000 +0200
@@ -457,7 +457,7 @@
by (Clarify_tac 1);
by (rotate_tac ~1 1);
by (etac rev_mp 1);
-by (res_inst_tac [("M","K")] multiset_induct 1);
+by (induct_thm_tac multiset_induct "K" 1);
by (Asm_simp_tac 1);
by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
by (Blast_tac 1);
@@ -476,7 +476,7 @@
qed "lemma3";
Goalw [W_def] "wf(r) ==> M : W";
-by (res_inst_tac [("M","M")] multiset_induct 1);
+by (induct_thm_tac multiset_induct "M" 1);
by (rtac accI 1);
by (Asm_full_simp_tac 1);
by (blast_tac (claset() addDs [export lemma3]) 1);
--- a/src/HOL/Induct/Perm.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Induct/Perm.ML Wed Aug 30 16:29:21 2000 +0200
@@ -145,7 +145,7 @@
AddIffs [cons_perm_eq];
Goal "ALL xs ys. zs@xs <~~> zs@ys --> xs <~~> ys";
-by (res_inst_tac [("xs","zs")] rev_induct 1);
+by (rev_induct_tac "zs" 1);
by (ALLGOALS Full_simp_tac);
by (Blast_tac 1);
qed_spec_mp "append_perm_imp_perm";
--- a/src/HOL/Induct/SList.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Induct/SList.ML Wed Aug 30 16:29:21 2000 +0200
@@ -52,7 +52,7 @@
(*Perform induction on xs. *)
fun list_ind_tac a M =
- EVERY [res_inst_tac [("l",a)] list_induct2 M,
+ EVERY [induct_thm_tac list_induct2 a M,
rename_last_tac a ["1"] (M+1)];
(*** Isomorphisms ***)
--- a/src/HOL/Integ/IntDiv.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Integ/IntDiv.ML Wed Aug 30 16:29:21 2000 +0200
@@ -113,7 +113,7 @@
(*Correctness of posDivAlg: it computes quotients correctly*)
Goal "#0 <= a --> #0 < b --> quorem ((a, b), posDivAlg (a, b))";
-by (res_inst_tac [("u", "a"), ("v", "b")] posDivAlg_induct 1);
+by (induct_thm_tac posDivAlg_induct "a b" 1);
by Auto_tac;
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
(*base case: a<b*)
@@ -152,7 +152,7 @@
(*Correctness of negDivAlg: it computes quotients correctly
It doesn't work if a=0 because the 0/b=0 rather than -1*)
Goal "a < #0 --> #0 < b --> quorem ((a, b), negDivAlg (a, b))";
-by (res_inst_tac [("u", "a"), ("v", "b")] negDivAlg_induct 1);
+by (induct_thm_tac negDivAlg_induct "a b" 1);
by Auto_tac;
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [quorem_def])));
(*base case: 0<=a+b*)
--- a/src/HOL/Integ/int_arith2.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Integ/int_arith2.ML Wed Aug 30 16:29:21 2000 +0200
@@ -88,7 +88,7 @@
(*Analogous to zadd_int, but more easily provable using the arithmetic in Bin*)
Goal "n<=m --> int m - int n = int (m-n)";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (induct_thm_tac diff_induct "m n" 1);
by Auto_tac;
qed_spec_mp "zdiff_int";
--- a/src/HOL/Lambda/ListApplication.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.ML Wed Aug 30 16:29:21 2000 +0200
@@ -97,7 +97,7 @@
"[| !!n ts. !t : set ts. P t ==> P((Var n)$$ts); \
\ !!u ts. [| P u; !t : set ts. P t |] ==> P((Abs u)$$ts) \
\|] ==> !t. size t = n --> P t";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
by (rtac allI 1);
by (cut_inst_tac [("t","t")] ex_head_tail 1);
by (Clarify_tac 1);
--- a/src/HOL/Lambda/ListBeta.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.ML Wed Aug 30 16:29:21 2000 +0200
@@ -66,7 +66,7 @@
AddSEs [apps_betasE];
Goal "r -> s ==> r$$ss -> s$$ss";
-by (res_inst_tac [("xs","ss")] rev_induct 1);
+by (rev_induct_tac "ss" 1);
by (Auto_tac);
qed "apps_preserves_beta";
Addsimps [apps_preserves_beta];
@@ -79,7 +79,7 @@
Addsimps [apps_preserves_beta2];
Goal "!ss. rs => ss --> r$$rs -> r$$ss";
-by (res_inst_tac [("xs","rs")] rev_induct 1);
+by (rev_induct_tac "rs" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
--- a/src/HOL/Lambda/ParRed.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lambda/ParRed.ML Wed Aug 30 16:29:21 2000 +0200
@@ -83,7 +83,7 @@
(*** cd ***)
Goal "!t. s => t --> t => cd s";
-by (res_inst_tac[("x","s")] cd.induct 1);
+by (induct_thm_tac cd.induct "s" 1);
by (Auto_tac);
by (fast_tac (claset() addSIs [par_beta_subst]) 1);
qed_spec_mp "par_beta_cd";
--- a/src/HOL/Lex/MaxChop.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lex/MaxChop.ML Wed Aug 30 16:29:21 2000 +0200
@@ -33,7 +33,7 @@
Goal "is_maxsplitter P splitf ==> \
\ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
-by (res_inst_tac [("xs","xs")] length_induct 1);
+by (induct_thm_tac length_induct "xs" 1);
by (asm_simp_tac (simpset() delsplits [split_if]
addsimps [chop_rule,is_maxsplitter_reducing]) 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
@@ -42,7 +42,7 @@
Goal "is_maxsplitter P splitf ==> \
\ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
-by (res_inst_tac [("xs","xs")] length_induct 1);
+by (induct_thm_tac length_induct "xs" 1);
by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]) 1);
by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
addsplits [split_split]) 1);
--- a/src/HOL/Lex/Prefix.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lex/Prefix.ML Wed Aug 30 16:29:21 2000 +0200
@@ -81,7 +81,7 @@
qed "prefix_Cons";
Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by (res_inst_tac [("xs","zs")] rev_induct 1);
+by (rev_induct_tac "zs" 1);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() delsimps [append_assoc]
addsimps [append_assoc RS sym])1);
--- a/src/HOL/Lex/RegExp2NAe.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML Wed Aug 30 16:29:21 2000 +0200
@@ -500,7 +500,7 @@
\ (? us v. w = concat us @ v & \
\ (!u:set us. accepts A u) & \
\ (? r. (start A,r) : steps A v & rr = True#r))";
-by (res_inst_tac [("xs","w")] rev_induct 1);
+by (rev_induct_tac "w" 1);
by (Asm_full_simp_tac 1);
by (Clarify_tac 1);
by (res_inst_tac [("x","[]")] exI 1);
--- a/src/HOL/List.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/List.ML Wed Aug 30 16:29:21 2000 +0200
@@ -414,10 +414,10 @@
by (eresolve_tac prems 1);
qed "rev_induct";
-fun rev_induct_tac xs = res_inst_tac [("xs",xs)] rev_induct;
+val rev_induct_tac = induct_thm_tac rev_induct;
Goal "(xs = [] --> P) --> (!ys y. xs = ys@[y] --> P) --> P";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
+by (rev_induct_tac "xs" 1);
by Auto_tac;
bind_thm ("rev_exhaust",
impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
@@ -752,7 +752,7 @@
Addsimps [butlast_snoc];
Goal "length(butlast xs) = length xs - 1";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
+by (rev_induct_tac "xs" 1);
by Auto_tac;
qed "length_butlast";
Addsimps [length_butlast];
@@ -1217,7 +1217,7 @@
qed "map_Suc_upt";
Goal "ALL i. i < n-m --> (map f [m..n(]) ! i = f(m+i)";
-by (res_inst_tac [("m","n"),("n","m")] diff_induct 1);
+by (induct_thm_tac diff_induct "n m" 1);
by (stac (map_Suc_upt RS sym) 3);
by (auto_tac (claset(), simpset() addsimps [less_diff_conv, nth_upt]));
qed_spec_mp "nth_map_upt";
@@ -1453,14 +1453,14 @@
Goal "map fst [p:zip xs [i..i + length xs(] . snd p : A] = \
\ map fst [p:zip xs [0..length xs(] . snd p + i : A]";
-by (res_inst_tac [("xs","xs")] rev_induct 1);
+by (rev_induct_tac "xs" 1);
by (asm_simp_tac (simpset() addsimps [add_commute]) 2);
by (Simp_tac 1);
qed "sublist_shift_lemma";
Goalw [sublist_def]
"sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}";
-by (res_inst_tac [("xs","l'")] rev_induct 1);
+by (rev_induct_tac "l'" 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset() addsimps [inst "i" "0" upt_add_eq_append,
zip_append, sublist_shift_lemma]) 1);
@@ -1470,7 +1470,7 @@
Addsimps [sublist_empty, sublist_nil];
Goal "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}";
-by (res_inst_tac [("xs","l")] rev_induct 1);
+by (rev_induct_tac "l" 1);
by (asm_simp_tac (simpset() delsimps [append_Cons]
addsimps [append_Cons RS sym, sublist_append]) 2);
by (simp_tac (simpset() addsimps [sublist_def]) 1);
@@ -1482,7 +1482,7 @@
Addsimps [sublist_singleton];
Goal "sublist l {..n(} = take n l";
-by (res_inst_tac [("xs","l")] rev_induct 1);
+by (rev_induct_tac "l" 1);
by (asm_simp_tac (simpset() addsplits [nat_diff_split]
addsimps [sublist_append]) 2);
by (Simp_tac 1);
--- a/src/HOL/MiniML/MiniML.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/MiniML/MiniML.ML Wed Aug 30 16:29:21 2000 +0200
@@ -114,7 +114,7 @@
qed "free_tv_alpha";
Goal "!!(k::nat). n <= n + k";
-by (res_inst_tac [("n","k")] nat_induct 1);
+by (induct_thm_tac nat_induct "k" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
val aux_plus = result();
--- a/src/HOL/MiniML/Type.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/MiniML/Type.ML Wed Aug 30 16:29:21 2000 +0200
@@ -150,7 +150,7 @@
by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
-by (res_inst_tac [("n","n")] nat_induct 1);
+by (induct_thm_tac nat_induct "n" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "free_tv_nth_A_impl_free_tv_A";
@@ -161,7 +161,7 @@
by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
-by (res_inst_tac [("n","nat")] nat_induct 1);
+by (induct_thm_tac nat_induct "nat" 1);
by (strip_tac 1);
by (Asm_full_simp_tac 1);
by (Simp_tac 1);
@@ -505,7 +505,7 @@
by (induct_tac "A" 1);
by (Asm_full_simp_tac 1);
by (rtac allI 1);
-by (res_inst_tac [("n","nat")] nat_induct 1);
+by (induct_thm_tac nat_induct "nat" 1);
by (strip_tac 1);
by (Asm_full_simp_tac 1);
by (Simp_tac 1);
@@ -718,7 +718,7 @@
by (Asm_full_simp_tac 1);
by (rtac allI 1);
by (rename_tac "n1" 1);
-by (res_inst_tac[("n","n1")] nat_induct 1);
+by (induct_thm_tac nat_induct "n1" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
qed_spec_mp "nth_subst";
--- a/src/HOL/NumberTheory/EulerFermat.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/NumberTheory/EulerFermat.ML Wed Aug 30 16:29:21 2000 +0200
@@ -30,7 +30,7 @@
qed "BnorRset_induct";
Goal "b:BnorRset(a,m) --> b<=a";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
by (stac BnorRset_eq 2);
by (rewtac Let_def);
by Auto_tac;
@@ -43,14 +43,14 @@
qed "Bnor_mem_zle_swap";
Goal "b:BnorRset(a,m) --> #0<b";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
by (stac BnorRset_eq 2);
by (rewtac Let_def);
by Auto_tac;
qed_spec_mp "Bnor_mem_zg";
Goal "zgcd(b,m) = #1 --> #0<b --> b<=a --> b:BnorRset(a,m)";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset.induct 1);
+by (induct_thm_tac BnorRset.induct "a m" 1);
by Auto_tac;
by (case_tac "a=b" 1);
by (asm_full_simp_tac (simpset() addsimps [zle_neq_implies_zless]) 2);
@@ -61,7 +61,7 @@
qed_spec_mp "Bnor_mem_if";
Goal "a<m --> BnorRset (a,m) : RsetR m";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
by (Simp_tac 1);
by (stac BnorRset_eq 1);
by (rewtac Let_def);
@@ -77,7 +77,7 @@
qed_spec_mp "Bnor_in_RsetR";
Goal "finite (BnorRset (a,m))";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
by (stac BnorRset_eq 2);
by (rewtac Let_def);
by Auto_tac;
@@ -210,7 +210,7 @@
Goal "x~=#0 ==> a<m --> setprod ((%a. a*x) `` BnorRset(a,m)) = \
\ setprod (BnorRset(a,m)) * x^card(BnorRset(a,m))";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
by (stac BnorRset_eq 2);
by (rewtac Let_def);
by Auto_tac;
@@ -235,7 +235,7 @@
Goalw [norRRset_def,phi_def]
"#0<m --> a<m --> zgcd (setprod (BnorRset (a,m)),m) = #1";
-by (res_inst_tac [("u","a"),("v","m")] BnorRset_induct 1);
+by (induct_thm_tac BnorRset_induct "a m" 1);
by (stac BnorRset_eq 2);
by (rewtac Let_def);
by Auto_tac;
@@ -270,7 +270,7 @@
Goalw [zprime_def]
"p:zprime ==> a<p --> (ALL b. #0<b & b<=a --> zgcd(b,p) = #1) \
\ --> card (BnorRset(a, p)) = nat a";
-by (res_inst_tac [("u","a"),("v","p")] BnorRset.induct 1);
+by (induct_thm_tac BnorRset.induct "a p" 1);
by (stac BnorRset_eq 1);
by (rewtac Let_def);
by Auto_tac;
--- a/src/HOL/NumberTheory/IntFact.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/NumberTheory/IntFact.ML Wed Aug 30 16:29:21 2000 +0200
@@ -42,13 +42,13 @@
qed "d22set_induct";
Goal "b:(d22set a) --> #1<b";
-by (res_inst_tac [("u","a")] d22set_induct 1);
+by (induct_thm_tac d22set_induct "a" 1);
by (stac d22set_eq 2);
by Auto_tac;
qed_spec_mp "d22set_g_1";
Goal "b:(d22set a) --> b<=a";
-by (res_inst_tac [("u","a")] d22set_induct 1);
+by (induct_thm_tac d22set_induct "a" 1);
by (stac d22set_eq 2);
by Auto_tac;
qed_spec_mp "d22set_le";
@@ -60,13 +60,13 @@
qed "d22set_le_swap";
Goal "#1<b --> b<=a --> b:(d22set a)";
-by (res_inst_tac [("x","a")] d22set.induct 1);
+by (induct_thm_tac d22set.induct "a" 1);
by Auto_tac;
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [d22set_eq])));
qed_spec_mp "d22set_mem";
Goal "finite (d22set a)";
-by (res_inst_tac [("u","a")] d22set_induct 1);
+by (induct_thm_tac d22set_induct "a" 1);
by (stac d22set_eq 2);
by Auto_tac;
qed "d22set_fin";
@@ -75,7 +75,7 @@
Delsimps zfact.simps;
Goal "setprod(d22set a) = zfact a";
-by (res_inst_tac [("x","a")] d22set.induct 1);
+by (induct_thm_tac d22set.induct "a" 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps [d22set_eq,zfact_eq]) 1);
by (stac d22set_eq 1);
--- a/src/HOL/NumberTheory/IntPrimes.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.ML Wed Aug 30 16:29:21 2000 +0200
@@ -181,7 +181,7 @@
Addsimps [zgcd_0_1_iff];
Goal "#0<=(n::int) --> (zgcd(m,n) dvd m) & (zgcd(m,n) dvd n)";
-by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (induct_thm_tac zgcd.induct "m n" 1);
by (case_tac "n=#0" 1);
by (auto_tac (claset() addDs [zdvd_zmod_imp_zdvd],
simpset() addsimps [zle_neq_implies_zless,neq_commute,
@@ -198,14 +198,14 @@
val lemma_false = result();
Goal "#0<=(n::int) --> (f dvd m) --> (f dvd n) --> f dvd zgcd(m,n)";
-by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (induct_thm_tac zgcd.induct "m n" 1);
by (case_tac "n=#0" 1);
by (auto_tac (claset() addDs [lemma_false] addIs [pos_mod_sign,zdvd_zmod],
simpset() addsimps [zgcd_non_0,neq_commute,zle_neq_implies_zless]));
qed_spec_mp "zgcd_greatest";
Goal "#0 < (n::int) --> #0 < zgcd (m, n)";
-by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (induct_thm_tac zgcd.induct "m n" 1);
by (auto_tac (claset(), simpset() addsimps zgcd.simps));
qed_spec_mp "zgcd_zless";
@@ -269,7 +269,7 @@
qed "zgcd_assoc";
Goal "#0<=(n::int) --> #0<=k --> k * zgcd(m,n) = zgcd(k*m, k*n)";
-by (res_inst_tac [("u","m"),("v","n")] zgcd.induct 1);
+by (induct_thm_tac zgcd.induct "m n" 1);
by (case_tac "n=#0" 1);
by (auto_tac (claset() addDs [lemma_false],
simpset() addsimps [zle_neq_implies_zless,pos_mod_sign,
--- a/src/HOL/NumberTheory/WilsonRuss.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.ML Wed Aug 30 16:29:21 2000 +0200
@@ -175,7 +175,7 @@
qed "wset_subset";
Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> #1<b";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
by Auto_tac;
by (case_tac "b=a" 1);
by (case_tac "b=inv p a" 2);
@@ -187,7 +187,7 @@
qed_spec_mp "wset_g_1";
Goal "p:zprime --> a<p-#1 --> b:(wset(a,p)) --> b<p-#1";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
by Auto_tac;
by (case_tac "b=a" 1);
by (case_tac "b=inv p a" 2);
@@ -199,7 +199,7 @@
qed_spec_mp "wset_less";
Goal "p:zprime --> a<p-#1 --> #1<b --> b<=a --> b:(wset(a,p))";
-by (res_inst_tac [("u","a"),("v","p")] wset.induct 1);
+by (induct_thm_tac wset.induct "a p" 1);
by Auto_tac;
by (subgoal_tac "b=a" 1);
by (rtac zle_anti_sym 2);
@@ -210,7 +210,7 @@
Goal "p:zprime --> #5<=p --> a<p-#1 --> b:(wset (a,p)) \
\ --> (inv p b):(wset (a,p))";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
by Auto_tac;
by (case_tac "b=a" 1);
by (stac wset_eq 1);
@@ -234,14 +234,14 @@
qed "wset_inv_mem_mem";
Goal "finite (wset (a,p))";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
by (stac wset_eq 2);
by (rewtac Let_def);
by Auto_tac;
qed "wset_fin";
Goal "p:zprime --> #5<=p --> a<p-#1 --> [setprod (wset (a,p)) = #1](mod p)";
-by (res_inst_tac [("u","a"),("v","p")] wset_induct 1);
+by (induct_thm_tac wset_induct "a p" 1);
by (stac wset_eq 2);
by (rewtac Let_def);
by Auto_tac;
--- a/src/HOL/Real/Hyperreal/Zorn.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Real/Hyperreal/Zorn.ML Wed Aug 30 16:29:21 2000 +0200
@@ -53,7 +53,7 @@
(*Perform induction on n, then prove the major premise using prems. *)
fun TFin_ind_tac a prems i =
- EVERY [res_inst_tac [("n",a)] TFin_induct i,
+ EVERY [induct_thm_tac TFin_induct a i,
rename_last_tac a ["1"] (i+1),
rename_last_tac a ["2"] (i+2),
ares_tac prems i];
--- a/src/HOL/Real/PNat.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Real/PNat.ML Wed Aug 30 16:29:21 2000 +0200
@@ -48,7 +48,7 @@
(*Perform induction on n. *)
fun pnat_ind_tac a i =
- res_inst_tac [("n",a)] pnat_induct i THEN rename_last_tac a [""] (i+1);
+ induct_thm_tac pnat_induct a i THEN rename_last_tac a [""] (i+1);
val prems = Goal
"[| !!x. P x 1p; \
--- a/src/HOL/Real/PReal.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Real/PReal.ML Wed Aug 30 16:29:21 2000 +0200
@@ -586,7 +586,7 @@
Goal "ALL xa : Rep_preal(A). xa + x : Rep_preal(A) ==> \
\ EX xb : Rep_preal(A). xb + (prat_of_pnat p)*x : Rep_preal(A)";
by (cut_facts_tac [mem_Rep_preal_Ex] 1);
-by (res_inst_tac [("n","p")] pnat_induct 1);
+by (induct_thm_tac pnat_induct "p" 1);
by (auto_tac (claset(),simpset() addsimps [pnat_one_def,
pSuc_is_plus_one,prat_add_mult_distrib,
prat_of_pnat_add,prat_add_assoc RS sym]));
--- a/src/HOL/Subst/AList.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Subst/AList.ML Wed Aug 30 16:29:21 2000 +0200
@@ -18,5 +18,5 @@
(*Perform induction on xs. *)
fun alist_ind_tac a M =
- EVERY [res_inst_tac [("l",a)] alist_induct M,
+ EVERY [induct_thm_tac alist_induct a M,
rename_last_tac a ["1"] (M+1)];
--- a/src/HOL/Tools/datatype_package.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed Aug 30 16:29:21 2000 +0200
@@ -9,6 +9,7 @@
signature BASIC_DATATYPE_PACKAGE =
sig
val induct_tac : string -> int -> tactic
+ val induct_thm_tac : thm -> string -> int -> tactic
val case_tac : string -> int -> tactic
val distinct_simproc : simproc
end;
@@ -199,6 +200,9 @@
fun induct_tac s = gen_induct_tac (map (Library.single o Some) (Syntax.read_idents s), None);
+fun induct_thm_tac th s =
+ gen_induct_tac ([map Some (Syntax.read_idents s)], Some th);
+
end;
--- a/src/HOL/UNITY/AllocBase.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.ML Wed Aug 30 16:29:21 2000 +0200
@@ -59,7 +59,7 @@
Goal "bag_of (sublist l A) = \
\ setsum (%i. {# l!i #}) (A Int lessThan (length l))";
-by (res_inst_tac [("xs","l")] rev_induct 1);
+by (rev_induct_tac "l" 1);
by (Simp_tac 1);
by (asm_simp_tac
(simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc,
--- a/src/HOL/UNITY/GenPrefix.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/UNITY/GenPrefix.ML Wed Aug 30 16:29:21 2000 +0200
@@ -341,7 +341,7 @@
Addsimps [prefix_snoc];
Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by (res_inst_tac [("xs","zs")] rev_induct 1);
+by (rev_induct_tac "zs" 1);
by (Force_tac 1);
by (asm_full_simp_tac (simpset() delsimps [append_assoc]
addsimps [append_assoc RS sym])1);
--- a/src/HOL/While.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/While.ML Wed Aug 30 16:29:21 2000 +0200
@@ -40,7 +40,7 @@
\ !!s. [| P s; ~b s |] ==> Q s; \
\ wf{(t,s). P s & b s & t = c s} |] \
\ ==> P s --> Q(while b c s)";
-by(res_inst_tac [("a","s")] (prem3 RS wf_induct) 1);
+by(induct_thm_tac (prem3 RS wf_induct) "s" 1);
by(Asm_full_simp_tac 1);
by(Clarify_tac 1);
by(stac while_unfold 1);
--- a/src/HOL/ex/Factorization.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Factorization.ML Wed Aug 30 16:29:21 2000 +0200
@@ -195,7 +195,7 @@
qed "split_primel";
Goal "1<n --> (EX l. primel l & prod l = n)";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
by (rtac impI 1);
by (case_tac "n:prime" 1);
by (rtac exI 1);
@@ -267,7 +267,7 @@
Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
\ --> xs <~~> ys)";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
by Safe_tac;
by (case_tac "xs" 1);
by (force_tac (claset() addIs [primel_one_empty], simpset()) 1);
--- a/src/HOL/ex/Fib.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Fib.ML Wed Aug 30 16:29:21 2000 +0200
@@ -24,7 +24,7 @@
(*Concrete Mathematics, page 280*)
Goal "fib (Suc (n + k)) = fib(Suc k) * fib(Suc n) + fib k * fib n";
-by (res_inst_tac [("x","n")] fib.induct 1);
+by (induct_thm_tac fib.induct "n" 1);
(*Simplify the LHS just enough to apply the induction hypotheses*)
by (asm_full_simp_tac
(simpset() addsimps [inst "x" "Suc(?m+?n)" fib_Suc_Suc]) 3);
@@ -35,7 +35,7 @@
Goal "fib (Suc n) ~= 0";
-by (res_inst_tac [("x","n")] fib.induct 1);
+by (induct_thm_tac fib.induct "n" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [fib_Suc_Suc])));
qed "fib_Suc_neq_0";
@@ -52,7 +52,7 @@
Goal "int (fib (Suc (Suc n)) * fib n) = \
\ (if n mod 2 = 0 then int (fib(Suc n) * fib(Suc n)) - #1 \
\ else int (fib(Suc n) * fib(Suc n)) + #1)";
-by (res_inst_tac [("x","n")] fib.induct 1);
+by (induct_thm_tac fib.induct "n" 1);
by (simp_tac (simpset() addsimps [fib_Suc_Suc, mod_Suc]) 2);
by (simp_tac (simpset() addsimps [fib_Suc_Suc]) 1);
by (asm_full_simp_tac
@@ -65,7 +65,7 @@
(** Towards Law 6.111 of Concrete Mathematics **)
Goal "gcd(fib n, fib (Suc n)) = 1";
-by (res_inst_tac [("x","n")] fib.induct 1);
+by (induct_thm_tac fib.induct "n" 1);
by (asm_simp_tac (simpset() addsimps [fib_Suc3, gcd_commute, gcd_add2]) 3);
by (ALLGOALS (simp_tac (simpset() addsimps [fib_Suc_Suc])));
qed "gcd_fib_Suc_eq_1";
@@ -90,7 +90,7 @@
qed "gcd_fib_diff";
Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac less_induct "n" 1);
by (stac mod_if 1);
by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq,
@@ -99,7 +99,7 @@
(*Law 6.111*)
Goal "fib(gcd(m,n)) = gcd(fib m, fib n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (induct_thm_tac gcd_induct "m n" 1);
by (Asm_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1);
by (asm_full_simp_tac (simpset() addsimps [gcd_commute, gcd_fib_mod]) 1);
--- a/src/HOL/ex/Primes.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Primes.ML Wed Aug 30 16:29:21 2000 +0200
@@ -24,7 +24,7 @@
"[| !!m. P m 0; \
\ !!m n. [| 0<n; P n (m mod n) |] ==> P m n \
\ |] ==> P (m::nat) (n::nat)";
-by (res_inst_tac [("u","m"),("v","n")] gcd.induct 1);
+by (induct_thm_tac gcd.induct "m n" 1);
by (case_tac "n=0" 1);
by (asm_simp_tac (simpset() addsimps prems) 1);
by Safe_tac;
@@ -50,7 +50,7 @@
(*gcd(m,n) divides m and n. The conjunctions don't seem provable separately*)
Goal "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (induct_thm_tac gcd_induct "m n" 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0])));
by (blast_tac (claset() addDs [dvd_mod_imp_dvd]) 1);
qed "gcd_dvd_both";
@@ -62,7 +62,7 @@
(*Maximality: for all m,n,f naturals,
if f divides m and f divides n then f divides gcd(m,n)*)
Goal "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (induct_thm_tac gcd_induct "m n" 1);
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps[gcd_non_0, dvd_mod])));
qed_spec_mp "gcd_greatest";
@@ -118,7 +118,7 @@
(*Davenport, page 27*)
Goal "k * gcd(m,n) = gcd(k*m, k*n)";
-by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (induct_thm_tac gcd_induct "m n" 1);
by (Asm_full_simp_tac 1);
by (case_tac "k=0" 1);
by (Asm_full_simp_tac 1);
--- a/src/HOL/ex/Primrec.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Primrec.ML Wed Aug 30 16:29:21 2000 +0200
@@ -46,7 +46,7 @@
(*PROPERTY A 4*)
Goal "j < ack(i,j)";
-by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
+by (induct_thm_tac ack.induct "i j" 1);
by (ALLGOALS Asm_simp_tac);
qed "less_ack2";
@@ -54,7 +54,7 @@
(*PROPERTY A 5-, the single-step lemma*)
Goal "ack(i,j) < ack(i, Suc(j))";
-by (res_inst_tac [("u","i"),("v","j")] ack.induct 1);
+by (induct_thm_tac ack.induct "i j" 1);
by (ALLGOALS Asm_simp_tac);
qed "ack_less_ack_Suc2";
@@ -62,7 +62,7 @@
(*PROPERTY A 5, monotonicity for < *)
Goal "j<k --> ack(i,j) < ack(i,k)";
-by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
+by (induct_thm_tac ack.induct "i k" 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addSEs [less_SucE] addIs [less_trans]) 1);
qed_spec_mp "ack_less_mono2";
@@ -115,10 +115,10 @@
(*PROPERTY A 7, monotonicity for < [not clear why ack_1 is now needed first!]*)
Goal "ack(i,k) < ack(Suc(i+i'),k)";
-by (res_inst_tac [("u","i"),("v","k")] ack.induct 1);
+by (induct_thm_tac ack.induct "i k" 1);
by (ALLGOALS Asm_full_simp_tac);
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 2);
-by (res_inst_tac [("u","i'"),("v","n")] ack.induct 1);
+by (induct_thm_tac ack.induct "i' n" 1);
by (ALLGOALS Asm_simp_tac);
by (blast_tac (claset() addIs [less_trans, ack_less_mono2]) 1);
by (blast_tac (claset() addIs [Suc_leI RS le_less_trans, ack_less_mono2]) 1);
--- a/src/HOL/ex/Puzzle.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Puzzle.ML Wed Aug 30 16:29:21 2000 +0200
@@ -11,7 +11,7 @@
AddSIs [Puzzle.f_ax];
Goal "! n. k=f(n) --> n <= f(n)";
-by (res_inst_tac [("n","k")] less_induct 1);
+by (induct_thm_tac less_induct "k" 1);
by (rtac allI 1);
by (rename_tac "i" 1);
by (case_tac "i" 1);
--- a/src/HOL/ex/Qsort.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Qsort.ML Wed Aug 30 16:29:21 2000 +0200
@@ -9,7 +9,7 @@
(*** Version one: higher-order ***)
Goal "multiset (qsort(le,xs)) x = multiset xs x";
-by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
+by (induct_thm_tac qsort.induct "le xs" 1);
by Auto_tac;
qed "qsort_permutes";
Addsimps [qsort_permutes];
@@ -21,7 +21,7 @@
Addsimps [set_qsort];
Goal "total(le) --> transf(le) --> sorted le (qsort(le,xs))";
-by (res_inst_tac [("v","xs"),("u","le")] qsort.induct 1);
+by (induct_thm_tac qsort.induct "le xs" 1);
by (ALLGOALS Asm_simp_tac);
by (rewrite_goals_tac [Sorting.total_def, Sorting.transf_def]);
by (Blast_tac 1);
--- a/src/HOL/ex/Recdefs.ML Wed Aug 30 16:24:29 2000 +0200
+++ b/src/HOL/ex/Recdefs.ML Wed Aug 30 16:29:21 2000 +0200
@@ -12,12 +12,12 @@
Addsimps g.simps;
Goal "g x < Suc x";
-by (res_inst_tac [("x","x")] g.induct 1);
+by (induct_thm_tac g.induct "x" 1);
by Auto_tac;
qed "g_terminates";
Goal "g x = 0";
-by (res_inst_tac [("x","x")] g.induct 1);
+by (induct_thm_tac g.induct "x" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [g_terminates])));
qed "g_zero";