diff --git a/thys/Cotangent_PFD_Formula/Cotangent_PFD_Formula.thy b/thys/Cotangent_PFD_Formula/Cotangent_PFD_Formula.thy
new file mode 100644
--- /dev/null
+++ b/thys/Cotangent_PFD_Formula/Cotangent_PFD_Formula.thy
@@ -0,0 +1,800 @@
+(*
+  File:     Cotangent_PFD_Formula.thy
+  Author:   Manuel Eberl, University of Innsbruck
+
+  A proof of the "partial fraction decomposition"-style sum formula for the contangent function.
+*)
+section \<open>The Partial-Fraction Formula for the Cotangent Function\<close>
+theory Cotangent_PFD_Formula
+  imports "HOL-Complex_Analysis.Complex_Analysis" "HOL-Real_Asymp.Real_Asymp" 
+begin
+
+subsection \<open>Auxiliary lemmas\<close>
+
+(* TODO Move *)
+text \<open>
+  The following variant of the comparison test for showing summability allows us to use
+  a `Big-O' estimate, which works well together with Isabelle's automation for real asymptotics.
+\<close>
+lemma summable_comparison_test_bigo:
+  fixes f :: "nat \<Rightarrow> real"
+  assumes "summable (\<lambda>n. norm (g n))" "f \<in> O(g)"
+  shows   "summable f"
+proof -
+  from \<open>f \<in> O(g)\<close> obtain C where C: "eventually (\<lambda>x. norm (f x) \<le> C * norm (g x)) at_top"
+    by (auto elim: landau_o.bigE)
+  thus ?thesis
+    by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
+qed
+
+lemma uniformly_on_image:
+  "uniformly_on (f ` A) g = filtercomap (\<lambda>h. h \<circ> f) (uniformly_on A (g \<circ> f))"
+  unfolding uniformly_on_def by (simp add: filtercomap_INF)
+
+lemma uniform_limit_image:
+  "uniform_limit (f ` A) g h F \<longleftrightarrow> uniform_limit A (\<lambda>x y. g x (f y)) (\<lambda>x. h (f x)) F"
+  by (simp add: uniformly_on_image filterlim_filtercomap_iff o_def)
+
+lemma Ints_add_iff1 [simp]: "x \<in> \<int> \<Longrightarrow> x + y \<in> \<int> \<longleftrightarrow> y \<in> \<int>"
+  by (metis Ints_add Ints_diff add.commute add_diff_cancel_right')
+
+lemma Ints_add_iff2 [simp]: "y \<in> \<int> \<Longrightarrow> x + y \<in> \<int> \<longleftrightarrow> x \<in> \<int>"
+  by (metis Ints_add Ints_diff add_diff_cancel_right')
+
+text \<open>
+  If a set is discrete (i.e. the difference between any two points is bounded from below),
+  it has no limit points:
+\<close>
+lemma discrete_imp_not_islimpt:
+  assumes e: "0 < e"
+    and d: "\<forall>x \<in> S. \<forall>y \<in> S. dist y x < e \<longrightarrow> y = x"
+  shows "\<not>x islimpt S"
+proof
+  assume "x islimpt S"
+  hence "x islimpt S - {x}"
+    by (meson islimpt_punctured)
+  moreover from assms have "closed (S - {x})"
+    by (intro discrete_imp_closed) auto
+  ultimately show False
+    unfolding closed_limpt by blast
+qed
+
+text \<open>
+  In particular, the integers have no limit point:
+\<close>
+lemma Ints_not_limpt: "\<not>((x :: 'a :: real_normed_algebra_1) islimpt \<int>)"
+  by (rule discrete_imp_not_islimpt[of 1]) (auto elim!: Ints_cases simp: dist_of_int)
+
+text \<open>
+  The following lemma allows evaluating telescoping sums of the form
+  \[\sum\limits_{n=0}^\infty \left(f(n) - f(n + k)\right)\]
+  where $f(n) \longrightarrow 0$, i.e.\ where all terms except for the first \<open>k\<close> are
+  cancelled by later summands.
+\<close>
+lemma sums_long_telescope:
+  fixes f :: "nat \<Rightarrow> 'a :: {topological_group_add, topological_comm_monoid_add, ab_group_add}"
+  assumes lim: "f \<longlonglongrightarrow> 0"
+  shows "(\<lambda>n. f n - f (n + c)) sums (\<Sum>k<c. f k)" (is "_ sums ?S")
+proof -
+  thm tendsto_diff
+  have "(\<lambda>N. ?S - (\<Sum>n<c. f (N + n))) \<longlonglongrightarrow> ?S - 0"
+    by (intro tendsto_intros tendsto_null_sum filterlim_compose[OF assms]; real_asymp)
+  hence "(\<lambda>N. ?S - (\<Sum>n<c. f (N + n))) \<longlonglongrightarrow> ?S"
+    by simp
+  moreover have "eventually (\<lambda>N. ?S - (\<Sum>n<c. f (N + n)) = (\<Sum>n<N. f n - f (n + c))) sequentially"
+    using eventually_ge_at_top[of c]
+  proof eventually_elim
+    case (elim N)
+    have "(\<Sum>n<N. f n - f (n + c)) = (\<Sum>n<N. f n) - (\<Sum>n<N. f (n + c))"
+      by (simp only: sum_subtractf)
+    also have "(\<Sum>n<N. f n) = (\<Sum>n\<in>{..<c} \<union> {c..<N}. f n)"
+      using elim by (intro sum.cong) auto
+    also have "\<dots> = (\<Sum>n<c. f n) + (\<Sum>n\<in>{c..<N}. f n)"
+      by (subst sum.union_disjoint) auto
+    also have "(\<Sum>n<N. f (n + c)) = (\<Sum>n\<in>{c..<N+c}. f n)"
+      using elim by (intro sum.reindex_bij_witness[of _ "\<lambda>n. n - c" "\<lambda>n. n + c"]) auto
+    also have "\<dots> = (\<Sum>n\<in>{c..<N}\<union>{N..<N+c}. f n)"
+      using elim by (intro sum.cong) auto
+    also have "\<dots> = (\<Sum>n\<in>{c..<N}. f n) + (\<Sum>n\<in>{N..<N+c}. f n)"
+      by (subst sum.union_disjoint) auto
+    also have "(\<Sum>n\<in>{N..<N+c}. f n) = (\<Sum>n<c. f (N + n))"
+      by (intro sum.reindex_bij_witness[of _ "\<lambda>n. n + N" "\<lambda>n. n - N"]) auto
+    finally show ?case
+      by simp
+  qed
+  ultimately show ?thesis
+    unfolding sums_def by (rule Lim_transform_eventually)
+qed
+
+
+subsection \<open>Definition of auxiliary function\<close>
+
+text \<open>
+  The following function is the infinite sum appearing on the right-hand side of the
+  cotangent formula. It can be written either as
+  \[\sum_{n=1}^\infty\left(\frac{1}{x + n} + \frac{1}{x - n}\right)\]
+  or as
+  \[2x \sum_{n=1}^\infty \frac{1}{x^2 - n^2}\ .\]
+\<close>
+definition cot_pfd :: "'a :: {real_normed_field, banach} \<Rightarrow> 'a" where
+  "cot_pfd x = (\<Sum>n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
+
+text \<open>
+  The sum in the definition of \<^const>\<open>cot_pfd\<close> converges uniformly on compact sets.
+  This implies, in particular, that \<^const>\<open>cot_pfd\<close> is holomorphic (and thus also continuous).
+\<close>
+lemma uniform_limit_cot_pfd_complex:
+  assumes "R \<ge> 0"
+  shows   "uniform_limit (cball 0 R :: complex set)
+             (\<lambda>N x. \<Sum>n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) cot_pfd sequentially"
+  unfolding cot_pfd_def
+proof (rule Weierstrass_m_test_ev)
+  have "eventually (\<lambda>N. of_nat (N + 1) > R) at_top"
+    by real_asymp
+  thus "\<forall>\<^sub>F N in sequentially. \<forall>(x::complex)\<in>cball 0 R. norm (2 * x / (x ^ 2 - of_nat (Suc N) ^ 2)) \<le>
+          2 * R / (real (N + 1) ^ 2 - R ^ 2)"
+  proof eventually_elim
+    case (elim N)
+    show ?case
+    proof safe
+      fix x :: complex assume x: "x \<in> cball 0 R"
+      have "(1 + real N)\<^sup>2 - R\<^sup>2 \<le> norm ((1 + of_nat N :: complex) ^ 2) - norm (x ^ 2)"
+        using x by (auto intro: power_mono simp: norm_power simp flip: of_nat_Suc)
+      also have "\<dots> \<le> norm (x\<^sup>2 - (1 + of_nat N :: complex)\<^sup>2)"
+        by (metis norm_minus_commute norm_triangle_ineq2)
+      finally show "norm (2 * x / (x\<^sup>2 - (of_nat (Suc N))\<^sup>2)) \<le> 2 * R / (real (N + 1) ^ 2 - R ^ 2)"
+        unfolding norm_mult norm_divide using \<open>R \<ge> 0\<close> x elim
+        by (intro mult_mono frac_le) (auto intro: power_strict_mono)
+    qed
+  qed
+next
+  show "summable (\<lambda>N. 2 * R / (real (N + 1) ^ 2 - R ^ 2))"
+  proof (rule summable_comparison_test_bigo)
+    show "(\<lambda>N. 2 * R / (real (N + 1) ^ 2 - R ^ 2)) \<in> O(\<lambda>N. 1 / real N ^ 2)"
+      by real_asymp
+  next
+    show "summable (\<lambda>n. norm (1 / real n ^ 2))"
+      using inverse_power_summable[of 2] by (simp add: field_simps)
+  qed
+qed
+
+lemma sums_cot_pfd_complex:
+  fixes x :: complex
+  shows "(\<lambda>n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) sums cot_pfd x"
+  using tendsto_uniform_limitI[OF uniform_limit_cot_pfd_complex[of "norm x"], of x]
+  by (simp add: sums_def)
+
+lemma sums_cot_pfd_complex':
+  fixes x :: complex
+  assumes "x \<notin> \<int>"
+  shows   "(\<lambda>n. 1 / (x + of_nat (Suc n)) + 1 / (x - of_nat (Suc n))) sums cot_pfd x"
+proof -
+  have "(\<lambda>n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) sums cot_pfd x"
+    by (rule sums_cot_pfd_complex)
+  also have "(\<lambda>n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) = 
+             (\<lambda>n. 1 / (x + of_nat (Suc n)) + 1 / (x - of_nat (Suc n)))" (is "?lhs = ?rhs")
+  proof
+    fix n :: nat
+    have neq1: "x + of_nat (Suc n) \<noteq> 0"
+      using assms by (metis Ints_0 Ints_add_iff2 Ints_of_nat)
+    have neq2: "x - of_nat (Suc n) \<noteq> 0"
+      using assms by force
+    have neq3: "x ^ 2 - of_nat (Suc n) ^ 2 \<noteq> 0"
+     using assms by (metis Ints_of_nat eq_iff_diff_eq_0 minus_in_Ints_iff power2_eq_iff)
+    show "?lhs n = ?rhs n" using neq1 neq2 neq3
+      by (simp add: divide_simps del: of_nat_Suc) (auto simp: power2_eq_square algebra_simps)
+  qed
+  finally show ?thesis .
+qed
+
+lemma summable_cot_pfd_complex:
+  fixes x :: complex
+  shows "summable (\<lambda>n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
+  using sums_cot_pfd_complex[of x] by (simp add: sums_iff)
+
+lemma summable_cot_pfd_real:
+  fixes x :: real
+  shows "summable (\<lambda>n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
+proof -
+  have "summable (\<lambda>n. complex_of_real (2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)))"
+    using summable_cot_pfd_complex[of "of_real x"] by simp
+  also have "?this \<longleftrightarrow> ?thesis"
+    by (rule summable_of_real_iff)
+  finally show ?thesis .
+qed
+
+lemma sums_cot_pfd_real:
+  fixes x :: real
+  shows "(\<lambda>n. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) sums cot_pfd x"
+  using summable_cot_pfd_real[of x] by (simp add: cot_pfd_def sums_iff)
+
+lemma cot_pfd_complex_of_real [simp]: "cot_pfd (complex_of_real x) = of_real (cot_pfd x)"
+  using sums_of_real[OF sums_cot_pfd_real[of x], where ?'a = complex]
+        sums_cot_pfd_complex[of "of_real x"] sums_unique2 by auto
+
+lemma uniform_limit_cot_pfd_real:
+  assumes "R \<ge> 0"
+  shows   "uniform_limit (cball 0 R :: real set)
+             (\<lambda>N x. \<Sum>n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)) cot_pfd sequentially"
+proof -
+  have "uniform_limit (cball 0 R)
+          (\<lambda>N x. Re (\<Sum>n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))) (\<lambda>x. Re (cot_pfd x)) sequentially"
+    by (intro uniform_limit_intros uniform_limit_cot_pfd_complex assms)
+  hence "uniform_limit (of_real ` cball 0 R)
+          (\<lambda>N x. Re (\<Sum>n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))) (\<lambda>x. Re (cot_pfd x)) sequentially"
+    by (rule uniform_limit_on_subset) auto
+  thus ?thesis
+    by (simp add: uniform_limit_image)
+qed
+
+
+subsection \<open>Holomorphicity and continuity\<close>
+
+lemma holomorphic_on_cot_pfd [holomorphic_intros]:
+  assumes "A \<subseteq> -(\<int>-{0})"
+  shows   "cot_pfd holomorphic_on A"
+proof -
+  have *: "open (-(\<int>-{0}) :: complex set)"
+    by (intro open_Compl closed_subset_Ints) auto
+  define f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+    where "f = (\<lambda>N x. \<Sum>n<N. 2 * x / (x ^ 2 - of_nat (Suc n) ^ 2))"
+  have "cot_pfd holomorphic_on -(\<int>-{0})"
+  proof (rule holomorphic_uniform_sequence[OF *])
+    fix n :: nat
+    have **: "x\<^sup>2 - (of_nat (Suc n))\<^sup>2 \<noteq> 0" if "x \<in> -(\<int>-{0})" for x :: complex and n :: nat
+    proof
+      assume "x\<^sup>2 - (of_nat (Suc n))\<^sup>2 = 0"
+      hence "(of_nat (Suc n))\<^sup>2 = x\<^sup>2"
+        by algebra
+      hence "x = of_nat (Suc n) \<or> x = -of_nat (Suc n)"
+        by (subst (asm) eq_commute, subst (asm) power2_eq_iff) auto
+      moreover have "(of_nat (Suc n) :: complex) \<in> \<int>" "(-of_nat (Suc n) :: complex) \<in> \<int>"
+        by (intro Ints_minus Ints_of_nat)+
+      ultimately show False using that
+        by (auto simp del: of_nat_Suc)
+    qed
+    show "f n holomorphic_on -(\<int> - {0})"
+      unfolding f_def by (intro holomorphic_intros **)
+  next
+    fix z :: complex assume z: "z \<in> -(\<int> - {0})"
+    from * z obtain r where r: "r > 0" "cball z r \<subseteq> -(\<int>-{0})"
+      using open_contains_cball by blast
+    have "uniform_limit (cball z r) f cot_pfd sequentially"
+      using uniform_limit_cot_pfd_complex[of "norm z + r"] unfolding f_def
+    proof (rule uniform_limit_on_subset)
+      show "cball z r \<subseteq> cball 0 (norm z + r)"
+        unfolding cball_subset_cball_iff by (auto simp: dist_norm)
+    qed (use \<open>r > 0\<close> in auto)
+    with r show "\<exists>d>0. cball z d \<subseteq> - (\<int> - {0}) \<and> uniform_limit (cball z d) f cot_pfd sequentially"
+      by blast
+  qed
+  thus ?thesis
+    by (rule holomorphic_on_subset) fact
+qed
+
+lemma continuous_on_cot_pfd_complex [continuous_intros]:
+  assumes "A \<subseteq> -(\<int>-{0})"
+  shows   "continuous_on A (cot_pfd :: complex \<Rightarrow> complex)"
+  by (rule holomorphic_on_imp_continuous_on holomorphic_intros assms)+
+
+lemma continuous_on_cot_pfd_real [continuous_intros]:
+  assumes "A \<subseteq> -(\<int>-{0})"
+  shows   "continuous_on A (cot_pfd :: real \<Rightarrow> real)"
+proof -
+  have "continuous_on A (Re \<circ> cot_pfd \<circ> of_real)"
+    by (intro continuous_intros) (use assms in auto)
+  also have "Re \<circ> cot_pfd \<circ> of_real = cot_pfd"
+    by auto
+  finally show ?thesis .
+qed
+
+
+subsection \<open>Functional equations\<close>
+
+text \<open>
+  In this section, we will show three few functional equations for the function \<^const>\<open>cot_pfd\<close>.
+  The first one is trivial; the other two are a bit tedious and not very insightful, so I
+  will not comment on them.
+\<close>
+
+text \<open>\<^const>\<open>cot_pfd\<close> is an odd function:\<close>
+lemma cot_pfd_complex_minus [simp]: "cot_pfd (-x :: complex) = -cot_pfd x"
+proof -
+  have "(\<lambda>n. 2 * (-x) / ((-x) ^ 2 - of_nat (Suc n) ^ 2)) =
+        (\<lambda>n. - (2 * x / (x ^ 2 - of_nat (Suc n) ^ 2)))"
+    by simp
+  also have "\<dots> sums -cot_pfd x"
+    by (intro sums_minus sums_cot_pfd_complex)
+  finally show ?thesis
+    using sums_cot_pfd_complex[of "-x"] sums_unique2 by blast
+qed
+
+lemma cot_pfd_real_minus [simp]: "cot_pfd (-x :: real) = -cot_pfd x"
+  using cot_pfd_complex_minus[of "of_real x"]
+  unfolding of_real_minus [symmetric] cot_pfd_complex_of_real of_real_eq_iff .
+
+text \<open>\<^const>\<open>cot_pfd\<close> is periodic with period 1:\<close>
+lemma cot_pfd_plus_1_complex:
+  assumes "x \<notin> \<int>"
+  shows   "cot_pfd (x + 1 :: complex) = cot_pfd x - 1 / (x + 1) + 1 / x"
+proof -
+  have *: "x ^ 2 \<noteq> of_nat n ^ 2" if "x \<notin> \<int>" for x :: complex and n
+    using that by (metis Ints_of_nat minus_in_Ints_iff power2_eq_iff)
+  have **: "x + of_nat n \<noteq> 0" if "x \<notin> \<int>" for x :: complex and n
+    using that by (metis Ints_0 Ints_add_iff2 Ints_of_nat)
+  have [simp]: "x \<noteq> 0"
+    using assms by auto
+  have [simp]: "x + 1 \<noteq> 0"
+    using assms by (metis "**" of_nat_1)
+  have [simp]: "x + 2 \<noteq> 0"
+    using **[of x 2] assms by simp
+
+  have lim: "(\<lambda>n. 1 / (x + of_nat (Suc n))) \<longlonglongrightarrow> 0"
+    by (intro tendsto_divide_0[OF tendsto_const] tendsto_add_filterlim_at_infinity[OF tendsto_const]
+              filterlim_compose[OF tendsto_of_nat] filterlim_Suc)
+  have sum1: "(\<lambda>n. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2))) sums
+          (\<Sum>n<2. 1 / (x + of_nat (Suc n)))"
+    using sums_long_telescope[OF lim, of 2] by (simp add: algebra_simps)
+
+  have "(\<lambda>n. 2 * x / (x\<^sup>2 - (of_nat (Suc n))\<^sup>2) - 2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc (Suc n)))\<^sup>2))
+          sums (cot_pfd x - (cot_pfd (x + 1) - 2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc 0) ^ 2))))"
+    using sums_cot_pfd_complex[of "x + 1"]
+    by (intro sums_diff sums_cot_pfd_complex, subst sums_Suc_iff) auto
+  also have "2 * (x + 1) / ((x + 1)^2 - (of_nat (Suc 0) ^ 2)) = 2 * (x + 1) / (x * (x + 2))"
+    by (simp add: algebra_simps power2_eq_square)
+  also have "(\<lambda>n. 2 * x / (x\<^sup>2 - (of_nat (Suc n))\<^sup>2) -
+                  2 * (x + 1) / ((x + 1)\<^sup>2 - (of_nat (Suc (Suc n)))\<^sup>2)) =
+             (\<lambda>n. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2)))"
+    using *[of x] *[of "x + 1"] **[of x] **[of "x + 1"] assms
+    apply (intro ext)
+    apply (simp add: divide_simps del: of_nat_add of_nat_Suc)
+    apply (simp add: algebra_simps power2_eq_square)
+    done
+  finally have sum2: "(\<lambda>n. 1 / (x + of_nat (Suc n)) - 1 / (x + of_nat (Suc n + 2))) sums
+                         (cot_pfd x - cot_pfd (x + 1) + 2 * (x + 1) / (x * (x + 2)))"
+    by (simp add: algebra_simps)
+
+  have "cot_pfd x - cot_pfd (x + 1) + 2 * (x + 1) / (x * (x + 2)) =
+        (\<Sum>n<2. 1 / (x + of_nat (Suc n)))"
+    using sum1 sum2 sums_unique2 by blast
+  hence "cot_pfd x - cot_pfd (x + 1) = -2 * (x + 1) / (x * (x + 2)) + 1 / (x + 1) + 1 / (x + 2)"
+    by (simp add: eval_nat_numeral divide_simps) algebra?
+  also have "\<dots> = 1 / (x + 1) - 1 / x"
+    by (simp add: divide_simps) algebra?
+  finally show ?thesis
+    by algebra
+qed
+   
+lemma cot_pfd_plus_1_real: 
+  assumes "x \<notin> \<int>"
+  shows   "cot_pfd (x + 1 :: real) = cot_pfd x - 1 / (x + 1) + 1 / x"
+proof -
+  have "cot_pfd (complex_of_real (x + 1)) = cot_pfd (of_real x) - 1 / (of_real x + 1) + 1 / of_real x"
+    using cot_pfd_plus_1_complex[of x] assms by simp
+  also have "\<dots> = complex_of_real (cot_pfd x - 1 / (x + 1) + 1 / x)"
+    by simp
+  finally show ?thesis
+    unfolding cot_pfd_complex_of_real of_real_eq_iff .
+qed
+
+text \<open>
+  \<^const>\<open>cot_pfd\<close> satisfies the following functional equation:
+  \[2 f(x) = f\left(\frac{x}{2}\right) + f\left(\frac{x+1}{2}\right) + \frac{2}{x+1}\]
+\<close>
+lemma cot_pfd_funeq_complex:
+  fixes x :: complex
+  assumes "x \<notin> \<int>"
+  shows   "2 * cot_pfd x = cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1)"
+proof -
+  define f :: "complex \<Rightarrow> nat \<Rightarrow> complex" where "f = (\<lambda>x n. 1 / (x + of_nat (Suc n)))"
+  define g :: "complex \<Rightarrow> nat \<Rightarrow> complex" where "g = (\<lambda>x n. 1 / (x - of_nat (Suc n)))"
+  define h :: "complex \<Rightarrow> nat \<Rightarrow> complex" where "h = (\<lambda>x n. 2 * (f x (n + 1) + g x n))"
+
+  have sums: "(\<lambda>n. f x n + g x n) sums cot_pfd x" if "x \<notin> \<int>" for x
+    unfolding f_def g_def by (intro sums_cot_pfd_complex' that)
+
+  have "x / 2 \<notin> \<int>"
+  proof
+    assume "x / 2 \<in> \<int>"
+    hence "2 * (x / 2) \<in> \<int>"
+      by (intro Ints_mult) auto
+    thus False using assms by simp
+  qed
+  moreover have "(x + 1) / 2 \<notin> \<int>"
+  proof
+    assume "(x + 1) / 2 \<in> \<int>"
+    hence "2 * ((x + 1) / 2) - 1 \<in> \<int>"
+      by (intro Ints_mult Ints_diff) auto
+    thus False using assms by (simp add: field_simps)
+  qed
+  ultimately have "(\<lambda>n. (f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n)) sums
+                     (cot_pfd (x / 2) + cot_pfd ((x + 1) / 2))"
+    by (intro sums_add sums)
+
+  also have "(\<lambda>n. (f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n)) =
+             (\<lambda>n. h x (2 * n) + h x (2 * n + 1))"
+  proof
+    fix n :: nat
+    have "(f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n) =
+          (f (x / 2) n + f ((x+1) / 2) n) + (g (x / 2) n + g ((x+1) / 2) n)"
+      by algebra
+    also have "f (x / 2) n + f ((x+1) / 2) n = 2 * (f x (2 * n + 1) + f x (2 * n + 2))"
+      by (simp add: f_def field_simps)
+    also have "g (x / 2) n + g ((x+1) / 2) n = 2 * (g x (2 * n) + g x (2 * n + 1))"
+      by (simp add: g_def field_simps)
+    also have "2 * (f x (2 * n + 1) + f x (2 * n + 2)) + \<dots> =
+               h x (2 * n) + h x (2 * n + 1)"
+      unfolding h_def by (simp add: algebra_simps)
+    finally show "(f (x / 2) n + g (x / 2) n) + (f ((x+1) / 2) n + g ((x+1) / 2) n) =
+                  h x (2 * n) + h x (2 * n + 1)" .
+  qed
+  finally have sum1:
+    "(\<lambda>n. h x (2 * n) + h x (2 * n + 1)) sums (cot_pfd (x / 2) + cot_pfd ((x + 1) / 2))" .
+
+  have "f x \<longlonglongrightarrow> 0" unfolding f_def
+    by (intro tendsto_divide_0[OF tendsto_const]
+              tendsto_add_filterlim_at_infinity[OF tendsto_const]
+              filterlim_compose[OF tendsto_of_nat] filterlim_Suc)
+  hence "(\<lambda>n. 2 * (f x n + g x n) + 2 * (f x (Suc n) - f x n)) sums (2 * cot_pfd x + 2 * (0 - f x 0))"
+    by (intro sums_add sums sums_mult telescope_sums assms)
+  also have "(\<lambda>n. 2 * (f x n + g x n) + 2 * (f x (Suc n) - f x n)) = h x"
+    by (simp add: h_def algebra_simps fun_eq_iff)
+  finally have *: "h x sums (2 * cot_pfd x - 2 * f x 0)"
+    by simp
+
+  have "(\<lambda>n. sum (h x) {n * 2..<n * 2 + 2}) sums (2 * cot_pfd x - 2 * f x 0)"
+    using sums_group[OF *, of 2] by simp
+  also have "(\<lambda>n. sum (h x) {n*2..<n*2+2}) = (\<lambda>n. h x (2 * n) + h x (2 * n + 1))"
+    by (simp add: mult_ac)
+  finally have sum2: "(\<lambda>n. h x (2 * n) + h x (2 * n + 1)) sums (2 * cot_pfd x - 2 * f x 0)" .
+
+  have "cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) = 2 * cot_pfd x - 2 * f x 0"
+    using sum1 sum2 sums_unique2 by blast
+  also have "2 * f x 0 = 2 / (x + 1)"
+    by (simp add: f_def)
+  finally show ?thesis by algebra
+qed
+
+lemma cot_pfd_funeq_real:
+  fixes x :: real
+  assumes "x \<notin> \<int>"
+  shows   "2 * cot_pfd x = cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1)"
+proof -
+  have "complex_of_real (2 * cot_pfd x) = 2 * cot_pfd (complex_of_real x)"
+    by simp
+  also have "\<dots> = complex_of_real (cot_pfd (x / 2) + cot_pfd ((x + 1) / 2) + 2 / (x + 1))"
+    using assms by (subst cot_pfd_funeq_complex) (auto simp flip: cot_pfd_complex_of_real)
+  finally show ?thesis
+    by (simp only: of_real_eq_iff)
+qed
+
+
+subsection \<open>The limit at 0\<close>
+
+lemma cot_pfd_real_tendsto_0: "cot_pfd \<midarrow>0\<rightarrow> (0 :: real)"
+proof -
+  have "filterlim cot_pfd (nhds 0) (at (0 :: real) within ball 0 1)"
+  proof (rule swap_uniform_limit)
+    show "uniform_limit (ball 0 1)
+            (\<lambda>N x. \<Sum>n<N. 2 * x / (x\<^sup>2 - (real (Suc n))\<^sup>2)) cot_pfd sequentially"
+      using uniform_limit_cot_pfd_real[OF zero_le_one] by (rule uniform_limit_on_subset) auto
+    have "((\<lambda>x. 2 * x / (x\<^sup>2 - (real (Suc n))\<^sup>2)) \<longlongrightarrow> 0) (at 0 within ball 0 1)" for n
+    proof (rule filterlim_mono)
+      show "((\<lambda>x. 2 * x / (x\<^sup>2 - (real (Suc n))\<^sup>2)) \<longlongrightarrow> 0) (at 0)"
+        by real_asymp
+    qed (auto simp: at_within_le_at)
+    thus "\<forall>\<^sub>F N in sequentially.
+             ((\<lambda>x. \<Sum>n<N. 2 * x / (x\<^sup>2 - (real (Suc n))\<^sup>2)) \<longlongrightarrow> 0) (at 0 within ball 0 1)"
+      by (intro always_eventually allI tendsto_null_sum)
+  qed auto
+  thus ?thesis
+    by (simp add: at_within_open_NO_MATCH)
+qed
+
+
+subsection \<open>Final result\<close>
+
+text \<open>
+  To show the final result, we first prove the real case using Herglotz's trick, following
+  the presentation in `Proofs from {THE BOOK}'.~\cite[Chapter~23]{thebook}.
+\<close>
+lemma cot_pfd_formula_real:
+  assumes "x \<notin> \<int>"
+  shows   "pi * cot (pi * x) = 1 / x + cot_pfd x"
+proof -
+  have ev_not_int: "eventually (\<lambda>x. r x \<notin> \<int>) (at x)"
+    if "filterlim r (at (r x)) (at x)" for r :: "real \<Rightarrow> real" and x :: real
+  proof (rule eventually_compose_filterlim[OF _ that])
+    show "eventually (\<lambda>x. x \<notin> \<int>) (at (r x))"
+      using Ints_not_limpt[of "r x"] islimpt_iff_eventually by blast
+  qed
+
+  text \<open>
+    We define the function $h(z)$ as the difference of the left-hand side and right-hand side.
+    The left-hand side and right-hand side have singularities at the integers, but we will
+    later see that these can be removed as \<open>h\<close> tends to \<open>0\<close> there.
+  \<close>
+  define f :: "real \<Rightarrow> real" where "f = (\<lambda>x. pi * cot (pi * x))"
+  define g :: "real \<Rightarrow> real" where "g = (\<lambda>x. 1 / x + cot_pfd x)"
+  define h where "h = (\<lambda>x. if x \<in> \<int> then 0 else f x - g x)"
+
+  have [simp]: "h x = 0" if "x \<in> \<int>" for x
+    using that by (simp add: h_def)
+
+  text \<open>
+    It is easy to see that the left-hand side and the right-hand side, and as a consequence
+    also our function \<open>h\<close>, are odd and periodic with period 1.
+  \<close>
+  have odd_h: "h (-x) = -h x" for x
+    by (simp add: h_def minus_in_Ints_iff f_def g_def)
+  have per_f: "f (x + 1) = f x" for x
+    by (simp add: f_def algebra_simps cot_def)
+  have per_g: "g (x + 1) = g x" if "x \<notin> \<int>" for x
+    using that by (simp add: g_def cot_pfd_plus_1_real)
+  interpret h: periodic_fun_simple' h
+    by standard (auto simp: h_def per_f per_g)
+
+  text \<open>
+    \<open>h\<close> tends to 0 at 0 (and thus at all the integers).
+  \<close>  
+  have h_lim: "h \<midarrow>0\<rightarrow> 0"
+  proof (rule Lim_transform_eventually)
+    have "eventually (\<lambda>x. x \<notin> \<int>) (at (0 :: real))"
+      by (rule ev_not_int) real_asymp
+    thus "eventually (\<lambda>x::real. pi * cot (pi * x) - 1 / x - cot_pfd x = h x) (at 0)"
+      by eventually_elim (simp add: h_def f_def g_def)
+  next
+    have "(\<lambda>x::real. pi * cot (pi * x) - 1 / x) \<midarrow>0\<rightarrow> 0"
+      unfolding cot_def by real_asymp
+    hence "(\<lambda>x::real. pi * cot (pi * x) - 1 / x - cot_pfd x) \<midarrow>0\<rightarrow> 0 - 0"
+      by (intro tendsto_intros cot_pfd_real_tendsto_0)
+    thus "(\<lambda>x. pi * cot (pi * x) - 1 / x - cot_pfd x) \<midarrow>0\<rightarrow> 0"
+      by simp
+  qed
+
+  text \<open>
+    This means that our \<open>h\<close> is in fact continuous everywhere:
+  \<close>
+  have cont_h: "continuous_on A h" for A
+  proof -
+    have "isCont h x" for x
+    proof (cases "x \<in> \<int>")
+      case True
+      then obtain n where [simp]: "x = of_int n"
+        by (auto elim: Ints_cases)
+      show ?thesis unfolding isCont_def
+        by (subst at_to_0) (use h_lim in \<open>simp add: filterlim_filtermap h.plus_of_int\<close>)
+    next
+      case False
+      have "continuous_on (-\<int>) (\<lambda>x. f x - g x)"
+        by (auto simp: f_def g_def sin_times_pi_eq_0 mult.commute[of pi] intro!: continuous_intros)
+      hence "isCont (\<lambda>x. f x - g x) x"
+        by (rule continuous_on_interior)
+           (use False in \<open>auto simp: interior_open open_Compl[OF closed_Ints]\<close>)
+      also have "eventually (\<lambda>y. y \<in> -\<int>) (nhds x)"
+        using False by (intro eventually_nhds_in_open) auto
+      hence "eventually (\<lambda>x. f x - g x = h x) (nhds x)"
+        by eventually_elim (auto simp: h_def)
+      hence "isCont (\<lambda>x. f x - g x) x \<longleftrightarrow> isCont h x"
+        by (rule isCont_cong)
+      finally show ?thesis .
+    qed
+    thus ?thesis
+      by (simp add: continuous_at_imp_continuous_on)
+  qed
+  note [continuous_intros] = continuous_on_compose2[OF cont_h]
+
+  text \<open>
+    Through the functional equations of the sine and cosine function, we can derive
+    the following functional equation for \<open>f\<close> that holds for all non-integer reals:
+  \<close>
+  have eq_f: "f x = (f (x / 2) + f ((x + 1) / 2)) / 2" if "x \<notin> \<int>" for x
+  proof -
+    have "x / 2 \<notin> \<int>"
+      using that by (metis Ints_add field_sum_of_halves)
+    hence nz1: "sin (x/2 * pi) \<noteq> 0"
+      by (subst sin_times_pi_eq_0) auto
+
+    have "(x + 1) / 2 \<notin> \<int>"
+    proof
+      assume "(x + 1) / 2 \<in> \<int>"
+      hence "2 * ((x + 1) / 2) - 1 \<in> \<int>"
+        by (intro Ints_mult Ints_diff) auto
+      thus False using that by (simp add: field_simps)
+    qed
+    hence nz2: "sin ((x+1)/2 * pi) \<noteq> 0"
+      by (subst sin_times_pi_eq_0) auto
+
+    have nz3: "sin (x * pi) \<noteq> 0"
+      using that by (subst sin_times_pi_eq_0) auto
+
+    have eq: "sin (pi * x) = 2 * sin (pi * x / 2) * cos (pi * x / 2)"
+             "cos (pi * x) = (cos (pi * x / 2))\<^sup>2 - (sin (pi * x / 2))\<^sup>2"
+      using sin_double[of "pi * x / 2"] cos_double[of "pi * x / 2"] by simp_all
+    show ?thesis using nz1 nz2 nz3
+      apply (simp add: f_def cot_def field_simps )
+      apply (simp add: add_divide_distrib sin_add cos_add power2_eq_square eq algebra_simps)
+      done
+  qed
+
+  text \<open>
+    The corresponding functional equation for \<^const>\<open>cot_pfd\<close> that we have already shown
+    leads to the same functional equation for \<open>g\<close> as we just showed for \<open>f\<close>:
+  \<close>
+  have eq_g: "g x = (g (x / 2) + g ((x + 1) / 2)) / 2" if "x \<notin> \<int>" for x
+    using cot_pfd_funeq_real[OF that] by (simp add: g_def)
+
+  text \<open>
+    This then leads to the same functional equation for \<open>h\<close>, and because \<open>h\<close> is continuous
+    everywhere, we can extend the validity of the equation to the full domain.
+  \<close>
+  have eq_h: "h x = (h (x / 2) + h ((x + 1) / 2)) / 2" for x
+  proof -
+    have "eventually (\<lambda>x. x \<notin> \<int>) (at x)" "eventually (\<lambda>x. x / 2 \<notin> \<int>) (at x)"
+         "eventually (\<lambda>x. (x + 1) / 2 \<notin> \<int>) (at x)"
+      by (rule ev_not_int; real_asymp)+
+    hence "eventually (\<lambda>x. h x - (h (x / 2) + h ((x + 1) / 2)) / 2 = 0) (at x)"
+    proof eventually_elim
+      case (elim x)
+      thus ?case using eq_f[of x] eq_g[of x]
+        by (simp add: h_def field_simps)
+    qed
+    hence "(\<lambda>x. h x - (h (x / 2) + h ((x + 1) / 2)) / 2) \<midarrow>x\<rightarrow> 0"
+      by (simp add: tendsto_eventually)
+    moreover have "continuous_on UNIV (\<lambda>x. h x - (h (x / 2) + h ((x + 1) / 2)) / 2)"
+      by (auto intro!: continuous_intros)
+    ultimately have "h x - (h (x / 2) + h ((x + 1) / 2)) / 2 = 0"
+      by (meson LIM_unique UNIV_I continuous_on_def)
+    thus ?thesis
+      by simp
+  qed
+
+  text \<open>
+    Since \<open>h\<close> is periodic with period 1 and continuous, it must attain a global maximum \<open>h\<close> 
+    somewhere in the interval $[0, 1]$. Let's call this maximum $m$ and let $x_0$ be some point
+    in the interval $[0, 1]$ such that $h(x_0) = m$.
+  \<close>
+  define m where "m = Sup (h ` {0..1})"
+  have "m \<in> h ` {0..1}"
+    unfolding m_def
+  proof (rule closed_contains_Sup)
+    have "compact (h ` {0..1})"
+      by (intro compact_continuous_image cont_h) auto
+    thus "bdd_above (h ` {0..1})" "closed (h ` {0..1})"
+      by (auto intro: compact_imp_closed compact_imp_bounded bounded_imp_bdd_above)
+  qed auto
+  then obtain x0 where x0: "x0 \<in> {0..1}" "h x0 = m"
+    by blast
+
+  have h_le_m: "h x \<le> m" for x
+  proof -
+    have "h x = h (frac x)"
+      unfolding frac_def by (rule h.minus_of_int [symmetric])
+    also have "\<dots> \<le> m" unfolding m_def
+    proof (rule cSup_upper)
+      have "frac x \<in> {0..1}"
+        using frac_lt_1[of x] by auto
+      thus "h (frac x) \<in> h ` {0..1}"
+        by blast
+    next
+      have "compact (h ` {0..1})"
+        by (intro compact_continuous_image cont_h) auto
+      thus "bdd_above (h ` {0..1})"
+        by (auto intro: compact_imp_bounded bounded_imp_bdd_above)
+    qed
+    finally show ?thesis .
+  qed
+
+  text \<open>
+    Through the functional equation for \<open>h\<close>, we can show that if \<open>h\<close> attains its maximum at
+    some point \<open>x\<close>, it also attains it at $\frac{1}{2} x$. By iterating this, it attains the
+    maximum at all points of the form $2^{-n} x_0$.
+  \<close>
+  have h_eq_m_iter_aux: "h (x / 2) = m" if "h x = m" for x
+    using eq_h[of x] that h_le_m[of "x / 2"] h_le_m[of "(x + 1) / 2"] by simp
+  have h_eq_m_iter: "h (x0 / 2 ^ n) = m" for n
+  proof (induction n)
+    case (Suc n)
+    have "h (x0 / 2 ^ Suc n) = h (x0 / 2 ^ n / 2)"
+      by (simp add: field_simps)
+    also have "\<dots> = m"
+      by (rule h_eq_m_iter_aux) (use Suc.IH in auto)
+    finally show ?case .
+  qed (use x0 in auto)
+
+  text \<open>
+    Since the sequence $n \mapsto 2^{-n} x_0$ tends to 0 and \<open>h\<close> is continuous, we derive \<open>m = 0\<close>.
+  \<close>
+  have "(\<lambda>n. h (x0 / 2 ^ n)) \<longlonglongrightarrow> h 0"
+    by (rule continuous_on_tendsto_compose[OF cont_h[of UNIV]]) (force | real_asymp)+
+  moreover from h_eq_m_iter have "(\<lambda>n. h (x0 / 2 ^ n)) \<longlonglongrightarrow> m"
+    by simp
+  ultimately have "m = h 0"
+    using tendsto_unique by force
+  hence "m = 0"
+    by simp
+
+  text \<open>
+    Since \<open>h\<close> is odd, this means that \<open>h\<close> is identically zero everywhere, and our result follows.
+  \<close>
+  have "h x = 0"
+    using h_le_m[of x] h_le_m[of "-x"] \<open>m = 0\<close> odd_h[of x] by linarith
+  thus ?thesis
+    using assms by (simp add: h_def f_def g_def)
+qed
+
+
+text \<open>
+  We now lift the result from the domain \<open>\<real>\<setminus>\<int>\<close> to \<open>\<complex>\<setminus>\<int>\<close>. We do this by noting that \<open>\<complex>\<setminus>\<int>\<close> is
+  connected and the point $\frac{1}{2}$ is both in \<open>\<complex>\<setminus>\<int>\<close> and a limit point of \<open>\<real>\<setminus>\<int>\<close>.
+\<close>
+lemma one_half_limit_point_Reals_minus_Ints: "(1 / 2 :: complex) islimpt \<real> - \<int>"
+proof (rule islimptI)
+  fix T :: "complex set"
+  assume "1 / 2 \<in> T" "open T"
+  then obtain r where r: "r > 0" "ball (1 / 2) r \<subseteq> T"
+    using open_contains_ball by blast
+  define y where "y = 1 / 2 + min r (1 / 2) / 2"
+  have "y \<in> {0<..<1}"
+    using r by (auto simp: y_def)
+  hence "complex_of_real y \<in> \<real> - \<int>"
+    by (auto elim!: Ints_cases)
+  moreover have "complex_of_real y \<noteq> 1 / 2"
+  proof
+    assume "complex_of_real y = 1 / 2"
+    also have "1 / 2 = complex_of_real (1 / 2)"
+      by simp
+    finally have "y = 1 / 2"
+      unfolding of_real_eq_iff .
+    with r show False
+      by (auto simp: y_def)
+  qed
+  moreover have "complex_of_real y \<in> ball (1 / 2) r"
+    using \<open>r > 0\<close> by (auto simp: y_def dist_norm)
+  with r have "complex_of_real y \<in> T"
+    by blast
+  ultimately show "\<exists>y\<in>\<real> - \<int>. y \<in> T \<and> y \<noteq> 1 / 2"
+    by blast
+qed
+
+theorem cot_pfd_formula_complex:
+  fixes z :: complex
+  assumes "z \<notin> \<int>"
+  shows   "pi * cot (pi * z) = 1 / z + cot_pfd z"
+proof -
+  let ?f = "\<lambda>z::complex. pi * cot (pi * z) - 1 / z - cot_pfd z"
+  have "pi * cot (pi * z) - 1 / z - cot_pfd z = 0"
+  proof (rule analytic_continuation[where f = ?f])
+    show "?f holomorphic_on -\<int>" 
+      unfolding cot_def by (intro holomorphic_intros) (auto simp: sin_eq_0)
+  next
+    show "open (-\<int> :: complex set)" "connected (-\<int> :: complex set)"
+      by (auto intro!: path_connected_imp_connected path_connected_complement_countable countable_int)
+  next
+    show "\<real> - \<int> \<subseteq> (-\<int> :: complex set)"
+      by auto
+  next
+    show "(1 / 2 :: complex) islimpt \<real> - \<int>"
+      by (rule one_half_limit_point_Reals_minus_Ints)
+  next
+    show "1 / (2 :: complex) \<in> -\<int>"
+      using fraction_not_in_ints[of 2 1, where ?'a = complex] by auto
+  next
+    show "z \<in> -\<int>"
+      using assms by simp
+  next
+    show "?f z = 0" if "z \<in> \<real> - \<int>" for z
+    proof -
+      have "complex_of_real pi * cot (complex_of_real pi * z) - 1 / z - cot_pfd z =
+            complex_of_real (pi * cot (pi * Re z) - 1 / Re z - cot_pfd (Re z))"
+        using that by (auto elim!: Reals_cases simp: cot_of_real)
+      also have "\<dots> = 0"
+        by (subst cot_pfd_formula_real) (use that in \<open>auto elim!: Reals_cases\<close>)
+      finally show ?thesis .
+    qed
+  qed
+  thus ?thesis
+    by algebra
+qed
+
+end
\ No newline at end of file
diff --git a/thys/Cotangent_PFD_Formula/ROOT b/thys/Cotangent_PFD_Formula/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Cotangent_PFD_Formula/ROOT
@@ -0,0 +1,12 @@
+chapter AFP
+
+session Cotangent_PFD_Formula (AFP) = "HOL-Complex_Analysis" +
+  options [timeout = 600]
+  sessions
+    "HOL-Real_Asymp"
+  theories
+    Cotangent_PFD_Formula
+  document_files
+    "root.tex"
+    "root.bib"
+
diff --git a/thys/Cotangent_PFD_Formula/document/root.bib b/thys/Cotangent_PFD_Formula/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Cotangent_PFD_Formula/document/root.bib
@@ -0,0 +1,8 @@
+@book{thebook,
+author = {Aigner, Martin and Ziegler, Günter M.},
+title = {Proofs from {THE BOOK}},
+year = {2009},
+isbn = {3642008550},
+publisher = {Springer},
+edition = {4th}
+}
diff --git a/thys/Cotangent_PFD_Formula/document/root.tex b/thys/Cotangent_PFD_Formula/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Cotangent_PFD_Formula/document/root.tex
@@ -0,0 +1,41 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+\usepackage{amsfonts,amsmath,amssymb}
+\usepackage{pgfplots}
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+\begin{document}
+
+\title{A Proof from THE BOOK: The Partial Fraction Expansion of the Cotangent}
+\author{Manuel Eberl}
+\maketitle
+
+\begin{abstract}
+In this article, I formalise a proof from THE BOOK~\cite[Chapter~23]{thebook}; namely a formula that was called `one of the most beautiful formulas involving elementary functions':
+\[\pi \cot(\pi z) = \frac{1}{z} + \sum_{n=1}^\infty\left(\frac{1}{z+n} + \frac{1}{z-n}\right)\]
+The proof uses Herglotz's trick to show the real case and analytic continuation for the complex case.
+\end{abstract}
+
+\tableofcontents
+\newpage
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\nocite{corless96}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,669 +1,670 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Actuarial_Mathematics
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BD_Security_Compositional
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
 Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CSP_RefTK
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CoCon
 CoSMeDis
 CoSMed
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
+Cotangent_PFD_Formula
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Equivalence_Relation_Enumeration
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Eval_FO
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 FOL_Seq_Calc2
 Factor_Algebraic_Polynomial
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Foundation_of_geometry
 Fourier
 FO_Theory_Rewriting
 Free-Boolean-Algebra
 Free-Groups
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Gale_Shapley
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Hahn_Jordan_Decomposition
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 Hyperdual
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Independence_CH
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpolation_Polynomials_HOL_Algebra
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 Irrationals_From_THEBOOK
 IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knights_Tour
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 LP_Duality
 Lucas_Theorem
 MDP-Algorithms
 MDP-Rewards
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Method
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PAL
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quasi_Borel_Spaces
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Real_Power
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Registers
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Regular_Tree_Relations
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 ResiduatedTransitionSystem
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Roth_Arithmetic_Progressions
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Simplicial_complexes_and_boolean_functions
 SimplifiedOntologicalArgument
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szemeredi_Regularity
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Transitive_Models
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Universal_Hash_Families
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_Emde_Boas_Trees
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 VYDRA_MDL
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weight_Balanced_Trees
 Weighted_Path_Order
 Well_Quasi_Orders
 Wetzels_Problem
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 X86_Semantics
 XML
 Youngs_Inequality
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL