# HG changeset patch
# User hoelzl
# Date 1245946360 -7200
# Node ID 64dea9a15031aedd27e9ca63b494a0dbd8420917
# Parent  a6b800855cdd14b6eb3d4191689dae52f44f7a76
Improved computation of bounds and implemented interval splitting for 'approximation'.

diff -r a6b800855cdd -r 64dea9a15031 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon Jun 08 18:37:35 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Jun 25 18:12:40 2009 +0200
@@ -2088,6 +2088,36 @@
 "interpret_floatarith (Num f) vs      = real f" |
 "interpret_floatarith (Atom n) vs     = vs ! n"
 
+lemma interpret_floatarith_divide: "interpret_floatarith (Mult a (Inverse b)) vs = (interpret_floatarith a vs) / (interpret_floatarith b vs)"
+  unfolding real_divide_def interpret_floatarith.simps ..
+
+lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
+  unfolding real_diff_def interpret_floatarith.simps ..
+
+lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
+  sin (interpret_floatarith a vs)"
+  unfolding sin_cos_eq interpret_floatarith.simps
+            interpret_floatarith_divide interpret_floatarith_diff real_diff_def
+  by auto
+
+lemma interpret_floatarith_tan:
+  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
+   tan (interpret_floatarith a vs)"
+  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def real_divide_def
+  by auto
+
+lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
+  unfolding powr_def interpret_floatarith.simps ..
+
+lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
+  unfolding log_def interpret_floatarith.simps real_divide_def ..
+
+lemma interpret_floatarith_num:
+  shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
+  and "interpret_floatarith (Num (Float 1 0)) vs = 1"
+  and "interpret_floatarith (Num (Float (number_of a) 0)) vs = number_of a" by auto
+
+
 subsection "Implement approximation function"
 
 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
@@ -2103,32 +2133,47 @@
 "lift_un' (Some (l1, u1)) f = Some (f l1 u1)" |
 "lift_un' b f = None"
 
-fun bounded_by :: "real list \<Rightarrow> (float * float) list \<Rightarrow> bool " where
-bounded_by_Cons: "bounded_by (v#vs) ((l, u)#bs) = ((real l \<le> v \<and> v \<le> real u) \<and> bounded_by vs bs)" |
-bounded_by_Nil: "bounded_by [] [] = True" |
-"bounded_by _ _ = False"
-
-lemma bounded_by: assumes "bounded_by vs bs" and "i < length bs"
-  shows "real (fst (bs ! i)) \<le> vs ! i \<and> vs ! i \<le> real (snd (bs ! i))"
-  using `bounded_by vs bs` and `i < length bs`
-proof (induct arbitrary: i rule: bounded_by.induct)
-  fix v :: real and vs :: "real list" and l u :: float and bs :: "(float * float) list" and i :: nat
-  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))"
-  assume bounded: "bounded_by (v # vs) ((l, u) # bs)" and length: "i < length ((l, u) # bs)"
-  show "real (fst (((l, u) # bs) ! i)) \<le> (v # vs) ! i \<and> (v # vs) ! i \<le> real (snd (((l, u) # bs) ! i))"
-  proof (cases i)
-    case 0
-    show ?thesis using bounded unfolding 0 nth_Cons_0 fst_conv snd_conv bounded_by.simps ..
-  next
-    case (Suc i) with length have "i < length bs" by auto
-    show ?thesis unfolding Suc nth_Cons_Suc bounded_by.simps
-      using hyp[OF bounded[unfolded bounded_by.simps, THEN conjunct2] `i < length bs`] .
-  qed
-qed auto
-
-fun approx approx' :: "nat \<Rightarrow> floatarith \<Rightarrow> (float * float) list \<Rightarrow> (float * float) option" where
+definition
+"bounded_by xs vs \<longleftrightarrow>
+  (\<forall> i < length vs. case vs ! i of None \<Rightarrow> True
+         | Some (l, u) \<Rightarrow> xs ! i \<in> { real l .. real u })"
+
+lemma bounded_byE:
+  assumes "bounded_by xs vs"
+  shows "\<And> i. i < length vs \<Longrightarrow> case vs ! i of None \<Rightarrow> True
+         | Some (l, u) \<Rightarrow> xs ! i \<in> { real l .. real u }"
+  using assms bounded_by_def by blast
+
+lemma bounded_by_update:
+  assumes "bounded_by xs vs"
+  and bnd: "xs ! i \<in> { real l .. real u }"
+  shows "bounded_by xs (vs[i := Some (l,u)])"
+proof -
+{ fix j
+  let ?vs = "vs[i := Some (l,u)]"
+  assume "j < length ?vs" hence [simp]: "j < length vs" by simp
+  have "case ?vs ! j of None \<Rightarrow> True | Some (l, u) \<Rightarrow> xs ! j \<in> { real l .. real u }"
+  proof (cases "?vs ! j")
+    case (Some b)
+    thus ?thesis
+    proof (cases "i = j")
+      case True
+      thus ?thesis using `?vs ! j = Some b` and bnd by auto
+    next
+      case False
+      thus ?thesis using `bounded_by xs vs` unfolding bounded_by_def by auto
+    qed
+  qed auto }
+  thus ?thesis unfolding bounded_by_def by auto
+qed
+
+lemma bounded_by_None:
+  shows "bounded_by xs (replicate (length xs) None)"
+  unfolding bounded_by_def by auto
+
+fun approx approx' :: "nat \<Rightarrow> floatarith \<Rightarrow> (float * float) option list \<Rightarrow> (float * float) option" where
 "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)" |
