src/HOL/Nat.thy
 changeset 30240 5b25fee0362c parent 29879 4425849f5db7 child 30242 aea5d7fa7ef5
```     1.1 --- a/src/HOL/Nat.thy	Wed Mar 04 10:43:39 2009 +0100
1.2 +++ b/src/HOL/Nat.thy	Wed Mar 04 10:45:52 2009 +0100
1.3 @@ -196,8 +196,8 @@
1.4
1.5  instance proof
1.6    fix n m q :: nat
1.7 -  show "0 \<noteq> (1::nat)" by simp
1.8 -  show "1 * n = n" by simp
1.9 +  show "0 \<noteq> (1::nat)" unfolding One_nat_def by simp
1.10 +  show "1 * n = n" unfolding One_nat_def by simp
1.11    show "n * m = m * n" by (induct n) simp_all
1.12    show "(n * m) * q = n * (m * q)" by (induct n) (simp_all add: add_mult_distrib)
1.13    show "(n + m) * q = n * q + m * q" by (rule add_mult_distrib)
1.14 @@ -280,6 +280,9 @@
1.15  lemma diff_add_0: "n - (n + m) = (0::nat)"
1.16    by (induct n) simp_all
1.17
1.18 +lemma diff_Suc_1 [simp]: "Suc n - 1 = n"
1.19 +  unfolding One_nat_def by simp
1.20 +
1.21  text {* Difference distributes over multiplication *}
1.22
1.23  lemma diff_mult_distrib: "((m::nat) - n) * k = (m * k) - (n * k)"
1.24 @@ -307,18 +310,24 @@
1.25  lemmas nat_distrib =
1.27
1.28 -lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
1.29 +lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
1.30    apply (induct m)
1.31     apply simp
1.32    apply (induct n)
1.33     apply auto
1.34    done
1.35
1.36 -lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
1.37 +lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
1.38    apply (rule trans)
1.39    apply (rule_tac [2] mult_eq_1_iff, fastsimp)
1.40    done
1.41
1.42 +lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
1.43 +  unfolding One_nat_def by (rule mult_eq_1_iff)
1.44 +
1.45 +lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
1.46 +  unfolding One_nat_def by (rule one_eq_mult_iff)
1.47 +
1.48  lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
1.49  proof -
1.50    have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
1.51 @@ -465,11 +474,11 @@
1.52  lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
1.53    unfolding less_Suc_eq_le le_less ..
1.54
1.55 -lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
1.56 +lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
1.58
1.59 -lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
1.60 -  by (simp add: less_Suc_eq)
1.61 +lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
1.62 +  unfolding One_nat_def by (rule less_Suc0)
1.63
1.64  lemma Suc_mono: "m < n ==> Suc m < Suc n"
1.65    by simp
1.66 @@ -692,6 +701,9 @@
1.67  lemma Suc_pred [simp]: "n>0 ==> Suc (n - Suc 0) = n"
1.68  by (simp add: diff_Suc split: nat.split)
1.69
1.70 +lemma Suc_diff_1 [simp]: "0 < n ==> Suc (n - 1) = n"
1.71 +unfolding One_nat_def by (rule Suc_pred)
1.72 +
1.73  lemma nat_add_left_cancel_le [simp]: "(k + m \<le> k + n) = (m\<le>(n::nat))"
1.74  by (induct k) simp_all
1.75
1.76 @@ -735,6 +747,11 @@
1.77    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
1.78  qed
1.79
1.80 +instance nat :: no_zero_divisors
1.81 +proof
1.82 +  fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
1.83 +qed
1.84 +
1.85  lemma nat_mult_1: "(1::nat) * n = n"
1.86  by simp
1.87
1.88 @@ -795,6 +812,7 @@
1.89    done
1.90
1.91  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)"
1.92 +  unfolding One_nat_def
1.93    apply (cases n)
1.94     apply blast
1.95    apply (frule (1) ex_least_nat_le)
1.96 @@ -1084,7 +1102,7 @@
1.97     apply simp_all
1.98    done
1.99
1.100 -lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
1.101 +lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"
1.102    apply (induct m)
1.103     apply simp
1.104    apply (case_tac n)
1.105 @@ -1159,7 +1177,7 @@
1.106    | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
1.107
1.108  lemma of_nat_1 [simp]: "of_nat 1 = 1"
1.109 -  by simp
1.110 +  unfolding One_nat_def by simp
1.111
1.112  lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
1.114 @@ -1271,7 +1289,7 @@
1.115  end
1.116
1.117  lemma of_nat_id [simp]: "of_nat n = n"
1.118 -  by (induct n) auto
1.119 +  by (induct n) (auto simp add: One_nat_def)
1.120
1.121  lemma of_nat_eq_id [simp]: "of_nat = id"
1.122    by (auto simp add: expand_fun_eq)
1.123 @@ -1376,7 +1394,7 @@
1.124  apply(induct_tac k)
1.125   apply simp
1.126  apply(erule_tac x="m+n" in meta_allE)
1.127 -apply(erule_tac x="m+n+1" in meta_allE)
1.128 +apply(erule_tac x="Suc(m+n)" in meta_allE)
1.129  apply simp
1.130  done
1.131
```