--- a/src/HOL/Nat.thy Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Nat.thy Wed Mar 04 10:45:52 2009 +0100
@@ -196,8 +196,8 @@
instance proof
fix n m q :: nat
- show "0 \<noteq> (1::nat)" by simp
- show "1 * n = n" by simp
+ show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
+ show "1 * n = n" unfolding One_nat_def by simp
show "n * m = m * n" by (induct n) simp_all
show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
@@ -280,6 +280,9 @@
lemma diff_add_0: "n - (n + m) = (0::nat)"
by (induct n) simp_all
+lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
+ unfolding One_nat_def by simp
+
text {* Difference distributes over multiplication *}
lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
@@ -307,18 +310,24 @@
lemmas nat_distrib =
add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
-lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
+lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
apply (induct m)
apply simp
apply (induct n)
apply auto
done
-lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
+lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
apply (rule trans)
apply (rule_tac [2] mult_eq_1_iff, fastsimp)
done
+lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
+ unfolding One_nat_def by (rule mult_eq_1_iff)
+
+lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
+ unfolding One_nat_def by (rule one_eq_mult_iff)
+
lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
proof -
have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
@@ -465,11 +474,11 @@
lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
unfolding less_Suc_eq_le le_less ..
-lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
by (simp add: less_Suc_eq)
-lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
- by (simp add: less_Suc_eq)
+lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
+ unfolding One_nat_def by (rule less_Suc0)
lemma Suc_mono: "m < n ==> Suc m < Suc n"
by simp
@@ -692,6 +701,9 @@
lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
by (simp add: diff_Suc split: nat.split)
+lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"
+unfolding One_nat_def by (rule Suc_pred)
+
lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
by (induct k) simp_all
@@ -735,6 +747,11 @@
show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
qed
+instance nat :: no_zero_divisors
+proof
+ fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
+qed
+
lemma nat_mult_1: "(1::nat) * n = n"
by simp
@@ -795,6 +812,7 @@
done
lemma ex_least_nat_less: "\<not>P(0) \<Longrightarrow> P(n::nat) \<Longrightarrow> \<exists>k<n. (\<forall>i\<le>k. \<not>P i) & P(k+1)"
+ unfolding One_nat_def
apply (cases n)
apply blast
apply (frule (1) ex_least_nat_le)
@@ -1084,7 +1102,7 @@
apply simp_all
done
-lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
+lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"
apply (induct m)
apply simp
apply (case_tac n)
@@ -1159,7 +1177,7 @@
| of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
lemma of_nat_1 [simp]: "of_nat 1 = 1"
- by simp
+ unfolding One_nat_def by simp
lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
by (induct m) (simp_all add: add_ac)
@@ -1271,7 +1289,7 @@
end
lemma of_nat_id [simp]: "of_nat n = n"
- by (induct n) auto
+ by (induct n) (auto simp add: One_nat_def)
lemma of_nat_eq_id [simp]: "of_nat = id"
by (auto simp add: expand_fun_eq)
@@ -1376,7 +1394,7 @@
apply(induct_tac k)
apply simp
apply(erule_tac x="m+n" in meta_allE)
-apply(erule_tac x="m+n+1" in meta_allE)
+apply(erule_tac x="Suc(m+n)" in meta_allE)
apply simp
done