author | wenzelm |
Tue, 31 Jul 2007 00:56:29 +0200 | |
changeset 24076 | ae946f751c44 |
parent 24075 | 366d4d234814 |
child 24286 | 7619080e49f0 |
permissions | -rw-r--r-- |
23462 | 1 |
(* Title: HOL/Arith_Tools.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Author: Amine Chaieb, TU Muenchen |
|
5 |
*) |
|
6 |
||
7 |
header {* Setup of arithmetic tools *} |
|
8 |
||
9 |
theory Arith_Tools |
|
23465 | 10 |
imports Groebner_Basis Dense_Linear_Order |
23462 | 11 |
uses |
12 |
"~~/src/Provers/Arith/cancel_numeral_factor.ML" |
|
13 |
"~~/src/Provers/Arith/extract_common_term.ML" |
|
14 |
"int_factor_simprocs.ML" |
|
15 |
"nat_simprocs.ML" |
|
16 |
begin |
|
17 |
||
18 |
subsection {* Simprocs for the Naturals *} |
|
19 |
||
24075 | 20 |
declaration {* K nat_simprocs_setup *} |
23462 | 21 |
|
22 |
subsubsection{*For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}*} |
|
23 |
||
24 |
text{*Where K above is a literal*} |
|
25 |
||
26 |
lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)" |
|
27 |
by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split) |
|
28 |
||
29 |
text {*Now just instantiating @{text n} to @{text "number_of v"} does |
|
30 |
the right simplification, but with some redundant inequality |
|
31 |
tests.*} |
|
32 |
lemma neg_number_of_pred_iff_0: |
|
33 |
"neg (number_of (Numeral.pred v)::int) = (number_of v = (0::nat))" |
|
34 |
apply (subgoal_tac "neg (number_of (Numeral.pred v)) = (number_of v < Suc 0) ") |
|
35 |
apply (simp only: less_Suc_eq_le le_0_eq) |
|
36 |
apply (subst less_number_of_Suc, simp) |
|
37 |
done |
|
38 |
||
39 |
text{*No longer required as a simprule because of the @{text inverse_fold} |
|
40 |
simproc*} |
|
41 |
lemma Suc_diff_number_of: |
|
42 |
"neg (number_of (uminus v)::int) ==> |
|
43 |
Suc m - (number_of v) = m - (number_of (Numeral.pred v))" |
|
44 |
apply (subst Suc_diff_eq_diff_pred) |
|
45 |
apply simp |
|
46 |
apply (simp del: nat_numeral_1_eq_1) |
|
47 |
apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric] |
|
48 |
neg_number_of_pred_iff_0) |
|
49 |
done |
|
50 |
||
51 |
lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n" |
|
52 |
by (simp add: numerals split add: nat_diff_split) |
|
53 |
||
54 |
||
55 |
subsubsection{*For @{term nat_case} and @{term nat_rec}*} |
|
56 |
||
57 |
lemma nat_case_number_of [simp]: |
|
58 |
"nat_case a f (number_of v) = |
|
59 |
(let pv = number_of (Numeral.pred v) in |
|
60 |
if neg pv then a else f (nat pv))" |
|
61 |
by (simp split add: nat.split add: Let_def neg_number_of_pred_iff_0) |
|
62 |
||
63 |
lemma nat_case_add_eq_if [simp]: |
|
64 |
"nat_case a f ((number_of v) + n) = |
|
65 |
(let pv = number_of (Numeral.pred v) in |
|
66 |
if neg pv then nat_case a f n else f (nat pv + n))" |
|
67 |
apply (subst add_eq_if) |
|
68 |
apply (simp split add: nat.split |
|
69 |
del: nat_numeral_1_eq_1 |
|
70 |
add: numeral_1_eq_Suc_0 [symmetric] Let_def |
|
71 |
neg_imp_number_of_eq_0 neg_number_of_pred_iff_0) |
|
72 |
done |
|
73 |
||
74 |
lemma nat_rec_number_of [simp]: |
|
75 |
"nat_rec a f (number_of v) = |
|
76 |
(let pv = number_of (Numeral.pred v) in |
|
77 |
if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))" |
|
78 |
apply (case_tac " (number_of v) ::nat") |
|
79 |
apply (simp_all (no_asm_simp) add: Let_def neg_number_of_pred_iff_0) |
|
80 |
apply (simp split add: split_if_asm) |
|
81 |
done |
|
82 |
||
83 |
lemma nat_rec_add_eq_if [simp]: |
|
84 |
"nat_rec a f (number_of v + n) = |
|
85 |
(let pv = number_of (Numeral.pred v) in |
|
86 |
if neg pv then nat_rec a f n |
|
87 |
else f (nat pv + n) (nat_rec a f (nat pv + n)))" |
|
88 |
apply (subst add_eq_if) |
|
89 |
apply (simp split add: nat.split |
|
90 |
del: nat_numeral_1_eq_1 |
|
91 |
add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0 |
|
92 |
neg_number_of_pred_iff_0) |
|
93 |
done |
|
94 |
||
95 |
||
96 |
subsubsection{*Various Other Lemmas*} |
|
97 |
||
98 |
text {*Evens and Odds, for Mutilated Chess Board*} |
|
99 |
||
100 |
text{*Lemmas for specialist use, NOT as default simprules*} |
|
101 |
lemma nat_mult_2: "2 * z = (z+z::nat)" |
|
102 |
proof - |
|
103 |
have "2*z = (1 + 1)*z" by simp |
|
104 |
also have "... = z+z" by (simp add: left_distrib) |
|
105 |
finally show ?thesis . |
|
106 |
qed |
|
107 |
||
108 |
lemma nat_mult_2_right: "z * 2 = (z+z::nat)" |
|
109 |
by (subst mult_commute, rule nat_mult_2) |
|
110 |
||
111 |
text{*Case analysis on @{term "n<2"}*} |
|
112 |
lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0" |
|
113 |
by arith |
|
114 |
||
115 |
lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)" |
|
116 |
by arith |
|
117 |
||
118 |
lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)" |
|
119 |
by (simp add: nat_mult_2 [symmetric]) |
|
120 |
||
121 |
lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2" |
|
122 |
apply (subgoal_tac "m mod 2 < 2") |
|
123 |
apply (erule less_2_cases [THEN disjE]) |
|
124 |
apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1) |
|
125 |
done |
|
126 |
||
127 |
lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)" |
|
128 |
apply (subgoal_tac "m mod 2 < 2") |
|
129 |
apply (force simp del: mod_less_divisor, simp) |
|
130 |
done |
|
131 |
||
132 |
text{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*} |
|
133 |
||
134 |
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" |
|
135 |
by simp |
|
136 |
||
137 |
lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)" |
|
138 |
by simp |
|
139 |
||
140 |
text{*Can be used to eliminate long strings of Sucs, but not by default*} |
|
141 |
lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n" |
|
142 |
by simp |
|
143 |
||
144 |
||
145 |
text{*These lemmas collapse some needless occurrences of Suc: |
|
146 |
at least three Sucs, since two and fewer are rewritten back to Suc again! |
|
147 |
We already have some rules to simplify operands smaller than 3.*} |
|
148 |
||
149 |
lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)" |
|
150 |
by (simp add: Suc3_eq_add_3) |
|
151 |
||
152 |
lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)" |
|
153 |
by (simp add: Suc3_eq_add_3) |
|
154 |
||
155 |
lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n" |
|
156 |
by (simp add: Suc3_eq_add_3) |
|
157 |
||
158 |
lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" |
|
159 |
by (simp add: Suc3_eq_add_3) |
|
160 |
||
161 |
lemmas Suc_div_eq_add3_div_number_of = |
|
162 |
Suc_div_eq_add3_div [of _ "number_of v", standard] |
|
163 |
declare Suc_div_eq_add3_div_number_of [simp] |
|
164 |
||
165 |
lemmas Suc_mod_eq_add3_mod_number_of = |
|
166 |
Suc_mod_eq_add3_mod [of _ "number_of v", standard] |
|
167 |
declare Suc_mod_eq_add3_mod_number_of [simp] |
|
168 |
||
169 |
||
170 |
subsubsection{*Special Simplification for Constants*} |
|
171 |
||
172 |
text{*These belong here, late in the development of HOL, to prevent their |
|
173 |
interfering with proofs of abstract properties of instances of the function |
|
174 |
@{term number_of}*} |
|
175 |
||
176 |
text{*These distributive laws move literals inside sums and differences.*} |
|
177 |
lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard] |
|
178 |
declare left_distrib_number_of [simp] |
|
179 |
||
180 |
lemmas right_distrib_number_of = right_distrib [of "number_of v", standard] |
|
181 |
declare right_distrib_number_of [simp] |
|
182 |
||
183 |
||
184 |
lemmas left_diff_distrib_number_of = |
|
185 |
left_diff_distrib [of _ _ "number_of v", standard] |
|
186 |
declare left_diff_distrib_number_of [simp] |
|
187 |
||
188 |
lemmas right_diff_distrib_number_of = |
|
189 |
right_diff_distrib [of "number_of v", standard] |
|
190 |
declare right_diff_distrib_number_of [simp] |
|
191 |
||
192 |
||
193 |
text{*These are actually for fields, like real: but where else to put them?*} |
|
194 |
lemmas zero_less_divide_iff_number_of = |
|
195 |
zero_less_divide_iff [of "number_of w", standard] |
|
196 |
declare zero_less_divide_iff_number_of [simp] |
|
197 |
||
198 |
lemmas divide_less_0_iff_number_of = |
|
199 |
divide_less_0_iff [of "number_of w", standard] |
|
200 |
declare divide_less_0_iff_number_of [simp] |
|
201 |
||
202 |
lemmas zero_le_divide_iff_number_of = |
|
203 |
zero_le_divide_iff [of "number_of w", standard] |
|
204 |
declare zero_le_divide_iff_number_of [simp] |
|
205 |
||
206 |
lemmas divide_le_0_iff_number_of = |
|
207 |
divide_le_0_iff [of "number_of w", standard] |
|
208 |
declare divide_le_0_iff_number_of [simp] |
|
209 |
||
210 |
||
211 |
(**** |
|
212 |
IF times_divide_eq_right and times_divide_eq_left are removed as simprules, |
|
213 |
then these special-case declarations may be useful. |
|
214 |
||
215 |
text{*These simprules move numerals into numerators and denominators.*} |
|
216 |
lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)" |
|
217 |
by (simp add: times_divide_eq) |
|
218 |
||
219 |
lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)" |
|
220 |
by (simp add: times_divide_eq) |
|
221 |
||
222 |
lemmas times_divide_eq_right_number_of = |
|
223 |
times_divide_eq_right [of "number_of w", standard] |
|
224 |
declare times_divide_eq_right_number_of [simp] |
|
225 |
||
226 |
lemmas times_divide_eq_right_number_of = |
|
227 |
times_divide_eq_right [of _ _ "number_of w", standard] |
|
228 |
declare times_divide_eq_right_number_of [simp] |
|
229 |
||
230 |
lemmas times_divide_eq_left_number_of = |
|
231 |
times_divide_eq_left [of _ "number_of w", standard] |
|
232 |
declare times_divide_eq_left_number_of [simp] |
|
233 |
||
234 |
lemmas times_divide_eq_left_number_of = |
|
235 |
times_divide_eq_left [of _ _ "number_of w", standard] |
|
236 |
declare times_divide_eq_left_number_of [simp] |
|
237 |
||
238 |
****) |
|
239 |
||
240 |
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks |
|
241 |
strange, but then other simprocs simplify the quotient.*} |
|
242 |
||
243 |
lemmas inverse_eq_divide_number_of = |
|
244 |
inverse_eq_divide [of "number_of w", standard] |
|
245 |
declare inverse_eq_divide_number_of [simp] |
|
246 |
||
247 |
||
248 |
text {*These laws simplify inequalities, moving unary minus from a term |
|
249 |
into the literal.*} |
|
250 |
lemmas less_minus_iff_number_of = |
|
251 |
less_minus_iff [of "number_of v", standard] |
|
252 |
declare less_minus_iff_number_of [simp] |
|
253 |
||
254 |
lemmas le_minus_iff_number_of = |
|
255 |
le_minus_iff [of "number_of v", standard] |
|
256 |
declare le_minus_iff_number_of [simp] |
|
257 |
||
258 |
lemmas equation_minus_iff_number_of = |
|
259 |
equation_minus_iff [of "number_of v", standard] |
|
260 |
declare equation_minus_iff_number_of [simp] |
|
261 |
||
262 |
||
263 |
lemmas minus_less_iff_number_of = |
|
264 |
minus_less_iff [of _ "number_of v", standard] |
|
265 |
declare minus_less_iff_number_of [simp] |
|
266 |
||
267 |
lemmas minus_le_iff_number_of = |
|
268 |
minus_le_iff [of _ "number_of v", standard] |
|
269 |
declare minus_le_iff_number_of [simp] |
|
270 |
||
271 |
lemmas minus_equation_iff_number_of = |
|
272 |
minus_equation_iff [of _ "number_of v", standard] |
|
273 |
declare minus_equation_iff_number_of [simp] |
|
274 |
||
275 |
||
276 |
text{*To Simplify Inequalities Where One Side is the Constant 1*} |
|
277 |
||
278 |
lemma less_minus_iff_1 [simp]: |
|
279 |
fixes b::"'b::{ordered_idom,number_ring}" |
|
280 |
shows "(1 < - b) = (b < -1)" |
|
281 |
by auto |
|
282 |
||
283 |
lemma le_minus_iff_1 [simp]: |
|
284 |
fixes b::"'b::{ordered_idom,number_ring}" |
|
285 |
shows "(1 \<le> - b) = (b \<le> -1)" |
|
286 |
by auto |
|
287 |
||
288 |
lemma equation_minus_iff_1 [simp]: |
|
289 |
fixes b::"'b::number_ring" |
|
290 |
shows "(1 = - b) = (b = -1)" |
|
291 |
by (subst equation_minus_iff, auto) |
|
292 |
||
293 |
lemma minus_less_iff_1 [simp]: |
|
294 |
fixes a::"'b::{ordered_idom,number_ring}" |
|
295 |
shows "(- a < 1) = (-1 < a)" |
|
296 |
by auto |
|
297 |
||
298 |
lemma minus_le_iff_1 [simp]: |
|
299 |
fixes a::"'b::{ordered_idom,number_ring}" |
|
300 |
shows "(- a \<le> 1) = (-1 \<le> a)" |
|
301 |
by auto |
|
302 |
||
303 |
lemma minus_equation_iff_1 [simp]: |
|
304 |
fixes a::"'b::number_ring" |
|
305 |
shows "(- a = 1) = (a = -1)" |
|
306 |
by (subst minus_equation_iff, auto) |
|
307 |
||
308 |
||
309 |
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *} |
|
310 |
||
311 |
lemmas mult_less_cancel_left_number_of = |
|
312 |
mult_less_cancel_left [of "number_of v", standard] |
|
313 |
declare mult_less_cancel_left_number_of [simp] |
|
314 |
||
315 |
lemmas mult_less_cancel_right_number_of = |
|
316 |
mult_less_cancel_right [of _ "number_of v", standard] |
|
317 |
declare mult_less_cancel_right_number_of [simp] |
|
318 |
||
319 |
lemmas mult_le_cancel_left_number_of = |
|
320 |
mult_le_cancel_left [of "number_of v", standard] |
|
321 |
declare mult_le_cancel_left_number_of [simp] |
|
322 |
||
323 |
lemmas mult_le_cancel_right_number_of = |
|
324 |
mult_le_cancel_right [of _ "number_of v", standard] |
|
325 |
declare mult_le_cancel_right_number_of [simp] |
|
326 |
||
327 |
||
328 |
text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *} |
|
329 |
||
330 |
lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard] |
|
331 |
declare le_divide_eq_number_of [simp] |
|
332 |
||
333 |
lemmas divide_le_eq_number_of = divide_le_eq [of _ "number_of w", standard] |
|
334 |
declare divide_le_eq_number_of [simp] |
|
335 |
||
336 |
lemmas less_divide_eq_number_of = less_divide_eq [of _ _ "number_of w", standard] |
|
337 |
declare less_divide_eq_number_of [simp] |
|
338 |
||
339 |
lemmas divide_less_eq_number_of = divide_less_eq [of _ "number_of w", standard] |
|
340 |
declare divide_less_eq_number_of [simp] |
|
341 |
||
342 |
lemmas eq_divide_eq_number_of = eq_divide_eq [of _ _ "number_of w", standard] |
|
343 |
declare eq_divide_eq_number_of [simp] |
|
344 |
||
345 |
lemmas divide_eq_eq_number_of = divide_eq_eq [of _ "number_of w", standard] |
|
346 |
declare divide_eq_eq_number_of [simp] |
|
347 |
||
348 |
||
349 |
||
350 |
subsubsection{*Optional Simplification Rules Involving Constants*} |
|
351 |
||
352 |
text{*Simplify quotients that are compared with a literal constant.*} |
|
353 |
||
354 |
lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard] |
|
355 |
lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard] |
|
356 |
lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard] |
|
357 |
lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard] |
|
358 |
lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard] |
|
359 |
lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard] |
|
360 |
||
361 |
||
362 |
text{*Not good as automatic simprules because they cause case splits.*} |
|
363 |
lemmas divide_const_simps = |
|
364 |
le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of |
|
365 |
divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of |
|
366 |
le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1 |
|
367 |
||
368 |
text{*Division By @{text "-1"}*} |
|
369 |
||
370 |
lemma divide_minus1 [simp]: |
|
371 |
"x/-1 = -(x::'a::{field,division_by_zero,number_ring})" |
|
372 |
by simp |
|
373 |
||
374 |
lemma minus1_divide [simp]: |
|
375 |
"-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)" |
|
376 |
by (simp add: divide_inverse inverse_minus_eq) |
|
377 |
||
378 |
lemma half_gt_zero_iff: |
|
379 |
"(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))" |
|
380 |
by auto |
|
381 |
||
382 |
lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, standard] |
|
383 |
declare half_gt_zero [simp] |
|
384 |
||
385 |
(* The following lemma should appear in Divides.thy, but there the proof |
|
386 |
doesn't work. *) |
|
387 |
||
388 |
lemma nat_dvd_not_less: |
|
389 |
"[| 0 < m; m < n |] ==> \<not> n dvd (m::nat)" |
|
390 |
by (unfold dvd_def) auto |
|
391 |
||
392 |
ML {* |
|
393 |
val divide_minus1 = @{thm divide_minus1}; |
|
394 |
val minus1_divide = @{thm minus1_divide}; |
|
395 |
*} |
|
396 |
||
397 |
||
398 |
subsection{* Groebner Bases for fields *} |
|
399 |
||
400 |
interpretation class_fieldgb: |
|
401 |
fieldgb["op +" "op *" "op ^" "0::'a::{field,recpower,number_ring}" "1" "op -" "uminus" "op /" "inverse"] apply (unfold_locales) by (simp_all add: divide_inverse) |
|
402 |
||
403 |
lemma divide_Numeral1: "(x::'a::{field,number_ring}) / Numeral1 = x" by simp |
|
404 |
lemma divide_Numeral0: "(x::'a::{field,number_ring, division_by_zero}) / Numeral0 = 0" |
|
405 |
by simp |
|
406 |
lemma mult_frac_frac: "((x::'a::{field,division_by_zero}) / y) * (z / w) = (x*z) / (y*w)" |
|
407 |
by simp |
|
408 |
lemma mult_frac_num: "((x::'a::{field, division_by_zero}) / y) * z = (x*z) / y" |
|
409 |
by simp |
|
410 |
lemma mult_num_frac: "((x::'a::{field, division_by_zero}) / y) * z = (x*z) / y" |
|
411 |
by simp |
|
412 |
||
413 |
lemma Numeral1_eq1_nat: "(1::nat) = Numeral1" by simp |
|
414 |
||
415 |
lemma add_frac_num: "y\<noteq> 0 \<Longrightarrow> (x::'a::{field, division_by_zero}) / y + z = (x + z*y) / y" |
|
416 |
by (simp add: add_divide_distrib) |
|
417 |
lemma add_num_frac: "y\<noteq> 0 \<Longrightarrow> z + (x::'a::{field, division_by_zero}) / y = (x + z*y) / y" |
|
418 |
by (simp add: add_divide_distrib) |
|
419 |
||
420 |
declaration{* |
|
421 |
let |
|
422 |
val zr = @{cpat "0"} |
|
423 |
val zT = ctyp_of_term zr |
|
424 |
val geq = @{cpat "op ="} |
|
425 |
val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd |
|
426 |
val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"} |
|
427 |
val add_frac_num = mk_meta_eq @{thm "add_frac_num"} |
|
428 |
val add_num_frac = mk_meta_eq @{thm "add_num_frac"} |
|
429 |
||
430 |
fun prove_nz ctxt = |
|
431 |
let val ss = local_simpset_of ctxt |
|
432 |
in fn T => fn t => |
|
433 |
let |
|
434 |
val z = instantiate_cterm ([(zT,T)],[]) zr |
|
435 |
val eq = instantiate_cterm ([(eqT,T)],[]) geq |
|
436 |
val th = Simplifier.rewrite (ss addsimps simp_thms) |
|
437 |
(Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"} |
|
438 |
(Thm.capply (Thm.capply eq t) z))) |
|
439 |
in equal_elim (symmetric th) TrueI |
|
440 |
end |
|
441 |
end |
|
442 |
||
443 |
fun proc ctxt phi ss ct = |
|
444 |
let |
|
445 |
val ((x,y),(w,z)) = |
|
446 |
(Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct |
|
447 |
val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] |
|
448 |
val T = ctyp_of_term x |
|
449 |
val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z] |
|
450 |
val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq |
|
451 |
in SOME (implies_elim (implies_elim th y_nz) z_nz) |
|
452 |
end |
|
453 |
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE |
|
454 |
||
455 |
fun proc2 ctxt phi ss ct = |
|
456 |
let |
|
457 |
val (l,r) = Thm.dest_binop ct |
|
458 |
val T = ctyp_of_term l |
|
459 |
in (case (term_of l, term_of r) of |
|
460 |
(Const(@{const_name "HOL.divide"},_)$_$_, _) => |
|
461 |
let val (x,y) = Thm.dest_binop l val z = r |
|
462 |
val _ = map (HOLogic.dest_number o term_of) [x,y,z] |
|
463 |
val ynz = prove_nz ctxt T y |
|
464 |
in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz) |
|
465 |
end |
|
466 |
| (_, Const (@{const_name "HOL.divide"},_)$_$_) => |
|
467 |
let val (x,y) = Thm.dest_binop r val z = l |
|
468 |
val _ = map (HOLogic.dest_number o term_of) [x,y,z] |
|
469 |
val ynz = prove_nz ctxt T y |
|
470 |
in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz) |
|
471 |
end |
|
472 |
| _ => NONE) |
|
473 |
end |
|
474 |
handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE |
|
475 |
||
476 |
fun is_number (Const(@{const_name "HOL.divide"},_)$a$b) = is_number a andalso is_number b |
|
477 |
| is_number t = can HOLogic.dest_number t |
|
478 |
||
479 |
val is_number = is_number o term_of |
|
480 |
||
481 |
fun proc3 phi ss ct = |
|
482 |
(case term_of ct of |
|
23881 | 483 |
Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ => |
23462 | 484 |
let |
485 |
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop |
|
486 |
val _ = map is_number [a,b,c] |
|
487 |
val T = ctyp_of_term c |
|
488 |
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"} |
|
489 |
in SOME (mk_meta_eq th) end |
|
23881 | 490 |
| Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ => |
23462 | 491 |
let |
492 |
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop |
|
493 |
val _ = map is_number [a,b,c] |
|
494 |
val T = ctyp_of_term c |
|
495 |
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"} |
|
496 |
in SOME (mk_meta_eq th) end |
|
497 |
| Const("op =",_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ => |
|
498 |
let |
|
499 |
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop |
|
500 |
val _ = map is_number [a,b,c] |
|
501 |
val T = ctyp_of_term c |
|
502 |
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"} |
|
503 |
in SOME (mk_meta_eq th) end |
|
23881 | 504 |
| Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) => |
23462 | 505 |
let |
506 |
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop |
|
507 |
val _ = map is_number [a,b,c] |
|
508 |
val T = ctyp_of_term c |
|
509 |
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"} |
|
510 |
in SOME (mk_meta_eq th) end |
|
23881 | 511 |
| Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) => |
23462 | 512 |
let |
513 |
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop |
|
514 |
val _ = map is_number [a,b,c] |
|
515 |
val T = ctyp_of_term c |
|
516 |
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"} |
|
517 |
in SOME (mk_meta_eq th) end |
|
518 |
| Const("op =",_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) => |
|
519 |
let |
|
520 |
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop |
|
521 |
val _ = map is_number [a,b,c] |
|
522 |
val T = ctyp_of_term c |
|
523 |
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "eq_divide_eq"} |
|
524 |
in SOME (mk_meta_eq th) end |
|
525 |
| _ => NONE) |
|
526 |
handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE |
|
527 |
||
528 |
fun add_frac_frac_simproc ctxt = |
|
529 |
make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], |
|
530 |
name = "add_frac_frac_simproc", |
|
531 |
proc = proc ctxt, identifier = []} |
|
532 |
||
533 |
fun add_frac_num_simproc ctxt = |
|
534 |
make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], |
|
535 |
name = "add_frac_num_simproc", |
|
536 |
proc = proc2 ctxt, identifier = []} |
|
537 |
||
538 |
val ord_frac_simproc = |
|
539 |
make_simproc |
|
540 |
{lhss = [@{cpat "(?a::(?'a::{field, ord}))/?b < ?c"}, |
|
541 |
@{cpat "(?a::(?'a::{field, ord}))/?b \<le> ?c"}, |
|
542 |
@{cpat "?c < (?a::(?'a::{field, ord}))/?b"}, |
|
543 |
@{cpat "?c \<le> (?a::(?'a::{field, ord}))/?b"}, |
|
544 |
@{cpat "?c = ((?a::(?'a::{field, ord}))/?b)"}, |
|
545 |
@{cpat "((?a::(?'a::{field, ord}))/ ?b) = ?c"}], |
|
546 |
name = "ord_frac_simproc", proc = proc3, identifier = []} |
|
547 |
||
548 |
val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of", |
|
549 |
"mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"] |
|
550 |
||
551 |
val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", |
|
552 |
"add_Suc", "add_number_of_left", "mult_number_of_left", |
|
553 |
"Suc_eq_add_numeral_1"])@ |
|
554 |
(map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"]) |
|
555 |
@ arith_simps@ nat_arith @ rel_simps |
|
556 |
val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, |
|
557 |
@{thm "divide_Numeral1"}, |
|
558 |
@{thm "Ring_and_Field.divide_zero"}, @{thm "divide_Numeral0"}, |
|
559 |
@{thm "divide_divide_eq_left"}, @{thm "mult_frac_frac"}, |
|
560 |
@{thm "mult_num_frac"}, @{thm "mult_frac_num"}, |
|
561 |
@{thm "mult_frac_frac"}, @{thm "times_divide_eq_right"}, |
|
562 |
@{thm "times_divide_eq_left"}, @{thm "divide_divide_eq_right"}, |
|
563 |
@{thm "diff_def"}, @{thm "minus_divide_left"}, |
|
564 |
@{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym] |
|
565 |
||
566 |
local |
|
567 |
open Conv |
|
568 |
in |
|
569 |
fun comp_conv ctxt = (Simplifier.rewrite |
|
570 |
(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} |
|
571 |
addsimps ths addsimps comp_arith addsimps simp_thms |
|
572 |
addsimprocs field_cancel_numeral_factors |
|
573 |
addsimprocs [add_frac_frac_simproc ctxt, add_frac_num_simproc ctxt, |
|
574 |
ord_frac_simproc] |
|
575 |
addcongs [@{thm "if_weak_cong"}])) |
|
576 |
then_conv (Simplifier.rewrite (HOL_basic_ss addsimps |
|
577 |
[@{thm numeral_1_eq_1},@{thm numeral_0_eq_0}] @ @{thms numerals(1-2)})) |
|
578 |
end |
|
579 |
||
580 |
fun numeral_is_const ct = |
|
581 |
case term_of ct of |
|
582 |
Const (@{const_name "HOL.divide"},_) $ a $ b => |
|
583 |
numeral_is_const (Thm.dest_arg1 ct) andalso numeral_is_const (Thm.dest_arg ct) |
|
584 |
| Const (@{const_name "HOL.uminus"},_)$t => numeral_is_const (Thm.dest_arg ct) |
|
585 |
| t => can HOLogic.dest_number t |
|
586 |
||
587 |
fun dest_const ct = case term_of ct of |
|
588 |
Const (@{const_name "HOL.divide"},_) $ a $ b=> |
|
589 |
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) |
|
590 |
| t => Rat.rat_of_int (snd (HOLogic.dest_number t)) |
|
591 |
||
592 |
fun mk_const phi cT x = |
|
593 |
let val (a, b) = Rat.quotient_of_rat x |
|
23572 | 594 |
in if b = 1 then Numeral.mk_cnumber cT a |
23462 | 595 |
else Thm.capply |
596 |
(Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) |
|
23572 | 597 |
(Numeral.mk_cnumber cT a)) |
598 |
(Numeral.mk_cnumber cT b) |
|
23462 | 599 |
end |
600 |
||
601 |
in |
|
602 |
NormalizerData.funs @{thm class_fieldgb.axioms} |
|
603 |
{is_const = K numeral_is_const, |
|
604 |
dest_const = K dest_const, |
|
605 |
mk_const = mk_const, |
|
606 |
conv = K comp_conv} |
|
607 |
end |
|
608 |
||
609 |
*} |
|
610 |
||
611 |
||
612 |
subsection {* Ferrante and Rackoff algorithm over ordered fields *} |
|
613 |
||
614 |
lemma neg_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x < 0) == (x > 0))" |
|
615 |
proof- |
|
616 |
assume H: "c < 0" |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
617 |
have "c*x < 0 = (0/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps) |
23462 | 618 |
also have "\<dots> = (0 < x)" by simp |
619 |
finally show "(c*x < 0) == (x > 0)" by simp |
|
620 |
qed |
|
621 |
||
622 |
lemma pos_prod_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x < 0) == (x < 0))" |
|
623 |
proof- |
|
624 |
assume H: "c > 0" |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
625 |
hence "c*x < 0 = (0/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps) |
23462 | 626 |
also have "\<dots> = (0 > x)" by simp |
627 |
finally show "(c*x < 0) == (x < 0)" by simp |
|
628 |
qed |
|
629 |
||
630 |
lemma neg_prod_sum_lt: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t< 0) == (x > (- 1/c)*t))" |
|
631 |
proof- |
|
632 |
assume H: "c < 0" |
|
633 |
have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
634 |
also have "\<dots> = (-t/c < x)" by (simp only: neg_divide_less_eq[OF H] ring_simps) |
23462 | 635 |
also have "\<dots> = ((- 1/c)*t < x)" by simp |
636 |
finally show "(c*x + t < 0) == (x > (- 1/c)*t)" by simp |
|
637 |
qed |
|
638 |
||
639 |
lemma pos_prod_sum_lt:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t < 0) == (x < (- 1/c)*t))" |
|
640 |
proof- |
|
641 |
assume H: "c > 0" |
|
642 |
have "c*x + t< 0 = (c*x < -t)" by (subst less_iff_diff_less_0 [of "c*x" "-t"], simp) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
643 |
also have "\<dots> = (-t/c > x)" by (simp only: pos_less_divide_eq[OF H] ring_simps) |
23462 | 644 |
also have "\<dots> = ((- 1/c)*t > x)" by simp |
645 |
finally show "(c*x + t < 0) == (x < (- 1/c)*t)" by simp |
|
646 |
qed |
|
647 |
||
648 |
lemma sum_lt:"((x::'a::pordered_ab_group_add) + t < 0) == (x < - t)" |
|
649 |
using less_diff_eq[where a= x and b=t and c=0] by simp |
|
650 |
||
651 |
lemma neg_prod_le:"(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x <= 0) == (x >= 0))" |
|
652 |
proof- |
|
653 |
assume H: "c < 0" |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
654 |
have "c*x <= 0 = (0/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps) |
23462 | 655 |
also have "\<dots> = (0 <= x)" by simp |
656 |
finally show "(c*x <= 0) == (x >= 0)" by simp |
|
657 |
qed |
|
658 |
||
659 |
lemma pos_prod_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x <= 0) == (x <= 0))" |
|
660 |
proof- |
|
661 |
assume H: "c > 0" |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
662 |
hence "c*x <= 0 = (0/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps) |
23462 | 663 |
also have "\<dots> = (0 >= x)" by simp |
664 |
finally show "(c*x <= 0) == (x <= 0)" by simp |
|
665 |
qed |
|
666 |
||
667 |
lemma neg_prod_sum_le: "(c\<Colon>'a\<Colon>ordered_field) < 0 \<Longrightarrow> ((c*x + t <= 0) == (x >= (- 1/c)*t))" |
|
668 |
proof- |
|
669 |
assume H: "c < 0" |
|
670 |
have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
671 |
also have "\<dots> = (-t/c <= x)" by (simp only: neg_divide_le_eq[OF H] ring_simps) |
23462 | 672 |
also have "\<dots> = ((- 1/c)*t <= x)" by simp |
673 |
finally show "(c*x + t <= 0) == (x >= (- 1/c)*t)" by simp |
|
674 |
qed |
|
675 |
||
676 |
lemma pos_prod_sum_le:"(c\<Colon>'a\<Colon>ordered_field) > 0 \<Longrightarrow> ((c*x + t <= 0) == (x <= (- 1/c)*t))" |
|
677 |
proof- |
|
678 |
assume H: "c > 0" |
|
679 |
have "c*x + t <= 0 = (c*x <= -t)" by (subst le_iff_diff_le_0 [of "c*x" "-t"], simp) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
680 |
also have "\<dots> = (-t/c >= x)" by (simp only: pos_le_divide_eq[OF H] ring_simps) |
23462 | 681 |
also have "\<dots> = ((- 1/c)*t >= x)" by simp |
682 |
finally show "(c*x + t <= 0) == (x <= (- 1/c)*t)" by simp |
|
683 |
qed |
|
684 |
||
685 |
lemma sum_le:"((x::'a::pordered_ab_group_add) + t <= 0) == (x <= - t)" |
|
686 |
using le_diff_eq[where a= x and b=t and c=0] by simp |
|
687 |
||
688 |
lemma nz_prod_eq:"(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x = 0) == (x = 0))" by simp |
|
689 |
lemma nz_prod_sum_eq: "(c\<Colon>'a\<Colon>ordered_field) \<noteq> 0 \<Longrightarrow> ((c*x + t = 0) == (x = (- 1/c)*t))" |
|
690 |
proof- |
|
691 |
assume H: "c \<noteq> 0" |
|
692 |
have "c*x + t = 0 = (c*x = -t)" by (subst eq_iff_diff_eq_0 [of "c*x" "-t"], simp) |
|
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23465
diff
changeset
|
693 |
also have "\<dots> = (x = -t/c)" by (simp only: nonzero_eq_divide_eq[OF H] ring_simps) |
23462 | 694 |
finally show "(c*x + t = 0) == (x = (- 1/c)*t)" by simp |
695 |
qed |
|
696 |
lemma sum_eq:"((x::'a::pordered_ab_group_add) + t = 0) == (x = - t)" |
|
697 |
using eq_diff_eq[where a= x and b=t and c=0] by simp |
|
698 |
||
699 |
||
23901 | 700 |
interpretation class_ordered_field_dense_linear_order: constr_dense_linear_order |
23462 | 701 |
["op <=" "op <" |
702 |
"\<lambda> x y. 1/2 * ((x::'a::{ordered_field,recpower,number_ring}) + y)"] |
|
23901 | 703 |
proof (unfold_locales, dlo, dlo, auto) |
23462 | 704 |
fix x y::'a assume lt: "x < y" |
705 |
from less_half_sum[OF lt] show "x < (x + y) /2" by simp |
|
706 |
next |
|
707 |
fix x y::'a assume lt: "x < y" |
|
708 |
from gt_half_sum[OF lt] show "(x + y) /2 < y" by simp |
|
709 |
qed |
|
710 |
||
711 |
declaration{* |
|
712 |
let |
|
713 |
fun earlier [] x y = false |
|
714 |
| earlier (h::t) x y = |
|
715 |
if h aconvc y then false else if h aconvc x then true else earlier t x y; |
|
716 |
||
717 |
fun dest_frac ct = case term_of ct of |
|
718 |
Const (@{const_name "HOL.divide"},_) $ a $ b=> |
|
719 |
Rat.rat_of_quotient (snd (HOLogic.dest_number a), snd (HOLogic.dest_number b)) |
|
720 |
| t => Rat.rat_of_int (snd (HOLogic.dest_number t)) |
|
721 |
||
722 |
fun mk_frac phi cT x = |
|
723 |
let val (a, b) = Rat.quotient_of_rat x |
|
23572 | 724 |
in if b = 1 then Numeral.mk_cnumber cT a |
23462 | 725 |
else Thm.capply |
726 |
(Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"}) |
|
23572 | 727 |
(Numeral.mk_cnumber cT a)) |
728 |
(Numeral.mk_cnumber cT b) |
|
23462 | 729 |
end |
730 |
||
731 |
fun whatis x ct = case term_of ct of |
|
732 |
Const(@{const_name "HOL.plus"}, _)$(Const(@{const_name "HOL.times"},_)$_$y)$_ => |
|
733 |
if y aconv term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct]) |
|
734 |
else ("Nox",[]) |
|
735 |
| Const(@{const_name "HOL.plus"}, _)$y$_ => |
|
736 |
if y aconv term_of x then ("x+t",[Thm.dest_arg ct]) |
|
737 |
else ("Nox",[]) |
|
738 |
| Const(@{const_name "HOL.times"}, _)$_$y => |
|
739 |
if y aconv term_of x then ("c*x",[Thm.dest_arg1 ct]) |
|
740 |
else ("Nox",[]) |
|
741 |
| t => if t aconv term_of x then ("x",[]) else ("Nox",[]); |
|
742 |
||
743 |
fun xnormalize_conv ctxt [] ct = reflexive ct |
|
744 |
| xnormalize_conv ctxt (vs as (x::_)) ct = |
|
745 |
case term_of ct of |
|
23881 | 746 |
Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) => |
23462 | 747 |
(case whatis x (Thm.dest_arg1 ct) of |
748 |
("c*x+t",[c,t]) => |
|
749 |
let |
|
750 |
val cr = dest_frac c |
|
751 |
val clt = Thm.dest_fun2 ct |
|
752 |
val cz = Thm.dest_arg ct |
|
753 |
val neg = cr </ Rat.zero |
|
754 |
val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
755 |
(Thm.capply @{cterm "Trueprop"} |
|
756 |
(if neg then Thm.capply (Thm.capply clt c) cz |
|
757 |
else Thm.capply (Thm.capply clt cz) c)) |
|
758 |
val cth = equal_elim (symmetric cthp) TrueI |
|
759 |
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t]) |
|
760 |
(if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth |
|
761 |
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
762 |
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
763 |
in rth end |
|
764 |
| ("x+t",[t]) => |
|
765 |
let |
|
766 |
val T = ctyp_of_term x |
|
767 |
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_lt"} |
|
768 |
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
769 |
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
770 |
in rth end |
|
771 |
| ("c*x",[c]) => |
|
772 |
let |
|
773 |
val cr = dest_frac c |
|
774 |
val clt = Thm.dest_fun2 ct |
|
775 |
val cz = Thm.dest_arg ct |
|
776 |
val neg = cr </ Rat.zero |
|
777 |
val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
778 |
(Thm.capply @{cterm "Trueprop"} |
|
779 |
(if neg then Thm.capply (Thm.capply clt c) cz |
|
780 |
else Thm.capply (Thm.capply clt cz) c)) |
|
781 |
val cth = equal_elim (symmetric cthp) TrueI |
|
782 |
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) |
|
783 |
(if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth |
|
784 |
val rth = th |
|
785 |
in rth end |
|
786 |
| _ => reflexive ct) |
|
787 |
||
788 |
||
23881 | 789 |
| Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) => |
23462 | 790 |
(case whatis x (Thm.dest_arg1 ct) of |
791 |
("c*x+t",[c,t]) => |
|
792 |
let |
|
793 |
val T = ctyp_of_term x |
|
794 |
val cr = dest_frac c |
|
795 |
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"} |
|
796 |
val cz = Thm.dest_arg ct |
|
797 |
val neg = cr </ Rat.zero |
|
798 |
val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
799 |
(Thm.capply @{cterm "Trueprop"} |
|
800 |
(if neg then Thm.capply (Thm.capply clt c) cz |
|
801 |
else Thm.capply (Thm.capply clt cz) c)) |
|
802 |
val cth = equal_elim (symmetric cthp) TrueI |
|
803 |
val th = implies_elim (instantiate' [SOME T] (map SOME [c,x,t]) |
|
804 |
(if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth |
|
805 |
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
806 |
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
807 |
in rth end |
|
808 |
| ("x+t",[t]) => |
|
809 |
let |
|
810 |
val T = ctyp_of_term x |
|
811 |
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_le"} |
|
812 |
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
813 |
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
814 |
in rth end |
|
815 |
| ("c*x",[c]) => |
|
816 |
let |
|
817 |
val T = ctyp_of_term x |
|
818 |
val cr = dest_frac c |
|
819 |
val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"} |
|
820 |
val cz = Thm.dest_arg ct |
|
821 |
val neg = cr </ Rat.zero |
|
822 |
val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
823 |
(Thm.capply @{cterm "Trueprop"} |
|
824 |
(if neg then Thm.capply (Thm.capply clt c) cz |
|
825 |
else Thm.capply (Thm.capply clt cz) c)) |
|
826 |
val cth = equal_elim (symmetric cthp) TrueI |
|
827 |
val th = implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x]) |
|
828 |
(if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth |
|
829 |
val rth = th |
|
830 |
in rth end |
|
831 |
| _ => reflexive ct) |
|
832 |
||
833 |
| Const("op =",_)$_$Const(@{const_name "HOL.zero"},_) => |
|
834 |
(case whatis x (Thm.dest_arg1 ct) of |
|
835 |
("c*x+t",[c,t]) => |
|
836 |
let |
|
837 |
val T = ctyp_of_term x |
|
838 |
val cr = dest_frac c |
|
839 |
val ceq = Thm.dest_fun2 ct |
|
840 |
val cz = Thm.dest_arg ct |
|
841 |
val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
842 |
(Thm.capply @{cterm "Trueprop"} |
|
843 |
(Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) |
|
844 |
val cth = equal_elim (symmetric cthp) TrueI |
|
845 |
val th = implies_elim |
|
846 |
(instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth |
|
847 |
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
848 |
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
849 |
in rth end |
|
850 |
| ("x+t",[t]) => |
|
851 |
let |
|
852 |
val T = ctyp_of_term x |
|
853 |
val th = instantiate' [SOME T] [SOME x, SOME t] @{thm "sum_eq"} |
|
854 |
val rth = Conv.fconv_rule (Conv.arg_conv (Conv.binop_conv |
|
855 |
(Normalizer.semiring_normalize_ord_conv ctxt (earlier vs)))) th |
|
856 |
in rth end |
|
857 |
| ("c*x",[c]) => |
|
858 |
let |
|
859 |
val T = ctyp_of_term x |
|
860 |
val cr = dest_frac c |
|
861 |
val ceq = Thm.dest_fun2 ct |
|
862 |
val cz = Thm.dest_arg ct |
|
863 |
val cthp = Simplifier.rewrite (local_simpset_of ctxt) |
|
864 |
(Thm.capply @{cterm "Trueprop"} |
|
865 |
(Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz))) |
|
866 |
val cth = equal_elim (symmetric cthp) TrueI |
|
867 |
val rth = implies_elim |
|
868 |
(instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth |
|
869 |
in rth end |
|
870 |
| _ => reflexive ct); |
|
871 |
||
872 |
local |
|
873 |
val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"} |
|
874 |
val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"} |
|
875 |
val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"} |
|
876 |
in |
|
877 |
fun field_isolate_conv phi ctxt vs ct = case term_of ct of |
|
23881 | 878 |
Const(@{const_name HOL.less},_)$a$b => |
23462 | 879 |
let val (ca,cb) = Thm.dest_binop ct |
880 |
val T = ctyp_of_term ca |
|
881 |
val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0 |
|
882 |
val nth = Conv.fconv_rule |
|
883 |
(Conv.arg_conv (Conv.arg1_conv |
|
884 |
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th |
|
885 |
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) |
|
886 |
in rth end |
|
23881 | 887 |
| Const(@{const_name HOL.less_eq},_)$a$b => |
23462 | 888 |
let val (ca,cb) = Thm.dest_binop ct |
889 |
val T = ctyp_of_term ca |
|
890 |
val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0 |
|
891 |
val nth = Conv.fconv_rule |
|
892 |
(Conv.arg_conv (Conv.arg1_conv |
|
893 |
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th |
|
894 |
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) |
|
895 |
in rth end |
|
896 |
||
897 |
| Const("op =",_)$a$b => |
|
898 |
let val (ca,cb) = Thm.dest_binop ct |
|
899 |
val T = ctyp_of_term ca |
|
900 |
val th = instantiate' [SOME T] [SOME ca, SOME cb] eq_iff_diff_eq_0 |
|
901 |
val nth = Conv.fconv_rule |
|
902 |
(Conv.arg_conv (Conv.arg1_conv |
|
903 |
(Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th |
|
904 |
val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth)) |
|
905 |
in rth end |
|
906 |
| @{term "Not"} $(Const("op =",_)$a$b) => Conv.arg_conv (field_isolate_conv phi ctxt vs) ct |
|
907 |
| _ => reflexive ct |
|
908 |
end; |
|
909 |
||
910 |
fun classfield_whatis phi = |
|
911 |
let |
|
912 |
fun h x t = |
|
913 |
case term_of t of |
|
914 |
Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq |
|
915 |
else Ferrante_Rackoff_Data.Nox |
|
916 |
| @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq |
|
917 |
else Ferrante_Rackoff_Data.Nox |
|
23881 | 918 |
| Const(@{const_name HOL.less},_)$y$z => |
23462 | 919 |
if term_of x aconv y then Ferrante_Rackoff_Data.Lt |
920 |
else if term_of x aconv z then Ferrante_Rackoff_Data.Gt |
|
921 |
else Ferrante_Rackoff_Data.Nox |
|
23881 | 922 |
| Const (@{const_name HOL.less_eq},_)$y$z => |
23462 | 923 |
if term_of x aconv y then Ferrante_Rackoff_Data.Le |
924 |
else if term_of x aconv z then Ferrante_Rackoff_Data.Ge |
|
925 |
else Ferrante_Rackoff_Data.Nox |
|
926 |
| _ => Ferrante_Rackoff_Data.Nox |
|
927 |
in h end; |
|
928 |
fun class_field_ss phi = |
|
929 |
HOL_basic_ss addsimps ([@{thm "linorder_not_less"}, @{thm "linorder_not_le"}]) |
|
930 |
addsplits [@{thm "abs_split"},@{thm "split_max"}, @{thm "split_min"}] |
|
931 |
||
932 |
in |
|
933 |
Ferrante_Rackoff_Data.funs @{thm "class_ordered_field_dense_linear_order.ferrack_axiom"} |
|
934 |
{isolate_conv = field_isolate_conv, whatis = classfield_whatis, simpset = class_field_ss} |
|
935 |
end |
|
936 |
*} |
|
937 |
||
938 |
end |