# HG changeset patch
# User wenzelm
# Date 1491424149 -7200
# Node ID faeccede95349eafcc993396bc30626be599d289
# Parent  83586780598b0f2281c30e8bd701bd0cf55f1263# Parent  079a6f850c0265c06227e143b4ca7bdc1e292a38
merged

diff -r 83586780598b -r faeccede9534 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Wed Apr 05 13:47:41 2017 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Wed Apr 05 22:29:09 2017 +0200
@@ -14,29 +14,28 @@
 subsection \<open>Fibonacci numbers\<close>
 
 fun fib :: "nat \<Rightarrow> nat"
-where
-  fib0: "fib 0 = 0"
-| fib1: "fib (Suc 0) = 1"
-| fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
+  where
+    fib0: "fib 0 = 0"
+  | fib1: "fib (Suc 0) = 1"
+  | fib2: "fib (Suc (Suc n)) = fib (Suc n) + fib n"
 
 
 subsection \<open>Basic Properties\<close>
 
-lemma fib_1 [simp]: "fib (1::nat) = 1"
+lemma fib_1 [simp]: "fib 1 = 1"
   by (metis One_nat_def fib1)
 
-lemma fib_2 [simp]: "fib (2::nat) = 1"
-  using fib.simps(3) [of 0]
-  by (simp add: numeral_2_eq_2)
+lemma fib_2 [simp]: "fib 2 = 1"
+  using fib.simps(3) [of 0] by (simp add: numeral_2_eq_2)
 
 lemma fib_plus_2: "fib (n + 2) = fib (n + 1) + fib n"
   by (metis Suc_eq_plus1 add_2_eq_Suc' fib.simps(3))
 
-lemma fib_add: "fib (Suc (n+k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
+lemma fib_add: "fib (Suc (n + k)) = fib (Suc k) * fib (Suc n) + fib k * fib n"
   by (induct n rule: fib.induct) (auto simp add: field_simps)
 
 lemma fib_neq_0_nat: "n > 0 \<Longrightarrow> fib n > 0"
-  by (induct n rule: fib.induct) (auto simp add: )
+  by (induct n rule: fib.induct) auto
 
 
 subsection \<open>More efficient code\<close>
@@ -45,21 +44,22 @@
   The naive approach is very inefficient since the branching recursion leads to many
   values of @{term fib} being computed multiple times. We can avoid this by ``remembering''
   the last two values in the sequence, yielding a tail-recursive version.
-  This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the 
+  This is far from optimal (it takes roughly $O(n\cdot M(n))$ time where $M(n)$ is the
   time required to multiply two $n$-bit integers), but much better than the naive version,
   which is exponential.
 \<close>
 
-fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
-  "gen_fib a b 0 = a"
-| "gen_fib a b (Suc 0) = b"
-| "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)"
+fun gen_fib :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat"
+  where
+    "gen_fib a b 0 = a"
+  | "gen_fib a b (Suc 0) = b"
+  | "gen_fib a b (Suc (Suc n)) = gen_fib b (a + b) (Suc n)"
 
 lemma gen_fib_recurrence: "gen_fib a b (Suc (Suc n)) = gen_fib a b n + gen_fib a b (Suc n)"
-  by (induction a b n rule: gen_fib.induct) simp_all
-  
+  by (induct a b n rule: gen_fib.induct) simp_all
+
 lemma gen_fib_fib: "gen_fib (fib n) (fib (Suc n)) m = fib (n + m)"
-  by (induction m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence)
+  by (induct m rule: fib.induct) (simp_all del: gen_fib.simps(3) add: gen_fib_recurrence)
 
 lemma fib_conv_gen_fib: "fib n = gen_fib 0 1 n"
   using gen_fib_fib[of 0 n] by simp
@@ -70,22 +70,22 @@
 subsection \<open>A Few Elementary Results\<close>
 
 text \<open>
-  \medskip Concrete Mathematics, page 278: Cassini's identity.  The proof is
+  \<^medskip> Concrete Mathematics, page 278: Cassini's identity.  The proof is
   much easier using integers, not natural numbers!
 \<close>
 
 lemma fib_Cassini_int: "int (fib (Suc (Suc n)) * fib n) - int((fib (Suc n))\<^sup>2) = - ((-1)^n)"
-  by (induct n rule: fib.induct)  (auto simp add: field_simps power2_eq_square power_add)
+  by (induct n rule: fib.induct) (auto simp add: field_simps power2_eq_square power_add)
 
 lemma fib_Cassini_nat:
   "fib (Suc (Suc n)) * fib n =
      (if even n then (fib (Suc n))\<^sup>2 - 1 else (fib (Suc n))\<^sup>2 + 1)"
-  using fib_Cassini_int [of n]  by (auto simp del: of_nat_mult of_nat_power)
+  using fib_Cassini_int [of n] by (auto simp del: of_nat_mult of_nat_power)
 
 
 subsection \<open>Law 6.111 of Concrete Mathematics\<close>
 
-lemma coprime_fib_Suc_nat: "coprime (fib (n::nat)) (fib (Suc n))"
+lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
   apply (induct n rule: fib.induct)
   apply auto
   apply (metis gcd_add1 add.commute)
@@ -109,12 +109,12 @@
   proof (cases "m < n")
     case True
     then have "m \<le> n" by auto
-    with \<open>0 < m\<close> have pos_n: "0 < n" by auto
-    with \<open>0 < m\<close> \<open>m < n\<close> have diff: "n - m < n" by auto
+    with \<open>0 < m\<close> have "0 < n" by auto
+    with \<open>0 < m\<close> \<open>m < n\<close> have *: "n - m < n" by auto
     have "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib ((n - m) mod m))"
-      by (simp add: mod_if [of n]) (insert \<open>m < n\<close>, auto)
+      by (simp add: mod_if [of n]) (use \<open>m < n\<close> in auto)
     also have "\<dots> = gcd (fib m)  (fib (n - m))"
-      by (simp add: less.hyps diff \<open>0 < m\<close>)
+      by (simp add: less.hyps * \<open>0 < m\<close>)
     also have "\<dots> = gcd (fib m) (fib n)"
       by (simp add: gcd_fib_diff \<open>m \<le> n\<close>)
     finally show "gcd (fib m) (fib (n mod m)) = gcd (fib m) (fib n)" .
@@ -125,8 +125,7 @@
   qed
 qed
 
-lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"
-    \<comment> \<open>Law 6.111\<close>
+lemma fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)"  \<comment> \<open>Law 6.111\<close>
   by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat gcd.commute gcd_fib_mod)
 
 theorem fib_mult_eq_sum_nat: "fib (Suc n) * fib n = (\<Sum>k \<in> {..n}. fib k * fib k)"
