src/HOL/Archimedean_Field.thy
changeset 54489 03ff4d1e6784
parent 54281 b01057e72233
child 58040 9a867afaab5a
     1.1 --- a/src/HOL/Archimedean_Field.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -204,8 +204,8 @@
     1.4  lemma floor_numeral [simp]: "floor (numeral v) = numeral v"
     1.5    using floor_of_int [of "numeral v"] by simp
     1.6  
     1.7 -lemma floor_neg_numeral [simp]: "floor (neg_numeral v) = neg_numeral v"
     1.8 -  using floor_of_int [of "neg_numeral v"] by simp
     1.9 +lemma floor_neg_numeral [simp]: "floor (- numeral v) = - numeral v"
    1.10 +  using floor_of_int [of "- numeral v"] by simp
    1.11  
    1.12  lemma zero_le_floor [simp]: "0 \<le> floor x \<longleftrightarrow> 0 \<le> x"
    1.13    by (simp add: le_floor_iff)
    1.14 @@ -218,7 +218,7 @@
    1.15    by (simp add: le_floor_iff)
    1.16  
    1.17  lemma neg_numeral_le_floor [simp]:
    1.18 -  "neg_numeral v \<le> floor x \<longleftrightarrow> neg_numeral v \<le> x"
    1.19 +  "- numeral v \<le> floor x \<longleftrightarrow> - numeral v \<le> x"
    1.20    by (simp add: le_floor_iff)
    1.21  
    1.22  lemma zero_less_floor [simp]: "0 < floor x \<longleftrightarrow> 1 \<le> x"
    1.23 @@ -232,7 +232,7 @@
    1.24    by (simp add: less_floor_iff)
    1.25  
    1.26  lemma neg_numeral_less_floor [simp]:
    1.27 -  "neg_numeral v < floor x \<longleftrightarrow> neg_numeral v + 1 \<le> x"
    1.28 +  "- numeral v < floor x \<longleftrightarrow> - numeral v + 1 \<le> x"
    1.29    by (simp add: less_floor_iff)
    1.30  
    1.31  lemma floor_le_zero [simp]: "floor x \<le> 0 \<longleftrightarrow> x < 1"
    1.32 @@ -246,7 +246,7 @@
    1.33    by (simp add: floor_le_iff)
    1.34  
    1.35  lemma floor_le_neg_numeral [simp]:
    1.36 -  "floor x \<le> neg_numeral v \<longleftrightarrow> x < neg_numeral v + 1"
    1.37 +  "floor x \<le> - numeral v \<longleftrightarrow> x < - numeral v + 1"
    1.38    by (simp add: floor_le_iff)
    1.39  
    1.40  lemma floor_less_zero [simp]: "floor x < 0 \<longleftrightarrow> x < 0"
    1.41 @@ -260,7 +260,7 @@
    1.42    by (simp add: floor_less_iff)
    1.43  
    1.44  lemma floor_less_neg_numeral [simp]:
    1.45 -  "floor x < neg_numeral v \<longleftrightarrow> x < neg_numeral v"
    1.46 +  "floor x < - numeral v \<longleftrightarrow> x < - numeral v"
    1.47    by (simp add: floor_less_iff)
    1.48  
    1.49  text {* Addition and subtraction of integers *}
    1.50 @@ -272,10 +272,6 @@
    1.51      "floor (x + numeral v) = floor x + numeral v"
    1.52    using floor_add_of_int [of x "numeral v"] by simp
    1.53  
    1.54 -lemma floor_add_neg_numeral [simp]:
    1.55 -    "floor (x + neg_numeral v) = floor x + neg_numeral v"
    1.56 -  using floor_add_of_int [of x "neg_numeral v"] by simp
    1.57 -
    1.58  lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1"
    1.59    using floor_add_of_int [of x 1] by simp
    1.60  
    1.61 @@ -286,10 +282,6 @@
    1.62    "floor (x - numeral v) = floor x - numeral v"
    1.63    using floor_diff_of_int [of x "numeral v"] by simp
    1.64  
    1.65 -lemma floor_diff_neg_numeral [simp]:
    1.66 -  "floor (x - neg_numeral v) = floor x - neg_numeral v"
    1.67 -  using floor_diff_of_int [of x "neg_numeral v"] by simp
    1.68 -
    1.69  lemma floor_diff_one [simp]: "floor (x - 1) = floor x - 1"
    1.70    using floor_diff_of_int [of x 1] by simp
    1.71  
    1.72 @@ -353,8 +345,8 @@
    1.73  lemma ceiling_numeral [simp]: "ceiling (numeral v) = numeral v"
    1.74    using ceiling_of_int [of "numeral v"] by simp
    1.75  
    1.76 -lemma ceiling_neg_numeral [simp]: "ceiling (neg_numeral v) = neg_numeral v"
    1.77 -  using ceiling_of_int [of "neg_numeral v"] by simp
    1.78 +lemma ceiling_neg_numeral [simp]: "ceiling (- numeral v) = - numeral v"
    1.79 +  using ceiling_of_int [of "- numeral v"] by simp
    1.80  
    1.81  lemma ceiling_le_zero [simp]: "ceiling x \<le> 0 \<longleftrightarrow> x \<le> 0"
    1.82    by (simp add: ceiling_le_iff)
    1.83 @@ -367,7 +359,7 @@
    1.84    by (simp add: ceiling_le_iff)
    1.85  
    1.86  lemma ceiling_le_neg_numeral [simp]:
    1.87 -  "ceiling x \<le> neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v"
    1.88 +  "ceiling x \<le> - numeral v \<longleftrightarrow> x \<le> - numeral v"
    1.89    by (simp add: ceiling_le_iff)
    1.90  
    1.91  lemma ceiling_less_zero [simp]: "ceiling x < 0 \<longleftrightarrow> x \<le> -1"
    1.92 @@ -381,7 +373,7 @@
    1.93    by (simp add: ceiling_less_iff)
    1.94  
    1.95  lemma ceiling_less_neg_numeral [simp]:
    1.96 -  "ceiling x < neg_numeral v \<longleftrightarrow> x \<le> neg_numeral v - 1"
    1.97 +  "ceiling x < - numeral v \<longleftrightarrow> x \<le> - numeral v - 1"
    1.98    by (simp add: ceiling_less_iff)
    1.99  
   1.100  lemma zero_le_ceiling [simp]: "0 \<le> ceiling x \<longleftrightarrow> -1 < x"
   1.101 @@ -395,7 +387,7 @@
   1.102    by (simp add: le_ceiling_iff)
   1.103  
   1.104  lemma neg_numeral_le_ceiling [simp]:
   1.105 -  "neg_numeral v \<le> ceiling x \<longleftrightarrow> neg_numeral v - 1 < x"
   1.106 +  "- numeral v \<le> ceiling x \<longleftrightarrow> - numeral v - 1 < x"
   1.107    by (simp add: le_ceiling_iff)
   1.108  
   1.109  lemma zero_less_ceiling [simp]: "0 < ceiling x \<longleftrightarrow> 0 < x"
   1.110 @@ -409,7 +401,7 @@
   1.111    by (simp add: less_ceiling_iff)
   1.112  
   1.113  lemma neg_numeral_less_ceiling [simp]:
   1.114 -  "neg_numeral v < ceiling x \<longleftrightarrow> neg_numeral v < x"
   1.115 +  "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
   1.116    by (simp add: less_ceiling_iff)
   1.117  
   1.118  text {* Addition and subtraction of integers *}
   1.119 @@ -421,10 +413,6 @@
   1.120      "ceiling (x + numeral v) = ceiling x + numeral v"
   1.121    using ceiling_add_of_int [of x "numeral v"] by simp
   1.122  
   1.123 -lemma ceiling_add_neg_numeral [simp]:
   1.124 -    "ceiling (x + neg_numeral v) = ceiling x + neg_numeral v"
   1.125 -  using ceiling_add_of_int [of x "neg_numeral v"] by simp
   1.126 -
   1.127  lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1"
   1.128    using ceiling_add_of_int [of x 1] by simp
   1.129  
   1.130 @@ -435,10 +423,6 @@
   1.131    "ceiling (x - numeral v) = ceiling x - numeral v"
   1.132    using ceiling_diff_of_int [of x "numeral v"] by simp
   1.133  
   1.134 -lemma ceiling_diff_neg_numeral [simp]:
   1.135 -  "ceiling (x - neg_numeral v) = ceiling x - neg_numeral v"
   1.136 -  using ceiling_diff_of_int [of x "neg_numeral v"] by simp
   1.137 -
   1.138  lemma ceiling_diff_one [simp]: "ceiling (x - 1) = ceiling x - 1"
   1.139    using ceiling_diff_of_int [of x 1] by simp
   1.140