src/HOL/Nat.thy
changeset 30079 293b896b9c25
parent 30056 0a35bee25c20
child 30093 ecb557b021b2
--- a/src/HOL/Nat.thy	Mon Feb 23 13:55:36 2009 -0800
+++ b/src/HOL/Nat.thy	Mon Feb 23 16:25:52 2009 -0800
@@ -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)
@@ -307,18 +307,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 +471,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
@@ -800,6 +806,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)
@@ -1089,7 +1096,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)
@@ -1125,7 +1132,7 @@
   by (cases m) (auto intro: le_add1)
 
 text {* Lemma for @{text gcd} *}
-lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
+lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
   apply (drule sym)
   apply (rule disjCI)
   apply (rule nat_less_cases, erule_tac [2] _)
@@ -1164,7 +1171,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)
@@ -1276,7 +1283,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)
@@ -1381,7 +1388,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