52 |
54 |
53 lemma real_mult_div_cancel_disj: |
55 lemma real_mult_div_cancel_disj: |
54 "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)" |
56 "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)" |
55 by (rule Ring_and_Field.mult_divide_cancel_eq_if) |
57 by (rule Ring_and_Field.mult_divide_cancel_eq_if) |
56 |
58 |
57 |
59 subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*} |
|
60 |
|
61 lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" |
|
62 by arith |
|
63 |
|
64 lemma real_add_eq_0_iff [iff]: "(x+y = (0::real)) = (y = -x)" |
|
65 by auto |
|
66 |
|
67 lemma real_add_less_0_iff [iff]: "(x+y < (0::real)) = (y < -x)" |
|
68 by auto |
|
69 |
|
70 lemma real_0_less_add_iff [iff]: "((0::real) < x+y) = (-x < y)" |
|
71 by auto |
|
72 |
|
73 lemma real_add_le_0_iff [iff]: "(x+y \<le> (0::real)) = (y \<le> -x)" |
|
74 by auto |
|
75 |
|
76 lemma real_0_le_add_iff [iff]: "((0::real) \<le> x+y) = (-x \<le> y)" |
|
77 by auto |
|
78 |
|
79 |
|
80 (** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc., |
|
81 in RealBin |
|
82 **) |
|
83 |
|
84 lemma real_0_less_diff_iff [iff]: "((0::real) < x-y) = (y < x)" |
|
85 by auto |
|
86 |
|
87 lemma real_0_le_diff_iff [iff]: "((0::real) \<le> x-y) = (y \<le> x)" |
|
88 by auto |
|
89 |
|
90 (* |
|
91 FIXME: we should have this, as for type int, but many proofs would break. |
|
92 It replaces x+-y by x-y. |
|
93 Addsimps [symmetric real_diff_def] |
|
94 *) |
|
95 |
|
96 |
|
97 (*FIXME: move most of these to Ring_and_Field*) |
|
98 |
|
99 subsection{*Simplification of Inequalities Involving Literal Divisors*} |
|
100 |
|
101 lemma pos_real_le_divide_eq: "0<z ==> ((x::real) \<le> y/z) = (x*z \<le> y)" |
|
102 apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ") |
|
103 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
104 apply (erule ssubst) |
|
105 apply (subst real_mult_le_cancel2, simp) |
|
106 done |
|
107 |
|
108 lemma neg_real_le_divide_eq: "z<0 ==> ((x::real) \<le> y/z) = (y \<le> x*z)" |
|
109 apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ") |
|
110 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
111 apply (erule ssubst) |
|
112 apply (subst real_mult_le_cancel2, simp) |
|
113 done |
|
114 |
|
115 lemma real_le_divide_eq: |
|
116 "((x::real) \<le> y/z) = (if 0<z then x*z \<le> y |
|
117 else if z<0 then y \<le> x*z |
|
118 else x\<le>0)" |
|
119 apply (case_tac "z=0", simp) |
|
120 apply (simp add: pos_real_le_divide_eq neg_real_le_divide_eq) |
|
121 done |
|
122 |
|
123 declare real_le_divide_eq [of _ _ "number_of w", standard, simp] |
|
124 |
|
125 lemma pos_real_divide_le_eq: "0<z ==> (y/z \<le> (x::real)) = (y \<le> x*z)" |
|
126 apply (subgoal_tac " (y \<le> x*z) = ((y/z) *z \<le> x*z) ") |
|
127 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
128 apply (erule ssubst) |
|
129 apply (subst real_mult_le_cancel2, simp) |
|
130 done |
|
131 |
|
132 lemma neg_real_divide_le_eq: "z<0 ==> (y/z \<le> (x::real)) = (x*z \<le> y)" |
|
133 apply (subgoal_tac " (x*z \<le> y) = (x*z \<le> (y/z) *z) ") |
|
134 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
135 apply (erule ssubst) |
|
136 apply (subst real_mult_le_cancel2, simp) |
|
137 done |
|
138 |
|
139 |
|
140 lemma real_divide_le_eq: |
|
141 "(y/z \<le> (x::real)) = (if 0<z then y \<le> x*z |
|
142 else if z<0 then x*z \<le> y |
|
143 else 0 \<le> x)" |
|
144 apply (case_tac "z=0", simp) |
|
145 apply (simp add: pos_real_divide_le_eq neg_real_divide_le_eq) |
|
146 done |
|
147 |
|
148 declare real_divide_le_eq [of _ "number_of w", standard, simp] |
|
149 |
|
150 |
|
151 lemma pos_real_less_divide_eq: "0<z ==> ((x::real) < y/z) = (x*z < y)" |
|
152 apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ") |
|
153 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
154 apply (erule ssubst) |
|
155 apply (subst real_mult_less_cancel2, simp) |
|
156 done |
|
157 |
|
158 lemma neg_real_less_divide_eq: "z<0 ==> ((x::real) < y/z) = (y < x*z)" |
|
159 apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ") |
|
160 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
161 apply (erule ssubst) |
|
162 apply (subst real_mult_less_cancel2, simp) |
|
163 done |
|
164 |
|
165 lemma real_less_divide_eq: |
|
166 "((x::real) < y/z) = (if 0<z then x*z < y |
|
167 else if z<0 then y < x*z |
|
168 else x<0)" |
|
169 apply (case_tac "z=0", simp) |
|
170 apply (simp add: pos_real_less_divide_eq neg_real_less_divide_eq) |
|
171 done |
|
172 |
|
173 declare real_less_divide_eq [of _ _ "number_of w", standard, simp] |
|
174 |
|
175 lemma pos_real_divide_less_eq: "0<z ==> (y/z < (x::real)) = (y < x*z)" |
|
176 apply (subgoal_tac " (y < x*z) = ((y/z) *z < x*z) ") |
|
177 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
178 apply (erule ssubst) |
|
179 apply (subst real_mult_less_cancel2, simp) |
|
180 done |
|
181 |
|
182 lemma neg_real_divide_less_eq: "z<0 ==> (y/z < (x::real)) = (x*z < y)" |
|
183 apply (subgoal_tac " (x*z < y) = (x*z < (y/z) *z) ") |
|
184 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
185 apply (erule ssubst) |
|
186 apply (subst real_mult_less_cancel2, simp) |
|
187 done |
|
188 |
|
189 lemma real_divide_less_eq: |
|
190 "(y/z < (x::real)) = (if 0<z then y < x*z |
|
191 else if z<0 then x*z < y |
|
192 else 0 < x)" |
|
193 apply (case_tac "z=0", simp) |
|
194 apply (simp add: pos_real_divide_less_eq neg_real_divide_less_eq) |
|
195 done |
|
196 |
|
197 declare real_divide_less_eq [of _ "number_of w", standard, simp] |
|
198 |
|
199 lemma nonzero_real_eq_divide_eq: "z\<noteq>0 ==> ((x::real) = y/z) = (x*z = y)" |
|
200 apply (subgoal_tac " (x*z = y) = (x*z = (y/z) *z) ") |
|
201 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
202 apply (erule ssubst) |
|
203 apply (subst real_mult_eq_cancel2, simp) |
|
204 done |
|
205 |
|
206 lemma real_eq_divide_eq: |
|
207 "((x::real) = y/z) = (if z\<noteq>0 then x*z = y else x=0)" |
|
208 by (simp add: nonzero_real_eq_divide_eq) |
|
209 |
|
210 declare real_eq_divide_eq [of _ _ "number_of w", standard, simp] |
|
211 |
|
212 lemma nonzero_real_divide_eq_eq: "z\<noteq>0 ==> (y/z = (x::real)) = (y = x*z)" |
|
213 apply (subgoal_tac " (y = x*z) = ((y/z) *z = x*z) ") |
|
214 prefer 2 apply (simp add: real_divide_def real_mult_assoc) |
|
215 apply (erule ssubst) |
|
216 apply (subst real_mult_eq_cancel2, simp) |
|
217 done |
|
218 |
|
219 lemma real_divide_eq_eq: |
|
220 "(y/z = (x::real)) = (if z\<noteq>0 then y = x*z else x=0)" |
|
221 by (simp add: nonzero_real_divide_eq_eq) |
|
222 |
|
223 declare real_divide_eq_eq [of _ "number_of w", standard, simp] |
|
224 |
|
225 lemma real_divide_eq_cancel2: "(m/k = n/k) = (k = 0 | m = (n::real))" |
|
226 apply (case_tac "k=0", simp) |
|
227 apply (simp add:divide_inverse) |
|
228 done |
|
229 |
|
230 lemma real_divide_eq_cancel1: "(k/m = k/n) = (k = 0 | m = (n::real))" |
|
231 by (force simp add: real_divide_eq_eq real_eq_divide_eq) |
|
232 |
|
233 lemma real_inverse_less_iff: |
|
234 "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)" |
|
235 by (rule Ring_and_Field.inverse_less_iff_less) |
|
236 |
|
237 lemma real_inverse_le_iff: |
|
238 "[| 0 < r; 0 < x|] ==> (inverse x \<le> inverse r) = (r \<le> (x::real))" |
|
239 by (rule Ring_and_Field.inverse_le_iff_le) |
|
240 |
|
241 |
|
242 (** Division by 1, -1 **) |
|
243 |
|
244 lemma real_divide_1: "(x::real)/1 = x" |
|
245 by (simp add: real_divide_def) |
|
246 |
|
247 lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)" |
|
248 by simp |
|
249 |
|
250 lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)" |
|
251 by (simp add: real_divide_def real_minus_inverse) |
|
252 |
|
253 lemma real_lbound_gt_zero: |
|
254 "[| (0::real) < d1; 0 < d2 |] ==> \<exists>e. 0 < e & e < d1 & e < d2" |
|
255 apply (rule_tac x = " (min d1 d2) /2" in exI) |
|
256 apply (simp add: min_def) |
|
257 done |
|
258 |
|
259 (*** Density of the Reals ***) |
|
260 |
|
261 lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)" |
|
262 by auto |
|
263 |
|
264 lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y" |
|
265 by auto |
|
266 |
|
267 lemma real_dense: "x < y ==> \<exists>r::real. x < r & r < y" |
|
268 by (blast intro!: real_less_half_sum real_gt_half_sum) |
58 |
269 |
59 end |
270 end |