src/HOL/Nat.thy

 lemma add_mult_distrib: "(m + n) * k = (m * k) + ((n * k)::nat)"
   by (induct m) (simp_all add: add_assoc)
 
 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)
   assume "n + m = n + q" thus "m = q" by (induct n) simp_all
 qed

   by (simp add: diff_cancel add_commute)
 
 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)"
 by (induct m n rule: diff_induct) (simp_all add: diff_cancel)
 

   by (induct m) auto
 
 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"
   proof (induct n arbitrary: m)

   by (rule notE) (rule not_less0)
 
 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)"
-  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
 
 text {* "Less than" is antisymmetric, sort of *}

 subsubsection {* Monotonicity of Addition *}
 
 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
 
 lemma nat_add_left_cancel_less [simp]: "(k + m < k + n) = (m<(n::nat))"
 by (induct k) simp_all

 proof
   fix i j k :: nat
   show "0 < (1::nat)" by simp
   show "i \<le> j ==> k + i \<le> k + j" by simp
   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
 

   apply (rule_tac x="LEAST k. P(k)" in exI)
   apply (blast intro: Least_le dest: not_less_Least intro: LeastI_ex)
   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)
   apply (erule exE)
   apply (case_tac k)

    apply simp
   apply (case_tac n)
    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)
    apply simp_all
   done

 where
   of_nat_0:     "of_nat 0 = 0"
   | 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)
 
 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"

   unfolding abs_if by auto
 
 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)
 
 

 lemma mono_nat_linear_lb:
   "(!!m n::nat. m<n \<Longrightarrow> f m < f n) \<Longrightarrow> f(m)+k \<le> f(m+k)"
 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
 
 
 text{*Subtraction laws, mostly by Clemens Ballarin*}