diff --git a/thys/Girth_Chromatic/Girth_Chromatic.thy b/thys/Girth_Chromatic/Girth_Chromatic.thy
--- a/thys/Girth_Chromatic/Girth_Chromatic.thy
+++ b/thys/Girth_Chromatic/Girth_Chromatic.thy
@@ -1,737 +1,737 @@
 theory Girth_Chromatic
 imports
   Ugraphs
   Girth_Chromatic_Misc
   "HOL-Probability.Probability"
   "HOL-Decision_Procs.Approximation"
 begin
 
 section \<open>Probability Space on Sets of Edges\<close>
 
 definition cylinder :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set set" where
   "cylinder S A B = {T \<in> Pow S. A \<subseteq> T \<and> B \<inter> T = {}}"
 
 lemma full_sum:
   fixes p :: real
   assumes "finite S"
   shows "(\<Sum>A\<in>Pow S. p^card A * (1 - p)^card (S - A)) = 1"
 using assms
 proof induct
   case (insert s S)
   have "inj_on (insert s) (Pow S)"
       and "\<And>x. S - insert s x = S - x"
       and "Pow S \<inter> insert s ` Pow S = {}"
       and "\<And>x. x \<in> Pow S \<Longrightarrow> card (insert s S - x) = Suc (card (S - x))"
     using insert(1-2) by (auto simp: insert_Diff_if intro!: inj_onI)
   moreover have "\<And>x. x \<subseteq> S \<Longrightarrow> card (insert s x) = Suc (card x)"
     using insert(1-2) by (subst card.insert) (auto dest: finite_subset)
   ultimately show ?case
     by (simp add: sum.reindex sum_distrib_left[symmetric] ac_simps
                   insert.hyps sum.union_disjoint Pow_insert)
 qed simp
 
 text \<open>Definition of the probability space on edges:\<close>
 locale edge_space =
   fixes n :: nat and p :: real
   assumes p_prob: "0 \<le> p" "p \<le> 1"
 begin
 
 definition S_verts :: "nat set" where
   "S_verts \<equiv> {1..n}"
 
 definition S_edges :: "uedge set" where
   "S_edges = all_edges S_verts"
 
 definition edge_ugraph :: "uedge set \<Rightarrow> ugraph" where
   "edge_ugraph es \<equiv> (S_verts, es \<inter> S_edges)"
 
 definition "P = point_measure (Pow S_edges) (\<lambda>s. p^card s * (1 - p)^card (S_edges - s))"
 
 lemma finite_verts[intro!]: "finite S_verts"
   by (auto simp: S_verts_def)
 
 lemma finite_edges[intro!]: "finite S_edges"
   by (auto simp: S_edges_def all_edges_def finite_verts)
 
 lemma finite_graph[intro!]: "finite (uverts (edge_ugraph es))"
   unfolding edge_ugraph_def by auto
 
 lemma uverts_edge_ugraph[simp]: "uverts (edge_ugraph es) = S_verts"
   by (simp add: edge_ugraph_def)
 
 lemma uedges_edge_ugraph[simp]: "uedges (edge_ugraph es) = es \<inter> S_edges"
   unfolding edge_ugraph_def by simp
 
 lemma space_eq: "space P = Pow S_edges" by (simp add: P_def space_point_measure)
 
 lemma sets_eq: "sets P = Pow (Pow S_edges)" by (simp add: P_def sets_point_measure)
 
 lemma emeasure_eq:
   "emeasure P A = (if A \<subseteq> Pow S_edges then (\<Sum>edges\<in>A. p^card edges * (1 - p)^card (S_edges - edges)) else 0)"
   using finite_edges p_prob
   by (simp add: P_def space_point_measure emeasure_point_measure_finite
     sets_point_measure emeasure_notin_sets)
 
 lemma integrable_P[intro, simp]: "integrable P (f::_ \<Rightarrow> real)"
   using finite_edges by (simp add: integrable_point_measure_finite P_def)
 
 lemma borel_measurable_P[measurable]: "f \<in> borel_measurable P"
   unfolding P_def by simp
 
 lemma prob_space_P: "prob_space P"
 proof
   show "emeasure P (space P) = 1" \<comment> \<open>Sum of probabilities equals 1\<close>
     using finite_edges by (simp add: emeasure_eq full_sum one_ereal_def space_eq)
 qed
 
 end
 
 sublocale edge_space \<subseteq> prob_space P
   by (rule prob_space_P)
 
 context edge_space
 begin
 
 lemma prob_eq:
   "prob A = (if A \<subseteq> Pow S_edges then (\<Sum>edges\<in>A. p^card edges * (1 - p)^card (S_edges - edges)) else 0)"
   using emeasure_eq[of A] p_prob unfolding emeasure_eq_measure by (simp add: sum_nonneg)
 
 lemma integral_finite_singleton: "integral\<^sup>L P f = (\<Sum>x\<in>Pow S_edges. f x * measure P {x})"
   using p_prob prob_eq unfolding P_def
   by (subst lebesgue_integral_point_measure_finite) (auto intro!: sum.cong)
 
 text \<open>Probability of cylinder sets:\<close>
 lemma cylinder_prob:
   assumes "A \<subseteq> S_edges" "B \<subseteq> S_edges" "A \<inter> B = {}"
   shows "prob (cylinder S_edges A B) = p ^ (card A) * (1 - p) ^ (card B)" (is "_ = ?pp A B")
 proof -
   have "Pow S_edges \<inter> cylinder S_edges A B = cylinder S_edges A B"
        "\<And>x. x \<in> cylinder S_edges A B \<Longrightarrow> A \<union> x = x"
        "\<And>x. x \<in> cylinder S_edges A B \<Longrightarrow> finite x"
        "\<And>x. x \<in> cylinder S_edges A B \<Longrightarrow> B \<inter> (S_edges - B - x) = {}"
        "\<And>x. x \<in> cylinder S_edges A B \<Longrightarrow> B \<union> (S_edges - B - x) = S_edges - x"
        "finite A" "finite B"
     using assms by (auto simp add: cylinder_def intro: finite_subset)
   then have "(\<Sum>T\<in>cylinder S_edges A B. ?pp T (S_edges - T))
       = (\<Sum>T \<in> cylinder S_edges A B. p^(card A + card (T - A)) * (1 - p)^(card B + card ((S_edges - B) - T)))"
     using finite_edges by (simp add: card_Un_Int)
   also have "\<dots> = ?pp A B * (\<Sum>T\<in>cylinder S_edges A B. ?pp (T - A) (S_edges - B - T))"
     by (simp add: power_add sum_distrib_left ac_simps)
   also have "\<dots> = ?pp A B"
   proof -
     have "\<And>T. T \<in> cylinder S_edges A B \<Longrightarrow> S_edges - B - T = (S_edges - A) - B - (T - A)"
          "Pow (S_edges - A - B) = (\<lambda>x. x - A) ` cylinder S_edges A B"
          "inj_on (\<lambda>x. x - A) (cylinder S_edges A B)"
          "finite (S_edges - A - B)"
       using assms by (auto simp: cylinder_def intro!: inj_onI)
     with full_sum[of "S_edges - A - B"] show ?thesis by (simp add: sum.reindex)
   qed
   finally show ?thesis by (auto simp add: prob_eq cylinder_def)
 qed
 
 lemma Markov_inequality:
   fixes a :: real and X :: "uedge set \<Rightarrow> real"
   assumes "0 < c" "\<And>x. 0 \<le> f x"
   shows "prob {x \<in> space P. c \<le> f x} \<le> (\<integral>x. f x \<partial> P) / c"
 proof -
   from assms have "(\<integral>\<^sup>+ x. ennreal (f x) \<partial>P) = (\<integral>x. f x \<partial>P)"
     by (intro nn_integral_eq_integral) auto
   with assms show ?thesis
-    using nn_integral_Markov_inequality[of f P "space P" "1 / c"]
+    using nn_integral_Markov_inequality[of f "space P" P "1 / c"]
     by (simp cong: nn_integral_cong add: emeasure_eq_measure ennreal_mult[symmetric])
 qed
 
 end
 
 subsection \<open>Graph Probabilities outside of @{term Edge_Space} locale\<close>
 
 text \<open>
  These abbreviations allow a compact expression of probabilities about random
  graphs outside of the @{term Edge_Space} locale. We also transfer a few of the lemmas
  we need from the locale into the toplevel theory.
 \<close>
 
 abbreviation MGn :: "(nat \<Rightarrow> real) \<Rightarrow> nat \<Rightarrow> (uedge set) measure" where
   "MGn p n \<equiv> (edge_space.P n (p n))"
 abbreviation probGn :: "(nat \<Rightarrow> real) \<Rightarrow> nat \<Rightarrow> (uedge set \<Rightarrow> bool) \<Rightarrow> real" where
   "probGn p n P \<equiv> measure (MGn p n) {es \<in> space (MGn p n). P es}"
 
 lemma probGn_le:
   assumes p_prob: "0 < p n" "p n < 1"
   assumes sub: "\<And>n es. es \<in> space (MGn p n) \<Longrightarrow> P n es \<Longrightarrow> Q n es"
   shows "probGn p n (P n) \<le> probGn p n (Q n)"
 proof -
   from p_prob interpret E: edge_space n "p n" by unfold_locales auto
   show ?thesis
     by (auto intro!: E.finite_measure_mono sub simp: E.space_eq E.sets_eq)
 qed
 
 section \<open>Short cycles\<close>
 
 definition short_cycles :: "ugraph \<Rightarrow> nat \<Rightarrow> uwalk set" where
   "short_cycles G k \<equiv> {p \<in> ucycles G. uwalk_length p \<le> k}"
 
 text \<open>obtains a vertex in a short cycle:\<close>
 definition choose_v :: "ugraph \<Rightarrow> nat \<Rightarrow> uvert" where
   "choose_v G k \<equiv> SOME u. \<exists>p. p \<in> short_cycles G k \<and> u \<in> set p"
 
 partial_function (tailrec) kill_short :: "ugraph \<Rightarrow> nat \<Rightarrow> ugraph" where
   "kill_short G k = (if short_cycles G k = {} then G else (kill_short (G -- (choose_v G k)) k))"
 
 lemma ksc_simps[simp]:
   "short_cycles G k = {} \<Longrightarrow> kill_short G k = G"
   "short_cycles G k \<noteq> {}  \<Longrightarrow> kill_short G k = kill_short (G -- (choose_v G k)) k"
   by (auto simp: kill_short.simps)
 
 lemma
   assumes "short_cycles G k \<noteq> {}"
   shows choose_v__in_uverts: "choose_v G k \<in> uverts G" (is ?t1)
     and choose_v__in_short: "\<exists>p. p \<in> short_cycles G k \<and> choose_v G k \<in> set p" (is ?t2)
 proof -
   from assms obtain p where "p \<in> ucycles G" "uwalk_length p \<le> k"
     unfolding short_cycles_def by auto
   moreover
   then obtain u where "u \<in> set p" unfolding ucycles_def
     by (cases p) (auto simp: uwalk_length_conv)
   ultimately have "\<exists>u p. p \<in> short_cycles G k \<and> u \<in> set p"
     by (auto simp: short_cycles_def)
   then show ?t2 by (auto simp: choose_v_def intro!: someI_ex)
   then show ?t1 by (auto simp: short_cycles_def ucycles_def uwalks_def)
 qed
 
 lemma kill_step_smaller:
   assumes "short_cycles G k \<noteq> {}"
   shows "short_cycles (G -- (choose_v G k)) k \<subset> short_cycles G k"
 proof -
   let ?cv = "choose_v G k"
   from assms obtain p where "p \<in> short_cycles G k" "?cv \<in> set p"
     by atomize_elim (rule choose_v__in_short)
 
   have "short_cycles (G -- ?cv) k \<subseteq> short_cycles G k"
   proof
     fix p assume "p \<in> short_cycles (G -- ?cv) k"
     then show "p \<in> short_cycles G k"
       unfolding short_cycles_def ucycles_def uwalks_def
       using edges_Gu[of G ?cv] by (auto simp: verts_Gu)
   qed
   moreover have "p \<notin> short_cycles (G -- ?cv) k"
     using \<open>?cv \<in> set p\<close> by (auto simp: short_cycles_def ucycles_def uwalks_def verts_Gu)
   ultimately show ?thesis using \<open>p \<in> short_cycles G k\<close> by auto
 qed
 
 text \<open>Induction rule for @{term kill_short}:\<close>
 lemma kill_short_induct[consumes 1, case_names empty kill_vert]:
   assumes fin: "finite (uverts G)"
   assumes a_empty: "\<And>G. short_cycles G k = {} \<Longrightarrow> P G k"
   assumes a_kill: "\<And>G. finite (short_cycles G k) \<Longrightarrow> short_cycles G k \<noteq> {}
     \<Longrightarrow> P (G -- (choose_v G k)) k \<Longrightarrow> P G k"
   shows "P G k"
 proof -
   have "finite (short_cycles G k)"
     using finite_ucycles[OF fin] by (auto simp: short_cycles_def)
   then show ?thesis
     by (induct "short_cycles G k" arbitrary: G rule: finite_psubset_induct)
       (metis kill_step_smaller a_kill a_empty)
 qed
 
 text \<open>Large Girth (after @{term kill_short}):\<close>
 lemma kill_short_large_girth:
   assumes "finite (uverts G)"
   shows "k < girth (kill_short G k)"
 using assms
 proof (induct G k rule: kill_short_induct)
   case (empty G)
   then have "\<And>p. p \<in> ucycles G \<Longrightarrow> k < enat (uwalk_length p)"
     by (auto simp: short_cycles_def)
   with empty show ?case by (auto simp: girth_def intro: enat_less_INF_I)
 qed simp
 
 text \<open>Order of graph (after @{term kill_short}):\<close>
 lemma kill_short_order_of_graph:
   assumes "finite (uverts G)"
   shows "card (uverts G) - card (short_cycles G k) \<le> card (uverts (kill_short G k))"
 using assms assms
 proof (induct G k rule: kill_short_induct)
   case (kill_vert G)
   let ?oG = "G -- (choose_v G k)"
 
   have "finite (uverts ?oG)"
     using kill_vert by (auto simp: remove_vertex_def)
   moreover
   have "uverts (kill_short G k) = uverts (kill_short ?oG k)"
     using kill_vert by simp
   moreover
   have "card (uverts G) = Suc (card (uverts ?oG))"
     using choose_v__in_uverts kill_vert
     by (simp add: remove_vertex_def card_Suc_Diff1 del: card_Diff_insert)
   moreover
   have "card (short_cycles ?oG k) < card (short_cycles G k)"
     by (intro psubset_card_mono kill_vert.hyps kill_step_smaller)
   ultimately show ?case using kill_vert.hyps by presburger
 qed simp
 
 text \<open>Independence number (after @{term kill_short}):\<close>
 lemma kill_short_\<alpha>:
   assumes "finite (uverts G)"
   shows "\<alpha> (kill_short G k) \<le> \<alpha> G"
 using assms
 proof (induct G k rule: kill_short_induct)
   case (kill_vert G)
   note kill_vert(3)
   also have "\<alpha> (G -- (choose_v G k)) \<le> \<alpha> G" by (rule \<alpha>_remove_le)
   finally show ?case using kill_vert by simp
 qed simp
 
 text \<open>Wellformedness (after @{term kill_short}):\<close>
 lemma kill_short_uwellformed:
   assumes "finite (uverts G)" "uwellformed G"
   shows "uwellformed (kill_short G k)"
 using assms
 proof (induct G k rule: kill_short_induct)
   case (kill_vert G)
   from kill_vert.prems have "uwellformed (G -- (choose_v G k))"
     by (auto simp: uwellformed_def remove_vertex_def)
   with kill_vert.hyps show ?case by simp
 qed simp
 
 
 section \<open>The Chromatic-Girth Theorem\<close>
 
 text \<open>Probability of Independent Edges:\<close>
 lemma (in edge_space) random_prob_independent:
   assumes "n \<ge> k" "k \<ge> 2"
   shows "prob {es \<in> space P. k \<le> \<alpha> (edge_ugraph es)}
     \<le> (n choose k)*(1-p)^(k choose 2)"
 proof -
   let "?k_sets" = "{vs. vs \<subseteq> S_verts \<and> card vs = k}"
 
   { fix vs assume A: "vs \<in> ?k_sets"
     then have B: "all_edges vs \<subseteq> S_edges"
       unfolding all_edges_def S_edges_def by blast
 
     have "{es \<in> space P. vs \<in> independent_sets (edge_ugraph es)}
         = cylinder S_edges {} (all_edges vs)" (is "?L = _")
       using A by (auto simp: independent_sets_def edge_ugraph_def space_eq cylinder_def)
     then have "prob ?L = (1-p)^(k choose 2)"
       using A B finite by (auto simp: cylinder_prob card_all_edges dest: finite_subset)
   }
   note prob_k_indep = this
     \<comment> \<open>probability that a fixed set of k vertices is independent in a random graph\<close>
 
   have "{es \<in> space P. k \<in> card ` independent_sets (edge_ugraph es)}
     = (\<Union>vs \<in> ?k_sets. {es \<in> space P. vs \<in> independent_sets (edge_ugraph es)})" (is "?L = ?R")
     unfolding image_def space_eq independent_sets_def by auto
   then have "prob ?L \<le> (\<Sum>vs \<in> ?k_sets. prob {es \<in> space P. vs \<in> independent_sets (edge_ugraph es)})"
     by (auto intro!: finite_measure_subadditive_finite simp: space_eq sets_eq)
   also have "\<dots> = (n choose k)*((1 - p) ^ (k choose 2))"
     by (simp add: prob_k_indep S_verts_def n_subsets)
   finally show ?thesis using \<open>k \<ge> 2\<close> by (simp add: le_\<alpha>_iff)
 qed
 
 text \<open>Almost never many independent edges:\<close>
 lemma almost_never_le_\<alpha>:
   fixes k :: nat
     and p :: "nat \<Rightarrow> real"
   assumes p_prob: "\<forall>\<^sup>\<infinity> n. 0 < p n \<and> p n < 1"
   assumes [arith]: "k > 0"
   assumes N_prop: "\<forall>\<^sup>\<infinity> n. (6 * k * ln n)/n \<le> p n"
   shows "(\<lambda>n. probGn p n (\<lambda>es. 1/2*n/k \<le> \<alpha> (edge_space.edge_ugraph n es))) \<longlonglongrightarrow> 0"
     (is "(\<lambda>n. ?prob_fun n) \<longlonglongrightarrow> 0")
 proof -
   let "?prob_fun_raw n" = "probGn p n (\<lambda>es. nat(ceiling (1/2*n/k)) \<le> \<alpha> (edge_space.edge_ugraph n es))"
 
   define r where "r n = 1 / 2 * n / k" for n :: nat
   let ?nr = "\<lambda>n. nat(ceiling (r n))"
 
   have r_pos: "\<And>n. 0 < n \<Longrightarrow> 0 < r n " by (auto simp: r_def field_simps)
 
   have nr_bounds: "\<forall>\<^sup>\<infinity> n. 2 \<le> ?nr n \<and> ?nr n \<le> n"
     by (intro eventually_sequentiallyI[of "4 * k"])
        (simp add: r_def nat_ceiling_le_eq le_natceiling_iff field_simps)
 
   from nr_bounds p_prob have ev_prob_fun_raw_le:
     "\<forall>\<^sup>\<infinity> n. probGn p n (\<lambda>es. ?nr n\<le> \<alpha> (edge_space.edge_ugraph n es))
       \<le> (n * exp (- p n * (real (?nr n) - 1) / 2)) powr ?nr n"
     (is "\<forall>\<^sup>\<infinity> n. ?prob_fun_raw_le n")
   proof (rule eventually_elim2)
     fix n :: nat assume A: "2 \<le> ?nr n \<and> ?nr n \<le> n" "0 < p n \<and>p n < 1"
     then interpret pG: edge_space n "p n" by unfold_locales auto
 
     have r: "real (?nr n - Suc 0) = real (?nr n) - Suc 0" using A by auto
 
     have [simp]: "n>0" using A by linarith
     have "probGn p n (\<lambda>es. ?nr n \<le> \<alpha> (edge_space.edge_ugraph n es))
         \<le> (n choose ?nr n) * (1 - p n)^(?nr n choose 2)"
       using A by (auto intro: pG.random_prob_independent)
     also have "\<dots> \<le> n powr ?nr n * (1 - p n) powr (?nr n choose 2)"
       using A  by (simp add: powr_realpow of_nat_power [symmetric] binomial_le_pow  del: of_nat_power)
     also have "\<dots> = n powr ?nr n * (1 - p n) powr (?nr n * (?nr n - 1) / 2)"
       by (cases "even (?nr n - 1)")
         (auto simp add: n_choose_2_nat real_of_nat_div)
     also have "\<dots> = n powr ?nr n * ((1 - p n) powr ((?nr n - 1) / 2)) powr ?nr n"
       by (auto simp add: powr_powr r ac_simps)
     also have "\<dots> \<le> (n * exp (- p n * (?nr n - 1) / 2)) powr ?nr n"
     proof -
       have "(1 - p n) powr ((?nr n - 1) / 2) \<le> exp (- p n) powr ((?nr n - 1) / 2)"
         using A by (auto simp: powr_mono2 diff_conv_add_uminus simp del: add_uminus_conv_diff)
       also have "\<dots> = exp (- p n * (?nr n - 1) / 2)" by (auto simp: powr_def)
       finally show ?thesis
         using A by (auto simp: powr_mono2 powr_mult)
     qed
     finally show "probGn p n (\<lambda>es. ?nr n \<le> \<alpha> (edge_space.edge_ugraph n es))
       \<le> (n * exp (- p n * (real (?nr n) - 1) / 2)) powr ?nr n"
       using A r by simp
   qed
 
   from p_prob N_prop
   have ev_expr_bound: "\<forall>\<^sup>\<infinity> n. n * exp (-p n * (real (?nr n) - 1) / 2) \<le> (exp 1 / n) powr (1 / 2)"
   proof (elim eventually_rev_mp, intro eventually_sequentiallyI conjI impI)
     fix n assume n_bound[arith]: "2 \<le> n"
       and p_bound: "0 < p n \<and> p n < 1" "(6 * k * ln n) / n \<le> p n"
     have r_bound: "r n \<le> ?nr n" by (rule real_nat_ceiling_ge)
 
     have "n * exp (-p n * (real (?nr n)- 1) / 2) \<le> n * exp (- 3 / 2 * ln n + p n / 2)"
     proof -
       have "0 < ln n" using "n_bound" by auto
       then have "(3 / 2) * ln n \<le> ((6 * k * ln n) / n) * (?nr n / 2)"
         using r_bound le_of_int_ceiling[of "n/2*k"]
         by (simp add: r_def field_simps del: le_of_int_ceiling)
       also have "\<dots> \<le> p n * (?nr n / 2)"
         using n_bound p_bound r_bound r_pos[of n] by (auto simp: field_simps)
       finally show ?thesis using r_bound by (auto simp: field_simps)
     qed
     also have "\<dots> \<le> n * n powr (- 3 / 2) * exp 1 powr (1 / 2)"
       using p_bound by (simp add: powr_def exp_add [symmetric])
     also have "\<dots> \<le> n powr (-1 / 2) * exp 1 powr (1 / 2)" by (simp add: powr_mult_base)
     also have "\<dots> = (exp 1 / n) powr (1/2)"
       by (simp add: powr_divide powr_minus_divide)
     finally show "n * exp (- p n * (real (?nr n) - 1) / 2) \<le> (exp 1 / n) powr (1 / 2)" .
   qed
 
   have ceil_bound: "\<And>G n. 1/2*n/k \<le> \<alpha> G \<longleftrightarrow> nat(ceiling (1/2*n/k)) \<le> \<alpha> G"
     by (case_tac "\<alpha> G") (auto simp: nat_ceiling_le_eq)
 
   show ?thesis
   proof (unfold ceil_bound, rule real_tendsto_sandwich)
     show "(\<lambda>n. 0) \<longlonglongrightarrow> 0"
         "(\<lambda>n. (exp 1 / n) powr (1 / 2)) \<longlonglongrightarrow> 0"
         "\<forall>\<^sup>\<infinity> n. 0 \<le> ?prob_fun_raw n"
       using p_prob by (auto intro: measure_nonneg LIMSEQ_inv_powr elim: eventually_mono)
   next
     from nr_bounds ev_expr_bound ev_prob_fun_raw_le
     show "\<forall>\<^sup>\<infinity> n. ?prob_fun_raw n \<le> (exp 1 / n) powr (1 / 2)"
     proof (elim eventually_rev_mp, intro eventually_sequentiallyI impI conjI)
       fix n assume A: "3 \<le> n"
         and nr_bounds: "2 \<le> ?nr n \<and> ?nr n \<le> n"
         and prob_fun_raw_le: "?prob_fun_raw_le n"
         and expr_bound: "n * exp (- p n * (real (nat(ceiling (r n))) - 1) / 2) \<le> (exp 1 / n) powr (1 / 2)"
 
       have "exp 1 < (3 :: real)" by (approximation 6)
       then have "(exp 1 / n) powr (1 / 2) \<le> 1 powr (1 / 2)"
         using A by (intro powr_mono2) (auto simp: field_simps)
       then have ep_bound: "(exp 1 / n) powr (1 / 2) \<le> 1" by simp
 
       have "?prob_fun_raw n \<le> (n * exp (- p n * (real (?nr n) - 1) / 2)) powr (?nr n)"
         using prob_fun_raw_le by (simp add: r_def)
       also have "\<dots> \<le> ((exp 1 / n) powr (1 / 2)) powr ?nr n"
         using expr_bound A by (auto simp: powr_mono2)
       also have "\<dots> \<le> ((exp 1 / n) powr (1 / 2))"
         using nr_bounds ep_bound A by (auto simp: powr_le_one_le)
       finally show "?prob_fun_raw n \<le> (exp 1 / n) powr (1 / 2)" .
     qed
   qed
 qed
 
 text \<open>Mean number of k-cycles in a graph. (Or rather of paths describing a circle of length @{term k}):\<close>
 lemma (in edge_space) mean_k_cycles:
   assumes "3 \<le> k" "k < n"
   shows "(\<integral>es. card {c \<in> ucycles (edge_ugraph es). uwalk_length c = k} \<partial> P)
     = of_nat (fact n div fact (n - k)) * p ^ k"
 proof -
   let ?k_cycle = "\<lambda>es c k. c \<in> ucycles (edge_ugraph es) \<and> uwalk_length c = k"
   define C where "C k = {c. ?k_cycle S_edges c k}" for k
     \<comment> \<open>@{term "C k"} is the set of all possible cycles of size @{term k} in @{term "edge_ugraph S_edges"}\<close>
   define XG  where "XG es = {c. ?k_cycle es c k}" for es
     \<comment> \<open>@{term "XG es"} is the set of cycles contained in a @{term "edge_ugraph es"}\<close>
   define XC where "XC c = {es \<in> space P. ?k_cycle es c k}" for c
     \<comment> \<open>"@{term "XC c"} is the set of graphs (edge sets) containing a cycle c"\<close>
   then have XC_in_sets: "\<And>c. XC c \<in> sets P"
       and XC_cyl: "\<And>c. c \<in> C k \<Longrightarrow> XC c = cylinder S_edges (set (uwalk_edges c)) {}"
     by (auto simp: ucycles_def space_eq uwalks_def C_def cylinder_def sets_eq)
 
   have "(\<integral>es. card {c \<in> ucycles (edge_ugraph es). uwalk_length c = k} \<partial> P)
       =  (\<Sum>x\<in>space P. card (XG x) * prob {x})"
     by (simp add: XG_def integral_finite_singleton space_eq)
   also have "\<dots> = (\<Sum>c\<in>C k. prob (cylinder S_edges (set (uwalk_edges c)) {}))"
   proof -
     have XG_Int_C: "\<And>s. s \<in> space P \<Longrightarrow> C k \<inter> XG s = XG s"
       unfolding XG_def C_def ucycles_def uwalks_def edge_ugraph_def by auto
     have fin_XC: "\<And>k. finite (XC k)" and fin_C: "finite (C k)"
       unfolding C_def XC_def by (auto simp: finite_edges space_eq intro!: finite_ucycles)
 
     have "(\<Sum>x\<in>space P. card (XG x) * prob {x}) = (\<Sum>x\<in>space P. (\<Sum>c \<in> XG x. prob {x}))"
       by simp
     also have "\<dots> = (\<Sum>x\<in>space P. (\<Sum>c \<in> C k. if c \<in> XG x then prob {x} else 0))"
       using fin_C by (simp add: sum.If_cases) (simp add: XG_Int_C)
     also have "\<dots> = (\<Sum>c \<in> C k. (\<Sum> x \<in> space P \<inter> XC c. prob {x}))"
       using finite_edges by (subst sum.swap) (simp add: sum.inter_restrict XG_def XC_def space_eq)
     also have "\<dots> = (\<Sum>c \<in> C k. prob (XC c))"
       using fin_XC XC_in_sets
       by (auto simp add: prob_eq sets_eq space_eq intro!: sum.cong)
     finally show ?thesis by (simp add: XC_cyl)
   qed
   also have "\<dots> = (\<Sum>c\<in>C k. p ^ k)"
   proof -
     have "\<And>x. x \<in> C k \<Longrightarrow> card (set (uwalk_edges x)) = uwalk_length x"
       by (auto simp: uwalk_length_def C_def ucycles_distinct_edges intro: distinct_card)
     then show ?thesis by (auto simp: C_def ucycles_def uwalks_def cylinder_prob)
   qed
   also have "\<dots> = of_nat (fact n div fact (n - k)) * p ^ k"
   proof -
     have inj_last_Cons: "\<And>A. inj_on (\<lambda>es. last es # es) A" by (rule inj_onI) simp
     { fix xs A assume "3 \<le> length xs - Suc 0" "hd xs = last xs"
       then have "xs \<in> (\<lambda>xs. last xs # xs) ` A \<longleftrightarrow> tl xs \<in> A"
         by (cases xs) (auto simp: inj_image_mem_iff[OF inj_last_Cons] split: if_split_asm) }
     note image_mem_iff_inst = this
 
     { fix xs have "xs \<in> uwalks (edge_ugraph S_edges) \<Longrightarrow> set (tl xs) \<subseteq> S_verts"
         unfolding uwalks_def by (induct xs) auto }
     moreover
     { fix xs assume "set xs \<subseteq> S_verts" "2 \<le> length xs" "distinct xs"
       then have "(last xs # xs) \<in> uwalks (edge_ugraph S_edges)"
       proof (induct xs rule: uwalk_edges.induct)
         case (3 x y ys)
         have S_edges_memI: "\<And>x y. x \<in> S_verts \<Longrightarrow> y \<in> S_verts \<Longrightarrow> x \<noteq> y \<Longrightarrow> {x, y} \<in> S_edges"
           unfolding S_edges_def all_edges_def image_def by auto
 
         have "ys \<noteq> [] \<Longrightarrow> set ys \<subseteq> S_verts \<Longrightarrow> last ys \<in> S_verts"  by auto
         with 3 show ?case
           by (auto simp add: uwalks_def Suc_le_eq intro: S_edges_memI)
       qed simp_all}
     moreover note \<open>3 \<le> k\<close>
     ultimately
     have "C k = (\<lambda>xs. last xs # xs) ` {xs. length xs = k \<and> distinct xs \<and> set xs \<subseteq> S_verts}"
       by (auto simp: C_def ucycles_def uwalk_length_conv image_mem_iff_inst)
     moreover have "card S_verts = n" by (simp add: S_verts_def)
     ultimately have "card (C k) = fact n div fact (n - k)"
       using \<open>k < n\<close>
       by (simp add: card_image[OF inj_last_Cons] card_lists_distinct_length_eq' fact_div_fact)
     then show ?thesis by simp
   qed
   finally show ?thesis by simp
 qed
 
 text \<open>Girth-Chromatic number theorem:\<close>
 theorem girth_chromatic:
   fixes l :: nat
   shows "\<exists>G. uwellformed G \<and> l < girth G \<and> l < chromatic_number G"
 proof -
   define k where "k = max 3 l"
   define \<epsilon> where "\<epsilon> = 1 / (2 * k)"
   define p where "p n = real n powr (\<epsilon> - 1)" for n :: nat
 
   let ?ug = edge_space.edge_ugraph
 
   define short_count where "short_count g = card (short_cycles g k)" for g
     \<comment> \<open>This random variable differs from the one used in the proof of theorem 11.2.2,
           as we count the number of paths describing a circle, not the circles themselves\<close>
 
   from k_def have "3 \<le> k" "l \<le> k" by auto
   from \<open>3 \<le> k\<close> have \<epsilon>_props: "0 < \<epsilon>" "\<epsilon> < 1 / k" "\<epsilon> < 1" by (auto simp: \<epsilon>_def field_simps)
 
   have ev_p: "\<forall>\<^sup>\<infinity> n. 0 < p n \<and> p n < 1"
   proof (rule eventually_sequentiallyI)
     fix n :: nat assume "2 \<le> n"
     with \<open>\<epsilon> < 1\<close> have "n powr (\<epsilon> - 1) < 1" by (auto intro!: powr_less_one)
     then show "0 < p n \<and> p n < 1" using \<open>2 \<le> n\<close>
       by (auto simp: p_def)
   qed
   then
   have prob_short_count_le: "\<forall>\<^sup>\<infinity> n. probGn p n (\<lambda>es. (real n/2) \<le> short_count (?ug n es))
       \<le> 2 * (k - 2) * n powr (\<epsilon> * k - 1)"  (is "\<forall>\<^sup>\<infinity> n. ?P n")
   proof (elim eventually_rev_mp, intro eventually_sequentiallyI impI)
     fix n :: nat assume A: "Suc k \<le> n" "0 < p n \<and> p n < 1"
     then interpret pG: edge_space n "p n" by unfold_locales auto
     have "1 \<le> n" using A by auto
 
     define mean_short_count where "mean_short_count = (\<integral>es. short_count (?ug n es) \<partial> pG.P)"
 
     have mean_short_count_le: "mean_short_count \<le> (k - 2) * n powr (\<epsilon> * k)"
     proof -
       have small_empty: "\<And>es k. k \<le> 2 \<Longrightarrow> short_cycles (edge_space.edge_ugraph n es) k = {}"
           by (auto simp add: short_cycles_def ucycles_def)
       have short_count_conv: "\<And>es. short_count (?ug n es) = (\<Sum>i=3..k. real (card {c \<in> ucycles (?ug n es). uwalk_length c = i}))"
       proof (unfold short_count_def, induct k)
         case 0 with small_empty show ?case by auto
       next
         case (Suc k)
         show ?case proof (cases "Suc k \<le> 2")
           case True with small_empty show ?thesis by auto
         next
           case False
           have "{c \<in> ucycles (?ug n es). uwalk_length c \<le> Suc k}
               = {c \<in> ucycles (?ug n es). uwalk_length c \<le> k} \<union> {c \<in> ucycles (?ug n es). uwalk_length c = Suc k}"
             by auto
           moreover
           have "finite (uverts (edge_space.edge_ugraph n es))" by auto
           ultimately
           have "card {c \<in> ucycles (?ug n es). uwalk_length c \<le> Suc k}
             = card {c \<in> ucycles (?ug n es). uwalk_length c \<le> k} + card {c \<in> ucycles (?ug n es). uwalk_length c = Suc k}"
             using finite_ucycles by (subst card_Un_disjoint[symmetric]) auto
           then show ?thesis
             using Suc False unfolding short_cycles_def by (auto simp: not_le)
         qed
       qed
 
       have "mean_short_count = (\<Sum>i=3..k. \<integral>es. card {c \<in> ucycles (?ug n es). uwalk_length c = i} \<partial> pG.P)"
         unfolding mean_short_count_def short_count_conv
         by (subst Bochner_Integration.integral_sum) (auto intro: pG.integral_finite_singleton)
       also have "\<dots> = (\<Sum>i\<in>{3..k}. of_nat (fact n div fact (n - i)) * p n ^ i)"
         using A by (simp add: pG.mean_k_cycles)
       also have "\<dots> \<le> (\<Sum> i\<in>{3..k}. n ^ i * p n ^ i)"
         apply (rule sum_mono)
         by (meson A fact_div_fact_le_pow  Suc_leD atLeastAtMost_iff of_nat_le_iff order_trans mult_le_cancel_iff1 zero_less_power)
       also have "... \<le> (\<Sum> i\<in>{3..k}. n powr (\<epsilon> * k))"
         using \<open>1 \<le> n\<close> \<open>0 < \<epsilon>\<close> A
         by (intro sum_mono) (auto simp: p_def field_simps powr_mult_base powr_powr
           powr_realpow[symmetric] powr_mult[symmetric] powr_add[symmetric])
       finally show ?thesis by simp
     qed
 
     have "pG.prob {es \<in> space pG.P. n/2 \<le> short_count (?ug n es)} \<le> mean_short_count / (n/2)"
       unfolding mean_short_count_def using \<open>1 \<le> n\<close>
       by (intro pG.Markov_inequality) (auto simp: short_count_def)
     also have "\<dots> \<le> 2 * (k - 2) * n powr (\<epsilon> * k - 1)"
     proof -
       have "mean_short_count / (n / 2) \<le> 2 * (k - 2) * (1 / n powr 1) * n powr (\<epsilon> * k)"
         using mean_short_count_le \<open>1 \<le> n\<close> by (simp add: field_simps)
       then show ?thesis by (simp add: powr_diff algebra_simps)
     qed
     finally show "?P n" .
   qed
 
   define pf_short_count pf_\<alpha>
     where "pf_short_count n = probGn p n (\<lambda>es. n/2 \<le> short_count (?ug n es))"
       and "pf_\<alpha> n = probGn p n (\<lambda>es. 1/2 * n/k \<le> \<alpha> (edge_space.edge_ugraph n es))"
     for n
 
   have ev_short_count_le: "\<forall>\<^sup>\<infinity> n. pf_short_count n < 1 / 2"
   proof -
     have "\<epsilon> * k - 1 < 0"
       using \<epsilon>_props \<open>3 \<le> k\<close> by (auto simp: field_simps)
     then have "(\<lambda>n. 2 * (k - 2) * n powr (\<epsilon> * k - 1)) \<longlonglongrightarrow> 0" (is "?bound \<longlonglongrightarrow> 0")
       by (intro tendsto_mult_right_zero LIMSEQ_neg_powr)
     then have "\<forall>\<^sup>\<infinity> n. dist (?bound n) 0  < 1 / 2"
       by (rule tendstoD) simp
     with prob_short_count_le show ?thesis
       by (rule eventually_elim2) (auto simp: dist_real_def pf_short_count_def)
   qed
 
   have lim_\<alpha>: "pf_\<alpha> \<longlonglongrightarrow> 0"
   proof -
     have "0 < k" using \<open>3 \<le> k\<close> by simp
 
     have "\<forall>\<^sup>\<infinity> n. (6*k) * ln n / n \<le> p n \<longleftrightarrow> (6*k) * ln n * n powr - \<epsilon> \<le> 1"
     proof (rule eventually_sequentiallyI)
      fix n :: nat assume "1 \<le> n"
       then have "(6 * k) * ln n / n \<le> p n \<longleftrightarrow> (6*k) * ln n * (n powr - 1) \<le> n powr (\<epsilon> - 1)"
         by  (subst powr_minus) (simp add: divide_inverse p_def)
       also have "\<dots> \<longleftrightarrow> (6*k) * ln n * ((n powr - 1) / (n powr (\<epsilon> - 1))) \<le> n powr (\<epsilon> - 1) / (n powr (\<epsilon> - 1))"
         using \<open>1 \<le> n\<close> by (auto simp: field_simps)
       also have "\<dots> \<longleftrightarrow> (6*k) * ln n * n powr - \<epsilon> \<le> 1"
         by (simp add: powr_diff [symmetric] )
       finally show "(6*k) * ln n / n \<le> p n \<longleftrightarrow> (6*k) * ln n * n powr - \<epsilon> \<le> 1" .
     qed
     then have "(\<forall>\<^sup>\<infinity> n. (6 * k) * ln n / real n \<le> p n)
         \<longleftrightarrow> (\<forall>\<^sup>\<infinity> n. (6*k) * ln n * n powr - \<epsilon> \<le> 1)"
       by (rule eventually_subst)
     also have "\<forall>\<^sup>\<infinity> n. (6*k) * ln n * n powr - \<epsilon> \<le> 1"
     proof -
       { fix n :: nat assume "0 < n"
         have "ln (real n) \<le> n powr (\<epsilon>/2) / (\<epsilon>/2)"
           using \<open>0 < n\<close> \<open>0 < \<epsilon>\<close> by (intro ln_powr_bound) auto
         also have "\<dots> \<le> 2/\<epsilon> * n powr (\<epsilon>/2)" by (auto simp: field_simps)
         finally have "(6*k) * ln n * (n powr - \<epsilon>)  \<le> (6*k) * (2/\<epsilon> * n powr (\<epsilon>/2)) * (n powr - \<epsilon>)"
           using \<open>0 < n\<close> \<open>0 < k\<close> by (intro mult_right_mono mult_left_mono) auto
         also have "\<dots> = 12*k/\<epsilon> * n powr (-\<epsilon>/2)"
           unfolding divide_inverse
           by (auto simp: field_simps powr_minus[symmetric] powr_add[symmetric])
         finally have "(6*k) * ln n * (n powr - \<epsilon>) \<le> 12*k/\<epsilon> * n powr (-\<epsilon>/2)" .
       }
       then have "\<forall>\<^sup>\<infinity> n. (6*k) * ln n * (n powr - \<epsilon>) \<le> 12*k/\<epsilon> * n powr (-\<epsilon>/2)"
         by (intro eventually_sequentiallyI[of 1]) auto
       also have "\<forall>\<^sup>\<infinity> n. 12*k/\<epsilon> * n powr (-\<epsilon>/2) \<le> 1"
       proof -
         have "(\<lambda>n. 12*k/\<epsilon> * n powr (-\<epsilon>/2)) \<longlonglongrightarrow> 0"
           using \<open>0 < \<epsilon>\<close> by (intro tendsto_mult_right_zero LIMSEQ_neg_powr) auto
         then show ?thesis
           using \<open>0 < \<epsilon>\<close> by - (drule tendstoD[where e=1], auto elim: eventually_mono)
       qed
       finally (eventually_le_le) show ?thesis .
     qed
     finally have "\<forall>\<^sup>\<infinity> n. real (6 * k) * ln (real n) / real n \<le> p n" .
     with ev_p \<open>0 < k\<close> show ?thesis unfolding pf_\<alpha>_def by (rule almost_never_le_\<alpha>)
   qed
 
   from ev_short_count_le lim_\<alpha>[THEN tendstoD, of "1/2"] ev_p
   have "\<forall>\<^sup>\<infinity> n. 0 < p n \<and> p n < 1 \<and> pf_short_count n < 1/2 \<and> pf_\<alpha> n < 1/2"
     by simp (elim eventually_rev_mp, auto simp: eventually_sequentially dist_real_def)
   then obtain n where "0 < p n" "p n < 1" and [arith]: "0 < n"
       and probs: "pf_short_count n < 1/2" "pf_\<alpha> n < 1/2"
     by (auto simp: eventually_sequentially)
   then interpret ES: edge_space n "(p n)" by unfold_locales auto
 
   have rest_compl: "\<And>A P. A - {x\<in>A. P x} = {x\<in>A. \<not>P x}" by blast
 
   from probs have "ES.prob ({es \<in> space ES.P. n/2 \<le> short_count (?ug n es)}
       \<union> {es \<in> space ES.P. 1/2 * n/k \<le> \<alpha> (?ug n es)}) \<le> pf_short_count n + pf_\<alpha> n"
     unfolding pf_short_count_def pf_\<alpha>_def  by (subst ES.finite_measure_subadditive) auto
   also have "\<dots> < 1" using probs by auto
   finally have "0 < ES.prob (space ES.P - ({es \<in> space ES.P. n/2 \<le> short_count (?ug n es)}
       \<union> {es \<in> space ES.P. 1/2 * n/k \<le> \<alpha> (?ug n es)}))" (is "0 < ES.prob ?S")
     by (subst ES.prob_compl) auto
   also have "?S = {es \<in> space ES.P. short_count (?ug n es) < n/2 \<and> \<alpha> (?ug n es) < 1/2* n/k}" (is "\<dots> = ?C")
     by (auto simp: not_less rest_compl)
   finally have "?C \<noteq> {}" by (intro notI) (simp only:, auto)
   then obtain es where es_props: "es \<in> space ES.P"
       "short_count (?ug n es) < n/2" "\<alpha> (?ug n es) < 1/2 * n/k"
     by auto
     \<comment> \<open>now we obtained a high colored graph (few independent nodes) with almost no short cycles\<close>
 
   define G where "G = ?ug n es"
   define H where "H = kill_short G k"
 
   have G_props: "uverts G = {1..n}" "finite (uverts G)" "short_count G < n/2" "\<alpha> G < 1/2 * n/k"
     unfolding G_def using es_props by (auto simp: ES.S_verts_def)
 
   have "uwellformed G" by (auto simp: G_def uwellformed_def all_edges_def ES.S_edges_def)
   with G_props have T1: "uwellformed H" unfolding H_def by (intro kill_short_uwellformed)
 
   have "enat l \<le> enat k" using \<open>l \<le> k\<close> by simp
   also have "\<dots> < girth H" using G_props by (auto simp: kill_short_large_girth H_def)
   finally have T2: "l < girth H" .
 
   have card_H: "n/2 \<le> card (uverts H)"
     using G_props es_props kill_short_order_of_graph[of G k] by (simp add: short_count_def H_def)
 
   then have uverts_H: "uverts H \<noteq> {}" "0 < card (uverts H)" by auto
   then have "0 < \<alpha> H" using zero_less_\<alpha> uverts_H by auto
 
   have \<alpha>_HG: "\<alpha> H \<le> \<alpha> G"
     unfolding H_def G_def by (auto intro: kill_short_\<alpha>)
 
   have "enat l \<le> ereal k" using \<open>l \<le> k\<close> by auto
   also have "\<dots> < (n/2) / \<alpha> G" using G_props \<open>3 \<le> k\<close>
     by (cases "\<alpha> G") (auto simp: field_simps)
   also have "\<dots> \<le> (n/2) / \<alpha> H" using \<alpha>_HG \<open>0 < \<alpha> H\<close>
     by (auto simp: ereal_of_enat_pushout intro!: ereal_divide_left_mono)
   also have "\<dots> \<le> card (uverts H) / \<alpha> H" using card_H \<open>0 < \<alpha> H\<close>
     by (auto intro!: ereal_divide_right_mono)
   also have "\<dots> \<le> chromatic_number H" using uverts_H T1 by (intro chromatic_lb) auto
   finally have T3: "l < chromatic_number H"
     by (simp del: ereal_of_enat_simps)
 
   from T1 T2 T3 show ?thesis by fast
 qed
 
 end