-"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))" |
+"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))" |
 "approx prec (Minus a) bs   = lift_un' (approx' prec a bs) (\<lambda> l u. (-u, -l))" |
 "approx prec (Mult a b) bs  = lift_bin' (approx' prec a bs) (approx' prec b bs)
                                     (\<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,
@@ -2145,7 +2190,7 @@
 "approx prec (Ln a) bs      = lift_un (approx' prec a bs) (\<lambda> l u. (lb_ln prec l, ub_ln prec u))" |
 "approx prec (Power a n) bs = lift_un' (approx' prec a bs) (float_power_bnds n)" |
 "approx prec (Num f) bs     = Some (f, f)" |
-"approx prec (Atom i) bs    = (if i < length bs then Some (bs ! i) else None)"
+"approx prec (Atom i) bs    = (if i < length bs then bs ! i else None)"
 
 lemma lift_bin'_ex:
   assumes lift_bin'_Some: "Some (l, u) = lift_bin' a b f"
@@ -2421,118 +2466,175 @@
 next case (Num f) thus ?case by auto
 next
   case (Atom n)
-  show ?case
-  proof (cases "n < length vs")
-    case True
-    with Atom have "vs ! n = (l, u)" by auto
-    thus ?thesis using bounded_by[OF assms(1) True] by auto
+  from this[symmetric] `bounded_by xs vs`[THEN bounded_byE, of n]
+  show ?case by (cases "n < length vs", auto)
+qed
+
+datatype form = Bound floatarith floatarith floatarith form
+              | Assign floatarith floatarith form
+              | Less floatarith floatarith
+              | LessEqual floatarith floatarith
+              | AtLeastAtMost floatarith floatarith floatarith
+
+fun interpret_form :: "form \<Rightarrow> real list \<Rightarrow> bool" where
+"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)" |
+"interpret_form (Assign x a f) vs  = (interpret_floatarith x vs = interpret_floatarith a vs \<longrightarrow> interpret_form f vs)" |
+"interpret_form (Less a b) vs      = (interpret_floatarith a vs < interpret_floatarith b vs)" |
+"interpret_form (LessEqual a b) vs = (interpret_floatarith a vs \<le> interpret_floatarith b vs)" |
+"interpret_form (AtLeastAtMost x a b) vs = (interpret_floatarith x vs \<in> { interpret_floatarith a vs .. interpret_floatarith b vs })"
+
+fun approx_form' and approx_form :: "nat \<Rightarrow> form \<Rightarrow> (float * float) option list \<Rightarrow> nat list \<Rightarrow> bool" where
+"approx_form' prec f 0 n l u bs ss = approx_form prec f (bs[n := Some (l, u)]) ss" |
+"approx_form' prec f (Suc s) n l u bs ss =
+  (let m = (l + u) * Float 1 -1
+   in approx_form' prec f s n l m bs ss \<and>
+      approx_form' prec f s n m u bs ss)" |
+"approx_form prec (Bound (Atom n) a b f) bs ss =
+   (case (approx prec a bs, approx prec b bs)
+   of (Some (l, _), Some (_, u)) \<Rightarrow> approx_form' prec f (ss ! n) n l u bs ss
+    | _ \<Rightarrow> False)" |
+"approx_form prec (Assign (Atom n) a f) bs ss =
+   (case (approx prec a bs)
+   of (Some (l, u)) \<Rightarrow> approx_form' prec f (ss ! n) n l u bs ss
+    | _ \<Rightarrow> False)" |
+"approx_form prec (Less a b) bs ss =
+   (case (approx prec a bs, approx prec b bs)
+   of (Some (l, u), Some (l', u')) \<Rightarrow> u < l'
+    | _ \<Rightarrow> False)" |
+"approx_form prec (LessEqual a b) bs ss =
+   (case (approx prec a bs, approx prec b bs)
+   of (Some (l, u), Some (l', u')) \<Rightarrow> u \<le> l'
+    | _ \<Rightarrow> False)" |
+"approx_form prec (AtLeastAtMost x a b) bs ss =
+   (case (approx prec x bs, approx prec a bs, approx prec b bs)
+   of (Some (lx, ux), Some (l, u), Some (l', u')) \<Rightarrow> u \<le> lx \<and> ux \<le> l'
+    | _ \<Rightarrow> False)" |
+"approx_form _ _ _ _ = False"
+
+lemma approx_form_approx_form':
+  assumes "approx_form' prec f s n l u bs ss" and "x \<in> { real l .. real u }"
+  obtains l' u' where "x \<in> { real l' .. real u' }"
+  and "approx_form prec f (bs[n := Some (l', u')]) ss"
+using assms proof (induct s arbitrary: l u)
+  case 0
+  from this(1)[of l u] this(2,3)
+  show thesis by auto
+next
+  case (Suc s)
+
+  let ?m = "(l + u) * Float 1 -1"
+  have "real l \<le> real ?m" and "real ?m \<le> real u"
+    unfolding le_float_def using Suc.prems by auto
+
+  with `x \<in> { real l .. real u }`
+  have "x \<in> { real l .. real ?m} \<or> x \<in> { real ?m .. real u }" by auto
+  thus thesis
+  proof (rule disjE)
+    assume *: "x \<in> { real l .. real ?m }"
+    with Suc.hyps[OF _ _ *] Suc.prems
+    show thesis by (simp add: Let_def)
   next
-    case False thus ?thesis using Atom by auto
+    assume *: "x \<in> { real ?m .. real u }"
+    with Suc.hyps[OF _ _ *] Suc.prems
+    show thesis by (simp add: Let_def)
   qed
 qed
 
-datatype inequality = Less floatarith floatarith
-                    | LessEqual floatarith floatarith
-
-fun interpret_inequality :: "inequality \<Rightarrow> real list \<Rightarrow> bool" where
-"interpret_inequality (Less a b) vs                   = (interpret_floatarith a vs < interpret_floatarith b vs)" |
-"interpret_inequality (LessEqual a b) vs              = (interpret_floatarith a vs \<le> interpret_floatarith b vs)"
-
-fun approx_inequality :: "nat \<Rightarrow> inequality \<Rightarrow> (float * float) list \<Rightarrow> bool" where
-"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)" |
-"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)"
-
-lemma approx_inequality: fixes m :: nat assumes "bounded_by vs bs" and "approx_inequality prec eq bs"
-  shows "interpret_inequality eq vs"
-proof (cases eq)
+lemma approx_form_aux:
+  assumes "approx_form prec f vs ss"
+  and "bounded_by xs vs"
+  shows "interpret_form f xs"
+using assms proof (induct f arbitrary: vs)
+  case (Bound x a b f)
+  then obtain n
+    where x_eq: "x = Atom n" by (cases x) auto
+
+  with Bound.prems obtain l u' l' u
+    where l_eq: "Some (l, u') = approx prec a vs"
+    and u_eq: "Some (l', u) = approx prec b vs"
+    and approx_form': "approx_form' prec f (ss ! n) n l u vs ss"
+    by (cases "approx prec a vs", simp,
+        cases "approx prec b vs", auto) blast
+
+  { assume "xs ! n \<in> { interpret_floatarith a xs .. interpret_floatarith b xs }"
+    with approx[OF Bound.prems(2) l_eq] and approx[OF Bound.prems(2) u_eq]
+    have "xs ! n \<in> { real l .. real u}" by auto
+
+    from approx_form_approx_form'[OF approx_form' this]
+    obtain lx ux where bnds: "xs ! n \<in> { real lx .. real ux }"
+      and approx_form: "approx_form prec f (vs[n := Some (lx, ux)]) ss" .
+
+    from `bounded_by xs vs` bnds
+    have "bounded_by xs (vs[n := Some (lx, ux)])" by (rule bounded_by_update)
+    with Bound.hyps[OF approx_form]
+    have "interpret_form f xs" by blast }
+  thus ?case using interpret_form.simps x_eq and interpret_floatarith.simps by simp
+next
+  case (Assign x a f)
+  then obtain n
+    where x_eq: "x = Atom n" by (cases x) auto
+
+  with Assign.prems obtain l u' l' u
+    where bnd_eq: "Some (l, u) = approx prec a vs"
+    and x_eq: "x = Atom n"
+    and approx_form': "approx_form' prec f (ss ! n) n l u vs ss"
+    by (cases "approx prec a vs") auto
+
+  { assume bnds: "xs ! n = interpret_floatarith a xs"
+    with approx[OF Assign.prems(2) bnd_eq]
+    have "xs ! n \<in> { real l .. real u}" by auto
+    from approx_form_approx_form'[OF approx_form' this]
+    obtain lx ux where bnds: "xs ! n \<in> { real lx .. real ux }"
+      and approx_form: "approx_form prec f (vs[n := Some (lx, ux)]) ss" .
+
+    from `bounded_by xs vs` bnds
+    have "bounded_by xs (vs[n := Some (lx, ux)])" by (rule bounded_by_update)
+    with Assign.hyps[OF approx_form]
+    have "interpret_form f xs" by blast }
+  thus ?case using interpret_form.simps x_eq and interpret_floatarith.simps by simp
+next
   case (Less a b)
