# HG changeset patch
# User wenzelm
# Date 1246389781 -7200
# Node ID 4a34d2a8a4970fb53563a11083e9a7aa6335ec03
# Parent  6129dea3d8a936b56ac7bcc08554d3db24191503# Parent  53acb8ec6c51e1a77ddc39c43574bea60cdb91b0
merged

diff -r 53acb8ec6c51 -r 4a34d2a8a497 NEWS
--- a/NEWS	Tue Jun 30 21:19:32 2009 +0200
+++ b/NEWS	Tue Jun 30 21:23:01 2009 +0200
@@ -73,8 +73,16 @@
 approximation method. 
 
 * "approximate" supports now arithmetic expressions as boundaries of intervals and implements
-interval splitting.
-
+interval splitting and taylor series expansion.
+
+* Changed DERIV_intros to a NamedThmsFun. Each of the theorems in DERIV_intros
+assumes composition with an additional function and matches a variable to the
+derivative, which has to be solved by the simplifier. Hence
+(auto intro!: DERIV_intros) computes the derivative of most elementary terms.
+
+* Maclauren.DERIV_tac and Maclauren.deriv_tac was removed, they are replaced by:
+(auto intro!: DERIV_intros)
+INCOMPATIBILITY.
 
 *** ML ***
 
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -2069,8 +2069,7 @@
   | Atom nat
   | Num float
 
-fun interpret_floatarith :: "floatarith \<Rightarrow> real list \<Rightarrow> real"
-where
+fun interpret_floatarith :: "floatarith \<Rightarrow> real list \<Rightarrow> real" where
 "interpret_floatarith (Add a b) vs   = (interpret_floatarith a vs) + (interpret_floatarith b vs)" |
 "interpret_floatarith (Minus a) vs    = - (interpret_floatarith a vs)" |
 "interpret_floatarith (Mult a b) vs   = (interpret_floatarith a vs) * (interpret_floatarith b vs)" |
@@ -2117,7 +2116,6 @@
   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
@@ -2632,6 +2630,560 @@
   shows "interpret_form f xs"
   using approx_form_aux[OF _ bounded_by_None] assms by auto
 
