# HG changeset patch
# User paulson
# Date 864642976 -7200
# Node ID cfa72a70f2b558e0c3b14f51e46da2780ad5f406
# Parent  b99d750f6a3727f705182936f6c893c7d8bf4e04
Tidying and a couple of useful lemmas

diff -r b99d750f6a37 -r cfa72a70f2b5 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon May 26 12:34:54 1997 +0200
+++ b/src/HOL/Arith.ML	Mon May 26 12:36:16 1997 +0200
@@ -34,49 +34,37 @@
 
 qed_goalw "diff_0_eq_0" Arith.thy [pred_def]
     "0 - n = 0"
- (fn _ => [nat_ind_tac "n" 1,  ALLGOALS Asm_simp_tac]);
+ (fn _ => [induct_tac "n" 1,  ALLGOALS Asm_simp_tac]);
 
 (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
   Suc(m) - Suc(n)   rewrites to   pred(Suc(m) - n)  *)
 qed_goalw "diff_Suc_Suc" Arith.thy [pred_def]
     "Suc(m) - Suc(n) = m - n"
  (fn _ =>
-  [Simp_tac 1, nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
+  [Simp_tac 1, induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
 
 Addsimps [diff_0_eq_0, diff_Suc_Suc];
 
 
-goal Arith.thy "!!k. 0<k ==> EX j. k = Suc(j)";
-by (etac rev_mp 1);
-by (nat_ind_tac "k" 1);
-by (Simp_tac 1);
-by (Blast_tac 1);
-val lemma = result();
-
-(* [| 0 < k; !!j. [| j: nat; k = succ(j) |] ==> Q |] ==> Q *)
-bind_thm ("zero_less_natE", lemma RS exE);
-
-
-
 (**** Inductive properties of the operators ****)
 
 (*** Addition ***)
 
 qed_goal "add_0_right" Arith.thy "m + 0 = m"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+ (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
 
 qed_goal "add_Suc_right" Arith.thy "m + Suc(n) = Suc(m+n)"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+ (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
 
 Addsimps [add_0_right,add_Suc_right];
 
 (*Associative law for addition*)
 qed_goal "add_assoc" Arith.thy "(m + n) + k = m + ((n + k)::nat)"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+ (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
 
 (*Commutative law for addition*)  
 qed_goal "add_commute" Arith.thy "m + n = n + (m::nat)"
- (fn _ =>  [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+ (fn _ =>  [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
 
 qed_goal "add_left_commute" Arith.thy "x+(y+z)=y+((x+z)::nat)"
  (fn _ => [rtac (add_commute RS trans) 1, rtac (add_assoc RS trans) 1,
@@ -86,25 +74,25 @@
 val add_ac = [add_assoc, add_commute, add_left_commute];
 
 goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_left_cancel";
 
 goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_right_cancel";
 
 goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_left_cancel_le";
 
 goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "add_left_cancel_less";
@@ -112,20 +100,22 @@
 Addsimps [add_left_cancel, add_right_cancel,
           add_left_cancel_le, add_left_cancel_less];
 
+(** Reasoning about m+0=0, etc. **)
+
 goal Arith.thy "(m+n = 0) = (m=0 & n=0)";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "add_is_0";
 Addsimps [add_is_0];
 
 goal Arith.thy "(pred (m+n) = 0) = (m=0 & pred n = 0 | pred m = 0 & n=0)";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (ALLGOALS (fast_tac (!claset addss (!simpset))));
 qed "pred_add_is_0";
 Addsimps [pred_add_is_0];
 
 goal Arith.thy "!!n. n ~= 0 ==> m + pred n = pred(m+n)";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "add_pred";
 Addsimps [add_pred];
@@ -133,21 +123,25 @@
 
 (**** Additional theorems about "less than" ****)
 
-goal Arith.thy "? k::nat. n = n+k";
-by (res_inst_tac [("x","0")] exI 1);
+goal Arith.thy "i<j --> (EX k. j = Suc(i+k))";
+by (induct_tac "j" 1);
 by (Simp_tac 1);
+by (blast_tac (!claset addSEs [less_SucE] 
+                       addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
 val lemma = result();
 
+(* [| i<j;  !!x. j = Suc(i+x) ==> Q |] ==> Q *)
+bind_thm ("less_natE", lemma RS mp RS exE);
+
 goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS (simp_tac (!simpset addsimps [less_Suc_eq])));
-by (step_tac (!claset addSIs [lemma]) 1);
-by (res_inst_tac [("x","Suc(k)")] exI 1);
-by (Simp_tac 1);
+by (blast_tac (!claset addSEs [less_SucE] 
+                       addSIs [add_0_right RS sym, add_Suc_right RS sym]) 1);
 qed_spec_mp "less_eq_Suc_add";
 
 goal Arith.thy "n <= ((m + n)::nat)";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (ALLGOALS Simp_tac);
 by (etac le_trans 1);
 by (rtac (lessI RS less_imp_le) 1);
@@ -175,7 +169,7 @@
 
 goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
 by (etac rev_mp 1);
-by (nat_ind_tac "j" 1);
+by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
 by (blast_tac (!claset addDs [Suc_lessD]) 1);
 qed "add_lessD1";
@@ -201,7 +195,7 @@
 qed "less_imp_add_less";
 
 goal Arith.thy "m+k<=n --> m<=(n::nat)";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
 by (blast_tac (!claset addDs [Suc_leD]) 1);
 qed_spec_mp "add_leD1";
@@ -229,7 +223,7 @@
 
 (*strict, in 1st argument*)
 goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "add_less_mono1";
 
@@ -237,7 +231,7 @@
 goal Arith.thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l";
 by (rtac (add_less_mono1 RS less_trans) 1);
 by (REPEAT (assume_tac 1));
-by (nat_ind_tac "j" 1);
+by (induct_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "add_less_mono";
 
@@ -271,11 +265,11 @@
 
 (*right annihilation in product*)
 qed_goal "mult_0_right" Arith.thy "m * 0 = 0"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+ (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
 
 (*right successor law for multiplication*)
 qed_goal "mult_Suc_right" Arith.thy  "m * Suc(n) = m + (m * n)"
- (fn _ => [nat_ind_tac "m" 1,
+ (fn _ => [induct_tac "m" 1,
            ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
 
 Addsimps [mult_0_right, mult_Suc_right];
@@ -290,20 +284,20 @@
 
 (*Commutative law for multiplication*)
 qed_goal "mult_commute" Arith.thy "m * n = n * (m::nat)"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+ (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
 
 (*addition distributes over multiplication*)
 qed_goal "add_mult_distrib" Arith.thy "(m + n)*k = (m*k) + ((n*k)::nat)"
- (fn _ => [nat_ind_tac "m" 1,
+ (fn _ => [induct_tac "m" 1,
            ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
 
 qed_goal "add_mult_distrib2" Arith.thy "k*(m + n) = (k*m) + ((k*n)::nat)"
- (fn _ => [nat_ind_tac "m" 1,
+ (fn _ => [induct_tac "m" 1,
            ALLGOALS(asm_simp_tac (!simpset addsimps add_ac))]);
 
 (*Associative law for multiplication*)
 qed_goal "mult_assoc" Arith.thy "(m * n) * k = m * ((n * k)::nat)"
-  (fn _ => [nat_ind_tac "m" 1, 
+  (fn _ => [induct_tac "m" 1, 
             ALLGOALS (asm_simp_tac (!simpset addsimps [add_mult_distrib]))]);
 
 qed_goal "mult_left_commute" Arith.thy "x*(y*z) = y*((x*z)::nat)"
@@ -313,8 +307,8 @@
 val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
 
 goal Arith.thy "(m*n = 0) = (m=0 | n=0)";
-by (nat_ind_tac "m" 1);
-by (nat_ind_tac "n" 2);
+by (induct_tac "m" 1);
+by (induct_tac "n" 2);
 by (ALLGOALS Asm_simp_tac);
 qed "mult_is_0";
 Addsimps [mult_is_0];
@@ -323,11 +317,11 @@
 (*** Difference ***)
 
 qed_goal "pred_Suc_diff" Arith.thy "pred(Suc m - n) = m - n"
- (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
+ (fn _ => [induct_tac "n" 1, ALLGOALS Asm_simp_tac]);
 Addsimps [pred_Suc_diff];
 
 qed_goal "diff_self_eq_0" Arith.thy "m - m = 0"
- (fn _ => [nat_ind_tac "m" 1, ALLGOALS Asm_simp_tac]);
+ (fn _ => [induct_tac "m" 1, ALLGOALS Asm_simp_tac]);
 Addsimps [diff_self_eq_0];
 
 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
@@ -354,7 +348,7 @@
 qed "diff_le_self";
 
 goal Arith.thy "!!n::nat. (n+m) - n = m";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_add_inverse";
 Addsimps [diff_add_inverse];
@@ -406,7 +400,7 @@
 qed "zero_induct";
 
 goal Arith.thy "!!k::nat. (k+m) - (k+n) = m - n";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_cancel";
 Addsimps [diff_cancel];
@@ -421,7 +415,7 @@
 goal Arith.thy "!!n::nat. [| k<=n; n<=m |] ==> (m-k) - (n-k) = m-n";
 by (subgoal_tac "k<=n --> n<=m --> (m-k) - (n-k) = m-n" 1);
 by (Asm_full_simp_tac 1);
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (Simp_tac 1);
 (* Induction step *)
 by (subgoal_tac "Suc na <= m --> n <= m --> Suc na <= n --> \
@@ -434,7 +428,7 @@
 qed "diff_right_cancel";
 
 goal Arith.thy "!!n::nat. n - (n+m) = 0";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_add_0";
 Addsimps [diff_add_0];
@@ -500,7 +494,7 @@
 qed "mod_eq_add";
 
 goal thy "!!n. 0<n ==> m*n mod n = 0";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (asm_simp_tac (!simpset addsimps [mod_less]) 1);
 by (dres_inst_tac [("m","m*n")] mod_eq_add 1);
 by (asm_full_simp_tac (!simpset addsimps [add_commute]) 1);
@@ -592,7 +586,7 @@
 qed "mod2_neq_0";
 
 goal thy "(m+m) mod 2 = 0";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (simp_tac (!simpset addsimps [mod_less]) 1);
 by (asm_simp_tac (!simpset addsimps [mod2_Suc_Suc, add_Suc_right]) 1);
 qed "mod2_add_self";
@@ -604,7 +598,7 @@
 (*** Monotonicity of Multiplication ***)
 
 goal Arith.thy "!!i::nat. i<=j ==> i*k<=j*k";
-by (nat_ind_tac "k" 1);
+by (induct_tac "k" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_le_mono])));
 qed "mult_le_mono1";
 
@@ -619,9 +613,9 @@
 
 (*strict, in 1st argument; proof is by induction on k>0*)
 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> k*i < k*j";
-by (etac zero_less_natE 1);
+by (eres_inst_tac [("i","0")] less_natE 1);
 by (Asm_simp_tac 1);
-by (nat_ind_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [add_less_mono])));
 qed "mult_less_mono2";
 
@@ -631,15 +625,15 @@
 qed "mult_less_mono1";
 
 goal Arith.thy "(0 < m*n) = (0<m & 0<n)";
-by (nat_ind_tac "m" 1);
-by (nat_ind_tac "n" 2);
+by (induct_tac "m" 1);
+by (induct_tac "n" 2);
 by (ALLGOALS Asm_simp_tac);
 qed "zero_less_mult_iff";
 
 goal Arith.thy "(m*n = 1) = (m=1 & n=1)";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (Simp_tac 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (Simp_tac 1);
 by (fast_tac (!claset addss !simpset) 1);
 qed "mult_eq_1_iff";