# HG changeset patch # User Lars Hupel # Date 1491489553 -7200 # Node ID da25458453e35272a3e5ce70428136589493e9e7 # Parent 3c628937899db6d6baba56f15bc8ec84980b3632# Parent 44253ed65acdcc664b187e775ddf9cd7f2284639 merged diff -r 3c628937899d -r da25458453e3 NEWS --- a/NEWS Wed Apr 05 19:23:41 2017 +0200 +++ b/NEWS Thu Apr 06 16:39:13 2017 +0200 @@ -50,6 +50,10 @@ *** HOL *** +* Constants E/L/F in Library/Formal_Power_Series were renamed to +fps_exp/fps_ln/fps_hypergeo to avoid polluting the name space. +INCOMPATIBILITY. + * Constant "surj" is a full input/output abbreviation (again). Minor INCOMPATIBILITY. diff -r 3c628937899d -r da25458453e3 src/HOL/Analysis/Harmonic_Numbers.thy --- a/src/HOL/Analysis/Harmonic_Numbers.thy Wed Apr 05 19:23:41 2017 +0200 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy Thu Apr 06 16:39:13 2017 +0200 @@ -37,6 +37,9 @@ lemma of_real_harm: "of_real (harm n) = harm n" unfolding harm_def by simp +lemma abs_harm [simp]: "(abs (harm n) :: real) = harm n" + using harm_nonneg[of n] by (rule abs_of_nonneg) + lemma norm_harm: "norm (harm n) = harm n" by (subst of_real_harm [symmetric]) (simp add: harm_nonneg) @@ -91,6 +94,15 @@ finally show "ln (real (Suc n) + 1) \ harm (Suc n)" by - simp qed (simp_all add: harm_def) +lemma harm_at_top: "filterlim (harm :: nat \ real) at_top sequentially" +proof (rule filterlim_at_top_mono) + show "eventually (\n. harm n \ ln (real (Suc n))) at_top" + using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac) + show "filterlim (\n. ln (real (Suc n))) at_top sequentially" + by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially] + filterlim_Suc) +qed + subsection \The Euler--Mascheroni constant\ diff -r 3c628937899d -r da25458453e3 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed Apr 05 19:23:41 2017 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Thu Apr 06 16:39:13 2017 +0200 @@ -393,6 +393,11 @@ lemma fps_of_nat: "fps_const (of_nat c) = of_nat c" by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add) +lemma numeral_neq_fps_zero [simp]: "(numeral f :: 'a :: field_char_0 fps) \ 0" +proof + assume "numeral f = (0 :: 'a fps)" + from arg_cong[of _ _ "\F. F $ 0", OF this] show False by simp +qed subsection \The eXtractor series X\ @@ -1531,6 +1536,10 @@ lemma fps_deriv_nth[simp]: "fps_deriv f $ n = of_nat (n +1) * f $ (n + 1)" by (simp add: fps_deriv_def) +lemma fps_0th_higher_deriv: + "(fps_deriv ^^ n) f $ 0 = (fact n * f $ n :: 'a :: {comm_ring_1, semiring_char_0})" + by (induction n arbitrary: f) (simp_all del: funpow.simps add: funpow_Suc_right algebra_simps) + lemma fps_deriv_linear[simp]: "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_deriv f + fps_const b * fps_deriv g" @@ -1593,6 +1602,12 @@ lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0" by (simp add: fps_ext fps_deriv_def fps_const_def) +lemma fps_deriv_of_nat [simp]: "fps_deriv (of_nat n) = 0" + by (simp add: fps_of_nat [symmetric]) + +lemma fps_deriv_numeral [simp]: "fps_deriv (numeral n) = 0" + by (simp add: numeral_fps_const) + lemma fps_deriv_mult_const_left[simp]: "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f" by simp @@ -3424,7 +3439,7 @@ lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)" by (simp add: fps_eq_iff fps_compose_nth field_simps sum_negf[symmetric]) - + lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" using fps_compose_add_distrib [of a "- b" c] by (simp add: fps_compose_uminus) @@ -3692,17 +3707,23 @@ "fps_compose (f :: 'a :: comm_ring_1 fps) (fps_const c * X) = Abs_fps (\n. c^n * f $ n)" by (simp add: fps_eq_iff fps_compose_def power_mult_distrib if_distrib sum.delta' cong: if_cong) + +lemma fps_compose_uminus': + "fps_compose f (-X :: 'a :: comm_ring_1 fps) = Abs_fps (\n. (-1)^n * f $ n)" + using fps_compose_linear[of f "-1"] + by (simp only: fps_const_neg [symmetric] fps_const_1_eq_1) simp subsection \Elementary series\ subsubsection \Exponential series\ -definition "E x = Abs_fps (\n. x^n / of_nat (fact n))" - -lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r") +definition "fps_exp x = Abs_fps (\n. x^n / of_nat (fact n))" + +lemma fps_exp_deriv[simp]: "fps_deriv (fps_exp a) = fps_const (a::'a::field_char_0) * fps_exp a" + (is "?l = ?r") proof - have "?l$n = ?r $ n" for n - apply (auto simp add: E_def field_simps power_Suc[symmetric] + apply (auto simp add: fps_exp_def field_simps power_Suc[symmetric] simp del: fact_Suc of_nat_Suc power_Suc) apply (simp add: field_simps) done @@ -3710,8 +3731,8 @@ by (simp add: fps_eq_iff) qed -lemma E_unique_ODE: - "fps_deriv a = fps_const c * a \ a = fps_const (a$0) * E (c::'a::field_char_0)" +lemma fps_exp_unique_ODE: + "fps_deriv a = fps_const c * a \ a = fps_const (a$0) * fps_exp (c::'a::field_char_0)" (is "?lhs \ ?rhs") proof show ?rhs if ?lhs @@ -3732,75 +3753,107 @@ done qed show ?thesis - by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro: th') + by (auto simp add: fps_eq_iff fps_const_mult_left fps_exp_def intro: th') qed show ?lhs if ?rhs - using that by (metis E_deriv fps_deriv_mult_const_left mult.left_commute) + using that by (metis fps_exp_deriv fps_deriv_mult_const_left mult.left_commute) qed -lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r") +lemma fps_exp_add_mult: "fps_exp (a + b) = fps_exp (a::'a::field_char_0) * fps_exp b" (is "?l = ?r") proof - have "fps_deriv ?r = fps_const (a + b) * ?r" by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add) then have "?r = ?l" - by (simp only: E_unique_ODE) (simp add: fps_mult_nth E_def) + by (simp only: fps_exp_unique_ODE) (simp add: fps_mult_nth fps_exp_def) then show ?thesis .. qed -lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)" - by (simp add: E_def) - -lemma E0[simp]: "E (0::'a::field) = 1" +lemma fps_exp_nth[simp]: "fps_exp a $ n = a^n / of_nat (fact n)" + by (simp add: fps_exp_def) + +lemma fps_exp_0[simp]: "fps_exp (0::'a::field) = 1" by (simp add: fps_eq_iff power_0_left) -lemma E_neg: "E (- a) = inverse (E (a::'a::field_char_0))" +lemma fps_exp_neg: "fps_exp (- a) = inverse (fps_exp (a::'a::field_char_0))" proof - - from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1" by simp + from fps_exp_add_mult[of a "- a"] have th0: "fps_exp a * fps_exp (- a) = 1" by simp from fps_inverse_unique[OF th0] show ?thesis by simp qed -lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)" +lemma fps_exp_nth_deriv[simp]: + "fps_nth_deriv n (fps_exp (a::'a::field_char_0)) = (fps_const a)^n * (fps_exp a)" by (induct n) auto -lemma X_compose_E[simp]: "X oo E (a::'a::field) = E a - 1" +lemma X_compose_fps_exp[simp]: "X oo fps_exp (a::'a::field) = fps_exp a - 1" by (simp add: fps_eq_iff X_fps_compose) -lemma LE_compose: +lemma fps_inv_fps_exp_compose: assumes a: "a \ 0" - shows "fps_inv (E a - 1) oo (E a - 1) = X" - and "(E a - 1) oo fps_inv (E a - 1) = X" + shows "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X" + and "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X" proof - - let ?b = "E a - 1" + let ?b = "fps_exp a - 1" have b0: "?b $ 0 = 0" by simp have b1: "?b $ 1 \ 0" by (simp add: a) - from fps_inv[OF b0 b1] show "fps_inv (E a - 1) oo (E a - 1) = X" . - from fps_inv_right[OF b0 b1] show "(E a - 1) oo fps_inv (E a - 1) = X" . + from fps_inv[OF b0 b1] show "fps_inv (fps_exp a - 1) oo (fps_exp a - 1) = X" . + from fps_inv_right[OF b0 b1] show "(fps_exp a - 1) oo fps_inv (fps_exp a - 1) = X" . qed -lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)" - by (induct n) (auto simp add: field_simps E_add_mult) - -lemma radical_E: +lemma fps_exp_power_mult: "(fps_exp (c::'a::field_char_0))^n = fps_exp (of_nat n * c)" + by (induct n) (auto simp add: field_simps fps_exp_add_mult) + +lemma radical_fps_exp: assumes r: "r (Suc k) 1 = 1" - shows "fps_radical r (Suc k) (E (c::'a::field_char_0)) = E (c / of_nat (Suc k))" + shows "fps_radical r (Suc k) (fps_exp (c::'a::field_char_0)) = fps_exp (c / of_nat (Suc k))" proof - let ?ck = "(c / of_nat (Suc k))" let ?r = "fps_radical r (Suc k)" have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c" by (simp_all del: of_nat_Suc) - have th0: "E ?ck ^ (Suc k) = E c" unfolding E_power_mult eq0 .. - have th: "r (Suc k) (E c $0) ^ Suc k = E c $ 0" - "r (Suc k) (E c $ 0) = E ?ck $ 0" "E c $ 0 \ 0" using r by simp_all + have th0: "fps_exp ?ck ^ (Suc k) = fps_exp c" unfolding fps_exp_power_mult eq0 .. + have th: "r (Suc k) (fps_exp c $0) ^ Suc k = fps_exp c $ 0" + "r (Suc k) (fps_exp c $ 0) = fps_exp ?ck $ 0" "fps_exp c $ 0 \ 0" using r by simp_all from th0 radical_unique[where r=r and k=k, OF th] show ?thesis by auto qed -lemma Ec_E1_eq: "E (1::'a::field_char_0) oo (fps_const c * X) = E c" - apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib) - apply (simp add: cond_value_iff cond_application_beta sum.delta' cong del: if_weak_cong) - done +lemma fps_exp_compose_linear [simp]: + "fps_exp (d::'a::field_char_0) oo (fps_const c * X) = fps_exp (c * d)" + by (simp add: fps_compose_linear fps_exp_def fps_eq_iff power_mult_distrib) + +lemma fps_fps_exp_compose_minus [simp]: + "fps_compose (fps_exp c) (-X) = fps_exp (-c :: 'a :: field_char_0)" + using fps_exp_compose_linear[of c "-1 :: 'a"] + unfolding fps_const_neg [symmetric] fps_const_1_eq_1 by simp + +lemma fps_exp_eq_iff [simp]: "fps_exp c = fps_exp d \ c = (d :: 'a :: field_char_0)" +proof + assume "fps_exp c = fps_exp d" + from arg_cong[of _ _ "\F. F $ 1", OF this] show "c = d" by simp +qed simp_all + +lemma fps_exp_eq_fps_const_iff [simp]: + "fps_exp (c :: 'a :: field_char_0) = fps_const c' \ c = 0 \ c' = 1" +proof + assume "c = 0 \ c' = 1" + thus "fps_exp c = fps_const c'" by (auto simp: fps_eq_iff) +next + assume "fps_exp c = fps_const c'" + from arg_cong[of _ _ "\F. F $ 1", OF this] arg_cong[of _ _ "\F. F $ 0", OF this] + show "c = 0 \ c' = 1" by simp_all +qed + +lemma fps_exp_neq_0 [simp]: "\fps_exp (c :: 'a :: field_char_0) = 0" + unfolding fps_const_0_eq_0 [symmetric] fps_exp_eq_fps_const_iff by simp + +lemma fps_exp_eq_1_iff [simp]: "fps_exp (c :: 'a :: field_char_0) = 1 \ c = 0" + unfolding fps_const_1_eq_1 [symmetric] fps_exp_eq_fps_const_iff by simp + +lemma fps_exp_neq_numeral_iff [simp]: + "fps_exp (c :: 'a :: field_char_0) = numeral n \ c = 0 \ n = Num.One" + unfolding numeral_fps_const fps_exp_eq_fps_const_iff by simp subsubsection \Logarithmic series\ @@ -3810,61 +3863,67 @@ fps_const v + X * Abs_fps (\n. f (Suc n))" by (auto simp add: fps_eq_iff) -definition L :: "'a::field_char_0 \ 'a fps" - where "L c = fps_const (1/c) * Abs_fps (\n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)" - -lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)" +definition fps_ln :: "'a::field_char_0 \ 'a fps" + where "fps_ln c = fps_const (1/c) * Abs_fps (\n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)" + +lemma fps_ln_deriv: "fps_deriv (fps_ln c) = fps_const (1/c) * inverse (1 + X)" unfolding fps_inverse_X_plus1 - by (simp add: L_def fps_eq_iff del: of_nat_Suc) - -lemma L_nth: "L c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))" - by (simp add: L_def field_simps) - -lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def) - -lemma L_E_inv: + by (simp add: fps_ln_def fps_eq_iff del: of_nat_Suc) + +lemma fps_ln_nth: "fps_ln c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))" + by (simp add: fps_ln_def field_simps) + +lemma fps_ln_0 [simp]: "fps_ln c $ 0 = 0" by (simp add: fps_ln_def) + +lemma fps_ln_fps_exp_inv: fixes a :: "'a::field_char_0" assumes a: "a \ 0" - shows "L a = fps_inv (E a - 1)" (is "?l = ?r") + shows "fps_ln a = fps_inv (fps_exp a - 1)" (is "?l = ?r") proof - - let ?b = "E a - 1" + let ?b = "fps_exp a - 1" have b0: "?b $ 0 = 0" by simp have b1: "?b $ 1 \ 0" by (simp add: a) - have "fps_deriv (E a - 1) oo fps_inv (E a - 1) = - (fps_const a * (E a - 1) + fps_const a) oo fps_inv (E a - 1)" + have "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = + (fps_const a * (fps_exp a - 1) + fps_const a) oo fps_inv (fps_exp a - 1)" by (simp add: field_simps) also have "\ = fps_const a * (X + 1)" apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1]) apply (simp add: field_simps) done - finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" . + finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (X + 1)" . from fps_inv_deriv[OF b0 b1, unfolded eq] have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)" - using a - by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult) + using a by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult) then have "fps_deriv ?l = fps_deriv ?r" - by (simp add: fps_deriv_L add.commute fps_divide_def divide_inverse) + by (simp add: fps_ln_deriv add.commute fps_divide_def divide_inverse) then show ?thesis unfolding fps_deriv_eq_iff - by (simp add: L_nth fps_inv_def) + by (simp add: fps_ln_nth fps_inv_def) qed -lemma L_mult_add: +lemma fps_ln_mult_add: assumes c0: "c\0" and d0: "d\0" - shows "L c + L d = fps_const (c+d) * L (c*d)" + shows "fps_ln c + fps_ln d = fps_const (c+d) * fps_ln (c*d)" (is "?r = ?l") proof- from c0 d0 have eq: "1/c + 1/d = (c+d)/(c*d)" by (simp add: field_simps) have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + X)" - by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add) + by (simp add: fps_ln_deriv fps_const_add[symmetric] algebra_simps del: fps_const_add) also have "\ = fps_deriv ?l" - apply (simp add: fps_deriv_L) + apply (simp add: fps_ln_deriv) apply (simp add: fps_eq_iff eq) done finally show ?thesis unfolding fps_deriv_eq_iff by simp qed +lemma X_dvd_fps_ln [simp]: "X dvd fps_ln c" +proof - + have "fps_ln c = X * Abs_fps (\n. (-1) ^ n / (of_nat (Suc n) * c))" + by (intro fps_ext) (auto simp: fps_ln_def of_nat_diff) + thus ?thesis by simp +qed + subsubsection \Binomial series\ @@ -4458,9 +4517,9 @@ finally show ?thesis by simp qed -text \Connection to E c over the complex numbers --- Euler and de Moivre.\ - -lemma Eii_sin_cos: "E (\ * c) = fps_cos c + fps_const \ * fps_sin c" +text \Connection to @{const "fps_exp"} over the complex numbers --- Euler and de Moivre.\ + +lemma fps_exp_ii_sin_cos: "fps_exp (\ * c) = fps_cos c + fps_const \ * fps_sin c" (is "?l = ?r") proof - have "?l $ n = ?r $ n" for n @@ -4480,8 +4539,8 @@ by (simp add: fps_eq_iff) qed -lemma E_minus_ii_sin_cos: "E (- (\ * c)) = fps_cos c - fps_const \ * fps_sin c" - unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd) +lemma fps_exp_minus_ii_sin_cos: "fps_exp (- (\ * c)) = fps_cos c - fps_const \ * fps_sin c" + unfolding minus_mult_right fps_exp_ii_sin_cos by (simp add: fps_sin_even fps_cos_odd) lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)" by (fact fps_const_sub) @@ -4490,30 +4549,34 @@ by (induction c) (simp_all add: fps_const_minus [symmetric] fps_of_nat fps_const_neg [symmetric] del: fps_const_minus fps_const_neg) +lemma fps_deriv_of_int [simp]: "fps_deriv (of_int n) = 0" + by (simp add: fps_of_int [symmetric]) + lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)" by (fact numeral_fps_const) (* FIXME: duplicate *) -lemma fps_cos_Eii: "fps_cos c = (E (\ * c) + E (- \ * c)) / fps_const 2" +lemma fps_cos_fps_exp_ii: "fps_cos c = (fps_exp (\ * c) + fps_exp (- \ * c)) / fps_const 2" proof - have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" by (simp add: numeral_fps_const) show ?thesis - unfolding Eii_sin_cos minus_mult_commute + unfolding fps_exp_ii_sin_cos minus_mult_commute by (simp add: fps_sin_even fps_cos_odd numeral_fps_const fps_divide_unit fps_const_inverse th) qed -lemma fps_sin_Eii: "fps_sin c = (E (\ * c) - E (- \ * c)) / fps_const (2*\)" +lemma fps_sin_fps_exp_ii: "fps_sin c = (fps_exp (\ * c) - fps_exp (- \ * c)) / fps_const (2*\)" proof - have th: "fps_const \ * fps_sin c + fps_const \ * fps_sin c = fps_sin c * fps_const (2 * \)" by (simp add: fps_eq_iff numeral_fps_const) show ?thesis - unfolding Eii_sin_cos minus_mult_commute + unfolding fps_exp_ii_sin_cos minus_mult_commute by (simp add: fps_sin_even fps_cos_odd fps_divide_unit fps_const_inverse th) qed -lemma fps_tan_Eii: - "fps_tan c = (E (\ * c) - E (- \ * c)) / (fps_const \ * (E (\ * c) + E (- \ * c)))" - unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg +lemma fps_tan_fps_exp_ii: + "fps_tan c = (fps_exp (\ * c) - fps_exp (- \ * c)) / + (fps_const \ * (fps_exp (\ * c) + fps_exp (- \ * c)))" + unfolding fps_tan_def fps_sin_fps_exp_ii fps_cos_fps_exp_ii mult_minus_left fps_exp_neg apply (simp add: fps_divide_unit fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult) apply simp done @@ -4521,21 +4584,20 @@ lemma fps_demoivre: "(fps_cos a + fps_const \ * fps_sin a)^n = fps_cos (of_nat n * a) + fps_const \ * fps_sin (of_nat n * a)" - unfolding Eii_sin_cos[symmetric] E_power_mult + unfolding fps_exp_ii_sin_cos[symmetric] fps_exp_power_mult by (simp add: ac_simps) subsection \Hypergeometric series\ -(* TODO: Rename this *) -definition "F as bs (c::'a::{field_char_0,field}) = +definition "fps_hypergeo as bs (c::'a::{field_char_0,field}) = Abs_fps (\n. (foldl (\r a. r* pochhammer a n) 1 as * c^n) / (foldl (\r b. r * pochhammer b n) 1 bs * of_nat (fact n)))" -lemma F_nth[simp]: "F as bs c $ n = +lemma fps_hypergeo_nth[simp]: "fps_hypergeo as bs c $ n = (foldl (\r a. r* pochhammer a n) 1 as * c^n) / (foldl (\r b. r * pochhammer b n) 1 bs * of_nat (fact n))" - by (simp add: F_def) + by (simp add: fps_hypergeo_def) lemma foldl_mult_start: fixes v :: "'a::comm_ring_1" @@ -4547,15 +4609,15 @@ shows "foldr (\x r. r * f x) as v = foldl (\r x. r * f x) v as" by (induct as arbitrary: v) (auto simp add: foldl_mult_start) -lemma F_nth_alt: - "F as bs c $ n = foldr (\a r. r * pochhammer a n) as (c ^ n) / +lemma fps_hypergeo_nth_alt: + "fps_hypergeo as bs c $ n = foldr (\a r. r * pochhammer a n) as (c ^ n) / foldr (\b r. r * pochhammer b n) bs (of_nat (fact n))" by (simp add: foldl_mult_start foldr_mult_foldl) -lemma F_E[simp]: "F [] [] c = E c" +lemma fps_hypergeo_fps_exp[simp]: "fps_hypergeo [] [] c = fps_exp c" by (simp add: fps_eq_iff) -lemma F_1_0[simp]: "F [1] [] c = 1/(1 - fps_const c * X)" +lemma fps_hypergeo_1_0[simp]: "fps_hypergeo [1] [] c = 1/(1 - fps_const c * X)" proof - let ?a = "(Abs_fps (\n. 1)) oo (fps_const c * X)" have th0: "(fps_const c * X) $ 0 = 0" by simp @@ -4564,10 +4626,10 @@ fps_compose_nth power_mult_distrib cond_value_iff sum.delta' cong del: if_weak_cong) qed -lemma F_B[simp]: "F [-a] [] (- 1) = fps_binomial a" +lemma fps_hypergeo_B[simp]: "fps_hypergeo [-a] [] (- 1) = fps_binomial a" by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps) -lemma F_0[simp]: "F as bs c $ 0 = 1" +lemma fps_hypergeo_0[simp]: "fps_hypergeo as bs c $ 0 = 1" apply simp apply (subgoal_tac "\as. foldl (\(r::'a) (a::'a). r) 1 as = 1") apply auto @@ -4581,9 +4643,9 @@ by (induct as arbitrary: v w) (auto simp add: algebra_simps) -lemma F_rec: - "F as bs c $ Suc n = ((foldl (\r a. r* (a + of_nat n)) c as) / - (foldl (\r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c $ n" +lemma fps_hypergeo_rec: + "fps_hypergeo as bs c $ Suc n = ((foldl (\r a. r* (a + of_nat n)) c as) / + (foldl (\r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * fps_hypergeo as bs c $ n" apply (simp del: of_nat_Suc of_nat_add fact_Suc) apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc) unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc @@ -4612,12 +4674,12 @@ lemma XDp_fps_integral [simp]: "XDp 0 (fps_integral a c) = X * a" by (simp add: fps_eq_iff fps_integral_def) -lemma F_minus_nat: - "F [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k = +lemma fps_hypergeo_minus_nat: + "fps_hypergeo [- of_nat n] [- of_nat (n + m)] (c::'a::{field_char_0,field}) $ k = (if k \ n then pochhammer (- of_nat n) k * c ^ k / (pochhammer (- of_nat (n + m)) k * of_nat (fact k)) else 0)" - "F [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k = + "fps_hypergeo [- of_nat m] [- of_nat (m + n)] (c::'a::{field_char_0,field}) $ k = (if k \ m then pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k)) else 0)" diff -r 3c628937899d -r da25458453e3 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Apr 05 19:23:41 2017 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Thu Apr 06 16:39:13 2017 +0200 @@ -5,8 +5,8 @@ section \Abstract euclidean algorithm in euclidean (semi)rings\ theory Euclidean_Algorithm - imports "~~/src/HOL/GCD" - "~~/src/HOL/Number_Theory/Factorial_Ring" +imports + "~~/src/HOL/Number_Theory/Factorial_Ring" begin subsection \Generic construction of the (simple) euclidean algorithm\ diff -r 3c628937899d -r da25458453e3 src/HOL/Number_Theory/Factorial_Ring.thy --- a/src/HOL/Number_Theory/Factorial_Ring.thy Wed Apr 05 19:23:41 2017 +0200 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy Thu Apr 06 16:39:13 2017 +0200 @@ -8,7 +8,7 @@ theory Factorial_Ring imports Main - "~~/src/HOL/GCD" + "../GCD" "~~/src/HOL/Library/Multiset" begin diff -r 3c628937899d -r da25458453e3 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Wed Apr 05 19:23:41 2017 +0200 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Apr 06 16:39:13 2017 +0200 @@ -663,6 +663,7 @@ lemma measurable_set_pmf[measurable]: "Measurable.pred (count_space UNIV) (\x. x \ set_pmf M)" by simp + subsection \ PMFs as function \ context @@ -754,6 +755,39 @@ apply (subst lebesgue_integral_count_space_finite_support) apply (auto intro!: finite_subset[OF _ \finite A\] sum.mono_neutral_left simp: pmf_eq_0_set_pmf) done + +lemma expectation_return_pmf [simp]: + fixes f :: "'a \ 'b::{banach, second_countable_topology}" + shows "measure_pmf.expectation (return_pmf x) f = f x" + by (subst integral_measure_pmf[of "{x}"]) simp_all + +lemma pmf_expectation_bind: + fixes p :: "'a pmf" and f :: "'a \ 'b pmf" + and h :: "'b \ 'c::{banach, second_countable_topology}" + assumes "finite A" "\x. x \ A \ finite (set_pmf (f x))" "set_pmf p \ A" + shows "measure_pmf.expectation (p \ f) h = + (\a\A. pmf p a *\<^sub>R measure_pmf.expectation (f a) h)" +proof - + have "measure_pmf.expectation (p \ f) h = (\a\(\x\A. set_pmf (f x)). pmf (p \ f) a *\<^sub>R h a)" + using assms by (intro integral_measure_pmf) auto + also have "\ = (\x\(\x\A. set_pmf (f x)). (\a\A. (pmf p a * pmf (f a) x) *\<^sub>R h x))" + proof (intro sum.cong refl, goal_cases) + case (1 x) + thus ?case + by (subst pmf_bind, subst integral_measure_pmf[of A]) + (insert assms, auto simp: scaleR_sum_left) + qed + also have "\ = (\j\A. pmf p j *\<^sub>R (\i\(\x\A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))" + by (subst sum.commute) (simp add: scaleR_sum_right) + also have "\ = (\j\A. pmf p j *\<^sub>R measure_pmf.expectation (f j) h)" + proof (intro sum.cong refl, goal_cases) + case (1 x) + thus ?case + by (subst integral_measure_pmf[of "(\x\A. set_pmf (f x))"]) + (insert assms, auto simp: scaleR_sum_left) + qed + finally show ?thesis . +qed lemma continuous_on_LINT_pmf: -- \This is dominated convergence!?\ fixes f :: "'i \ 'a::topological_space \ 'b::{banach, second_countable_topology}" @@ -1725,6 +1759,14 @@ by (simp add: measure_nonneg measure_pmf.emeasure_eq_measure) end + +lemma pmf_expectation_bind_pmf_of_set: + fixes A :: "'a set" and f :: "'a \ 'b pmf" + and h :: "'b \ 'c::{banach, second_countable_topology}" + assumes "A \ {}" "finite A" "\x. x \ A \ finite (set_pmf (f x))" + shows "measure_pmf.expectation (pmf_of_set A \ f) h = + (\a\A. measure_pmf.expectation (f a) h /\<^sub>R real (card A))" + using assms by (subst pmf_expectation_bind[of A]) (auto simp: divide_simps) lemma map_pmf_of_set: assumes "finite A" "A \ {}" @@ -1773,6 +1815,16 @@ qed qed +lemma map_pmf_of_set_bij_betw: + assumes "bij_betw f A B" "A \ {}" "finite A" + shows "map_pmf f (pmf_of_set A) = pmf_of_set B" +proof - + have "map_pmf f (pmf_of_set A) = pmf_of_set (f ` A)" + by (intro map_pmf_of_set_inj assms bij_betw_imp_inj_on[OF assms(1)]) + also from assms have "f ` A = B" by (simp add: bij_betw_def) + finally show ?thesis . +qed + text \ Choosing an element uniformly at random from the union of a disjoint family of finite non-empty sets with the same size is the same as first choosing a set diff -r 3c628937899d -r da25458453e3 src/HOL/Probability/Random_Permutations.thy --- a/src/HOL/Probability/Random_Permutations.thy Wed Apr 05 19:23:41 2017 +0200 +++ b/src/HOL/Probability/Random_Permutations.thy Thu Apr 06 16:39:13 2017 +0200 @@ -176,4 +176,56 @@ using assms by (simp add: fold_bind_random_permutation_altdef bind_assoc_pmf fold_random_permutation_fold bind_return_pmf map_pmf_def) +text \ + The following useful lemma allows us to swap partitioning a set w.\,r.\,t.\ a + predicate and drawing a random permutation of that set. +\ +lemma partition_random_permutations: + assumes "finite A" + shows "map_pmf (partition P) (pmf_of_set (permutations_of_set A)) = + pair_pmf (pmf_of_set (permutations_of_set {x\A. P x})) + (pmf_of_set (permutations_of_set {x\A. \P x}))" (is "?lhs = ?rhs") +proof (rule pmf_eqI, clarify, goal_cases) + case (1 xs ys) + show ?case + proof (cases "xs \ permutations_of_set {x\A. P x} \ ys \ permutations_of_set {x\A. \P x}") + case True + let ?n1 = "card {x\A. P x}" and ?n2 = "card {x\A. \P x}" + have card_eq: "card A = ?n1 + ?n2" + proof - + have "?n1 + ?n2 = card ({x\A. P x} \ {x\A. \P x})" + using assms by (intro card_Un_disjoint [symmetric]) auto + also have "{x\A. P x} \ {x\A. \P x} = A" by blast + finally show ?thesis .. + qed + + from True have lengths [simp]: "length xs = ?n1" "length ys = ?n2" + by (auto intro!: length_finite_permutations_of_set) + have "pmf ?lhs (xs, ys) = + real (card (permutations_of_set A \ partition P -` {(xs, ys)})) / fact (card A)" + using assms by (auto simp: pmf_map measure_pmf_of_set) + also have "partition P -` {(xs, ys)} = shuffle xs ys" + using True by (intro inv_image_partition) (auto simp: permutations_of_set_def) + also have "permutations_of_set A \ shuffle xs ys = shuffle xs ys" + using True distinct_disjoint_shuffle[of xs ys] + by (auto simp: permutations_of_set_def dest: set_shuffle) + also have "card (shuffle xs ys) = length xs + length ys choose length xs" + using True by (intro card_disjoint_shuffle) (auto simp: permutations_of_set_def) + also have "length xs + length ys = card A" by (simp add: card_eq) + also have "real (card A choose length xs) = fact (card A) / (fact ?n1 * fact (card A - ?n1))" + by (subst binomial_fact) (auto intro!: card_mono assms) + also have "\ / fact (card A) = 1 / (fact ?n1 * fact ?n2)" + by (simp add: divide_simps card_eq) + also have "\ = pmf ?rhs (xs, ys)" using True assms by (simp add: pmf_pair) + finally show ?thesis . + next + case False + hence *: "xs \ permutations_of_set {x\A. P x} \ ys \ permutations_of_set {x\A. \P x}" by blast + hence eq: "permutations_of_set A \ (partition P -` {(xs, ys)}) = {}" + by (auto simp: o_def permutations_of_set_def) + from * show ?thesis + by (elim disjE) (insert assms eq, simp_all add: pmf_pair pmf_map measure_pmf_of_set) + qed +qed + end diff -r 3c628937899d -r da25458453e3 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Wed Apr 05 19:23:41 2017 +0200 +++ b/src/Pure/General/position.scala Thu Apr 06 16:39:13 2017 +0200 @@ -132,7 +132,7 @@ /* here: user output */ - def here(props: T, delimited: Boolean = false): String = + def here(props: T, delimited: Boolean = true): String = { val pos = props.filter(p => Markup.POSITION_PROPERTIES(p._1)) if (pos.isEmpty) "" diff -r 3c628937899d -r da25458453e3 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Wed Apr 05 19:23:41 2017 +0200 +++ b/src/Pure/PIDE/document.scala Thu Apr 06 16:39:13 2017 +0200 @@ -98,7 +98,6 @@ object Name { val empty = Name("") - def theory(theory: String): Name = Name(theory, "", theory) object Ordering extends scala.math.Ordering[Name] { @@ -115,7 +114,9 @@ case _ => false } + def loaded_theory: Name = Name(theory, "", theory) def is_theory: Boolean = theory.nonEmpty + override def toString: String = if (is_theory) theory else node def map(f: String => String): Name = copy(f(node), f(master_dir), theory) diff -r 3c628937899d -r da25458453e3 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Wed Apr 05 19:23:41 2017 +0200 +++ b/src/Pure/PIDE/resources.scala Thu Apr 06 16:39:13 2017 +0200 @@ -69,24 +69,19 @@ def import_name(dir: String, s: String): Document.Node.Name = { - 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 theory0 = Thy_Header.base_name(s) + val theory = + if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0 + else Long_Name.qualify(session_name, theory0) - val known_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) + session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match + { + case Some(name) if session_base.loaded_theory(name) => name.loaded_theory case Some(name) => name case None => val path = Path.explode(s) 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) } } diff -r 3c628937899d -r da25458453e3 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Wed Apr 05 19:23:41 2017 +0200 +++ b/src/Pure/Thy/present.scala Thu Apr 06 16:39:13 2017 +0200 @@ -14,32 +14,6 @@ object Present { - /* session graph */ - - def session_graph( - parent_session: String, - 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_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_base.loaded_theory(dep.name)) g - else { - val a = node(dep.name) - val bs = dep.header.imports.map({ case (name, _) => node(name) }) - ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) - } - } - } - - /* maintain chapter index -- NOT thread-safe */ private val index_path = Path.basic("index.html") diff -r 3c628937899d -r da25458453e3 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Apr 05 19:23:41 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Thu Apr 06 16:39:13 2017 +0200 @@ -42,115 +42,113 @@ loaded_theories.contains(name.theory) } - sealed case class Deps(deps: Map[String, Base]) + sealed case class Deps(sessions: Map[String, Base]) { - def is_empty: Boolean = deps.isEmpty - def apply(name: String): Base = deps(name) - def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2) + def is_empty: Boolean = sessions.isEmpty + def apply(name: String): Base = sessions(name) + def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2) } - def dependencies( + def deps(tree: Tree, progress: Progress = No_Progress, inlined_files: Boolean = false, verbose: Boolean = false, list_files: Boolean = false, check_keywords: Set[String] = Set.empty, - global_theories: Set[String] = Set.empty, - tree: Tree): Deps = + global_theories: Set[String] = Set.empty): Deps = { - Deps((Map.empty[String, Base] /: tree.topological_order)( - { case (deps, (name, info)) => - if (progress.stopped) throw Exn.Interrupt() + Deps((Map.empty[String, Base] /: tree.topological_order)({ case (sessions, (name, info)) => + if (progress.stopped) throw Exn.Interrupt() - try { - val parent_base = - info.parent match { - case None => Base.bootstrap - case Some(parent) => deps(parent) - } - val resources = new Resources(name, parent_base) + try { + val parent_base = + info.parent match { + case None => Base.bootstrap + case Some(parent) => sessions(parent) + } + val resources = new Resources(name, parent_base) - if (verbose || list_files) { - val groups = - if (info.groups.isEmpty) "" - else info.groups.mkString(" (", " ", ")") - progress.echo("Session " + info.chapter + "/" + name + groups) - } + if (verbose || list_files) { + val groups = + if (info.groups.isEmpty) "" + else info.groups.mkString(" (", " ", ")") + progress.echo("Session " + info.chapter + "/" + name + groups) + } - val thy_deps = - { - val root_theories = - info.theories.flatMap({ case (_, thys) => - thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos)) - }) - val thy_deps = resources.thy_info.dependencies(root_theories) + val thy_deps = + { + val root_theories = + info.theories.flatMap({ case (_, thys) => + thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos)) + }) + val thy_deps = resources.thy_info.dependencies(root_theories) - thy_deps.errors match { - case Nil => thy_deps - case errs => error(cat_lines(errs)) + thy_deps.errors match { + case Nil => thy_deps + case errs => error(cat_lines(errs)) + } + } + + val known_theories = + (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) => + val name = dep.name + known.get(name.theory) match { + case Some(name1) if name != name1 => + error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) + case _ => + known + (name.theory -> name) + + (Long_Name.base_name(name.theory) -> name) // legacy } - } - - val known_theories = - (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) => - val name = dep.name - known.get(name.theory) match { - case Some(name1) if name != name1 => - error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node)) - case _ => - known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name) - } - }) + }) - val loaded_theories = thy_deps.loaded_theories - val keywords = thy_deps.keywords - val syntax = thy_deps.syntax + val loaded_theories = thy_deps.loaded_theories + val keywords = thy_deps.keywords + val syntax = thy_deps.syntax - val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) - val loaded_files = - if (inlined_files) { - val pure_files = - if (is_pure(name)) { - val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1)) - val files = - roots.flatMap(root => resources.loaded_files(syntax, File.read(root))). - map(file => info.dir + Path.explode(file)) - roots ::: files - } - else Nil - pure_files ::: thy_deps.loaded_files - } - else Nil - - val all_files = - (theory_files ::: loaded_files ::: - info.files.map(file => info.dir + file) ::: - info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) + val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node)) + val loaded_files = + if (inlined_files) { + val pure_files = + if (is_pure(name)) { + val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1)) + val files = + roots.flatMap(root => resources.loaded_files(syntax, File.read(root))). + map(file => info.dir + Path.explode(file)) + roots ::: files + } + else Nil + pure_files ::: thy_deps.loaded_files + } + else Nil - if (list_files) - progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) + val all_files = + (theory_files ::: loaded_files ::: + info.files.map(file => info.dir + file) ::: + info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand) - if (check_keywords.nonEmpty) - Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files) + if (list_files) + progress.echo(cat_lines(all_files.map(_.implode).sorted.map(" " + _))) + + if (check_keywords.nonEmpty) + Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files) - val base = - Base(global_theories = global_theories, - loaded_theories = loaded_theories, - known_theories = known_theories, - keywords = keywords, - syntax = syntax, - sources = all_files.map(p => (p, SHA1.digest(p.file))), - session_graph = - Present.session_graph(info.parent getOrElse "", parent_base, thy_deps.deps)) + val base = + Base(global_theories = global_theories, + loaded_theories = loaded_theories, + known_theories = known_theories, + keywords = keywords, + syntax = syntax, + sources = all_files.map(p => (p, SHA1.digest(p.file))), + session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base)) - deps + (name -> base) - } - catch { - case ERROR(msg) => - cat_error(msg, "The error(s) above occurred in session " + - quote(name) + Position.here(info.pos)) - } - })) + sessions + (name -> base) + } + catch { + case ERROR(msg) => + cat_error(msg, "The error(s) above occurred in session " + + quote(name) + Position.here(info.pos)) + } + })) } def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base = @@ -158,7 +156,7 @@ val full_tree = load(options, dirs = dirs) val (_, tree) = full_tree.selection(sessions = List(session)) - dependencies(global_theories = full_tree.global_theories, tree = tree)(session) + deps(tree, global_theories = full_tree.global_theories)(session) } diff -r 3c628937899d -r da25458453e3 src/Pure/Thy/thy_info.scala --- a/src/Pure/Thy/thy_info.scala Wed Apr 05 19:23:41 2017 +0200 +++ b/src/Pure/Thy/thy_info.scala Thu Apr 06 16:39:13 2017 +0200 @@ -38,7 +38,7 @@ object Dependencies { - val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty) + val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty) } final class Dependencies private( @@ -46,21 +46,17 @@ val keywords: Thy_Header.Keywords, val abbrevs: Thy_Header.Abbrevs, val seen: Set[Document.Node.Name], - val seen_names: Multi_Map[String, Document.Node.Name], - val seen_positions: Multi_Map[String, Position.T]) + val seen_theory: Multi_Map[String, (Document.Node.Name, Position.T)]) { def :: (dep: Thy_Info.Dep): Dependencies = new Dependencies( dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs, - seen, seen_names, seen_positions) + seen, seen_theory) def + (thy: (Document.Node.Name, Position.T)): Dependencies = { - val (name, pos) = thy - new Dependencies(rev_deps, keywords, abbrevs, - seen + name, - seen_names + (name.theory -> name), - seen_positions + (name.theory -> pos)) + val (name, _) = thy + new Dependencies(rev_deps, keywords, abbrevs, seen + name, seen_theory + (name.theory -> thy)) } def deps: List[Thy_Info.Dep] = rev_deps.reverse @@ -70,15 +66,14 @@ val header_errors = deps.flatMap(dep => dep.header.errors) val import_errors = (for { - (theory, names) <- seen_names.iterator_list + (theory, imports) <- seen_theory.iterator_list if !resources.session_base.loaded_theories(theory) - if names.length > 1 - } yield + if imports.length > 1 + } yield { "Incoherent imports for theory " + quote(theory) + ":\n" + - cat_lines(names.flatMap(name => - seen_positions.get_list(theory).map(pos => - " " + quote(name.node) + Position.here(pos)))) - ).toList + cat_lines(imports.map({ case (name, pos) => + " " + quote(name.node) + Position.here(pos) })) + }).toList header_errors ::: import_errors } @@ -87,7 +82,9 @@ def loaded_theories: Set[String] = (resources.session_base.loaded_theories /: rev_deps) { - case (loaded, dep) => loaded + dep.name.theory + case (loaded, dep) => + loaded + dep.name.theory + + Long_Name.base_name(dep.name.theory) // legacy } def loaded_files: List[Path] = @@ -103,6 +100,26 @@ ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files } } + def session_graph(parent_session: String, parent_base: Sessions.Base): 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_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_base.loaded_theory(dep.name)) g + else { + val a = node(dep.name) + val bs = dep.header.imports.map({ case (name, _) => node(name) }) + ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) + } + } + } + override def toString: String = deps.toString } @@ -120,7 +137,8 @@ required_by(initiators) + Position.here(require_pos) val required1 = required + thy - if (required.seen(name) || resources.session_base.loaded_theory(name)) required1 + if (required.seen(name)) required + else if (resources.session_base.loaded_theory(name)) required1 else { try { if (initiators.contains(name)) error(cycle_msg(initiators)) diff -r 3c628937899d -r da25458453e3 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 05 19:23:41 2017 +0200 +++ b/src/Pure/Tools/build.scala Thu Apr 06 16:39:13 2017 +0200 @@ -395,9 +395,9 @@ val full_tree = Sessions.load(build_options, dirs, select_dirs) val (selected, selected_tree) = selection(full_tree) val deps = - Sessions.dependencies( - progress, true, verbose, list_files, check_keywords, - full_tree.global_theories, selected_tree) + Sessions.deps(selected_tree, progress = progress, inlined_files = true, + verbose = verbose, list_files = list_files, check_keywords = check_keywords, + global_theories = full_tree.global_theories) def sources_stamp(name: String): List[String] = (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted