Theory RandomXOR
section ‹Random XORs›
text ‹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}
›
theory RandomXOR imports
ApproxMCPreliminaries
Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
Monad_Normalisation.Monad_Normalisation
begin
text ‹A random XOR constraint is modeled
as a random subset of variables and a randomly chosen RHS bit. ›
definition random_xor :: "'a set ⇒ ('a set × 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 (λb. {x ∈ V. b x = Some True})
(Pi_pmf V def (λ_. map_pmf Some (bernoulli_pmf (1 / 2))))"
proof -
have *: "Pi_pmf V def (λ_. map_pmf Some (bernoulli_pmf (1 / 2))) =
map_pmf (λf x. if x ∈ V then f x else def)
(Pi_pmf V (Some False) (λ_. map_pmf Some (bernoulli_pmf (1 / 2))))"
unfolding Pi_pmf_default_swap[OF V] by auto
have **: "pmf_of_set (Pow V) =
map_pmf
(λx. {xa. (xa ∈ V ⟶ x xa) ∧ xa ∈ V})
(Pi_pmf V False (λ_. 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
lemma random_xor_from_bits:
assumes V:"finite V"
shows "random_xor V =
pair_pmf
(map_pmf (λb. {x ∈ V. b x = Some True})
(Pi_pmf V def (λ_. 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
fun satisfies_xor :: "('a set × bool) ⇒ 'a set ⇒ bool"
where "satisfies_xor (x,b) ω =
even (card (ω ∩ x) + of_bool b) "
lemma satisfies_xor_inter:
shows "satisfies_xor ( ω ∩ x ,b) ω = satisfies_xor (x,b) ω"
by (auto simp add: Int_commute)
lemma prob_bernoulli_bind_pmf:
assumes "0 ≤ p" "p ≤ 1"
assumes "finite E"
shows "measure_pmf.prob
(bernoulli_pmf p ⤜ 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) × 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 ≠ {}" "Q ≠ {}"
assumes "finite P" "finite Q"
shows "pmf_of_set (P × 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) × 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 ⊆ V ∧ 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:"¬b"
have "{c. P c} ∈ 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 ω} = 1 / 2"
proof -
have eq: "{(c::'a set × bool). fst c ⊆ V} = {c. c ⊆ V} × UNIV"
by auto
then have "finite {(c::'a set × bool). fst c ⊆ V}"
using assms by auto
then have *: "
x ⊆ V ⟹
measure_pmf.prob (bernoulli_pmf (1 / 2) ⤜ (λy. return_pmf (x, y)))
{c. fst c ⊆ V ∧ satisfies_xor c ω} = 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 ω} =
prob_space.prob (random_xor V) {c. fst c ⊆ V ∧ satisfies_xor c ω}"
using prob_random_xor_with_set_pmf[OF V] by auto
also have "... =
prob_space.expectation (random_xor V)
(indicat_real {c. fst c ⊆ V ∧ satisfies_xor c ω})"
by auto
also have "... = (∑a∈Pow V.
inverse (real (card (Pow V))) *
measure_pmf.prob
(bernoulli_pmf (1 / 2) ⤜
(λy. return_pmf (a, y)))
{c. fst c ⊆ V ∧ satisfies_xor c ω})"
unfolding random_xor_def pair_pmf_def
apply (subst pmf_expectation_bind_pmf_of_set)
using assms by auto
also have "... = (∑a∈Pow V.
inverse (real (card (Pow V))) * (1/2))"
by (simp add: *)
also have "... =
inverse (real (card (Pow V))) * (1/2) * (∑a∈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 ω = 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 ⊆ V" "finite V"
shows "
map_pmf (λ(x,y). x ∪ y)
(pmf_of_set (Pow S × 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 ⊆ V ⟹
∃xa∈Pow S.
∃y∈Pow (V - S). x = xa ∪ 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 (λ(x, y). x ∪ y)
(Pow S × Pow (V - S))"
unfolding inj_on_def
by auto
then have bij: "bij_betw (λ(x, y). x ∪ y)
((Pow S) × Pow (V - S))
(Pow V)"
unfolding bij_betw_def
using assms(1) xsub by (auto simp add: image_def)
have "map_pmf (λ(x, y). x ∪ y)
(pmf_of_set (Pow S × 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) ⤜
(λ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} × Pow V) =
map_pmf (λ(r,c). (if c then {x} else {}, r)) (random_xor V)"
proof -
have *: "pmf_of_set (Pow {x} × 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
lemma measure_pmf_prob_dependent_product_bound_eq:
assumes "countable A" "⋀i. countable (B i)"
assumes "⋀a. a ∈ A ⟹ 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) =
(∑⇩a(a, b) ∈ Sigma A B. pmf M a * pmf N b)"
by (auto intro!: infsetsum_cong simp add: measure_pmf_conv_infsetsum pmf_pair)
also have "... = (∑⇩aa∈A. ∑⇩ab∈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 "... = (∑⇩aa∈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 "... = (∑⇩aa∈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
lemma measure_pmf_prob_dependent_product_bound_eq':
assumes "countable (A ∩ set_pmf M)" "⋀i. countable (B i ∩ set_pmf N)"
assumes "⋀a. a ∈ A ∩ set_pmf M ⟹ measure_pmf.prob N (B a ∩ 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 ∩ (set_pmf M × set_pmf N) =
Sigma (A ∩ set_pmf M) (λi. B i ∩ 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 ∩ set_pmf M) (λi. B i ∩ set_pmf N))"
by (metis * measure_Int_set_pmf set_pair_pmf)
moreover have "... =
measure_pmf.prob M (A ∩ 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 ∈ ω" "finite ω"
assumes "finite a" "x ∉ a"
shows "measure_pmf.prob (pmf_of_set (Pow {x}))
{y. even (card ((a ∪ y) ∩ ω)) = b} = 1/2"
proof -
have "insert x a ∩ ω = insert x (a ∩ ω)"
using assms by auto
then have *: "card (insert x a ∩ ω) = 1 + card (a ∩ ω)"
by (simp add: assms(2) assms(4))
have "measure_pmf.prob (pmf_of_set (Pow {x}))
{y. even (card ((a ∪ y) ∩ ω)) = b} =
measure_pmf.prob (bernoulli_pmf (1/2))
{odd (card (a ∩ ω)) = 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
lemma prob_pmf_of_set_nonempty_parity:
assumes V: "finite V"
assumes "x ∈ ω" "ω ⊆ V"
assumes "⋀c. c ∈ E ⟷ c - {x} ∈ E"
shows "prob_space.prob (pmf_of_set (Pow V))
(E ∩ {c. even (card (c ∩ ω)) = 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} × Pow (V - {x}))) = Pow {x} × Pow (V - {x})"
by (simp add: Pow_not_empty assms(1))
have "{x} ⊆ V" using assms by auto
from pmf_of_set_powerset_split[OF this assms(1)]
have e: "map_pmf (λ(x, y). x ∪ y)
(pmf_of_set (Pow {x} × Pow (V - {x}))) =
pmf_of_set (Pow V)" using 1 2 by auto
have "map_pmf (λ(x, y). x ∪ y)
(pair_pmf (pmf_of_set (Pow {x}))
(pmf_of_set (Pow (V - {x})))) =
map_pmf (λ(x, y). x ∪ 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 (λ(x, y). x ∪ 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 **: "((λ(x, y). x ∪ y) -` (E ∩ S)) ∩ (Pow (V - {x}) × Pow{x}) =
Sigma E (λx. {y. (x ∪ y) ∈ S}) ∩ (Pow (V - {x}) × Pow{x})" for S
proof -
have 11: "⋀a b. a ∪ b ∈ E ⟹
a ∪ b ∈ S ⟹
a ⊆ V - {x} ⟹
b ⊆ {x} ⟹ a ∈ E"
by (metis Diff_insert_absorb Un_insert_right assms(4) boolean_algebra_cancel.sup0 subset_Diff_insert subset_singleton_iff)
have 21: " ⋀a b. a ∈ E ⟹
a ∪ b ∈ S ⟹
a ⊆ V - {x} ⟹
b ⊆ {x} ⟹ a ∪ b ∈ E"
by (metis Diff_cancel Un_Diff Un_empty_left assms(4) inf_sup_aci(5) subset_singletonD)
have 1: "
⋀ab. ab ∈ ((λ(x, y). x ∪ y) -` (E ∩ S)) ∩ (Pow (V - {x}) × Pow{x}) ⟹
ab ∈ Sigma E (λx. {y. (x ∪ y) ∈ S}) ∩ (Pow (V - {x}) × Pow{x})"
using 11 by clarsimp
also have 2: "
⋀ab. ab ∈ Sigma E (λx. {y. (x ∪ y) ∈ S}) ∩ (Pow (V - {x}) × Pow{x}) ⟹
ab ∈ ((λ(x, y). x ∪ y) -` (E ∩ S)) ∩ (Pow (V - {x}) × Pow{x})"
using 21 by clarsimp
ultimately show ?thesis
apply (intro antisym)
by (meson subsetI)+
qed
have eR: "⋀a. a ∈ E ∩ set_pmf (pmf_of_set (Pow (V - {x}))) ⟹
measure_pmf.prob (pmf_of_set (Pow {x}))
({y. even (card ((a ∪ y) ∩ ω)) = b} ∩
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 ∩ {c. even (card (c ∩ ω)) = b}) =
prob_space.prob (map_pmf (λ(x, y). x ∪ y)
(pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x}))))
(E ∩ {c. even (card (c ∩ ω)) = b})" unfolding * by auto
moreover have "... =
prob_space.prob (pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x})))
((λ(x, y). x ∪ y) -` (E ∩ {c. even (card (c ∩ ω)) = b}))"
by auto
moreover have "... =
prob_space.prob (pair_pmf (pmf_of_set (Pow (V - {x}))) (pmf_of_set (Pow {x})))
((λ(x, y). x ∪ y) -` (E ∩ {c. even (card (c ∩ ω)) = b}) ∩ (Pow (V - {x}) × 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 (λx. {y. even (card ((x ∪ y) ∩ ω)) = b}) ∩ (Pow (V - {x}) × 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 (λx. {y. even (card ((x ∪ y) ∩ ω)) = 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) ∈ E} +
1 / 2 * prob_space.prob (pmf_of_set (Pow V)) {e. (e,False) ∈ E}"
proof -
have fin: "finite (set_pmf (random_xor V))"
by (simp add: V set_pmf_random_xor)
have fin2: "finite ((λ(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) ∈ E ∧ (x, b) ∈ set_pmf (random_xor V)} =
{x. (x,b) ∈ E} ∩ set_pmf (pmf_of_set (Pow V))" for b
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 ∩ 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)))
((λ(x, y). (y, x)) -` (E ∩ 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) ∈ E} +
1 / 2 *
measure_pmf.prob (pmf_of_set (Pow V)) {x. (x, False) ∈ 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 ω: "x ∈ ω" "ω ⊆ V"
assumes E: "⋀c. c ∈ E ⟷ (fst c - {x},snd c) ∈ E"
shows "prob_space.prob (random_xor V)
(E ∩ {c. satisfies_xor c ω = b}) =
1 / 2 * prob_space.prob (random_xor (V - {x})) E"
proof -
have *: "{e. (e, b') ∈ E ∩ {c. satisfies_xor c ω = b}} =
{e. (e, b') ∈ E} ∩ {c. even (card (c ∩ ω)) = (b ≠ b')}" for b'
by (auto simp add: Int_commute)
have "prob_space.prob (random_xor V)
(E ∩ {c. satisfies_xor c ω = b}) =
1 / 2 *
measure_pmf.prob (pmf_of_set (Pow V))
{e. (e, True) ∈ E ∩ {c. satisfies_xor c ω = b}} +
1 / 2 *
measure_pmf.prob (pmf_of_set (Pow V))
{e. (e, False) ∈ E ∩ {c. satisfies_xor c ω = 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) ∈ E} ∩ {c. even (card (c ∩ ω)) = (b ≠ True)}) +
1 / 2 *
measure_pmf.prob (pmf_of_set (Pow V))
({e. (e, False) ∈ E} ∩ {c. even (card (c ∩ ω)) = (b ≠ False)})"
unfolding * by auto
also have "... =
1 / 2 *
(1 / 2 *
measure_pmf.prob (pmf_of_set (Pow (V - {x})))
{e. (e, True) ∈ E} +
1 / 2 *
measure_pmf.prob (pmf_of_set (Pow (V - {x})))
{e. (e, False) ∈ E})"
apply (subst prob_pmf_of_set_nonempty_parity[OF V ω])
subgoal using E by clarsimp
apply (subst prob_pmf_of_set_nonempty_parity[OF V ω])
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 ∉ ω" "x ∈ ω'"
assumes ω: "ω ⊆ V" "ω' ⊆ V"
shows "prob_space.prob (random_xor V)
{c. satisfies_xor c ω = b ∧ satisfies_xor c ω' = b'} = 1 / 4"
proof -
have wa: "ω ∩ (a - {x}) = ω ∩ a" for a
using x
by blast
have "prob_space.prob (random_xor V)
{c. satisfies_xor c ω = b ∧ satisfies_xor c ω' = b'} =
prob_space.prob (random_xor V)
({c. satisfies_xor c ω = b} ∩ {c. satisfies_xor c ω' = b'})"
by (simp add: Collect_conj_eq)
also have "... =
1 / 2 *
measure_pmf.prob (random_xor (V - {x})) {c. satisfies_xor c ω = b}"
apply (subst prob_random_xor_nonempty_parity[OF V x(2) ω(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 ω: "ω ≠ ω'" "ω ⊆ V" "ω' ⊆ V"
shows "prob_space.prob (random_xor V)
{c. satisfies_xor c ω = b ∧ satisfies_xor c ω' = b'} = 1 / 4"
proof -
obtain x where "x ∉ ω ∧ x ∈ ω' ∨ x ∉ ω' ∧ x ∈ ω"
using ω
by blast
moreover {
assume x: "x ∉ ω" "x ∈ ω'"
have ?thesis using pair_satisfies_random_xor_parity_1[OF V x ω(2-3)]
by blast
}
moreover {
assume x: "x ∉ ω'" "x ∈ ω"
then have ?thesis using pair_satisfies_random_xor_parity_1[OF V x ω(3) ω(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 ∈ ω" "ω ⊆ V"
shows "prob_space.prob (pmf_of_set (Pow V))
{c. even (card (c ∩ ω)) = b} = 1 / 2"
using prob_pmf_of_set_nonempty_parity[OF assms, of UNIV]
by auto
lemma prob_Pow_split:
assumes "ω ⊆ V" "finite V"
shows "prob_space.prob (pmf_of_set (Pow V))
{x. P (ω ∩ x) ∧ Q ((V - ω) ∩ x)} =
prob_space.prob (pmf_of_set (Pow ω))
{x. P x} *
prob_space.prob (pmf_of_set (Pow (V - ω)))
{x. Q x}"
proof -
have 1: "set_pmf (pmf_of_set (Pow ω)) = Pow ω"
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 - ω))) = Pow (V - ω )"
by (simp add: Pow_not_empty assms(2))
have *: "(pmf_of_set (Pow ω × Pow (V - ω))) =
(pair_pmf (pmf_of_set (Pow ω)) (pmf_of_set (Pow (V - ω))))"
unfolding 1 2
apply (subst pmf_of_set_prod)
using assms rev_finite_subset by auto
have **: "(((λ(x, y). x ∪ y) -`
{x. P (ω ∩ x) ∧ Q ((V - ω) ∩ x)}) ∩ ((Pow ω) × (Pow (V - ω)))) =
({x. P x} ∩ Pow ω) × ({x. Q x} ∩ Pow (V - ω))"
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 (ω ∩ x) ∧ Q ((V - ω) ∩ x)} =
prob_space.prob (map_pmf (λ(x,y). x ∪ y)
(pmf_of_set (Pow ω × Pow (V - ω))))
{x. P (ω ∩ x) ∧ Q ((V - ω) ∩ 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 ω)) (pmf_of_set (Pow (V - ω))))
((λ(x, y). x ∪ y) -`
{x. P (ω ∩ x) ∧ Q ((V - ω) ∩ x)})"
unfolding measure_map_pmf
using *
by presburger
moreover have "... =
measure_pmf.prob
(pair_pmf (pmf_of_set (Pow ω)) (pmf_of_set (Pow (V - ω))))
(((λ(x, y). x ∪ y) -`
{x. P (ω ∩ x) ∧ Q ((V - ω) ∩ x)}) ∩ ((Pow ω) × (Pow (V - ω))))"
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 ω)) (pmf_of_set (Pow (V - ω))))
(({x. P x} ∩ Pow ω) × ({x. Q x} ∩ Pow (V - ω)))"
unfolding **
by auto
moreover have "... =
measure_pmf.prob
(pmf_of_set (Pow ω)) ({x. P x} ∩ Pow ω) *
measure_pmf.prob
(pmf_of_set (Pow (V - ω))) ({x. Q x} ∩ Pow (V - ω))"
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 ω)) {x. P x} *
measure_pmf.prob
(pmf_of_set (Pow (V - ω))) {x. Q x}"
by (metis "1" "2" measure_Int_set_pmf)
ultimately show ?thesis by auto
qed
lemma disjoint_prob_pmf_of_set_nonempty:
assumes ω: "x ∈ ω" "ω ⊆ V"
assumes ω': "x' ∈ ω'" "ω' ⊆ V"
assumes "ω ∩ ω' = {}"
assumes V: "finite V"
shows "prob_space.prob (pmf_of_set (Pow V))
{c. even (card (ω ∩ c)) = b ∧ even (card (ω' ∩ c)) = b'} = 1 / 4"
proof -
have "prob_space.prob (pmf_of_set (Pow V))
{c. even (card (ω ∩ c)) = b ∧ even (card (ω' ∩ c)) = b'} =
prob_space.prob (pmf_of_set (Pow V))
{c. even (card (ω ∩ c)) = b ∧ even (card (((V - ω) ∩ c) ∩ ω')) = b'}"
by (smt (verit) Collect_cong Diff_Diff_Int Diff_eq_empty_iff Int_Diff Int_commute ω'(2) assms(5) inf.orderE)
moreover have "... =
measure_pmf.prob (pmf_of_set (Pow ω))
{x. even (card x) = b} *
measure_pmf.prob (pmf_of_set (Pow (V - ω)))
{x. even (card (x ∩ ω')) = b'}"
apply (subst prob_Pow_split)
using assms by auto
moreover have "... =
measure_pmf.prob (pmf_of_set (Pow ω))
{x. even (card (x ∩ ω)) = b} *
measure_pmf.prob (pmf_of_set (Pow (V - ω)))
{x. even (card (x ∩ ω')) = b'} "
by (smt (verit, best) PowD Pow_not_empty ω(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 _ ω(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 × B) =
measure_pmf.prob M A * measure_pmf.prob N B"
proof -
have A: "measure_pmf.prob M A = measure_pmf.prob M (A ∩ set_pmf M)"
by (simp add: measure_Int_set_pmf)
have B: "measure_pmf.prob N B = measure_pmf.prob N (B ∩ 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 ∩ set_pmf M) * measure_pmf.prob N (B ∩ set_pmf N)"
using A B by auto
moreover have "... = measure_pmf.prob (pair_pmf M N)
((A ∩ set_pmf M) × (B ∩ set_pmf N))"
apply (subst measure_pmf_prob_product[symmetric])
by auto
moreover have "... = measure_pmf.prob (pair_pmf M N)
((A × B) ∩ set_pmf (pair_pmf M N))"
by (simp add: Times_Int_Times)
moreover have "... = measure_pmf.prob (pair_pmf M N)
((A × B) )"
using measure_Int_set_pmf by blast
ultimately show ?thesis by auto
qed
lemma prob_random_xor_split_space:
assumes "ω ⊆ V" "finite V"
shows "prob_space.prob (random_xor V)
{(x,b). P (ω ∩ x) b ∧ Q ((V - ω) ∩ x)} =
prob_space.prob (random_xor ω)
{(x,b). P x b} *
prob_space.prob (pmf_of_set (Pow (V - ω)))
{x. Q x}"
proof -
have d1: "set_pmf (random_xor ω) = Pow ω × UNIV"
by (metis assms(1) assms(2) infinite_super set_pmf_random_xor)
have d2: "set_pmf (pmf_of_set (Pow (V - ω))) = Pow (V- ω)"
by (simp add: Pow_not_empty assms(2))
have rhs: "prob_space.prob (random_xor ω)
{(x,b). P x b} *
prob_space.prob (pmf_of_set (Pow (V - ω)))
{x. Q x} =
prob_space.prob (pair_pmf (random_xor ω) (pmf_of_set (Pow (V - ω))))
({(x,b). P x b} × {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 (λ(x, y). x ∪ y)
(pair_pmf (pmf_of_set (Pow ω)) (pmf_of_set (Pow (V - ω))))"
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 (λ((x,b),y). (x ∪ y,b)) (pair_pmf (random_xor ω) (pmf_of_set (Pow (V - ω))))"
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 (ω ∩ x) b ∧ Q ((V - ω) ∩ x)} =
measure_pmf.prob
(pair_pmf (random_xor ω) (pmf_of_set (Pow (V - ω))))
{y. P (ω ∩ (fst (fst y) ∪ snd y)) (snd (fst y)) ∧
Q ((V - ω) ∩ (fst (fst y) ∪ snd y))}"
unfolding **
by (auto simp add:case_prod_unfold)
moreover have "... =
prob_space.prob (pair_pmf (random_xor ω) (pmf_of_set (Pow (V - ω))))
({(x,b). P x b} × {x. Q x})"
apply (intro measure_pmf.measure_pmf_eq[where p ="pair_pmf (random_xor ω)
(pmf_of_set (Pow (V - ω)))"])
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 ω: "ω ≠ {}" "ω ⊆ V"
assumes ω': "ω' ≠ {}" "ω' ⊆ V"
assumes I: "I ⊆ V"
assumes int: "I ∩ ω = {}" "I ∩ ω' = {}" "ω ∩ ω' = {}"
assumes V: "finite V"
shows "prob_space.prob (random_xor V)
{c. satisfies_xor c I = b ∧
even (card (ω ∩ fst c)) = b' ∧
even (card (ω' ∩ 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 ∈ ω" "x' ∈ ω'" using ω ω'
by blast
have rw1:"ω ∩ ((V - I) ∩ xx) = ω ∩ xx " for xx
by (metis Diff_Int_distrib2 Diff_empty ω(2) assms(6) inf.absorb_iff2 inf_assoc inf_left_commute)
have rw2:"ω' ∩ ((V - I) ∩ xx)= ω' ∩ xx" for xx
by (metis Diff_Int_distrib2 Diff_empty ω'(2) assms(7) inf.absorb_iff2 inf_assoc inf_left_commute)
have "prob_space.prob (random_xor V)
{c. satisfies_xor c I = b ∧
even (card ( ω ∩ fst c )) = b' ∧
even (card (ω' ∩ fst c )) = b''} =
prob_space.prob (random_xor V)
{(x,bb). satisfies_xor (I ∩ x, bb) I = b ∧
even (card (ω ∩ ((V - I) ∩ x))) = b' ∧
even (card ( ω' ∩ ((V - I) ∩ 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 (ω ∩ x)) = b' ∧
even (card (ω' ∩ 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 ω ω' int finVI by auto
ultimately show ?thesis by auto
qed
lemma three_disjoint_prob_pmf_of_set_nonempty:
assumes ω: "x ∈ ω" "ω ⊆ V"
assumes ω': "x' ∈ ω'" "ω' ⊆ V"
assumes ω'': "x'' ∈ ω''" "ω'' ⊆ V"
assumes int: "ω ∩ ω' = {}" "ω' ∩ ω'' = {}" "ω'' ∩ ω = {}"
assumes V: "finite V"
shows "prob_space.prob (pmf_of_set (Pow V))
{c. even (card (ω ∩ c)) = b ∧ even (card (ω' ∩ c)) = b' ∧ even (card (ω'' ∩ c)) = b''} = 1 / 8"
proof -
have "prob_space.prob (pmf_of_set (Pow V))
{c. even (card (ω ∩ c)) = b ∧ even (card (ω' ∩ c)) = b' ∧ even (card (ω'' ∩ c)) = b''} =
prob_space.prob (pmf_of_set (Pow V))
{c. even (card (ω ∩ c)) = b ∧
even (card (((V - ω) ∩ c) ∩ ω')) = b' ∧
even (card (((V - ω) ∩ c) ∩ ω'')) = b''}"
by (smt (verit,best) Collect_cong Diff_Diff_Int Diff_eq_empty_iff Int_Diff Int_commute ω' ω'' int inf.orderE)
moreover have "... =
measure_pmf.prob (pmf_of_set (Pow ω))
{x. even (card x) = b} *
measure_pmf.prob (pmf_of_set (Pow (V - ω)))
{x. even (card (ω' ∩ x)) = b' ∧ even (card (ω'' ∩ x)) = b''}"
apply (subst prob_Pow_split)
using assms by (auto simp add: inf.commute)
moreover have "... =
measure_pmf.prob (pmf_of_set (Pow ω))
{x. even (card (x ∩ ω)) = b} *
measure_pmf.prob (pmf_of_set (Pow (V - ω)))
{x. even (card (ω' ∩ x)) = b'∧ even (card (ω'' ∩ x)) = b''} "
by (smt (verit, best) PowD Pow_not_empty ω 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 _ ω(1)])
subgoal using ω(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 ω: "ω ≠ {}" "ω ⊆ V"
assumes ω': "ω' ≠ {}" "ω' ⊆ V"
assumes ω'': "ω'' ≠ {}" "ω'' ⊆ V"
assumes I: "I ⊆ V"
assumes int: "I ∩ ω = {}" "I ∩ ω' = {}" "I ∩ ω'' = {}"
"ω ∩ ω' = {}" "ω' ∩ ω'' = {}" "ω'' ∩ ω = {}"
assumes V: "finite V"
shows "prob_space.prob (random_xor V)
{c. satisfies_xor c I = b0 ∧
even (card (ω ∩ fst c)) = b ∧
even (card (ω' ∩ fst c)) = b' ∧
even (card (ω'' ∩ 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 ∈ ω" "x' ∈ ω'" "x'' ∈ ω''"
using ω ω' ω''
by blast
have rw1:"ω ∩ ((V - I) ∩ xx) = ω ∩ xx " for xx
by (metis Diff_Int_distrib2 Diff_empty ω(2) int(1) inf.absorb_iff2 inf_assoc inf_left_commute)
have rw2:"ω' ∩ ((V - I) ∩ xx)= ω' ∩ xx" for xx
by (metis Diff_Int_distrib2 Diff_empty ω'(2) int(2) inf.absorb_iff2 inf_assoc inf_left_commute)
have rw3:"ω'' ∩ ((V - I) ∩ xx)= ω'' ∩ xx" for xx
by (metis Diff_Int_distrib2 Diff_empty ω''(2) int(3) inf.absorb_iff2 inf_assoc inf_left_commute)
have "prob_space.prob (random_xor V)
{c. satisfies_xor c I = b0 ∧
even (card (ω ∩ fst c)) = b ∧
even (card (ω' ∩ fst c)) = b' ∧
even (card (ω'' ∩ fst c)) = b''} =
prob_space.prob (random_xor V)
{(x,bb). satisfies_xor (I ∩ x, bb) I = b0 ∧
even (card (ω ∩ ((V - I) ∩ x))) = b ∧
even (card (ω' ∩ ((V - I) ∩ x))) = b' ∧
even (card (ω'' ∩ ((V - I) ∩ 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 (ω ∩ x)) = b ∧
even (card (ω' ∩ x)) = b' ∧
even (card (ω'' ∩ 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 ω ω' ω'' int finVI by auto
ultimately show ?thesis by auto
qed
lemma three_satisfies_random_xor_parity_1:
assumes V:"finite V"
assumes ω: "ω ⊆ V" "ω' ⊆ V" "ω'' ⊆ V"
assumes x: "x ∉ ω" "x ∉ ω'" "x ∈ ω''"
assumes d: "ω ≠ ω'"
shows "prob_space.prob (random_xor V)
{c.
satisfies_xor c ω = b ∧
satisfies_xor c ω' = b' ∧
satisfies_xor c ω'' = b''} = 1 / 8"
proof -
have wa: "ω ∩ (a - {x}) = ω ∩ a" for a
using x
by blast
have wa': "ω' ∩ (a - {x}) = ω' ∩ a" for a
using x
by blast
have "prob_space.prob (random_xor V)
{c.
satisfies_xor c ω = b ∧ satisfies_xor c ω' = b' ∧
satisfies_xor c ω'' = b''} =
prob_space.prob (random_xor V)
({c. satisfies_xor c ω = b ∧ satisfies_xor c ω' = b'} ∩
{c. satisfies_xor c ω'' = b''})"
by (simp add: Collect_conj_eq inf_assoc)
moreover have "... =
1 / 2 *
measure_pmf.prob (random_xor (V - {x}))
{c. satisfies_xor c ω = b ∧ satisfies_xor c ω' = b'}"
apply (subst prob_random_xor_nonempty_parity[OF V x(3) ω(3)])
by (auto simp add: wa wa')
moreover have "... = 1/8"
apply (subst pair_satisfies_random_xor_parity)
using V ω x d by auto
ultimately show ?thesis by auto
qed
lemma split_boolean_eq:
shows"(A ⟷ B) = (b ⟷ I) ∧
(B ⟷ C) = (b' ⟷ I) ∧
(C ⟷ A) = (b'' ⟷ I)
⟷
I = odd(of_bool b + of_bool b' + of_bool b'') ∧
(A = True ∧
B = (b'=b'') ∧
C = (b = b') ∨
A = False ∧
B = (b' ≠ b'') ∧
C = (b ≠ b'))"
by auto
lemma three_satisfies_random_xor_parity:
assumes V:"finite V"
assumes ω:
"ω ≠ ω'" "ω ≠ ω''" "ω' ≠ ω''"
"ω ⊆ V" "ω' ⊆ V" "ω'' ⊆ V"
shows "prob_space.prob (random_xor V)
{c. satisfies_xor c ω = b ∧
satisfies_xor c ω' = b' ∧
satisfies_xor c ω'' = b''} = 1 / 8"
proof -
have "(∃x.
x ∈ ω ∧ x ∉ ω' ∧ x ∉ ω'' ∨
x ∈ ω' ∧ x ∉ ω ∧ x ∉ ω'' ∨
x ∈ ω'' ∧ x ∉ ω ∧ x ∉ ω') ∨
ω - (ω' ∪ ω'') = {} ∧
ω' - (ω ∪ ω'') = {} ∧
ω'' - (ω ∪ ω') = {}"
by blast
moreover {
assume "(∃x.
x ∈ ω ∧ x ∉ ω' ∧ x ∉ ω'' ∨
x ∈ ω' ∧ x ∉ ω ∧ x ∉ ω'' ∨
x ∈ ω'' ∧ x ∉ ω ∧ x ∉ ω')"
then obtain x where "
x ∈ ω ∧ x ∉ ω' ∧ x ∉ ω'' ∨
x ∈ ω' ∧ x ∉ ω ∧ x ∉ ω'' ∨
x ∈ ω'' ∧ x ∉ ω ∧ x ∉ ω'" by auto
moreover {
assume x: "x ∉ ω'" "x ∉ ω''" "x ∈ ω"
have "measure_pmf.prob (random_xor V)
{c. satisfies_xor c ω' = b' ∧
satisfies_xor c ω'' = b'' ∧
satisfies_xor c ω = b} = 1 / 8"
apply (intro three_satisfies_random_xor_parity_1[OF V _ _ _ x])
using ω by auto
then have ?thesis
by (smt (verit, ccfv_SIG) Collect_cong)
}
moreover {
assume x: "x ∉ ω" "x ∉ ω''" "x ∈ ω'"
have "measure_pmf.prob (random_xor V)
{c. satisfies_xor c ω = b ∧
satisfies_xor c ω'' = b'' ∧
satisfies_xor c ω' = b'} = 1 / 8"
apply (intro three_satisfies_random_xor_parity_1[OF V _ _ _ x])
using ω by auto
then have ?thesis
by (smt (verit, ccfv_SIG) Collect_cong)
}
moreover {
assume x: "x ∉ ω" "x ∉ ω'" "x ∈ ω''"
have "measure_pmf.prob (random_xor V)
{c. satisfies_xor c ω = b ∧
satisfies_xor c ω' = b' ∧
satisfies_xor c ω'' = b''} = 1 / 8"
apply (intro three_satisfies_random_xor_parity_1[OF V _ _ _ x])
using ω by auto
then have ?thesis
by (smt (verit, ccfv_SIG) Collect_cong)
}
ultimately have ?thesis by auto
}
moreover {
assume dis: "ω - (ω' ∪ ω'') = {} ∧
ω' - (ω ∪ ω'') = {} ∧
ω'' - (ω ∪ ω') = {}"
define A where "A = (ω ∩ ω'') - ω'"
define B where "B = (ω ∩ ω') - ω''"
define C where "C = (ω' ∩ ω'') - ω"
define I where "I = ω ∩ ω' ∩ ω''"
have f: "finite A" "finite B" "finite C" "finite I"
unfolding A_def B_def C_def I_def
by (meson V ω finite_Diff finite_Int rev_finite_subset)+
have s: "A ⊆ V" "B ⊆ V" "C ⊆ V" "I ⊆ V"
unfolding A_def B_def C_def I_def
using ω by auto
have i: "I ∩ A = {}" "I ∩ B = {}" "I ∩ C = {}"
"B ∩ C = {}" "C ∩ A = {}" "A ∩ B = {}"
unfolding A_def B_def C_def I_def
by blast +
have s1: "ω = A ∪ B ∪ I"
unfolding A_def B_def I_def
using dis by auto
have sx1: "satisfies_xor (xx,bb) ω = b ⟷
even (card (A ∩ xx)) = even (card (B ∩ xx)) = (b ⟷ 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: "ω' = B ∪ C ∪ I"
unfolding B_def C_def I_def
using dis by auto
have sx2: "satisfies_xor (xx,bb) ω' = b' ⟷
even (card (B ∩ xx)) = even (card (C ∩ xx)) = (b' ⟷ 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: "ω'' = A ∪ C ∪ I"
unfolding A_def C_def I_def
using dis by auto
have sx3: "satisfies_xor (xx,bb) ω'' = b'' ⟷
even (card (C ∩ xx)) = even (card (A ∩ xx)) = (b'' ⟷ 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 = {} ∧ B ≠ {} ∧ C ≠ {} ∨
A ≠ {} ∧ B = {} ∧ C ≠ {} ∨
A ≠ {} ∧ B ≠ {} ∧ C = {} ∨
A ≠ {} ∧ B ≠ {} ∧ C ≠ {}"
by (metis Un_commute ω(1) ω(2) ω(3) s1 s2 s3)
moreover {
assume as: "A = {}" "B ≠ {}" "C ≠ {}"
have "satisfies_xor (xx,bb) ω = b
∧ satisfies_xor (xx,bb) ω' = b'
∧ satisfies_xor (xx,bb) ω'' = b'' ⟷
(satisfies_xor (xx, bb) I =
odd (of_bool b + of_bool b' + of_bool b'') ∧
(even (card (B ∩ xx)) = (b' = b'') ∧
even (card (C ∩ 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 ω = b
∧ satisfies_xor c ω' = b'
∧ satisfies_xor c ω'' = b''} =
{c. satisfies_xor c I =
odd (of_bool b + of_bool b' + of_bool b'') ∧
even (card (B ∩ fst c)) = (b' = b'') ∧
even (card (C ∩ 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 ≠ {}" "B ≠ {}" "C = {}"
have "satisfies_xor (xx,bb) ω'' = b''
∧ satisfies_xor (xx,bb) ω = b
∧ satisfies_xor (xx,bb) ω' = b' ⟷
(satisfies_xor (xx, bb) I =
odd (of_bool b'' + of_bool b + of_bool b') ∧
(even (card (A ∩ xx)) = (b = b') ∧
even (card (B ∩ 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 ω = b
∧ satisfies_xor c ω' = b'
∧ satisfies_xor c ω'' = b''} =
{c. satisfies_xor c I =
odd (of_bool b'' + of_bool b + of_bool b') ∧
(even (card (A ∩ fst c)) = (b = b') ∧
even (card (B ∩ 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 ≠ {}" "B = {}" "C ≠ {}"
have "satisfies_xor (xx,bb) ω' = b'
∧ satisfies_xor (xx,bb) ω'' = b''
∧ satisfies_xor (xx,bb) ω = b ⟷
(satisfies_xor (xx, bb) I =
odd (of_bool b' + of_bool b'' + of_bool b) ∧
(even (card (C ∩ xx)) = (b'' = b) ∧
even (card (A ∩ 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 ω = b
∧ satisfies_xor c ω' = b'
∧ satisfies_xor c ω'' = b''} =
{c. satisfies_xor c I =
odd (of_bool b' + of_bool b'' + of_bool b) ∧
(even (card (C ∩ fst c)) = (b'' = b) ∧
even (card (A ∩ 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 ≠ {}" "B ≠ {}" "C ≠ {}"
have 1: "satisfies_xor (xx,bb) ω = b
∧ satisfies_xor (xx,bb) ω' = b'
∧ satisfies_xor (xx,bb) ω'' = b'' ⟷
(satisfies_xor (xx, bb) I =
odd (of_bool b + of_bool b' + of_bool b'') ∧
even (card (A ∩ xx)) = True ∧
even (card (B ∩ xx)) = (b' = b'') ∧
even (card (C ∩ xx)) = (b = b') ∨
satisfies_xor (xx, bb) I =
odd (of_bool b + of_bool b' + of_bool b'') ∧
even (card (A ∩ xx)) = False ∧
even (card (B ∩ xx)) = (b' ≠ b'') ∧
even (card (C ∩ xx)) = (b ≠ b'))" for xx bb
unfolding sx1 sx2 sx3
apply(subst split_boolean_eq)
by auto
have 2: "satisfies_xor c ω = b
∧ satisfies_xor c ω' = b'
∧ satisfies_xor c ω'' = b'' ⟷
(satisfies_xor c I =
odd (of_bool b + of_bool b' + of_bool b'') ∧
even (card (A ∩ fst c)) = True ∧
even (card (B ∩ fst c)) = (b' = b'') ∧
even (card (C ∩ fst c)) = (b = b') ∨
satisfies_xor c I =
odd (of_bool b + of_bool b' + of_bool b'') ∧
even (card (A ∩ fst c)) = False ∧
even (card (B ∩ fst c)) = (b' ≠ b'') ∧
even (card (C ∩ fst c)) = (b ≠ 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 ω = b
∧ satisfies_xor c ω' = b'
∧ satisfies_xor c ω'' = b''} =
{c. satisfies_xor c I =
odd (of_bool b + of_bool b' + of_bool b'') ∧
even (card (A ∩ fst c)) = True ∧
even (card (B ∩ fst c)) = (b' = b'') ∧
even (card (C ∩ fst c)) = (b = b')} ∪
{c. satisfies_xor c I =
odd (of_bool b + of_bool b' + of_bool b'') ∧
even (card (A ∩ fst c)) = False ∧
even (card (B ∩ fst c)) = (b' ≠ b'') ∧
even (card (C ∩ fst c)) = (b ≠ 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'') ∧
even (card (A ∩ fst c)) =
False ∧
even (card (B ∩ fst c)) =
(b' ≠ b'') ∧
even (card (C ∩ fst c)) =
(b ≠ 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 ‹ We can lift the previous result to a list of independent sampled XORs. ›
definition random_xors :: "'a set ⇒ nat ⇒
(nat ⇀ 'a set × bool) pmf"
where "random_xors V n =
Pi_pmf {..<(n::nat)} None
(λ_. map_pmf Some (random_xor V))"
lemma random_xors_set:
assumes V:"finite V"
shows
"PiE_dflt {..<n} None
(set_pmf ∘ (λ_. map_pmf Some (random_xor V))) =
{xors. dom xors = {..<n} ∧
ran xors ⊆ (Pow V) × UNIV}" (is "?lhs = ?rhs")
proof -
have "?lhs =
{f. dom f = {..<n} ∧
(∀x ∈ {..<n}. f x ∈ Some ` (Pow V × 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} ∧ ran xors ⊆ (Pow V) × UNIV}"
proof -
have "pmf_of_set
{xors. dom xors = {..<n} ∧
ran xors ⊆ (Pow V) × UNIV} =
pmf_of_set
(PiE_dflt {..<n} None
(set_pmf ∘ (λ_. map_pmf Some (random_xor V))))"
unfolding random_xors_set[OF V] by auto
also have "... =
Pi_pmf {..<n} None
(λx. pmf_of_set
((set_pmf ∘
(λ_. 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
definition xor_hash ::
"('a ⇀ bool) ⇒
(nat ⇀ ('a set × bool)) ⇒
(nat ⇀ bool)"
where "xor_hash ω xors =
(map_option
(λxor. satisfies_xor xor {x. ω x = Some True}) ∘ xors)"
lemma finite_map_set_nonempty:
assumes "R ≠ {}"
shows "
{xors.
dom xors = D ∧ ran xors ⊆ R} ≠ {}"
proof -
obtain r where "r ∈ R"
using assms by blast
then have "(λx. if x ∈ D then Some r else None) ∈
{xors. dom xors = D ∧ ran xors ⊆ 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} ∧
ran xors ⊆ (Pow V) × 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 "⋀x. x ∈ dom f ⟹ 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 α = {..<n}"
shows"xor_hash ω x = α ⟷
(dom x = {..<n} ∧
(∀i. i < n ⟶
(∃xor. x i = Some xor ∧
satisfies_xor xor {x. ω x = Some True} = the (α i))
))"
proof -
have 1: "xor_hash ω x = α ⟷
(dom (xor_hash ω x) = dom α) ∧
(∀i ∈ dom α. the (xor_hash ω x i) = the (α i))"
using map_eq_1 by fastforce
have 2: "dom (xor_hash ω x) = dom x"
unfolding xor_hash_def
by auto
have 3: "⋀i. i ∈ dom x ⟹
xor_hash ω x i = Some (satisfies_xor (the (x i)) {x. ω 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 α = {..<n}"
shows
"{xors. xor_hash ω xors = α} =
PiE_dflt {..<n} None
(λi. Some `
{xor. satisfies_xor xor {x. ω x = Some True} = the (α i)})"
proof -
have *: "⋀x xa a b.
(¬ xa < n ⟶ x xa = None) ⟹
x xa = Some (a, b) ⟹ 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 α: "dom α = {..<n}"
shows "
measure_pmf.prob (random_xors V n)
{xors. xor_hash ω xors = α} = 1 / 2 ^ n"
proof -
have "measure_pmf.prob (random_xors V n)
{xors. xor_hash ω xors = α} =
measure_pmf.prob
(Pi_pmf {..<(n::nat)} None
(λ_. map_pmf Some (random_xor V)))
(PiE_dflt {..<n} None
(λi. Some ` {xor. satisfies_xor xor {x. ω x = Some True} = the (α i)}))"
unfolding random_xors_def xor_hash_eq_PiE_dflt[OF α]
by auto
also have "... =
(∏x<n. measure_pmf.prob (random_xor V)
({xor.
satisfies_xor xor {x. ω x = Some True} =
the (α x)}))"
by (subst measure_Pi_pmf_PiE_dflt)
(auto simp add: inj_vimage_image_eq)
also have "... = (∏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 ∩ PiE_dflt A dflt B' =
PiE_dflt A dflt (λb. B b ∩ B' b)"
unfolding PiE_dflt_def
by auto
lemma random_xors_xor_hash_pair:
assumes V: "finite V"
assumes α: "dom α = {..<n}"
assumes α': "dom α' = {..<n}"
assumes ω: "dom ω = V"
assumes ω': "dom ω' = V"
assumes neq: "ω ≠ ω'"
shows "
measure_pmf.prob (random_xors V n)
{xors. xor_hash ω xors = α ∧ xor_hash ω' xors = α'} =
1 / 4 ^ n"
proof -
obtain y where "ω y ≠ ω' y"
using neq
by blast
then have neq:"{x. ω x = Some True} ≠ {x. ω' 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 ω xors = α ∧ xor_hash ω' xors = α'} =
measure_pmf.prob (random_xors V n)
({xors. xor_hash ω xors = α} ∩
{xors. xor_hash ω' xors = α'})"
by (simp add: Collect_conj_eq)
also have "... =
measure_pmf.prob
(Pi_pmf {..<(n::nat)} None
(λ_. map_pmf Some (random_xor V)))
(PiE_dflt {..<n} None
(λi. Some ` {xor. satisfies_xor xor {x. ω x = Some True} = the (α i)})
∩
PiE_dflt {..<n} None
(λi. Some ` {xor. satisfies_xor xor {x. ω' x = Some True} = the (α' i)}))"
unfolding random_xors_def xor_hash_eq_PiE_dflt[OF α] xor_hash_eq_PiE_dflt[OF α']
by auto
also have "... =
measure_pmf.prob
(Pi_pmf {..<(n::nat)} None
(λ_. map_pmf Some (random_xor V)))
(PiE_dflt {..<n} None
(λi.
Some ` {xor.
satisfies_xor xor {x. ω x = Some True} = the (α i) ∧
satisfies_xor xor {x. ω' x = Some True} = the (α' i)}))"
unfolding PiE_dflt_inter
apply (subst image_Int[symmetric])
by (auto simp add: Collect_conj_eq)
also have "... =
(∏x<n. measure_pmf.prob (random_xor V)
({xor.
satisfies_xor xor {x. ω x = Some True} = the (α x) ∧
satisfies_xor xor {x. ω' x = Some True} = the (α' x)}))"
by (subst measure_Pi_pmf_PiE_dflt)
(auto simp add: inj_vimage_image_eq)
also have "... = (∏x<n. 1/4)"
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 α: "dom α = {..<n}"
assumes α': "dom α' = {..<n}"
assumes α'': "dom α'' = {..<n}"
assumes ω: "dom ω = V"
assumes ω': "dom ω' = V"
assumes ω': "dom ω'' = V"
assumes neq: "ω ≠ ω'" "ω' ≠ ω''" "ω'' ≠ ω"
shows "
measure_pmf.prob (random_xors V n)
{xors.
xor_hash ω xors = α
∧ xor_hash ω' xors = α'
∧ xor_hash ω'' xors = α''} =
1 / 8 ^ n"
proof -
obtain x y z where "ω x ≠ ω' x" "ω' y ≠ ω'' y" "ω'' z ≠ ω z"
using neq
by blast
then have neq:
"{x. ω x = Some True} ≠ {x. ω' x = Some True}"
"{x. ω' x = Some True} ≠ {x. ω'' x = Some True}"
"{x. ω'' x = Some True} ≠ {x. ω 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 ω xors = α ∧ xor_hash ω' xors = α' ∧ xor_hash ω'' xors = α''} =
measure_pmf.prob (random_xors V n)
({xors. xor_hash ω xors = α} ∩
{xors. xor_hash ω' xors = α'} ∩
{xors. xor_hash ω'' xors = α''})"
by (simp add: measure_pmf.measure_pmf_eq)
moreover have "... =
measure_pmf.prob
(Pi_pmf {..<(n::nat)} None
(λ_. map_pmf Some (random_xor V)))
(PiE_dflt {..<n} None
(λi. Some ` {xor. satisfies_xor xor {x. ω x = Some True} = the (α i)})
∩
PiE_dflt {..<n} None
(λi. Some ` {xor. satisfies_xor xor {x. ω' x = Some True} = the (α' i)})
∩
PiE_dflt {..<n} None
(λi. Some ` {xor. satisfies_xor xor {x. ω'' x = Some True} = the (α'' i)}))"
unfolding random_xors_def xor_hash_eq_PiE_dflt[OF α] xor_hash_eq_PiE_dflt[OF α'] xor_hash_eq_PiE_dflt[OF α'']
by auto
moreover have "... =
measure_pmf.prob
(Pi_pmf {..<(n::nat)} None
(λ_. map_pmf Some (random_xor V)))
(PiE_dflt {..<n} None
(λi.
Some ` {xor.
satisfies_xor xor {x. ω x = Some True} = the (α i) ∧
satisfies_xor xor {x. ω' x = Some True} = the (α' i) ∧
satisfies_xor xor {x. ω'' x = Some True} = the (α'' 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
(λ_. map_pmf Some (random_xor V)))"])
apply (intro arg_cong[where f="PiE_dflt {..<n} None"])
by auto
moreover have "... =
(∏x<n. measure_pmf.prob (random_xor V)
({xor.
satisfies_xor xor {x. ω x = Some True} = the (α x) ∧
satisfies_xor xor {x. ω' x = Some True} = the (α' x)∧
satisfies_xor xor {x. ω'' x = Some True} = the (α'' x)}))"
apply (subst measure_Pi_pmf_PiE_dflt)
by (auto simp add: inj_vimage_image_eq)
moreover have "... = (∏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