@@ -136,49 +135,55 @@
 subsection \<open>Closed form\<close>
 
 lemma fib_closed_form:
-  defines "\<phi> \<equiv> (1 + sqrt 5) / (2::real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2::real)"
-  shows   "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
-proof (induction n rule: fib.induct)
+  fixes \<phi> \<psi> :: real
+  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
+  shows "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
+proof (induct n rule: fib.induct)
   fix n :: nat
   assume IH1: "of_nat (fib n) = (\<phi> ^ n - \<psi> ^ n) / sqrt 5"
   assume IH2: "of_nat (fib (Suc n)) = (\<phi> ^ Suc n - \<psi> ^ Suc n) / sqrt 5"
   have "of_nat (fib (Suc (Suc n))) = of_nat (fib (Suc n)) + of_nat (fib n)" by simp
-  also have "... = (\<phi>^n*(\<phi> + 1) - \<psi>^n*(\<psi> + 1)) / sqrt 5"
+  also have "\<dots> = (\<phi>^n * (\<phi> + 1) - \<psi>^n * (\<psi> + 1)) / sqrt 5"
     by (simp add: IH1 IH2 field_simps)
   also have "\<phi> + 1 = \<phi>\<^sup>2" by (simp add: \<phi>_def field_simps power2_eq_square)
   also have "\<psi> + 1 = \<psi>\<^sup>2" by (simp add: \<psi>_def field_simps power2_eq_square)
-  also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)"  
+  also have "\<phi>^n * \<phi>\<^sup>2 - \<psi>^n * \<psi>\<^sup>2 = \<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)"
     by (simp add: power2_eq_square)
   finally show "of_nat (fib (Suc (Suc n))) = (\<phi> ^ Suc (Suc n) - \<psi> ^ Suc (Suc n)) / sqrt 5" .
 qed (simp_all add: \<phi>_def \<psi>_def field_simps)
 
 lemma fib_closed_form':
-  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
+  fixes \<phi> \<psi> :: real
+  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
   assumes "n > 0"
