# HG changeset patch
# User paulson
# Date 1528798715 -3600
# Node ID f75d765a281f0f949d6ff16c3b7a91c1760a137f
# Parent  c1db7503dbaa1ee53d79813c6933b8510724b496# Parent  e0b5f2d14bf9315769caf461a55ddd51803de6fe
merged

diff -r e0b5f2d14bf9 -r f75d765a281f src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jun 11 16:23:21 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jun 12 11:18:35 2018 +0100
@@ -6338,12 +6338,10 @@
   have 1: "(\<lambda>z. \<Sum>i\<le>n. a i * z^i) holomorphic_on UNIV"
     by (rule holomorphic_intros)+
   show thesis
-    apply (rule Liouville_weak_inverse [OF 1])
-    apply (rule polyfun_extremal)
-    apply (rule nz)
-    using i that
-    apply auto
-    done
+  proof (rule Liouville_weak_inverse [OF 1])
+    show "\<forall>\<^sub>F x in at_infinity. B \<le> cmod (\<Sum>i\<le>n. a i * x ^ i)" for B
+      using i polyfun_extremal nz by force
+  qed (use that in auto)
 qed
 
 
@@ -6358,14 +6356,15 @@
   case less then show ?thesis by (force simp: ball_empty less_imp_le continuous_on_def holomorphic_on_def intro: that)
 next
   case equal then show ?thesis
-    by (force simp: holomorphic_on_def continuous_on_sing intro: that)
+    by (force simp: holomorphic_on_def intro: that)
 next
   case greater
   have contg: "continuous_on (cball z r) g"
     using cont uniform_limit_theorem [OF eventually_mono ulim F]  by blast
-  have 1: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1 / (2 * complex_of_real pi * \<i>) * g x)"
-    apply (rule continuous_intros continuous_on_subset [OF contg])+
+  have "path_image (circlepath z r) \<subseteq> cball z r"
     using \<open>0 < r\<close> by auto
+  then have 1: "continuous_on (path_image (circlepath z r)) (\<lambda>x. 1 / (2 * complex_of_real pi * \<i>) * g x)"
+    by (intro continuous_intros continuous_on_subset [OF contg])
   have 2: "((\<lambda>u. 1 / (2 * of_real pi * \<i>) * g u / (u - w) ^ 1) has_contour_integral g w) (circlepath z r)"
        if w: "w \<in> ball z r" for w
   proof -
@@ -6389,18 +6388,16 @@
     have cif_tends_cig: "((\<lambda>n. contour_integral(circlepath z r) (\<lambda>u. f n u / (u - w))) \<longlongrightarrow> contour_integral(circlepath z r) (\<lambda>u. g u/(u - w))) F"
       by (rule contour_integral_uniform_limit_circlepath [OF ev_int ul_less F \<open>0 < r\<close>])
     have f_tends_cig: "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> contour_integral (circlepath z r) (\<lambda>u. g u / (u - w))) F"
-      apply (rule Lim_transform_eventually [where f = "\<lambda>n. contour_integral (circlepath z r) (\<lambda>u. f n u/(u - w))"])
-      apply (rule eventually_mono [OF cont])
-      apply (rule contour_integral_unique [OF Cauchy_integral_circlepath])
-      using w
-      apply (auto simp: norm_minus_commute dist_norm cif_tends_cig)
-      done
-    have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> 2 * of_real pi * \<i> * g w) F"
-      apply (rule tendsto_mult_left [OF tendstoI])
-      apply (rule eventually_mono [OF uniform_limitD [OF ulim]], assumption)
-      using w
-      apply (force simp: dist_norm)
-      done
+    proof (rule Lim_transform_eventually)
+      show "\<forall>\<^sub>F x in F. contour_integral (circlepath z r) (\<lambda>u. f x u / (u - w)) 
+                     = 2 * of_real pi * \<i> * f x w"
+        apply (rule eventually_mono [OF cont contour_integral_unique [OF Cauchy_integral_circlepath]])
+        using w\<open>0 < d\<close> d_def by auto
+    qed (auto simp: cif_tends_cig)
+    have "\<And>e. 0 < e \<Longrightarrow> \<forall>\<^sub>F n in F. dist (f n w) (g w) < e"
+      by (rule eventually_mono [OF uniform_limitD [OF ulim]]) (use w in auto)
+    then have "((\<lambda>n. 2 * of_real pi * \<i> * f n w) \<longlongrightarrow> 2 * of_real pi * \<i> * g w) F"
+      by (rule tendsto_mult_left [OF tendstoI])
     then have "((\<lambda>u. g u / (u - w)) has_contour_integral 2 * of_real pi * \<i> * g w) (circlepath z r)"
       using has_contour_integral_integral [OF g_cint] tendsto_unique [OF F f_tends_cig] w
       by (force simp: dist_norm)
@@ -6455,12 +6452,17 @@
     define d where "d = (r - norm(w - z))^2"
     have "d > 0"
       using w by (simp add: dist_commute dist_norm d_def)
-    have dle: "\<And>y. r = cmod (z - y) \<Longrightarrow> d \<le> cmod ((y - w)\<^sup>2)"
-      apply (simp add: d_def norm_power)
-      apply (rule power_mono)
-      apply (metis add_diff_eq diff_add_cancel norm_diff_ineq norm_minus_commute)
-      apply (metis diff_ge_0_iff_ge dist_commute dist_norm less_eq_real_def mem_ball w)
-      done
+    have dle: "d \<le> cmod ((y - w)\<^sup>2)" if "r = cmod (z - y)" for y
+    proof -
+      have "w \<in> ball z (cmod (z - y))"
+        using that w by fastforce
+      then have "cmod (w - z) \<le> cmod (z - y)"
+        by (simp add: dist_complex_def norm_minus_commute)
+      moreover have "cmod (z - y) - cmod (w - z) \<le> cmod (y - w)"
+        by (metis diff_add_cancel diff_add_eq_diff_diff_swap norm_minus_commute norm_triangle_ineq2)
+      ultimately show ?thesis
+        using that by (simp add: d_def norm_power power_mono)
+    qed
     have 1: "\<forall>\<^sub>F n in F. (\<lambda>x. f n x / (x - w)\<^sup>2) contour_integrable_on circlepath z r"
       by (force simp: holomorphic_on_open intro: w Cauchy_derivative_integral_circlepath eventually_mono [OF cont])
     have 2: "uniform_limit (sphere z r) (\<lambda>n x. f n x / (x - w)\<^sup>2) (\<lambda>x. g x / (x - w)\<^sup>2) F"
@@ -6468,9 +6470,8 @@
     proof clarify
       fix e::real
       assume "0 < e"
-      with  \<open>r > 0\<close>
-      show "\<forall>\<^sub>F n in F. \<forall>x\<in>sphere z r. dist (f n x / (x - w)\<^sup>2) (g x / (x - w)\<^sup>2) < e"
-        apply (simp add: diff_divide_distrib [symmetric] norm_divide divide_simps sphere_def dist_norm)
+      with \<open>r > 0\<close> show "\<forall>\<^sub>F n in F. \<forall>x\<in>sphere z r. dist (f n x / (x - w)\<^sup>2) (g x / (x - w)\<^sup>2) < e"
+        apply (simp add: norm_divide divide_simps sphere_def dist_norm)
         apply (rule eventually_mono [OF uniform_limitD [OF ulim], of "e*d"])
          apply (simp add: \<open>0 < d\<close>)
         apply (force simp: dist_norm dle intro: less_le_trans)
@@ -6508,10 +6509,12 @@
                and ul: "uniform_limit (cball z r) f g sequentially"
       using ulim_g [OF \<open>z \<in> S\<close>] by blast 
     have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and> f n holomorphic_on ball z r"
-      apply (intro eventuallyI conjI)
-      using hol_fn holomorphic_on_imp_continuous_on holomorphic_on_subset r apply blast
-      apply (metis hol_fn holomorphic_on_subset interior_cball interior_subset r)
-      done
+    proof (intro eventuallyI conjI)
+      show "continuous_on (cball z r) (f x)" for x
+        using hol_fn holomorphic_on_imp_continuous_on holomorphic_on_subset r by blast
+      show "f x holomorphic_on ball z r" for x
+        by (metis hol_fn holomorphic_on_subset interior_cball interior_subset r)
+    qed
     show ?thesis
       apply (rule holomorphic_uniform_limit [OF *])
       using \<open>0 < r\<close> centre_in_ball ul
@@ -6537,15 +6540,14 @@
       using ulim_g [OF \<open>z \<in> S\<close>] by blast 
     have *: "\<forall>\<^sub>F n in sequentially. continuous_on (cball z r) (f n) \<and>
                                    (\<forall>w \<in> ball z r. ((f n) has_field_derivative (f' n w)) (at w))"
-      apply (intro eventuallyI conjI)
-      apply (meson hfd holomorphic_on_imp_continuous_on holomorphic_on_open holomorphic_on_subset r S)
-      using ball_subset_cball hfd r apply blast
-      done
+    proof (intro eventuallyI conjI ballI)
+      show "continuous_on (cball z r) (f x)" for x
+        by (meson S continuous_on_subset hfd holomorphic_on_imp_continuous_on holomorphic_on_open r)
+      show "w \<in> ball z r \<Longrightarrow> (f x has_field_derivative f' x w) (at w)" for w x
+        using ball_subset_cball hfd r by blast
+    qed
     show ?thesis
-      apply (rule has_complex_derivative_uniform_limit [OF *, of g])
-      using \<open>0 < r\<close> centre_in_ball ul
-      apply force+
-      done
+      by (rule has_complex_derivative_uniform_limit [OF *, of g]) (use \<open>0 < r\<close> ul in \<open>force+\<close>)
   qed
   show ?thesis
     by (rule bchoice) (blast intro: y)
@@ -6569,11 +6571,11 @@
   proof -
     obtain d where "d>0" and d: "cball x d \<subseteq> S"
       using open_contains_cball [of "S"] \<open>x \<in> S\<close> S by blast
-    then show ?thesis
-      apply (rule_tac x=d in exI)
-        using g uniform_limit_on_subset
-        apply (force simp: dist_norm eventually_sequentially)
-          done
+    show ?thesis
+    proof (intro conjI exI)
+      show "uniform_limit (cball x d) (\<lambda>n x. \<Sum>i<n. f i x) g sequentially"
+        using d g uniform_limit_on_subset by (force simp: dist_norm eventually_sequentially)
+    qed (use \<open>d > 0\<close> d in auto)
   qed
   have "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. \<Sum>i<n. f i x) \<longlonglongrightarrow> g x"
     by (metis tendsto_uniform_limitI [OF g])
@@ -6612,14 +6614,14 @@
       using  summable_sums centre_in_ball \<open>0 < d\<close> \<open>summable h\<close> le_h
       by (metis (full_types) Int_iff gg' summable_def that)
     moreover have "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' z) (at z)"
-      apply (rule_tac f=g in DERIV_transform_at [OF _ \<open>0 < r\<close>])
-      apply (simp add: gg' \<open>z \<in> S\<close> \<open>0 < d\<close>)
-      apply (metis (full_types) contra_subsetD dist_commute gg' mem_ball r sums_unique)
-      done
+    proof (rule DERIV_transform_at)
+      show "\<And>x. dist x z < r \<Longrightarrow> g x = (\<Sum>n. f n x)"
+        by (metis subsetD dist_commute gg' mem_ball r sums_unique)
+    qed (use \<open>0 < r\<close> gg' \<open>z \<in> S\<close> \<open>0 < d\<close> in auto)
     ultimately show ?thesis by auto
   qed
   then show ?thesis
-    by (rule_tac x="\<lambda>x. suminf  (\<lambda>n. f n x)" in exI) meson
+    by (rule_tac x="\<lambda>x. suminf (\<lambda>n. f n x)" in exI) meson
 qed
 
 
@@ -6682,12 +6684,9 @@
                (\<lambda>n. of_nat n * (a n) * z ^ (n - 1)) sums g' z \<and> (g has_field_derivative g' z) (at z)"
       apply (rule series_and_derivative_comparison_complex [OF open_ball der])
       apply (rule_tac x="(r - norm z)/2" in exI)
-      apply (simp add: dist_norm)
       apply (rule_tac x="\<lambda>n. of_real(norm(a n)*((r + norm z)/2)^n)" in exI)
       using \<open>r > 0\<close>
-      apply (auto simp: sum eventually_sequentially norm_mult norm_divide norm_power)
-      apply (rule_tac x=0 in exI)
-      apply (force simp: dist_norm intro!: mult_left_mono power_mono y_le)
+      apply (auto simp: sum eventually_sequentially norm_mult norm_power dist_norm intro!: mult_left_mono power_mono y_le)
       done
   then show ?thesis
     by (simp add: ball_def)
@@ -6742,12 +6741,10 @@
         apply (auto simp: assms dist_norm)
         done
     qed
-    show ?thesis
-      apply (rule_tac x="g' w" in exI)
-      apply (rule DERIV_transform_at [where f=g and d="(r - norm(z - w))/2"])
-      using w gg' [of w]
-      apply (auto simp: dist_norm)
-      done
+    have "(f has_field_derivative g' w) (at w)"
+      by (rule DERIV_transform_at [where d="(r - norm(z - w))/2"])
+      (use w gg' [of w] in \<open>(force simp: dist_norm)+\<close>)
+    then show ?thesis ..
   qed
   then show ?thesis by (simp add: holomorphic_on_open)
 qed
@@ -6755,10 +6752,8 @@
 corollary holomorphic_iff_power_series:
      "f holomorphic_on ball z r \<longleftrightarrow>
       (\<forall>w \<in> ball z r. (\<lambda>n. (deriv ^^ n) f z / (fact n) * (w - z)^n) sums f w)"
-  apply (intro iffI ballI)
-   using holomorphic_power_series  apply force
-  apply (rule power_series_holomorphic [where a = "\<lambda>n. (deriv ^^ n) f z / (fact n)"])
-  apply force
+  apply (intro iffI ballI holomorphic_power_series, assumption+)
+  apply (force intro: power_series_holomorphic [where a = "\<lambda>n. (deriv ^^ n) f z / (fact n)"])
   done
 
 corollary power_series_analytic:
@@ -6791,102 +6786,104 @@
   done
 
 lemma holomorphic_fun_eq_0_on_connected:
-  assumes holf: "f holomorphic_on s" and "open s"
-      and cons: "connected s"
+  assumes holf: "f holomorphic_on S" and "open S"
+      and cons: "connected S"
       and der: "\<And>n. (deriv ^^ n) f z = 0"
-      and "z \<in> s" "w \<in> s"
+      and "z \<in> S" "w \<in> S"
     shows "f w = 0"
 proof -
-  have *: "\<And>x e. \<lbrakk> \<forall>xa. (deriv ^^ xa) f x = 0;  ball x e \<subseteq> s\<rbrakk>
-           \<Longrightarrow> ball x e \<subseteq> (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
-    apply auto
-    apply (rule holomorphic_fun_eq_0_on_ball [OF holomorphic_higher_deriv])
-    apply (rule holomorphic_on_subset [OF holf], simp_all)
-    by (metis funpow_add o_apply)
-  have 1: "openin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
+  have *: "ball x e \<subseteq> (\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0})"
+    if "\<forall>u. (deriv ^^ u) f x = 0" "ball x e \<subseteq> S" for x e
+  proof -
+    have "\<And>x' n. dist x x' < e \<Longrightarrow> (deriv ^^ n) f x' = 0"
+      apply (rule holomorphic_fun_eq_0_on_ball [OF holomorphic_higher_deriv])
+         apply (rule holomorphic_on_subset [OF holf])
+      using that apply simp_all
+      by (metis funpow_add o_apply)
+    with that show ?thesis by auto
+  qed
+  have 1: "openin (subtopology euclidean S) (\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0})"
     apply (rule open_subset, force)
-    using \<open>open s\<close>
+    using \<open>open S\<close>
     apply (simp add: open_contains_ball Ball_def)
     apply (erule all_forward)
     using "*" by auto blast+
-  have 2: "closedin (subtopology euclidean s) (\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0})"
+  have 2: "closedin (subtopology euclidean S) (\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0})"
     using assms
     by (auto intro: continuous_closedin_preimage_constant holomorphic_on_imp_continuous_on holomorphic_higher_deriv)
-  obtain e where "e>0" and e: "ball w e \<subseteq> s" using openE [OF \<open>open s\<close> \<open>w \<in> s\<close>] .
+  obtain e where "e>0" and e: "ball w e \<subseteq> S" using openE [OF \<open>open S\<close> \<open>w \<in> S\<close>] .
   then have holfb: "f holomorphic_on ball w e"
     using holf holomorphic_on_subset by blast
-  have 3: "(\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0}) = s \<Longrightarrow> f w = 0"
+  have 3: "(\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0}) = S \<Longrightarrow> f w = 0"
     using \<open>e>0\<close> e by (force intro: holomorphic_fun_eq_0_on_ball [OF holfb])
   show ?thesis
-    using cons der \<open>z \<in> s\<close>
+    using cons der \<open>z \<in> S\<close>
     apply (simp add: connected_clopen)
-    apply (drule_tac x="\<Inter>n. {w \<in> s. (deriv ^^ n) f w = 0}" in spec)
+    apply (drule_tac x="\<Inter>n. {w \<in> S. (deriv ^^ n) f w = 0}" in spec)
     apply (auto simp: 1 2 3)
     done
 qed
 
 lemma holomorphic_fun_eq_on_connected:
-  assumes "f holomorphic_on s" "g holomorphic_on s" and "open s"  "connected s"
+  assumes "f holomorphic_on S" "g holomorphic_on S" and "open S"  "connected S"
       and "\<And>n. (deriv ^^ n) f z = (deriv ^^ n) g z"
-      and "z \<in> s" "w \<in> s"
+      and "z \<in> S" "w \<in> S"
     shows "f w = g w"
-  apply (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>x. f x - g x" s z, simplified])
-  apply (intro assms holomorphic_intros)
-  using assms apply simp_all
-  apply (subst higher_deriv_diff, auto)
-  done
+proof (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>x. f x - g x" S z, simplified])
+  show "(\<lambda>x. f x - g x) holomorphic_on S"
+    by (intro assms holomorphic_intros)
+  show "\<And>n. (deriv ^^ n) (\<lambda>x. f x - g x) z = 0"
+    using assms higher_deriv_diff by auto
+qed (use assms in auto)
 
 lemma holomorphic_fun_eq_const_on_connected:
-  assumes holf: "f holomorphic_on s" and "open s"
-      and cons: "connected s"
+  assumes holf: "f holomorphic_on S" and "open S"
+      and cons: "connected S"
       and der: "\<And>n. 0 < n \<Longrightarrow> (deriv ^^ n) f z = 0"
-      and "z \<in> s" "w \<in> s"
+      and "z \<in> S" "w \<in> S"
     shows "f w = f z"
-  apply (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>w. f w - f z" s z, simplified])
-  apply (intro assms holomorphic_intros)
-  using assms apply simp_all
-  apply (subst higher_deriv_diff)
-  apply (intro holomorphic_intros | simp)+
-  done
-
+proof (rule holomorphic_fun_eq_0_on_connected [of "\<lambda>w. f w - f z" S z, simplified])
+  show "(\<lambda>w. f w - f z) holomorphic_on S"
+    by (intro assms holomorphic_intros)
+  show "\<And>n. (deriv ^^ n) (\<lambda>w. f w - f z) z = 0"
+    by (subst higher_deriv_diff) (use assms in \<open>auto intro: holomorphic_intros\<close>)
+qed (use assms in auto)
 
 subsection\<open>Some basic lemmas about poles/singularities\<close>
 
 lemma pole_lemma:
-  assumes holf: "f holomorphic_on s" and a: "a \<in> interior s"
+  assumes holf: "f holomorphic_on S" and a: "a \<in> interior S"
     shows "(\<lambda>z. if z = a then deriv f a
-                 else (f z - f a) / (z - a)) holomorphic_on s" (is "?F holomorphic_on s")
+                 else (f z - f a) / (z - a)) holomorphic_on S" (is "?F holomorphic_on S")
 proof -
-  have F1: "?F field_differentiable (at u within s)" if "u \<in> s" "u \<noteq> a" for u
+  have F1: "?F field_differentiable (at u within S)" if "u \<in> S" "u \<noteq> a" for u
   proof -
-    have fcd: "f field_differentiable at u within s"
-      using holf holomorphic_on_def by (simp add: \<open>u \<in> s\<close>)
-    have cd: "(\<lambda>z. (f z - f a) / (z - a)) field_differentiable at u within s"
+    have fcd: "f field_differentiable at u within S"
+      using holf holomorphic_on_def by (simp add: \<open>u \<in> S\<close>)
+    have cd: "(\<lambda>z. (f z - f a) / (z - a)) field_differentiable at u within S"
       by (rule fcd derivative_intros | simp add: that)+
     have "0 < dist a u" using that dist_nz by blast
     then show ?thesis
-      by (rule field_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> s\<close>)
+      by (rule field_differentiable_transform_within [OF _ _ _ cd]) (auto simp: \<open>u \<in> S\<close>)
   qed
-  have F2: "?F field_differentiable at a" if "0 < e" "ball a e \<subseteq> s" for e
+  have F2: "?F field_differentiable at a" if "0 < e" "ball a e \<subseteq> S" for e
   proof -
     have holfb: "f holomorphic_on ball a e"
-      by (rule holomorphic_on_subset [OF holf \<open>ball a e \<subseteq> s\<close>])
+      by (rule holomorphic_on_subset [OF holf \<open>ball a e \<subseteq> S\<close>])
     have 2: "?F holomorphic_on ball a e - {a}"
-      apply (rule holomorphic_on_subset [where s = "s - {a}"])
-      apply (simp add: holomorphic_on_def field_differentiable_def [symmetric])
+      apply (simp add: holomorphic_on_def flip: field_differentiable_def)
       using mem_ball that
       apply (auto intro: F1 field_differentiable_within_subset)
       done
     have "isCont (\<lambda>z. if z = a then deriv f a else (f z - f a) / (z - a)) x"
             if "dist a x < e" for x
     proof (cases "x=a")
-      case True then show ?thesis
-      using holfb \<open>0 < e\<close>
-      apply (simp add: holomorphic_on_open field_differentiable_def [symmetric])
-      apply (drule_tac x=a in bspec)
-      apply (auto simp: DERIV_deriv_iff_field_differentiable [symmetric] continuous_at DERIV_iff2
+      case True 
+      then have "f field_differentiable at a"
+        using holfb \<open>0 < e\<close> holomorphic_on_imp_differentiable_at by auto
+      with True show ?thesis
+        by (auto simp: continuous_at DERIV_iff2 simp flip: DERIV_deriv_iff_field_differentiable
                 elim: rev_iffD1 [OF _ LIM_equal])
-      done
     next
       case False with 2 that show ?thesis
         by (force simp: holomorphic_on_open open_Diff field_differentiable_def [symmetric] field_differentiable_imp_continuous_at)
@@ -6901,29 +6898,29 @@
   qed
   show ?thesis
   proof
-    fix x assume "x \<in> s" show "?F field_differentiable at x within s"
+    fix x assume "x \<in> S" show "?F field_differentiable at x within S"
     proof (cases "x=a")
       case True then show ?thesis
       using a by (auto simp: mem_interior intro: field_differentiable_at_within F2)
     next
-      case False with F1 \<open>x \<in> s\<close>
+      case False with F1 \<open>x \<in> S\<close>
       show ?thesis by blast
     qed
   qed
 qed
 
 proposition pole_theorem:
-  assumes holg: "g holomorphic_on s" and a: "a \<in> interior s"
-      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
+  assumes holg: "g holomorphic_on S" and a: "a \<in> interior S"
+      and eq: "\<And>z. z \<in> S - {a} \<Longrightarrow> g z = (z - a) * f z"
     shows "(\<lambda>z. if z = a then deriv g a
-                 else f z - g a/(z - a)) holomorphic_on s"
+                 else f z - g a/(z - a)) holomorphic_on S"
   using pole_lemma [OF holg a]
   by (rule holomorphic_transform) (simp add: eq divide_simps)
 
 lemma pole_lemma_open:
-  assumes "f holomorphic_on s" "open s"
-    shows "(\<lambda>z. if z = a then deriv f a else (f z - f a)/(z - a)) holomorphic_on s"
-proof (cases "a \<in> s")
+  assumes "f holomorphic_on S" "open S"
+    shows "(\<lambda>z. if z = a then deriv f a else (f z - f a)/(z - a)) holomorphic_on S"
+proof (cases "a \<in> S")
   case True with assms interior_eq pole_lemma
     show ?thesis by fastforce
 next
@@ -6935,48 +6932,53 @@
 qed
 
 proposition pole_theorem_open:
-  assumes holg: "g holomorphic_on s" and s: "open s"
-      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
+  assumes holg: "g holomorphic_on S" and S: "open S"
+      and eq: "\<And>z. z \<in> S - {a} \<Longrightarrow> g z = (z - a) * f z"
     shows "(\<lambda>z. if z = a then deriv g a
-                 else f z - g a/(z - a)) holomorphic_on s"
-  using pole_lemma_open [OF holg s]
+                 else f z - g a/(z - a)) holomorphic_on S"
+  using pole_lemma_open [OF holg S]
   by (rule holomorphic_transform) (auto simp: eq divide_simps)
 
 proposition pole_theorem_0:
-  assumes holg: "g holomorphic_on s" and a: "a \<in> interior s"
-      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
+  assumes holg: "g holomorphic_on S" and a: "a \<in> interior S"
+      and eq: "\<And>z. z \<in> S - {a} \<Longrightarrow> g z = (z - a) * f z"
       and [simp]: "f a = deriv g a" "g a = 0"
-    shows "f holomorphic_on s"
+    shows "f holomorphic_on S"
   using pole_theorem [OF holg a eq]
   by (rule holomorphic_transform) (auto simp: eq divide_simps)
 
 proposition pole_theorem_open_0:
-  assumes holg: "g holomorphic_on s" and s: "open s"
-      and eq: "\<And>z. z \<in> s - {a} \<Longrightarrow> g z = (z - a) * f z"
+  assumes holg: "g holomorphic_on S" and S: "open S"
+      and eq: "\<And>z. z \<in> S - {a} \<Longrightarrow> g z = (z - a) * f z"
       and [simp]: "f a = deriv g a" "g a = 0"
-    shows "f holomorphic_on s"
-  using pole_theorem_open [OF holg s eq]
+    shows "f holomorphic_on S"
+  using pole_theorem_open [OF holg S eq]
   by (rule holomorphic_transform) (auto simp: eq divide_simps)
 
 lemma pole_theorem_analytic:
-  assumes g: "g analytic_on s"
-      and eq: "\<And>z. z \<in> s
+  assumes g: "g analytic_on S"
+      and eq: "\<And>z. z \<in> S
              \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
-    shows "(\<lambda>z. if z = a then deriv g a
-                 else f z - g a/(z - a)) analytic_on s"
-using g
-apply (simp add: analytic_on_def Ball_def)
-apply (safe elim!: all_forward dest!: eq)
-apply (rule_tac x="min d e" in exI, simp)
-apply (rule pole_theorem_open)
-apply (auto simp: holomorphic_on_subset subset_ball)
-done
+    shows "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on S" (is "?F analytic_on S")
+  unfolding analytic_on_def
+proof 
+  fix x
+  assume "x \<in> S"
+  with g obtain e where "0 < e" and e: "g holomorphic_on ball x e" 
+    by (auto simp add: analytic_on_def)
+  obtain d where "0 < d" and d: "\<And>w. w \<in> ball x d - {a} \<Longrightarrow> g w = (w - a) * f w"
+    using \<open>x \<in> S\<close> eq by blast
+  have "?F holomorphic_on ball x (min d e)"
+    using d e \<open>x \<in> S\<close> by (fastforce simp: holomorphic_on_subset subset_ball intro!: pole_theorem_open)
+  then show "\<exists>e>0. ?F holomorphic_on ball x e"
+    using \<open>0 < d\<close> \<open>0 < e\<close> not_le by fastforce
+qed
 
 lemma pole_theorem_analytic_0:
-  assumes g: "g analytic_on s"
-      and eq: "\<And>z. z \<in> s \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
+  assumes g: "g analytic_on S"
+      and eq: "\<And>z. z \<in> S \<Longrightarrow> \<exists>d. 0 < d \<and> (\<forall>w \<in> ball z d - {a}. g w = (w - a) * f w)"
       and [simp]: "f a = deriv g a" "g a = 0"
-    shows "f analytic_on s"
+    shows "f analytic_on S"
 proof -
   have [simp]: "(\<lambda>z. if z = a then deriv g a else f z - g a / (z - a)) = f"
     by auto
@@ -6985,22 +6987,27 @@
 qed
 
 lemma pole_theorem_analytic_open_superset:
-  assumes g: "g analytic_on s" and "s \<subseteq> t" "open t"
-      and eq: "\<And>z. z \<in> t - {a} \<Longrightarrow> g z = (z - a) * f z"
+  assumes g: "g analytic_on S" and "S \<subseteq> T" "open T"
+      and eq: "\<And>z. z \<in> T - {a} \<Longrightarrow> g z = (z - a) * f z"
     shows "(\<lambda>z. if z = a then deriv g a
-                 else f z - g a/(z - a)) analytic_on s"
-  apply (rule pole_theorem_analytic [OF g])
-  apply (rule openE [OF \<open>open t\<close>])
-  using assms eq by auto
+                 else f z - g a/(z - a)) analytic_on S"
+proof (rule pole_theorem_analytic [OF g])
+  fix z
+  assume "z \<in> S"
+  then obtain e where "0 < e" and e: "ball z e \<subseteq> T"
+    using assms openE by blast
+  then show "\<exists>d>0. \<forall>w\<in>ball z d - {a}. g w = (w - a) * f w"
+    using eq by auto
+qed
 
 lemma pole_theorem_analytic_open_superset_0:
-  assumes g: "g analytic_on s" "s \<subseteq> t" "open t" "\<And>z. z \<in> t - {a} \<Longrightarrow> g z = (z - a) * f z"
+  assumes g: "g analytic_on S" "S \<subseteq> T" "open T" "\<And>z. z \<in> T - {a} \<Longrightarrow> g z = (z - a) * f z"
       and [simp]: "f a = deriv g a" "g a = 0"
-    shows "f analytic_on s"
+    shows "f analytic_on S"
 proof -
   have [simp]: "(\<lambda>z. if z = a then deriv g a else f z - g a / (z - a)) = f"
     by auto
-  have "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on s"
+  have "(\<lambda>z. if z = a then deriv g a else f z - g a/(z - a)) analytic_on S"
     by (rule pole_theorem_analytic_open_superset [OF g])
   then show ?thesis by simp
 qed
@@ -7011,24 +7018,25 @@
 text\<open>Proof is based on Dixon's, as presented in Lang's "Complex Analysis" book (page 147).\<close>
 
 lemma contour_integral_continuous_on_linepath_2D:
-  assumes "open u" and cont_dw: "\<And>w. w \<in> u \<Longrightarrow> F w contour_integrable_on (linepath a b)"
-      and cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). F x y)"
-      and abu: "closed_segment a b \<subseteq> u"
-    shows "continuous_on u (\<lambda>w. contour_integral (linepath a b) (F w))"
+  assumes "open U" and cont_dw: "\<And>w. w \<in> U \<Longrightarrow> F w contour_integrable_on (linepath a b)"
+      and cond_uu: "continuous_on (U \<times> U) (\<lambda>(x,y). F x y)"
+      and abu: "closed_segment a b \<subseteq> U"
+    shows "continuous_on U (\<lambda>w. contour_integral (linepath a b) (F w))"
 proof -
-  have *: "\<exists>d>0. \<forall>x'\<in>u. dist x' w < d \<longrightarrow>
+  have *: "\<exists>d>0. \<forall>x'\<in>U. dist x' w < d \<longrightarrow>
                          dist (contour_integral (linepath a b) (F x'))
                               (contour_integral (linepath a b) (F w)) \<le> \<epsilon>"
-          if "w \<in> u" "0 < \<epsilon>" "a \<noteq> b" for w \<epsilon>
+          if "w \<in> U" "0 < \<epsilon>" "a \<noteq> b" for w \<epsilon>
   proof -
-    obtain \<delta> where "\<delta>>0" and \<delta>: "cball w \<delta> \<subseteq> u" using open_contains_cball \<open>open u\<close> \<open>w \<in> u\<close> by force
-    let ?TZ = "{(t,z) |t z. t \<in> cball w \<delta> \<and> z \<in> closed_segment a b}"
+    obtain \<delta> where "\<delta>>0" and \<delta>: "cball w \<delta> \<subseteq> U" using open_contains_cball \<open>open U\<close> \<open>w \<in> U\<close> by force
+    let ?TZ = "cball w \<delta>  \<times> closed_segment a b"
     have "uniformly_continuous_on ?TZ (\<lambda>(x,y). F x y)"
-      apply (rule compact_uniformly_continuous)
-      apply (rule continuous_on_subset[OF cond_uu])
-      using abu \<delta>
-      apply (auto simp: compact_Times simp del: mem_cball)
-      done
+    proof (rule compact_uniformly_continuous)
+      show "continuous_on ?TZ (\<lambda>(x,y). F x y)"
+        by (rule continuous_on_subset[OF cond_uu]) (use SigmaE \<delta> abu in blast)
+      show "compact ?TZ"
+        by (simp add: compact_Times)
+    qed
     then obtain \<eta> where "\<eta>>0"
         and \<eta>: "\<And>x x'. \<lbrakk>x\<in>?TZ; x'\<in>?TZ; dist x' x < \<eta>\<rbrakk> \<Longrightarrow>
                          dist ((\<lambda>(x,y). F x y) x') ((\<lambda>(x,y). F x y) x) < \<epsilon>/norm(b - a)"
@@ -7040,13 +7048,13 @@
              for x1 x2 x1' x2'
       using \<eta> [of "(x1,x2)" "(x1',x2')"] by (force simp: dist_norm)
     have le_ee: "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>"
-                if "x' \<in> u" "cmod (x' - w) < \<delta>" "cmod (x' - w) < \<eta>"  for x'
+                if "x' \<in> U" "cmod (x' - w) < \<delta>" "cmod (x' - w) < \<eta>"  for x'
     proof -
-      have "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>/norm(b - a) * norm(b - a)"
+      have "(\<lambda>x. F x' x - F w x) contour_integrable_on linepath a b"
+        by (simp add: \<open>w \<in> U\<close> cont_dw contour_integrable_diff that)
+      then have "cmod (contour_integral (linepath a b) (\<lambda>x. F x' x - F w x)) \<le> \<epsilon>/norm(b - a) * norm(b - a)"
         apply (rule has_contour_integral_bound_linepath [OF has_contour_integral_integral _ \<eta>])
-        apply (rule contour_integrable_diff [OF cont_dw cont_dw])
-        using \<open>0 < \<epsilon>\<close> \<open>a \<noteq> b\<close> \<open>0 < \<delta>\<close> \<open>w \<in> u\<close> that
-        apply (auto simp: norm_minus_commute)
+        using \<open>0 < \<epsilon>\<close> \<open>0 < \<delta>\<close> that apply (auto simp: norm_minus_commute)
         done
       also have "\<dots> = \<epsilon>" using \<open>a \<noteq> b\<close> by simp
       finally show ?thesis .
@@ -7054,22 +7062,26 @@
     show ?thesis
       apply (rule_tac x="min \<delta> \<eta>" in exI)
       using \<open>0 < \<delta>\<close> \<open>0 < \<eta>\<close>
-      apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> u\<close> intro: le_ee)
+      apply (auto simp: dist_norm contour_integral_diff [OF cont_dw cont_dw, symmetric] \<open>w \<in> U\<close> intro: le_ee)
       done
   qed
   show ?thesis
-    apply (rule continuous_onI)
-    apply (cases "a=b")
-    apply (auto intro: *)
-    done
+  proof (cases "a=b")
+    case True
+    then show ?thesis by simp
+  next
+    case False
+    show ?thesis
+      by (rule continuous_onI) (use False in \<open>auto intro: *\<close>)
+  qed
 qed
 
 text\<open>This version has @{term"polynomial_function \<gamma>"} as an additional assumption.\<close>
 lemma Cauchy_integral_formula_global_weak:
-    assumes u: "open u" and holf: "f holomorphic_on u"
-        and z: "z \<in> u" and \<gamma>: "polynomial_function \<gamma>"
-        and pasz: "path_image \<gamma> \<subseteq> u - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
-        and zero: "\<And>w. w \<notin> u \<Longrightarrow> winding_number \<gamma> w = 0"
+  assumes "open U" and holf: "f holomorphic_on U"
+        and z: "z \<in> U" and \<gamma>: "polynomial_function \<gamma>"
+        and pasz: "path_image \<gamma> \<subseteq> U - {z}" and loop: "pathfinish \<gamma> = pathstart \<gamma>"
+        and zero: "\<And>w. w \<notin> U \<Longrightarrow> winding_number \<gamma> w = 0"
       shows "((\<lambda>w. f w / (w - z)) has_contour_integral (2*pi * \<i> * winding_number \<gamma> z * f z)) \<gamma>"
 proof -
   obtain \<gamma>' where pf\<gamma>': "polynomial_function \<gamma>'" and \<gamma>': "\<And>x. (\<gamma> has_vector_derivative (\<gamma>' x)) (at x)"
@@ -7084,46 +7096,50 @@
     by (auto simp: path_polynomial_function valid_path_polynomial_function)
   then have ov: "open v"
     by (simp add: v_def open_winding_number_levelsets loop)
-  have uv_Un: "u \<union> v = UNIV"
+  have uv_Un: "U \<union> v = UNIV"
     using pasz zero by (auto simp: v_def)
-  have conf: "continuous_on u f"
+  have conf: "continuous_on U f"
     by (metis holf holomorphic_on_imp_continuous_on)
-  have hol_d: "(d y) holomorphic_on u" if "y \<in> u" for y
+  have hol_d: "(d y) holomorphic_on U" if "y \<in> U" for y
   proof -
-    have *: "(\<lambda>c. if c = y then deriv f y else (f c - f y) / (c - y)) holomorphic_on u"
-      by (simp add: holf pole_lemma_open u)
+    have *: "(\<lambda>c. if c = y then deriv f y else (f c - f y) / (c - y)) holomorphic_on U"
+      by (simp add: holf pole_lemma_open \<open>open U\<close>)
     then have "isCont (\<lambda>x. if x = y then deriv f y else (f x - f y) / (x - y)) y"
-      using at_within_open field_differentiable_imp_continuous_at holomorphic_on_def that u by fastforce
-    then have "continuous_on u (d y)"
-      apply (simp add: d_def continuous_on_eq_continuous_at u, clarify)
+      using at_within_open field_differentiable_imp_continuous_at holomorphic_on_def that \<open>open U\<close> by fastforce
+    then have "continuous_on U (d y)"
+      apply (simp add: d_def continuous_on_eq_continuous_at \<open>open U\<close>, clarify)
       using * holomorphic_on_def
-      by (meson field_differentiable_within_open field_differentiable_imp_continuous_at u)
-    moreover have "d y holomorphic_on u - {y}"
-      apply (simp add: d_def holomorphic_on_open u open_delete field_differentiable_def [symmetric])
-      apply (intro ballI)
-      apply (rename_tac w)
-      apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in field_differentiable_transform_within)
-      apply (auto simp: dist_pos_lt dist_commute intro!: derivative_intros)
-      using analytic_on_imp_differentiable_at analytic_on_open holf u apply blast
-      done
+      by (meson field_differentiable_within_open field_differentiable_imp_continuous_at \<open>open U\<close>)
+    moreover have "d y holomorphic_on U - {y}"
+    proof -
+      have "\<And>w. w \<in> U - {y} \<Longrightarrow>
+                 (\<lambda>w. if w = y then deriv f y else (f w - f y) / (w - y)) field_differentiable at w"
+        apply (rule_tac d="dist w y" and f = "\<lambda>w. (f w - f y)/(w - y)" in field_differentiable_transform_within)
+           apply (auto simp: dist_pos_lt dist_commute intro!: derivative_intros)
+        using \<open>open U\<close> holf holomorphic_on_imp_differentiable_at by blast
+      then show ?thesis
+        unfolding field_differentiable_def by (simp add: d_def holomorphic_on_open \<open>open U\<close> open_delete)
+    qed
     ultimately show ?thesis
-      by (rule no_isolated_singularity) (auto simp: u)
+      by (rule no_isolated_singularity) (auto simp: \<open>open U\<close>)
   qed
   have cint_fxy: "(\<lambda>x. (f x - f y) / (x - y)) contour_integrable_on \<gamma>" if "y \<notin> path_image \<gamma>" for y
-    apply (rule contour_integrable_holomorphic_simple [where S = "u-{y}"])
-    using \<open>valid_path \<gamma>\<close> pasz
-    apply (auto simp: u open_delete)
-    apply (rule continuous_intros holomorphic_intros continuous_on_subset [OF conf] holomorphic_on_subset [OF holf] |
-                force simp: that)+
-    done
+  proof (rule contour_integrable_holomorphic_simple [where S = "U-{y}"])
+    show "(\<lambda>x. (f x - f y) / (x - y)) holomorphic_on U - {y}"
+      by (force intro: holomorphic_intros holomorphic_on_subset [OF holf])
+    show "path_image \<gamma> \<subseteq> U - {y}"
+      using pasz that by blast
+  qed (auto simp: \<open>open U\<close> open_delete \<open>valid_path \<gamma>\<close>)
   define h where
-    "h z = (if z \<in> u then contour_integral \<gamma> (d z) else contour_integral \<gamma> (\<lambda>w. f w/(w - z)))" for z
-  have U: "\<And>z. z \<in> u \<Longrightarrow> ((d z) has_contour_integral h z) \<gamma>"
+    "h z = (if z \<in> U then contour_integral \<gamma> (d z) else contour_integral \<gamma> (\<lambda>w. f w/(w - z)))" for z
+  have U: "((d z) has_contour_integral h z) \<gamma>" if "z \<in> U" for z
+  proof -
+    have "d z holomorphic_on U"
+      by (simp add: hol_d that)
+    with that show ?thesis
     apply (simp add: h_def)
-    apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=u]])
-    using u pasz \<open>valid_path \<gamma>\<close>
-    apply (auto intro: holomorphic_on_imp_continuous_on hol_d)
-    done
+      by (meson Diff_subset \<open>open U\<close> \<open>valid_path \<gamma>\<close> contour_integrable_holomorphic_simple has_contour_integral_integral pasz subset_trans)
+  qed
   have V: "((\<lambda>w. f w / (w - z)) has_contour_integral h z) \<gamma>" if z: "z \<in> v" for z
   proof -
     have 0: "0 = (f z) * 2 * of_real (2 * pi) * \<i> * winding_number \<gamma> z"
