# HG changeset patch # User eberlm # Date 1491466905 -7200 # Node ID 3f291f7a36460f16f7ed889ef0cdaa977f36fccd # Parent 27c1b5e952bdd9d15c3b0cc140418fa076ce439e# Parent a14fa655b48c9231eb6957d52d923416b2c01eeb Merged diff -r 27c1b5e952bd -r 3f291f7a3646 NEWS --- a/NEWS Tue Apr 04 17:14:41 2017 +0200 +++ b/NEWS Thu Apr 06 10:21:45 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 27c1b5e952bd -r 3f291f7a3646 src/HOL/Analysis/Harmonic_Numbers.thy --- a/src/HOL/Analysis/Harmonic_Numbers.thy Tue Apr 04 17:14:41 2017 +0200 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy Thu Apr 06 10:21:45 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 27c1b5e952bd -r 3f291f7a3646 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Tue Apr 04 17:14:41 2017 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Thu Apr 06 10:21:45 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 27c1b5e952bd -r 3f291f7a3646 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Tue Apr 04 17:14:41 2017 +0200 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Thu Apr 06 10:21:45 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 27c1b5e952bd -r 3f291f7a3646 src/HOL/Number_Theory/Factorial_Ring.thy --- a/src/HOL/Number_Theory/Factorial_Ring.thy Tue Apr 04 17:14:41 2017 +0200 +++ b/src/HOL/Number_Theory/Factorial_Ring.thy Thu Apr 06 10:21:45 2017 +0200 @@ -8,7 +8,7 @@ theory Factorial_Ring imports Main - "~~/src/HOL/GCD" + GCD "~~/src/HOL/Library/Multiset" begin diff -r 27c1b5e952bd -r 3f291f7a3646 src/HOL/Probability/Probability_Mass_Function.thy --- a/src/HOL/Probability/Probability_Mass_Function.thy Tue Apr 04 17:14:41 2017 +0200 +++ b/src/HOL/Probability/Probability_Mass_Function.thy Thu Apr 06 10:21:45 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 27c1b5e952bd -r 3f291f7a3646 src/HOL/Probability/Random_Permutations.thy --- a/src/HOL/Probability/Random_Permutations.thy Tue Apr 04 17:14:41 2017 +0200 +++ b/src/HOL/Probability/Random_Permutations.thy Thu Apr 06 10:21:45 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