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.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.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
```