src/HOL/Int.thy
changeset 62348 9a5f43dac883
parent 62347 2230b7047376
child 62390 842917225d56
     1.1 --- a/src/HOL/Int.thy	Wed Feb 17 21:51:57 2016 +0100
     1.2 +++ b/src/HOL/Int.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -570,15 +570,19 @@
     1.4  lemma negative_eq_positive [simp]: "(- int n = of_nat m) = (n = 0 & m = 0)"
     1.5  by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)
     1.6  
     1.7 -lemma zle_iff_zadd: "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)"
     1.8 -proof -
     1.9 -  have "(w \<le> z) = (0 \<le> z - w)"
    1.10 -    by (simp only: le_diff_eq add_0_left)
    1.11 -  also have "\<dots> = (\<exists>n. z - w = of_nat n)"
    1.12 -    by (auto elim: zero_le_imp_eq_int)
    1.13 -  also have "\<dots> = (\<exists>n. z = w + of_nat n)"
    1.14 -    by (simp only: algebra_simps)
    1.15 -  finally show ?thesis .
    1.16 +lemma zle_iff_zadd:
    1.17 +  "w \<le> z \<longleftrightarrow> (\<exists>n. z = w + int n)" (is "?P \<longleftrightarrow> ?Q")
    1.18 +proof
    1.19 +  assume ?Q
    1.20 +  then show ?P by auto
    1.21 +next
    1.22 +  assume ?P
    1.23 +  then have "0 \<le> z - w" by simp
    1.24 +  then obtain n where "z - w = int n"
    1.25 +    using zero_le_imp_eq_int [of "z - w"] by blast
    1.26 +  then have "z = w + int n"
    1.27 +    by simp
    1.28 +  then show ?Q ..
    1.29  qed
    1.30  
    1.31  lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
    1.32 @@ -1725,34 +1729,9 @@
    1.33  hide_const (open) Pos Neg sub dup
    1.34  
    1.35  
    1.36 -subsection \<open>Legacy theorems\<close>
    1.37 -
    1.38 -lemmas inj_int = inj_of_nat [where 'a=int]
    1.39 -lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
    1.40 -lemmas int_mult = of_nat_mult [where 'a=int]
    1.41 -lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
    1.42 -lemmas zless_int = of_nat_less_iff [where 'a=int]
    1.43 -lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
    1.44 -lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
    1.45 -lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
    1.46 -lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
    1.47 -lemmas int_0 = of_nat_0 [where 'a=int]
    1.48 -lemmas int_1 = of_nat_1 [where 'a=int]
    1.49 -lemmas int_Suc = of_nat_Suc [where 'a=int]
    1.50 -lemmas int_numeral = of_nat_numeral [where 'a=int]
    1.51 -lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
    1.52 -lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
    1.53 -lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
    1.54 -lemmas zpower_numeral_even = power_numeral_even [where 'a=int]
    1.55 -lemmas zpower_numeral_odd = power_numeral_odd [where 'a=int]
    1.56 -
    1.57  text \<open>De-register \<open>int\<close> as a quotient type:\<close>
    1.58  
    1.59  lifting_update int.lifting
    1.60  lifting_forget int.lifting
    1.61  
    1.62 -text\<open>Also the class for fields with characteristic zero.\<close>
    1.63 -class field_char_0 = field + ring_char_0
    1.64 -subclass (in linordered_field) field_char_0 ..
    1.65 -
    1.66  end