diff --git a/thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy b/thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy
--- a/thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy
+++ b/thys/Random_Graph_Subgraph_Threshold/Prob_Lemmas.thy
@@ -1,342 +1,342 @@
 theory Prob_Lemmas
 imports
   "HOL-Probability.Probability"
   Girth_Chromatic.Girth_Chromatic
   Ugraph_Misc
 begin
 
 section\<open>Lemmas about probabilities\<close>
 
 text\<open>In this section, auxiliary lemmas for computing bounds on expectation and probabilites
 of random variables are set up.\<close>
 
 subsection\<open>Indicator variables and valid probability values\<close>
 
 abbreviation rind :: "'a set \<Rightarrow> 'a \<Rightarrow> real" where
 "rind \<equiv> indicator"
 
 lemma product_indicator:
   "rind A x * rind B x = rind (A \<inter> B) x"
 unfolding indicator_def
 by auto
 
 text\<open>We call a real number `valid' iff it is in the range 0 to 1, inclusively, and additionally
 `nonzero' iff it is neither 0 nor 1.\<close>
 
 abbreviation "valid_prob (p :: real) \<equiv> 0 \<le> p \<and> p \<le> 1"
 abbreviation "nonzero_prob (p :: real) \<equiv> 0 < p \<and> p < 1"
 
 text\<open>A function @{typ "'a \<Rightarrow> real"} is a `valid probability function' iff each value in the image
 is valid, and similarly for `nonzero'.\<close>
 
 abbreviation "valid_prob_fun f \<equiv> (\<forall>n. valid_prob (f n))"
 abbreviation "nonzero_prob_fun f \<equiv> (\<forall>n. nonzero_prob (f n))"
 
 lemma nonzero_fun_is_valid_fun: "nonzero_prob_fun f \<Longrightarrow> valid_prob_fun f"
 by (simp add: less_imp_le)
 
 subsection\<open>Expectation and variance\<close>
 
 context prob_space
 begin
 
 text\<open>Note that there is already a notion of independent sets (see @{term indep_set}), but we use
 the following -- simpler -- definition:\<close>
 
 definition "indep A B \<longleftrightarrow> prob (A \<inter> B) = prob A * prob B"
 
 text\<open>The probability of an indicator variable is equal to its expectation:\<close>
 
 lemma expectation_indicator:
   "A \<in> events \<Longrightarrow> expectation (rind A) = prob A"
   by simp
 
 text\<open>For a non-negative random variable @{term X}, the Markov inequality gives the following
 upper bound: \[ \Pr[X \ge a] \le \frac{\Ex[X]}{a} \]\<close>
 
 lemma markov_inequality:
   assumes "\<And>a. 0 \<le> X a" and "integrable M X" "0 < t"
   shows "prob {a \<in> space M. t \<le> X a} \<le> expectation X / t"
 proof -
   \<comment> \<open>proof adapted from @{thm [source] edge_space.Markov_inequality}, but generalized to arbitrary
        @{term prob_space}s\<close>
   have "(\<integral>\<^sup>+ x. ennreal (X x) \<partial>M) = (\<integral>x. X x \<partial>M)"
     using assms by (intro nn_integral_eq_integral) auto
   thus ?thesis
-    using assms nn_integral_Markov_inequality[of X M "space M" "1 / t"]
+    using assms nn_integral_Markov_inequality[of X "space M" M "1 / t"]
     by (auto cong: nn_integral_cong simp: emeasure_eq_measure ennreal_mult[symmetric])
 qed
 
 text\<open>$\Var[X] = \Ex[X^2] - \Ex[X]^2 $\<close>
 
 lemma variance_expectation:
   fixes X :: "'a \<Rightarrow> real"
   assumes "integrable M (\<lambda>x. (X x)^2)" and "X \<in> borel_measurable M"
   shows
     "integrable M (\<lambda>x. (X x - expectation X)^2)" (is ?integrable)
     "variance X = expectation (\<lambda>x. (X x)^2) - (expectation X)^2" (is ?variance)
 proof -
   have int: "integrable M X"
     using integrable_squareD[OF assms] by simp
 
   have "(\<lambda>x. (X x - expectation X)^2) = (\<lambda>x. (X x)^2 + (expectation X)^2 - (2 * X x * expectation X))"
     by (simp only: power2_diff)
   hence
     "variance X = expectation (\<lambda>x. (X x)^2) + (expectation X)^2 + expectation (\<lambda>x. - (2 * X x * expectation X))"
     ?integrable
     using integral_add by (simp add: int assms prob_space)+
 
   thus ?variance ?integrable
     by (simp add: int power2_eq_square)+
 qed
 
 text\<open>A corollary from the Markov inequality is Chebyshev's inequality, which gives an upper
 bound for the deviation of a random variable from its expectation:
 \[ \Pr[\left| Y - \Ex[Y] \right| \ge s] \le \frac{\Var[X]}{a^2} \]\<close>
 
 lemma chebyshev_inequality:
   fixes Y :: "'a \<Rightarrow> real"
   assumes Y_int: "integrable M (\<lambda>y. (Y y)^2)"
   assumes Y_borel: "Y \<in> borel_measurable M"
   fixes s :: "real"
   assumes s_pos: "0 < s"
   shows "prob {a \<in> space M. s \<le> \<bar>Y a - expectation Y\<bar>} \<le> variance Y / s^2"
 proof -
   let ?X = "\<lambda>a. (Y a - expectation Y)^2"
   let ?t = "s^2"
 
   have "0 < ?t"
     using s_pos by simp
   hence "prob {a \<in> space M. ?t \<le> ?X a} \<le> variance Y / s^2"
     using markov_inequality variance_expectation[OF Y_int Y_borel] by (simp add: field_simps)
   moreover have "{a \<in> space M. ?t \<le> ?X a} = {a \<in> space M. s \<le> \<bar>Y a - expectation Y\<bar>}"
     using abs_le_square_iff s_pos by force
   ultimately show ?thesis
     by simp
 qed
 
 text\<open>Hence, we can derive an upper bound for the probability that a random variable is $0$.\<close>
 
 corollary chebyshev_prob_zero:
   fixes Y :: "'a \<Rightarrow> real"
   assumes Y_int: "integrable M (\<lambda>y. (Y y)^2)"
   assumes Y_borel: "Y \<in> borel_measurable M"
   assumes \<mu>_pos: "expectation Y > 0"
   shows "prob {a \<in> space M. Y a = 0} \<le> expectation (\<lambda>y. (Y y)^2) / (expectation Y)^2 - 1"
 proof -
   let ?s = "expectation Y"
 
   have "prob {a \<in> space M. Y a = 0} \<le> prob {a \<in> space M. ?s \<le> \<bar>Y a - ?s\<bar>}"
     using Y_borel by (auto intro!: finite_measure_mono borel_measurable_diff borel_measurable_abs borel_measurable_le)
   also have "\<dots> \<le> variance Y / ?s^2"
     using assms by (fact chebyshev_inequality)
   also have "\<dots> = (expectation (\<lambda>y. (Y y)^2) - ?s^2) / ?s^2"
     using Y_int Y_borel by (simp add: variance_expectation)
   also have "\<dots> = expectation (\<lambda>y. (Y y)^2) / ?s^2 - 1"
     using \<mu>_pos by (simp add: field_simps)
   finally show ?thesis .
 qed
 
 end
 
 subsection\<open>Sets of indicator variables\<close>
 
 text\<open>\label{sec:delta}
 This section introduces some inequalities about expectation and other values related to the sum of
 a set of random indicators.\<close>
 
 locale prob_space_with_indicators = prob_space +
   fixes I :: "'i set"
   assumes finite_I: "finite I"
 
   fixes A :: "'i \<Rightarrow> 'a set"
   assumes A: "A ` I \<subseteq> events"
 
   assumes prob_non_zero: "\<exists>i \<in> I. 0 < prob (A i)"
 begin
 
 text\<open>We call the underlying sets @{term "A i"} for each @{term "i \<in> I"}, and the corresponding
 indicator variables @{term "X i"}. The sum is denoted by @{term Y}, and its expectation by
 @{term \<mu>}.\<close>
 
 definition "X i = rind (A i)"
 definition "Y x = (\<Sum>i \<in> I. X i x)"
 
 definition "\<mu> = expectation Y"
 
 text\<open>In the lecture notes, the following two relations are called $\sim$ and $\nsim$,
 respectively. Note that they are not the opposite of each other.\<close>
 
 abbreviation ineq_indep :: "'i \<Rightarrow> 'i \<Rightarrow> bool" where
 "ineq_indep i j \<equiv> (i \<noteq> j \<and> indep (A i) (A j))"
 
 abbreviation ineq_dep :: "'i \<Rightarrow> 'i \<Rightarrow> bool" where
 "ineq_dep i j \<equiv> (i \<noteq> j \<and> \<not>indep (A i) (A j))"
 
 definition "\<Delta>\<^sub>a = (\<Sum>i \<in> I. \<Sum>j | j \<in> I \<and> i \<noteq> j. prob (A i \<inter> A j))"
 definition "\<Delta>\<^sub>d = (\<Sum>i \<in> I. \<Sum>j | j \<in> I \<and> ineq_dep i j. prob (A i \<inter> A j))"
 
 lemma \<Delta>_zero:
   assumes "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<noteq> j \<Longrightarrow> indep (A i) (A j)"
   shows "\<Delta>\<^sub>d = 0"
 proof -
   {
     fix i
     assume "i \<in> I"
     hence "{j. j \<in> I \<and> ineq_dep i j} = {}"
       using assms by auto
     hence "(\<Sum>j | j \<in> I \<and> ineq_dep i j. prob (A i \<inter> A j)) = 0"
       using sum.empty by metis
   }
   hence "\<Delta>\<^sub>d = (0 :: real) * card I"
     unfolding \<Delta>\<^sub>d_def by simp
   thus ?thesis
     by simp
 qed
 
 lemma A_events[measurable]: "i \<in> I \<Longrightarrow> A i \<in> events"
 using A by auto
 
 lemma expectation_X_Y: "\<mu> = (\<Sum>i\<in>I. expectation (X i))"
 unfolding \<mu>_def Y_def[abs_def] X_def
 by (simp add: less_top[symmetric])
 
 lemma expectation_X_non_zero: "\<exists>i \<in> I. 0 < expectation (X i)"
 unfolding X_def using prob_non_zero expectation_indicator by simp
 
 corollary \<mu>_non_zero[simp]: "0 < \<mu>"
 unfolding expectation_X_Y
 using expectation_X_non_zero
 by (auto intro!: sum_lower finite_I
          simp add: expectation_indicator X_def)
 
 lemma \<Delta>\<^sub>d_nonneg: "0 \<le> \<Delta>\<^sub>d"
 unfolding \<Delta>\<^sub>d_def
 by (simp add: sum_nonneg)
 
 corollary \<mu>_sq_non_zero[simp]: "0 < \<mu>^2"
 by (rule zero_less_power) simp
 
 lemma Y_square_unfold: "(\<lambda>x. (Y x)^2) = (\<lambda>x. \<Sum>i \<in> I. \<Sum>j \<in> I. rind (A i \<inter> A j) x)"
 unfolding fun_eq_iff Y_def X_def
 by (auto simp: sum_square product_indicator)
 
 lemma integrable_Y_sq[simp]: "integrable M (\<lambda>y. (Y y)^2)"
 unfolding Y_square_unfold
 by (simp add: sets.Int less_top[symmetric])
 
 lemma measurable_Y[measurable]: "Y \<in> borel_measurable M"
 unfolding Y_def[abs_def] X_def by simp
 
 lemma expectation_Y_\<Delta>: "expectation (\<lambda>x. (Y x)^2) = \<mu> + \<Delta>\<^sub>a"
 proof -
   let ?ei = "\<lambda>i j. expectation (rind (A i \<inter> A j))"
 
   have "expectation (\<lambda>x. (Y x)^2) = (\<Sum>i \<in> I. \<Sum>j \<in> I. ?ei i j)"
     unfolding Y_square_unfold by (simp add: less_top[symmetric])
   also have "\<dots> = (\<Sum>i \<in> I. \<Sum>j \<in> I. if i = j then ?ei i j else ?ei i j)"
     by simp
   also have "\<dots> = (\<Sum>i \<in> I. (\<Sum>j | j \<in> I \<and> i = j. ?ei i j) + (\<Sum>j | j \<in> I \<and> i \<noteq> j. ?ei i j))"
     by (simp only: sum_split[OF finite_I])
   also have "\<dots> = (\<Sum>i \<in> I. \<Sum>j | j \<in> I \<and> i = j. ?ei i j) + (\<Sum>i \<in> I. \<Sum>j | j \<in> I \<and> i \<noteq> j. ?ei i j)" (is "_ = ?lhs + ?rhs")
     by (fact sum.distrib)
   also have "\<dots> =  \<mu> + \<Delta>\<^sub>a"
     proof -
       have "?lhs = \<mu>"
         proof -
           {
             fix i
             assume i: "i \<in> I"
             have "(\<Sum>j | j \<in> I \<and> i = j. ?ei i j) = (\<Sum>j | j \<in> I \<and> i = j. ?ei i i)"
               by simp
             also have "\<dots> = (\<Sum>j | i = j. ?ei i i)"
               using i by metis
             also have "\<dots> = expectation (rind (A i))"
               by auto
             finally have "(\<Sum>j | j \<in> I \<and> i = j. ?ei i j) = \<dots>" .
           }
           hence "?lhs = (\<Sum>i\<in>I. expectation (rind (A i)))"
             by force
           also have "\<dots> = \<mu>"
             unfolding expectation_X_Y X_def ..
           finally show "?lhs = \<mu>" .
         qed
       moreover have "?rhs = \<Delta>\<^sub>a"
         proof -
           {
             fix i j
             assume "i \<in> I" "j \<in> I"
             with A have "A i \<inter> A j \<in> events" by blast
             hence "?ei i j = prob (A i \<inter> A j)"
               by (fact expectation_indicator)
           }
           thus ?thesis
             unfolding \<Delta>\<^sub>a_def by simp
         qed
       ultimately show "?lhs + ?rhs = \<mu> + \<Delta>\<^sub>a"
         by simp
     qed
   finally show ?thesis .
 qed
 
 lemma \<Delta>_expectation_X: "\<Delta>\<^sub>a \<le> \<mu>^2 + \<Delta>\<^sub>d"
 proof -
   let ?p = "\<lambda>i j. prob (A i \<inter> A j)"
   let ?p' = "\<lambda>i j. prob (A i) * prob (A j)"
   let ?ie = "\<lambda>i j. indep (A i) (A j)"
 
   have "\<Delta>\<^sub>a = (\<Sum>i \<in> I. \<Sum>j | j \<in> I \<and> i \<noteq> j. if ?ie i j then ?p i j else ?p i j)"
     unfolding \<Delta>\<^sub>a_def by simp
   also have "\<dots> = (\<Sum>i \<in> I. (\<Sum>j | j \<in> I \<and> ineq_indep i j. ?p i j) + (\<Sum>j | j \<in> I \<and> ineq_dep i j. ?p i j))"
     by (simp only: sum_split2[OF finite_I])
   also have "\<dots> = (\<Sum>i \<in> I. \<Sum>j | j \<in> I \<and> ineq_indep i j. ?p i j) + \<Delta>\<^sub>d" (is "_ = ?lhs + _")
     unfolding \<Delta>\<^sub>d_def by (fact sum.distrib)
   also have "\<dots> \<le> \<mu>^2 + \<Delta>\<^sub>d"
     proof (rule add_right_mono)
       have "(\<Sum>i\<in>I. \<Sum>j | j \<in> I \<and> ineq_indep i j. ?p i j) = (\<Sum>i \<in> I. \<Sum>j | j \<in> I \<and> ineq_indep i j. ?p' i j)"
         unfolding indep_def by simp
       also have "\<dots> \<le> (\<Sum>i \<in> I. \<Sum>j \<in> I. ?p' i j)"
         proof (rule sum_mono)
           fix i
           assume "i \<in> I"
           show "(\<Sum>j | j \<in> I \<and> ineq_indep i j. ?p' i j) \<le> (\<Sum>j\<in>I. ?p' i j)"
             by (rule sum_upper[OF finite_I]) (simp add: zero_le_mult_iff)
         qed
       also have "\<dots> = (\<Sum>i \<in> I. prob (A i))^2"
         by (fact sum_square[symmetric])
       also have "\<dots> = (\<Sum>i \<in> I. expectation (X i))^2"
         unfolding X_def using expectation_indicator A by simp
       also have "\<dots> = \<mu>^2"
         using expectation_X_Y[symmetric] by simp
       finally show "?lhs \<le> \<mu>^2" .
     qed
   finally show ?thesis .
 qed
 
 lemma prob_\<mu>_\<Delta>\<^sub>a: "prob {a \<in> space M. Y a = 0} \<le> 1 / \<mu> + \<Delta>\<^sub>a / \<mu>^2 - 1"
 proof -
   have "prob {a \<in> space M. Y a = 0} \<le> expectation (\<lambda>y. (Y y)^2) / \<mu>^2 - 1"
     unfolding \<mu>_def by (rule chebyshev_prob_zero) (simp add: \<mu>_def[symmetric])+
   also have "\<dots> = (\<mu> + \<Delta>\<^sub>a) / \<mu>^2 - 1"
     using expectation_Y_\<Delta> by simp
   also have "\<dots> = 1 / \<mu> + \<Delta>\<^sub>a / \<mu>^2 - 1"
     unfolding power2_eq_square by (simp add: field_simps add_divide_distrib)
   finally show ?thesis .
 qed
 
 lemma prob_\<mu>_\<Delta>\<^sub>d: "prob {a \<in> space M. Y a = 0} \<le> 1/\<mu> + \<Delta>\<^sub>d/\<mu>^2"
 proof -
   have "prob {a \<in> space M. Y a = 0} \<le> 1/\<mu> + \<Delta>\<^sub>a/\<mu>^2 - 1"
     by (fact prob_\<mu>_\<Delta>\<^sub>a)
   also have "\<dots> = (1/\<mu> - 1) + \<Delta>\<^sub>a/\<mu>^2"
     by simp
   also have "\<dots> \<le> (1/\<mu> - 1) + (\<mu>^2 + \<Delta>\<^sub>d)/\<mu>^2"
     using divide_right_mono[OF \<Delta>_expectation_X] by simp
   also have "\<dots> = 1/\<mu> + \<Delta>\<^sub>d/\<mu>^2"
     using \<mu>_sq_non_zero by (simp add: field_simps)
   finally show ?thesis .
 qed
 
 end
 
 end
