--- a/src/HOL/Divides.ML Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/Divides.ML Wed Sep 06 08:04:41 2000 +0200
@@ -104,7 +104,7 @@
Goal "(m mod n) * (k::nat) = (m*k) mod (n*k)";
by (div_undefined_case_tac "n=0" 1);
by (div_undefined_case_tac "k=0" 1);
-by (res_inst_tac [("n","m")] less_induct 1);
+by (induct_thm_tac nat_less_induct "m" 1);
by (stac mod_if 1);
by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [mod_geq,
@@ -158,7 +158,7 @@
(*Main Result about quotient and remainder.*)
Goal "(m div n)*n + m mod n = (m::nat)";
by (div_undefined_case_tac "n=0" 1);
-by (res_inst_tac [("n","m")] less_induct 1);
+by (induct_thm_tac nat_less_induct "m" 1);
by (stac mod_if 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps [add_assoc, div_geq,
@@ -220,7 +220,7 @@
(* Monotonicity of div in first argument *)
Goal "ALL m::nat. m <= n --> (m div k) <= (n div k)";
by (div_undefined_case_tac "k=0" 1);
-by (res_inst_tac [("n","n")] less_induct 1);
+by (induct_thm_tac nat_less_induct "n" 1);
by (Clarify_tac 1);
by (case_tac "n<k" 1);
(* 1 case n<k *)
@@ -237,7 +237,7 @@
Goal "!!m::nat. [| 0<m; m<=n |] ==> (k div n) <= (k div m)";
by (subgoal_tac "0<n" 1);
by (Asm_simp_tac 2);
-by (res_inst_tac [("n","k")] less_induct 1);
+by (induct_thm_tac nat_less_induct "k" 1);
by (rename_tac "k" 1);
by (case_tac "k<n" 1);
by (Asm_simp_tac 1);
@@ -262,7 +262,7 @@
(* Similar for "less than" *)
Goal "!!n::nat. 1<n ==> (0 < m) --> (m div n < m)";
-by (res_inst_tac [("n","m")] less_induct 1);
+by (induct_thm_tac nat_less_induct "m" 1);
by (rename_tac "m" 1);
by (case_tac "m<n" 1);
by (Asm_full_simp_tac 1);
@@ -284,7 +284,7 @@
(*** Further facts about mod (mainly for the mutilated chess board ***)
Goal "0<n ==> Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))";
-by (res_inst_tac [("n","m")] less_induct 1);
+by (induct_thm_tac nat_less_induct "m" 1);
by (case_tac "Suc(na)<n" 1);
(* case Suc(na) < n *)
by (forward_tac [lessI RS less_trans] 1
@@ -297,7 +297,7 @@
qed "mod_Suc";
Goal "0<n ==> m mod n < (n::nat)";
-by (res_inst_tac [("n","m")] less_induct 1);
+by (induct_thm_tac nat_less_induct "m" 1);
by (case_tac "na<n" 1);
(*case n le na*)
by (asm_full_simp_tac (simpset() addsimps [mod_geq, diff_less]) 2);
@@ -321,7 +321,7 @@
(*Cancellation law for division*)
Goal "0<k ==> (k*m) div (k*n) = m div (n::nat)";
by (div_undefined_case_tac "n=0" 1);
-by (res_inst_tac [("n","m")] less_induct 1);
+by (induct_thm_tac nat_less_induct "m" 1);
by (case_tac "na<n" 1);
by (asm_simp_tac (simpset() addsimps [zero_less_mult_iff, mult_less_mono2]) 1);
by (subgoal_tac "~ k*na < k*n" 1);
--- a/src/HOL/IMP/Transition.ML Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/IMP/Transition.ML Wed Sep 06 08:04:41 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 (induct_thm_tac less_induct "n" 1);
+by (induct_thm_tac nat_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 (induct_thm_tac less_induct "n" 1);
+by (induct_thm_tac nat_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 Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/Induct/LList.ML Wed Sep 06 08:04:41 2000 +0200
@@ -128,7 +128,7 @@
qed "LListD_unfold";
Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
-by (induct_thm_tac less_induct "k" 1);
+by (induct_thm_tac nat_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 (induct_thm_tac less_induct "k" 1);
+by (induct_thm_tac nat_less_induct "k" 1);
by (rename_tac "n" 1);
by (rtac allI 1);
by (rename_tac "y" 1);
--- a/src/HOL/Isar_examples/Fibonacci.thy Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/Isar_examples/Fibonacci.thy Wed Sep 06 08:04:41 2000 +0200
@@ -126,7 +126,7 @@
lemma gcd_fib_mod:
"0 < m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
-proof (induct n rule: less_induct);
+proof (induct n rule: nat_less_induct);
fix n;
assume m: "0 < m"
and hyp: "ALL ma. ma < n
--- a/src/HOL/Isar_examples/Puzzle.thy Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy Wed Sep 06 08:04:41 2000 +0200
@@ -26,7 +26,7 @@
{;
fix k;
have "ALL x. k = f x --> ?C x" (is "?Q k");
- proof (rule less_induct);
+ proof (rule nat_less_induct);
fix k; assume hyp: "ALL m<k. ?Q m";
show "?Q k";
proof;
--- a/src/HOL/Lambda/ListApplication.thy Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/Lambda/ListApplication.thy Wed Sep 06 08:04:41 2000 +0200
@@ -110,7 +110,7 @@
proof -
case antecedent
show ?thesis
- apply (induct_tac n rule: less_induct)
+ apply (induct_tac n rule: nat_less_induct)
apply (rule allI)
apply (cut_tac t = t in ex_head_tail)
apply clarify
@@ -159,4 +159,4 @@
done
qed
-end
\ No newline at end of file
+end
--- a/src/HOL/Nat.ML Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/Nat.ML Wed Sep 06 08:04:41 2000 +0200
@@ -95,7 +95,7 @@
qed "Least_Suc";
val prems = Goal "[| P 0; P 1; !!k. P k ==> P (Suc (Suc k)) |] ==> P n";
-by (rtac less_induct 1);
+by (rtac nat_less_induct 1);
by (case_tac "n" 1);
by (case_tac "nat" 2);
by (ALLGOALS (blast_tac (claset() addIs prems@[less_trans])));
--- a/src/HOL/NatDef.ML Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/NatDef.ML Wed Sep 06 08:04:41 2000 +0200
@@ -295,7 +295,7 @@
"[| !!n. [| ALL m::nat. m<n --> P(m) |] ==> P(n) |] ==> P(n)";
by (wf_ind_tac "n" [wf_pred_nat RS wf_trancl] 1);
by (eresolve_tac prems 1);
-qed "less_induct";
+qed "nat_less_induct";
(*** Properties of <= ***)
@@ -484,7 +484,7 @@
Goal "P(k::nat) ==> P(LEAST x. P(x))";
by (etac rev_mp 1);
-by (res_inst_tac [("n","k")] less_induct 1);
+by (res_inst_tac [("n","k")] nat_less_induct 1);
by (rtac impI 1);
by (rtac classical 1);
by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
@@ -496,7 +496,7 @@
(*Proof is almost identical to the one above!*)
Goal "P(k::nat) ==> (LEAST x. P(x)) <= k";
by (etac rev_mp 1);
-by (res_inst_tac [("n","k")] less_induct 1);
+by (res_inst_tac [("n","k")] nat_less_induct 1);
by (rtac impI 1);
by (rtac classical 1);
by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
--- a/src/HOL/ex/Factorization.ML Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/ex/Factorization.ML Wed Sep 06 08:04:41 2000 +0200
@@ -198,7 +198,7 @@
qed "split_primel";
Goal "1<n --> (EX l. primel l & prod l = n)";
-by (induct_thm_tac less_induct "n" 1);
+by (induct_thm_tac nat_less_induct "n" 1);
by (rtac impI 1);
by (case_tac "n:prime" 1);
by (rtac exI 1);
@@ -270,7 +270,7 @@
Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \
\ --> xs <~~> ys)";
-by (induct_thm_tac less_induct "n" 1);
+by (induct_thm_tac nat_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 Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/ex/Fib.ML Wed Sep 06 08:04:41 2000 +0200
@@ -97,7 +97,7 @@
qed "gcd_fib_diff";
Goal "0<m ==> gcd (fib m, fib (n mod m)) = gcd (fib m, fib n)";
-by (induct_thm_tac less_induct "n" 1);
+by (induct_thm_tac nat_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,
--- a/src/HOL/ex/Puzzle.ML Tue Sep 05 21:06:01 2000 +0200
+++ b/src/HOL/ex/Puzzle.ML Wed Sep 06 08:04:41 2000 +0200
@@ -11,7 +11,7 @@
AddSIs [Puzzle.f_ax];
Goal "! n. k=f(n) --> n <= f(n)";
-by (induct_thm_tac less_induct "k" 1);
+by (induct_thm_tac nat_less_induct "k" 1);
by (rtac allI 1);
by (rename_tac "i" 1);
by (case_tac "i" 1);