# HG changeset patch # User nipkow # Date 967645761 -7200 # Node ID 043098ba5098c4b7a2fa12799b919ca44f5a873b # Parent 64b803edef396c5897eb080549cb76330f1e2eca introduced induct_thm_tac diff -r 64b803edef39 -r 043098ba5098 src/HOL/IMP/Transition.ML --- 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-> 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/Induct/LList.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/Induct/Multiset.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/Induct/Perm.ML --- 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"; diff -r 64b803edef39 -r 043098ba5098 src/HOL/Induct/SList.ML --- 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 ***) diff -r 64b803edef39 -r 043098ba5098 src/HOL/Integ/IntDiv.ML --- 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 #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*) diff -r 64b803edef39 -r 043098ba5098 src/HOL/Integ/int_arith2.ML --- 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"; diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lambda/ListApplication.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lambda/ListBeta.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lambda/ParRed.ML --- 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"; diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lex/MaxChop.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lex/Prefix.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/Lex/RegExp2NAe.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/List.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/MiniML/MiniML.ML --- 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(); diff -r 64b803edef39 -r 043098ba5098 src/HOL/MiniML/Type.ML --- 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"; diff -r 64b803edef39 -r 043098ba5098 src/HOL/NumberTheory/EulerFermat.ML --- 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 #0 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 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 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 a 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

(ALL b. #0 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; diff -r 64b803edef39 -r 043098ba5098 src/HOL/NumberTheory/IntFact.ML --- 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<=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<=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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/NumberTheory/IntPrimes.ML --- 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, diff -r 64b803edef39 -r 043098ba5098 src/HOL/NumberTheory/WilsonRuss.ML --- 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 b:(wset(a,p)) --> #1 a b:(wset(a,p)) --> b a #1 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 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 [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; diff -r 64b803edef39 -r 043098ba5098 src/HOL/Real/Hyperreal/Zorn.ML --- 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]; diff -r 64b803edef39 -r 043098ba5098 src/HOL/Real/PNat.ML --- 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; \ diff -r 64b803edef39 -r 043098ba5098 src/HOL/Real/PReal.ML --- 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])); diff -r 64b803edef39 -r 043098ba5098 src/HOL/Subst/AList.ML --- 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)]; diff -r 64b803edef39 -r 043098ba5098 src/HOL/Tools/datatype_package.ML --- 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; diff -r 64b803edef39 -r 043098ba5098 src/HOL/UNITY/AllocBase.ML --- 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, diff -r 64b803edef39 -r 043098ba5098 src/HOL/UNITY/GenPrefix.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/While.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Factorization.ML --- 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 (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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Fib.ML --- 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 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Primes.ML --- 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 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Primrec.ML --- 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 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Puzzle.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Qsort.ML --- 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); diff -r 64b803edef39 -r 043098ba5098 src/HOL/ex/Recdefs.ML --- 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";