-  shows   "fib n = round (\<phi> ^ n / sqrt 5)"
+  shows "fib n = round (\<phi> ^ n / sqrt 5)"
 proof (rule sym, rule round_unique')
   have "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> = \<bar>\<psi>\<bar> ^ n / sqrt 5"
     by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power_abs)
   also {
     from assms have "\<bar>\<psi>\<bar>^n \<le> \<bar>\<psi>\<bar>^1"
       by (intro power_decreasing) (simp_all add: algebra_simps real_le_lsqrt)
-    also have "... < sqrt 5 / 2" by (simp add: \<psi>_def field_simps)
+    also have "\<dots> < sqrt 5 / 2" by (simp add: \<psi>_def field_simps)
     finally have "\<bar>\<psi>\<bar>^n / sqrt 5 < 1/2" by (simp add: field_simps)
   }
   finally show "\<bar>\<phi> ^ n / sqrt 5 - of_int (int (fib n))\<bar> < 1/2" .
 qed
 
 lemma fib_asymptotics:
-  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)"
-  shows   "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1"
+  fixes \<phi> :: real
+  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+  shows "(\<lambda>n. real (fib n) / (\<phi> ^ n / sqrt 5)) \<longlonglongrightarrow> 1"
 proof -
-  define \<psi> where "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
+  define \<psi> :: real where "\<psi> \<equiv> (1 - sqrt 5) / 2"
   have "\<phi> > 1" by (simp add: \<phi>_def)
-  hence A: "\<phi> \<noteq> 0" by auto
+  then have *: "\<phi> \<noteq> 0" by auto
   have "(\<lambda>n. (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 0"
     by (rule LIMSEQ_power_zero) (simp_all add: \<phi>_def \<psi>_def field_simps add_pos_pos)
-  hence "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0" by (intro tendsto_diff tendsto_const)
-  with A show ?thesis
+  then have "(\<lambda>n. 1 - (\<psi> / \<phi>) ^ n) \<longlonglongrightarrow> 1 - 0"
+    by (intro tendsto_diff tendsto_const)
+  with * show ?thesis
     by (simp add: divide_simps fib_closed_form [folded \<phi>_def \<psi>_def])
 qed
 
@@ -186,58 +191,72 @@
 subsection \<open>Divide-and-Conquer recurrence\<close>
 
 text \<open>
-  The following divide-and-conquer recurrence allows for a more efficient computation 
-  of Fibonacci numbers; however, it requires memoisation of values to be reasonably 
+  The following divide-and-conquer recurrence allows for a more efficient computation
+  of Fibonacci numbers; however, it requires memoisation of values to be reasonably
   efficient, cutting the number of values to be computed to logarithmically many instead of
-  linearly many. The vast majority of the computation time is then actually spent on the 
+  linearly many. The vast majority of the computation time is then actually spent on the
   multiplication, since the output number is exponential in the input number.
 \<close>
 
 lemma fib_rec_odd:
-  defines "\<phi> \<equiv> (1 + sqrt 5) / (2 :: real)" and "\<psi> \<equiv> (1 - sqrt 5) / (2 :: real)"
-  shows   "fib (Suc (2*n)) = fib n^2 + fib (Suc n)^2"
+  fixes \<phi> \<psi> :: real
+  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
+    and "\<psi> \<equiv> (1 - sqrt 5) / 2"
+  shows "fib (Suc (2 * n)) = fib n^2 + fib (Suc n)^2"
 proof -
   have "of_nat (fib n^2 + fib (Suc n)^2) = ((\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2)/5"
     by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] field_simps power2_eq_square)
