src/HOL/Nat.thy
changeset 30079 293b896b9c25
parent 30056 0a35bee25c20
child 30093 ecb557b021b2
     1.1 --- a/src/HOL/Nat.thy	Mon Feb 23 13:55:36 2009 -0800
     1.2 +++ b/src/HOL/Nat.thy	Mon Feb 23 16:25:52 2009 -0800
     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 @@ -307,18 +307,24 @@
    1.15  lemmas nat_distrib =
    1.16    add_mult_distrib add_mult_distrib2 diff_mult_distrib diff_mult_distrib2
    1.17  
    1.18 -lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = 1 & n = 1)"
    1.19 +lemma mult_eq_1_iff [simp]: "(m * n = Suc 0) = (m = Suc 0 & n = Suc 0)"
    1.20    apply (induct m)
    1.21     apply simp
    1.22    apply (induct n)
    1.23     apply auto
    1.24    done
    1.25  
    1.26 -lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = 1 & n = 1)"
    1.27 +lemma one_eq_mult_iff [simp,noatp]: "(Suc 0 = m * n) = (m = Suc 0 & n = Suc 0)"
    1.28    apply (rule trans)
    1.29    apply (rule_tac [2] mult_eq_1_iff, fastsimp)
    1.30    done
    1.31  
    1.32 +lemma nat_mult_eq_1_iff [simp]: "m * n = (1::nat) \<longleftrightarrow> m = 1 \<and> n = 1"
    1.33 +  unfolding One_nat_def by (rule mult_eq_1_iff)
    1.34 +
    1.35 +lemma nat_1_eq_mult_iff [simp]: "(1::nat) = m * n \<longleftrightarrow> m = 1 \<and> n = 1"
    1.36 +  unfolding One_nat_def by (rule one_eq_mult_iff)
    1.37 +
    1.38  lemma mult_cancel1 [simp]: "(k * m = k * n) = (m = n | (k = (0::nat)))"
    1.39  proof -
    1.40    have "k \<noteq> 0 \<Longrightarrow> k * m = k * n \<Longrightarrow> m = n"
    1.41 @@ -465,11 +471,11 @@
    1.42  lemma less_Suc_eq: "(m < Suc n) = (m < n | m = n)"
    1.43    unfolding less_Suc_eq_le le_less ..
    1.44  
    1.45 -lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
    1.46 +lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
    1.47    by (simp add: less_Suc_eq)
    1.48  
    1.49 -lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
    1.50 -  by (simp add: less_Suc_eq)
    1.51 +lemma less_one [iff, noatp]: "(n < (1::nat)) = (n = 0)"
    1.52 +  unfolding One_nat_def by (rule less_Suc0)
    1.53  
    1.54  lemma Suc_mono: "m < n ==> Suc m < Suc n"
    1.55    by simp
    1.56 @@ -800,6 +806,7 @@
    1.57    done
    1.58  
    1.59  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.60 +  unfolding One_nat_def
    1.61    apply (cases n)
    1.62     apply blast
    1.63    apply (frule (1) ex_least_nat_le)
    1.64 @@ -1089,7 +1096,7 @@
    1.65     apply simp_all
    1.66    done
    1.67  
    1.68 -lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (1 \<le> m & 1 \<le> n)"
    1.69 +lemma one_le_mult_iff [simp]: "(Suc 0 \<le> m * n) = (Suc 0 \<le> m & Suc 0 \<le> n)"
    1.70    apply (induct m)
    1.71     apply simp
    1.72    apply (case_tac n)
    1.73 @@ -1125,7 +1132,7 @@
    1.74    by (cases m) (auto intro: le_add1)
    1.75  
    1.76  text {* Lemma for @{text gcd} *}
    1.77 -lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = 1 | m = 0"
    1.78 +lemma mult_eq_self_implies_10: "(m::nat) = m * n ==> n = Suc 0 | m = 0"
    1.79    apply (drule sym)
    1.80    apply (rule disjCI)
    1.81    apply (rule nat_less_cases, erule_tac [2] _)
    1.82 @@ -1164,7 +1171,7 @@
    1.83    | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
    1.84  
    1.85  lemma of_nat_1 [simp]: "of_nat 1 = 1"
    1.86 -  by simp
    1.87 +  unfolding One_nat_def by simp
    1.88  
    1.89  lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
    1.90    by (induct m) (simp_all add: add_ac)
    1.91 @@ -1276,7 +1283,7 @@
    1.92  end
    1.93  
    1.94  lemma of_nat_id [simp]: "of_nat n = n"
    1.95 -  by (induct n) auto
    1.96 +  by (induct n) (auto simp add: One_nat_def)
    1.97  
    1.98  lemma of_nat_eq_id [simp]: "of_nat = id"
    1.99    by (auto simp add: expand_fun_eq)
   1.100 @@ -1381,7 +1388,7 @@
   1.101  apply(induct_tac k)
   1.102   apply simp
   1.103  apply(erule_tac x="m+n" in meta_allE)
   1.104 -apply(erule_tac x="m+n+1" in meta_allE)
   1.105 +apply(erule_tac x="Suc(m+n)" in meta_allE)
   1.106  apply simp
   1.107  done
   1.108