@@ -7142,24 +7158,24 @@
     ultimately have *: "((\<lambda>x. f z / (x - z) + (f x - f z) / (x - z)) has_contour_integral (0 + contour_integral \<gamma> (d z))) \<gamma>"
       by (rule has_contour_integral_add)
     have "((\<lambda>w. f w / (w - z)) has_contour_integral contour_integral \<gamma> (d z)) \<gamma>"
-            if  "z \<in> u"
+            if  "z \<in> U"
       using * by (auto simp: divide_simps has_contour_integral_eq)
     moreover have "((\<lambda>w. f w / (w - z)) has_contour_integral contour_integral \<gamma> (\<lambda>w. f w / (w - z))) \<gamma>"
-            if "z \<notin> u"
-      apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=u]])
-      using u pasz \<open>valid_path \<gamma>\<close> that
+            if "z \<notin> U"
+      apply (rule has_contour_integral_integral [OF contour_integrable_holomorphic_simple [where S=U]])
+      using U pasz \<open>valid_path \<gamma>\<close> that
       apply (auto intro: holomorphic_on_imp_continuous_on hol_d)
-      apply (rule continuous_intros conf holomorphic_intros holf | force)+
+       apply (rule continuous_intros conf holomorphic_intros holf assms | force)+
       done
     ultimately show ?thesis
       using z by (simp add: h_def)
   qed
   have znot: "z \<notin> path_image \<gamma>"
     using pasz by blast
-  obtain d0 where "d0>0" and d0: "\<And>x y. x \<in> path_image \<gamma> \<Longrightarrow> y \<in> - u \<Longrightarrow> d0 \<le> dist x y"
-    using separate_compact_closed [of "path_image \<gamma>" "-u"] pasz u
+  obtain d0 where "d0>0" and d0: "\<And>x y. x \<in> path_image \<gamma> \<Longrightarrow> y \<in> - U \<Longrightarrow> d0 \<le> dist x y"
+    using separate_compact_closed [of "path_image \<gamma>" "-U"] pasz \<open>open U\<close>
     by (fastforce simp add: \<open>path \<gamma>\<close> compact_path_image)
-  obtain dd where "0 < dd" and dd: "{y + k | y k. y \<in> path_image \<gamma> \<and> k \<in> ball 0 dd} \<subseteq> u"
+  obtain dd where "0 < dd" and dd: "{y + k | y k. y \<in> path_image \<gamma> \<and> k \<in> ball 0 dd} \<subseteq> U"
     apply (rule that [of "d0/2"])
     using \<open>0 < d0\<close>
     apply (auto simp: dist_norm dest: d0)
@@ -7174,27 +7190,27 @@
     using \<open>0 < dd\<close>
     apply (rule_tac x="dd/2" in exI, auto)
     done
-  obtain t where "compact t" and subt: "path_image \<gamma> \<subseteq> interior t" and t: "t \<subseteq> u"
+  obtain T where "compact T" and subt: "path_image \<gamma> \<subseteq> interior T" and T: "T \<subseteq> U"
     apply (rule that [OF _ 1])
     apply (fastforce simp add: \<open>valid_path \<gamma>\<close> compact_valid_path_image intro!: compact_sums)
     apply (rule order_trans [OF _ dd])
     using \<open>0 < dd\<close> by fastforce
   obtain L where "L>0"
-           and L: "\<And>f B. \<lbrakk>f holomorphic_on interior t; \<And>z. z\<in>interior t \<Longrightarrow> cmod (f z) \<le> B\<rbrakk> \<Longrightarrow>
+           and L: "\<And>f B. \<lbrakk>f holomorphic_on interior T; \<And>z. z\<in>interior T \<Longrightarrow> cmod (f z) \<le> B\<rbrakk> \<Longrightarrow>
                          cmod (contour_integral \<gamma> f) \<le> L * B"
       using contour_integral_bound_exists [OF open_interior \<open>valid_path \<gamma>\<close> subt]
       by blast
-  have "bounded(f ` t)"
-    by (meson \<open>compact t\<close> compact_continuous_image compact_imp_bounded conf continuous_on_subset t)
-  then obtain D where "D>0" and D: "\<And>x. x \<in> t \<Longrightarrow> norm (f x) \<le> D"
+  have "bounded(f ` T)"
+    by (meson \<open>compact T\<close> compact_continuous_image compact_imp_bounded conf continuous_on_subset T)
+  then obtain D where "D>0" and D: "\<And>x. x \<in> T \<Longrightarrow> norm (f x) \<le> D"
     by (auto simp: bounded_pos)
-  obtain C where "C>0" and C: "\<And>x. x \<in> t \<Longrightarrow> norm x \<le> C"
-    using \<open>compact t\<close> bounded_pos compact_imp_bounded by force
+  obtain C where "C>0" and C: "\<And>x. x \<in> T \<Longrightarrow> norm x \<le> C"
+    using \<open>compact T\<close> bounded_pos compact_imp_bounded by force
   have "dist (h y) 0 \<le> e" if "0 < e" and le: "D * L / e + C \<le> cmod y" for e y
   proof -
     have "D * L / e > 0"  using \<open>D>0\<close> \<open>L>0\<close> \<open>e>0\<close> by simp
     with le have ybig: "norm y > C" by force
-    with C have "y \<notin> t"  by force
+    with C have "y \<notin> T"  by force
     then have ynot: "y \<notin> path_image \<gamma>"
       using subt interior_subset by blast
     have [simp]: "winding_number \<gamma> y = 0"
@@ -7204,12 +7220,12 @@
       done
     have [simp]: "h y = contour_integral \<gamma> (\<lambda>w. f w/(w - y))"
       by (rule contour_integral_unique [symmetric]) (simp add: v_def ynot V)
-    have holint: "(\<lambda>w. f w / (w - y)) holomorphic_on interior t"
+    have holint: "(\<lambda>w. f w / (w - y)) holomorphic_on interior T"
       apply (rule holomorphic_on_divide)
-      using holf holomorphic_on_subset interior_subset t apply blast
+      using holf holomorphic_on_subset interior_subset T apply blast
       apply (rule holomorphic_intros)+
-      using \<open>y \<notin> t\<close> interior_subset by auto
-    have leD: "cmod (f z / (z - y)) \<le> D * (e / L / D)" if z: "z \<in> interior t" for z
+      using \<open>y \<notin> T\<close> interior_subset by auto
+    have leD: "cmod (f z / (z - y)) \<le> D * (e / L / D)" if z: "z \<in> interior T" for z
     proof -
       have "D * L / e + cmod z \<le> cmod y"
         using le C [of z] z using interior_subset by force
@@ -7238,32 +7254,33 @@
   moreover have "h holomorphic_on UNIV"
   proof -
     have con_ff: "continuous (at (x,z)) (\<lambda>(x,y). (f y - f x) / (y - x))"
-                 if "x \<in> u" "z \<in> u" "x \<noteq> z" for x z
+                 if "x \<in> U" "z \<in> U" "x \<noteq> z" for x z
       using that conf
-      apply (simp add: split_def continuous_on_eq_continuous_at u)
+      apply (simp add: split_def continuous_on_eq_continuous_at \<open>open U\<close>)
       apply (simp | rule continuous_intros continuous_within_compose2 [where g=f])+
       done
     have con_fstsnd: "continuous_on UNIV (\<lambda>x. (fst x - snd x) ::complex)"
       by (rule continuous_intros)+
-    have open_uu_Id: "open (u \<times> u - Id)"
+    have open_uu_Id: "open (U \<times> U - Id)"
       apply (rule open_Diff)
-      apply (simp add: open_Times u)
+      apply (simp add: open_Times \<open>open U\<close>)
       using continuous_closed_preimage_constant [OF con_fstsnd closed_UNIV, of 0]
       apply (auto simp: Id_fstsnd_eq algebra_simps)
       done
-    have con_derf: "continuous (at z) (deriv f)" if "z \<in> u" for z
-      apply (rule continuous_on_interior [of u])
-      apply (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on u)
-      by (simp add: interior_open that u)
+    have con_derf: "continuous (at z) (deriv f)" if "z \<in> U" for z
+      apply (rule continuous_on_interior [of U])
+      apply (simp add: holf holomorphic_deriv holomorphic_on_imp_continuous_on \<open>open U\<close>)
+      by (simp add: interior_open that \<open>open U\<close>)
     have tendsto_f': "((\<lambda>(x,y). if y = x then deriv f (x)
                                 else (f (y) - f (x)) / (y - x)) \<longlongrightarrow> deriv f x)
-                      (at (x, x) within u \<times> u)" if "x \<in> u" for x
+                      (at (x, x) within U \<times> U)" if "x \<in> U" for x
     proof (rule Lim_withinI)
       fix e::real assume "0 < e"
       obtain k1 where "k1>0" and k1: "\<And>x'. norm (x' - x) \<le> k1 \<Longrightarrow> norm (deriv f x' - deriv f x) < e"
-        using \<open>0 < e\<close> continuous_within_E [OF con_derf [OF \<open>x \<in> u\<close>]]
+        using \<open>0 < e\<close> continuous_within_E [OF con_derf [OF \<open>x \<in> U\<close>]]
         by (metis UNIV_I dist_norm)
-      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> u" by (blast intro: openE [OF u] \<open>x \<in> u\<close>)
+      obtain k2 where "k2>0" and k2: "ball x k2 \<subseteq> U" 
+        by (blast intro: openE [OF \<open>open U\<close>] \<open>x \<in> U\<close>)
       have neq: "norm ((f z' - f x') / (z' - x') - deriv f x) \<le> e"
                     if "z' \<noteq> x'" and less_k1: "norm (x'-x, z'-x) < k1" and less_k2: "norm (x'-x, z'-x) < k2"
                  for x' z'
@@ -7273,9 +7290,9 @@
           by (metis (no_types) dist_commute dist_norm norm_fst_le norm_snd_le order_trans)
         have derf_le: "w \<in> closed_segment x' z' \<Longrightarrow> z' \<noteq> x' \<Longrightarrow> cmod (deriv f w - deriv f x) \<le> e" for w
           by (blast intro: cs_less less_k1 k1 [unfolded divide_const_simps dist_norm] less_imp_le le_less_trans)
-        have f_has_der: "\<And>x. x \<in> u \<Longrightarrow> (f has_field_derivative deriv f x) (at x within u)"
-          by (metis DERIV_deriv_iff_field_differentiable at_within_open holf holomorphic_on_def u)
-        have "closed_segment x' z' \<subseteq> u"
+        have f_has_der: "\<And>x. x \<in> U \<Longrightarrow> (f has_field_derivative deriv f x) (at x within U)"
+          by (metis DERIV_deriv_iff_field_differentiable at_within_open holf holomorphic_on_def \<open>open U\<close>)
+        have "closed_segment x' z' \<subseteq> U"
           by (rule order_trans [OF _ k2]) (simp add: cs_less  le_less_trans [OF _ less_k2] dist_complex_def norm_minus_commute subset_iff)
         then have cint_derf: "(deriv f has_contour_integral f z' - f x') (linepath x' z')"
           using contour_integral_primitive [OF f_has_der valid_path_linepath] pasz  by simp
@@ -7290,7 +7307,7 @@
         also have "\<dots> \<le> e" using \<open>0 < e\<close> by simp
         finally show ?thesis .
       qed
-      show "\<exists>d>0. \<forall>xa\<in>u \<times> u.
+      show "\<exists>d>0. \<forall>xa\<in>U \<times> U.
                   0 < dist xa (x, x) \<and> dist xa (x, x) < d \<longrightarrow>
                   dist (case xa of (x, y) \<Rightarrow> if y = x then deriv f x else (f y - f x) / (y - x)) (deriv f x) \<le> e"
         apply (rule_tac x="min k1 k2" in exI)
@@ -7299,49 +7316,51 @@
         done
     qed
     have con_pa_f: "continuous_on (path_image \<gamma>) f"
-      by (meson holf holomorphic_on_imp_continuous_on holomorphic_on_subset interior_subset subt t)
-    have le_B: "\<And>t. t \<in> {0..1} \<Longrightarrow> cmod (vector_derivative \<gamma> (at t)) \<le> B"
+      by (meson holf holomorphic_on_imp_continuous_on holomorphic_on_subset interior_subset subt T)
+    have le_B: "\<And>T. T \<in> {0..1} \<Longrightarrow> cmod (vector_derivative \<gamma> (at T)) \<le> B"
       apply (rule B)
       using \<gamma>' using path_image_def vector_derivative_at by fastforce
     have f_has_cint: "\<And>w. w \<in> v - path_image \<gamma> \<Longrightarrow> ((\<lambda>u. f u / (u - w) ^ 1) has_contour_integral h w) \<gamma>"
       by (simp add: V)
-    have cond_uu: "continuous_on (u \<times> u) (\<lambda>(x,y). d x y)"
+    have cond_uu: "continuous_on (U \<times> U) (\<lambda>(x,y). d x y)"
       apply (simp add: continuous_on_eq_continuous_within d_def continuous_within tendsto_f')
-      apply (simp add: tendsto_within_open_NO_MATCH open_Times u, clarify)
+      apply (simp add: tendsto_within_open_NO_MATCH open_Times \<open>open U\<close>, clarify)
       apply (rule Lim_transform_within_open [OF _ open_uu_Id, where f = "(\<lambda>(x,y). (f y - f x) / (y - x))"])
       using con_ff
       apply (auto simp: continuous_within)
       done
-    have hol_dw: "(\<lambda>z. d z w) holomorphic_on u" if "w \<in> u" for w
+    have hol_dw: "(\<lambda>z. d z w) holomorphic_on U" if "w \<in> U" for w
     proof -
-      have "continuous_on u ((\<lambda>(x,y). d x y) \<circ> (\<lambda>z. (w,z)))"
+      have "continuous_on U ((\<lambda>(x,y). d x y) \<circ> (\<lambda>z. (w,z)))"
         by (rule continuous_on_compose continuous_intros continuous_on_subset [OF cond_uu] | force intro: that)+
-      then have *: "continuous_on u (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
+      then have *: "continuous_on U (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z))"
         by (rule rev_iffD1 [OF _ continuous_on_cong [OF refl]]) (simp add: d_def field_simps)
-      have **: "\<And>x. \<lbrakk>x \<in> u; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) field_differentiable at x"
+      have **: "\<And>x. \<lbrakk>x \<in> U; x \<noteq> w\<rbrakk> \<Longrightarrow> (\<lambda>z. if w = z then deriv f z else (f w - f z) / (w - z)) field_differentiable at x"
         apply (rule_tac f = "\<lambda>x. (f w - f x)/(w - x)" and d = "dist x w" in field_differentiable_transform_within)
-        apply (rule u derivative_intros holomorphic_on_imp_differentiable_at [OF holf] | force simp: dist_commute)+
+        apply (rule \<open>open U\<close> derivative_intros holomorphic_on_imp_differentiable_at [OF holf] | force simp: dist_commute)+
         done
       show ?thesis
         unfolding d_def
-        apply (rule no_isolated_singularity [OF * _ u, where K = "{w}"])
-        apply (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff u **)
+        apply (rule no_isolated_singularity [OF * _ \<open>open U\<close>, where K = "{w}"])
+        apply (auto simp: field_differentiable_def [symmetric] holomorphic_on_open open_Diff \<open>open U\<close> **)
         done
     qed
     { fix a b
-      assume abu: "closed_segment a b \<subseteq> u"
-      then have "\<And>w. w \<in> u \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
+      assume abu: "closed_segment a b \<subseteq> U"
+      then have "\<And>w. w \<in> U \<Longrightarrow> (\<lambda>z. d z w) contour_integrable_on (linepath a b)"
         by (metis hol_dw continuous_on_subset contour_integrable_continuous_linepath holomorphic_on_imp_continuous_on)
-      then have cont_cint_d: "continuous_on u (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
-        apply (rule contour_integral_continuous_on_linepath_2D [OF \<open>open u\<close> _ _ abu])
+      then have cont_cint_d: "continuous_on U (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
+        apply (rule contour_integral_continuous_on_linepath_2D [OF \<open>open U\<close> _ _ abu])
         apply (auto intro: continuous_on_swap_args cond_uu)
         done
       have cont_cint_d\<gamma>: "continuous_on {0..1} ((\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w)) \<circ> \<gamma>)"
-        apply (rule continuous_on_compose)
-        using \<open>path \<gamma>\<close> path_def pasz
-        apply (auto intro!: continuous_on_subset [OF cont_cint_d])
-        apply (force simp: path_image_def)
-        done
+      proof (rule continuous_on_compose)
+        show "continuous_on {0..1} \<gamma>"
+          using \<open>path \<gamma>\<close> path_def by blast
+        show "continuous_on (\<gamma> ` {0..1}) (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))"
+          using pasz unfolding path_image_def
+          by (auto intro!: continuous_on_subset [OF cont_cint_d])
+      qed
       have cint_cint: "(\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w)) contour_integrable_on \<gamma>"
         apply (simp add: contour_integrable_on)
         apply (rule integrable_continuous_real)
@@ -7361,13 +7380,13 @@
                     contour_integral \<gamma> (\<lambda>w. contour_integral (linepath a b) (\<lambda>z. d z w))" .
       note cint_cint cint_h_eq
     } note cint_h = this
-    have conthu: "continuous_on u h"
+    have conthu: "continuous_on U h"
     proof (simp add: continuous_on_sequentially, clarify)
       fix a x
-      assume x: "x \<in> u" and au: "\<forall>n. a n \<in> u" and ax: "a \<longlonglongrightarrow> x"
+      assume x: "x \<in> U" and au: "\<forall>n. a n \<in> U" and ax: "a \<longlonglongrightarrow> x"
       then have A1: "\<forall>\<^sub>F n in sequentially. d (a n) contour_integrable_on \<gamma>"
         by (meson U contour_integrable_on_def eventuallyI)
-      obtain dd where "dd>0" and dd: "cball x dd \<subseteq> u" using open_contains_cball u x by force
+      obtain dd where "dd>0" and dd: "cball x dd \<subseteq> U" using open_contains_cball \<open>open U\<close> x by force
       have A2: "uniform_limit (path_image \<gamma>) (\<lambda>n. d (a n)) (d x) sequentially"
         unfolding uniform_limit_iff dist_norm
       proof clarify
@@ -7382,10 +7401,9 @@
              apply (auto simp: compact_Times compact_valid_path_image simp del: mem_cball)
             done
           then obtain kk where "kk>0"
-            and kk: "\<And>x x'. \<lbrakk>x\<in>?ddpa; x'\<in>?ddpa; dist x' x < kk\<rbrakk> \<Longrightarrow>
+            and kk: "\<And>x x'. \<lbrakk>x \<in> ?ddpa; x' \<in> ?ddpa; dist x' x < kk\<rbrakk> \<Longrightarrow>
                              dist ((\<lambda>(x,y). d x y) x') ((\<lambda>(x,y). d x y) x) < ee"
-            apply (rule uniformly_continuous_onE [where e = ee])
-            using \<open>0 < ee\<close> by auto
+            by (rule uniformly_continuous_onE [where e = ee]) (use \<open>0 < ee\<close> in auto)
           have kk: "\<lbrakk>norm (w - x) \<le> dd; z \<in> path_image \<gamma>; norm ((w, z) - (x, z)) < kk\<rbrakk> \<Longrightarrow> norm (d w z - d x z) < ee"
             for  w z
             using \<open>dd>0\<close> kk [of "(x,z)" "(w,z)"] by (force simp: norm_minus_commute dist_norm)
@@ -7397,35 +7415,34 @@
             done
         qed
       qed
-      have tendsto_hx: "(\<lambda>n. contour_integral \<gamma> (d (a n))) \<longlonglongrightarrow> h x"
-        apply (simp add: contour_integral_unique [OF U, symmetric] x)
-        apply (rule contour_integral_uniform_limit [OF A1 A2 le_B])
-        apply (auto simp: \<open>valid_path \<gamma>\<close>)
-        done
+      have "(\<lambda>n. contour_integral \<gamma> (d (a n))) \<longlonglongrightarrow> contour_integral \<gamma> (d x)"
+        by (rule contour_integral_uniform_limit [OF A1 A2 le_B]) (auto simp: \<open>valid_path \<gamma>\<close>)
+      then have tendsto_hx: "(\<lambda>n. contour_integral \<gamma> (d (a n))) \<longlonglongrightarrow> h x"
+        by (simp add: h_def x)
       then show "(h \<circ> a) \<longlonglongrightarrow> h x"
         by (simp add: h_def x au o_def)
     qed
     show ?thesis
     proof (simp add: holomorphic_on_open field_differentiable_def [symmetric], clarify)
       fix z0
-      consider "z0 \<in> v" | "z0 \<in> u" using uv_Un by blast
+      consider "z0 \<in> v" | "z0 \<in> U" using uv_Un by blast
       then show "h field_differentiable at z0"
       proof cases
         assume "z0 \<in> v" then show ?thesis
           using Cauchy_next_derivative [OF con_pa_f le_B f_has_cint _ ov] V f_has_cint \<open>valid_path \<gamma>\<close>
           by (auto simp: field_differentiable_def v_def)
       next
-        assume "z0 \<in> u" then
-        obtain e where "e>0" and e: "ball z0 e \<subseteq> u" by (blast intro: openE [OF u])
+        assume "z0 \<in> U" then
+        obtain e where "e>0" and e: "ball z0 e \<subseteq> U" by (blast intro: openE [OF \<open>open U\<close>])
         have *: "contour_integral (linepath a b) h + contour_integral (linepath b c) h + contour_integral (linepath c a) h = 0"
                 if abc_subset: "convex hull {a, b, c} \<subseteq> ball z0 e"  for a b c
         proof -
-          have *: "\<And>x1 x2 z. z \<in> u \<Longrightarrow> closed_segment x1 x2 \<subseteq> u \<Longrightarrow> (\<lambda>w. d w z) contour_integrable_on linepath x1 x2"
-            using  hol_dw holomorphic_on_imp_continuous_on u
+          have *: "\<And>x1 x2 z. z \<in> U \<Longrightarrow> closed_segment x1 x2 \<subseteq> U \<Longrightarrow> (\<lambda>w. d w z) contour_integrable_on linepath x1 x2"
+            using  hol_dw holomorphic_on_imp_continuous_on \<open>open U\<close>
             by (auto intro!: contour_integrable_holomorphic_simple)
-          have abc: "closed_segment a b \<subseteq> u"  "closed_segment b c \<subseteq> u"  "closed_segment c a \<subseteq> u"
+          have abc: "closed_segment a b \<subseteq> U"  "closed_segment b c \<subseteq> U"  "closed_segment c a \<subseteq> U"
             using that e segments_subset_convex_hull by fastforce+
-          have eq0: "\<And>w. w \<in> u \<Longrightarrow> contour_integral (linepath a b +++ linepath b c +++ linepath c a) (\<lambda>z. d z w) = 0"
+          have eq0: "\<And>w. w \<in> U \<Longrightarrow> contour_integral (linepath a b +++ linepath b c +++ linepath c a) (\<lambda>z. d z w) = 0"
             apply (rule contour_integral_unique [OF Cauchy_theorem_triangle])
             apply (rule holomorphic_on_subset [OF hol_dw])
             using e abc_subset by auto
@@ -7434,7 +7451,7 @@
                         (contour_integral (linepath b c) (\<lambda>z. d z x) +
                          contour_integral (linepath c a) (\<lambda>z. d z x)))  =  0"
             apply (rule contour_integral_eq_0)
-            using abc pasz u
+            using abc pasz U
             apply (subst contour_integral_join [symmetric], auto intro: eq0 *)+
             done
           then show ?thesis
@@ -7540,13 +7557,12 @@
            "path_image g \<subseteq> S" "pathfinish g = pathstart g" "z \<notin> S"
     shows "winding_number g z = 0"
 proof -
-  have "winding_number g z = winding_number(linepath (pathstart g) (pathstart g)) z"
-    apply (rule winding_number_homotopic_paths)
-    apply (rule homotopic_loops_imp_homotopic_paths_null [where a = "pathstart g"])
-    apply (rule homotopic_loops_subset [of S])
-    using assms
-    apply (auto simp: homotopic_paths_imp_homotopic_loops path_defs simply_connected_eq_contractible_path)
-    done
+  have hom: "homotopic_loops S g (linepath (pathstart g) (pathstart g))"
+    by (meson assms homotopic_paths_imp_homotopic_loops pathfinish_linepath simply_connected_eq_contractible_path)
+  then have "homotopic_paths (- {z}) g (linepath (pathstart g) (pathstart g))"
+    by (meson \<open>z \<notin> S\<close> homotopic_loops_imp_homotopic_paths_null homotopic_paths_subset subset_Compl_singleton)
+  then have "winding_number g z = winding_number(linepath (pathstart g) (pathstart g)) z"
+    by (rule winding_number_homotopic_paths)
   also have "\<dots> = 0"
     using assms by (force intro: winding_number_trivial)
   finally show ?thesis .
@@ -7562,7 +7578,7 @@
                          homotopic_paths_imp_homotopic_loops)
 using valid_path_imp_path by blast
 
