diff --git a/thys/Approximate_Model_Counting/ApproxMCAnalysis.thy b/thys/Approximate_Model_Counting/ApproxMCAnalysis.thy
--- a/thys/Approximate_Model_Counting/ApproxMCAnalysis.thy
+++ b/thys/Approximate_Model_Counting/ApproxMCAnalysis.thy
@@ -1,764 +1,764 @@
 section \<open> ApproxMC definition and analysis \<close>
 
 text \<open>
   This section puts together preceding results to formalize the
   PAC guarantee of ApproxMC.
 \<close>
 
 theory ApproxMCAnalysis imports
   ApproxMCCoreAnalysis
   RandomXORHashFamily
   Median_Method.Median
 begin
 
 lemma replicate_pmf_Pi_pmf:
   assumes "distinct ls"
   shows "replicate_pmf (length ls) P =
     map_pmf (\<lambda>f. map f ls)
       (Pi_pmf (set ls) def (\<lambda>_. P))"
   using assms
 proof (induction ls)
   case Nil
   then show ?case
   by auto
 next
   case (Cons x xs)
   then show ?case
     by (auto intro!: bind_pmf_cong simp add: Pi_pmf_insert' map_bind_pmf bind_map_pmf)
 qed
 
 lemma replicate_pmf_Pi_pmf':
   assumes "finite V"
   shows "replicate_pmf (card V) P =
     map_pmf (\<lambda>f. map f (sorted_list_of_set V))
       (Pi_pmf V def (\<lambda>_. P))"
 proof -
   have *:"card V = length (sorted_list_of_set V)"
     using assms by auto
   show ?thesis
     unfolding *
     apply (subst replicate_pmf_Pi_pmf)
     using assms by auto
 qed
 
 definition map_of_default::"('a \<times> 'b) list \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
 where "map_of_default ls def =
   (let m = map_of ls in
   (\<lambda>x. case m x of None \<Rightarrow> def | Some v \<Rightarrow> v))"
 
 lemma Pi_pmf_replicate_pmf:
   assumes "finite V"
   shows
     "(Pi_pmf V def (\<lambda>_. p)) =
     map_pmf (\<lambda>bs.
       map_of_default (zip (sorted_list_of_set V) bs) def)
       (replicate_pmf (card V) p)"
 proof -
   show ?thesis
    apply (subst replicate_pmf_Pi_pmf'[OF assms, where def="def"])
   unfolding map_pmf_comp
    apply (intro map_pmf_idI[symmetric])
    unfolding map_of_default_def Let_def fun_eq_iff map_of_zip_map
    by (smt (verit, del_insts) assms option.case(1) option.case(2) pmf_Pi pmf_eq_0_set_pmf sorted_list_of_set.set_sorted_key_list_of_set)
 qed
 
 lemma proj_inter_neutral:
   assumes "\<And>w. w \<in> B \<longleftrightarrow> restr S w \<in> C"
   shows "proj S (A \<inter> B) = proj S A \<inter> C"
   unfolding ApproxMCCore.proj_def
   using assms by auto
 
 text \<open>
   An abstract spec of ApproxMC for any Boolean theory.
   This locale must be instantiated with a theory implementing the two
   the functions below (and satisfying the assumption linking them).
 \<close>
 locale ApproxMC =
   fixes sols :: "'fml \<Rightarrow> ('a \<Rightarrow> bool) set"
   fixes enc_xor :: "'a set \<times> bool \<Rightarrow> 'fml \<Rightarrow> 'fml"
   assumes sols_enc_xor:
     "\<And>F xor. finite (fst xor) \<Longrightarrow>
       sols (enc_xor xor F) =
       sols F \<inter> {\<omega>. satisfies_xor xor {x. \<omega> x}}"
 begin
 
 definition compute_thresh :: "real \<Rightarrow> nat"
   where "compute_thresh \<epsilon> =
   nat \<lceil>1 + 9.84 * (1 + \<epsilon> / (1 + \<epsilon>)) * (1 + 1 / \<epsilon>)^2\<rceil>"
 
 definition fix_t :: "real \<Rightarrow> nat"
   where "fix_t \<delta> =
   nat \<lceil>ln (1 / \<delta>) /(2 * (0.5-0.36)^2)\<rceil>"
 
 definition raw_median_bound :: "real \<Rightarrow> nat \<Rightarrow> real"
   where "raw_median_bound \<alpha> t =
   (\<Sum>i = 0..t div 2.
     (t choose i) * (1 / 2 + \<alpha>) ^ i * (1 / 2 - \<alpha>) ^ (t - i))"
 
 definition compute_t :: "real \<Rightarrow> nat \<Rightarrow> nat"
   where "compute_t \<delta> n =
   (if raw_median_bound 0.14 n < \<delta> then n
   else fix_t \<delta>)"
 
 (* The size of the projected solution set after adding i XORs*)
 definition size_xor ::"
   'fml \<Rightarrow> 'a set \<Rightarrow>
   (nat \<Rightarrow> ('a set \<times> bool) option) \<Rightarrow>
   nat \<Rightarrow> nat"
   where "size_xor F S xorsf i = (
     let xors = map (the \<circ> xorsf) [0..<i] in
     let Fenc = fold enc_xor xors F in
       card (proj S (sols Fenc))
     )"
 
 definition check_xor ::"
   'fml \<Rightarrow> 'a set \<Rightarrow>
   nat \<Rightarrow>
   (nat \<Rightarrow> ('a set \<times> bool) option) \<Rightarrow>
   nat \<Rightarrow> bool"
   where "check_xor F S thresh xorsf i =
   (size_xor F S xorsf i < thresh)"
 
 definition approxcore_xors :: "
   'fml \<Rightarrow> 'a set \<Rightarrow>
   nat \<Rightarrow>
   (nat \<Rightarrow> ('a set \<times> bool) option) \<Rightarrow>
   nat"
   where "
     approxcore_xors F S thresh xorsf =
     (case List.find
       (check_xor F S thresh xorsf) [1..<card S] of
       None \<Rightarrow> 2 ^ card S
     | Some m \<Rightarrow>
       (2 ^ m * size_xor F S xorsf m))"
 
 definition approxmccore :: "'fml \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> nat pmf"
 where "approxmccore F S thresh =
   map_pmf (approxcore_xors F S thresh) (random_xors S (card S - 1))"
 
 definition approxmc :: "'fml \<Rightarrow> 'a set \<Rightarrow> real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> nat pmf"
   where "approxmc F S \<epsilon> \<delta> n = (
     let thresh = compute_thresh \<epsilon> in
     if card (proj S (sols F)) < thresh then
       return_pmf (card (proj S (sols F)))
     else
       let t = compute_t \<delta> n in
       map_pmf (median t)
         (prod_pmf {0..<t::nat} (\<lambda>i. approxmccore F S thresh))
   )"
 
 lemma median_commute:
   assumes "t \<ge> 1"
   shows "(real \<circ> median t) = (\<lambda>w::nat \<Rightarrow> nat. median t (real \<circ> w))"
   unfolding median_def map_map[symmetric]
   apply (subst Median.map_sort[where f = "\<lambda>x. real x"])
   subgoal by (clarsimp simp add:mono_def)
   apply (subst nth_map)
   using assms by auto
 
 lemma median_default:
   shows "median t y = median t (\<lambda>x. if x < t then y x else def)"
   unfolding median_def
   by (auto intro!: arg_cong[where f = "\<lambda>ls. sort ls ! (t div 2)"])
 
 definition default_\<alpha>::"'a set \<Rightarrow> nat assg"
   where "default_\<alpha> S i = (if i < card S - 1 then Some True else None)"
 
 lemma dom_default_\<alpha>:
   "dom (default_\<alpha> S) = {0..<card S -1}"
   by (auto simp add:default_\<alpha>_def split: if_splits)
 
 lemma compute_thresh_bound_4:
   assumes "\<epsilon> > 0"
   shows"4 < compute_thresh \<epsilon>"
 proof -
   have 1: "(1 + \<epsilon> / (1 + \<epsilon>)) > 1"
     using assms
     by simp
   have 2: "(1 + 1 / \<epsilon>)^2 > 1"
     using assms by simp
 
   define a where "a = (1 + \<epsilon> / (1 + \<epsilon>)) * (1 + 1 / \<epsilon>)\<^sup>2"
   have "a > 1" unfolding a_def
     using 1 2
     using less_1_mult by blast
   then have "(984 / 10\<^sup>2) * a \<ge> 4"
     by auto
 
   thus ?thesis
     unfolding compute_thresh_def
     by (smt (verit) a_def arith_special(2) arithmetic_simps(1) more_arith_simps(11) nat_less_real_le numeral_Bit0 of_nat_numeral real_nat_ceiling_ge)
 qed
 
 lemma satisfies_xor_with_domain:
   assumes "fst x \<subseteq> S"
   shows "satisfies_xor x {x. w x} \<longleftrightarrow>
     satisfies_xor x ({x. w x} \<inter> S)"
   using assms
   apply (cases x)
   by (simp add: Int_assoc inf.absorb_iff2)
 
 (* The main step, where we instantiate the ApproxMCCore locale *)
 lemma approxcore_xors_eq:
   assumes thresh:
     "thresh = compute_thresh \<epsilon>"
     "thresh \<le> card (proj S (sols F))"
   assumes \<epsilon>: "\<epsilon> > (0::real)" "\<epsilon> \<le> 1"
   assumes S: "finite S"
   shows "measure_pmf.prob (random_xors S (card S - 1))
        {xors. real (approxcore_xors F S thresh xors) \<in>
         {real (card (proj S (sols F))) / (1 + \<epsilon>)..
         (1 + \<epsilon>) * real (card (proj S (sols F)))}} \<ge> 0.64"
 proof -
 
   have "ApproxMCCore (sols F) S \<epsilon> (default_\<alpha> S) thresh"
     apply unfold_locales
     subgoal using dom_default_\<alpha> by simp
     subgoal using \<epsilon> by simp
     subgoal using thresh assms(3) compute_thresh_bound_4 by blast
     using thresh S by auto
   then interpret amc: ApproxMCCore "sols F" _ _ "(default_\<alpha> S)" .
 
   have "
     m < card S \<Longrightarrow>
     {0..<m} \<subseteq> dom xors \<Longrightarrow>
     (\<And>i. i < m \<Longrightarrow> fst (the (xors i)) \<subseteq> S) \<Longrightarrow>
     (proj S
        (sols (fold enc_xor (map (the \<circ> xors) [0..<m]) F))) =
      proj S (sols F) \<inter>
         {w. hslice m (\<lambda>\<omega>. xor_hash \<omega> xors) w =
           aslice m (default_\<alpha> S)}" for m xors
   proof (induction m)
     case 0
     then show ?case
       unfolding hslice_def aslice_def
       by auto
   next
     case (Suc m)
     have m: "m \<in> dom xors"
       by (meson Set.basic_monos(7) Suc(3) atLeastLessThan_iff le0 lessI)
     have sp: "fst (the (xors m)) \<subseteq> S"
       by (simp add: Suc(4))
 
     then obtain xor where x: "xors m = Some xor"
       using m by blast
 
     have eq: "{w. xor_hash w xors m = Some True} =
         {\<omega>. satisfies_xor xor {x. \<omega> x = Some True}}"
       unfolding xor_hash_def
       by (clarsimp simp add: x)
 
     have neut: "\<And>w.
       w \<in> {\<omega>. satisfies_xor xor {x. \<omega> x}} \<longleftrightarrow>
       restr S w \<in> {\<omega>. satisfies_xor xor {x. \<omega> x = Some True}}"
       using sp unfolding restr_def
       by (smt (verit, ccfv_SIG) Collect_cong Int_def mem_Collect_eq option.sel satisfies_xor_with_domain x)
 
     have lhs: "
       proj S
        (sols (fold enc_xor (map (the \<circ> xors) [0..<Suc m]) F)) =
       proj S (sols (fold enc_xor (map (the \<circ> xors) [0..<m]) F)) \<inter>
         {w. xor_hash w xors m = Some True}"
       apply clarsimp
       apply (subst sols_enc_xor)
       subgoal using assms(5) rev_finite_subset sp by blast
       apply (subst proj_inter_neutral)
       using eq neut x by auto
 
     have rhs1:" hslice (Suc m) (\<lambda>\<omega>. xor_hash \<omega> xors) w = aslice (Suc m) (default_\<alpha> S) \<Longrightarrow>
       hslice m (\<lambda>\<omega>. xor_hash \<omega> xors) w = aslice m (default_\<alpha> S)" for w
       unfolding hslice_def aslice_def fun_eq_iff
       by (auto simp add:lessThan_Suc restrict_map_def split: if_splits)
 
     have rhs2:"hslice (Suc m) (\<lambda>\<omega>. xor_hash \<omega> xors) w = aslice (Suc m) (default_\<alpha> S) \<Longrightarrow>
       xor_hash w xors m = Some True" for w
       unfolding hslice_def aslice_def fun_eq_iff
       apply (clarsimp simp add:lessThan_Suc restrict_map_def )
       by (metis default_\<alpha>_def domIff m xor_hash_eq_dom)
 
     have rhs3: "hslice m (\<lambda>\<omega>. xor_hash \<omega> xors) w = aslice m (default_\<alpha> S) \<Longrightarrow>
       xor_hash w xors m = Some True \<Longrightarrow>
       hslice (Suc m) (\<lambda>\<omega>. xor_hash \<omega> xors) w = aslice (Suc m) (default_\<alpha> S)" for w
       unfolding hslice_def aslice_def fun_eq_iff
       apply (clarsimp simp add:lessThan_Suc restrict_map_def )
       by (metis One_nat_def Suc.prems(1) Suc_lessD Suc_less_eq Suc_pred default_\<alpha>_def gr_zeroI zero_less_diff)
 
     have rhs: "{w. hslice (Suc m) (\<lambda>\<omega>. xor_hash \<omega> xors) w = aslice (Suc m) (default_\<alpha> S)} =
       {w. hslice m (\<lambda>\<omega>. xor_hash \<omega> xors) w = aslice m (default_\<alpha> S)} \<inter>
       {w. xor_hash w xors m = Some True}"
       by (auto simp add: rhs1 rhs2 rhs3)
 
     have ih: "proj S (sols (fold enc_xor (map (the \<circ> xors) [0..<m]) F)) =
       proj S (sols F) \<inter>
       {w. hslice m (\<lambda>\<omega>. xor_hash \<omega> xors) w = aslice m (default_\<alpha> S)}"
       apply (intro Suc(1))
       using Suc(2) Suc_lessD apply blast
       using Suc(3) atLeast0_lessThan_Suc apply blast
       using Suc(4) less_SucI by blast
 
     show ?case
       unfolding lhs rhs
       by (simp add: Int_ac(1) ih)
   qed
   then have *: "
     m < card S \<Longrightarrow>
     {0..<m} \<subseteq> dom xors \<Longrightarrow>
     (\<And>i. i < m \<Longrightarrow> fst (the (xors i)) \<subseteq> S) \<Longrightarrow>
      size_xor F S xors m =
      amc.card_slice (\<lambda>\<omega>. xor_hash \<omega> xors) m" for m xors
     unfolding size_xor_def amc.card_slice_def
     by auto
 
   have **: "
    {0..<card S - 1} \<subseteq> dom xors \<Longrightarrow>
    (\<And>i. i < card S - 1 \<Longrightarrow> fst (the (xors i)) \<subseteq> S) \<Longrightarrow>
    find (check_xor F S thresh xors) [1..<card S] =
    find (\<lambda>i. (\<lambda>\<omega>. xor_hash \<omega> xors) \<in> amc.T i) [1..<card S]" for xors
     apply (intro find_cong)
     unfolding check_xor_def amc.T_def
     subgoal by simp
     apply (subst *)
       subgoal by clarsimp
       subgoal by (clarsimp simp add: domIff subset_iff)
     by auto
 
   have rw: "
     {0..<card S - 1} \<subseteq> dom xors \<Longrightarrow>
     (\<And>i. i < card S - 1 \<Longrightarrow> fst (the (xors i)) \<subseteq> S) \<Longrightarrow>
     approxcore_xors F S thresh xors =
       (\<lambda>(a,b). a*b) (amc.approxcore (\<lambda>\<omega>. xor_hash \<omega> xors))" for  xors
     apply (subst amc.approxcore_def)
     unfolding approxcore_xors_def
     apply (subst **)
       subgoal by clarsimp
       subgoal by clarsimp
     apply (clarsimp split: option.split)
     apply (subst *)
     subgoal by (auto simp add: find_Some_iff domIff subset_iff)
     subgoal by (auto simp add: find_Some_iff domIff subset_iff)
     subgoal
       using \<open>\<And>x2. \<lbrakk>{0..<card S - Suc 0} \<subseteq> dom xors; \<And>i. i < card S - Suc 0 \<Longrightarrow> fst (the (xors i)) \<subseteq> S; find (\<lambda>i. (\<lambda>\<omega>. xor_hash \<omega> xors) \<in> amc.T i) [Suc 0..<card S] = Some x2\<rbrakk> \<Longrightarrow> x2 < card S\<close> by auto 
     by auto
 
   from xor_hash_family_2_universal[OF S]
   have univ:"prob_space.k_universal (measure_pmf (random_xors S (card S - 1))) 2
    xor_hash {\<alpha>. dom \<alpha> = S} {\<alpha>. dom \<alpha> = {0..<card S - 1}}" .
 
   have "measure_pmf.prob
    (map_pmf (\<lambda>s w. xor_hash w s) (random_xors S (card S - 1)))
    amc.approxcore_fail \<le> 0.36"
     apply (intro amc.analysis_3[OF _ _ univ])
     apply (smt (verit, ccfv_SIG) Groups.mult_ac(3) amc.pivot_def assms(1) compute_thresh_def more_arith_simps(11) real_nat_ceiling_ge)
     using S finite_random_xors_set_pmf apply blast
     using \<epsilon> by auto
 
   then have b: "measure_pmf.prob
     (random_xors S (card S - 1))
     {xors.
       (real ((\<lambda>(a,b). a*b) (amc.approxcore (\<lambda>\<omega>. xor_hash \<omega> xors))))
       \<notin>
       {real (card (proj S (sols F))) / (1 + \<epsilon>)..
         (1 + \<epsilon>) * real (card (proj S (sols F)))}} \<le> 0.36"
     unfolding amc.approxcore_fail_def
     by (auto simp add: case_prod_unfold Let_def)
 
   have 1: "x \<in> set_pmf (random_xors S (card S - Suc 0)) \<Longrightarrow>
     {0..<card S - 1} \<subseteq> dom x" for x
     by (auto simp add:random_xors_set_pmf[OF S])
   have 2: "x \<in> set_pmf (random_xors S (card S - Suc 0)) \<Longrightarrow>
     (\<forall>i. i < card S - 1 \<longrightarrow> fst (the (x i)) \<subseteq> S)" for x
   proof -
     assume x: "x \<in> set_pmf (random_xors S (card S - Suc 0))"
     moreover {
       fix i
       assume i: "i < card S - 1"
       from random_xors_set_pmf[OF S]
       have xx: "dom x = {..<(card S - Suc 0)}" "ran x \<subseteq> Pow S \<times> UNIV"
         using x by auto
       obtain xi where xi: "x i = Some xi"
         using xx i apply clarsimp
         by (metis atLeast0LessThan atLeastLessThan_iff bot_nat_0.extremum domIff option.exhaust surj_pair)
       then have "fst xi \<subseteq> S" using xx(2)
         unfolding ran_def apply (clarsimp simp add: subset_iff)
         by (metis prod.collapse)
       then have "fst (the (x i)) \<subseteq> S" by (simp add: xi)
     }
     thus "(\<forall>i. i < card S - 1 \<longrightarrow> fst (the (x i)) \<subseteq> S)" by auto
   qed
 
   have "measure_pmf.prob (random_xors S (card S - 1))
        {xors. real (approxcore_xors F S thresh xors) \<in>
         {real (card (proj S (sols F))) / (1 + \<epsilon>)..
         (1 + \<epsilon>) * real (card (proj S (sols F)))}} =
     measure_pmf.prob
     (random_xors S (card S - 1))
     {xors.
       (real ((\<lambda>(a,b). a*b) (amc.approxcore (\<lambda>\<omega>. xor_hash \<omega> xors))))
       \<in>
       {real (card (proj S (sols F))) / (1 + \<epsilon>)..
         (1 + \<epsilon>) * real (card (proj S (sols F)))}}"
     apply (intro measure_pmf.measure_pmf_eq[where p = "(random_xors S (card S - 1))"])
     subgoal by auto
     apply clarsimp
     apply (frule 1)
     apply (drule 2)
     apply (frule rw)
     by auto
 
   moreover have "... =
      1 - measure_pmf.prob
       (random_xors S (card S - 1))
       {xors.
         (real ((\<lambda>(a,b). a*b) (amc.approxcore (\<lambda>\<omega>. xor_hash \<omega> xors))))
         \<notin>
         {real (card (proj S (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj S (sols F)))}}"
     apply (subst measure_pmf.prob_compl[symmetric])
     by (auto intro!: measure_pmf.measure_pmf_eq)
   moreover have "... \<ge> 0.64"
     using b
     by auto
   ultimately show ?thesis by auto
 qed
 
 lemma compute_t_ge1:
   assumes "0 < \<delta>" "\<delta> < 1"
   shows"compute_t \<delta> n \<ge> 1"
 proof -
   have "ln (1 / \<delta>) > 0"
     by (simp add: assms)
   then have fix_t: "1 \<le> fix_t \<delta>"
     unfolding fix_t_def
     by (simp add: Suc_leI)
 
   show ?thesis
   unfolding compute_t_def
   using fix_t
   apply (cases n)
   unfolding raw_median_bound_def
   using assms by auto
 qed
 
 lemma success_arith_bound:
   assumes "s \<le> (f ::nat)"
   assumes "p \<le> (1::real)" "q \<le> p" "1 /2 \<le> q"
   shows "p ^ s * (1 - p) ^ f \<le> q ^ s * (1 - q) ^ f"
 proof -
   have ple: "p * (1-p) \<le> q * (1-q)"
     using assms(2-4)
     by (sos "(((A<0 * R<1) + ((R<1 * (R<1 * [p + ~1*q]^2)) + ((A<=1 * (A<=2 * R<1)) * (R<2 * [1]^2)))))")
 
   have feq:"f = (f-s)+s"
     using Nat.le_imp_diff_is_add assms(1) by blast
   then have "(1-p)^f = (1-p)^s * (1-p)^(f-s)"
     by (metis add.commute power_add)
   then have "p ^ s * (1 - p) ^ f =
     (p * (1-p)) ^ s * (1 - p) ^ (f-s)"
     by (simp add: power_mult_distrib)
   moreover have "... \<le>
     (q * (1-q)) ^ s * (1 - p) ^ (f-s)"
     by (smt (verit) assms(1) assms(2) assms(3) assms(4) diff_self_eq_0 divide_nonneg_nonneg mult_nonneg_nonneg mult_right_mono order_le_less ple power_0 power_eq_0_iff power_mono zero_less_diff zero_less_power)
   moreover have "... \<le>
     (q * (1-q)) ^ s * (1 - q) ^ (f-s)"
     by (smt (verit, ccfv_SIG) assms(2) assms(3) assms(4) divide_eq_0_iff divide_nonneg_nonneg mult_left_mono mult_pos_pos power_mono zero_less_power)
   moreover have "... = q ^ s * (1 - q) ^ f"
     by (smt (verit) feq mult.assoc mult.commute power_add power_mult_distrib)
   ultimately show ?thesis by auto
 qed
 
 lemma prob_binomial_pmf_upto_mono:
   assumes "1/2 \<le> q" "q \<le> p" "p \<le> 1"
   shows "
   measure_pmf.prob (binomial_pmf n p) {..n div 2} \<le>
   measure_pmf.prob (binomial_pmf n q) {..n div 2}"
 proof -
   have i: "i \<le> n div 2 \<Longrightarrow>
     p ^ i * (1 - p) ^ (n - i) \<le> q ^ i * (1 - q) ^ (n - i)" for i
     using assms by(auto intro!: success_arith_bound)
 
   show ?thesis
     apply (subst prob_binomial_pmf_upto)
     subgoal using assms by auto
     subgoal using assms by auto
     apply (subst prob_binomial_pmf_upto)
     subgoal using assms by auto
     subgoal using assms by auto
     by (auto intro!: sum_mono simp add: i ab_semigroup_mult_class.mult_ac(1) mult_left_mono)
 qed
 
 (* The main result *)
 theorem approxmc_sound:
   assumes \<delta>: "\<delta> > 0" "\<delta> < 1"
   assumes \<epsilon>: "\<epsilon> > 0" "\<epsilon> \<le> 1"
   assumes S: "finite S"
   shows "measure_pmf.prob (approxmc F S \<epsilon> \<delta> n)
       {c. real c \<in>
         {real (card (proj S (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj S (sols F)))}}
       \<ge> 1 - \<delta>"
 proof -
   define thresh where "thresh = compute_thresh \<epsilon>"
   define t where "t = compute_t \<delta> n"
   then have t1: "1 \<le> t"
     using compute_t_ge1[OF \<delta>] by auto
 
   have "card (proj S (sols F)) < thresh \<or>
       card (proj S (sols F)) \<ge> thresh" by auto
   moreover {
     assume "card (proj S (sols F)) < thresh"
     then have "approxmc F S \<epsilon> \<delta> n =
       return_pmf (card (proj S (sols F)))"
       unfolding approxmc_def Let_def thresh_def
       by auto
     then have "?thesis"
       unfolding indicator_def of_bool_def
       using assms \<epsilon>
-      by (auto simp add: mult_le_cancel_left1 mult_le_cancel_right1 divide_le_eq mult_le_cancel_left1)
+      by (auto simp add: mult_le_cancel_left1 mult_le_cancel_right1 divide_le_eq)
   }
   moreover {
     assume a: "card (proj S (sols F)) \<ge> thresh"
     define Xf where "Xf = (\<lambda>(i::nat) xs.
       approxcore_xors F S thresh (xs i))"
 
     then have *: "approxmc F S \<epsilon> \<delta> n =
       map_pmf (median t)
       (prod_pmf {0..<t} (\<lambda>i. approxmccore F S thresh))"
       using a
       unfolding approxmc_def Let_def thresh_def t_def
       by auto
 
     have **: "map_pmf (real \<circ> median t)
       (Pi_pmf {0..<t} (approxcore_xors F S thresh undefined)
        (\<lambda>i. approxmccore F S thresh)) =
        map_pmf (\<lambda>\<omega>. median t (\<lambda>i. real (Xf i \<omega>)))
       (prod_pmf {0..<t} (\<lambda>i. random_xors S (card S - 1)))"
       apply (subst median_commute)
       subgoal using t1 by simp
       unfolding approxmccore_def
        apply (subst Pi_pmf_map)
       unfolding Xf_def by (auto simp add: pmf.map_comp o_def)
 
     define \<alpha> where "\<alpha> = (0.14 ::real)"
     then have \<alpha>: "\<alpha> > 0" by auto
 
     have indep:"prob_space.indep_vars
      (measure_pmf
        (prod_pmf {0..<t} (\<lambda>i. random_xors S (card S - 1))))
       (\<lambda>_. borel) (\<lambda>x xa. real (Xf x xa)) {0..<t}"
       unfolding Xf_def
       apply (intro indep_vars_restrict_intro')
       by (auto simp add: restrict_dfl_def)
 
     have d: "\<delta> \<in> {0<..<1}" using \<delta> by auto
 
     from approxcore_xors_eq[OF thresh_def a \<epsilon> S]
     have b1: "1 / 2 + \<alpha> \<le>
      measure_pmf.prob (random_xors S (card S - 1))
       {xors.
        real (approxcore_xors F S thresh xors)
        \<in> {real (card (proj S (sols F))) /
            (1 + \<epsilon>)..(1 + \<epsilon>) * real (card (proj S (sols F)))}}"
       unfolding \<alpha>_def by auto
     then have b2: "i < t \<Longrightarrow>
       1 / 2 + \<alpha> \<le>
       measure_pmf.prob
          (prod_pmf {0..<t}
            (\<lambda>i. random_xors S (card S - 1)))
          {\<omega> \<in> space
                 (measure_pmf
                   (prod_pmf {0..<t}
                     (\<lambda>i. random_xors S (card S - 1)))).
           real (Xf i \<omega>)
           \<in> {real (card (proj S (sols F))) /(1 + \<epsilon>)..
               (1 + \<epsilon>) *real (card (proj S (sols F)))}}" for i
     unfolding Xf_def apply clarsimp
     apply (subst prob_prod_pmf_slice)
     by auto
 
     have ***: "1 - \<delta>
       \<le> measure_pmf.prob (prod_pmf {0..<t} (\<lambda>i. random_xors S (card S - 1)))
       {\<omega>.
        median t (\<lambda>i. real (Xf i \<omega>))
        \<in> {real (card (proj S (sols F))) /
            (1 + \<epsilon>)..(1 + \<epsilon>) * real (card (proj S (sols F)))}}"
     proof -
       have "t = fix_t \<delta> \<or> t = n \<and> raw_median_bound \<alpha> n < \<delta>"
       unfolding t_def compute_t_def \<alpha>_def by auto
       moreover {
         assume "t = fix_t \<delta>"
         then have tb:"- ln \<delta> / (2 * \<alpha>\<^sup>2) \<le> real t"
         unfolding fix_t_def \<alpha>_def
         apply clarsimp
         by (metis assms(1) divide_minus_left inverse_eq_divide ln_inverse real_nat_ceiling_ge)
 
         from measure_pmf.median_bound_1[OF \<alpha> d indep tb]
         have ?thesis using b2 by auto
       }
       moreover {
         assume *: "t = n" "raw_median_bound \<alpha> n < \<delta>"
         have s: "1 / 2 - \<alpha> = 1 - (1 /2 + \<alpha>)"
           by auto
 
         have d1: "0 < t" using t1 by linarith
         have d2: "1 / 2 + \<alpha> \<ge> 0" using \<alpha> by auto
         have d3: "interval{x..y::real}" for x y
           unfolding interval_def by auto
 
         from prob_space.median_bound_raw[OF _ d1 d2 d3 indep b2]
         have "1 -
           measure_pmf.prob (binomial_pmf t (1 / 2 + \<alpha>)) {..t div 2}
           \<le> measure_pmf.prob
               (prod_pmf {0..<t}
                 (\<lambda>i. random_xors S (card S - 1)))
               {\<omega>.
                median t (\<lambda>i. real (Xf i \<omega>))
                \<in> {real (card (proj S (sols F))) /
                    (1 + \<epsilon>)..(1 + \<epsilon>) * real (card (proj S (sols F)))}}"
           by (auto simp add: prob_space_measure_pmf)
 
         moreover have "measure_pmf.prob (binomial_pmf t (1 / 2 + \<alpha>)) {..t div 2} \<le> \<delta>"
           by (smt (verit, ccfv_SIG) * b1 d2 measure_pmf.prob_le_1 prob_binomial_pmf_upto raw_median_bound_def s sum.cong)
 
         ultimately have ?thesis by auto
       }
       ultimately show ?thesis by auto
     qed
 
     have "measure_pmf.prob (approxmc F S \<epsilon> \<delta> n)
         {c. real c
             \<in> {real (card (proj S (sols F))) /
                 (1 + \<epsilon>)..(1 + \<epsilon>) * real (card (proj S (sols F)))}} =
       measure_pmf.prob (map_pmf (real \<circ> median t)
         (prod_pmf {0..<t}
          (\<lambda>i. approxmccore F S thresh)))
           {c. c \<in> {real (card (proj S (sols F))) /
                   (1 + \<epsilon>)..(1 + \<epsilon>) * real (card (proj S (sols F)))}}"
       using * by auto
     moreover have "... =
       measure_pmf.prob (map_pmf (real \<circ> median t)
       (map_pmf (\<lambda>f x. if x \<in> {0..<t} then f x else undefined) (Pi_pmf {0..<t} (approxcore_xors F S thresh undefined)
        (\<lambda>i. approxmccore F S thresh))))
       {c. c \<in> {real (card (proj S (sols F))) /
                 (1 + \<epsilon>)..(1 + \<epsilon>) * real (card (proj S (sols F)))}}"
       apply (subst Pi_pmf_default_swap)
       by auto
     moreover have "... =
       measure_pmf.prob (map_pmf (real \<circ> median t)
       (Pi_pmf {0..<t} (approxcore_xors F S thresh undefined)
        (\<lambda>i. approxmccore F S thresh)))
       {c. c \<in> {real (card (proj S (sols F))) /
                 (1 + \<epsilon>)..(1 + \<epsilon>) * real (card (proj S (sols F)))}}"
       by (clarsimp simp add: median_default[symmetric])
     moreover have "... \<ge> 1 - \<delta>"
       unfolding **
       using ***
       by auto
     ultimately have ?thesis by auto
   }
   ultimately show ?thesis by auto
 qed
 
 text \<open> To simplify further analyses, we can remove the (required) upper bound on epsilon. \<close>
 
 definition mk_eps :: "real \<Rightarrow> real"
   where "mk_eps \<epsilon> = (if \<epsilon> > 1 then 1 else \<epsilon>)"
 
 definition approxmc'::"
   'fml \<Rightarrow> 'a set \<Rightarrow>
   real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow> nat pmf"
   where "approxmc' F S \<epsilon> \<delta> n =
     approxmc F S (mk_eps \<epsilon>) \<delta> n"
 
 corollary approxmc'_sound:
   assumes \<delta>: "\<delta> > 0" "\<delta> < 1"
   assumes \<epsilon>: "\<epsilon> > 0"
   assumes S: "finite S"
   shows "prob_space.prob (approxmc' F S \<epsilon> \<delta> n)
       {c. real c \<in>
         {real (card (proj S (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj S (sols F)))}}
       \<ge> 1 - \<delta>"
 proof -
   define \<epsilon>' where "\<epsilon>' = (if \<epsilon> > 1 then 1 else \<epsilon>)"
   have \<epsilon>': "0 < \<epsilon>'" "\<epsilon>' \<le> 1"
     unfolding \<epsilon>'_def using \<epsilon> by auto
 
   from approxmc_sound[OF \<delta> \<epsilon>' S]
   have *: "prob_space.prob (approxmc F S \<epsilon>' \<delta> n)
       {c. real c \<in>
         {real (card (proj S (sols F))) / (1 + \<epsilon>')..
           (1 + \<epsilon>') * real (card (proj S (sols F)))}}
       \<ge> 1 - \<delta>" .
 
   have **: "
     {c. real c \<in>
         {real (card (proj S (sols F))) / (1 + \<epsilon>')..
           (1 + \<epsilon>') * real (card (proj S (sols F)))}}
     \<subseteq>
     {c. real c \<in>
         {real (card (proj S (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj S (sols F)))}}"
     unfolding \<epsilon>'_def
     apply clarsimp
     apply (rule conjI)
     apply (smt (verit) field_sum_of_halves frac_less2 zero_less_divide_iff)
     by (metis (no_types, opaque_lifting) add_le_cancel_left arith_special(3) dual_order.trans less_eq_real_def mult_right_mono of_nat_0_le_iff)
 
   show ?thesis
     apply (intro order.trans[OF *])
     unfolding approxmc'_def \<epsilon>'_def mk_eps_def
     apply (intro measure_pmf.finite_measure_mono)
     using **[unfolded  \<epsilon>'_def]
     by auto
 qed
 
 text \<open> This shows we can lift all randomness to the top-level (i.e., eagerly sample it). \<close>
 
 definition approxmc_map::"
   'fml \<Rightarrow> 'a set \<Rightarrow>
   real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow>
   (nat \<Rightarrow> nat \<Rightarrow> ('a set \<times> bool) option) \<Rightarrow>
   nat"
   where "approxmc_map F S \<epsilon> \<delta> n xorsFs = (
     let \<epsilon> = mk_eps \<epsilon> in
     let thresh = compute_thresh \<epsilon> in
     if card (proj S (sols F)) < thresh then
       card (proj S (sols F))
     else
       let t = compute_t \<delta> n in
       median t (approxcore_xors F S thresh \<circ> xorsFs))"
 
 lemma approxmc_map_eq:
   shows "
     map_pmf (approxmc_map F S \<epsilon> \<delta> n)
       (Pi_pmf {0..<compute_t \<delta> n} def
          (\<lambda>i. random_xors S (card S - 1))) =
     approxmc' F S \<epsilon> \<delta> n"
 proof -
   define def' where "def' = approxcore_xors F S (compute_thresh (mk_eps \<epsilon>)) def"
 
   have *: "
      map_pmf (median (compute_t \<delta> n))
      (prod_pmf {0..<compute_t \<delta> n}
        (\<lambda>i. map_pmf
               (approxcore_xors F S
                 (compute_thresh (mk_eps \<epsilon>)))
               (random_xors S (card S - Suc 0)))) =
      map_pmf (median (compute_t \<delta> n))
      (Pi_pmf {0..<compute_t \<delta> n} def'
        (\<lambda>i. map_pmf
               (approxcore_xors F S
                 (compute_thresh (mk_eps \<epsilon>)))
               (random_xors S (card S - Suc 0))))"
     apply (subst Pi_pmf_default_swap[symmetric, where dflt ="undefined", where dflt'="def'"])
     by (auto simp add: map_pmf_comp median_default[symmetric])
 
   show ?thesis
   unfolding approxmc'_def approxmc_map_def approxmc_def Let_def approxmccore_def
   using def'_def
   by (auto simp add: map_pmf_comp  Pi_pmf_map[of _ _ def] *)
 qed
 
 end
 
 end
diff --git a/thys/Approximate_Model_Counting/ApproxMCCoreAnalysis.thy b/thys/Approximate_Model_Counting/ApproxMCCoreAnalysis.thy
--- a/thys/Approximate_Model_Counting/ApproxMCCoreAnalysis.thy
+++ b/thys/Approximate_Model_Counting/ApproxMCCoreAnalysis.thy
@@ -1,1273 +1,1273 @@
 section \<open> ApproxMCCore analysis \<close>
 
 text \<open>
   This section analyzes ApproxMCCore with respect to a universal hash family.
   The proof follows Lemmas 1 and 2 from Chakraborty et al.~\cite{DBLP:conf/ijcai/ChakrabortyMV16}.
   \<close>
 theory ApproxMCCoreAnalysis imports
   ApproxMCCore
 begin
 
 (* Slicing after a family *)
 definition Hslice :: "nat \<Rightarrow>
   ('a assg \<Rightarrow> 'b \<Rightarrow> nat assg) \<Rightarrow> ('a assg \<Rightarrow> 'b \<Rightarrow> nat assg)"
   where "Hslice i H = (\<lambda>w s. aslice i (H w s))"
 
 context prob_space
 begin
 
 lemma indep_vars_prefix:
   assumes "indep_vars (\<lambda>_. count_space UNIV) H J"
   shows "indep_vars (\<lambda>_. count_space UNIV) (Hslice i H) J"
 proof -
   have "indep_vars (\<lambda>_. count_space UNIV) (\<lambda>y. (\<lambda>x. aslice i x) \<circ> H y) J"
     by (auto intro!: indep_vars_compose[OF assms(1)])
   thus ?thesis
     unfolding o_def Hslice_def
     by auto
 qed
 
 lemma assg_nonempty_dom:
   shows "
   (\<lambda>x. if x < i then Some True else None) \<in>
     {\<alpha>::nat assg. dom \<alpha> = {0..<i}}"
   by (auto split: if_splits)
 
 lemma card_dom_ran_nat_assg:
   shows "card {\<alpha>::nat assg. dom \<alpha> = {0..<n}} = 2^n"
 proof -
   have *: " {\<alpha>::nat assg. dom \<alpha> = {0..<n}} =
     {w. dom w = {0..<n} \<and> ran w \<subseteq> {True,False}}"
     by auto
   have "finite {0..<n}" by auto
   from card_dom_ran[OF this]
   have "card {w. dom w = {0..<n} \<and> ran w \<subseteq> {True,False}} =
     card {True,False} ^ card {0..<n}" .
   thus ?thesis
     unfolding *
     by (auto simp add: numeral_2_eq_2)
 qed
 
 lemma card_nat_assg_le:
   assumes "i \<le> n"
   shows "card {\<alpha>::nat assg. dom \<alpha> = {0..<n}} =
     2^(n-i) * card {\<alpha>::nat assg. dom \<alpha> = {0..<i}}"
   unfolding card_dom_ran_nat_assg
   by (metis assms le_add_diff_inverse mult.commute power_add)
 
 lemma empty_nat_assg_slice_notin:
   assumes "i \<le> n"
   assumes "dom \<beta> \<noteq> {0..<i}"
   shows"{\<alpha>::nat assg. dom \<alpha> = {0..<n} \<and> aslice i \<alpha> = \<beta>} = {}"
 proof (intro equals0I)
   fix x
   assume "x \<in> {\<alpha>. dom \<alpha> = {0..<n} \<and> aslice i \<alpha> = \<beta>}"
   then have "dom \<beta> = {0..<i}"
     unfolding aslice_def
     using assms(1) by force
   thus False using assms(2) by blast
 qed
 
 lemma restrict_map_dom:
   shows "\<alpha> |` dom \<alpha> = \<alpha>"
   unfolding restrict_map_def fun_eq_iff
   by (simp add: domIff)
 
 lemma aslice_refl:
   assumes "dom \<alpha> = {..<i}"
   shows "aslice i \<alpha> = \<alpha>"
   unfolding aslice_def assms[symmetric]
   using restrict_map_dom by auto
 
 lemma bij_betw_with_inverse:
   assumes "f ` A \<subseteq> B"
   assumes "\<And>x. x \<in> A \<Longrightarrow> g (f x) = x"
   assumes "g ` B \<subseteq> A"
   assumes "\<And>x. x \<in> B \<Longrightarrow> f (g x) = x"
   shows "bij_betw f A B"
 proof -
   have "inj_on f A"
     by (metis assms(2) inj_onI)
 
   thus ?thesis
     unfolding bij_betw_def
     using assms
     by (metis image_subset_iff subsetI subset_antisym)
 qed
 
 lemma card_nat_assg_slice:
   assumes "i \<le> n"
   assumes "dom \<beta> = {0..<i}"
   shows"card {\<alpha>::nat assg. dom \<alpha> = {0..<n} \<and> aslice i \<alpha> = \<beta>} =
     2 ^ (n-i)"
 proof -
   have "dom \<alpha> = {0..<i} \<and> aslice i \<alpha> = \<beta> \<longleftrightarrow> \<alpha> = \<beta>" for \<alpha>
     using aslice_refl
     by (metis assms(2) lessThan_atLeast0)
   then have r2:
     "{\<alpha>::nat assg. dom \<alpha> = {0..<i} \<and> aslice i \<alpha> = \<beta>} = {\<beta>}"
     by simp
 
   define f where "f =
     (\<lambda>(\<alpha>::nat assg,\<beta>::nat assg) j.
     if j < i then \<beta> j else \<alpha> (j-i))"
   let ?lhs = "({\<alpha>. dom \<alpha> = {0..<n - i}} \<times>
       {\<alpha>. dom \<alpha> = {0..<i} \<and> aslice i \<alpha> = \<beta>})"
   let ?rhs = "{\<alpha>::nat assg. dom \<alpha> = {0..<n} \<and> aslice i \<alpha> = \<beta>}"
 
   define finv where "finv =
     (\<lambda>fab::nat assg.
       ((\<lambda>j. fab (j + i)),
         fab |` {..<i})
     )"
   have 11: "\<And>x. dom (f x) = {j. if j < i then j \<in> dom (snd x) else j - i \<in> dom (fst x)}"
     unfolding f_def
       by (auto simp add: fun_eq_iff split: if_splits)
   have 1: " f ` ?lhs  \<subseteq> ?rhs"
   proof standard
     fix x
     assume x: "x \<in> f ` ({\<alpha>. dom \<alpha> = {0..<n - i}} \<times> {\<alpha>. dom \<alpha> = {0..<i} \<and> aslice i \<alpha> = \<beta>})"
     obtain a b where ab: "dom a = {0..<n - i}" "dom b = {0..<i}"
       "x = f (a,b)"
       using x by blast
     have 1: "dom x = {0..<n}"
       unfolding ab 11 using assms(1)
       by (auto simp add: ab)
     have 2: "aslice i x = \<beta>"
       using x unfolding f_def
       by (auto simp add: aslice_def restrict_map_def split: if_splits)
     show " x \<in> {\<alpha>. dom \<alpha> = {0..<n} \<and> aslice i \<alpha> = \<beta>}"
       using 1 2 by blast
   qed
 
   have " dom a = {0..<n - i} \<Longrightarrow>
        dom b = {0..<i} \<Longrightarrow>
        \<forall>x. aslice i b x = \<beta> x \<Longrightarrow>
-       \<not> x < i \<Longrightarrow> None = b x" for a b x
+       \<not> x < i \<Longrightarrow> None = b x" for a b :: "nat assg" and x
     by (metis atLeastLessThan_iff domIff)
   then have 2: "\<And>x. x \<in> ?lhs \<Longrightarrow> finv (f x) = x"
     unfolding finv_def f_def
     by (clarsimp simp add: fun_eq_iff restrict_map_def)
 
   have 31: "\<And>fab x y.
        dom fab = {0..<n} \<Longrightarrow>
        \<beta> = aslice i fab \<Longrightarrow>
        fab (x + i) = Some y \<Longrightarrow>
        x < n - i" 
     by (metis atLeastLessThan_iff domI less_diff_conv)
   also have "\<And>fab x.
        dom fab = {0..<n} \<Longrightarrow>
        \<beta> = aslice i fab \<Longrightarrow>
        x < i \<Longrightarrow> \<exists>y. fab x = Some y"
     by (metis assms(1) domD dual_order.trans lessThan_atLeast0 lessThan_iff linorder_not_less)
   ultimately have 3: "finv ` ?rhs \<subseteq> ?lhs"
     unfolding finv_def
     by (auto simp add: aslice_def split: if_splits)
 
   have 4: "\<And>x. x \<in> ?rhs \<Longrightarrow> f (finv x) = x"
     unfolding finv_def f_def
     by (auto simp add: fun_eq_iff restrict_map_def)
 
   have "bij_betw f ?lhs ?rhs"
     by (auto intro: bij_betw_with_inverse[OF 1 2 3 4])
 
   from bij_betw_same_card[OF this]
   have
   "card {\<alpha>::nat assg. dom \<alpha> = {0..<n} \<and> aslice i \<alpha> = \<beta>} =
    card ({\<alpha>::nat assg. dom \<alpha> = {0..<n-i}} \<times>
         {\<alpha>::nat assg. dom \<alpha> = {0..<i} \<and> aslice i \<alpha> = \<beta>})"
     by auto
   moreover have "... = 2^(n-i)"
     using r2 card_dom_ran_nat_assg
     by (simp add: card_cartesian_product)
 
   ultimately show ?thesis by auto
 qed
 
 lemma finite_dom:
   assumes "finite V"
   shows "finite {w :: 'a \<rightharpoonup> bool. dom w = V}"
 proof -
   have *: "{w :: 'a \<rightharpoonup> bool. dom w = V} =
     {w. dom w = V \<and> ran w \<subseteq> {True,False}}"
     by auto
   show ?thesis unfolding *
     apply (intro finite_set_of_finite_maps)
     using assms by auto
 qed
 
 (* TODO: generalizable to any finite output alphabet instead of just booleans *)
 lemma universal_prefix_family_from_hash:
   assumes M: "M = measure_pmf p"
   assumes kH: "k_universal k H D {\<alpha>::nat assg. dom \<alpha> = {0..<n}}"
   assumes i: "i \<le> n"
   shows "k_universal k (Hslice i H) D {\<alpha>. dom \<alpha> = {0..<i}}"
 proof -
   have "k_wise_indep_vars k (\<lambda>_. count_space UNIV) H D"
     using kH unfolding k_universal_def
     by auto
   then have 1: "k_wise_indep_vars k (\<lambda>_. count_space UNIV) (Hslice i H) D"
     unfolding k_wise_indep_vars_def
     using indep_vars_prefix
     by auto
 
   have fdom: "finite {\<alpha>::nat assg. dom \<alpha> = {0..<i}}"
     using measure_pmf.finite_dom by blast
   have nempty: "{\<alpha>::nat assg. dom \<alpha> = {0..<i}} \<noteq> {}"
     using assg_nonempty_dom
     by (metis empty_iff)
   have 2: "x \<in> D \<Longrightarrow>
     uniform_on (Hslice i H x) {\<alpha>. dom \<alpha> = {0..<i}}" for x
   proof -
     assume "x \<in> D"
     then have unif: "uniform_on (H x) {\<alpha>. dom \<alpha> = {0..<n}}"
       by (metis kH k_universal_def)
     show "uniform_on (Hslice i H x) {\<alpha>. dom \<alpha> = {0..<i}}"
     proof (intro uniform_onI[OF M fdom nempty])
       fix \<beta>
       have *: "{\<omega> \<in> space M. H x \<omega> \<in> {\<alpha>. aslice i \<alpha> = \<beta>}} =
         {\<omega>. Hslice i H x \<omega> = \<beta>}"
         unfolding Hslice_def
         by (auto simp add: M)
 
       have "{\<alpha>::nat assg. dom \<alpha> = {0..<n}} \<inter> {\<alpha>.  aslice i \<alpha> = \<beta>} =
         {\<alpha>::nat assg. dom \<alpha> = {0..<n} \<and> aslice i \<alpha> = \<beta>}"
         by auto
 
       then have "(card ({\<alpha>::nat assg. dom \<alpha> = {0..<n}} \<inter> {\<alpha>.  aslice i \<alpha> = \<beta>}))
         = (if dom \<beta> = {0..<i} then 2^(n-i) else 0)"
        using card_nat_assg_slice[OF i]
        by (simp add: empty_nat_assg_slice_notin i)
 
      then have **: "real (card ({\<alpha>::nat assg. dom \<alpha> = {0..<n}} \<inter> {\<alpha>.  aslice i \<alpha> = \<beta>}))
         = indicat_real {\<alpha>. dom \<alpha> = {0..<i}} \<beta>  * 2^(n-i)"
        by simp
 
       from uniform_onD[OF unif, of "{\<alpha>. aslice i \<alpha> = \<beta>}"]
       have "prob {\<omega>. Hslice i H x \<omega> = \<beta>} =
         real (card ({\<alpha>. dom \<alpha> = {0..<n}} \<inter> {\<alpha>. aslice i \<alpha> = \<beta>})) /
         real (card {\<alpha>::nat assg. dom \<alpha> = {0..<n}})"
         unfolding * by auto
       moreover have "... =
         indicat_real {\<alpha>. dom \<alpha> = {0..<i}} \<beta>  * 2^(n-i) /
         real (card {\<alpha>::nat assg. dom \<alpha> = {0..<n}})"
         unfolding ** by auto
       moreover have "... = indicat_real {\<alpha>. dom \<alpha> = {0..<i}} \<beta> * 2^(n-i) / 2^n"
         by (simp add: card_dom_ran_nat_assg)
       moreover have "... = indicat_real {\<alpha>. dom \<alpha> = {0..<i}} \<beta> / 2^i"
         by (simp add: i power_diff)
       moreover have "... =  indicat_real {\<alpha>. dom \<alpha> = {0..<i}} \<beta> / real ((2^i)::nat)" by auto
       moreover have "... =  indicat_real {\<alpha>. dom \<alpha> = {0..<i}} \<beta> / real (card {\<alpha>::nat assg. dom \<alpha> = {0..<i}})"
         using card_dom_ran_nat_assg
         by auto
       ultimately show "prob {\<omega>. Hslice i H x \<omega> = \<beta>} =
          indicat_real {\<alpha>. dom \<alpha> = {0..<i}} \<beta> /
          real (card {\<alpha>::nat assg. dom \<alpha> = {0..<i}})"
         by presburger
     qed
   qed
   show ?thesis
     unfolding k_universal_def
     using 1 2
     by blast
 qed
 
 end
 
 context ApproxMCCore
 begin
 
 definition pivot :: "real"
   where "pivot = 9.84 * ( 1 + 1 / \<epsilon> )^2"
 
 context
   assumes thresh: "thresh \<ge> (1 + \<epsilon> / (1 + \<epsilon>)) * pivot"
 begin
 
 lemma aux_1:
   assumes fin:"finite (set_pmf p)"
   assumes \<sigma>: "\<sigma> > 0"
   assumes exp: "\<mu> i = measure_pmf.expectation p Y"
   assumes var: "\<sigma>^2 = measure_pmf.variance p Y"
   assumes var_bound: "\<sigma>^2 \<le> \<mu> i"
   shows "
     measure_pmf.prob p {y. \<bar> Y y - \<mu> i \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * \<mu> i }
     \<le> (1 + \<epsilon>)^2 / (\<epsilon>^2 * \<mu> i) "
 proof -
   have pvar: "measure_pmf.variance p Y > 0"
     using var \<sigma>
     by (metis zero_less_power)
   have kmu: "\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>) > 0"
     using \<sigma> pvar var var_bound
     using \<epsilon> by auto
   have mupos: "\<mu> i > 0"
     using pvar var var_bound by linarith
   from spec_chebyshev_inequality [OF fin pvar kmu]
   have "measure_pmf.prob p
     {y. (Y y - measure_pmf.expectation p Y)^2 \<ge>
        (\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>))^2 * measure_pmf.variance p Y} \<le> 1 / (\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>))^2"
     by simp
   then have ineq1:"measure_pmf.prob p
     {y. (Y y - \<mu> i)^2 \<ge>
        (\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>))^2 * \<sigma>^2} \<le> 1 / (\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>))^2"
     using exp var by simp
   have "(\<lambda>y. (Y y - \<mu> i)^2 \<ge> (\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>))^2 * \<sigma>^2)
         = (\<lambda>y. (Y y - \<mu> i)^2 \<ge> (\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>) * \<sigma> )^2)"
     by (metis power_mult_distrib)
   moreover have "... = (\<lambda>y. \<bar> Y y - \<mu> i \<bar> \<ge> \<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>) * \<sigma>)"
   proof -
     have "0 \<le> \<epsilon> * \<mu> i / (1 + \<epsilon>)"
       by (simp add: \<epsilon> less_eq_real_def mupos zero_compare_simps(1))
     then show ?thesis
       apply clarsimp
       by (metis abs_le_square_iff abs_of_nonneg)
   qed
   moreover have "... = (\<lambda>y. \<bar> Y y - \<mu> i \<bar> \<ge> \<epsilon> * (\<mu> i) / (1 + \<epsilon>))"
     using \<sigma> by auto
   ultimately have simp1:"(\<lambda>y. (Y y - \<mu> i)^2 \<ge> (\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>))^2 * \<sigma>^2)
                   = (\<lambda>y. \<bar> Y y - \<mu> i \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * (\<mu> i))"
     by auto
 
   have "\<sigma>^2/(\<mu> i)^2 \<le> (\<mu> i)/(\<mu> i)^2"
     using var_bound \<mu>_gt_zero
     by (simp add: divide_right_mono)
   moreover have "... = 1 / (\<mu> i)"
     by (simp add: power2_eq_square)
   ultimately have simp2: "\<sigma>^2/(\<mu> i)^2 \<le> 1 / (\<mu> i)" by auto
 
   have "measure_pmf.prob p {y. \<bar> Y y - \<mu> i \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * (\<mu> i)}
         \<le> 1 / (\<epsilon> * (\<mu> i) / ((1 + \<epsilon>) * \<sigma>))^2"
     using ineq1 simp1
     by auto
   moreover have "... = (1 + \<epsilon>)^2 / \<epsilon>^2 * \<sigma>^2/(\<mu> i)^2"
     by (simp add: power_divide power_mult_distrib)
   moreover have "... \<le> (1 + \<epsilon>)^2 / \<epsilon>^2 * (1 / (\<mu> i))"
     using simp2
     by (smt (verit, best) \<epsilon> divide_pos_pos mult_left_mono times_divide_eq_right zero_less_power)
   ultimately have "measure_pmf.prob p {y. \<bar> Y y - \<mu> i \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * (\<mu> i)}
                     \<le> (1 + \<epsilon>)^2 / (\<epsilon>^2 * (\<mu> i))"
     by auto
   thus ?thesis by auto
 qed
 
 (* Lem 1.1 in IJCAI'16 paper *)
 lemma analysis_1_1:
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   assumes i: "i \<le> card S - 1"
   shows "
     measure_pmf.prob p
     {s. \<bar> card_slice ((\<lambda>w. H w s)) i - \<mu> i \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * \<mu> i}
     \<le> (1 + \<epsilon>)^2 / (\<epsilon>^2 * \<mu> i)"
 proof -
 
   (* The variance for i-th slice *)
   define var where "var =
       (\<lambda>i. measure_pmf.variance p
         (\<lambda>s. real (card (proj S W \<inter>
           {w. Hslice i H w s = aslice i \<alpha>}))))"
 
   from prob_space.universal_prefix_family_from_hash[OF _ _ ind]
   have hf: "prob_space.k_universal (measure_pmf p) 2
    (Hslice i H) {\<alpha>::'a assg. dom \<alpha> = S} {\<alpha>. dom \<alpha> = {0..<i}}"
     using prob_space_measure_pmf
     using i ind prob_space.universal_prefix_family_from_hash
     by blast
 
   have pSW: "proj S W \<subseteq> {\<alpha>. dom \<alpha> = S}"
     unfolding proj_def restr_def by (auto split:if_splits)
 
   have ain: "aslice i \<alpha> \<in> {\<alpha>. dom \<alpha> = {0..<i}}" using \<alpha>
     unfolding aslice_def using i by auto
 
   from k_universal_expectation_eq[OF p hf finite_proj_S pSW ain]
   have exp:"measure_pmf.expectation p
    (\<lambda>s. real (card (proj S W \<inter>
                      {w. Hslice i H w s = aslice i \<alpha>}))) =
     real (card (proj S W)) /
     real (card {\<alpha>::nat assg. dom \<alpha> = {0..<i}})" .
 
   have exp_mu:"real (card (proj S W)) /
     real (card {\<alpha>::nat assg. dom \<alpha> = {0..<i}}) = \<mu> i"
     unfolding \<mu>_def
     by (simp add: measure_pmf.card_dom_ran_nat_assg)
 
   have "proj S W \<inter>
                {w. Hslice i H w s = aslice i \<alpha>} =
     proj S W \<inter> {w. hslice i (\<lambda>w. H w s) w =  aslice i \<alpha>}" for s
     unfolding proj_def Hslice_def hslice_def
     by auto
   then have extend_card_slice:
     "\<And>s. (card (proj S W \<inter> {w. Hslice i H w s = aslice i \<alpha>})) =
     card_slice ((\<lambda>w. H w s)) i"
     unfolding card_slice_def by auto
 
   have mu_exp:" \<mu> i = measure_pmf.expectation p
    (\<lambda>s. real (card (proj S W \<inter> {w. Hslice i H w s = aslice i \<alpha>})))"
     using exp exp_mu by auto
 
   from two_universal_variance_bound[OF p hf finite_proj_S pSW ain]
   have "
     var i \<le>
     measure_pmf.expectation p
       (\<lambda>s. real (card (proj S W \<inter>
                         {w. Hslice i H w s = aslice i \<alpha>})))"
     unfolding var_def  .
   then have var_bound: "var i \<le> \<mu> i" using exp exp_mu
     by linarith
 
   have "var i \<ge> 0" unfolding var_def by auto
   then have "var i > 0 \<or>  var i = 0" by auto
   moreover {
     assume "var i = 0"
 
     then have 1: "
       measure_pmf.expectation p
         (\<lambda>s. (card_slice (\<lambda>w. H w s) i - \<mu> i)^2) = 0"
       unfolding var_def extend_card_slice mu_exp by auto
 
     have 2: "measure_pmf.expectation p
         (\<lambda>s. (card_slice (\<lambda>w. H w s) i - \<mu> i)^2) =
       sum (\<lambda>s. (card_slice (\<lambda>w. H w s) i - \<mu> i)^2 * pmf p s) (set_pmf p)"
       using assms by (auto intro!: integral_measure_pmf_real)
 
     have "\<forall>x \<in> set_pmf p. (card_slice (\<lambda>w. H w x) i - \<mu> i)^2 * pmf p x = 0"
       apply (subst sum_nonneg_eq_0_iff[symmetric])
       using 1 2 p by auto
     then have *: "\<And>x. x \<in> set_pmf p \<Longrightarrow> (card_slice (\<lambda>w. H w x) i - \<mu> i)^2 = 0"
       by (meson mult_eq_0_iff set_pmf_iff)
 
     have **: "(1 + \<epsilon>)^2 / (\<epsilon>^2 * \<mu> i) > 0"
       using \<mu>_gt_zero \<epsilon> by auto
     have "\<epsilon> / (1 + \<epsilon>) * \<mu> i > 0"
       using \<mu>_gt_zero \<epsilon> by auto
     then have "\<And>s. s \<in> set_pmf p \<Longrightarrow> \<bar> card_slice ((\<lambda>w. H w s)) i - \<mu> i \<bar> < \<epsilon> / (1 + \<epsilon>) * \<mu> i"
       using * by auto
     then have "
     measure_pmf.prob p
     {s. \<bar> card_slice ((\<lambda>w. H w s)) i - \<mu> i \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * \<mu> i } = 0"
       apply (subst measure_pmf_zero_iff)
       using linorder_not_less by auto
     then have "
     measure_pmf.prob p
       {s. \<bar> card_slice ((\<lambda>w. H w s)) i - \<mu> i \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * \<mu> i }
       \<le> (1 + \<epsilon>)^2 / (\<epsilon>^2 * \<mu> i)"
       using ** by auto
   }
   moreover {
     define sigma where "sigma = sqrt(var i)"
     assume "var i > 0"
 
     then have sigma_gt_0: "sigma > 0"
       unfolding sigma_def by simp
 
     have extend_sigma: "sigma^2 = measure_pmf.variance p
         (\<lambda>s. real (card (proj S W \<inter>
         {w. Hslice i H w s = aslice i \<alpha>})))"
       unfolding sigma_def var_def
       using less_eq_real_def local.var_def real_sqrt_pow2 sigma_def sigma_gt_0
       by fastforce
 
     have sigma_bound: "sigma^2 \<le> \<mu> i"
       using var_bound sigma_gt_0
       using sigma_def by force
 
     from aux_1[OF p sigma_gt_0 mu_exp extend_sigma sigma_bound]
     have "
       measure_pmf.prob p
       {s. \<bar> card_slice ((\<lambda>w. H w s)) i - \<mu> i \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * \<mu> i }
       \<le> (1 + \<epsilon>)^2 / (\<epsilon>^2 * \<mu> i)"
       using extend_card_slice by auto
   }
 
   ultimately show ?thesis by auto
 qed
 
 (* Lem 1.2 in IJCAI'16 paper *)
 lemma analysis_1_2:
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   assumes i: "i \<le> card S - 1"
   assumes \<beta>: "\<beta> \<le> 1"
   shows "measure_pmf.prob p
     {s. real(card_slice ((\<lambda>w. H w s)) i) \<le> \<beta> * \<mu> i }
     \<le> 1 / (1 + (1 - \<beta>)^2 * \<mu> i)"
 proof -
   have *: "(\<And>s. (0::real) \<le> card_slice ((\<lambda>w. H w s)) i)"
     by simp
   from spec_paley_zygmund_inequality[OF p * \<beta>]
   have paley_zigmund:
     "(measure_pmf.variance p (\<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) )
     + (1-\<beta>)^2 * (measure_pmf.expectation p (\<lambda>s. card_slice ((\<lambda>w. H w s)) i))^2) *
     measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) > \<beta> * measure_pmf.expectation p (\<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) )} \<ge>
     (1-\<beta>)^2 * (measure_pmf.expectation p (\<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) ))^2"
     by auto
   define var where "var = (\<lambda>i. measure_pmf.variance p
       (\<lambda>s. real (card (proj S W \<inter>
       {w. Hslice i H w s = aslice i \<alpha>}))))"
 
   from prob_space.universal_prefix_family_from_hash[OF _ _ ind]
   have hf: "prob_space.k_universal (measure_pmf p) 2
    (Hslice i H) {\<alpha>::'a assg. dom \<alpha> = S} {\<alpha>. dom \<alpha> = {0..<i}}"
     using prob_space_measure_pmf
     using i ind prob_space.universal_prefix_family_from_hash
     by blast
 
   have pSW: "proj S W \<subseteq> {\<alpha>. dom \<alpha> = S}"
     unfolding proj_def restr_def
     by (auto split:if_splits)
 
   have ain: "aslice i \<alpha> \<in> {\<alpha>. dom \<alpha> = {0..<i}}" using \<alpha>
     unfolding aslice_def using i by auto
 
   from k_universal_expectation_eq[OF p hf finite_proj_S pSW ain]
   have exp:"measure_pmf.expectation p
    (\<lambda>s. real (card (proj S W \<inter>
                      {w. Hslice i H w s = aslice i \<alpha>}))) =
     real (card (proj S W)) /
     real (card {\<alpha>::nat assg. dom \<alpha> = {0..<i}})" .
 
   have exp_mu:"real (card (proj S W)) /
     real (card {\<alpha>::nat assg. dom \<alpha> = {0..<i}}) = \<mu> i"
     unfolding \<mu>_def
     by (simp add: measure_pmf.card_dom_ran_nat_assg)
 
   have "proj S W \<inter>
                {w. Hslice i H w s = aslice i \<alpha>} =
     proj S W \<inter> {w. hslice i (\<lambda>w. H w s) w =  aslice i \<alpha>}" for s
     unfolding proj_def Hslice_def hslice_def
     by auto
 
   then have extend_card_slice:"\<And>s. (card (proj S W \<inter>
                      {w. Hslice i H w s = aslice i \<alpha>})) =
     card_slice ((\<lambda>w. H w s)) i"
     unfolding card_slice_def by auto
 
   have mu_exp:" \<mu> i = measure_pmf.expectation p
    (\<lambda>s. real (card (proj S W \<inter>
                      {w. Hslice i H w s = aslice i \<alpha>})))"
     using exp exp_mu by auto
 
   from two_universal_variance_bound[OF p hf finite_proj_S pSW ain]
   have "
     var i \<le>
     measure_pmf.expectation p
       (\<lambda>s. real (card (proj S W \<inter>
                         {w. Hslice i H w s = aslice i \<alpha>})))"
     unfolding var_def  .
   then have var_bound: "var i \<le> \<mu> i" using exp exp_mu
     by linarith
 
   have pos_mu: "\<mu> i > 0"
     unfolding \<mu>_def
     by (simp add: card_proj_witnesses)
 
   have comp: "measure_pmf.prob p
       {s. \<beta> * \<mu> i < real (card_slice (\<lambda>w. H w s) i)} =
     (1 - measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) \<le> \<beta> * \<mu> i})"
     apply (subst measure_pmf.prob_compl[symmetric])
     by (auto intro!: arg_cong[where f = "measure_pmf.prob p"])
 
   have extend_var_bound: "measure_pmf.variance p (\<lambda>s. card_slice ((\<lambda>w. H w s)) i) \<le> \<mu> i"
     using var_bound
     unfolding var_def
     by (simp add: extend_card_slice)
   then have
     "(measure_pmf.variance p (\<lambda>s. real(card_slice ((\<lambda>w. H w s)) i))
       + (1-\<beta>)^2 * (measure_pmf.expectation p (\<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) ) )^2)
       * measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) > \<beta> * measure_pmf.expectation p (\<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) )} \<le>
     (\<mu> i + (1-\<beta>)^2 * (measure_pmf.expectation p ( \<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) ) )^2)
     * measure_pmf.prob p
           {s. real(card_slice ((\<lambda>w. H w s)) i) > \<beta> * measure_pmf.expectation p (\<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) )}"
     by (auto intro!: mult_right_mono)
   moreover have
     "... \<le> (\<mu> i + (1-\<beta>)^2 * (measure_pmf.expectation p ( \<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) ) )^2)
     * measure_pmf.prob p
           {s. real(card_slice ((\<lambda>w. H w s)) i) > \<beta> * measure_pmf.expectation p (\<lambda>s. real(card_slice ((\<lambda>w. H w s)) i) )}"
     by fastforce
   ultimately have
     "(\<mu> i + (1-\<beta>)^2 * (\<mu> i)^2) * measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) > \<beta> * \<mu> i} \<ge> (1-\<beta>)^2 * (\<mu> i)^2"
     unfolding mu_exp extend_card_slice
     using paley_zigmund by linarith
   then have
     "(1 + (1-\<beta>)^2 * (\<mu> i)) * (\<mu> i) * measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) > \<beta> * \<mu> i} \<ge> (1-\<beta>)^2 * (\<mu> i) * (\<mu> i)"
     by (smt (verit) left_diff_distrib' more_arith_simps(11) mult_cancel_right mult_cancel_right2 power2_eq_square)
   then have
     "(1 + (1-\<beta>)^2 * (\<mu> i)) * measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) > \<beta> * \<mu> i} \<ge> (1-\<beta>)^2 * (\<mu> i)"
     using pos_mu by force
   then have
     "(1 + (1-\<beta>)^2 * (\<mu> i)) * (1 - measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) \<le> \<beta> * \<mu> i}) \<ge> (1-\<beta>)^2 * (\<mu> i)"
     using comp by auto
   then have
     "(1 + (1-\<beta>)^2 * (\<mu> i)) - (1 + (1-\<beta>)^2 * (\<mu> i)) * measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) \<le> \<beta> * \<mu> i} \<ge> (1-\<beta>)^2 * (\<mu> i)"
     by (simp add: right_diff_distrib)
   then have
     "(1 + (1-\<beta>)^2 * (\<mu> i)) * measure_pmf.prob p {s. real(card_slice ((\<lambda>w. H w s)) i) \<le> \<beta> * \<mu> i} \<le> 1"
     by simp
   thus ?thesis by (smt (verit, best) mult_nonneg_nonneg nonzero_mult_div_cancel_left pos_mu real_divide_pos_left zero_le_power2)
 qed
 
 lemma shift_\<mu>:
   assumes "k \<le> i"
   shows"\<mu> i * 2^k = \<mu> (i-k)"
   unfolding \<mu>_def
   by (auto simp add: assms power_diff)
 
 (* Lem 2.1 in IJCAI'16 paper *)
 lemma analysis_2_1:
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   assumes \<epsilon>_up: "\<epsilon> \<le> 1"
   shows "
     measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3))
       \<le> 1 / 62.5"
 proof -
   have "1 + 1 / \<epsilon> > 0"
     by (simp add: \<epsilon> pos_add_strict)
   then have pos_pivot: "pivot > 0"
     unfolding pivot_def
     by simp
 
   have "mstar \<ge> 4 \<or> mstar < 4" by auto
   moreover {
     assume "mstar < 4"
     then have " measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3))
       \<le> 1 / 62.5"
       by (auto simp add: T0_empty)
   }
   moreover {
     assume lo_mstar: "mstar \<ge> 4"
 
     have extend_mu3: "\<mu> (mstar-1) * 2^2 = \<mu> (mstar-3)"
       apply (subst shift_\<mu>)
       subgoal using lo_mstar by linarith
       using numeral_3_eq_3
       using Suc_1 diff_Suc_eq_diff_pred numeral_nat(7) by presburger
 
     have ******: "1 + \<epsilon> / (1 + \<epsilon>) \<le> 3 / 2"
       using \<epsilon> assms(3) by auto
     have mu_mstar_3_gt_zero: "\<mu> (mstar - 3) / 4 > 0"
       using \<mu>_gt_zero by simp
 
     from mstar_prop(1)
     have "thresh < \<mu> (mstar - 1) *2^2 / 4 * (1 + \<epsilon> / (1 + \<epsilon>))"
       by auto
     also have "... = \<mu> (mstar - 3) / 4 * (1 + \<epsilon> / (1 + \<epsilon>))"
       unfolding extend_mu3 by auto
     also have "... \<le> \<mu> (mstar - 3) / 4 * (3 / 2)"
       apply (intro mult_left_mono)
       using ****** mu_mstar_3_gt_zero by auto
     also have "... = 3 / 8 * \<mu> (mstar - 3)"
       by auto
     finally have thresh2mu: "thresh < 3 / 8 * \<mu> (mstar - 3)" .
 
     have "1 + \<epsilon> / (1 + \<epsilon>) > 0"
       by (simp add: add_nonneg_pos \<epsilon>)
     then have "\<mu> (mstar-1) > pivot" (* pivot = thresh / (1 + \<epsilon>/(1+\<epsilon>)) *)
       using mstar_prop(1) thresh
       by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
     then have lo_mu_mstar_3: "\<mu> (mstar-3) > 4*pivot"
       using extend_mu3
       by simp
 
     have mstar_3: "mstar-3 \<le> card S - 1"
       using lo_mstar
       using diff_le_self dual_order.trans mstar_prop(3) by blast
 
     have *: "(5 / 8)^2 = ((25 / 64)::real)"
       by (auto simp add: field_simps)
     have **: " 1 + 25/64 * 4*pivot \<le> 1+ 25 / 64 * \<mu> (mstar - 3) "
       using lo_mu_mstar_3
       by auto
 
     have "1 + 1/\<epsilon> \<ge> 2"
       by (simp add: \<epsilon> assms(3))
     then have "(1 + 1/\<epsilon>)^2 \<ge> 2^2"
       by (smt (verit) power_mono)
     then have ***: " 1 + 25/64 * 4 * 4*9.84 \<le> 1+ 25 / 64 * 4*pivot"
       unfolding pivot_def
       by auto
     have ****: "1 + 25/64 * 4 * 4*9.84 > (0::real)"
       by simp
 
     have "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 3)) \<le>
         3 / 8 * \<mu> (mstar - 3)}
       \<le> 1 / (1 + (1 - 3 / 8)\<^sup>2 * \<mu> (mstar - 3))"
       apply(intro analysis_1_2[OF p ind mstar_3])
       by auto
     also have "... = 1 / (1 + (5 / 8)^2 * \<mu> (mstar-3))"
       by simp
     also have "... = 1 / (1 + 25 / 64 * \<mu> (mstar-3))"
       unfolding * by auto
     also have "... \<le> 1 / (1+ 25/64 * 4*pivot)"
       using **
       by (metis Groups.add_ac(2) add_sign_intros(3) divide_nonneg_nonneg frac_le mult_right_mono mult_zero_left of_nat_0_le_iff of_nat_numeral order_le_less pos_pivot zero_less_one)
     also have "... \<le> 1 / (1+ 25/64 * 4 * 4*9.84)"
       using *** ****
       by (smt (verit) frac_le)
     also have "... \<le> 1 / 62.5"
       by simp
     finally have *****: "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 3)) \<le> 3 / 8 * \<mu> (mstar - 3)} \<le> 1 / 62.5"
       by auto
 
     have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3))
         = measure_pmf.prob p {s. real (card_slice (\<lambda>w. H w s) (mstar - 3)) < thresh}"
       unfolding T_def
       by auto
     also have "... \<le> measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 3)) \<le> 3 / 8 * \<mu> (mstar - 3)}"
       using thresh2mu by (auto intro!: measure_pmf.finite_measure_mono)
     also have "... \<le> 1 / 62.5"
       using *****
       by auto
     finally have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3)) \<le> 1 / 62.5" .
   }
 
   ultimately show ?thesis by auto
 qed
 
 (* Alternative Lem 2.1 in IJCAI'16 paper without bound on epsilon *)
 lemma analysis_2_1':
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   shows "
     measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3))
       \<le> 1 / 10.84"
 proof -
   have "1 + 1 / \<epsilon> > 0"
     by (simp add: \<epsilon> pos_add_strict)
   then have pos_pivot: "pivot > 0"
     unfolding pivot_def
     by simp
 
   have "mstar \<ge> 4 \<or> mstar < 4" by auto
   moreover {
     assume "mstar < 4"
     then have " measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3))
       \<le> 1 / 10.84"
       by (auto simp add: T0_empty)
   }
   moreover {
     assume lo_mstar: "mstar \<ge> 4"
 
     have extend_mu3: "\<mu> (mstar-1) * 2^2 = \<mu> (mstar-3)"
       apply (subst shift_\<mu>)
       subgoal using lo_mstar semiring_norm(87) by linarith
       using diff_Suc_eq_diff_pred eval_nat_numeral(3) by presburger
 
     have "\<epsilon> / (1 + \<epsilon>) < 1"
       using \<epsilon> by auto
     then have ******: "1 + \<epsilon> / (1 + \<epsilon>) < 2"
       using \<epsilon> by auto
     have mu_mstar_3_gt_zero: "\<mu> (mstar - 3) / 4 > 0"
       using \<mu>_gt_zero by simp
 
     from mstar_prop(1)
     have "thresh < \<mu> (mstar - 1) * (1 + \<epsilon> / (1 + \<epsilon>))"
       by auto
     also have "... = \<mu> (mstar - 1) *2^2 / 4 * (1 + \<epsilon> / (1 + \<epsilon>))"
       by auto
     also have "... = \<mu> (mstar - 3) / 4 * (1 + \<epsilon> / (1 + \<epsilon>))"
       unfolding extend_mu3 by auto
     also have "... < \<mu> (mstar - 3) / 4 * 2"
       apply (intro mult_strict_left_mono)
       using ****** mu_mstar_3_gt_zero by auto
     also have "... = 1 / 2 * \<mu> (mstar - 3)"
       by auto
     finally have thresh2mu: "thresh < 1 / 2 * \<mu> (mstar - 3)" .
 
     have "1 + \<epsilon> / (1 + \<epsilon>) > 0"
       by (simp add: add_nonneg_pos \<epsilon>)
     then have "\<mu> (mstar-1) * 4 > 4*pivot"
       using mstar_prop(1) thresh
       by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
     then have lo_mu_mstar_3: "\<mu> (mstar-3) > 4*pivot"
       using extend_mu3
       by simp
 
     have mstar_3: "mstar-3 \<le> card S - 1"
       using lo_mstar
       using diff_le_self dual_order.trans mstar_prop(3) by blast
 
     have *: "(1 / 2)^2 = ((1 / 4)::real)"
       by (auto simp add: field_simps)
     have **: " 1 + 1/4 * 4*pivot \<le> 1+ 1/4 * \<mu> (mstar - 3) "
       using lo_mu_mstar_3
       by auto
 
     have "(1 + 1/\<epsilon>)^2 > 1^2"
       by (simp add: \<epsilon>)
     then have ***: " 1 + 1/4 * 4*9.84 \<le> 1+ 1/4 * 4 *pivot"
       unfolding pivot_def by auto
     have ****: "1 + 1/4 * 4 * 9.84 > (0::real)"
       by simp
 
     have "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 3)) \<le>
         1 / 2 * \<mu> (mstar - 3)}
       \<le> 1 / (1 + (1 - 1 / 2)\<^sup>2 * \<mu> (mstar - 3))"
       apply(intro analysis_1_2[OF p ind mstar_3])
       by auto
     also have "... = 1 / (1 + 1 / 4 * \<mu> (mstar-3))"
       using * by force
     also have "... \<le> 1 / (1+ 1/4 * 4*pivot)"
       using **
       by (simp add: add_nonneg_pos frac_le pos_pivot)
     also have "... \<le> 1 / (1+ 1/4 * 4 *9.84)"
       using *** ****
       by (smt (verit) frac_le)
     also have "... \<le> 1 / 10.84"
       by simp
     finally have *****: "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 3)) \<le> 1/2 * \<mu> (mstar - 3)} \<le> 1 / 10.84" .
 
     have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3))
         = measure_pmf.prob p {s. real (card_slice (\<lambda>w. H w s) (mstar - 3)) < thresh}"
       unfolding T_def
       by auto
     also have "... \<le> measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 3)) \<le> 1 / 2 * \<mu> (mstar - 3)}"
       using thresh2mu by (auto intro!: measure_pmf.finite_measure_mono)
     also have "... \<le> 1 /  10.84"
       using *****
       by auto
     finally have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3)) \<le> 1 /  10.84" .
   }
 
   ultimately show ?thesis by auto
 qed
 
 (* Lem 2.2 in IJCAI'16 paper *)
 lemma analysis_2_2:
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   shows "
     measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-2)) \<le> 1 / 20.68"
 proof -
   have epos: "1 + 1 / \<epsilon> > 0"
     by (simp add: \<epsilon> pos_add_strict)
   then have pos_pivot: "pivot > 0"
     unfolding pivot_def
     by simp
 
   have "mstar \<ge> 3 \<or> mstar < 3" by auto
   moreover {
     assume "mstar < 3"
     then have " measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-2))
           \<le> 1 / 20.68"
       by (auto simp add: L0_empty)
   }
   moreover {
     assume lo_mstar: "mstar \<ge> 3"
 
     have extend_mu2: "\<mu> (mstar-1) * 2^1 = \<mu> (mstar-2)"
       apply (subst shift_\<mu>)
       subgoal using lo_mstar by linarith
       by (metis diff_diff_left one_add_one)
 
     have "1 + \<epsilon> / (1 + \<epsilon>) > 0"
       by (simp add: add_nonneg_pos \<epsilon>)
     then have "\<mu> (mstar-1) > pivot"
       using mstar_prop(1) thresh
       by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
     then have lo_mu_mstar_2: "\<mu> (mstar-2) > 2*pivot"
       using extend_mu2
       by simp
 
     have mstar_2: "mstar-2 \<le> card S - 1"
       using lo_mstar
       using diff_le_self dual_order.trans mstar_prop(3) by blast
 
     have beta:"1/(1+\<epsilon>) \<le> (1::real)"
       using \<epsilon> by auto
     have pos: "(1 / (1 + 1/\<epsilon>))\<^sup>2 > 0"
       using epos by auto
     then have *: "1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * 2*pivot \<le> 1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * \<mu> (mstar - 2)"
       using lo_mu_mstar_2
       by auto
 
     have "1 - 1/(1+\<epsilon>) = 1 / (1 + 1/\<epsilon>)"
       by (smt (verit, ccfv_threshold) \<epsilon> conjugate_exponent_def conjugate_exponent_real(1))
     then have **: "(1 - 1/(1+\<epsilon>))^2 = (1 / (1 + 1/\<epsilon>))^2"
       by simp
     have ***: "1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * 2 * 9.84 * ( 1 + 1/\<epsilon> )^2
             = 1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * ( 1 + 1/\<epsilon> )^2 *  2 * 9.84"
       by (simp add: mult.commute)
     have ****: "(1 / (1 + 1/\<epsilon>))\<^sup>2 * ( 1 + 1/\<epsilon> )^2 = 1"
       using pos
       by (simp add: power_one_over)
 
     from analysis_1_2[OF p ind mstar_2 beta]
     have "measure_pmf.prob p
       {s. real (card_slice (\<lambda>w. H w s) (mstar - 2)) \<le> 1/(1+\<epsilon>) * \<mu> (mstar - 2)}
         \<le> 1 / (1 + (1 - 1/(1+\<epsilon>))\<^sup>2 * \<mu> (mstar - 2))"
       by auto
     also have "... = 1 / (1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * \<mu> (mstar - 2))"
       unfolding ** by auto
     also have "... \<le> 1 / (1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * 2 * pivot)"
       using *
       by (smt (verit) epos divide_pos_pos frac_le pivot_def pos_prod_le zero_less_power)
     also have "... = 1 / (1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * 2 * 9.84 * ( 1 + 1/\<epsilon> )^2)"
       unfolding pivot_def by auto
     also have "... = 1 / 20.68"
       unfolding *** **** by auto
     finally have *****: "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 2)) \<le> 1/(1+\<epsilon>) * \<mu> (mstar - 2)} \<le> 1 / 20.68" .
 
     have "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 2)) < 1/(1+\<epsilon>) * \<mu> (mstar - 2)}
         \<le> measure_pmf.prob p {s. real (card_slice (\<lambda>w. H w s) (mstar - 2)) \<le> 1/(1+\<epsilon>) * \<mu> (mstar - 2)}"
       by (auto intro!: measure_pmf.finite_measure_mono)
     then have ******: "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 2)) < 1/(1+\<epsilon>) * \<mu> (mstar - 2)}
           \<le> 1 / 20.68"
       using ***** by auto
 
     have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-2))
         = measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 2)) < 1/(1+\<epsilon>) * \<mu> (mstar - 2)}"
       unfolding L_def
       by auto
     also have "... \<le> 1 / 20.68"
       using ****** by auto
     finally have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-2)) \<le> 1 / 20.68" .
   }
 
   ultimately show ?thesis by auto
 qed
 
 (* Lem 2.3 in IJCAI'16 paper *)
 lemma analysis_2_3:
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   shows "
     measure_pmf.prob
     (map_pmf (\<lambda>s w. H w s) p) (L (mstar-1)) \<le> 1 / 10.84"
 proof -
   have epos: "1 + 1 / \<epsilon> > 0"
     by (simp add: \<epsilon> pos_add_strict)
   then have pos_pivot: "pivot > 0"
     unfolding pivot_def
     by simp
 
   have "mstar \<ge> 2 \<or> mstar < 2" by auto
   moreover {
     assume "mstar < 2"
     then have " measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-2))
           \<le> 1 / 10.84"
       by (auto simp add: L0_empty)
   }
   moreover {
     assume lo_mstar: "mstar \<ge> 2"
 
     have "1 + \<epsilon> / (1 + \<epsilon>) > 0"
       by (simp add: add_nonneg_pos \<epsilon>)
     then have lo_mu_mstar_1: "\<mu> (mstar-1) > pivot"
       using mstar_prop(1) using thresh
       by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
 
     have mstar_1: "mstar-1 \<le> card S - 1"
       using lo_mstar diff_le_self dual_order.trans mstar_prop(3) by blast
 
     have beta: "1/(1+\<epsilon>) \<le> (1::real)"
       using \<epsilon> by auto
     have "(1 / (1 + 1/\<epsilon>))\<^sup>2 > 0"
       using epos by auto
     then have *: "1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * pivot \<le> 1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * \<mu> (mstar - 1)"
       using lo_mu_mstar_1
       by auto
 
     have "1 - 1/(1+\<epsilon>) = 1 / (1 + 1/\<epsilon>)"
       by (smt (verit, ccfv_threshold) \<epsilon> conjugate_exponent_def conjugate_exponent_real(1))
     then have **: "(1 - 1/(1+\<epsilon>))^2 = (1 / (1 + 1/\<epsilon>))^2"
       by simp
     have ***: "1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * 9.84 * ( 1 + 1/\<epsilon> )^2
             = 1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * ( 1 + 1/\<epsilon> )^2 * 9.84"
       by (simp add: mult.commute)
     have ****: "(1 / (1 + 1/\<epsilon>))\<^sup>2 * ( 1 + 1/\<epsilon> )^2 = 1"
       by (metis (mono_tags, opaque_lifting) \<open>0 < 1 + 1 / \<epsilon>\<close> div_by_1 divide_divide_eq_right divide_self_if less_irrefl mult.commute power_mult_distrib power_one)
 
     from analysis_1_2[OF p ind mstar_1 beta]
     have "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 1)) \<le> 1/(1+\<epsilon>) * \<mu> (mstar - 1)}
     \<le> 1 / (1 + (1 - 1/(1+\<epsilon>))\<^sup>2 * \<mu> (mstar - 1))"
       by auto
     moreover have "... = 1 / (1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * \<mu> (mstar - 1))"
       unfolding ** by auto
     moreover have "... \<le> 1 / (1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * pivot)"
       using *
       by (smt (verit) \<open>0 < (1 / (1 + 1 / \<epsilon>))\<^sup>2\<close> frac_le pos_pivot zero_le_mult_iff)
     moreover have "... = 1 / (1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * 9.84 * ( 1 + 1/\<epsilon> )^2)"
       unfolding pivot_def by auto
     moreover have "... = 1 / (1 + (1 / (1 + 1/\<epsilon>))\<^sup>2 * ( 1 + 1/\<epsilon> )^2 * 9.84)"
       unfolding *** by auto
     moreover have "... = 1 / (1 + 9.84)"
       unfolding **** by auto
     moreover have "... = 1 / 10.84"
       by auto
     ultimately have *****: "measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 1)) \<le> 1/(1+\<epsilon>) * \<mu> (mstar - 1)} \<le> 1 / 10.84"
       by linarith
     have "measure_pmf.prob p
       {s. real (card_slice (\<lambda>w. H w s) (mstar - 1)) < 1/(1+\<epsilon>) * \<mu> (mstar - 1)}
         \<le> measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 1)) \<le> 1/(1+\<epsilon>) * \<mu> (mstar - 1)}"
       by (auto intro!: measure_pmf.finite_measure_mono)
     then have ******: "measure_pmf.prob p
       {s. real (card_slice (\<lambda>w. H w s) (mstar - 1)) < 1/(1+\<epsilon>) * \<mu> (mstar - 1)}
           \<le> 1 / 10.84"
       using ***** by auto
 
     have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-1))
         = measure_pmf.prob p
      {s. real (card_slice (\<lambda>w. H w s) (mstar - 1)) < 1/(1+\<epsilon>) * \<mu> (mstar - 1)}"
       unfolding L_def
       by auto
     moreover have "... \<le> 1 / 10.84"
       using ****** by auto
     ultimately have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-1)) \<le> 1 / 10.84"
       by auto
   }
 
   ultimately show ?thesis by auto
 qed
 
 (* Lem 2.4 in IJCAI'16 paper *)
 lemma analysis_2_4:
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   shows "
     measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar) \<le> 1 / 4.92"
 proof -
   have "1 + 1 / \<epsilon> > 0"
     by (simp add: \<epsilon> pos_add_strict)
   then have pos_pivot: "pivot > 0"
     unfolding pivot_def
     by simp
 
   have "mstar \<ge> 1 \<or> mstar < 1" by auto
   moreover {
     assume "mstar < 1"
     have LU0_empty: "L mstar \<union> U mstar = {}"
       using L0_empty U0_empty
       using \<open>mstar < 1\<close> less_one by auto
     then have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar)
           \<le> 1 / 4.92"
       by auto
   }
   moreover {
     assume lo_mstar: "mstar \<ge> 1"
     have extend_mu: "\<mu> mstar * 2^1 = \<mu> (mstar-1)"
       using lo_mstar
       apply (subst shift_\<mu>)
       by auto
 
     have "1 + \<epsilon> / (1 + \<epsilon>) > 0"
       by (simp add: add_nonneg_pos \<epsilon>)
     then have "\<mu> (mstar-1) > pivot"
       using mstar_prop(1) thresh
       by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left)
     then have lo_mu_star: "\<mu> mstar > pivot / 2"
       using extend_mu
       by auto
 
     have mstar: "mstar \<le> card S - 1"
       using lo_mstar
       using diff_le_self dual_order.trans mstar_prop(3) by blast
 
     have "\<epsilon>*(1+1/\<epsilon>) = 1+\<epsilon>"
       by (smt (verit) \<epsilon> add_divide_eq_if_simps(1) divide_cancel_right divide_self_if nonzero_mult_div_cancel_left)
     then have *: "9.84 * \<epsilon>^2*(1+1/\<epsilon>)^2 / 2 = 9.84 * (1+\<epsilon>)^2 / 2"
       by (metis (mono_tags, opaque_lifting) more_arith_simps(11) power_mult_distrib)
 
     have "\<epsilon>^2 * \<mu> mstar \<ge> \<epsilon>^2 * pivot / 2"
       using lo_mu_star
       by (metis less_eq_real_def ordered_comm_semiring_class.comm_mult_left_mono times_divide_eq_right zero_le_power2)
     then have **: "\<epsilon>^2 * \<mu> mstar \<ge> 9.84 * (1+\<epsilon>)^2 / 2"
       unfolding pivot_def using * by auto
 
     from analysis_1_1[OF p ind mstar]
     have "measure_pmf.prob p
       {s. \<bar> card_slice ((\<lambda>w. H w s)) mstar - \<mu> mstar \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * \<mu> mstar }
           \<le> (1 + \<epsilon>)^2 / (\<epsilon>^2 * \<mu> mstar)"
       by auto
     also have "... \<le> (1 + \<epsilon>)^2 / (9.84 * (1+\<epsilon>)^2 / 2)"
       using **
       by (smt (verit) divide_cancel_left divide_le_0_iff frac_le pos_prod_le power2_less_0 zero_eq_power2)
     also have "... = (1 + \<epsilon>)^2 / (4.92 * (1+\<epsilon>)^2)"
       by simp
     also have "... = 1 / 4.92"
       using \<epsilon> by simp
     finally have *******: "measure_pmf.prob p
       {s. \<bar> card_slice ((\<lambda>w. H w s)) mstar - \<mu> mstar \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * \<mu> mstar }
           \<le> 1 / 4.92" .
 
     have "\<mu> mstar / (1 + \<epsilon>) - \<mu> mstar = \<mu> mstar * (1 / (1+\<epsilon>) - 1)"
       by (simp add: right_diff_distrib')
     also have "... = \<mu> mstar * (- \<epsilon> / (1+\<epsilon>))"
       by (smt (verit) \<epsilon> add_divide_distrib div_self minus_divide_left)
     finally have ***: "\<mu> mstar / (1 + \<epsilon>) - \<mu> mstar = \<mu> mstar * (- \<epsilon> / (1+\<epsilon>))" .
 
     have "{h. real (card_slice h mstar) \<le> \<mu> mstar / (1 + \<epsilon>)}
         = {h. real (card_slice h mstar) - \<mu> mstar \<le> \<mu> mstar / (1 + \<epsilon>) - \<mu> mstar}"
       by auto
     also have "... = {h. real (card_slice h mstar) - \<mu> mstar \<le> \<mu> mstar * (- \<epsilon> / (1+\<epsilon>))}"
       using *** by auto
     finally have ****: "
       {h. real (card_slice h mstar) \<le> \<mu> mstar / (1 + \<epsilon>)} =
       {h. real (card_slice h mstar) - \<mu> mstar \<le> \<mu> mstar * (- \<epsilon> / (1+\<epsilon>))}" .
 
     have "L mstar
             = {h. real (card_slice h mstar) < \<mu> mstar / (1 + \<epsilon>)}"
       unfolding L_def by auto
     also have "...\<subseteq> {h. real (card_slice h mstar) \<le> \<mu> mstar / (1 + \<epsilon>)}"
       by auto
     also have "... = {h. real (card_slice h mstar) - \<mu> mstar \<le> \<mu> mstar * (- \<epsilon> / (1+\<epsilon>))}"
       unfolding **** by auto
     finally have extend_L: "L mstar \<subseteq> {h. real (card_slice h mstar) - \<mu> mstar \<le> \<mu> mstar * (- \<epsilon> / (1+\<epsilon>))}" .
 
     have *****: "\<mu> mstar * (1 + \<epsilon> / (1+\<epsilon>)) - \<mu> mstar = \<mu> mstar * (\<epsilon> / (1+\<epsilon>))"
       by (metis (no_types, opaque_lifting) add.commute diff_add_cancel group_cancel.sub1 mult.right_neutral right_diff_distrib')
 
     have ******: "U mstar = {h. real (card_slice h mstar) \<ge> \<mu> mstar * (1 + \<epsilon> / (1+\<epsilon>))}"
       unfolding U_def by auto
     have "{h. real (card_slice h mstar) \<ge> \<mu> mstar * (1 + \<epsilon> / (1+\<epsilon>))}
           = {h. real (card_slice h mstar) - \<mu> mstar \<ge> \<mu> mstar * (1 + \<epsilon> / (1+\<epsilon>)) - \<mu> mstar}"
       by auto
     also have "... = {h. real (card_slice h mstar) - \<mu> mstar \<ge> \<mu> mstar * (\<epsilon> / (1+\<epsilon>))}"
       unfolding ***** by auto
     finally have extend_U: "U mstar = {h. real (card_slice h mstar) - \<mu> mstar \<ge> \<mu> mstar * (\<epsilon> / (1+\<epsilon>))}"
       using ****** by auto
 
     have "L mstar \<union> U mstar \<subseteq>
                     {h. real (card_slice h mstar) - \<mu> mstar \<le> \<mu> mstar * (- \<epsilon> / (1+\<epsilon>))}
                   \<union> {h. real (card_slice h mstar) - \<mu> mstar \<ge> \<mu> mstar * (\<epsilon> / (1+\<epsilon>))}"
       unfolding extend_U
       using extend_L
       by auto
     also have "... = {h. \<bar> real (card_slice h mstar) - \<mu> mstar \<bar> \<ge> \<mu> mstar * (\<epsilon> / (1+\<epsilon>))}"
       by auto
     finally have extend_LU: "L mstar \<union> U mstar \<subseteq> {h. \<bar> real (card_slice h mstar) - \<mu> mstar \<bar> \<ge> \<mu> mstar * (\<epsilon> / (1+\<epsilon>))}" .
 
     have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar)
         \<le> measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) {h. \<bar> real (card_slice h mstar) - \<mu> mstar \<bar> \<ge> \<mu> mstar * (\<epsilon> / (1+\<epsilon>))}"
       using extend_LU
       by (auto intro!: measure_pmf.finite_measure_mono)
     also have "... = measure_pmf.prob p
       {s. \<bar> real (card_slice (\<lambda>w. H w s) mstar) - \<mu> mstar \<bar> \<ge> \<epsilon> / (1 + \<epsilon>) * \<mu> mstar }"
       by (simp add: mult.commute)
     also have "... \<le> 1 / 4.92"
       using ******* by auto
     finally have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar) \<le> 1 / 4.92" .
   }
 
   ultimately show ?thesis by auto
 qed
 
 (* Lem 3 in IJCAI'16 paper *)
 lemma analysis_3:
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   assumes \<epsilon>_up: "\<epsilon> \<le> 1"
   shows "
     measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p)
     approxcore_fail \<le> 0.36"
 proof -
   have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) approxcore_fail
     \<le> measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p)
    (T (mstar-3) \<union>
     L (mstar-2) \<union>
     L (mstar-1) \<union>
     (L mstar \<union> U mstar))"
     using failure_bound
     by (auto intro!: measure_pmf.finite_measure_mono)
 
   moreover have "... \<le>
       measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3) \<union> L (mstar-2) \<union> L (mstar-1))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar)"
     by (auto intro!: measure_pmf.finite_measure_subadditive)
   moreover have "... \<le>
       measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3) \<union> L (mstar-2))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-1))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar)"
     by (auto intro!: measure_pmf.finite_measure_subadditive)
   moreover have "... \<le>
       measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-2))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-1))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar)"
     by (auto intro!: measure_pmf.finite_measure_subadditive)
   moreover have "... \<le> 1/62.5 + 1/20.68 + 1/10.84 + 1/4.92"
     using analysis_2_1[OF p ind \<epsilon>_up]
     using analysis_2_2[OF p ind]
     using analysis_2_3[OF p ind]
     using analysis_2_4[OF p ind]
     by auto
   ultimately show ?thesis by force
 qed
 
 (* Alternative Lem 3 in IJCAI'16 paper without bound on epsilon *)
 lemma analysis_3':
   assumes p: "finite (set_pmf p)"
   assumes ind: "prob_space.k_universal (measure_pmf p) 2 H
     {\<alpha>::'a assg. dom \<alpha> = S}
     {\<alpha>::nat assg. dom \<alpha> = {0..<card S - 1}}"
   shows "
     measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p)
     approxcore_fail \<le> 0.44"
 proof -
   have "measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) approxcore_fail
     \<le> measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p)
    (T (mstar-3) \<union>
     L (mstar-2) \<union>
     L (mstar-1) \<union>
     (L mstar \<union> U mstar))"
     using failure_bound
     by (auto intro!: measure_pmf.finite_measure_mono)
 
   moreover have "... \<le>
       measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3) \<union> L (mstar-2) \<union> L (mstar-1))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar)"
     by (auto intro!: measure_pmf.finite_measure_subadditive)
   moreover have "... \<le>
       measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3) \<union> L (mstar-2))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-1))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar)"
     by (auto intro!: measure_pmf.finite_measure_subadditive)
   moreover have "... \<le>
       measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (T (mstar-3))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-2))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L (mstar-1))
     + measure_pmf.prob (map_pmf (\<lambda>s w. H w s) p) (L mstar \<union> U mstar)"
     by (auto intro!: measure_pmf.finite_measure_subadditive)
   moreover have "... \<le> 1/10.84 + 1/20.68 + 1/10.84 + 1/4.92"
     using analysis_2_1'[OF p ind]
     using analysis_2_2[OF p ind]
     using analysis_2_3[OF p ind]
     using analysis_2_4[OF p ind]
     by auto
   ultimately show ?thesis by auto
 qed
 end
 
 end
 
 end
