# HG changeset patch
# User nipkow
# Date 1504119045 -7200
# Node ID b17d41779768c997db17336667000a68513cc23e
# Parent  39257f39c7daf4aa124796d34a51dd931131d7c8# Parent  2d24e2c021302421476332e42e44c3e0f4a6fdee
merged

diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Aug 30 20:50:45 2017 +0200
@@ -314,7 +314,7 @@
     then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on \<Omega>"
       by (auto simp: integrable_on_def cong: has_integral_cong)
     then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on (\<Omega> \<union> B n)"
-      by (rule integrable_on_superset[rotated 2]) auto
+      by (rule integrable_on_superset) auto
     then have "(\<lambda>x. f x * indicator \<Omega> x) integrable_on B n"
       unfolding B_def by (rule integrable_on_subcbox) auto
     then show "(\<lambda>x. f x * indicator \<Omega> x) \<in> lebesgue_on \<Omega>' \<rightarrow>\<^sub>M borel"
@@ -2717,7 +2717,7 @@
   note intl = has_integral_integrable[OF int]
   have af: "f absolutely_integrable_on (closure S)"
     using nonneg
-    by (intro absolutely_integrable_onI intl integrable_eq[OF _ intl]) simp
+    by (intro absolutely_integrable_onI intl integrable_eq[OF intl]) simp
   then have "integral (closure S) f = set_lebesgue_integral lebesgue (closure S) f"
     by (intro set_lebesgue_integral_eq_integral(2)[symmetric])
   also have "\<dots> = 0 \<longleftrightarrow> (AE x in lebesgue. indicator (closure S) x *\<^sub>R f x = 0)"
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Aug 30 20:50:45 2017 +0200
@@ -261,8 +261,8 @@
   have f'_nonpos: "f' \<le> 0" using assms by (simp add: f'_def divide_simps)
   let ?f = "\<lambda>t. (t - x) * f' + inverse x"
   let ?F = "\<lambda>t. (t - x)^2 * f' / 2 + t * inverse x"
-  have diff: "\<forall>t\<in>{x..x+a}. (?F has_vector_derivative ?f t)
-                               (at t within {x..x+a})" using assms
+  have diff: "\<And>t. t \<in> {x..x+a} \<Longrightarrow> (?F has_vector_derivative ?f t) (at t within {x..x+a})" 
+    using assms
     by (auto intro!: derivative_eq_intros
              simp: has_field_derivative_iff_has_vector_derivative[symmetric])
   from assms have "(?f has_integral (?F (x+a) - ?F x)) {x..x+a}"
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 30 20:50:45 2017 +0200
@@ -716,7 +716,7 @@
   using assms(1)
   by auto
 
-lemma integrable_eq: "(\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f integrable_on s \<Longrightarrow> g integrable_on s"
+lemma integrable_eq: "\<lbrakk>f integrable_on s; \<And>x. x \<in> s \<Longrightarrow> f x = g x\<rbrakk> \<Longrightarrow> g integrable_on s"
   unfolding integrable_on_def
   using has_integral_eq[of s f g] has_integral_eq by blast
 
@@ -2615,79 +2615,70 @@
     and "Inf {a..b} = a"
   using assms by auto
 
-lemma fundamental_theorem_of_calculus:
+theorem fundamental_theorem_of_calculus:
   fixes f :: "real \<Rightarrow> 'a::banach"
-  assumes "a \<le> b"
-    and vecd: "\<forall>x\<in>{a..b}. (f has_vector_derivative f' x) (at x within {a..b})"
+  assumes "a \<le> b" 
+      and vecd: "\<And>x. x \<in> {a..b} \<Longrightarrow> (f has_vector_derivative f' x) (at x within {a..b})"
   shows "(f' has_integral (f b - f a)) {a..b}"
   unfolding has_integral_factor_content box_real[symmetric]
 proof safe
   fix e :: real
   assume "e > 0"
-  then have "\<forall>x. \<exists>d>0.
-         x \<in> {a..b} \<longrightarrow>
-         (\<forall>y\<in>{a..b}.
-             norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x))"
+  then have "\<forall>x. \<exists>d>0. x \<in> {a..b} \<longrightarrow>
+         (\<forall>y\<in>{a..b}. norm (y-x) < d \<longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x))"
     using vecd[unfolded has_vector_derivative_def has_derivative_within_alt] by blast
   then obtain d where d: "\<And>x. 0 < d x"
                  "\<And>x y. \<lbrakk>x \<in> {a..b}; y \<in> {a..b}; norm (y-x) < d x\<rbrakk>
                         \<Longrightarrow> norm (f y - f x - (y-x) *\<^sub>R f' x) \<le> e * norm (y-x)"
-    by metis
-  
+    by metis  
   show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of (cbox a b) \<and> d fine p \<longrightarrow>
     norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b))"
-    apply (rule_tac x="\<lambda>x. ball x (d x)" in exI)
-    apply safe
-    apply (rule gauge_ball_dependent)
-    apply rule
-    apply (rule d(1))
-  proof -
+  proof (rule exI, safe)
+    show "gauge (\<lambda>x. ball x (d x))"
+      using d(1) gauge_ball_dependent by blast
+  next
     fix p
-    assume as: "p tagged_division_of cbox a b" "(\<lambda>x. ball x (d x)) fine p"
-    show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)"
-      unfolding content_real[OF assms(1), simplified box_real[symmetric]] additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of f,symmetric]
-      unfolding additive_tagged_division_1[OF assms(1) as(1)[simplified box_real],of "\<lambda>x. x",symmetric]
-      unfolding sum_distrib_left
-      defer
-      unfolding sum_subtractf[symmetric]
+    assume ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x (d x)) fine p"
+    have ba: "b - a = (\<Sum>(x,K)\<in>p. Sup K - Inf K)" "f b - f a = (\<Sum>(x,K)\<in>p. f(Sup K) - f(Inf K))"
+      using additive_tagged_division_1[where f= "\<lambda>x. x"] additive_tagged_division_1[where f= f]
+            \<open>a \<le> b\<close> ptag by auto
+    have "norm (\<Sum>(x, K) \<in> p. (content K *\<^sub>R f' x) - (f (Sup K) - f (Inf K)))
+          \<le> (\<Sum>n\<in>p. e * (case n of (x, k) \<Rightarrow> Sup k - Inf k))"
     proof (rule sum_norm_le,safe)
