author | paulson |
Fri, 02 Nov 2001 17:55:24 +0100 | |
changeset 12018 | ec054019c910 |
parent 11704 | 3c50a2cd6f00 |
child 13462 | 56610e2ba220 |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title: HOL/Hyperreal/hypreal_arith.ML |
2 |
ID: $Id$ |
|
3 |
Author: Tobias Nipkow, TU Muenchen |
|
4 |
Copyright 1999 TU Muenchen |
|
5 |
||
6 |
Instantiation of the generic linear arithmetic package for type hypreal. |
|
7 |
*) |
|
8 |
||
9 |
local |
|
10 |
||
11 |
(* reduce contradictory <= to False *) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
12 |
val add_rules = |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
13 |
[order_less_irrefl, hypreal_numeral_0_eq_0, hypreal_numeral_1_eq_1, |
10751 | 14 |
add_hypreal_number_of, minus_hypreal_number_of, diff_hypreal_number_of, |
15 |
mult_hypreal_number_of, eq_hypreal_number_of, less_hypreal_number_of, |
|
16 |
le_hypreal_number_of_eq_not_less, hypreal_diff_def, |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
17 |
hypreal_minus_add_distrib, hypreal_minus_minus, hypreal_mult_assoc, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
18 |
hypreal_minus_zero, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
19 |
hypreal_add_zero_left, hypreal_add_zero_right, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
20 |
hypreal_add_minus, hypreal_add_minus_left, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
21 |
hypreal_mult_0, hypreal_mult_0_right, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
22 |
hypreal_mult_1, hypreal_mult_1_right, |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
23 |
hypreal_mult_minus_1, hypreal_mult_minus_1_right]; |
10751 | 24 |
|
25 |
val simprocs = [Hyperreal_Times_Assoc.conv, |
|
26 |
Hyperreal_Numeral_Simprocs.combine_numerals]@ |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
27 |
Hyperreal_Numeral_Simprocs.cancel_numerals @ |
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
28 |
Hyperreal_Numeral_Simprocs.eval_numerals; |
10751 | 29 |
|
30 |
val mono_ss = simpset() addsimps |
|
31 |
[hypreal_add_le_mono,hypreal_add_less_mono, |
|
32 |
hypreal_add_less_le_mono,hypreal_add_le_less_mono]; |
|
33 |
||
34 |
val add_mono_thms_hypreal = |
|
35 |
map (fn s => prove_goal (the_context ()) s |
|
36 |
(fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) |
|
37 |
["(i <= j) & (k <= l) ==> i + k <= j + (l::hypreal)", |
|
38 |
"(i = j) & (k <= l) ==> i + k <= j + (l::hypreal)", |
|
39 |
"(i <= j) & (k = l) ==> i + k <= j + (l::hypreal)", |
|
40 |
"(i = j) & (k = l) ==> i + k = j + (l::hypreal)", |
|
41 |
"(i < j) & (k = l) ==> i + k < j + (l::hypreal)", |
|
42 |
"(i = j) & (k < l) ==> i + k < j + (l::hypreal)", |
|
43 |
"(i < j) & (k <= l) ==> i + k < j + (l::hypreal)", |
|
44 |
"(i <= j) & (k < l) ==> i + k < j + (l::hypreal)", |
|
45 |
"(i < j) & (k < l) ==> i + k < j + (l::hypreal)"]; |
|
46 |
||
47 |
val hypreal_arith_simproc_pats = |
|
48 |
map (fn s => Thm.read_cterm (Theory.sign_of (the_context ())) |
|
49 |
(s, HOLogic.boolT)) |
|
50 |
["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]; |
|
51 |
||
52 |
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
|
53 |
||
54 |
val hypreal_mult_mono_thms = |
|
55 |
[(rotate_prems 1 hypreal_mult_less_mono2, |
|
56 |
cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), |
|
57 |
(hypreal_mult_le_mono2, |
|
58 |
cvar(hypreal_mult_le_mono2, hd(tl(prems_of hypreal_mult_le_mono2))))] |
|
59 |
||
60 |
in |
|
61 |
||
62 |
val fast_hypreal_arith_simproc = mk_simproc |
|
63 |
"fast_hypreal_arith" hypreal_arith_simproc_pats Fast_Arith.lin_arith_prover; |
|
64 |
||
65 |
val hypreal_arith_setup = |
|
66 |
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
|
67 |
{add_mono_thms = add_mono_thms @ add_mono_thms_hypreal, |
|
68 |
mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, |
|
69 |
inj_thms = inj_thms, (*FIXME: add hypreal*) |
|
70 |
lessD = lessD, (*We don't change LA_Data_Ref.lessD because the hypreal ordering is dense!*) |
|
12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset
|
71 |
simpset = simpset addsimps add_rules addsimprocs simprocs}), |
10751 | 72 |
arith_discrete ("HyperDef.hypreal",false), |
73 |
Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; |
|
74 |
||
75 |
end; |
|
76 |
||
77 |
||
78 |
(* Some test data [omitting examples that assume the ordering to be discrete!] |
|
79 |
Goal "!!a::hypreal. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"; |
|
80 |
by (fast_arith_tac 1); |
|
81 |
qed ""; |
|
82 |
||
83 |
Goal "!!a::hypreal. [| a <= b; b+b <= c |] ==> a+a <= c"; |
|
84 |
by (fast_arith_tac 1); |
|
85 |
qed ""; |
|
86 |
||
87 |
Goal "!!a::hypreal. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"; |
|
88 |
by (fast_arith_tac 1); |
|
89 |
qed ""; |
|
90 |
||
91 |
Goal "!!a::hypreal. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"; |
|
92 |
by (arith_tac 1); |
|
93 |
qed ""; |
|
94 |
||
95 |
Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
96 |
\ ==> a <= l"; |
|
97 |
by (fast_arith_tac 1); |
|
98 |
qed ""; |
|
99 |
||
100 |
Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
101 |
\ ==> a+a+a+a <= l+l+l+l"; |
|
102 |
by (fast_arith_tac 1); |
|
103 |
qed ""; |
|
104 |
||
105 |
Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
106 |
\ ==> a+a+a+a+a <= l+l+l+l+i"; |
|
107 |
by (fast_arith_tac 1); |
|
108 |
qed ""; |
|
109 |
||
110 |
Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
111 |
\ ==> a+a+a+a+a+a <= l+l+l+l+i+l"; |
|
112 |
by (fast_arith_tac 1); |
|
113 |
qed ""; |
|
114 |
||
115 |
Goal "!!a::hypreal. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |] \ |
|
11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset
|
116 |
\ ==> 6*a <= 5*l+i"; |
10751 | 117 |
by (fast_arith_tac 1); |
118 |
qed ""; |
|
119 |
*) |