diff --git a/thys/Approximate_Model_Counting/CertCheck.thy b/thys/Approximate_Model_Counting/CertCheck.thy
--- a/thys/Approximate_Model_Counting/CertCheck.thy
+++ b/thys/Approximate_Model_Counting/CertCheck.thy
@@ -1,1159 +1,1159 @@
 section \<open> Certificate-based ApproxMC \<close>
 
 text \<open> This turns the randomized algorithm into an
   executable certificate checker \<close>
 
 theory CertCheck
 imports ApproxMCAnalysis
 
 begin
 
 subsection \<open> ApproxMC with lists instead of sets \<close>
 
 type_synonym 'a xor = "'a list \<times> bool"
 
 definition satisfies_xorL :: "'a xor \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   where "satisfies_xorL xb \<omega> =
     even (sum_list (map (of_bool \<circ> \<omega>) (fst xb)) +
       of_bool (snd xb)::nat)"
 
 (* Extract a sublist based on bits *)
 definition sublist_bits::"'a list \<Rightarrow> bool list \<Rightarrow> 'a list"
   where "sublist_bits ls bs =
     map fst (filter snd (zip ls bs))"
 
 definition xor_from_bits::
   "'a list \<Rightarrow> bool list \<times> bool \<Rightarrow> 'a xor"
   where "xor_from_bits V xsb =
     (sublist_bits V (fst xsb), snd xsb)"
 
 locale ApproxMCL =
   fixes sols :: "'fml \<Rightarrow> ('a \<Rightarrow> bool) set"
   fixes enc_xor :: "'a xor \<Rightarrow> 'fml \<Rightarrow> 'fml"
   assumes sols_enc_xor:
     "\<And>F xor.
       sols (enc_xor xor F) =
       sols F \<inter> {\<omega>. satisfies_xorL xor \<omega>}"
 begin
 
 definition list_of_set ::"'a set \<Rightarrow> 'a list"
 where "list_of_set x = (@ls. set ls = x \<and> distinct ls)"
 
 definition xor_conc :: "'a set \<times> bool \<Rightarrow> 'a xor"
   where "xor_conc xsb = (list_of_set (fst xsb), snd xsb)"
 
 definition enc_xor_conc :: "'a set \<times> bool \<Rightarrow> 'fml \<Rightarrow> 'fml"
   where "enc_xor_conc = enc_xor \<circ> xor_conc"
 
 lemma distinct_count_list:
   assumes "distinct ls"
   shows "count_list ls x = of_bool (x \<in> set ls)"
   using assms
   apply (induction ls)
   by auto
 
 lemma list_of_set:
   assumes "finite x"
   shows "distinct (list_of_set x)" "set (list_of_set x) = x"
   unfolding list_of_set_def
   by (metis (mono_tags, lifting) assms finite_distinct_list someI_ex)+
 
 lemma count_list_list_of_set:
   assumes "finite x"
   shows "count_list (list_of_set x) y = of_bool (y \<in> x)"
   apply (subst distinct_count_list)
   using list_of_set[OF assms]
   by auto
 
 lemma satisfies_xorL_xor_conc:
   assumes "finite x"
   shows"satisfies_xorL (xor_conc (x,b)) \<omega> \<longleftrightarrow> satisfies_xor (x,b) {x. \<omega> x}"
   unfolding satisfies_xorL_def xor_conc_def
   using list_of_set[OF assms]
   by (auto simp add: sum_list_map_eq_sum_count count_list_list_of_set[OF assms] Int_ac(3) assms)
 
 sublocale appmc: ApproxMC sols enc_xor_conc
   apply unfold_locales
   unfolding enc_xor_conc_def o_def
   apply (subst sols_enc_xor)
   using satisfies_xorL_xor_conc by fastforce
 
 definition size_xorL ::"
   'fml \<Rightarrow> 'a list \<Rightarrow>
   (nat \<Rightarrow> bool list \<times> bool) \<Rightarrow>
   nat \<Rightarrow> nat"
   where "size_xorL F S xorsl i = (
     let xors = map (xor_from_bits S \<circ> xorsl) [0..<i] in
     let Fenc = fold enc_xor xors F in
       card (proj (set S) (sols Fenc)))"
 
 definition check_xorL ::"
   'fml \<Rightarrow> 'a list \<Rightarrow>
   nat \<Rightarrow>
   (nat \<Rightarrow> bool list \<times> bool) \<Rightarrow>
   nat \<Rightarrow> bool"
   where "check_xorL F S thresh xorsl i =
   (size_xorL F S xorsl i < thresh)"
 
 definition approxcore_xorsL :: "
   'fml \<Rightarrow> 'a list \<Rightarrow>
   nat \<Rightarrow>
   (nat \<Rightarrow> (bool list \<times> bool)) \<Rightarrow>
   nat"
   where "
     approxcore_xorsL F S thresh xorsl =
     (case List.find
       (check_xorL F S thresh xorsl) [1..<length S] of
       None \<Rightarrow> 2 ^ length S
     | Some m \<Rightarrow>
       (2 ^ m * size_xorL F S xorsl m))"
 
 definition xor_abs :: "'a xor \<Rightarrow> 'a set \<times> bool"
   where "xor_abs xsb = (set (fst xsb), snd xsb)"
 
 lemma sols_fold_enc_xor:
   assumes "list_all2 (\<lambda>x y.
     \<forall>w. satisfies_xorL x w = satisfies_xorL y w) xs ys"
   assumes "sols F = sols G"
   shows "sols (fold enc_xor xs F) = sols (fold enc_xor ys G)"
   using assms
 proof (induction xs arbitrary: ys F G)
   case Nil
   then show ?case
     by auto
   next
   case (Cons x xss)
   then obtain y yss where ys: "ys = y#yss"
   by (meson list_all2_Cons1)
   have all2: "\<forall>w. satisfies_xorL x w = satisfies_xorL y w"
     using Cons.prems(1) ys by blast
   have *: "sols (enc_xor x F) = sols (enc_xor y G)"
     apply (subst sols_enc_xor)
     using all2 local.Cons(3) sols_enc_xor by presburger
   then show ?case unfolding ys
   using "*" Cons.IH Cons.prems(2) local.Cons(2) local.Cons(3) ys by auto
 qed
 
 lemma satisfies_xor_xor_abs:
   assumes "distinct x"
   shows"satisfies_xor (xor_abs (x,b)) {x. \<omega> x} \<longleftrightarrow> satisfies_xorL (x,b) \<omega>"
   unfolding satisfies_xorL_def xor_abs_def
   apply (clarsimp simp add: sum_list_map_eq_sum_count)
   by (smt (verit, ccfv_SIG) IntD1 Int_commute assms card_eq_sum distinct_count_list of_bool_eq(2) sum.cong)
 
 lemma xor_conc_xor_abs_rel:
   assumes "distinct (fst x)"
   shows"satisfies_xorL (xor_conc (xor_abs x)) w \<longleftrightarrow>
     satisfies_xorL x w"
   unfolding xor_abs_def
   apply (subst satisfies_xorL_xor_conc)
   subgoal by (simp add: xor_abs_def[symmetric])
   using assms satisfies_xor_xor_abs xor_abs_def by auto
 
 lemma sorted_sublist_bits:
   assumes "sorted V"
   shows"sorted (sublist_bits V bs)"
   unfolding sublist_bits_def
   using assms
   by (auto intro!: sorted_filter sorted_wrt_take simp add: map_fst_zip_take)
 
 lemma distinct_sublist_bits:
   assumes "distinct V"
   shows"distinct (sublist_bits V bs)"
   unfolding sublist_bits_def
   using assms
   by (auto intro!: distinct_map_filter simp add: map_fst_zip_take)
 
 lemma distinct_fst_xor_from_bits:
   assumes "distinct V"
   shows"distinct (fst (xor_from_bits V bs))"
   unfolding xor_from_bits_def
   using distinct_sublist_bits[OF assms]
   by auto
 
 lemma size_xorL:
   assumes "\<And>j. j < i \<Longrightarrow>
     xorsf j =
     Some (xor_abs (xor_from_bits S (xorsl j)))"
   assumes "distinct S"
   shows "size_xorL F S xorsl i =
     appmc.size_xor F (set S) xorsf i"
   unfolding appmc.size_xor_def size_xorL_def
   apply (clarsimp simp add: enc_xor_conc_def fold_map[symmetric])
   apply (intro arg_cong[where f = "(\<lambda>x. card (proj (set S) x))"])
   apply (intro sols_fold_enc_xor)
   by (auto simp add: list_all2_map1 list_all2_map2 list_all2_same assms(1) assms(2) distinct_fst_xor_from_bits xor_conc_xor_abs_rel)
 
 lemma fold_enc_xor_more:
   assumes "x \<in> sols (fold enc_xor (xs @ rev ys) F)"
   shows "x \<in> sols (fold enc_xor xs F)"
   using assms
 proof (induction ys arbitrary: F)
   case Nil
   then show ?case
     by auto
 next
   case ih: (Cons y ys)
   show ?case
     using ih by (auto simp add: ih.prems(1) sols_enc_xor)
 qed
 
 lemma size_xorL_anti_mono:
   assumes "x \<le> y" "distinct S"
   shows "size_xorL F S xorsl x \<ge> size_xorL F S xorsl y"
 proof -
   obtain ys where ys: "[0..<y] = [0..<x] @ ys" "distinct ys"
