author | paulson |
Fri, 19 Dec 2003 10:38:39 +0100 | |
changeset 14303 | 995212a00a50 |
parent 13485 | acf39e924091 |
child 14305 | f17ca9f6dc8c |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title: HOL/Hyperreal/HyperRealArith0.ML |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1999 University of Cambridge |
|
5 |
||
6 |
Assorted facts that need binary literals and the arithmetic decision procedure |
|
7 |
||
8 |
Also, common factor cancellation |
|
9 |
*) |
|
10 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
11 |
Goal "x - - y = x + (y::hypreal)"; |
13462 | 12 |
by (Simp_tac 1); |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
13 |
qed "hypreal_diff_minus_eq"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
14 |
Addsimps [hypreal_diff_minus_eq]; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
15 |
|
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
16 |
Goal "((x * y = 0) = (x = 0 | y = (0::hypreal)))"; |
13462 | 17 |
by Auto_tac; |
10751 | 18 |
qed "hypreal_mult_is_0"; |
19 |
AddIffs [hypreal_mult_is_0]; |
|
20 |
||
21 |
(** Division and inverse **) |
|
22 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
23 |
Goal "0/x = (0::hypreal)"; |
13462 | 24 |
by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); |
10751 | 25 |
qed "hypreal_0_divide"; |
26 |
Addsimps [hypreal_0_divide]; |
|
27 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
28 |
Goal "((0::hypreal) < inverse x) = (0 < x)"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
29 |
by (case_tac "x=0" 1); |
13462 | 30 |
by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1); |
31 |
by (auto_tac (claset() addDs [hypreal_inverse_less_0], |
|
32 |
simpset() addsimps [linorder_neq_iff, |
|
33 |
hypreal_inverse_gt_0])); |
|
10751 | 34 |
qed "hypreal_0_less_inverse_iff"; |
35 |
Addsimps [hypreal_0_less_inverse_iff]; |
|
36 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
37 |
Goal "(inverse x < (0::hypreal)) = (x < 0)"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
38 |
by (case_tac "x=0" 1); |
13462 | 39 |
by (asm_simp_tac (HOL_ss addsimps [HYPREAL_INVERSE_ZERO]) 1); |
40 |
by (auto_tac (claset() addDs [hypreal_inverse_less_0], |
|
41 |
simpset() addsimps [linorder_neq_iff, |
|
42 |
hypreal_inverse_gt_0])); |
|
10751 | 43 |
qed "hypreal_inverse_less_0_iff"; |
44 |
Addsimps [hypreal_inverse_less_0_iff]; |
|
45 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
46 |
Goal "((0::hypreal) <= inverse x) = (0 <= x)"; |
13462 | 47 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
10751 | 48 |
qed "hypreal_0_le_inverse_iff"; |
49 |
Addsimps [hypreal_0_le_inverse_iff]; |
|
50 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
51 |
Goal "(inverse x <= (0::hypreal)) = (x <= 0)"; |
13462 | 52 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
10751 | 53 |
qed "hypreal_inverse_le_0_iff"; |
54 |
Addsimps [hypreal_inverse_le_0_iff]; |
|
55 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
56 |
Goalw [hypreal_divide_def] "x/(0::hypreal) = 0"; |
13462 | 57 |
by (stac (HYPREAL_INVERSE_ZERO) 1); |
58 |
by (Simp_tac 1); |
|
10751 | 59 |
qed "HYPREAL_DIVIDE_ZERO"; |
60 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
61 |
Goal "inverse (x::hypreal) = 1/x"; |
13462 | 62 |
by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); |
10751 | 63 |
qed "hypreal_inverse_eq_divide"; |
64 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
65 |
Goal "((0::hypreal) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)"; |
10751 | 66 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_less_mult_iff]) 1); |
67 |
qed "hypreal_0_less_divide_iff"; |
|
68 |
Addsimps [inst "x" "number_of ?w" hypreal_0_less_divide_iff]; |
|
69 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
70 |
Goal "(x/y < (0::hypreal)) = (0 < x & y < 0 | x < 0 & 0 < y)"; |
10751 | 71 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_less_0_iff]) 1); |
72 |
qed "hypreal_divide_less_0_iff"; |
|
73 |
Addsimps [inst "x" "number_of ?w" hypreal_divide_less_0_iff]; |
|
74 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
75 |
Goal "((0::hypreal) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"; |
10751 | 76 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_0_le_mult_iff]) 1); |
13462 | 77 |
by Auto_tac; |
10751 | 78 |
qed "hypreal_0_le_divide_iff"; |
79 |
Addsimps [inst "x" "number_of ?w" hypreal_0_le_divide_iff]; |
|
80 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
81 |
Goal "(x/y <= (0::hypreal)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))"; |
13462 | 82 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, |
10751 | 83 |
hypreal_mult_le_0_iff]) 1); |
13462 | 84 |
by Auto_tac; |
10751 | 85 |
qed "hypreal_divide_le_0_iff"; |
86 |
Addsimps [inst "x" "number_of ?w" hypreal_divide_le_0_iff]; |
|
87 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
88 |
Goal "(inverse(x::hypreal) = 0) = (x = 0)"; |
13462 | 89 |
by (auto_tac (claset(), |
90 |
simpset() addsimps [HYPREAL_INVERSE_ZERO])); |
|
91 |
by (rtac ccontr 1); |
|
92 |
by (blast_tac (claset() addDs [hypreal_inverse_not_zero]) 1); |
|
10751 | 93 |
qed "hypreal_inverse_zero_iff"; |
94 |
Addsimps [hypreal_inverse_zero_iff]; |
|
95 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
96 |
Goal "(x/y = 0) = (x=0 | y=(0::hypreal))"; |
13462 | 97 |
by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def])); |
10751 | 98 |
qed "hypreal_divide_eq_0_iff"; |
99 |
Addsimps [hypreal_divide_eq_0_iff]; |
|
100 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
101 |
Goal "h ~= (0::hypreal) ==> h/h = 1"; |
13462 | 102 |
by (asm_simp_tac |
10751 | 103 |
(simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left]) 1); |
13462 | 104 |
qed "hypreal_divide_self_eq"; |
10751 | 105 |
Addsimps [hypreal_divide_self_eq]; |
106 |
||
107 |
||
108 |
(**** Factor cancellation theorems for "hypreal" ****) |
|
109 |
||
110 |
(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, |
|
111 |
but not (yet?) for k*m < n*k. **) |
|
112 |
||
113 |
bind_thm ("hypreal_mult_minus_right", hypreal_minus_mult_eq2 RS sym); |
|
114 |
||
115 |
Goal "(-y < -x) = ((x::hypreal) < y)"; |
|
116 |
by (arith_tac 1); |
|
117 |
qed "hypreal_minus_less_minus"; |
|
118 |
Addsimps [hypreal_minus_less_minus]; |
|
119 |
||
120 |
Goal "[| i<j; k < (0::hypreal) |] ==> j*k < i*k"; |
|
121 |
by (rtac (hypreal_minus_less_minus RS iffD1) 1); |
|
13462 | 122 |
by (auto_tac (claset(), |
10751 | 123 |
simpset() delsimps [hypreal_minus_mult_eq2 RS sym] |
124 |
addsimps [hypreal_minus_mult_eq2, |
|
13462 | 125 |
hypreal_mult_less_mono1])); |
10751 | 126 |
qed "hypreal_mult_less_mono1_neg"; |
127 |
||
128 |
Goal "[| i<j; k < (0::hypreal) |] ==> k*j < k*i"; |
|
129 |
by (rtac (hypreal_minus_less_minus RS iffD1) 1); |
|
13462 | 130 |
by (auto_tac (claset(), |
10751 | 131 |
simpset() delsimps [hypreal_minus_mult_eq1 RS sym] |
132 |
addsimps [hypreal_minus_mult_eq1, |
|
133 |
hypreal_mult_less_mono2])); |
|
134 |
qed "hypreal_mult_less_mono2_neg"; |
|
135 |
||
136 |
Goal "[| i <= j; k <= (0::hypreal) |] ==> j*k <= i*k"; |
|
13462 | 137 |
by (auto_tac (claset(), |
138 |
simpset() addsimps [order_le_less, hypreal_mult_less_mono1_neg])); |
|
10751 | 139 |
qed "hypreal_mult_le_mono1_neg"; |
140 |
||
141 |
Goal "[| i <= j; k <= (0::hypreal) |] ==> k*j <= k*i"; |
|
142 |
by (dtac hypreal_mult_le_mono1_neg 1); |
|
143 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]))); |
|
144 |
qed "hypreal_mult_le_mono2_neg"; |
|
145 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
146 |
Goal "(m*k < n*k) = (((0::hypreal) < k & m<n) | (k < 0 & n<m))"; |
10751 | 147 |
by (case_tac "k = (0::hypreal)" 1); |
13462 | 148 |
by (auto_tac (claset(), |
149 |
simpset() addsimps [linorder_neq_iff, |
|
150 |
hypreal_mult_less_mono1, hypreal_mult_less_mono1_neg])); |
|
151 |
by (auto_tac (claset(), |
|
10751 | 152 |
simpset() addsimps [linorder_not_less, |
13462 | 153 |
inst "y1" "m*k" (linorder_not_le RS sym), |
10751 | 154 |
inst "y1" "m" (linorder_not_le RS sym)])); |
155 |
by (TRYALL (etac notE)); |
|
13462 | 156 |
by (auto_tac (claset(), |
10751 | 157 |
simpset() addsimps [order_less_imp_le, hypreal_mult_le_mono1, |
13462 | 158 |
hypreal_mult_le_mono1_neg])); |
10751 | 159 |
qed "hypreal_mult_less_cancel2"; |
160 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
161 |
Goal "(m*k <= n*k) = (((0::hypreal) < k --> m<=n) & (k < 0 --> n<=m))"; |
13462 | 162 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, |
10751 | 163 |
hypreal_mult_less_cancel2]) 1); |
164 |
qed "hypreal_mult_le_cancel2"; |
|
165 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
166 |
Goal "(k*m < k*n) = (((0::hypreal) < k & m<n) | (k < 0 & n<m))"; |
13462 | 167 |
by (simp_tac (simpset() addsimps [inst "z" "k" hypreal_mult_commute, |
10751 | 168 |
hypreal_mult_less_cancel2]) 1); |
169 |
qed "hypreal_mult_less_cancel1"; |
|
170 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
171 |
Goal "!!k::hypreal. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"; |
13462 | 172 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, |
10751 | 173 |
hypreal_mult_less_cancel1]) 1); |
174 |
qed "hypreal_mult_le_cancel1"; |
|
175 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
176 |
Goal "!!k::hypreal. (k*m = k*n) = (k = 0 | m=n)"; |
10751 | 177 |
by (case_tac "k=0" 1); |
13462 | 178 |
by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_cancel])); |
10751 | 179 |
qed "hypreal_mult_eq_cancel1"; |
180 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
181 |
Goal "!!k::hypreal. (m*k = n*k) = (k = 0 | m=n)"; |
10751 | 182 |
by (case_tac "k=0" 1); |
13462 | 183 |
by (auto_tac (claset(), simpset() addsimps [hypreal_mult_right_cancel])); |
10751 | 184 |
qed "hypreal_mult_eq_cancel2"; |
185 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
186 |
Goal "!!k::hypreal. k~=0 ==> (k*m) / (k*n) = (m/n)"; |
10751 | 187 |
by (asm_simp_tac |
13462 | 188 |
(simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]) 1); |
10751 | 189 |
by (subgoal_tac "k * m * (inverse k * inverse n) = \ |
190 |
\ (k * inverse k) * (m * inverse n)" 1); |
|
13462 | 191 |
by (asm_full_simp_tac (simpset() addsimps []) 1); |
192 |
by (asm_full_simp_tac (HOL_ss addsimps hypreal_mult_ac) 1); |
|
10751 | 193 |
qed "hypreal_mult_div_cancel1"; |
194 |
||
195 |
(*For ExtractCommonTerm*) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
196 |
Goal "(k*m) / (k*n) = (if k = (0::hypreal) then 0 else m/n)"; |
13462 | 197 |
by (simp_tac (simpset() addsimps [hypreal_mult_div_cancel1]) 1); |
10751 | 198 |
qed "hypreal_mult_div_cancel_disj"; |
199 |
||
200 |
||
201 |
local |
|
202 |
open Hyperreal_Numeral_Simprocs |
|
203 |
in |
|
204 |
||
13462 | 205 |
val rel_hypreal_number_of = [eq_hypreal_number_of, less_hypreal_number_of, |
10751 | 206 |
le_hypreal_number_of_eq_not_less]; |
207 |
||
208 |
structure CancelNumeralFactorCommon = |
|
209 |
struct |
|
13462 | 210 |
val mk_coeff = mk_coeff |
211 |
val dest_coeff = dest_coeff 1 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
212 |
val trans_tac = Real_Numeral_Simprocs.trans_tac |
13462 | 213 |
val norm_tac = |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
214 |
ALLGOALS (simp_tac (HOL_ss addsimps hypreal_minus_from_mult_simps @ mult_1s)) |
10751 | 215 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hypreal_mult_minus_simps)) |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
216 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps hypreal_mult_ac)) |
13462 | 217 |
val numeral_simp_tac = |
10751 | 218 |
ALLGOALS (simp_tac (HOL_ss addsimps rel_hypreal_number_of@bin_simps)) |
219 |
val simplify_meta_eq = simplify_meta_eq |
|
220 |
end |
|
221 |
||
222 |
structure DivCancelNumeralFactor = CancelNumeralFactorFun |
|
223 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
224 |
val prove_conv = Bin_Simprocs.prove_conv |
10751 | 225 |
val mk_bal = HOLogic.mk_binop "HOL.divide" |
226 |
val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT |
|
227 |
val cancel = hypreal_mult_div_cancel1 RS trans |
|
228 |
val neg_exchanges = false |
|
229 |
) |
|
230 |
||
231 |
structure EqCancelNumeralFactor = CancelNumeralFactorFun |
|
232 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
233 |
val prove_conv = Bin_Simprocs.prove_conv |
10751 | 234 |
val mk_bal = HOLogic.mk_eq |
235 |
val dest_bal = HOLogic.dest_bin "op =" hyprealT |
|
236 |
val cancel = hypreal_mult_eq_cancel1 RS trans |
|
237 |
val neg_exchanges = false |
|
238 |
) |
|
239 |
||
240 |
structure LessCancelNumeralFactor = CancelNumeralFactorFun |
|
241 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
242 |
val prove_conv = Bin_Simprocs.prove_conv |
10751 | 243 |
val mk_bal = HOLogic.mk_binrel "op <" |
244 |
val dest_bal = HOLogic.dest_bin "op <" hyprealT |
|
245 |
val cancel = hypreal_mult_less_cancel1 RS trans |
|
246 |
val neg_exchanges = true |
|
247 |
) |
|
248 |
||
249 |
structure LeCancelNumeralFactor = CancelNumeralFactorFun |
|
250 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
251 |
val prove_conv = Bin_Simprocs.prove_conv |
10751 | 252 |
val mk_bal = HOLogic.mk_binrel "op <=" |
253 |
val dest_bal = HOLogic.dest_bin "op <=" hyprealT |
|
254 |
val cancel = hypreal_mult_le_cancel1 RS trans |
|
255 |
val neg_exchanges = true |
|
256 |
) |
|
257 |
||
13462 | 258 |
val hypreal_cancel_numeral_factors_relations = |
10751 | 259 |
map prep_simproc |
260 |
[("hyprealeq_cancel_numeral_factor", |
|
13462 | 261 |
["(l::hypreal) * m = n", "(l::hypreal) = m * n"], |
10751 | 262 |
EqCancelNumeralFactor.proc), |
13462 | 263 |
("hyprealless_cancel_numeral_factor", |
264 |
["(l::hypreal) * m < n", "(l::hypreal) < m * n"], |
|
10751 | 265 |
LessCancelNumeralFactor.proc), |
13462 | 266 |
("hyprealle_cancel_numeral_factor", |
267 |
["(l::hypreal) * m <= n", "(l::hypreal) <= m * n"], |
|
10751 | 268 |
LeCancelNumeralFactor.proc)]; |
269 |
||
270 |
val hypreal_cancel_numeral_factors_divide = prep_simproc |
|
13462 | 271 |
("hyprealdiv_cancel_numeral_factor", |
272 |
["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)", |
|
273 |
"((number_of v)::hypreal) / (number_of w)"], |
|
274 |
DivCancelNumeralFactor.proc); |
|
10751 | 275 |
|
13462 | 276 |
val hypreal_cancel_numeral_factors = |
277 |
hypreal_cancel_numeral_factors_relations @ |
|
10751 | 278 |
[hypreal_cancel_numeral_factors_divide]; |
279 |
||
280 |
end; |
|
281 |
||
282 |
Addsimprocs hypreal_cancel_numeral_factors; |
|
283 |
||
284 |
||
285 |
(*examples: |
|
286 |
print_depth 22; |
|
287 |
set timing; |
|
288 |
set trace_simp; |
|
13462 | 289 |
fun test s = (Goal s; by (Simp_tac 1)); |
10751 | 290 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
291 |
test "0 <= (y::hypreal) * -2"; |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
292 |
test "9*x = 12 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
293 |
test "(9*x) / (12 * (y::hypreal)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
294 |
test "9*x < 12 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
295 |
test "9*x <= 12 * (y::hypreal)"; |
10751 | 296 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
297 |
test "-99*x = 123 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
298 |
test "(-99*x) / (123 * (y::hypreal)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
299 |
test "-99*x < 123 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
300 |
test "-99*x <= 123 * (y::hypreal)"; |
10751 | 301 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
302 |
test "999*x = -396 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
303 |
test "(999*x) / (-396 * (y::hypreal)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
304 |
test "999*x < -396 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
305 |
test "999*x <= -396 * (y::hypreal)"; |
10751 | 306 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
307 |
test "-99*x = -81 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
308 |
test "(-99*x) / (-81 * (y::hypreal)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
309 |
test "-99*x <= -81 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
310 |
test "-99*x < -81 * (y::hypreal)"; |
10751 | 311 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
312 |
test "-2 * x = -1 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
313 |
test "-2 * x = -(y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
314 |
test "(-2 * x) / (-1 * (y::hypreal)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
315 |
test "-2 * x < -(y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
316 |
test "-2 * x <= -1 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
317 |
test "-x < -23 * (y::hypreal)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
318 |
test "-x <= -23 * (y::hypreal)"; |
10751 | 319 |
*) |
320 |
||
321 |
||
322 |
(** Declarations for ExtractCommonTerm **) |
|
323 |
||
324 |
local |
|
325 |
open Hyperreal_Numeral_Simprocs |
|
326 |
in |
|
327 |
||
328 |
structure CancelFactorCommon = |
|
329 |
struct |
|
13462 | 330 |
val mk_sum = long_mk_prod |
331 |
val dest_sum = dest_prod |
|
332 |
val mk_coeff = mk_coeff |
|
333 |
val dest_coeff = dest_coeff |
|
334 |
val find_first = find_first [] |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
335 |
val trans_tac = Real_Numeral_Simprocs.trans_tac |
10751 | 336 |
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hypreal_mult_ac)) |
337 |
end; |
|
338 |
||
339 |
structure EqCancelFactor = ExtractCommonTermFun |
|
340 |
(open CancelFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
341 |
val prove_conv = Bin_Simprocs.prove_conv |
10751 | 342 |
val mk_bal = HOLogic.mk_eq |
343 |
val dest_bal = HOLogic.dest_bin "op =" hyprealT |
|
344 |
val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_eq_cancel1 |
|
345 |
); |
|
346 |
||
347 |
||
348 |
structure DivideCancelFactor = ExtractCommonTermFun |
|
349 |
(open CancelFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
350 |
val prove_conv = Bin_Simprocs.prove_conv |
10751 | 351 |
val mk_bal = HOLogic.mk_binop "HOL.divide" |
352 |
val dest_bal = HOLogic.dest_bin "HOL.divide" hyprealT |
|
353 |
val simplify_meta_eq = cancel_simplify_meta_eq hypreal_mult_div_cancel_disj |
|
354 |
); |
|
355 |
||
13462 | 356 |
val hypreal_cancel_factor = |
10751 | 357 |
map prep_simproc |
13462 | 358 |
[("hypreal_eq_cancel_factor", ["(l::hypreal) * m = n", "(l::hypreal) = m * n"], |
10751 | 359 |
EqCancelFactor.proc), |
13462 | 360 |
("hypreal_divide_cancel_factor", ["((l::hypreal) * m) / n", "(l::hypreal) / (m * n)"], |
10751 | 361 |
DivideCancelFactor.proc)]; |
362 |
||
363 |
end; |
|
364 |
||
365 |
Addsimprocs hypreal_cancel_factor; |
|
366 |
||
367 |
||
368 |
(*examples: |
|
369 |
print_depth 22; |
|
370 |
set timing; |
|
371 |
set trace_simp; |
|
13462 | 372 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
10751 | 373 |
|
374 |
test "x*k = k*(y::hypreal)"; |
|
13462 | 375 |
test "k = k*(y::hypreal)"; |
10751 | 376 |
test "a*(b*c) = (b::hypreal)"; |
377 |
test "a*(b*c) = d*(b::hypreal)*(x*a)"; |
|
378 |
||
379 |
||
380 |
test "(x*k) / (k*(y::hypreal)) = (uu::hypreal)"; |
|
13462 | 381 |
test "(k) / (k*(y::hypreal)) = (uu::hypreal)"; |
10751 | 382 |
test "(a*(b*c)) / ((b::hypreal)) = (uu::hypreal)"; |
383 |
test "(a*(b*c)) / (d*(b::hypreal)*(x*a)) = (uu::hypreal)"; |
|
384 |
||
385 |
(*FIXME: what do we do about this?*) |
|
386 |
test "a*(b*c)/(y*z) = d*(b::hypreal)*(x*a)/z"; |
|
387 |
*) |
|
388 |
||
389 |
||
390 |
(*** Simplification of inequalities involving literal divisors ***) |
|
391 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
392 |
Goal "0<z ==> ((x::hypreal) <= y/z) = (x*z <= y)"; |
10751 | 393 |
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1); |
13462 | 394 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 395 |
by (etac ssubst 1); |
13462 | 396 |
by (stac hypreal_mult_le_cancel2 1); |
397 |
by (Asm_simp_tac 1); |
|
10751 | 398 |
qed "pos_hypreal_le_divide_eq"; |
399 |
Addsimps [inst "z" "number_of ?w" pos_hypreal_le_divide_eq]; |
|
400 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
401 |
Goal "z<0 ==> ((x::hypreal) <= y/z) = (y <= x*z)"; |
10751 | 402 |
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1); |
13462 | 403 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 404 |
by (etac ssubst 1); |
13462 | 405 |
by (stac hypreal_mult_le_cancel2 1); |
406 |
by (Asm_simp_tac 1); |
|
10751 | 407 |
qed "neg_hypreal_le_divide_eq"; |
408 |
Addsimps [inst "z" "number_of ?w" neg_hypreal_le_divide_eq]; |
|
409 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
410 |
Goal "0<z ==> (y/z <= (x::hypreal)) = (y <= x*z)"; |
10751 | 411 |
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1); |
13462 | 412 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 413 |
by (etac ssubst 1); |
13462 | 414 |
by (stac hypreal_mult_le_cancel2 1); |
415 |
by (Asm_simp_tac 1); |
|
10751 | 416 |
qed "pos_hypreal_divide_le_eq"; |
417 |
Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_le_eq]; |
|
418 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
419 |
Goal "z<0 ==> (y/z <= (x::hypreal)) = (x*z <= y)"; |
10751 | 420 |
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1); |
13462 | 421 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 422 |
by (etac ssubst 1); |
13462 | 423 |
by (stac hypreal_mult_le_cancel2 1); |
424 |
by (Asm_simp_tac 1); |
|
10751 | 425 |
qed "neg_hypreal_divide_le_eq"; |
426 |
Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_le_eq]; |
|
427 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
428 |
Goal "0<z ==> ((x::hypreal) < y/z) = (x*z < y)"; |
10751 | 429 |
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1); |
13462 | 430 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 431 |
by (etac ssubst 1); |
13462 | 432 |
by (stac hypreal_mult_less_cancel2 1); |
433 |
by (Asm_simp_tac 1); |
|
10751 | 434 |
qed "pos_hypreal_less_divide_eq"; |
435 |
Addsimps [inst "z" "number_of ?w" pos_hypreal_less_divide_eq]; |
|
436 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
437 |
Goal "z<0 ==> ((x::hypreal) < y/z) = (y < x*z)"; |
10751 | 438 |
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1); |
13462 | 439 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 440 |
by (etac ssubst 1); |
13462 | 441 |
by (stac hypreal_mult_less_cancel2 1); |
442 |
by (Asm_simp_tac 1); |
|
10751 | 443 |
qed "neg_hypreal_less_divide_eq"; |
444 |
Addsimps [inst "z" "number_of ?w" neg_hypreal_less_divide_eq]; |
|
445 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
446 |
Goal "0<z ==> (y/z < (x::hypreal)) = (y < x*z)"; |
10751 | 447 |
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1); |
13462 | 448 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 449 |
by (etac ssubst 1); |
13462 | 450 |
by (stac hypreal_mult_less_cancel2 1); |
451 |
by (Asm_simp_tac 1); |
|
10751 | 452 |
qed "pos_hypreal_divide_less_eq"; |
453 |
Addsimps [inst "z" "number_of ?w" pos_hypreal_divide_less_eq]; |
|
454 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
455 |
Goal "z<0 ==> (y/z < (x::hypreal)) = (x*z < y)"; |
10751 | 456 |
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1); |
13462 | 457 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 458 |
by (etac ssubst 1); |
13462 | 459 |
by (stac hypreal_mult_less_cancel2 1); |
460 |
by (Asm_simp_tac 1); |
|
10751 | 461 |
qed "neg_hypreal_divide_less_eq"; |
462 |
Addsimps [inst "z" "number_of ?w" neg_hypreal_divide_less_eq]; |
|
463 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
464 |
Goal "z~=0 ==> ((x::hypreal) = y/z) = (x*z = y)"; |
10751 | 465 |
by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1); |
13462 | 466 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 467 |
by (etac ssubst 1); |
13462 | 468 |
by (stac hypreal_mult_eq_cancel2 1); |
469 |
by (Asm_simp_tac 1); |
|
10751 | 470 |
qed "hypreal_eq_divide_eq"; |
471 |
Addsimps [inst "z" "number_of ?w" hypreal_eq_divide_eq]; |
|
472 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
473 |
Goal "z~=0 ==> (y/z = (x::hypreal)) = (y = x*z)"; |
10751 | 474 |
by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1); |
13462 | 475 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 2); |
10751 | 476 |
by (etac ssubst 1); |
13462 | 477 |
by (stac hypreal_mult_eq_cancel2 1); |
478 |
by (Asm_simp_tac 1); |
|
10751 | 479 |
qed "hypreal_divide_eq_eq"; |
480 |
Addsimps [inst "z" "number_of ?w" hypreal_divide_eq_eq]; |
|
481 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
482 |
Goal "(m/k = n/k) = (k = 0 | m = (n::hypreal))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
483 |
by (case_tac "k=0" 1); |
13462 | 484 |
by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVIDE_ZERO]) 1); |
485 |
by (asm_simp_tac (simpset() addsimps [hypreal_divide_eq_eq, hypreal_eq_divide_eq, |
|
486 |
hypreal_mult_eq_cancel2]) 1); |
|
10751 | 487 |
qed "hypreal_divide_eq_cancel2"; |
488 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
489 |
Goal "(k/m = k/n) = (k = 0 | m = (n::hypreal))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
490 |
by (case_tac "m=0 | n = 0" 1); |
13462 | 491 |
by (auto_tac (claset(), |
492 |
simpset() addsimps [HYPREAL_DIVIDE_ZERO, hypreal_divide_eq_eq, |
|
493 |
hypreal_eq_divide_eq, hypreal_mult_eq_cancel1])); |
|
10751 | 494 |
qed "hypreal_divide_eq_cancel1"; |
495 |
||
496 |
(** Division by 1, -1 **) |
|
497 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
498 |
Goal "(x::hypreal)/1 = x"; |
13462 | 499 |
by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); |
10751 | 500 |
qed "hypreal_divide_1"; |
501 |
Addsimps [hypreal_divide_1]; |
|
502 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
503 |
Goal "x/-1 = -(x::hypreal)"; |
13462 | 504 |
by (Simp_tac 1); |
10751 | 505 |
qed "hypreal_divide_minus1"; |
506 |
Addsimps [hypreal_divide_minus1]; |
|
507 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
508 |
Goal "-1/(x::hypreal) = - (1/x)"; |
13462 | 509 |
by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1); |
10751 | 510 |
qed "hypreal_minus1_divide"; |
511 |
Addsimps [hypreal_minus1_divide]; |
|
512 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
513 |
Goal "[| (0::hypreal) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2"; |
13462 | 514 |
by (res_inst_tac [("x","(min d1 d2)/2")] exI 1); |
515 |
by (asm_simp_tac (simpset() addsimps [min_def]) 1); |
|
10751 | 516 |
qed "hypreal_lbound_gt_zero"; |
517 |
||
518 |
||
519 |
(*** General rewrites to improve automation, like those for type "int" ***) |
|
520 |
||
521 |
(** The next several equations can make the simplifier loop! **) |
|
522 |
||
523 |
Goal "(x < - y) = (y < - (x::hypreal))"; |
|
13462 | 524 |
by Auto_tac; |
525 |
qed "hypreal_less_minus"; |
|
10751 | 526 |
|
527 |
Goal "(- x < y) = (- y < (x::hypreal))"; |
|
13462 | 528 |
by Auto_tac; |
529 |
qed "hypreal_minus_less"; |
|
10751 | 530 |
|
531 |
Goal "(x <= - y) = (y <= - (x::hypreal))"; |
|
13462 | 532 |
by Auto_tac; |
533 |
qed "hypreal_le_minus"; |
|
10751 | 534 |
|
535 |
Goal "(- x <= y) = (- y <= (x::hypreal))"; |
|
13462 | 536 |
by Auto_tac; |
537 |
qed "hypreal_minus_le"; |
|
10751 | 538 |
|
539 |
Goal "(x = - y) = (y = - (x::hypreal))"; |
|
540 |
by Auto_tac; |
|
541 |
qed "hypreal_equation_minus"; |
|
542 |
||
543 |
Goal "(- x = y) = (- (y::hypreal) = x)"; |
|
544 |
by Auto_tac; |
|
545 |
qed "hypreal_minus_equation"; |
|
546 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
547 |
Goal "(x + - a = (0::hypreal)) = (x=a)"; |
10751 | 548 |
by (arith_tac 1); |
549 |
qed "hypreal_add_minus_iff"; |
|
550 |
Addsimps [hypreal_add_minus_iff]; |
|
551 |
||
552 |
Goal "(-b = -a) = (b = (a::hypreal))"; |
|
553 |
by (arith_tac 1); |
|
554 |
qed "hypreal_minus_eq_cancel"; |
|
555 |
Addsimps [hypreal_minus_eq_cancel]; |
|
556 |
||
557 |
Goal "(-s <= -r) = ((r::hypreal) <= s)"; |
|
13462 | 558 |
by (stac hypreal_minus_le 1); |
559 |
by (Simp_tac 1); |
|
10751 | 560 |
qed "hypreal_le_minus_iff"; |
13462 | 561 |
Addsimps [hypreal_le_minus_iff]; |
10751 | 562 |
|
563 |
||
564 |
(*Distributive laws for literals*) |
|
565 |
Addsimps (map (inst "w" "number_of ?v") |
|
13462 | 566 |
[hypreal_add_mult_distrib, hypreal_add_mult_distrib2, |
567 |
hypreal_diff_mult_distrib, hypreal_diff_mult_distrib2]); |
|
10751 | 568 |
|
13462 | 569 |
Addsimps (map (inst "x" "number_of ?v") |
570 |
[hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]); |
|
571 |
Addsimps (map (inst "y" "number_of ?v") |
|
572 |
[hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]); |
|
10751 | 573 |
|
13462 | 574 |
Addsimps (map (simplify (simpset()) o inst "x" "1") |
575 |
[hypreal_less_minus, hypreal_le_minus, hypreal_equation_minus]); |
|
576 |
Addsimps (map (simplify (simpset()) o inst "y" "1") |
|
577 |
[hypreal_minus_less, hypreal_minus_le, hypreal_minus_equation]); |
|
10751 | 578 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
579 |
(*** Simprules combining x+y and 0 ***) |
10751 | 580 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
581 |
Goal "(x+y = (0::hypreal)) = (y = -x)"; |
13462 | 582 |
by Auto_tac; |
10751 | 583 |
qed "hypreal_add_eq_0_iff"; |
584 |
AddIffs [hypreal_add_eq_0_iff]; |
|
585 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
586 |
Goal "(x+y < (0::hypreal)) = (y < -x)"; |
13462 | 587 |
by Auto_tac; |
10751 | 588 |
qed "hypreal_add_less_0_iff"; |
589 |
AddIffs [hypreal_add_less_0_iff]; |
|
590 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
591 |
Goal "((0::hypreal) < x+y) = (-x < y)"; |
13462 | 592 |
by Auto_tac; |
10751 | 593 |
qed "hypreal_0_less_add_iff"; |
594 |
AddIffs [hypreal_0_less_add_iff]; |
|
595 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
596 |
Goal "(x+y <= (0::hypreal)) = (y <= -x)"; |
13462 | 597 |
by Auto_tac; |
10751 | 598 |
qed "hypreal_add_le_0_iff"; |
599 |
AddIffs [hypreal_add_le_0_iff]; |
|
600 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
601 |
Goal "((0::hypreal) <= x+y) = (-x <= y)"; |
13462 | 602 |
by Auto_tac; |
10751 | 603 |
qed "hypreal_0_le_add_iff"; |
604 |
AddIffs [hypreal_0_le_add_iff]; |
|
605 |
||
606 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
607 |
(** Simprules combining x-y and 0; see also hypreal_less_iff_diff_less_0 etc |
10751 | 608 |
in HyperBin |
609 |
**) |
|
610 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
611 |
Goal "((0::hypreal) < x-y) = (y < x)"; |
13462 | 612 |
by Auto_tac; |
10751 | 613 |
qed "hypreal_0_less_diff_iff"; |
614 |
AddIffs [hypreal_0_less_diff_iff]; |
|
615 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
616 |
Goal "((0::hypreal) <= x-y) = (y <= x)"; |
13462 | 617 |
by Auto_tac; |
10751 | 618 |
qed "hypreal_0_le_diff_iff"; |
619 |
AddIffs [hypreal_0_le_diff_iff]; |
|
620 |
||
621 |
(* |
|
622 |
FIXME: we should have this, as for type int, but many proofs would break. |
|
623 |
It replaces x+-y by x-y. |
|
624 |
Addsimps [symmetric hypreal_diff_def]; |
|
625 |
*) |
|
626 |
||
627 |
Goal "-(x-y) = y - (x::hypreal)"; |
|
628 |
by (arith_tac 1); |
|
629 |
qed "hypreal_minus_diff_eq"; |
|
630 |
Addsimps [hypreal_minus_diff_eq]; |
|
631 |
||
632 |
||
633 |
(*** Density of the Hyperreals ***) |
|
634 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
635 |
Goal "x < y ==> x < (x+y) / (2::hypreal)"; |
10751 | 636 |
by Auto_tac; |
637 |
qed "hypreal_less_half_sum"; |
|
638 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
639 |
Goal "x < y ==> (x+y)/(2::hypreal) < y"; |
10751 | 640 |
by Auto_tac; |
641 |
qed "hypreal_gt_half_sum"; |
|
642 |
||
643 |
Goal "x < y ==> EX r::hypreal. x < r & r < y"; |
|
644 |
by (blast_tac (claset() addSIs [hypreal_less_half_sum, hypreal_gt_half_sum]) 1); |
|
645 |
qed "hypreal_dense"; |
|
646 |
||
647 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
648 |
(*Replaces "inverse #nn" by 1/#nn *) |
10751 | 649 |
Addsimps [inst "x" "number_of ?w" hypreal_inverse_eq_divide]; |