100 |
100 |
101 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, |
102 real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add, |
102 real_of_nat_mult, real_of_int_zero, real_of_one, real_of_int_add, |
103 real_of_int_minus, real_of_int_diff, |
103 real_of_int_minus, real_of_int_diff, |
104 real_of_int_mult, real_of_int_of_nat_eq, |
104 real_of_int_mult, real_of_int_of_nat_eq, |
105 real_of_nat_number_of, real_number_of]; |
105 real_of_nat_number_of, real_number_of] |
106 |
106 |
107 val int_inj_thms = [real_of_int_le_iff RS iffD2, real_of_int_less_iff RS iffD2, |
107 val nat_inj_thms = [real_of_nat_le_iff RS iffD2, |
108 real_of_int_inject RS iffD2]; |
108 real_of_nat_inject RS iffD2] |
|
109 (* not needed because x < (y::nat) can be rewritten as Suc x <= y: |
|
110 real_of_nat_less_iff RS iffD2 *) |
109 |
111 |
110 val nat_inj_thms = [real_of_nat_le_iff RS iffD2, real_of_nat_less_iff RS iffD2, |
112 val int_inj_thms = [real_of_int_le_iff RS iffD2, |
111 real_of_nat_inject RS iffD2]; |
113 real_of_int_inject RS iffD2] |
|
114 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: |
|
115 real_of_int_less_iff RS iffD2 *) |
112 |
116 |
113 in |
117 in |
114 |
118 |
115 val fast_real_arith_simproc = |
119 val fast_real_arith_simproc = |
116 Simplifier.simproc (Theory.sign_of (the_context ())) |
120 Simplifier.simproc (the_context ()) |
117 "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] |
121 "fast_real_arith" ["(m::real) < n","(m::real) <= n", "(m::real) = n"] |
118 Fast_Arith.lin_arith_prover; |
122 Fast_Arith.lin_arith_prover; |
119 |
123 |
120 val real_arith_setup = |
124 val real_arith_setup = |
121 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
125 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
126 neqE = neqE, |
130 neqE = neqE, |
127 simpset = simpset addsimps simps}) #> |
131 simpset = simpset addsimps simps}) #> |
128 arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #> |
132 arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #> |
129 arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT) #> |
133 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)); |
134 (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)); |
131 |
|
132 (* some thms for injection nat => real: |
|
133 real_of_nat_zero |
|
134 real_of_nat_add |
|
135 *) |
|
136 |
135 |
137 end; |
136 end; |
138 |
137 |
139 |
138 |
140 (* Some test data [omitting examples that assume the ordering to be discrete!] |
139 (* Some test data [omitting examples that assume the ordering to be discrete!] |