author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 28952  15a4b2cf8c34 
child 30498  55f2933bef6e 
permissions  rwrr 
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  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  15 
val simps = 
16 
[@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, 

27239  17 
read_instantiate @{context} [(("a", 0), "(number_of ?v)")] @{thm right_distrib}, 
27225  18 
@{thm divide_1}, @{thm divide_zero_left}, 
19 
@{thm times_divide_eq_right}, @{thm times_divide_eq_left}, 

20 
@{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, 

21 
@{thm of_int_0}, @{thm of_int_1}, @{thm of_int_add}, 

22 
@{thm of_int_minus}, @{thm of_int_diff}, 

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  25 
val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2, 
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  30 
val int_inj_thms = [@{thm of_int_le_iff} RS iffD2, 
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  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  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  44 
lessD = lessD, (*Can't change lessD: the rats are dense!*) 
15923  45 
neqE = neqE, 
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
14378
diff
changeset

46 
simpset = simpset addsimps simps 
18708  47 
addsimprocs simprocs}) #> 
24196  48 
arith_inj_const (@{const_name of_nat}, HOLogic.natT > ratT) #> 
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; 