src/HOL/Archimedean_Field.thy
changeset 61070 b72a990adfe2
parent 60758 d8d85a8172b5
child 61378 3e04c9ca001a
     1.1 --- a/src/HOL/Archimedean_Field.thy	Mon Aug 31 21:01:21 2015 +0200
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Aug 31 21:28:08 2015 +0200
     1.3 @@ -546,14 +546,14 @@
     1.4  lemma frac_lt_1: "frac x < 1"
     1.5    by  (simp add: frac_def) linarith
     1.6  
     1.7 -lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> Ints"
     1.8 +lemma frac_eq_0_iff [simp]: "frac x = 0 \<longleftrightarrow> x \<in> \<int>"
     1.9    by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )
    1.10  
    1.11  lemma frac_ge_0 [simp]: "frac x \<ge> 0"
    1.12    unfolding frac_def
    1.13    by linarith
    1.14  
    1.15 -lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> Ints"
    1.16 +lemma frac_gt_0_iff [simp]: "frac x > 0 \<longleftrightarrow> x \<notin> \<int>"
    1.17    by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)
    1.18  
    1.19  lemma frac_of_int [simp]: "frac (of_int z) = 0"
    1.20 @@ -582,7 +582,7 @@
    1.21  
    1.22  lemma frac_unique_iff:
    1.23    fixes x :: "'a::floor_ceiling"
    1.24 -  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> Ints \<and> 0 \<le> a \<and> a < 1"
    1.25 +  shows  "(frac x) = a \<longleftrightarrow> x - a \<in> \<int> \<and> 0 \<le> a \<and> a < 1"
    1.26    apply (auto simp: Ints_def frac_def)
    1.27    apply linarith
    1.28    apply linarith
    1.29 @@ -593,7 +593,7 @@
    1.30    
    1.31  lemma frac_neg:
    1.32    fixes x :: "'a::floor_ceiling"
    1.33 -  shows  "frac (-x) = (if x \<in> Ints then 0 else 1 - frac x)"
    1.34 +  shows  "frac (-x) = (if x \<in> \<int> then 0 else 1 - frac x)"
    1.35    apply (auto simp add: frac_unique_iff)
    1.36    apply (simp add: frac_def)
    1.37    by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)