--- 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.
--- 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) \<le> harm (Suc n)" by - simp
qed (simp_all add: harm_def)
+lemma harm_at_top: "filterlim (harm :: nat \<Rightarrow> real) at_top sequentially"
+proof (rule filterlim_at_top_mono)
+ show "eventually (\<lambda>n. harm n \<ge> ln (real (Suc n))) at_top"
+ using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac)
+ show "filterlim (\<lambda>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 \<open>The Euler--Mascheroni constant\<close>
--- 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) \<noteq> 0"
+proof
+ assume "numeral f = (0 :: 'a fps)"
+ from arg_cong[of _ _ "\<lambda>F. F $ 0", OF this] show False by simp
+qed
subsection \<open>The eXtractor series X\<close>
@@ -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 (\<lambda>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 (\<lambda>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 \<open>Elementary series\<close>
subsubsection \<open>Exponential series\<close>
-definition "E x = Abs_fps (\<lambda>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 (\<lambda>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 \<longleftrightarrow> a = fps_const (a$0) * E (c::'a::field_char_0)"
+lemma fps_exp_unique_ODE:
+ "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * fps_exp (c::'a::field_char_0)"
(is "?lhs \<longleftrightarrow> ?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 \<noteq> 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 \<noteq> 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 \<noteq> 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 \<noteq> 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 \<longleftrightarrow> c = (d :: 'a :: field_char_0)"
+proof
+ assume "fps_exp c = fps_exp d"
+ from arg_cong[of _ _ "\<lambda>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' \<longleftrightarrow> c = 0 \<and> c' = 1"
+proof
+ assume "c = 0 \<and> 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 _ _ "\<lambda>F. F $ 1", OF this] arg_cong[of _ _ "\<lambda>F. F $ 0", OF this]
+ show "c = 0 \<and> c' = 1" by simp_all
+qed
+
+lemma fps_exp_neq_0 [simp]: "\<not>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 \<longleftrightarrow> 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 \<longleftrightarrow> c = 0 \<and> n = Num.One"
+ unfolding numeral_fps_const fps_exp_eq_fps_const_iff by simp
subsubsection \<open>Logarithmic series\<close>
@@ -3810,61 +3863,67 @@
fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))"
by (auto simp add: fps_eq_iff)
-definition L :: "'a::field_char_0 \<Rightarrow> 'a fps"
- where "L c = fps_const (1/c) * Abs_fps (\<lambda>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 \<Rightarrow> 'a fps"
+ where "fps_ln c = fps_const (1/c) * Abs_fps (\<lambda>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 \<noteq> 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 \<noteq> 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 "\<dots> = 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\<noteq>0"
and d0: "d\<noteq>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 "\<dots> = 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 (\<lambda>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 \<open>Binomial series\<close>
@@ -4458,9 +4517,9 @@
finally show ?thesis by simp
qed
-text \<open>Connection to E c over the complex numbers --- Euler and de Moivre.\<close>
-
-lemma Eii_sin_cos: "E (\<i> * c) = fps_cos c + fps_const \<i> * fps_sin c"
+text \<open>Connection to @{const "fps_exp"} over the complex numbers --- Euler and de Moivre.\<close>
+
+lemma fps_exp_ii_sin_cos: "fps_exp (\<i> * c) = fps_cos c + fps_const \<i> * 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 (- (\<i> * c)) = fps_cos c - fps_const \<i> * 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 (- (\<i> * c)) = fps_cos c - fps_const \<i> * 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 (\<i> * c) + E (- \<i> * c)) / fps_const 2"
+lemma fps_cos_fps_exp_ii: "fps_cos c = (fps_exp (\<i> * c) + fps_exp (- \<i> * 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 (\<i> * c) - E (- \<i> * c)) / fps_const (2*\<i>)"
+lemma fps_sin_fps_exp_ii: "fps_sin c = (fps_exp (\<i> * c) - fps_exp (- \<i> * c)) / fps_const (2*\<i>)"
proof -
have th: "fps_const \<i> * fps_sin c + fps_const \<i> * fps_sin c = fps_sin c * fps_const (2 * \<i>)"
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 (\<i> * c) - E (- \<i> * c)) / (fps_const \<i> * (E (\<i> * c) + E (- \<i> * 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 (\<i> * c) - fps_exp (- \<i> * c)) /
+ (fps_const \<i> * (fps_exp (\<i> * c) + fps_exp (- \<i> * 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 \<i> * fps_sin a)^n =
fps_cos (of_nat n * a) + fps_const \<i> * 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 \<open>Hypergeometric series\<close>
-(* 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 (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
(foldl (\<lambda>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 (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
(foldl (\<lambda>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 (\<lambda>x r. r * f x) as v = foldl (\<lambda>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 (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
+lemma fps_hypergeo_nth_alt:
+ "fps_hypergeo as bs c $ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
foldr (\<lambda>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 (\<lambda>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 "\<forall>as. foldl (\<lambda>(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 (\<lambda>r a. r* (a + of_nat n)) c as) /
- (foldl (\<lambda>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 (\<lambda>r a. r* (a + of_nat n)) c as) /
+ (foldl (\<lambda>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 \<le> 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 \<le> m then
pochhammer (- of_nat m) k * c ^ k / (pochhammer (- of_nat (m + n)) k * of_nat (fact k))
else 0)"
--- 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 \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close>
theory Euclidean_Algorithm
- imports "~~/src/HOL/GCD"
- "~~/src/HOL/Number_Theory/Factorial_Ring"
+imports
+ "~~/src/HOL/Number_Theory/Factorial_Ring"
begin
subsection \<open>Generic construction of the (simple) euclidean algorithm\<close>
--- 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
--- 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) (\<lambda>x. x \<in> set_pmf M)"
by simp
+
subsection \<open> PMFs as function \<close>
context
@@ -754,6 +755,39 @@
apply (subst lebesgue_integral_count_space_finite_support)
apply (auto intro!: finite_subset[OF _ \<open>finite A\<close>] sum.mono_neutral_left simp: pmf_eq_0_set_pmf)
done
+
+lemma expectation_return_pmf [simp]:
+ fixes f :: "'a \<Rightarrow> '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 \<Rightarrow> 'b pmf"
+ and h :: "'b \<Rightarrow> 'c::{banach, second_countable_topology}"
+ assumes "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (set_pmf (f x))" "set_pmf p \<subseteq> A"
+ shows "measure_pmf.expectation (p \<bind> f) h =
+ (\<Sum>a\<in>A. pmf p a *\<^sub>R measure_pmf.expectation (f a) h)"
+proof -
+ have "measure_pmf.expectation (p \<bind> f) h = (\<Sum>a\<in>(\<Union>x\<in>A. set_pmf (f x)). pmf (p \<bind> f) a *\<^sub>R h a)"
+ using assms by (intro integral_measure_pmf) auto
+ also have "\<dots> = (\<Sum>x\<in>(\<Union>x\<in>A. set_pmf (f x)). (\<Sum>a\<in>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 "\<dots> = (\<Sum>j\<in>A. pmf p j *\<^sub>R (\<Sum>i\<in>(\<Union>x\<in>A. set_pmf (f x)). pmf (f j) i *\<^sub>R h i))"
+ by (subst sum.commute) (simp add: scaleR_sum_right)
+ also have "\<dots> = (\<Sum>j\<in>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 "(\<Union>x\<in>A. set_pmf (f x))"])
+ (insert assms, auto simp: scaleR_sum_left)
+ qed
+ finally show ?thesis .
+qed
lemma continuous_on_LINT_pmf: -- \<open>This is dominated convergence!?\<close>
fixes f :: "'i \<Rightarrow> 'a::topological_space \<Rightarrow> '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 \<Rightarrow> 'b pmf"
+ and h :: "'b \<Rightarrow> 'c::{banach, second_countable_topology}"
+ assumes "A \<noteq> {}" "finite A" "\<And>x. x \<in> A \<Longrightarrow> finite (set_pmf (f x))"
+ shows "measure_pmf.expectation (pmf_of_set A \<bind> f) h =
+ (\<Sum>a\<in>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 \<noteq> {}"
@@ -1773,6 +1815,16 @@
qed
qed
+lemma map_pmf_of_set_bij_betw:
+ assumes "bij_betw f A B" "A \<noteq> {}" "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 \<open>
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
--- 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 \<open>
+ The following useful lemma allows us to swap partitioning a set w.\,r.\,t.\ a
+ predicate and drawing a random permutation of that set.
+\<close>
+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\<in>A. P x}))
+ (pmf_of_set (permutations_of_set {x\<in>A. \<not>P x}))" (is "?lhs = ?rhs")
+proof (rule pmf_eqI, clarify, goal_cases)
+ case (1 xs ys)
+ show ?case
+ proof (cases "xs \<in> permutations_of_set {x\<in>A. P x} \<and> ys \<in> permutations_of_set {x\<in>A. \<not>P x}")
+ case True
+ let ?n1 = "card {x\<in>A. P x}" and ?n2 = "card {x\<in>A. \<not>P x}"
+ have card_eq: "card A = ?n1 + ?n2"
+ proof -
+ have "?n1 + ?n2 = card ({x\<in>A. P x} \<union> {x\<in>A. \<not>P x})"
+ using assms by (intro card_Un_disjoint [symmetric]) auto
+ also have "{x\<in>A. P x} \<union> {x\<in>A. \<not>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 \<inter> 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 \<inter> 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 "\<dots> / fact (card A) = 1 / (fact ?n1 * fact ?n2)"
+ by (simp add: divide_simps card_eq)
+ also have "\<dots> = pmf ?rhs (xs, ys)" using True assms by (simp add: pmf_pair)
+ finally show ?thesis .
+ next
+ case False
+ hence *: "xs \<notin> permutations_of_set {x\<in>A. P x} \<or> ys \<notin> permutations_of_set {x\<in>A. \<not>P x}" by blast
+ hence eq: "permutations_of_set A \<inter> (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
--- 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) ""
--- 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)
--- 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)
}
}
--- 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")
--- 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)
}
--- 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))
--- 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