197 declare zero_float.rep_eq[simp] |
197 declare zero_float.rep_eq[simp] |
198 |
198 |
199 lift_definition one_float :: float is 1 by simp |
199 lift_definition one_float :: float is 1 by simp |
200 declare one_float.rep_eq[simp] |
200 declare one_float.rep_eq[simp] |
201 |
201 |
202 lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op +" by simp |
202 lift_definition plus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(+)" by simp |
203 declare plus_float.rep_eq[simp] |
203 declare plus_float.rep_eq[simp] |
204 |
204 |
205 lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op *" by simp |
205 lift_definition times_float :: "float \<Rightarrow> float \<Rightarrow> float" is "( * )" by simp |
206 declare times_float.rep_eq[simp] |
206 declare times_float.rep_eq[simp] |
207 |
207 |
208 lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "op -" by simp |
208 lift_definition minus_float :: "float \<Rightarrow> float \<Rightarrow> float" is "(-)" by simp |
209 declare minus_float.rep_eq[simp] |
209 declare minus_float.rep_eq[simp] |
210 |
210 |
211 lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp |
211 lift_definition uminus_float :: "float \<Rightarrow> float" is "uminus" by simp |
212 declare uminus_float.rep_eq[simp] |
212 declare uminus_float.rep_eq[simp] |
213 |
213 |
215 declare abs_float.rep_eq[simp] |
215 declare abs_float.rep_eq[simp] |
216 |
216 |
217 lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp |
217 lift_definition sgn_float :: "float \<Rightarrow> float" is sgn by simp |
218 declare sgn_float.rep_eq[simp] |
218 declare sgn_float.rep_eq[simp] |
219 |
219 |
220 lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op = :: real \<Rightarrow> real \<Rightarrow> bool" . |
220 lift_definition equal_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "(=) :: real \<Rightarrow> real \<Rightarrow> bool" . |
221 |
221 |
222 lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op \<le>" . |
222 lift_definition less_eq_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "(\<le>)" . |
223 declare less_eq_float.rep_eq[simp] |
223 declare less_eq_float.rep_eq[simp] |
224 |
224 |
225 lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "op <" . |
225 lift_definition less_float :: "float \<Rightarrow> float \<Rightarrow> bool" is "(<)" . |
226 declare less_float.rep_eq[simp] |
226 declare less_float.rep_eq[simp] |
227 |
227 |
228 instance |
228 instance |
229 by standard (transfer; fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+ |
229 by standard (transfer; fastforce simp add: field_simps intro: mult_left_mono mult_right_mono)+ |
230 |
230 |
288 apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq float_of_inverse |
288 apply (simp_all only: numeral_Bit0 numeral_Bit1 real_of_float_eq float_of_inverse |
289 plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float) |
289 plus_float.rep_eq one_float.rep_eq plus_float numeral_float one_float) |
290 done |
290 done |
291 |
291 |
292 lemma transfer_numeral [transfer_rule]: |
292 lemma transfer_numeral [transfer_rule]: |
293 "rel_fun (op =) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)" |
293 "rel_fun (=) pcr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)" |
294 by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def) |
294 by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def) |
295 |
295 |
296 lemma float_neg_numeral[simp]: "real_of_float (- numeral x :: float) = - numeral x" |
296 lemma float_neg_numeral[simp]: "real_of_float (- numeral x :: float) = - numeral x" |
297 by simp |
297 by simp |
298 |
298 |
299 lemma transfer_neg_numeral [transfer_rule]: |
299 lemma transfer_neg_numeral [transfer_rule]: |
300 "rel_fun (op =) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)" |
300 "rel_fun (=) pcr_float (- numeral :: _ \<Rightarrow> real) (- numeral :: _ \<Rightarrow> float)" |
301 by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def) |
301 by (simp add: rel_fun_def float.pcr_cr_eq cr_float_def) |
302 |
302 |
303 lemma float_of_numeral[simp]: "numeral k = float_of (numeral k)" |
303 lemma float_of_numeral[simp]: "numeral k = float_of (numeral k)" |
304 and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)" |
304 and float_of_neg_numeral[simp]: "- numeral k = float_of (- numeral k)" |
305 unfolding real_of_float_eq by simp_all |
305 unfolding real_of_float_eq by simp_all |
590 |
590 |
591 qualified lemma compute_float_sgn[code]: |
591 qualified lemma compute_float_sgn[code]: |
592 "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)" |
592 "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)" |
593 by transfer (simp add: sgn_mult) |
593 by transfer (simp add: sgn_mult) |
594 |
594 |
595 lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" . |
595 lift_definition is_float_pos :: "float \<Rightarrow> bool" is "(<) 0 :: real \<Rightarrow> bool" . |
596 |
596 |
597 qualified lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m" |
597 qualified lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m" |
598 by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0]) |
598 by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0]) |
599 |
599 |
600 lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" . |
600 lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "(\<le>) 0 :: real \<Rightarrow> bool" . |
601 |
601 |
602 qualified lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m" |
602 qualified lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m" |
603 by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0]) |
603 by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0]) |
604 |
604 |
605 lift_definition is_float_zero :: "float \<Rightarrow> bool" is "op = 0 :: real \<Rightarrow> bool" . |
605 lift_definition is_float_zero :: "float \<Rightarrow> bool" is "(=) 0 :: real \<Rightarrow> bool" . |
606 |
606 |
607 qualified lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m" |
607 qualified lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m" |
608 by transfer (auto simp add: is_float_zero_def) |
608 by transfer (auto simp add: is_float_zero_def) |
609 |
609 |
610 qualified lemma compute_float_abs[code]: "\<bar>Float m e\<bar> = Float \<bar>m\<bar> e" |
610 qualified lemma compute_float_abs[code]: "\<bar>Float m e\<bar> = Float \<bar>m\<bar> e" |
1335 |
1335 |
1336 lift_definition power_down_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_down |
1336 lift_definition power_down_fl :: "nat \<Rightarrow> float \<Rightarrow> nat \<Rightarrow> float" is power_down |
1337 by (induct_tac rule: power_down.induct) simp_all |
1337 by (induct_tac rule: power_down.induct) simp_all |
1338 |
1338 |
1339 lemma power_float_transfer[transfer_rule]: |
1339 lemma power_float_transfer[transfer_rule]: |
1340 "(rel_fun pcr_float (rel_fun op = pcr_float)) op ^ op ^" |
1340 "(rel_fun pcr_float (rel_fun (=) pcr_float)) (^) (^)" |
1341 unfolding power_def |
1341 unfolding power_def |
1342 by transfer_prover |
1342 by transfer_prover |
1343 |
1343 |
1344 lemma compute_power_up_fl[code]: |
1344 lemma compute_power_up_fl[code]: |
1345 "power_up_fl p x 0 = 1" |
1345 "power_up_fl p x 0 = 1" |