-      fix x k
-      assume "(x, k) \<in> p"
-      note xk = tagged_division_ofD(2-4)[OF as(1) this]
-      then obtain u v where k: "k = cbox u v" by blast
-      have *: "u \<le> v"
-        using xk unfolding k by auto
-      have ball: "\<forall>xa\<in>k. xa \<in> ball x (d x)"
-        using as(2)[unfolded fine_def,rule_format,OF \<open>(x,k)\<in>p\<close>,unfolded split_conv subset_eq] .
-      have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
-        norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
-        apply (rule order_trans[OF _ norm_triangle_ineq4])
-        apply (rule eq_refl)
-        apply (rule arg_cong[where f=norm])
-        unfolding scaleR_diff_left
-        apply (auto simp add:algebra_simps)
-        done
+      fix x K
+      assume "(x, K) \<in> p"
+      then have "x \<in> K" and kab: "K \<subseteq> cbox a b"
+        using ptag by blast+
+      then obtain u v where k: "K = cbox u v" and "x \<in> K" and kab: "K \<subseteq> cbox a b"
+        using ptag \<open>(x, K) \<in> p\<close> by auto 
+      have "u \<le> v"
+        using \<open>x \<in> K\<close> unfolding k by auto
+      have ball: "\<forall>y\<in>K. y \<in> ball x (d x)"
+        using finep \<open>(x, K) \<in> p\<close> by blast
+      have "u \<in> K" "v \<in> K"
+        by (simp_all add: \<open>u \<le> v\<close> k)
+      have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) = norm (f u - f x - (u - x) *\<^sub>R f' x - (f v - f x - (v - x) *\<^sub>R f' x))"
+        by (auto simp add: algebra_simps)
+      also have "... \<le> norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)"
+        by (rule norm_triangle_ineq4)
+      finally have "norm ((v - u) *\<^sub>R f' x - (f v - f u)) \<le>
+        norm (f u - f x - (u - x) *\<^sub>R f' x) + norm (f v - f x - (v - x) *\<^sub>R f' x)" .
       also have "\<dots> \<le> e * norm (u - x) + e * norm (v - x)"
-        apply (rule add_mono)
-        apply (rule d(2)[of "x" "u",unfolded o_def])
-        prefer 4
-        apply (rule d(2)[of "x" "v",unfolded o_def])
-        using ball[rule_format,of u] ball[rule_format,of v]
-        using xk(1-2)
-        unfolding k subset_eq
-        apply (auto simp add:dist_real_def)
-        done
-      also have "\<dots> \<le> e * (Sup k - Inf k)"
-        unfolding k interval_bounds_real[OF *]
-        using xk(1)
-        unfolding k
-        by (auto simp add: dist_real_def field_simps)
-      finally show "norm (content k *\<^sub>R f' x - (f (Sup k) - f (Inf k))) \<le>
-        e * (Sup k - Inf k)"
-        unfolding box_real k interval_bounds_real[OF *] content_real[OF *]
-          interval_upperbound_real interval_lowerbound_real
-          .
+      proof (rule add_mono)
+        show "norm (f u - f x - (u - x) *\<^sub>R f' x) \<le> e * norm (u - x)"
+          apply (rule d(2)[of x u])
+          using \<open>x \<in> K\<close> kab \<open>u \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
+        show "norm (f v - f x - (v - x) *\<^sub>R f' x) \<le> e * norm (v - x)"
+          apply (rule d(2)[of x v])
+          using \<open>x \<in> K\<close> kab \<open>v \<in> K\<close> ball dist_real_def by (auto simp add:dist_real_def)
+      qed
+      also have "\<dots> \<le> e * (Sup K - Inf K)"
+        using \<open>x \<in> K\<close> by (auto simp: k interval_bounds_real[OF \<open>u \<le> v\<close>] field_simps)
+      finally show "norm (content K *\<^sub>R f' x - (f (Sup K) - f (Inf K))) \<le> e * (Sup K - Inf K)"
+        using \<open>u \<le> v\<close> by (simp add: k)
     qed
+    with \<open>a \<le> b\<close> show "norm ((\<Sum>(x, K)\<in>p. content K *\<^sub>R f' x) - (f b - f a)) \<le> e * content (cbox a b)"
+      by (auto simp: ba split_def sum_subtractf [symmetric] sum_distrib_left)
   qed
 qed
 
@@ -2697,7 +2688,7 @@
   shows "((\<lambda>x. x) has_integral (b\<^sup>2 - a\<^sup>2)/2) {a..b}"
 proof -
   have "((\<lambda>x. x) has_integral inverse 2 * b\<^sup>2 - inverse 2 * a\<^sup>2) {a..b}"
-    apply (rule fundamental_theorem_of_calculus [OF assms], clarify)
+    apply (rule fundamental_theorem_of_calculus [OF assms])
     unfolding power2_eq_square
     by (rule derivative_eq_intros | simp)+
   then show ?thesis
@@ -3144,10 +3135,10 @@
     using  antiderivative_continuous[OF assms] by metis
   have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
   proof -
-    have "\<forall>x\<in>cbox u v. (g has_vector_derivative f x) (at x within cbox u v)"
+    have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
       by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
     then show ?thesis
-      by (simp add: fundamental_theorem_of_calculus that(3))
+      by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
   qed
   then show ?thesis
     using that by blast
@@ -3158,39 +3149,30 @@
 
 lemma has_integral_twiddle:
   assumes "0 < r"