-  show ?thesis
-  proof (cases "\<exists> u l u' l'. approx prec a bs = Some (l, u) \<and>
-                             approx prec b bs = Some (l', u')")
-    case True
-    then obtain l u l' u' where a_approx: "approx prec a bs = Some (l, u)"
-      and b_approx: "approx prec b bs = Some (l', u') " by auto
-    with `approx_inequality prec eq bs` have "real u < real l'"
-      unfolding Less approx_inequality.simps less_float_def by auto
-    moreover from a_approx[symmetric] and b_approx[symmetric] and `bounded_by vs bs`
-    have "interpret_floatarith a vs \<le> real u" and "real l' \<le> interpret_floatarith b vs"
-      using approx by auto
-    ultimately show ?thesis unfolding interpret_inequality.simps Less by auto
-  next
-    case False
-    hence "approx prec a bs = None \<or> approx prec b bs = None"
-      unfolding not_Some_eq[symmetric] by auto
-    hence "\<not> approx_inequality prec eq bs" unfolding Less approx_inequality.simps
-      by (cases "approx prec a bs = None", auto)
-    thus ?thesis using assms by auto
-  qed
+  then obtain l u l' u'
+    where l_eq: "Some (l, u) = approx prec a vs"
+    and u_eq: "Some (l', u') = approx prec b vs"
+    and inequality: "u < l'"
+    by (cases "approx prec a vs", auto,
+      cases "approx prec b vs", auto)
+  from inequality[unfolded less_float_def] approx[OF Less.prems(2) l_eq] approx[OF Less.prems(2) u_eq]
+  show ?case by auto
 next
   case (LessEqual a b)
-  show ?thesis
-  proof (cases "\<exists> u l u' l'. approx prec a bs = Some (l, u) \<and>
-                             approx prec b bs = Some (l', u')")
-    case True
-    then obtain l u l' u' where a_approx: "approx prec a bs = Some (l, u)"
-      and b_approx: "approx prec b bs = Some (l', u') " by auto
-    with `approx_inequality prec eq bs` have "real u \<le> real l'"
-      unfolding LessEqual approx_inequality.simps le_float_def by auto
-    moreover from a_approx[symmetric] and b_approx[symmetric] and `bounded_by vs bs`
-    have "interpret_floatarith a vs \<le> real u" and "real l' \<le> interpret_floatarith b vs"
-      using approx by auto
-    ultimately show ?thesis unfolding interpret_inequality.simps LessEqual by auto
-  next
-    case False
-    hence "approx prec a bs = None \<or> approx prec b bs = None"
-      unfolding not_Some_eq[symmetric] by auto
-    hence "\<not> approx_inequality prec eq bs" unfolding LessEqual approx_inequality.simps
-      by (cases "approx prec a bs = None", auto)
-    thus ?thesis using assms by auto
-  qed
+  then obtain l u l' u'
+    where l_eq: "Some (l, u) = approx prec a vs"
+    and u_eq: "Some (l', u') = approx prec b vs"
+    and inequality: "u \<le> l'"
+    by (cases "approx prec a vs", auto,
+      cases "approx prec b vs", auto)
+  from inequality[unfolded le_float_def] approx[OF LessEqual.prems(2) l_eq] approx[OF LessEqual.prems(2) u_eq]
+  show ?case by auto
+next
+  case (AtLeastAtMost x a b)
+  then obtain lx ux l u l' u'
+    where x_eq: "Some (lx, ux) = approx prec x vs"
+    and l_eq: "Some (l, u) = approx prec a vs"
+    and u_eq: "Some (l', u') = approx prec b vs"
+    and inequality: "u \<le> lx \<and> ux \<le> l'"
+    by (cases "approx prec x vs", auto,
+      cases "approx prec a vs", auto,
+      cases "approx prec b vs", auto, blast)
+  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]
+  show ?case by auto
 qed
 
-lemma interpret_floatarith_divide: "interpret_floatarith (Mult a (Inverse b)) vs = (interpret_floatarith a vs) / (interpret_floatarith b vs)"
-  unfolding real_divide_def interpret_floatarith.simps ..
-
-lemma interpret_floatarith_diff: "interpret_floatarith (Add a (Minus b)) vs = (interpret_floatarith a vs) - (interpret_floatarith b vs)"
-  unfolding real_diff_def interpret_floatarith.simps ..
-
-lemma interpret_floatarith_sin: "interpret_floatarith (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) vs =
-  sin (interpret_floatarith a vs)"
-  unfolding sin_cos_eq interpret_floatarith.simps
-            interpret_floatarith_divide interpret_floatarith_diff real_diff_def
-  by auto
-
-lemma interpret_floatarith_tan:
-  "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (Inverse (Cos a))) vs =
-   tan (interpret_floatarith a vs)"
-  unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def real_divide_def
-  by auto
-
-lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
-  unfolding powr_def interpret_floatarith.simps ..
-
-lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
-  unfolding log_def interpret_floatarith.simps real_divide_def ..
-
-lemma interpret_floatarith_num:
-  shows "interpret_floatarith (Num (Float 0 0)) vs = 0"
-  and "interpret_floatarith (Num (Float 1 0)) vs = 1"
-  and "interpret_floatarith (Num (Float (number_of a) 0)) vs = number_of a" by auto
+lemma approx_form:
+  assumes "n = length xs"
+  assumes "approx_form prec f (replicate n None) ss"
+  shows "interpret_form f xs"
+  using approx_form_aux[OF _ bounded_by_None] assms by auto
 
 subsection {* Implement proof method \texttt{approximation} *}
 
-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)
-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)
-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)"
-                     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)"
-                     and "real (Float (number_of A) (int B)) = (number_of A) * 2^B"
-                     and "real (Float 1 (int B)) = 2^B"
-                     and "real (Float (number_of A) (- int B)) = (number_of A) / 2^B"
-                     and "real (Float 1 (- int B)) = 1 / 2^B"
-  by (auto simp add: real_of_float_simp pow2_def real_divide_def)
-
-lemmas bounded_by_equations = bounded_by_Cons bounded_by_Nil float_power bounded_divl bounded_divr bounded_num HOL.simp_thms
-lemmas interpret_inequality_equations = interpret_inequality.simps interpret_floatarith.simps interpret_floatarith_num
+lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
   interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
   interpret_floatarith_sin
 
