Lemmas about analysis and permutations
authorManuel Eberl <eberlm@in.tum.de>
Tue Aug 22 21:36:48 2017 +0200 (21 months ago)
changeset 66486ffaaa83543b2
parent 66485 ddb31006e315
child 66487 307c19f24d5c
child 66488 9d83e8fe3de3
Lemmas about analysis and permutations
src/HOL/Analysis/Complex_Analysis_Basics.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Library/Permutations.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Aug 22 14:34:26 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Tue Aug 22 21:36:48 2017 +0200
     1.3 @@ -367,6 +367,14 @@
     1.4    "(\<And>i. i \<in> I \<Longrightarrow> (f i) holomorphic_on s) \<Longrightarrow> (\<lambda>x. sum (\<lambda>i. f i x) I) holomorphic_on s"
     1.5    unfolding holomorphic_on_def by (metis field_differentiable_sum)
     1.6  
     1.7 +lemma holomorphic_pochhammer [holomorphic_intros]:
     1.8 +  "f holomorphic_on A \<Longrightarrow> (\<lambda>s. pochhammer (f s) n) holomorphic_on A"
     1.9 +  by (induction n) (auto intro!: holomorphic_intros simp: pochhammer_Suc)
    1.10 +
    1.11 +lemma holomorphic_on_scaleR [holomorphic_intros]:
    1.12 +  "f holomorphic_on A \<Longrightarrow> (\<lambda>x. c *\<^sub>R f x) holomorphic_on A"
    1.13 +  by (auto simp: scaleR_conv_of_real intro!: holomorphic_intros)
    1.14 +
    1.15  lemma DERIV_deriv_iff_field_differentiable:
    1.16    "DERIV f x :> deriv f x \<longleftrightarrow> f field_differentiable at x"
    1.17    unfolding field_differentiable_def by (metis DERIV_imp_deriv)
     2.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Aug 22 14:34:26 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Aug 22 21:36:48 2017 +0200
     2.3 @@ -3928,6 +3928,166 @@
     2.4  
     2.5  subsection \<open>More facts about poles and residues\<close>
     2.6  
     2.7 +lemma zorder_cong:
     2.8 +  assumes "eventually (\<lambda>z. f z = g z) (nhds z)" "z = z'"
     2.9 +  shows   "zorder f z = zorder g z'"
    2.10 +proof -
    2.11 +  let ?P = "(\<lambda>f n h r. 0 < r \<and> h holomorphic_on cball z r \<and>
    2.12 +              (\<forall>w\<in>cball z r. f w = h w * (w - z) ^ n \<and> h w \<noteq> 0))"
    2.13 +  have "(\<lambda>n. n > 0 \<and> (\<exists>h r. ?P f n h r)) = (\<lambda>n. n > 0 \<and> (\<exists>h r. ?P g n h r))"
    2.14 +  proof (intro ext conj_cong refl iff_exI[where ?'a = "complex \<Rightarrow> complex"], goal_cases)
    2.15 +    case (1 n h)
    2.16 +    have *: "\<exists>r. ?P g n h r" if "\<exists>r. ?P f n h r" and "eventually (\<lambda>x. f x = g x) (nhds z)" for f g
    2.17 +    proof -
    2.18 +      from that(1) obtain r where "?P f n h r" by blast
    2.19 +      moreover from that(2) obtain r' where "r' > 0" "\<And>w. dist w z < r' \<Longrightarrow> f w = g w"
    2.20 +        by (auto simp: eventually_nhds_metric)
    2.21 +      hence "\<forall>w\<in>cball z (r'/2). f w = g w" by (auto simp: dist_commute)
    2.22 +      ultimately show ?thesis using \<open>r' > 0\<close>
    2.23 +        by (intro exI[of _ "min r (r'/2)"]) (auto simp: cball_def)
    2.24 +    qed
    2.25 +    from assms have eq': "eventually (\<lambda>z. g z = f z) (nhds z)"
    2.26 +      by (simp add: eq_commute)
    2.27 +    show ?case
    2.28 +      by (rule iffI[OF *[OF _ assms(1)] *[OF _ eq']])
    2.29 +  qed
    2.30 +  with assms(2) show ?thesis unfolding zorder_def by simp
    2.31 +qed
    2.32 +
    2.33 +lemma porder_cong:
    2.34 +  assumes "eventually (\<lambda>z. f z = g z) (at z)" "z = z'"
    2.35 +  shows   "porder f z = porder g z'"
    2.36 +proof -
    2.37 +  from assms(1) have *: "eventually (\<lambda>w. w \<noteq> z \<longrightarrow> f w = g w) (nhds z)"
    2.38 +    by (auto simp: eventually_at_filter)
    2.39 +  from assms(2) show ?thesis
    2.40 +    unfolding porder_def Let_def
    2.41 +    by (intro zorder_cong eventually_mono [OF *]) auto
    2.42 +qed
    2.43 +
    2.44 +lemma zer_poly_cong:
    2.45 +  assumes "eventually (\<lambda>z. f z = g z) (nhds z)" "z = z'"
    2.46 +  shows   "zer_poly f z = zer_poly g z'"
    2.47 +  unfolding zer_poly_def
    2.48 +proof (rule Eps_cong, goal_cases)
    2.49 +  case (1 h)
    2.50 +  let ?P = "\<lambda>w f. f w = h w * (w - z) ^ zorder f z \<and> h w \<noteq> 0"
    2.51 +  from assms have eq': "eventually (\<lambda>z. g z = f z) (nhds z)"
    2.52 +    by (simp add: eq_commute)
    2.53 +  have "\<exists>r>0. h holomorphic_on cball z r \<and> (\<forall>w\<in>cball z r. ?P w g)"
    2.54 +    if "r > 0" "h holomorphic_on cball z r" "\<And>w. w \<in> cball z r \<Longrightarrow> ?P w f"
    2.55 +       "eventually (\<lambda>z. f z = g z) (nhds z)" for f g r
    2.56 +  proof -
    2.57 +    from that have [simp]: "zorder f z = zorder g z"
    2.58 +      by (intro zorder_cong) auto
    2.59 +    from that(4) obtain r' where r': "r' > 0" "\<And>w. w \<in> ball z r' \<Longrightarrow> g w = f w"
    2.60 +      by (auto simp: eventually_nhds_metric ball_def dist_commute)
    2.61 +    define R where "R = min r (r' / 2)"
    2.62 +    have "R > 0" "cball z R \<subseteq> cball z r" "cball z R \<subseteq> ball z r'"
    2.63 +      using that(1) r' by (auto simp: R_def)
    2.64 +    with that(1,2,3) r'
    2.65 +    have "R > 0" "h holomorphic_on cball z R" "\<forall>w\<in>cball z R. ?P w g" 
    2.66 +      by force+
    2.67 +    thus ?thesis by blast
    2.68 +  qed
    2.69 +  from this[of _ f g] and this[of _ g f] and assms and eq'
    2.70 +    show ?case by blast
    2.71 +qed
    2.72 +      
    2.73 +lemma pol_poly_cong:
    2.74 +  assumes "eventually (\<lambda>z. f z = g z) (at z)" "z = z'"
    2.75 +  shows   "pol_poly f z = pol_poly g z'"
    2.76 +proof -
    2.77 +  from assms have *: "eventually (\<lambda>w. w \<noteq> z \<longrightarrow> f w = g w) (nhds z)"
    2.78 +    by (auto simp: eventually_at_filter)
    2.79 +  have "zer_poly (\<lambda>x. if x = z then 0 else inverse (f x)) z =
    2.80 +          zer_poly (\<lambda>x. if x = z' then 0 else inverse (g x)) z"
    2.81 +    by (intro zer_poly_cong eventually_mono[OF *] refl) (auto simp: assms(2))
    2.82 +  thus "pol_poly f z = pol_poly g z'"
    2.83 +    by (simp add: pol_poly_def Let_def o_def fun_eq_iff assms(2))
    2.84 +qed
    2.85 +
    2.86 +lemma porder_nonzero_div_power:
    2.87 +  assumes "open s" "z \<in> s" "f holomorphic_on s" "f z \<noteq> 0" "n > 0"
    2.88 +  shows   "porder (\<lambda>w. f w / (w - z) ^ n) z = n"
    2.89 +proof -
    2.90 +  let ?s' = "(f -` (-{0}) \<inter> s)"
    2.91 +  have "continuous_on s f"
    2.92 +    by (rule holomorphic_on_imp_continuous_on) fact
    2.93 +  moreover have "open (-{0::complex})" by auto
    2.94 +  ultimately have s': "open ?s'"
    2.95 +    unfolding continuous_on_open_vimage[OF \<open>open s\<close>] by blast
    2.96 +  show ?thesis unfolding Let_def porder_def
    2.97 +  proof (rule zorder_eqI)
    2.98 +    show "(\<lambda>x. inverse (f x)) holomorphic_on ?s'"
    2.99 +      using assms by (auto intro!: holomorphic_intros)
   2.100 +  qed (insert assms s', auto simp: field_simps)
   2.101 +qed
   2.102 +
   2.103 +lemma is_pole_inverse_power: "n > 0 \<Longrightarrow> is_pole (\<lambda>z::complex. 1 / (z - a) ^ n) a"
   2.104 +  unfolding is_pole_def inverse_eq_divide [symmetric]
   2.105 +  by (intro filterlim_compose[OF filterlim_inverse_at_infinity] tendsto_intros)
   2.106 +     (auto simp: filterlim_at eventually_at intro!: exI[of _ 1] tendsto_eq_intros)
   2.107 +
   2.108 +lemma is_pole_inverse: "is_pole (\<lambda>z::complex. 1 / (z - a)) a"
   2.109 +  using is_pole_inverse_power[of 1 a] by simp
   2.110 +
   2.111 +lemma is_pole_divide:
   2.112 +  fixes f :: "'a :: t2_space \<Rightarrow> 'b :: real_normed_field"
   2.113 +  assumes "isCont f z" "filterlim g (at 0) (at z)" "f z \<noteq> 0"
   2.114 +  shows   "is_pole (\<lambda>z. f z / g z) z"
   2.115 +proof -
   2.116 +  have "filterlim (\<lambda>z. f z * inverse (g z)) at_infinity (at z)"
   2.117 +    by (intro tendsto_mult_filterlim_at_infinity[of _ "f z"]
   2.118 +                 filterlim_compose[OF filterlim_inverse_at_infinity])+
   2.119 +       (insert assms, auto simp: isCont_def)
   2.120 +  thus ?thesis by (simp add: divide_simps is_pole_def)
   2.121 +qed
   2.122 +
   2.123 +lemma is_pole_basic:
   2.124 +  assumes "f holomorphic_on A" "open A" "z \<in> A" "f z \<noteq> 0" "n > 0"
   2.125 +  shows   "is_pole (\<lambda>w. f w / (w - z) ^ n) z"
   2.126 +proof (rule is_pole_divide)
   2.127 +  have "continuous_on A f" by (rule holomorphic_on_imp_continuous_on) fact
   2.128 +  with assms show "isCont f z" by (auto simp: continuous_on_eq_continuous_at)
   2.129 +  have "filterlim (\<lambda>w. (w - z) ^ n) (nhds 0) (at z)"
   2.130 +    using assms by (auto intro!: tendsto_eq_intros)
   2.131 +  thus "filterlim (\<lambda>w. (w - z) ^ n) (at 0) (at z)"
   2.132 +    by (intro filterlim_atI tendsto_eq_intros)
   2.133 +       (insert assms, auto simp: eventually_at_filter)
   2.134 +qed fact+
   2.135 +
   2.136 +lemma is_pole_basic':
   2.137 +  assumes "f holomorphic_on A" "open A" "0 \<in> A" "f 0 \<noteq> 0" "n > 0"
   2.138 +  shows   "is_pole (\<lambda>w. f w / w ^ n) 0"
   2.139 +  using is_pole_basic[of f A 0] assms by simp
   2.140 +
   2.141 +lemma zer_poly_eq:
   2.142 +  assumes "open s" "connected s" "z \<in> s" "f holomorphic_on s" "f z = 0" "\<exists>w\<in>s. f w \<noteq> 0"
   2.143 +  shows "eventually (\<lambda>w. zer_poly f z w = f w / (w - z) ^ zorder f z) (at z)"
   2.144 +proof -
   2.145 +  from zorder_exist [OF assms] obtain r where r: "r > 0" 
   2.146 +    and "\<forall>w\<in>cball z r. f w = zer_poly f z w * (w - z) ^ zorder f z" by blast
   2.147 +  hence *: "\<forall>w\<in>ball z r - {z}. zer_poly f z w = f w / (w - z) ^ zorder f z" 
   2.148 +    by (auto simp: field_simps)
   2.149 +  have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
   2.150 +    using r eventually_at_ball'[of r z UNIV] by auto
   2.151 +  thus ?thesis by eventually_elim (insert *, auto)
   2.152 +qed
   2.153 +
   2.154 +lemma pol_poly_eq:
   2.155 +  assumes "open s" "z \<in> s" "f holomorphic_on s - {z}" "is_pole f z" "\<exists>w\<in>s. f w \<noteq> 0"
   2.156 +  shows "eventually (\<lambda>w. pol_poly f z w = f w * (w - z) ^ porder f z) (at z)"
   2.157 +proof -
   2.158 +  from porder_exist[OF assms(1-4)] obtain r where r: "r > 0" 
   2.159 +    and "\<forall>w\<in>cball z r. w \<noteq> z \<longrightarrow> f w = pol_poly f z w / (w - z) ^ porder f z" by blast
   2.160 +  hence *: "\<forall>w\<in>ball z r - {z}. pol_poly f z w = f w * (w - z) ^ porder f z" 
   2.161 +    by (auto simp: field_simps)
   2.162 +  have "eventually (\<lambda>w. w \<in> ball z r - {z}) (at z)"
   2.163 +    using r eventually_at_ball'[of r z UNIV] by auto
   2.164 +  thus ?thesis by eventually_elim (insert *, auto)
   2.165 +qed
   2.166 +
   2.167  lemma lhopital_complex_simple:
   2.168    assumes "(f has_field_derivative f') (at z)" 
   2.169    assumes "(g has_field_derivative g') (at z)"
     3.1 --- a/src/HOL/Analysis/Inner_Product.thy	Tue Aug 22 14:34:26 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Tue Aug 22 21:36:48 2017 +0200
     3.3 @@ -305,6 +305,56 @@
     3.4    unfolding inner_complex_def by simp
     3.5  
     3.6  
     3.7 +lemma dot_square_norm: "inner x x = (norm x)\<^sup>2"
     3.8 +  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
     3.9 +
    3.10 +lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> inner x x = a\<^sup>2"
    3.11 +  by (auto simp add: norm_eq_sqrt_inner)
    3.12 +
    3.13 +lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> inner x x \<le> a\<^sup>2"
    3.14 +  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    3.15 +  using norm_ge_zero[of x]
    3.16 +  apply arith
    3.17 +  done
    3.18 +
    3.19 +lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> inner x x \<ge> a\<^sup>2"
    3.20 +  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    3.21 +  using norm_ge_zero[of x]
    3.22 +  apply arith
    3.23 +  done
    3.24 +
    3.25 +lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> inner x x < a\<^sup>2"
    3.26 +  by (metis not_le norm_ge_square)
    3.27 +
    3.28 +lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> inner x x > a\<^sup>2"
    3.29 +  by (metis norm_le_square not_less)
    3.30 +
    3.31 +text\<open>Dot product in terms of the norm rather than conversely.\<close>
    3.32 +
    3.33 +lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
    3.34 +  inner_scaleR_left inner_scaleR_right
    3.35 +
    3.36 +lemma dot_norm: "inner x y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
    3.37 +  by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
    3.38 +
    3.39 +lemma dot_norm_neg: "inner x y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
    3.40 +  by (simp only: power2_norm_eq_inner inner_simps inner_commute)
    3.41 +    (auto simp add: algebra_simps)
    3.42 +
    3.43 +lemma of_real_inner_1 [simp]: 
    3.44 +  "inner (of_real x) (1 :: 'a :: {real_inner, real_normed_algebra_1}) = x"
    3.45 +  by (simp add: of_real_def dot_square_norm)
    3.46 +  
    3.47 +lemma summable_of_real_iff: 
    3.48 +  "summable (\<lambda>x. of_real (f x) :: 'a :: {real_normed_algebra_1,real_inner}) \<longleftrightarrow> summable f"
    3.49 +proof
    3.50 +  assume *: "summable (\<lambda>x. of_real (f x) :: 'a)"
    3.51 +  interpret bounded_linear "\<lambda>x::'a. inner x 1"
    3.52 +    by (rule bounded_linear_inner_left)
    3.53 +  from summable [OF *] show "summable f" by simp
    3.54 +qed (auto intro: summable_of_real)
    3.55 +
    3.56 +
    3.57  subsection \<open>Gradient derivative\<close>
    3.58  
    3.59  definition
     4.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Aug 22 14:34:26 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Tue Aug 22 21:36:48 2017 +0200
     4.3 @@ -1397,43 +1397,6 @@
     4.4  lemma norm_eq_1: "norm x = 1 \<longleftrightarrow> x \<bullet> x = 1"
     4.5    by (simp add: norm_eq_sqrt_inner)
     4.6  
     4.7 -text\<open>Squaring equations and inequalities involving norms.\<close>
     4.8 -
     4.9 -lemma dot_square_norm: "x \<bullet> x = (norm x)\<^sup>2"
    4.10 -  by (simp only: power2_norm_eq_inner) (* TODO: move? *)
    4.11 -
    4.12 -lemma norm_eq_square: "norm x = a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x = a\<^sup>2"
    4.13 -  by (auto simp add: norm_eq_sqrt_inner)
    4.14 -
    4.15 -lemma norm_le_square: "norm x \<le> a \<longleftrightarrow> 0 \<le> a \<and> x \<bullet> x \<le> a\<^sup>2"
    4.16 -  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    4.17 -  using norm_ge_zero[of x]
    4.18 -  apply arith
    4.19 -  done
    4.20 -
    4.21 -lemma norm_ge_square: "norm x \<ge> a \<longleftrightarrow> a \<le> 0 \<or> x \<bullet> x \<ge> a\<^sup>2"
    4.22 -  apply (simp add: dot_square_norm abs_le_square_iff[symmetric])
    4.23 -  using norm_ge_zero[of x]
    4.24 -  apply arith
    4.25 -  done
    4.26 -
    4.27 -lemma norm_lt_square: "norm x < a \<longleftrightarrow> 0 < a \<and> x \<bullet> x < a\<^sup>2"
    4.28 -  by (metis not_le norm_ge_square)
    4.29 -
    4.30 -lemma norm_gt_square: "norm x > a \<longleftrightarrow> a < 0 \<or> x \<bullet> x > a\<^sup>2"
    4.31 -  by (metis norm_le_square not_less)
    4.32 -
    4.33 -text\<open>Dot product in terms of the norm rather than conversely.\<close>
    4.34 -
    4.35 -lemmas inner_simps = inner_add_left inner_add_right inner_diff_right inner_diff_left
    4.36 -  inner_scaleR_left inner_scaleR_right
    4.37 -
    4.38 -lemma dot_norm: "x \<bullet> y = ((norm (x + y))\<^sup>2 - (norm x)\<^sup>2 - (norm y)\<^sup>2) / 2"
    4.39 -  by (simp only: power2_norm_eq_inner inner_simps inner_commute) auto
    4.40 -
    4.41 -lemma dot_norm_neg: "x \<bullet> y = (((norm x)\<^sup>2 + (norm y)\<^sup>2) - (norm (x - y))\<^sup>2) / 2"
    4.42 -  by (simp only: power2_norm_eq_inner inner_simps inner_commute)
    4.43 -    (auto simp add: algebra_simps)
    4.44  
    4.45  text\<open>Equality of vectors in terms of @{term "op \<bullet>"} products.\<close>
    4.46  
     5.1 --- a/src/HOL/Library/Permutations.thy	Tue Aug 22 14:34:26 2017 +0200
     5.2 +++ b/src/HOL/Library/Permutations.thy	Tue Aug 22 21:36:48 2017 +0200
     5.3 @@ -204,6 +204,82 @@
     5.4    by (simp add: bij_vimage_eq_inv_image permutes_bij permutes_image[OF permutes_inv])
     5.5  
     5.6  
     5.7 +subsection \<open>Mapping permutations with bijections\<close>
     5.8 +
     5.9 +lemma bij_betw_permutations:
    5.10 +  assumes "bij_betw f A B"
    5.11 +  shows   "bij_betw (\<lambda>\<pi> x. if x \<in> B then f (\<pi> (inv_into A f x)) else x) 
    5.12 +             {\<pi>. \<pi> permutes A} {\<pi>. \<pi> permutes B}" (is "bij_betw ?f _ _")
    5.13 +proof -
    5.14 +  let ?g = "(\<lambda>\<pi> x. if x \<in> A then inv_into A f (\<pi> (f x)) else x)"
    5.15 +  show ?thesis
    5.16 +  proof (rule bij_betw_byWitness [of _ ?g], goal_cases)
    5.17 +    case 3
    5.18 +    show ?case using permutes_bij_inv_into[OF _ assms] by auto
    5.19 +  next
    5.20 +    case 4
    5.21 +    have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms)
    5.22 +    {
    5.23 +      fix \<pi> assume "\<pi> permutes B"
    5.24 +      from permutes_bij_inv_into[OF this bij_inv] and assms
    5.25 +        have "(\<lambda>x. if x \<in> A then inv_into A f (\<pi> (f x)) else x) permutes A"
    5.26 +        by (simp add: inv_into_inv_into_eq cong: if_cong)
    5.27 +    }
    5.28 +    from this show ?case by (auto simp: permutes_inv)
    5.29 +  next
    5.30 +    case 1
    5.31 +    thus ?case using assms
    5.32 +      by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left
    5.33 +               dest: bij_betwE)
    5.34 +  next
    5.35 +    case 2
    5.36 +    moreover have "bij_betw (inv_into A f) B A"
    5.37 +      by (intro bij_betw_inv_into assms)
    5.38 +    ultimately show ?case using assms
    5.39 +      by (auto simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right 
    5.40 +               dest: bij_betwE)
    5.41 +  qed
    5.42 +qed
    5.43 +
    5.44 +lemma bij_betw_derangements:
    5.45 +  assumes "bij_betw f A B"
    5.46 +  shows   "bij_betw (\<lambda>\<pi> x. if x \<in> B then f (\<pi> (inv_into A f x)) else x) 
    5.47 +             {\<pi>. \<pi> permutes A \<and> (\<forall>x\<in>A. \<pi> x \<noteq> x)} {\<pi>. \<pi> permutes B \<and> (\<forall>x\<in>B. \<pi> x \<noteq> x)}" 
    5.48 +           (is "bij_betw ?f _ _")
    5.49 +proof -
    5.50 +  let ?g = "(\<lambda>\<pi> x. if x \<in> A then inv_into A f (\<pi> (f x)) else x)"
    5.51 +  show ?thesis
    5.52 +  proof (rule bij_betw_byWitness [of _ ?g], goal_cases)
    5.53 +    case 3
    5.54 +    have "?f \<pi> x \<noteq> x" if "\<pi> permutes A" "\<And>x. x \<in> A \<Longrightarrow> \<pi> x \<noteq> x" "x \<in> B" for \<pi> x
    5.55 +      using that and assms by (metis bij_betwE bij_betw_imp_inj_on bij_betw_imp_surj_on
    5.56 +                                     inv_into_f_f inv_into_into permutes_imp_bij)
    5.57 +    with permutes_bij_inv_into[OF _ assms] show ?case by auto
    5.58 +  next
    5.59 +    case 4
    5.60 +    have bij_inv: "bij_betw (inv_into A f) B A" by (intro bij_betw_inv_into assms)
    5.61 +    have "?g \<pi> permutes A" if "\<pi> permutes B" for \<pi>
    5.62 +      using permutes_bij_inv_into[OF that bij_inv] and assms
    5.63 +      by (simp add: inv_into_inv_into_eq cong: if_cong)
    5.64 +    moreover have "?g \<pi> x \<noteq> x" if "\<pi> permutes B" "\<And>x. x \<in> B \<Longrightarrow> \<pi> x \<noteq> x" "x \<in> A" for \<pi> x
    5.65 +      using that and assms by (metis bij_betwE bij_betw_imp_surj_on f_inv_into_f permutes_imp_bij)
    5.66 +    ultimately show ?case by auto
    5.67 +  next
    5.68 +    case 1
    5.69 +    thus ?case using assms
    5.70 +      by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_left
    5.71 +                dest: bij_betwE)
    5.72 +  next
    5.73 +    case 2
    5.74 +    moreover have "bij_betw (inv_into A f) B A"
    5.75 +      by (intro bij_betw_inv_into assms)
    5.76 +    ultimately show ?case using assms
    5.77 +      by (force simp: fun_eq_iff permutes_not_in permutes_in_image bij_betw_inv_into_right 
    5.78 +                dest: bij_betwE)
    5.79 +  qed
    5.80 +qed
    5.81 +
    5.82 +
    5.83  subsection \<open>The number of permutations on a finite set\<close>
    5.84  
    5.85  lemma permutes_insert_lemma:
     6.1 --- a/src/HOL/Transcendental.thy	Tue Aug 22 14:34:26 2017 +0200
     6.2 +++ b/src/HOL/Transcendental.thy	Tue Aug 22 21:36:48 2017 +0200
     6.3 @@ -1313,6 +1313,9 @@
     6.4    for A :: "'a::real_normed_field set"
     6.5    by (intro continuous_at_imp_continuous_on ballI isCont_pochhammer)
     6.6  
     6.7 +lemmas continuous_on_pochhammer' [continuous_intros] =
     6.8 +  continuous_on_compose2[OF continuous_on_pochhammer _ subset_UNIV]
     6.9 +
    6.10  
    6.11  subsection \<open>Exponential Function\<close>
    6.12