-  by (metis assms bot_nat_0.extremum distinct_upt ordered_cancel_comm_monoid_diff_class.add_diff_inverse upt_add_eq_append)
+  by (metis assms(1) bot_nat_0.extremum distinct_upt ordered_cancel_comm_monoid_diff_class.add_diff_inverse upt_add_eq_append)
 
   define rys where"rys = (rev (map (xor_from_bits S \<circ> xorsl) ys))"
   have *: "\<And>y. y \<in> set rys \<Longrightarrow> distinct (fst y)"
     unfolding rys_def
     using assms(2) distinct_fst_xor_from_bits
     by (metis (no_types, opaque_lifting) ex_map_conv o_apply set_rev)
 
   show ?thesis
     unfolding size_xorL_def Let_def
   apply (intro card_mono proj_mono)
   subgoal using card_proj(1) by blast
   unfolding ys
   by (metis fold_enc_xor_more map_append rev_rev_ident subsetI)
 qed
 
 lemma find_upto_SomeI:
   assumes "\<And>i. a \<le> i \<Longrightarrow> i < x \<Longrightarrow> \<not>P i"
   assumes "P x" "a \<le> x" "x < b"
   shows "find P [a..<b] = Some x"
 proof -
   have x: "[a..<b] ! (x-a) = x"
     by (simp add: assms(3) assms(4))
   have j: "\<And>j. j<x-a \<Longrightarrow> \<not> P ([a..<b] ! j)"
     using assms(1) assms(4) by auto
   show ?thesis
   unfolding find_Some_iff
   using x j
   by (metis assms(2) assms(3) assms(4) diff_less_mono length_upt)
 qed
 
 lemma check_xorL:
   assumes "\<And>j. j < i \<Longrightarrow>
     xorsf j =
     Some (xor_abs (xor_from_bits S (xorsl j)))"
   assumes "distinct S"
   shows "check_xorL F S thresh xorsl i =
     appmc.check_xor F (set S) thresh xorsf i"
   unfolding appmc.check_xor_def check_xorL_def
   using size_xorL[OF assms] by presburger
 
 lemma approxcore_xorsL:
   assumes "\<And>j. j < length S - 1  \<Longrightarrow>
     xorsf j =
     Some (xor_abs (xor_from_bits S (xorsl j)))"
   assumes S: "distinct S"
   shows "approxcore_xorsL F S thresh xorsl =
     appmc.approxcore_xors F (set S) thresh xorsf"
 proof -
   have c:"card (set S) = length S" using S
   by (simp add: distinct_card)
 
   have *: "find (check_xorL F S thresh xorsl) [1..<length S] =
    find (appmc.check_xor F (set S) thresh xorsf) [1..<card (set S)]"
     unfolding c
     by (auto intro!: find_cong check_xorL[OF assms(1) S])
 
   have **: "find (appmc.check_xor F
                   (set S) thresh xorsf)
             [Suc 0..<length S] =
            Some a \<Longrightarrow>
            j < a \<Longrightarrow>
            xorsf j =
            Some
             (xor_abs
               (xor_from_bits S
                 (xorsl j)))" for a j
     unfolding find_Some_iff
     by (auto simp add: assms(1))
   show ?thesis
   unfolding appmc.approxcore_xors_def approxcore_xorsL_def * c
   apply (cases "find (appmc.check_xor F (set S) thresh xorsf)
            [Suc 0..<length S]")
   subgoal by clarsimp
   by (auto intro!: ApproxMCL.size_xorL simp add: ApproxMCL_axioms assms **)
 qed
 
 definition approxmc_mapL::"
   'fml \<Rightarrow> 'a list \<Rightarrow>
   real \<Rightarrow> real \<Rightarrow> nat \<Rightarrow>
   (nat \<Rightarrow> nat \<Rightarrow> (bool list \<times> bool)) \<Rightarrow>
   nat"
   where "approxmc_mapL F S \<epsilon> \<delta> n xorsLs = (
     let \<epsilon> = appmc.mk_eps \<epsilon> in
     let thresh = appmc.compute_thresh \<epsilon> in
     if card (proj (set S) (sols F)) < thresh then
       card (proj (set S) (sols F))
     else
       let t = appmc.compute_t \<delta> n in
       median t (approxcore_xorsL F S thresh \<circ> xorsLs))"
 
 definition random_xorB :: "nat \<Rightarrow> (bool list \<times> bool) pmf"
   where "random_xorB n =
     pair_pmf
       (replicate_pmf n (bernoulli_pmf (1/2)))
       (bernoulli_pmf (1/2))"
 
 (* Actually, we can restrict i too *)
 lemma approxmc_mapL:
   assumes "\<And>i j. j < length S - 1 \<Longrightarrow>
     xorsFs i j =
     Some (xor_abs (xor_from_bits S (xorsLs i j)))"
   assumes S: "distinct S"
   shows "
     approxmc_mapL F S \<epsilon> \<delta> n xorsLs =
     appmc.approxmc_map F (set S) \<epsilon> \<delta> n xorsFs"
 proof -
   show ?thesis
     unfolding approxmc_mapL_def appmc.approxmc_map_def Let_def
     using assms by (auto intro!: median_cong approxcore_xorsL)
 qed
 
 lemma approxmc_mapL':
   assumes S: "distinct S"
   shows "
     approxmc_mapL F S \<epsilon> \<delta> n xorsLs =
     appmc.approxmc_map F (set S) \<epsilon> \<delta> n
       (\<lambda>i j. if j < length S - 1
          then Some (xor_abs (xor_from_bits S (xorsLs i j)))
          else None)"
   apply (intro approxmc_mapL)
   using assms by auto
 
 lemma bits_to_random_xor:
   assumes "distinct S"
   shows "map_pmf
     (\<lambda>x. xor_abs (xor_from_bits S x))
     (random_xorB (length S)) =
     random_xor (set S)"
 proof -
   have "xor_abs (xor_from_bits S (a,b)) = apfst (set \<circ> sublist_bits S) (a,b)" for a b
    using xor_abs_def by (auto simp add: xor_from_bits_def)
 
   then have *: "(\<lambda>x. xor_abs (xor_from_bits S x)) = apfst (set \<circ> sublist_bits S)"
     by auto
 
   have "\<And>x. x \<in> set S \<Longrightarrow>
          z x \<Longrightarrow>
          \<exists>b. (\<exists>n. S ! n = x \<and>
                   map z S ! n = b \<and>
                   n < length S) \<and> b" for z
     by (metis assms distinct_Ex1 nth_map)
 
   then have " set (map fst
                (filter snd
                  (zip S (map z S)))) =
          {x \<in> set S. Some (z x) = Some True}" for z
     by (auto elim: in_set_zipE simp add: in_set_zip image_def )
 
   then have **: "map_pmf (set \<circ> sublist_bits S)
        (replicate_pmf (length S) (bernoulli_pmf (1 / 2))) =
     map_pmf (\<lambda>b. {x \<in> set S. b x = Some True})
        (Pi_pmf (set S) (Some undefined)
          (\<lambda>_. map_pmf Some (bernoulli_pmf (1 / 2))))"
     apply (subst replicate_pmf_Pi_pmf[OF assms, where def = "undefined"])
     apply (subst Pi_pmf_map[of _  _ "undefined"])
     subgoal by (auto intro!: pmf.map_cong0 simp add: map_pmf_comp sublist_bits_def)
     subgoal by (meson set_zip_leftD)
     unfolding map_pmf_comp sublist_bits_def o_def
     by (auto intro!: pmf.map_cong0)
 
   show ?thesis
     unfolding random_xorB_def
     apply (subst random_xor_from_bits)
     by (auto simp add: * ** pair_map_pmf1[symmetric])
 qed
 
 lemma Pi_pmf_map_pmf_Some:
   assumes "finite S"
   shows "Pi_pmf S None (\<lambda>_. map_pmf Some p) =
     map_pmf (\<lambda>f v. if v \<in> S then Some (f v) else None)
     (Pi_pmf S def (\<lambda>_. p))"
 proof -
   have *: "Pi_pmf S None (\<lambda>_. map_pmf Some p) =
     map_pmf (\<lambda>f x. if x \<in> S then f x else None)
     (Pi_pmf S (Some def) (\<lambda>_. map_pmf Some p))"
     apply (subst Pi_pmf_default_swap[OF assms])
       by auto
 
   show ?thesis unfolding *
     apply (subst Pi_pmf_map[OF assms, of  _ def])
     subgoal by simp
     apply (simp add: map_pmf_comp o_def )
     by (metis comp_eq_dest_lhs)
 qed
 
 lemma bits_to_random_xors:
   assumes "distinct S"
   shows "
     map_pmf
     (\<lambda>f j.
       if j < n
       then Some (xor_abs (xor_from_bits S (f j)))
       else None)
     (Pi_pmf {..<(n::nat)} def (\<lambda>_. random_xorB (length S))) =
     random_xors (set S) n"
   unfolding random_xors_def
   apply (subst Pi_pmf_map_pmf_Some)
   subgoal using assms by simp
   apply (subst bits_to_random_xor[symmetric, OF assms])
   apply (subst Pi_pmf_map[where dflt = "def", where dflt'="xor_abs (xor_from_bits S def)"])
   subgoal by simp
   subgoal by simp
   apply (clarsimp simp add: map_pmf_comp o_def)
   by (metis o_apply)
 
 lemma bits_to_all_random_xors:
   assumes "distinct S"
   assumes "(\<lambda>j. if j < n
           then Some (xor_abs (xor_from_bits S (def1 j)))
           else None) = def"
   shows "
     map_pmf
     ((\<circ>) (\<lambda>f j. if j < n
                  then Some (xor_abs (xor_from_bits S (f j)))
                  else None))
     (Pi_pmf {0..<(m::nat)} def1
       (\<lambda>_.
         Pi_pmf {..<(n::nat)} def2 (\<lambda>_. random_xorB (length S)))) =
     Pi_pmf {0..<m} def
          (\<lambda>i. random_xors (set S) n)"
   apply (subst bits_to_random_xors[symmetric, OF assms(1), of _ "def2"])
   apply (subst Pi_pmf_map[OF _])
   using assms(2) by auto
 
 (* Sample t * (l-1) * l XORs *)
 definition random_seed_xors::"nat \<Rightarrow> nat \<Rightarrow> (nat \<Rightarrow> nat \<Rightarrow> bool list \<times> bool) pmf"
   where "random_seed_xors t l =
     (prod_pmf {0..<t}
       (\<lambda>_. prod_pmf {..<l-1} (\<lambda>_. random_xorB l)))"
 
 lemma approxmcL_sound:
   assumes \<delta>: "\<delta> > 0" "\<delta> < 1"
   assumes \<epsilon>: "\<epsilon> > 0"
   assumes S: "distinct S"
   shows "
     prob_space.prob
       (map_pmf (approxmc_mapL F S \<epsilon> \<delta> n)
         (random_seed_xors (appmc.compute_t \<delta> n) (length S)))
       {c. real c \<in>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}}
       \<ge> 1 - \<delta>"
 proof -
   define def where "def =
       (\<lambda>j. if j < degree S
           then Some (xor_abs (xor_from_bits S (undefined j)))
           else None)"
   have *: "(map_pmf (approxmc_mapL F S \<epsilon> \<delta> n)
         (Pi_pmf {0..<appmc.compute_t \<delta> n} undefined
            (\<lambda>_. Pi_pmf {..<length S - 1} undefined
             (\<lambda>_. random_xorB (length S))))) =
      (map_pmf (appmc.approxmc_map F (set S) \<epsilon> \<delta> n)
       (map_pmf ((\<circ>) (\<lambda>f.
           (\<lambda>j. if j < length S - 1
                  then Some (xor_abs (xor_from_bits S (f j)))
                  else None)))
        (Pi_pmf {0..<appmc.compute_t \<delta> n} undefined
          (\<lambda>_. Pi_pmf {..<length S - 1} undefined
                 (\<lambda>_. random_xorB (length S))))))"
     unfolding approxmc_mapL'[OF S]
     by (simp add: map_pmf_comp o_def)
   have **: "
     (map_pmf (approxmc_mapL F S \<epsilon> \<delta> n)
         (Pi_pmf {0..<appmc.compute_t \<delta> n} undefined
            (\<lambda>_. Pi_pmf {..<length S - 1} undefined
             (\<lambda>_. random_xorB (length S))))) =
     map_pmf (appmc.approxmc_map F (set S) \<epsilon> \<delta> n)
      (Pi_pmf {0..<appmc.compute_t \<delta> n} def
        (\<lambda>i. random_xors (set S) (card (set S) - 1)))"
     unfolding *
     apply (subst bits_to_all_random_xors[OF S])
     using def_def
     by (auto simp add: assms(4) distinct_card)
   show ?thesis
     unfolding ** appmc.approxmc_map_eq random_seed_xors_def
     using \<delta>(2) \<epsilon> appmc.approxmc'_sound assms(1) by blast
 qed
 
 (* This is more convenient for stating what happens when
   certification returns the "wrong" result *)
 lemma approxmcL_sound':
   assumes \<delta>: "\<delta> > 0" "\<delta> < 1"
   assumes \<epsilon>: "\<epsilon> > 0"
   assumes S: "distinct S"
   shows "
     prob_space.prob
       (map_pmf (approxmc_mapL F S \<epsilon> \<delta> n)
         (random_seed_xors (appmc.compute_t \<delta> n) (length S)))
       {c. real c \<notin>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}} \<le> \<delta>"
 proof -
   have "prob_space.prob
       (map_pmf (approxmc_mapL F S \<epsilon> \<delta> n)
         (Pi_pmf {0..<appmc.compute_t \<delta> n} undefined
            (\<lambda>_. Pi_pmf {..<length S - 1} undefined
             (\<lambda>_. random_xorB (length S)))))
       {c. real c \<notin>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}} =
     1 - prob_space.prob
       (map_pmf (approxmc_mapL F S \<epsilon> \<delta> n)
         (Pi_pmf {0..<appmc.compute_t \<delta> n} undefined
            (\<lambda>_. Pi_pmf {..<length S - 1} undefined
             (\<lambda>_. random_xorB (length S)))))
       {c. real c \<in>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}}"
     apply (subst measure_pmf.prob_compl[symmetric])
     by (auto simp add: vimage_def)
   thus ?thesis using approxmcL_sound[OF assms, of "F" "n"] \<delta>
     unfolding random_seed_xors_def
     by linarith
 qed
 
 end
 
 subsection \<open> ApproxMC certificate checker \<close>
 
 (* Helper functions *)
 definition str_of_bool :: "bool \<Rightarrow> String.literal"
   where "str_of_bool b = (
   if b then STR ''true'' else STR ''false'')"
 
 fun str_of_nat_aux :: "nat \<Rightarrow> char list \<Rightarrow> char list"
   where "str_of_nat_aux n acc = (
   let c = char_of_integer (of_nat (48 + n mod 10)) in
   if n < 10 then c # acc
   else str_of_nat_aux (n div 10) (c # acc))"
 
 definition str_of_nat :: "nat \<Rightarrow> String.literal"
   where "str_of_nat n = String.implode (str_of_nat_aux n [])"
 
 type_synonym 'a sol = "('a \<times> bool) list"
 
 (* The canonical assignment specified by a list *)
 definition canon_map_of :: "('a \<times> bool) list \<Rightarrow> ('a \<Rightarrow> bool)"
   where "canon_map_of ls =
     (let m = map_of ls in
     (\<lambda>x. case m x of None \<Rightarrow> False | Some b \<Rightarrow> b))"
 
 (* The canonical assignment specified by a list *)
 lemma canon_map_of[code]:
   shows "canon_map_of ls =
     (let m = Mapping.of_alist ls in
      Mapping.lookup_default False m)"
   unfolding canon_map_of_def lookup_default_def
   by (auto simp add: lookup_of_alist)
 
 definition proj_sol :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool list"
   where "proj_sol S w = map w S"
 
 text \<open> The following extended locale assumes
   additional support for syntactically working with solutions \<close>
 locale CertCheck = ApproxMCL sols enc_xor
   for sols :: "'fml \<Rightarrow> ('a \<Rightarrow> bool) set"
   and enc_xor :: "'a list \<times> bool \<Rightarrow> 'fml \<Rightarrow> 'fml" +
   fixes check_sol :: "'fml \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
   fixes ban_sol :: "'a sol \<Rightarrow> 'fml \<Rightarrow> 'fml"
   assumes sols_ban_sol:
     "\<And>F vs.
       sols (ban_sol vs F) =
       sols F \<inter> {\<omega>. map \<omega> (map fst vs) \<noteq> map snd vs}"
   assumes check_sol:
     "\<And>F w. check_sol F w \<longleftrightarrow> w \<in> sols F"
 begin
 
 text \<open> Assuming parameter access to an UNSAT checking oracle \<close>
 context
   fixes check_unsat :: "'fml \<Rightarrow> bool"
 begin
 
 text \<open> Throughout this checker, INL indicates error, INR indicates success \<close>
 
 definition check_BSAT_sols::"
   'fml \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> bool) list \<Rightarrow> String.literal + unit"
 where "check_BSAT_sols F S thresh cms = (
   let ps = map (proj_sol S) cms in
   let b1 = list_all (check_sol F) cms in
   let b2 = distinct ps in
   let b3 =
     (length cms < thresh \<longrightarrow>
       check_unsat (fold ban_sol (map (zip S) ps) F)) in
     if b1 \<and> b2 \<and> b3 then Inr ()
     else Inl (STR  ''checks ---'' +
       STR '' all valid sols: '' + str_of_bool b1 +
       STR '', all distinct sols: '' + str_of_bool b2 +
       STR '', unsat check (< thresh sols): '' + str_of_bool b3)
   )"
 
 definition BSAT ::"
   'fml \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> ('a \<Rightarrow> bool) list \<Rightarrow> String.literal + nat"
 where "BSAT F S thresh xs = (
   case check_BSAT_sols F S thresh xs of
     Inl err \<Rightarrow> Inl err
   | Inr _ \<Rightarrow> Inr (length xs)
 )"
 
 (* A size certificate is simply a list of solutions*)
 definition size_xorL_cert :: "
   'fml \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow>
   (nat \<Rightarrow> (bool list \<times> bool)) \<Rightarrow> nat \<Rightarrow>
   (('a \<Rightarrow> bool) list) \<Rightarrow> String.literal + nat"
   where "size_xorL_cert F S thresh xorsl i xs = (
     let xors = map (xor_from_bits S \<circ> xorsl) [0..<i]  in
     let Fenc = fold enc_xor xors F in
     BSAT Fenc S thresh xs
   )"
 
 (* Checks whether the value of m is an appropriate value
   Especially in the case where 1 \<le> m \<le> |S|-1 *)
 fun approxcore_xorsL_cert :: "
   'fml \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow>
   nat \<times> ('a \<Rightarrow> bool) list \<times> ('a \<Rightarrow> bool) list \<Rightarrow>
   (nat \<Rightarrow> (bool list \<times> bool))
   \<Rightarrow> String.literal + nat"
 where "approxcore_xorsL_cert F S thresh (m,cert1,cert2) xorsl = (
   if 1 \<le> m \<and> m \<le> length S
   then
     case size_xorL_cert F S thresh xorsl (m-1) cert1 of
       Inl err \<Rightarrow> Inl (STR ''cert1 '' + err)
     | Inr n \<Rightarrow>
     if n \<ge> thresh
     then
       if m = length S
       then Inr (2 ^ length S)
       else
         case size_xorL_cert F S thresh xorsl m cert2 of
           Inl err \<Rightarrow> Inl (STR ''cert2 '' + err)
         | Inr c \<Rightarrow>
           if c < thresh then Inr (2 ^ m * c)
           else Inl (STR ''too many solutions at m added XORs'')
     else Inl (STR ''too few solutions at m-1 added XORs'')
   else
      Inl (STR ''invalid value of m, need 1 <= m <= |S|''))"
 
 (* Compute the correct choice of n up to a bound arbitrarily set to 256 for now *)
 definition find_t :: "real \<Rightarrow> nat"
 where "find_t \<delta> = (
   case find (\<lambda>i. appmc.raw_median_bound 0.14 i < \<delta>) [0..<256] of
     Some m \<Rightarrow> m
   | None \<Rightarrow> appmc.fix_t \<delta>
   )"
 
 fun fold_approxcore_xorsL_cert:: "
   'fml \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow>
   nat \<Rightarrow> nat \<Rightarrow>
   (nat \<Rightarrow> (nat \<times> ('a \<Rightarrow> bool) list \<times> ('a \<Rightarrow> bool) list)) \<Rightarrow>
   (nat \<Rightarrow> nat \<Rightarrow> (bool list \<times> bool))
   \<Rightarrow> String.literal + (nat list)"
   where
   "fold_approxcore_xorsL_cert F S thresh t 0 cs xorsLs = Inr []"
 | "fold_approxcore_xorsL_cert F S thresh t (Suc i) cs xorsLs = (
     let it = t - Suc i in
     case approxcore_xorsL_cert F S thresh (cs it) (xorsLs it) of
       Inl err \<Rightarrow> Inl (STR ''round '' + str_of_nat it + STR '' '' + err)
     | Inr n \<Rightarrow>
       (case fold_approxcore_xorsL_cert F S thresh t i cs xorsLs of
           Inl err \<Rightarrow> Inl err
         | Inr ns \<Rightarrow> Inr (n # ns)))"
 
 definition calc_median::"
   'fml \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow>
   (nat \<Rightarrow> (nat \<times> ('a \<Rightarrow> bool) list \<times> ('a \<Rightarrow> bool) list)) \<Rightarrow>
   (nat \<Rightarrow> nat \<Rightarrow> (bool list \<times> bool)) \<Rightarrow>
   String.literal + nat"
   where "calc_median F S thresh t ms xorsLs = (
       case fold_approxcore_xorsL_cert F S thresh t t ms xorsLs of
         Inl err \<Rightarrow> Inl err
       | Inr ls \<Rightarrow> Inr (sort ls ! (t div 2))
   )"
 
 fun certcheck::"
   'fml \<Rightarrow> 'a list \<Rightarrow>
   real \<Rightarrow> real \<Rightarrow>
   (('a \<Rightarrow> bool) list \<times>
   (nat \<Rightarrow> (nat \<times> ('a \<Rightarrow> bool) list \<times> ('a \<Rightarrow> bool) list))) \<Rightarrow>
   (nat \<Rightarrow> nat \<Rightarrow> (bool list \<times> bool)) \<Rightarrow>
   String.literal + nat"
   where "certcheck F S \<epsilon> \<delta> (m0,ms) xorsLs = (
     let \<epsilon> = appmc.mk_eps \<epsilon> in
     let thresh = appmc.compute_thresh \<epsilon> in
     case BSAT F S thresh m0 of Inl err \<Rightarrow> Inl err
     | Inr Y \<Rightarrow>
     if Y < thresh then Inr Y
     else
       let t = find_t \<delta> in
       calc_median F S thresh t ms xorsLs)"
 
 (* The correctness property for BSAT oracle calls that
    will be certified externally through proof logging *)
 context
   assumes check_unsat: "\<And>F. check_unsat F \<Longrightarrow> sols F = {}"
 begin
 
 lemma sols_fold_ban_sol:
   shows"sols (fold ban_sol ls F) =
   sols F \<inter> {\<omega>. (\<forall>vs \<in> set ls. map \<omega> (map fst vs) \<noteq> map snd vs)}"
 proof (induction ls arbitrary: F)
   case Nil
   then show ?case by auto
 next
   case (Cons vs ls)
   show ?case
     using Cons(1) sols_ban_sol
     by auto
 qed
 
 lemma inter_cong_right:
   assumes "\<And>x. x \<in> A \<Longrightarrow> x \<in> B \<longleftrightarrow> x \<in> C"
   shows "A \<inter> B = A \<inter> C"
   using assms by auto
 
 lemma proj_sol_canon_map_of:
   assumes "distinct S" "length S = length w"
   shows "proj_sol S (canon_map_of (zip S w)) = w"
   using assms
   unfolding proj_sol_def canon_map_of_def
 proof (induction w arbitrary: S)
   case Nil
   then show ?case
     by auto
 next
   case (Cons a w)
   obtain s ss where ss: "S = s # ss"
     by (metis Cons.prems(2) Suc_le_length_iff order.refl)
   then show ?case
     apply clarsimp
     by (smt (z3) Cons.IH Cons.prems(2) add.right_neutral add_Suc_right distinct.simps(2) list.size(4) local.Cons(2) map_eq_conv nat.inject)
 qed
 
 lemma proj_sol_cong:
   assumes "restr (set S) A = restr (set S) B"
   shows "proj_sol S A = proj_sol S B"
   using assms
   unfolding proj_sol_def restr_def map_eq_conv
   by (metis option.simps(1))
 
 lemma canon_map_of_map_of:
   assumes "length S = length x"
   assumes "canon_map_of (zip S x) \<in> A"
   shows "map_of (zip S x) \<in> proj (set S) A"
 proof -
   define f where "f = (\<lambda>xa. case map_of (zip S x) xa of
            None \<Rightarrow> False | Some b \<Rightarrow> b)"
   have "map_of (zip S x) =
        (\<lambda>y. if y \<in> set S then Some (f y) else None)"
     unfolding f_def fun_eq_iff
     using map_of_zip_is_Some[OF assms(1)]
     by (metis option.case_eq_if option.distinct(1) option.exhaust option.sel)
   thus ?thesis
   using assms unfolding canon_map_of_def ApproxMCCore.proj_def restr_def image_def
   using f_def by auto
 qed
 
 lemma proj_proj_sol_map_of_zip_1:
   assumes "distinct S" "length S = length w"
   assumes w: "w \<in> rdb"
   shows "
     map_of (zip S w) \<in>
     proj (set S) {\<omega>. proj_sol S \<omega> \<in> rdb}"
   apply (intro canon_map_of_map_of[OF assms(2)])
   using proj_sol_canon_map_of[OF assms(1-2)] w by auto
 
 lemma proj_proj_sol_map_of_zip_2:
   assumes "\<And>bs. bs \<in> rdb \<Longrightarrow> length bs = length S"
   assumes w: "w \<in> proj (set S) {\<omega>. proj_sol S \<omega> \<in> rdb}"
   shows "
     w \<in> (map_of \<circ> zip S) ` rdb"
 proof -
   obtain ww where ww: "proj_sol S ww \<in> rdb" "w = restr (set S) ww"
   using w unfolding ApproxMCCore.proj_def
   by auto
 
   have "w = map_of (zip S (proj_sol S ww))"
     unfolding ww restr_def proj_sol_def map_of_zip_map
     by auto
 
   thus ?thesis using ww
   by (auto simp add: image_def)
 qed
 
 lemma proj_proj_sol_map_of_zip:
   assumes "distinct S"
   assumes "\<And>bs. bs \<in> rdb \<Longrightarrow> length bs = length S"
   shows "
     proj (set S) {\<omega>. proj_sol S \<omega> \<in> rdb} =
     (map_of \<circ> zip S) ` rdb"
   apply (rule antisym)
   subgoal
     using proj_proj_sol_map_of_zip_2[OF assms(2)]
     by blast
   using assms(2)
   by (auto intro!: proj_proj_sol_map_of_zip_1[OF assms(1)])
 
 definition ban_proj_sol ::"'a list \<Rightarrow> ('a \<Rightarrow> bool) list \<Rightarrow> 'fml \<Rightarrow> 'fml"
 where "ban_proj_sol S xs F =
     fold ban_sol (map (zip S \<circ> proj_sol S) xs) F"
 
 lemma check_sol_imp_proj:
   assumes "w \<in> sols F"
   shows "map_of (zip S (proj_sol S w)) \<in> proj (set S) (sols F)"
   unfolding proj_sol_def map_of_zip_map ApproxMCCore.proj_def image_def restr_def
   using assms by auto
 
 lemma checked_BSAT_lower:
   assumes S: "distinct S"
   assumes "check_BSAT_sols F S thresh xs = Inr ()"
   shows "length xs \<le> card (proj (set S) (sols F))"
   "length xs < thresh \<Longrightarrow>
     card (proj (set S) (sols F)) = length xs"
 proof -
   define Sxs where "Sxs = map (proj_sol S) xs"
   have dSxs: "distinct Sxs"
     using assms unfolding Sxs_def check_BSAT_sols_def Let_def
     by (auto split: if_splits)
 
   have lSxs: "\<And>x. x \<in> set Sxs \<Longrightarrow> length x = length S"
     unfolding Sxs_def proj_sol_def by auto
   define SSxs where "SSxs = map (zip S) Sxs"
   have dSSxs: "distinct (map map_of SSxs)"
     unfolding SSxs_def
     using dSxs unfolding inj_on_def distinct_map
     by (smt (verit) assms(1) imageE lSxs list.set_map map_of_zip_inject)
 
   have *: "set (map map_of SSxs) \<subseteq> proj (set S) (sols F)"
     unfolding Sxs_def SSxs_def
     using assms unfolding check_BSAT_sols_def Let_def
     by (auto intro!: check_sol_imp_proj split: if_splits simp add: check_sol list_all_iff)
   have "length xs = card (set (map map_of SSxs))"
     by (metis SSxs_def Sxs_def dSSxs length_map length_remdups_card_conv remdups_id_iff_distinct)
 
   thus "length xs \<le> card (proj (set S) (sols F))"
     by (metis * List.finite_set card_mono card_proj(1))
 
   have frr1: "(\<forall>vs \<in> set SSxs. map \<omega> (map fst vs) \<noteq> map snd vs) \<Longrightarrow>
     (\<forall>vs \<in> set Sxs. proj_sol S \<omega> \<noteq> vs)" for \<omega>
     apply (clarsimp simp add: proj_sol_def SSxs_def)
     by (metis (mono_tags, lifting) in_set_zip nth_map)
   have frr2: "(\<forall>vs \<in> set Sxs. proj_sol S \<omega> \<noteq> vs) \<Longrightarrow>
     (vs \<in> set SSxs \<Longrightarrow> map \<omega> (map fst vs) \<noteq> map snd vs)" for vs \<omega>
     apply (clarsimp simp add: proj_sol_def SSxs_def)
     by (smt (z3) Sxs_def assms(1) length_map length_map length_map map_eq_conv map_fst_zip map_of_zip_inject mem_Collect_eq nth_map nth_map nth_map proj_sol_def set_conv_nth set_conv_nth zip_map_fst_snd)
 
   have frr: "{\<omega>. (\<forall>vs \<in> set SSxs. map \<omega> (map fst vs) \<noteq> map snd vs)} =
     {\<omega>. (\<forall>vs \<in> set Sxs. proj_sol S \<omega> \<noteq> vs)}"
     using frr1 frr2 by auto
 
   moreover {
     assume "length xs < thresh"
     then have "sols (ban_proj_sol S xs F) = {}"
       apply (intro check_unsat)
       using assms(2) unfolding check_BSAT_sols_def Let_def
       by (auto simp add:ban_proj_sol_def o_assoc split: if_splits)
 
     then have "sols F \<inter> {\<omega>. (\<forall>vs \<in> set Sxs. proj_sol S \<omega> \<noteq> vs)} = {}"
       unfolding ban_proj_sol_def sols_fold_ban_sol
       frr[symmetric]
       by (auto simp add: SSxs_def Sxs_def)
     then have 1:"proj (set S) (sols F) \<inter>
       proj (set S)
        {\<omega>. \<forall>vs\<in>set Sxs. proj_sol S \<omega> \<noteq> vs} = {}"
       unfolding ApproxMCCore.proj_def
       using proj_sol_cong
       by (smt (verit, del_insts) disjoint_iff_not_equal image_iff mem_Collect_eq)
 
     have 2: "proj (set S) (sols F) \<inter> -proj (set S) {\<omega>. (\<forall>vs \<in> set Sxs. proj_sol S \<omega> \<noteq> vs)} =
       proj (set S) (sols F) \<inter> proj (set S)  {\<omega>. proj_sol S \<omega> \<in> set Sxs}"
       apply (intro inter_cong_right)
       by (auto intro!: proj_sol_cong simp add: ApproxMCCore.proj_def ) 
       
     have 3: "proj (set S)  {\<omega>. proj_sol S \<omega> \<in> set Sxs} = (map_of \<circ> zip S) ` (set Sxs)"
       apply (intro proj_proj_sol_map_of_zip[OF S])
       using lSxs by auto
 
     have 4: " proj (set S) (sols F) \<inter> (map_of \<circ> zip S) ` (set Sxs) =
       (map_of \<circ> zip S) ` (set Sxs)"
       using "*" SSxs_def by auto
 
     have **:"proj (set S) (sols F) =
       proj (set S) (sols F) \<inter> proj (set S) {\<omega>. (\<forall>vs \<in> set Sxs. proj_sol S \<omega> \<noteq> vs)} \<union>
       proj (set S) (sols F) \<inter> -proj (set S) {\<omega>. (\<forall>vs \<in> set Sxs. proj_sol S \<omega> \<noteq> vs)}"
       by auto
 
     have "card (proj (set S) (sols F)) =
       card ((map_of \<circ> zip S) ` (set Sxs))"
       apply (subst **)
       apply (subst card_Un_disjoint)
       using 1 2 3 4 by (auto simp add: card_proj(1))
 
     then have "card (proj (set S) (sols F)) = length xs"
       by (simp add: SSxs_def \<open>length xs = card (set (map map_of SSxs))\<close>)
   }
   thus "length xs < thresh \<Longrightarrow> card (proj (set S) (sols F)) = length xs"
   by auto
 qed
 
 lemma good_BSAT:
   assumes "distinct S"
   assumes "BSAT F S thresh xs = Inr n"
   shows "n \<le> card (proj (set S) (sols F))"
     "n < thresh \<Longrightarrow>
       card (proj (set S) (sols F)) = n"
   using checked_BSAT_lower[OF assms(1)] assms(2)
   by (auto simp add: BSAT_def split: if_splits sum.splits)
 
 lemma size_xorL_cert:
   assumes "distinct S"
   assumes "size_xorL_cert F S thresh xorsl i xs = Inr n"
   shows
     "size_xorL F S xorsl i \<ge> n"
     "n < thresh \<longrightarrow> size_xorL F S xorsl i = n"
   using assms unfolding size_xorL_def size_xorL_cert_def
   using good_BSAT by auto
 
 lemma approxcore_xorsL_cert:
   assumes S: "distinct S"
   assumes "approxcore_xorsL_cert F S thresh mc xorsl = Inr n"
   shows "approxcore_xorsL F S thresh xorsl = n"
 proof -
   obtain m cert1 cert2 where mc: "mc = (m,cert1,cert2)"
     using prod_cases3 by blast
   obtain nn1 where
     nn1:"size_xorL_cert F S thresh xorsl (m-1) cert1 = Inr nn1"
     using assms unfolding mc
     by (auto split: if_splits sum.splits)
 
   from  size_xorL_cert[OF S this]
   have nn1l:
     "nn1 \<le> size_xorL F S xorsl (m - 1)"
     "nn1 < thresh \<longrightarrow> size_xorL F S xorsl (m - 1) = nn1" by auto
 
   have m: "1 \<le> m" "m \<le> length S"
     "nn1 \<ge> thresh" and
     ms: "m = length S \<and> n = 2 ^ length S \<or>
       m < length S"
     using nn1 assms unfolding mc
     by (auto split: if_splits simp add: Let_def)
 
   have bnd: "\<And>i. 1 \<le> i \<Longrightarrow> i \<le> m -1 \<Longrightarrow>
       size_xorL F S xorsl i \<ge> thresh"
     using nn1l m(3)
     by (meson assms(1) dual_order.trans size_xorL_anti_mono)
 
   note ms
   moreover {
     assume *: "m = length S"
     then have "find (check_xorL F S thresh xorsl) [1..<length S] = None"
       unfolding find_None_iff check_xorL_def
       by (auto simp add: bnd leD)
     then have ?thesis
       unfolding approxcore_xorsL_def
       using * ms by force
   }
   moreover {
     assume *: "m < length S"
 
     obtain nn2 where
       nn2:"size_xorL_cert F S thresh xorsl m cert2 = Inr nn2"
         "nn2 < thresh"
         "n = 2 ^ m * nn2"
       using assms * unfolding mc
       by (auto split: if_splits sum.splits)
 
     from size_xorL_cert[OF S nn2(1)]
     have nn2l:
       "size_xorL F S xorsl m = nn2"
       using nn2(2) by blast
 
     then have "find (check_xorL F S thresh xorsl) [Suc 0..<length S] = Some m"
       apply (intro find_upto_SomeI)
       subgoal by (auto  simp add: m * bnd check_xorL_def leD)
       subgoal 
         using "*" calculation(1) size_xorL_cert(2) nn2
         by (auto  simp add: m * bnd check_xorL_def leD) 
       subgoal using m(1) by linarith
       by (auto  simp add: m * bnd check_xorL_def leD)
 
     then have ?thesis
       unfolding approxcore_xorsL_def using nn2 nn2l
       by auto
   }
   ultimately show ?thesis by auto
 qed
 
 lemma fold_approxcore_xorsL_cert:
   assumes S: "distinct S"
   assumes "i \<le> t"
   assumes "fold_approxcore_xorsL_cert F S thresh t i cs xorsLs = Inr ns"
   shows "map (approxcore_xorsL F S thresh \<circ> xorsLs) [t-i..<t] = ns "
   using assms(2-3)
 proof (induction i arbitrary: ns)
   case 0
   then show ?case
     by auto
 next
   case c:(Suc i)
   from c(3)
   obtain n nss where *:"ns = n # nss"
      "fold_approxcore_xorsL_cert F S thresh t i cs xorsLs = Inr nss"
      "approxcore_xorsL_cert F S thresh (cs (t-Suc i)) (xorsLs (t-Suc i)) = Inr n"
     by (auto simp add: Let_def split: sum.splits)
 
   have "i \<le> t" using c by auto
   from c(1)[OF this *(2)]
   have 2: "nss =
     map (approxcore_xorsL F S thresh \<circ> xorsLs) [t - i..<t]"
     by auto
 
   have i:"[t - Suc i..<t] = (t - Suc i) # [t - i..<t]"
     apply (subst upt_rec)
     using c(2)
     using Suc_diff_Suc Suc_le_lessD by presburger
 
   show ?case
     unfolding i *
     apply (clarsimp simp add: 2 )
     using  2 "*"(3) approxcore_xorsL_cert assms(1) by blast
 qed
 
 lemma calc_median:
   assumes S: "distinct S"
   assumes "calc_median F S thresh t ms xorsLs = Inr n"
   shows "median t (approxcore_xorsL F S thresh \<circ> xorsLs) = n"
   using assms
   unfolding calc_median_def  median_def
   apply (clarsimp simp add: assms split: if_splits sum.splits)
   using  fold_approxcore_xorsL_cert[OF S]
   by (metis diff_is_0_eq' dual_order.refl)
 
 lemma compute_t_find_t[simp]:
   shows "appmc.compute_t \<delta> (find_t \<delta>) = find_t \<delta>"
   unfolding find_t_def appmc.compute_t_def
   apply (clarsimp simp add: option.case_eq_if)
   unfolding find_Some_iff
   by auto
 
 lemma certcheck:
   assumes "distinct S"
   assumes "certcheck F S \<epsilon> \<delta> (m0,ms) xorsLs = Inr n"
   shows "approxmc_mapL F S \<epsilon> \<delta> (find_t \<delta>) xorsLs = n"
   using assms(2)
   unfolding approxmc_mapL_def
   using good_BSAT apply (clarsimp split: sum.splits if_splits simp add: Let_def)
   subgoal using order_le_less_trans assms by blast
   using assms order.strict_trans1
   by (meson assms(1) calc_median)
 
 lemma certcheck':
   assumes "distinct S"
   assumes "\<not>isl (certcheck F S \<epsilon> \<delta> m xorsLs)"
   shows "projr (certcheck F S \<epsilon> \<delta> m xorsLs) =
     approxmc_mapL F S \<epsilon> \<delta> (find_t \<delta>) xorsLs"
   by (metis certcheck assms(1) assms(2) sum.collapse(2) surj_pair)
 
 (* For any function f mapping randomness to certificates,
   The probability that the certificate accepts (\<not>isl)
   With output c not in the interval is at most \<delta> *)
 lemma certcheck_sound:
   assumes \<delta>: "\<delta> > 0" "\<delta> < 1"
   assumes \<epsilon>: "\<epsilon> > 0"
   assumes S: "distinct S"
   shows "
     measure_pmf.prob
       (map_pmf (\<lambda>r. certcheck F S \<epsilon> \<delta> (f r) r)
         (random_seed_xors (find_t \<delta>) (length S)))
       {c. \<not>isl c \<and>
         real (projr c) \<notin>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}} \<le> \<delta>"
 proof -
   have "measure_pmf.prob
       (map_pmf (\<lambda>r. certcheck F S \<epsilon> \<delta> (f r) r)
         (random_seed_xors (find_t \<delta>) (length S)))
       {c. \<not>isl c \<and>
         real (projr c) \<notin>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}} \<le>
    prob_space.prob
       (map_pmf (approxmc_mapL F S \<epsilon> \<delta> (find_t \<delta>))
         (random_seed_xors (appmc.compute_t \<delta> (find_t \<delta>)) (length S)))
       {c. real c \<notin>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}}"
     unfolding measure_map_pmf compute_t_find_t
     by (auto intro!: measure_pmf.finite_measure_mono simp add: certcheck'[OF S])
   also have "... \<le> \<delta>"
     by (intro approxmcL_sound'[OF assms])
   finally show ?thesis by auto
 qed
 
 (* A completeness theorem for the checker in the face of probabilistic guarantees
   It is stated with a "promise"-style guarantee:
   For any function f mapping randomness to certificates,
   If the checker accepts (\<not>isl) the output of f on any randomness
   Then the output c is in the interval with high probability (1 - \<delta>) *)
 lemma certcheck_promise_complete:
   assumes \<delta>: "\<delta> > 0" "\<delta> < 1"
   assumes \<epsilon>: "\<epsilon> > 0"
   assumes S: "distinct S"
   assumes r: "\<And>r.
     r \<in> set_pmf (random_seed_xors (find_t \<delta>) (length S)) \<Longrightarrow>
     \<not>isl (certcheck F S \<epsilon> \<delta> (f r) r)"
   shows "
     measure_pmf.prob
       (map_pmf (\<lambda>r. certcheck F S \<epsilon> \<delta> (f r) r)
         (random_seed_xors (find_t \<delta>) (length S)))
       {c. real (projr c) \<in>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}} \<ge> 1 - \<delta>"
 proof -
   have "
    measure_pmf.prob
       (map_pmf (\<lambda>r. certcheck F S \<epsilon> \<delta> (f r) r)
         (random_seed_xors (find_t \<delta>) (length S)))
       {c. real (projr c) \<in>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}} =
    measure_pmf.prob
       (map_pmf (approxmc_mapL F S \<epsilon> \<delta> (find_t \<delta>))
         (random_seed_xors (appmc.compute_t \<delta> (find_t \<delta>)) (length S)))
       {c. real c \<in>
         {real (card (proj (set S) (sols F))) / (1 + \<epsilon>)..
           (1 + \<epsilon>) * real (card (proj (set S) (sols F)))}}"
     unfolding measure_map_pmf compute_t_find_t
     by (auto intro!: measure_pmf.measure_pmf_eq simp add: certcheck'[OF S] r)
   also have "... \<ge> 1 -  \<delta>"
     by (intro approxmcL_sound[OF assms(1-4)])
   finally show ?thesis by auto
 qed
 
+end
+
 lemma certcheck_code[code]:
    "certcheck F S \<epsilon> \<delta> (m0,ms) xorsLs = (
     if \<delta> > 0 \<and> \<delta> < 1 \<and> \<epsilon> > 0 \<and> distinct S then
       (let \<epsilon> = appmc.mk_eps \<epsilon> in
       let thresh = appmc.compute_thresh \<epsilon> in
       case BSAT F S thresh m0 of Inl err \<Rightarrow> Inl err
       | Inr Y \<Rightarrow>
       if Y < thresh then Inr Y
       else
         let t = find_t \<delta> in
         calc_median F S thresh t ms xorsLs)
      else Code.abort (STR ''invalid inputs'')
         (\<lambda>_. certcheck F S \<epsilon> \<delta> (m0,ms) xorsLs))"
   by auto
 
 end
 
 end
 
 end
