author | nipkow |
Mon, 16 Aug 2004 14:22:27 +0200 | |
changeset 15131 | c69542757a4d |
parent 14387 | e96d5c42c4b0 |
child 15184 | d2c19aea17bc |
permissions | -rw-r--r-- |
14309 | 1 |
(* Title: HOL/Hyperreal/hypreal_arith.ML |
10751 | 2 |
ID: $Id$ |
3 |
Author: Tobias Nipkow, TU Muenchen |
|
4 |
Copyright 1999 TU Muenchen |
|
5 |
||
14352 | 6 |
Simprocs for common factor cancellation & Rational coefficient handling |
7 |
||
8 |
Instantiation of the generic linear arithmetic package for type hypreal. |
|
10751 | 9 |
*) |
10 |
||
14369 | 11 |
(*FIXME DELETE*) |
14370 | 12 |
val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2"; |
13 |
||
14369 | 14 |
val hypreal_mult_left_mono = |
15 |
read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono; |
|
16 |
||
17 |
||
14352 | 18 |
(****Instantiation of the generic linear arithmetic package****) |
19 |
||
14309 | 20 |
|
10751 | 21 |
local |
22 |
||
23 |
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
|
24 |
||
25 |
val hypreal_mult_mono_thms = |
|
26 |
[(rotate_prems 1 hypreal_mult_less_mono2, |
|
27 |
cvar(hypreal_mult_less_mono2, hd(prems_of hypreal_mult_less_mono2))), |
|
14352 | 28 |
(hypreal_mult_left_mono, |
29 |
cvar(hypreal_mult_left_mono, hd(tl(prems_of hypreal_mult_left_mono))))] |
|
10751 | 30 |
|
14369 | 31 |
val real_inj_thms = [hypreal_of_real_le_iff RS iffD2, |
32 |
hypreal_of_real_less_iff RS iffD2, |
|
33 |
hypreal_of_real_eq_iff RS iffD2]; |
|
34 |
||
10751 | 35 |
in |
36 |
||
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14370
diff
changeset
|
37 |
val hyprealT = Type("Rational.hypreal", []); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14370
diff
changeset
|
38 |
|
14352 | 39 |
val fast_hypreal_arith_simproc = |
40 |
Simplifier.simproc (Theory.sign_of (the_context ())) |
|
41 |
"fast_hypreal_arith" |
|
42 |
["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"] |
|
43 |
Fast_Arith.lin_arith_prover; |
|
44 |
||
10751 | 45 |
val hypreal_arith_setup = |
46 |
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
|
14369 | 47 |
{add_mono_thms = add_mono_thms, |
10751 | 48 |
mult_mono_thms = mult_mono_thms @ hypreal_mult_mono_thms, |
14369 | 49 |
inj_thms = inj_thms @ real_inj_thms, |
14352 | 50 |
lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14370
diff
changeset
|
51 |
simpset = simpset}), |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14370
diff
changeset
|
52 |
arith_inj_const ("HyperDef.hypreal_of_real", HOLogic.realT --> hyprealT), |
14352 | 53 |
arith_discrete ("HyperDef.hypreal",false), |
54 |
Simplifier.change_simpset_of (op addsimprocs) [fast_hypreal_arith_simproc]]; |
|
10751 | 55 |
|
56 |
end; |
|
57 |
||
14352 | 58 |
|
59 |