@@ -2543,9 +2645,9 @@
 @{code_datatype float = Float}
 @{code_datatype floatarith = Add | Minus | Mult | Inverse | Cos | Arctan
                            | Abs | Max | Min | Pi | Sqrt | Exp | Ln | Power | Atom | Num }
-@{code_datatype inequality = Less | LessEqual }
-
-val approx_inequality = @{code approx_inequality}
+@{code_datatype form = Bound | Assign | Less | LessEqual | AtLeastAtMost}
+
+val approx_form = @{code approx_form}
 val approx' = @{code approx'}
 
 end
@@ -2566,103 +2668,109 @@
         "Float'_Arith.Exp" and "Float'_Arith.Ln" and "Float'_Arith.Power/ (_,/ _)" and
         "Float'_Arith.Atom" and "Float'_Arith.Num")
 
-code_type inequality (Eval "Float'_Arith.inequality")
-code_const Less and LessEqual (Eval "Float'_Arith.Less/ (_,/ _)" and "Float'_Arith.LessEqual/ (_,/ _)")
-
-code_const approx_inequality (Eval "Float'_Arith.approx'_inequality")
-code_const approx' (Eval "Float'_Arith.approx''")
+code_type form (Eval "Float'_Arith.form")
+code_const Bound and Assign and Less and LessEqual and AtLeastAtMost
+      (Eval "Float'_Arith.Bound/ (_,/ _,/ _,/ _)" and "Float'_Arith.Assign/ (_,/ _,/ _)" and
+            "Float'_Arith.Less/ (_,/ _)" and "Float'_Arith.LessEqual/ (_,/ _)"  and
+            "Float'_Arith.AtLeastAtMost/ (_,/ _,/ _)")
+
+code_const approx_form (Eval "Float'_Arith.approx'_form")
+code_const approx' (Eval "Float'_Arith.approx'")
 
 ML {*
-  val ineq_equations = PureThy.get_thms @{theory} "interpret_inequality_equations";
-  val bounded_by_equations = PureThy.get_thms @{theory} "bounded_by_equations";
-  val bounded_by_simpset = (HOL_basic_ss addsimps bounded_by_equations)
-
-  fun reify_ineq ctxt i = (fn st =>
+  fun reorder_bounds_tac i prems =
     let
-      val to = HOLogic.dest_Trueprop (Logic.strip_imp_concl (List.nth (prems_of st, i - 1)))
-    in (Reflection.genreify_tac ctxt ineq_equations (SOME to) i) st
-    end)
-
-  fun rule_ineq ctxt prec i thm = let
-    fun conv_num typ = HOLogic.dest_number #> snd #> HOLogic.mk_number typ
-    val to_natc = conv_num @{typ "nat"} #> Thm.cterm_of (ProofContext.theory_of ctxt)
-    val to_nat = conv_num @{typ "nat"}
-    val to_int = conv_num @{typ "int"}
-    fun int_to_float A = @{term "Float"} $ to_int A $ @{term "0 :: int"}
-
-    val prec' = to_nat prec
-
-    fun bot_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
-                   = @{term "Float"} $ to_int mantisse $ to_int exp
-      | bot_float (Const (@{const_name "divide"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
-                   = @{term "Float"} $ to_int mantisse $ (@{term "uminus :: int \<Rightarrow> int"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp))
-      | bot_float (Const (@{const_name "times"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
-                   = @{term "Float"} $ to_int mantisse $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
-      | bot_float (Const (@{const_name "divide"}, _) $ A $ (@{term "power 10 :: nat \<Rightarrow> real"} $ exp))
-                   = @{term "float_divl"} $ prec' $ (int_to_float A) $ (@{term "power (Float 5 1)"} $ to_nat exp)
-      | bot_float (Const (@{const_name "divide"}, _) $ A $ B)
-                   = @{term "float_divl"} $ prec' $ int_to_float A $ int_to_float B
-      | bot_float (@{term "power 2 :: nat \<Rightarrow> real"} $ exp)
-                   = @{term "Float 1"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
-      | bot_float A = int_to_float A
-
-    fun top_float (Const (@{const_name "times"}, _) $ mantisse $ (Const (@{const_name "pow2"}, _) $ exp))
-                   = @{term "Float"} $ to_int mantisse $ to_int exp
-      | top_float (Const (@{const_name "divide"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
-                   = @{term "Float"} $ to_int mantisse $ (@{term "uminus :: int \<Rightarrow> int"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp))
-      | top_float (Const (@{const_name "times"}, _) $ mantisse $ (@{term "power 2 :: nat \<Rightarrow> real"} $ exp))
-                   = @{term "Float"} $ to_int mantisse $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
-      | top_float (Const (@{const_name "divide"}, _) $ A $ (@{term "power 10 :: nat \<Rightarrow> real"} $ exp))
-                   = @{term "float_divr"} $ prec' $ (int_to_float A) $ (@{term "power (Float 5 1)"} $ to_nat exp)
-      | top_float (Const (@{const_name "divide"}, _) $ A $ B)
-                   = @{term "float_divr"} $ prec' $ int_to_float A $ int_to_float B
-      | top_float (@{term "power 2 :: nat \<Rightarrow> real"} $ exp)
-                   = @{term "Float 1"} $ (@{term "int :: nat \<Rightarrow> int"} $ to_nat exp)
-      | top_float A = int_to_float A
-
-    val goal' : term = List.nth (prems_of thm, i - 1)
-
-    fun lift_bnd (t as (Const (@{const_name "op &"}, _) $
-                        (Const (@{const_name "less_eq"}, _) $
-                         bottom $ (Free (name, _))) $
-                        (Const (@{const_name "less_eq"}, _) $ _ $ top)))
-         = ((name, HOLogic.mk_prod (bot_float bottom, top_float top))
-            handle TERM (txt, ts) => raise TERM ("Invalid bound number format: " ^
-                                  (Syntax.string_of_term ctxt t), [t]))
-      | lift_bnd t = raise TERM ("Premisse needs format '<num> <= <var> & <var> <= <num>', but found " ^
-                                 (Syntax.string_of_term ctxt t), [t])
-    val bound_eqs = map (HOLogic.dest_Trueprop #> lift_bnd)  (Logic.strip_imp_prems goal')
-
-    fun lift_var (Free (varname, _)) = (case AList.lookup (op =) bound_eqs varname of
-                                          SOME bound => bound
-                                        | NONE => raise TERM ("No bound equations found for " ^ varname, []))
-      | lift_var t = raise TERM ("Can not convert expression " ^
-                                 (Syntax.string_of_term ctxt t), [t])
-
-    val _ $ vs = HOLogic.dest_Trueprop (Logic.strip_imp_concl goal')
-
-    val bs = (HOLogic.dest_list #> map lift_var #> HOLogic.mk_list @{typ "float * float"}) vs
-    val map = [(@{cpat "?prec::nat"}, to_natc prec),
-               (@{cpat "?bs::(float * float) list"}, Thm.cterm_of (ProofContext.theory_of ctxt) bs)]
-  in rtac (Thm.instantiate ([], map) @{thm "approx_inequality"}) i thm end
-
-  val eval_tac = CSUBGOAL (fn (ct, i) => rtac (eval_oracle ct) i)
-
+      fun variable_of_bound (Const ("Trueprop", _) $
+                             (Const (@{const_name "op :"}, _) $
+                              Free (name, _) $ _)) = name
+        | variable_of_bound (Const ("Trueprop", _) $
+                             (Const ("op =", _) $
+                              Free (name, _) $ _)) = name
+        | variable_of_bound t = raise TERM ("variable_of_bound", [t])
+
+      val variable_bounds
+        = map (` (variable_of_bound o prop_of)) prems
+
+      fun add_deps (name, bnds)
+        = Graph.add_deps_acyclic
+            (name, remove (op =) name (Term.add_free_names (prop_of bnds) []))
+      val order = Graph.empty
+                  |> fold Graph.new_node variable_bounds
+                  |> fold add_deps variable_bounds
+                  |> Graph.topological_order |> rev
+                  |> map_filter (AList.lookup (op =) variable_bounds)
+
+      fun prepend_prem th tac
+        = tac THEN rtac (th RSN (2, @{thm mp})) i
+    in
+      fold prepend_prem order all_tac
+    end
+
+  (* Should be in HOL.thy ? *)
   fun gen_eval_tac conv ctxt = CONVERSION (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)
                                THEN' rtac TrueI
 
+  val form_equations = PureThy.get_thms @{theory} "interpret_form_equations";
+
+  fun rewrite_interpret_form_tac ctxt prec splitting i st = let
+      val vs = nth (prems_of st) (i - 1)
+               |> Logic.strip_imp_concl
+               |> HOLogic.dest_Trueprop
+               |> Term.strip_comb |> snd |> List.last
+               |> HOLogic.dest_list
+      val n = vs |> length
+              |> HOLogic.mk_number @{typ nat}
+              |> Thm.cterm_of (ProofContext.theory_of ctxt)
+      val p = prec
+              |> HOLogic.mk_number @{typ nat}
+              |> Thm.cterm_of (ProofContext.theory_of ctxt)
+      val s = vs
+              |> map (fn Free (name, typ) =>
+                      case AList.lookup (op =) splitting name of
+                        SOME s => HOLogic.mk_number @{typ nat} s
+                      | NONE => @{term "0 :: nat"})
+              |> HOLogic.mk_list @{typ nat}
+              |> Thm.cterm_of (ProofContext.theory_of ctxt)
+    in
+      rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
+                                  (@{cpat "?prec::nat"}, p),
+                                  (@{cpat "?ss::nat list"}, s)])
+           @{thm "approx_form"}) i st
+    end
+
+  (* copied from Tools/induct.ML should probably in args.ML *)
+  val free = Args.context -- Args.term >> (fn (_, Free (n, t)) => n | (ctxt, t) =>
+    error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
+
 *}
 
+lemma intervalE: "a \<le> x \<and> x \<le> b \<Longrightarrow> \<lbrakk> x \<in> { a .. b } \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+  by auto
+
+lemma meta_eqE: "x \<equiv> a \<Longrightarrow> \<lbrakk> x = a \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+  by auto
+
 method_setup approximation = {*
-  Args.term >>
-  (fn prec => fn ctxt =>
+  Scan.lift (OuterParse.nat) --
+  Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
+    |-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
+  >>
+  (fn (prec, splitting) => fn ctxt =>
     SIMPLE_METHOD' (fn i =>
-     (DETERM (reify_ineq ctxt i)
-      THEN rule_ineq ctxt prec i
-      THEN Simplifier.asm_full_simp_tac bounded_by_simpset i
-      THEN (TRY (filter_prems_tac (fn t => false) i))
-      THEN (gen_eval_tac eval_oracle ctxt) i)))
-*} "real number approximation"
+      REPEAT (FIRST' [etac @{thm intervalE},
+                      etac @{thm meta_eqE},
+                      rtac @{thm impI}] i)
+      THEN METAHYPS (reorder_bounds_tac i) i
+      THEN TRY (filter_prems_tac (K false) i)
+      THEN DETERM (Reflection.genreify_tac ctxt form_equations NONE i)
+      THEN print_tac "approximation"
+      THEN rewrite_interpret_form_tac ctxt prec splitting i
+      THEN simp_tac @{simpset} i
+      THEN gen_eval_tac eval_oracle ctxt i))
+ *} "real number approximation"
+
+lemma "\<phi> \<in> {0..1 :: real} \<Longrightarrow> \<phi> < \<phi> + 0.7"
+  by (approximation 10 splitting: "\<phi>" = 1)
 
 ML {*
   fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs)
@@ -2733,7 +2841,7 @@
 
   fun approx prec ctxt t = let val t = realify t in
           t
-       |> Reflection.genreif ctxt ineq_equations
+       |> Reflection.genreif ctxt form_equations
        |> prop_of
        |> HOLogic.dest_Trueprop
        |> HOLogic.dest_eq |> snd
diff -r a6b800855cdd -r 64dea9a15031 src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Mon Jun 08 18:37:35 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Jun 25 18:12:40 2009 +0200
@@ -40,6 +40,9 @@
 lemma "0.5 \<le> x \<and> x \<le> 4.5 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
   by (approximation 10)
 
+lemma "x \<in> {0.5 .. 4.5} \<longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
+  by (approximation 10)
+
 lemma "0.49 \<le> x \<and> x \<le> 4.49 \<Longrightarrow> \<bar> arctan x - 0.91 \<bar> < 0.455"
   by (approximation 20)
 
@@ -49,5 +52,9 @@
 lemma "3.2 \<le> x \<and> x \<le> 6.2 \<Longrightarrow> sin x \<le> 0"
   by (approximation 9)
 
+lemma
+  defines "g \<equiv> 9.80665" and "v \<equiv> 128.61" and "d \<equiv> pi / 180"
+  shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
+  using assms by (approximation 80)
+
 end
-