src/HOL/Tools/rat_arith.ML
author wenzelm
Sun, 01 Mar 2009 23:36:12 +0100
changeset 30190 479806475f3c
parent 28952 15a4b2cf8c34
child 30498 55f2933bef6e
permissions -rw-r--r--
use long names for old-style fold combinators;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
     1
(*  Title:      HOL/Real/rat_arith.ML
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
     2
    ID:         $Id$
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
     4
    Copyright   2004 University of Cambridge
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
     5
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
     6
Simprocs for common factor cancellation & Rational coefficient handling
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
     7
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
     8
Instantiation of the generic linear arithmetic package for type rat.
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
     9
*)
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    10
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    11
local
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    12
14390
55fe71faadda further tweaks to the numeric theories
paulson
parents: 14387
diff changeset
    13
val simprocs = field_cancel_numeral_factors
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    14
27225
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
    15
val simps =
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
    16
 [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals},
27239
f2f42f9fa09d pervasive RuleInsts;
wenzelm
parents: 27225
diff changeset
    17
  read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib},
27225
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
    18
  @{thm divide_1}, @{thm divide_zero_left},
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
    19
  @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
    20
  @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
    21
  @{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add},
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
    22
  @{thm of_int_minus}, @{thm of_int_diff},
b316dde851f5 eliminated OldGoals.inst;
wenzelm
parents: 27154
diff changeset
    23
  @{thm of_int_mult}, @{thm of_int_of_nat_eq}]
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    24
22803
5129e02f4df2 slightly tuned
haftmann
parents: 22548
diff changeset
    25
val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2,
5129e02f4df2 slightly tuned
haftmann
parents: 22548
diff changeset
    26
                    @{thm of_nat_eq_iff} RS iffD2]
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    27
(* 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
    28
                    of_nat_less_iff RS iffD2 *)
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    29
22803
5129e02f4df2 slightly tuned
haftmann
parents: 22548
diff changeset
    30
val int_inj_thms = [@{thm of_int_le_iff} RS iffD2,
5129e02f4df2 slightly tuned
haftmann
parents: 22548
diff changeset
    31
                    @{thm of_int_eq_iff} RS iffD2]
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    32
(* 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
    33
                    of_int_less_iff RS iffD2 *)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    34
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    35
in
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    36
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    37
val ratT = Type ("Rational.rat", [])
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    38
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    39
val rat_arith_setup =
24093
5d0ecd0c8f3c tuned LinArith setup;
wenzelm
parents: 23346
diff changeset
    40
  LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
15121
1198032bad25 Initial changes to extend arithmetic from individual types to type classes.
nipkow
parents: 14390
diff changeset
    41
   {add_mono_thms = add_mono_thms,
15184
d2c19aea17bc made mult_mono_thms generic.
nipkow
parents: 15121
diff changeset
    42
    mult_mono_thms = mult_mono_thms,
20254
58b71535ed00 lin_arith_prover splits certain operators (e.g. min, max, abs)
webertj
parents: 18708
diff changeset
    43
    inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
24093
5d0ecd0c8f3c tuned LinArith setup;
wenzelm
parents: 23346
diff changeset
    44
    lessD = lessD,  (*Can't change lessD: the rats are dense!*)
15923
01d5d0c1c078 fixed lin.arith
nipkow
parents: 15186
diff changeset
    45
    neqE =  neqE,
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
    46
    simpset = simpset addsimps simps
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17876
diff changeset
    47
                      addsimprocs simprocs}) #>
24196
f1dbfd7e3223 localized of_nat
haftmann
parents: 24093
diff changeset
    48
  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #>
f1dbfd7e3223 localized of_nat
haftmann
parents: 24093
diff changeset
    49
  arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    50
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff changeset
    51
end;