author  wenzelm 
Sun, 01 Mar 2009 23:36:12 +0100  
changeset 30190  479806475f3c 
parent 28952  15a4b2cf8c34 
child 30685  dd5fe091ff04 
permissions  rwrr 
14426  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  4 
Copyright 1999 TU Muenchen 
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

5 

14352  6 
Simprocs for common factor cancellation & Rational coefficient handling 
7 

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  11 
local 
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  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  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  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  36 
lessD = lessD, (*Can't change lessD: the reals are dense!*) 
15923  37 
neqE = neqE, 
18708  38 
simpset = simpset addsimps simps}) #> 
27545  39 
arith_inj_const (@{const_name real}, HOLogic.natT > HOLogic.realT) #> 
40 
arith_inj_const (@{const_name real}, HOLogic.intT > HOLogic.realT) 

14352  41 

9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
diff
changeset

42 
end; 