-  also have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = 
-    \<phi>^(2*n) + \<psi>^(2*n) - 2*(\<phi>*\<psi>)^n + \<phi>^(2*n+2) + \<psi>^(2*n+2) - 2*(\<phi>*\<psi>)^(n+1)" (is "_ = ?A")
-      by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib)
-  also have "\<phi> * \<psi> = -1" by (simp add: \<phi>_def \<psi>_def field_simps)
-  hence "?A = \<phi>^(2*n+1) * (\<phi> + inverse \<phi>) + \<psi>^(2*n+1) * (\<psi> + inverse \<psi>)" 
+  also
+  let ?A = "\<phi>^(2 * n) + \<psi>^(2 * n) - 2*(\<phi> * \<psi>)^n + \<phi>^(2 * n + 2) + \<psi>^(2 * n + 2) - 2*(\<phi> * \<psi>)^(n + 1)"
+  have "(\<phi> ^ n - \<psi> ^ n)\<^sup>2 + (\<phi> * \<phi> ^ n - \<psi> * \<psi> ^ n)\<^sup>2 = ?A"
+    by (simp add: power2_eq_square algebra_simps power_mult power_mult_distrib)
+  also have "\<phi> * \<psi> = -1"
+    by (simp add: \<phi>_def \<psi>_def field_simps)
+  then have "?A = \<phi>^(2 * n + 1) * (\<phi> + inverse \<phi>) + \<psi>^(2 * n + 1) * (\<psi> + inverse \<psi>)"
     by (auto simp: field_simps power2_eq_square)
