src/HOL/Archimedean_Field.thy
changeset 47108 2a1953f0d20d
parent 43733 a6ca7b83612f
child 47307 5e5ca36692b3
     1.1 --- a/src/HOL/Archimedean_Field.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  text {* Archimedean fields have no infinite elements. *}
     1.6  
     1.7 -class archimedean_field = linordered_field + number_ring +
     1.8 +class archimedean_field = linordered_field +
     1.9    assumes ex_le_of_int: "\<exists>z. x \<le> of_int z"
    1.10  
    1.11  lemma ex_less_of_int:
    1.12 @@ -202,8 +202,11 @@
    1.13  lemma floor_one [simp]: "floor 1 = 1"
    1.14    using floor_of_int [of 1] by simp
    1.15  
    1.16 -lemma floor_number_of [simp]: "floor (number_of v) = number_of v"
    1.17 -  using floor_of_int [of "number_of v"] by simp
    1.18 +lemma floor_numeral [simp]: "floor (numeral v) = numeral v"
    1.19 +  using floor_of_int [of "numeral v"] by simp
    1.20 +
    1.21 +lemma floor_neg_numeral [simp]: "floor (neg_numeral v) = neg_numeral v"
    1.22 +  using floor_of_int [of "neg_numeral v"] by simp
    1.23  
    1.24  lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
    1.25    by (simp add: le_floor_iff)
    1.26 @@ -211,7 +214,12 @@
    1.27  lemma one_le_floor [simp]: "1 \<le> floor x \<longleftrightarrow> 1 \<le> x"
    1.28    by (simp add: le_floor_iff)
    1.29  
    1.30 -lemma number_of_le_floor [simp]: "number_of v \<le> floor x \<longleftrightarrow> number_of v \<le> x"
    1.31 +lemma numeral_le_floor [simp]:
    1.32 +  "numeral v \<le> floor x \<longleftrightarrow> numeral v \<le> x"
    1.33 +  by (simp add: le_floor_iff)
    1.34 +
    1.35 +lemma neg_numeral_le_floor [simp]:
    1.36 +  "neg_numeral v \<le> floor x \<longleftrightarrow> neg_numeral v \<le> x"
    1.37    by (simp add: le_floor_iff)
    1.38  
    1.39  lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
    1.40 @@ -220,8 +228,12 @@
    1.41  lemma one_less_floor [simp]: "1 < floor x \<longleftrightarrow> 2 \<le> x"
    1.42    by (simp add: less_floor_iff)
    1.43  
    1.44 -lemma number_of_less_floor [simp]:
    1.45 -  "number_of v < floor x \<longleftrightarrow> number_of v + 1 \<le> x"
    1.46 +lemma numeral_less_floor [simp]:
    1.47 +  "numeral v < floor x \<longleftrightarrow> numeral v + 1 \<le> x"
    1.48 +  by (simp add: less_floor_iff)
    1.49 +
    1.50 +lemma neg_numeral_less_floor [simp]:
    1.51 +  "neg_numeral v < floor x \<longleftrightarrow> neg_numeral v + 1 \<le> x"
    1.52    by (simp add: less_floor_iff)
    1.53  
    1.54  lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
    1.55 @@ -230,8 +242,12 @@
    1.56  lemma floor_le_one [simp]: "floor x \<le> 1 \<longleftrightarrow> x < 2"
    1.57    by (simp add: floor_le_iff)
    1.58  
    1.59 -lemma floor_le_number_of [simp]:
    1.60 -  "floor x \<le> number_of v \<longleftrightarrow> x < number_of v + 1"
    1.61 +lemma floor_le_numeral [simp]:
    1.62 +  "floor x \<le> numeral v \<longleftrightarrow> x < numeral v + 1"
    1.63 +  by (simp add: floor_le_iff)
    1.64 +
    1.65 +lemma floor_le_neg_numeral [simp]:
    1.66 +  "floor x \<le> neg_numeral v \<longleftrightarrow> x < neg_numeral v + 1"
    1.67    by (simp add: floor_le_iff)
    1.68  
    1.69  lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
    1.70 @@ -240,8 +256,12 @@
    1.71  lemma floor_less_one [simp]: "floor x < 1 \<longleftrightarrow> x < 1"
    1.72    by (simp add: floor_less_iff)
    1.73  
    1.74 -lemma floor_less_number_of [simp]:
    1.75 -  "floor x < number_of v \<longleftrightarrow> x < number_of v"
    1.76 +lemma floor_less_numeral [simp]:
    1.77 +  "floor x < numeral v \<longleftrightarrow> x < numeral v"
    1.78 +  by (simp add: floor_less_iff)
    1.79 +
    1.80 +lemma floor_less_neg_numeral [simp]:
    1.81 +  "floor x < neg_numeral v \<longleftrightarrow> x < neg_numeral v"
    1.82    by (simp add: floor_less_iff)
    1.83  
    1.84  text {* Addition and subtraction of integers *}
    1.85 @@ -249,9 +269,13 @@
    1.86  lemma floor_add_of_int [simp]: "floor (x + of_int z) = floor x + z"
    1.87    using floor_correct [of x] by (simp add: floor_unique)
    1.88  
    1.89 -lemma floor_add_number_of [simp]:
    1.90 -    "floor (x + number_of v) = floor x + number_of v"
    1.91 -  using floor_add_of_int [of x "number_of v"] by simp
    1.92 +lemma floor_add_numeral [simp]:
    1.93 +    "floor (x + numeral v) = floor x + numeral v"
    1.94 +  using floor_add_of_int [of x "numeral v"] by simp
    1.95 +
    1.96 +lemma floor_add_neg_numeral [simp]:
    1.97 +    "floor (x + neg_numeral v) = floor x + neg_numeral v"
    1.98 +  using floor_add_of_int [of x "neg_numeral v"] by simp
    1.99  
   1.100  lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
   1.101    using floor_add_of_int [of x 1] by simp
   1.102 @@ -259,9 +283,13 @@
   1.103  lemma floor_diff_of_int [simp]: "floor (x - of_int z) = floor x - z"
   1.104    using floor_add_of_int [of x "- z"] by (simp add: algebra_simps)
   1.105  
   1.106 -lemma floor_diff_number_of [simp]:
   1.107 -  "floor (x - number_of v) = floor x - number_of v"
   1.108 -  using floor_diff_of_int [of x "number_of v"] by simp
   1.109 +lemma floor_diff_numeral [simp]:
   1.110 +  "floor (x - numeral v) = floor x - numeral v"
   1.111 +  using floor_diff_of_int [of x "numeral v"] by simp
   1.112 +
   1.113 +lemma floor_diff_neg_numeral [simp]:
   1.114 +  "floor (x - neg_numeral v) = floor x - neg_numeral v"
   1.115 +  using floor_diff_of_int [of x "neg_numeral v"] by simp
   1.116  
   1.117  lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
   1.118    using floor_diff_of_int [of x 1] by simp
   1.119 @@ -320,8 +348,11 @@
   1.120  lemma ceiling_one [simp]: "ceiling 1 = 1"
   1.121    using ceiling_of_int [of 1] by simp
   1.122  
   1.123 -lemma ceiling_number_of [simp]: "ceiling (number_of v) = number_of v"
   1.124 -  using ceiling_of_int [of "number_of v"] by simp
   1.125 +lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v"
   1.126 +  using ceiling_of_int [of "numeral v"] by simp
   1.127 +
   1.128 +lemma ceiling_neg_numeral [simp]: "ceiling (neg_numeral v) = neg_numeral v"
   1.129 +  using ceiling_of_int [of "neg_numeral v"] by simp
   1.130  
   1.131  lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
   1.132    by (simp add: ceiling_le_iff)
   1.133 @@ -329,8 +360,12 @@
   1.134  lemma ceiling_le_one [simp]: "ceiling x \<le> 1 \<longleftrightarrow> x \<le> 1"
   1.135    by (simp add: ceiling_le_iff)
   1.136  
   1.137 -lemma ceiling_le_number_of [simp]:
   1.138 -  "ceiling x \<le> number_of v \<longleftrightarrow> x \<le> number_of v"
   1.139 +lemma ceiling_le_numeral [simp]:
   1.140 +  "ceiling x \<le> numeral v \<longleftrightarrow> x \<le> numeral v"
   1.141 +  by (simp add: ceiling_le_iff)
   1.142 +
   1.143 +lemma ceiling_le_neg_numeral [simp]:
   1.144 +  "ceiling x \<le> neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v"
   1.145    by (simp add: ceiling_le_iff)
   1.146  
   1.147  lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
   1.148 @@ -339,8 +374,12 @@
   1.149  lemma ceiling_less_one [simp]: "ceiling x < 1 \<longleftrightarrow> x \<le> 0"
   1.150    by (simp add: ceiling_less_iff)
   1.151  
   1.152 -lemma ceiling_less_number_of [simp]:
   1.153 -  "ceiling x < number_of v \<longleftrightarrow> x \<le> number_of v - 1"
   1.154 +lemma ceiling_less_numeral [simp]:
   1.155 +  "ceiling x < numeral v \<longleftrightarrow> x \<le> numeral v - 1"
   1.156 +  by (simp add: ceiling_less_iff)
   1.157 +
   1.158 +lemma ceiling_less_neg_numeral [simp]:
   1.159 +  "ceiling x < neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v - 1"
   1.160    by (simp add: ceiling_less_iff)
   1.161  
   1.162  lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
   1.163 @@ -349,8 +388,12 @@
   1.164  lemma one_le_ceiling [simp]: "1 \<le> ceiling x \<longleftrightarrow> 0 < x"
   1.165    by (simp add: le_ceiling_iff)
   1.166  
   1.167 -lemma number_of_le_ceiling [simp]:
   1.168 -  "number_of v \<le> ceiling x\<longleftrightarrow> number_of v - 1 < x"
   1.169 +lemma numeral_le_ceiling [simp]:
   1.170 +  "numeral v \<le> ceiling x \<longleftrightarrow> numeral v - 1 < x"
   1.171 +  by (simp add: le_ceiling_iff)
   1.172 +
   1.173 +lemma neg_numeral_le_ceiling [simp]:
   1.174 +  "neg_numeral v \<le> ceiling x \<longleftrightarrow> neg_numeral v - 1 < x"
   1.175    by (simp add: le_ceiling_iff)
   1.176  
   1.177  lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
   1.178 @@ -359,8 +402,12 @@
   1.179  lemma one_less_ceiling [simp]: "1 < ceiling x \<longleftrightarrow> 1 < x"
   1.180    by (simp add: less_ceiling_iff)
   1.181  
   1.182 -lemma number_of_less_ceiling [simp]:
   1.183 -  "number_of v < ceiling x \<longleftrightarrow> number_of v < x"
   1.184 +lemma numeral_less_ceiling [simp]:
   1.185 +  "numeral v < ceiling x \<longleftrightarrow> numeral v < x"
   1.186 +  by (simp add: less_ceiling_iff)
   1.187 +
   1.188 +lemma neg_numeral_less_ceiling [simp]:
   1.189 +  "neg_numeral v < ceiling x \<longleftrightarrow> neg_numeral v < x"
   1.190    by (simp add: less_ceiling_iff)
   1.191  
   1.192  text {* Addition and subtraction of integers *}
   1.193 @@ -368,9 +415,13 @@
   1.194  lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
   1.195    using ceiling_correct [of x] by (simp add: ceiling_unique)
   1.196  
   1.197 -lemma ceiling_add_number_of [simp]:
   1.198 -    "ceiling (x + number_of v) = ceiling x + number_of v"
   1.199 -  using ceiling_add_of_int [of x "number_of v"] by simp
   1.200 +lemma ceiling_add_numeral [simp]:
   1.201 +    "ceiling (x + numeral v) = ceiling x + numeral v"
   1.202 +  using ceiling_add_of_int [of x "numeral v"] by simp
   1.203 +
   1.204 +lemma ceiling_add_neg_numeral [simp]:
   1.205 +    "ceiling (x + neg_numeral v) = ceiling x + neg_numeral v"
   1.206 +  using ceiling_add_of_int [of x "neg_numeral v"] by simp
   1.207  
   1.208  lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
   1.209    using ceiling_add_of_int [of x 1] by simp
   1.210 @@ -378,9 +429,13 @@
   1.211  lemma ceiling_diff_of_int [simp]: "ceiling (x - of_int z) = ceiling x - z"
   1.212    using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps)
   1.213  
   1.214 -lemma ceiling_diff_number_of [simp]:
   1.215 -  "ceiling (x - number_of v) = ceiling x - number_of v"
   1.216 -  using ceiling_diff_of_int [of x "number_of v"] by simp
   1.217 +lemma ceiling_diff_numeral [simp]:
   1.218 +  "ceiling (x - numeral v) = ceiling x - numeral v"
   1.219 +  using ceiling_diff_of_int [of x "numeral v"] by simp
   1.220 +
   1.221 +lemma ceiling_diff_neg_numeral [simp]:
   1.222 +  "ceiling (x - neg_numeral v) = ceiling x - neg_numeral v"
   1.223 +  using ceiling_diff_of_int [of x "neg_numeral v"] by simp
   1.224  
   1.225  lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   1.226    using ceiling_diff_of_int [of x 1] by simp