# HG changeset patch
# User nipkow
# Date 968220281 -7200
# Node ID 2374ba026fc6ab2a0b86206503dee878e875affc
# Parent  95dca9f991f26be223194ebb03a530fc3f845a58
less_induct -> nat_less_induct

diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/Divides.ML
--- 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);
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/IMP/Transition.ML
--- 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);
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/Induct/LList.ML
--- 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);
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/Isar_examples/Fibonacci.thy
--- 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
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/Isar_examples/Puzzle.thy
--- 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;
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/Lambda/ListApplication.thy
--- 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
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/Nat.ML
--- 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])));
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/NatDef.ML
--- 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);
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/ex/Factorization.ML
--- 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);
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/ex/Fib.ML
--- 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, 
diff -r 95dca9f991f2 -r 2374ba026fc6 src/HOL/ex/Puzzle.ML
--- 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);