-    and "\<forall>x. h(g x) = x"
-    and "\<forall>x. g(h x) = x"
+    and hg: "\<And>x. h(g x) = x"
+    and gh: "\<And>x. g(h x) = x"
     and contg: "\<And>x. continuous (at x) g"
-    and "\<forall>u v. \<exists>w z. g ` cbox u v = cbox w z"
-    and h: "\<forall>u v. \<exists>w z. h ` cbox u v = cbox w z"
-    and "\<forall>u v. content(g ` cbox u v) = r * content (cbox u v)"
+    and g: "\<And>u v. \<exists>w z. g ` cbox u v = cbox w z"
+    and h: "\<And>u v. \<exists>w z. h ` cbox u v = cbox w z"
+    and r: "\<And>u v. content(g ` cbox u v) = r * content (cbox u v)"
     and intfi: "(f has_integral i) (cbox a b)"
   shows "((\<lambda>x. f(g x)) has_integral (1 / r) *\<^sub>R i) (h ` cbox a b)"
-proof -
-  show ?thesis when *: "cbox a b \<noteq> {} \<Longrightarrow> ?thesis"
-    apply cases
-    defer
-    apply (rule *)
-    apply assumption
-  proof goal_cases
-    case prems: 1
-    then show ?thesis
-      unfolding prems assms(8)[unfolded prems has_integral_empty_eq] by auto
-  qed
-  assume "cbox a b \<noteq> {}"
+proof (cases "cbox a b = {}")
+  case True
+  then show ?thesis 
+    using intfi by auto
+next
+  case False
   obtain w z where wz: "h ` cbox a b = cbox w z"
     using h by blast
   have inj: "inj g" "inj h"
-    apply (metis assms(2) injI)
-    by (metis assms(3) injI)
+    using hg gh injI by metis+
   from h obtain ha hb where h_eq: "h ` cbox a b = cbox ha hb" by blast
-  show ?thesis
-    unfolding h_eq has_integral
-    unfolding h_eq[symmetric]
-  proof safe
-    fix e :: real
-    assume e: "e > 0"
-    with \<open>0 < r\<close> have "e * r > 0" by simp
+  have "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p 
+              \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
+    if "e > 0" for e
+  proof -
+    have "e * r > 0" using that \<open>0 < r\<close> by simp
     with intfi[unfolded has_integral]
     obtain d where d: "gauge d"
                    "\<And>p. p tagged_division_of cbox a b \<and> d fine p 
@@ -3199,69 +3181,49 @@
     define d' where "d' x = {y. g y \<in> d (g x)}" for x
     have d': "\<And>x. d' x = {y. g y \<in> (d (g x))}"
       unfolding d'_def ..
