hide code generation facts in the Float theory, they are only exported for Approximation
authorhoelzl
Fri Apr 20 11:14:39 2012 +0200 (2012-04-20)
changeset 476214cf6011fb884
parent 47620 148d0b3db78d
child 47622 6d53f2ef4a97
hide code generation facts in the Float theory, they are only exported for Approximation
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Library/Float.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 20 10:47:04 2012 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Fri Apr 20 11:14:39 2012 +0200
     1.3 @@ -891,7 +891,7 @@
     1.4      case True
     1.5      thus ?thesis unfolding `n = 0` get_even_def get_odd_def
     1.6        using `real x = 0` lapprox_rat[where x="-1" and y=1]
     1.7 -      by (auto simp: compute_lapprox_rat compute_rapprox_rat)
     1.8 +      by (auto simp: Float.compute_lapprox_rat Float.compute_rapprox_rat)
     1.9    next
    1.10      case False with not0_implies_Suc obtain m where "n = Suc m" by blast
    1.11      thus ?thesis unfolding `n = Suc m` get_even_def get_odd_def using `real x = 0` rapprox_rat[where x=1 and y=1] lapprox_rat[where x=1 and y=1] by (cases "even (Suc m)", auto)
    1.12 @@ -1468,7 +1468,8 @@
    1.13    have "1 / 4 = (Float 1 -2)" unfolding Float_num by auto
    1.14    also have "\<dots> \<le> lb_exp_horner 1 (get_even 4) 1 1 (- 1)"
    1.15      unfolding get_even_def eq4
    1.16 -    by (auto simp add: compute_lapprox_rat compute_rapprox_rat compute_lapprox_posrat compute_rapprox_posrat rat_precision_def compute_bitlen)
    1.17 +    by (auto simp add: Float.compute_lapprox_rat Float.compute_rapprox_rat
    1.18 +                  Float.compute_lapprox_posrat Float.compute_rapprox_posrat rat_precision_def Float.compute_bitlen)
    1.19    also have "\<dots> \<le> exp (- 1 :: float)" using bnds_exp_horner[where x="- 1"] by auto
    1.20    finally show ?thesis by simp
    1.21  qed
    1.22 @@ -1738,7 +1739,7 @@
    1.23    have lb2: "0 \<le> real (Float 1 -1)" and ub2: "real (Float 1 -1) < 1" unfolding Float_num by auto
    1.24  
    1.25    have "0 \<le> (1::int)" and "0 < (3::int)" by auto
    1.26 -  have ub3_ub: "real ?uthird < 1" by (simp add: compute_rapprox_rat rapprox_posrat_less1)
    1.27 +  have ub3_ub: "real ?uthird < 1" by (simp add: Float.compute_rapprox_rat rapprox_posrat_less1)
    1.28  
    1.29    have third_gt0: "(0 :: real) < 1 / 3 + 1" by auto
    1.30    have uthird_gt0: "0 < real ?uthird + 1" using ub3_lb by auto
     2.1 --- a/src/HOL/Library/Float.thy	Fri Apr 20 10:47:04 2012 +0200
     2.2 +++ b/src/HOL/Library/Float.thy	Fri Apr 20 11:14:39 2012 +0200
     2.3 @@ -218,14 +218,14 @@
     2.4  
     2.5  lemma transfer_numeral [transfer_rule]: 
     2.6    "fun_rel (op =) cr_float (numeral :: _ \<Rightarrow> real) (numeral :: _ \<Rightarrow> float)"
     2.7 -  unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def[symmetric])
     2.8 +  unfolding fun_rel_def cr_float_def by simp
     2.9  
    2.10  lemma float_neg_numeral[simp]: "real (neg_numeral x :: float) = neg_numeral x"
    2.11    by (simp add: minus_numeral[symmetric] del: minus_numeral)
    2.12  
    2.13  lemma transfer_neg_numeral [transfer_rule]: 
    2.14    "fun_rel (op =) cr_float (neg_numeral :: _ \<Rightarrow> real) (neg_numeral :: _ \<Rightarrow> float)"
    2.15 -  unfolding fun_rel_def cr_float_def by (simp add: real_of_float_def[symmetric])
    2.16 +  unfolding fun_rel_def cr_float_def by simp
    2.17  
    2.18  lemma
    2.19    shows float_of_numeral[simp]: "numeral k = float_of (numeral k)"
    2.20 @@ -366,10 +366,6 @@
    2.21  
    2.22  subsection {* Compute arithmetic operations *}
    2.23  
    2.24 -lemma real_of_float_Float[code]: "real_of_float (Float m e) =
    2.25 -  (if e \<ge> 0 then m * 2 ^ nat e else m * inverse (2 ^ nat (- e)))"
    2.26 -by (auto simp add: powr_realpow[symmetric] powr_minus real_of_float_def[symmetric])
    2.27 -
    2.28  lemma Float_mantissa_exponent: "Float (mantissa f) (exponent f) = f"
    2.29    unfolding real_of_float_eq mantissa_exponent[of f] by simp
    2.30  
    2.31 @@ -415,11 +411,13 @@
    2.32      unfolding real_of_int_inject by auto
    2.33  qed
    2.34  
    2.35 -lemma compute_zero[code_unfold, code]: "0 = Float 0 0"
    2.36 +lemma compute_float_zero[code_unfold, code]: "0 = Float 0 0"
    2.37    by transfer simp
    2.38 +hide_fact (open) compute_float_zero
    2.39  
    2.40 -lemma compute_one[code_unfold, code]: "1 = Float 1 0"
    2.41 +lemma compute_float_one[code_unfold, code]: "1 = Float 1 0"
    2.42    by transfer simp
    2.43 +hide_fact (open) compute_float_one
    2.44  
    2.45  definition normfloat :: "float \<Rightarrow> float" where
    2.46    [simp]: "normfloat x = x"
    2.47 @@ -429,56 +427,71 @@
    2.48                             else if m = 0 then 0 else Float m e)"
    2.49    unfolding normfloat_def
    2.50    by transfer (auto simp add: powr_add zmod_eq_0_iff)
    2.51 +hide_fact (open) compute_normfloat
    2.52  
    2.53  lemma compute_float_numeral[code_abbrev]: "Float (numeral k) 0 = numeral k"
    2.54    by transfer simp
    2.55 +hide_fact (open) compute_float_numeral
    2.56  
    2.57  lemma compute_float_neg_numeral[code_abbrev]: "Float (neg_numeral k) 0 = neg_numeral k"
    2.58    by transfer simp
    2.59 +hide_fact (open) compute_float_neg_numeral
    2.60  
    2.61  lemma compute_float_uminus[code]: "- Float m1 e1 = Float (- m1) e1"
    2.62    by transfer simp
    2.63 +hide_fact (open) compute_float_uminus
    2.64  
    2.65  lemma compute_float_times[code]: "Float m1 e1 * Float m2 e2 = Float (m1 * m2) (e1 + e2)"
    2.66    by transfer (simp add: field_simps powr_add)
    2.67 +hide_fact (open) compute_float_times
    2.68  
    2.69  lemma compute_float_plus[code]: "Float m1 e1 + Float m2 e2 =
    2.70    (if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
    2.71                else Float (m2 + m1 * 2^nat (e1 - e2)) e2)"
    2.72    by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric])
    2.73 +hide_fact (open) compute_float_plus
    2.74  
    2.75  lemma compute_float_minus[code]: fixes f g::float shows "f - g = f + (-g)"
    2.76    by simp
    2.77 +hide_fact (open) compute_float_minus
    2.78  
    2.79  lemma compute_float_sgn[code]: "sgn (Float m1 e1) = (if 0 < m1 then 1 else if m1 < 0 then -1 else 0)"
    2.80    by transfer (simp add: sgn_times)
    2.81 +hide_fact (open) compute_float_sgn
    2.82  
    2.83  lift_definition is_float_pos :: "float \<Rightarrow> bool" is "op < 0 :: real \<Rightarrow> bool" ..
    2.84  
    2.85  lemma compute_is_float_pos[code]: "is_float_pos (Float m e) \<longleftrightarrow> 0 < m"
    2.86    by transfer (auto simp add: zero_less_mult_iff not_le[symmetric, of _ 0])
    2.87 +hide_fact (open) compute_is_float_pos
    2.88  
    2.89  lemma compute_float_less[code]: "a < b \<longleftrightarrow> is_float_pos (b - a)"
    2.90    by transfer (simp add: field_simps)
    2.91 +hide_fact (open) compute_float_less
    2.92  
    2.93  lift_definition is_float_nonneg :: "float \<Rightarrow> bool" is "op \<le> 0 :: real \<Rightarrow> bool" ..
    2.94  
    2.95  lemma compute_is_float_nonneg[code]: "is_float_nonneg (Float m e) \<longleftrightarrow> 0 \<le> m"
    2.96    by transfer (auto simp add: zero_le_mult_iff not_less[symmetric, of _ 0])
    2.97 +hide_fact (open) compute_is_float_nonneg
    2.98  
    2.99  lemma compute_float_le[code]: "a \<le> b \<longleftrightarrow> is_float_nonneg (b - a)"
   2.100    by transfer (simp add: field_simps)
   2.101 +hide_fact (open) compute_float_le
   2.102  
   2.103  lift_definition is_float_zero :: "float \<Rightarrow> bool"  is "op = 0 :: real \<Rightarrow> bool" by simp
   2.104  
   2.105  lemma compute_is_float_zero[code]: "is_float_zero (Float m e) \<longleftrightarrow> 0 = m"
   2.106    by transfer (auto simp add: is_float_zero_def)
   2.107 +hide_fact (open) compute_is_float_zero
   2.108  
   2.109  lemma compute_float_abs[code]: "abs (Float m e) = Float (abs m) e"
   2.110    by transfer (simp add: abs_mult)
   2.111 +hide_fact (open) compute_float_abs
   2.112  
   2.113  lemma compute_float_eq[code]: "equal_class.equal f g = is_float_zero (f - g)"
   2.114    by transfer simp
   2.115 +hide_fact (open) compute_float_eq
   2.116  
   2.117  subsection {* Rounding Real numbers *}
   2.118  
   2.119 @@ -581,6 +594,7 @@
   2.120      by transfer
   2.121         (auto simp add: round_down_def field_simps powr_add powr_minus inverse_eq_divide)
   2.122  qed
   2.123 +hide_fact (open) compute_float_down
   2.124  
   2.125  lemma ceil_divide_floor_conv:
   2.126  assumes "b \<noteq> 0"
   2.127 @@ -643,6 +657,7 @@
   2.128      by transfer
   2.129         (simp add: round_up_def floor_divide_eq_div field_simps powr_add powr_minus inverse_eq_divide)
   2.130  qed
   2.131 +hide_fact (open) compute_float_up
   2.132  
   2.133  lemmas real_of_ints =
   2.134    real_of_int_zero
   2.135 @@ -777,6 +792,7 @@
   2.136      unfolding bitlen_def
   2.137      by (auto simp: pos_imp_zdiv_pos_iff not_le)
   2.138  qed
   2.139 +hide_fact (open) compute_bitlen
   2.140  
   2.141  lemma float_gt1_scale: assumes "1 \<le> Float m e"
   2.142    shows "0 \<le> e + (bitlen m - 1)"
   2.143 @@ -853,6 +869,7 @@
   2.144      by transfer
   2.145         (simp add: round_down_def powr_int real_div_nat_eq_floor_of_divide field_simps Let_def
   2.146               del: two_powr_minus_int_float)
   2.147 +hide_fact (open) compute_lapprox_posrat
   2.148  
   2.149  lift_definition rapprox_posrat :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> float"
   2.150    is "\<lambda>prec (x::nat) (y::nat). round_up (rat_precision prec x y) (x / y)" by simp
   2.151 @@ -900,6 +917,7 @@
   2.152           (simp add: round_up_def ceil_divide_floor_conv floor_divide_eq_div[symmetric] dvd_eq_mod_eq_0)
   2.153    qed
   2.154  qed
   2.155 +hide_fact (open) compute_rapprox_posrat
   2.156  
   2.157  lemma rat_precision_pos:
   2.158    assumes "0 \<le> x" and "0 < y" and "2 * x < y" and "0 < n"
   2.159 @@ -959,6 +977,7 @@
   2.160          then - (rapprox_posrat prec (nat (-x)) (nat y))
   2.161          else lapprox_posrat prec (nat (-x)) (nat (-y))))"
   2.162    by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
   2.163 +hide_fact (open) compute_lapprox_rat
   2.164  
   2.165  lift_definition rapprox_rat :: "nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> float" is
   2.166    "\<lambda>prec (x::int) (y::int). round_up (rat_precision prec \<bar>x\<bar> \<bar>y\<bar>) (x / y)" by simp
   2.167 @@ -973,6 +992,7 @@
   2.168          then - (lapprox_posrat prec (nat (-x)) (nat y))
   2.169          else rapprox_posrat prec (nat (-x)) (nat (-y))))"
   2.170    by transfer (auto simp: round_up_def round_down_def ceiling_def ac_simps)
   2.171 +hide_fact (open) compute_rapprox_rat
   2.172  
   2.173  subsection {* Division *}
   2.174  
   2.175 @@ -994,6 +1014,7 @@
   2.176      using not_0 
   2.177      by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_down_shift, simp add: field_simps)
   2.178  qed (transfer, auto)
   2.179 +hide_fact (open) compute_float_divl
   2.180  
   2.181  lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is
   2.182    "\<lambda>(prec::nat) a b. round_up (prec + \<lfloor> log 2 \<bar>b\<bar> \<rfloor> - \<lfloor> log 2 \<bar>a\<bar> \<rfloor>) (a / b)" by simp
   2.183 @@ -1013,6 +1034,7 @@
   2.184      using not_0 
   2.185      by (transfer fixing: m1 s1 m2 s2 prec) (unfold eq1 eq2 round_up_shift, simp add: field_simps)
   2.186  qed (transfer, auto)
   2.187 +hide_fact (open) compute_float_divr
   2.188  
   2.189  subsection {* Lemmas needed by Approximate *}
   2.190  
   2.191 @@ -1208,34 +1230,28 @@
   2.192    "float_round_down prec (Float m e) = (let d = bitlen (abs m) - int prec in
   2.193      if 0 < d then let P = 2^nat d ; n = m div P in Float n (e + d)
   2.194               else Float m e)"
   2.195 -  using compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   2.196 +  using Float.compute_float_down[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   2.197    by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
   2.198 +hide_fact (open) compute_float_round_down
   2.199  
   2.200  lemma compute_float_round_up[code]:
   2.201    "float_round_up prec (Float m e) = (let d = (bitlen (abs m) - int prec) in
   2.202       if 0 < d then let P = 2^nat d ; n = m div P ; r = m mod P
   2.203                     in Float (n + (if r = 0 then 0 else 1)) (e + d)
   2.204                else Float m e)"
   2.205 -  using compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   2.206 +  using Float.compute_float_up[of "prec - bitlen \<bar>m\<bar> - e" m e, symmetric]
   2.207    unfolding Let_def
   2.208    by transfer (simp add: field_simps abs_mult log_mult bitlen_def cong del: if_weak_cong)
   2.209 +hide_fact (open) compute_float_round_up
   2.210  
   2.211  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
   2.212   apply (auto simp: zero_float_def mult_le_0_iff)
   2.213   using powr_gt_zero[of 2 b] by simp
   2.214  
   2.215 -(* TODO: how to use as code equation? -> pprt_float?! *)
   2.216 -lemma compute_pprt[code]: "pprt (Float a e) = (if a <= 0 then 0 else (Float a e))"
   2.217 -unfolding pprt_def sup_float_def max_def Float_le_zero_iff ..
   2.218 -
   2.219 -(* TODO: how to use as code equation? *)
   2.220 -lemma compute_nprt[code]: "nprt (Float a e) = (if a <= 0 then (Float a e) else 0)"
   2.221 -unfolding nprt_def inf_float_def min_def Float_le_zero_iff ..
   2.222 -
   2.223 -lemma of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
   2.224 +lemma real_of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
   2.225    unfolding pprt_def sup_float_def max_def sup_real_def by auto
   2.226  
   2.227 -lemma of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
   2.228 +lemma real_of_float_nprt[simp]: fixes a::float shows "real (nprt a) = nprt (real a)"
   2.229    unfolding nprt_def inf_float_def min_def inf_real_def by auto
   2.230  
   2.231  lift_definition int_floor_fl :: "float \<Rightarrow> int" is floor by simp
   2.232 @@ -1243,12 +1259,14 @@
   2.233  lemma compute_int_floor_fl[code]:
   2.234    "int_floor_fl (Float m e) = (if 0 \<le> e then m * 2 ^ nat e else m div (2 ^ (nat (-e))))"
   2.235    by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
   2.236 +hide_fact (open) compute_int_floor_fl
   2.237  
   2.238  lift_definition floor_fl :: "float \<Rightarrow> float" is "\<lambda>x. real (floor x)" by simp
   2.239  
   2.240  lemma compute_floor_fl[code]:
   2.241    "floor_fl (Float m e) = (if 0 \<le> e then Float m e else Float (m div (2 ^ (nat (-e)))) 0)"
   2.242    by transfer (simp add: powr_int int_of_reals floor_divide_eq_div del: real_of_ints)
   2.243 +hide_fact (open) compute_floor_fl
   2.244  
   2.245  lemma floor_fl: "real (floor_fl x) \<le> real x" by transfer simp
   2.246