--- 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";