src/HOL/Hyperreal/hypreal_arith.ML
author wenzelm
Tue, 31 Jul 2007 00:56:26 +0200
changeset 24075 366d4d234814
parent 20254 58b71535ed00
child 24093 5d0ecd0c8f3c
permissions -rw-r--r--
arith method setup: proper context;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14309
f508492af9b4 moving HyperArith0.ML to other theories
paulson
parents: 14305
diff changeset
     1
(*  Title:      HOL/Hyperreal/hypreal_arith.ML
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     2
    ID:         $Id$
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     3
    Author:     Tobias Nipkow, TU Muenchen
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     4
    Copyright   1999 TU Muenchen
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     5
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14334
diff changeset
     6
Simprocs for common factor cancellation & Rational coefficient handling
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14334
diff changeset
     7
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14334
diff changeset
     8
Instantiation of the generic linear arithmetic package for type hypreal.
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
     9
*)
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    10
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    11
local
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    12
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    13
val simps = [thm "star_of_zero",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    14
             thm "star_of_one",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    15
             thm "star_of_number_of",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    16
             thm "star_of_add",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    17
             thm "star_of_minus",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    18
             thm "star_of_diff",
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    19
             thm "star_of_mult"]
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    20
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    21
val real_inj_thms = [thm "star_of_le" RS iffD2,
17318
bc1c75855f3d starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents: 15923
diff changeset
    22
                     thm "star_of_less" RS iffD2,
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    23
                     thm "star_of_eq" RS iffD2]
14369
c50188fe6366 tidying up arithmetic for the hyperreals
paulson
parents: 14352
diff changeset
    24
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    25
in
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    26
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    27
val hyprealT = Type ("StarDef.star", [HOLogic.realT]);
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14370
diff changeset
    28
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14334
diff changeset
    29
val fast_hypreal_arith_simproc =
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    30
    Simplifier.simproc (the_context ())
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14334
diff changeset
    31
      "fast_hypreal_arith" 
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14334
diff changeset
    32
      ["(m::hypreal) < n", "(m::hypreal) <= n", "(m::hypreal) = n"]
24075
366d4d234814 arith method setup: proper context;
wenzelm
parents: 20254
diff changeset
    33
    (K Fast_Arith.lin_arith_simproc);
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14334
diff changeset
    34
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    35
val hypreal_arith_setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17876
diff changeset
    36
  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
14369
c50188fe6366 tidying up arithmetic for the hyperreals
paulson
parents: 14352
diff changeset
    37
   {add_mono_thms = add_mono_thms,
15184
d2c19aea17bc made mult_mono_thms generic.
nipkow
parents: 14387
diff changeset
    38
    mult_mono_thms = mult_mono_thms,
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    39
    inj_thms = real_inj_thms @ inj_thms,
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14334
diff changeset
    40
    lessD = lessD,  (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
15923
01d5d0c1c078 fixed lin.arith
nipkow
parents: 15186
diff changeset
    41
    neqE = neqE,
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    42
    simpset = simpset addsimps simps}) #>
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17876
diff changeset
    43
  arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
24075
366d4d234814 arith method setup: proper context;
wenzelm
parents: 20254
diff changeset
    44
  Simplifier.map_ss (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]);
10751
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    45
a81ea5d3dd41 separation of HOL-Hyperreal from HOL-Real
paulson
parents:
diff changeset
    46
end;