src/HOL/Int.thy
changeset 54223 85705ba18add
parent 54147 97a8ff4e4ac9
child 54230 b1d955791529
     1.1 --- a/src/HOL/Int.thy	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/src/HOL/Int.thy	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -349,12 +349,33 @@
     1.4    shows P
     1.5    using assms by (blast dest: nat_0_le sym)
     1.6  
     1.7 -lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"
     1.8 +lemma nat_eq_iff:
     1.9 +  "nat w = m \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
    1.10    by transfer (clarsimp simp add: le_imp_diff_is_add)
    1.11 + 
    1.12 +corollary nat_eq_iff2:
    1.13 +  "m = nat w \<longleftrightarrow> (if 0 \<le> w then w = int m else m = 0)"
    1.14 +  using nat_eq_iff [of w m] by auto
    1.15 +
    1.16 +lemma nat_0 [simp]:
    1.17 +  "nat 0 = 0"
    1.18 +  by (simp add: nat_eq_iff)
    1.19  
    1.20 -corollary nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"
    1.21 -by (simp only: eq_commute [of m] nat_eq_iff)
    1.22 +lemma nat_1 [simp]:
    1.23 +  "nat 1 = Suc 0"
    1.24 +  by (simp add: nat_eq_iff)
    1.25 +
    1.26 +lemma nat_numeral [simp]:
    1.27 +  "nat (numeral k) = numeral k"
    1.28 +  by (simp add: nat_eq_iff)
    1.29  
    1.30 +lemma nat_neg_numeral [simp]:
    1.31 +  "nat (neg_numeral k) = 0"
    1.32 +  by simp
    1.33 +
    1.34 +lemma nat_2: "nat 2 = Suc (Suc 0)"
    1.35 +  by simp
    1.36 + 
    1.37  lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < of_nat m)"
    1.38    by transfer (clarsimp, arith)
    1.39  
    1.40 @@ -374,12 +395,16 @@
    1.41  by (insert zless_nat_conj [of 0], auto)
    1.42  
    1.43  lemma nat_add_distrib:
    1.44 -     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
    1.45 +  "0 \<le> z \<Longrightarrow> 0 \<le> z' \<Longrightarrow> nat (z + z') = nat z + nat z'"
    1.46    by transfer clarsimp
    1.47  
    1.48 +lemma nat_diff_distrib':
    1.49 +  "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> nat (x - y) = nat x - nat y"
    1.50 +  by transfer clarsimp
    1.51 + 
    1.52  lemma nat_diff_distrib:
    1.53 -     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
    1.54 -  by transfer clarsimp
    1.55 +  "0 \<le> z' \<Longrightarrow> z' \<le> z \<Longrightarrow> nat (z - z') = nat z - nat z'"
    1.56 +  by (rule nat_diff_distrib') auto
    1.57  
    1.58  lemma nat_zminus_int [simp]: "nat (- int n) = 0"
    1.59    by transfer simp
    1.60 @@ -770,15 +795,6 @@
    1.61  text{*Simplify the term @{term "w + - z"}*}
    1.62  lemmas diff_int_def_symmetric = diff_def [where 'a=int, symmetric, simp]
    1.63  
    1.64 -lemma nat_0 [simp]: "nat 0 = 0"
    1.65 -by (simp add: nat_eq_iff)
    1.66 -
    1.67 -lemma nat_1 [simp]: "nat 1 = Suc 0"
    1.68 -by (subst nat_eq_iff, simp)
    1.69 -
    1.70 -lemma nat_2: "nat 2 = Suc (Suc 0)"
    1.71 -by (subst nat_eq_iff, simp)
    1.72 -
    1.73  lemma one_less_nat_eq [simp]: "(Suc 0 < nat z) = (1 < z)"
    1.74  apply (insert zless_nat_conj [of 1 z])
    1.75  apply auto
    1.76 @@ -860,21 +876,6 @@
    1.77                if d < 0 then 0 else nat d)"
    1.78  by (simp add: Let_def nat_diff_distrib [symmetric])
    1.79  
    1.80 -(* nat_diff_distrib has too-strong premises *)
    1.81 -lemma nat_diff_distrib': "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> nat (x - y) = nat x - nat y"
    1.82 -apply (rule int_int_eq [THEN iffD1], clarsimp)
    1.83 -apply (subst of_nat_diff)
    1.84 -apply (rule nat_mono, simp_all)
    1.85 -done
    1.86 -
    1.87 -lemma nat_numeral [simp]:
    1.88 -  "nat (numeral k) = numeral k"
    1.89 -  by (simp add: nat_eq_iff)
    1.90 -
    1.91 -lemma nat_neg_numeral [simp]:
    1.92 -  "nat (neg_numeral k) = 0"
    1.93 -  by simp
    1.94 -
    1.95  lemma diff_nat_numeral [simp]: 
    1.96    "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
    1.97    by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)