Improved computation of bounds and implemented interval splitting for 'approximation'.
authorhoelzl
Thu Jun 25 18:12:40 2009 +0200 (2009-06-25)
changeset 3181164dea9a15031
parent 31810 a6b800855cdd
child 31812 73dc3a98669c
Improved computation of bounds and implemented interval splitting for 'approximation'.
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/ex/Approximation_Ex.thy
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Mon Jun 08 18:37:35 2009 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Jun 25 18:12:40 2009 +0200
     1.3 @@ -2088,6 +2088,36 @@
     1.4  "interpret_floatarith (Num f) vs      = real f" |
     1.5  "interpret_floatarith (Atom n) vs     = vs ! n"
     1.6  
     1.7 +lemma interpret_floatarith_divide: "interpret_floatarith (Mult a (Inverse b)) vs = (interpret_floatarith a vs) / (interpret_floatarith b vs)"
     1.8 +  unfolding real_divide_def interpret_floatarith.simps ..
     1.9 +
    1.10 +lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
    1.11 +  unfolding real_diff_def interpret_floatarith.simps ..
    1.12 +
    1.13 +lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
    1.14 +  sin (interpret_floatarith a vs)"
    1.15 +  unfolding sin_cos_eq interpret_floatarith.simps
    1.16 +            interpret_floatarith_divide interpret_floatarith_diff real_diff_def
    1.17 +  by auto
    1.18 +
    1.19 +lemma interpret_floatarith_tan:
    1.20 +  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
    1.21 +   tan (interpret_floatarith a vs)"
    1.22 +  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def real_divide_def
    1.23 +  by auto
    1.24 +
    1.25 +lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
    1.26 +  unfolding powr_def interpret_floatarith.simps ..
    1.27 +
    1.28 +lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
    1.29 +  unfolding log_def interpret_floatarith.simps real_divide_def ..
    1.30 +
    1.31 +lemma interpret_floatarith_num:
    1.32 +  shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
    1.33 +  and "interpret_floatarith (Num (Float 1 0)) vs = 1"
    1.34 +  and "interpret_floatarith (Num (Float (number_of a) 0)) vs = number_of a" by auto
    1.35 +
    1.36 +
    1.37  subsection "Implement approximation function"
    1.38  
    1.39  fun lift_bin' :: "(float * float) option \<Rightarrow> (float * float) option \<Rightarrow> (float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> (float * float)) \<Rightarrow> (float * float) option" where
    1.40 @@ -2103,32 +2133,47 @@
    1.41  "lift_un' (Some (l1, u1)) f = Some (f l1 u1)" |
    1.42  "lift_un' b f = None"
    1.43  
    1.44 -fun bounded_by :: "real list \<Rightarrow> (float * float) list \<Rightarrow> bool " where
    1.45 -bounded_by_Cons: "bounded_by (v#vs) ((l, u)#bs) = ((real l \<le> v \<and> v \<le> real u) \<and> bounded_by vs bs)" |
    1.46 -bounded_by_Nil: "bounded_by [] [] = True" |
    1.47 -"bounded_by _ _ = False"
    1.48 -
    1.49 -lemma bounded_by: assumes "bounded_by vs bs" and "i < length bs"
    1.50 -  shows "real (fst (bs ! i)) \<le> vs ! i \<and> vs ! i \<le> real (snd (bs ! i))"
    1.51 -  using `bounded_by vs bs` and `i < length bs`
    1.52 -proof (induct arbitrary: i rule: bounded_by.induct)
    1.53 -  fix v :: real and vs :: "real list" and l u :: float and bs :: "(float * float) list" and i :: nat
    1.54 -  assume hyp: "\<And>i. \<lbrakk>bounded_by vs bs; i < length bs\<rbrakk> \<Longrightarrow> real (fst (bs ! i)) \<le> vs ! i \<and> vs ! i \<le> real (snd (bs ! i))"
    1.55 -  assume bounded: "bounded_by (v # vs) ((l, u) # bs)" and length: "i < length ((l, u) # bs)"
    1.56 -  show "real (fst (((l, u) # bs) ! i)) \<le> (v # vs) ! i \<and> (v # vs) ! i \<le> real (snd (((l, u) # bs) ! i))"
    1.57 -  proof (cases i)
    1.58 -    case 0
    1.59 -    show ?thesis using bounded unfolding 0 nth_Cons_0 fst_conv snd_conv bounded_by.simps ..
    1.60 -  next
    1.61 -    case (Suc i) with length have "i < length bs" by auto
    1.62 -    show ?thesis unfolding Suc nth_Cons_Suc bounded_by.simps
    1.63 -      using hyp[OF bounded[unfolded bounded_by.simps, THEN conjunct2] `i < length bs`] .
    1.64 -  qed
    1.65 -qed auto
    1.66 -
    1.67 -fun approx approx' :: "nat \<Rightarrow> floatarith \<Rightarrow> (float * float) list \<Rightarrow> (float * float) option" where
    1.68 +definition
    1.69 +"bounded_by xs vs \<longleftrightarrow>
    1.70 +  (\<forall> i < length vs. case vs ! i of None \<Rightarrow> True
    1.71 +         | Some (l, u) \<Rightarrow> xs ! i \<in> { real l .. real u })"
    1.72 +
    1.73 +lemma bounded_byE:
    1.74 +  assumes "bounded_by xs vs"
    1.75 +  shows "\<And> i. i < length vs \<Longrightarrow> case vs ! i of None \<Rightarrow> True
    1.76 +         | Some (l, u) \<Rightarrow> xs ! i \<in> { real l .. real u }"
    1.77 +  using assms bounded_by_def by blast
    1.78 +
    1.79 +lemma bounded_by_update:
    1.80 +  assumes "bounded_by xs vs"
    1.81 +  and bnd: "xs ! i \<in> { real l .. real u }"
    1.82 +  shows "bounded_by xs (vs[i := Some (l,u)])"
    1.83 +proof -
    1.84 +{ fix j
    1.85 +  let ?vs = "vs[i := Some (l,u)]"
    1.86 +  assume "j < length ?vs" hence [simp]: "j < length vs" by simp
    1.87 +  have "case ?vs ! j of None \<Rightarrow> True | Some (l, u) \<Rightarrow> xs ! j \<in> { real l .. real u }"
    1.88 +  proof (cases "?vs ! j")
    1.89 +    case (Some b)
    1.90 +    thus ?thesis
    1.91 +    proof (cases "i = j")
    1.92 +      case True
    1.93 +      thus ?thesis using `?vs ! j = Some b` and bnd by auto
    1.94 +    next
    1.95 +      case False
    1.96 +      thus ?thesis using `bounded_by xs vs` unfolding bounded_by_def by auto
    1.97 +    qed
    1.98 +  qed auto }
    1.99 +  thus ?thesis unfolding bounded_by_def by auto
   1.100 +qed
   1.101 +
   1.102 +lemma bounded_by_None:
   1.103 +  shows "bounded_by xs (replicate (length xs) None)"
   1.104 +  unfolding bounded_by_def by auto
   1.105 +
   1.106 +fun approx approx' :: "nat \<Rightarrow> floatarith \<Rightarrow> (float * float) option list \<Rightarrow> (float * float) option" where
   1.107  "approx' prec a bs          = (case (approx prec a bs) of Some (l, u) \<Rightarrow> Some (round_down prec l, round_up prec u) | None \<Rightarrow> None)" |
   1.108 -"approx prec (Add a b) bs  = lift_bin' (approx' prec a bs) (approx' prec b bs) (\<lambda> l1 u1 l2 u2. (l1 + l2, u1 + u2))" |
   1.109 +"approx prec (Add a b) bs   = lift_bin' (approx' prec a bs) (approx' prec b bs) (\<lambda> l1 u1 l2 u2. (l1 + l2, u1 + u2))" |
   1.110  "approx prec (Minus a) bs   = lift_un' (approx' prec a bs) (\<lambda> l u. (-u, -l))" |
   1.111  "approx prec (Mult a b) bs  = lift_bin' (approx' prec a bs) (approx' prec b bs)
   1.112                                      (\<lambda> a1 a2 b1 b2. (float_nprt a1 * float_pprt b2 + float_nprt a2 * float_nprt b2 + float_pprt a1 * float_pprt b1 + float_pprt a2 * float_nprt b1,
   1.113 @@ -2145,7 +2190,7 @@
   1.114  "approx prec (Ln a) bs      = lift_un (approx' prec a bs) (\<lambda> l u. (lb_ln prec l, ub_ln prec u))" |
   1.115  "approx prec (Power a n) bs = lift_un' (approx' prec a bs) (float_power_bnds n)" |
   1.116  "approx prec (Num f) bs     = Some (f, f)" |
   1.117 -"approx prec (Atom i) bs    = (if i < length bs then Some (bs ! i) else None)"
   1.118 +"approx prec (Atom i) bs    = (if i < length bs then bs ! i else None)"
   1.119  
   1.120  lemma lift_bin'_ex:
   1.121    assumes lift_bin'_Some: "Some (l, u) = lift_bin' a b f"
   1.122 @@ -2421,118 +2466,175 @@
   1.123  next case (Num f) thus ?case by auto
   1.124  next
   1.125    case (Atom n)
   1.126 -  show ?case
   1.127 -  proof (cases "n < length vs")
   1.128 -    case True
   1.129 -    with Atom have "vs ! n = (l, u)" by auto
   1.130 -    thus ?thesis using bounded_by[OF assms(1) True] by auto
   1.131 +  from this[symmetric] `bounded_by xs vs`[THEN bounded_byE, of n]
   1.132 +  show ?case by (cases "n < length vs", auto)
   1.133 +qed
   1.134 +
   1.135 +datatype form = Bound floatarith floatarith floatarith form
   1.136 +              | Assign floatarith floatarith form
   1.137 +              | Less floatarith floatarith
   1.138 +              | LessEqual floatarith floatarith
   1.139 +              | AtLeastAtMost floatarith floatarith floatarith
   1.140 +
   1.141 +fun interpret_form :: "form \<Rightarrow> real list \<Rightarrow> bool" where
   1.142 +"interpret_form (Bound x a b f) vs = (interpret_floatarith x vs \<in> { interpret_floatarith a vs .. interpret_floatarith b vs } \<longrightarrow> interpret_form f vs)" |
   1.143 +"interpret_form (Assign x a f) vs  = (interpret_floatarith x vs = interpret_floatarith a vs \<longrightarrow> interpret_form f vs)" |
   1.144 +"interpret_form (Less a b) vs      = (interpret_floatarith a vs < interpret_floatarith b vs)" |
   1.145 +"interpret_form (LessEqual a b) vs = (interpret_floatarith a vs \<le> interpret_floatarith b vs)" |
   1.146 +"interpret_form (AtLeastAtMost x a b) vs = (interpret_floatarith x vs \<in> { interpret_floatarith a vs .. interpret_floatarith b vs })"
   1.147 +
   1.148 +fun approx_form' and approx_form :: "nat \<Rightarrow> form \<Rightarrow> (float * float) option list \<Rightarrow> nat list \<Rightarrow> bool" where
   1.149 +"approx_form' prec f 0 n l u bs ss = approx_form prec f (bs[n := Some (l, u)]) ss" |
   1.150 +"approx_form' prec f (Suc s) n l u bs ss =
   1.151 +  (let m = (l + u) * Float 1 -1
   1.152 +   in approx_form' prec f s n l m bs ss \<and>
   1.153 +      approx_form' prec f s n m u bs ss)" |
   1.154 +"approx_form prec (Bound (Atom n) a b f) bs ss =
   1.155 +   (case (approx prec a bs, approx prec b bs)
   1.156 +   of (Some (l, _), Some (_, u)) \<Rightarrow> approx_form' prec f (ss ! n) n l u bs ss
   1.157 +    | _ \<Rightarrow> False)" |
   1.158 +"approx_form prec (Assign (Atom n) a f) bs ss =
   1.159 +   (case (approx prec a bs)
   1.160 +   of (Some (l, u)) \<Rightarrow> approx_form' prec f (ss ! n) n l u bs ss
   1.161 +    | _ \<Rightarrow> False)" |
   1.162 +"approx_form prec (Less a b) bs ss =
   1.163 +   (case (approx prec a bs, approx prec b bs)
   1.164 +   of (Some (l, u), Some (l', u')) \<Rightarrow> u < l'
   1.165 +    | _ \<Rightarrow> False)" |
   1.166 +"approx_form prec (LessEqual a b) bs ss =
   1.167 +   (case (approx prec a bs, approx prec b bs)
   1.168 +   of (Some (l, u), Some (l', u')) \<Rightarrow> u \<le> l'
   1.169 +    | _ \<Rightarrow> False)" |
   1.170 +"approx_form prec (AtLeastAtMost x a b) bs ss =
   1.171 +   (case (approx prec x bs, approx prec a bs, approx prec b bs)
   1.172 +   of (Some (lx, ux), Some (l, u), Some (l', u')) \<Rightarrow> u \<le> lx \<and> ux \<le> l'
   1.173 +    | _ \<Rightarrow> False)" |
   1.174 +"approx_form _ _ _ _ = False"
   1.175 +
   1.176 +lemma approx_form_approx_form':
   1.177 +  assumes "approx_form' prec f s n l u bs ss" and "x \<in> { real l .. real u }"
   1.178 +  obtains l' u' where "x \<in> { real l' .. real u' }"
   1.179 +  and "approx_form prec f (bs[n := Some (l', u')]) ss"
   1.180 +using assms proof (induct s arbitrary: l u)
   1.181 +  case 0
   1.182 +  from this(1)[of l u] this(2,3)
   1.183 +  show thesis by auto
   1.184 +next
   1.185 +  case (Suc s)
   1.186 +
   1.187 +  let ?m = "(l + u) * Float 1 -1"
   1.188 +  have "real l \<le> real ?m" and "real ?m \<le> real u"
   1.189 +    unfolding le_float_def using Suc.prems by auto
   1.190 +
   1.191 +  with `x \<in> { real l .. real u }`
   1.192 +  have "x \<in> { real l .. real ?m} \<or> x \<in> { real ?m .. real u }" by auto
   1.193 +  thus thesis
   1.194 +  proof (rule disjE)
   1.195 +    assume *: "x \<in> { real l .. real ?m }"
   1.196 +    with Suc.hyps[OF _ _ *] Suc.prems
   1.197 +    show thesis by (simp add: Let_def)
   1.198    next
   1.199 -    case False thus ?thesis using Atom by auto
   1.200 +    assume *: "x \<in> { real ?m .. real u }"
   1.201 +    with Suc.hyps[OF _ _ *] Suc.prems
   1.202 +    show thesis by (simp add: Let_def)
   1.203    qed
   1.204  qed
   1.205  
   1.206 -datatype inequality = Less floatarith floatarith
   1.207 -                    | LessEqual floatarith floatarith
   1.208 -
   1.209 -fun interpret_inequality :: "inequality \<Rightarrow> real list \<Rightarrow> bool" where
   1.210 -"interpret_inequality (Less a b) vs                   = (interpret_floatarith a vs < interpret_floatarith b vs)" |
   1.211 -"interpret_inequality (LessEqual a b) vs              = (interpret_floatarith a vs \<le> interpret_floatarith b vs)"
   1.212 -
   1.213 -fun approx_inequality :: "nat \<Rightarrow> inequality \<Rightarrow> (float * float) list \<Rightarrow> bool" where
   1.214 -"approx_inequality prec (Less a b) bs = (case (approx prec a bs, approx prec b bs) of (Some (l, u), Some (l', u')) \<Rightarrow> u < l' | _ \<Rightarrow> False)" |
   1.215 -"approx_inequality prec (LessEqual a b) bs = (case (approx prec a bs, approx prec b bs) of (Some (l, u), Some (l', u')) \<Rightarrow> u \<le> l' | _ \<Rightarrow> False)"
   1.216 -
   1.217 -lemma approx_inequality: fixes m :: nat assumes "bounded_by vs bs" and "approx_inequality prec eq bs"
   1.218 -  shows "interpret_inequality eq vs"
   1.219 -proof (cases eq)
   1.220 +lemma approx_form_aux:
   1.221 +  assumes "approx_form prec f vs ss"
   1.222 +  and "bounded_by xs vs"
   1.223 +  shows "interpret_form f xs"
   1.224 +using assms proof (induct f arbitrary: vs)
   1.225 +  case (Bound x a b f)
   1.226 +  then obtain n
   1.227 +    where x_eq: "x = Atom n" by (cases x) auto
   1.228 +
   1.229 +  with Bound.prems obtain l u' l' u
   1.230 +    where l_eq: "Some (l, u') = approx prec a vs"
   1.231 +    and u_eq: "Some (l', u) = approx prec b vs"
   1.232 +    and approx_form': "approx_form' prec f (ss ! n) n l u vs ss"
   1.233 +    by (cases "approx prec a vs", simp,
   1.234 +        cases "approx prec b vs", auto) blast
   1.235 +
   1.236 +  { assume "xs ! n \<in> { interpret_floatarith a xs .. interpret_floatarith b xs }"
   1.237 +    with approx[OF Bound.prems(2) l_eq] and approx[OF Bound.prems(2) u_eq]
   1.238 +    have "xs ! n \<in> { real l .. real u}" by auto
   1.239 +
   1.240 +    from approx_form_approx_form'[OF approx_form' this]
   1.241 +    obtain lx ux where bnds: "xs ! n \<in> { real lx .. real ux }"
   1.242 +      and approx_form: "approx_form prec f (vs[n := Some (lx, ux)]) ss" .
   1.243 +
   1.244 +    from `bounded_by xs vs` bnds
   1.245 +    have "bounded_by xs (vs[n := Some (lx, ux)])" by (rule bounded_by_update)
   1.246 +    with Bound.hyps[OF approx_form]
   1.247 +    have "interpret_form f xs" by blast }
   1.248 +  thus ?case using interpret_form.simps x_eq and interpret_floatarith.simps by simp
   1.249 +next
   1.250 +  case (Assign x a f)
   1.251 +  then obtain n
   1.252 +    where x_eq: "x = Atom n" by (cases x) auto
   1.253 +
   1.254 +  with Assign.prems obtain l u' l' u
   1.255 +    where bnd_eq: "Some (l, u) = approx prec a vs"
   1.256 +    and x_eq: "x = Atom n"
   1.257 +    and approx_form': "approx_form' prec f (ss ! n) n l u vs ss"
   1.258 +    by (cases "approx prec a vs") auto
   1.259 +
   1.260 +  { assume bnds: "xs ! n = interpret_floatarith a xs"
   1.261 +    with approx[OF Assign.prems(2) bnd_eq]
   1.262 +    have "xs ! n \<in> { real l .. real u}" by auto
   1.263 +    from approx_form_approx_form'[OF approx_form' this]
   1.264 +    obtain lx ux where bnds: "xs ! n \<in> { real lx .. real ux }"
   1.265 +      and approx_form: "approx_form prec f (vs[n := Some (lx, ux)]) ss" .
   1.266 +
   1.267 +    from `bounded_by xs vs` bnds
   1.268 +    have "bounded_by xs (vs[n := Some (lx, ux)])" by (rule bounded_by_update)
   1.269 +    with Assign.hyps[OF approx_form]
   1.270 +    have "interpret_form f xs" by blast }
   1.271 +  thus ?case using interpret_form.simps x_eq and interpret_floatarith.simps by simp
   1.272 +next
   1.273    case (Less a b)
   1.274 -  show ?thesis
   1.275 -  proof (cases "\<exists> u l u' l'. approx prec a bs = Some (l, u) \<and>
   1.276 -                             approx prec b bs = Some (l', u')")
   1.277 -    case True
   1.278 -    then obtain l u l' u' where a_approx: "approx prec a bs = Some (l, u)"
   1.279 -      and b_approx: "approx prec b bs = Some (l', u') " by auto
   1.280 -    with `approx_inequality prec eq bs` have "real u < real l'"
   1.281 -      unfolding Less approx_inequality.simps less_float_def by auto
   1.282 -    moreover from a_approx[symmetric] and b_approx[symmetric] and `bounded_by vs bs`
   1.283 -    have "interpret_floatarith a vs \<le> real u" and "real l' \<le> interpret_floatarith b vs"
   1.284 -      using approx by auto
   1.285 -    ultimately show ?thesis unfolding interpret_inequality.simps Less by auto
   1.286 -  next
   1.287 -    case False
   1.288 -    hence "approx prec a bs = None \<or> approx prec b bs = None"
   1.289 -      unfolding not_Some_eq[symmetric] by auto
   1.290 -    hence "\<not> approx_inequality prec eq bs" unfolding Less approx_inequality.simps
   1.291 -      by (cases "approx prec a bs = None", auto)
   1.292 -    thus ?thesis using assms by auto
   1.293 -  qed
   1.294 +  then obtain l u l' u'
   1.295 +    where l_eq: "Some (l, u) = approx prec a vs"
   1.296 +    and u_eq: "Some (l', u') = approx prec b vs"
   1.297 +    and inequality: "u < l'"
   1.298 +    by (cases "approx prec a vs", auto,
   1.299 +      cases "approx prec b vs", auto)
   1.300 +  from inequality[unfolded less_float_def] approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq]
   1.301 +  show ?case by auto
   1.302  next
   1.303    case (LessEqual a b)
   1.304 -  show ?thesis
   1.305 -  proof (cases "\<exists> u l u' l'. approx prec a bs = Some (l, u) \<and>
   1.306 -                             approx prec b bs = Some (l', u')")
   1.307 -    case True
   1.308 -    then obtain l u l' u' where a_approx: "approx prec a bs = Some (l, u)"
   1.309 -      and b_approx: "approx prec b bs = Some (l', u') " by auto
   1.310 -    with `approx_inequality prec eq bs` have "real u \<le> real l'"
   1.311 -      unfolding LessEqual approx_inequality.simps le_float_def by auto
   1.312 -    moreover from a_approx[symmetric] and b_approx[symmetric] and `bounded_by vs bs`
   1.313 -    have "interpret_floatarith a vs \<le> real u" and "real l' \<le> interpret_floatarith b vs"
   1.314 -      using approx by auto
   1.315 -    ultimately show ?thesis unfolding interpret_inequality.simps LessEqual by auto
   1.316 -  next
   1.317 -    case False
   1.318 -    hence "approx prec a bs = None \<or> approx prec b bs = None"
   1.319 -      unfolding not_Some_eq[symmetric] by auto
   1.320 -    hence "\<not> approx_inequality prec eq bs" unfolding LessEqual approx_inequality.simps
   1.321 -      by (cases "approx prec a bs = None", auto)
   1.322 -    thus ?thesis using assms by auto
   1.323 -  qed
   1.324 +  then obtain l u l' u'
   1.325 +    where l_eq: "Some (l, u) = approx prec a vs"
   1.326 +    and u_eq: "Some (l', u') = approx prec b vs"
   1.327 +    and inequality: "u \<le> l'"
   1.328 +    by (cases "approx prec a vs", auto,
   1.329 +      cases "approx prec b vs", auto)
   1.330 +  from inequality[unfolded le_float_def] approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq]
   1.331 +  show ?case by auto
   1.332 +next
   1.333 +  case (AtLeastAtMost x a b)
   1.334 +  then obtain lx ux l u l' u'
   1.335 +    where x_eq: "Some (lx, ux) = approx prec x vs"
   1.336 +    and l_eq: "Some (l, u) = approx prec a vs"
   1.337 +    and u_eq: "Some (l', u') = approx prec b vs"
   1.338 +    and inequality: "u \<le> lx \<and> ux \<le> l'"
   1.339 +    by (cases "approx prec x vs", auto,
   1.340 +      cases "approx prec a vs", auto,
   1.341 +      cases "approx prec b vs", auto, blast)
   1.342 +  from inequality[unfolded le_float_def] approx[OF AtLeastAtMost.prems(2) l_eq] approx[OF AtLeastAtMost.prems(2) u_eq] approx[OF AtLeastAtMost.prems(2) x_eq]
   1.343 +  show ?case by auto
   1.344  qed
   1.345  
   1.346 -lemma interpret_floatarith_divide: "interpret_floatarith (Mult a (Inverse b)) vs = (interpret_floatarith a vs) / (interpret_floatarith b vs)"
   1.347 -  unfolding real_divide_def interpret_floatarith.simps ..
   1.348 -
   1.349 -lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
   1.350 -  unfolding real_diff_def interpret_floatarith.simps ..
   1.351 -
   1.352 -lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
   1.353 -  sin (interpret_floatarith a vs)"
   1.354 -  unfolding sin_cos_eq interpret_floatarith.simps
   1.355 -            interpret_floatarith_divide interpret_floatarith_diff real_diff_def
   1.356 -  by auto
   1.357 -
   1.358 -lemma interpret_floatarith_tan:
   1.359 -  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
   1.360 -   tan (interpret_floatarith a vs)"
   1.361 -  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def real_divide_def
   1.362 -  by auto
   1.363 -
   1.364 -lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
   1.365 -  unfolding powr_def interpret_floatarith.simps ..
   1.366 -
   1.367 -lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
   1.368 -  unfolding log_def interpret_floatarith.simps real_divide_def ..
   1.369 -
   1.370 -lemma interpret_floatarith_num:
   1.371 -  shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
   1.372 -  and "interpret_floatarith (Num (Float 1 0)) vs = 1"
   1.373 -  and "interpret_floatarith (Num (Float (number_of a) 0)) vs = number_of a" by auto
   1.374 +lemma approx_form:
   1.375 +  assumes "n = length xs"
   1.376 +  assumes "approx_form prec f (replicate n None) ss"
   1.377 +  shows "interpret_form f xs"
   1.378 +  using approx_form_aux[OF _ bounded_by_None] assms by auto
   1.379  
   1.380  subsection {* Implement proof method \texttt{approximation} *}
   1.381  
   1.382 -lemma bounded_divl: assumes "real a / real b \<le> x" shows "real (float_divl p a b) \<le> x" by (rule order_trans[OF _ assms], rule float_divl)
   1.383 -lemma bounded_divr: assumes "x \<le> real a / real b" shows "x \<le> real (float_divr p a b)" by (rule order_trans[OF assms _], rule float_divr)
   1.384 -lemma bounded_num: shows "real (Float 5 1) = 10" and "real (Float 0 0) = 0" and "real (Float 1 0) = 1" and "real (Float (number_of n) 0) = (number_of n)"
   1.385 -                     and "0 * pow2 e = real (Float 0 e)" and "1 * pow2 e = real (Float 1 e)" and "number_of m * pow2 e = real (Float (number_of m) e)"
   1.386 -                     and "real (Float (number_of A) (int B)) = (number_of A) * 2^B"
   1.387 -                     and "real (Float 1 (int B)) = 2^B"
   1.388 -                     and "real (Float (number_of A) (- int B)) = (number_of A) / 2^B"
   1.389 -                     and "real (Float 1 (- int B)) = 1 / 2^B"
   1.390 -  by (auto simp add: real_of_float_simp pow2_def real_divide_def)
   1.391 -
   1.392 -lemmas bounded_by_equations = bounded_by_Cons bounded_by_Nil float_power bounded_divl bounded_divr bounded_num HOL.simp_thms
   1.393 -lemmas interpret_inequality_equations = interpret_inequality.simps interpret_floatarith.simps interpret_floatarith_num
   1.394 +lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
   1.395    interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
   1.396    interpret_floatarith_sin
   1.397  
   1.398 @@ -2543,9 +2645,9 @@
   1.399  @{code_datatype float = Float}
   1.400  @{code_datatype floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
   1.401                             | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Atom | Num }
   1.402 -@{code_datatype inequality = Less | LessEqual }
   1.403 -
   1.404 -val approx_inequality = @{code approx_inequality}
   1.405 +@{code_datatype form = Bound | Assign | Less | LessEqual | AtLeastAtMost}
   1.406 +
   1.407 +val approx_form = @{code approx_form}
   1.408  val approx' = @{code approx'}
   1.409  
   1.410  end
   1.411 @@ -2566,103 +2668,109 @@
   1.412          "Float'_Arith.Exp" and "Float'_Arith.Ln" and "Float'_Arith.Power/ (_,/ _)" and
   1.413          "Float'_Arith.Atom" and "Float'_Arith.Num")
   1.414  
   1.415 -code_type inequality (Eval "Float'_Arith.inequality")
   1.416 -code_const Less and LessEqual (Eval "Float'_Arith.Less/ (_,/ _)" and "Float'_Arith.LessEqual/ (_,/ _)")
   1.417 -
   1.418 -code_const approx_inequality (Eval "Float'_Arith.approx'_inequality")
   1.419 -code_const approx' (Eval "Float'_Arith.approx''")
   1.420 +code_type form (Eval "Float'_Arith.form")
   1.421 +code_const Bound and Assign and Less and LessEqual and AtLeastAtMost
   1.422 +      (Eval "Float'_Arith.Bound/ (_,/ _,/ _,/ _)" and "Float'_Arith.Assign/ (_,/ _,/ _)" and
   1.423 +            "Float'_Arith.Less/ (_,/ _)" and "Float'_Arith.LessEqual/ (_,/ _)"  and
   1.424 +            "Float'_Arith.AtLeastAtMost/ (_,/ _,/ _)")
   1.425 +
   1.426 +code_const approx_form (Eval "Float'_Arith.approx'_form")
   1.427 +code_const approx' (Eval "Float'_Arith.approx'")
   1.428  
   1.429  ML {*
   1.430 -  val ineq_equations = PureThy.get_thms @{theory} "interpret_inequality_equations";
   1.431 -  val bounded_by_equations = PureThy.get_thms @{theory} "bounded_by_equations";
   1.432 -  val bounded_by_simpset = (HOL_basic_ss addsimps bounded_by_equations)
   1.433 -
   1.434 -  fun reify_ineq ctxt i = (fn st =>
   1.435 +  fun reorder_bounds_tac i prems =
   1.436      let
   1.437 -      val to = HOLogic.dest_Trueprop (Logic.strip_imp_concl (List.nth (prems_of st, i - 1)))
   1.438 -    in (Reflection.genreify_tac ctxt ineq_equations (SOME to) i) st
   1.439 -    end)
   1.440 -
   1.441 -  fun rule_ineq ctxt prec i thm = let
   1.442 -    fun conv_num typ = HOLogic.dest_number #> snd #> HOLogic.mk_number typ
   1.443 -    val to_natc = conv_num @{typ "nat"} #> Thm.cterm_of (ProofContext.theory_of ctxt)
   1.444 -    val to_nat = conv_num @{typ "nat"}
   1.445 -    val to_int = conv_num @{typ "int"}
   1.446 -    fun int_to_float A = @{term "Float"} $ to_int A $ @{term "0 :: int"}
   1.447 -
   1.448 -    val prec' = to_nat prec
   1.449 -
   1.450 -    fun bot_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
   1.451 -                   = @{term "Float"} $ to_int mantisse $ to_int exp
   1.452 -      | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
   1.453 -                   = @{term "Float"} $ to_int mantisse $ (@{term "uminus :: int \<Rightarrow> int"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp))
   1.454 -      | bot_float (Const (@{const_name "times"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
   1.455 -                   = @{term "Float"} $ to_int mantisse $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
   1.456 -      | bot_float (Const (@{const_name "divide"}, _) $ A $ (@{term "power 10 :: nat \<Rightarrow> real"} $ exp))
   1.457 -                   = @{term "float_divl"} $ prec' $ (int_to_float A) $ (@{term "power (Float 5 1)"} $ to_nat exp)
   1.458 -      | bot_float (Const (@{const_name "divide"}, _) $ A $ B)
   1.459 -                   = @{term "float_divl"} $ prec' $ int_to_float A $ int_to_float B
   1.460 -      | bot_float (@{term "power 2 :: nat \<Rightarrow> real"} $ exp)
   1.461 -                   = @{term "Float 1"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
   1.462 -      | bot_float A = int_to_float A
   1.463 -
   1.464 -    fun top_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
   1.465 -                   = @{term "Float"} $ to_int mantisse $ to_int exp
   1.466 -      | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
   1.467 -                   = @{term "Float"} $ to_int mantisse $ (@{term "uminus :: int \<Rightarrow> int"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp))
   1.468 -      | top_float (Const (@{const_name "times"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
   1.469 -                   = @{term "Float"} $ to_int mantisse $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
   1.470 -      | top_float (Const (@{const_name "divide"}, _) $ A $ (@{term "power 10 :: nat \<Rightarrow> real"} $ exp))
   1.471 -                   = @{term "float_divr"} $ prec' $ (int_to_float A) $ (@{term "power (Float 5 1)"} $ to_nat exp)
   1.472 -      | top_float (Const (@{const_name "divide"}, _) $ A $ B)
   1.473 -                   = @{term "float_divr"} $ prec' $ int_to_float A $ int_to_float B
   1.474 -      | top_float (@{term "power 2 :: nat \<Rightarrow> real"} $ exp)
   1.475 -                   = @{term "Float 1"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
   1.476 -      | top_float A = int_to_float A
   1.477 -
   1.478 -    val goal' : term = List.nth (prems_of thm, i - 1)
   1.479 -
   1.480 -    fun lift_bnd (t as (Const (@{const_name "op &"}, _) $
   1.481 -                        (Const (@{const_name "less_eq"}, _) $
   1.482 -                         bottom $ (Free (name, _))) $
   1.483 -                        (Const (@{const_name "less_eq"}, _) $ _ $ top)))
   1.484 -         = ((name, HOLogic.mk_prod (bot_float bottom, top_float top))
   1.485 -            handle TERM (txt, ts) => raise TERM ("Invalid bound number format: " ^
   1.486 -                                  (Syntax.string_of_term ctxt t), [t]))
   1.487 -      | lift_bnd t = raise TERM ("Premisse needs format '<num> <= <var> & <var> <= <num>', but found " ^
   1.488 -                                 (Syntax.string_of_term ctxt t), [t])
   1.489 -    val bound_eqs = map (HOLogic.dest_Trueprop #> lift_bnd)  (Logic.strip_imp_prems goal')
   1.490 -
   1.491 -    fun lift_var (Free (varname, _)) = (case AList.lookup (op =) bound_eqs varname of
   1.492 -                                          SOME bound => bound
   1.493 -                                        | NONE => raise TERM ("No bound equations found for " ^ varname, []))
   1.494 -      | lift_var t = raise TERM ("Can not convert expression " ^
   1.495 -                                 (Syntax.string_of_term ctxt t), [t])
   1.496 -
   1.497 -    val _ $ vs = HOLogic.dest_Trueprop (Logic.strip_imp_concl goal')
   1.498 -
   1.499 -    val bs = (HOLogic.dest_list #> map lift_var #> HOLogic.mk_list @{typ "float * float"}) vs
   1.500 -    val map = [(@{cpat "?prec::nat"}, to_natc prec),
   1.501 -               (@{cpat "?bs::(float * float) list"}, Thm.cterm_of (ProofContext.theory_of ctxt) bs)]
   1.502 -  in rtac (Thm.instantiate ([], map) @{thm "approx_inequality"}) i thm end
   1.503 -
   1.504 -  val eval_tac = CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
   1.505 -
   1.506 +      fun variable_of_bound (Const ("Trueprop", _) $
   1.507 +                             (Const (@{const_name "op :"}, _) $
   1.508 +                              Free (name, _) $ _)) = name
   1.509 +        | variable_of_bound (Const ("Trueprop", _) $
   1.510 +                             (Const ("op =", _) $
   1.511 +                              Free (name, _) $ _)) = name
   1.512 +        | variable_of_bound t = raise TERM ("variable_of_bound", [t])
   1.513 +
   1.514 +      val variable_bounds
   1.515 +        = map (` (variable_of_bound o prop_of)) prems
   1.516 +
   1.517 +      fun add_deps (name, bnds)
   1.518 +        = Graph.add_deps_acyclic
   1.519 +            (name, remove (op =) name (Term.add_free_names (prop_of bnds) []))
   1.520 +      val order = Graph.empty
   1.521 +                  |> fold Graph.new_node variable_bounds
   1.522 +                  |> fold add_deps variable_bounds
   1.523 +                  |> Graph.topological_order |> rev
   1.524 +                  |> map_filter (AList.lookup (op =) variable_bounds)
   1.525 +
   1.526 +      fun prepend_prem th tac
   1.527 +        = tac THEN rtac (th RSN (2, @{thm mp})) i
   1.528 +    in
   1.529 +      fold prepend_prem order all_tac
   1.530 +    end
   1.531 +
   1.532 +  (* Should be in HOL.thy ? *)
   1.533    fun gen_eval_tac conv ctxt = CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
   1.534                                 THEN' rtac TrueI
   1.535  
   1.536 +  val form_equations = PureThy.get_thms @{theory} "interpret_form_equations";
   1.537 +
   1.538 +  fun rewrite_interpret_form_tac ctxt prec splitting i st = let
   1.539 +      val vs = nth (prems_of st) (i - 1)
   1.540 +               |> Logic.strip_imp_concl
   1.541 +               |> HOLogic.dest_Trueprop
   1.542 +               |> Term.strip_comb |> snd |> List.last
   1.543 +               |> HOLogic.dest_list
   1.544 +      val n = vs |> length
   1.545 +              |> HOLogic.mk_number @{typ nat}
   1.546 +              |> Thm.cterm_of (ProofContext.theory_of ctxt)
   1.547 +      val p = prec
   1.548 +              |> HOLogic.mk_number @{typ nat}
   1.549 +              |> Thm.cterm_of (ProofContext.theory_of ctxt)
   1.550 +      val s = vs
   1.551 +              |> map (fn Free (name, typ) =>
   1.552 +                      case AList.lookup (op =) splitting name of
   1.553 +                        SOME s => HOLogic.mk_number @{typ nat} s
   1.554 +                      | NONE => @{term "0 :: nat"})
   1.555 +              |> HOLogic.mk_list @{typ nat}
   1.556 +              |> Thm.cterm_of (ProofContext.theory_of ctxt)
   1.557 +    in
   1.558 +      rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
   1.559 +                                  (@{cpat "?prec::nat"}, p),
   1.560 +                                  (@{cpat "?ss::nat list"}, s)])
   1.561 +           @{thm "approx_form"}) i st
   1.562 +    end
   1.563 +
   1.564 +  (* copied from Tools/induct.ML should probably in args.ML *)
   1.565 +  val free = Args.context -- Args.term >> (fn (_, Free (n, t)) => n | (ctxt, t) =>
   1.566 +    error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
   1.567 +
   1.568  *}
   1.569  
   1.570 +lemma intervalE: "a \<le> x \<and> x \<le> b \<Longrightarrow> \<lbrakk> x \<in> { a .. b } \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   1.571 +  by auto
   1.572 +
   1.573 +lemma meta_eqE: "x \<equiv> a \<Longrightarrow> \<lbrakk> x = a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   1.574 +  by auto
   1.575 +
   1.576  method_setup approximation = {*
   1.577 -  Args.term >>
   1.578 -  (fn prec => fn ctxt =>
   1.579 +  Scan.lift (OuterParse.nat) --
   1.580 +  Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
   1.581 +    |-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
   1.582 +  >>
   1.583 +  (fn (prec, splitting) => fn ctxt =>
   1.584      SIMPLE_METHOD' (fn i =>
   1.585 -     (DETERM (reify_ineq ctxt i)
   1.586 -      THEN rule_ineq ctxt prec i
   1.587 -      THEN Simplifier.asm_full_simp_tac bounded_by_simpset i
   1.588 -      THEN (TRY (filter_prems_tac (fn t => false) i))
   1.589 -      THEN (gen_eval_tac eval_oracle ctxt) i)))
   1.590 -*} "real number approximation"
   1.591 +      REPEAT (FIRST' [etac @{thm intervalE},
   1.592 +                      etac @{thm meta_eqE},
   1.593 +                      rtac @{thm impI}] i)
   1.594 +      THEN METAHYPS (reorder_bounds_tac i) i
   1.595 +      THEN TRY (filter_prems_tac (K false) i)
   1.596 +      THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
   1.597 +      THEN print_tac "approximation"
   1.598 +      THEN rewrite_interpret_form_tac ctxt prec splitting i
   1.599 +      THEN simp_tac @{simpset} i
   1.600 +      THEN gen_eval_tac eval_oracle ctxt i))
   1.601 + *} "real number approximation"
   1.602 +
   1.603 +lemma "\<phi> \<in> {0..1 :: real} \<Longrightarrow> \<phi> < \<phi> + 0.7"
   1.604 +  by (approximation 10 splitting: "\<phi>" = 1)
   1.605  
   1.606  ML {*
   1.607    fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs)
   1.608 @@ -2733,7 +2841,7 @@
   1.609  
   1.610    fun approx prec ctxt t = let val t = realify t in
   1.611            t
   1.612 -       |> Reflection.genreif ctxt ineq_equations
   1.613 +       |> Reflection.genreif ctxt form_equations
   1.614         |> prop_of
   1.615         |> HOLogic.dest_Trueprop
   1.616         |> HOLogic.dest_eq |> snd
     2.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Mon Jun 08 18:37:35 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Jun 25 18:12:40 2009 +0200
     2.3 @@ -40,6 +40,9 @@
     2.4  lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
     2.5    by (approximation 10)
     2.6  
     2.7 +lemma "x \<in> {0.5 .. 4.5} \<longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
     2.8 +  by (approximation 10)
     2.9 +
    2.10  lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
    2.11    by (approximation 20)
    2.12  
    2.13 @@ -49,5 +52,9 @@
    2.14  lemma "3.2 \<le> x \<and> x \<le> 6.2 \<Longrightarrow> sin x \<le> 0"
    2.15    by (approximation 9)
    2.16  
    2.17 +lemma
    2.18 +  defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180"
    2.19 +  shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
    2.20 +  using assms by (approximation 80)
    2.21 +
    2.22  end
    2.23 -