-lemma holomorphic_logarithm_exists:
+proposition holomorphic_logarithm_exists:
   assumes A: "convex A" "open A" 
       and f: "f holomorphic_on A" "\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> 0"
       and z0: "z0 \<in> A"
@@ -7586,7 +7602,6 @@
     from 2 and z0 and f show ?case
       by (auto simp: h_def exp_diff field_simps intro!: derivative_eq_intros g f')
   qed fact+
-
   then obtain c where c: "\<And>x. x \<in> A \<Longrightarrow> f x / exp (h x) - 1 = c"
     by blast
   from c[OF z0] and z0 and f have "c = 0"
diff -r e0b5f2d14bf9 -r f75d765a281f src/HOL/Data_Structures/AVL_Map.thy
--- a/src/HOL/Data_Structures/AVL_Map.thy	Mon Jun 11 16:23:21 2018 +0100
+++ b/src/HOL/Data_Structures/AVL_Map.thy	Tue Jun 12 11:18:35 2018 +0100
@@ -23,7 +23,7 @@
    GT \<Rightarrow> balL l (a,b) (delete x r))"
 
 
-subsection \<open>Functional Correctness Proofs\<close>
+subsection \<open>Functional Correctness\<close>
 
 theorem inorder_update:
   "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
@@ -36,9 +36,153 @@
   (auto simp: del_list_simps inorder_balL inorder_balR
      inorder_del_root inorder_split_maxD split: prod.splits)
 
+
+subsection \<open>AVL invariants\<close>
+
+
+subsubsection \<open>Insertion maintains AVL balance\<close>
+
+theorem avl_update:
+  assumes "avl t"
+  shows "avl(update x y t)"
+        "(height (update x y t) = height t \<or> height (update x y t) = height t + 1)"
+using assms
+proof (induction x y t rule: update.induct)
+  case eq2: (2 x y l a b h r)
+  case 1
+  show ?case
+  proof(cases "x = a")
+    case True with eq2 1 show ?thesis by simp
+  next
+    case False
+    with eq2 1 show ?thesis 
+    proof(cases "x<a")
+      case True with eq2 1 show ?thesis by (auto simp add:avl_balL)
+    next
+      case False with eq2 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
+    qed
+  qed
+  case 2
+  show ?case
+  proof(cases "x = a")
+    case True with eq2 1 show ?thesis by simp
+  next
+    case False
+    show ?thesis 
+    proof(cases "x<a")
+      case True
+      show ?thesis
+      proof(cases "height (update x y l) = height r + 2")
+        case False with eq2 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
+      next
+        case True 
+        hence "(height (balL (update x y l) (a,b) r) = height r + 2) \<or>
+          (height (balL (update x y l) (a,b) r) = height r + 3)" (is "?A \<or> ?B")
+          using eq2 2 \<open>x<a\<close> by (intro height_balL) simp_all
+        thus ?thesis
+        proof
+          assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
+        next
+          assume ?B with True 1 eq2(2) \<open>x < a\<close> show ?thesis by (simp) arith
+        qed
+      qed
+    next
+      case False
+      show ?thesis
+      proof(cases "height (update x y r) = height l + 2")
+        case False with eq2 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
+      next
+        case True 
+        hence "(height (balR l (a,b) (update x y r)) = height l + 2) \<or>
+          (height (balR l (a,b) (update x y r)) = height l + 3)"  (is "?A \<or> ?B")
+          using eq2 2 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by (intro height_balR) simp_all
+        thus ?thesis 
+        proof
+          assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
+        next
+          assume ?B with True 1 eq2(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
+        qed
+      qed
+    qed
+  qed
+qed simp_all
+
+
+subsubsection \<open>Deletion maintains AVL balance\<close>
+
+theorem avl_delete:
+  assumes "avl t" 
+  shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
+using assms
+proof (induct t)
+  case (Node l n h r)
+  obtain a b where [simp]: "n = (a,b)" by fastforce
+  case 1
+  show ?case
+  proof(cases "x = a")
+    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
+  next
+    case False
+    show ?thesis 
+    proof(cases "x<a")
+      case True with Node 1 show ?thesis by (auto simp add:avl_balR)
+    next
+      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balL)
+    qed
+  qed
+  case 2
+  show ?case
+  proof(cases "x = a")
+    case True
+    with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
+      \<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1"
+      by (subst height_del_root,simp_all)
+    with True show ?thesis by simp
+  next
+    case False
+    show ?thesis 
+    proof(cases "x<a")
+      case True
+      show ?thesis
+      proof(cases "height r = height (delete x l) + 2")
+        case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def)
+      next
+        case True 
+        hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or>
+          height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B")
+          using Node 2 by (intro height_balR) auto
+        thus ?thesis 
+        proof
+          assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def)
+        next
+          assume ?B with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def)
+        qed
+      qed
+    next
+      case False
+      show ?thesis
+      proof(cases "height l = height (delete x r) + 2")
+        case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def)
+      next
+        case True 
+        hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or>
+          height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B")
+          using Node 2 by (intro height_balL) auto
+        thus ?thesis 
+        proof
+          assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def)
+        next
+          assume ?B with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def)
+        qed
+      qed
+    qed
+  qed
+qed simp_all
+
+
 interpretation Map_by_Ordered
 where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and inv = "\<lambda>_. True"
+and inorder = inorder and inv = avl
 proof (standard, goal_cases)
   case 1 show ?case by simp
 next
@@ -47,6 +191,12 @@
   case 3 thus ?case by(simp add: inorder_update)
 next
   case 4 thus ?case by(simp add: inorder_delete)
-qed auto
+next
+  case 5 show ?case by simp
+next
+  case 6 thus ?case by(simp add: avl_update(1))
+next
+  case 7 thus ?case by(simp add: avl_delete(1))
+qed
 
 end
diff -r e0b5f2d14bf9 -r f75d765a281f src/HOL/Data_Structures/AVL_Set.thy
--- a/src/HOL/Data_Structures/AVL_Set.thy	Mon Jun 11 16:23:21 2018 +0100
+++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue Jun 12 11:18:35 2018 +0100
@@ -121,22 +121,6 @@
     inorder_del_root inorder_split_maxD split: prod.splits)
 
 
