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.26    add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
    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.57    by (simp add: less_Suc_eq)
    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.113    by (induct m) (simp_all add: add_ac)
   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