-
-end
diff --git a/thys/Approximate_Model_Counting/RandomXOR.thy b/thys/Approximate_Model_Counting/RandomXOR.thy
--- a/thys/Approximate_Model_Counting/RandomXOR.thy
+++ b/thys/Approximate_Model_Counting/RandomXOR.thy
@@ -1,1634 +1,1634 @@
 section \<open>Random XORs\<close>
 
 text \<open>The goal of this section is to prove that,
   for a randomly sampled XOR $X$ from a set of variables $V$:
   \begin{enumerate}
   \item the probability of an assignment $w$ satisfying $X$ is $\frac{1}{2}$;
   \item for any distinct assignments $w$, $w'$ the probability of both satisfying $X$ is equal to $\frac{1}{4}$ (2-wise independence); and
   \item for any distinct assignments $w$, $w'$, $w''$ the probability of all three
      satisfying $X$ is equal to $\frac{1}{8}$ (3-wise independence).
   \end{enumerate}
   \<close>
 
 theory RandomXOR imports
   ApproxMCPreliminaries
   Frequency_Moments.Product_PMF_Ext
   Monad_Normalisation.Monad_Normalisation
 begin
 
 
 text \<open>A random XOR constraint is modeled
   as a random subset of variables and a randomly chosen RHS bit. \<close>
 definition random_xor :: "'a set \<Rightarrow> ('a set \<times> bool) pmf"
   where "random_xor V =
     pair_pmf (pmf_of_set (Pow V)) (bernoulli_pmf (1/2))"
 
 lemma pmf_of_set_Pow_fin_map:
   assumes V:"finite V"
   shows "pmf_of_set (Pow V) =
     map_pmf (\<lambda>b. {x \<in> V. b x = Some True})
      (Pi_pmf V def (\<lambda>_. map_pmf Some (bernoulli_pmf (1 / 2))))"
 proof -
   have *: "Pi_pmf V def (\<lambda>_. map_pmf Some (bernoulli_pmf (1 / 2))) =
     map_pmf (\<lambda>f x. if x \<in> V then f x else def)
     (Pi_pmf V (Some False) (\<lambda>_. map_pmf Some (bernoulli_pmf (1 / 2))))"
     unfolding Pi_pmf_default_swap[OF V] by auto
 
   have **: "pmf_of_set (Pow V) =
     map_pmf
      (\<lambda>x. {xa. (xa \<in> V \<longrightarrow> x xa) \<and> xa \<in> V})
      (Pi_pmf V False  (\<lambda>_. bernoulli_pmf (1 / 2)))"
     by (smt (verit, ccfv_SIG) Collect_cong pmf_of_set_Pow_conv_bernoulli V pmf.map_cong)
   show ?thesis
     unfolding *
     apply (subst Pi_pmf_map[OF V, of _ "False"])
     using ** by (auto simp add: pmf.map_comp o_def)
 qed
 
 (* A random XOR can also be sampled as a
   map |V| \<Rightarrow> bool + a coin flip *)
 lemma random_xor_from_bits:
   assumes V:"finite V"
   shows "random_xor V =
     pair_pmf
       (map_pmf (\<lambda>b. {x \<in> V. b x = Some True})
         (Pi_pmf V def (\<lambda>_. map_pmf Some (bernoulli_pmf (1/2)))))
       (bernoulli_pmf (1/2))"
   unfolding random_xor_def
   using V pmf_of_set_Pow_fin_map by fastforce
 
 (* An assignment is a subset \<omega> of V
    i.e., those variables assigned to true *)
 fun satisfies_xor :: "('a set \<times> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   where "satisfies_xor (x,b) \<omega> =
      even (card (\<omega> \<inter> x) + of_bool b) "
 
 (*
 (* x_0 \<oplus> x_1 \<oplus> x_2 = 0 *)
 value "satisfies_xor ({0,1,2},False) {0::nat}"
 (* x_0 \<oplus> x_1 \<oplus> x_2 = 1 *)
 value "satisfies_xor ({0,1,2},True) {0::nat}"
 *)
 
 lemma satisfies_xor_inter:
   shows "satisfies_xor ( \<omega> \<inter> x ,b) \<omega> = satisfies_xor (x,b) \<omega>"
   by (auto simp add: Int_commute)
 
 lemma prob_bernoulli_bind_pmf:
   assumes "0 \<le> p" "p \<le> 1"
   assumes "finite E"
   shows "measure_pmf.prob
    (bernoulli_pmf p \<bind> x) E =
   p * (measure_pmf.prob (x True) E) +
   (1 - p) * (measure_pmf.prob (x False) E) "
   using assms
   by (auto simp add: pmf_bind measure_measure_pmf_finite[OF assms(3)] vector_space_over_itself.scale_sum_right comm_monoid_add_class.sum.distrib mult.commute)
 
 lemma set_pmf_random_xor:
   assumes V: "finite V"
   shows "set_pmf (random_xor V) = (Pow V) \<times> UNIV"
   unfolding random_xor_def
   using assms by (auto simp add: Pow_not_empty Set.basic_monos(7))
 
 lemma pmf_of_set_prod:
   assumes "P \<noteq> {}" "Q \<noteq> {}"
   assumes "finite P" "finite Q"
   shows "pmf_of_set (P \<times> Q) = pair_pmf (pmf_of_set P) (pmf_of_set Q)"
   by (auto intro!: pmf_eqI simp add: indicator_def pmf_pair assms)
 
 lemma random_xor_pmf_of_set:
   assumes V:"finite V"
   shows "random_xor V  = pmf_of_set ((Pow V) \<times> UNIV)"
   unfolding random_xor_def
   apply (subst pmf_of_set_prod)
   using V bernoulli_pmf_half_conv_pmf_of_set by auto
 
 lemma prob_random_xor_with_set_pmf:
   assumes V: "finite V"
   shows "prob_space.prob (random_xor V) {c. P c} =
     prob_space.prob (random_xor V) {c. fst c \<subseteq> V \<and> P c}"
   by (smt (verit, best) PowD assms measure_pmf.measure_pmf_eq mem_Collect_eq mem_Sigma_iff prod.collapse set_pmf_random_xor)
 
 lemma prob_set_parity:
   assumes "measure_pmf.prob M
     {c. P c} = q"
   shows "measure_pmf.prob M
     {c. P c = b} = (if b then q else 1 - q)"
 proof -
   {
     assume b:"b"
     have ?thesis using assms
       using b by presburger
   }
   moreover {
     assume b:"\<not>b"
     have "{c. P c} \<in> measure_pmf.events M" by auto
     from measure_pmf.prob_compl[OF this]
     have "1 - q = measure_pmf.prob M (UNIV - {c. P c})"
       using assms by auto
     moreover have " ... =
       prob_space.prob M
       {c. P c = b}"
       by (simp add: b measure_pmf.measure_pmf_eq)
     ultimately have ?thesis
       using b by presburger
   }
   ultimately show ?thesis by auto
 qed
 
 lemma satisfies_random_xor:
   assumes V: "finite V"
   shows "prob_space.prob (random_xor V)
     {c. satisfies_xor c \<omega>} = 1 / 2"
 proof -
   have eq: "{(c::'a set \<times> bool). fst c \<subseteq> V} = {c. c \<subseteq> V} \<times> UNIV"
     by auto
   then have "finite {(c::'a set \<times> bool). fst c \<subseteq> V}"
     using assms by auto
 
   then have *: "
     x \<subseteq> V \<Longrightarrow>
     measure_pmf.prob (bernoulli_pmf (1 / 2) \<bind> (\<lambda>y. return_pmf (x, y)))
         {c. fst c \<subseteq> V \<and> satisfies_xor c \<omega>} = 1 / 2" for x
     apply (subst prob_bernoulli_bind_pmf)
     by (auto simp add: indicator_def)
 
   have "prob_space.prob (random_xor V) {c. satisfies_xor c \<omega>} =
     prob_space.prob (random_xor V) {c. fst c \<subseteq> V \<and> satisfies_xor c \<omega>}"
     using prob_random_xor_with_set_pmf[OF V] by auto
   also have "... =
     prob_space.expectation (random_xor V)
     (indicat_real {c. fst c \<subseteq> V \<and> satisfies_xor c \<omega>})"
     by auto
   also have "... = (\<Sum>a\<in>Pow V.
        inverse (real (card (Pow V))) *
        measure_pmf.prob
         (bernoulli_pmf (1 / 2) \<bind>
          (\<lambda>y. return_pmf (a, y)))
         {c. fst c \<subseteq> V \<and> satisfies_xor c \<omega>})"
     unfolding random_xor_def pair_pmf_def
     apply (subst pmf_expectation_bind_pmf_of_set)
     using assms by auto
   also have "... = (\<Sum>a\<in>Pow V.
        inverse (real (card (Pow V))) * (1/2))"
     by (simp add: *)
   also have "... =
        inverse (real (card (Pow V))) * (1/2) * (\<Sum>a\<in>Pow V. 1)"
     using * by force
   also have "... = 1/2"
     by (metis One_nat_def Suc_leI assms card_Pow divide_real_def inverse_inverse_eq inverse_nonzero_iff_nonzero nat_one_le_power nonzero_mult_div_cancel_left not_one_le_zero of_nat_eq_0_iff pos2 real_of_card)
   finally show ?thesis
     by presburger
 qed
 
 lemma satisfies_random_xor_parity:
   assumes V: "finite V"
   shows "prob_space.prob (random_xor V)
     {c. satisfies_xor c \<omega> = b} = 1 / 2"
   using prob_set_parity[OF satisfies_random_xor[OF V]]
     by auto
 
 subsection "Independence properties of random XORs"
 
 lemma pmf_of_set_powerset_split:
   assumes "S \<subseteq> V" "finite V"
   shows "
     map_pmf (\<lambda>(x,y). x \<union> y)
     (pmf_of_set (Pow S \<times> Pow (V - S))) =
   pmf_of_set (Pow V)"
 proof -
   have spmfS: "set_pmf (pmf_of_set (Pow S)) = Pow S"
     using assms
     by (auto intro!: set_pmf_of_set simp add: rev_finite_subset)
   have spmfVS: "set_pmf (pmf_of_set (Pow (V-S))) = Pow (V-S)"
     using assms by (auto intro!: set_pmf_of_set)
 
   have xsub: "x \<subseteq> V \<Longrightarrow>
          \<exists>xa\<in>Pow S.
             \<exists>y\<in>Pow (V - S). x = xa \<union> y" for x 
     by (metis Diff_subset_conv Pow_iff Un_Diff_Int basic_trans_rules(23) inf_le2 sup_commute)
 
   have inj: "inj_on (\<lambda>(x, y). x \<union> y)
      (Pow S \<times> Pow (V - S))"
     unfolding inj_on_def
     by auto
   then have bij: "bij_betw (\<lambda>(x, y). x \<union> y)
      ((Pow S) \<times> Pow (V - S))
      (Pow V)"
     unfolding bij_betw_def
     using assms(1) xsub by (auto simp add: image_def)
 
   have "map_pmf (\<lambda>(x, y). x \<union> y)
      (pmf_of_set (Pow S \<times> Pow (V - S))) =
     pmf_of_set (Pow V)"
     apply (subst map_pmf_of_set_inj[OF inj])
     subgoal by (auto simp add: image_def)
     subgoal using bij assms(2) bij_betw_finite by blast
     apply (intro arg_cong[where f = "pmf_of_set"])
     using assms(1) xsub by (auto  simp add: image_def)
 
   thus ?thesis
     unfolding spmfS spmfVS
     by auto
 qed
 
 lemma pmf_of_set_Pow_sing:
   shows"pmf_of_set (Pow {x}) =
      bernoulli_pmf (1 / 2) \<bind>
      (\<lambda>b. return_pmf (if b then {x} else {}))"
   apply (intro pmf_eqI)
   apply (subst pmf_of_set)
   by (auto simp add: pmf_bind card_Pow indicator_def subset_singleton_iff)
 
 lemma pmf_of_set_sing_coin_flip:
   assumes "finite V"
   shows "pmf_of_set (Pow {x} \<times> Pow V) =
     map_pmf (\<lambda>(r,c). (if c then {x} else {}, r)) (random_xor V)"
 proof -
   have *: "pmf_of_set (Pow {x} \<times> Pow V) =
     pair_pmf (pmf_of_set (Pow {x})) (pmf_of_set (Pow V))"
     apply(intro pmf_of_set_prod)
     using assms by auto
   show ?thesis
     unfolding *
     apply (intro pmf_eqI)
     including monad_normalisation
     by (auto simp add: map_pmf_def pair_pmf_def random_xor_def pmf_of_set_Pow_sing)
 qed
 
 (* TODO: there is a more general version below *)
 lemma measure_pmf_prob_dependent_product_bound_eq:
   assumes "countable A" "\<And>i. countable (B i)"
   assumes "\<And>a. a \<in> A \<Longrightarrow> measure_pmf.prob N (B a) = r"
   shows "measure_pmf.prob (pair_pmf M N) (Sigma A B) =
     measure_pmf.prob M A * r"
 proof -
   have "measure_pmf.prob (pair_pmf M N) (Sigma A B) =
     (\<Sum>\<^sub>a(a, b) \<in> Sigma A B. pmf M a * pmf N b)"
     by (auto intro!: infsetsum_cong simp add: measure_pmf_conv_infsetsum pmf_pair)
   also have "... = (\<Sum>\<^sub>aa\<in>A. \<Sum>\<^sub>ab\<in>B a. pmf M a * pmf N b)"
     apply (subst infsetsum_Sigma[OF assms(1-2)])
     subgoal by (metis (no_types, lifting) SigmaE abs_summable_on_cong case_prod_conv pmf_abs_summable pmf_pair)
     by (auto simp add: assms case_prod_unfold)
 
   also have "... = (\<Sum>\<^sub>aa\<in>A. pmf M a * (measure_pmf.prob N (B a)))"
     by (simp add: infsetsum_cmult_right measure_pmf_conv_infsetsum pmf_abs_summable)
   also have "... = (\<Sum>\<^sub>aa\<in>A. pmf M a * r)"
     using assms(3) by force
   also have"... = measure_pmf.prob M A * r"
     by (simp add: infsetsum_cmult_left pmf_abs_summable measure_pmf_conv_infsetsum)
   finally show ?thesis
     by linarith
 qed
 
 (* TODO: duplicated in Schwartz_Zippel, but
   we don't want to pull in the multivariate polynomials library *)
 lemma measure_pmf_prob_dependent_product_bound_eq':
   assumes "countable (A \<inter> set_pmf M)" "\<And>i. countable (B i \<inter> set_pmf N)"
   assumes "\<And>a. a \<in> A \<inter> set_pmf M \<Longrightarrow> measure_pmf.prob N (B a \<inter> set_pmf N) = r"
   shows "measure_pmf.prob (pair_pmf M N) (Sigma A B) = measure_pmf.prob M A * r"
 proof -
   have *: "Sigma A B \<inter> (set_pmf M \<times> set_pmf N) =
     Sigma (A \<inter> set_pmf M) (\<lambda>i. B i \<inter> set_pmf N)"
     by auto
 
   have "measure_pmf.prob (pair_pmf M N) (Sigma A B) =
     measure_pmf.prob (pair_pmf M N) (Sigma (A \<inter> set_pmf M) (\<lambda>i. B i \<inter> set_pmf N))"
     by (metis * measure_Int_set_pmf set_pair_pmf)
   moreover have "... =
     measure_pmf.prob M (A \<inter> set_pmf M) * r"
     using measure_pmf_prob_dependent_product_bound_eq[OF assms(1-3)]
     by auto
   moreover have "... = measure_pmf.prob M A * r"
     by (simp add: measure_Int_set_pmf)
   ultimately show ?thesis by linarith
 qed
 
 lemma single_var_parity_coin_flip:
   assumes "x \<in> \<omega>" "finite \<omega>"
   assumes "finite a" "x \<notin> a"
   shows "measure_pmf.prob (pmf_of_set (Pow {x}))
           {y. even (card ((a \<union> y) \<inter> \<omega>)) = b}  = 1/2"
 proof -
   have "insert x a \<inter> \<omega> = insert x (a \<inter> \<omega>)"
     using assms by auto
   then have *: "card (insert x a \<inter> \<omega>) = 1 + card (a \<inter> \<omega>)"
     by (simp add: assms(2) assms(4))
 
   have "measure_pmf.prob (pmf_of_set (Pow {x}))
           {y. even (card ((a \<union> y) \<inter> \<omega>)) = b} =
     measure_pmf.prob (bernoulli_pmf (1/2))
           {odd (card (a \<inter> \<omega>)) = b}"
     unfolding pmf_of_set_Pow_sing map_pmf_def[symmetric]
     by (auto intro!: measure_prob_cong_0 simp add:image_def * )
   moreover have "... = 1/2"
     by (simp add: measure_pmf_single)
   ultimately show ?thesis by auto
 qed
 
 (*
   Fix any event E that does not touch x
   Then we can sample that event separately
 *)
 lemma prob_pmf_of_set_nonempty_parity:
   assumes V: "finite V"
   assumes "x \<in> \<omega>" "\<omega> \<subseteq> V"
   assumes "\<And>c. c \<in> E \<longleftrightarrow> c - {x} \<in> E"
   shows "prob_space.prob (pmf_of_set (Pow V))
     (E \<inter> {c. even (card (c \<inter> \<omega>)) = b}) =
     1 / 2 * prob_space.prob (pmf_of_set (Pow (V - {x}))) E"
 proof -
   have 1: "set_pmf (pmf_of_set (Pow {x})) = Pow {x}"
     by (simp add: Pow_not_empty)
   have 2: "set_pmf (pmf_of_set (Pow (V-{x}))) = Pow (V-{x})"
     by (simp add: Pow_not_empty assms(1))
   have 3: "set_pmf (pmf_of_set (Pow {x} \<times> Pow (V - {x}))) = Pow {x} \<times> Pow (V - {x})"
     by (simp add: Pow_not_empty assms(1))
 
   have "{x} \<subseteq> V" using assms by auto
   from pmf_of_set_powerset_split[OF this assms(1)]
   have e: "map_pmf (\<lambda>(x, y). x \<union> y)
      (pmf_of_set (Pow {x} \<times> Pow (V - {x}))) =
     pmf_of_set (Pow V)" using 1 2 by auto
   have "map_pmf (\<lambda>(x, y). x \<union> y)
      (pair_pmf (pmf_of_set (Pow {x}))
        (pmf_of_set (Pow (V - {x})))) =
     map_pmf (\<lambda>(x, y). x \<union> y)
      (pair_pmf (pmf_of_set (Pow (V - {x})))
        (pmf_of_set (Pow {x})))"
     apply (subst pair_commute_pmf)
     by (auto simp add: pmf.map_comp o_def case_prod_unfold Un_commute)
   then have *: "pmf_of_set (Pow V) =
     map_pmf (\<lambda>(x, y). x \<union> y)
      (pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x})))"
     unfolding e[symmetric]
     apply (subst pmf_of_set_prod)
     using V by auto
 
   have **: "((\<lambda>(x, y). x \<union> y) -` (E \<inter> S)) \<inter> (Pow (V - {x}) \<times> Pow{x}) =
     Sigma E (\<lambda>x. {y. (x \<union> y) \<in> S}) \<inter> (Pow (V - {x}) \<times> Pow{x})" for S
   proof -
     have 11: "\<And>a b. a \<union> b \<in> E \<Longrightarrow>
            a \<union> b \<in> S \<Longrightarrow>
            a \<subseteq> V - {x} \<Longrightarrow>
            b \<subseteq> {x} \<Longrightarrow> a \<in> E"
       by (metis Diff_insert_absorb Un_insert_right assms(4) boolean_algebra_cancel.sup0 subset_Diff_insert subset_singleton_iff)
 
     have 21: " \<And>a b. a \<in> E \<Longrightarrow>
            a \<union> b \<in> S \<Longrightarrow>
            a \<subseteq> V - {x} \<Longrightarrow>
            b \<subseteq> {x} \<Longrightarrow> a \<union> b \<in> E"
       by (metis Diff_cancel Un_Diff Un_empty_left assms(4) inf_sup_aci(5) subset_singletonD)
 
     have 1: "
       \<And>ab.  ab \<in> ((\<lambda>(x, y). x \<union> y) -` (E \<inter> S)) \<inter> (Pow (V - {x}) \<times> Pow{x}) \<Longrightarrow>
         ab \<in> Sigma E (\<lambda>x. {y. (x \<union> y) \<in> S}) \<inter> (Pow (V - {x}) \<times> Pow{x})"
         using 11 by clarsimp
 
     also have 2: "
       \<And>ab. ab \<in> Sigma E (\<lambda>x. {y. (x \<union> y) \<in> S}) \<inter> (Pow (V - {x}) \<times> Pow{x}) \<Longrightarrow>
          ab \<in> ((\<lambda>(x, y). x \<union> y) -` (E \<inter> S)) \<inter> (Pow (V - {x}) \<times> Pow{x})"
       using 21 by clarsimp
     ultimately show ?thesis
       apply (intro antisym)
       by (meson subsetI)+
   qed
 
   have eR: "\<And>a. a \<in> E \<inter> set_pmf (pmf_of_set (Pow (V - {x}))) \<Longrightarrow>
    measure_pmf.prob (pmf_of_set (Pow {x}))
     ({y. even (card ((a \<union> y) \<inter> \<omega>)) = b} \<inter>
      set_pmf (pmf_of_set (Pow {x}))) = 1/2 "
     apply (subst measure_Int_set_pmf)
     apply (intro single_var_parity_coin_flip)
     subgoal using assms by clarsimp
     subgoal using assms rev_finite_subset by blast
     subgoal by (metis 2 IntD2 PowD assms(1) finite_Diff rev_finite_subset)
     using 2 by blast
 
   have "
     prob_space.prob (pmf_of_set (Pow V))
       (E \<inter> {c. even (card (c \<inter> \<omega>)) = b}) =
     prob_space.prob (map_pmf (\<lambda>(x, y). x \<union> y)
        (pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x}))))
       (E \<inter> {c. even (card (c \<inter> \<omega>)) = b})" unfolding * by auto
   moreover have "... =
     prob_space.prob (pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x})))
       ((\<lambda>(x, y). x \<union> y) -` (E \<inter> {c. even (card (c \<inter> \<omega>)) = b}))"
     by auto
   moreover have "... =
    prob_space.prob (pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x})))
     ((\<lambda>(x, y). x \<union> y) -` (E \<inter> {c. even (card (c \<inter> \<omega>)) = b}) \<inter> (Pow (V - {x}) \<times> Pow{x}))"
     by (smt (verit) "1" "2" Int_iff Sigma_cong measure_pmf.measure_pmf_eq set_pair_pmf)
   moreover have "... =
    prob_space.prob (pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x})))
     (Sigma E (\<lambda>x. {y. even (card ((x \<union> y) \<inter> \<omega>)) = b}) \<inter> (Pow (V - {x}) \<times> Pow{x}))"
     unfolding ** by auto
   moreover have "... =
    prob_space.prob (pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x})))
     (Sigma E (\<lambda>x. {y. even (card ((x \<union> y) \<inter> \<omega>)) = b}))"
     by (smt (verit, best) 1 2 Int_iff Sigma_cong measure_pmf.measure_pmf_eq set_pair_pmf)
   moreover have "... =
     measure_pmf.prob (pmf_of_set (Pow (V - {x}))) E *
     (1 / 2)"
     apply (subst measure_pmf_prob_dependent_product_bound_eq'[OF _ _ eR])
     by auto
   ultimately show ?thesis by auto
 qed
 
 lemma prob_random_xor_split:
   assumes V: "finite V"
   shows "prob_space.prob (random_xor V) E =
     1 / 2 * prob_space.prob (pmf_of_set (Pow V)) {e. (e,True) \<in> E} +
     1 / 2 * prob_space.prob (pmf_of_set (Pow V)) {e. (e,False) \<in> E}"
 proof -
   have fin: "finite (set_pmf (random_xor V))"
     by (simp add: V set_pmf_random_xor)
 
   have fin2: "finite ((\<lambda>(x, y). (y, x)) -` set_pmf (random_xor V))"
     by(auto intro!: finite_vimageI[OF fin] simp add: inj_def)
 
   have rw: "{x. (x, b) \<in> E \<and> (x, b) \<in> set_pmf (random_xor V)} =
     {x. (x,b) \<in> E} \<inter> set_pmf (pmf_of_set (Pow V))" for b
-    by (auto simp add: V set_pmf_random_xor Pow_not_empty V)
+    by (auto simp add: V set_pmf_random_xor Pow_not_empty)
 
   have "prob_space.prob (random_xor V) E =
     prob_space.prob (random_xor V) (E \<inter> set_pmf (random_xor V))"
     by (simp add: measure_Int_set_pmf)
 
   moreover have "... =
      measure_pmf.prob
      (pair_pmf (bernoulli_pmf (1 / 2))
        (pmf_of_set (Pow V)))
      ((\<lambda>(x, y). (y, x)) -` (E \<inter> set_pmf (random_xor V)))"
     unfolding random_xor_def
     apply (subst pair_commute_pmf)
     by simp
   moreover have "... =
     1 / 2 *
       measure_pmf.prob (pmf_of_set (Pow V)) {x. (x, True) \<in> E} +
     1 / 2 *
       measure_pmf.prob (pmf_of_set (Pow V)) {x. (x, False) \<in> E}"
     unfolding pair_pmf_def
     apply (subst prob_bernoulli_bind_pmf)
     using fin2
     unfolding map_pmf_def[symmetric] measure_map_pmf
     by (auto simp add: vimage_def rw simp add: measure_Int_set_pmf)
   ultimately show ?thesis by auto
 qed
 
 lemma prob_random_xor_nonempty_parity:
   assumes V: "finite V"
   assumes \<omega>: "x \<in> \<omega>" "\<omega> \<subseteq> V"
   assumes E: "\<And>c. c \<in> E \<longleftrightarrow> (fst c - {x},snd c) \<in> E"
   shows "prob_space.prob (random_xor V)
     (E \<inter> {c. satisfies_xor c \<omega> = b}) =
     1 / 2 * prob_space.prob (random_xor (V - {x})) E"
 proof -
   have *: "{e. (e, b') \<in> E \<inter> {c. satisfies_xor c \<omega> = b}} =
     {e. (e, b') \<in> E} \<inter> {c. even (card (c \<inter> \<omega>)) = (b \<noteq> b')}" for b'
     by (auto simp add: Int_commute)
 
   have "prob_space.prob (random_xor V)
     (E \<inter> {c. satisfies_xor c \<omega> = b})  =
     1 / 2 *
     measure_pmf.prob (pmf_of_set (Pow V))
      {e. (e, True) \<in> E \<inter> {c. satisfies_xor c \<omega> = b}} +
     1 / 2 *
     measure_pmf.prob (pmf_of_set (Pow V))
      {e. (e, False) \<in> E \<inter> {c. satisfies_xor c \<omega> = b}}"
     unfolding prob_random_xor_split[OF V] by auto
   also have "... =
     1 / 2 *
     measure_pmf.prob (pmf_of_set (Pow V))
      ({e. (e, True) \<in> E} \<inter> {c. even (card (c \<inter> \<omega>)) = (b \<noteq> True)}) +
     1 / 2 *
     measure_pmf.prob (pmf_of_set (Pow V))
      ({e. (e, False) \<in> E} \<inter> {c. even (card (c \<inter> \<omega>)) = (b \<noteq> False)})"
     unfolding * by auto
   also have "... =
     1 / 2 *
     (1 / 2 *
      measure_pmf.prob (pmf_of_set (Pow (V - {x})))
       {e. (e, True) \<in> E} +
      1 / 2 *
      measure_pmf.prob (pmf_of_set (Pow (V - {x})))
       {e. (e, False) \<in> E})"
     apply (subst prob_pmf_of_set_nonempty_parity[OF V \<omega>])
     subgoal using E by clarsimp
     apply (subst prob_pmf_of_set_nonempty_parity[OF V \<omega>])
     using E by auto
   also have "... =
     1 / 2 * measure_pmf.prob (random_xor (V - {x})) E"
     apply (subst prob_random_xor_split[symmetric])
     using V by auto
   finally show ?thesis by auto
 qed
 
 lemma pair_satisfies_random_xor_parity_1:
   assumes V:"finite V"
   assumes x: "x \<notin> \<omega>" "x \<in> \<omega>'"
   assumes \<omega>: "\<omega> \<subseteq> V" "\<omega>' \<subseteq> V"
   shows "prob_space.prob (random_xor V)
     {c. satisfies_xor c \<omega> = b \<and> satisfies_xor c \<omega>' = b'} = 1 / 4"
 proof -
   have wa: "\<omega> \<inter> (a - {x}) = \<omega> \<inter> a" for a
     using x
     by blast
   have "prob_space.prob (random_xor V)
     {c. satisfies_xor c \<omega> = b \<and> satisfies_xor c \<omega>' = b'} =
     prob_space.prob (random_xor V)
     ({c. satisfies_xor c \<omega> = b} \<inter> {c. satisfies_xor c \<omega>' = b'})"
     by (simp add: Collect_conj_eq)
   also have "... =
     1 / 2 *
     measure_pmf.prob (random_xor (V - {x})) {c. satisfies_xor c \<omega> = b}"
     apply (subst prob_random_xor_nonempty_parity[OF V x(2) \<omega>(2)])
     by (auto simp add: wa)
   also have "... = 1/4"
     apply (subst satisfies_random_xor_parity)
     using V by auto
   finally show ?thesis by auto
 qed
 
 lemma pair_satisfies_random_xor_parity:
   assumes V:"finite V"
   assumes \<omega>: "\<omega> \<noteq> \<omega>'" "\<omega> \<subseteq> V" "\<omega>' \<subseteq> V"
   shows "prob_space.prob (random_xor V)
     {c. satisfies_xor c \<omega> = b \<and> satisfies_xor c \<omega>' = b'} = 1 / 4"
 proof -
   obtain x where "x \<notin> \<omega> \<and> x \<in> \<omega>' \<or> x \<notin> \<omega>' \<and> x \<in> \<omega>"
     using \<omega>
     by blast
   moreover {
     assume x: "x \<notin> \<omega>" "x \<in> \<omega>'"
     have ?thesis using pair_satisfies_random_xor_parity_1[OF V x \<omega>(2-3)]
       by blast
   }
   moreover {
     assume x: "x \<notin> \<omega>'" "x \<in> \<omega>"
     then have ?thesis using pair_satisfies_random_xor_parity_1[OF V x \<omega>(3) \<omega>(2)]
       by (simp add: Collect_conj_eq Int_commute)
   }
   ultimately show ?thesis by auto
 qed
 
 lemma prob_pmf_of_set_nonempty_parity_UNIV:
   assumes "finite V"
   assumes "x \<in> \<omega>" "\<omega> \<subseteq> V"
   shows "prob_space.prob (pmf_of_set (Pow V))
     {c. even (card (c \<inter> \<omega>)) = b} = 1 / 2"
   using prob_pmf_of_set_nonempty_parity[OF assms, of UNIV]
   by auto
 
 lemma prob_Pow_split:
   assumes "\<omega> \<subseteq> V" "finite V"
   shows "prob_space.prob (pmf_of_set (Pow V))
     {x. P (\<omega> \<inter> x) \<and> Q ((V - \<omega>) \<inter> x)} =
   prob_space.prob (pmf_of_set (Pow \<omega>))
     {x. P x} *
   prob_space.prob (pmf_of_set (Pow (V - \<omega>)))
     {x. Q x}"
 proof -
   have 1: "set_pmf (pmf_of_set (Pow \<omega>)) = Pow \<omega>"
     by (meson Pow_not_empty assms(1) assms(2) finite_Pow_iff finite_subset set_pmf_of_set)
   have 2: "set_pmf
          (pmf_of_set (Pow (V - \<omega>))) = Pow (V - \<omega> )"
     by (simp add: Pow_not_empty assms(2))
 
   have *: "(pmf_of_set (Pow \<omega> \<times> Pow (V - \<omega>))) =
      (pair_pmf (pmf_of_set (Pow \<omega>)) (pmf_of_set (Pow (V - \<omega>))))"
     unfolding 1 2
     apply (subst pmf_of_set_prod)
     using assms rev_finite_subset by auto
   have **: "(((\<lambda>(x, y). x \<union> y) -`
       {x. P (\<omega> \<inter> x) \<and> Q ((V - \<omega>) \<inter> x)}) \<inter> ((Pow \<omega>) \<times> (Pow (V - \<omega>)))) =
     ({x. P x} \<inter> Pow \<omega>) \<times> ({x. Q x} \<inter> Pow (V - \<omega>))"
     apply (rule antisym)
     subgoal
       apply clarsimp
       by (smt (verit) Diff_disjoint Int_Un_eq(4) inf.orderE inf_commute inf_sup_distrib1 sup_bot.right_neutral sup_commute)
     apply (intro subsetI)
     apply clarsimp
     by (smt (verit, ccfv_threshold) Diff_Int Diff_disjoint Diff_empty Diff_eq_empty_iff Un_Int_assoc_eq Un_commute sup_bot.left_neutral)
 
   have "prob_space.prob (pmf_of_set (Pow V))
     {x. P (\<omega> \<inter> x) \<and> Q ((V - \<omega>) \<inter> x)} =
     prob_space.prob (map_pmf (\<lambda>(x,y). x \<union> y)
       (pmf_of_set (Pow \<omega> \<times> Pow (V - \<omega>))))
     {x. P (\<omega> \<inter> x) \<and>  Q ((V - \<omega>) \<inter> x)}"
     apply (subst pmf_of_set_powerset_split[symmetric, OF assms(1-2)])
     by auto
   moreover have "... =
     measure_pmf.prob
      (pair_pmf (pmf_of_set (Pow \<omega>)) (pmf_of_set (Pow (V - \<omega>))))
      ((\<lambda>(x, y). x \<union> y) -`
       {x. P (\<omega> \<inter> x) \<and> Q ((V - \<omega>) \<inter> x)})"
     unfolding measure_map_pmf
     using *
     by presburger
   moreover have "... =
     measure_pmf.prob
      (pair_pmf (pmf_of_set (Pow \<omega>)) (pmf_of_set (Pow (V - \<omega>))))
      (((\<lambda>(x, y). x \<union> y) -`
       {x. P (\<omega> \<inter> x) \<and> Q ((V - \<omega>) \<inter> x)}) \<inter> ((Pow \<omega>) \<times> (Pow (V - \<omega>))))"
     using 1 2
     by (smt (verit) Int_Collect Int_def Sigma_cong inf_idem measure_pmf.measure_pmf_eq set_pair_pmf)
   moreover have "... =
      measure_pmf.prob
      (pair_pmf (pmf_of_set (Pow \<omega>)) (pmf_of_set (Pow (V - \<omega>))))
       (({x. P x} \<inter> Pow \<omega>) \<times> ({x. Q x} \<inter> Pow (V - \<omega>)))"
     unfolding **
     by auto
   moreover have "... =
      measure_pmf.prob
      (pmf_of_set (Pow \<omega>)) ({x. P x} \<inter> Pow \<omega>) *
      measure_pmf.prob
      (pmf_of_set (Pow (V - \<omega>))) ({x. Q x} \<inter> Pow (V - \<omega>))"
     apply (intro measure_pmf_prob_product)
     subgoal by (meson assms(1) assms(2) countable_finite finite_Int finite_Pow_iff rev_finite_subset)
     by (simp add: assms(2) countable_finite)
   moreover have "... =
      measure_pmf.prob
      (pmf_of_set (Pow \<omega>)) {x. P x} *
      measure_pmf.prob
      (pmf_of_set (Pow (V - \<omega>))) {x. Q x}"
     by (metis "1" "2" measure_Int_set_pmf)
   ultimately show ?thesis by auto
 qed
 
 (* Split probability for two disjoint non-empty sets *)
 lemma disjoint_prob_pmf_of_set_nonempty:
   assumes \<omega>: "x \<in> \<omega>" "\<omega> \<subseteq> V"
   assumes \<omega>': "x' \<in> \<omega>'" "\<omega>' \<subseteq> V"
   assumes "\<omega> \<inter> \<omega>' = {}"
   assumes V: "finite V"
   shows "prob_space.prob (pmf_of_set (Pow V))
     {c. even (card (\<omega> \<inter> c)) = b \<and> even (card (\<omega>' \<inter> c)) = b'} = 1 / 4"
 proof -
   have "prob_space.prob (pmf_of_set (Pow V))
     {c. even (card (\<omega> \<inter> c)) = b \<and> even (card (\<omega>' \<inter> c)) = b'} =
     prob_space.prob (pmf_of_set (Pow V))
     {c. even (card (\<omega> \<inter> c)) = b \<and> even (card (((V - \<omega>) \<inter> c) \<inter> \<omega>')) = b'}"
     by (smt (verit) Collect_cong Diff_Diff_Int Diff_eq_empty_iff Int_Diff Int_commute \<omega>'(2) assms(5) inf.orderE)
 
   moreover have "... =
     measure_pmf.prob (pmf_of_set (Pow \<omega>))
      {x. even (card x) = b} *
     measure_pmf.prob (pmf_of_set (Pow (V - \<omega>)))
      {x. even (card (x \<inter> \<omega>')) = b'}"
     apply (subst prob_Pow_split)
     using assms by auto
   moreover have "... =
     measure_pmf.prob (pmf_of_set (Pow \<omega>))
      {x. even (card (x \<inter> \<omega>)) = b} *
     measure_pmf.prob (pmf_of_set (Pow (V - \<omega>)))
      {x. even (card (x \<inter> \<omega>')) = b'} "
     by (smt (verit, best) PowD Pow_not_empty \<omega>(2) assms(6) finite_Pow_iff inf.orderE measure_pmf.measure_pmf_eq mem_Collect_eq rev_finite_subset set_pmf_of_set)
 
    moreover have "... = 1/4"
     apply (subst prob_pmf_of_set_nonempty_parity_UNIV[OF _ \<omega>(1)])
      subgoal using assms rev_finite_subset by blast
      subgoal by simp
     apply (subst prob_pmf_of_set_nonempty_parity_UNIV)
     using assms by auto
   ultimately show ?thesis by auto
 qed
 
 lemma measure_pmf_prob_product_finite_set_pmf:
   assumes "finite (set_pmf M)" "finite (set_pmf N)"
   shows "measure_pmf.prob (pair_pmf M N) (A \<times> B) =
   measure_pmf.prob M A * measure_pmf.prob N B"
 proof -
   have A: "measure_pmf.prob M A = measure_pmf.prob M (A \<inter> set_pmf M)"
     by (simp add: measure_Int_set_pmf)
   have B: "measure_pmf.prob N B = measure_pmf.prob N (B \<inter> set_pmf N)"
     by (simp add: measure_Int_set_pmf)
   have "measure_pmf.prob M A * measure_pmf.prob N B =
     measure_pmf.prob M (A \<inter> set_pmf M) *  measure_pmf.prob N (B \<inter> set_pmf N)"
     using A B by auto
   moreover have "... = measure_pmf.prob (pair_pmf M N)
      ((A \<inter> set_pmf M) \<times> (B \<inter> set_pmf N))"
     apply (subst measure_pmf_prob_product[symmetric])
     by auto
   moreover have "... = measure_pmf.prob (pair_pmf M N)
      ((A \<times> B) \<inter> set_pmf (pair_pmf M N))"
     by (simp add: Times_Int_Times)
   moreover have "... = measure_pmf.prob (pair_pmf M N)
      ((A \<times> B) )"
     using measure_Int_set_pmf by blast
   ultimately show ?thesis by auto
 qed
 
 lemma prob_random_xor_split_space:
   assumes "\<omega> \<subseteq> V" "finite V"
   shows "prob_space.prob (random_xor V)
     {(x,b). P (\<omega> \<inter> x) b \<and> Q ((V - \<omega>) \<inter> x)} =
   prob_space.prob (random_xor \<omega>)
     {(x,b). P x b} *
   prob_space.prob (pmf_of_set (Pow (V - \<omega>)))
     {x. Q x}"
 proof -
   have d1: "set_pmf (random_xor \<omega>) = Pow \<omega> \<times> UNIV"
     by (metis assms(1) assms(2) infinite_super set_pmf_random_xor)
   have d2: "set_pmf (pmf_of_set (Pow (V - \<omega>))) = Pow (V- \<omega>)"
     by (simp add: Pow_not_empty assms(2))
   have rhs: "prob_space.prob (random_xor \<omega>)
     {(x,b). P x b} *
   prob_space.prob (pmf_of_set (Pow (V - \<omega>)))
     {x. Q x} =
   prob_space.prob (pair_pmf (random_xor \<omega>) (pmf_of_set (Pow (V - \<omega>))))
     ({(x,b). P x b} \<times> {x. Q x})"
     apply (subst measure_pmf_prob_product_finite_set_pmf)
     subgoal by (metis Pow_def assms(1) assms(2) finite_Collect_subsets finite_SigmaI finite_code rev_finite_subset set_pmf_random_xor)
     using assms by (auto simp add: Pow_not_empty)
 
   from pmf_of_set_powerset_split[OF assms]
   have *: "pmf_of_set (Pow V) =
     map_pmf (\<lambda>(x, y). x \<union> y)
    (pair_pmf (pmf_of_set (Pow \<omega>)) (pmf_of_set (Pow (V - \<omega>))))"
     by (metis Pow_not_empty assms(1) assms(2) finite_Diff finite_Pow_iff pmf_of_set_prod rev_finite_subset)
 
   have **: "random_xor V =
     map_pmf (\<lambda>((x,b),y). (x \<union> y,b)) (pair_pmf (random_xor \<omega>) (pmf_of_set (Pow (V - \<omega>))))"
     unfolding random_xor_def *
     including monad_normalisation
     by (auto simp add: pair_pmf_def map_pmf_def case_prod_unfold)
 
   have "prob_space.prob (random_xor V) {(x,b). P (\<omega> \<inter> x) b \<and> Q ((V - \<omega>) \<inter> x)} =
     measure_pmf.prob
      (pair_pmf (random_xor \<omega>) (pmf_of_set (Pow (V - \<omega>))))
      {y. P (\<omega> \<inter> (fst (fst y) \<union> snd y)) (snd (fst y)) \<and>
          Q ((V - \<omega>) \<inter> (fst (fst y) \<union> snd y))}"
     unfolding **
     by (auto simp add:case_prod_unfold)
 
   moreover have "... =
   prob_space.prob (pair_pmf (random_xor \<omega>) (pmf_of_set (Pow (V - \<omega>))))
     ({(x,b). P x b} \<times> {x. Q x})"
     apply (intro measure_pmf.measure_pmf_eq[where p ="pair_pmf (random_xor \<omega>)
        (pmf_of_set (Pow (V - \<omega>)))"])
     subgoal by simp
     apply (clarsimp simp add: d1 d2)
     by (smt (verit, del_insts) Diff_disjoint Int_Diff boolean_algebra_cancel.sup0 inf.orderE inf_commute inf_sup_distrib1 sup_bot.left_neutral)
   ultimately show ?thesis using rhs
     by simp
 qed
 
 lemma three_disjoint_prob_random_xor_nonempty:
   assumes \<omega>: "\<omega> \<noteq> {}" "\<omega> \<subseteq> V"
   assumes \<omega>': "\<omega>' \<noteq> {}" "\<omega>' \<subseteq> V"
   assumes I: "I \<subseteq> V"
   assumes int: "I \<inter> \<omega> = {}" "I \<inter> \<omega>' = {}" "\<omega> \<inter> \<omega>' = {}"
   assumes V: "finite V"
   shows "prob_space.prob (random_xor V)
     {c. satisfies_xor c I = b \<and>
       even (card (\<omega> \<inter> fst c)) = b' \<and>
       even (card (\<omega>' \<inter> fst c)) = b''} = 1 / 8"
 proof -
   have finI: "finite I"
     using V I
     using rev_finite_subset by blast
   have finVI: "finite (V - I)"
     using V I
     using rev_finite_subset by blast
   obtain x x' where x: "x \<in> \<omega>" "x' \<in> \<omega>'" using \<omega> \<omega>'
     by blast
 
   have rw1:"\<omega> \<inter> ((V - I) \<inter> xx) = \<omega> \<inter>  xx " for xx
     by (metis Diff_Int_distrib2 Diff_empty \<omega>(2) assms(6) inf.absorb_iff2 inf_assoc inf_left_commute)
 
   have rw2:"\<omega>' \<inter> ((V - I) \<inter> xx)= \<omega>' \<inter>  xx" for xx
     by (metis Diff_Int_distrib2 Diff_empty \<omega>'(2) assms(7) inf.absorb_iff2 inf_assoc inf_left_commute)
 
   have "prob_space.prob (random_xor V)
     {c. satisfies_xor c I = b \<and>
       even (card ( \<omega> \<inter> fst c )) = b' \<and>
       even (card (\<omega>' \<inter>  fst c )) = b''} =
     prob_space.prob (random_xor V)
     {(x,bb). satisfies_xor (I \<inter> x, bb) I = b \<and>
       even (card (\<omega> \<inter> ((V - I) \<inter> x))) = b' \<and>
       even (card ( \<omega>' \<inter> ((V - I) \<inter> x))) = b''}"
     apply (intro arg_cong[where f = "prob_space.prob (random_xor V)"])
     unfolding rw1 rw2 satisfies_xor_inter
     by (smt (verit) Collect_cong prod.collapse split_conv)
 
   moreover have "... =
     measure_pmf.prob (random_xor I)
      {c. satisfies_xor c I = b} *
     measure_pmf.prob (pmf_of_set (Pow (V - I)))
      {x. even (card (\<omega> \<inter> x)) = b' \<and>
          even (card (\<omega>' \<inter> x)) = b''}"
     apply (subst prob_random_xor_split_space[OF I V])
     by (metis (no_types, lifting) Collect_cong case_prodE case_prodI2)
   moreover have "... = 1 / 8"
     apply (subst satisfies_random_xor_parity[OF finI])
     apply (subst disjoint_prob_pmf_of_set_nonempty)
     using x \<omega> \<omega>' int finVI by auto
   ultimately show ?thesis by auto
 qed
 
 (* Split probability for three disjoint non-empty sets *)
 lemma three_disjoint_prob_pmf_of_set_nonempty:
   assumes \<omega>: "x \<in> \<omega>" "\<omega> \<subseteq> V"
   assumes \<omega>': "x' \<in> \<omega>'" "\<omega>' \<subseteq> V"
   assumes \<omega>'': "x'' \<in> \<omega>''" "\<omega>'' \<subseteq> V"
   assumes int: "\<omega> \<inter> \<omega>' = {}" "\<omega>' \<inter> \<omega>'' = {}" "\<omega>'' \<inter> \<omega> = {}"
   assumes V: "finite V"
   shows "prob_space.prob (pmf_of_set (Pow V))
     {c. even (card (\<omega> \<inter> c)) = b \<and> even (card (\<omega>' \<inter> c)) = b' \<and> even (card (\<omega>'' \<inter> c)) = b''} = 1 / 8"
 proof -
   have "prob_space.prob (pmf_of_set (Pow V))
     {c. even (card (\<omega> \<inter> c)) = b \<and> even (card (\<omega>' \<inter> c)) = b' \<and> even (card (\<omega>'' \<inter> c)) = b''} =
     prob_space.prob (pmf_of_set (Pow V))
     {c. even (card (\<omega> \<inter> c)) = b \<and>
         even (card (((V - \<omega>) \<inter> c) \<inter> \<omega>')) = b' \<and>
         even (card (((V - \<omega>) \<inter> c) \<inter> \<omega>'')) = b''}"
     by (smt (verit,best) Collect_cong Diff_Diff_Int Diff_eq_empty_iff Int_Diff Int_commute \<omega>' \<omega>'' int inf.orderE)
 
   moreover have "... =
     measure_pmf.prob (pmf_of_set (Pow \<omega>))
      {x. even (card x) = b} *
     measure_pmf.prob (pmf_of_set (Pow (V - \<omega>)))
      {x. even (card (\<omega>' \<inter> x)) = b' \<and> even (card (\<omega>'' \<inter> x)) = b''}"
     apply (subst prob_Pow_split)
     using assms by (auto simp add: inf.commute)
   moreover have "... =
     measure_pmf.prob (pmf_of_set (Pow \<omega>))
      {x. even (card (x \<inter> \<omega>)) = b} *
     measure_pmf.prob (pmf_of_set (Pow (V - \<omega>)))
      {x. even (card (\<omega>' \<inter> x)) = b'\<and> even (card (\<omega>'' \<inter> x)) = b''} "
     by (smt (verit, best) PowD Pow_not_empty \<omega> V finite_Pow_iff inf.orderE measure_pmf.measure_pmf_eq mem_Collect_eq rev_finite_subset set_pmf_of_set)
 
    moreover have "... = 1/8"
     apply (subst prob_pmf_of_set_nonempty_parity_UNIV[OF _ \<omega>(1)])
      subgoal using \<omega>(2) V rev_finite_subset by blast
      subgoal by simp
      apply (subst disjoint_prob_pmf_of_set_nonempty)
      using assms by auto
   ultimately show ?thesis by auto
 qed
 
 lemma four_disjoint_prob_random_xor_nonempty:
   assumes \<omega>: "\<omega> \<noteq> {}" "\<omega> \<subseteq> V"
   assumes \<omega>': "\<omega>' \<noteq> {}" "\<omega>' \<subseteq> V"
   assumes \<omega>'': "\<omega>'' \<noteq> {}" "\<omega>'' \<subseteq> V"
   assumes I: "I \<subseteq> V"
   assumes int: "I \<inter> \<omega> = {}" "I \<inter> \<omega>' = {}" "I \<inter> \<omega>'' = {}"
     "\<omega> \<inter> \<omega>' = {}" "\<omega>' \<inter> \<omega>'' = {}" "\<omega>'' \<inter> \<omega> = {}"
   assumes V: "finite V"
   shows "prob_space.prob (random_xor V)
     {c. satisfies_xor c I = b0 \<and>
       even (card (\<omega> \<inter> fst c)) = b \<and>
       even (card (\<omega>' \<inter> fst c)) = b' \<and>
       even (card (\<omega>'' \<inter> fst c)) = b''} = 1 / 16"
 proof -
   have finI: "finite I"
     using V I
     using rev_finite_subset by blast
   have finVI: "finite (V - I)"
     using V I
     using rev_finite_subset by blast
   obtain x x' x'' where x: "x \<in> \<omega>" "x' \<in> \<omega>'" "x'' \<in> \<omega>''"
     using \<omega> \<omega>' \<omega>''
     by blast
 
   have rw1:"\<omega> \<inter> ((V - I) \<inter> xx) = \<omega> \<inter>  xx " for xx
     by (metis Diff_Int_distrib2 Diff_empty \<omega>(2) int(1) inf.absorb_iff2 inf_assoc inf_left_commute)
 
   have rw2:"\<omega>' \<inter> ((V - I) \<inter> xx)= \<omega>' \<inter>  xx" for xx
     by (metis Diff_Int_distrib2 Diff_empty \<omega>'(2) int(2) inf.absorb_iff2 inf_assoc inf_left_commute)
 
   have rw3:"\<omega>'' \<inter> ((V - I) \<inter> xx)= \<omega>'' \<inter>  xx" for xx
     by (metis Diff_Int_distrib2 Diff_empty \<omega>''(2) int(3) inf.absorb_iff2 inf_assoc inf_left_commute)
 
   have "prob_space.prob (random_xor V)
     {c. satisfies_xor c I = b0 \<and>
       even (card (\<omega> \<inter> fst c)) = b \<and>
       even (card (\<omega>' \<inter>  fst c)) = b' \<and>
       even (card (\<omega>'' \<inter>  fst c)) = b''} =
     prob_space.prob (random_xor V)
     {(x,bb). satisfies_xor (I \<inter> x, bb) I = b0 \<and>
       even (card (\<omega> \<inter> ((V - I) \<inter> x))) = b \<and>
       even (card (\<omega>' \<inter> ((V - I) \<inter> x))) = b' \<and>
       even (card (\<omega>'' \<inter> ((V - I) \<inter> x))) = b''}"
     apply (intro arg_cong[where f = "prob_space.prob (random_xor V)"])
     unfolding rw1 rw2 rw3 satisfies_xor_inter
     by (smt (verit) Collect_cong prod.collapse split_conv)
 
   moreover have "... =
     measure_pmf.prob (random_xor I)
      {c. satisfies_xor c I = b0} *
     measure_pmf.prob (pmf_of_set (Pow (V - I)))
      {x. even (card (\<omega> \<inter> x)) = b \<and>
          even (card (\<omega>' \<inter> x)) = b' \<and>
          even (card (\<omega>'' \<inter> x)) = b''}"
     apply (subst prob_random_xor_split_space[OF I V])
     by (metis (no_types, lifting) Collect_cong case_prodE case_prodI2)
   moreover have "... = 1 / 16"
     apply(subst satisfies_random_xor_parity[OF finI])
     apply (subst three_disjoint_prob_pmf_of_set_nonempty)
     using x \<omega> \<omega>' \<omega>'' int finVI by auto
   ultimately show ?thesis by auto
 qed
 
 lemma three_satisfies_random_xor_parity_1:
   assumes V:"finite V"
   assumes \<omega>: "\<omega> \<subseteq> V" "\<omega>' \<subseteq> V" "\<omega>'' \<subseteq> V"
   assumes x: "x \<notin> \<omega>" "x \<notin> \<omega>'" "x \<in> \<omega>''"
   assumes d: "\<omega> \<noteq> \<omega>'"
   shows "prob_space.prob (random_xor V)
     {c.
     satisfies_xor c \<omega> = b \<and>
     satisfies_xor c \<omega>' = b' \<and>
     satisfies_xor c \<omega>'' = b''} = 1 / 8"
 proof -
   have wa: "\<omega> \<inter> (a - {x}) = \<omega> \<inter> a" for a
     using x
     by blast
   have wa': "\<omega>' \<inter> (a - {x}) = \<omega>' \<inter> a" for a
     using x
     by blast
   have "prob_space.prob (random_xor V)
     {c.
       satisfies_xor c \<omega> = b \<and> satisfies_xor c \<omega>' = b' \<and>
       satisfies_xor c \<omega>'' = b''} =
     prob_space.prob (random_xor V)
     ({c. satisfies_xor c \<omega> = b \<and> satisfies_xor c \<omega>' = b'} \<inter>
       {c. satisfies_xor c \<omega>'' = b''})"
     by (simp add: Collect_conj_eq inf_assoc)
   moreover have "... =
     1 / 2 *
     measure_pmf.prob (random_xor (V - {x}))
       {c. satisfies_xor c \<omega> = b \<and> satisfies_xor c \<omega>' = b'}"
     apply (subst prob_random_xor_nonempty_parity[OF V x(3) \<omega>(3)])
     by (auto simp add: wa wa')
   moreover have "... = 1/8"
     apply (subst pair_satisfies_random_xor_parity)
     using V \<omega> x d by auto
   ultimately show ?thesis by auto
 qed
 
 lemma split_boolean_eq:
   shows"(A \<longleftrightarrow> B) = (b \<longleftrightarrow> I) \<and>
     (B \<longleftrightarrow> C) = (b' \<longleftrightarrow>  I) \<and>
     (C \<longleftrightarrow> A) = (b'' \<longleftrightarrow> I)
   \<longleftrightarrow>
     I = odd(of_bool b + of_bool b' + of_bool b'') \<and>
      (A = True \<and>
       B = (b'=b'') \<and>
       C = (b = b') \<or>
       A = False \<and>
       B = (b' \<noteq> b'') \<and>
       C = (b \<noteq> b'))"
   by auto
 
 lemma three_satisfies_random_xor_parity:
   assumes V:"finite V"
   assumes \<omega>:
       "\<omega> \<noteq> \<omega>'" "\<omega> \<noteq> \<omega>''" "\<omega>' \<noteq> \<omega>''"
       "\<omega> \<subseteq> V" "\<omega>' \<subseteq> V" "\<omega>'' \<subseteq> V"
   shows "prob_space.prob (random_xor V)
     {c. satisfies_xor c \<omega> = b \<and>
         satisfies_xor c \<omega>' = b' \<and>
         satisfies_xor c \<omega>'' = b''} = 1 / 8"
 proof -
   have "(\<exists>x.
     x \<in> \<omega> \<and> x \<notin> \<omega>' \<and> x \<notin> \<omega>'' \<or>
     x \<in> \<omega>' \<and> x \<notin> \<omega> \<and> x \<notin> \<omega>'' \<or>
     x \<in> \<omega>'' \<and> x \<notin> \<omega> \<and> x \<notin> \<omega>') \<or>
     \<omega> - (\<omega>' \<union> \<omega>'') = {} \<and>
     \<omega>' - (\<omega> \<union> \<omega>'') = {} \<and>
     \<omega>'' - (\<omega> \<union> \<omega>') = {}"
     by blast
   moreover {
     assume "(\<exists>x.
     x \<in> \<omega> \<and> x \<notin> \<omega>' \<and> x \<notin> \<omega>'' \<or>
     x \<in> \<omega>' \<and> x \<notin> \<omega> \<and> x \<notin> \<omega>'' \<or>
     x \<in> \<omega>'' \<and> x \<notin> \<omega> \<and> x \<notin> \<omega>')"
     then obtain x where "
       x \<in> \<omega> \<and> x \<notin> \<omega>' \<and> x \<notin> \<omega>'' \<or>
       x \<in> \<omega>' \<and> x \<notin> \<omega> \<and> x \<notin> \<omega>'' \<or>
       x \<in> \<omega>'' \<and> x \<notin> \<omega> \<and> x \<notin> \<omega>'" by auto
     moreover {
       assume x: "x \<notin> \<omega>'" "x \<notin> \<omega>''" "x \<in> \<omega>"
       have "measure_pmf.prob (random_xor V)
        {c. satisfies_xor c \<omega>' = b' \<and>
            satisfies_xor c \<omega>'' = b'' \<and>
            satisfies_xor c \<omega> = b} = 1 / 8"
         apply (intro three_satisfies_random_xor_parity_1[OF V _ _ _ x])
         using \<omega> by auto
       then have ?thesis
         by (smt (verit, ccfv_SIG) Collect_cong)
     }
     moreover {
       assume x: "x \<notin> \<omega>" "x \<notin> \<omega>''" "x \<in> \<omega>'"
       have "measure_pmf.prob (random_xor V)
        {c. satisfies_xor c \<omega> = b \<and>
            satisfies_xor c \<omega>'' = b'' \<and>
            satisfies_xor c \<omega>' = b'} = 1 / 8"
         apply (intro three_satisfies_random_xor_parity_1[OF V _ _ _ x])
         using \<omega> by auto
       then have ?thesis
         by (smt (verit, ccfv_SIG) Collect_cong)
     }
     moreover {
       assume x: "x \<notin> \<omega>" "x \<notin> \<omega>'" "x \<in> \<omega>''"
       have "measure_pmf.prob (random_xor V)
        {c. satisfies_xor c \<omega> = b \<and>
            satisfies_xor c \<omega>' = b' \<and>
            satisfies_xor c \<omega>'' = b''} = 1 / 8"
         apply (intro three_satisfies_random_xor_parity_1[OF V _ _ _ x])
         using \<omega> by auto
       then have ?thesis
         by (smt (verit, ccfv_SIG) Collect_cong)
     }
     ultimately have ?thesis by auto
   }
   moreover {
     assume dis: "\<omega> - (\<omega>' \<union> \<omega>'') = {} \<and>
       \<omega>' - (\<omega> \<union> \<omega>'') = {} \<and>
       \<omega>'' - (\<omega> \<union> \<omega>') = {}"
 
     define A where "A = (\<omega> \<inter> \<omega>'') - \<omega>'"
     define B where "B = (\<omega> \<inter> \<omega>') - \<omega>''"
     define C where "C = (\<omega>' \<inter> \<omega>'') - \<omega>"
     define I where "I = \<omega> \<inter> \<omega>' \<inter> \<omega>''"
 
     have f: "finite A" "finite B" "finite C" "finite I"
       unfolding A_def B_def C_def I_def
       by (meson V \<omega> finite_Diff finite_Int rev_finite_subset)+
 
     have s: "A \<subseteq> V" "B \<subseteq> V" "C \<subseteq> V" "I \<subseteq> V"
       unfolding A_def B_def C_def I_def
       using \<omega> by auto
 
     have i: "I \<inter> A = {}" "I \<inter> B = {}" "I \<inter> C = {}"
         "B \<inter> C = {}" "C \<inter> A = {}" "A \<inter> B = {}"
       unfolding A_def B_def C_def I_def
       by blast +
 
     have s1: "\<omega> = A \<union> B \<union> I"
       unfolding A_def B_def I_def
       using dis by auto
     have sx1: "satisfies_xor (xx,bb) \<omega> = b \<longleftrightarrow>
       even (card (A \<inter> xx)) = even (card (B \<inter> xx)) = (b \<longleftrightarrow> satisfies_xor(xx,bb) I)" for xx bb
       unfolding s1 satisfies_xor.simps Int_Un_distrib2
       apply (subst card_Un_disjoint)
       subgoal using f by auto
       subgoal using f by auto
       subgoal using A_def B_def I_def by blast
       apply (subst card_Un_disjoint)
       subgoal using f by auto
       subgoal using f by auto
       subgoal using A_def B_def I_def by blast
       by auto
 
     have s2: "\<omega>' = B \<union> C \<union> I"
       unfolding B_def C_def I_def
       using dis by auto
     have sx2: "satisfies_xor (xx,bb) \<omega>' = b' \<longleftrightarrow>
       even (card (B \<inter> xx)) = even (card (C \<inter> xx)) = (b' \<longleftrightarrow> satisfies_xor(xx,bb) I)" for xx bb
       unfolding s2 satisfies_xor.simps Int_Un_distrib2
       apply (subst card_Un_disjoint)
       subgoal using f by auto
       subgoal using f by auto
       subgoal using B_def C_def I_def by blast
       apply (subst card_Un_disjoint)
       subgoal using f by auto
       subgoal using f by auto
       subgoal using B_def C_def I_def by blast
       by auto
 
     have s3: "\<omega>'' = A \<union> C \<union> I"
       unfolding A_def C_def I_def
       using dis by auto
     have sx3: "satisfies_xor (xx,bb) \<omega>'' = b'' \<longleftrightarrow>
       even (card (C \<inter> xx)) = even (card (A \<inter> xx)) = (b'' \<longleftrightarrow> satisfies_xor(xx,bb) I)" for xx bb
       unfolding s3 satisfies_xor.simps Int_Un_distrib2
       apply (subst card_Un_disjoint)
       subgoal using f by auto
       subgoal using f by auto
       subgoal using A_def B_def C_def I_def by blast
       apply (subst card_Un_disjoint)
       subgoal using f by auto
       subgoal using f by auto
       subgoal using A_def B_def C_def I_def by blast
       by auto
 
     have "A = {} \<and> B \<noteq> {} \<and> C \<noteq> {} \<or>
       A \<noteq> {} \<and> B = {} \<and> C \<noteq> {} \<or>
       A \<noteq> {} \<and> B \<noteq> {} \<and> C = {} \<or>
       A \<noteq> {} \<and> B \<noteq> {} \<and> C \<noteq> {}"
       by (metis Un_commute \<omega>(1) \<omega>(2) \<omega>(3) s1 s2 s3)
 
     moreover {
       assume as: "A = {}" "B \<noteq> {}" "C \<noteq> {}"
       have "satisfies_xor (xx,bb) \<omega> = b
         \<and> satisfies_xor (xx,bb) \<omega>' = b'
         \<and> satisfies_xor (xx,bb) \<omega>'' = b'' \<longleftrightarrow>
       (satisfies_xor (xx, bb) I =
        odd (of_bool b + of_bool b' + of_bool b'') \<and>
        (even (card (B \<inter> xx)) = (b' = b'') \<and>
         even (card (C \<inter> xx)) = (b = b')))" for xx bb
         unfolding sx1 sx2 sx3
         apply(subst split_boolean_eq)
         using as by simp
       then have *: "{c. satisfies_xor c \<omega> = b
         \<and> satisfies_xor c \<omega>' = b'
         \<and> satisfies_xor c \<omega>'' = b''} =
       {c. satisfies_xor c I =
        odd (of_bool b + of_bool b' + of_bool b'') \<and>
        even (card (B \<inter> fst c)) = (b' = b'') \<and>
        even (card (C \<inter> fst c)) = (b = b')}"
         by (smt (verit,best) Collect_cong prod.collapse)
       have ?thesis
         apply (subst *)
         apply (intro three_disjoint_prob_random_xor_nonempty)
         using as s i V by auto
     }
 
     moreover {
       assume as: "A \<noteq> {}" "B \<noteq> {}" "C = {}"
       have "satisfies_xor (xx,bb) \<omega>'' = b''
         \<and> satisfies_xor (xx,bb) \<omega> = b
         \<and> satisfies_xor (xx,bb) \<omega>' = b' \<longleftrightarrow>
       (satisfies_xor (xx, bb) I =
        odd (of_bool b'' + of_bool b + of_bool b') \<and>
        (even (card (A \<inter> xx)) = (b = b') \<and>
         even (card (B \<inter> xx)) = (b'' = b)))" for xx bb
         unfolding sx1 sx2 sx3
         apply(subst split_boolean_eq)
         using as by simp
       then have *: "{c. satisfies_xor c \<omega> = b
         \<and> satisfies_xor c \<omega>' = b'
         \<and> satisfies_xor c \<omega>'' = b''} =
       {c. satisfies_xor c I =
        odd (of_bool b'' + of_bool b + of_bool b') \<and>
        (even (card (A \<inter> fst c)) = (b = b') \<and>
         even (card (B \<inter> fst c)) = (b'' = b))}"
         by (smt (verit,best) Collect_cong prod.collapse)
       have ?thesis
         apply (subst *)
         apply (intro three_disjoint_prob_random_xor_nonempty)
         using as s i V by auto
     }
 
     moreover {
       assume as: "A \<noteq> {}" "B = {}" "C \<noteq> {}"
       have "satisfies_xor (xx,bb) \<omega>' = b'
         \<and> satisfies_xor (xx,bb) \<omega>'' = b''
         \<and> satisfies_xor (xx,bb) \<omega> = b \<longleftrightarrow>
       (satisfies_xor (xx, bb) I =
        odd (of_bool b' + of_bool b'' + of_bool b) \<and>
        (even (card (C \<inter> xx)) = (b'' = b) \<and>
         even (card (A \<inter> xx)) = (b' = b'')))" for xx bb
         unfolding sx1 sx2 sx3
         apply(subst split_boolean_eq)
         using as by simp
       then have *: "{c. satisfies_xor c \<omega> = b
         \<and> satisfies_xor c \<omega>' = b'
         \<and> satisfies_xor c \<omega>'' = b''} =
       {c. satisfies_xor c I =
        odd (of_bool b' + of_bool b'' + of_bool b) \<and>
        (even (card (C \<inter> fst c)) = (b'' = b) \<and>
         even (card (A \<inter> fst c)) = (b' = b''))}"
         by (smt (verit,best) Collect_cong prod.collapse)
       have ?thesis
         apply (subst *)
         apply (intro three_disjoint_prob_random_xor_nonempty)
         using as s i V by auto
     }
 
     moreover {
       assume as: "A \<noteq> {}" "B \<noteq> {}" "C \<noteq> {}"
       have 1: "satisfies_xor (xx,bb) \<omega> = b
         \<and> satisfies_xor (xx,bb) \<omega>' = b'
         \<and> satisfies_xor (xx,bb) \<omega>'' = b'' \<longleftrightarrow>
       (satisfies_xor (xx, bb) I =
         odd (of_bool b + of_bool b' + of_bool b'') \<and>
         even (card (A \<inter> xx)) = True \<and>
         even (card (B \<inter> xx)) = (b' = b'') \<and>
         even (card (C \<inter> xx)) = (b = b') \<or>
        satisfies_xor (xx, bb) I =
         odd (of_bool b + of_bool b' + of_bool b'') \<and>
         even (card (A \<inter> xx)) = False \<and>
         even (card (B \<inter> xx)) = (b' \<noteq> b'') \<and>
         even (card (C \<inter> xx)) = (b \<noteq> b'))" for xx bb
         unfolding sx1 sx2 sx3
         apply(subst split_boolean_eq)
         by auto
       have 2: "satisfies_xor c \<omega> = b
         \<and> satisfies_xor c \<omega>' = b'
         \<and> satisfies_xor c \<omega>'' = b'' \<longleftrightarrow>
       (satisfies_xor c I =
         odd (of_bool b + of_bool b' + of_bool b'') \<and>
         even (card (A \<inter> fst c)) = True \<and>
         even (card (B \<inter> fst c)) = (b' = b'') \<and>
         even (card (C \<inter> fst c)) = (b = b') \<or>
        satisfies_xor c I =
         odd (of_bool b + of_bool b' + of_bool b'') \<and>
         even (card (A \<inter> fst c)) = False \<and>
         even (card (B \<inter> fst c)) = (b' \<noteq> b'') \<and>
         even (card (C \<inter> fst c)) = (b \<noteq> b'))" for c
       proof -
         obtain xx bb where c:"c = (xx,bb)" by fastforce
         show ?thesis unfolding c
           apply (subst 1)
           by auto
       qed
       have *: "{c. satisfies_xor c \<omega> = b
         \<and> satisfies_xor c \<omega>' = b'
         \<and> satisfies_xor c \<omega>'' = b''} =
       {c. satisfies_xor c I =
         odd (of_bool b + of_bool b' + of_bool b'') \<and>
         even (card (A \<inter> fst c)) = True \<and>
         even (card (B \<inter> fst c)) = (b' = b'') \<and>
         even (card (C \<inter> fst c)) = (b = b')} \<union>
       {c. satisfies_xor c I =
         odd (of_bool b + of_bool b' + of_bool b'') \<and>
         even (card (A \<inter> fst c)) = False \<and>
         even (card (B \<inter> fst c)) = (b' \<noteq> b'') \<and>
         even (card (C \<inter> fst c)) = (b \<noteq> b')}"
         apply (subst Un_def)
         apply (intro Collect_cong)
         apply (subst 2)
         by simp
 
       have **: "1 / 16 +
         measure_pmf.prob (random_xor V)
          {c. satisfies_xor c I =
              odd (of_bool b + of_bool b' +
                   of_bool b'') \<and>
              even (card (A \<inter> fst c)) =
              False \<and>
              even (card (B \<inter> fst c)) =
              (b' \<noteq> b'') \<and>
              even (card (C \<inter> fst c)) =
              (b \<noteq> b')} =
         1 / 8" 
         apply (subst four_disjoint_prob_random_xor_nonempty)
         using as s i V by auto
       have ?thesis
         apply (subst *)
         apply (subst measure_pmf.finite_measure_Union)
         subgoal by simp
         subgoal by simp
         subgoal by auto
         apply (subst four_disjoint_prob_random_xor_nonempty)
         using as s i V ** by auto
     }
 
     ultimately have ?thesis by auto
   }
   ultimately show ?thesis by auto
 qed
 
 subsection "Independence for repeated XORs"
 
 text \<open> We can lift the previous result to a list of independent sampled XORs. \<close>
 
 definition random_xors :: "'a set \<Rightarrow> nat \<Rightarrow>
     (nat \<rightharpoonup> 'a set \<times> bool) pmf"
   where "random_xors V n =
     Pi_pmf {..<(n::nat)} None
       (\<lambda>_. map_pmf Some (random_xor V))"
 
 (* The set of random XORs expressed in various ways*)
 lemma random_xors_set:
   assumes V:"finite V"
   shows
     "PiE_dflt {..<n} None
       (set_pmf \<circ> (\<lambda>_. map_pmf Some (random_xor V))) =
      {xors. dom xors = {..<n} \<and>
         ran xors \<subseteq> (Pow V) \<times> UNIV}" (is "?lhs = ?rhs")
 proof -
   have "?lhs =
     {f. dom f = {..<n} \<and>
         (\<forall>x \<in> {..<n}. f x \<in> Some ` (Pow V \<times> UNIV))}"
     unfolding PiE_dflt_def o_def set_map_pmf set_pmf_random_xor[OF V]
     by force
 
   also have "... = ?rhs"
     apply (rule antisym)
     subgoal
       apply clarsimp
       by (smt (z3) PowD domI image_iff mem_Collect_eq mem_Sigma_iff option.simps(1) ran_def subsetD)
     apply clarsimp
     by (smt (verit, ccfv_threshold) domD image_iff lessThan_iff ranI subsetD)
   finally show ?thesis .
 qed
 
 lemma random_xors_eq:
   assumes V:"finite V"
   shows"random_xors V n =
     pmf_of_set
     {xors. dom xors = {..<n} \<and> ran xors \<subseteq> (Pow V) \<times> UNIV}"
 proof -
   have "pmf_of_set
     {xors. dom xors = {..<n} \<and>
         ran xors \<subseteq> (Pow V) \<times> UNIV} =
     pmf_of_set
       (PiE_dflt {..<n} None
       (set_pmf \<circ> (\<lambda>_. map_pmf Some (random_xor V))))"
     unfolding random_xors_set[OF V] by auto
   also have "... =
     Pi_pmf {..<n} None
      (\<lambda>x. pmf_of_set
             ((set_pmf \<circ>
               (\<lambda>_. map_pmf Some (random_xor V))) x))"
     apply (subst Pi_pmf_of_set[symmetric])
     by (auto simp add:set_pmf_random_xor[OF V] V)
   also have "... = random_xors V n"
     unfolding random_xors_def o_def set_map_pmf
     apply (subst map_pmf_of_set_inj[symmetric])
     subgoal by (auto simp add:set_pmf_random_xor[OF V] V)
     subgoal by (auto simp add:set_pmf_random_xor[OF V] V)
     subgoal by (auto simp add:set_pmf_random_xor[OF V] V)
     by (metis V random_xor_pmf_of_set set_pmf_random_xor)
   ultimately show ?thesis by auto
 qed
 
 (* The XOR hash function from a mapping nat \<rightharpoonup> XOR *)
 definition xor_hash ::
   "('a \<rightharpoonup> bool) \<Rightarrow>
    (nat \<rightharpoonup> ('a set \<times> bool)) \<Rightarrow>
    (nat \<rightharpoonup> bool)"
   where "xor_hash \<omega> xors =
       (map_option
         (\<lambda>xor. satisfies_xor xor {x. \<omega> x = Some True}) \<circ> xors)"
 
 lemma finite_map_set_nonempty:
   assumes "R \<noteq> {}"
   shows "
     {xors.
       dom xors = D \<and> ran xors \<subseteq> R} \<noteq> {}"
 proof -
   obtain r where "r \<in> R"
     using assms by blast
   then have "(\<lambda>x. if x \<in> D then Some r else None) \<in>
     {xors. dom xors = D \<and> ran xors \<subseteq> R}"
     by (auto split:if_splits simp:ran_def)
   thus ?thesis by auto
 qed
 
 lemma random_xors_set_pmf:
   assumes V: "finite V"
   shows "
     set_pmf (random_xors V n) =
       {xors. dom xors = {..<n} \<and>
         ran xors \<subseteq> (Pow V) \<times> UNIV}"
   unfolding random_xors_eq[OF V]
   apply (intro set_pmf_of_set)
   subgoal
     apply (intro finite_map_set_nonempty)
     by blast
   apply (intro finite_set_of_finite_maps)
   by (auto simp add: V)
 
 lemma finite_random_xors_set_pmf:
   assumes V: "finite V"
   shows "
     finite (set_pmf (random_xors V n))"
   unfolding random_xors_set_pmf[OF V]
   by (auto intro!: finite_set_of_finite_maps simp add: V)
 
 lemma map_eq_1:
   assumes "dom f = dom g"
   assumes "\<And>x. x \<in> dom f \<Longrightarrow> the (f x) = the (g x)"
   shows "f = g"
   by (metis assms(1) assms(2) domIff map_le_antisym map_le_def option.expand)
 
 lemma xor_hash_eq_iff:
   assumes "dom \<alpha> = {..<n}"
   shows"xor_hash \<omega> x = \<alpha> \<longleftrightarrow>
   (dom x = {..<n} \<and>
   (\<forall>i. i < n \<longrightarrow>
     (\<exists>xor. x i = Some xor \<and>
     satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> i))
   ))"
 proof -
   have 1: "xor_hash \<omega> x = \<alpha> \<longleftrightarrow>
     (dom (xor_hash \<omega> x) = dom \<alpha>) \<and>
     (\<forall>i \<in> dom \<alpha>. the (xor_hash \<omega> x i) = the (\<alpha> i))"
     using map_eq_1 by fastforce
   have 2: "dom (xor_hash \<omega> x) = dom x"
     unfolding xor_hash_def
     by auto
   have 3: "\<And>i. i \<in> dom x \<Longrightarrow>
     xor_hash \<omega> x i = Some (satisfies_xor (the (x i)) {x. \<omega> x = Some True})"
     unfolding xor_hash_def
     by fastforce
   show ?thesis 
     unfolding 1 assms 2
     using 3
     by (smt (verit, best) domD lessThan_iff option.sel)
 qed
 
 lemma xor_hash_eq_PiE_dflt:
   assumes "dom \<alpha> = {..<n}"
   shows
     "{xors. xor_hash \<omega> xors = \<alpha>} =
     PiE_dflt {..<n} None
       (\<lambda>i. Some `
         {xor. satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> i)})"
 proof -
   have *: "\<And>x xa a b.
        (\<not> xa < n \<longrightarrow> x xa = None) \<Longrightarrow>
        x xa = Some (a, b) \<Longrightarrow> xa < n"
   by (metis option.distinct(2))
   show ?thesis
   unfolding PiE_dflt_def
   unfolding xor_hash_eq_iff[OF assms]
   by (auto intro: * simp del: satisfies_xor.simps)
 qed
 
 lemma prob_random_xors_xor_hash:
   assumes V: "finite V"
   assumes \<alpha>: "dom \<alpha> = {..<n}"
   shows "
   measure_pmf.prob (random_xors V n)
     {xors. xor_hash \<omega> xors = \<alpha>} = 1 / 2  ^ n"
 proof -
   have "measure_pmf.prob (random_xors V n)
     {xors. xor_hash \<omega> xors = \<alpha>} =
     measure_pmf.prob
     (Pi_pmf {..<(n::nat)} None
       (\<lambda>_. map_pmf Some (random_xor V)))
     (PiE_dflt {..<n} None
       (\<lambda>i. Some ` {xor. satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> i)}))"
     unfolding random_xors_def xor_hash_eq_PiE_dflt[OF \<alpha>]
     by auto
   also have "... =
     (\<Prod>x<n. measure_pmf.prob (random_xor V)
              ({xor.
                satisfies_xor xor {x. \<omega> x = Some True} =
                the (\<alpha> x)}))"
     by (subst measure_Pi_pmf_PiE_dflt)
-     (auto simp add: measure_map_pmf inj_vimage_image_eq)
+     (auto simp add: inj_vimage_image_eq)
   also have "... = (\<Prod>x<n. 1/2)"
     by (simp add: assms(1) satisfies_random_xor_parity)
   also have "... = 1/ 2 ^ n"
     by (simp add: power_one_over)
   finally show ?thesis by auto
 qed
 
 lemma PiE_dflt_inter:
   shows"PiE_dflt A dflt B \<inter> PiE_dflt A dflt B' =
     PiE_dflt A dflt (\<lambda>b. B b \<inter> B' b)"
   unfolding PiE_dflt_def
   by auto
 
 lemma random_xors_xor_hash_pair:
   assumes V: "finite V"
   assumes \<alpha>: "dom \<alpha> = {..<n}"
   assumes \<alpha>': "dom \<alpha>' = {..<n}"
   assumes \<omega>: "dom \<omega> = V"
   assumes \<omega>': "dom \<omega>' = V"
   assumes neq: "\<omega> \<noteq> \<omega>'"
   shows "
   measure_pmf.prob (random_xors V n)
     {xors. xor_hash \<omega> xors = \<alpha> \<and> xor_hash \<omega>' xors = \<alpha>'} =
     1 / 4  ^ n"
 proof -
   obtain y where "\<omega> y \<noteq> \<omega>' y"
     using neq
     by blast
   then have neq:"{x. \<omega> x = Some True} \<noteq> {x. \<omega>' x = Some True}"
     by (smt (verit, ccfv_threshold) assms(4) assms(5) domD domIff mem_Collect_eq)
   have "measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha> \<and> xor_hash \<omega>' xors = \<alpha>'} =
     measure_pmf.prob (random_xors V n)
       ({xors. xor_hash \<omega> xors = \<alpha>} \<inter>
         {xors. xor_hash \<omega>' xors = \<alpha>'})"
     by (simp add: Collect_conj_eq)
   also have "... =
     measure_pmf.prob
     (Pi_pmf {..<(n::nat)} None
       (\<lambda>_. map_pmf Some (random_xor V)))
     (PiE_dflt {..<n} None
       (\<lambda>i. Some ` {xor. satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> i)})
     \<inter>
     PiE_dflt {..<n} None
       (\<lambda>i. Some ` {xor. satisfies_xor xor {x. \<omega>' x = Some True} = the (\<alpha>' i)}))"
     unfolding random_xors_def xor_hash_eq_PiE_dflt[OF \<alpha>] xor_hash_eq_PiE_dflt[OF \<alpha>']
     by auto
   also have "... =
     measure_pmf.prob
     (Pi_pmf {..<(n::nat)} None
       (\<lambda>_. map_pmf Some (random_xor V)))
     (PiE_dflt {..<n} None
       (\<lambda>i.
       Some ` {xor.
         satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> i) \<and>
         satisfies_xor xor {x. \<omega>' x = Some True} = the (\<alpha>' i)}))"
     unfolding PiE_dflt_inter
     apply (subst image_Int[symmetric])
     by (auto simp add: Collect_conj_eq)
 
   also have "... =
     (\<Prod>x<n. measure_pmf.prob (random_xor V)
        ({xor.
          satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> x) \<and>
          satisfies_xor xor {x. \<omega>' x = Some True} = the (\<alpha>' x)}))"
     by (subst measure_Pi_pmf_PiE_dflt)
-     (auto simp add: measure_map_pmf inj_vimage_image_eq)
+     (auto simp add: inj_vimage_image_eq)
   also have "... = (\<Prod>x<n. 1/4)"
-    apply (subst  pair_satisfies_random_xor_parity)
+    apply (subst pair_satisfies_random_xor_parity)
     using assms neq by auto
   also have "... = 1/ 4 ^ n"
     by (simp add: power_one_over)
   finally show ?thesis by auto
 qed
 
 lemma random_xors_xor_hash_three:
   assumes V: "finite V"
   assumes \<alpha>: "dom \<alpha> = {..<n}"
   assumes \<alpha>': "dom \<alpha>' = {..<n}"
   assumes \<alpha>'': "dom \<alpha>'' = {..<n}"
   assumes \<omega>: "dom \<omega> = V"
   assumes \<omega>': "dom \<omega>' = V"
   assumes \<omega>': "dom \<omega>'' = V"
   assumes neq: "\<omega> \<noteq> \<omega>'" "\<omega>' \<noteq> \<omega>''" "\<omega>'' \<noteq> \<omega>"
   shows "
   measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha>
       \<and> xor_hash \<omega>' xors = \<alpha>'
       \<and> xor_hash \<omega>'' xors = \<alpha>''} =
     1 / 8  ^ n"
 proof -
   obtain x y z where "\<omega> x \<noteq> \<omega>' x" "\<omega>' y \<noteq> \<omega>'' y" "\<omega>'' z \<noteq> \<omega> z"
     using neq
     by blast
   then have neq:
     "{x. \<omega> x = Some True} \<noteq> {x. \<omega>' x = Some True}"
     "{x. \<omega>' x = Some True} \<noteq> {x. \<omega>'' x = Some True}"
     "{x. \<omega>'' x = Some True} \<noteq> {x. \<omega> x = Some True}"
     by (smt (verit, ccfv_threshold) assms domD domIff mem_Collect_eq)+
   have "measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha> \<and> xor_hash \<omega>' xors = \<alpha>' \<and> xor_hash \<omega>'' xors = \<alpha>''} =
     measure_pmf.prob (random_xors V n)
       ({xors. xor_hash \<omega> xors = \<alpha>} \<inter>
       {xors. xor_hash \<omega>' xors = \<alpha>'} \<inter>
       {xors. xor_hash \<omega>'' xors = \<alpha>''})"
     by (simp add: measure_pmf.measure_pmf_eq)
   moreover have "... =
     measure_pmf.prob
     (Pi_pmf {..<(n::nat)} None
       (\<lambda>_. map_pmf Some (random_xor V)))
     (PiE_dflt {..<n} None
       (\<lambda>i. Some ` {xor. satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> i)})
     \<inter>
     PiE_dflt {..<n} None
       (\<lambda>i. Some ` {xor. satisfies_xor xor {x. \<omega>' x = Some True} = the (\<alpha>' i)})
     \<inter>
     PiE_dflt {..<n} None
       (\<lambda>i. Some ` {xor. satisfies_xor xor {x. \<omega>'' x = Some True} = the (\<alpha>'' i)}))"
     unfolding random_xors_def xor_hash_eq_PiE_dflt[OF \<alpha>] xor_hash_eq_PiE_dflt[OF \<alpha>'] xor_hash_eq_PiE_dflt[OF \<alpha>'']
     by auto
   moreover have "... =
     measure_pmf.prob
     (Pi_pmf {..<(n::nat)} None
       (\<lambda>_. map_pmf Some (random_xor V)))
     (PiE_dflt {..<n} None
       (\<lambda>i.
       Some ` {xor.
         satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> i) \<and>
         satisfies_xor xor {x. \<omega>' x = Some True} = the (\<alpha>' i) \<and>
         satisfies_xor xor {x. \<omega>'' x = Some True} = the (\<alpha>'' i)}))
     "
     unfolding PiE_dflt_inter
     apply (subst image_Int[symmetric])
     subgoal by simp
     apply (intro arg_cong[where f="measure_pmf.prob
      (Pi_pmf {..<n} None
        (\<lambda>_. map_pmf Some (random_xor V)))"])
     apply (intro arg_cong[where f="PiE_dflt {..<n} None"])
     by auto
 
   moreover have "... =
     (\<Prod>x<n. measure_pmf.prob (random_xor V)
        ({xor.
          satisfies_xor xor {x. \<omega> x = Some True} = the (\<alpha> x) \<and>
          satisfies_xor xor {x. \<omega>' x = Some True} = the (\<alpha>' x)\<and>
          satisfies_xor xor {x. \<omega>'' x = Some True} = the (\<alpha>'' x)}))"
      apply (subst measure_Pi_pmf_PiE_dflt)
-     by (auto simp add: measure_map_pmf inj_vimage_image_eq)
+     by (auto simp add: inj_vimage_image_eq)
   moreover have "... = (\<Prod>x<n. 1/8)"
     apply (subst three_satisfies_random_xor_parity)
     subgoal using assms neq by clarsimp
     subgoal using assms neq by clarsimp
     subgoal using assms neq by clarsimp
     subgoal using assms neq by clarsimp
     subgoal using assms(5) by blast
     subgoal using assms(6) by blast
     subgoal using assms(7) by blast
     by auto
   moreover have "... = 1/ 8 ^ n"
     by (simp add: power_one_over)
   ultimately show ?thesis by auto
 qed
 
 end
diff --git a/thys/Approximate_Model_Counting/RandomXORHashFamily.thy b/thys/Approximate_Model_Counting/RandomXORHashFamily.thy
--- a/thys/Approximate_Model_Counting/RandomXORHashFamily.thy
+++ b/thys/Approximate_Model_Counting/RandomXORHashFamily.thy
@@ -1,302 +1,302 @@
 section \<open>Random XOR hash family\<close>
 
 text \<open>This section defines a hash family based on random XORs and proves
   that this hash family is 3-universal. \<close>
 
 theory RandomXORHashFamily imports
   RandomXOR
 begin
 
 lemma finite_dom:
   assumes "finite V"
   shows "finite {w :: 'a \<rightharpoonup> bool. dom w = V}"
 proof -
   have *: "{w :: 'a \<rightharpoonup> bool. dom w = V} =
     {w. dom w = V \<and> ran w \<subseteq> {True,False}}"
     by auto
   show ?thesis unfolding *
     apply (intro finite_set_of_finite_maps)
     using assms by auto
 qed
 
 lemma xor_hash_eq_dom:
   assumes "xor_hash \<omega> xors = \<alpha>"
   shows "dom xors = dom \<alpha>"
   using assms unfolding xor_hash_def
   by auto
 
 lemma prob_random_xors_xor_hash_indicat_real:
   assumes V: "finite V"
   shows"
   measure_pmf.prob (random_xors V n)
     {xors. xor_hash \<omega> xors = \<alpha>} =
      indicat_real {\<alpha>::nat \<rightharpoonup> bool. dom \<alpha> = {0..<n}} \<alpha> /
      real (card {\<alpha>::nat \<rightharpoonup> bool. dom \<alpha> = {0..<n}})"
 proof -
   have *: "{\<alpha>::nat \<rightharpoonup> bool. dom \<alpha> = {0..<n}} =
      {\<alpha>. dom \<alpha> = {0..<n} \<and> ran \<alpha> \<subseteq> {True, False}}"
     by auto
   have **: "card {\<alpha>::nat \<rightharpoonup> bool. dom \<alpha> = {0..<n}} = 2^n"
     unfolding *
     apply (subst card_dom_ran)
     by (auto simp add: numerals(2))
   have "dom \<alpha> = {..<n} \<or> dom \<alpha> \<noteq> {..<n}"
     by auto
   moreover {
     assume "dom \<alpha> = {..<n}"
     from prob_random_xors_xor_hash[OF V this]
     have ?thesis
       unfolding **
       by (simp add: \<open>dom \<alpha> = {..<n}\<close> atLeast0LessThan)
   }
   moreover {
     assume *:"dom \<alpha> \<noteq> {..<n}"
     then have "x \<in> set_pmf (random_xors V n) \<Longrightarrow>
          \<alpha> \<noteq> xor_hash \<omega> x" for x
       by (metis (mono_tags, lifting) V mem_Collect_eq random_xors_set_pmf xor_hash_eq_dom)
     then have "measure_pmf.prob (random_xors V n)
      {xors. xor_hash \<omega> xors = \<alpha>} = 0"
       apply (intro measure_pmf.measure_exclude[where A = "set_pmf ((random_xors V n))"])
       by (auto simp add: Sigma_Algebra.measure_def emeasure_pmf xor_hash_eq_dom)
     then have ?thesis
       by (simp add: * atLeast0LessThan)
   }
   ultimately show ?thesis
     by auto
 qed
 
 lemma xor_hash_family_uniform:
   assumes V: "finite V"
   assumes "dom \<omega> = V"
   shows "prob_space.uniform_on
          (random_xors V n)
          (xor_hash i) {\<alpha>. dom \<alpha> = {0..<n}}"
   apply (intro measure_pmf.uniform_onI[where p = "random_xors V n"])
   subgoal by clarsimp
   subgoal  using finite_dom by blast
   using prob_random_xors_xor_hash_indicat_real[OF V]
   by (auto intro!: exI[where x = "(\<lambda>i. if i < n then Some True else None)"] split:if_splits)
 
 lemma random_xors_xor_hash_pair_indicat:
   assumes V: "finite V"
   assumes \<omega>: "dom \<omega> = V"
   assumes \<omega>': "dom \<omega>' = V"
   assumes neq: "\<omega> \<noteq> \<omega>'"
   shows "
   measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha> \<and> xor_hash \<omega>' xors = \<alpha>'} =
   (measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha>} *
    measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega>' xors = \<alpha>'})"
 proof -
   have "dom \<alpha> = {..<n} \<and> dom \<alpha>' = {..<n} \<or>
     \<not>(dom \<alpha> = {..<n} \<and> dom \<alpha>' = {..<n})" by auto
   moreover {
     assume *: "dom \<alpha> = {..<n}" "dom \<alpha>' = {..<n}"
     have "measure_pmf.prob (random_xors V n)
      {xors.
       xor_hash \<omega> xors = \<alpha> \<and> xor_hash \<omega>' xors = \<alpha>'} = 1 / 4 ^n"
       by (simp add: "*"(1) "*"(2) assms(1) assms(2) assms(3) assms(4) random_xors_xor_hash_pair)
     moreover have "
     measure_pmf.prob (random_xors V n)
       {xors.  xor_hash \<omega> xors = \<alpha>} = 1/2^n"
       by (simp add: "*"(1) assms(1) prob_random_xors_xor_hash)
     moreover have "
     measure_pmf.prob (random_xors V n)
       {xors.  xor_hash \<omega>' xors = \<alpha>'} = 1/2^n"
       by (simp add: "*"(2) assms(1) prob_random_xors_xor_hash)
     ultimately have ?thesis
       by (metis (full_types) Groups.mult_ac(2) four_x_squared power2_eq_square power_mult power_one_over verit_prod_simplify(2))
   }
   moreover {
     assume *: "dom \<alpha> \<noteq> {..<n} \<or> dom \<alpha>' \<noteq> {..<n}"
     then have **: "x \<in> set_pmf (random_xors V n) \<Longrightarrow>
          \<alpha> = xor_hash \<omega> x \<Longrightarrow>
          \<alpha>' = xor_hash \<omega>' x \<Longrightarrow> False" for x
       by (metis (mono_tags, lifting) CollectD assms(1) random_xors_set_pmf xor_hash_eq_dom)
     have "measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha>} = 0 \<or>
      measure_pmf.prob (random_xors V n)
       {xors.
         xor_hash \<omega>' xors = \<alpha>'} = 0"
       unfolding prob_random_xors_xor_hash_indicat_real[OF V]
-      by (metis * atLeast0LessThan div_0 indicator_simps(2) mem_Collect_eq)
+      by (metis (full_types) * atLeast0LessThan div_0 indicator_simps(2) mem_Collect_eq)
     moreover have "
     measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha> \<and> xor_hash \<omega>' xors = \<alpha>'} = 0"
       apply (intro measure_pmf.measure_exclude[where A = "set_pmf ((random_xors V n))"])
       using ** by (auto simp add: Sigma_Algebra.measure_def emeasure_pmf)
     ultimately have ?thesis by auto
   }
   ultimately show ?thesis by auto
 qed
 
 lemma prod_3_expand:
   assumes "a \<noteq> b" "b \<noteq> c" "c \<noteq> a"
   shows"(\<Prod>\<omega>\<in>{a, b, c}. f \<omega>) = f a * (f b * f c)"
   using assms by auto
 
 lemma random_xors_xor_hash_three_indicat:
   assumes V: "finite V"
   assumes \<omega>: "dom \<omega> = V"
   assumes \<omega>': "dom \<omega>' = V"
   assumes \<omega>'': "dom \<omega>'' = V"
   assumes neq: "\<omega> \<noteq> \<omega>'" "\<omega>' \<noteq> \<omega>''" "\<omega>'' \<noteq> \<omega>"
   shows "
   measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha>
     \<and> xor_hash \<omega>' xors = \<alpha>'
     \<and> xor_hash \<omega>'' xors = \<alpha>''} =
   (measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha>} *
    measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega>' xors = \<alpha>'} *
    measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega>'' xors = \<alpha>''})"
 proof -
   have "dom \<alpha> = {..<n} \<and> dom \<alpha>' = {..<n} \<and> dom \<alpha>'' = {..<n} \<or>
     \<not>(dom \<alpha> = {..<n} \<and> dom \<alpha>' = {..<n} \<and> dom \<alpha>'' = {..<n})" by auto
   moreover {
     assume *: "dom \<alpha> = {..<n}" "dom \<alpha>' = {..<n}" "dom \<alpha>'' = {..<n}"
     have 1:"measure_pmf.prob (random_xors V n)
      {xors.
       xor_hash \<omega> xors = \<alpha> \<and>
       xor_hash \<omega>' xors = \<alpha>' \<and>
       xor_hash \<omega>'' xors = \<alpha>''} = 1 / 8 ^n"
       apply (intro random_xors_xor_hash_three)
       using V * \<omega> \<omega>' \<omega>'' neq by auto
     have 2:"
     measure_pmf.prob (random_xors V n)
       {xors.  xor_hash \<omega> xors = \<alpha>} = 1/2^n"
       by (simp add: "*"(1) assms(1) prob_random_xors_xor_hash)
     have 3:"
     measure_pmf.prob (random_xors V n)
       {xors.  xor_hash \<omega>' xors = \<alpha>'} = 1/2^n"
       by (simp add: "*"(2) assms(1) prob_random_xors_xor_hash)
     have 4: "
     measure_pmf.prob (random_xors V n)
       {xors.  xor_hash \<omega>'' xors = \<alpha>''} = 1/2^n"
       by (simp add: "*"(3) assms(1) prob_random_xors_xor_hash)
     have ?thesis
       unfolding 1 2 3 4
       by (metis (mono_tags, opaque_lifting) arith_simps(11) arith_simps(12) arith_simps(58) divide_divide_eq_left mult.right_neutral power_mult_distrib times_divide_eq_right)
   }
   moreover {
     assume *: "dom \<alpha> \<noteq> {..<n} \<or> dom \<alpha>' \<noteq> {..<n} \<or> dom \<alpha>'' \<noteq> {..<n}"
     then have **: "x \<in> set_pmf (random_xors V n) \<Longrightarrow>
          \<alpha> = xor_hash \<omega> x \<Longrightarrow>
          \<alpha>' = xor_hash \<omega>' x \<Longrightarrow>
          \<alpha>'' = xor_hash \<omega>'' x \<Longrightarrow> False" for x
       by (metis (mono_tags, lifting) CollectD assms(1) random_xors_set_pmf xor_hash_eq_dom)
     have "measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha>} = 0 \<or>
      measure_pmf.prob (random_xors V n)
       {xors.
         xor_hash \<omega>' xors = \<alpha>'} = 0 \<or>
      measure_pmf.prob (random_xors V n)
       {xors.
         xor_hash \<omega>'' xors = \<alpha>''} = 0"
       unfolding prob_random_xors_xor_hash_indicat_real[OF V]
-      by (metis * atLeast0LessThan div_0 indicator_simps(2) mem_Collect_eq)
+      by (metis (full_types) * atLeast0LessThan div_0 indicator_simps(2) mem_Collect_eq)
     moreover have "
     measure_pmf.prob (random_xors V n)
     {xors.
       xor_hash \<omega> xors = \<alpha> \<and> xor_hash \<omega>' xors = \<alpha>' \<and> xor_hash \<omega>'' xors = \<alpha>''} = 0"
       apply (intro measure_pmf.measure_exclude[where A = "set_pmf ((random_xors V n))"])
       using ** by (auto simp add: Sigma_Algebra.measure_def emeasure_pmf)
     ultimately have ?thesis by auto
   }
   ultimately show ?thesis
     by fastforce
 qed
 
 lemma xor_hash_3_indep:
   assumes V: "finite V"
   assumes J: "card J \<le> 3" "J \<subseteq> {\<alpha>. dom \<alpha> = V}"
   shows "
     measure_pmf.prob (random_xors V n)
       {xors. \<forall>\<omega>\<in>J. xor_hash \<omega> xors = f \<omega>} =
        (\<Prod>\<omega>\<in>J.
           measure_pmf.prob (random_xors V n)
            {xors. xor_hash \<omega> xors = f \<omega>})"
 proof -
   have "card J = 0 \<or> card J = 1 \<or> card J = 2 \<or> card J = 3"
     using assms by auto
   moreover {
     assume" card J = 0"
     then have "J = {}"
       by (meson assms(1) assms(3) card_eq_0_iff finite_dom finite_subset)
     then have ?thesis
       by clarsimp
   }
   moreover {
     assume "card J = 1"
     then obtain x where "J = {x}"
       using card_1_singletonE by blast
     then have ?thesis
       by auto
   }
   moreover {
     assume "card J = 2"
     then obtain \<omega> \<omega>' where J:"J = {\<omega>, \<omega>'}" and
       \<omega>: "\<omega> \<noteq> \<omega>'" "dom \<omega> = V" "dom \<omega>' = V"
       unfolding card_2_iff
       using J
       by force
     have ?thesis unfolding J
       by (auto simp add: random_xors_xor_hash_pair_indicat V \<omega>)
   }
   moreover {
     assume "card J = 3"
     then obtain \<omega> \<omega>' \<omega>'' where J:"J = {\<omega>, \<omega>', \<omega>''}" and
       \<omega>: "\<omega> \<noteq> \<omega>'" "\<omega>' \<noteq> \<omega>''" "\<omega>'' \<noteq> \<omega>"
         "dom \<omega> = V" "dom \<omega>' = V" "dom \<omega>'' = V"
       unfolding card_3_iff
       using J
       by force
     have ?thesis unfolding J
       by (auto simp add: random_xors_xor_hash_three_indicat V \<omega>  prod_3_expand[OF \<omega>(1-3)])
   }
   ultimately show ?thesis by auto
 qed
 
 lemma xor_hash_3_wise_indep:
   assumes "finite V"
   shows "prob_space.k_wise_indep_vars
      (random_xors V n) 3
      (\<lambda>_. Universal_Hash_Families_More_Independent_Families.discrete) xor_hash
      {\<alpha>. dom \<alpha> = V}"
   apply (subst prob_space.k_wise_indep_vars_def)
   by (auto intro!: measure_pmf.indep_vars_pmf xor_hash_3_indep simp add: measure_pmf.prob_space_axioms assms card_mono dual_order.trans)
 
 theorem xor_hash_family_3_universal:
   assumes "finite V"
   shows"prob_space.k_universal
     (random_xors V n) 3 xor_hash
     {\<alpha>::'a \<rightharpoonup> bool. dom \<alpha> = V}
     {\<alpha>::nat \<rightharpoonup> bool. dom \<alpha> = {0..<n}}"
   apply (subst prob_space.k_universal_def)
   subgoal by (clarsimp simp add: measure_pmf.prob_space_axioms )
   using xor_hash_3_wise_indep assms xor_hash_family_uniform assms by blast
 
 corollary xor_hash_family_2_universal:
   assumes "finite V"
   shows"prob_space.k_universal
     (random_xors V n) 2 xor_hash
     {\<alpha>::'a \<rightharpoonup> bool. dom \<alpha> = V}
     {\<alpha>::nat \<rightharpoonup> bool. dom \<alpha> = {0..<n}}"
   using assms
   by (auto intro!: prob_space.k_universal_mono[OF _ _ xor_hash_family_3_universal] measure_pmf.prob_space_axioms)
 
 end