-    show "\<exists>d. gauge d \<and> (\<forall>p. p tagged_division_of h ` cbox a b \<and> d fine p 
-              \<longrightarrow> norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e)"
+    show ?thesis
     proof (rule_tac x=d' in exI, safe)
       show "gauge d'"
-        using d(1)
-        unfolding gauge_def d'
-        using continuous_open_preimage_univ[OF _ contg]
-        by auto
+        using d(1) continuous_open_preimage_univ[OF _ contg] by (auto simp: gauge_def d')
+    next
       fix p
-      assume as: "p tagged_division_of h ` cbox a b" "d' fine p"
-      note p = tagged_division_ofD[OF as(1)]
-      have "(\<lambda>(x, k). (g x, g ` k)) ` p tagged_division_of (cbox a b) \<and> d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
+      assume ptag: "p tagged_division_of h ` cbox a b" and finep: "d' fine p"
+      note p = tagged_division_ofD[OF ptag]
+      have gab: "g y \<in> cbox a b" if "y \<in> K" "(x, K) \<in> p" for x y K
+        by (metis hg inj(2) inj_image_mem_iff p(3) subsetCE that that)
+      have gimp: "(\<lambda>(x,K). (g x, g ` K)) ` p tagged_division_of (cbox a b) \<and> 
+                  d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
         unfolding tagged_division_of
       proof safe
         show "finite ((\<lambda>(x, k). (g x, g ` k)) ` p)"
-          using as by auto
+          using ptag by auto
         show "d fine (\<lambda>(x, k). (g x, g ` k)) ` p"
-          using as(2) unfolding fine_def d' by auto
+          using finep unfolding fine_def d' by auto
+      next
         fix x k
-        assume xk[intro]: "(x, k) \<in> p"
+        assume xk: "(x, k) \<in> p"
         show "g x \<in> g ` k"
           using p(2)[OF xk] by auto
         show "\<exists>u v. g ` k = cbox u v"
           using p(4)[OF xk] using assms(5-6) by auto
-        {
-          fix y
-          assume "y \<in> k"
-          then show "g y \<in> cbox a b" "g y \<in> cbox a b"
-            using p(3)[OF xk,unfolded subset_eq,rule_format,of "h (g y)"]
-            using assms(2)[rule_format,of y]
-            unfolding inj_image_mem_iff[OF inj(2)]
-            by auto
-        }
-        fix x' k'
-        assume xk': "(x', k') \<in> p"
-        fix z
-        assume z: "z \<in> interior (g ` k)" "z \<in> interior (g ` k')"
-        have same: "(x, k) = (x', k')"
-          apply -
-          apply (rule ccontr)
-          apply (drule p(5)[OF xk xk'])
-        proof -
-          assume as: "interior k \<inter> interior k' = {}"
-          have "z \<in> g ` (interior k \<inter> interior k')"
-            using interior_image_subset[OF \<open>inj g\<close> contg] z
+        fix x' K' u
+        assume xk': "(x', K') \<in> p" and u: "u \<in> interior (g ` k)" "u \<in> interior (g ` K')"
+        have "interior k \<inter> interior K' \<noteq> {}"
+        proof 
+          assume "interior k \<inter> interior K' = {}"
+          moreover have "u \<in> g ` (interior k \<inter> interior K')"
+            using interior_image_subset[OF \<open>inj g\<close> contg] u
             unfolding image_Int[OF inj(1)] by blast
-          then show False
-            using as by blast
+          ultimately show False by blast
         qed
+        then have same: "(x, k) = (x', K')"
+          using ptag xk' xk by blast
         then show "g x = g x'"
           by auto
-        {
-          fix z
-          assume "z \<in> k"
-          then show "g z \<in> g ` k'"
-            using same by auto
-        }
-        {
-          fix z
-          assume "z \<in> k'"
-          then show "g z \<in> g ` k"
-            using same by auto
-        }
+        show "g u \<in> g ` K'"if "u \<in> k" for u
+          using that same by auto
+        show "g u \<in> g ` k"if "u \<in> K'" for u
+          using that same by auto
       next
         fix x
         assume "x \<in> cbox a b"
@@ -3269,31 +3231,26 @@
           using p(6) by auto
         then obtain X y where "h x \<in> X" "(y, X) \<in> p" by blast
         then show "x \<in> \<Union>{k. \<exists>x. (x, k) \<in> (\<lambda>(x, k). (g x, g ` k)) ` p}"
-          apply (clarsimp simp: )
+          apply clarsimp
           by (metis (no_types, lifting) assms(3) image_eqI pair_imageI)
-      qed
-        note ** = d(2)[OF this]
-        have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
-          using inj(1) unfolding inj_on_def by fastforce
-        have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
-          using assms(7)
-          apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
-          apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
-          apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
-          done
+      qed (use gab in auto)
+      have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
+        using inj(1) unfolding inj_on_def by fastforce
+      have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
+        using r
+        apply (simp only: algebra_simps add_left_cancel scaleR_right.sum)
+        apply (subst sum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
+         apply (auto intro!: * sum.cong simp: bij_betw_def dest!: p(4))
+        done
       also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r")
-        unfolding scaleR_diff_right scaleR_scaleR
-        using assms(1)
-        by auto
-      finally have *: "?l = ?r" .
-      show "norm ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
-        using **
-        unfolding *
-        unfolding norm_scaleR
-        using assms(1)
-        by (auto simp add:field_simps)
+        using \<open>0 < r\<close> by (auto simp: scaleR_diff_right)
+      finally have eq: "?l = ?r" .
+      show "norm ((\<Sum>(x,K)\<in>p. content K *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i) < e"
+        using d(2)[OF gimp] \<open>0 < r\<close> by (auto simp add: eq)
     qed
   qed
+  then show ?thesis
+    by (auto simp: h_eq has_integral)
 qed
 
 
@@ -4408,10 +4365,7 @@
     then have "?g integrable_on cbox c d"
       using assms has_integral_integrable integrable_subinterval by blast
     then have "f integrable_on cbox c d"
-      apply -
-      apply (rule integrable_eq)
-      apply auto
-      done
+      by (rule integrable_eq) auto
     moreover then have "i = integral (cbox c d) f"
       by (meson \<open>((\<lambda>x. if x \<in> cbox c d then f x else 0) has_integral i) (cbox a b)\<close> assms has_integral_restrict_closed_subinterval has_integral_unique integrable_integral)
     ultimately show ?r by auto
@@ -4591,9 +4545,9 @@
 
 lemma integrable_on_superset:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  assumes "\<forall>x. x \<notin> s \<longrightarrow> f x = 0"
-    and "s \<subseteq> t"
-    and "f integrable_on s"
+  assumes "f integrable_on S"
+    and "\<And>x. x \<notin> S \<Longrightarrow> f x = 0"
+    and "S \<subseteq> t"
   shows "f integrable_on t"
   using assms
   unfolding integrable_on_def
@@ -4601,7 +4555,7 @@
 
 lemma integral_restrict_UNIV [intro]:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
-  shows "f integrable_on s \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> s then f x else 0) = integral s f"
+  shows "f integrable_on S \<Longrightarrow> integral UNIV (\<lambda>x. if x \<in> S then f x else 0) = integral S f"
   apply (rule integral_unique)
   unfolding has_integral_restrict_UNIV
   apply auto
@@ -6881,7 +6835,7 @@
 proof -
   have "((\<lambda>(x, y). f x y) has_integral integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)) (prod.swap ` (cbox (c, a) (d, b)))"
     apply (rule has_integral_twiddle [of 1 prod.swap prod.swap "\<lambda>(x,y). f y x" "integral (cbox (c, a) (d, b)) (\<lambda>(x, y). f y x)", simplified])
-    apply (auto simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)
+    apply (force simp: isCont_swap content_Pair has_integral_integral [symmetric] integrable_continuous swap_continuous assms)+
     done
  then show ?thesis
    by force
@@ -6934,10 +6888,10 @@
     fix k ::nat
     have "(\<lambda>x. exp (-a*x)) integrable_on {c..of_real k}" (is ?P)
       unfolding f_def by (auto intro!: continuous_intros integrable_continuous_real)
-    hence int: "(f k) integrable_on {c..of_real k}"
-      by (rule integrable_eq[rotated]) (simp add: f_def)
-    show "f k integrable_on {c..}"
-      by (rule integrable_on_superset[OF _ _ int]) (auto simp: f_def)
+    hence  "(f k) integrable_on {c..of_real k}"
+      by (rule integrable_eq) (simp add: f_def)
+    then show "f k integrable_on {c..}"
+      by (rule integrable_on_superset) (auto simp: f_def)
   next
     fix x assume x: "x \<in> {c..}"
     have "sequentially \<le> principal {nat \<lceil>x\<rceil>..}" unfolding at_top_def by (simp add: Inf_lower)
@@ -7118,9 +7072,9 @@
     from assms have "(\<lambda>x. x powr e) integrable_on {a..n}"
       by (auto intro!: integrable_continuous_real continuous_intros)
     hence "f n integrable_on {a..n}"
-      by (rule integrable_eq [rotated]) (auto simp: f_def)
+      by (rule integrable_eq) (auto simp: f_def)
     thus "f n integrable_on {a..}"
-      by (rule integrable_on_superset [rotated 2]) (auto simp: f_def)
+      by (rule integrable_on_superset) (auto simp: f_def)
   next
     fix n :: nat and x :: real
     show "f n x \<le> f (Suc n) x" by (auto simp: f_def)
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Analysis/Improper_Integral.thy
--- a/src/HOL/Analysis/Improper_Integral.thy	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy	Wed Aug 30 20:50:45 2017 +0200
@@ -220,7 +220,10 @@
     qed
   qed
   then show ?thesis
-    using assms by (auto simp: equiintegrable_on_def integrable_eq)
+    using assms
+    apply (auto simp: equiintegrable_on_def)
+    apply (rule integrable_eq)
+    by auto 
 qed
 
 subsection\<open>Subinterval restrictions for equiintegrable families\<close>
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Aug 30 20:50:45 2017 +0200
@@ -1386,6 +1386,22 @@
 lemmas fps_numeral_simps = 
   fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const
 
+lemma subdegree_div:
+  assumes "q dvd p"
+  shows   "subdegree ((p :: 'a :: field fps) div q) = subdegree p - subdegree q"
+proof (cases "p = 0")
+  case False
+  from assms have "p = p div q * q" by simp
+  also from assms False have "subdegree \<dots> = subdegree (p div q) + subdegree q"
+    by (intro subdegree_mult) (auto simp: dvd_div_eq_0_iff)
+  finally show ?thesis by simp
+qed simp_all
+
+lemma subdegree_div_unit:
+  assumes "q $ 0 \<noteq> 0"
+  shows   "subdegree ((p :: 'a :: field fps) div q) = subdegree p"
+  using assms by (subst subdegree_div) simp_all
+
 
 subsection \<open>Formal power series form a Euclidean ring\<close>
 
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Computational_Algebra/Polynomial.thy
--- a/src/HOL/Computational_Algebra/Polynomial.thy	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Wed Aug 30 20:50:45 2017 +0200
@@ -1388,6 +1388,9 @@
   for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   by (auto simp: degree_mult_eq)
 
+lemma degree_power_eq: "p \<noteq> 0 \<Longrightarrow> degree ((p :: 'a :: idom poly) ^ n) = n * degree p"
+  by (induction n) (simp_all add: degree_mult_eq)
+
 lemma degree_mult_right_le:
   fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
   assumes "q \<noteq> 0"
@@ -2454,9 +2457,6 @@
   qed
 qed
 
-lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
-  by (induct n arbitrary: f) auto
-
 lemma coeffs_pderiv_code [code abstract]: "coeffs (pderiv p) = pderiv_coeffs (coeffs p)"
   unfolding pderiv_coeffs_def
 proof (rule coeffs_eqI, unfold pderiv_coeffs_code coeff_pderiv, goal_cases)
@@ -2539,6 +2539,10 @@
   apply (simp add: algebra_simps)
   done
 
+lemma pderiv_pcompose: "pderiv (pcompose p q) = pcompose (pderiv p) q * pderiv q"
+  by (induction p rule: pCons_induct)
+     (auto simp: pcompose_pCons pderiv_add pderiv_mult pderiv_pCons pcompose_add algebra_simps)
+
 lemma pderiv_prod: "pderiv (prod f (as)) = (\<Sum>a\<in>as. prod f (as - {a}) * pderiv (f a))"
 proof (induct as rule: infinite_finite_induct)
   case (insert a as)
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/List.thy	Wed Aug 30 20:50:45 2017 +0200
@@ -3108,7 +3108,10 @@
 done
 
 lemma map_decr_upt: "map (\<lambda>n. n - Suc 0) [Suc m..<Suc n] = [m..<n]"
-by (induct n) simp_all
+  by (induct n) simp_all
+
+lemma map_upt_Suc: "map f [0 ..< Suc n] = f 0 # map (\<lambda>i. f (Suc i)) [0 ..< n]"
+  by (induct n arbitrary: f) auto
 
 
 lemma nth_take_lemma:
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/SMT.thy
--- a/src/HOL/SMT.thy	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/SMT.thy	Wed Aug 30 20:50:45 2017 +0200
@@ -1,12 +1,13 @@
 (*  Title:      HOL/SMT.thy
     Author:     Sascha Boehme, TU Muenchen
+    Author:     Jasmin Blanchette, VU Amsterdam
 *)
 
 section \<open>Bindings to Satisfiability Modulo Theories (SMT) solvers based on SMT-LIB 2\<close>
 
 theory SMT
-imports Divides
-keywords "smt_status" :: diag
+  imports Divides
+  keywords "smt_status" :: diag
 begin
 
 subsection \<open>A skolemization tactic and proof method\<close>
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/cvc4_interface.ML
--- a/src/HOL/Tools/SMT/cvc4_interface.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/cvc4_interface.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -7,24 +7,30 @@
 signature CVC4_INTERFACE =
 sig
   val smtlib_cvc4C: SMT_Util.class
+  val hosmtlib_cvc4C: SMT_Util.class
 end;
 
 structure CVC4_Interface: CVC4_INTERFACE =
 struct
 
-val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ ["cvc4"]
+val cvc4C = ["cvc4"]
+val smtlib_cvc4C = SMTLIB_Interface.smtlibC @ cvc4C
+val hosmtlib_cvc4C = SMTLIB_Interface.hosmtlibC @ cvc4C
 
 
 (* interface *)
 
 local
-  fun translate_config ctxt =
-    {logic = K "(set-logic ALL_SUPPORTED)\n", fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
-     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+  fun translate_config order ctxt =
+    {order = order,
+     logic = K "(set-logic ALL_SUPPORTED)\n",
+     fp_kinds = [BNF_Util.Least_FP, BNF_Util.Greatest_FP],
+     serialize = #serialize (SMTLIB_Interface.translate_config order ctxt)}
 in
 
-val _ =
-  Theory.setup (Context.theory_map (SMT_Translate.add_config (smtlib_cvc4C, translate_config)))
+val _ = Theory.setup (Context.theory_map
+  (SMT_Translate.add_config (smtlib_cvc4C, translate_config SMT_Util.First_Order) #>
+   SMT_Translate.add_config (hosmtlib_cvc4C, translate_config SMT_Util.Higher_Order)))
 
 end
 
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/smt_builtin.ML
--- a/src/HOL/Tools/SMT/smt_builtin.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_builtin.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -11,11 +11,11 @@
 
   (*built-in types*)
   val add_builtin_typ: SMT_Util.class ->
-    typ * (typ -> string option) * (typ -> int -> string option) -> Context.generic ->
+    typ * (typ -> (string * typ list) option) * (typ -> int -> string option) -> Context.generic ->
     Context.generic
   val add_builtin_typ_ext: typ * (Proof.context -> typ -> bool) -> Context.generic ->
     Context.generic
-  val dest_builtin_typ: Proof.context -> typ -> string option
+  val dest_builtin_typ: Proof.context -> typ -> (string * typ list) option
   val is_builtin_typ_ext: Proof.context -> typ -> bool
 
   (*built-in numbers*)
@@ -93,7 +93,8 @@
 structure Builtins = Generic_Data
 (
   type T =
-    (Proof.context -> typ -> bool, (typ -> string option) * (typ -> int -> string option)) ttab *
+    (Proof.context -> typ -> bool,
+     (typ -> (string * typ list) option) * (typ -> int -> string option)) ttab *
     (term list bfun, bfunr option bfun) btab
   val empty = ([], Symtab.empty)
   val extend = I
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/smt_config.ML
--- a/src/HOL/Tools/SMT/smt_config.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_config.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -32,6 +32,7 @@
   val statistics: bool Config.T
   val monomorph_limit: int Config.T
   val monomorph_instances: int Config.T
+  val higher_order: bool Config.T
   val nat_as_int: bool Config.T
   val infer_triggers: bool Config.T
   val debug_files: string Config.T
@@ -180,6 +181,7 @@
 val statistics = Attrib.setup_config_bool @{binding smt_statistics} (K false)
 val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10)
 val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500)
+val higher_order = Attrib.setup_config_bool @{binding smt_higher_order} (K false)
 val nat_as_int = Attrib.setup_config_bool @{binding smt_nat_as_int} (K false)
 val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false)
 val debug_files = Attrib.setup_config_string @{binding smt_debug_files} (K "")
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/smt_real.ML
--- a/src/HOL/Tools/SMT/smt_real.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -32,7 +32,7 @@
 
 val setup_builtins =
   SMT_Builtin.add_builtin_typ SMTLIB_Interface.smtlibC
-    (@{typ real}, K (SOME "Real"), real_num) #>
+    (@{typ real}, K (SOME ("Real", [])), real_num) #>
   fold (SMT_Builtin.add_builtin_fun' SMTLIB_Interface.smtlibC) [
     (@{const less (real)}, "<"),
     (@{const less_eq (real)}, "<="),
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/smt_systems.ML
--- a/src/HOL/Tools/SMT/smt_systems.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -62,6 +62,7 @@
 
 end
 
+
 (* CVC4 *)
 
 val cvc4_extensions = Attrib.setup_config_bool @{binding cvc4_extensions} (K false)
@@ -75,8 +76,16 @@
     "--tlimit", string_of_int (Real.ceil (1000.0 * Config.get ctxt SMT_Config.timeout))]
 
   fun select_class ctxt =
-    if Config.get ctxt cvc4_extensions then CVC4_Interface.smtlib_cvc4C
-    else SMTLIB_Interface.smtlibC
+    if Config.get ctxt cvc4_extensions then
+      if Config.get ctxt SMT_Config.higher_order then
+        CVC4_Interface.hosmtlib_cvc4C
+      else
+        CVC4_Interface.smtlib_cvc4C
+    else
+      if Config.get ctxt SMT_Config.higher_order then
+        SMTLIB_Interface.hosmtlibC
+      else
+        SMTLIB_Interface.smtlibC
 in
 
 val cvc4: SMT_Solver.solver_config = {
@@ -93,11 +102,20 @@
 
 end
 
+
 (* veriT *)
 
+local
+  fun select_class ctxt =
+    if Config.get ctxt SMT_Config.higher_order then
+      SMTLIB_Interface.hosmtlibC
+    else
+      SMTLIB_Interface.smtlibC
+in
+
 val veriT: SMT_Solver.solver_config = {
   name = "verit",
-  class = K SMTLIB_Interface.smtlibC,
+  class = select_class,
   avail = make_avail "VERIT",
   command = make_command "VERIT",
   options = (fn ctxt => [
@@ -113,6 +131,9 @@
   parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
   replay = NONE }
 
+end
+
+
 (* Z3 *)
 
 val z3_extensions = Attrib.setup_config_bool @{binding z3_extensions} (K false)
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -10,8 +10,8 @@
   datatype squant = SForall | SExists
   datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
   datatype sterm =
-    SVar of int |
-    SApp of string * sterm list |
+    SVar of int * sterm list |
+    SConst of string * sterm list |
     SQua of squant * string list * sterm spattern list * sterm
 
   (*translation configuration*)
@@ -21,6 +21,7 @@
     dtyps: (BNF_Util.fp_kind * (string * (string * (string * string) list) list)) list,
     funcs: (string * (string list * string)) list }
   type config = {
+    order: SMT_Util.order,
     logic: term list -> string,
     fp_kinds: BNF_Util.fp_kind list,
     serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -50,8 +51,8 @@
   SPat of 'a list | SNoPat of 'a list
 
 datatype sterm =
-  SVar of int |
-  SApp of string * sterm list |
+  SVar of int * sterm list |
+  SConst of string * sterm list |
   SQua of squant * string list * sterm spattern list * sterm
 
 
@@ -64,6 +65,7 @@
   funcs: (string * (string list * string)) list }
 
 type config = {
+  order: SMT_Util.order,
   logic: term list -> string,
   fp_kinds: BNF_Util.fp_kind list,
   serialize: (string * string) list -> string list -> sign -> sterm list -> string }
@@ -147,7 +149,7 @@
 
     fun add_typ' T proper =
       (case SMT_Builtin.dest_builtin_typ ctxt' T of
-        SOME n => pair n
+        SOME (n, Ts) => pair n (* FIXME HO: Consider Ts *)
       | NONE => add_typ T proper)
 
     fun tr_select sel =
@@ -425,11 +427,12 @@
       | transT (T as TVar _) = (fn _ => raise TYPE ("bad SMT type", [T], []))
       | transT (T as Type _) =
           (case SMT_Builtin.dest_builtin_typ ctxt T of
-            SOME n => pair n
+            SOME (n, []) => pair n
+          | SOME (n, Ts) =>
+            fold_map transT Ts
+            #>> (fn ns => enclose "(" ")" (space_implode " " (n :: ns)))
           | NONE => add_typ T true)
 
-    fun app n ts = SApp (n, ts)
-
     fun trans t =
       (case Term.strip_comb t of
         (Const (qn, _), [Abs (_, T, t1)]) =>
@@ -440,17 +443,17 @@
           | NONE => raise TERM ("unsupported quantifier", [t]))
       | (u as Const (c as (_, T)), ts) =>
           (case builtin ctxt c ts of
-            SOME (n, _, us, _) => fold_map trans us #>> app n
-          | NONE => transs u T ts)
-      | (u as Free (_, T), ts) => transs u T ts
-      | (Bound i, []) => pair (SVar i)
+            SOME (n, _, us, _) => fold_map trans us #>> curry SConst n
+          | NONE => trans_applied_fun u T ts)
+      | (u as Free (_, T), ts) => trans_applied_fun u T ts
+      | (Bound i, ts) => pair i ##>> fold_map trans ts #>> SVar
       | _ => raise TERM ("bad SMT term", [t]))
 
-    and transs t T ts =
+    and trans_applied_fun t T ts =
       let val (Us, U) = SMT_Util.dest_funT (length ts) T
       in
         fold_map transT Us ##>> transT U #-> (fn Up =>
-          add_fun t (SOME Up) ##>> fold_map trans ts #>> SApp)
+          add_fun t (SOME Up) ##>> fold_map trans ts #>> SConst)
       end
 
     val (us, trx') = fold_map trans ts trx
@@ -480,7 +483,7 @@
 
 fun translate ctxt smt_options comments ithms =
   let
-    val {logic, fp_kinds, serialize} = get_config ctxt
+    val {order, logic, fp_kinds, serialize} = get_config ctxt
 
     fun no_dtyps (tr_context, ctxt) ts =
       ((Termtab.empty, [], tr_context, ctxt), ts)
@@ -510,10 +513,14 @@
       |> rpair ctxt1
       |-> Lambda_Lifting.lift_lambdas NONE is_binder
       |-> (fn (ts', ll_defs) => fn ctxt' =>
-          (ctxt', (intro_explicit_application ctxt' funcs (map mk_trigger ll_defs @ ts'), ll_defs)))
-
+        let
+          val ts'' = map mk_trigger ll_defs @ ts'
+            |> order = SMT_Util.First_Order ? intro_explicit_application ctxt' funcs
+        in
+          (ctxt', (ts'', ll_defs))
+        end)
     val ((rewrite_rules, builtin), ts4) = folify ctxt2 ts3
-      |>> apfst (cons fun_app_eq)
+      |>> order = SMT_Util.First_Order ? apfst (cons fun_app_eq)
   in
     (ts4, tr_context)
     |-> intermediate logic dtyps (builtin SMT_Builtin.dest_builtin) ctxt2
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/smt_util.ML
--- a/src/HOL/Tools/SMT/smt_util.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smt_util.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -10,6 +10,8 @@
   val repeat: ('a -> 'a option) -> 'a -> 'a
   val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
 
+  datatype order = First_Order | Higher_Order
+
   (*class dictionaries*)
   type class = string list
   val basicC: class
@@ -79,6 +81,11 @@
   in rep end
 
 
+(* order *)
+
+datatype order = First_Order | Higher_Order
+
+
 (* class dictionaries *)
 
 type class = string list
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/smtlib_interface.ML
--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -8,8 +8,9 @@
 signature SMTLIB_INTERFACE =
 sig
   val smtlibC: SMT_Util.class
+  val hosmtlibC: SMT_Util.class
   val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
-  val translate_config: Proof.context -> SMT_Translate.config
+  val translate_config: SMT_Util.order -> Proof.context -> SMT_Translate.config
   val assert_name_of_index: int -> string
   val assert_index_of_name: string -> int
   val assert_prefix : string
@@ -18,7 +19,10 @@
 structure SMTLIB_Interface: SMTLIB_INTERFACE =
 struct
 
-val smtlibC = ["smtlib"]
+val hoC = ["ho"]
+
+val smtlibC = ["smtlib"]   (* SMT-LIB 2 *)
+val hosmtlibC = smtlibC @ hoC   (* possibly SMT-LIB 3 *)
 
 
 (* builtins *)
@@ -36,9 +40,11 @@
 in
 
 val setup_builtins =
+  SMT_Builtin.add_builtin_typ hosmtlibC
+    (@{typ "'a => 'b"}, fn Type (@{type_name fun}, Ts) => SOME ("->", Ts), K (K NONE)) #>
   fold (SMT_Builtin.add_builtin_typ smtlibC) [
-    (@{typ bool}, K (SOME "Bool"), K (K NONE)),
-    (@{typ int}, K (SOME "Int"), int_num)] #>
+    (@{typ bool}, K (SOME ("Bool", [])), K (K NONE)),
+    (@{typ int}, K (SOME ("Int", [])), int_num)] #>
   fold (SMT_Builtin.add_builtin_fun' smtlibC) [
     (@{const True}, "true"),
     (@{const False}, "false"),
@@ -90,9 +96,11 @@
 
 fun var i = "?v" ^ string_of_int i
 
-fun tree_of_sterm l (SMT_Translate.SVar i) = SMTLIB.Sym (var (l - i - 1))
-  | tree_of_sterm _ (SMT_Translate.SApp (n, [])) = SMTLIB.Sym n
-  | tree_of_sterm l (SMT_Translate.SApp (n, ts)) =
+fun tree_of_sterm l (SMT_Translate.SVar (i, [])) = SMTLIB.Sym (var (l - i - 1))
+  | tree_of_sterm l (SMT_Translate.SVar (i, ts)) =
+      SMTLIB.S (SMTLIB.Sym (var (l - i - 1)) :: map (tree_of_sterm l) ts)
+  | tree_of_sterm _ (SMT_Translate.SConst (n, [])) = SMTLIB.Sym n
+  | tree_of_sterm l (SMT_Translate.SConst (n, ts)) =
       SMTLIB.S (SMTLIB.Sym n :: map (tree_of_sterm l) ts)
   | tree_of_sterm l (SMT_Translate.SQua (q, ss, pats, t)) =
       let
@@ -157,13 +165,15 @@
 
 (* interface *)
 
-fun translate_config ctxt = {
+fun translate_config order ctxt = {
+  order = order,
   logic = choose_logic ctxt,
   fp_kinds = [],
   serialize = serialize}
 
 val _ = Theory.setup (Context.theory_map
   (setup_builtins #>
-   SMT_Translate.add_config (smtlibC, translate_config)))
+   SMT_Translate.add_config (smtlibC, translate_config SMT_Util.First_Order) #>
+   SMT_Translate.add_config (hosmtlibC, translate_config SMT_Util.Higher_Order)))
 
 end;
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Tools/SMT/z3_interface.ML
--- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -24,15 +24,19 @@
 structure Z3_Interface: Z3_INTERFACE =
 struct
 
-val smtlib_z3C = SMTLIB_Interface.smtlibC @ ["z3"]
+val z3C = ["z3"]
+
+val smtlib_z3C = SMTLIB_Interface.smtlibC @ z3C
 
 
 (* interface *)
 
 local
   fun translate_config ctxt =
-    {logic = K "", fp_kinds = [BNF_Util.Least_FP],
-     serialize = #serialize (SMTLIB_Interface.translate_config ctxt)}
+    {order = SMT_Util.First_Order,
+     logic = K "",
+     fp_kinds = [BNF_Util.Least_FP],
+     serialize = #serialize (SMTLIB_Interface.translate_config SMT_Util.First_Order ctxt)}
 
   fun is_div_mod @{const divide (int)} = true
     | is_div_mod @{const modulo (int)} = true
diff -r 2d24e2c02130 -r b17d41779768 src/HOL/Word/Tools/smt_word.ML
--- a/src/HOL/Word/Tools/smt_word.ML	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/HOL/Word/Tools/smt_word.ML	Wed Aug 30 20:50:45 2017 +0200
@@ -28,7 +28,8 @@
   fun index1 s i = "(_ " ^ s ^ " " ^ string_of_int i ^ ")"
   fun index2 s i j = "(_ " ^ s ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^ ")"
 
-  fun word_typ (Type (@{type_name word}, [T])) = Option.map (index1 "BitVec") (try dest_binT T)
+  fun word_typ (Type (@{type_name word}, [T])) =
+      Option.map (rpair [] o index1 "BitVec") (try dest_binT T)
     | word_typ _ = NONE
 
   fun word_num (Type (@{type_name word}, [T])) k =
diff -r 2d24e2c02130 -r b17d41779768 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Aug 30 20:50:45 2017 +0200
@@ -22,6 +22,7 @@
 declare -a SOURCES_BASE=(
   "src-base/isabelle_encoding.scala"
   "src-base/plugin.scala"
+  "src-base/syntax_style.scala"
 )
 
 declare -a RESOURCES_BASE=(
diff -r 2d24e2c02130 -r b17d41779768 src/Tools/jEdit/src-base/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala	Wed Aug 30 18:35:23 2017 +0200
+++ b/src/Tools/jEdit/src-base/plugin.scala	Wed Aug 30 20:50:45 2017 +0200
@@ -10,6 +10,7 @@
 import isabelle._
 
 import org.gjt.sp.jedit.EBPlugin
+import org.gjt.sp.util.SyntaxUtilities
 
 
 class Plugin extends EBPlugin
@@ -17,5 +18,7 @@
   override def start()
   {
     Isabelle_System.init()
+
+    SyntaxUtilities.setStyleExtender(Syntax_Style.Dummy_Extender)
   }
 }
diff -r 2d24e2c02130 -r b17d41779768 src/Tools/jEdit/src-base/syntax_style.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/syntax_style.scala	Wed Aug 30 20:50:45 2017 +0200
@@ -0,0 +1,32 @@
+/*  Title:      Tools/jEdit/src-base/syntax_style.scala
+    Author:     Makarius
+
+Extended syntax styles: dummy version.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import org.gjt.sp.util.SyntaxUtilities
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
+
+
+object Syntax_Style
+{
+  private val plain_range: Int = JEditToken.ID_COUNT
+  private val full_range = 6 * plain_range + 1
+
+  object Dummy_Extender extends SyntaxUtilities.StyleExtender
+  {
+    override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
+    {
+      val new_styles = new Array[SyntaxStyle](full_range)
+      for (i <- 0 until full_range) {
+        new_styles(i) = styles(i % plain_range)
+      }
+      new_styles
+    }
+  }
+}