-subsubsection "Overall functional correctness"
-
-interpretation Set_by_Ordered
-where empty = Leaf and isin = isin and insert = insert and delete = delete
-and inorder = inorder and inv = "\<lambda>_. True"
-proof (standard, goal_cases)
-  case 1 show ?case by simp
-next
-  case 2 thus ?case by(simp add: isin_set_inorder)
-next
-  case 3 thus ?case by(simp add: inorder_insert)
-next
-  case 4 thus ?case by(simp add: inorder_delete)
-qed (rule TrueI)+
-
-
 subsection \<open>AVL invariants\<close>
 
 text\<open>Essentially the AFP/AVL proofs\<close>
@@ -224,7 +208,7 @@
 
 text\<open>Insertion maintains the AVL property:\<close>
 
-theorem avl_insert_aux:
+theorem avl_insert:
   assumes "avl t"
   shows "avl(insert x t)"
         "(height (insert x t) = height t \<or> height (insert x t) = height t + 1)"
@@ -232,32 +216,28 @@
 proof (induction t)
   case (Node l a h r)
   case 1
-  with Node show ?case
+  show ?case
   proof(cases "x = a")
-    case True
-    with Node 1 show ?thesis by simp
+    case True with Node 1 show ?thesis by simp
   next
     case False
-    with Node 1 show ?thesis 
+    show ?thesis 
     proof(cases "x<a")
-      case True
-      with Node 1 show ?thesis by (auto simp add:avl_balL)
+      case True with Node 1 show ?thesis by (auto simp add:avl_balL)
     next
-      case False
-      with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
+      case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR)
     qed
   qed
   case 2
-  from 2 Node show ?case
+  show ?case
   proof(cases "x = a")
-    case True
-    with Node 1 show ?thesis by simp
+    case True with Node 1 show ?thesis by simp
   next
     case False
-    with Node 1 show ?thesis 
-     proof(cases "x<a")
+    show ?thesis 
+    proof(cases "x<a")
       case True
-      with Node 2 show ?thesis
+      show ?thesis
       proof(cases "height (insert x l) = height r + 2")
         case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2)
       next
@@ -267,19 +247,16 @@
           using Node 2 by (intro height_balL) simp_all
         thus ?thesis
         proof
-          assume ?A
-          with 2 \<open>x < a\<close> show ?thesis by (auto)
+          assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto)
         next
-          assume ?B
-          with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
+          assume ?B with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith
         qed
       qed
     next
       case False
-      with Node 2 show ?thesis 
+      show ?thesis 
       proof(cases "height (insert x r) = height l + 2")
-        case False
-        with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
+        case False with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2)
       next
         case True 
         hence "(height (balR l a (insert x r)) = height l + 2) \<or>
@@ -287,11 +264,9 @@
           using Node 2 by (intro height_balR) simp_all
         thus ?thesis 
         proof
-          assume ?A
-          with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
+          assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto)
         next
-          assume ?B
-          with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
+          assume ?B with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith
         qed
       qed
     qed
@@ -310,9 +285,7 @@
   case (Node l a h r)
   case 1
   thus ?case using Node
-    by (auto simp: height_balL height_balL2 avl_balL
-      linorder_class.max.absorb1 linorder_class.max.absorb2
-      split:prod.split)
+    by (auto simp: height_balL height_balL2 avl_balL split:prod.split)
 next
   case (Node l a h r)
   case 2
@@ -360,16 +333,15 @@
   have "height t = height ?t' \<or> height t = height ?t' + 1" using  \<open>avl t\<close> Node_Node
   proof(cases "height ?r = height ?l' + 2")
     case False
-    show ?thesis using l'_height t_height False by (subst  height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
+    show ?thesis using l'_height t_height False
+      by (subst height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith
   next
     case True
     show ?thesis
     proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (split_max ?l)"]])
-      case 1
-      thus ?thesis using l'_height t_height True by arith
+      case 1 thus ?thesis using l'_height t_height True by arith
     next
-      case 2
-      thus ?thesis using l'_height t_height True by arith
+      case 2 thus ?thesis using l'_height t_height True by arith
     qed
   qed
   thus ?thesis using Node_Node by (auto split:prod.splits)
@@ -377,30 +349,27 @@
 
 text\<open>Deletion maintains the AVL property:\<close>
 
-theorem avl_delete_aux:
+theorem avl_delete:
   assumes "avl t" 
   shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1"
 using assms
 proof (induct t)
   case (Node l n h r)
   case 1
-  with Node show ?case
+  show ?case
   proof(cases "x = n")
-    case True
-    with Node 1 show ?thesis by (auto simp:avl_del_root)
+    case True with Node 1 show ?thesis by (auto simp:avl_del_root)
   next
     case False
-    with Node 1 show ?thesis 
+    show ?thesis 
     proof(cases "x<n")
-      case True
-      with Node 1 show ?thesis by (auto simp add:avl_balR)
+      case True with Node 1 show ?thesis by (auto simp add:avl_balR)
     next
-      case False
-      with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
+      case False with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL)
     qed
   qed
   case 2
-  with Node show ?case
+  show ?case
   proof(cases "x = n")
     case True
     with 1 have "height (Node l n h r) = height(del_root (Node l n h r))
@@ -409,8 +378,8 @@
     with True show ?thesis by simp
   next
     case False
-    with Node 1 show ?thesis 
-     proof(cases "x<n")
+    show ?thesis 
+    proof(cases "x<n")
       case True
       show ?thesis
       proof(cases "height r = height (delete x l) + 2")
@@ -422,11 +391,9 @@
           using Node 2 by (intro height_balR) auto
         thus ?thesis 
         proof
-          assume ?A
-          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
+          assume ?A with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
         next
-          assume ?B
-          with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
+          assume ?B with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def)
         qed
       qed
     next
@@ -441,11 +408,9 @@
           using Node 2 by (intro height_balL) auto
         thus ?thesis 
         proof
-          assume ?A
-          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
+          assume ?A with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
         next
-          assume ?B
-          with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
+          assume ?B with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def)
         qed
       qed
     qed
@@ -453,6 +418,28 @@
 qed simp_all
 
 
+subsection "Overall correctness"
+
+interpretation Set_by_Ordered
+where empty = Leaf and isin = isin and insert = insert and delete = delete
+and inorder = inorder and inv = avl
+proof (standard, goal_cases)
+  case 1 show ?case by simp
+next
+  case 2 thus ?case by(simp add: isin_set_inorder)
+next
+  case 3 thus ?case by(simp add: inorder_insert)
+next
+  case 4 thus ?case by(simp add: inorder_delete)
+next
+  case 5 thus ?case by simp
+next
+  case 6 thus ?case by (simp add: avl_insert(1))
+next
+  case 7 thus ?case by (simp add: avl_delete(1))
+qed
+
+
 subsection \<open>Height-Size Relation\<close>
 
 text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
diff -r e0b5f2d14bf9 -r f75d765a281f src/HOL/Data_Structures/RBT_Map.thy
--- a/src/HOL/Data_Structures/RBT_Map.thy	Mon Jun 11 16:23:21 2018 +0100
+++ b/src/HOL/Data_Structures/RBT_Map.thy	Tue Jun 12 11:18:35 2018 +0100
@@ -22,19 +22,14 @@
 definition update :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
 "update x y t = paint Black (upd x y t)"
 
-fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
-and delL :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
-and delR :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> 'a*'b \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt"
-where
+fun del :: "'a::linorder \<Rightarrow> ('a*'b)rbt \<Rightarrow> ('a*'b)rbt" where
 "del x Leaf = Leaf" |
-"del x (Node t1 (a,b) c t2) = (case cmp x a of
-  LT \<Rightarrow> delL x t1 (a,b) t2 |
-  GT \<Rightarrow> delR x t1 (a,b) t2 |
-  EQ \<Rightarrow> combine t1 t2)" |
-"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" |
-"delL x t1 a t2 = R (del x t1) a t2" |
-"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" | 
-"delR x t1 a t2 = R t1 a (del x t2)"
+"del x (Node l (a,b) c r) = (case cmp x a of
+     LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
+           then baldL (del x l) (a,b) r else R (del x l) (a,b) r |
+     GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black
+           then baldR l (a,b) (del x r) else R l (a,b) (del x r) |
+  EQ \<Rightarrow> combine l r)"
 
 definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
 "delete x t = paint Black (del x t)"
@@ -52,21 +47,66 @@
 by(simp add: update_def inorder_upd inorder_paint)
 
 lemma inorder_del:
- "sorted1(inorder t1) \<Longrightarrow>  inorder(del x t1) = del_list x (inorder t1)" and
- "sorted1(inorder t1) \<Longrightarrow>  inorder(delL x t1 a t2) =
-    del_list x (inorder t1) @ a # inorder t2" and
- "sorted1(inorder t2) \<Longrightarrow>  inorder(delR x t1 a t2) =
-    inorder t1 @ a # del_list x (inorder t2)"
-by(induction x t1 and x t1 a t2 and x t1 a t2 rule: del_delL_delR.induct)
+ "sorted1(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
+by(induction x t rule: del.induct)
   (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
 
 lemma inorder_delete:
   "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
 by(simp add: delete_def inorder_del inorder_paint)
 
+
+subsection \<open>Structural invariants\<close>
+
+subsubsection \<open>Update\<close>
+
+lemma invc_upd: assumes "invc t"
+  shows "color t = Black \<Longrightarrow> invc (upd x y t)" "invc2 (upd x y t)"
+using assms
+by (induct x y t rule: upd.induct) (auto simp: invc_baliL invc_baliR invc2I)
+
+lemma invh_upd: assumes "invh t"
+  shows "invh (upd x y t)" "bheight (upd x y t) = bheight t"
+using assms
+by(induct x y t rule: upd.induct)
+  (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
+
+theorem rbt_update: "rbt t \<Longrightarrow> rbt (update x y t)"
+by (simp add: invc_upd(2) invh_upd(1) color_paint_Black invc_paint_Black invh_paint
+  rbt_def update_def)
+
+
+subsubsection \<open>Deletion\<close>
+
+lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and>
+   (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
+    color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
+proof (induct x t rule: del.induct)
+case (2 x _ y _ c)
+  have "x = y \<or> x < y \<or> x > y" by auto
+  thus ?case proof (elim disjE)
+    assume "x = y"
+    with 2 show ?thesis
+    by (cases c) (simp_all add: invh_combine invc_combine)
+  next
+    assume "x < y"
+    with 2 show ?thesis
+      by(cases c)
+        (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD)
+  next
+    assume "y < x"
+    with 2 show ?thesis
+      by(cases c)
+        (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD)
+  qed
+qed auto
+
+theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
+by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
+
 interpretation Map_by_Ordered
 where empty = Leaf and lookup = lookup and update = update and delete = delete
-and inorder = inorder and inv = "\<lambda>_. True"
+and inorder = inorder and inv = rbt
 proof (standard, goal_cases)
   case 1 show ?case by simp
 next
@@ -75,6 +115,12 @@
   case 3 thus ?case by(simp add: inorder_update)
 next
   case 4 thus ?case by(simp add: inorder_delete)
-qed auto
+next
+  case 5 thus ?case by (simp add: rbt_Leaf) 
+next
+  case 6 thus ?case by (simp add: rbt_update) 
+next
+  case 7 thus ?case by (simp add: rbt_delete) 
+qed
 
 end
diff -r e0b5f2d14bf9 -r f75d765a281f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Jun 11 16:23:21 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Jun 12 11:18:35 2018 +0100
@@ -539,6 +539,7 @@
     def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body
     def messages: List[(XML.Tree, Position.T)]
     def exports: List[Export.Entry]
+    def exports_map: Map[String, Export.Entry]
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)]
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
@@ -1030,7 +1031,7 @@
         def markup_to_XML(range: Text.Range, elements: Markup.Elements): XML.Body =
           state.markup_to_XML(version, node_name, range, elements)
 
-        def messages: List[(XML.Tree, Position.T)] =
+        lazy val messages: List[(XML.Tree, Position.T)] =
           (for {
             (command, start) <-
               Document.Node.Commands.starts_pos(
@@ -1039,13 +1040,16 @@
             (_, tree) <- state.command_results(version, command).iterator
            } yield (tree, pos)).toList
 
-        def exports: List[Export.Entry] =
+        lazy val exports: List[Export.Entry] =
           Command.Exports.merge(
             for {
               command <- node.commands.iterator
               st <- state.command_states(version, command).iterator
             } yield st.exports).iterator.map(_._2).toList
 
+        lazy val exports_map: Map[String, Export.Entry] =
+          (for (entry <- exports.iterator) yield (entry.name, entry)).toMap
+
 
         /* find command */
 
diff -r e0b5f2d14bf9 -r f75d765a281f src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon Jun 11 16:23:21 2018 +0100
+++ b/src/Pure/Thy/export.scala	Tue Jun 12 11:18:35 2018 +0100
@@ -185,6 +185,35 @@
   }
 
 
+  /* abstract provider */
+
+  object Provider
+  {
+    def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
+      new Provider {
+        def apply(export_name: String): Option[Entry] =
+          read_entry(db, session_name, theory_name, export_name)
+      }
+
+    def snapshot(snapshot: Document.Snapshot): Provider =
+      new Provider {
+        def apply(export_name: String): Option[Entry] =
+          snapshot.exports_map.get(export_name)
+      }
+  }
+
+  trait Provider
+  {
+    def apply(export_name: String): Option[Entry]
+
+    def uncompressed_yxml(export_name: String, cache: XZ.Cache = XZ.cache()): XML.Body =
+      apply(export_name) match {
+        case Some(entry) => entry.uncompressed_yxml(cache = cache)
+        case None => Nil
+      }
+  }
+
+
   /* export to file-system */
 
   def export_files(
diff -r e0b5f2d14bf9 -r f75d765a281f src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Mon Jun 11 16:23:21 2018 +0100
+++ b/src/Pure/Thy/export_theory.scala	Tue Jun 12 11:18:35 2018 +0100
@@ -40,7 +40,8 @@
       {
         db.transaction {
           Export.read_theory_names(db, session_name).map((theory_name: String) =>
-            read_theory(db, session_name, theory_name, types = types, consts = consts,
+            read_theory(Export.Provider.database(db, session_name, theory_name),
+              session_name, theory_name, types = types, consts = consts,
               axioms = axioms, facts = facts, classes = classes, typedefs = typedefs,
               cache = Some(cache)))
         }
@@ -90,7 +91,7 @@
   def empty_theory(name: String): Theory =
     Theory(name, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil)
 
-  def read_theory(db: SQL.Database, session_name: String, theory_name: String,
+  def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
     types: Boolean = true,
     consts: Boolean = true,
     axioms: Boolean = true,
@@ -102,7 +103,7 @@
     cache: Option[Term.Cache] = None): Theory =
   {
     val parents =
-      Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
+      provider(export_prefix + "parents") match {
         case Some(entry) => split_lines(entry.uncompressed().text)
         case None =>
           error("Missing theory export in session " + quote(session_name) + ": " +
@@ -110,14 +111,14 @@
       }
     val theory =
       Theory(theory_name, parents,
-        if (types) read_types(db, session_name, theory_name) else Nil,
-        if (consts) read_consts(db, session_name, theory_name) else Nil,
-        if (axioms) read_axioms(db, session_name, theory_name) else Nil,
-        if (facts) read_facts(db, session_name, theory_name) else Nil,
-        if (classes) read_classes(db, session_name, theory_name) else Nil,
-        if (typedefs) read_typedefs(db, session_name, theory_name) else Nil,
-        if (classrel) read_classrel(db, session_name, theory_name) else Nil,
-        if (arities) read_arities(db, session_name, theory_name) else Nil)
+        if (types) read_types(provider) else Nil,
+        if (consts) read_consts(provider) else Nil,
+        if (axioms) read_axioms(provider) else Nil,
+        if (facts) read_facts(provider) else Nil,
+        if (classes) read_classes(provider) else Nil,
+        if (typedefs) read_typedefs(provider) else Nil,
+        if (classrel) read_classrel(provider) else Nil,
+        if (arities) read_arities(provider) else Nil)
     if (cache.isDefined) theory.cache(cache.get) else theory
   }
 
@@ -146,22 +147,6 @@
     }
   }
 
-  def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
-    export_name: String, decode: XML.Body => List[A]): List[A] =
-  {
-    Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
-      case Some(entry) => decode(entry.uncompressed_yxml())
-      case None => Nil
-    }
-  }
-
-  def read_entities[A](db: SQL.Database, session_name: String, theory_name: String,
-    export_name: String, decode: XML.Tree => A): List[A] =
-  {
-    read_export(db, session_name, theory_name, export_name,
-      (body: XML.Body) => body.map(decode(_)))
-  }
-
 
   /* types */
 
