Merge (resolved trivial conflict)
authorpaulson <lp15@cam.ac.uk>
Fri Sep 29 14:17:17 2017 +0100 (19 months ago)
changeset 66709b034d2ae541c
parent 66708 015a95f15040
parent 66707 41bf4d324ac4
child 66710 676258a1cf01
Merge (resolved trivial conflict)
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
     1.1 --- a/Admin/PLATFORMS	Fri Sep 29 14:12:14 2017 +0100
     1.2 +++ b/Admin/PLATFORMS	Fri Sep 29 14:17:17 2017 +0100
     1.3 @@ -41,6 +41,7 @@
     1.4    x86-windows       Windows 7
     1.5    x86_64-windows    Windows 7
     1.6    x86-cygwin        Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86/release)
     1.7 +  x86_64-cygwin     Cygwin 2.8 http://isabelle.in.tum.de/cygwin_2017 (x86_64/release)
     1.8  
     1.9  All of the above platforms are 100% supported by Isabelle -- end-users
    1.10  should not have to care about the differences (at least in theory).
    1.11 @@ -67,7 +68,7 @@
    1.12  help configuring platform-dependent tools:
    1.13  
    1.14    ISABELLE_PLATFORM64  (potentially empty)
    1.15 -  ISABELLE_PLATFORM32
    1.16 +  ISABELLE_PLATFORM32  (potentially empty)
    1.17    ISABELLE_PLATFORM
    1.18  
    1.19  The ISABELLE_PLATFORM setting variable refers to the 32 bit version of
     2.1 --- a/Admin/bash_process/build	Fri Sep 29 14:12:14 2017 +0100
     2.2 +++ b/Admin/bash_process/build	Fri Sep 29 14:17:17 2017 +0100
     2.3 @@ -42,7 +42,7 @@
     2.4    x86-linux | x86-darwin)
     2.5      cc -Wall -m32 bash_process.c -o "$TARGET/bash_process"
     2.6      ;;
     2.7 -  x86-cygwin)
     2.8 +  x86_64-cygwin | x86-cygwin)
     2.9      cc -Wall bash_process.c -o "$TARGET/bash_process.exe"
    2.10      ;;
    2.11    *)
     3.1 --- a/Admin/components/components.sha1	Fri Sep 29 14:12:14 2017 +0100
     3.2 +++ b/Admin/components/components.sha1	Fri Sep 29 14:17:17 2017 +0100
     3.3 @@ -1,6 +1,7 @@
     3.4  fbe83b522cb37748ac1b3c943ad71704fdde2f82  bash_process-1.1.1.tar.gz
     3.5  bb9ef498cd594b4289221b96146d529c899da209  bash_process-1.1.tar.gz
     3.6  81250148f8b89ac3587908fb20645081d7f53207  bash_process-1.2.1.tar.gz
     3.7 +97b2491382130a841b3bbaebdcf8720c4d4fb227  bash_process-1.2.2.tar.gz
     3.8  9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
     3.9  e7ffe4238b61a3c1ee87aca4421e7a612e09b836  ci-extras-1.tar.gz
    3.10  70105fd6fbfd1a868383fc510772b95234325d31  csdp-6.x.tar.gz
    3.11 @@ -144,6 +145,7 @@
    3.12  b668e1f43a41608a8eb365c5e19db6c54c72748a  polyml-5.5.3-20150911.tar.gz
    3.13  1f5cd9b1390dab13861f90dfc06d4180cc107587  polyml-5.5.3-20150916.tar.gz
    3.14  f78896e588e8ebb4da57bf0c95210b0f0fa9e551  polyml-5.6-1.tar.gz
    3.15 +21fa0592b7dfd23269063f42604438165630c0f0  polyml-5.6-2.tar.gz
    3.16  03ba81e595fa6d6df069532d67ad3195c37d9046  polyml-5.6-20151123.tar.gz
    3.17  822f489c18e38ce5ef979ec21dccce4473e09be6  polyml-5.6-20151206.tar.gz
    3.18  bd6a448f0e0d5787747f4f30ca661f9c1868e4a7  polyml-5.6-20151223.tar.gz
     4.1 --- a/Admin/components/main	Fri Sep 29 14:12:14 2017 +0100
     4.2 +++ b/Admin/components/main	Fri Sep 29 14:17:17 2017 +0100
     4.3 @@ -1,5 +1,5 @@
     4.4  #main components for everyday use, without big impact on overall build time
     4.5 -bash_process-1.2.1
     4.6 +bash_process-1.2.2
     4.7  csdp-6.x
     4.8  cvc4-1.5-3
     4.9  e-2.0-1
    4.10 @@ -10,7 +10,7 @@
    4.11  jortho-1.0-2
    4.12  kodkodi-1.5.2
    4.13  nunchaku-0.5
    4.14 -polyml-5.6-1
    4.15 +polyml-5.6-2
    4.16  postgresql-42.1.4
    4.17  scala-2.12.3
    4.18  smbc-0.4.1
     5.1 --- a/Admin/polyml/settings	Fri Sep 29 14:12:14 2017 +0100
     5.2 +++ b/Admin/polyml/settings	Fri Sep 29 14:17:17 2017 +0100
     5.3 @@ -13,10 +13,10 @@
     5.4  fi
     5.5  
     5.6  case "${ISABELLE_PLATFORM}:${ML_SYSTEM_64}" in
     5.7 -  x86-cygwin:true)
     5.8 +  *-cygwin:true)
     5.9      PLATFORMS="x86_64-windows x86-windows"
    5.10      ;;
    5.11 -  x86-cygwin:*)
    5.12 +  *-cygwin:*)
    5.13      PLATFORMS="x86-windows x86_64-windows"
    5.14      ;;
    5.15    *:true)
     6.1 --- a/lib/scripts/isabelle-platform	Fri Sep 29 14:12:14 2017 +0100
     6.2 +++ b/lib/scripts/isabelle-platform	Fri Sep 29 14:17:17 2017 +0100
     6.3 @@ -40,15 +40,18 @@
     6.4      ;;
     6.5    CYGWIN_NT*)
     6.6      ISABELLE_PLATFORM_FAMILY="windows"
     6.7 +    if [ "$PROCESSOR_ARCHITECTURE" = "AMD64" -o "$PROCESSOR_ARCHITEW6432" = "AMD64" ]; then
     6.8 +      ISABELLE_WINDOWS_PLATFORM32="x86-windows"
     6.9 +      ISABELLE_WINDOWS_PLATFORM64="x86_64-windows"
    6.10 +    else
    6.11 +      ISABELLE_WINDOWS_PLATFORM32="x86-windows"
    6.12 +    fi
    6.13      case $(uname -m) in
    6.14 -      i?86 | x86_64)
    6.15 +      x86_64)
    6.16 +        ISABELLE_PLATFORM64=x86_64-cygwin
    6.17 +        ;;
    6.18 +      i?86)
    6.19          ISABELLE_PLATFORM32=x86-cygwin
    6.20 -        if [ "$PROCESSOR_ARCHITECTURE" = "AMD64" -o "$PROCESSOR_ARCHITEW6432" = "AMD64" ]; then
    6.21 -          ISABELLE_WINDOWS_PLATFORM32="x86-windows"
    6.22 -          ISABELLE_WINDOWS_PLATFORM64="x86_64-windows"
    6.23 -        else
    6.24 -          ISABELLE_WINDOWS_PLATFORM32="x86-windows"
    6.25 -        fi
    6.26          ;;
    6.27      esac
    6.28      ;;
    6.29 @@ -62,5 +65,5 @@
    6.30      ;;
    6.31  esac
    6.32  
    6.33 -ISABELLE_PLATFORM="$ISABELLE_PLATFORM32"
    6.34 -ISABELLE_WINDOWS_PLATFORM="$ISABELLE_WINDOWS_PLATFORM32"
    6.35 +ISABELLE_PLATFORM="${ISABELLE_PLATFORM32:-$ISABELLE_PLATFORM64}"
    6.36 +ISABELLE_WINDOWS_PLATFORM="${ISABELLE_WINDOWS_PLATFORM32:-$ISABELLE_WINDOWS_PLATFORM64}"
     7.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 29 14:12:14 2017 +0100
     7.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Sep 29 14:17:17 2017 +0100
     7.3 @@ -2253,9 +2253,7 @@
     7.4      have "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S" 
     7.5        using assms integrable_component [OF fcomp, where y=i] that by simp
     7.6      then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on S"
     7.7 -      apply -
     7.8 -      apply (rule abs_absolutely_integrableI_1, auto)
     7.9 -      by (simp add: f integrable_component)
    7.10 +      using abs_absolutely_integrableI_1 f integrable_component by blast
    7.11      then show ?thesis
    7.12        by (rule absolutely_integrable_scaleR_right)
    7.13    qed
     8.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 29 14:12:14 2017 +0100
     8.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Fri Sep 29 14:17:17 2017 +0100
     8.3 @@ -3060,8 +3060,8 @@
     8.4    unfolding integrable_on_def by blast
     8.5  
     8.6  lemma integral_has_vector_derivative_continuous_at:
     8.7 - fixes f :: "real \<Rightarrow> 'a::banach"
     8.8 - assumes f: "f integrable_on {a..b}"
     8.9 +  fixes f :: "real \<Rightarrow> 'a::banach"
    8.10 +  assumes f: "f integrable_on {a..b}"
    8.11       and x: "x \<in> {a..b} - S"
    8.12       and "finite S"
    8.13       and fx: "continuous (at x within ({a..b} - S)) f"
    8.14 @@ -3091,7 +3091,7 @@
    8.15        show ?thesis
    8.16          using False
    8.17          apply (simp add: abs_eq_content del: content_real_if measure_lborel_Icc)
    8.18 -        apply (rule has_integral_bound_real [where f="(\<lambda>u. f u - f x)"])
    8.19 +        apply (rule has_integral_bound_real[where f="(\<lambda>u. f u - f x)"])
    8.20          using yx False d x y \<open>e>0\<close> assms by (auto simp: Idiff fux_int)
    8.21      next
    8.22        case True
    8.23 @@ -6062,8 +6062,7 @@
    8.24    have "norm (integral S f) \<le> integral S ((\<lambda>x. x \<bullet> k) \<circ> g)"
    8.25      apply (rule integral_norm_bound_integral[OF f integrable_linear[OF g]])
    8.26      apply (simp add: bounded_linear_inner_left)
    8.27 -    unfolding o_def
    8.28 -    apply (metis fg)
    8.29 +    apply (metis fg o_def)
    8.30      done
    8.31    then show ?thesis
    8.32      unfolding o_def integral_component_eq[OF g] .
    8.33 @@ -6180,7 +6179,6 @@
    8.34        have "closed_segment x0 x \<subseteq> U"
    8.35          by (rule \<open>convex U\<close>[unfolded convex_contains_segment, rule_format, OF \<open>x0 \<in> U\<close> \<open>x \<in> U\<close>])
    8.36        from elim have [intro]: "x \<in> U" by auto
    8.37 -
    8.38        have "?F x - ?F x0 - ?dF (x - x0) =
    8.39          integral (cbox a b) (\<lambda>y. f x y - f x0 y - fx x0 y (x - x0))"
    8.40          (is "_ = ?id")
    8.41 @@ -6217,7 +6215,7 @@
    8.42        also have "\<dots> < e' * norm (x - x0)"
    8.43          using \<open>e' > 0\<close>
    8.44          apply (intro mult_strict_right_mono[OF _ \<open>0 < norm (x - x0)\<close>])
    8.45 -        apply  (auto simp: divide_simps e_def)
    8.46 +        apply (auto simp: divide_simps e_def)
    8.47          by (metis \<open>0 < e\<close> e_def order.asym zero_less_divide_iff)
    8.48        finally have "norm (?F x - ?F x0 - ?dF (x - x0)) < e' * norm (x - x0)" .
    8.49        then show ?case
    8.50 @@ -6306,14 +6304,12 @@
    8.51      by atomize_elim (auto simp: integrable_on_def intro!: choice)
    8.52  
    8.53    moreover
    8.54 -
    8.55    have gi[simp]: "g integrable_on (cbox a b)"
    8.56      by (auto intro!: integrable_continuous uniform_limit_theorem[OF _ u] eventuallyI c)
    8.57    then obtain J where J: "(g has_integral J) (cbox a b)"
    8.58      by blast
    8.59  
    8.60    moreover
    8.61 -
    8.62    have "(I \<longlongrightarrow> J) F"
    8.63    proof cases
    8.64      assume "content (cbox a b) = 0"
    8.65 @@ -6461,19 +6457,17 @@
    8.66            f integrable_continuous_real)+
    8.67    have deriv: "(((\<lambda>x. integral {c..x} f) \<circ> g) has_vector_derivative g' x *\<^sub>R f (g x))
    8.68                   (at x within {a..b})" if "x \<in> {a..b} - s" for x
    8.69 -    apply (rule has_vector_derivative_eq_rhs)
    8.70 -    apply (rule vector_diff_chain_within)
    8.71 -    apply (subst has_field_derivative_iff_has_vector_derivative [symmetric])
    8.72 -    apply (rule deriv that)+
    8.73 -    apply (rule has_vector_derivative_within_subset)
    8.74 -    apply (rule integral_has_vector_derivative f)+
    8.75 -    using that le subset
    8.76 -    apply blast+
    8.77 -    done
    8.78 +  proof (rule has_vector_derivative_eq_rhs [OF vector_diff_chain_within refl])
    8.79 +    show "(g has_vector_derivative g' x) (at x within {a..b})"
    8.80 +      using deriv has_field_derivative_iff_has_vector_derivative that by blast
    8.81 +    show "((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) 
    8.82 +          (at (g x) within g ` {a..b})"
    8.83 +      using that le subset
    8.84 +      by (blast intro: has_vector_derivative_within_subset integral_has_vector_derivative f)
    8.85 +  qed
    8.86    have deriv: "(?F has_vector_derivative g' x *\<^sub>R f (g x))
    8.87                    (at x)" if "x \<in> {a..b} - (s \<union> {a,b})" for x
    8.88      using deriv[of x] that by (simp add: at_within_closed_interval o_def)
    8.89 -
    8.90    have "((\<lambda>x. g' x *\<^sub>R f (g x)) has_integral (?F b - ?F a)) {a..b}"
    8.91      using le cont_int s deriv cont_int
    8.92      by (intro fundamental_theorem_of_calculus_interior_strong[of "s \<union> {a,b}"]) simp_all
    8.93 @@ -6805,20 +6799,21 @@
    8.94              \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX"
    8.95          by (rule norm_xx [OF integral_Pair_const 1 2])
    8.96      } note * = this
    8.97 -    show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
    8.98 +    have "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e" 
    8.99 +      if "\<forall>x\<in>?CBOX. \<forall>x'\<in>?CBOX. norm (x' - x) < k \<longrightarrow> norm (f x' - f x) < e /(2 * content (?CBOX))" "0 < k" for k
   8.100 +    proof -
   8.101 +      obtain p where ptag: "p tagged_division_of cbox (a, c) (b, d)" 
   8.102 +                 and fine: "(\<lambda>x. ball x k) fine p"
   8.103 +        using fine_division_exists \<open>0 < k\<close> by blast
   8.104 +      show ?thesis
   8.105 +        apply (rule op_acbd [OF division_of_tagged_division [OF ptag]])
   8.106 +        using that fine ptag \<open>0 < k\<close> by (auto simp: *)
   8.107 +    qed
   8.108 +    then show "norm (integral ?CBOX f - integral (cbox a b) (\<lambda>x. integral (cbox c d) (\<lambda>y. f (x,y)))) \<le> e"
   8.109        using compact_uniformly_continuous [OF assms compact_cbox]
   8.110        apply (simp add: uniformly_continuous_on_def dist_norm)
   8.111        apply (drule_tac x="e/2 / content?CBOX" in spec)
   8.112 -      using cbp \<open>0 < e\<close>
   8.113 -      apply (auto simp: zero_less_mult_iff)
   8.114 -      apply (rename_tac k)
   8.115 -      apply (rule_tac e1=k in fine_division_exists [OF gauge_ball, where a = "(a,c)" and b = "(b,d)"])
   8.116 -      apply assumption
   8.117 -      apply (rule op_acbd)
   8.118 -      apply (erule division_of_tagged_division)
   8.119 -      using *
   8.120 -      apply auto
   8.121 -      done
   8.122 +      using cbp \<open>0 < e\<close> by (auto simp: zero_less_mult_iff)
   8.123    qed
   8.124    then show ?thesis
   8.125      by simp
   8.126 @@ -6861,7 +6856,6 @@
   8.127    shows   "((\<lambda>x::real. exp (-a*x)) has_integral exp (-a*c)/a) {c..}"
   8.128  proof -
   8.129    define f where "f = (\<lambda>k x. if x \<in> {c..real k} then exp (-a*x) else 0)"
   8.130 -
   8.131    {
   8.132      fix k :: nat assume k: "of_nat k \<ge> c"
   8.133      from k a
     9.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Fri Sep 29 14:12:14 2017 +0100
     9.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Fri Sep 29 14:17:17 2017 +0100
     9.3 @@ -1919,89 +1919,71 @@
     9.4  
     9.5  lemma interval_bisection_step:
     9.6    fixes type :: "'a::euclidean_space"
     9.7 -  assumes "P {}"
     9.8 -    and "\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P (s \<union> t)"
     9.9 -    and "\<not> P (cbox a (b::'a))"
    9.10 +  assumes emp: "P {}"
    9.11 +    and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
    9.12 +    and non: "\<not> P (cbox a (b::'a))"
    9.13    obtains c d where "\<not> P (cbox c d)"
    9.14 -    and "\<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
    9.15 +    and "\<And>i. i \<in> Basis \<Longrightarrow> a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
    9.16  proof -
    9.17    have "cbox a b \<noteq> {}"
    9.18 -    using assms(1,3) by metis
    9.19 +    using emp non by metis
    9.20    then have ab: "\<And>i. i\<in>Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
    9.21      by (force simp: mem_box)
    9.22 -  have UN_cases: "\<lbrakk>finite f;
    9.23 -           \<And>s. s\<in>f \<Longrightarrow> P s;
    9.24 -           \<And>s. s\<in>f \<Longrightarrow> \<exists>a b. s = cbox a b;
    9.25 -           \<And>s t. s\<in>f \<Longrightarrow> t\<in>f \<Longrightarrow> s \<noteq> t \<Longrightarrow> interior s \<inter> interior t = {}\<rbrakk> \<Longrightarrow> P (\<Union>f)" for f
    9.26 -  proof (induct f rule: finite_induct)
    9.27 -    case empty
    9.28 -    show ?case
    9.29 -      using assms(1) by auto
    9.30 +  have UN_cases: "\<lbrakk>finite \<F>;
    9.31 +           \<And>S. S\<in>\<F> \<Longrightarrow> P S;
    9.32 +           \<And>S. S\<in>\<F> \<Longrightarrow> \<exists>a b. S = cbox a b;
    9.33 +           \<And>S T. S\<in>\<F> \<Longrightarrow> T\<in>\<F> \<Longrightarrow> S \<noteq> T \<Longrightarrow> interior S \<inter> interior T = {}\<rbrakk> \<Longrightarrow> P (\<Union>\<F>)" for \<F>
    9.34 +  proof (induct \<F> rule: finite_induct)
    9.35 +    case empty show ?case
    9.36 +      using emp by auto
    9.37    next
    9.38      case (insert x f)
    9.39 -    show ?case
    9.40 -      unfolding Union_insert
    9.41 -      apply (rule assms(2)[rule_format])
    9.42 -      using Int_interior_Union_intervals [of f "interior x"]
    9.43 -      by (metis (no_types, lifting) insert insert_iff open_interior)
    9.44 +    then show ?case
    9.45 +      unfolding Union_insert by (metis Int_interior_Union_intervals Un insert_iff open_interior)
    9.46    qed
    9.47 -  let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<or>
    9.48 -    (c\<bullet>i = (a\<bullet>i + b\<bullet>i) / 2) \<and> (d\<bullet>i = b\<bullet>i)}"
    9.49 -  let ?PP = "\<lambda>c d. \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i"
    9.50 -  {
    9.51 -    presume "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d) \<Longrightarrow> False"
    9.52 -    then show thesis
    9.53 -      unfolding atomize_not not_all
    9.54 -      by (blast intro: that)
    9.55 -  }
    9.56 -  assume as: "\<forall>c d. ?PP c d \<longrightarrow> P (cbox c d)"
    9.57 -  have "P (\<Union>?A)"
    9.58 +  let ?ab = "\<lambda>i. (a\<bullet>i + b\<bullet>i) / 2"
    9.59 +  let ?A = "{cbox c d | c d::'a. \<forall>i\<in>Basis. (c\<bullet>i = a\<bullet>i) \<and> (d\<bullet>i = ?ab i) \<or>
    9.60 +    (c\<bullet>i = ?ab i) \<and> (d\<bullet>i = b\<bullet>i)}"
    9.61 +  have "P (\<Union>?A)" 
    9.62 +    if "\<And>c d.  \<forall>i\<in>Basis. a\<bullet>i \<le> c\<bullet>i \<and> c\<bullet>i \<le> d\<bullet>i \<and> d\<bullet>i \<le> b\<bullet>i \<and> 2 * (d\<bullet>i - c\<bullet>i) \<le> b\<bullet>i - a\<bullet>i \<Longrightarrow> P (cbox c d)"
    9.63    proof (rule UN_cases)
    9.64 -    let ?B = "(\<lambda>s. cbox (\<Sum>i\<in>Basis. (if i \<in> s then a\<bullet>i else (a\<bullet>i + b\<bullet>i) / 2) *\<^sub>R i::'a)
    9.65 -      (\<Sum>i\<in>Basis. (if i \<in> s then (a\<bullet>i + b\<bullet>i) / 2 else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
    9.66 +    let ?B = "(\<lambda>S. cbox (\<Sum>i\<in>Basis. (if i \<in> S then a\<bullet>i else ?ab i) *\<^sub>R i::'a)
    9.67 +                        (\<Sum>i\<in>Basis. (if i \<in> S then ?ab i else b\<bullet>i) *\<^sub>R i)) ` {s. s \<subseteq> Basis}"
    9.68      have "?A \<subseteq> ?B"
    9.69      proof
    9.70        fix x
    9.71        assume "x \<in> ?A"
    9.72        then obtain c d
    9.73          where x:  "x = cbox c d"
    9.74 -                  "\<And>i. i \<in> Basis \<Longrightarrow>
    9.75 -                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
    9.76 -                        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i" by blast
    9.77 -      show "x \<in> ?B"
    9.78 -        unfolding image_iff x
    9.79 -        apply (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in bexI)
    9.80 -        apply (rule arg_cong2 [where f = cbox])
    9.81 -        using x(2) ab
    9.82 -        apply (auto simp add: euclidean_eq_iff[where 'a='a])
    9.83 -        by fastforce
    9.84 +          "\<And>i. i \<in> Basis \<Longrightarrow>
    9.85 +                        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i" 
    9.86 +        by blast
    9.87 +      have "c = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then a \<bullet> i else ?ab i) *\<^sub>R i)"
    9.88 +           "d = (\<Sum>i\<in>Basis. (if c \<bullet> i = a \<bullet> i then ?ab i else b \<bullet> i) *\<^sub>R i)"
    9.89 +        using x(2) ab by (fastforce simp add: euclidean_eq_iff[where 'a='a])+
    9.90 +      then show "x \<in> ?B"
    9.91 +        unfolding x by (rule_tac x="{i. i\<in>Basis \<and> c\<bullet>i = a\<bullet>i}" in image_eqI) auto
    9.92      qed
    9.93      then show "finite ?A"
    9.94        by (rule finite_subset) auto
    9.95    next
    9.96 -    fix s
    9.97 -    assume "s \<in> ?A"
    9.98 +    fix S
    9.99 +    assume "S \<in> ?A"
   9.100      then obtain c d
   9.101 -      where s: "s = cbox c d"
   9.102 -               "\<And>i. i \<in> Basis \<Longrightarrow>
   9.103 -                     c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   9.104 -                     c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
   9.105 +      where s: "S = cbox c d"
   9.106 +               "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
   9.107        by blast
   9.108 -    show "P s"
   9.109 -      unfolding s
   9.110 -      apply (rule as[rule_format])
   9.111 -      using ab s(2) by force
   9.112 -    show "\<exists>a b. s = cbox a b"
   9.113 +    show "P S"
   9.114 +      unfolding s using ab s(2) by (fastforce intro!: that)
   9.115 +    show "\<exists>a b. S = cbox a b"
   9.116        unfolding s by auto
   9.117 -    fix t
   9.118 -    assume "t \<in> ?A"
   9.119 +    fix T
   9.120 +    assume "T \<in> ?A"
   9.121      then obtain e f where t:
   9.122 -      "t = cbox e f"
   9.123 -      "\<And>i. i \<in> Basis \<Longrightarrow>
   9.124 -        e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   9.125 -        e \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> f \<bullet> i = b \<bullet> i"
   9.126 +      "T = cbox e f"
   9.127 +      "\<And>i. i \<in> Basis \<Longrightarrow> e \<bullet> i = a \<bullet> i \<and> f \<bullet> i = ?ab i \<or> e \<bullet> i = ?ab i \<and> f \<bullet> i = b \<bullet> i"
   9.128        by blast
   9.129 -    assume "s \<noteq> t"
   9.130 +    assume "S \<noteq> T"
   9.131      then have "\<not> (c = e \<and> d = f)"
   9.132        unfolding s t by auto
   9.133      then obtain i where "c\<bullet>i \<noteq> e\<bullet>i \<or> d\<bullet>i \<noteq> f\<bullet>i" and i': "i \<in> Basis"
   9.134 @@ -2011,24 +1993,15 @@
   9.135        using t(2)[OF i'] \<open>c \<bullet> i \<noteq> e \<bullet> i \<or> d \<bullet> i \<noteq> f \<bullet> i\<close> i' s(2) t(2) by fastforce
   9.136      have *: "\<And>s t. (\<And>a. a \<in> s \<Longrightarrow> a \<in> t \<Longrightarrow> False) \<Longrightarrow> s \<inter> t = {}"
   9.137        by auto
   9.138 -    show "interior s \<inter> interior t = {}"
   9.139 +    show "interior S \<inter> interior T = {}"
   9.140        unfolding s t interior_cbox
   9.141      proof (rule *)
   9.142        fix x
   9.143        assume "x \<in> box c d" "x \<in> box e f"
   9.144        then have x: "c\<bullet>i < d\<bullet>i" "e\<bullet>i < f\<bullet>i" "c\<bullet>i < f\<bullet>i" "e\<bullet>i < d\<bullet>i"
   9.145 -        unfolding mem_box using i'
   9.146 -        by force+
   9.147 -      show False  using s(2)[OF i']
   9.148 -      proof safe
   9.149 -        assume as: "c \<bullet> i = a \<bullet> i" "d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2"
   9.150 -        show False
   9.151 -          using t(2)[OF i'] and i x unfolding as by (fastforce simp add:field_simps)
   9.152 -      next
   9.153 -        assume as: "c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2" "d \<bullet> i = b \<bullet> i"
   9.154 -        show False
   9.155 -          using t(2)[OF i'] and i x unfolding as by(fastforce simp add:field_simps)
   9.156 -      qed
   9.157 +        unfolding mem_box using i'  by force+
   9.158 +      show False  using s(2)[OF i'] t(2)[OF i'] and i x  
   9.159 +        by auto
   9.160      qed
   9.161    qed
   9.162    also have "\<Union>?A = cbox a b"
   9.163 @@ -2037,48 +2010,30 @@
   9.164      assume "x \<in> \<Union>?A"
   9.165      then obtain c d where x:
   9.166        "x \<in> cbox c d"
   9.167 -      "\<And>i. i \<in> Basis \<Longrightarrow>
   9.168 -        c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   9.169 -        c \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> d \<bullet> i = b \<bullet> i"
   9.170 +      "\<And>i. i \<in> Basis \<Longrightarrow> c \<bullet> i = a \<bullet> i \<and> d \<bullet> i = ?ab i \<or> c \<bullet> i = ?ab i \<and> d \<bullet> i = b \<bullet> i"
   9.171        by blast
   9.172 -    show "x\<in>cbox a b"
   9.173 -      unfolding mem_box
   9.174 -    proof safe
   9.175 -      fix i :: 'a
   9.176 -      assume i: "i \<in> Basis"
   9.177 -      then show "a \<bullet> i \<le> x \<bullet> i" "x \<bullet> i \<le> b \<bullet> i"
   9.178 -        using x(2)[OF i] x(1)[unfolded mem_box,THEN bspec, OF i] by auto
   9.179 -    qed
   9.180 +    then show "x\<in>cbox a b"
   9.181 +      unfolding mem_box by force
   9.182    next
   9.183      fix x
   9.184      assume x: "x \<in> cbox a b"
   9.185 -    have "\<forall>i\<in>Basis.
   9.186 -      \<exists>c d. (c = a\<bullet>i \<and> d = (a\<bullet>i + b\<bullet>i) / 2 \<or> c = (a\<bullet>i + b\<bullet>i) / 2 \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
   9.187 +    then have "\<forall>i\<in>Basis. \<exists>c d. (c = a\<bullet>i \<and> d = ?ab i \<or> c = ?ab i \<and> d = b\<bullet>i) \<and> c\<le>x\<bullet>i \<and> x\<bullet>i \<le> d"
   9.188        (is "\<forall>i\<in>Basis. \<exists>c d. ?P i c d")
   9.189 -      unfolding mem_box
   9.190 -    proof
   9.191 -      fix i :: 'a
   9.192 -      assume i: "i \<in> Basis"
   9.193 -      have "?P i (a\<bullet>i) ((a \<bullet> i + b \<bullet> i) / 2) \<or> ?P i ((a \<bullet> i + b \<bullet> i) / 2) (b\<bullet>i)"
   9.194 -        using x[unfolded mem_box,THEN bspec, OF i] by auto
   9.195 -      then show "\<exists>c d. ?P i c d"
   9.196 -        by blast
   9.197 -    qed
   9.198 -    then obtain \<alpha> \<beta> where
   9.199 -     "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<or>
   9.200 -         \<alpha> \<bullet> i = (a \<bullet> i + b \<bullet> i) / 2 \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
   9.201 +      unfolding mem_box by (metis linear)
   9.202 +    then obtain \<alpha> \<beta> where "\<forall>i\<in>Basis. (\<alpha> \<bullet> i = a \<bullet> i \<and> \<beta> \<bullet> i = ?ab i \<or>
   9.203 +         \<alpha> \<bullet> i = ?ab i \<and> \<beta> \<bullet> i = b \<bullet> i) \<and> \<alpha> \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> \<beta> \<bullet> i"
   9.204        by (auto simp: choice_Basis_iff)
   9.205      then show "x\<in>\<Union>?A"
   9.206        by (force simp add: mem_box)
   9.207    qed
   9.208 -  finally show False
   9.209 -    using assms by auto
   9.210 +  finally show thesis
   9.211 +      by (metis (no_types, lifting) assms(3) that)
   9.212  qed
   9.213  
   9.214  lemma interval_bisection:
   9.215    fixes type :: "'a::euclidean_space"
   9.216    assumes "P {}"
   9.217 -    and "(\<forall>s t. P s \<and> P t \<and> interior(s) \<inter> interior(t) = {} \<longrightarrow> P(s \<union> t))"
   9.218 +    and Un: "\<And>S T. \<lbrakk>P S; P T; interior(S) \<inter> interior(T) = {}\<rbrakk> \<Longrightarrow> P (S \<union> T)"
   9.219      and "\<not> P (cbox a (b::'a))"
   9.220    obtains x where "x \<in> cbox a b"
   9.221      and "\<forall>e>0. \<exists>c d. x \<in> cbox c d \<and> cbox c d \<subseteq> ball x e \<and> cbox c d \<subseteq> cbox a b \<and> \<not> P (cbox c d)"
   9.222 @@ -2092,14 +2047,14 @@
   9.223        case True
   9.224        then show ?thesis by auto
   9.225      next
   9.226 -      case as: False
   9.227 +      case False
   9.228        obtain c d where "\<not> P (cbox c d)"
   9.229 -        "\<forall>i\<in>Basis.
   9.230 +        "\<And>i. i \<in> Basis \<Longrightarrow>
   9.231             fst x \<bullet> i \<le> c \<bullet> i \<and>
   9.232             c \<bullet> i \<le> d \<bullet> i \<and>
   9.233             d \<bullet> i \<le> snd x \<bullet> i \<and>
   9.234             2 * (d \<bullet> i - c \<bullet> i) \<le> snd x \<bullet> i - fst x \<bullet> i"
   9.235 -        by (rule interval_bisection_step[of P, OF assms(1-2) as])
   9.236 +        by (blast intro: interval_bisection_step[of P, OF assms(1-2) False])
   9.237        then show ?thesis
   9.238          by (rule_tac x="(c,d)" in exI) auto
   9.239      qed
   9.240 @@ -2281,33 +2236,17 @@
   9.241  
   9.242  lemma tagged_division_finer:
   9.243    fixes p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
   9.244 -  assumes "p tagged_division_of (cbox a b)"
   9.245 +  assumes ptag: "p tagged_division_of (cbox a b)"
   9.246      and "gauge d"
   9.247    obtains q where "q tagged_division_of (cbox a b)"
   9.248      and "d fine q"
   9.249      and "\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q"
   9.250  proof -
   9.251 -  let ?P = "\<lambda>p. p tagged_partial_division_of (cbox a b) \<longrightarrow> gauge d \<longrightarrow>
   9.252 -    (\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and>
   9.253 -      (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))"
   9.254 -  {
   9.255 -    have *: "finite p" "p tagged_partial_division_of (cbox a b)"
   9.256 -      using assms(1)
   9.257 -      unfolding tagged_division_of_def
   9.258 -      by auto
   9.259 -    presume "\<And>p. finite p \<Longrightarrow> ?P p"
   9.260 -    from this[rule_format,OF * assms(2)] 
   9.261 -    obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "(\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q)"
   9.262 -      by auto
   9.263 -    with that[of q] show ?thesis
   9.264 -      using assms(1) by auto
   9.265 -  }
   9.266 -  fix p :: "('a::euclidean_space \<times> ('a::euclidean_space set)) set"
   9.267 -  assume as: "finite p"
   9.268 -  show "?P p"
   9.269 -    apply rule
   9.270 -    apply rule
   9.271 -    using as
   9.272 +  have p: "finite p" "p tagged_partial_division_of (cbox a b)"
   9.273 +    using ptag unfolding tagged_division_of_def by auto
   9.274 +  have "(\<exists>q. q tagged_division_of (\<Union>{k. \<exists>x. (x,k) \<in> p}) \<and> d fine q \<and> (\<forall>(x,k) \<in> p. k \<subseteq> d(x) \<longrightarrow> (x,k) \<in> q))" 
   9.275 +    if "finite p" "p tagged_partial_division_of (cbox a b)" "gauge d" for p
   9.276 +    using that
   9.277    proof (induct p)
   9.278      case empty
   9.279      show ?case
   9.280 @@ -2325,7 +2264,7 @@
   9.281        unfolding xk by auto
   9.282      note p = tagged_partial_division_ofD[OF insert(4)]
   9.283      obtain u v where uv: "k = cbox u v"
   9.284 -      using p(4)[unfolded xk, OF insertI1] by blast
   9.285 +      using p(4) xk by blast
   9.286      have "finite {k. \<exists>x. (x, k) \<in> p}"
   9.287        apply (rule finite_subset[of _ "snd ` p"])
   9.288        using image_iff apply fastforce
   9.289 @@ -2363,6 +2302,9 @@
   9.290          done
   9.291      qed
   9.292    qed
   9.293 +  with p obtain q where q: "q tagged_division_of \<Union>{k. \<exists>x. (x, k) \<in> p}" "d fine q" "\<forall>(x, k)\<in>p. k \<subseteq> d x \<longrightarrow> (x, k) \<in> q"
   9.294 +    by (meson \<open>gauge d\<close>)
   9.295 +  with ptag that show ?thesis by auto
   9.296  qed
   9.297  
   9.298  subsubsection \<open>Covering lemma\<close>
    10.1 --- a/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri Sep 29 14:12:14 2017 +0100
    10.2 +++ b/src/HOL/Tools/SMT/z3_replay_methods.ML	Fri Sep 29 14:17:17 2017 +0100
    10.3 @@ -426,8 +426,10 @@
    10.4      abstract_eq abstract_prop (dest_prop t))
    10.5  
    10.6  fun arith_rewrite_tac ctxt _ =
    10.7 -  TRY o Simplifier.simp_tac ctxt
    10.8 -  THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
    10.9 +  let val backup_tac = Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt in
   10.10 +    (TRY o Simplifier.simp_tac ctxt) THEN_ALL_NEW backup_tac
   10.11 +    ORELSE' backup_tac
   10.12 +  end
   10.13  
   10.14  fun prove_arith_rewrite ctxt t =
   10.15    prove_abstract' ctxt t arith_rewrite_tac (
    11.1 --- a/src/Pure/General/file.scala	Fri Sep 29 14:12:14 2017 +0100
    11.2 +++ b/src/Pure/General/file.scala	Fri Sep 29 14:17:17 2017 +0100
    11.3 @@ -106,6 +106,21 @@
    11.4    def pwd(): Path = path(Path.current.absolute_file)
    11.5  
    11.6  
    11.7 +  /* relative paths */
    11.8 +
    11.9 +  def relative_path(base: Path, other: Path): Option[Path] =
   11.10 +  {
   11.11 +    val base_path = base.file.toPath
   11.12 +    val other_path = other.file.toPath
   11.13 +    if (other_path.startsWith(base_path))
   11.14 +      Some(path(base_path.relativize(other_path).toFile))
   11.15 +    else None
   11.16 +  }
   11.17 +
   11.18 +  def rebase_path(base: Path, other: Path): Option[Path] =
   11.19 +    relative_path(base, other).map(base + _)
   11.20 +
   11.21 +
   11.22    /* bash path */
   11.23  
   11.24    def bash_path(path: Path): String = Bash.string(standard_path(path))
    12.1 --- a/src/Pure/PIDE/resources.scala	Fri Sep 29 14:12:14 2017 +0100
    12.2 +++ b/src/Pure/PIDE/resources.scala	Fri Sep 29 14:17:17 2017 +0100
    12.3 @@ -57,12 +57,33 @@
    12.4  
    12.5    /* theory files */
    12.6  
    12.7 -  def loaded_files(syntax: Outer_Syntax, text: String): List[String] =
    12.8 -    if (syntax.load_commands_in(text)) {
    12.9 -      val spans = syntax.parse_spans(text)
   12.10 -      spans.iterator.map(Command.span_files(syntax, _)._1).flatten.toList
   12.11 +  def loaded_files(syntax: Outer_Syntax, name: Document.Node.Name): () => List[Path] =
   12.12 +  {
   12.13 +    val raw_text = with_thy_reader(name, reader => reader.source.toString)
   12.14 +    () => {
   12.15 +      val text = Symbol.decode(raw_text)
   12.16 +      if (syntax.load_commands_in(text)) {
   12.17 +        val spans = syntax.parse_spans(text)
   12.18 +        val dir = Path.explode(name.master_dir)
   12.19 +        spans.iterator.map(Command.span_files(syntax, _)._1).flatten.
   12.20 +          map(a => (dir + Path.explode(a)).expand).toList
   12.21 +      }
   12.22 +      else Nil
   12.23      }
   12.24 -    else Nil
   12.25 +  }
   12.26 +
   12.27 +  def pure_files(syntax: Outer_Syntax, dir: Path): List[Path] =
   12.28 +  {
   12.29 +    val roots =
   12.30 +      for { (name, _) <- Thy_Header.ml_roots }
   12.31 +      yield (dir + Path.explode(name)).expand
   12.32 +    val files =
   12.33 +      for {
   12.34 +        (path, (_, theory)) <- roots zip Thy_Header.ml_roots
   12.35 +        file <- loaded_files(syntax, Document.Node.Name(path.implode, path.dir.implode, theory))()
   12.36 +      } yield file
   12.37 +    roots ::: files
   12.38 +  }
   12.39  
   12.40    def theory_qualifier(name: Document.Node.Name): String =
   12.41      session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
    13.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 14:12:14 2017 +0100
    13.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 14:17:17 2017 +0100
    13.3 @@ -27,7 +27,9 @@
    13.4    {
    13.5      val empty: Known = Known()
    13.6  
    13.7 -    def make(local_dir: Path, bases: List[Base], theories: List[Document.Node.Name]): Known =
    13.8 +    def make(local_dir: Path, bases: List[Base],
    13.9 +      theories: List[Document.Node.Name] = Nil,
   13.10 +      loaded_files: List[(String, List[Path])] = Nil): Known =
   13.11      {
   13.12        def bases_iterator(local: Boolean) =
   13.13          for {
   13.14 @@ -66,15 +68,21 @@
   13.15                known
   13.16              else known + (file -> (name :: theories1))
   13.17          })
   13.18 +
   13.19 +      val known_loaded_files =
   13.20 +        (loaded_files.toMap /: bases.map(base => base.known.loaded_files))(_ ++ _)
   13.21 +
   13.22        Known(known_theories, known_theories_local,
   13.23 -        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
   13.24 +        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap,
   13.25 +        known_loaded_files)
   13.26      }
   13.27    }
   13.28  
   13.29    sealed case class Known(
   13.30      theories: Map[String, Document.Node.Name] = Map.empty,
   13.31      theories_local: Map[String, Document.Node.Name] = Map.empty,
   13.32 -    files: Map[JFile, List[Document.Node.Name]] = Map.empty)
   13.33 +    files: Map[JFile, List[Document.Node.Name]] = Map.empty,
   13.34 +    loaded_files: Map[String, List[Path]] = Map.empty)
   13.35    {
   13.36      def platform_path: Known =
   13.37        copy(theories = for ((a, b) <- theories) yield (a, b.map(File.platform_path(_))),
   13.38 @@ -106,7 +114,6 @@
   13.39  
   13.40    sealed case class Base(
   13.41      pos: Position.T = Position.none,
   13.42 -    imports: Option[Base] = None,
   13.43      global_theories: Map[String, String] = Map.empty,
   13.44      loaded_theories: Map[String, String] = Map.empty,
   13.45      known: Known = Known.empty,
   13.46 @@ -114,10 +121,9 @@
   13.47      syntax: Outer_Syntax = Outer_Syntax.empty,
   13.48      sources: List[(Path, SHA1.Digest)] = Nil,
   13.49      session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
   13.50 -    errors: List[String] = Nil)
   13.51 +    errors: List[String] = Nil,
   13.52 +    imports: Option[Base] = None)
   13.53    {
   13.54 -    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
   13.55 -
   13.56      def platform_path: Base = copy(known = known.platform_path)
   13.57      def standard_path: Base = copy(known = known.standard_path)
   13.58  
   13.59 @@ -130,6 +136,8 @@
   13.60      def dest_known_theories: List[(String, String)] =
   13.61        for ((theory, node_name) <- known.theories.toList)
   13.62          yield (theory, node_name.node)
   13.63 +
   13.64 +    def get_imports: Base = imports getOrElse Base.bootstrap(global_theories)
   13.65    }
   13.66  
   13.67    sealed case class Deps(session_bases: Map[String, Base], all_known: Known)
   13.68 @@ -174,7 +182,7 @@
   13.69                }
   13.70              val imports_base: Sessions.Base =
   13.71                parent_base.copy(known =
   13.72 -                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
   13.73 +                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_))))
   13.74  
   13.75              val resources = new Resources(imports_base)
   13.76  
   13.77 @@ -200,21 +208,16 @@
   13.78              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
   13.79              val loaded_files =
   13.80                if (inlined_files) {
   13.81 -                val pure_files =
   13.82 -                  if (is_pure(info.name)) {
   13.83 -                    val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
   13.84 -                    val files =
   13.85 -                      roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
   13.86 -                        map(file => info.dir + Path.explode(file))
   13.87 -                    roots ::: files
   13.88 -                  }
   13.89 -                  else Nil
   13.90 -                pure_files ::: thy_deps.loaded_files
   13.91 +                if (Sessions.is_pure(info.name)) {
   13.92 +                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
   13.93 +                    thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
   13.94 +                }
   13.95 +                else thy_deps.loaded_files
   13.96                }
   13.97                else Nil
   13.98  
   13.99              val all_files =
  13.100 -              (theory_files ::: loaded_files :::
  13.101 +              (theory_files ::: loaded_files.flatMap(_._2) :::
  13.102                  info.files.map(file => info.dir + file) :::
  13.103                  info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
  13.104  
  13.105 @@ -257,6 +260,11 @@
  13.106                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
  13.107              }
  13.108  
  13.109 +            val known =
  13.110 +              Known.make(info.dir, List(imports_base),
  13.111 +                theories = thy_deps.deps.map(_.name),
  13.112 +                loaded_files = loaded_files)
  13.113 +
  13.114              val sources =
  13.115                for (p <- all_files if p.is_file) yield (p, SHA1.digest(p.file))
  13.116              val sources_errors =
  13.117 @@ -265,15 +273,15 @@
  13.118              val base =
  13.119                Base(
  13.120                  pos = info.pos,
  13.121 -                imports = Some(imports_base),
  13.122                  global_theories = global_theories,
  13.123                  loaded_theories = thy_deps.loaded_theories,
  13.124 -                known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
  13.125 +                known = known,
  13.126                  keywords = thy_deps.keywords,
  13.127                  syntax = syntax,
  13.128                  sources = sources,
  13.129                  session_graph = session_graph,
  13.130 -                errors = thy_deps.errors ::: sources_errors)
  13.131 +                errors = thy_deps.errors ::: sources_errors,
  13.132 +                imports = Some(imports_base))
  13.133  
  13.134              session_bases + (info.name -> base)
  13.135            }
  13.136 @@ -284,13 +292,14 @@
  13.137            }
  13.138        })
  13.139  
  13.140 -    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil))
  13.141 +    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
  13.142    }
  13.143  
  13.144    def session_base_errors(
  13.145      options: Options,
  13.146      session: String,
  13.147      dirs: List[Path] = Nil,
  13.148 +    inlined_files: Boolean = false,
  13.149      all_known: Boolean = false): (List[String], Base) =
  13.150    {
  13.151      val full_sessions = load(options, dirs = dirs)
  13.152 @@ -298,7 +307,8 @@
  13.153      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
  13.154  
  13.155      val sessions: T = if (all_known) full_sessions else selected_sessions
  13.156 -    val deps = Sessions.deps(sessions, global_theories = global_theories)
  13.157 +    val deps =
  13.158 +      Sessions.deps(sessions, inlined_files = inlined_files, global_theories = global_theories)
  13.159      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
  13.160      (deps.errors, base)
  13.161    }
  13.162 @@ -307,9 +317,12 @@
  13.163      options: Options,
  13.164      session: String,
  13.165      dirs: List[Path] = Nil,
  13.166 +    inlined_files: Boolean = false,
  13.167      all_known: Boolean = false): Base =
  13.168    {
  13.169 -    val (errs, base) = session_base_errors(options, session, dirs = dirs, all_known = all_known)
  13.170 +    val (errs, base) =
  13.171 +      session_base_errors(options, session, dirs = dirs,
  13.172 +        inlined_files = inlined_files, all_known = all_known)
  13.173      if (errs.isEmpty) base else error(cat_lines(errs))
  13.174    }
  13.175  
    14.1 --- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 14:12:14 2017 +0100
    14.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 14:17:17 2017 +0100
    14.3 @@ -88,17 +88,11 @@
    14.4              (name.theory_base_name -> name.theory)  // legacy
    14.5        }
    14.6  
    14.7 -    def loaded_files: List[Path] =
    14.8 +    def loaded_files: List[(String, List[Path])] =
    14.9      {
   14.10 -      def loaded(dep: Thy_Info.Dep): List[Path] =
   14.11 -      {
   14.12 -        val string = resources.with_thy_reader(dep.name,
   14.13 -          reader => Symbol.decode(reader.source.toString))
   14.14 -        resources.loaded_files(syntax, string).
   14.15 -          map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
   14.16 -      }
   14.17 -      val dep_files = Par_List.map(loaded _, rev_deps)
   14.18 -      ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
   14.19 +      val names = deps.map(_.name)
   14.20 +      names.map(_.theory) zip
   14.21 +        Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
   14.22      }
   14.23  
   14.24      override def toString: String = deps.toString