diff --git a/thys/Skip_Lists/Geometric_PMF.thy b/thys/Skip_Lists/Geometric_PMF.thy
--- a/thys/Skip_Lists/Geometric_PMF.thy
+++ b/thys/Skip_Lists/Geometric_PMF.thy
@@ -1,345 +1,244 @@
 (*
   File:    Pi_pmf.thy
   Authors: Manuel Eberl, Max W. Haslbeck
 *)
 section \<open>Theorems about the Geometric Distribution\<close>
 theory Geometric_PMF
   imports
     "HOL-Probability.Probability"
     Pi_pmf
     "Monad_Normalisation.Monad_Normalisation"
 begin
 
-lemma geometric_sums_times_n:
-  fixes c::"'a::{banach,real_normed_field}"
-  assumes "norm c < 1"
-  shows "(\<lambda>n. c^n * of_nat n) sums (c / (1 - c)\<^sup>2)"
-proof -
-  have "(\<lambda>n. c * z ^ n) sums (c / (1 - z))" if "norm z < 1" for z
-    using geometric_sums sums_mult that by fastforce
-  moreover have "((\<lambda>z. c / (1 - z)) has_field_derivative (c / (1 - c)\<^sup>2)) (at c)"
-      using assms by (auto intro!: derivative_eq_intros simp add: semiring_normalization_rules)
-  ultimately have "(\<lambda>n. diffs (\<lambda>n. c) n * c ^ n) sums (c / (1 - c)\<^sup>2)"
-    using assms by (intro termdiffs_sums_strong)
-  then have "(\<lambda>n. of_nat (Suc n) * c ^ (Suc n)) sums (c / (1 - c)\<^sup>2)"
-    unfolding diffs_def by (simp add: power_eq_if mult.assoc)
-  then show ?thesis
-    by (subst (asm) sums_Suc_iff) (auto simp add: mult.commute)
-qed
-
-lemma geometric_sums_times_norm:
-  fixes c::"'a::{banach,real_normed_field}"
-  assumes "norm c < 1"
-  shows "(\<lambda>n. norm (c^n * of_nat n)) sums (norm c / (1 - norm c)\<^sup>2)"
-proof -
-  have "norm (c^n * of_nat n) = (norm c) ^ n * of_nat n" for n::nat
-    by (simp add: norm_power norm_mult)
-  then show ?thesis
-    using geometric_sums_times_n[of "norm c"] assms
-    by force
-qed
-
-lemma integrable_real_geometric_pmf:
-  assumes "p \<in> {0<..1}"
-  shows   "integrable (geometric_pmf p) real"
-proof -
-  have "summable (\<lambda>x. p * ((1 - p) ^ x * real x))"
-    using geometric_sums_times_norm[of "1 - p"] assms
-    by (intro summable_mult) (auto simp: sums_iff)
-  hence "summable (\<lambda>x. (1 - p) ^ x * real x)"
-    by (rule summable_mult_D) (use assms in auto)
-  thus ?thesis
-    unfolding measure_pmf_eq_density using assms
-    by (subst integrable_density)
-       (auto simp: integrable_count_space_nat_iff mult_ac)
-qed
-
-lemma expectation_geometric_pmf:
-  assumes "p \<in> {0<..1}"
-  shows   "measure_pmf.expectation (geometric_pmf p) real = (1 - p) / p"
-proof -
-  have "(\<lambda>n. p * ((1 - p) ^ n * n)) sums (p * ((1 - p) / p^2))"
-    using assms geometric_sums_times_n[of "1-p"] by (intro sums_mult) auto
-  moreover have "(\<lambda>n. p * ((1 - p) ^ n * n)) = (\<lambda>n. (1 - p) ^ n * p  * real n)"
-    by auto
-  ultimately have *: "(\<lambda>n. (1 - p) ^ n * p  * real n) sums ((1 - p) / p)"
-    using assms sums_subst by (auto simp add: power2_eq_square)
-  have "measure_pmf.expectation (geometric_pmf p) real =
-        (\<integral>n. pmf (geometric_pmf p) n * real n \<partial>count_space UNIV)"
-    unfolding measure_pmf_eq_density by (subst integral_density) auto
-  also have "integrable (count_space UNIV) (\<lambda>n. pmf (geometric_pmf p) n * real n)"
-    using * assms unfolding integrable_count_space_nat_iff by (simp add: sums_iff)
-  hence "(\<integral>n. pmf (geometric_pmf p) n * real n \<partial>count_space UNIV) = (1 - p) / p"
-    using * assms by (subst integral_count_space_nat) (simp_all add: sums_iff)
-  finally show ?thesis by auto
-qed
-
 lemma nn_integral_geometric_pmf:
   assumes "p \<in> {0<..1}"
   shows   "nn_integral (geometric_pmf p) real = (1 - p) / p"
  using assms expectation_geometric_pmf integrable_real_geometric_pmf
   by (subst nn_integral_eq_integral) auto
 