@@ -173,18 +158,17 @@
         abbrev.map(cache.typ(_)))
   }
 
-  def read_types(db: SQL.Database, session_name: String, theory_name: String): List[Type] =
-    read_entities(db, session_name, theory_name, "types",
-      (tree: XML.Tree) =>
+  def read_types(provider: Export.Provider): List[Type] =
+    provider.uncompressed_yxml(export_prefix + "types").map((tree: XML.Tree) =>
+      {
+        val (entity, body) = decode_entity(tree)
+        val (args, abbrev) =
         {
-          val (entity, body) = decode_entity(tree)
-          val (args, abbrev) =
-          {
-            import XML.Decode._
-            pair(list(string), option(Term_XML.Decode.typ))(body)
-          }
-          Type(entity, args, abbrev)
-        })
+          import XML.Decode._
+          pair(list(string), option(Term_XML.Decode.typ))(body)
+        }
+        Type(entity, args, abbrev)
+      })
 
 
   /* consts */
@@ -199,18 +183,17 @@
         abbrev.map(cache.term(_)))
   }
 
-  def read_consts(db: SQL.Database, session_name: String, theory_name: String): List[Const] =
-    read_entities(db, session_name, theory_name, "consts",
-      (tree: XML.Tree) =>
+  def read_consts(provider: Export.Provider): List[Const] =
+    provider.uncompressed_yxml(export_prefix + "consts").map((tree: XML.Tree) =>
+      {
+        val (entity, body) = decode_entity(tree)
+        val (args, typ, abbrev) =
         {
-          val (entity, body) = decode_entity(tree)
-          val (args, typ, abbrev) =
-          {
-            import XML.Decode._
-            triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
-          }
-          Const(entity, args, typ, abbrev)
-        })
+          import XML.Decode._
+          triple(list(string), Term_XML.Decode.typ, option(Term_XML.Decode.term))(body)
+        }
+        Const(entity, args, typ, abbrev)
+      })
 
 
   /* axioms and facts */
@@ -236,14 +219,13 @@
         cache.term(prop))
   }
 
-  def read_axioms(db: SQL.Database, session_name: String, theory_name: String): List[Axiom] =
-    read_entities(db, session_name, theory_name, "axioms",
-      (tree: XML.Tree) =>
-        {
-          val (entity, body) = decode_entity(tree)
-          val (typargs, args, List(prop)) = decode_props(body)
-          Axiom(entity, typargs, args, prop)
-        })
+  def read_axioms(provider: Export.Provider): List[Axiom] =
+    provider.uncompressed_yxml(export_prefix + "axioms").map((tree: XML.Tree) =>
+      {
+        val (entity, body) = decode_entity(tree)
+        val (typargs, args, List(prop)) = decode_props(body)
+        Axiom(entity, typargs, args, prop)
+      })
 
   sealed case class Fact(
     entity: Entity,
@@ -258,14 +240,13 @@
         props.map(cache.term(_)))
   }
 
-  def read_facts(db: SQL.Database, session_name: String, theory_name: String): List[Fact] =
-    read_entities(db, session_name, theory_name, "facts",
-      (tree: XML.Tree) =>
-        {
-          val (entity, body) = decode_entity(tree)
-          val (typargs, args, props) = decode_props(body)
-          Fact(entity, typargs, args, props)
-        })
+  def read_facts(provider: Export.Provider): List[Fact] =
+    provider.uncompressed_yxml(export_prefix + "facts").map((tree: XML.Tree) =>
+      {
+        val (entity, body) = decode_entity(tree)
+        val (typargs, args, props) = decode_props(body)
+        Fact(entity, typargs, args, props)
+      })
 
 
   /* type classes */
@@ -279,19 +260,18 @@
         axioms.map(cache.term(_)))
   }
 
-  def read_classes(db: SQL.Database, session_name: String, theory_name: String): List[Class] =
-    read_entities(db, session_name, theory_name, "classes",
-      (tree: XML.Tree) =>
+  def read_classes(provider: Export.Provider): List[Class] =
+    provider.uncompressed_yxml(export_prefix + "classes").map((tree: XML.Tree) =>
+      {
+        val (entity, body) = decode_entity(tree)
+        val (params, axioms) =
         {
-          val (entity, body) = decode_entity(tree)
-          val (params, axioms) =
-          {
-            import XML.Decode._
-            import Term_XML.Decode._
-            pair(list(pair(string, typ)), list(term))(body)
-          }
-          Class(entity, params, axioms)
-        })
+          import XML.Decode._
+          import Term_XML.Decode._
+          pair(list(pair(string, typ)), list(term))(body)
+        }
+        Class(entity, params, axioms)
+      })
 
 
   /* sort algebra */
@@ -302,17 +282,16 @@
       Classrel(cache.string(class_name), super_names.map(cache.string(_)))
   }
 
-  def read_classrel(db: SQL.Database, session_name: String, theory_name: String): List[Classrel] =
-    read_export(db, session_name, theory_name, "classrel",
-      (body: XML.Body) =>
-        {
-          val classrel =
-          {
-            import XML.Decode._
-            list(pair(string, list(string)))(body)
-          }
-          for ((c, cs) <- classrel) yield Classrel(c, cs)
-        })
+  def read_classrel(provider: Export.Provider): List[Classrel] =
+  {
+    val body = provider.uncompressed_yxml(export_prefix + "classrel")
+    val classrel =
+    {
+      import XML.Decode._
+      list(pair(string, list(string)))(body)
+    }
+    for ((c, cs) <- classrel) yield Classrel(c, cs)
+  }
 
   sealed case class Arity(type_name: String, domain: List[Term.Sort], codomain: String)
   {
@@ -320,18 +299,17 @@
       Arity(cache.string(type_name), domain.map(cache.sort(_)), cache.string(codomain))
   }
 
-  def read_arities(db: SQL.Database, session_name: String, theory_name: String): List[Arity] =
-    read_export(db, session_name, theory_name, "arities",
-      (body: XML.Body) =>
-        {
-          val arities =
-          {
-            import XML.Decode._
-            import Term_XML.Decode._
-            list(triple(string, list(sort), string))(body)
-          }
-          for ((a, b, c) <- arities) yield Arity(a, b, c)
-        })
+  def read_arities(provider: Export.Provider): List[Arity] =
+  {
+    val body = provider.uncompressed_yxml(export_prefix + "arities")
+    val arities =
+    {
+      import XML.Decode._
+      import Term_XML.Decode._
+      list(triple(string, list(sort), string))(body)
+    }
+    for ((a, b, c) <- arities) yield Arity(a, b, c)
+  }
 
 
   /* HOL typedefs */
@@ -348,17 +326,16 @@
         cache.string(axiom_name))
   }
 
-  def read_typedefs(db: SQL.Database, session_name: String, theory_name: String): List[Typedef] =
-    read_export(db, session_name, theory_name, "typedefs",
-      (body: XML.Body) =>
-        {
-          val typedefs =
-          {
-            import XML.Decode._
-            import Term_XML.Decode._
-            list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
-          }
-          for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
-          yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
-        })
+  def read_typedefs(provider: Export.Provider): List[Typedef] =
+  {
+    val body = provider.uncompressed_yxml(export_prefix + "typedefs")
+    val typedefs =
+    {
+      import XML.Decode._
+      import Term_XML.Decode._
+      list(pair(string, pair(typ, pair(typ, pair(string, pair(string, string))))))(body)
+    }
+    for { (name, (rep_type, (abs_type, (rep_name, (abs_name, axiom_name))))) <- typedefs }
+    yield Typedef(name, rep_type, abs_type, rep_name, abs_name, axiom_name)
+  }
 }
diff -r e0b5f2d14bf9 -r f75d765a281f src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Jun 11 16:23:21 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Tue Jun 12 11:18:35 2018 +0100
@@ -78,6 +78,10 @@
 
   val default_output_dir = Path.explode("dump")
 
+  def make_options(options: Options, aspects: List[Aspect]): Options =
+    (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
+      { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+
   def dump(options: Options, logic: String,
     aspects: List[Aspect] = Nil,
     progress: Progress = No_Progress,
@@ -92,9 +96,7 @@
     if (Build.build_logic(options, logic, progress = progress, dirs = dirs,
       system_mode = system_mode) != 0) error(logic + " FAILED")
 
-    val dump_options =
-      (options.int.update("completion_limit", 0).bool.update("ML_statistics", false) /: aspects)(
-        { case (opts, aspect) => (opts /: aspect.options)(_ + _) })
+    val dump_options = make_options(options, aspects)
 
 
     /* dependencies */