src/HOL/Int.thy
changeset 60570 7ed2cde6806d
parent 60162 645058aa9d6f
child 60758 d8d85a8172b5
     1.1 --- a/src/HOL/Int.thy	Thu Jun 25 15:01:41 2015 +0200
     1.2 +++ b/src/HOL/Int.thy	Thu Jun 25 15:01:42 2015 +0200
     1.3 @@ -859,6 +859,23 @@
     1.4                        nat_mult_distrib_neg [symmetric] mult_less_0_iff)
     1.5  done
     1.6  
     1.7 +lemma int_in_range_abs [simp]:
     1.8 +  "int n \<in> range abs"
     1.9 +proof (rule range_eqI)
    1.10 +  show "int n = \<bar>int n\<bar>"
    1.11 +    by simp
    1.12 +qed
    1.13 +
    1.14 +lemma range_abs_Nats [simp]:
    1.15 +  "range abs = (\<nat> :: int set)"
    1.16 +proof -
    1.17 +  have "\<bar>k\<bar> \<in> \<nat>" for k :: int
    1.18 +    by (cases k) simp_all
    1.19 +  moreover have "k \<in> range abs" if "k \<in> \<nat>" for k :: int
    1.20 +    using that by induct simp
    1.21 +  ultimately show ?thesis by blast
    1.22 +qed  
    1.23 +
    1.24  lemma Suc_nat_eq_nat_zadd1: "(0::int) <= z ==> Suc (nat z) = nat (1 + z)"
    1.25  apply (rule sym)
    1.26  apply (simp add: nat_eq_iff)