-lemma geometric_bind_pmf_unfold:
-  assumes "p \<in> {0<..1}"
-  shows "geometric_pmf p =
-     do {b \<leftarrow> bernoulli_pmf p;
-         if b then return_pmf 0 else map_pmf Suc (geometric_pmf p)}"
-proof -
-  have *: "(Suc -` {i}) = (if i = 0 then {} else {i - 1})" for i
-    by force
-  have "pmf (geometric_pmf p) i =
-        pmf (bernoulli_pmf p \<bind>
-            (\<lambda>b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p)))
-            i" for i
-  proof -
-    have "pmf (geometric_pmf p) i =
-          (if i = 0 then p else (1 - p) * pmf (geometric_pmf p) (i - 1))"
-      using assms by (simp add: power_eq_if)
-    also have "\<dots> = (if i = 0  then p else (1 - p) * pmf (map_pmf Suc (geometric_pmf p)) i)"
-      by (simp add: pmf_map indicator_def measure_pmf_single *)
-    also have "\<dots> = measure_pmf.expectation (bernoulli_pmf p)
-          (\<lambda>x. pmf (if x then return_pmf 0 else map_pmf Suc (geometric_pmf p)) i)"
-      using assms by (auto simp add: pmf_map *)
-    also have "\<dots> = pmf (bernoulli_pmf p \<bind>
-                   (\<lambda>b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p)))
-                   i"
-      by (auto simp add: pmf_bind)
-    finally show ?thesis .
-  qed
-  then show ?thesis
-    using pmf_eqI by blast
-qed
-
-lemma "p \<in> {0<..<1} \<Longrightarrow> set_pmf (geometric_pmf p) = UNIV"
-  by (auto simp add: measure_pmf_single set_pmf_def)
-
-lemma "set_pmf (geometric_pmf 1) = 0"
-  by (auto simp add: measure_pmf_single set_pmf_def)
-
 lemma geometric_pmf_prob_atMost:
   assumes "p \<in> {0<..1}"
   shows  "measure_pmf.prob (geometric_pmf p) {..n} = (1 - (1 - p)^(n + 1))"
 proof -
   have "(\<Sum>x\<le>n. (1 - p) ^ x * p) = 1 - (1 - p) * (1 - p) ^ n"
     by (induction n) (auto simp add: algebra_simps)
   then show ?thesis
   using assms by (auto simp add: measure_pmf_conv_infsetsum)
 qed
 
 lemma geometric_pmf_prob_lessThan:
   assumes "p \<in> {0<..1}"
   shows  "measure_pmf.prob (geometric_pmf p) {..<n} = 1 - (1 - p) ^ n"
 proof -
   have "(\<Sum>x<n. (1 - p) ^ x * p) = 1 - (1 - p) ^ n"
     by (induction n) (auto simp add: algebra_simps)
   then show ?thesis
   using assms by (auto simp add: measure_pmf_conv_infsetsum)
 qed
 
 lemma geometric_pmf_prob_greaterThan:
   assumes "p \<in> {0<..1}"
   shows  "measure_pmf.prob (geometric_pmf p) {n<..} = (1 - p)^(n + 1)"
 proof -
   have "(UNIV - {..n}) = {n<..}"
     by auto
   moreover have "measure_pmf.prob (geometric_pmf p) (UNIV - {..n}) = (1 - p) ^ (n + 1)"
     using assms by (subst measure_pmf.finite_measure_Diff)
                    (auto simp add: geometric_pmf_prob_atMost)
   ultimately show ?thesis
     by auto
 qed
 
 lemma geometric_pmf_prob_atLeast:
   assumes "p \<in> {0<..1}"
   shows  "measure_pmf.prob (geometric_pmf p) {n..} = (1 - p)^n"
 proof -
   have "(UNIV - {..<n}) = {n..}"
     by auto
   moreover have "measure_pmf.prob (geometric_pmf p) (UNIV - {..<n}) = (1 - p) ^ n"
     using assms by (subst measure_pmf.finite_measure_Diff)
                    (auto simp add: geometric_pmf_prob_lessThan)
   ultimately show ?thesis
     by auto
 qed
 
 lemma bernoulli_pmf_of_set':
   assumes "finite A"
   shows "map_pmf (\<lambda>b. {x \<in> A. \<not> b x}) (Pi_pmf A P (\<lambda>_. bernoulli_pmf (1/2))) = pmf_of_set (Pow A)"
 proof -
   have *: "Pi_pmf A P (\<lambda>_. pmf_of_set (UNIV :: bool set)) = pmf_of_set (PiE_dflt A P (\<lambda>_. UNIV :: bool set))"
     using assms by (intro Pi_pmf_of_set) auto
   have "map_pmf (\<lambda>b. {x \<in> A. \<not> b x}) (Pi_pmf A P (\<lambda>_. bernoulli_pmf (1 / 2))) =
         map_pmf (\<lambda>b. {x \<in> A. \<not> b x}) (Pi_pmf A P (\<lambda>_. pmf_of_set UNIV))"
     using bernoulli_pmf_half_conv_pmf_of_set by auto
   also have "\<dots> = map_pmf (\<lambda>b. {x \<in> A. \<not> b x}) (pmf_of_set (PiE_dflt A P (\<lambda>_. UNIV)))"
     using assms by (subst Pi_pmf_of_set) (auto)
   also have "\<dots> = pmf_of_set (Pow A)"
   proof -
     have "bij_betw (\<lambda>b. {x \<in> A. \<not> b x}) (PiE_dflt A P (\<lambda>_. UNIV)) (Pow A)"
       by (rule bij_betwI[of _ _ _ "\<lambda>B b. if b \<in> A then \<not> (b \<in> B) else P"]) (auto simp add: PiE_dflt_def)
     then show ?thesis
       using assms by (intro map_pmf_of_set_bij_betw) auto
   qed
   finally show ?thesis
     by simp
 qed
 
 lemma Pi_pmf_pmf_of_set_Suc:
   assumes "finite A"
   shows "Pi_pmf A 0 (\<lambda>_. geometric_pmf (1/2)) =
        do {
          B \<leftarrow> pmf_of_set (Pow A);
          Pi_pmf B 0 (\<lambda>_. map_pmf Suc (geometric_pmf (1/2))) }"
 proof -
   have "Pi_pmf A 0 (\<lambda>_. geometric_pmf (1/2)) =
         Pi_pmf A 0 (\<lambda>_. bernoulli_pmf (1/2) \<bind>
         (\<lambda>b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))"
     using assms by (subst geometric_bind_pmf_unfold) auto
   also have "\<dots> =
              Pi_pmf A False (\<lambda>_. bernoulli_pmf (1/2)) \<bind>
              (\<lambda>b. Pi_pmf A 0 (\<lambda>x. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))"
     using assms by (subst Pi_pmf_bind[of _ _ _ _ False]) auto
   also have "\<dots> =
              do {b \<leftarrow> Pi_pmf A False (\<lambda>_. bernoulli_pmf (1/2));
                  Pi_pmf {x \<in> A. ~b x} 0 (\<lambda>x. map_pmf Suc (geometric_pmf (1/2)))}"
     using assms by (subst Pi_pmf_if_set') auto
   also have "\<dots> =
              do {B \<leftarrow> map_pmf (\<lambda>b. {x \<in> A. \<not> b x}) (Pi_pmf A False (\<lambda>_. bernoulli_pmf (1/2)));
                  Pi_pmf B 0 (\<lambda>x. map_pmf Suc (geometric_pmf (1/2)))}"
     unfolding map_pmf_def apply(subst bind_assoc_pmf) apply(subst bind_return_pmf) by auto
   also have "\<dots> = pmf_of_set (Pow A) \<bind> (\<lambda>B. Pi_pmf B 0 (\<lambda>x. map_pmf Suc (geometric_pmf (1 / 2))))"
     unfolding assms using assms by (subst bernoulli_pmf_of_set') auto
   finally show ?thesis
     by simp
 qed
 
 lemma Pi_pmf_pmf_of_set_Suc':
   assumes "finite A"
   shows "Pi_pmf A 0 (\<lambda>_. geometric_pmf (1/2)) =
        do {
          B \<leftarrow> pmf_of_set (Pow A);
          Pi_pmf B 0 (\<lambda>_. map_pmf Suc (geometric_pmf (1/2))) }"
 proof -
   have "Pi_pmf A 0 (\<lambda>_. geometric_pmf (1/2)) =
         Pi_pmf A 0 (\<lambda>_. bernoulli_pmf (1/2) \<bind>
         (\<lambda>b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))"
     using assms by (subst geometric_bind_pmf_unfold) auto
   also have "\<dots> =
              Pi_pmf A False (\<lambda>_. bernoulli_pmf (1/2)) \<bind>
              (\<lambda>b. Pi_pmf A 0 (\<lambda>x. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf (1/2))))"
     using assms by (subst Pi_pmf_bind[of _ _ _ _ False]) auto
   also have "\<dots> =
              do {b \<leftarrow> Pi_pmf A False (\<lambda>_. bernoulli_pmf (1/2));
                  Pi_pmf {x \<in> A. ~b x} 0 (\<lambda>x. map_pmf Suc (geometric_pmf (1/2)))}"
     using assms by (subst Pi_pmf_if_set') auto
   also have "\<dots> =
              do {B \<leftarrow> map_pmf (\<lambda>b. {x \<in> A. \<not> b x}) (Pi_pmf A False (\<lambda>_. bernoulli_pmf (1/2)));
                  Pi_pmf B 0 (\<lambda>x. map_pmf Suc (geometric_pmf (1/2)))}"
     unfolding map_pmf_def by (auto simp add: bind_assoc_pmf bind_return_pmf)
   also have "\<dots> = pmf_of_set (Pow A) \<bind> (\<lambda>B. Pi_pmf B 0 (\<lambda>x. map_pmf Suc (geometric_pmf (1 / 2))))"
     unfolding assms using assms by (subst bernoulli_pmf_of_set') auto
   finally show ?thesis
     by simp
 qed
 
 lemma binomial_pmf_altdef':
   fixes A :: "'a set"
   assumes "finite A" and "card A = n" and p: "p \<in> {0..1}"
   shows   "binomial_pmf n p =
              map_pmf (\<lambda>f. card {x\<in>A. f x}) (Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p))" (is "?lhs = ?rhs")
 proof -
   from assms have "?lhs = binomial_pmf (card A) p"
     by simp
   also have "\<dots> = ?rhs"
   using assms(1)
   proof (induction rule: finite_induct)
     case empty
     with p show ?case by (simp add: binomial_pmf_0)
   next
     case (insert x A)
     from insert.hyps have "card (insert x A) = Suc (card A)"
       by simp
     also have "binomial_pmf \<dots> p = do {
                                      b \<leftarrow> bernoulli_pmf p;
                                      f \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p);
                                      return_pmf ((if b then 1 else 0) + card {y \<in> A. f y})
                                    }"
       using p by (simp add: binomial_pmf_Suc insert.IH bind_map_pmf)
     also have "\<dots> = do {
                       b \<leftarrow> bernoulli_pmf p;
                       f \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p);
                       return_pmf (card {y \<in> insert x A. (f(x := b)) y})
                     }"
     proof (intro bind_pmf_cong refl, goal_cases)
       case (1 b f)
       have "(if b then 1 else 0) + card {y\<in>A. f y} = card ((if b then {x} else {}) \<union> {y\<in>A. f y})"
         using insert.hyps by auto
       also have "(if b then {x} else {}) \<union> {y\<in>A. f y} = {y\<in>insert x A. (f(x := b)) y}"
         using insert.hyps by auto
       finally show ?case by simp
     qed
     also have "\<dots> = map_pmf (\<lambda>f. card {y\<in>insert x A. f y})
                       (Pi_pmf (insert x A) dflt (\<lambda>_. bernoulli_pmf p))"
       using insert.hyps by (subst Pi_pmf_insert) (simp_all add: pair_pmf_def map_bind_pmf)
     finally show ?case .
   qed
   finally show ?thesis .
 qed
 
 lemma bernoulli_pmf_Not:
   assumes "p \<in> {0..1}"
   shows "bernoulli_pmf p = map_pmf Not (bernoulli_pmf (1 - p))"
 proof -
   have *: "(Not -` {True}) = {False}" "(Not -` {False}) = {True}"
     by blast+
   have "pmf (bernoulli_pmf p) b = pmf (map_pmf Not (bernoulli_pmf (1 - p))) b" for b
     using assms by (cases b) (auto simp add: pmf_map * measure_pmf_single)
   then show ?thesis
     by (rule pmf_eqI)
 qed
 
 lemma binomial_pmf_altdef'':
   assumes p: "p \<in> {0..1}"
   shows   "binomial_pmf n p =
            map_pmf (\<lambda>f. card {x. x < n \<and> f x}) (Pi_pmf {..<n} dflt (\<lambda>_. bernoulli_pmf p))"
   using assms by (subst binomial_pmf_altdef'[of "{..<n}"]) (auto)
 
 context includes monad_normalisation
 begin
 
 lemma Pi_pmf_geometric_filter:
   assumes "finite A" "p \<in> {0<..1}"
   shows "Pi_pmf A 0 (\<lambda>_. geometric_pmf p) =
        do {
          fb \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p);
          Pi_pmf {x \<in> A. \<not> fb x} 0 (\<lambda>_. map_pmf Suc (geometric_pmf p)) }"
 proof -
   have "Pi_pmf A 0 (\<lambda>_. geometric_pmf p) =
         Pi_pmf A 0 (\<lambda>_. bernoulli_pmf p \<bind>
                    (\<lambda>b. if b then return_pmf 0 else map_pmf Suc (geometric_pmf p)))"
     using assms by (subst geometric_bind_pmf_unfold) auto
   also have "\<dots> =
              Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p) \<bind>
              (\<lambda>b. Pi_pmf A 0 (\<lambda>x. if b x then return_pmf 0 else map_pmf Suc (geometric_pmf p)))"
     using assms by (subst Pi_pmf_bind[of _ _ _ _ dflt]) auto
   also have "\<dots> =
              do {b \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf p);
                  Pi_pmf {x \<in> A. \<not> b x} 0 (\<lambda>x. map_pmf Suc (geometric_pmf p))}"
     using assms by (subst Pi_pmf_if_set') (auto)
   finally show ?thesis
     by simp
 qed
 
 lemma Pi_pmf_geometric_filter':
   assumes "finite A" "p \<in> {0<..1}"
   shows "Pi_pmf A 0 (\<lambda>_. geometric_pmf p) =
        do {
          fb \<leftarrow> Pi_pmf A dflt (\<lambda>_. bernoulli_pmf (1 - p));
          Pi_pmf {x \<in> A. fb x} 0 (\<lambda>_. map_pmf Suc (geometric_pmf p)) }"
   using assms by (auto simp add: Pi_pmf_geometric_filter[of _ _ "\<not> dflt"] bernoulli_pmf_Not[of p]
       Pi_pmf_map[of _ _ dflt] map_pmf_def[of "((\<circ>) Not)"])
 
 end
 
 end
diff --git a/thys/Skip_Lists/Skip_List.thy b/thys/Skip_Lists/Skip_List.thy
--- a/thys/Skip_Lists/Skip_List.thy
+++ b/thys/Skip_Lists/Skip_List.thy
@@ -1,1346 +1,1345 @@
 (*
   File:    Skip_List.thy
   Authors: Max W. Haslbeck, Manuel Eberl
 *)
 
 section \<open>Randomized Skip Lists\<close>
 theory Skip_List
   imports Geometric_PMF
-          Pi_pmf
           Misc
           "Monad_Normalisation.Monad_Normalisation"
 begin
 
 subsection \<open>Preliminaries\<close>
 
 lemma bind_pmf_if': "(do {c \<leftarrow> C;
                          ab \<leftarrow> (if c then A else B);
                          D ab}::'a pmf) =
                      do {c \<leftarrow> C;
                          (if c then (A \<bind> D) else (B \<bind> D))}"
   by (metis (mono_tags, lifting))
 
 abbreviation (input) Max\<^sub>0 where "Max\<^sub>0 \<equiv> (\<lambda>A. Max (A \<union> {0}))"
 
 
 subsection \<open>Definition of a Randomised Skip List\<close>
 
 text \<open>
   Given a set A we assign a geometric random variable (counting the number of failed Bernoulli
   trials before the first success) to every element in A. That means an arbitrary element of A is
   on level n with probability $(1-p)^{n}p$. We define he height of the skip list as the maximum
   assigned level. So a skip list with only one level has height 0 but the calculation of the
   expected height is cleaner this way.
 \<close>
 
 locale random_skip_list =
   fixes p::real
 begin
 
 definition q where "q = 1 - p"
 
 definition SL :: "('a::linorder) set \<Rightarrow> ('a \<Rightarrow> nat) pmf" where "SL A = Pi_pmf A 0 (\<lambda>_. geometric_pmf p)"
 definition SL\<^sub>N :: "nat \<Rightarrow> (nat \<Rightarrow> nat) pmf" where "SL\<^sub>N n = SL {..<n}"
 
 subsection \<open>Height of Skip List\<close>
 
 definition H where "H A = map_pmf (\<lambda>f. Max\<^sub>0 (f ` A)) (SL A)"
 definition H\<^sub>N :: "nat \<Rightarrow> nat pmf" where "H\<^sub>N n = H {..<n}"
 
 context includes monad_normalisation
 begin
 
 text \<open>
   The height of a skip list is independent of the values in a set A. For simplicity we can
   therefore work on the skip list over the set @{term "{..< card A}"}
 \<close>
 
 lemma
   assumes "finite A"
   shows "H A = H\<^sub>N (card A)"
 proof -
   define f' where "f' = (\<lambda>x. if x \<in> A
                              then the_inv_into {..<card A} ((!) (sorted_list_of_set A)) x
                              else card A)"
   have bij_f': "bij_betw f' A {..<card A}"
   proof -
     (* I know the proof looks weird, but for some reason all tools have problems with this proof *)
     have "bij_betw (the_inv_into {..<card A} ((!) (sorted_list_of_set A))) A {..<card A}"
       unfolding f'_def using sorted_list_of_set_bij_betw assms bij_betw_the_inv_into by blast
     moreover have "bij_betw (the_inv_into {..<card A} ((!) (sorted_list_of_set A))) A {..<card A}
                      = bij_betw f' A {..<card A}"
       unfolding f'_def by (rule bij_betw_cong) simp
     ultimately show ?thesis
       by blast
   qed
   have *: "Max\<^sub>0 ((f \<circ> f') ` A) = Max\<^sub>0 (f ` {..<card A})" for f :: "nat \<Rightarrow> nat"
     using  bij_betw_imp_surj_on bij_f' image_comp by metis
   have "H A = map_pmf (\<lambda>f. Max\<^sub>0 (f ` A)) (map_pmf (\<lambda>g. g \<circ> f') (SL\<^sub>N (card A)))"
     using assms bij_f' unfolding H_def SL_def SL\<^sub>N_def
     by (subst Pi_pmf_bij_betw[of _ f' "{..<card A}"]) (auto simp add: f'_def)
   also have "\<dots> =  H\<^sub>N (card A)"
     unfolding H\<^sub>N_def H_def SL\<^sub>N_def using * by (auto intro!: bind_pmf_cong simp add: map_pmf_def)
   finally show ?thesis
     by simp
 qed
 
 text \<open>
   The cumulative distribution function (CDF) of the height is the CDF of the geometric PMF to the
   power of n
 \<close>
 
 lemma prob_Max_IID_geometric_atMost:
   assumes "p \<in> {0..1}"
   shows "measure_pmf.prob (H\<^sub>N n) {..i}
        = (measure_pmf.prob (geometric_pmf p) {..i}) ^ n" (is "?lhs = ?rhs")
 proof -
   note SL_def[simp] SL\<^sub>N_def[simp] H_def[simp] H\<^sub>N_def[simp]
   have "{f. Max\<^sub>0 (f ` {..<n}) \<le> i}  = {..<n} \<rightarrow> {..i}"
     by auto
   then have "?lhs = measure_pmf.prob (SL\<^sub>N n) ({..<n} \<rightarrow> {..i})"
     by (simp add: vimage_def)
   also have "\<dots> = measure_pmf.prob (SL\<^sub>N n) (PiE_dflt {..<n} 0 (\<lambda>_. {..i}))"
     by (intro measure_prob_cong_0) (auto simp add: PiE_dflt_def pmf_Pi split: if_splits)
   also have "\<dots> = measure_pmf.prob (geometric_pmf p) {..i} ^ n"
     using assms by (auto simp add: measure_Pi_pmf_PiE_dflt)
   finally show ?thesis
     by simp
 qed
 
 lemma prob_Max_IID_geometric_greaterThan:
   assumes "p \<in> {0<..1}"
   shows "measure_pmf.prob (H\<^sub>N n) {i<..} =
          1 - (1 - q ^ (i + 1)) ^ n"
 proof -
   have "UNIV - {..i} = {i<..}"
     by auto
   then have "measure_pmf.prob (H\<^sub>N n) {i<..} = measure_pmf.prob (H\<^sub>N n) (space (measure_pmf (H\<^sub>N n)) - {..i})"
     by (auto)
   also have "\<dots> = 1 - (measure_pmf.prob (geometric_pmf p) {..i}) ^ n"
     using assms by (subst measure_pmf.prob_compl) (auto simp add: prob_Max_IID_geometric_atMost)
   also have "\<dots> =   1 - (1 - q ^ (i + 1)) ^ n"
     using assms unfolding q_def by (subst geometric_pmf_prob_atMost) auto
   finally show ?thesis
     by simp
 qed
 
 end (* context includes monad_normalisation *)
 end (* locale skip_list *)
 
 text \<open>
   An alternative definition of the expected value of a non-negative random variable
   \footnote{\url{https://en.wikipedia.org/w/index.php?title=Expected\_value&oldid=881384346\#Formula\_for\_non-negative\_random\_variables}}
 \<close>
 
 lemma expectation_prob_atLeast:
   assumes "(\<lambda>i. measure_pmf.prob N {i..}) abs_summable_on {1..}"
   shows "measure_pmf.expectation N real = infsetsum (\<lambda>i. measure_pmf.prob N {i..}) {1..}"
     "integrable N real"
 proof -
   have "(\<lambda>(x, y). pmf N y) abs_summable_on Sigma {Suc 0..} atLeast"
     using assms by (auto simp add: measure_pmf_conv_infsetsum abs_summable_on_Sigma_iff)
   then have summable: "(\<lambda>(x, y). pmf N x) abs_summable_on Sigma {Suc 0..} (atLeastAtMost (Suc 0))"
     by (subst abs_summable_on_reindex_bij_betw[of "\<lambda>(x,y). (y,x)", symmetric])
       (auto intro!: bij_betw_imageI simp add: inj_on_def case_prod_beta)
   have "measure_pmf.expectation N real = (\<Sum>\<^sub>ax. pmf N x *\<^sub>R real x)"
     by (auto simp add: infsetsum_def integral_density measure_pmf_eq_density)
   also have "\<dots> = (\<Sum>\<^sub>ax \<in> ({0} \<union> {Suc 0..}). pmf N x *\<^sub>R real x)"
     by (auto intro!: infsetsum_cong)
   also have "\<dots> = (\<Sum>\<^sub>ax\<in>{Suc 0..}. pmf N x * real x)"
   proof -
     have "(\<lambda>x. pmf N x *\<^sub>R real x) abs_summable_on {0} \<union> {Suc 0..}"
       using summable by (subst (asm) abs_summable_on_Sigma_iff) (auto simp add: mult.commute)
     then show ?thesis
       by (subst infsetsum_Un_Int) auto
   qed
   also have "\<dots> = (\<Sum>\<^sub>a(x, y)\<in>Sigma {Suc 0..} (atLeastAtMost (Suc 0)). pmf N x)"
     using summable by (subst infsetsum_Sigma) (auto simp add: mult.commute)
   also have "\<dots> = (\<Sum>\<^sub>ax\<in>Sigma {Suc 0..} atLeast. pmf N (snd x))"
     by (subst infsetsum_reindex_bij_betw[of "\<lambda>(x,y). (y,x)", symmetric])
       (auto intro!: bij_betw_imageI simp add: inj_on_def case_prod_beta)
   also have "\<dots> = infsetsum (\<lambda>i. measure_pmf.prob N {i..}) {1..}"
     using assms
     by (subst infsetsum_Sigma)
       (auto simp add: measure_pmf_conv_infsetsum abs_summable_on_Sigma_iff infsetsum_Sigma')
   finally show "measure_pmf.expectation N real = infsetsum (\<lambda>i. measure_pmf.prob N {i..}) {1..}"
     by simp
   have "(\<lambda>x. pmf N x *\<^sub>R real x) abs_summable_on {0} \<union> {Suc 0..}"
     using summable by (subst (asm) abs_summable_on_Sigma_iff) (auto simp add: mult.commute)
   then have "(\<lambda>x. pmf N x *\<^sub>R real x) abs_summable_on UNIV"
     by (simp add: atLeast_Suc)
   then have "integrable (count_space UNIV) (\<lambda>x. pmf N x *\<^sub>R real x)"
     by (subst abs_summable_on_def[symmetric]) blast
   then show "integrable N real"
     by (subst measure_pmf_eq_density, subst integrable_density) auto
 qed
 
 text \<open>
   The expected height of a skip list has no closed-form expression but we can approximate it. We
   start by showing how we can calculate an infinite sum over the natural numbers with an integral
   over the positive reals and the floor function.
 \<close>
 
 lemma infsetsum_set_nn_integral_reals:
   assumes "f abs_summable_on UNIV" "\<And>n. f n \<ge> 0"
   shows "infsetsum f UNIV = set_nn_integral lborel {0::real..} (\<lambda>x. f (nat (floor x)))"
 proof -
   have "x < 1 + (floor x)"for x::real
     by linarith
   then have "\<exists>n. real n \<le> x \<and> x < 1 + real n" if "x \<ge> 0" for x
     using that of_nat_floor by (intro exI[of _ "nat (floor x)"]) auto
   then have "{0..} = (\<Union>n. {real n..<real (Suc n)})"
     by auto
   then have "\<integral>\<^sup>+x\<in>{0::real..}. ennreal (f (nat \<lfloor>x\<rfloor>))\<partial>lborel =
              (\<Sum>n. \<integral>\<^sup>+x\<in>{real n..<1 + real n}. ennreal (f (nat \<lfloor>x\<rfloor>))\<partial>lborel)"
     by (auto simp add: disjoint_family_on_def nn_integral_disjoint_family)
   also have "\<dots> = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n..<1 + real n}. ennreal (f n)\<partial>lborel)"
     by(subst suminf_cong, rule nn_integral_cong_AE)
       (auto intro!: eventuallyI  simp add: indicator_def floor_eq4)
   also have "\<dots> = (\<Sum>n. ennreal (f n))"
     by (auto intro!: suminf_cong simp add: nn_integral_cmult)
   also have "\<dots> = infsetsum f {0..}"
     using assms suminf_ennreal2 abs_summable_on_nat_iff' summable_norm_cancel
     by (auto simp add: infsetsum_nat)
   finally show ?thesis
     by simp
 qed
 
 lemma nn_integral_nats_reals:
   shows "(\<integral>\<^sup>+ i. ennreal (f i) \<partial>count_space UNIV) = \<integral>\<^sup>+x\<in>{0::real..}. ennreal (f (nat \<lfloor>x\<rfloor>))\<partial>lborel"
 proof -
   have "x < 1 + (floor x)"for x::real
     by linarith
   then have "\<exists>n. real n \<le> x \<and> x < 1 + real n" if "x \<ge> 0" for x
     using that of_nat_floor by (intro exI[of _ "nat (floor x)"]) auto
   then have "{0..} = (\<Union>n. {real n..<real (Suc n)})"
     by auto
   then have "\<integral>\<^sup>+x\<in>{0::real..}. f (nat \<lfloor>x\<rfloor>)\<partial>lborel =
              (\<Sum>n. \<integral>\<^sup>+x\<in>{real n..<1 + real n}. ennreal (f (nat \<lfloor>x\<rfloor>))\<partial>lborel)"
     by (auto simp add: disjoint_family_on_def nn_integral_disjoint_family)
   also have "\<dots> = (\<Sum>n. \<integral>\<^sup>+x\<in>{real n..<1 + real n}. ennreal (f n)\<partial>lborel)"
     by(subst suminf_cong,rule nn_integral_cong_AE)
       (auto intro!: eventuallyI  simp add: indicator_def floor_eq4)
   also have "\<dots> = (\<Sum>n. ennreal (f n))"
     by (auto intro!: suminf_cong simp add: nn_integral_cmult)
   also have "\<dots> = (\<integral>\<^sup>+ i. ennreal (f i) \<partial>count_space UNIV)"
     by (simp add: nn_integral_count_space_nat)
   finally show ?thesis
     by simp
 qed
 
 lemma nn_integral_floor_less_eq:
   assumes "\<And>x y. x \<le> y \<Longrightarrow> f y \<le> f x"
   shows "\<integral>\<^sup>+x\<in>{0::real..}. ennreal (f x)\<partial>lborel \<le> \<integral>\<^sup>+x\<in>{0::real..}. ennreal (f (nat \<lfloor>x\<rfloor>))\<partial>lborel"
   using assms by (auto simp add: indicator_def intro!: nn_integral_mono ennreal_leI)
 
 lemma nn_integral_finite_imp_abs_sumable_on:
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes "nn_integral (count_space A) (\<lambda>x. norm (f x)) < \<infinity>"
   shows   "f abs_summable_on A"
   using assms unfolding abs_summable_on_def integrable_iff_bounded by auto
 
 lemma nn_integral_finite_imp_abs_sumable_on':
   assumes "nn_integral (count_space A) (\<lambda>x. ennreal (f x)) < \<infinity>" "\<And>x. f x \<ge> 0"
   shows   "f abs_summable_on A"
   using assms unfolding abs_summable_on_def integrable_iff_bounded by auto
 
 text \<open>
   We now show that $\int_0^\infty 1 - (1 - q^x) ^ n\;dx = \frac{- H_n}{\ln q}$ if $0 < q < 1$.
 \<close>
 
 lemma harm_integral_x_raised_n:
   "set_integrable lborel {0::real..1} (\<lambda>x. (\<Sum>i\<in>{..<n}. x ^ i))" (is ?thesis1)
   "LBINT x = 0..1. (\<Sum>i\<in>{..<n}. x ^ i) = harm n" (is ?thesis2)
 proof -
   have h: "set_integrable lborel {0::real..1} (\<lambda>x. (\<Sum>i\<in>{..<n}. x ^ i))" for n
     by (intro borel_integrable_atLeastAtMost') (auto intro!: continuous_intros)
   then show ?thesis1
     by (intro borel_integrable_atLeastAtMost') (auto intro!: continuous_intros)
   show ?thesis2
   proof (induction n)
     case (Suc n)
     have "(LBINT x=0..1.(\<Sum>i\<in>{..<n}. x ^ i) + x ^ n) =
           (LBINT x=0..1. (\<Sum>i\<in>{..<n}. x ^ i)) + (LBINT x=0..1. x ^ n)"
     proof -
       have "set_integrable lborel (einterval 0 1) (\<lambda>x. (\<Sum>i\<in>{..<n}. x ^ i))"
         by (rule set_integrable_subset) (use h in \<open>auto simp add: einterval_def\<close>)
       moreover have "set_integrable lborel (einterval 0 1) (\<lambda>x. (x ^ n))"
       proof -
         have "set_integrable lborel {0::real..1} (\<lambda>x. (x ^ n))"
           by (rule borel_integrable_atLeastAtMost')
             (auto intro!: borel_integrable_atLeastAtMost' continuous_intros)
         then show ?thesis
           by (rule set_integrable_subset) (auto simp add: einterval_def)
       qed
       ultimately show ?thesis
         by (auto intro!: borel_integrable_atLeastAtMost' simp add:  interval_lebesgue_integrable_def)
     qed
     also have "(LBINT x=0..1. x ^ n) = 1 / (1 + real n)"
     proof -
       have "(LBINT x=0..1. x ^ n) = LBINT x. x ^ n * indicator {0..1} x "
       proof -
         have "AE x in lborel. x ^ n * indicator {0..1} x = indicator (einterval 0 1) x * x ^ n"
           by(rule eventually_mono[OF eventually_conj[OF  AE_lborel_singleton[of 1]
                   AE_lborel_singleton[of 0]]])
             (auto simp add: indicator_def einterval_def)
         then show ?thesis
           using integral_cong_AE unfolding interval_lebesgue_integral_def set_lebesgue_integral_def
           by (auto intro!: integral_cong_AE)
       qed
       then show ?thesis
         by (auto simp add: integral_power)
     qed
     finally show ?case
       using Suc by (auto simp add: harm_def inverse_eq_divide)
   qed (auto simp add: harm_def)
 qed
 
 lemma harm_integral_0_1_fraction:
   "set_integrable lborel {0::real..1} (\<lambda>x. (1 - x ^ n) / (1 - x))"
   "(LBINT x = 0..1. ((1 - x ^ n) / (1 - x))) = harm n"
 proof -
   show "set_integrable lborel {0::real..1} (\<lambda>x. (1 - x ^ n) / (1 - x))"
   proof -
     have "AE x\<in>{0::real..1} in lborel. (1 - x ^ n) / (1 - x) = sum ((^) x) {..<n}"
       by (auto intro!: eventually_mono[OF AE_lborel_singleton[of 1]] simp add: sum_gp_strict)
     with harm_integral_x_raised_n show ?thesis
       by (subst set_integrable_cong_AE) auto
   qed
   moreover have "AE x\<in>{0::real<..<1} in lborel. (1 - x ^ n) / (1 - x) = sum ((^) x) {..<n}"
     by (auto simp add: sum_gp_strict)
   moreover have "einterval (min 0 1) (max 0 1) = {0::real<..<1}"
     by (auto simp add: min_def max_def einterval_iff)
   ultimately show "(LBINT x = 0..1. ((1 - x ^ n) / (1 - x))) = harm n"
     using harm_integral_x_raised_n by (subst interval_integral_cong_AE) auto
 qed
 
 lemma one_minus_one_minus_q_x_n_integral:
   assumes "q \<in> {0<..<1}"
   shows "set_integrable lborel (einterval 0 \<infinity>) (\<lambda>x. (1 - (1 - q powr x) ^ n))"
         "(LBINT x=0..\<infinity>. 1 - (1 - q powr x) ^ n) = - harm n / ln q"
 proof -
   have [simp]: "q powr (log q (1-x)) = 1 - x" if "x \<in> {0<..<1}" for x
     using that assms by (subst powr_log_cancel) auto
   have 1: "((ereal \<circ> (\<lambda>x. log q (1 - x)) \<circ> real_of_ereal) \<longlongrightarrow> 0) (at_right 0)"
     using assms unfolding zero_ereal_def ereal_tendsto_simps by (auto intro!: tendsto_eq_intros)
   have 2: "((ereal \<circ> (\<lambda>x. log q (1-x)) \<circ> real_of_ereal) \<longlongrightarrow> \<infinity>) (at_left 1)"
   proof -
     have "filterlim ((-) 1) (at_right 0) (at_left (1::real))"
       by (intro filterlim_at_withinI eventually_at_leftI[of 0]) (auto intro!: tendsto_eq_intros)
     then have "LIM x at_left 1. - inverse (ln q) * - ln (1 - x) :> at_top"
       using assms
       by (intro filterlim_tendsto_pos_mult_at_top [OF tendsto_const])
         (auto simp: filterlim_uminus_at_top intro!: filterlim_compose[OF ln_at_0])
     then show ?thesis
       unfolding one_ereal_def ereal_tendsto_simps log_def by (simp add: field_simps)
   qed
   have 3: "set_integrable lborel (einterval 0 1)
      (\<lambda>x. (1 - (1 - q powr (log q (1 - x))) ^ n) * (- 1 / (ln q * (1 - x))))"
   proof -
     have "set_integrable lborel (einterval 0 1) (\<lambda>x. - (1 / ln q) * ((1 - x ^ n) / (1 - x)))"
       by(intro set_integrable_mult_right)
         (auto intro!: harm_integral_0_1_fraction intro: set_integrable_subset simp add: einterval_def)
     then show ?thesis
       by(subst set_integrable_cong_AE[where g="\<lambda>x. - (1 / ln q) * ((1 - x ^ n) / (1 - x))"])
         (auto intro!: eventuallyI simp add: einterval_def)
   qed
   have 4: "LBINT x=0..1. - ((1 - (1 - q powr log q (1 - x)) ^ n) / (ln q * (1 - x))) = - (harm n / ln q)"
     (is "?lhs = ?rhs")
   proof -
     have "?lhs = LBINT x=0..1. ((1 - x ^ n) / (1 - x)) * (- 1 / ln q)"
       using assms
       by (intro interval_integral_cong_AE)
       (auto intro!: eventuallyI simp add: max_def einterval_def field_simps)
     also have "\<dots> = harm n * (-1 / ln q)"
       using harm_integral_0_1_fraction by (subst interval_lebesgue_integral_mult_left) auto
     finally show ?thesis
       by auto
   qed
   note sub = interval_integral_substitution_nonneg
              [where f = "(\<lambda>x. (1 - (1 - q powr x) ^ n))" and g="(\<lambda>x. log q (1-x))"
                     and g'="(\<lambda>x. - 1 / (ln q * (1 - x)))" and a = 0 and b = 1]
   show "set_integrable lborel (einterval 0 \<infinity>) (\<lambda>x. (1 - (1 - q powr x) ^ n))"
     using assms 1 2 3 4
     by (intro sub) (auto intro!: derivative_eq_intros mult_nonneg_nonpos2 tendsto_intros power_le_one)
   show "(LBINT x=0..\<infinity>. 1 - (1 - q powr x) ^ n) = - harm n / ln q"
     using assms 1 2 3 4
     by (subst sub) (auto intro!: derivative_eq_intros mult_nonneg_nonpos2 tendsto_intros power_le_one)
 qed
 
 lemma one_minus_one_minus_q_x_n_nn_integral:
   fixes q::real
   assumes "q \<in> {0<..<1}"
   shows "set_nn_integral lborel {0..} (\<lambda>x. (1 - (1 - q powr x) ^ n)) =
         LBINT x=0..\<infinity>. 1 - (1 - q powr x) ^ n"
 proof -
   have "set_nn_integral  lborel {0..} (\<lambda>x. (1 - (1 - q powr x) ^ n)) =
         nn_integral lborel (\<lambda>x. indicator (einterval 0 \<infinity>) x *  (1 - (1 - q powr x) ^ n))"
     using assms by (intro nn_integral_cong_AE eventually_mono[OF AE_lborel_singleton[of 0]])
       (auto simp add: indicator_def einterval_def)
   also have "\<dots> = ennreal (LBINT x. indicator (einterval 0 \<infinity>) x * (1 - (1 - q powr x) ^ n))"
   using one_minus_one_minus_q_x_n_integral assms
   by(intro nn_integral_eq_integral)
     (auto simp add: indicator_def einterval_def set_integrable_def
       intro!: eventuallyI power_le_one powr_le1)
   finally show ?thesis
     by (simp add: interval_lebesgue_integral_def set_lebesgue_integral_def)
 qed
 
 text \<open>
   We can now derive bounds for the expected height.
 \<close>
 
 context random_skip_list
 begin
 
 definition EH\<^sub>N where "EH\<^sub>N n = measure_pmf.expectation (H\<^sub>N n) real"
 
 lemma EH\<^sub>N_bounds':
   fixes n::nat
   assumes "p \<in> {0<..<1}" "0 < n"
   shows "- harm n / ln q - 1 \<le> EH\<^sub>N n"
      "EH\<^sub>N n \<le> - harm n / ln q"
      "integrable (H\<^sub>N n) real"
 proof -
   define f where "f = (\<lambda>x. 1 - (1 - q ^ x) ^ n)"
   define f' where "f' = (\<lambda>x. 1 - (1 - q powr x) ^ n)"
   have q: "q \<in> {0<..<1}"
     unfolding q_def using assms by auto
   have f_descending: "f y \<le> f x" if "x \<le> y" for x y
     unfolding f_def using that q
     by (auto intro!: power_mono simp add: power_decreasing power_le_one_iff)
   have f'_descending: "f' y \<le> f' x" if "x \<le> y" "0 \<le> x" for x y
     unfolding f'_def using that q
     by (auto intro!: power_mono simp add: ln_powr powr_def mult_nonneg_nonpos)
   have [simp]: "harm n / ln q <= 0"
     using harm_nonneg ln_ge_zero_imp_ge_one q by (intro divide_nonneg_neg) auto
   have f_nn_integral_harm:
     "- harm n / ln q \<le> \<integral>\<^sup>+ x. (f x) \<partial>count_space UNIV"
     "(\<integral>\<^sup>+ i. f (i + 1) \<partial>count_space UNIV) \<le> - harm n / ln q"
   proof -
     have "(\<integral>\<^sup>+ i. f (i + 1) \<partial>count_space UNIV) = (\<integral>\<^sup>+x\<in>{0::real..}. (f (nat \<lfloor>x\<rfloor> + 1))\<partial>lborel)"
       using nn_integral_nats_reals by auto
     also have "\<dots> = \<integral>\<^sup>+x\<in>{0::real..}. ennreal (f' (nat \<lfloor>x\<rfloor> + 1))\<partial>lborel"
     proof -
       have "0 \<le> x \<Longrightarrow> (1 - q * q ^ nat \<lfloor>x\<rfloor>) ^ n = (1 - q powr (1 + real_of_int \<lfloor>x\<rfloor>)) ^ n" for x::real
         using q by (subst powr_realpow [symmetric]) (auto simp: powr_add)
       then show ?thesis
         unfolding f_def f'_def using q
         by (auto intro!: nn_integral_cong ennreal_cong  simp add: powr_real_of_int indicator_def)
     qed
     also have "\<dots> \<le> set_nn_integral lborel {0..} f'"
     proof -
       have "x \<le> 1 + real_of_int \<lfloor>x\<rfloor>" for x
         by linarith
       then show ?thesis
         by (auto simp add: indicator_def intro!: f'_descending nn_integral_mono ennreal_leI)
     qed
     also have harm_integral_f': "\<dots> = - harm n / ln q"
       unfolding f'_def using q
       by (auto intro!: ennreal_cong
           simp add: one_minus_one_minus_q_x_n_nn_integral one_minus_one_minus_q_x_n_integral)
     finally show "(\<integral>\<^sup>+ i. f (i + 1) \<partial>count_space UNIV) \<le> - harm n / ln q"
       by simp
     note harm_integral_f'[symmetric]
     also have "set_nn_integral lborel {0..} f' \<le> \<integral>\<^sup>+x\<in>{0::real..}. f' (nat \<lfloor>x\<rfloor>)\<partial>lborel"
       using assms f'_descending
       by (auto simp add: indicator_def intro!: nn_integral_mono ennreal_leI)
     also have "\<dots> = \<integral>\<^sup>+x\<in>{0::real..}. f (nat \<lfloor>x\<rfloor>)\<partial>lborel"
       unfolding f_def f'_def
       using q by (auto intro!: nn_integral_cong ennreal_cong simp add: powr_real_of_int indicator_def)
     also have "\<dots> = (\<integral>\<^sup>+ x. f x \<partial>count_space UNIV)"
       using nn_integral_nats_reals by auto
     finally show "- harm n / ln q \<le> \<integral>\<^sup>+ x. f x \<partial>count_space UNIV"
       by simp
   qed
   then have f1_abs_summable_on: "(\<lambda>i. f (i + 1)) abs_summable_on UNIV"
     unfolding f_def using q
     by (intro nn_integral_finite_imp_abs_sumable_on')
       (auto simp add: f_def le_less_trans intro!: power_le_one mult_le_one)
   then have f_abs_summable_on: "f abs_summable_on {1..}"
     using Suc_le_lessD greaterThan_0
     by (subst abs_summable_on_reindex_bij_betw[symmetric, where g="\<lambda>x. x + 1" and A="UNIV"]) auto
   also have "(f abs_summable_on {1..}) = ((\<lambda>x. measure_pmf.prob (H\<^sub>N n) {x..}) abs_summable_on {1..})"
   proof -
     have "((\<lambda>x. measure_pmf.prob (H\<^sub>N n) {x..}) abs_summable_on {1..}) =
           ((\<lambda>x. measure_pmf.prob (H\<^sub>N n) {x - 1<..}) abs_summable_on {1..})"
       by (auto intro!: measure_prob_cong_0 abs_summable_on_cong)
     also have "\<dots> = (f abs_summable_on {1..})"
       using assms
       by (intro abs_summable_on_cong) (auto simp add: f_def prob_Max_IID_geometric_greaterThan)
     finally show ?thesis
       by simp
   qed
   finally have EH\<^sub>N_sum:
     "EH\<^sub>N n = (\<Sum>\<^sub>ai\<in>{1..}. measure_pmf.prob (H\<^sub>N n) {i..})"
     "integrable (measure_pmf (H\<^sub>N n)) real"
     unfolding EH\<^sub>N_def using expectation_prob_atLeast by auto
   then show "integrable (measure_pmf (H\<^sub>N n)) real"
     by simp
   have EH\<^sub>N_sum': "EH\<^sub>N n = infsetsum f {1..}"
   proof -
     have "EH\<^sub>N n = (\<Sum>\<^sub>ak\<in>{1..}. measure_pmf.prob (H\<^sub>N n) {k - 1<..})"
       unfolding EH\<^sub>N_sum by (auto intro!: measure_prob_cong_0 infsetsum_cong)
     also have "\<dots> = infsetsum f {1..}"
       using assms
       by (intro infsetsum_cong) (auto simp add: f_def prob_Max_IID_geometric_greaterThan)
     finally show ?thesis
       by simp
   qed
   also have "\<dots> = (\<Sum>\<^sub>ak. f (k + 1))"
     using Suc_le_lessD greaterThan_0
     by (subst infsetsum_reindex_bij_betw[symmetric, where g="\<lambda>x. x + 1" and A="UNIV"]) auto
   also have "ennreal \<dots> = (\<integral>\<^sup>+x\<in>{0::real..}. f (nat \<lfloor>x\<rfloor> + 1)\<partial>lborel)"
     using f1_abs_summable_on q
     by (intro infsetsum_set_nn_integral_reals) (auto simp add: f_def mult_le_one power_le_one)
   also have "\<dots> = (\<integral>\<^sup>+ i. f (i + 1) \<partial>count_space UNIV)"
     using nn_integral_nats_reals by auto
   also have "\<dots> \<le> - harm n / ln q"
     using f_nn_integral_harm by auto
   finally show "EH\<^sub>N n \<le> - harm n / ln q"
     by (subst (asm) ennreal_le_iff) (auto)
   have "EH\<^sub>N n + 1 = (\<Sum>\<^sub>ax\<in>{Suc 0..}. f x) + (\<Sum>\<^sub>ax\<in>{0}. f x)"
     using assms by (subst EH\<^sub>N_sum') (auto simp add: f_def)
   also have "\<dots> = infsetsum f UNIV"
     using f_abs_summable_on by (subst infsetsum_Un_disjoint[symmetric]) (auto intro!: infsetsum_cong)
   also have "\<dots> = (\<integral>\<^sup>+x\<in>{0::real..}. f (nat \<lfloor>x\<rfloor>)\<partial>lborel)"
   proof -
     have "f abs_summable_on ({0} \<union> {1..})"
       using f_abs_summable_on by (intro abs_summable_on_union) (auto)
     also have "{0::nat} \<union> {1..} = UNIV"
       by auto
     finally show ?thesis
       using q
       by (intro infsetsum_set_nn_integral_reals) (auto simp add: f_def mult_le_one power_le_one)
   qed
   also have "\<dots> = (\<integral>\<^sup>+ x. f x \<partial>count_space UNIV)"
     using nn_integral_nats_reals by auto
   also have "... \<ge> - harm n / ln q"
     using f_nn_integral_harm by auto
   finally have "- harm n / ln q \<le> EH\<^sub>N n + 1"
     by (subst (asm) ennreal_le_iff) (auto simp add: EH\<^sub>N_def)
   then show "- harm n / ln q - 1 \<le> EH\<^sub>N n"
     by simp
 qed
 
 theorem EH\<^sub>N_bounds:
   fixes n::nat
   assumes "p \<in> {0<..<1}"
   shows
     "- harm n / ln q - 1 \<le> EH\<^sub>N n"
     "EH\<^sub>N n \<le> - harm n / ln q"
     "integrable (H\<^sub>N n) real"
 proof -
   show "- harm n / ln q - 1 \<le> EH\<^sub>N n"
     using assms EH\<^sub>N_bounds'
     by (cases "n = 0") (auto simp add: EH\<^sub>N_def H\<^sub>N_def H_def SL_def harm_expand)
   show "EH\<^sub>N n \<le> - harm n / ln q"
     using assms EH\<^sub>N_bounds'
     by (cases "n = 0") (auto simp add: EH\<^sub>N_def H\<^sub>N_def H_def SL_def harm_expand)
   show "integrable (H\<^sub>N n) real"
     using assms EH\<^sub>N_bounds'
     by (cases "n = 0") (auto simp add: H\<^sub>N_def H_def SL_def intro!: integrable_measure_pmf_finite)
 qed
 
 end (* context random_skip_list *)
 
 subsection \<open>Expected Length of Search Path\<close>
 
 text \<open>
   Let @{term "A::'a::linorder set"} and @{term "f::'a \<Rightarrow> nat"} where f is an abstract description
   of a skip list (assign each value its maximum level). steps A f s u l starts on the rightmost element
   on level s in the skip lists. If possible it moves up, if not it moves to the left. For every step
   up it adds cost u and for every step to the left it adds cost l. steps A f 0 1 1 therefore walks
   from the bottom right corner of a skip list to the top left corner of a skip list and counts
   all steps.
 \<close>
 
 \<comment> \<open>NOTE: You could also define steps with lsteps and then prove that the following recursive
     definition holds\<close>
 
 function steps :: "'a :: linorder set \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   "steps A f l up left = (if A = {} \<or> infinite A
               then 0
               else (let m = Max A in (if f m < l then       steps (A - {m}) f l up left
                                       else (if f m > l then up + steps A f (l + 1) up left
                                       else                  left + steps (A - {m}) f l up left))))"
   by pat_completeness auto
 termination
 proof (relation "(\<lambda>(A,f,l,a,b). card A) <*mlex*> (\<lambda>(A,f,l,a,b). Max (f ` A) - l) <*mlex*> {}", goal_cases)
   case 1
   then show ?case
     by(intro wf_mlex wf_empty)
 next
   case 2
   then show ?case
     by (intro mlex_less) (auto simp: card_gt_0_iff)
 next
   case (3 A f l a b x)
   then have "Max (f ` A) - Suc l < Max (f ` A) - l"
     by (meson Max_gr_iff Max_in diff_less_mono2 finite_imageI imageI image_is_empty lessI)
    with 3 have "((A, f, l + 1, a, b), A, f, l, a, b) \<in> (\<lambda>(A, f, l, a, b). Max (f ` A) - l) <*mlex*> {}"
      by (intro mlex_less) (auto)
    with 3 show ?case apply - apply(rule mlex_leq) by auto
 next
   case 4
   then show ?case by (intro mlex_less) (auto simp: card_gt_0_iff)
 qed
 
 declare steps.simps[simp del]
 
 text \<open>
   lsteps is similar to steps but is using lists instead of sets. This makes the proofs where we use
   induction easier.
 \<close>
 
 function lsteps :: "'a list \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   "lsteps [] f l up left = 0" |
   "lsteps (x#xs) f l up left = (if       f x < l then lsteps xs f l up left
                                  else (if f x > l then up + lsteps (x#xs) f (l + 1) up left
                                  else                        left + lsteps xs f l up left))"
   by pat_completeness auto
 termination
 proof (relation "(\<lambda>(xs,f,l,a,b). length xs) <*mlex*> (\<lambda>(xs,f,l,a,b).
                  Max (f ` set xs) - l) <*mlex*> {}",
        goal_cases)
   case 1
   then show ?case
     by(intro wf_mlex wf_empty)
 next
   case 2
   then show ?case
     by (auto intro: mlex_less simp: card_gt_0_iff)
 next
   case (3 n f l a b)
   show ?case
     by (rule mlex_leq) (use 3 in \<open>auto intro: mlex_less mlex_leq intro!:  diff_less_mono2 simp add: Max_gr_iff\<close>)
 next
   case 4
   then show ?case by (intro mlex_less) (auto simp: card_gt_0_iff)
 qed
 
 declare lsteps.simps(2)[simp del]
 
 lemma steps_empty [simp]: "steps {} f l up left = 0"
   by (simp add: steps.simps)
 
 lemma steps_lsteps: "steps A f l u v = lsteps (rev (sorted_list_of_set A)) f l u v"
 proof (cases "finite A \<and> A \<noteq> {}")
   case True
   then show ?thesis
   proof(induction "(rev (sorted_list_of_set A))" f l u v arbitrary: A rule: lsteps.induct)
     case (2 y ys f l u v A)
     then have y_ys: "y = Max A" "ys  = rev (sorted_list_of_set (A - {y}))"
       by (auto simp add: sorted_list_of_set_Max_snoc)
     consider (a) "l < f y" | (b) "f y < l" | (c) "f y = l"
       by fastforce
     then have "steps A f l u v = lsteps (y#ys) f l u v"
     proof cases
       case a
       then show ?thesis
         by (subst steps.simps, subst lsteps.simps) (use y_ys 2 in auto)
     next
       case b
       then show ?thesis
         using y_ys 2(1) by (cases "ys = []") (auto simp add: steps.simps lsteps.simps)
     next
       case c
       then have "steps (A - {Max A}) f l u v =
                  lsteps (rev (sorted_list_of_set (A - {Max A}))) f l u v"
         by (cases "A = {Max A}") (use y_ys 2 in \<open>auto intro!: 2(3) simp add: steps.simps\<close>)
       then show ?thesis
         by (subst steps.simps, subst lsteps.simps) (use y_ys 2 in auto)
     qed
     then show ?case
       using 2 by simp
   qed (auto simp add: steps.simps)
 qed (auto simp add: steps.simps)
 
 lemma lsteps_comp_map: "lsteps zs (f \<circ> g) l u v = lsteps (map g zs) f l u v"
   by (induction zs "f \<circ> g" l u v rule: lsteps.induct) (auto simp add: lsteps.simps)
 
 lemma steps_image:
   assumes "finite A" "mono_on g A" "inj_on g A"
   shows "steps A (f \<circ> g) l u v = steps (g ` A) f l u v"
 proof -
   have "(sorted_list_of_set (g ` A)) = map g (sorted_list_of_set A)"
     using sorted_list_of_set_image assms by auto
   also have "rev \<dots> = map g (rev (sorted_list_of_set A))"
     using rev_map by auto
   finally show ?thesis
     by (simp add: steps_lsteps lsteps_comp_map)
 qed
 
 lemma lsteps_cong:
   assumes "ys = xs" "\<And>x. x \<in> set xs \<Longrightarrow> f x = g x" "l = l'"
   shows "lsteps xs f l u v = lsteps ys g l' u v"
   using assms proof (induction xs f l u v arbitrary: ys l' rule: lsteps.induct)
   case (2 x xs f l up left)
   then show ?case
     by (subst \<open>ys = x # xs\<close>, subst lsteps.simps, subst (2) lsteps.simps) auto
 qed (auto)
 
 lemma steps_cong:
   assumes "A = B" "\<And>x. x \<in> A \<Longrightarrow> f x = g x" "l = l'"
   shows   "steps A f l u v = steps B g l' u v"
   using assms
   by (cases "A = {} \<or> infinite A") (auto simp add: steps_lsteps steps.simps intro!: lsteps_cong)
 
 lemma lsteps_f_add':
   shows "lsteps xs f l u v = lsteps xs (\<lambda>x. f x + m) (l + m) u v"
   by  (induction xs f l u v rule: lsteps.induct) (auto simp add: lsteps.simps)
 
 lemma steps_f_add':
   shows "steps A f l u v = steps A (\<lambda>x. f x + m) (l + m) u v"
   by (cases "A = {} \<or> infinite A") (auto simp add: steps_lsteps steps.simps intro!: lsteps_f_add')
 
 lemma lsteps_smaller_set:
   assumes "m \<le> l"
   shows "lsteps xs f l u v = lsteps [x \<leftarrow> xs. m \<le> f x] f l u v"
   using assms by (induction xs f l u v rule: lsteps.induct) (auto simp add: lsteps.simps)
 
 lemma steps_smaller_set:
   assumes "finite A" "m \<le> l"
   shows "steps A f l u v = steps {x\<in>A. f x \<ge> m} f l u v"
   using assms
   by(cases "A = {} \<or> infinite A")
     (auto simp add: steps_lsteps steps.simps rev_filter sorted_list_of_set_filter
       intro!: lsteps_smaller_set)
 
 lemma lsteps_level_greater_fun_image:
   assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x < l"
   shows   "lsteps xs f l u v = 0"
   using assms by (induction xs f l u v rule: lsteps.induct) (auto simp add: lsteps.simps)
 
 lemma lsteps_smaller_card_Max_fun':
   assumes "\<exists>x \<in> set xs. l \<le> f x"
   shows   "lsteps xs f l u v + l * u \<le> v * length xs + u * Max ((f ` (set xs)) \<union> {0})"
   using assms proof (induction xs f l u v rule: lsteps.induct)
   case (1 f l up left)
   then show ?case by (simp)
 next
   case (2 x xs f l up left)
   consider "l = f x" "\<exists>y\<in>set xs. l \<le> f y" | "f x = l" "\<not> (\<exists>y\<in>set xs. l \<le> f y)" |
    "f x < l" | "l < f x"
     by fastforce
   then show ?case
   proof cases
     assume a: "l = f x" "\<exists>y\<in>set xs. l \<le> f y"
     have "lsteps (x # xs) f l up left + l * up = lsteps xs f l up left + f x * up + left"
       using a by (auto simp add: lsteps.simps)
     also have "lsteps xs f l up left + f x * up \<le> left * length xs + up * Max (f ` set xs \<union> {0})"
       using a 2 by blast
     also have "up * Max (f ` set xs \<union> {0}) \<le> up * Max (insert (f x) (f ` set xs))"
       by simp
     finally  show ?case
       by auto
   next
     assume a: "f x = l" "\<not> (\<exists>y\<in>set xs. l \<le> f y)"
     have "lsteps (x # xs) f l up left + l * up = lsteps xs f l up left + f x * up + left"
       using a by (auto simp add: lsteps.simps)
     also have "lsteps xs f l up left = 0"
       using a by (subst lsteps_level_greater_fun_image) auto
     also have "f x * up \<le> up * Max (insert (f x) (f ` set xs))"
       by simp
     finally show ?case
       by simp
   next
     assume a: "f x < l"
     then have "lsteps (x # xs) f l up left = lsteps xs f l up left"
       by (auto simp add: lsteps.simps)
     also have "\<dots> + l * up \<le> left * length (x # xs) + up * Max (insert 0 (f ` set xs))"
       using a 2 by auto
     also have "Max (insert 0 (f ` set xs)) \<le> Max (f ` set (x # xs) \<union> {0})"
       by simp
     finally show ?case
       by simp
   next
   assume "f x > l"
     then show ?case
       using 2 by (subst lsteps.simps) auto
   qed
 qed
 
 lemma steps_smaller_card_Max_fun':
   assumes "finite A" "\<exists>x\<in>A. l \<le> f x"
   shows   "steps A f l up left + l * up \<le> left * card A + up * Max\<^sub>0 (f ` A)"
 proof -
   let ?xs = "rev (sorted_list_of_set A)"
   have "steps A f l up left  = lsteps (rev (sorted_list_of_set A)) f l up left"
     using steps_lsteps by blast
   also have "\<dots> + l * up \<le> left * length ?xs + up * Max (f ` set ?xs \<union> {0})"
     using assms by (intro lsteps_smaller_card_Max_fun') auto
   also have "left * length ?xs = left * card A"
     using assms sorted_list_of_set_length by (auto)
   also have "set ?xs = A"
     using assms by (auto)
   finally show ?thesis
     by simp
 qed
 
 lemma lsteps_height:
   assumes  "\<exists>x \<in> set xs. l \<le> f x"
   shows "lsteps xs f l up 0 + up * l = up * Max\<^sub>0 (f ` (set xs))"
   using assms proof (induction xs f l up "0::nat" rule: lsteps.induct)
   case (2 x xs f l up)
   consider "l = f x" "\<exists>y\<in>set xs. l \<le> f y" | "f x = l" "\<not> (\<exists>y\<in>set xs. l \<le> f y)" |
    "f x < l" | "l < f x"
     by fastforce
   then show ?case
  proof cases
    assume 0: "l = f x" "\<exists>y\<in>set xs. l \<le> f y"
     then have 1: "set xs \<noteq> {}"
       using 2 by auto
     then have "\<exists>xa\<in>set xs. f x \<le> f xa"
       using 0 2 by force
     then have "f x \<le> Max (f ` set xs)"
       using 0 2 by (subst Max_ge_iff) auto
     then have "max (f x) (Max (f ` set xs)) = (Max (f ` set xs))"
       using 0 2 by (auto intro!: simp add: max_def)
     then show ?case
       using 0 1 2 by (subst lsteps.simps) (auto)
   next
     assume 0: "f x = l" "\<not> (\<exists>y\<in>set xs. l \<le> f y)"
     then have "Max (insert l (f ` set xs)) = l"
       by (intro Max_eqI) (auto)
     moreover have "lsteps xs f l up 0 = 0"
       using 0 by (subst lsteps_level_greater_fun_image) auto
     ultimately show ?case
        using 0 by (subst lsteps.simps) auto
   next
     assume 0: "f x < l"
     then have 1: "set xs \<noteq> {}"
       using 2 by auto
     then have "\<exists>xa\<in>set xs. f x \<le> f xa"
       using 0 2 by force
     then have " f x \<le> Max (f ` set xs)"
       using 0 2 by (subst Max_ge_iff) auto
     then have "max (f x) (Max (f ` set xs)) = Max (f ` set xs)"
       using 0 2 by (auto intro!: simp add: max_def)
     then show ?case
       using 0 1 2 by (subst lsteps.simps) (auto)
   next
   assume "f x > l"
     then show ?case
       using 2 by (subst lsteps.simps) auto
   qed
 qed (simp)
 
 lemma steps_height:
   assumes "finite A"
   shows   "steps A f 0 up 0 = up * Max\<^sub>0 (f ` A)"
 proof -
   have "steps A f 0 up 0 = lsteps (rev (sorted_list_of_set A)) f 0 up 0 + up * 0"
     by (subst steps_lsteps) simp
   also have "\<dots> = up * Max (f ` A \<union> {0})" if "A \<noteq> {}"
     using assms that by (subst lsteps_height) auto
   finally show ?thesis
     using assms by (cases "A = {}") (auto)
 qed
 
 context random_skip_list
 begin
 
 text \<open>
   We can now define the pmf describing the length of the search path in a skip list.
   Like the height it only depends on the number of elements in the skip list's underlying set.
 \<close>
 
 definition R where "R A u l = map_pmf (\<lambda>f. steps A f 0 u l) (SL A)"
 definition R\<^sub>N :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat pmf" where "R\<^sub>N n u l = R {..<n} u l"
 
 
 lemma R\<^sub>N_alt_def: "R\<^sub>N n u l = map_pmf (\<lambda>f. steps {..<n} f 0 u l) (SL\<^sub>N n)"
   unfolding SL\<^sub>N_def R\<^sub>N_def R_def by simp
 
 context includes monad_normalisation
 begin
 
 lemma R_R\<^sub>N:
   assumes "finite A" "p \<in> {0..1}"
   shows "R A u l = R\<^sub>N (card A) u l"
 proof -
   let ?steps = "\<lambda>A f. steps A f 0 u l"
   let ?f' = "bij_mono_map_set_to_nat A"
   have "R A u l = SL A \<bind> (\<lambda>f. return_pmf (?steps A f))"
     unfolding R_def map_pmf_def by simp
   also have "\<dots> = SL\<^sub>N (card A) \<bind> (\<lambda>f. return_pmf (?steps A (f \<circ> ?f')))"
   proof -
     have "?f' x \<notin> {..<card A}" if "x \<notin> A" for x
       using that unfolding bij_mono_map_set_to_nat_def by (auto)
     then show ?thesis
       using assms bij_mono_map_set_to_nat unfolding SL_def SL\<^sub>N_def
       by (subst Pi_pmf_bij_betw[of _ ?f' "{..<card A}"])
         (auto simp add: map_pmf_def)
   qed
   also have "\<dots> = SL\<^sub>N (card A) \<bind> (\<lambda>f. return_pmf (?steps {..<card A} f))"
     using assms bij_mono_map_set_to_nat bij_betw_def by (subst steps_image) (fastforce)+
   finally show ?thesis
     unfolding R\<^sub>N_def R_def SL\<^sub>N_def SL_def by (simp add: map_pmf_def)
 qed
 
 text \<open>
   @{const R\<^sub>N} fulfills a recurrence relation. If we move up or to the left the ``remaining'' length of the
   search path is again a slightly different probability distribution over the length.
 \<close>
 
 lemma R\<^sub>N_recurrence:
   assumes "0 < n" "p \<in> {0<..1}"
   shows   "R\<^sub>N n u l =
              do {
                b \<leftarrow> bernoulli_pmf p;
                if b then               \<comment> \<open>leftwards\<close>
                  map_pmf (\<lambda>n. n + l) (R\<^sub>N (n - 1) u l)
                else do {               \<comment> \<open>upwards\<close>
                  m \<leftarrow> binomial_pmf (n - 1) (1 - p);
                  map_pmf (\<lambda>n. n + u) (R\<^sub>N (m + 1) u l)
                }
              }"
 proof -
   define B where "B = (\<lambda>b. insert (n-1) {x \<in> {..<n - 1}. \<not> b x})"
   have "R\<^sub>N n u l = map_pmf (\<lambda>f. steps {..<n} f 0 u l) (SL\<^sub>N n)"
     by (auto simp add: R\<^sub>N_def R_def SL\<^sub>N_def)
   also have "\<dots> = map_pmf (\<lambda>f. steps {..<n} f 0 u l)
                           (map_pmf (\<lambda>(y, f). f(n-1 := y)) (pair_pmf (geometric_pmf p) (SL\<^sub>N (n - 1))))"
   proof -
     have "{..<n} = insert (n - Suc 0) {..<n - 1}"
       using assms by force
     then have "(Pi_pmf {..<n} 0 (\<lambda>_. geometric_pmf p)) =
                 map_pmf (\<lambda>(y, f). f(n - 1 := y)) (pair_pmf (geometric_pmf p)
                      (Pi_pmf {..<n-1} 0 (\<lambda>_. geometric_pmf p)))"
       using assms
       by (subst Pi_pmf_insert[of "{..<n-1}" "n-1" 0 "\<lambda>_. geometric_pmf p", symmetric])  (auto)
     then show ?thesis
       by (simp add: SL\<^sub>N_def SL_def)
   qed
   also have "\<dots> =
         do { g \<leftarrow> geometric_pmf p;
              f \<leftarrow> SL\<^sub>N (n - 1);
              return_pmf (steps {..<n} (f(n - 1 := g)) 0 u l)}"
     by (simp add: case_prod_beta map_pmf_def pair_pmf_def)
   also have "\<dots> =
         do { b \<leftarrow>  bernoulli_pmf p;
              g \<leftarrow> if b then return_pmf 0 else map_pmf Suc (geometric_pmf p);
              f \<leftarrow> SL\<^sub>N (n - 1);
              return_pmf (steps {..<n} (f(n - 1 := g)) 0 u l)}"
     using assms by (subst geometric_bind_pmf_unfold) (auto)
   also have "\<dots> =
         do { b \<leftarrow> bernoulli_pmf p;
              if b
                then do { g \<leftarrow> return_pmf 0;
                          f \<leftarrow> SL\<^sub>N (n - 1);
                          return_pmf (steps {..<n} (f(n - 1 := g)) 0 u l) }
                else do { g \<leftarrow> map_pmf Suc (geometric_pmf p);
                          f \<leftarrow> SL\<^sub>N (n - 1);
                          return_pmf (steps {..<n} (f(n - 1 := g)) 0 u l) }}"
     by (subst bind_pmf_if') (auto)
   also have "do { g \<leftarrow> return_pmf 0;
                        f \<leftarrow> SL\<^sub>N (n - 1);
                        return_pmf (steps {..<n} (f(n - 1 := g)) 0 u l) }  =
               do { f \<leftarrow> SL\<^sub>N (n - 1);
                         return_pmf (steps {..<n} (f(n - 1 := 0)) 0 u l) }"
     by (subst bind_return_pmf) auto
   also have "\<dots> = map_pmf (\<lambda>n. n + l) (map_pmf (\<lambda>f. steps {..<n - 1} f 0 u l) (SL\<^sub>N (n - 1)))"
   proof -
     have I: "{..<n} - {n - Suc 0} = {..<n - Suc 0}"
       by fastforce
     have "Max {..<n} = n - Suc 0"
       using assms by (intro Max_eqI) (auto)
     then have "steps {..<n} (f(n - 1 := 0)) 0 u l = l + steps {..<n - 1} f 0 u l" for f
       using assms by (subst steps.simps) (auto intro!: steps_cong simp add: I simp add: Let_def)
     then show ?thesis
       by (auto simp add: add_ac map_pmf_def)
   qed
   also have "\<dots> = map_pmf (\<lambda>n. n + l) (R\<^sub>N (n - 1) u l)"
     unfolding R\<^sub>N_def R_def SL\<^sub>N_def by simp
   also have "map_pmf Suc (geometric_pmf p) \<bind>
              (\<lambda>g. SL\<^sub>N (n - 1) \<bind>
              (\<lambda>f. return_pmf (steps {..<n} (f(n - 1 := g)) 0 u l)))
              =
              Pi_pmf {..<n - 1} True (\<lambda>_. bernoulli_pmf p) \<bind>
              (\<lambda>b. map_pmf Suc (geometric_pmf p) \<bind>
              (\<lambda>g. Pi_pmf {x \<in> {..<n - 1}. \<not> b x} 0 (\<lambda>_. map_pmf Suc (geometric_pmf p)) \<bind>
              (\<lambda>f. return_pmf (steps {..<n} (f(n - 1 := g)) 0 u l))))"
     using assms unfolding SL\<^sub>N_def SL_def by (subst Pi_pmf_geometric_filter) (auto)
   also have "\<dots> =
              do {
              b \<leftarrow> Pi_pmf {..<n - 1} True (\<lambda>_. bernoulli_pmf p);
              f \<leftarrow> Pi_pmf (insert (n-1) {x \<in> {..<n - 1}. \<not> b x}) 0 (\<lambda>_. map_pmf Suc (geometric_pmf p));
              return_pmf (steps {..<n} f 0 u l)}" (is "_ = ?rhs")
     using assms by (subst Pi_pmf_insert') (auto)
   also have "\<dots> =
              do {
                b \<leftarrow> Pi_pmf {..<n - 1} True (\<lambda>_. bernoulli_pmf p);
                f \<leftarrow> Pi_pmf (B b) 1 (\<lambda>_. map_pmf Suc (geometric_pmf p));
                return_pmf (steps {..<n} (\<lambda>x. if x \<in> (B b) then f x else 0) 0 u l)}"
     by (subst Pi_pmf_default_swap[symmetric, of _ _ _ 1]) (auto simp add: map_pmf_def B_def)
   also have "\<dots> =
              do {
                b \<leftarrow> Pi_pmf {..<n - 1} True (\<lambda>_. bernoulli_pmf p);
                f \<leftarrow> SL (B b);
                return_pmf (steps {..<n} (\<lambda>x. if x \<in> (B b) then Suc (f x) else 0) 0 u l)}"
   proof -
     have *: "(Suc \<circ> f) x = Suc (f x)" for x and f::"nat \<Rightarrow> nat"
       by simp
     have "(\<lambda>f. return_pmf (steps {..<n} (\<lambda>x. if x \<in> B b then (Suc \<circ> f) x else 0) 0 u l)) =
           (\<lambda>f. return_pmf (steps {..<n} (\<lambda>x. if x \<in> B b then Suc (f x) else 0) 0 u l))" for b
       by (subst *) (simp)
     then show ?thesis
       by (subst Pi_pmf_map[of _ _ 0]) (auto simp add: map_pmf_def B_def SL_def)
   qed
   also have "\<dots> =
                do {
                b \<leftarrow> Pi_pmf {..<n - 1} True (\<lambda>_. bernoulli_pmf p);
                r \<leftarrow> R (B b) u l;
                return_pmf (u + r)}"
   proof -
     have "steps {..<n} (\<lambda>x. if x \<in> B b then Suc (f x) else 0) 0 u l = u + steps (B b) f 0 u l"
       for f b
     proof -
       have "Max {..<n} = n - 1"
         using assms by (intro Max_eqI) auto
       then have "steps {..<n} (\<lambda>x. if x \<in> B b then Suc (f x) else 0) 0 u l =
               u + (steps {..<n} (\<lambda>x. if x \<in> (B b) then Suc (f x) else 0) 1 u l)"
         unfolding B_def using assms by (subst steps.simps) (auto simp add: Let_def)
       also have "steps {..<n} (\<lambda>x. if x \<in> (B b) then Suc (f x) else 0) 1 u l =
                    steps (B b) (\<lambda>x. if x \<in> (B b) then Suc (f x) else 0) 1 u l"
       proof -
         have "{x \<in> {..<n}. 1 \<le> (if x \<in> B b then Suc (f x) else 0)} = B b"
           using assms unfolding B_def by force
         then show ?thesis
           by (subst steps_smaller_set[of _ 1]) auto
       qed
       also have "\<dots> = steps (B b) (\<lambda>x. f x + 1) 1 u l"
         by (rule steps_cong) (auto)
       also have "\<dots> = steps (B b) f 0 u l"
         by (subst (2) steps_f_add'[of _ _ _ _ _ 1]) simp
       finally show ?thesis
         by auto
     qed
     then show ?thesis
       by (simp add: R_def map_pmf_def)
   qed
   also have "\<dots> = do {
                    b \<leftarrow> Pi_pmf {..<n - 1} False (\<lambda>_. bernoulli_pmf (1 - p));
                    let m = 1 + card {x. x < n - 1 \<and> b x};
                    r \<leftarrow> R {..<m} u l;
                    return_pmf (u + r)}"
   proof -
     have *: "card (insert (n - Suc 0) {x. x < n - 1 \<and> b x}) =
               (Suc (card {x. x < n - 1 \<and> b x}))" for b
       using assms by (auto simp add: card_insert_if)
     have "Pi_pmf {..<n - 1} True (\<lambda>_. bernoulli_pmf p) =
               Pi_pmf {..<n - 1} True (\<lambda>_. map_pmf Not (bernoulli_pmf (1 - p)))"
       using assms by (subst bernoulli_pmf_Not) auto
     also have "\<dots> = map_pmf ((\<circ>) Not) (Pi_pmf {..<n - 1}  False (\<lambda>_. bernoulli_pmf (1 - p)))"
       using assms by (subst Pi_pmf_map[of _ _ False]) auto
     finally show ?thesis
       unfolding B_def using assms *
       by (subst R_R\<^sub>N) (auto simp add: R_R\<^sub>N map_pmf_def)
   qed
   also have "\<dots> = binomial_pmf (n - 1) (1 - p) \<bind> (\<lambda>m. map_pmf (\<lambda>n. n + u) (R\<^sub>N (m + 1) u l))"
     using assms
     by (subst binomial_pmf_altdef'[where A = "{..<n - 1}" and dflt = "False"])
       (auto simp add: R\<^sub>N_def R_def SL_def map_pmf_def ac_simps)
   finally show ?thesis
     by simp
 qed
 
 end (* context includes monad_normalisation *)
 
 text \<open>
   The expected height and length of search path defined as non-negative integral. It's easier
   to prove the recurrence relation of the expected length of the search path using non-negative
   integrals.
 \<close>
 
 definition NH\<^sub>N where "NH\<^sub>N n = nn_integral (H\<^sub>N n) real"
 definition NR\<^sub>N where "NR\<^sub>N n u l = nn_integral (R\<^sub>N n u l) real"
 
 lemma NH\<^sub>N_EH\<^sub>N:
   assumes "p \<in> {0<..<1}"
   shows "NH\<^sub>N n = EH\<^sub>N n"
   using assms EH\<^sub>N_bounds unfolding EH\<^sub>N_def NH\<^sub>N_def by (subst nn_integral_eq_integral) (auto)
 
 lemma R\<^sub>N_0 [simp]: "R\<^sub>N 0 u l = return_pmf 0"
   unfolding R\<^sub>N_def R_def SL_def by (auto simp add: steps.simps)
 
 lemma NR\<^sub>N_bounds:
   fixes u l::nat
   shows "NR\<^sub>N n u l \<le> l * n + u * NH\<^sub>N n"
 proof -
   have "NR\<^sub>N n u l = \<integral>\<^sup>+ x. x \<partial>measure_pmf (R\<^sub>N n u l)"
     unfolding NR\<^sub>N_def R\<^sub>N_alt_def
     by (simp add: ennreal_of_nat_eq_real_of_nat)
   also have "\<dots> \<le> \<integral>\<^sup>+ x. x \<partial>(measure_pmf (map_pmf (\<lambda>f. l * n + u * Max\<^sub>0 (f ` {..<n})) (SL\<^sub>N n)))"
     using of_nat_mono[OF steps_smaller_card_Max_fun'[of "{..<n}" 0 _ u l]] unfolding R\<^sub>N_alt_def
     by (cases "n = 0") (auto intro!: nn_integral_mono)
   also have "\<dots> = l * n + u * NH\<^sub>N n"
     unfolding NH\<^sub>N_def H\<^sub>N_def H_def SL\<^sub>N_def
     by (auto simp add: nn_integral_add nn_integral_cmult ennreal_of_nat_eq_real_of_nat ennreal_mult)
   finally show "NR\<^sub>N n u l \<le> l * n + u * NH\<^sub>N n"
     by simp
 qed
 
 lemma NR\<^sub>N_recurrence:
   assumes "0 < n" "p \<in> {0<..<1}"
   shows "NR\<^sub>N n u l = (p * (l + NR\<^sub>N (n - 1) u l) +
                      q * (u + (\<Sum>k<n - 1. NR\<^sub>N (k + 1) u l * (pmf (binomial_pmf (n - 1) q) k))))
                      / (1 - (q ^ n))"
 proof -
   define B where "B = (\<lambda>n k. pmf (binomial_pmf n q) k)"
   have q: "q \<in> {0<..<1}"
     using assms unfolding q_def by auto
   then have "q ^ n < 1"
     using assms power_Suc_less_one by (induction n) (auto)
   then have qn: "q ^ n \<in> {0<..<1}"
     using assms q by (auto)
   have "NR\<^sub>N n u l = p * (l + NR\<^sub>N (n - 1) u l) +
                     q * (u + \<integral>\<^sup>+ k. NR\<^sub>N (k + 1) u l  \<partial>measure_pmf (binomial_pmf (n - 1) q))"
     using assms unfolding NR\<^sub>N_def
     by(subst R\<^sub>N_recurrence)
       (auto simp add: field_simps nn_integral_add q_def ennreal_of_nat_eq_real_of_nat)
   also have "(\<integral>\<^sup>+ m. NR\<^sub>N (m + 1) u l  \<partial>measure_pmf (binomial_pmf (n - 1) q)) =
     (\<Sum>k\<le>n - 1. NR\<^sub>N (k + 1) u l * B (n - 1) k)"
     using assms unfolding B_def q_def
     by (auto simp add: nn_integral_measure_pmf_finite)
   also have "\<dots> = (\<Sum>k\<in>{..<n - 1} \<union> {n - 1}. NR\<^sub>N (k + 1) u l * B (n - 1) k)"
     by (rule sum.cong) (auto)
   also have "\<dots> = (\<Sum>k<n - 1. NR\<^sub>N (k + 1) u l * B (n - 1) k) + NR\<^sub>N n u l * q ^ (n - 1)"
     unfolding B_def q_def using assms by (subst sum.union_disjoint) (auto)
   finally have "NR\<^sub>N n u l = p * (l + NR\<^sub>N (n - 1) u l) +
                             q * ((\<Sum>k<n - 1. NR\<^sub>N (k + 1) u l * B (n - 1) k) + u) +
                             NR\<^sub>N n u l * (q ^ (n - 1)) * q"
     using assms by (auto simp add: field_simps numerals)
   also have "NR\<^sub>N n u l * (q ^ (n - 1)) * q = (q ^ n) * NR\<^sub>N n u l"
     using q power_minus_mult[of _ q] assms
     by (subst mult_ac, subst ennreal_mult[symmetric], auto simp add: mult_ac)
   finally have 1: "NR\<^sub>N n u l = p * (l + NR\<^sub>N (n - 1) u l) +
                                q * (u + (\<Sum>k<n - 1. NR\<^sub>N (k + 1) u l * (B (n - 1) k))) +
                                (q ^ n) * NR\<^sub>N n u l "
     by (simp add: add_ac)
   have "x - z = y" if "x = y + z" "z \<noteq> \<top>" for x y z::ennreal
      using that by (subst that) (auto)
    have "NR\<^sub>N n u l \<le> l * n + u * NH\<^sub>N n"
      using NR\<^sub>N_bounds by (auto simp add: ennreal_of_nat_eq_real_of_nat)
    also have "NH\<^sub>N n = EH\<^sub>N n"
      using assms NH\<^sub>N_EH\<^sub>N by auto
    also have "(l * n) + u * ennreal (EH\<^sub>N n) < \<top>"
      by (simp add: ennreal_mult_less_top of_nat_less_top)
    finally have 3: "NR\<^sub>N n u l \<noteq> \<top>"
      by simp
   have 2: "x = y / (1 - a)" if "x = y + a * x" and t: "x \<noteq> \<top>" "a \<in> {0<..<1}" for x y::ennreal
           and a::real
   proof -
     have "y = x - a * x"
       using t by (subst that) (auto simp add: ennreal_mult_eq_top_iff)
     also have "\<dots> = x * (ennreal 1 - ennreal a)"
       using that by (auto simp add: mult_ac ennreal_right_diff_distrib)
     also have "ennreal 1 - ennreal a = ennreal (1 - a)"
       using that by (subst ennreal_minus) (auto)
     also have "x * (1 - a) / (1 - a) = x"
       using that ennreal_minus_eq_0 not_less by (subst mult_divide_eq_ennreal) auto
     finally show ?thesis
       by simp
   qed
   have "NR\<^sub>N n u l = (p * (l + NR\<^sub>N (n - 1) u l) +
                      q * (u + (\<Sum>k<n - 1. NR\<^sub>N (k + 1) u l * (B (n - 1) k))))
                    / (1 - (q ^ n))"
     using 1 3 assms qn by (intro 2) auto
   then show ?thesis
     unfolding B_def by simp
 qed
 
 lemma NR\<^sub>n_NH\<^sub>N: "NR\<^sub>N n u 0 = u * NH\<^sub>N n"
 proof -
   have "NR\<^sub>N n u 0 = \<integral>\<^sup>+ f. steps {..<n} f 0 u 0 \<partial>measure_pmf (SL\<^sub>N n)"
     unfolding NR\<^sub>N_def R\<^sub>N_alt_def by (auto simp add: ennreal_of_nat_eq_real_of_nat)
   also have "\<dots> = \<integral>\<^sup>+ f. of_nat u * of_nat (Max\<^sub>0 (f ` {..<n})) \<partial>measure_pmf (SL\<^sub>N n)"
     by (intro nn_integral_cong) (auto simp add: steps_height)
   also have "\<dots> = u * NH\<^sub>N n"
     by (auto simp add: NH\<^sub>N_def H\<^sub>N_def H_def SL\<^sub>N_def  ennreal_of_nat_eq_real_of_nat nn_integral_cmult)
   finally show ?thesis
     by simp
 qed
 
 lemma NR\<^sub>N_recurrence':
   assumes "0 < n" "p \<in> {0<..<1}"
   shows "NR\<^sub>N n u l = (p * l + p * NR\<^sub>N (n - 1) u l +
                      q * u + q * (\<Sum>k<n - 1. NR\<^sub>N (k + 1) u l * (pmf (binomial_pmf (n - 1) q) k)))
                      / (1 - (q ^ n))"
   unfolding NR\<^sub>N_recurrence[OF assms]
   by (auto simp add: field_simps ennreal_of_nat_eq_real_of_nat ennreal_mult' ennreal_mult'')
 
 
 lemma NR\<^sub>N_l_0:
   assumes "0 < n" "p \<in> {0<..<1}"
   shows "NR\<^sub>N n u 0 = (p * NR\<^sub>N (n - 1) u 0 +
                      q * (u + (\<Sum>k<n - 1. NR\<^sub>N (k + 1) u 0 * (pmf (binomial_pmf (n - 1) q) k))))
                      / (1 - (q ^ n))"
   unfolding NR\<^sub>N_recurrence[OF assms] by (simp)
 
 lemma NR\<^sub>N_u_0:
   assumes "0 < n" "p \<in> {0<..<1}"
   shows "NR\<^sub>N n 0 l = (p * (l + NR\<^sub>N (n - 1) 0 l) +
                      q * (\<Sum>k<n - 1. NR\<^sub>N (k + 1) 0 l * (pmf (binomial_pmf (n - 1) q) k)))
                      / (1 - (q ^ n))"
   unfolding NR\<^sub>N_recurrence[OF assms] by (simp)
 
 lemma NR\<^sub>N_0[simp]: "NR\<^sub>N 0 u l = 0"
   unfolding NR\<^sub>N_def R\<^sub>N_def R_def by (auto)
 
 lemma NR\<^sub>N_1:
   assumes "p \<in> {0<..<1}"
   shows "NR\<^sub>N 1 u l = (u * q + l * p) / p"
 proof -
   have "NR\<^sub>N 1 u l = (ennreal p * of_nat l + ennreal q * of_nat u) / ennreal (1 - q)"
     using assms by (subst NR\<^sub>N_recurrence) auto
   also have "(ennreal p * of_nat l + ennreal q * of_nat u) = (u * q + l * p)"
     using assms q_def by (subst ennreal_plus)
       (auto simp add: field_simps ennreal_mult' ennreal_of_nat_eq_real_of_nat)
   also have "\<dots> / ennreal (1 - q) = ennreal ((u * q + l * p) / (1 - q))"
      using q_def assms by (intro divide_ennreal) auto
   finally show ?thesis
     unfolding q_def by simp
 qed
 
 lemma NR\<^sub>N_NR\<^sub>N_l_0:
   assumes n: "0 < n" and p: "p \<in> {0<..<1}" and "u \<ge> 1"
   shows "NR\<^sub>N n u 0 = (u * q / (u * q + l * p)) * NR\<^sub>N n u l"
   using n proof (induction n rule: less_induct)
   case (less i)
   have 1: "0 < u * q"
     unfolding q_def using assms by simp
   moreover have "0 \<le> l * p"
     using assms by auto
   ultimately have 2: "0 < u * q + l * p"
     by arith
   define c where "c = ennreal (u * q / (u * q + l * p))"
   have [simp]: "c / c = 1"
   proof -
     have "u * q / (u * q + l * p) \<noteq> 0"
       using assms q_def 2 by auto
     then show ?thesis
       unfolding c_def using p q_def by (auto intro!: ennreal_divide_self)
   qed
   show ?case
   proof (cases "i = 1")
     case True
     have "c * NR\<^sub>N i u l = c * ((u * q + l * p) / p)"
       unfolding c_def True by (subst NR\<^sub>N_1[OF p]) auto
     also have "\<dots> = ennreal ((u * q / (u * q + l * p)) * ((u * q + l * p) / p))"
       unfolding c_def using assms q_def by (subst ennreal_mult'') auto
     also have "(u * q / (u * q + l * p)) * ((u * q + l * p) / p) = u * q / p"
     proof -
       have I: "(a / b) * (b / c) = a / c" if "0 < b" for a b c::"real"
         using that by (auto)
       show ?thesis
         using 2 q_def by (intro I) auto
     qed
     also have "\<dots> = NR\<^sub>N i u 0"
       unfolding True c_def by (subst NR\<^sub>N_1[OF p]) (auto)
     finally show ?thesis
       unfolding c_def using True by simp
   next
     case False
     then have i: "i > 1"
       using less by auto
     define c where "c = ennreal (u * q / (u * q + l * p))"
     define B where "B = (\<Sum>k<i - 1. NR\<^sub>N (k + 1) u l * ennreal (pmf (binomial_pmf (i - 1) q) k))"
     have "NR\<^sub>N i u 0 = (p * NR\<^sub>N (i - 1) u 0 +
                      q * (u + (\<Sum>k<i - 1. NR\<^sub>N (k + 1) u 0 * (pmf (binomial_pmf (i - 1) q) k))))
                      / (1 - (q ^ i))"
       using less assms by (subst NR\<^sub>N_l_0) auto
     also have "q * (u + (\<Sum>k<i - 1. NR\<^sub>N (k + 1) u 0 * (pmf (binomial_pmf (i - 1) q) k))) =
              q * u + q * (\<Sum>k<i - 1. NR\<^sub>N (k + 1) u 0 * (pmf (binomial_pmf (i - 1) q) k))"
       using assms q_def
       by (auto simp add: field_simps ennreal_of_nat_eq_real_of_nat ennreal_mult)
     also have "NR\<^sub>N (i - 1) u 0 = c * NR\<^sub>N (i - 1) u l"
       unfolding c_def using less i by (intro less) (auto)
     also have "(\<Sum>k<i - 1. NR\<^sub>N (k + 1) u 0 * ennreal (pmf (binomial_pmf (i - 1) q) k)) =
              (\<Sum>k<i - 1. c * NR\<^sub>N (k + 1) u l * ennreal (pmf (binomial_pmf (i - 1) q) k))"
       by (auto intro!: sum.cong simp add: less c_def)
     also have "\<dots> = c * B"
       unfolding B_def by (subst sum_distrib_left) (auto intro!: sum.cong mult_ac)
     also have "q * (c * B) = c * (q * B)"
       by (simp add: mult_ac)
     also have "ennreal (q * real u) = q * u * ((u * q + l * p) / (u * q + l * p))"
       using assms 2 by (auto simp add: field_simps q_def)
     also have "\<dots> = c * (real u * q + real l * p)"
       unfolding c_def using 2 by (subst ennreal_mult''[symmetric]) (auto simp add: mult_ac)
     also have "c * ennreal (real u * q + real l * p) + c * (ennreal q * B) =
              c * (ennreal (real u * q + real l * p) + (ennreal q * B))"
       by (auto simp add: field_simps)
     also have "ennreal p * (c * NR\<^sub>N (i - 1) u l) = c * (ennreal p * NR\<^sub>N (i - 1) u l)"
       by (simp add: mult_ac)
     also have "(c * (ennreal p * NR\<^sub>N (i - 1) u l) + c * (ennreal (u * q + l * p) + ennreal q * B))
             = c * ((ennreal p * NR\<^sub>N (i - 1) u l) + (ennreal (u * q + l * p) + ennreal q * B))"
       by (auto simp add: field_simps)
     also have " c * (ennreal p * NR\<^sub>N (i - 1) u l + (ennreal (u * q + l * p) + ennreal q * B)) / ennreal (1 - q ^ i)
          =  c * ((ennreal p * NR\<^sub>N (i - 1) u l + (ennreal (u * q + l * p) + ennreal q * B)) / ennreal (1 - q ^ i))"
       by (auto simp add: ennreal_times_divide)
     also have "(ennreal p * NR\<^sub>N (i - 1) u l + (ennreal (real u * q + real l * p) + ennreal q * B)) / ennreal (1 - q ^ i)
         = NR\<^sub>N i u l"
       apply(subst (2) NR\<^sub>N_recurrence')
       using i assms q_def by
         (auto simp add: field_simps B_def ennreal_of_nat_eq_real_of_nat ennreal_mult' ennreal_mult'')
     finally show ?thesis
       unfolding c_def by simp
   qed
 qed
 
 text \<open>
   Assigning 1 as the cost for going up and/or left, we can now show the relation between the
   expected length of the reverse search path and the expected height.
 \<close>
 
 definition EL\<^sub>N where "EL\<^sub>N n = measure_pmf.expectation (R\<^sub>N n 1 1) real"
 
 
 theorem EH\<^sub>N_EL\<^sub>s\<^sub>p:
   assumes "p \<in> {0<..<1}"
   shows "1 / q * EH\<^sub>N n = EL\<^sub>N n"
 proof -
   have 1: "ennreal (1 / y * x) = r" if "ennreal x = y * r" "x \<ge> 0" "y > 0"
     for x y::real and r::ennreal
   proof -
     have "ennreal ((1 / y) * x) = ennreal (1 / y) * ennreal x"
       using that apply(subst ennreal_mult'') by auto
     also note that(1)
     also have "ennreal (1 / y) * (ennreal y * r) = ennreal ((1 / y) * y) * r"
       using that by (subst ennreal_mult'') (auto simp add: mult_ac)
     also have "(1 / y) * y = 1"
       using that by (auto)
     finally show ?thesis
       by auto
   qed
   have "EH\<^sub>N n = NH\<^sub>N n"
     using NH\<^sub>N_EH\<^sub>N assms by auto
   also have "NH\<^sub>N n = NR\<^sub>N n 1 0"
     using NR\<^sub>n_NH\<^sub>N by auto
   also have "NR\<^sub>N n 1 0 = q * NR\<^sub>N n 1 1" if "n > 0"
     using NR\<^sub>N_NR\<^sub>N_l_0[of _ 1 1] that assms q_def by force
   finally have "ennreal (EH\<^sub>N n) = q * NR\<^sub>N n 1 1" if "n > 0"
     using that by blast
   then have "1 / q * EH\<^sub>N n = NR\<^sub>N n 1 1" if "n > 0"
     using that assms q_def by (intro 1) (auto simp add: EH\<^sub>N_def H\<^sub>N_def H_def)
   moreover have "1 / q * EH\<^sub>N n = NR\<^sub>N n 1 1" if "n = 0"
     unfolding that by (auto simp add: EH\<^sub>N_def H\<^sub>N_def H_def)
   ultimately have 2: "ennreal (1 / q * EH\<^sub>N n) = NR\<^sub>N n 1 1"
     by blast
   also have "NR\<^sub>N n 1 1 = EL\<^sub>N n"
     using 2 assms EH\<^sub>N_bounds unfolding EL\<^sub>N_def NR\<^sub>N_def
     by(subst nn_integral_eq_integral)
       (auto intro!: integrableI_nn_integral_finite[where x="EH\<^sub>N n / q"])
   finally show ?thesis
     using assms q_def ennreal_inj unfolding EL\<^sub>N_def EH\<^sub>N_def H\<^sub>N_def H_def SL_def
     by (auto)
 qed
 
 end (* context random_skip_list *)
 
 thm random_skip_list.EH\<^sub>N_EL\<^sub>s\<^sub>p[unfolded random_skip_list.q_def]
     random_skip_list.EH\<^sub>N_bounds'[unfolded random_skip_list.q_def]
 
 
 end