-  also have "1 + sqrt 5 > 0" by (auto intro: add_pos_pos)
-  hence "\<phi> + inverse \<phi> = sqrt 5" by (simp add: \<phi>_def field_simps)
-  also have "\<psi> + inverse \<psi> = -sqrt 5" by (simp add: \<psi>_def field_simps)
-  also have "(\<phi> ^ (2*n+1) * sqrt 5 + \<psi> ^ (2*n+1)* - sqrt 5) / 5 =
-               (\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * (sqrt 5 / 5)" by (simp add: field_simps)
-  also have "sqrt 5 / 5 = inverse (sqrt 5)" by (simp add: field_simps)
-  also have "(\<phi> ^ (2*n+1) - \<psi> ^ (2*n+1)) * ... = of_nat (fib (Suc (2*n)))"
+  also have "1 + sqrt 5 > 0"
+    by (auto intro: add_pos_pos)
+  then have "\<phi> + inverse \<phi> = sqrt 5"
+    by (simp add: \<phi>_def field_simps)
+  also have "\<psi> + inverse \<psi> = -sqrt 5"
+    by (simp add: \<psi>_def field_simps)
+  also have "(\<phi> ^ (2 * n + 1) * sqrt 5 + \<psi> ^ (2 * n + 1) * - sqrt 5) / 5 =
+    (\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * (sqrt 5 / 5)"
+    by (simp add: field_simps)
+  also have "sqrt 5 / 5 = inverse (sqrt 5)"
+    by (simp add: field_simps)
+  also have "(\<phi> ^ (2 * n + 1) - \<psi> ^ (2 * n + 1)) * \<dots> = of_nat (fib (Suc (2 * n)))"
     by (simp add: fib_closed_form[folded \<phi>_def \<psi>_def] divide_inverse)
-  finally show ?thesis by (simp only: of_nat_eq_iff)
+  finally show ?thesis
+    by (simp only: of_nat_eq_iff)
 qed
 
-lemma fib_rec_even: "fib (2*n) = (fib (n - 1) + fib (n + 1)) * fib n"
-proof (induction n)
+lemma fib_rec_even: "fib (2 * n) = (fib (n - 1) + fib (n + 1)) * fib n"
+proof (induct n)
+  case 0
+  then show ?case by simp
+next
   case (Suc n)
   let ?rfib = "\<lambda>x. real (fib x)"
-  have "2 * (Suc n) = Suc (Suc (2*n))" by simp
-  also have "real (fib ...) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n" 
+  have "2 * (Suc n) = Suc (Suc (2 * n))" by simp
+  also have "real (fib \<dots>) = ?rfib n^2 + ?rfib (Suc n)^2 + (?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n"
     by (simp add: fib_rec_odd Suc)
   also have "(?rfib (n - 1) + ?rfib (n + 1)) * ?rfib n = (2 * ?rfib (n + 1) - ?rfib n) * ?rfib n"
     by (cases n) simp_all
-  also have "?rfib n^2 + ?rfib (Suc n)^2 + ... = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)"
+  also have "?rfib n^2 + ?rfib (Suc n)^2 + \<dots> = (?rfib (Suc n) + 2 * ?rfib n) * ?rfib (Suc n)"
     by (simp add: algebra_simps power2_eq_square)
-  also have "... = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp
+  also have "\<dots> = real ((fib (Suc n - 1) + fib (Suc n + 1)) * fib (Suc n))" by simp
   finally show ?case by (simp only: of_nat_eq_iff)
-qed simp
+qed
 
-lemma fib_rec_even': "fib (2*n) = (2*fib (n - 1) + fib n) * fib n"
+lemma fib_rec_even': "fib (2 * n) = (2 * fib (n - 1) + fib n) * fib n"
   by (subst fib_rec_even, cases n) simp_all
 
 lemma fib_rec:
-  "fib n = (if n = 0 then 0 else if n = 1 then 1 else
-            if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn
-            else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)"
+  "fib n =
+    (if n = 0 then 0 else if n = 1 then 1
+     else if even n then let n' = n div 2; fn = fib n' in (2 * fib (n' - 1) + fn) * fn
+     else let n' = n div 2 in fib n' ^ 2 + fib (Suc n') ^ 2)"
   by (auto elim: evenE oddE simp: fib_rec_odd fib_rec_even' Let_def)
 
 
@@ -247,7 +266,8 @@
   by (induct n) auto
 
 lemma sum_choose_drop_zero:
-    "(\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k) choose (k - 1)) = (\<Sum>j = 0..n. (n-j) choose j)"
+  "(\<Sum>k = 0..Suc n. if k = 0 then 0 else (Suc n - k) choose (k - 1)) =
+    (\<Sum>j = 0..n. (n-j) choose j)"
   by (rule trans [OF sum.cong sum_drop_zero]) auto
 
 lemma ne_diagonal_fib: "(\<Sum>k = 0..n. (n-k) choose k) = fib (Suc n)"
@@ -260,17 +280,16 @@
 next
   case (3 n)
   have "(\<Sum>k = 0..Suc n. Suc (Suc n) - k choose k) =
-        (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k=0 then 0 else (Suc n - k choose (k - 1))))"
+     (\<Sum>k = 0..Suc n. (Suc n - k choose k) + (if k = 0 then 0 else (Suc n - k choose (k - 1))))"
     by (rule sum.cong) (simp_all add: choose_reduce_nat)
-  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
-                   (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
+  also have "\<dots> =
+    (\<Sum>k = 0..Suc n. Suc n - k choose k) +
+    (\<Sum>k = 0..Suc n. if k=0 then 0 else (Suc n - k choose (k - 1)))"
     by (simp add: sum.distrib)
-  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) +
-                   (\<Sum>j = 0..n. n - j choose j)"
+  also have "\<dots> = (\<Sum>k = 0..Suc n. Suc n - k choose k) + (\<Sum>j = 0..n. n - j choose j)"
     by (metis sum_choose_drop_zero)
   finally show ?case using 3
     by simp
 qed
 
 end
-
diff -r 83586780598b -r faeccede9534 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Apr 05 13:47:41 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Apr 05 22:29:09 2017 +0200
@@ -67,38 +67,27 @@
     }
     else Nil
 
-  def qualify(name: String): String =
-    if (session_base.global_theories.contains(name) || Long_Name.is_qualified(name)) name
-    else Long_Name.qualify(session_name, name)
-
-  def init_name(raw_path: Path): Document.Node.Name =
+  def import_name(dir: String, s: String): Document.Node.Name =
   {
-    val path = raw_path.expand
-    val node = path.implode
-    val theory = qualify(Thy_Header.thy_name(node).getOrElse(""))
-    val master_dir = if (theory == "") "" else path.dir.implode
-    Document.Node.Name(node, master_dir, theory)
-  }
-
-  def import_name(master: Document.Node.Name, s: String): Document.Node.Name =
-  {
-    val theory = Thy_Header.base_name(s)
-    val is_qualified = Thy_Header.is_base_name(s) && Long_Name.is_qualified(s)
+    val thy = Thy_Header.base_name(s)
+    val is_global = session_base.global_theories.contains(thy)
+    val is_qualified = Long_Name.is_qualified(thy)
 
     val known_theory =
-      session_base.known_theories.get(theory) orElse
-      (if (is_qualified) session_base.known_theories.get(Long_Name.base_name(theory))
-       else session_base.known_theories.get(Long_Name.qualify(session_name, theory)))
+      session_base.known_theories.get(thy) orElse
+      (if (is_global) None
+       else if (is_qualified) session_base.known_theories.get(Long_Name.base_name(thy))
+       else session_base.known_theories.get(Long_Name.qualify(session_name, thy)))
 
     known_theory match {
       case Some(name) if session_base.loaded_theory(name) => Document.Node.Name.theory(name.theory)
       case Some(name) => name
-      case None if is_qualified => Document.Node.Name.theory(theory)
       case None =>
         val path = Path.explode(s)
-        val node = append(master.master_dir, thy_path(path))
-        val master_dir = append(master.master_dir, path.dir)
-        Document.Node.Name(node, master_dir, Long_Name.qualify(session_name, theory))
+        val node = append(dir, thy_path(path))
+        val master_dir = append(dir, path.dir)
+        val theory = if (is_global || is_qualified) thy else Long_Name.qualify(session_name, thy)
+        Document.Node.Name(node, master_dir, theory)
     }
   }
 
@@ -126,7 +115,7 @@
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
-          header.imports.map({ case (s, pos) => (import_name(node_name, s), pos) })
+          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -143,9 +132,11 @@
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
     if (Thy_Header.is_ml_root(name.theory))
-      Some(Document.Node.Header(List((import_name(name, Thy_Header.ML_BOOTSTRAP), Position.none))))
+      Some(Document.Node.Header(
+        List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
     else if (Thy_Header.is_bootstrap(name.theory))
-      Some(Document.Node.Header(List((import_name(name, Thy_Header.PURE), Position.none))))
+      Some(Document.Node.Header(
+        List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
     else None
 
 
diff -r 83586780598b -r faeccede9534 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Wed Apr 05 13:47:41 2017 +0200
+++ b/src/Pure/Thy/present.scala	Wed Apr 05 22:29:09 2017 +0200
@@ -18,19 +18,19 @@
 
   def session_graph(
     parent_session: String,
-    parent_loaded: Document.Node.Name => Boolean,
+    parent_base: Sessions.Base,
     deps: List[Thy_Info.Dep]): Graph_Display.Graph =
   {
     val parent_session_node =
       Graph_Display.Node("[" + parent_session + "]", "session." + parent_session)
 
     def node(name: Document.Node.Name): Graph_Display.Node =
-      if (parent_loaded(name)) parent_session_node
+      if (parent_base.loaded_theory(name)) parent_session_node
       else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
 
     (Graph_Display.empty_graph /: deps) {
       case (g, dep) =>
-        if (parent_loaded(dep.name)) g
+        if (parent_base.loaded_theory(dep.name)) g
         else {
           val a = node(dep.name)
           val bs = dep.header.imports.map({ case (name, _) => node(name) })
diff -r 83586780598b -r faeccede9534 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Apr 05 13:47:41 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 05 22:29:09 2017 +0200
@@ -81,8 +81,7 @@
             {
               val root_theories =
                 info.theories.flatMap({ case (_, thys) =>
-                  thys.map(thy =>
-                    (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
+                  thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos))
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
@@ -142,8 +141,7 @@
                 syntax = syntax,
                 sources = all_files.map(p => (p, SHA1.digest(p.file))),
                 session_graph =
-                  Present.session_graph(info.parent getOrElse "",
-                    parent_base.loaded_theory _, thy_deps.deps))
+                  Present.session_graph(info.parent getOrElse "", parent_base, thy_deps.deps))
 
             deps + (name -> base)
           }
@@ -175,7 +173,7 @@
     parent: Option[String],
     description: String,
     options: Options,
-    theories: List[(Options, List[Path])],
+    theories: List[(Options, List[String])],
     global_theories: List[String],
     files: List[Path],
     document_files: List[(Path, Path)],
@@ -390,8 +388,7 @@
           val session_options = options ++ entry.options
 
           val theories =
-            entry.theories.map({ case (opts, thys) =>
-              (session_options ++ opts, thys.map(thy => Path.explode(thy._1))) })
+            entry.theories.map({ case (opts, thys) => (session_options ++ opts, thys.map(_._1)) })
 
           val global_theories =
             for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
diff -r 83586780598b -r faeccede9534 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Wed Apr 05 13:47:41 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Wed Apr 05 22:29:09 2017 +0200
@@ -80,9 +80,6 @@
   private val Base_Name = new Regex(""".*?([^/\\:]+)""")
   private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
 
-  def is_base_name(s: String): Boolean =
-    s != "" && !s.exists("/\\:".contains(_))
-
   def base_name(s: String): String =
     s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
 
diff -r 83586780598b -r faeccede9534 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 05 13:47:41 2017 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 05 22:29:09 2017 +0200
@@ -204,7 +204,7 @@
               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
-                list(pair(Options.encode, list(Path.encode))))))))))))))(
+                list(pair(Options.encode, list(string))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,