author | paulson |
Tue, 17 Feb 2004 10:41:59 +0100 | |
changeset 14390 | 55fe71faadda |
parent 14387 | e96d5c42c4b0 |
child 15121 | 1198032bad25 |
permissions | -rw-r--r-- |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/Real/rat_arith0.ML |
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 |
|
14390 | 11 |
(*FIXME: these monomorphic versions are necessary because of a bug in the arith |
12 |
procedure*) |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
13 |
val rat_mult_strict_left_mono = |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
14 |
read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
15 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
16 |
val rat_mult_left_mono = |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
17 |
read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono; |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
18 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
19 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
20 |
(****Instantiation of the generic linear arithmetic package for fields****) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
21 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
22 |
local |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
23 |
|
14390 | 24 |
val simprocs = field_cancel_numeral_factors |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
25 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
26 |
val mono_ss = simpset() addsimps |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
27 |
[add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono]; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
28 |
|
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14365
diff
changeset
|
29 |
val add_mono_thms_ordered_field = |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
30 |
map (fn s => prove_goal (the_context ()) s |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
31 |
(fn prems => [cut_facts_tac prems 1, asm_simp_tac mono_ss 1])) |
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14365
diff
changeset
|
32 |
["(i < j) & (k = l) ==> i + k < j + (l::'a::ordered_field)", |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14365
diff
changeset
|
33 |
"(i = j) & (k < l) ==> i + k < j + (l::'a::ordered_field)", |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14365
diff
changeset
|
34 |
"(i < j) & (k <= l) ==> i + k < j + (l::'a::ordered_field)", |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14365
diff
changeset
|
35 |
"(i <= j) & (k < l) ==> i + k < j + (l::'a::ordered_field)", |
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14365
diff
changeset
|
36 |
"(i < j) & (k < l) ==> i + k < j + (l::'a::ordered_field)"]; |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
37 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
38 |
fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
39 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
40 |
val rat_mult_mono_thms = |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
41 |
[(rat_mult_strict_left_mono, |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
42 |
cvar(rat_mult_strict_left_mono, hd(tl(prems_of rat_mult_strict_left_mono)))), |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
43 |
(rat_mult_left_mono, |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
44 |
cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
45 |
|
14390 | 46 |
val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals, |
14369 | 47 |
inst "a" "(number_of ?v)" right_distrib, |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
48 |
divide_1, divide_zero_left, |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
49 |
times_divide_eq_right, times_divide_eq_left, |
14390 | 50 |
minus_divide_left RS sym, minus_divide_right RS sym, |
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14369
diff
changeset
|
51 |
of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff, |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
52 |
of_int_mult, of_int_of_nat_eq]; |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
53 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
54 |
in |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
55 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
56 |
val fast_rat_arith_simproc = |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
57 |
Simplifier.simproc (Theory.sign_of(the_context())) |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
58 |
"fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"] |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
59 |
Fast_Arith.lin_arith_prover; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
60 |
|
14378
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14369
diff
changeset
|
61 |
val nat_inj_thms = [of_nat_le_iff RS iffD2, of_nat_less_iff RS iffD2, |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14369
diff
changeset
|
62 |
of_nat_eq_iff RS iffD2]; |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14369
diff
changeset
|
63 |
|
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14369
diff
changeset
|
64 |
val int_inj_thms = [of_int_le_iff RS iffD2, of_int_less_iff RS iffD2, |
69c4d5997669
generic of_nat and of_int functions, and generalization of iszero
paulson
parents:
14369
diff
changeset
|
65 |
of_int_eq_iff RS iffD2]; |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
66 |
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
67 |
val ratT = Type("Rational.rat", []); |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
68 |
|
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
69 |
val rat_arith_setup = |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
70 |
[Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
14368
2763da611ad9
converted Real/Lubs to Isar script. Converting arithmetic setup
paulson
parents:
14365
diff
changeset
|
71 |
{add_mono_thms = add_mono_thms @ add_mono_thms_ordered_field, |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
72 |
mult_mono_thms = mult_mono_thms @ rat_mult_mono_thms, |
14369 | 73 |
inj_thms = int_inj_thms @ inj_thms, |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
74 |
lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*) |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
75 |
simpset = simpset addsimps simps |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
76 |
addsimprocs simprocs}), |
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
77 |
arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT), |
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset
|
78 |
arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT), |
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
79 |
arith_discrete ("Rational.rat",false), |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
80 |
Simplifier.change_simpset_of (op addsimprocs) [fast_rat_arith_simproc]]; |
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
81 |
|
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
diff
changeset
|
82 |
end; |