src/HOL/Tools/real_arith.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 28952 15a4b2cf8c34
child 30685 dd5fe091ff04
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14426
de890c247b38 fixed bugs in the setup of arithmetic procedures
paulson
parents: 14390
diff changeset
     1
(*  Title:      HOL/Real/real_arith.ML
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     3
    Author:     Tobias Nipkow, TU Muenchen
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     4
    Copyright   1999 TU Muenchen
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     5
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     6
Simprocs for common factor cancellation & Rational coefficient handling
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     7
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
     8
Instantiation of the generic linear arithmetic package for type real.
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
     9
*)
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    10
14289
deb8e1e62002 combining Real/{RealArith0,real_arith}.ML
paulson
parents: 14288
diff changeset
    11
local
deb8e1e62002 combining Real/{RealArith0,real_arith}.ML
paulson
parents: 14288
diff changeset
    12
23080
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    13
val simps = [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    14
             @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    15
             @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    16
             @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    17
             @{thm real_of_nat_number_of}, @{thm real_number_of}]
14355
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
    18
23080
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    19
val nat_inj_thms = [@{thm real_of_nat_le_iff} RS iffD2,
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    20
                    @{thm real_of_nat_inject} RS iffD2]
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    21
(* not needed because x < (y::nat) can be rewritten as Suc x <= y:
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    22
                    real_of_nat_less_iff RS iffD2 *)
14355
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
    23
23080
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    24
val int_inj_thms = [@{thm real_of_int_le_iff} RS iffD2,
2f8d7aa1263b remove redundant simproc; remove legacy ML bindings
huffman
parents: 22970
diff changeset
    25
                    @{thm real_of_int_inject} RS iffD2]
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    26
(* not needed because x < (y::int) can be rewritten as x + 1 <= y:
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    27
                    real_of_int_less_iff RS iffD2 *)
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
    28
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    29
in
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    30
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    31
val real_arith_setup =
24093
5d0ecd0c8f3c tuned LinArith setup;
wenzelm
parents: 23081
diff changeset
    32
  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
14368
2763da611ad9 converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents: 14365
diff changeset
    33
   {add_mono_thms = add_mono_thms,
15184
d2c19aea17bc made mult_mono_thms generic.
nipkow
parents: 15003
diff changeset
    34
    mult_mono_thms = mult_mono_thms,
14355
67e2e96bfe36 Told linear arithmetic package about injections "real" from nat/int into real.
nipkow
parents: 14352
diff changeset
    35
    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
24093
5d0ecd0c8f3c tuned LinArith setup;
wenzelm
parents: 23081
diff changeset
    36
    lessD = lessD,  (*Can't change lessD: the reals are dense!*)
15923
01d5d0c1c078 fixed lin.arith
nipkow
parents: 15661
diff changeset
    37
    neqE = neqE,
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17876
diff changeset
    38
    simpset = simpset addsimps simps}) #>
27545
7165068bb61f antiquotation
haftmann
parents: 24093
diff changeset
    39
  arith_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
7165068bb61f antiquotation
haftmann
parents: 24093
diff changeset
    40
  arith_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
14352
a8b1a44d8264 Modified real arithmetic simplification
paulson
parents: 14336
diff changeset
    41
9436
62bb04ab4b01 rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff changeset
    42
end;