author | berghofe |
Fri, 11 Jul 2003 14:55:17 +0200 | |
changeset 14102 | 8af7334af4b3 |
parent 13485 | acf39e924091 |
child 14268 | 5cf13e80be0e |
permissions | -rw-r--r-- |
10722 | 1 |
(* Title: HOL/Real/RealArith.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::real)"; |
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 "real_diff_minus_eq"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
14 |
Addsimps [real_diff_minus_eq]; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
15 |
|
10722 | 16 |
(** Division and inverse **) |
17 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
18 |
Goal "0/x = (0::real)"; |
13462 | 19 |
by (simp_tac (simpset() addsimps [real_divide_def]) 1); |
10722 | 20 |
qed "real_0_divide"; |
21 |
Addsimps [real_0_divide]; |
|
22 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
23 |
Goal "((0::real) < inverse x) = (0 < x)"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
24 |
by (case_tac "x=0" 1); |
13462 | 25 |
by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1); |
26 |
by (auto_tac (claset() addDs [real_inverse_less_0], |
|
27 |
simpset() addsimps [linorder_neq_iff, real_inverse_gt_0])); |
|
10722 | 28 |
qed "real_0_less_inverse_iff"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
29 |
Addsimps [real_0_less_inverse_iff]; |
10722 | 30 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
31 |
Goal "(inverse x < (0::real)) = (x < 0)"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
32 |
by (case_tac "x=0" 1); |
13462 | 33 |
by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1); |
34 |
by (auto_tac (claset() addDs [real_inverse_less_0], |
|
35 |
simpset() addsimps [linorder_neq_iff, real_inverse_gt_0])); |
|
10722 | 36 |
qed "real_inverse_less_0_iff"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
37 |
Addsimps [real_inverse_less_0_iff]; |
10722 | 38 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
39 |
Goal "((0::real) <= inverse x) = (0 <= x)"; |
13462 | 40 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
10722 | 41 |
qed "real_0_le_inverse_iff"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
42 |
Addsimps [real_0_le_inverse_iff]; |
10722 | 43 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
44 |
Goal "(inverse x <= (0::real)) = (x <= 0)"; |
13462 | 45 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); |
10722 | 46 |
qed "real_inverse_le_0_iff"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
47 |
Addsimps [real_inverse_le_0_iff]; |
10722 | 48 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
49 |
Goalw [real_divide_def] "x/(0::real) = 0"; |
13462 | 50 |
by (stac INVERSE_ZERO 1); |
51 |
by (Simp_tac 1); |
|
10722 | 52 |
qed "REAL_DIVIDE_ZERO"; |
53 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
54 |
Goal "inverse (x::real) = 1/x"; |
13462 | 55 |
by (simp_tac (simpset() addsimps [real_divide_def]) 1); |
10722 | 56 |
qed "real_inverse_eq_divide"; |
57 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
58 |
Goal "((0::real) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)"; |
10722 | 59 |
by (simp_tac (simpset() addsimps [real_divide_def, real_0_less_mult_iff]) 1); |
60 |
qed "real_0_less_divide_iff"; |
|
61 |
Addsimps [inst "x" "number_of ?w" real_0_less_divide_iff]; |
|
62 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
63 |
Goal "(x/y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)"; |
10722 | 64 |
by (simp_tac (simpset() addsimps [real_divide_def, real_mult_less_0_iff]) 1); |
65 |
qed "real_divide_less_0_iff"; |
|
66 |
Addsimps [inst "x" "number_of ?w" real_divide_less_0_iff]; |
|
67 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
68 |
Goal "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"; |
10722 | 69 |
by (simp_tac (simpset() addsimps [real_divide_def, real_0_le_mult_iff]) 1); |
13462 | 70 |
by Auto_tac; |
10722 | 71 |
qed "real_0_le_divide_iff"; |
72 |
Addsimps [inst "x" "number_of ?w" real_0_le_divide_iff]; |
|
73 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
74 |
Goal "(x/y <= (0::real)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))"; |
10722 | 75 |
by (simp_tac (simpset() addsimps [real_divide_def, real_mult_le_0_iff]) 1); |
13462 | 76 |
by Auto_tac; |
10722 | 77 |
qed "real_divide_le_0_iff"; |
78 |
Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff]; |
|
79 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
80 |
Goal "(inverse(x::real) = 0) = (x = 0)"; |
13462 | 81 |
by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO])); |
82 |
by (rtac ccontr 1); |
|
83 |
by (blast_tac (claset() addDs [real_inverse_not_zero]) 1); |
|
10722 | 84 |
qed "real_inverse_zero_iff"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
85 |
Addsimps [real_inverse_zero_iff]; |
10722 | 86 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
87 |
Goal "(x/y = 0) = (x=0 | y=(0::real))"; |
13462 | 88 |
by (auto_tac (claset(), simpset() addsimps [real_divide_def])); |
10722 | 89 |
qed "real_divide_eq_0_iff"; |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
90 |
Addsimps [real_divide_eq_0_iff]; |
10722 | 91 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
92 |
Goal "h ~= (0::real) ==> h/h = 1"; |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
93 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_inv_left]) 1); |
13462 | 94 |
qed "real_divide_self_eq"; |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
95 |
Addsimps [real_divide_self_eq]; |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
96 |
|
10722 | 97 |
|
98 |
(**** Factor cancellation theorems for "real" ****) |
|
99 |
||
100 |
(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, |
|
101 |
but not (yet?) for k*m < n*k. **) |
|
12483
0a01efff43e9
new rewrite rules for use by arith_tac to take care of uminus.
nipkow
parents:
12018
diff
changeset
|
102 |
(* unused?? bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym); *) |
10722 | 103 |
|
104 |
Goal "(-y < -x) = ((x::real) < y)"; |
|
105 |
by (arith_tac 1); |
|
106 |
qed "real_minus_less_minus"; |
|
107 |
Addsimps [real_minus_less_minus]; |
|
108 |
||
109 |
Goal "[| i<j; k < (0::real) |] ==> j*k < i*k"; |
|
110 |
by (rtac (real_minus_less_minus RS iffD1) 1); |
|
12483
0a01efff43e9
new rewrite rules for use by arith_tac to take care of uminus.
nipkow
parents:
12018
diff
changeset
|
111 |
by (auto_tac (claset(), |
0a01efff43e9
new rewrite rules for use by arith_tac to take care of uminus.
nipkow
parents:
12018
diff
changeset
|
112 |
simpset() delsimps [real_mult_minus_eq2] |
13462 | 113 |
addsimps [real_minus_mult_eq2])); |
10722 | 114 |
qed "real_mult_less_mono1_neg"; |
115 |
||
116 |
Goal "[| i<j; k < (0::real) |] ==> k*j < k*i"; |
|
117 |
by (rtac (real_minus_less_minus RS iffD1) 1); |
|
13462 | 118 |
by (auto_tac (claset(), |
12483
0a01efff43e9
new rewrite rules for use by arith_tac to take care of uminus.
nipkow
parents:
12018
diff
changeset
|
119 |
simpset() delsimps [real_mult_minus_eq1] |
13462 | 120 |
addsimps [real_minus_mult_eq1])); |
10722 | 121 |
qed "real_mult_less_mono2_neg"; |
122 |
||
123 |
Goal "[| i <= j; k <= (0::real) |] ==> j*k <= i*k"; |
|
13462 | 124 |
by (auto_tac (claset(), |
125 |
simpset() addsimps [order_le_less, real_mult_less_mono1_neg])); |
|
10722 | 126 |
qed "real_mult_le_mono1_neg"; |
127 |
||
128 |
Goal "[| i <= j; k <= (0::real) |] ==> k*j <= k*i"; |
|
129 |
by (dtac real_mult_le_mono1_neg 1); |
|
130 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute]))); |
|
131 |
qed "real_mult_le_mono2_neg"; |
|
132 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
133 |
Goal "(m*k < n*k) = (((0::real) < k & m<n) | (k < 0 & n<m))"; |
10722 | 134 |
by (case_tac "k = (0::real)" 1); |
13462 | 135 |
by (auto_tac (claset(), |
136 |
simpset() addsimps [linorder_neq_iff, |
|
137 |
real_mult_less_mono1, real_mult_less_mono1_neg])); |
|
138 |
by (auto_tac (claset(), |
|
10722 | 139 |
simpset() addsimps [linorder_not_less, |
13462 | 140 |
inst "y1" "m*k" (linorder_not_le RS sym), |
10722 | 141 |
inst "y1" "m" (linorder_not_le RS sym)])); |
142 |
by (TRYALL (etac notE)); |
|
13462 | 143 |
by (auto_tac (claset(), |
10722 | 144 |
simpset() addsimps [order_less_imp_le, real_mult_le_mono1, |
13462 | 145 |
real_mult_le_mono1_neg])); |
10722 | 146 |
qed "real_mult_less_cancel2"; |
147 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
148 |
Goal "(m*k <= n*k) = (((0::real) < k --> m<=n) & (k < 0 --> n<=m))"; |
13462 | 149 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, |
10722 | 150 |
real_mult_less_cancel2]) 1); |
151 |
qed "real_mult_le_cancel2"; |
|
152 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
153 |
Goal "(k*m < k*n) = (((0::real) < k & m<n) | (k < 0 & n<m))"; |
13462 | 154 |
by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute, |
10722 | 155 |
real_mult_less_cancel2]) 1); |
156 |
qed "real_mult_less_cancel1"; |
|
157 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
158 |
Goal "!!k::real. (k*m <= k*n) = ((0 < k --> m<=n) & (k < 0 --> n<=m))"; |
13462 | 159 |
by (simp_tac (simpset() addsimps [linorder_not_less RS sym, |
10722 | 160 |
real_mult_less_cancel1]) 1); |
161 |
qed "real_mult_le_cancel1"; |
|
162 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
163 |
Goal "!!k::real. (k*m = k*n) = (k = 0 | m=n)"; |
10722 | 164 |
by (case_tac "k=0" 1); |
13462 | 165 |
by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel])); |
10722 | 166 |
qed "real_mult_eq_cancel1"; |
167 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
168 |
Goal "!!k::real. (m*k = n*k) = (k = 0 | m=n)"; |
10722 | 169 |
by (case_tac "k=0" 1); |
13462 | 170 |
by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel])); |
10722 | 171 |
qed "real_mult_eq_cancel2"; |
172 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
173 |
Goal "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)"; |
10722 | 174 |
by (asm_simp_tac |
13462 | 175 |
(simpset() addsimps [real_divide_def, real_inverse_distrib]) 1); |
10722 | 176 |
by (subgoal_tac "k * m * (inverse k * inverse n) = \ |
177 |
\ (k * inverse k) * (m * inverse n)" 1); |
|
13462 | 178 |
by (asm_full_simp_tac (simpset() addsimps []) 1); |
179 |
by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1); |
|
10722 | 180 |
qed "real_mult_div_cancel1"; |
181 |
||
182 |
(*For ExtractCommonTerm*) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
183 |
Goal "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"; |
13462 | 184 |
by (simp_tac (simpset() addsimps [real_mult_div_cancel1]) 1); |
10722 | 185 |
qed "real_mult_div_cancel_disj"; |
186 |
||
187 |
||
188 |
local |
|
189 |
open Real_Numeral_Simprocs |
|
190 |
in |
|
191 |
||
13462 | 192 |
val rel_real_number_of = [eq_real_number_of, less_real_number_of, |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
193 |
le_real_number_of_eq_not_less] |
10722 | 194 |
|
195 |
structure CancelNumeralFactorCommon = |
|
196 |
struct |
|
13462 | 197 |
val mk_coeff = mk_coeff |
198 |
val dest_coeff = dest_coeff 1 |
|
10722 | 199 |
val trans_tac = trans_tac |
13462 | 200 |
val norm_tac = |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
201 |
ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps @ mult_1s)) |
10722 | 202 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps)) |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
203 |
THEN ALLGOALS (simp_tac (HOL_ss addsimps real_mult_ac)) |
13462 | 204 |
val numeral_simp_tac = |
10722 | 205 |
ALLGOALS (simp_tac (HOL_ss addsimps rel_real_number_of@bin_simps)) |
206 |
val simplify_meta_eq = simplify_meta_eq |
|
207 |
end |
|
208 |
||
209 |
structure DivCancelNumeralFactor = CancelNumeralFactorFun |
|
210 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
211 |
val prove_conv = Bin_Simprocs.prove_conv |
10722 | 212 |
val mk_bal = HOLogic.mk_binop "HOL.divide" |
213 |
val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT |
|
214 |
val cancel = real_mult_div_cancel1 RS trans |
|
215 |
val neg_exchanges = false |
|
216 |
) |
|
217 |
||
218 |
structure EqCancelNumeralFactor = CancelNumeralFactorFun |
|
219 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
220 |
val prove_conv = Bin_Simprocs.prove_conv |
10722 | 221 |
val mk_bal = HOLogic.mk_eq |
222 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT |
|
223 |
val cancel = real_mult_eq_cancel1 RS trans |
|
224 |
val neg_exchanges = false |
|
225 |
) |
|
226 |
||
227 |
structure LessCancelNumeralFactor = CancelNumeralFactorFun |
|
228 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
229 |
val prove_conv = Bin_Simprocs.prove_conv |
10722 | 230 |
val mk_bal = HOLogic.mk_binrel "op <" |
231 |
val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT |
|
232 |
val cancel = real_mult_less_cancel1 RS trans |
|
233 |
val neg_exchanges = true |
|
234 |
) |
|
235 |
||
236 |
structure LeCancelNumeralFactor = CancelNumeralFactorFun |
|
237 |
(open CancelNumeralFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
238 |
val prove_conv = Bin_Simprocs.prove_conv |
10722 | 239 |
val mk_bal = HOLogic.mk_binrel "op <=" |
240 |
val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT |
|
241 |
val cancel = real_mult_le_cancel1 RS trans |
|
242 |
val neg_exchanges = true |
|
243 |
) |
|
244 |
||
13462 | 245 |
val real_cancel_numeral_factors_relations = |
10722 | 246 |
map prep_simproc |
247 |
[("realeq_cancel_numeral_factor", |
|
13462 | 248 |
["(l::real) * m = n", "(l::real) = m * n"], |
10722 | 249 |
EqCancelNumeralFactor.proc), |
13462 | 250 |
("realless_cancel_numeral_factor", |
251 |
["(l::real) * m < n", "(l::real) < m * n"], |
|
10722 | 252 |
LessCancelNumeralFactor.proc), |
13462 | 253 |
("realle_cancel_numeral_factor", |
254 |
["(l::real) * m <= n", "(l::real) <= m * n"], |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
255 |
LeCancelNumeralFactor.proc)] |
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
256 |
|
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
257 |
val real_cancel_numeral_factors_divide = prep_simproc |
13462 | 258 |
("realdiv_cancel_numeral_factor", |
259 |
["((l::real) * m) / n", "(l::real) / (m * n)", |
|
260 |
"((number_of v)::real) / (number_of w)"], |
|
261 |
DivCancelNumeralFactor.proc) |
|
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
262 |
|
13462 | 263 |
val real_cancel_numeral_factors = |
264 |
real_cancel_numeral_factors_relations @ |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
265 |
[real_cancel_numeral_factors_divide] |
10722 | 266 |
|
267 |
end; |
|
268 |
||
269 |
Addsimprocs real_cancel_numeral_factors; |
|
270 |
||
271 |
||
272 |
(*examples: |
|
273 |
print_depth 22; |
|
274 |
set timing; |
|
275 |
set trace_simp; |
|
13462 | 276 |
fun test s = (Goal s; by (Simp_tac 1)); |
10722 | 277 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
278 |
test "0 <= (y::real) * -2"; |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
279 |
test "9*x = 12 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
280 |
test "(9*x) / (12 * (y::real)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
281 |
test "9*x < 12 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
282 |
test "9*x <= 12 * (y::real)"; |
10722 | 283 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
284 |
test "-99*x = 132 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
285 |
test "(-99*x) / (132 * (y::real)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
286 |
test "-99*x < 132 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
287 |
test "-99*x <= 132 * (y::real)"; |
10722 | 288 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
289 |
test "999*x = -396 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
290 |
test "(999*x) / (-396 * (y::real)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
291 |
test "999*x < -396 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
292 |
test "999*x <= -396 * (y::real)"; |
10722 | 293 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
294 |
test "(- ((2::real) * x) <= 2 * y)"; |
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
295 |
test "-99*x = -81 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
296 |
test "(-99*x) / (-81 * (y::real)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
297 |
test "-99*x <= -81 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
298 |
test "-99*x < -81 * (y::real)"; |
10722 | 299 |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
300 |
test "-2 * x = -1 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
301 |
test "-2 * x = -(y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
302 |
test "(-2 * x) / (-1 * (y::real)) = z"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
303 |
test "-2 * x < -(y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
304 |
test "-2 * x <= -1 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
305 |
test "-x < -23 * (y::real)"; |
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
306 |
test "-x <= -23 * (y::real)"; |
10722 | 307 |
*) |
308 |
||
309 |
||
310 |
(** Declarations for ExtractCommonTerm **) |
|
311 |
||
312 |
local |
|
313 |
open Real_Numeral_Simprocs |
|
314 |
in |
|
315 |
||
316 |
structure CancelFactorCommon = |
|
317 |
struct |
|
13462 | 318 |
val mk_sum = long_mk_prod |
319 |
val dest_sum = dest_prod |
|
320 |
val mk_coeff = mk_coeff |
|
321 |
val dest_coeff = dest_coeff |
|
322 |
val find_first = find_first [] |
|
10722 | 323 |
val trans_tac = trans_tac |
324 |
val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_mult_ac)) |
|
325 |
end; |
|
326 |
||
327 |
structure EqCancelFactor = ExtractCommonTermFun |
|
328 |
(open CancelFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
329 |
val prove_conv = Bin_Simprocs.prove_conv |
10722 | 330 |
val mk_bal = HOLogic.mk_eq |
331 |
val dest_bal = HOLogic.dest_bin "op =" HOLogic.realT |
|
332 |
val simplify_meta_eq = cancel_simplify_meta_eq real_mult_eq_cancel1 |
|
333 |
); |
|
334 |
||
335 |
||
336 |
structure DivideCancelFactor = ExtractCommonTermFun |
|
337 |
(open CancelFactorCommon |
|
13485
acf39e924091
tuned prove_conv (error reporting done within meta_simplifier.ML);
wenzelm
parents:
13462
diff
changeset
|
338 |
val prove_conv = Bin_Simprocs.prove_conv |
10722 | 339 |
val mk_bal = HOLogic.mk_binop "HOL.divide" |
340 |
val dest_bal = HOLogic.dest_bin "HOL.divide" HOLogic.realT |
|
341 |
val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj |
|
342 |
); |
|
343 |
||
13462 | 344 |
val real_cancel_factor = |
10722 | 345 |
map prep_simproc |
13462 | 346 |
[("real_eq_cancel_factor", ["(l::real) * m = n", "(l::real) = m * n"], EqCancelFactor.proc), |
347 |
("real_divide_cancel_factor", ["((l::real) * m) / n", "(l::real) / (m * n)"], |
|
10722 | 348 |
DivideCancelFactor.proc)]; |
349 |
||
350 |
end; |
|
351 |
||
352 |
Addsimprocs real_cancel_factor; |
|
353 |
||
354 |
||
355 |
(*examples: |
|
356 |
print_depth 22; |
|
357 |
set timing; |
|
358 |
set trace_simp; |
|
13462 | 359 |
fun test s = (Goal s; by (Asm_simp_tac 1)); |
10722 | 360 |
|
361 |
test "x*k = k*(y::real)"; |
|
13462 | 362 |
test "k = k*(y::real)"; |
10722 | 363 |
test "a*(b*c) = (b::real)"; |
364 |
test "a*(b*c) = d*(b::real)*(x*a)"; |
|
365 |
||
366 |
||
367 |
test "(x*k) / (k*(y::real)) = (uu::real)"; |
|
13462 | 368 |
test "(k) / (k*(y::real)) = (uu::real)"; |
10722 | 369 |
test "(a*(b*c)) / ((b::real)) = (uu::real)"; |
370 |
test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)"; |
|
371 |
||
372 |
(*FIXME: what do we do about this?*) |
|
373 |
test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z"; |
|
374 |
*) |
|
375 |
||
376 |
||
377 |
(*** Simplification of inequalities involving literal divisors ***) |
|
378 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
379 |
Goal "0<z ==> ((x::real) <= y/z) = (x*z <= y)"; |
10722 | 380 |
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1); |
13462 | 381 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 382 |
by (etac ssubst 1); |
13462 | 383 |
by (stac real_mult_le_cancel2 1); |
384 |
by (Asm_simp_tac 1); |
|
10722 | 385 |
qed "pos_real_le_divide_eq"; |
386 |
Addsimps [inst "z" "number_of ?w" pos_real_le_divide_eq]; |
|
387 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
388 |
Goal "z<0 ==> ((x::real) <= y/z) = (y <= x*z)"; |
10722 | 389 |
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1); |
13462 | 390 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 391 |
by (etac ssubst 1); |
13462 | 392 |
by (stac real_mult_le_cancel2 1); |
393 |
by (Asm_simp_tac 1); |
|
10722 | 394 |
qed "neg_real_le_divide_eq"; |
395 |
Addsimps [inst "z" "number_of ?w" neg_real_le_divide_eq]; |
|
396 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
397 |
Goal "0<z ==> (y/z <= (x::real)) = (y <= x*z)"; |
10722 | 398 |
by (subgoal_tac "(y <= x*z) = ((y/z)*z <= x*z)" 1); |
13462 | 399 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 400 |
by (etac ssubst 1); |
13462 | 401 |
by (stac real_mult_le_cancel2 1); |
402 |
by (Asm_simp_tac 1); |
|
10722 | 403 |
qed "pos_real_divide_le_eq"; |
404 |
Addsimps [inst "z" "number_of ?w" pos_real_divide_le_eq]; |
|
405 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
406 |
Goal "z<0 ==> (y/z <= (x::real)) = (x*z <= y)"; |
10722 | 407 |
by (subgoal_tac "(x*z <= y) = (x*z <= (y/z)*z)" 1); |
13462 | 408 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 409 |
by (etac ssubst 1); |
13462 | 410 |
by (stac real_mult_le_cancel2 1); |
411 |
by (Asm_simp_tac 1); |
|
10722 | 412 |
qed "neg_real_divide_le_eq"; |
413 |
Addsimps [inst "z" "number_of ?w" neg_real_divide_le_eq]; |
|
414 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
415 |
Goal "0<z ==> ((x::real) < y/z) = (x*z < y)"; |
10722 | 416 |
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1); |
13462 | 417 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 418 |
by (etac ssubst 1); |
13462 | 419 |
by (stac real_mult_less_cancel2 1); |
420 |
by (Asm_simp_tac 1); |
|
10722 | 421 |
qed "pos_real_less_divide_eq"; |
422 |
Addsimps [inst "z" "number_of ?w" pos_real_less_divide_eq]; |
|
423 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
424 |
Goal "z<0 ==> ((x::real) < y/z) = (y < x*z)"; |
10722 | 425 |
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1); |
13462 | 426 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 427 |
by (etac ssubst 1); |
13462 | 428 |
by (stac real_mult_less_cancel2 1); |
429 |
by (Asm_simp_tac 1); |
|
10722 | 430 |
qed "neg_real_less_divide_eq"; |
431 |
Addsimps [inst "z" "number_of ?w" neg_real_less_divide_eq]; |
|
432 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
433 |
Goal "0<z ==> (y/z < (x::real)) = (y < x*z)"; |
10722 | 434 |
by (subgoal_tac "(y < x*z) = ((y/z)*z < x*z)" 1); |
13462 | 435 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 436 |
by (etac ssubst 1); |
13462 | 437 |
by (stac real_mult_less_cancel2 1); |
438 |
by (Asm_simp_tac 1); |
|
10722 | 439 |
qed "pos_real_divide_less_eq"; |
440 |
Addsimps [inst "z" "number_of ?w" pos_real_divide_less_eq]; |
|
441 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
442 |
Goal "z<0 ==> (y/z < (x::real)) = (x*z < y)"; |
10722 | 443 |
by (subgoal_tac "(x*z < y) = (x*z < (y/z)*z)" 1); |
13462 | 444 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 445 |
by (etac ssubst 1); |
13462 | 446 |
by (stac real_mult_less_cancel2 1); |
447 |
by (Asm_simp_tac 1); |
|
10722 | 448 |
qed "neg_real_divide_less_eq"; |
449 |
Addsimps [inst "z" "number_of ?w" neg_real_divide_less_eq]; |
|
450 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
451 |
Goal "z~=0 ==> ((x::real) = y/z) = (x*z = y)"; |
10722 | 452 |
by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1); |
13462 | 453 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 454 |
by (etac ssubst 1); |
13462 | 455 |
by (stac real_mult_eq_cancel2 1); |
456 |
by (Asm_simp_tac 1); |
|
10722 | 457 |
qed "real_eq_divide_eq"; |
458 |
Addsimps [inst "z" "number_of ?w" real_eq_divide_eq]; |
|
459 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
460 |
Goal "z~=0 ==> (y/z = (x::real)) = (y = x*z)"; |
10722 | 461 |
by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1); |
13462 | 462 |
by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_assoc]) 2); |
10722 | 463 |
by (etac ssubst 1); |
13462 | 464 |
by (stac real_mult_eq_cancel2 1); |
465 |
by (Asm_simp_tac 1); |
|
10722 | 466 |
qed "real_divide_eq_eq"; |
467 |
Addsimps [inst "z" "number_of ?w" real_divide_eq_eq]; |
|
468 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
469 |
Goal "(m/k = n/k) = (k = 0 | m = (n::real))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
470 |
by (case_tac "k=0" 1); |
13462 | 471 |
by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1); |
472 |
by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq, |
|
473 |
real_mult_eq_cancel2]) 1); |
|
10722 | 474 |
qed "real_divide_eq_cancel2"; |
475 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
476 |
Goal "(k/m = k/n) = (k = 0 | m = (n::real))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
477 |
by (case_tac "m=0 | n = 0" 1); |
13462 | 478 |
by (auto_tac (claset(), |
479 |
simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq, |
|
480 |
real_eq_divide_eq, real_mult_eq_cancel1])); |
|
10722 | 481 |
qed "real_divide_eq_cancel1"; |
482 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
483 |
(*Moved from RealOrd.ML to use 0 *) |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
484 |
Goal "[| 0 < r; 0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)"; |
10722 | 485 |
by (auto_tac (claset() addIs [real_inverse_less_swap], simpset())); |
486 |
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1); |
|
487 |
by (res_inst_tac [("t","x")] (real_inverse_inverse RS subst) 1); |
|
488 |
by (auto_tac (claset() addIs [real_inverse_less_swap], |
|
13462 | 489 |
simpset() delsimps [real_inverse_inverse] |
490 |
addsimps [real_inverse_gt_0])); |
|
10722 | 491 |
qed "real_inverse_less_iff"; |
492 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
493 |
Goal "[| 0 < r; 0 < x|] ==> (inverse x <= inverse r) = (r <= (x::real))"; |
13462 | 494 |
by (asm_simp_tac (simpset() addsimps [linorder_not_less RS sym, |
495 |
real_inverse_less_iff]) 1); |
|
10722 | 496 |
qed "real_inverse_le_iff"; |
497 |
||
498 |
(** Division by 1, -1 **) |
|
499 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
500 |
Goal "(x::real)/1 = x"; |
13462 | 501 |
by (simp_tac (simpset() addsimps [real_divide_def]) 1); |
10722 | 502 |
qed "real_divide_1"; |
503 |
Addsimps [real_divide_1]; |
|
504 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
505 |
Goal "x/-1 = -(x::real)"; |
13462 | 506 |
by (Simp_tac 1); |
10722 | 507 |
qed "real_divide_minus1"; |
508 |
Addsimps [real_divide_minus1]; |
|
509 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
510 |
Goal "-1/(x::real) = - (1/x)"; |
13462 | 511 |
by (simp_tac (simpset() addsimps [real_divide_def, real_minus_inverse]) 1); |
10722 | 512 |
qed "real_minus1_divide"; |
513 |
Addsimps [real_minus1_divide]; |
|
514 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
515 |
Goal "[| (0::real) < d1; 0 < d2 |] ==> EX e. 0 < e & e < d1 & e < d2"; |
13462 | 516 |
by (res_inst_tac [("x","(min d1 d2)/2")] exI 1); |
517 |
by (asm_simp_tac (simpset() addsimps [min_def]) 1); |
|
10722 | 518 |
qed "real_lbound_gt_zero"; |
519 |
||
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
520 |
Goal "(inverse x = inverse y) = (x = (y::real))"; |
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
521 |
by (case_tac "x=0 | y=0" 1); |
13462 | 522 |
by (auto_tac (claset(), |
523 |
simpset() addsimps [real_inverse_eq_divide, |
|
524 |
DIVISION_BY_ZERO])); |
|
525 |
by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1); |
|
526 |
by (Asm_full_simp_tac 1); |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
527 |
qed "real_inverse_eq_iff"; |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
528 |
Addsimps [real_inverse_eq_iff]; |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
529 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
530 |
Goal "(z/x = z/y) = (z = 0 | x = (y::real))"; |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
531 |
by (case_tac "x=0 | y=0" 1); |
13462 | 532 |
by (auto_tac (claset(), |
533 |
simpset() addsimps [DIVISION_BY_ZERO])); |
|
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
534 |
by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1); |
13462 | 535 |
by Auto_tac; |
10778
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
536 |
qed "real_divide_eq_iff"; |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
537 |
Addsimps [real_divide_eq_iff]; |
2c6605049646
more tidying, especially to remove real_of_posnat
paulson
parents:
10752
diff
changeset
|
538 |
|
10722 | 539 |
|
540 |
(*** General rewrites to improve automation, like those for type "int" ***) |
|
541 |
||
542 |
(** The next several equations can make the simplifier loop! **) |
|
543 |
||
544 |
Goal "(x < - y) = (y < - (x::real))"; |
|
13462 | 545 |
by Auto_tac; |
546 |
qed "real_less_minus"; |
|
10722 | 547 |
|
548 |
Goal "(- x < y) = (- y < (x::real))"; |
|
13462 | 549 |
by Auto_tac; |
550 |
qed "real_minus_less"; |
|
10722 | 551 |
|
552 |
Goal "(x <= - y) = (y <= - (x::real))"; |
|
13462 | 553 |
by Auto_tac; |
554 |
qed "real_le_minus"; |
|
10722 | 555 |
|
556 |
Goal "(- x <= y) = (- y <= (x::real))"; |
|
13462 | 557 |
by Auto_tac; |
558 |
qed "real_minus_le"; |
|
10722 | 559 |
|
560 |
Goal "(x = - y) = (y = - (x::real))"; |
|
561 |
by Auto_tac; |
|
562 |
qed "real_equation_minus"; |
|
563 |
||
564 |
Goal "(- x = y) = (- (y::real) = x)"; |
|
565 |
by Auto_tac; |
|
566 |
qed "real_minus_equation"; |
|
567 |
||
568 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
569 |
Goal "(x + - a = (0::real)) = (x=a)"; |
10722 | 570 |
by (arith_tac 1); |
571 |
qed "real_add_minus_iff"; |
|
572 |
Addsimps [real_add_minus_iff]; |
|
573 |
||
574 |
Goal "(-b = -a) = (b = (a::real))"; |
|
575 |
by (arith_tac 1); |
|
576 |
qed "real_minus_eq_cancel"; |
|
577 |
Addsimps [real_minus_eq_cancel]; |
|
578 |
||
579 |
||
580 |
(*Distributive laws for literals*) |
|
581 |
Addsimps (map (inst "w" "number_of ?v") |
|
13462 | 582 |
[real_add_mult_distrib, real_add_mult_distrib2, |
583 |
real_diff_mult_distrib, real_diff_mult_distrib2]); |
|
10722 | 584 |
|
13462 | 585 |
Addsimps (map (inst "x" "number_of ?v") |
586 |
[real_less_minus, real_le_minus, real_equation_minus]); |
|
587 |
Addsimps (map (inst "y" "number_of ?v") |
|
588 |
[real_minus_less, real_minus_le, real_minus_equation]); |
|
10722 | 589 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
590 |
(*Equations and inequations involving 1*) |
13462 | 591 |
Addsimps (map (simplify (simpset()) o inst "x" "1") |
592 |
[real_less_minus, real_le_minus, real_equation_minus]); |
|
593 |
Addsimps (map (simplify (simpset()) o inst "y" "1") |
|
594 |
[real_minus_less, real_minus_le, real_minus_equation]); |
|
10722 | 595 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
596 |
(*** Simprules combining x+y and 0 ***) |
10722 | 597 |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
598 |
Goal "(x+y = (0::real)) = (y = -x)"; |
13462 | 599 |
by Auto_tac; |
10722 | 600 |
qed "real_add_eq_0_iff"; |
601 |
AddIffs [real_add_eq_0_iff]; |
|
602 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
603 |
Goal "(x+y < (0::real)) = (y < -x)"; |
13462 | 604 |
by Auto_tac; |
10722 | 605 |
qed "real_add_less_0_iff"; |
606 |
AddIffs [real_add_less_0_iff]; |
|
607 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
608 |
Goal "((0::real) < x+y) = (-x < y)"; |
13462 | 609 |
by Auto_tac; |
10722 | 610 |
qed "real_0_less_add_iff"; |
611 |
AddIffs [real_0_less_add_iff]; |
|
612 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
613 |
Goal "(x+y <= (0::real)) = (y <= -x)"; |
13462 | 614 |
by Auto_tac; |
10722 | 615 |
qed "real_add_le_0_iff"; |
616 |
AddIffs [real_add_le_0_iff]; |
|
617 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
618 |
Goal "((0::real) <= x+y) = (-x <= y)"; |
13462 | 619 |
by Auto_tac; |
10722 | 620 |
qed "real_0_le_add_iff"; |
621 |
AddIffs [real_0_le_add_iff]; |
|
622 |
||
623 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
624 |
(** Simprules combining x-y and 0; see also real_less_iff_diff_less_0, etc., |
10722 | 625 |
in RealBin |
626 |
**) |
|
627 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
628 |
Goal "((0::real) < x-y) = (y < x)"; |
13462 | 629 |
by Auto_tac; |
10722 | 630 |
qed "real_0_less_diff_iff"; |
631 |
AddIffs [real_0_less_diff_iff]; |
|
632 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
633 |
Goal "((0::real) <= x-y) = (y <= x)"; |
13462 | 634 |
by Auto_tac; |
10722 | 635 |
qed "real_0_le_diff_iff"; |
636 |
AddIffs [real_0_le_diff_iff]; |
|
637 |
||
638 |
(* |
|
10752
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
639 |
FIXME: we should have this, as for type int, but many proofs would break. |
c4f1bf2acf4c
tidying, and separation of HOL-Hyperreal from HOL-Real
paulson
parents:
10722
diff
changeset
|
640 |
It replaces x+-y by x-y. |
10722 | 641 |
Addsimps [symmetric real_diff_def]; |
642 |
*) |
|
643 |
||
644 |
Goal "-(x-y) = y - (x::real)"; |
|
645 |
by (arith_tac 1); |
|
646 |
qed "real_minus_diff_eq"; |
|
647 |
Addsimps [real_minus_diff_eq]; |
|
648 |
||
649 |
||
650 |
(*** Density of the Reals ***) |
|
651 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
652 |
Goal "x < y ==> x < (x+y) / (2::real)"; |
10722 | 653 |
by Auto_tac; |
654 |
qed "real_less_half_sum"; |
|
655 |
||
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
656 |
Goal "x < y ==> (x+y)/(2::real) < y"; |
10722 | 657 |
by Auto_tac; |
658 |
qed "real_gt_half_sum"; |
|
659 |
||
660 |
Goal "x < y ==> EX r::real. x < r & r < y"; |
|
661 |
by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1); |
|
662 |
qed "real_dense"; |
|
663 |
||
664 |
||
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
665 |
(*Replaces "inverse #nn" by 1/#nn *) |
10722 | 666 |
Addsimps [inst "x" "number_of ?w" real_inverse_eq_divide]; |
667 |
||
668 |