+subsection {* Implementing Taylor series expansion *}
+
+fun isDERIV :: "nat \<Rightarrow> floatarith \<Rightarrow> real list \<Rightarrow> bool" where
+"isDERIV x (Add a b) vs         = (isDERIV x a vs \<and> isDERIV x b vs)" |
+"isDERIV x (Mult a b) vs        = (isDERIV x a vs \<and> isDERIV x b vs)" |
+"isDERIV x (Minus a) vs         = isDERIV x a vs" |
+"isDERIV x (Inverse a) vs       = (isDERIV x a vs \<and> interpret_floatarith a vs \<noteq> 0)" |
+"isDERIV x (Cos a) vs           = isDERIV x a vs" |
+"isDERIV x (Arctan a) vs        = isDERIV x a vs" |
+"isDERIV x (Min a b) vs         = False" |
+"isDERIV x (Max a b) vs         = False" |
+"isDERIV x (Abs a) vs           = False" |
+"isDERIV x Pi vs                = True" |
+"isDERIV x (Sqrt a) vs          = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
+"isDERIV x (Exp a) vs           = isDERIV x a vs" |
+"isDERIV x (Ln a) vs            = (isDERIV x a vs \<and> interpret_floatarith a vs > 0)" |
+"isDERIV x (Power a 0) vs       = True" |
+"isDERIV x (Power a (Suc n)) vs = isDERIV x a vs" |
+"isDERIV x (Num f) vs           = True" |
+"isDERIV x (Atom n) vs          = True"
+
+fun DERIV_floatarith :: "nat \<Rightarrow> floatarith \<Rightarrow> floatarith" where
+"DERIV_floatarith x (Add a b)         = Add (DERIV_floatarith x a) (DERIV_floatarith x b)" |
+"DERIV_floatarith x (Mult a b)        = Add (Mult a (DERIV_floatarith x b)) (Mult (DERIV_floatarith x a) b)" |
+"DERIV_floatarith x (Minus a)         = Minus (DERIV_floatarith x a)" |
+"DERIV_floatarith x (Inverse a)       = Minus (Mult (DERIV_floatarith x a) (Inverse (Power a 2)))" |
+"DERIV_floatarith x (Cos a)           = Minus (Mult (Cos (Add (Mult Pi (Num (Float 1 -1))) (Minus a))) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Arctan a)        = Mult (Inverse (Add (Num 1) (Power a 2))) (DERIV_floatarith x a)" |
+"DERIV_floatarith x (Min a b)         = Num 0" |
+"DERIV_floatarith x (Max a b)         = Num 0" |
+"DERIV_floatarith x (Abs a)           = Num 0" |
+"DERIV_floatarith x Pi                = Num 0" |
+"DERIV_floatarith x (Sqrt a)          = (Mult (Inverse (Mult (Sqrt a) (Num 2))) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Exp a)           = Mult (Exp a) (DERIV_floatarith x a)" |
+"DERIV_floatarith x (Ln a)            = Mult (Inverse a) (DERIV_floatarith x a)" |
+"DERIV_floatarith x (Power a 0)       = Num 0" |
+"DERIV_floatarith x (Power a (Suc n)) = Mult (Num (Float (int (Suc n)) 0)) (Mult (Power a n) (DERIV_floatarith x a))" |
+"DERIV_floatarith x (Num f)           = Num 0" |
+"DERIV_floatarith x (Atom n)          = (if x = n then Num 1 else Num 0)"
+
+lemma DERIV_floatarith:
+  assumes "n < length vs"
+  assumes isDERIV: "isDERIV n f (vs[n := x])"
+  shows "DERIV (\<lambda> x'. interpret_floatarith f (vs[n := x'])) x :>
+               interpret_floatarith (DERIV_floatarith n f) (vs[n := x])"
+   (is "DERIV (?i f) x :> _")
+using isDERIV proof (induct f arbitrary: x)
+     case (Inverse a) thus ?case
+    by (auto intro!: DERIV_intros
+             simp add: algebra_simps power2_eq_square)
+next case (Cos a) thus ?case
+  by (auto intro!: DERIV_intros
+           simp del: interpret_floatarith.simps(5)
+           simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
+next case (Power a n) thus ?case
+  by (cases n, auto intro!: DERIV_intros
+                    simp del: power_Suc simp add: real_eq_of_nat)
+next case (Ln a) thus ?case
+    by (auto intro!: DERIV_intros simp add: divide_inverse)
+next case (Atom i) thus ?case using `n < length vs` by auto
+qed (auto intro!: DERIV_intros)
+
+declare approx.simps[simp del]
+
+fun isDERIV_approx :: "nat \<Rightarrow> nat \<Rightarrow> floatarith \<Rightarrow> (float * float) option list \<Rightarrow> bool" where
+"isDERIV_approx prec x (Add a b) vs         = (isDERIV_approx prec x a vs \<and> isDERIV_approx prec x b vs)" |
+"isDERIV_approx prec x (Mult a b) vs        = (isDERIV_approx prec x a vs \<and> isDERIV_approx prec x b vs)" |
+"isDERIV_approx prec x (Minus a) vs         = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Inverse a) vs       =
+  (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l \<or> u < 0 | None \<Rightarrow> False))" |
+"isDERIV_approx prec x (Cos a) vs           = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Arctan a) vs        = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Min a b) vs         = False" |
+"isDERIV_approx prec x (Max a b) vs         = False" |
+"isDERIV_approx prec x (Abs a) vs           = False" |
+"isDERIV_approx prec x Pi vs                = True" |
+"isDERIV_approx prec x (Sqrt a) vs          =
+  (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l | None \<Rightarrow> False))" |
+"isDERIV_approx prec x (Exp a) vs           = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Ln a) vs            =
+  (isDERIV_approx prec x a vs \<and> (case approx prec a vs of Some (l, u) \<Rightarrow> 0 < l | None \<Rightarrow> False))" |
+"isDERIV_approx prec x (Power a 0) vs       = True" |
+"isDERIV_approx prec x (Power a (Suc n)) vs = isDERIV_approx prec x a vs" |
+"isDERIV_approx prec x (Num f) vs           = True" |
+"isDERIV_approx prec x (Atom n) vs          = True"
+
+lemma isDERIV_approx:
+  assumes "bounded_by xs vs"
+  and isDERIV_approx: "isDERIV_approx prec x f vs"
+  shows "isDERIV x f xs"
+using isDERIV_approx proof (induct f)
+  case (Inverse a)
+  then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
+    and *: "0 < l \<or> u < 0"
+    by (cases "approx prec a vs", auto)
+  with approx[OF `bounded_by xs vs` approx_Some]
+  have "interpret_floatarith a xs \<noteq> 0" unfolding less_float_def by auto
+  thus ?case using Inverse by auto
+next
+  case (Ln a)
+  then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
+    and *: "0 < l"
+    by (cases "approx prec a vs", auto)
+  with approx[OF `bounded_by xs vs` approx_Some]
+  have "0 < interpret_floatarith a xs" unfolding less_float_def by auto
+  thus ?case using Ln by auto
+next
+  case (Sqrt a)
+  then obtain l u where approx_Some: "Some (l, u) = approx prec a vs"
+    and *: "0 < l"
+    by (cases "approx prec a vs", auto)
+  with approx[OF `bounded_by xs vs` approx_Some]
+  have "0 < interpret_floatarith a xs" unfolding less_float_def by auto
+  thus ?case using Sqrt by auto
+next
+  case (Power a n) thus ?case by (cases n, auto)
+qed auto
+
+lemma bounded_by_update_var:
+  assumes "bounded_by xs vs" and "vs ! i = Some (l, u)"
+  and bnd: "x \<in> { real l .. real u }"
+  shows "bounded_by (xs[i := x]) vs"
+proof (cases "i < length xs")
+  case False thus ?thesis using `bounded_by xs vs` by auto
+next
+  let ?xs = "xs[i := x]"
+  case True hence "i < length ?xs" by auto
+{ fix j
+  assume "j < length vs"
+  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 ! i = Some (l, u)` Some and bnd `i < length ?xs`
+	by auto
+    next
+      case False
+      thus ?thesis using `bounded_by xs vs`[THEN bounded_byE, OF `j < length vs`] Some
+	by auto
+    qed
+  qed auto }
+  thus ?thesis unfolding bounded_by_def by auto
+qed
+
+lemma isDERIV_approx':
+  assumes "bounded_by xs vs"
+  and vs_x: "vs ! x = Some (l, u)" and X_in: "X \<in> { real l .. real u }"
+  and approx: "isDERIV_approx prec x f vs"
+  shows "isDERIV x f (xs[x := X])"
+proof -
+  note bounded_by_update_var[OF `bounded_by xs vs` vs_x X_in] approx
+  thus ?thesis by (rule isDERIV_approx)
+qed
+
+lemma DERIV_approx:
+  assumes "n < length xs" and bnd: "bounded_by xs vs"
+  and isD: "isDERIV_approx prec n f vs"
+  and app: "Some (l, u) = approx prec (DERIV_floatarith n f) vs" (is "_ = approx _ ?D _")
+  shows "\<exists>x. real l \<le> x \<and> x \<le> real u \<and>
+             DERIV (\<lambda> x. interpret_floatarith f (xs[n := x])) (xs!n) :> x"
+         (is "\<exists> x. _ \<and> _ \<and> DERIV (?i f) _ :> _")
+proof (rule exI[of _ "?i ?D (xs!n)"], rule conjI[OF _ conjI])
+  let "?i f x" = "interpret_floatarith f (xs[n := x])"
+  from approx[OF bnd app]
+  show "real l \<le> ?i ?D (xs!n)" and "?i ?D (xs!n) \<le> real u"
+    using `n < length xs` by auto
+  from DERIV_floatarith[OF `n < length xs`, of f "xs!n"] isDERIV_approx[OF bnd isD]
+  show "DERIV (?i f) (xs!n) :> (?i ?D (xs!n))" by simp
+qed
+
+fun lift_bin :: "(float * float) option \<Rightarrow> (float * float) option \<Rightarrow> (float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float \<Rightarrow> (float * float) option) \<Rightarrow> (float * float) option" where
+"lift_bin (Some (l1, u1)) (Some (l2, u2)) f = f l1 u1 l2 u2" |
+"lift_bin a b f = None"
+
+lemma lift_bin:
+  assumes lift_bin_Some: "Some (l, u) = lift_bin a b f"
+  obtains l1 u1 l2 u2
+  where "a = Some (l1, u1)"
+  and "b = Some (l2, u2)"
+  and "f l1 u1 l2 u2 = Some (l, u)"
+using assms by (cases a, simp, cases b, simp, auto)
+
+fun approx_tse where
+"approx_tse prec n 0 c k f bs = approx prec f bs" |
+"approx_tse prec n (Suc s) c k f bs =
+  (if isDERIV_approx prec n f bs then
+    lift_bin (approx prec f (bs[n := Some (c,c)]))
+             (approx_tse prec n s c (Suc k) (DERIV_floatarith n f) bs)
+             (\<lambda> l1 u1 l2 u2. approx prec
+                 (Add (Atom 0)
+                      (Mult (Inverse (Num (Float (int k) 0)))
+                                 (Mult (Add (Atom (Suc (Suc 0))) (Minus (Num c)))
+                                       (Atom (Suc 0))))) [Some (l1, u1), Some (l2, u2), bs!n])
+  else approx prec f bs)"
+
+lemma bounded_by_Cons:
+  assumes bnd: "bounded_by xs vs"
+  and x: "x \<in> { real l .. real u }"
+  shows "bounded_by (x#xs) ((Some (l, u))#vs)"
+proof -
+  { fix i assume *: "i < length ((Some (l, u))#vs)"
+    have "case ((Some (l,u))#vs) ! i of Some (l, u) \<Rightarrow> (x#xs)!i \<in> { real l .. real u } | None \<Rightarrow> True"
+    proof (cases i)
+      case 0 with x show ?thesis by auto
+    next
+      case (Suc i) with * have "i < length vs" by auto
+      from bnd[THEN bounded_byE, OF this]
+      show ?thesis unfolding Suc nth_Cons_Suc .
+    qed }
+  thus ?thesis by (auto simp add: bounded_by_def)
+qed
+
+lemma approx_tse_generic:
+  assumes "bounded_by xs vs"
+  and bnd_c: "bounded_by (xs[x := real c]) vs" and "x < length vs" and "x < length xs"
+  and bnd_x: "vs ! x = Some (lx, ux)"
+  and ate: "Some (l, u) = approx_tse prec x s c k f vs"
+  shows "\<exists> n. (\<forall> m < n. \<forall> z \<in> {real lx .. real ux}.
+      DERIV (\<lambda> y. interpret_floatarith ((DERIV_floatarith x ^^ m) f) (xs[x := y])) z :>
+            (interpret_floatarith ((DERIV_floatarith x ^^ (Suc m)) f) (xs[x := z])))
+   \<and> (\<forall> t \<in> {real lx .. real ux}.  (\<Sum> i = 0..<n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) *
+                  interpret_floatarith ((DERIV_floatarith x ^^ i) f) (xs[x := real c]) *
+                  (xs!x - real c)^i) +
+      inverse (real (\<Prod> j \<in> {k..<k+n}. j)) *
+      interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := t]) *
+      (xs!x - real c)^n \<in> {real l .. real u})" (is "\<exists> n. ?taylor f k l u n")
+using ate proof (induct s arbitrary: k f l u)
+  case 0
+  { fix t assume "t \<in> {real lx .. real ux}"
+    note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
+    from approx[OF this 0[unfolded approx_tse.simps]]
+    have "(interpret_floatarith f (xs[x := t])) \<in> {real l .. real u}"
+      by (auto simp add: algebra_simps)
+  } thus ?case by (auto intro!: exI[of _ 0])
+next
+  case (Suc s)
+  show ?case
+  proof (cases "isDERIV_approx prec x f vs")
+    case False
+    note ap = Suc.prems[unfolded approx_tse.simps if_not_P[OF False]]
+
+    { fix t assume "t \<in> {real lx .. real ux}"
+      note bounded_by_update_var[OF `bounded_by xs vs` bnd_x this]
+      from approx[OF this ap]
+      have "(interpret_floatarith f (xs[x := t])) \<in> {real l .. real u}"
+	by (auto simp add: algebra_simps)
+    } thus ?thesis by (auto intro!: exI[of _ 0])
+  next
+    case True
+    with Suc.prems
+    obtain l1 u1 l2 u2
+      where a: "Some (l1, u1) = approx prec f (vs[x := Some (c,c)])"
+      and ate: "Some (l2, u2) = approx_tse prec x s c (Suc k) (DERIV_floatarith x f) vs"
+      and final: "Some (l, u) = approx prec
+        (Add (Atom 0)
+             (Mult (Inverse (Num (Float (int k) 0)))
+                   (Mult (Add (Atom (Suc (Suc 0))) (Minus (Num c)))
+                         (Atom (Suc 0))))) [Some (l1, u1), Some (l2, u2), vs!x]"
+      by (auto elim!: lift_bin) blast
+
+    from bnd_c `x < length xs`
+    have bnd: "bounded_by (xs[x:=real c]) (vs[x:= Some (c,c)])"
+      by (auto intro!: bounded_by_update)
+
+    from approx[OF this a]
+    have f_c: "interpret_floatarith ((DERIV_floatarith x ^^ 0) f) (xs[x := real c]) \<in> { real l1 .. real u1 }"
+              (is "?f 0 (real c) \<in> _")
+      by auto
+
+    { fix f :: "'a \<Rightarrow> 'a" fix n :: nat fix x :: 'a
+      have "(f ^^ Suc n) x = (f ^^ n) (f x)"
+	by (induct n, auto) }
+    note funpow_Suc = this[symmetric]
+    from Suc.hyps[OF ate, unfolded this]
+    obtain n
+      where DERIV_hyp: "\<And> m z. \<lbrakk> m < n ; z \<in> { real lx .. real ux } \<rbrakk> \<Longrightarrow> DERIV (?f (Suc m)) z :> ?f (Suc (Suc m)) z"
+      and hyp: "\<forall> t \<in> {real lx .. real ux}. (\<Sum> i = 0..<n. inverse (real (\<Prod> j \<in> {Suc k..<Suc k + i}. j)) * ?f (Suc i) (real c) * (xs!x - real c)^i) +
+           inverse (real (\<Prod> j \<in> {Suc k..<Suc k + n}. j)) * ?f (Suc n) t * (xs!x - real c)^n \<in> {real l2 .. real u2}"
+          (is "\<forall> t \<in> _. ?X (Suc k) f n t \<in> _")
+      by blast
+
+    { fix m z
+      assume "m < Suc n" and bnd_z: "z \<in> { real lx .. real ux }"
+      have "DERIV (?f m) z :> ?f (Suc m) z"
+      proof (cases m)
+	case 0
+	with DERIV_floatarith[OF `x < length xs` isDERIV_approx'[OF `bounded_by xs vs` bnd_x bnd_z True]]
+	show ?thesis by simp
+      next
+	case (Suc m')
+	hence "m' < n" using `m < Suc n` by auto
+	from DERIV_hyp[OF this bnd_z]
+	show ?thesis using Suc by simp
+      qed } note DERIV = this
+
+    have "\<And> k i. k < i \<Longrightarrow> {k ..< i} = insert k {Suc k ..< i}" by auto
+    hence setprod_head_Suc: "\<And> k i. \<Prod> {k ..< k + Suc i} = k * \<Prod> {Suc k ..< Suc k + i}" by auto
+    have setsum_move0: "\<And> k F. setsum F {0..<Suc k} = F 0 + setsum (\<lambda> k. F (Suc k)) {0..<k}"
+      unfolding setsum_shift_bounds_Suc_ivl[symmetric]
+      unfolding setsum_head_upt_Suc[OF zero_less_Suc] ..
+    def C \<equiv> "xs!x - real c"
+
+    { fix t assume t: "t \<in> {real lx .. real ux}"
+      hence "bounded_by [xs!x] [vs!x]"
+	using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`]
+	by (cases "vs!x", auto simp add: bounded_by_def)
+
+      with hyp[THEN bspec, OF t] f_c
+      have "bounded_by [?f 0 (real c), ?X (Suc k) f n t, xs!x] [Some (l1, u1), Some (l2, u2), vs!x]"
+	by (auto intro!: bounded_by_Cons)
+      from approx[OF this final, unfolded atLeastAtMost_iff[symmetric]]
+      have "?X (Suc k) f n t * (xs!x - real c) * inverse (real k) + ?f 0 (real c) \<in> {real l .. real u}"
+	by (auto simp add: algebra_simps)
+      also have "?X (Suc k) f n t * (xs!x - real c) * inverse (real k) + ?f 0 (real c) =
+               (\<Sum> i = 0..<Suc n. inverse (real (\<Prod> j \<in> {k..<k+i}. j)) * ?f i (real c) * (xs!x - real c)^i) +
+               inverse (real (\<Prod> j \<in> {k..<k+Suc n}. j)) * ?f (Suc n) t * (xs!x - real c)^Suc n" (is "_ = ?T")
+	unfolding funpow_Suc C_def[symmetric] setsum_move0 setprod_head_Suc
+	by (auto simp add: algebra_simps setsum_right_distrib[symmetric])
+      finally have "?T \<in> {real l .. real u}" . }
+    thus ?thesis using DERIV by blast
+  qed
+qed
+
+lemma setprod_fact: "\<Prod> {1..<1 + k} = fact (k :: nat)"
+proof (induct k)
+  case (Suc k)
+  have "{ 1 ..< Suc (Suc k) } = insert (Suc k) { 1 ..< Suc k }" by auto
+  hence "\<Prod> { 1 ..< Suc (Suc k) } = (Suc k) * \<Prod> { 1 ..< Suc k }" by auto
+  thus ?case using Suc by auto
+qed simp
+
+lemma approx_tse:
+  assumes "bounded_by xs vs"
+  and bnd_x: "vs ! x = Some (lx, ux)" and bnd_c: "real c \<in> {real lx .. real ux}"
+  and "x < length vs" and "x < length xs"
+  and ate: "Some (l, u) = approx_tse prec x s c 1 f vs"
+  shows "interpret_floatarith f xs \<in> { real l .. real u }"
+proof -
+  def F \<equiv> "\<lambda> n z. interpret_floatarith ((DERIV_floatarith x ^^ n) f) (xs[x := z])"
+  hence F0: "F 0 = (\<lambda> z. interpret_floatarith f (xs[x := z]))" by auto
+
+  hence "bounded_by (xs[x := real c]) vs" and "x < length vs" "x < length xs"
+    using `bounded_by xs vs` bnd_x bnd_c `x < length vs` `x < length xs`
+    by (auto intro!: bounded_by_update_var)
+
+  from approx_tse_generic[OF `bounded_by xs vs` this bnd_x ate]
+  obtain n
+    where DERIV: "\<forall> m z. m < n \<and> real lx \<le> z \<and> z \<le> real ux \<longrightarrow> DERIV (F m) z :> F (Suc m) z"
+    and hyp: "\<And> t. t \<in> {real lx .. real ux} \<Longrightarrow>
+           (\<Sum> j = 0..<n. inverse (real (fact j)) * F j (real c) * (xs!x - real c)^j) +
+             inverse (real (fact n)) * F n t * (xs!x - real c)^n
+             \<in> {real l .. real u}" (is "\<And> t. _ \<Longrightarrow> ?taylor t \<in> _")
+    unfolding F_def atLeastAtMost_iff[symmetric] setprod_fact by blast
+
+  have bnd_xs: "xs ! x \<in> { real lx .. real ux }"
+    using `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
+
+  show ?thesis
+  proof (cases n)
+    case 0 thus ?thesis using hyp[OF bnd_xs] unfolding F_def by auto
+  next
+    case (Suc n')
+    show ?thesis
+    proof (cases "xs ! x = real c")
+      case True
+      from True[symmetric] hyp[OF bnd_xs] Suc show ?thesis
+	unfolding F_def Suc setsum_head_upt_Suc[OF zero_less_Suc] setsum_shift_bounds_Suc_ivl by auto
+    next
+      case False
+
+      have "real lx \<le> real c" "real c \<le> real ux" "real lx \<le> xs!x" "xs!x \<le> real ux"
+	using Suc bnd_c `bounded_by xs vs`[THEN bounded_byE, OF `x < length vs`] bnd_x by auto
+      from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
+      obtain t where t_bnd: "if xs ! x < real c then xs ! x < t \<and> t < real c else real c < t \<and> t < xs ! x"
+	and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
+	   (\<Sum>m = 0..<Suc n'. F m (real c) / real (fact m) * (xs ! x - real c) ^ m) +
+           F (Suc n') t / real (fact (Suc n')) * (xs ! x - real c) ^ Suc n'"
+	by blast
+
+      from t_bnd bnd_xs bnd_c have *: "t \<in> {real lx .. real ux}"
+	by (cases "xs ! x < real c", auto)
+
+      have "interpret_floatarith f (xs[x := xs ! x]) = ?taylor t"
+	unfolding fl_eq Suc by (auto simp add: algebra_simps divide_inverse)
+      also have "\<dots> \<in> {real l .. real u}" using * by (rule hyp)
+      finally show ?thesis by simp
+    qed
+  qed
+qed
+
+fun approx_tse_form' where
+"approx_tse_form' prec t f 0 l u cmp =
+  (case approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)]
+     of Some (l, u) \<Rightarrow> cmp l u | None \<Rightarrow> False)" |
+"approx_tse_form' prec t f (Suc s) l u cmp =
+  (let m = (l + u) * Float 1 -1
+   in approx_tse_form' prec t f s l m cmp \<and>
+      approx_tse_form' prec t f s m u cmp)"
+
+lemma approx_tse_form':
+  assumes "approx_tse_form' prec t f s l u cmp" and "x \<in> {real l .. real u}"
+  shows "\<exists> l' u' ly uy. x \<in> { real l' .. real u' } \<and> real l \<le> real l' \<and> real u' \<le> real u \<and> cmp ly uy \<and>
+                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)"
+using assms proof (induct s arbitrary: l u)
+  case 0
+  then obtain ly uy
+    where *: "approx_tse prec 0 t ((l + u) * Float 1 -1) 1 f [Some (l, u)] = Some (ly, uy)"
+    and **: "cmp ly uy" by (auto elim!: option_caseE)
+  with 0 show ?case by (auto intro!: exI)
+next
+  case (Suc s)
+  let ?m = "(l + u) * Float 1 -1"
+  from Suc.prems
+  have l: "approx_tse_form' prec t f s l ?m cmp"
+    and u: "approx_tse_form' prec t f s ?m u cmp"
+    by (auto simp add: Let_def)
+
+  have m_l: "real l \<le> real ?m" and m_u: "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 ?case
+  proof (rule disjE)
+    assume "x \<in> { real l .. real ?m}"
+    from Suc.hyps[OF l this]
+    obtain l' u' ly uy
+      where "x \<in> { real l' .. real u' } \<and> real l \<le> real l' \<and> real u' \<le> real ?m \<and> cmp ly uy \<and>
+                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
+    with m_u show ?thesis by (auto intro!: exI)
+  next
+    assume "x \<in> { real ?m .. real u }"
+    from Suc.hyps[OF u this]
+    obtain l' u' ly uy
+      where "x \<in> { real l' .. real u' } \<and> real ?m \<le> real l' \<and> real u' \<le> real u \<and> cmp ly uy \<and>
+                  approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 f [Some (l', u')] = Some (ly, uy)" by blast
+    with m_u show ?thesis by (auto intro!: exI)
+  qed
+qed
+
+lemma approx_tse_form'_less:
+  assumes tse: "approx_tse_form' prec t (Add a (Minus b)) s l u (\<lambda> l u. 0 < l)"
+  and x: "x \<in> {real l .. real u}"
+  shows "interpret_floatarith b [x] < interpret_floatarith a [x]"
+proof -
+  from approx_tse_form'[OF tse x]
+  obtain l' u' ly uy
+    where x': "x \<in> { real l' .. real u' }" and "real l \<le> real l'"
+    and "real u' \<le> real u" and "0 < ly"
+    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
+    by blast
+
+  hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
+
+  from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
+  have "real ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
+    by (auto simp add: diff_minus)
+  from order_less_le_trans[OF `0 < ly`[unfolded less_float_def] this]
+  show ?thesis by auto
+qed
+
+lemma approx_tse_form'_le:
+  assumes tse: "approx_tse_form' prec t (Add a (Minus b)) s l u (\<lambda> l u. 0 \<le> l)"
+  and x: "x \<in> {real l .. real u}"
+  shows "interpret_floatarith b [x] \<le> interpret_floatarith a [x]"
+proof -
+  from approx_tse_form'[OF tse x]
+  obtain l' u' ly uy
+    where x': "x \<in> { real l' .. real u' }" and "real l \<le> real l'"
+    and "real u' \<le> real u" and "0 \<le> ly"
+    and tse: "approx_tse prec 0 t ((l' + u') * Float 1 -1) 1 (Add a (Minus b)) [Some (l', u')] = Some (ly, uy)"
+    by blast
+
+  hence "bounded_by [x] [Some (l', u')]" by (auto simp add: bounded_by_def)
+
+  from approx_tse[OF this _ _ _ _ tse[symmetric], of l' u'] x'
+  have "real ly \<le> interpret_floatarith a [x] - interpret_floatarith b [x]"
+    by (auto simp add: diff_minus)
+  from order_trans[OF `0 \<le> ly`[unfolded le_float_def] this]
+  show ?thesis by auto
+qed
+
+definition
+"approx_tse_form prec t s f =
+  (case f
+   of (Bound x a b f) \<Rightarrow> x = Atom 0 \<and>
+     (case (approx prec a [None], approx prec b [None])
+      of (Some (l, u), Some (l', u')) \<Rightarrow>
+        (case f
+         of Less lf rt \<Rightarrow> approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 < l)
+          | LessEqual lf rt \<Rightarrow> approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)
+          | AtLeastAtMost x lf rt \<Rightarrow>
+            approx_tse_form' prec t (Add x (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l) \<and>
+            approx_tse_form' prec t (Add rt (Minus x)) s l u' (\<lambda> l u. 0 \<le> l)
+          | _ \<Rightarrow> False)
+       | _ \<Rightarrow> False)
+   | _ \<Rightarrow> False)"
+
+lemma approx_tse_form:
+  assumes "approx_tse_form prec t s f"
+  shows "interpret_form f [x]"
+proof (cases f)
+  case (Bound i a b f') note f_def = this
+  with assms obtain l u l' u'
+    where a: "approx prec a [None] = Some (l, u)"
+    and b: "approx prec b [None] = Some (l', u')"
+    unfolding approx_tse_form_def by (auto elim!: option_caseE)
+
+  from Bound assms have "i = Atom 0" unfolding approx_tse_form_def by auto
+  hence i: "interpret_floatarith i [x] = x" by auto
+
+  { let "?f z" = "interpret_floatarith z [x]"
+    assume "?f i \<in> { ?f a .. ?f b }"
+    with approx[OF _ a[symmetric], of "[x]"] approx[OF _ b[symmetric], of "[x]"]
+    have bnd: "x \<in> { real l .. real u'}" unfolding bounded_by_def i by auto
+
+    have "interpret_form f' [x]"
+    proof (cases f')
+      case (Less lf rt)
+      with Bound a b assms
+      have "approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 < l)"
+	unfolding approx_tse_form_def by auto
+      from approx_tse_form'_less[OF this bnd]
+      show ?thesis using Less by auto
+    next
+      case (LessEqual lf rt)
+      with Bound a b assms
+      have "approx_tse_form' prec t (Add rt (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)"
+	unfolding approx_tse_form_def by auto
+      from approx_tse_form'_le[OF this bnd]
+      show ?thesis using LessEqual by auto
+    next
+      case (AtLeastAtMost x lf rt)
+      with Bound a b assms
+      have "approx_tse_form' prec t (Add rt (Minus x)) s l u' (\<lambda> l u. 0 \<le> l)"
+	and "approx_tse_form' prec t (Add x (Minus lf)) s l u' (\<lambda> l u. 0 \<le> l)"
+	unfolding approx_tse_form_def by auto
+      from approx_tse_form'_le[OF this(1) bnd] approx_tse_form'_le[OF this(2) bnd]
+      show ?thesis using AtLeastAtMost by auto
+    next
+      case (Bound x a b f') with assms
+      show ?thesis by (auto elim!: option_caseE simp add: f_def approx_tse_form_def)
+    next
+      case (Assign x a f') with assms
+      show ?thesis by (auto elim!: option_caseE simp add: f_def approx_tse_form_def)
+    qed } thus ?thesis unfolding f_def by auto
+next case Assign with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next case LessEqual with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next case Less with assms show ?thesis by (auto simp add: approx_tse_form_def)
+next case AtLeastAtMost with assms show ?thesis by (auto simp add: approx_tse_form_def)
+qed
+
 subsection {* Implement proof method \texttt{approximation} *}
 
 lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
@@ -2648,6 +3200,7 @@
 @{code_datatype form = Bound | Assign | Less | LessEqual | AtLeastAtMost}
 
 val approx_form = @{code approx_form}
+val approx_tse_form = @{code approx_tse_form}
 val approx' = @{code approx'}
 
 end
@@ -2675,6 +3228,7 @@
             "Float'_Arith.AtLeastAtMost/ (_,/ _,/ _)")
 
 code_const approx_form (Eval "Float'_Arith.approx'_form")
+code_const approx_tse_form (Eval "Float'_Arith.approx'_tse'_form")
 code_const approx' (Eval "Float'_Arith.approx'")
 
 ML {*
@@ -2712,30 +3266,49 @@
 
   val form_equations = PureThy.get_thms @{theory} "interpret_form_equations";
 
-  fun rewrite_interpret_form_tac ctxt prec splitting i st = let
+  fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let
+      fun lookup_splitting (Free (name, typ))
+        = case AList.lookup (op =) splitting name
+          of SOME s => HOLogic.mk_number @{typ nat} s
+           | NONE => @{term "0 :: nat"}
       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}
+    in case taylor
+    of NONE => let
+         val n = vs |> length
+                 |> HOLogic.mk_number @{typ nat}
+                 |> Thm.cterm_of (ProofContext.theory_of ctxt)
+         val s = vs
+                 |> map lookup_splitting
+                 |> 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
+          THEN simp_tac @{simpset} i) st
+       end
+
+     | SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st]))
+       else let
+         val t = t
+              |> HOLogic.mk_number @{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
+         val s = vs |> map lookup_splitting |> hd
+              |> Thm.cterm_of (ProofContext.theory_of ctxt)
+       in
+         rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
+                                     (@{cpat "?t::nat"}, t),
+                                     (@{cpat "?prec::nat"}, p)])
+              @{thm "approx_tse_form"}) i st
+       end
     end
 
   (* copied from Tools/induct.ML should probably in args.ML *)
@@ -2751,11 +3324,15 @@
   by auto
 
 method_setup approximation = {*
-  Scan.lift (OuterParse.nat) --
+  Scan.lift (OuterParse.nat)
+  --
   Scan.optional (Scan.lift (Args.$$$ "splitting" |-- Args.colon)
     |-- OuterParse.and_list' (free --| Scan.lift (Args.$$$ "=") -- Scan.lift OuterParse.nat)) []
+  --
+  Scan.option (Scan.lift (Args.$$$ "taylor" |-- Args.colon)
+    |-- (free |-- Scan.lift (Args.$$$ "=") |-- Scan.lift OuterParse.nat))
   >>
-  (fn (prec, splitting) => fn ctxt =>
+  (fn ((prec, splitting), taylor) => fn ctxt =>
     SIMPLE_METHOD' (fn i =>
       REPEAT (FIRST' [etac @{thm intervalE},
                       etac @{thm meta_eqE},
@@ -2763,15 +3340,10 @@
       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 rewrite_interpret_form_tac ctxt prec splitting taylor 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)
   | dest_interpret t = raise TERM ("dest_interpret", [t])
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Decision_Procs/ex/Approximation_Ex.thy
--- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -8,13 +8,28 @@
 
 Here are some examples how to use the approximation method.
 
-The parameter passed to the method specifies the precision used by the computations, it is specified
-as number of bits to calculate. When a variable is used it needs to be bounded by an interval. This
-interval is specified as a conjunction of the lower and upper bound. It must have the form
-@{text "\<lbrakk> l\<^isub>1 \<le> x\<^isub>1 \<and> x\<^isub>1 \<le> u\<^isub>1 ; \<dots> ; l\<^isub>n \<le> x\<^isub>n \<and> x\<^isub>n \<le> u\<^isub>n \<rbrakk> \<Longrightarrow> F"} where @{term F} is the formula, and
-@{text "x\<^isub>1, \<dots>, x\<^isub>n"} are the variables. The lower bounds @{text "l\<^isub>1, \<dots>, l\<^isub>n"} and the upper bounds
-@{text "u\<^isub>1, \<dots>, u\<^isub>n"} must either be integer numerals, floating point numbers or of the form
-@{term "m * pow2 e"} to specify a exact floating point value.
+The approximation method has the following syntax:
+
+approximate "prec" (splitting: "x" = "depth" and "y" = "depth" ...)? (taylor: "z" = "derivates")?
+
+Here "prec" specifies the precision used in all computations, it is specified as
+number of bits to calculate. In the proposition to prove an arbitrary amount of
+variables can be used, but each one need to be bounded by an upper and lower
+bound.
+
+To specify the bounds either @{term "l\<^isub>1 \<le> x \<and> x \<le> u\<^isub>1"},
+@{term "x \<in> { l\<^isub>1 .. u\<^isub>1 }"} or @{term "x = bnd"} can be used. Where the
+bound specification are again arithmetic formulas containing variables. They can
+be connected using either meta level or HOL equivalence.
+
+To use interval splitting add for each variable whos interval should be splitted
+to the "splitting:" parameter. The parameter specifies how often each interval
+should be divided, e.g. when x = 16 is specified, there will be @{term "65536 = 2^16"}
+intervals to be calculated.
+
+To use taylor series expansion specify the variable to derive. You need to
+specify the amount of derivations to compute. When using taylor series expansion
+only one variable can be used.
 
 *}
 
@@ -57,4 +72,7 @@
   shows "g / v * tan (35 * d) \<in> { 3 * d .. 3.1 * d }"
   using assms by (approximation 80)
 
+lemma "\<phi> \<in> { 0 .. 1 :: real } \<longrightarrow> \<phi> ^ 2 \<le> \<phi>"
+  by (approximation 30 splitting: \<phi>=1 taylor: \<phi> = 3)
+
 end
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Deriv.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -115,12 +115,16 @@
 
 text{*Differentiation of finite sum*}
 
+lemma DERIV_setsum:
+  assumes "finite S"
+  and "\<And> n. n \<in> S \<Longrightarrow> DERIV (%x. f x n) x :> (f' x n)"
+  shows "DERIV (%x. setsum (f x) S) x :> setsum (f' x) S"
+  using assms by induct (auto intro!: DERIV_add)
+
 lemma DERIV_sumr [rule_format (no_asm)]:
      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))
       --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
-apply (induct "n")
-apply (auto intro: DERIV_add)
-done
+  by (auto intro: DERIV_setsum)
 
 text{*Alternative definition for differentiability*}
 
@@ -216,7 +220,6 @@
   shows "DERIV (\<lambda>x. f x ^ n) x :> of_nat n * (D * f x ^ (n - Suc 0))"
 by (cases "n", simp, simp add: DERIV_power_Suc f del: power_Suc)
 
-
 text {* Caratheodory formulation of derivative at a point *}
 
 lemma CARAT_DERIV:
@@ -308,6 +311,30 @@
 lemma lemma_DERIV_subst: "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E"
 by auto
 
+text {* DERIV_intros *}
+
+ML{*
+structure DerivIntros =
+  NamedThmsFun(val name = "DERIV_intros"
+               val description = "DERIV introduction rules");
+*}
+setup DerivIntros.setup
+
+lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = Y \<rbrakk> \<Longrightarrow> DERIV f x :> Y"
+  by simp
+
+declare
+  DERIV_const[THEN DERIV_cong, DERIV_intros]
+  DERIV_ident[THEN DERIV_cong, DERIV_intros]
+  DERIV_add[THEN DERIV_cong, DERIV_intros]
+  DERIV_minus[THEN DERIV_cong, DERIV_intros]
+  DERIV_mult[THEN DERIV_cong, DERIV_intros]
+  DERIV_diff[THEN DERIV_cong, DERIV_intros]
+  DERIV_inverse'[THEN DERIV_cong, DERIV_intros]
+  DERIV_divide[THEN DERIV_cong, DERIV_intros]
+  DERIV_power[where 'a=real, THEN DERIV_cong,
+              unfolded real_of_nat_def[symmetric], DERIV_intros]
+  DERIV_setsum[THEN DERIV_cong, DERIV_intros]
 
 subsection {* Differentiability predicate *}
 
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Imperative_HOL/Array.thy
--- a/src/HOL/Imperative_HOL/Array.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -1,5 +1,4 @@
-(*  Title:      HOL/Library/Array.thy
-    ID:         $Id$
+(*  Title:      HOL/Imperative_HOL/Array.thy
     Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -306,67 +306,75 @@
 code_const "Heap_Monad.Fail" (OCaml "Failure")
 code_const "Heap_Monad.raise_exc" (OCaml "!(fun/ ()/ ->/ raise/ _)")
 
-setup {* let
-  open Code_Thingol;
+setup {*
+
+let
 
-  fun lookup naming = the o Code_Thingol.lookup_const naming;
+open Code_Thingol;
+
+fun imp_program naming =
 
-  fun imp_monad_bind'' bind' return' unit' ts =
-    let
-      val dummy_name = "";
-      val dummy_type = ITyVar dummy_name;
-      val dummy_case_term = IVar dummy_name;
-      (*assumption: dummy values are not relevant for serialization*)
-      val unitt = IConst (unit', (([], []), []));
-      fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
-        | dest_abs (t, ty) =
-            let
-              val vs = Code_Thingol.fold_varnames cons t [];
-              val v = Name.variant vs "x";
-              val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
-            in ((v, ty'), t `$ IVar v) end;
-      fun force (t as IConst (c, _) `$ t') = if c = return'
-            then t' else t `$ unitt
-        | force t = t `$ unitt;
-      fun tr_bind' [(t1, _), (t2, ty2)] =
-        let
-          val ((v, ty), t) = dest_abs (t2, ty2);
-        in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
-      and tr_bind'' t = case Code_Thingol.unfold_app t
-           of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
-                then tr_bind' [(x1, ty1), (x2, ty2)]
-                else force t
-            | _ => force t;
-    in (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
-      [(unitt, tr_bind' ts)]), dummy_case_term) end
-  and imp_monad_bind' bind' return' unit' (const as (c, (_, tys))) ts = if c = bind' then case (ts, tys)
-     of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)]
-      | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' bind' return' unit' [(t1, ty1), (t2, ty2)] `$ t3
-      | (ts, _) => imp_monad_bind bind' return' unit' (eta_expand 2 (const, ts))
-    else IConst const `$$ map (imp_monad_bind bind' return' unit') ts
-  and imp_monad_bind bind' return' unit' (IConst const) = imp_monad_bind' bind' return' unit' const []
-    | imp_monad_bind bind' return' unit' (t as IVar _) = t
-    | imp_monad_bind bind' return' unit' (t as _ `$ _) = (case unfold_app t
-       of (IConst const, ts) => imp_monad_bind' bind' return' unit' const ts
-        | (t, ts) => imp_monad_bind bind' return' unit' t `$$ map (imp_monad_bind bind' return' unit') ts)
-    | imp_monad_bind bind' return' unit' (v_ty `|=> t) = v_ty `|=> imp_monad_bind bind' return' unit' t
-    | imp_monad_bind bind' return' unit' (ICase (((t, ty), pats), t0)) = ICase
-        (((imp_monad_bind bind' return' unit' t, ty), (map o pairself) (imp_monad_bind bind' return' unit') pats), imp_monad_bind bind' return' unit' t0);
+  let
+    fun is_const c = case lookup_const naming c
+     of SOME c' => (fn c'' => c' = c'')
+      | NONE => K false;
+    val is_bindM = is_const @{const_name bindM};
+    val is_return = is_const @{const_name return};
+    val dummy_name = "X";
+    val dummy_type = ITyVar dummy_name;
+    val dummy_case_term = IVar "";
+    (*assumption: dummy values are not relevant for serialization*)
+    val unitt = case lookup_const naming @{const_name Unity}
+     of SOME unit' => IConst (unit', (([], []), []))
+      | NONE => error ("Must include " ^ @{const_name Unity} ^ " in generated constants.");
+    fun dest_abs ((v, ty) `|=> t, _) = ((v, ty), t)
+      | dest_abs (t, ty) =
+          let
+            val vs = fold_varnames cons t [];
+            val v = Name.variant vs "x";
+            val ty' = (hd o fst o unfold_fun) ty;
+          in ((v, ty'), t `$ IVar v) end;
+    fun force (t as IConst (c, _) `$ t') = if is_return c
+          then t' else t `$ unitt
+      | force t = t `$ unitt;
+    fun tr_bind' [(t1, _), (t2, ty2)] =
+      let
+        val ((v, ty), t) = dest_abs (t2, ty2);
+      in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
+    and tr_bind'' t = case unfold_app t
+         of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if is_bindM c
+              then tr_bind' [(x1, ty1), (x2, ty2)]
+              else force t
+          | _ => force t;
+    fun imp_monad_bind'' ts = (dummy_name, dummy_type) `|=> ICase (((IVar dummy_name, dummy_type),
+      [(unitt, tr_bind' ts)]), dummy_case_term)
+    and imp_monad_bind' (const as (c, (_, tys))) ts = if is_bindM c then case (ts, tys)
+       of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)]
+        | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3
+        | (ts, _) => imp_monad_bind (eta_expand 2 (const, ts))
+      else IConst const `$$ map imp_monad_bind ts
+    and imp_monad_bind (IConst const) = imp_monad_bind' const []
+      | imp_monad_bind (t as IVar _) = t
+      | imp_monad_bind (t as _ `$ _) = (case unfold_app t
+         of (IConst const, ts) => imp_monad_bind' const ts
+          | (t, ts) => imp_monad_bind t `$$ map imp_monad_bind ts)
+      | imp_monad_bind (v_ty `|=> t) = v_ty `|=> imp_monad_bind t
+      | imp_monad_bind (ICase (((t, ty), pats), t0)) = ICase
+          (((imp_monad_bind t, ty),
+            (map o pairself) imp_monad_bind pats),
+              imp_monad_bind t0);
 
-  fun imp_program naming = (Graph.map_nodes o map_terms_stmt)
-    (imp_monad_bind (lookup naming @{const_name bindM})
-      (lookup naming @{const_name return})
-      (lookup naming @{const_name Unity}));
+  in (Graph.map_nodes o map_terms_stmt) imp_monad_bind end;
 
 in
 
-  Code_Target.extend_target ("SML_imp", ("SML", imp_program))
-  #> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
+Code_Target.extend_target ("SML_imp", ("SML", imp_program))
+#> Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program))
 
 end
+
 *}
 
-
 code_reserved OCaml Failure raise
 
 
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Imperative_HOL/Imperative_HOL_ex.thy
--- a/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Imperative_HOL/Imperative_HOL_ex.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -1,8 +1,9 @@
 (*  Title:      HOL/Imperative_HOL/Imperative_HOL_ex.thy
-    Author:     John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
+    Author:     John Matthews, Galois Connections;
+                Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen
 *)
 
-header {* Mmonadic imperative HOL with examples *}
+header {* Monadic imperative HOL with examples *}
 
 theory Imperative_HOL_ex
 imports Imperative_HOL "ex/Imperative_Quicksort"
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
--- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -631,9 +631,9 @@
 
 ML {* @{code qsort} (Array.fromList [42, 2, 3, 5, 0, 1705, 8, 3, 15]) () *}
 
-export_code qsort in SML_imp module_name QSort
+(*export_code qsort in SML_imp module_name QSort*)
 export_code qsort in OCaml module_name QSort file -
-export_code qsort in OCaml_imp module_name QSort file -
+(*export_code qsort in OCaml_imp module_name QSort file -*)
 export_code qsort in Haskell module_name QSort file -
 
 end
\ No newline at end of file
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Library/Float.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -59,6 +59,12 @@
    "real (Float -1 0) = -1" and "real (Float (number_of n) 0) = number_of n"
   by auto
 
+lemma float_number_of[simp]: "real (number_of x :: float) = number_of x"
+  by (simp only:number_of_float_def Float_num[unfolded number_of_is_id])
+
+lemma float_number_of_int[simp]: "real (Float n 0) = real n"
+  by (simp add: Float_num[unfolded number_of_is_id] real_of_float_simp pow2_def)
+
 lemma pow2_0[simp]: "pow2 0 = 1" by simp
 lemma pow2_1[simp]: "pow2 1 = 2" by simp
 lemma pow2_neg: "pow2 x = inverse (pow2 (-x))" by simp
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -85,13 +85,7 @@
 by (rule lemma_DERIV_subst, rule DERIV_add, auto)
 
 lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
-apply (induct p)
-apply simp
-apply (simp add: pderiv_pCons)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+
-apply simp
-done
+  by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
 
 text{* Consequences of the derivative theorem above*}
 
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Ln.thy
--- a/src/HOL/Ln.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Ln.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -343,43 +343,7 @@
 done
 
 lemma DERIV_ln: "0 < x ==> DERIV ln x :> 1 / x"
-  apply (unfold deriv_def, unfold LIM_eq, clarsimp)
-  apply (rule exI)
-  apply (rule conjI)
-  prefer 2
-  apply clarsimp
-  apply (subgoal_tac "(ln (x + xa) - ln x) / xa - (1 / x) = 
-      (ln (1 + xa / x) - xa / x) / xa")
-  apply (erule ssubst)
-  apply (subst abs_divide)
-  apply (rule mult_imp_div_pos_less)
-  apply force
-  apply (rule order_le_less_trans)
-  apply (rule abs_ln_one_plus_x_minus_x_bound)
-  apply (subst abs_divide)
-  apply (subst abs_of_pos, assumption)
-  apply (erule mult_imp_div_pos_le)
-  apply (subgoal_tac "abs xa < min (x / 2) (r * x^2 / 2)")
-  apply force
-  apply assumption
-  apply (simp add: power2_eq_square mult_compare_simps)
-  apply (rule mult_imp_div_pos_less)
-  apply (rule mult_pos_pos, assumption, assumption)
-  apply (subgoal_tac "xa * xa = abs xa * abs xa")
-  apply (erule ssubst)
-  apply (subgoal_tac "abs xa * (abs xa * 2) < abs xa * (r * (x * x))")
-  apply (simp only: mult_ac)
-  apply (rule mult_strict_left_mono)
-  apply (erule conjE, assumption)
-  apply force
-  apply simp
-  apply (subst ln_div [THEN sym])
-  apply arith
-  apply (auto simp add: algebra_simps add_frac_eq frac_eq_eq 
-    add_divide_distrib power2_eq_square)
-  apply (rule mult_pos_pos, assumption)+
-  apply assumption
-done
+  by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
 
 lemma ln_x_over_x_mono: "exp 1 <= x ==> x <= y ==> (ln y / y) <= (ln x / x)"  
 proof -
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/MacLaurin.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -27,36 +27,6 @@
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
 by arith
 
-text{*A crude tactic to differentiate by proof.*}
-
-lemmas deriv_rulesI =
-  DERIV_ident DERIV_const DERIV_cos DERIV_cmult
-  DERIV_sin DERIV_exp DERIV_inverse DERIV_pow
-  DERIV_add DERIV_diff DERIV_mult DERIV_minus
-  DERIV_inverse_fun DERIV_quotient DERIV_fun_pow
-  DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos
-  DERIV_ident DERIV_const DERIV_cos
-
-ML
-{*
-local
-exception DERIV_name;
-fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
-|   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
-|   get_fun_name _ = raise DERIV_name;
-
-in
-
-fun deriv_tac ctxt = SUBGOAL (fn (prem, i) =>
-  resolve_tac @{thms deriv_rulesI} i ORELSE
-    ((rtac (read_instantiate ctxt [(("f", 0), get_fun_name prem)]
-                     @{thm DERIV_chain2}) i) handle DERIV_name => no_tac));
-
-fun DERIV_tac ctxt = ALLGOALS (fn i => REPEAT (deriv_tac ctxt i));
-
-end
-*}
-
 lemma Maclaurin_lemma2:
   assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   assumes n: "n = Suc k"
@@ -91,13 +61,12 @@
  apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
  apply (rule DERIV_cmult)
  apply (rule lemma_DERIV_subst)
-  apply (best intro: DERIV_chain2 intro!: DERIV_intros)
+  apply (best intro!: DERIV_intros)
  apply (subst fact_Suc)
  apply (subst real_of_nat_mult)
  apply (simp add: mult_ac)
 done
 
-
 lemma Maclaurin:
   assumes h: "0 < h"
   assumes n: "0 < n"
@@ -565,9 +534,7 @@
     apply (clarify)
     apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
     apply (cut_tac m=m in mod_exhaust_less_4)
-    apply (safe, simp_all)
-    apply (rule DERIV_minus, simp)
-    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
+    apply (safe, auto intro!: DERIV_intros)
     done
   from Maclaurin_all_le [OF diff_0 DERIV_diff]
   obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -450,7 +450,7 @@
 qed
 
 lemma [code]:
-  "iter f step ss w = while (\<lambda>(ss, w). \<not> (is_empty w))
+  "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
     (\<lambda>(ss, w).
         let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
     (ss, w)"
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/NthRoot.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -372,6 +372,41 @@
     using odd_pos [OF n] by (rule isCont_real_root)
 qed
 
+lemma DERIV_even_real_root:
+  assumes n: "0 < n" and "even n"
+  assumes x: "x < 0"
+  shows "DERIV (root n) x :> inverse (- real n * root n x ^ (n - Suc 0))"
+proof (rule DERIV_inverse_function)
+  show "x - 1 < x" by simp
+  show "x < 0" using x .
+next
+  show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
+  proof (rule allI, rule impI, erule conjE)
+    fix y assume "x - 1 < y" and "y < 0"
+    hence "root n (-y) ^ n = -y" using `0 < n` by simp
+    with real_root_minus[OF `0 < n`] and `even n`
+    show "- (root n y ^ n) = y" by simp
+  qed
+next
+  show "DERIV (\<lambda>x. - (x ^ n)) (root n x) :> - real n * root n x ^ (n - Suc 0)"
+    by  (auto intro!: DERIV_intros)
+  show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
+    using n x by simp
+  show "isCont (root n) x"
+    using n by (rule isCont_real_root)
+qed
+
+lemma DERIV_real_root_generic:
+  assumes "0 < n" and "x \<noteq> 0"
+  and even: "\<lbrakk> even n ; 0 < x \<rbrakk> \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+  and even: "\<lbrakk> even n ; x < 0 \<rbrakk> \<Longrightarrow> D = - inverse (real n * root n x ^ (n - Suc 0))"
+  and odd: "odd n \<Longrightarrow> D = inverse (real n * root n x ^ (n - Suc 0))"
+  shows "DERIV (root n) x :> D"
+using assms by (cases "even n", cases "0 < x",
+  auto intro: DERIV_real_root[THEN DERIV_cong]
+              DERIV_odd_real_root[THEN DERIV_cong]
+              DERIV_even_real_root[THEN DERIV_cong])
+
 subsection {* Square Root *}
 
 definition
@@ -456,9 +491,21 @@
 lemma isCont_real_sqrt: "isCont sqrt x"
 unfolding sqrt_def by (rule isCont_real_root [OF pos2])
 
+lemma DERIV_real_sqrt_generic:
+  assumes "x \<noteq> 0"
+  assumes "x > 0 \<Longrightarrow> D = inverse (sqrt x) / 2"
+  assumes "x < 0 \<Longrightarrow> D = - inverse (sqrt x) / 2"
+  shows "DERIV sqrt x :> D"
+  using assms unfolding sqrt_def
+  by (auto intro!: DERIV_real_root_generic)
+
 lemma DERIV_real_sqrt:
   "0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2"
-unfolding sqrt_def by (rule DERIV_real_root [OF pos2, simplified])
+  using DERIV_real_sqrt_generic by simp
+
+declare
+  DERIV_real_sqrt_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_real_root_generic[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
 
 lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
 apply auto
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -18,7 +18,7 @@
   val the_info : theory -> string -> info
   val the_descr : theory -> string list
     -> descr * (string * sort) list * string list
-      * (string list * string list) * (typ list * typ list)
+      * string * (string list * string list) * (typ list * typ list)
   val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
   val get_constrs : theory -> string -> (string * typ) list option
   val get_all : theory -> info Symtab.table
@@ -125,9 +125,10 @@
 
     val names = map Long_Name.base_name (the_default tycos (#alt_names info));
     val (auxnames, _) = Name.make_context names
-      |> fold_map (yield_singleton Name.variants o name_of_typ) Us
+      |> fold_map (yield_singleton Name.variants o name_of_typ) Us;
+    val prefix = space_implode "_" names;
 
-  in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
+  in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
 
 fun get_constrs thy dtco =
   case try (the_spec thy) dtco
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -11,10 +11,10 @@
     -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed
   val ensure_random_typecopy: string -> theory -> theory
-  val random_aux_specification: string -> term list -> local_theory -> local_theory
+  val random_aux_specification: string -> string -> term list -> local_theory -> local_theory
   val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list
     -> string list -> string list * string list -> typ list * typ list
-    -> string * (term list * (term * term) list)
+    -> term list * (term * term) list
   val ensure_random_datatype: Datatype.config -> string list -> theory -> theory
   val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
   val setup: theory -> theory
@@ -184,18 +184,18 @@
 
 end;
 
-fun random_aux_primrec_multi prefix [eq] lthy =
+fun random_aux_primrec_multi auxname [eq] lthy =
       lthy
       |> random_aux_primrec eq
       |>> (fn simp => [simp])
-  | random_aux_primrec_multi prefix (eqs as _ :: _ :: _) lthy =
+  | random_aux_primrec_multi auxname (eqs as _ :: _ :: _) lthy =
       let
         val thy = ProofContext.theory_of lthy;
         val (lhss, rhss) = map_split (HOLogic.dest_eq o HOLogic.dest_Trueprop) eqs;
         val (vs, (arg as Free (v, _)) :: _) = map_split (fn (t1 $ t2) => (t1, t2)) lhss;
         val Ts = map fastype_of lhss;
         val tupleT = foldr1 HOLogic.mk_prodT Ts;
-        val aux_lhs = Free ("mutual_" ^ prefix, fastype_of arg --> tupleT) $ arg;
+        val aux_lhs = Free ("mutual_" ^ auxname, fastype_of arg --> tupleT) $ arg;
         val aux_eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq)
           (aux_lhs, foldr1 HOLogic.mk_prod rhss);
         fun mk_proj t [T] = [t]
@@ -223,7 +223,7 @@
         |-> (fn (aux_simp, proj_defs) => prove_eqs aux_simp proj_defs)
       end;
 
-fun random_aux_specification prefix eqs lthy =
+fun random_aux_specification prfx name eqs lthy =
   let
     val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq
       o HOLogic.dest_Trueprop o hd) eqs) [];
@@ -237,10 +237,10 @@
         val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
         val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
       in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
-    val b = Binding.qualify true prefix (Binding.name "simps");
+    val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
   in
     lthy
-    |> random_aux_primrec_multi prefix proto_eqs
+    |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> (fn proto_simps => prove_simps proto_simps)
     |-> (fn simps => LocalTheory.note Thm.generatedK ((b,
            Code.add_default_eqn_attrib :: map (Attrib.internal o K)
@@ -252,6 +252,8 @@
 
 (* constructing random instances on datatypes *)
 
+val random_auxN = "random_aux";
+
 fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) =
   let
     val mk_const = curry (Sign.mk_const thy);
@@ -259,7 +261,6 @@
     val i1 = @{term "(i\<Colon>code_numeral) - 1"};
     val j = @{term "j\<Colon>code_numeral"};
     val seed = @{term "s\<Colon>Random.seed"};
-    val random_auxN = "random_aux";
     val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames);
     fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \<Rightarrow> term"});
     val rTs = Ts @ Us;
@@ -316,10 +317,9 @@
           $ seed;
     val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs;
     val auxs_rhss = map mk_select gen_exprss;
-    val prefix = space_implode "_" (random_auxN :: names);
-  in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
+  in (random_auxs, auxs_lhss ~~ auxs_rhss) end;
 
-fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
+fun mk_random_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
   let
     val _ = DatatypeAux.message config "Creating quickcheck generators ...";
     val i = @{term "i\<Colon>code_numeral"};
@@ -329,14 +329,14 @@
           else @{term "max :: code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"}
             $ HOLogic.mk_number @{typ code_numeral} l $ i
       | NONE => i;
-    val (prefix, (random_auxs, auxs_eqs)) = (apsnd o apsnd o map) mk_prop_eq
+    val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq
       (mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us));
     val random_defs = map_index (fn (k, T) => mk_prop_eq
       (HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts;
   in
     thy
     |> TheoryTarget.instantiation (tycos, vs, @{sort random})
-    |> random_aux_specification prefix auxs_eqs
+    |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
           Specification.definition (NONE, (Attrib.empty_binding,
@@ -359,7 +359,7 @@
   let
     val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy;
-    val (descr, raw_vs, tycos, (names, auxnames), raw_TUs) =
+    val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
       Datatype.the_descr thy raw_tycos;
     val typrep_vs = (map o apsnd)
       (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
@@ -374,7 +374,7 @@
   in if has_inst then thy
     else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
      of SOME constrain => mk_random_datatype config descr
-          (map constrain typrep_vs) tycos (names, auxnames)
+          (map constrain typrep_vs) tycos prfx (names, auxnames)
             ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
       | NONE => thy
   end;
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -11,8 +11,9 @@
   val prepare_clauses : bool -> thm list -> thm list ->
     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
-    ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
-    ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
+    ResHolClause.axiom_name vector *
+      (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list *
+      ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
 end;
 
 structure ResAtp: RES_ATP =
@@ -550,13 +551,14 @@
     and tycons = type_consts_of_terms thy (ccltms@axtms)
     (*TFrees in conjecture clauses; TVars in axiom clauses*)
     val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
+    val (_, extra_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy extra_cls)
     val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
     val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
     val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
     val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   in
     (Vector.fromList clnames,
-      (conjectures, axiom_clauses, helper_clauses, classrel_clauses, arity_clauses))
+      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   end
 
 end;
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -36,10 +36,12 @@
        clause list * (thm * (axiom_name * clause_id)) list * string list ->
        clause list
   val tptp_write_file: bool -> Path.T ->
-    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
+    clause list * clause list * clause list * clause list *
+    ResClause.classrelClause list * ResClause.arityClause list ->
     int * int
   val dfg_write_file: bool -> Path.T ->
-    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list ->
+    clause list * clause list * clause list * clause list *
+    ResClause.classrelClause list * ResClause.arityClause list ->
     int * int
 end
 
@@ -459,11 +461,11 @@
   Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
                 (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
 
-fun count_constants (conjectures, axclauses, helper_clauses, _, _) =
+fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
   if minimize_applies then
      let val (const_min_arity, const_needs_hBOOL) =
           fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
-       |> fold count_constants_clause axclauses
+       |> fold count_constants_clause extra_clauses
        |> fold count_constants_clause helper_clauses
      val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
      in (const_min_arity, const_needs_hBOOL) end
@@ -473,7 +475,8 @@
 
 fun tptp_write_file t_full file clauses =
   let
-    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+    val (conjectures, axclauses, _, helper_clauses,
+      classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
     val params = (t_full, cma, cnh)
     val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
@@ -494,7 +497,8 @@
 
 fun dfg_write_file t_full file clauses =
   let
-    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
+    val (conjectures, axclauses, _, helper_clauses,
+      classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
     val params = (t_full, cma, cnh)
     val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -457,9 +457,28 @@
     in  trace msg; msg  end;
 
 
-    
-  (* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
-  
+  (*=== EXTRACTING PROOF-TEXT === *)
+
+  val begin_proof_strings = ["# SZS output start CNFRefutation.",
+      "=========== Refutation ==========",
+  "Here is a proof"];
+  val end_proof_strings = ["# SZS output end CNFRefutation",
+      "======= End of refutation =======",
+  "Formulae used in the proof"];
+  fun get_proof_extract proof =
+    let
+    (*splits to_split by the first possible of a list of splitters*)
+    val (begin_string, end_string) =
+      (find_first (fn s => String.isSubstring s proof) begin_proof_strings,
+      find_first (fn s => String.isSubstring s proof) end_proof_strings)
+    in
+      if is_none begin_string orelse is_none end_string
+      then error "Could not extract proof (no substring indicating a proof)"
+      else proof |> first_field (the begin_string) |> the |> snd
+                 |> first_field (the end_string) |> the |> fst end;
+
+(* ==== CHECK IF PROOF OF E OR VAMPIRE WAS SUCCESSFUL === *)
+
   val failure_strings_E = ["SZS status: Satisfiable","SZS status Satisfiable",
     "SZS status: ResourceOut","SZS status ResourceOut","# Cannot determine problem status"];
   val failure_strings_vampire = ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
@@ -469,31 +488,15 @@
   fun find_failure proof =
     let val failures =
       map_filter (fn s => if String.isSubstring s proof then SOME s else NONE)
-         (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
-    in if null failures then NONE else SOME (hd failures) end;
-    
-  (*=== EXTRACTING PROOF-TEXT === *)
-  
-  val begin_proof_strings = ["# SZS output start CNFRefutation.",
-      "=========== Refutation ==========",
-  "Here is a proof"];
-  val end_proof_strings = ["# SZS output end CNFRefutation",
-      "======= End of refutation =======",
-  "Formulae used in the proof"];
-  fun get_proof_extract proof =
-    let
-    (*splits to_split by the first possible of a list of splitters*)
-    fun first_field_any [] to_split = NONE
-      | first_field_any (splitter::splitters) to_split =
-      let
-      val result = (first_field splitter to_split)
-      in
-        if isSome result then result else first_field_any splitters to_split
-      end
-    val (a:string, b:string) = valOf (first_field_any begin_proof_strings proof)
-    val (proofextract:string, c:string) = valOf (first_field_any end_proof_strings b)
-    in proofextract end;
-  
+        (failure_strings_E @ failure_strings_vampire @ failure_strings_SPASS @ failure_strings_remote)
+    val correct = null failures andalso
+      exists (fn s => String.isSubstring s proof) begin_proof_strings andalso
+      exists (fn s => String.isSubstring s proof) end_proof_strings
+    in
+      if correct then NONE
+      else if null failures then SOME "Output of ATP not in proper format"
+      else SOME (hd failures) end;
+
   (* === EXTRACTING LEMMAS === *)
   (* lines have the form "cnf(108, axiom, ...",
   the number (108) has to be extracted)*)
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/Transcendental.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -784,9 +784,8 @@
 	  also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
 	  finally show ?thesis .
 	qed }
-      { fix n
-	from DERIV_pow[of "Suc n" x0, THEN DERIV_cmult[where c="f n"]]
-	show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" unfolding real_mult_assoc by auto }
+      { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
+	  by (auto intro!: DERIV_intros simp del: power_Suc) }
       { fix x assume "x \<in> {-R' <..< R'}" hence "R' \<in> {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto
 	have "summable (\<lambda> n. f n * x^n)"
 	proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI)
@@ -1362,6 +1361,12 @@
 by (rule DERIV_cos [THEN DERIV_isCont])
 
 
+declare
+  DERIV_exp[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_ln[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_sin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_cos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
 subsection {* Properties of Sine and Cosine *}
 
 lemma sin_zero [simp]: "sin 0 = 0"
@@ -1410,24 +1415,17 @@
 by auto
 
 lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_realpow2a, auto)
-done
+  by (auto intro!: DERIV_intros)
 
 (* most useful *)
 lemma DERIV_cos_cos_mult3 [simp]:
      "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_cos_mult2, auto)
-done
+  by (auto intro!: DERIV_intros)
 
 lemma DERIV_sin_circle_all: 
      "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>  
              (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
-apply (simp only: diff_minus, safe)
-apply (rule DERIV_add) 
-apply (auto simp add: numeral_2_eq_2)
-done
+  by (auto intro!: DERIV_intros)
 
 lemma DERIV_sin_circle_all_zero [simp]:
      "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
@@ -1513,22 +1511,12 @@
 apply (rule DERIV_cos, auto)
 done
 
-lemmas DERIV_intros = DERIV_ident DERIV_const DERIV_cos DERIV_cmult 
-                    DERIV_sin  DERIV_exp  DERIV_inverse DERIV_pow 
-                    DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
-                    DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
-                    DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
-
 (* lemma *)
 lemma lemma_DERIV_sin_cos_add:
      "\<forall>x.  
          DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
                (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2) 
-  --{*replaces the old @{text DERIV_tac}*}
-apply (auto simp add: algebra_simps)
-done
+  by (auto intro!: DERIV_intros simp add: algebra_simps)
 
 lemma sin_cos_add [simp]:
      "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
@@ -1550,10 +1538,8 @@
 
 lemma lemma_DERIV_sin_cos_minus:
     "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
-apply (simp add: algebra_simps)
-done
+  by (auto intro!: DERIV_intros simp add: algebra_simps)
+
 
 lemma sin_cos_minus: 
     "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
@@ -1722,7 +1708,7 @@
 apply (assumption, rule_tac y=y in order_less_le_trans, simp_all) 
 apply (drule_tac y1 = y in order_le_less_trans [THEN sin_gt_zero], assumption, simp_all) 
 done
-    
+
 lemma pi_half: "pi/2 = (THE x. 0 \<le> x & x \<le> 2 & cos x = 0)"
 by (simp add: pi_def)
 
@@ -2121,10 +2107,7 @@
 
 lemma lemma_DERIV_tan:
      "cos x \<noteq> 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\<twosuperior>)"
-apply (rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2) 
-apply (auto simp add: divide_inverse numeral_2_eq_2)
-done
+  by (auto intro!: DERIV_intros simp add: field_simps numeral_2_eq_2)
 
 lemma DERIV_tan [simp]: "cos x \<noteq> 0 ==> DERIV tan x :> inverse((cos x)\<twosuperior>)"
 by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
@@ -2500,6 +2483,11 @@
 apply (simp, simp, simp, rule isCont_arctan)
 done
 
+declare
+  DERIV_arcsin[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_arccos[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+  DERIV_arctan[THEN DERIV_chain2, THEN DERIV_cong, DERIV_intros]
+
 subsection {* More Theorems about Sin and Cos *}
 
 lemma cos_45: "cos (pi / 4) = sqrt 2 / 2"
@@ -2589,11 +2577,7 @@
 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
 
 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = sin and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+  by (auto intro!: DERIV_intros)
 
 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
 proof -
@@ -2634,11 +2618,7 @@
 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
 
 lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = cos and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+  by (auto intro!: DERIV_intros)
 
 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
 by (auto simp add: sin_zero_iff even_mult_two_ex)
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/ex/Predicate_Compile_ex.thy
--- a/src/HOL/ex/Predicate_Compile_ex.thy	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile_ex.thy	Tue Jun 30 21:23:01 2009 +0200
@@ -58,7 +58,7 @@
 
 lemma [code_pred_intros]:
 "r a b ==> tranclp r a b"
-"r a b ==> tranclp r b c ==> tranclp r a c" 
+"r a b ==> tranclp r b c ==> tranclp r a c"
 by auto
 
 (* Setup requires quick and dirty proof *)
@@ -71,7 +71,6 @@
 
 thm tranclp.equation
 *)
-
 inductive succ :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
     "succ 0 1"
   | "succ m n \<Longrightarrow> succ (Suc m) (Suc n)"
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -9,6 +9,8 @@
   type mode = int list option list * int list
   val add_equations_of: string list -> theory -> theory
   val register_predicate : (thm list * thm * int) -> theory -> theory
+  val is_registered : theory -> string -> bool
+  val fetch_pred_data : theory -> string -> (thm list * thm * int)  
   val predfun_intro_of: theory -> string -> mode -> thm
   val predfun_elim_of: theory -> string -> mode -> thm
   val strip_intro_concl: int -> term -> term * (term list * term list)
@@ -17,14 +19,18 @@
   val modes_of: theory -> string -> mode list
   val intros_of: theory -> string -> thm list
   val nparams_of: theory -> string -> int
+  val add_intro: thm -> theory -> theory
+  val set_elim: thm -> theory -> theory
   val setup: theory -> theory
   val code_pred: string -> Proof.context -> Proof.state
   val code_pred_cmd: string -> Proof.context -> Proof.state
-(*  val print_alternative_rules: theory -> theory (*FIXME diagnostic command?*) *)
+  val print_stored_rules: theory -> unit
   val do_proofs: bool ref
+  val mk_casesrule : Proof.context -> int -> thm list -> term
   val analyze_compr: theory -> term -> term
   val eval_ref: (unit -> term Predicate.pred) option ref
   val add_equations : string -> theory -> theory
+  val code_pred_intros_attrib : attribute
 end;
 
 structure Predicate_Compile : PREDICATE_COMPILE =
@@ -187,7 +193,7 @@
  of NONE => error ("No such predicate " ^ quote name)  
   | SOME data => data;
 
-val is_pred = is_some oo lookup_pred_data 
+val is_registered = is_some oo lookup_pred_data 
 
 val all_preds_of = Graph.keys o PredData.get
 
@@ -223,25 +229,26 @@
 
 val predfun_elim_of = #elim ooo the_predfun_data
 
+fun print_stored_rules thy =
+  let
+    val preds = (Graph.keys o PredData.get) thy
+    fun print pred () = let
+      val _ = writeln ("predicate: " ^ pred)
+      val _ = writeln ("number of parameters: " ^ string_of_int (nparams_of thy pred))
+      val _ = writeln ("introrules: ")
+      val _ = fold (fn thm => fn u =>  writeln (Display.string_of_thm thm))
+        (rev (intros_of thy pred)) ()
+    in
+      if (has_elim thy pred) then
+        writeln ("elimrule: " ^ Display.string_of_thm (the_elim_of thy pred))
+      else
+        writeln ("no elimrule defined")
+    end
+  in
+    fold print preds ()
+  end;
 
-(* replaces print_alternative_rules *)
-(* TODO:
-fun print_alternative_rules thy = let
-    val d = IndCodegenData.get thy
-    val preds = (Symtab.keys (#intro_rules d)) union (Symtab.keys (#elim_rules d))
-    val _ = tracing ("preds: " ^ (makestring preds))
-    fun print pred = let
-      val _ = tracing ("predicate: " ^ pred)
-      val _ = tracing ("introrules: ")
-      val _ = fold (fn thm => fn u => tracing (makestring thm))
-        (rev (Symtab.lookup_list (#intro_rules d) pred)) ()
-      val _ = tracing ("casesrule: ")
-      val _ = tracing (makestring (Symtab.lookup (#elim_rules d) pred))
-    in () end
-    val _ = map print preds
- in thy end;
-*)
-
+(** preprocessing rules **)  
 
 fun imp_prems_conv cv ct =
   case Thm.term_of ct of
@@ -298,6 +305,23 @@
     val add = apsnd (cons (mode, mk_predfun_data data))
   in PredData.map (Graph.map_node name (map_pred_data add)) end
 
+fun is_inductive_predicate thy name =
+  is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
+
+fun depending_preds_of thy intros = fold Term.add_consts (map Thm.prop_of intros) [] |> map fst
+    |> filter (fn c => is_inductive_predicate thy c orelse is_registered thy c)
+
+(* code dependency graph *)    
+fun dependencies_of thy name =
+  let
+    val (intros, elim, nparams) = fetch_pred_data thy name 
+    val data = mk_pred_data ((intros, SOME elim, nparams), [])
+    val keys = depending_preds_of thy intros
+  in
+    (data, keys)
+  end;
+
+(* TODO: add_edges - by analysing dependencies *)
 fun add_intro thm thy = let
    val (name, _) = dest_Const (fst (strip_intro_concl 0 (prop_of thm)))
    fun cons_intro gr =
@@ -320,10 +344,13 @@
     fun set (intros, elim, _ ) = (intros, elim, nparams) 
   in PredData.map (Graph.map_node name (map_pred_data (apfst set))) end
 
-fun register_predicate (intros, elim, nparams) = let
+fun register_predicate (intros, elim, nparams) thy = let
     val (name, _) = dest_Const (fst (strip_intro_concl nparams (prop_of (hd intros))))
     fun set _ = (intros, SOME elim, nparams)
-  in PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))) end
+  in
+    PredData.map (Graph.new_node (name, mk_pred_data ((intros, SOME elim, nparams), []))
+      #> fold Graph.add_edge (map (pair name) (depending_preds_of thy intros))) thy
+  end
 
   
 (* Mode analysis *)
@@ -625,10 +652,11 @@
 
 and compile_param thy modes (NONE, t) = t
  | compile_param thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
-   (case t of
-     Abs _ => compile_param_ext thy modes (m, t)
-   |  _ => let
-     val (f, args) = strip_comb t
+   (* (case t of
+     Abs _ => error "compile_param: Invalid term" *) (* compile_param_ext thy modes (m, t) *)
+   (*  |  _ => let *)
+   let  
+     val (f, args) = strip_comb (Envir.eta_contract t)
      val (params, args') = chop (length ms) args
      val params' = map (compile_param thy modes) (ms ~~ params)
      val f' = case f of
@@ -637,7 +665,7 @@
              Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
           else error "compile param: Not an inductive predicate with correct mode"
       | Free (name, T) => Free (name, funT_of T (SOME is'))
-   in list_comb (f', params' @ args') end)
+   in list_comb (f', params' @ args') end
  | compile_param _ _ _ = error "compile params"
   
   
@@ -1116,7 +1144,7 @@
 (* VERY LARGE SIMILIRATIY to function prove_param 
 -- join both functions
 *)
-(*
+
 fun prove_param2 thy modes (NONE, t) = all_tac 
   | prove_param2 thy modes (m as SOME (Mode (mode, is, ms)), t) = let
     val  (f, args) = strip_comb t
@@ -1132,7 +1160,7 @@
     THEN print_tac "after simplification in prove_args"
     THEN (EVERY (map (prove_param2 thy modes) (ms ~~ params)))
   end
-*)
+
 
 fun prove_expr2 thy modes (SOME (Mode (mode, is, ms)), t) = 
   (case strip_comb t of
@@ -1140,14 +1168,16 @@
       if AList.defined op = modes name then
         etac @{thm bindE} 1
         THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
+        THEN new_print_tac "prove_expr2-before"
         THEN (debug_tac (Syntax.string_of_term_global thy
           (prop_of (predfun_elim_of thy name mode))))
         THEN (etac (predfun_elim_of thy name mode) 1)
         THEN new_print_tac "prove_expr2"
         (* TODO -- FIXME: replace remove_last_goal*)
-        THEN (EVERY (replicate (length args) (remove_last_goal thy)))
+        (* THEN (EVERY (replicate (length args) (remove_last_goal thy))) *)
+        THEN (EVERY (map (prove_param thy modes) (ms ~~ args)))
         THEN new_print_tac "finished prove_expr2"
-        (* THEN (EVERY (map (prove_param thy modes) (ms ~~ args))) *)
+      
       else error "Prove expr2 if case not implemented"
     | _ => etac @{thm bindE} 1)
   | prove_expr2 _ _ _ = error "Prove expr2 not implemented"
@@ -1243,7 +1273,7 @@
     end;
   val prems_tac = prove_prems2 in_ts' param_vs ps 
 in
-  print_tac "starting prove_clause2"
+  new_print_tac "starting prove_clause2"
   THEN etac @{thm bindE} 1
   THEN (etac @{thm singleE'} 1)
   THEN (TRY (etac @{thm Pair_inject} 1))
@@ -1259,6 +1289,7 @@
   (DETERM (TRY (rtac @{thm unit.induct} 1)))
    THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
    THEN (rtac (predfun_intro_of thy pred mode) 1)
+   THEN (REPEAT_DETERM (rtac @{thm refl} 2))
    THEN (EVERY (map prove_clause (clauses ~~ (1 upto (length clauses)))))
 end;
 
@@ -1321,7 +1352,7 @@
         | Negprem _ => error ("Double negation not allowed in premise: " ^ (Syntax.string_of_term_global thy (c $ t))) 
         | Sidecond t => Sidecond (c $ t))
       | (c as Const (s, _), ts) =>
-        if is_pred thy s then
+        if is_registered thy s then
           let val (ts1, ts2) = chop (nparams_of thy s) ts
           in Prem (ts2, list_comb (c, ts1)) end
         else Sidecond t
@@ -1373,7 +1404,7 @@
   val _ = map (Output.tracing o (Syntax.string_of_term_global thy')) (flat ts)
   val pred_mode =
     maps (fn (s, (T, _)) => map (pair (s, T)) ((the o AList.lookup (op =) modes) s)) clauses' 
-  val _ = tracing "Proving equations..."
+  val _ = Output.tracing "Proving equations..."
   val result_thms =
     prove_preds thy' all_vs param_vs (extra_modes @ modes) clauses (pred_mode ~~ (flat ts))
   val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
@@ -1409,21 +1440,6 @@
     val cases = map mk_case intros
   in Logic.list_implies (assm :: cases, prop) end;
 
-(* code dependency graph *)
-
-fun dependencies_of thy name =
-  let
-    fun is_inductive_predicate thy name =
-      is_some (try (Inductive.the_inductive (ProofContext.init thy)) name)
-    val (intro, elim, nparams) = fetch_pred_data thy name 
-    val data = mk_pred_data ((intro, SOME elim, nparams), [])
-    val intros = map Thm.prop_of (#intros (rep_pred_data data))
-    val keys = fold Term.add_consts intros [] |> map fst
-    |> filter (is_inductive_predicate thy)
-  in
-    (data, keys)
-  end;
-
 fun add_equations name thy =
   let
     val thy' = PredData.map (Graph.extend (dependencies_of thy) name) thy |> Theory.checkpoint;
@@ -1437,17 +1453,15 @@
       scc thy' |> Theory.checkpoint
   in thy'' end
 
+  
+fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
+
+val code_pred_intros_attrib = attrib add_intro;
+
 (** user interface **)
 
 local
 
-fun attrib f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
-
-(*
-val add_elim_attrib = attrib set_elim;
-*)
-
-
 (* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
 (* TODO: must create state to prove multiple cases *)
 fun generic_code_pred prep_const raw_const lthy =
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -32,6 +32,7 @@
   (*instances*)
   val init_instantiation: string list * (string * sort) list * sort
     -> theory -> local_theory
+  val instance_arity_cmd: xstring list * xstring list * xstring -> theory -> Proof.state
   val instantiation_instance: (local_theory -> local_theory)
     -> local_theory -> Proof.state
   val prove_instantiation_instance: (Proof.context -> tactic)
@@ -44,7 +45,8 @@
   val instantiation_param: local_theory -> binding -> string option
   val confirm_declaration: binding -> local_theory -> local_theory
   val pretty_instantiation: local_theory -> Pretty.T
-  val instance_arity_cmd: xstring * xstring list * xstring -> theory -> Proof.state
+  val read_multi_arity: theory -> xstring list * xstring list * xstring
+    -> string list * (string * sort) list * sort
   val type_name: string -> string
 
   (*subclasses*)
@@ -419,6 +421,15 @@
   |> find_first (fn (_, (v, _)) => Binding.name_of b = v)
   |> Option.map (fst o fst);
 
+fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
+  let
+    val all_arities = map (fn raw_tyco => Sign.read_arity thy
+      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
+    val tycos = map #1 all_arities;
+    val (_, sorts, sort) = hd all_arities;
+    val vs = Name.names Name.context Name.aT sorts;
+  in (tycos, vs, sort) end;
+
 
 (* syntax *)
 
@@ -578,15 +589,17 @@
 
 (* simplified instantiation interface with no class parameter *)
 
-fun instance_arity_cmd arities thy =
+fun instance_arity_cmd raw_arities thy =
   let
+    val (tycos, vs, sort) = read_multi_arity thy raw_arities;
+    val sorts = map snd vs;
+    val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
     fun after_qed results = ProofContext.theory
       ((fold o fold) AxClass.add_arity results);
   in
     thy
     |> ProofContext.init
-    |> Proof.theorem_i NONE after_qed ((map (fn t => [(t, [])])
-        o Logic.mk_arities o Sign.read_arity thy) arities)
+    |> Proof.theorem_i NONE after_qed (map (fn t => [(t, [])]) arities)
   end;
 
 
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -465,7 +465,7 @@
 val _ =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> Class.classrel_cmd ||
-    P.arity >> Class.instance_arity_cmd)
+    P.multi_arity >> Class.instance_arity_cmd)
     >> (Toplevel.print oo Toplevel.theory_to_proof)
   || Scan.succeed (Toplevel.print o Toplevel.local_theory_to_proof NONE (Class.instantiation_instance I)));
 
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -330,15 +330,6 @@
        else I)}
 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;
 
-fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
-  let
-    val all_arities = map (fn raw_tyco => Sign.read_arity thy
-      (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
-    val tycos = map #1 all_arities;
-    val (_, sorts, sort) = hd all_arities;
-    val vs = Name.names Name.context Name.aT sorts;
-  in (tycos, vs, sort) end;
-
 fun gen_overloading prep_const raw_ops thy =
   let
     val ctxt = ProofContext.init thy;
@@ -356,7 +347,7 @@
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
 fun instantiation_cmd raw_arities thy =
-  instantiation (read_multi_arity thy raw_arities) thy;
+  instantiation (Class_Target.read_multi_arity thy raw_arities) thy;
 
 val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
 val overloading_cmd = gen_overloading Syntax.read_term;
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/Tools/Code/code_haskell.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -25,10 +25,8 @@
 
 fun pr_haskell_bind pr_term =
   let
-    fun pr_bind ((NONE, NONE), _) = str "_"
-      | pr_bind ((SOME v, NONE), _) = str v
-      | pr_bind ((NONE, SOME p), _) = p
-      | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
+    fun pr_bind (NONE, _) = str "_"
+      | pr_bind (SOME p, _) = p;
   in gen_pr_bind pr_bind pr_term end;
 
 fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
@@ -72,9 +70,8 @@
           (str o Code_Printer.lookup_var vars) v
       | pr_term tyvars thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
-            val (ps, vars') = fold_map pr binds vars;
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            val (ps, vars') = fold_map (pr_bind tyvars thm BR) binds vars;
           in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end
       | pr_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
           (case Code_Thingol.unfold_const_app t0
@@ -103,7 +100,7 @@
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
+              |> pr_bind tyvars thm BR (SOME pat, ty)
               |>> (fn p => semicolon [p, str "=", pr_term tyvars thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in brackify_block fxy (str "let {")
@@ -114,7 +111,7 @@
           let
             fun pr (pat, body) =
               let
-                val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind tyvars thm NOBR (SOME pat, ty) vars;
               in semicolon [p, str "->", pr_term tyvars thm vars' NOBR body] end;
           in brackify_block fxy
             (concat [str "case", pr_term tyvars thm vars NOBR t, str "of", str "{"])
@@ -240,8 +237,6 @@
           end
       | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
           let
-            val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE);
-            val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure;
             val tyvars = Code_Printer.intro_vars (map fst vs) init_syms;
             fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam
              of NONE => semicolon [
@@ -255,7 +250,7 @@
                     val const = if (is_some o syntax_const) c_inst_name
                       then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
                     val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
-                    val (vs, rhs) = unfold_abs_pure proto_rhs;
+                    val (vs, rhs) = (apfst o map) fst (Code_Thingol.unfold_abs proto_rhs);
                     val vars = init_syms
                       |> Code_Printer.intro_vars (the_list const)
                       |> Code_Printer.intro_vars vs;
@@ -447,16 +442,16 @@
 
 fun pretty_haskell_monad c_bind =
   let
-    fun dest_bind t1 t2 = case Code_Thingol.split_abs t2
-     of SOME (((v, pat), ty), t') =>
-          SOME ((SOME (((SOME v, pat), ty), true), t1), t')
+    fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
+     of SOME ((some_pat, ty), t') =>
+          SOME ((SOME ((some_pat, ty), true), t1), t')
       | NONE => NONE;
     fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
           if c = c_bind_name then dest_bind t1 t2
           else NONE
       | dest_monad _ t = case Code_Thingol.split_let t
          of SOME (((pat, ty), tbind), t') =>
-              SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
+              SOME ((SOME ((SOME pat, ty), false), tbind), t')
           | NONE => NONE;
     fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
     fun pr_monad pr_bind pr (NONE, t) vars =
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/Tools/Code/code_ml.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -94,9 +94,9 @@
                [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) =
-              pr_bind is_closure thm NOBR ((SOME v, pat), ty)
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            fun pr (some_pat, ty) =
+              pr_bind is_closure thm NOBR (some_pat, ty)
               #>> (fn p => concat [str "fn", p, str "=>"]);
             val (ps, vars') = fold_map pr binds vars;
           in brackets (ps @ [pr_term is_closure thm vars' NOBR t']) end
@@ -122,17 +122,15 @@
           :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
     and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
       syntax_const thm vars
-    and pr_bind' ((NONE, NONE), _) = str "_"
-      | pr_bind' ((SOME v, NONE), _) = str v
-      | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+    and pr_bind' (NONE, _) = str "_"
+      | pr_bind' (SOME p, _) = p
     and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
     and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+              |> pr_bind is_closure thm NOBR (SOME pat, ty)
               |>> (fn p => semicolon [str "val", p, str "=", pr_term is_closure thm vars NOBR t])
             val (ps, vars') = fold_map pr binds vars;
           in
@@ -146,7 +144,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
               in
                 concat [str delim, p, str "=>", pr_term is_closure thm vars' NOBR body]
               end;
@@ -403,9 +401,8 @@
                 brackify fxy [pr_term is_closure thm vars NOBR t1, pr_term is_closure thm vars BR t2])
       | pr_term is_closure thm vars fxy (t as _ `|=> _) =
           let
-            val (binds, t') = Code_Thingol.unfold_abs t;
-            fun pr ((v, pat), ty) = pr_bind is_closure thm BR ((SOME v, pat), ty);
-            val (ps, vars') = fold_map pr binds vars;
+            val (binds, t') = Code_Thingol.unfold_pat_abs t;
+            val (ps, vars') = fold_map (pr_bind is_closure thm BR) binds vars;
           in brackets (str "fun" :: ps @ str "->" @@ pr_term is_closure thm vars' NOBR t') end
       | pr_term is_closure thm vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
            of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
@@ -427,17 +424,15 @@
         :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
     and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
       syntax_const
-    and pr_bind' ((NONE, NONE), _) = str "_"
-      | pr_bind' ((SOME v, NONE), _) = str v
-      | pr_bind' ((NONE, SOME p), _) = p
-      | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
+    and pr_bind' (NONE, _) = str "_"
+      | pr_bind' (SOME p, _) = p
     and pr_bind is_closure = gen_pr_bind pr_bind' (pr_term is_closure)
     and pr_case is_closure thm vars fxy (cases as ((_, [_]), _)) =
           let
             val (binds, body) = Code_Thingol.unfold_let (ICase cases);
             fun pr ((pat, ty), t) vars =
               vars
-              |> pr_bind is_closure thm NOBR ((NONE, SOME pat), ty)
+              |> pr_bind is_closure thm NOBR (SOME pat, ty)
               |>> (fn p => concat
                   [str "let", p, str "=", pr_term is_closure thm vars NOBR t, str "in"])
             val (ps, vars') = fold_map pr binds vars;
@@ -449,7 +444,7 @@
           let
             fun pr delim (pat, body) =
               let
-                val (p, vars') = pr_bind is_closure thm NOBR ((NONE, SOME pat), ty) vars;
+                val (p, vars') = pr_bind is_closure thm NOBR (SOME pat, ty) vars;
               in concat [str delim, p, str "->", pr_term is_closure thm vars' NOBR body] end;
           in
             brackets (
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/Tools/Code/code_printer.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -68,10 +68,10 @@
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> (string -> const_syntax option)
     -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
-  val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
+  val gen_pr_bind: (Pretty.T option * itype -> Pretty.T)
     -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
     -> thm -> fixity
-    -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
+    -> iterm option * itype -> var_ctxt -> Pretty.T * var_ctxt
 
   val mk_name_module: Name.context -> string option -> (string -> string option)
     -> 'a Graph.T -> string -> string
@@ -216,16 +216,14 @@
           else pr_term thm vars fxy (Code_Thingol.eta_expand k app)
         end;
 
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
+fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) (some_pat, ty : itype) vars =
   let
-    val vs = case pat
+    val vs = case some_pat
      of SOME pat => Code_Thingol.fold_varnames (insert (op =)) pat []
       | NONE => [];
-    val vars' = intro_vars (the_list v) vars;
-    val vars'' = intro_vars vs vars';
-    val v' = Option.map (lookup_var vars') v;
-    val pat' = Option.map (pr_term thm vars'' fxy) pat;
-  in (pr_bind ((v', pat'), ty), vars'') end;
+    val vars' = intro_vars vs vars;
+    val some_pat' = Option.map (pr_term thm vars' fxy) some_pat;
+  in (pr_bind (some_pat', ty), vars') end;
 
 
 (* mixfix syntax *)
diff -r 53acb8ec6c51 -r 4a34d2a8a497 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Jun 30 21:19:32 2009 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Jun 30 21:23:01 2009 +0200
@@ -40,13 +40,12 @@
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   val unfold_fun: itype -> itype list * itype
   val unfold_app: iterm -> iterm * iterm list
-  val split_abs: iterm -> (((vname * iterm option) * itype) * iterm) option
-  val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
+  val unfold_abs: iterm -> (vname * itype) list * iterm
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
+  val split_pat_abs: iterm -> ((iterm option * itype) * iterm) option
+  val unfold_pat_abs: iterm -> (iterm option * itype) list * iterm
   val unfold_const_app: iterm -> (const * iterm list) option
-  val collapse_let: ((vname * itype) * iterm) * iterm
-    -> (iterm * itype) * (iterm * iterm) list
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dictvar: iterm -> bool
   val locally_monomorphic: iterm -> bool
@@ -139,14 +138,10 @@
   (fn op `$ t => SOME t
     | _ => NONE);
 
-val split_abs =
-  (fn (v, ty) `|=> (t as ICase (((IVar w, _), [(p, t')]), _)) =>
-        if v = w then SOME (((v, SOME p), ty), t') else SOME (((v, NONE), ty), t)
-    | (v, ty) `|=> t => SOME (((v, NONE), ty), t)
+val unfold_abs = unfoldr
+  (fn op `|=> t => SOME t
     | _ => NONE);
 
-val unfold_abs = unfoldr split_abs;
-
 val split_let = 
   (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
     | _ => NONE);
@@ -186,17 +181,17 @@
       | add vs (ICase (_, t)) = add vs t;
   in add [] end;
 
-fun collapse_let (((v, ty), se), be as ICase (((IVar w, _), ds), _)) =
-      let
-        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
-          b orelse v = w) t false;
-      in if v = w andalso forall (fn (t1, t2) =>
-        exists_v t1 orelse not (exists_v t2)) ds
-        then ((se, ty), ds)
-        else ((se, ty), [(IVar v, be)])
-      end
-  | collapse_let (((v, ty), se), be) =
-      ((se, ty), [(IVar v, be)])
+fun exists_var t v = fold_unbound_varnames (fn w => fn b => v = w orelse b) t false;
+
+val split_pat_abs = (fn (v, ty) `|=> t => (case t
+   of ICase (((IVar w, _), [(p, t')]), _) =>
+        if v = w andalso (exists_var p v orelse not (exists_var t' v))
+        then SOME ((SOME p, ty), t')
+        else SOME ((SOME (IVar v), ty), t)
+    | _ => SOME ((if exists_var t v then SOME (IVar v) else NONE, ty), t))
+  | _ => NONE);
+
+val unfold_pat_abs = unfoldr split_pat_abs;
 
 fun eta_expand k (c as (_, (_, tys)), ts) =
   let