5 |
5 |
6 Simprocs for common factor cancellation & Rational coefficient handling |
6 Simprocs for common factor cancellation & Rational coefficient handling |
7 |
7 |
8 Instantiation of the generic linear arithmetic package for type real. |
8 Instantiation of the generic linear arithmetic package for type real. |
9 *) |
9 *) |
10 |
|
11 (*FIXME DELETE*) |
|
12 val real_mult_left_mono = |
|
13 read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono; |
|
14 |
10 |
15 val real_le_def = thm "real_le_def"; |
11 val real_le_def = thm "real_le_def"; |
16 val real_diff_def = thm "real_diff_def"; |
12 val real_diff_def = thm "real_diff_def"; |
17 val real_divide_def = thm "real_divide_def"; |
13 val real_divide_def = thm "real_divide_def"; |
18 |
14 |
100 |
96 |
101 (****Instantiation of the generic linear arithmetic package****) |
97 (****Instantiation of the generic linear arithmetic package****) |
102 |
98 |
103 local |
99 local |
104 |
100 |
105 fun cvar(th,_ $ (_ $ _ $ var)) = cterm_of (#sign(rep_thm th)) var; |
|
106 |
|
107 val real_mult_mono_thms = |
|
108 [(rotate_prems 1 real_mult_less_mono2, |
|
109 cvar(real_mult_less_mono2, hd(prems_of real_mult_less_mono2))), |
|
110 (real_mult_left_mono, |
|
111 cvar(real_mult_left_mono, hd(tl(prems_of real_mult_left_mono))))] |
|
112 |
|
113 val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, |
101 val simps = [real_of_nat_zero, real_of_nat_Suc, real_of_nat_add, |
114 real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym, |
102 real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add RS sym, |
115 real_of_int_minus RS sym, real_of_int_diff RS sym, |
103 real_of_int_minus RS sym, real_of_int_diff RS sym, |
116 real_of_int_mult RS sym, real_of_int_of_nat_eq, |
104 real_of_int_mult RS sym, real_of_int_of_nat_eq, |
117 real_of_nat_number_of, real_number_of]; |
105 real_of_nat_number_of, real_number_of]; |
130 Fast_Arith.lin_arith_prover; |
118 Fast_Arith.lin_arith_prover; |
131 |
119 |
132 val real_arith_setup = |
120 val real_arith_setup = |
133 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
121 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset} => |
134 {add_mono_thms = add_mono_thms, |
122 {add_mono_thms = add_mono_thms, |
135 mult_mono_thms = mult_mono_thms @ real_mult_mono_thms, |
123 mult_mono_thms = mult_mono_thms, |
136 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
124 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
137 lessD = lessD, (*Can't change LA_Data_Ref.lessD: the reals are dense!*) |
125 lessD = lessD, (*Can't change LA_Data_Ref.lessD: the reals are dense!*) |
138 simpset = simpset addsimps simps}), |
126 simpset = simpset addsimps simps}), |
139 arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT), |
127 arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT), |
140 arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT), |
128 arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT), |