116 Simplifier.simproc (Theory.sign_of (the_context ())) |
116 Simplifier.simproc (Theory.sign_of (the_context ())) |
117 "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] |
117 "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] |
118 Fast_Arith.lin_arith_prover; |
118 Fast_Arith.lin_arith_prover; |
119 |
119 |
120 val real_arith_setup = |
120 val real_arith_setup = |
121 [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
121 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
122 {add_mono_thms = add_mono_thms, |
122 {add_mono_thms = add_mono_thms, |
123 mult_mono_thms = mult_mono_thms, |
123 mult_mono_thms = mult_mono_thms, |
124 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
124 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
125 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!*) |
126 neqE = neqE, |
126 neqE = neqE, |
127 simpset = simpset addsimps simps}), |
127 simpset = simpset addsimps simps}) #> |
128 arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT), |
128 arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #> |
129 arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT), |
129 arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT) #> |
130 fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)]; |
130 (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)); |
131 |
131 |
132 (* some thms for injection nat => real: |
132 (* some thms for injection nat => real: |
133 real_of_nat_zero |
133 real_of_nat_zero |
134 real_of_nat_add |
134 real_of_nat_add |
135 *) |
135 *) |