diff --git a/thys/Approximate_Model_Counting/ApproxMCAnalysis.thy b/thys/Approximate_Model_Counting/ApproxMCAnalysis.thy new file mode 100644 --- /dev/null +++ b/thys/Approximate_Model_Counting/ApproxMCAnalysis.thy @@ -0,0 +1,764 @@ +section \ ApproxMC definition and analysis \ + +text \ + This section puts together preceding results to formalize the + PAC guarantee of ApproxMC. +\ + +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 (\f. map f ls) + (Pi_pmf (set ls) def (\_. 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 (\f. map f (sorted_list_of_set V)) + (Pi_pmf V def (\_. 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 \ 'b) list \ 'b \ 'a \ 'b" +where "map_of_default ls def = + (let m = map_of ls in + (\x. case m x of None \ def | Some v \ v))" + +lemma Pi_pmf_replicate_pmf: + assumes "finite V" + shows + "(Pi_pmf V def (\_. p)) = + map_pmf (\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 "\w. w \ B \ restr S w \ C" + shows "proj S (A \ B) = proj S A \ C" + unfolding ApproxMCCore.proj_def + using assms by auto + +text \ + 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). +\ +locale ApproxMC = + fixes sols :: "'fml \ ('a \ bool) set" + fixes enc_xor :: "'a set \ bool \ 'fml \ 'fml" + assumes sols_enc_xor: + "\F xor. finite (fst xor) \ + sols (enc_xor xor F) = + sols F \ {\. satisfies_xor xor {x. \ x}}" +begin + +definition compute_thresh :: "real \ nat" + where "compute_thresh \ = + nat \1 + 9.84 * (1 + \ / (1 + \)) * (1 + 1 / \)^2\" + +definition fix_t :: "real \ nat" + where "fix_t \ = + nat \ln (1 / \) /(2 * (0.5-0.36)^2)\" + +definition raw_median_bound :: "real \ nat \ real" + where "raw_median_bound \ t = + (\i = 0..t div 2. + (t choose i) * (1 / 2 + \) ^ i * (1 / 2 - \) ^ (t - i))" + +definition compute_t :: "real \ nat \ nat" + where "compute_t \ n = + (if raw_median_bound 0.14 n < \ then n + else fix_t \)" + +(* The size of the projected solution set after adding i XORs*) +definition size_xor ::" + 'fml \ 'a set \ + (nat \ ('a set \ bool) option) \ + nat \ nat" + where "size_xor F S xorsf i = ( + let xors = map (the \ xorsf) [0.. 'a set \ + nat \ + (nat \ ('a set \ bool) option) \ + nat \ bool" + where "check_xor F S thresh xorsf i = + (size_xor F S xorsf i < thresh)" + +definition approxcore_xors :: " + 'fml \ 'a set \ + nat \ + (nat \ ('a set \ bool) option) \ + nat" + where " + approxcore_xors F S thresh xorsf = + (case List.find + (check_xor F S thresh xorsf) [1.. 2 ^ card S + | Some m \ + (2 ^ m * size_xor F S xorsf m))" + +definition approxmccore :: "'fml \ 'a set \ nat \ nat pmf" +where "approxmccore F S thresh = + map_pmf (approxcore_xors F S thresh) (random_xors S (card S - 1))" + +definition approxmc :: "'fml \ 'a set \ real \ real \ nat \ nat pmf" + where "approxmc F S \ \ n = ( + let thresh = compute_thresh \ in + if card (proj S (sols F)) < thresh then + return_pmf (card (proj S (sols F))) + else + let t = compute_t \ n in + map_pmf (median t) + (prod_pmf {0..i. approxmccore F S thresh)) + )" + +lemma median_commute: + assumes "t \ 1" + shows "(real \ median t) = (\w::nat \ nat. median t (real \ w))" + unfolding median_def map_map[symmetric] + apply (subst Median.map_sort[where f = "\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 (\x. if x < t then y x else def)" + unfolding median_def + by (auto intro!: arg_cong[where f = "\ls. sort ls ! (t div 2)"]) + +definition default_\::"'a set \ nat assg" + where "default_\ S i = (if i < card S - 1 then Some True else None)" + +lemma dom_default_\: + "dom (default_\ S) = {0.._def split: if_splits) + +lemma compute_thresh_bound_4: + assumes "\ > 0" + shows"4 < compute_thresh \" +proof - + have 1: "(1 + \ / (1 + \)) > 1" + using assms + by simp + have 2: "(1 + 1 / \)^2 > 1" + using assms by simp + + define a where "a = (1 + \ / (1 + \)) * (1 + 1 / \)\<^sup>2" + have "a > 1" unfolding a_def + using 1 2 + using less_1_mult by blast + then have "(984 / 10\<^sup>2) * a \ 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 \ S" + shows "satisfies_xor x {x. w x} \ + satisfies_xor x ({x. w x} \ 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 \" + "thresh \ card (proj S (sols F))" + assumes \: "\ > (0::real)" "\ \ 1" + assumes S: "finite S" + shows "measure_pmf.prob (random_xors S (card S - 1)) + {xors. real (approxcore_xors F S thresh xors) \ + {real (card (proj S (sols F))) / (1 + \).. + (1 + \) * real (card (proj S (sols F)))}} \ 0.64" +proof - + + have "ApproxMCCore (sols F) S \ (default_\ S) thresh" + apply unfold_locales + subgoal using dom_default_\ by simp + subgoal using \ 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_\ S)" . + + have " + m < card S \ + {0.. dom xors \ + (\i. i < m \ fst (the (xors i)) \ S) \ + (proj S + (sols (fold enc_xor (map (the \ xors) [0.. + {w. hslice m (\\. xor_hash \ xors) w = + aslice m (default_\ 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 \ dom xors" + by (meson Set.basic_monos(7) Suc(3) atLeastLessThan_iff le0 lessI) + have sp: "fst (the (xors m)) \ 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} = + {\. satisfies_xor xor {x. \ x = Some True}}" + unfolding xor_hash_def + by (clarsimp simp add: x) + + have neut: "\w. + w \ {\. satisfies_xor xor {x. \ x}} \ + restr S w \ {\. satisfies_xor xor {x. \ 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 \ xors) [0.. xors) [0.. + {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) (\\. xor_hash \ xors) w = aslice (Suc m) (default_\ S) \ + hslice m (\\. xor_hash \ xors) w = aslice m (default_\ 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) (\\. xor_hash \ xors) w = aslice (Suc m) (default_\ S) \ + 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_\_def domIff m xor_hash_eq_dom) + + have rhs3: "hslice m (\\. xor_hash \ xors) w = aslice m (default_\ S) \ + xor_hash w xors m = Some True \ + hslice (Suc m) (\\. xor_hash \ xors) w = aslice (Suc m) (default_\ 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_\_def gr_zeroI zero_less_diff) + + have rhs: "{w. hslice (Suc m) (\\. xor_hash \ xors) w = aslice (Suc m) (default_\ S)} = + {w. hslice m (\\. xor_hash \ xors) w = aslice m (default_\ S)} \ + {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 \ xors) [0.. + {w. hslice m (\\. xor_hash \ xors) w = aslice m (default_\ 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 \ + {0.. dom xors \ + (\i. i < m \ fst (the (xors i)) \ S) \ + size_xor F S xors m = + amc.card_slice (\\. xor_hash \ xors) m" for m xors + unfolding size_xor_def amc.card_slice_def + by auto + + have **: " + {0.. dom xors \ + (\i. i < card S - 1 \ fst (the (xors i)) \ S) \ + find (check_xor F S thresh xors) [1..i. (\\. xor_hash \ xors) \ amc.T i) [1.. dom xors \ + (\i. i < card S - 1 \ fst (the (xors i)) \ S) \ + approxcore_xors F S thresh xors = + (\(a,b). a*b) (amc.approxcore (\\. xor_hash \ 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 \\x2. \{0.. dom xors; \i. i < card S - Suc 0 \ fst (the (xors i)) \ S; find (\i. (\\. xor_hash \ xors) \ amc.T i) [Suc 0.. \ x2 < card S\ 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 {\. dom \ = S} {\. dom \ = {0..s w. xor_hash w s) (random_xors S (card S - 1))) + amc.approxcore_fail \ 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 \ by auto + + then have b: "measure_pmf.prob + (random_xors S (card S - 1)) + {xors. + (real ((\(a,b). a*b) (amc.approxcore (\\. xor_hash \ xors)))) + \ + {real (card (proj S (sols F))) / (1 + \).. + (1 + \) * real (card (proj S (sols F)))}} \ 0.36" + unfolding amc.approxcore_fail_def + by (auto simp add: case_prod_unfold Let_def) + + have 1: "x \ set_pmf (random_xors S (card S - Suc 0)) \ + {0.. dom x" for x + by (auto simp add:random_xors_set_pmf[OF S]) + have 2: "x \ set_pmf (random_xors S (card S - Suc 0)) \ + (\i. i < card S - 1 \ fst (the (x i)) \ S)" for x + proof - + assume x: "x \ 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 \ Pow S \ 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 \ S" using xx(2) + unfolding ran_def apply (clarsimp simp add: subset_iff) + by (metis prod.collapse) + then have "fst (the (x i)) \ S" by (simp add: xi) + } + thus "(\i. i < card S - 1 \ fst (the (x i)) \ S)" by auto + qed + + have "measure_pmf.prob (random_xors S (card S - 1)) + {xors. real (approxcore_xors F S thresh xors) \ + {real (card (proj S (sols F))) / (1 + \).. + (1 + \) * real (card (proj S (sols F)))}} = + measure_pmf.prob + (random_xors S (card S - 1)) + {xors. + (real ((\(a,b). a*b) (amc.approxcore (\\. xor_hash \ xors)))) + \ + {real (card (proj S (sols F))) / (1 + \).. + (1 + \) * 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 ((\(a,b). a*b) (amc.approxcore (\\. xor_hash \ xors)))) + \ + {real (card (proj S (sols F))) / (1 + \).. + (1 + \) * real (card (proj S (sols F)))}}" + apply (subst measure_pmf.prob_compl[symmetric]) + by (auto intro!: measure_pmf.measure_pmf_eq) + moreover have "... \ 0.64" + using b + by auto + ultimately show ?thesis by auto +qed + +lemma compute_t_ge1: + assumes "0 < \" "\ < 1" + shows"compute_t \ n \ 1" +proof - + have "ln (1 / \) > 0" + by (simp add: assms) + then have fix_t: "1 \ fix_t \" + 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 \ (f ::nat)" + assumes "p \ (1::real)" "q \ p" "1 /2 \ q" + shows "p ^ s * (1 - p) ^ f \ q ^ s * (1 - q) ^ f" +proof - + have ple: "p * (1-p) \ 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 "... \ + (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 "... \ + (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 \ q" "q \ p" "p \ 1" + shows " + measure_pmf.prob (binomial_pmf n p) {..n div 2} \ + measure_pmf.prob (binomial_pmf n q) {..n div 2}" +proof - + have i: "i \ n div 2 \ + p ^ i * (1 - p) ^ (n - i) \ 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 \: "\ > 0" "\ < 1" + assumes \: "\ > 0" "\ \ 1" + assumes S: "finite S" + shows "measure_pmf.prob (approxmc F S \ \ n) + {c. real c \ + {real (card (proj S (sols F))) / (1 + \).. + (1 + \) * real (card (proj S (sols F)))}} + \ 1 - \" +proof - + define thresh where "thresh = compute_thresh \" + define t where "t = compute_t \ n" + then have t1: "1 \ t" + using compute_t_ge1[OF \] by auto + + have "card (proj S (sols F)) < thresh \ + card (proj S (sols F)) \ thresh" by auto + moreover { + assume "card (proj S (sols F)) < thresh" + then have "approxmc F S \ \ 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 \ + by (auto simp add: mult_le_cancel_left1 mult_le_cancel_right1 divide_le_eq mult_le_cancel_left1) + } + moreover { + assume a: "card (proj S (sols F)) \ thresh" + define Xf where "Xf = (\(i::nat) xs. + approxcore_xors F S thresh (xs i))" + + then have *: "approxmc F S \ \ n = + map_pmf (median t) + (prod_pmf {0..i. approxmccore F S thresh))" + using a + unfolding approxmc_def Let_def thresh_def t_def + by auto + + have **: "map_pmf (real \ median t) + (Pi_pmf {0..i. approxmccore F S thresh)) = + map_pmf (\\. median t (\i. real (Xf i \))) + (prod_pmf {0..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 \ where "\ = (0.14 ::real)" + then have \: "\ > 0" by auto + + have indep:"prob_space.indep_vars + (measure_pmf + (prod_pmf {0..i. random_xors S (card S - 1)))) + (\_. borel) (\x xa. real (Xf x xa)) {0.. \ {0<..<1}" using \ by auto + + from approxcore_xors_eq[OF thresh_def a \ S] + have b1: "1 / 2 + \ \ + measure_pmf.prob (random_xors S (card S - 1)) + {xors. + real (approxcore_xors F S thresh xors) + \ {real (card (proj S (sols F))) / + (1 + \)..(1 + \) * real (card (proj S (sols F)))}}" + unfolding \_def by auto + then have b2: "i < t \ + 1 / 2 + \ \ + measure_pmf.prob + (prod_pmf {0..i. random_xors S (card S - 1))) + {\ \ space + (measure_pmf + (prod_pmf {0..i. random_xors S (card S - 1)))). + real (Xf i \) + \ {real (card (proj S (sols F))) /(1 + \).. + (1 + \) *real (card (proj S (sols F)))}}" for i + unfolding Xf_def apply clarsimp + apply (subst prob_prod_pmf_slice) + by auto + + have ***: "1 - \ + \ measure_pmf.prob (prod_pmf {0..i. random_xors S (card S - 1))) + {\. + median t (\i. real (Xf i \)) + \ {real (card (proj S (sols F))) / + (1 + \)..(1 + \) * real (card (proj S (sols F)))}}" + proof - + have "t = fix_t \ \ t = n \ raw_median_bound \ n < \" + unfolding t_def compute_t_def \_def by auto + moreover { + assume "t = fix_t \" + then have tb:"- ln \ / (2 * \\<^sup>2) \ real t" + unfolding fix_t_def \_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 \ d indep tb] + have ?thesis using b2 by auto + } + moreover { + assume *: "t = n" "raw_median_bound \ n < \" + have s: "1 / 2 - \ = 1 - (1 /2 + \)" + by auto + + have d1: "0 < t" using t1 by linarith + have d2: "1 / 2 + \ \ 0" using \ 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 + \)) {..t div 2} + \ measure_pmf.prob + (prod_pmf {0..i. random_xors S (card S - 1))) + {\. + median t (\i. real (Xf i \)) + \ {real (card (proj S (sols F))) / + (1 + \)..(1 + \) * real (card (proj S (sols F)))}}" + by (auto simp add: prob_space_measure_pmf) + + moreover have "measure_pmf.prob (binomial_pmf t (1 / 2 + \)) {..t div 2} \ \" + 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 \ \ n) + {c. real c + \ {real (card (proj S (sols F))) / + (1 + \)..(1 + \) * real (card (proj S (sols F)))}} = + measure_pmf.prob (map_pmf (real \ median t) + (prod_pmf {0..i. approxmccore F S thresh))) + {c. c \ {real (card (proj S (sols F))) / + (1 + \)..(1 + \) * real (card (proj S (sols F)))}}" + using * by auto + moreover have "... = + measure_pmf.prob (map_pmf (real \ median t) + (map_pmf (\f x. if x \ {0..i. approxmccore F S thresh)))) + {c. c \ {real (card (proj S (sols F))) / + (1 + \)..(1 + \) * real (card (proj S (sols F)))}}" + apply (subst Pi_pmf_default_swap) + by auto + moreover have "... = + measure_pmf.prob (map_pmf (real \ median t) + (Pi_pmf {0..i. approxmccore F S thresh))) + {c. c \ {real (card (proj S (sols F))) / + (1 + \)..(1 + \) * real (card (proj S (sols F)))}}" + by (clarsimp simp add: median_default[symmetric]) + moreover have "... \ 1 - \" + unfolding ** + using *** + by auto + ultimately have ?thesis by auto + } + ultimately show ?thesis by auto +qed + +text \ To simplify further analyses, we can remove the (required) upper bound on epsilon. \ + +definition mk_eps :: "real \ real" + where "mk_eps \ = (if \ > 1 then 1 else \)" + +definition approxmc'::" + 'fml \ 'a set \ + real \ real \ nat \ nat pmf" + where "approxmc' F S \ \ n = + approxmc F S (mk_eps \) \ n" + +corollary approxmc'_sound: + assumes \: "\ > 0" "\ < 1" + assumes \: "\ > 0" + assumes S: "finite S" + shows "prob_space.prob (approxmc' F S \ \ n) + {c. real c \ + {real (card (proj S (sols F))) / (1 + \).. + (1 + \) * real (card (proj S (sols F)))}} + \ 1 - \" +proof - + define \' where "\' = (if \ > 1 then 1 else \)" + have \': "0 < \'" "\' \ 1" + unfolding \'_def using \ by auto + + from approxmc_sound[OF \ \' S] + have *: "prob_space.prob (approxmc F S \' \ n) + {c. real c \ + {real (card (proj S (sols F))) / (1 + \').. + (1 + \') * real (card (proj S (sols F)))}} + \ 1 - \" . + + have **: " + {c. real c \ + {real (card (proj S (sols F))) / (1 + \').. + (1 + \') * real (card (proj S (sols F)))}} + \ + {c. real c \ + {real (card (proj S (sols F))) / (1 + \).. + (1 + \) * real (card (proj S (sols F)))}}" + unfolding \'_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 \'_def mk_eps_def + apply (intro measure_pmf.finite_measure_mono) + using **[unfolded \'_def] + by auto +qed + +text \ This shows we can lift all randomness to the top-level (i.e., eagerly sample it). \ + +definition approxmc_map::" + 'fml \ 'a set \ + real \ real \ nat \ + (nat \ nat \ ('a set \ bool) option) \ + nat" + where "approxmc_map F S \ \ n xorsFs = ( + let \ = mk_eps \ in + let thresh = compute_thresh \ in + if card (proj S (sols F)) < thresh then + card (proj S (sols F)) + else + let t = compute_t \ n in + median t (approxcore_xors F S thresh \ xorsFs))" + +lemma approxmc_map_eq: + shows " + map_pmf (approxmc_map F S \ \ n) + (Pi_pmf {0.. n} def + (\i. random_xors S (card S - 1))) = + approxmc' F S \ \ n" +proof - + define def' where "def' = approxcore_xors F S (compute_thresh (mk_eps \)) def" + + have *: " + map_pmf (median (compute_t \ n)) + (prod_pmf {0.. n} + (\i. map_pmf + (approxcore_xors F S + (compute_thresh (mk_eps \))) + (random_xors S (card S - Suc 0)))) = + map_pmf (median (compute_t \ n)) + (Pi_pmf {0.. n} def' + (\i. map_pmf + (approxcore_xors F S + (compute_thresh (mk_eps \))) + (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/ApproxMCCore.thy b/thys/Approximate_Model_Counting/ApproxMCCore.thy new file mode 100644 --- /dev/null +++ b/thys/Approximate_Model_Counting/ApproxMCCore.thy @@ -0,0 +1,570 @@ +section \ ApproxMCCore definitions \ + +text \ + This section defines the ApproxMCCore locale and various failure events to be used in its probabilistic analysis. + The definitions closely follow Section 4.2 of Chakraborty et al.~\cite{DBLP:conf/ijcai/ChakrabortyMV16}. + Some non-probabilistic properties of the events are proved, most notably, the event inclusions of Lemma 3~\cite{DBLP:conf/ijcai/ChakrabortyMV16}. + Note that ``events'' here refer to subsets of hash functions. +\ + +theory ApproxMCCore imports + ApproxMCPreliminaries +begin + +(* An 'a assg is a finite map from 'a to bool + It is useful to think of 'a as the type of (projected) variables *) +type_synonym 'a assg = "'a \ bool" + +(* Restrict function to a domain (analogous to restrict_map) *) +definition restr :: "'a set \ ('a \ bool) \ 'a assg" + where "restr S w = (\x. if x \ S then Some (w x) else None)" + +lemma restrict_eq_mono: + assumes "x \ y" + assumes "f |` y = g |` y" + shows "f |` x = g |` x" + using assms + by (metis Map.restrict_restrict inf.absorb_iff2) + +(* Projection of a solution set W onto variables S *) +definition proj :: "'a set \ ('a \ bool) set \ 'a assg set" + where "proj S W = restr S ` W" + +lemma card_proj: + assumes "finite S" + shows "finite (proj S W)" "card (proj S W) \ 2 ^ card S" +proof - + have *: "proj S W \ {w. dom w = S}" + unfolding proj_def restr_def + by (auto split: if_splits) + also have 1: "{w. dom w = S} = {w. dom w = S \ ran w \ {True,False}}" + by auto + have f: "finite {w. dom w = S \ ran w \ {True,False}}" + by (simp add: assms finite_set_of_finite_maps) + thus "finite (proj S W)" + using * 1 + by (metis finite_subset) + + have 2:"card {w. dom w = S \ ran w \ {True,False}} = (card {True,False}) ^ card S" + apply (intro card_dom_ran) + using assms by auto + + show "card (proj S W) \ 2 ^ card S" + using * 1 2 + by (metis (no_types, lifting) f card.empty card_insert_disjoint card_mono finite.emptyI finite.insertI insert_absorb insert_not_empty numeral_2_eq_2 singleton_insert_inj_eq) +qed + +lemma proj_mono: + assumes "x \ y" + shows "proj w x \ proj w y" + unfolding proj_def + using assms by blast + +(* We can view nat assg as bit vectors, and take the i-th prefix slices *) +definition aslice :: "nat \ nat assg \ nat assg" + where "aslice i a = a |` {.. n" + assumes "dom a = {.. + ('a assg \ nat assg) \ ('a assg \ nat assg)" + where "hslice i h = aslice i \ h" + +(* Convenient grouping of assumptions and parameters *) +locale ApproxMCCore = + fixes W :: "('a \ bool) set" + fixes S :: "'a set" + fixes \ :: "real" + fixes \ :: "nat assg" + fixes thresh :: "nat" + assumes \: "dom \ = {0..: "\ > 0" + assumes thresh: + "thresh > 4" + "card (proj S W) \ thresh" + assumes S: "finite S" +begin + +lemma finite_proj_S: + shows "finite (proj S W)" + using S by (auto intro!: card_proj) + +definition \ :: "nat \ real" + where "\ i = card (proj S W) / 2 ^ i" + +(* A frequently used expression for the number of projected + witnesses w whose i-th slices match the target *) +definition card_slice ::" + ('a assg \ nat assg) \ + nat \ nat" + where "card_slice h i = + card (proj S W \ {w. hslice i h w = aslice i \})" + +lemma card_slice_anti_mono: + assumes "i \ j" + shows "card_slice h j \ card_slice h i" +proof - + have *: "{.. {..} + \ {w. hslice i h w = aslice i \}" + by (auto intro: restrict_eq_mono[OF *] simp add: hslice_def aslice_def) + thus ?thesis + unfolding card_slice_def + apply (intro card_mono) + subgoal using finite_proj_S by blast + by (auto intro!: proj_mono) +qed + +lemma hslice_eq: + assumes "n \ i" + assumes "\w. dom (h w) = {.. i" + assumes "\w. dom (h w) = {..<(card S - 1)}" + shows "card_slice h i = card_slice h (card S - 1)" + unfolding card_slice_def + apply(subst aslice_eq[OF assms(1)]) + subgoal using \ by auto + apply(subst hslice_eq[OF assms(1)]) + using assms by auto + +(* Defining the various events with respect to a fixed h *) +definition T :: "nat \ + ('a assg \ nat assg) set" + where "T i = {h. card_slice h i < thresh}" + +lemma T_mono: + assumes "i \ j" + shows "T i \ T j" + unfolding T_def + using card_slice_anti_mono[OF assms] + dual_order.strict_trans2 + of_nat_mono + by blast + +lemma \_anti_mono: + assumes "i \ j" + shows "\ i \ \ j" +proof - + have "2^ i \ (2::real) ^ j" + by (simp add: assms) + then show ?thesis unfolding \_def + by (simp add: frac_le) +qed + +lemma card_proj_witnesses: + "card (proj S W) > 0" + using thresh by linarith + +lemma \_strict_anti_mono: + assumes "i < j" + shows "\ i > \ j" +proof - + have "2^ i < (2::real) ^ j" + by (simp add: assms) + then show ?thesis unfolding \_def + using card_proj_witnesses + by (simp add: frac_less2) +qed + +lemma \_gt_zero: + shows "\ i > 0" + unfolding \_def + using card_proj_witnesses + by auto + +definition L :: "nat \ + ('a assg \ nat assg) set" + where " + L i = + {h. real (card_slice h i) < \ i / (1 + \)}" + +definition U :: "nat \ + ('a assg \ nat assg) set" + where " + U i = + {h. real (card_slice h i) \ \ i * (1 + \ / (1 + \))}" + +(* Model of ApproxMC core without random choice of h *) +definition approxcore :: " + ('a assg \ nat assg) \ + nat \ nat" + where " + approxcore h = + (case List.find + (\i. h \ T i) [1.. (2 ^ card S, 1) + | Some m \ + (2 ^ m, card_slice h m))" + +(* The failure event as a set over hashes *) +definition approxcore_fail :: " + ('a assg \ nat assg) set" + where "approxcore_fail = + {h. + let (cells,sols) = approxcore h in + cells * sols \ + { card (proj S W) / (1 + \) .. + (1 + \::real) * card (proj S W)} + }" + +(* This is a global assumption of the locale *) +lemma T0_empty: + shows "T 0 = {}" + unfolding T_def card_slice_def + hslice_def aslice_def + using thresh(2) by auto + +lemma L0_empty: + shows "L 0 = {}" +proof - + have "0 < \ \ + real (card (proj S W)) + < real (card (proj S W)) / (1 + \) \ + False" + by (smt (z3) card_proj_witnesses divide_minus1 frac_less2 nonzero_minus_divide_right of_nat_0_less_iff) + thus ?thesis + unfolding L_def card_slice_def + hslice_def aslice_def \_def + using \ by clarsimp +qed + +lemma U0_empty: + shows "U 0 = {}" +proof - + have *: "(1 + \ / (1 + \)) > 1" + using \ by auto + have **: "U 0 = {}" + unfolding U_def card_slice_def + hslice_def aslice_def \_def + using * + by (simp add: card_proj_witnesses) + thus ?thesis using ** by auto +qed + +lemma real_divide_pos_left: + assumes "(0::real) < a" + assumes "a * b < c" + shows "b < c / a" + using assms + by (simp add: mult.commute mult_imp_less_div_pos) + +lemma real_divide_pos_right: + assumes "a > (0::real)" + assumes "b < a * c" + shows "b / a < c" + using assms + by (simp add: mult.commute mult_imp_div_pos_less) + +(* The first inclusion used in the upper bound of Lemma 3 *) +lemma failure_imp: + shows "approxcore_fail \ + (\i\{1.. (L i \ U i)) \ + -T (card S - 1)" +proof standard + fix h + assume "h \ approxcore_fail" + then obtain cells sols where + h: "approxcore h = (cells, sols)" + "cells * sols \ + { card (proj S W) / (1 + \) .. + (1 + \::real) * card (proj S W)}" (is "_ \ {?lower..?upper}") + unfolding approxcore_fail_def + by auto + + have "List.find (\i. h \ T i) [1.. + List.find (\i. h \ T i) [1.. None" by auto + moreover { + assume "List.find (\i. h \ T i) [1.. T (card S - 1)" + unfolding find_None_iff + by (metis T0_empty atLeastLessThan_iff diff_is_0_eq' diff_less empty_iff gr_zeroI leI less_one not_less_zero set_upt) + } + moreover { + assume "List.find (\i. h \ T i) [1.. None" + then obtain m where + findm: "List.find (\i. h \ T i) [1.. m" "m < card S" + "h \ T m" + "\i. 1 \ i \ i < m \ h \ T i" + unfolding find_Some_iff + using less_Suc_eq_0_disj by auto + + then have 1: "h \ T (m - 1)" + by (metis T0_empty bot_nat_0.not_eq_extremum diff_is_0_eq diff_less empty_iff less_one) + + have "2 ^ m * card_slice h m < ?lower \ + 2 ^ m * card_slice h m > ?upper" + using h unfolding approxcore_def findm by auto + moreover { + assume "2 ^ m * card_slice h m < ?lower" + then have "card_slice h m < ?lower / 2 ^ m" + using real_divide_pos_left + by (metis numeral_power_eq_of_nat_cancel_iff of_nat_mult zero_less_numeral zero_less_power) + + then have "h \ L m" unfolding L_def + by (simp add: \_def mult.commute) + } + moreover { + assume *: "?upper < 2 ^ m * card_slice h m" + have "1 / (1 + \) < 1" + using \ divide_less_eq_1 by fastforce + then have "\ / (1 + \) < \" + using \ + by (metis (no_types, opaque_lifting) add_cancel_left_right div_by_1 divide_divide_eq_left divide_less_eq_1_pos mult.commute nonzero_divide_mult_cancel_left) + then have "card (proj S W) * (1 + \ / (1 + \)) \ ?upper" + using linorder_not_less not_less_iff_gr_or_eq by fastforce + then have "(card (proj S W) * (1 + \ / (1 + \))) / 2 ^ m < card_slice h m" + apply (intro real_divide_pos_right) + using * by auto + then have "h \ U m" unfolding U_def + by (simp add: \_def) + } + ultimately have "h \ L m \ h \ U m" by blast + then have "\m\{Suc 0.. T m \ + h \ T (m - Suc 0) \ + h \ L m \ h \ U m \ + h \ T (card S - Suc 0) \ False" + using m 1 by auto + } + ultimately show + "h \ (\i\{1.. (L i \ U i)) \ + - T (card S - 1)" + by auto +qed + +(* technically not smallest, but doesn't matter for our use *) +lemma smallest_nat_exists: + assumes "P i" "\P (0::nat)" + obtains m where "m \ i" "P m" "\P (m-1)" + using assms +proof (induction i) + case 0 + then show ?case by auto +next + case (Suc i) + then show ?case + by (metis diff_Suc_1 le_Suc_eq) +qed + +lemma mstar_non_zero: + shows "\ \ 0 * (1 + \ / (1 + \)) \ thresh" +proof - + have "\ 0 \ thresh" + unfolding \_def + by (auto simp add: thresh(2)) + thus ?thesis + by (smt (verit, best) \ \_gt_zero divide_pos_pos mult_le_cancel_left2) +qed + +lemma real_div_less: + assumes "c > 0" + assumes "a \ b * (c::nat)" + shows "real a / real c \ b" + by (metis assms(1) assms(2) divide_le_eq of_nat_0_less_iff of_nat_mono of_nat_mult) + +(* Instead of giving mstar explicitly, we'll select it implicitly by the properties below *) +lemma mstar_exists: + obtains m where + "\ (m - 1) * (1 + \ / (1 + \)) > thresh" + "\ m * (1 + \ / (1 + \)) \ thresh" + "m \ card S - 1" +proof - + have e1:"1 + \ / (1 + \) > 1" + by (simp add: \ add_nonneg_pos) + have e2:"1 + \ / (1 + \) < 2" + by (simp add: \ add_nonneg_pos) + have "thresh \ (4::real)" + using thresh(1) by linarith + then have up:"thresh / (1 + \ / (1 + \)) > 2" + by (smt (verit) e1 e2 field_sum_of_halves frac_less2) + + have "card (proj S W) \ 2 * 2 ^ (card S - Suc 0)" + by (metis One_nat_def S Suc_diff_Suc card.empty card_gt_0_iff card_proj(2) diff_zero less_one order_less_le_trans plus_1_eq_Suc power_0 power_Suc0_right power_add thresh(1) thresh(2) zero_neq_numeral) + + then have low:"\ (card S - 1) \ 2" + unfolding \_def + using real_div_less + by (smt (verit) Num.of_nat_simps(2) Num.of_nat_simps(4) Suc_1 nat_zero_less_power_iff numeral_nat(7) of_nat_power plus_1_eq_Suc pos2) + + have pi: "\ (card S - 1) * (1 + \ / (1 + \)) \ thresh" + using up low + by (smt (verit, ccfv_SIG) divide_le_eq e1) + + from smallest_nat_exists[OF pi mstar_non_zero] + show ?thesis + by (metis linorder_not_less that) +qed + +definition mstar :: "nat" + where "mstar = (@m. + \ (m - 1) * (1 + \ / (1 + \)) > thresh \ + \ m * (1 + \ / (1 + \)) \ thresh \ + m \ card S - 1)" + +(* The main inequalities we need from mstar *) +lemma mstar_prop: + shows + "\ (mstar - 1) * (1 + \ / (1 + \)) > thresh" + "\ mstar * (1 + \ / (1 + \)) \ thresh" + "mstar \ card S - 1" + unfolding mstar_def + by (smt (verit) some_eq_ex mstar_exists)+ + +lemma O1_lem: + assumes "i \ m" + shows "(T i - T (i-1)) \ (L i \ U i) \ T m" + using T_mono assms by blast + +lemma O1: + shows "(\i\{1..mstar-3}. + (T i - T (i-1)) \ (L i \ U i)) \ T (mstar-3)" + using T_mono by force + +lemma T_anti_mono_neg: + assumes "i \ j" + shows "- T j \ - T i" + by (simp add: Diff_mono T_mono assms) + +lemma O2_lem: + assumes "mstar < i" + shows "(T i - T (i-1)) \ (L i \ U i) \ -T mstar" +proof - + have "(T i - T (i-1)) \ (L i \ U i) \ -T (i-1)" + by blast + thus ?thesis + by (smt (verit) T_mono ApproxMCCore_axioms One_nat_def Suc_diff_Suc Suc_le_eq assms compl_mono diff_is_0_eq' diff_less_mono leI minus_nat.diff_0 subset_trans) +qed + +lemma O2: + shows "(\i\{mstar.. (L i \ U i)) \ + -T (card S - 1) \ L mstar \ U mstar" +proof - + have 0: "(\i\{mstar.. (L i \ U i)) \ + (T mstar - T (mstar-1)) \ (L mstar \ U mstar) \ + (\i\{mstar+1.. (L i \ U i))" + apply (intro subsetI) + apply clarsimp + by (metis Suc_le_eq atLeastLessThan_iff basic_trans_rules(18)) + + have 1: "(\i\{mstar+1.. (L i \ U i)) \ -T mstar" + apply clarsimp + by (metis (no_types, lifting) ApproxMCCore.T_mono ApproxMCCore_axioms One_nat_def diff_Suc_1 diff_le_mono subsetD) + + have 2: "-T (card S - 1) \ - T mstar" + using T_anti_mono_neg mstar_prop(3) by presburger + + (* Note that the strict inequality is needed here *) + have "thresh \ \ mstar * (1 + \ / (1 + \))" + using mstar_prop(2) thresh by linarith + + then have *: "- T mstar \ U mstar" + unfolding T_def U_def + by auto + + have "(\i\{mstar.. (L i \ U i)) \ + -T (card S - 1) \ + ((T mstar - T (mstar-1)) \ (L mstar \ U mstar)) \ -T mstar" + using 0 1 2 by (smt (z3) Un_iff subset_iff) + + moreover have "... \ L mstar \ U mstar" + using * + by blast + ultimately show ?thesis by auto +qed + +lemma O3: + assumes "i \ mstar - 1" + shows "(T i - T (i-1)) \ (L i \ U i) \ L i" +proof - + have *: "\ i * (1 + \ / (1 + \)) > thresh" + by (smt (verit, ccfv_SIG) \ \_anti_mono assms divide_nonneg_nonneg mstar_prop(1) mult_right_mono) + + have "x \ T i \ x \ U i \ False" for x + unfolding T_def U_def + using * by auto + thus ?thesis + by blast +qed + +lemma union_split_lem: + assumes x: "x \ (\i\{1.. (\i\{1..m-3}. P i) \ + P (m-2) \ + P (m-1) \ + (\i\{m.. {1.. P i" using x by auto + have "i \ {1..m-3} \ i = m-2 \ i = m-1 \ i \ {m..i\{1.. + (\i\{1..m-3}. P i) \ + P (m-2) \ + P (m-1) \ + (\i\{m.. + T (mstar-3) \ + L (mstar-2) \ + L (mstar-1) \ + (L mstar \ U mstar)" +proof - + + have *: "approxcore_fail \ + (\i\{1.. (L i \ U i)) \ -T (card S - 1)" (is "_ \ (\i\{1.. _") + using failure_imp . + + moreover have "... \ + (\i\{1..mstar - 3}. ?P i) \ + ?P (mstar - 2) \ + ?P (mstar - 1) \ + ((\i\{mstar.. -T (card S - 1))" + using + union_split[of "\i. ?P i" "card S" "mstar"] + by blast + moreover have "... \ + T (mstar - 3) \ + L (mstar - 2) \ + L (mstar - 1) \ + (L mstar \ U mstar) + " + using O1 O2 O3 + by (metis (no_types, lifting) One_nat_def Un_mono diff_Suc_eq_diff_pred diff_le_self nat_1_add_1 plus_1_eq_Suc) + ultimately show ?thesis + by (meson order_trans) +qed + +end + +end diff --git a/thys/Approximate_Model_Counting/ApproxMCCoreAnalysis.thy b/thys/Approximate_Model_Counting/ApproxMCCoreAnalysis.thy new file mode 100644 --- /dev/null +++ b/thys/Approximate_Model_Counting/ApproxMCCoreAnalysis.thy @@ -0,0 +1,1273 @@ +section \ ApproxMCCore analysis \ + +text \ + 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}. + \ +theory ApproxMCCoreAnalysis imports + ApproxMCCore +begin + +(* Slicing after a family *) +definition Hslice :: "nat \ + ('a assg \ 'b \ nat assg) \ ('a assg \ 'b \ nat assg)" + where "Hslice i H = (\w s. aslice i (H w s))" + +context prob_space +begin + +lemma indep_vars_prefix: + assumes "indep_vars (\_. count_space UNIV) H J" + shows "indep_vars (\_. count_space UNIV) (Hslice i H) J" +proof - + have "indep_vars (\_. count_space UNIV) (\y. (\x. aslice i x) \ 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 " + (\x. if x < i then Some True else None) \ + {\::nat assg. dom \ = {0..::nat assg. dom \ = {0..::nat assg. dom \ = {0.. ran w \ {True,False}}" + by auto + have "finite {0.. ran w \ {True,False}} = + card {True,False} ^ card {0.. n" + shows "card {\::nat assg. dom \ = {0..::nat assg. dom \ = {0.. n" + assumes "dom \ \ {0..::nat assg. dom \ = {0.. aslice i \ = \} = {}" +proof (intro equals0I) + fix x + assume "x \ {\. dom \ = {0.. aslice i \ = \}" + then have "dom \ = {0.. |` dom \ = \" + unfolding restrict_map_def fun_eq_iff + by (simp add: domIff) + +lemma aslice_refl: + assumes "dom \ = {.. = \" + unfolding aslice_def assms[symmetric] + using restrict_map_dom by auto + +lemma bij_betw_with_inverse: + assumes "f ` A \ B" + assumes "\x. x \ A \ g (f x) = x" + assumes "g ` B \ A" + assumes "\x. x \ B \ 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 \ n" + assumes "dom \ = {0..::nat assg. dom \ = {0.. aslice i \ = \} = + 2 ^ (n-i)" +proof - + have "dom \ = {0.. aslice i \ = \ \ \ = \" for \ + using aslice_refl + by (metis assms(2) lessThan_atLeast0) + then have r2: + "{\::nat assg. dom \ = {0.. aslice i \ = \} = {\}" + by simp + + define f where "f = + (\(\::nat assg,\::nat assg) j. + if j < i then \ j else \ (j-i))" + let ?lhs = "({\. dom \ = {0.. + {\. dom \ = {0.. aslice i \ = \})" + let ?rhs = "{\::nat assg. dom \ = {0.. aslice i \ = \}" + + define finv where "finv = + (\fab::nat assg. + ((\j. fab (j + i)), + fab |` {..x. dom (f x) = {j. if j < i then j \ dom (snd x) else j - i \ dom (fst x)}" + unfolding f_def + by (auto simp add: fun_eq_iff split: if_splits) + have 1: " f ` ?lhs \ ?rhs" + proof standard + fix x + assume x: "x \ f ` ({\. dom \ = {0.. {\. dom \ = {0.. aslice i \ = \})" + obtain a b where ab: "dom a = {0.." + using x unfolding f_def + by (auto simp add: aslice_def restrict_map_def split: if_splits) + show " x \ {\. dom \ = {0.. aslice i \ = \}" + using 1 2 by blast + qed + + have " dom a = {0.. + dom b = {0.. + \x. aslice i b x = \ x \ + \ x < i \ None = b x" for a b x + by (metis atLeastLessThan_iff domIff) + then have 2: "\x. x \ ?lhs \ finv (f x) = x" + unfolding finv_def f_def + by (clarsimp simp add: fun_eq_iff restrict_map_def) + + have 31: "\fab x y. + dom fab = {0.. + \ = aslice i fab \ + fab (x + i) = Some y \ + x < n - i" + by (metis atLeastLessThan_iff domI less_diff_conv) + also have "\fab x. + dom fab = {0.. + \ = aslice i fab \ + x < i \ \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 \ ?lhs" + unfolding finv_def + by (auto simp add: aslice_def split: if_splits) + + have 4: "\x. x \ ?rhs \ 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 {\::nat assg. dom \ = {0.. aslice i \ = \} = + card ({\::nat assg. dom \ = {0.. + {\::nat assg. dom \ = {0.. aslice i \ = \})" + 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 \ bool. dom w = V}" +proof - + have *: "{w :: 'a \ bool. dom w = V} = + {w. dom w = V \ ran w \ {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 {\::nat assg. dom \ = {0.. n" + shows "k_universal k (Hslice i H) D {\. dom \ = {0.._. count_space UNIV) H D" + using kH unfolding k_universal_def + by auto + then have 1: "k_wise_indep_vars k (\_. count_space UNIV) (Hslice i H) D" + unfolding k_wise_indep_vars_def + using indep_vars_prefix + by auto + + have fdom: "finite {\::nat assg. dom \ = {0..::nat assg. dom \ = {0.. {}" + using assg_nonempty_dom + by (metis empty_iff) + have 2: "x \ D \ + uniform_on (Hslice i H x) {\. dom \ = {0.. D" + then have unif: "uniform_on (H x) {\. dom \ = {0... dom \ = {0.. + have *: "{\ \ space M. H x \ \ {\. aslice i \ = \}} = + {\. Hslice i H x \ = \}" + unfolding Hslice_def + by (auto simp add: M) + + have "{\::nat assg. dom \ = {0.. {\. aslice i \ = \} = + {\::nat assg. dom \ = {0.. aslice i \ = \}" + by auto + + then have "(card ({\::nat assg. dom \ = {0.. {\. aslice i \ = \})) + = (if dom \ = {0..::nat assg. dom \ = {0.. {\. aslice i \ = \})) + = indicat_real {\. dom \ = {0.. * 2^(n-i)" + by simp + + from uniform_onD[OF unif, of "{\. aslice i \ = \}"] + have "prob {\. Hslice i H x \ = \} = + real (card ({\. dom \ = {0.. {\. aslice i \ = \})) / + real (card {\::nat assg. dom \ = {0... dom \ = {0.. * 2^(n-i) / + real (card {\::nat assg. dom \ = {0... dom \ = {0.. * 2^(n-i) / 2^n" + by (simp add: card_dom_ran_nat_assg) + moreover have "... = indicat_real {\. dom \ = {0.. / 2^i" + by (simp add: i power_diff) + moreover have "... = indicat_real {\. dom \ = {0.. / real ((2^i)::nat)" by auto + moreover have "... = indicat_real {\. dom \ = {0.. / real (card {\::nat assg. dom \ = {0... Hslice i H x \ = \} = + indicat_real {\. dom \ = {0.. / + real (card {\::nat assg. dom \ = {0.. )^2" + +context + assumes thresh: "thresh \ (1 + \ / (1 + \)) * pivot" +begin + +lemma aux_1: + assumes fin:"finite (set_pmf p)" + assumes \: "\ > 0" + assumes exp: "\ i = measure_pmf.expectation p Y" + assumes var: "\^2 = measure_pmf.variance p Y" + assumes var_bound: "\^2 \ \ i" + shows " + measure_pmf.prob p {y. \ Y y - \ i \ \ \ / (1 + \) * \ i } + \ (1 + \)^2 / (\^2 * \ i) " +proof - + have pvar: "measure_pmf.variance p Y > 0" + using var \ + by (metis zero_less_power) + have kmu: "\ * (\ i) / ((1 + \) * \) > 0" + using \ pvar var var_bound + using \ by auto + have mupos: "\ 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 \ + (\ * (\ i) / ((1 + \) * \))^2 * measure_pmf.variance p Y} \ 1 / (\ * (\ i) / ((1 + \) * \))^2" + by simp + then have ineq1:"measure_pmf.prob p + {y. (Y y - \ i)^2 \ + (\ * (\ i) / ((1 + \) * \))^2 * \^2} \ 1 / (\ * (\ i) / ((1 + \) * \))^2" + using exp var by simp + have "(\y. (Y y - \ i)^2 \ (\ * (\ i) / ((1 + \) * \))^2 * \^2) + = (\y. (Y y - \ i)^2 \ (\ * (\ i) / ((1 + \) * \) * \ )^2)" + by (metis power_mult_distrib) + moreover have "... = (\y. \ Y y - \ i \ \ \ * (\ i) / ((1 + \) * \) * \)" + proof - + have "0 \ \ * \ i / (1 + \)" + by (simp add: \ 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 "... = (\y. \ Y y - \ i \ \ \ * (\ i) / (1 + \))" + using \ by auto + ultimately have simp1:"(\y. (Y y - \ i)^2 \ (\ * (\ i) / ((1 + \) * \))^2 * \^2) + = (\y. \ Y y - \ i \ \ \ / (1 + \) * (\ i))" + by auto + + have "\^2/(\ i)^2 \ (\ i)/(\ i)^2" + using var_bound \_gt_zero + by (simp add: divide_right_mono) + moreover have "... = 1 / (\ i)" + by (simp add: power2_eq_square) + ultimately have simp2: "\^2/(\ i)^2 \ 1 / (\ i)" by auto + + have "measure_pmf.prob p {y. \ Y y - \ i \ \ \ / (1 + \) * (\ i)} + \ 1 / (\ * (\ i) / ((1 + \) * \))^2" + using ineq1 simp1 + by auto + moreover have "... = (1 + \)^2 / \^2 * \^2/(\ i)^2" + by (simp add: power_divide power_mult_distrib) + moreover have "... \ (1 + \)^2 / \^2 * (1 / (\ i))" + using simp2 + by (smt (verit, best) \ divide_pos_pos mult_left_mono times_divide_eq_right zero_less_power) + ultimately have "measure_pmf.prob p {y. \ Y y - \ i \ \ \ / (1 + \) * (\ i)} + \ (1 + \)^2 / (\^2 * (\ 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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0.. card S - 1" + shows " + measure_pmf.prob p + {s. \ card_slice ((\w. H w s)) i - \ i \ \ \ / (1 + \) * \ i} + \ (1 + \)^2 / (\^2 * \ i)" +proof - + + (* The variance for i-th slice *) + define var where "var = + (\i. measure_pmf.variance p + (\s. real (card (proj S W \ + {w. Hslice i H w s = aslice i \}))))" + + from prob_space.universal_prefix_family_from_hash[OF _ _ ind] + have hf: "prob_space.k_universal (measure_pmf p) 2 + (Hslice i H) {\::'a assg. dom \ = S} {\. dom \ = {0.. {\. dom \ = S}" + unfolding proj_def restr_def by (auto split:if_splits) + + have ain: "aslice i \ \ {\. dom \ = {0.. + 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 + (\s. real (card (proj S W \ + {w. Hslice i H w s = aslice i \}))) = + real (card (proj S W)) / + real (card {\::nat assg. dom \ = {0..::nat assg. dom \ = {0.. i" + unfolding \_def + by (simp add: measure_pmf.card_dom_ran_nat_assg) + + have "proj S W \ + {w. Hslice i H w s = aslice i \} = + proj S W \ {w. hslice i (\w. H w s) w = aslice i \}" for s + unfolding proj_def Hslice_def hslice_def + by auto + then have extend_card_slice: + "\s. (card (proj S W \ {w. Hslice i H w s = aslice i \})) = + card_slice ((\w. H w s)) i" + unfolding card_slice_def by auto + + have mu_exp:" \ i = measure_pmf.expectation p + (\s. real (card (proj S W \ {w. Hslice i H w s = aslice i \})))" + using exp exp_mu by auto + + from two_universal_variance_bound[OF p hf finite_proj_S pSW ain] + have " + var i \ + measure_pmf.expectation p + (\s. real (card (proj S W \ + {w. Hslice i H w s = aslice i \})))" + unfolding var_def . + then have var_bound: "var i \ \ i" using exp exp_mu + by linarith + + have "var i \ 0" unfolding var_def by auto + then have "var i > 0 \ var i = 0" by auto + moreover { + assume "var i = 0" + + then have 1: " + measure_pmf.expectation p + (\s. (card_slice (\w. H w s) i - \ i)^2) = 0" + unfolding var_def extend_card_slice mu_exp by auto + + have 2: "measure_pmf.expectation p + (\s. (card_slice (\w. H w s) i - \ i)^2) = + sum (\s. (card_slice (\w. H w s) i - \ i)^2 * pmf p s) (set_pmf p)" + using assms by (auto intro!: integral_measure_pmf_real) + + have "\x \ set_pmf p. (card_slice (\w. H w x) i - \ i)^2 * pmf p x = 0" + apply (subst sum_nonneg_eq_0_iff[symmetric]) + using 1 2 p by auto + then have *: "\x. x \ set_pmf p \ (card_slice (\w. H w x) i - \ i)^2 = 0" + by (meson mult_eq_0_iff set_pmf_iff) + + have **: "(1 + \)^2 / (\^2 * \ i) > 0" + using \_gt_zero \ by auto + have "\ / (1 + \) * \ i > 0" + using \_gt_zero \ by auto + then have "\s. s \ set_pmf p \ \ card_slice ((\w. H w s)) i - \ i \ < \ / (1 + \) * \ i" + using * by auto + then have " + measure_pmf.prob p + {s. \ card_slice ((\w. H w s)) i - \ i \ \ \ / (1 + \) * \ i } = 0" + apply (subst measure_pmf_zero_iff) + using linorder_not_less by auto + then have " + measure_pmf.prob p + {s. \ card_slice ((\w. H w s)) i - \ i \ \ \ / (1 + \) * \ i } + \ (1 + \)^2 / (\^2 * \ 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 + (\s. real (card (proj S W \ + {w. Hslice i H w s = aslice i \})))" + 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 \ \ 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. \ card_slice ((\w. H w s)) i - \ i \ \ \ / (1 + \) * \ i } + \ (1 + \)^2 / (\^2 * \ 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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0.. card S - 1" + assumes \: "\ \ 1" + shows "measure_pmf.prob p + {s. real(card_slice ((\w. H w s)) i) \ \ * \ i } + \ 1 / (1 + (1 - \)^2 * \ i)" +proof - + have *: "(\s. (0::real) \ card_slice ((\w. H w s)) i)" + by simp + from spec_paley_zygmund_inequality[OF p * \] + have paley_zigmund: + "(measure_pmf.variance p (\s. real(card_slice ((\w. H w s)) i) ) + + (1-\)^2 * (measure_pmf.expectation p (\s. card_slice ((\w. H w s)) i))^2) * + measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) > \ * measure_pmf.expectation p (\s. real(card_slice ((\w. H w s)) i) )} \ + (1-\)^2 * (measure_pmf.expectation p (\s. real(card_slice ((\w. H w s)) i) ))^2" + by auto + define var where "var = (\i. measure_pmf.variance p + (\s. real (card (proj S W \ + {w. Hslice i H w s = aslice i \}))))" + + from prob_space.universal_prefix_family_from_hash[OF _ _ ind] + have hf: "prob_space.k_universal (measure_pmf p) 2 + (Hslice i H) {\::'a assg. dom \ = S} {\. dom \ = {0.. {\. dom \ = S}" + unfolding proj_def restr_def + by (auto split:if_splits) + + have ain: "aslice i \ \ {\. dom \ = {0.. + 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 + (\s. real (card (proj S W \ + {w. Hslice i H w s = aslice i \}))) = + real (card (proj S W)) / + real (card {\::nat assg. dom \ = {0..::nat assg. dom \ = {0.. i" + unfolding \_def + by (simp add: measure_pmf.card_dom_ran_nat_assg) + + have "proj S W \ + {w. Hslice i H w s = aslice i \} = + proj S W \ {w. hslice i (\w. H w s) w = aslice i \}" for s + unfolding proj_def Hslice_def hslice_def + by auto + + then have extend_card_slice:"\s. (card (proj S W \ + {w. Hslice i H w s = aslice i \})) = + card_slice ((\w. H w s)) i" + unfolding card_slice_def by auto + + have mu_exp:" \ i = measure_pmf.expectation p + (\s. real (card (proj S W \ + {w. Hslice i H w s = aslice i \})))" + using exp exp_mu by auto + + from two_universal_variance_bound[OF p hf finite_proj_S pSW ain] + have " + var i \ + measure_pmf.expectation p + (\s. real (card (proj S W \ + {w. Hslice i H w s = aslice i \})))" + unfolding var_def . + then have var_bound: "var i \ \ i" using exp exp_mu + by linarith + + have pos_mu: "\ i > 0" + unfolding \_def + by (simp add: card_proj_witnesses) + + have comp: "measure_pmf.prob p + {s. \ * \ i < real (card_slice (\w. H w s) i)} = + (1 - measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) \ \ * \ 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 (\s. card_slice ((\w. H w s)) i) \ \ i" + using var_bound + unfolding var_def + by (simp add: extend_card_slice) + then have + "(measure_pmf.variance p (\s. real(card_slice ((\w. H w s)) i)) + + (1-\)^2 * (measure_pmf.expectation p (\s. real(card_slice ((\w. H w s)) i) ) )^2) + * measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) > \ * measure_pmf.expectation p (\s. real(card_slice ((\w. H w s)) i) )} \ + (\ i + (1-\)^2 * (measure_pmf.expectation p ( \s. real(card_slice ((\w. H w s)) i) ) )^2) + * measure_pmf.prob p + {s. real(card_slice ((\w. H w s)) i) > \ * measure_pmf.expectation p (\s. real(card_slice ((\w. H w s)) i) )}" + by (auto intro!: mult_right_mono) + moreover have + "... \ (\ i + (1-\)^2 * (measure_pmf.expectation p ( \s. real(card_slice ((\w. H w s)) i) ) )^2) + * measure_pmf.prob p + {s. real(card_slice ((\w. H w s)) i) > \ * measure_pmf.expectation p (\s. real(card_slice ((\w. H w s)) i) )}" + by fastforce + ultimately have + "(\ i + (1-\)^2 * (\ i)^2) * measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) > \ * \ i} \ (1-\)^2 * (\ i)^2" + unfolding mu_exp extend_card_slice + using paley_zigmund by linarith + then have + "(1 + (1-\)^2 * (\ i)) * (\ i) * measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) > \ * \ i} \ (1-\)^2 * (\ i) * (\ i)" + by (smt (verit) left_diff_distrib' more_arith_simps(11) mult_cancel_right mult_cancel_right2 power2_eq_square) + then have + "(1 + (1-\)^2 * (\ i)) * measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) > \ * \ i} \ (1-\)^2 * (\ i)" + using pos_mu by force + then have + "(1 + (1-\)^2 * (\ i)) * (1 - measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) \ \ * \ i}) \ (1-\)^2 * (\ i)" + using comp by auto + then have + "(1 + (1-\)^2 * (\ i)) - (1 + (1-\)^2 * (\ i)) * measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) \ \ * \ i} \ (1-\)^2 * (\ i)" + by (simp add: right_diff_distrib) + then have + "(1 + (1-\)^2 * (\ i)) * measure_pmf.prob p {s. real(card_slice ((\w. H w s)) i) \ \ * \ i} \ 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_\: + assumes "k \ i" + shows"\ i * 2^k = \ (i-k)" + unfolding \_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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0.._up: "\ \ 1" + shows " + measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) + \ 1 / 62.5" +proof - + have "1 + 1 / \ > 0" + by (simp add: \ pos_add_strict) + then have pos_pivot: "pivot > 0" + unfolding pivot_def + by simp + + have "mstar \ 4 \ mstar < 4" by auto + moreover { + assume "mstar < 4" + then have " measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) + \ 1 / 62.5" + by (auto simp add: T0_empty) + } + moreover { + assume lo_mstar: "mstar \ 4" + + have extend_mu3: "\ (mstar-1) * 2^2 = \ (mstar-3)" + apply (subst shift_\) + 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 + \ / (1 + \) \ 3 / 2" + using \ assms(3) by auto + have mu_mstar_3_gt_zero: "\ (mstar - 3) / 4 > 0" + using \_gt_zero by simp + + from mstar_prop(1) + have "thresh < \ (mstar - 1) *2^2 / 4 * (1 + \ / (1 + \))" + by auto + also have "... = \ (mstar - 3) / 4 * (1 + \ / (1 + \))" + unfolding extend_mu3 by auto + also have "... \ \ (mstar - 3) / 4 * (3 / 2)" + apply (intro mult_left_mono) + using ****** mu_mstar_3_gt_zero by auto + also have "... = 3 / 8 * \ (mstar - 3)" + by auto + finally have thresh2mu: "thresh < 3 / 8 * \ (mstar - 3)" . + + have "1 + \ / (1 + \) > 0" + by (simp add: add_nonneg_pos \) + then have "\ (mstar-1) > pivot" (* pivot = thresh / (1 + \/(1+\)) *) + using mstar_prop(1) thresh + by (smt (verit) nonzero_mult_div_cancel_right real_divide_pos_left) + then have lo_mu_mstar_3: "\ (mstar-3) > 4*pivot" + using extend_mu3 + by simp + + have mstar_3: "mstar-3 \ 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 \ 1+ 25 / 64 * \ (mstar - 3) " + using lo_mu_mstar_3 + by auto + + have "1 + 1/\ \ 2" + by (simp add: \ assms(3)) + then have "(1 + 1/\)^2 \ 2^2" + by (smt (verit) power_mono) + then have ***: " 1 + 25/64 * 4 * 4*9.84 \ 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 (\w. H w s) (mstar - 3)) \ + 3 / 8 * \ (mstar - 3)} + \ 1 / (1 + (1 - 3 / 8)\<^sup>2 * \ (mstar - 3))" + apply(intro analysis_1_2[OF p ind mstar_3]) + by auto + also have "... = 1 / (1 + (5 / 8)^2 * \ (mstar-3))" + by simp + also have "... = 1 / (1 + 25 / 64 * \ (mstar-3))" + unfolding * by auto + also have "... \ 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 "... \ 1 / (1+ 25/64 * 4 * 4*9.84)" + using *** **** + by (smt (verit) frac_le) + also have "... \ 1 / 62.5" + by simp + finally have *****: "measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 3)) \ 3 / 8 * \ (mstar - 3)} \ 1 / 62.5" + by auto + + have "measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) + = measure_pmf.prob p {s. real (card_slice (\w. H w s) (mstar - 3)) < thresh}" + unfolding T_def + by auto + also have "... \ measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 3)) \ 3 / 8 * \ (mstar - 3)}" + using thresh2mu by (auto intro!: measure_pmf.finite_measure_mono) + also have "... \ 1 / 62.5" + using ***** + by auto + finally have "measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) \ 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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0..s w. H w s) p) (T (mstar-3)) + \ 1 / 10.84" +proof - + have "1 + 1 / \ > 0" + by (simp add: \ pos_add_strict) + then have pos_pivot: "pivot > 0" + unfolding pivot_def + by simp + + have "mstar \ 4 \ mstar < 4" by auto + moreover { + assume "mstar < 4" + then have " measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) + \ 1 / 10.84" + by (auto simp add: T0_empty) + } + moreover { + assume lo_mstar: "mstar \ 4" + + have extend_mu3: "\ (mstar-1) * 2^2 = \ (mstar-3)" + apply (subst shift_\) + subgoal using lo_mstar semiring_norm(87) by linarith + using diff_Suc_eq_diff_pred eval_nat_numeral(3) by presburger + + have "\ / (1 + \) < 1" + using \ by auto + then have ******: "1 + \ / (1 + \) < 2" + using \ by auto + have mu_mstar_3_gt_zero: "\ (mstar - 3) / 4 > 0" + using \_gt_zero by simp + + from mstar_prop(1) + have "thresh < \ (mstar - 1) * (1 + \ / (1 + \))" + by auto + also have "... = \ (mstar - 1) *2^2 / 4 * (1 + \ / (1 + \))" + by auto + also have "... = \ (mstar - 3) / 4 * (1 + \ / (1 + \))" + unfolding extend_mu3 by auto + also have "... < \ (mstar - 3) / 4 * 2" + apply (intro mult_strict_left_mono) + using ****** mu_mstar_3_gt_zero by auto + also have "... = 1 / 2 * \ (mstar - 3)" + by auto + finally have thresh2mu: "thresh < 1 / 2 * \ (mstar - 3)" . + + have "1 + \ / (1 + \) > 0" + by (simp add: add_nonneg_pos \) + then have "\ (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: "\ (mstar-3) > 4*pivot" + using extend_mu3 + by simp + + have mstar_3: "mstar-3 \ 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 \ 1+ 1/4 * \ (mstar - 3) " + using lo_mu_mstar_3 + by auto + + have "(1 + 1/\)^2 > 1^2" + by (simp add: \) + then have ***: " 1 + 1/4 * 4*9.84 \ 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 (\w. H w s) (mstar - 3)) \ + 1 / 2 * \ (mstar - 3)} + \ 1 / (1 + (1 - 1 / 2)\<^sup>2 * \ (mstar - 3))" + apply(intro analysis_1_2[OF p ind mstar_3]) + by auto + also have "... = 1 / (1 + 1 / 4 * \ (mstar-3))" + using * by force + also have "... \ 1 / (1+ 1/4 * 4*pivot)" + using ** + by (simp add: add_nonneg_pos frac_le pos_pivot) + also have "... \ 1 / (1+ 1/4 * 4 *9.84)" + using *** **** + by (smt (verit) frac_le) + also have "... \ 1 / 10.84" + by simp + finally have *****: "measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 3)) \ 1/2 * \ (mstar - 3)} \ 1 / 10.84" . + + have "measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) + = measure_pmf.prob p {s. real (card_slice (\w. H w s) (mstar - 3)) < thresh}" + unfolding T_def + by auto + also have "... \ measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 3)) \ 1 / 2 * \ (mstar - 3)}" + using thresh2mu by (auto intro!: measure_pmf.finite_measure_mono) + also have "... \ 1 / 10.84" + using ***** + by auto + finally have "measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) \ 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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0..s w. H w s) p) (L (mstar-2)) \ 1 / 20.68" +proof - + have epos: "1 + 1 / \ > 0" + by (simp add: \ pos_add_strict) + then have pos_pivot: "pivot > 0" + unfolding pivot_def + by simp + + have "mstar \ 3 \ mstar < 3" by auto + moreover { + assume "mstar < 3" + then have " measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-2)) + \ 1 / 20.68" + by (auto simp add: L0_empty) + } + moreover { + assume lo_mstar: "mstar \ 3" + + have extend_mu2: "\ (mstar-1) * 2^1 = \ (mstar-2)" + apply (subst shift_\) + subgoal using lo_mstar by linarith + by (metis diff_diff_left one_add_one) + + have "1 + \ / (1 + \) > 0" + by (simp add: add_nonneg_pos \) + then have "\ (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: "\ (mstar-2) > 2*pivot" + using extend_mu2 + by simp + + have mstar_2: "mstar-2 \ card S - 1" + using lo_mstar + using diff_le_self dual_order.trans mstar_prop(3) by blast + + have beta:"1/(1+\) \ (1::real)" + using \ by auto + have pos: "(1 / (1 + 1/\))\<^sup>2 > 0" + using epos by auto + then have *: "1 + (1 / (1 + 1/\))\<^sup>2 * 2*pivot \ 1 + (1 / (1 + 1/\))\<^sup>2 * \ (mstar - 2)" + using lo_mu_mstar_2 + by auto + + have "1 - 1/(1+\) = 1 / (1 + 1/\)" + by (smt (verit, ccfv_threshold) \ conjugate_exponent_def conjugate_exponent_real(1)) + then have **: "(1 - 1/(1+\))^2 = (1 / (1 + 1/\))^2" + by simp + have ***: "1 + (1 / (1 + 1/\))\<^sup>2 * 2 * 9.84 * ( 1 + 1/\ )^2 + = 1 + (1 / (1 + 1/\))\<^sup>2 * ( 1 + 1/\ )^2 * 2 * 9.84" + by (simp add: mult.commute) + have ****: "(1 / (1 + 1/\))\<^sup>2 * ( 1 + 1/\ )^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 (\w. H w s) (mstar - 2)) \ 1/(1+\) * \ (mstar - 2)} + \ 1 / (1 + (1 - 1/(1+\))\<^sup>2 * \ (mstar - 2))" + by auto + also have "... = 1 / (1 + (1 / (1 + 1/\))\<^sup>2 * \ (mstar - 2))" + unfolding ** by auto + also have "... \ 1 / (1 + (1 / (1 + 1/\))\<^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/\))\<^sup>2 * 2 * 9.84 * ( 1 + 1/\ )^2)" + unfolding pivot_def by auto + also have "... = 1 / 20.68" + unfolding *** **** by auto + finally have *****: "measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 2)) \ 1/(1+\) * \ (mstar - 2)} \ 1 / 20.68" . + + have "measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 2)) < 1/(1+\) * \ (mstar - 2)} + \ measure_pmf.prob p {s. real (card_slice (\w. H w s) (mstar - 2)) \ 1/(1+\) * \ (mstar - 2)}" + by (auto intro!: measure_pmf.finite_measure_mono) + then have ******: "measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 2)) < 1/(1+\) * \ (mstar - 2)} + \ 1 / 20.68" + using ***** by auto + + have "measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-2)) + = measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 2)) < 1/(1+\) * \ (mstar - 2)}" + unfolding L_def + by auto + also have "... \ 1 / 20.68" + using ****** by auto + finally have "measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-2)) \ 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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0..s w. H w s) p) (L (mstar-1)) \ 1 / 10.84" +proof - + have epos: "1 + 1 / \ > 0" + by (simp add: \ pos_add_strict) + then have pos_pivot: "pivot > 0" + unfolding pivot_def + by simp + + have "mstar \ 2 \ mstar < 2" by auto + moreover { + assume "mstar < 2" + then have " measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-2)) + \ 1 / 10.84" + by (auto simp add: L0_empty) + } + moreover { + assume lo_mstar: "mstar \ 2" + + have "1 + \ / (1 + \) > 0" + by (simp add: add_nonneg_pos \) + then have lo_mu_mstar_1: "\ (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 \ card S - 1" + using lo_mstar diff_le_self dual_order.trans mstar_prop(3) by blast + + have beta: "1/(1+\) \ (1::real)" + using \ by auto + have "(1 / (1 + 1/\))\<^sup>2 > 0" + using epos by auto + then have *: "1 + (1 / (1 + 1/\))\<^sup>2 * pivot \ 1 + (1 / (1 + 1/\))\<^sup>2 * \ (mstar - 1)" + using lo_mu_mstar_1 + by auto + + have "1 - 1/(1+\) = 1 / (1 + 1/\)" + by (smt (verit, ccfv_threshold) \ conjugate_exponent_def conjugate_exponent_real(1)) + then have **: "(1 - 1/(1+\))^2 = (1 / (1 + 1/\))^2" + by simp + have ***: "1 + (1 / (1 + 1/\))\<^sup>2 * 9.84 * ( 1 + 1/\ )^2 + = 1 + (1 / (1 + 1/\))\<^sup>2 * ( 1 + 1/\ )^2 * 9.84" + by (simp add: mult.commute) + have ****: "(1 / (1 + 1/\))\<^sup>2 * ( 1 + 1/\ )^2 = 1" + by (metis (mono_tags, opaque_lifting) \0 < 1 + 1 / \\ 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 (\w. H w s) (mstar - 1)) \ 1/(1+\) * \ (mstar - 1)} + \ 1 / (1 + (1 - 1/(1+\))\<^sup>2 * \ (mstar - 1))" + by auto + moreover have "... = 1 / (1 + (1 / (1 + 1/\))\<^sup>2 * \ (mstar - 1))" + unfolding ** by auto + moreover have "... \ 1 / (1 + (1 / (1 + 1/\))\<^sup>2 * pivot)" + using * + by (smt (verit) \0 < (1 / (1 + 1 / \))\<^sup>2\ frac_le pos_pivot zero_le_mult_iff) + moreover have "... = 1 / (1 + (1 / (1 + 1/\))\<^sup>2 * 9.84 * ( 1 + 1/\ )^2)" + unfolding pivot_def by auto + moreover have "... = 1 / (1 + (1 / (1 + 1/\))\<^sup>2 * ( 1 + 1/\ )^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 (\w. H w s) (mstar - 1)) \ 1/(1+\) * \ (mstar - 1)} \ 1 / 10.84" + by linarith + have "measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 1)) < 1/(1+\) * \ (mstar - 1)} + \ measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 1)) \ 1/(1+\) * \ (mstar - 1)}" + by (auto intro!: measure_pmf.finite_measure_mono) + then have ******: "measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 1)) < 1/(1+\) * \ (mstar - 1)} + \ 1 / 10.84" + using ***** by auto + + have "measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-1)) + = measure_pmf.prob p + {s. real (card_slice (\w. H w s) (mstar - 1)) < 1/(1+\) * \ (mstar - 1)}" + unfolding L_def + by auto + moreover have "... \ 1 / 10.84" + using ****** by auto + ultimately have "measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-1)) \ 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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0..s w. H w s) p) (L mstar \ U mstar) \ 1 / 4.92" +proof - + have "1 + 1 / \ > 0" + by (simp add: \ pos_add_strict) + then have pos_pivot: "pivot > 0" + unfolding pivot_def + by simp + + have "mstar \ 1 \ mstar < 1" by auto + moreover { + assume "mstar < 1" + have LU0_empty: "L mstar \ U mstar = {}" + using L0_empty U0_empty + using \mstar < 1\ less_one by auto + then have "measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar) + \ 1 / 4.92" + by auto + } + moreover { + assume lo_mstar: "mstar \ 1" + have extend_mu: "\ mstar * 2^1 = \ (mstar-1)" + using lo_mstar + apply (subst shift_\) + by auto + + have "1 + \ / (1 + \) > 0" + by (simp add: add_nonneg_pos \) + then have "\ (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: "\ mstar > pivot / 2" + using extend_mu + by auto + + have mstar: "mstar \ card S - 1" + using lo_mstar + using diff_le_self dual_order.trans mstar_prop(3) by blast + + have "\*(1+1/\) = 1+\" + by (smt (verit) \ add_divide_eq_if_simps(1) divide_cancel_right divide_self_if nonzero_mult_div_cancel_left) + then have *: "9.84 * \^2*(1+1/\)^2 / 2 = 9.84 * (1+\)^2 / 2" + by (metis (mono_tags, opaque_lifting) more_arith_simps(11) power_mult_distrib) + + have "\^2 * \ mstar \ \^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 **: "\^2 * \ mstar \ 9.84 * (1+\)^2 / 2" + unfolding pivot_def using * by auto + + from analysis_1_1[OF p ind mstar] + have "measure_pmf.prob p + {s. \ card_slice ((\w. H w s)) mstar - \ mstar \ \ \ / (1 + \) * \ mstar } + \ (1 + \)^2 / (\^2 * \ mstar)" + by auto + also have "... \ (1 + \)^2 / (9.84 * (1+\)^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 + \)^2 / (4.92 * (1+\)^2)" + by simp + also have "... = 1 / 4.92" + using \ by simp + finally have *******: "measure_pmf.prob p + {s. \ card_slice ((\w. H w s)) mstar - \ mstar \ \ \ / (1 + \) * \ mstar } + \ 1 / 4.92" . + + have "\ mstar / (1 + \) - \ mstar = \ mstar * (1 / (1+\) - 1)" + by (simp add: right_diff_distrib') + also have "... = \ mstar * (- \ / (1+\))" + by (smt (verit) \ add_divide_distrib div_self minus_divide_left) + finally have ***: "\ mstar / (1 + \) - \ mstar = \ mstar * (- \ / (1+\))" . + + have "{h. real (card_slice h mstar) \ \ mstar / (1 + \)} + = {h. real (card_slice h mstar) - \ mstar \ \ mstar / (1 + \) - \ mstar}" + by auto + also have "... = {h. real (card_slice h mstar) - \ mstar \ \ mstar * (- \ / (1+\))}" + using *** by auto + finally have ****: " + {h. real (card_slice h mstar) \ \ mstar / (1 + \)} = + {h. real (card_slice h mstar) - \ mstar \ \ mstar * (- \ / (1+\))}" . + + have "L mstar + = {h. real (card_slice h mstar) < \ mstar / (1 + \)}" + unfolding L_def by auto + also have "...\ {h. real (card_slice h mstar) \ \ mstar / (1 + \)}" + by auto + also have "... = {h. real (card_slice h mstar) - \ mstar \ \ mstar * (- \ / (1+\))}" + unfolding **** by auto + finally have extend_L: "L mstar \ {h. real (card_slice h mstar) - \ mstar \ \ mstar * (- \ / (1+\))}" . + + have *****: "\ mstar * (1 + \ / (1+\)) - \ mstar = \ mstar * (\ / (1+\))" + 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) \ \ mstar * (1 + \ / (1+\))}" + unfolding U_def by auto + have "{h. real (card_slice h mstar) \ \ mstar * (1 + \ / (1+\))} + = {h. real (card_slice h mstar) - \ mstar \ \ mstar * (1 + \ / (1+\)) - \ mstar}" + by auto + also have "... = {h. real (card_slice h mstar) - \ mstar \ \ mstar * (\ / (1+\))}" + unfolding ***** by auto + finally have extend_U: "U mstar = {h. real (card_slice h mstar) - \ mstar \ \ mstar * (\ / (1+\))}" + using ****** by auto + + have "L mstar \ U mstar \ + {h. real (card_slice h mstar) - \ mstar \ \ mstar * (- \ / (1+\))} + \ {h. real (card_slice h mstar) - \ mstar \ \ mstar * (\ / (1+\))}" + unfolding extend_U + using extend_L + by auto + also have "... = {h. \ real (card_slice h mstar) - \ mstar \ \ \ mstar * (\ / (1+\))}" + by auto + finally have extend_LU: "L mstar \ U mstar \ {h. \ real (card_slice h mstar) - \ mstar \ \ \ mstar * (\ / (1+\))}" . + + have "measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar) + \ measure_pmf.prob (map_pmf (\s w. H w s) p) {h. \ real (card_slice h mstar) - \ mstar \ \ \ mstar * (\ / (1+\))}" + using extend_LU + by (auto intro!: measure_pmf.finite_measure_mono) + also have "... = measure_pmf.prob p + {s. \ real (card_slice (\w. H w s) mstar) - \ mstar \ \ \ / (1 + \) * \ mstar }" + by (simp add: mult.commute) + also have "... \ 1 / 4.92" + using ******* by auto + finally have "measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar) \ 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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0.._up: "\ \ 1" + shows " + measure_pmf.prob (map_pmf (\s w. H w s) p) + approxcore_fail \ 0.36" +proof - + have "measure_pmf.prob (map_pmf (\s w. H w s) p) approxcore_fail + \ measure_pmf.prob (map_pmf (\s w. H w s) p) + (T (mstar-3) \ + L (mstar-2) \ + L (mstar-1) \ + (L mstar \ U mstar))" + using failure_bound + by (auto intro!: measure_pmf.finite_measure_mono) + + moreover have "... \ + measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3) \ L (mstar-2) \ L (mstar-1)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar)" + by (auto intro!: measure_pmf.finite_measure_subadditive) + moreover have "... \ + measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3) \ L (mstar-2)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-1)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar)" + by (auto intro!: measure_pmf.finite_measure_subadditive) + moreover have "... \ + measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-2)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-1)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar)" + by (auto intro!: measure_pmf.finite_measure_subadditive) + moreover have "... \ 1/62.5 + 1/20.68 + 1/10.84 + 1/4.92" + using analysis_2_1[OF p ind \_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 + {\::'a assg. dom \ = S} + {\::nat assg. dom \ = {0..s w. H w s) p) + approxcore_fail \ 0.44" +proof - + have "measure_pmf.prob (map_pmf (\s w. H w s) p) approxcore_fail + \ measure_pmf.prob (map_pmf (\s w. H w s) p) + (T (mstar-3) \ + L (mstar-2) \ + L (mstar-1) \ + (L mstar \ U mstar))" + using failure_bound + by (auto intro!: measure_pmf.finite_measure_mono) + + moreover have "... \ + measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3) \ L (mstar-2) \ L (mstar-1)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar)" + by (auto intro!: measure_pmf.finite_measure_subadditive) + moreover have "... \ + measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3) \ L (mstar-2)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-1)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar)" + by (auto intro!: measure_pmf.finite_measure_subadditive) + moreover have "... \ + measure_pmf.prob (map_pmf (\s w. H w s) p) (T (mstar-3)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-2)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L (mstar-1)) + + measure_pmf.prob (map_pmf (\s w. H w s) p) (L mstar \ U mstar)" + by (auto intro!: measure_pmf.finite_measure_subadditive) + moreover have "... \ 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/ApproxMCPreliminaries.thy b/thys/Approximate_Model_Counting/ApproxMCPreliminaries.thy new file mode 100644 --- /dev/null +++ b/thys/Approximate_Model_Counting/ApproxMCPreliminaries.thy @@ -0,0 +1,342 @@ +section \Preliminary probability/UHF lemmas\ + +text \ This section proves some simplified/specialized forms of lemmas + that will be used in the algorithm's analysis later. \ + +theory ApproxMCPreliminaries imports + Frequency_Moments.Probability_Ext + Concentration_Inequalities.Paley_Zygmund_Inequality +begin + +lemma card_inter_sum_indicat_real: + assumes "finite A" + shows "card (A \ B) = sum (indicat_real B) A" + by (simp add: assms indicator_def) + +(* Counting number of finite maps *) +lemma card_dom_ran: + assumes "finite D" + shows "card {w. dom w = D \ ran w \ R} = card R ^ card D" + using assms +proof (induct rule: finite_induct) + case empty + have "{w::'a \ 'b option. w = Map.empty \ ran w \ R} = {Map.empty}" + by auto + then show ?case + by auto +next + case (insert a A) + have 1: "inj_on (\(w, r). w(a \ r)) + ({w. dom w = A \ ran w \ R} \ R)" + unfolding inj_on_def + by (smt (verit, del_insts) CollectD SigmaE fun_upd_None_if_notin_dom local.insert(2) map_upd_eqD1 prod.simps(2) restrict_complement_singleton_eq restrict_upd_same) + have 21: "(\(w, r). w(a \ r)) ` + ({w. dom w = A \ ran w \ R} \ R) \ + {w. dom w = insert a A \ ran w \ R}" + unfolding image_def + using CollectD local.insert(2) by force + + have "\x. dom x = insert a A \ + ran x \ R \ + \xa. dom xa = A \ + ran xa \ R \ (\y\R. x = xa(a \ y))" + by (smt (verit, del_insts) Diff_insert_absorb domD dom_fun_upd fun_upd_triv fun_upd_upd insert.hyps(2) insertCI insert_subset ran_map_upd) + then have 22: " + {w. dom w = insert a A \ ran w \ R} \ + (\(w, r). w(a \ r)) ` + ({w. dom w = A \ ran w \ R} \ R)" + by (clarsimp simp add: image_def) + + have "bij_betw (\(w,r). w(a\r)) + ({w. dom w = A \ ran w \ R} \ R) + {w. dom w = insert a A \ ran w \ R} " + unfolding bij_betw_def + using 1 21 22 by clarsimp + + then have "card {w. dom w = insert a A \ ran w \ R} = card ({w. dom w = A \ ran w \ R} \ R)" + by (auto simp add: bij_betw_same_card 1 21 22) + + moreover have "... = card R ^ card A * card R" + by(subst card_cartesian_product) (use insert.hyps(3) in auto) + + ultimately show ?case + using insert.hyps by (auto simp add: card_insert_if) +qed + +lemma finite_set_pmf_expectation_sum: + fixes f :: "'a \ 'c \ 'b::{banach, second_countable_topology}" + assumes "finite (set_pmf A)" + shows "measure_pmf.expectation A (\x. sum (f x) T) = + (\i\T. measure_pmf.expectation A (\x. f x i))" + apply (intro Bochner_Integration.integral_sum integrable_measure_pmf_finite) + using assms by auto + +lemma (in prob_space) k_universal_prob_unif: + assumes "k_universal k H D R" + assumes "w \ D" "\ \ R" + shows "prob {s \ space M. H w s = \} = 1 / card R" +proof - + have "uniform_on (H w) R" + using assms unfolding k_universal_def + by auto + + from uniform_onD[OF this] + have "prob + {\ \ space M. H w \ \ {\}} = + real (card (R \ {\})) / real (card R)" . + + thus ?thesis + using assms by auto +qed + +(* For h: D \ R, k-universal, S \ D. + E( | {w \ S. h w = \} | ) = |S| / |R| *) +lemma k_universal_expectation_eq: + assumes p: "finite (set_pmf p)" + assumes ind: "prob_space.k_universal p k H D R" + assumes S: "finite S" "S \ D" + assumes a: "\ \ R" + shows + "prob_space.expectation p + (\s. real (card (S \ {w. H w s = \}))) = + real (card S) / card R" +proof - + have 1: "prob_space (measure_pmf p)" + by (simp add: prob_space_measure_pmf) + have 2: "space (measure_pmf p) = UNIV" by auto + from prob_space.k_universal_prob_unif[OF 1 ind _ a] + have *: "\w. w \ S \ + prob_space.prob p {s. H w s = \} = 1 / real (card R)" + using S(2) by auto + + have "measure_pmf.expectation p + (\s. real (card (S \ {w. H w s = \}))) = + measure_pmf.expectation p + (\s. sum (indicat_real {w. H w s = \}) S)" + unfolding card_inter_sum_indicat_real[OF S(1)] + by presburger + + moreover have "... = + (\i\S. + measure_pmf.expectation p + (indicat_real {s. H i s = \}))" + apply (subst finite_set_pmf_expectation_sum) + using assms unfolding indicator_def by auto + + moreover have " ... = + (\i\ S. + measure_pmf.prob p {s. H i s = \})" + by auto + + moreover have "... = (\i\S. 1 / card R)" + using * by auto + + ultimately show ?thesis by auto +qed + +lemma (in prob_space) two_universal_indep_var: + assumes "k_universal 2 H D R" + assumes "w \ D" "w' \ D" "w \ w'" + shows "indep_var + borel + (\x. indicat_real {w. H w x = \} w) + borel + (\x. indicat_real {w. H w x = \} w')" +proof - + have Y: "(\z. (of_bool (z = \))::real) \ (count_space UNIV) \\<^sub>M borel" + by auto + + have "k_wise_indep_vars 2 + (\_. count_space UNIV) + H D" + using assms + unfolding k_universal_def + by auto + + then have "indep_vars (\_. count_space UNIV) H {w, w'}" + unfolding k_wise_indep_vars_def + by (metis UNIV_bool assms(2) assms(3) card.empty card.insert card_UNIV_bool card_insert_le empty_iff empty_subsetI finite.emptyI finite.insertI insert_subset order.refl singletonD singleton_insert_inj_eq') + + from indep_var_from_indep_vars[OF assms(4) this] + have "indep_var + (count_space UNIV) (H w) + (count_space UNIV) (H w')" . + + from indep_var_compose[OF this Y Y] + show ?thesis + unfolding indicator_def + by (auto simp add: o_def) +qed + +(* For h: D \ R, 2-universal, S \ D. + V( | {w \ S. h w = \} | ) \ E( | {w \ S. h w = \} | ) *) +lemma two_universal_variance_bound: + assumes p: "finite (set_pmf p)" + assumes ind: "prob_space.k_universal (measure_pmf p) 2 H D R" + assumes S: "finite S" "S \ D" + assumes a: "\ \ R" + shows + "measure_pmf.variance p + (\s. real (card (S \ {w. H w s = \}))) \ + measure_pmf.expectation p + (\s. real (card (S \ {w. H w s = \})))" +proof - + have vb: "measure_pmf.variance p + (\x. (indicat_real {w. H w x = \} i)) \ + measure_pmf.expectation p + (\x. (indicat_real {w. H w x = \} i))" for i + proof - + have "measure_pmf.variance p + (\x. (indicat_real {w. H w x = \} i)) = + measure_pmf.expectation p + (\x. (indicat_real {w. H w x = \} i)\<^sup>2) - + (measure_pmf.expectation p + (\x. indicat_real {w. H w x = \} i))\<^sup>2" + apply (subst measure_pmf.variance_eq) + by (auto simp add: p integrable_measure_pmf_finite) + moreover have "... \ measure_pmf.expectation p + (\x. (indicat_real {w. H w x = \} i)\<^sup>2)" + by simp + moreover have "... = measure_pmf.expectation p + (\x. (indicat_real {w. H w x = \} i))" + by (metis (mono_tags, lifting) indicator_simps(1) indicator_simps(2) power2_eq_1_iff zero_eq_power2) + ultimately show ?thesis by linarith + qed + + have "measure_pmf.variance p + (\s. real (card (S \ {w. H w s = \}))) = + measure_pmf.variance p + (\s. sum (indicat_real {w. H w s = \}) S)" + unfolding card_inter_sum_indicat_real[OF S(1)] + by presburger + + then have "... = (\i\S. + measure_pmf.variance p + (\x. (indicat_real {w. H w x = \} i)))" + apply (subst measure_pmf.var_sum_pairwise_indep) + using S prob_space_measure_pmf + by (auto intro!: prob_space.two_universal_indep_var[OF _ ind] simp add: p integrable_measure_pmf_finite) + + moreover have "... \ (\i\S. + measure_pmf.expectation p + (\x. (indicat_real {w. H w x = \} i)))" + by (simp add: sum_mono vb) + moreover have "... = measure_pmf.expectation p + (\s. sum (indicat_real {w. H w s = \}) S)" + apply (subst finite_set_pmf_expectation_sum) + using assms by auto + ultimately show ?thesis + by (simp add: assms(3) card_inter_sum_indicat_real) +qed + +lemma (in prob_space) k_universal_mono: + assumes "k' \ k" + assumes"k_universal k H D R" + shows"k_universal k' H D R" + using assms + unfolding k_universal_def k_wise_indep_vars_def + by auto + +lemma finite_set_pmf_expectation_add: + assumes "finite (set_pmf S)" + shows "measure_pmf.expectation S (\x. ((f x)::real) + g x) = + measure_pmf.expectation S f + measure_pmf.expectation S g" + by (auto intro: Bochner_Integration.integral_add simp add: assms integrable_measure_pmf_finite) + +lemma finite_set_pmf_expectation_add_const: + assumes "finite (set_pmf S)" + shows "measure_pmf.expectation S (\x. ((f x)::real) + g) = + measure_pmf.expectation S f + g" +proof - + have "g = measure_pmf.expectation S (\x. g)" + by simp + thus ?thesis + by (simp add: assms finite_set_pmf_expectation_add) +qed + +lemma finite_set_pmf_expectation_diff: + assumes "finite (set_pmf S)" + shows "measure_pmf.expectation S (\x. ((f x)::real) - g x) = + measure_pmf.expectation S f - measure_pmf.expectation S g" + by (auto intro: Bochner_Integration.integral_diff simp add: assms integrable_measure_pmf_finite) + +(* convenient forms of library inequalities *) +lemma spec_paley_zygmund_inequality: + assumes fin: "finite (set_pmf p)" + assumes Zpos: "\z. Z z \ 0" + assumes t: "\ \ 1" + shows " + (measure_pmf.variance p Z + (1-\)^2 * (measure_pmf.expectation p Z)^2) * + measure_pmf.prob p {z. Z z > \ * measure_pmf.expectation p Z} \ + (1-\)^2 * (measure_pmf.expectation p Z)^2" +proof - + have "prob_space (measure_pmf p)" by (auto simp add: prob_space_measure_pmf) + + from prob_space.paley_zygmund_inequality[OF this _ integrable_measure_pmf_finite[OF fin] t] + show ?thesis + using Zpos by auto +qed + +lemma spec_chebyshev_inequality: + assumes fin: "finite (set_pmf p)" + assumes pvar: "measure_pmf.variance p Y > 0" + assumes k: "k > 0" + shows " + measure_pmf.prob p + {y. (Y y - measure_pmf.expectation p Y)^2 \ + k^2 * measure_pmf.variance p Y} \ 1 / k^2" +proof - + define f where + "f x = Y x / sqrt(measure_pmf.variance p Y)" for x + have 1: + "measure_pmf.random_variable p borel f" + by auto + have *: "(\x. (f x)\<^sup>2) = (\x. (Y x)\<^sup>2/ measure_pmf.variance p Y)" + unfolding f_def + by (simp add: power_divide) + have 2: + "integrable p (\x. (f x)\<^sup>2)" + unfolding * + by (intro integrable_measure_pmf_finite[OF fin]) + from + measure_pmf.Chebyshev_inequality[OF 1 2 k] + have ineq1:"measure_pmf.prob p + {x . k \ \f x - measure_pmf.expectation p f\} + \ measure_pmf.expectation p + (\x. (f x - measure_pmf.expectation p f)\<^sup>2) / k\<^sup>2" by auto + + have "(\x. (f x - measure_pmf.expectation p f)\<^sup>2) = + (\x. ((Y x - measure_pmf.expectation p Y) / sqrt(measure_pmf.variance p Y))\<^sup>2)" + unfolding f_def + by (simp add: diff_divide_distrib) + + moreover have "... = (\x. (Y x - measure_pmf.expectation p Y)^2 / (sqrt(measure_pmf.variance p Y))^2)" + by (simp add: power_divide) + moreover have "... = (\x. (Y x - measure_pmf.expectation p Y)^2 / measure_pmf.variance p Y)" + by simp + ultimately have unfold:"(\x. (f x - measure_pmf.expectation p f)\<^sup>2) + = (\x. (Y x - measure_pmf.expectation p Y)^2 / measure_pmf.variance p Y)" + by auto + then have "measure_pmf.expectation p (\x. (f x - measure_pmf.expectation p f)\<^sup>2) / k\<^sup>2 + = measure_pmf.expectation p (\x. (Y x - measure_pmf.expectation p Y)^2 / measure_pmf.variance p Y) / k\<^sup>2" + by auto + moreover have "... = measure_pmf.variance p Y / measure_pmf.variance p Y / k\<^sup>2" + by simp + moreover have "... = 1 / k\<^sup>2" + using pvar by force + ultimately have eq1:"measure_pmf.expectation p (\x. (f x - measure_pmf.expectation p f)\<^sup>2) / k\<^sup>2 = 1 / k\<^sup>2" + by auto + have "(\x. k \ \f x - measure_pmf.expectation p f\) = (\x. k\<^sup>2 \ (f x - measure_pmf.expectation p f)\<^sup>2)" + by (metis (no_types, opaque_lifting) abs_of_nonneg k less_le real_le_rsqrt real_sqrt_abs sqrt_ge_absD) + moreover have "... = (\x. k\<^sup>2 \ ((Y x - measure_pmf.expectation p Y)^2 / measure_pmf.variance p Y))" + by (metis unfold) + moreover have "... = (\x. (Y x - measure_pmf.expectation p Y)^2 \ k\<^sup>2 * measure_pmf.variance p Y)" + by (simp add: pos_le_divide_eq pvar) + ultimately have cond:"(\x. k \ \f x - measure_pmf.expectation p f\) + = (\x. (Y x - measure_pmf.expectation p Y)^2 \ k\<^sup>2 * measure_pmf.variance p Y)" + by auto + show "?thesis" using ineq1 cond eq1 + by auto +qed + +end diff --git a/thys/Approximate_Model_Counting/CertCheck.thy b/thys/Approximate_Model_Counting/CertCheck.thy new file mode 100644 --- /dev/null +++ b/thys/Approximate_Model_Counting/CertCheck.thy @@ -0,0 +1,1159 @@ +section \ Certificate-based ApproxMC \ + +text \ This turns the randomized algorithm into an + executable certificate checker \ + +theory CertCheck +imports ApproxMCAnalysis + +begin + +subsection \ ApproxMC with lists instead of sets \ + +type_synonym 'a xor = "'a list \ bool" + +definition satisfies_xorL :: "'a xor \ ('a \ bool) \ bool" + where "satisfies_xorL xb \ = + even (sum_list (map (of_bool \ \) (fst xb)) + + of_bool (snd xb)::nat)" + +(* Extract a sublist based on bits *) +definition sublist_bits::"'a list \ bool list \ 'a list" + where "sublist_bits ls bs = + map fst (filter snd (zip ls bs))" + +definition xor_from_bits:: + "'a list \ bool list \ bool \ 'a xor" + where "xor_from_bits V xsb = + (sublist_bits V (fst xsb), snd xsb)" + +locale ApproxMCL = + fixes sols :: "'fml \ ('a \ bool) set" + fixes enc_xor :: "'a xor \ 'fml \ 'fml" + assumes sols_enc_xor: + "\F xor. + sols (enc_xor xor F) = + sols F \ {\. satisfies_xorL xor \}" +begin + +definition list_of_set ::"'a set \ 'a list" +where "list_of_set x = (@ls. set ls = x \ distinct ls)" + +definition xor_conc :: "'a set \ bool \ 'a xor" + where "xor_conc xsb = (list_of_set (fst xsb), snd xsb)" + +definition enc_xor_conc :: "'a set \ bool \ 'fml \ 'fml" + where "enc_xor_conc = enc_xor \ xor_conc" + +lemma distinct_count_list: + assumes "distinct ls" + shows "count_list ls x = of_bool (x \ 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 \ 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)) \ \ satisfies_xor (x,b) {x. \ 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 \ 'a list \ + (nat \ bool list \ bool) \ + nat \ nat" + where "size_xorL F S xorsl i = ( + let xors = map (xor_from_bits S \ xorsl) [0.. 'a list \ + nat \ + (nat \ bool list \ bool) \ + nat \ bool" + where "check_xorL F S thresh xorsl i = + (size_xorL F S xorsl i < thresh)" + +definition approxcore_xorsL :: " + 'fml \ 'a list \ + nat \ + (nat \ (bool list \ bool)) \ + nat" + where " + approxcore_xorsL F S thresh xorsl = + (case List.find + (check_xorL F S thresh xorsl) [1.. 2 ^ length S + | Some m \ + (2 ^ m * size_xorL F S xorsl m))" + +definition xor_abs :: "'a xor \ 'a set \ bool" + where "xor_abs xsb = (set (fst xsb), snd xsb)" + +lemma sols_fold_enc_xor: + assumes "list_all2 (\x y. + \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: "\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. \ x} \ satisfies_xorL (x,b) \" + 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 \ + 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 "\j. j < i \ + 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 = "(\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 \ sols (fold enc_xor (xs @ rev ys) F)" + shows "x \ 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 \ y" "distinct S" + shows "size_xorL F S xorsl x \ size_xorL F S xorsl y" +proof - + obtain ys where ys: "[0.. xorsl) ys))" + have *: "\y. y \ set rys \ 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 "\i. a \ i \ i < x \ \P i" + assumes "P x" "a \ x" "x < b" + shows "find P [a..j. j \ P ([a..j. j < i \ + 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 "\j. j < length S - 1 \ + 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.. + j < a \ + 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.. 'a list \ + real \ real \ nat \ + (nat \ nat \ (bool list \ bool)) \ + nat" + where "approxmc_mapL F S \ \ n xorsLs = ( + let \ = appmc.mk_eps \ in + let thresh = appmc.compute_thresh \ in + if card (proj (set S) (sols F)) < thresh then + card (proj (set S) (sols F)) + else + let t = appmc.compute_t \ n in + median t (approxcore_xorsL F S thresh \ xorsLs))" + +definition random_xorB :: "nat \ (bool list \ 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 "\i j. j < length S - 1 \ + xorsFs i j = + Some (xor_abs (xor_from_bits S (xorsLs i j)))" + assumes S: "distinct S" + shows " + approxmc_mapL F S \ \ n xorsLs = + appmc.approxmc_map F (set S) \ \ 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 \ \ n xorsLs = + appmc.approxmc_map F (set S) \ \ n + (\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 + (\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 \ sublist_bits S) (a,b)" for a b + using xor_abs_def by (auto simp add: xor_from_bits_def) + + then have *: "(\x. xor_abs (xor_from_bits S x)) = apfst (set \ sublist_bits S)" + by auto + + have "\x. x \ set S \ + z x \ + \b. (\n. S ! n = x \ + map z S ! n = b \ + n < length S) \ b" for z + by (metis assms distinct_Ex1 nth_map) + + then have " set (map fst + (filter snd + (zip S (map z S)))) = + {x \ 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 \ sublist_bits S) + (replicate_pmf (length S) (bernoulli_pmf (1 / 2))) = + map_pmf (\b. {x \ set S. b x = Some True}) + (Pi_pmf (set S) (Some undefined) + (\_. 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 (\_. map_pmf Some p) = + map_pmf (\f v. if v \ S then Some (f v) else None) + (Pi_pmf S def (\_. p))" +proof - + have *: "Pi_pmf S None (\_. map_pmf Some p) = + map_pmf (\f x. if x \ S then f x else None) + (Pi_pmf S (Some def) (\_. 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 + (\f j. + if j < n + then Some (xor_abs (xor_from_bits S (f j))) + else None) + (Pi_pmf {..<(n::nat)} def (\_. 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 "(\j. if j < n + then Some (xor_abs (xor_from_bits S (def1 j))) + else None) = def" + shows " + map_pmf + ((\) (\f j. if j < n + then Some (xor_abs (xor_from_bits S (f j))) + else None)) + (Pi_pmf {0..<(m::nat)} def1 + (\_. + Pi_pmf {..<(n::nat)} def2 (\_. random_xorB (length S)))) = + Pi_pmf {0..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 \ nat \ (nat \ nat \ bool list \ bool) pmf" + where "random_seed_xors t l = + (prod_pmf {0.._. prod_pmf {.._. random_xorB l)))" + +lemma approxmcL_sound: + assumes \: "\ > 0" "\ < 1" + assumes \: "\ > 0" + assumes S: "distinct S" + shows " + prob_space.prob + (map_pmf (approxmc_mapL F S \ \ n) + (random_seed_xors (appmc.compute_t \ n) (length S))) + {c. real c \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} + \ 1 - \" +proof - + define def where "def = + (\j. if j < degree S + then Some (xor_abs (xor_from_bits S (undefined j))) + else None)" + have *: "(map_pmf (approxmc_mapL F S \ \ n) + (Pi_pmf {0.. n} undefined + (\_. Pi_pmf {.._. random_xorB (length S))))) = + (map_pmf (appmc.approxmc_map F (set S) \ \ n) + (map_pmf ((\) (\f. + (\j. if j < length S - 1 + then Some (xor_abs (xor_from_bits S (f j))) + else None))) + (Pi_pmf {0.. n} undefined + (\_. Pi_pmf {.._. random_xorB (length S))))))" + unfolding approxmc_mapL'[OF S] + by (simp add: map_pmf_comp o_def) + have **: " + (map_pmf (approxmc_mapL F S \ \ n) + (Pi_pmf {0.. n} undefined + (\_. Pi_pmf {.._. random_xorB (length S))))) = + map_pmf (appmc.approxmc_map F (set S) \ \ n) + (Pi_pmf {0.. n} def + (\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 \(2) \ 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 \: "\ > 0" "\ < 1" + assumes \: "\ > 0" + assumes S: "distinct S" + shows " + prob_space.prob + (map_pmf (approxmc_mapL F S \ \ n) + (random_seed_xors (appmc.compute_t \ n) (length S))) + {c. real c \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} \ \" +proof - + have "prob_space.prob + (map_pmf (approxmc_mapL F S \ \ n) + (Pi_pmf {0.. n} undefined + (\_. Pi_pmf {.._. random_xorB (length S))))) + {c. real c \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} = + 1 - prob_space.prob + (map_pmf (approxmc_mapL F S \ \ n) + (Pi_pmf {0.. n} undefined + (\_. Pi_pmf {.._. random_xorB (length S))))) + {c. real c \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * 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"] \ + unfolding random_seed_xors_def + by linarith +qed + +end + +subsection \ ApproxMC certificate checker \ + +(* Helper functions *) +definition str_of_bool :: "bool \ String.literal" + where "str_of_bool b = ( + if b then STR ''true'' else STR ''false'')" + +fun str_of_nat_aux :: "nat \ char list \ 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 \ String.literal" + where "str_of_nat n = String.implode (str_of_nat_aux n [])" + +type_synonym 'a sol = "('a \ bool) list" + +(* The canonical assignment specified by a list *) +definition canon_map_of :: "('a \ bool) list \ ('a \ bool)" + where "canon_map_of ls = + (let m = map_of ls in + (\x. case m x of None \ False | Some b \ 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 \ ('a \ bool) \ bool list" + where "proj_sol S w = map w S" + +text \ The following extended locale assumes + additional support for syntactically working with solutions \ +locale CertCheck = ApproxMCL sols enc_xor + for sols :: "'fml \ ('a \ bool) set" + and enc_xor :: "'a list \ bool \ 'fml \ 'fml" + + fixes check_sol :: "'fml \ ('a \ bool) \ bool" + fixes ban_sol :: "'a sol \ 'fml \ 'fml" + assumes sols_ban_sol: + "\F vs. + sols (ban_sol vs F) = + sols F \ {\. map \ (map fst vs) \ map snd vs}" + assumes check_sol: + "\F w. check_sol F w \ w \ sols F" +begin + +text \ Assuming parameter access to an UNSAT checking oracle \ +context + fixes check_unsat :: "'fml \ bool" +begin + +text \ Throughout this checker, INL indicates error, INR indicates success \ + +definition check_BSAT_sols::" + 'fml \ 'a list \ nat \ ('a \ bool) list \ 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 \ + check_unsat (fold ban_sol (map (zip S) ps) F)) in + if b1 \ b2 \ 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 \ 'a list \ nat \ ('a \ bool) list \ String.literal + nat" +where "BSAT F S thresh xs = ( + case check_BSAT_sols F S thresh xs of + Inl err \ Inl err + | Inr _ \ Inr (length xs) +)" + +(* A size certificate is simply a list of solutions*) +definition size_xorL_cert :: " + 'fml \ 'a list \ nat \ + (nat \ (bool list \ bool)) \ nat \ + (('a \ bool) list) \ String.literal + nat" + where "size_xorL_cert F S thresh xorsl i xs = ( + let xors = map (xor_from_bits S \ xorsl) [0.. m \ |S|-1 *) +fun approxcore_xorsL_cert :: " + 'fml \ 'a list \ nat \ + nat \ ('a \ bool) list \ ('a \ bool) list \ + (nat \ (bool list \ bool)) + \ String.literal + nat" +where "approxcore_xorsL_cert F S thresh (m,cert1,cert2) xorsl = ( + if 1 \ m \ m \ length S + then + case size_xorL_cert F S thresh xorsl (m-1) cert1 of + Inl err \ Inl (STR ''cert1 '' + err) + | Inr n \ + if n \ 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 \ Inl (STR ''cert2 '' + err) + | Inr c \ + 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 \ nat" +where "find_t \ = ( + case find (\i. appmc.raw_median_bound 0.14 i < \) [0..<256] of + Some m \ m + | None \ appmc.fix_t \ + )" + +fun fold_approxcore_xorsL_cert:: " + 'fml \ 'a list \ nat \ + nat \ nat \ + (nat \ (nat \ ('a \ bool) list \ ('a \ bool) list)) \ + (nat \ nat \ (bool list \ bool)) + \ 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 \ Inl (STR ''round '' + str_of_nat it + STR '' '' + err) + | Inr n \ + (case fold_approxcore_xorsL_cert F S thresh t i cs xorsLs of + Inl err \ Inl err + | Inr ns \ Inr (n # ns)))" + +definition calc_median::" + 'fml \ 'a list \ nat \ nat \ + (nat \ (nat \ ('a \ bool) list \ ('a \ bool) list)) \ + (nat \ nat \ (bool list \ bool)) \ + 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 \ Inl err + | Inr ls \ Inr (sort ls ! (t div 2)) + )" + +fun certcheck::" + 'fml \ 'a list \ + real \ real \ + (('a \ bool) list \ + (nat \ (nat \ ('a \ bool) list \ ('a \ bool) list))) \ + (nat \ nat \ (bool list \ bool)) \ + String.literal + nat" + where "certcheck F S \ \ (m0,ms) xorsLs = ( + let \ = appmc.mk_eps \ in + let thresh = appmc.compute_thresh \ in + case BSAT F S thresh m0 of Inl err \ Inl err + | Inr Y \ + if Y < thresh then Inr Y + else + let t = find_t \ 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: "\F. check_unsat F \ sols F = {}" +begin + +lemma sols_fold_ban_sol: + shows"sols (fold ban_sol ls F) = + sols F \ {\. (\vs \ set ls. map \ (map fst vs) \ 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 "\x. x \ A \ x \ B \ x \ C" + shows "A \ B = A \ 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) \ A" + shows "map_of (zip S x) \ proj (set S) A" +proof - + define f where "f = (\xa. case map_of (zip S x) xa of + None \ False | Some b \ b)" + have "map_of (zip S x) = + (\y. if y \ 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 \ rdb" + shows " + map_of (zip S w) \ + proj (set S) {\. proj_sol S \ \ 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 "\bs. bs \ rdb \ length bs = length S" + assumes w: "w \ proj (set S) {\. proj_sol S \ \ rdb}" + shows " + w \ (map_of \ zip S) ` rdb" +proof - + obtain ww where ww: "proj_sol S ww \ 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 "\bs. bs \ rdb \ length bs = length S" + shows " + proj (set S) {\. proj_sol S \ \ rdb} = + (map_of \ 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 \ ('a \ bool) list \ 'fml \ 'fml" +where "ban_proj_sol S xs F = + fold ban_sol (map (zip S \ proj_sol S) xs) F" + +lemma check_sol_imp_proj: + assumes "w \ sols F" + shows "map_of (zip S (proj_sol S w)) \ 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 \ card (proj (set S) (sols F))" + "length xs < thresh \ + 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: "\x. x \ set Sxs \ 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) \ 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 \ card (proj (set S) (sols F))" + by (metis * List.finite_set card_mono card_proj(1)) + + have frr1: "(\vs \ set SSxs. map \ (map fst vs) \ map snd vs) \ + (\vs \ set Sxs. proj_sol S \ \ vs)" for \ + apply (clarsimp simp add: proj_sol_def SSxs_def) + by (metis (mono_tags, lifting) in_set_zip nth_map) + have frr2: "(\vs \ set Sxs. proj_sol S \ \ vs) \ + (vs \ set SSxs \ map \ (map fst vs) \ map snd vs)" for vs \ + 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: "{\. (\vs \ set SSxs. map \ (map fst vs) \ map snd vs)} = + {\. (\vs \ set Sxs. proj_sol S \ \ 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 \ {\. (\vs \ set Sxs. proj_sol S \ \ 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) \ + proj (set S) + {\. \vs\set Sxs. proj_sol S \ \ 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) \ -proj (set S) {\. (\vs \ set Sxs. proj_sol S \ \ vs)} = + proj (set S) (sols F) \ proj (set S) {\. proj_sol S \ \ set Sxs}" + apply (intro inter_cong_right) + by (auto intro!: proj_sol_cong simp add: ApproxMCCore.proj_def ) + + have 3: "proj (set S) {\. proj_sol S \ \ set Sxs} = (map_of \ 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) \ (map_of \ zip S) ` (set Sxs) = + (map_of \ zip S) ` (set Sxs)" + using "*" SSxs_def by auto + + have **:"proj (set S) (sols F) = + proj (set S) (sols F) \ proj (set S) {\. (\vs \ set Sxs. proj_sol S \ \ vs)} \ + proj (set S) (sols F) \ -proj (set S) {\. (\vs \ set Sxs. proj_sol S \ \ vs)}" + by auto + + have "card (proj (set S) (sols F)) = + card ((map_of \ 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 \length xs = card (set (map map_of SSxs))\) + } + thus "length xs < thresh \ 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 \ card (proj (set S) (sols F))" + "n < thresh \ + 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 \ n" + "n < thresh \ 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 \ size_xorL F S xorsl (m - 1)" + "nn1 < thresh \ size_xorL F S xorsl (m - 1) = nn1" by auto + + have m: "1 \ m" "m \ length S" + "nn1 \ thresh" and + ms: "m = length S \ n = 2 ^ length S \ + m < length S" + using nn1 assms unfolding mc + by (auto split: if_splits simp add: Let_def) + + have bnd: "\i. 1 \ i \ i \ m -1 \ + size_xorL F S xorsl i \ 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.. t" + assumes "fold_approxcore_xorsL_cert F S thresh t i cs xorsLs = Inr ns" + shows "map (approxcore_xorsL F S thresh \ xorsLs) [t-i.. t" using c by auto + from c(1)[OF this *(2)] + have 2: "nss = + map (approxcore_xorsL F S thresh \ xorsLs) [t - i.. 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 \ (find_t \) = find_t \" + 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 \ \ (m0,ms) xorsLs = Inr n" + shows "approxmc_mapL F S \ \ (find_t \) 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 "\isl (certcheck F S \ \ m xorsLs)" + shows "projr (certcheck F S \ \ m xorsLs) = + approxmc_mapL F S \ \ (find_t \) 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 (\isl) + With output c not in the interval is at most \ *) +lemma certcheck_sound: + assumes \: "\ > 0" "\ < 1" + assumes \: "\ > 0" + assumes S: "distinct S" + shows " + measure_pmf.prob + (map_pmf (\r. certcheck F S \ \ (f r) r) + (random_seed_xors (find_t \) (length S))) + {c. \isl c \ + real (projr c) \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} \ \" +proof - + have "measure_pmf.prob + (map_pmf (\r. certcheck F S \ \ (f r) r) + (random_seed_xors (find_t \) (length S))) + {c. \isl c \ + real (projr c) \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} \ + prob_space.prob + (map_pmf (approxmc_mapL F S \ \ (find_t \)) + (random_seed_xors (appmc.compute_t \ (find_t \)) (length S))) + {c. real c \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * 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 "... \ \" + 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 (\isl) the output of f on any randomness + Then the output c is in the interval with high probability (1 - \) *) +lemma certcheck_promise_complete: + assumes \: "\ > 0" "\ < 1" + assumes \: "\ > 0" + assumes S: "distinct S" + assumes r: "\r. + r \ set_pmf (random_seed_xors (find_t \) (length S)) \ + \isl (certcheck F S \ \ (f r) r)" + shows " + measure_pmf.prob + (map_pmf (\r. certcheck F S \ \ (f r) r) + (random_seed_xors (find_t \) (length S))) + {c. real (projr c) \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} \ 1 - \" +proof - + have " + measure_pmf.prob + (map_pmf (\r. certcheck F S \ \ (f r) r) + (random_seed_xors (find_t \) (length S))) + {c. real (projr c) \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} = + measure_pmf.prob + (map_pmf (approxmc_mapL F S \ \ (find_t \)) + (random_seed_xors (appmc.compute_t \ (find_t \)) (length S))) + {c. real c \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * 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 "... \ 1 - \" + by (intro approxmcL_sound[OF assms(1-4)]) + finally show ?thesis by auto +qed + +lemma certcheck_code[code]: + "certcheck F S \ \ (m0,ms) xorsLs = ( + if \ > 0 \ \ < 1 \ \ > 0 \ distinct S then + (let \ = appmc.mk_eps \ in + let thresh = appmc.compute_thresh \ in + case BSAT F S thresh m0 of Inl err \ Inl err + | Inr Y \ + if Y < thresh then Inr Y + else + let t = find_t \ in + calc_median F S thresh t ms xorsLs) + else Code.abort (STR ''invalid inputs'') + (\_. certcheck F S \ \ (m0,ms) xorsLs))" + by auto + +end + +end + +end + +end diff --git a/thys/Approximate_Model_Counting/CertCheck_CNF_XOR.thy b/thys/Approximate_Model_Counting/CertCheck_CNF_XOR.thy new file mode 100644 --- /dev/null +++ b/thys/Approximate_Model_Counting/CertCheck_CNF_XOR.thy @@ -0,0 +1,670 @@ +section \ ApproxMC certification for CNF-XOR \ + +text \ + This concretely instantiates the locales with a syntax and + semantics for CNF-XOR, giving us a certificate checker for + approximate counting in this theory. +\ + +theory CertCheck_CNF_XOR imports + ApproxMCAnalysis + CertCheck + HOL.String "HOL-Library.Code_Target_Numeral" + Show.Show_Real +begin + +text \ + This follows CryptoMiniSAT's CNF-XOR formula syntax. + A clause is a list of literals (one of which must be satisfied). + An XOR constraint has the form $l_1 + l_2 + \dots + l_n = 1$ where addition is taken over $F_2$. + Syntactically, they are specified by the list of LHS literals. + Variables are natural numbers (in practice, variable 0 is never used) +\ + +datatype lit = Pos nat | Neg nat +type_synonym clause = "lit list" +type_synonym cmsxor = "lit list" +type_synonym fml = "clause list \ cmsxor list" + +type_synonym assignment = "nat \ bool" + +definition sat_lit :: "assignment \ lit \ bool" where + "sat_lit w l = (case l of Pos x \ w x | Neg x \ \w x)" + +definition sat_clause :: "assignment \ clause \ bool" where + "sat_clause w C = (\l \ set C. sat_lit w l)" + +definition sat_cmsxor :: "assignment \ cmsxor \ bool" where + "sat_cmsxor w C = odd ((sum_list (map (of_bool \ (sat_lit w)) C))::nat)" + +definition sat_fml :: "assignment \ fml \ bool" + where + "sat_fml w f = ( + (\C \ set (fst f). sat_clause w C) \ + (\C \ set (snd f). sat_cmsxor w C))" + +(* The solution set *) +definition sols :: "fml \ assignment set" + where "sols f = {w. sat_fml w f}" + +lemma sat_fml_cons[simp]: + shows + "sat_fml w (FC, x # FX) \ + sat_fml w (FC,FX) \ sat_cmsxor w x" + "sat_fml w (c # FC, FX) \ + sat_fml w (FC,FX) \ sat_clause w c" + unfolding sat_fml_def by auto + +(* Construct clauses for a given XOR *) +fun enc_xor :: "nat xor \ fml \ fml" + where + "enc_xor (x,b) (FC,FX) = ( + if b then (FC, map Pos x # FX) + else + case x of + [] \ (FC,FX) + | (v#vs) \ (FC, (Neg v # map Pos vs) # FX))" + +lemma sols_enc_xor: + shows "sols (enc_xor (x,b) (FC,FX)) = + sols (FC,FX) \ {\. satisfies_xorL (x,b) \}" + unfolding sols_def + by (cases x; auto simp add: satisfies_xorL_def sat_cmsxor_def o_def sat_lit_def list.case_eq_if) + +(* Solution checking *) +definition check_sol :: "fml \ (nat \ bool) \ bool" + where "check_sol fml w = ( + list_all (list_ex (sat_lit w)) (fst fml) \ + list_all (sat_cmsxor w) (snd fml))" + +definition ban_sol :: "(nat \ bool) list \ fml \ fml" + where "ban_sol vs fml = + ((map (\(v,b). if b then Neg v else Pos v) vs)#fst fml, snd fml)" + +lemma check_sol_sol: + shows "w \ sols F \ + check_sol F w" + unfolding check_sol_def sols_def sat_fml_def + apply clarsimp + by (metis Ball_set_list_all Bex_set_list_ex sat_clause_def) + +lemma ban_sat_clause: + shows "sat_clause w (map (\(v, b). if b then Neg v else Pos v) vs) \ + map w (map fst vs) \ map snd vs" + unfolding sat_clause_def + by (force simp add: sat_lit_def split: if_splits) + +lemma sols_ban_sol: + shows"sols (ban_sol vs F) = + sols F \ + {\. map \ (map fst vs) \ map snd vs}" + unfolding ban_sol_def sols_def + by (auto simp add: ban_sat_clause) + +(* Globally interpret the ApproxMC locale to make + ApproxMC certification available for CNF-XOR *) +global_interpretation CertCheck_CNF_XOR : + CertCheck "sols" "enc_xor" "check_sol" "ban_sol" + defines + random_seed_xors = CertCheck_CNF_XOR.random_seed_xors and + fix_t = CertCheck_CNF_XOR.appmc.fix_t and + find_t = CertCheck_CNF_XOR.find_t and + BSAT = CertCheck_CNF_XOR.BSAT and + check_BSAT_sols = CertCheck_CNF_XOR.check_BSAT_sols and + size_xorL_cert = CertCheck_CNF_XOR.size_xorL_cert and + approxcore_xorsL = CertCheck_CNF_XOR.approxcore_xorsL and + fold_approxcore_xorsL_cert = CertCheck_CNF_XOR.fold_approxcore_xorsL_cert and + approxcore_xorsL_cert = CertCheck_CNF_XOR.approxcore_xorsL_cert and + calc_median = CertCheck_CNF_XOR.calc_median and + certcheck = CertCheck_CNF_XOR.certcheck + apply unfold_locales + subgoal by (metis sols_enc_xor surj_pair) + subgoal by (metis sols_ban_sol) + by (metis check_sol_sol) + +(* Note that we automatically get the associated theorems +thm CertCheck_CNF_XOR.certcheck_sound + +thm CertCheck_CNF_XOR.certcheck_promise_complete +*) + +subsection \ Blasting XOR constraints to CNF \ + +text \ + This formalizes the usual linear conversion from CNF-XOR into CNF. + It is not necessary to use this conversion for solvers that support + CNF-XOR formulas natively. +\ + +definition negate_lit :: "lit \ lit" + where "negate_lit l = (case l of Pos x \ Neg x | Neg x \ Pos x)" + +(* Naive direct encoding XOR *) +fun xor_clauses :: "cmsxor \ bool \ clause list" + where + "xor_clauses [] b = (if b then [[]] else [])" + | "xor_clauses (x#xs) b = + (let p_x = xor_clauses xs b in + let n_x = xor_clauses xs (\b) in + map (\c. x # c) p_x @ map (\c. negate_lit x # c) n_x)" + +lemma sat_cmsxor_nil[simp]: + shows"\ (sat_cmsxor w [])" + unfolding sat_cmsxor_def + by auto + +lemma sat_cmsxor_cons: + shows "sat_cmsxor w (x # xs) = + (if sat_lit w x then \ (sat_cmsxor w xs) else sat_cmsxor w xs)" + unfolding sat_cmsxor_def + by auto + +lemma sat_cmsxor_append: + shows "sat_cmsxor w (xs @ ys) = + (if sat_cmsxor w xs then \ (sat_cmsxor w ys) else sat_cmsxor w ys)" +proof (induction xs) + case Nil + then show ?case + by (auto simp add: sat_cmsxor_def) +next + case (Cons x xs) + then show ?case + by (auto simp add: sat_cmsxor_cons) +qed + +definition sat_clauses:: "assignment \ clause list \ bool" + where "sat_clauses w cs = (\c \ set cs. sat_clause w c)" + +lemma sat_clauses_append: + shows "sat_clauses w (xs @ ys) = + (sat_clauses w xs \ sat_clauses w ys)" + unfolding sat_clauses_def by auto + +lemma sat_clauses_map: + shows "sat_clauses w (map ((#) x) cs) = + (sat_lit w x \ sat_clauses w cs)" + unfolding sat_clauses_def sat_clause_def by auto + +lemma sat_lit_negate_lit[simp]: + "sat_lit w (negate_lit l) = (\sat_lit w l)" + apply (cases l) + by (auto simp add: negate_lit_def sat_lit_def) + +lemma sols_xor_clauses: + shows " + sat_clauses w (xor_clauses xs b) \ + (sat_cmsxor w xs = b)" +proof (induction xs arbitrary: b) + case Nil + then show ?case + by (auto simp add: sat_cmsxor_def sat_clauses_def sat_clause_def) +next + case (Cons x xs b) + have *: "(sat_cmsxor w (x # xs) = b) = + (if sat_lit w x + then (sat_cmsxor w xs = (\b)) + else (sat_cmsxor w xs = b))" unfolding sat_cmsxor_cons + by auto + + have "sat_clauses w (xor_clauses (x # xs) b) \ + ((sat_lit w x \ sat_clauses w (xor_clauses xs b)) \ + (\(sat_lit w x) \ sat_clauses w (xor_clauses xs (\ b))))" + unfolding xor_clauses.simps Let_def sat_clauses_append sat_clauses_map + by auto + moreover have "... = ( + (sat_lit w x \ (sat_cmsxor w xs = b)) \ + (\(sat_lit w x) \ (sat_cmsxor w xs = (\ b))))" + using Cons.IH by auto + moreover have "... = (sat_cmsxor w (x # xs) = b)" + unfolding * by auto + ultimately show ?case + by auto +qed + +(* This can be done more generally with freshness *) +definition var_lit :: "lit \ nat" + where "var_lit l = (case l of Pos x \ x | Neg x \ x)" + +definition var_lits :: "lit list \ nat" + where "var_lits ls = fold max (map var_lit ls) 0" + +lemma sat_lit_same: + assumes "\x. x \ var_lit l \ w x = w' x" + shows "sat_lit w l = sat_lit w' l" + using assms + apply (cases l) + by (auto simp add: sat_lit_def var_lit_def) + +lemma var_lits_eq: + "var_lits ls = Max (set (0 # map var_lit ls))" + unfolding var_lits_def Max.set_eq_fold + by auto + +lemma sat_lits_same: + assumes "\x. x \ var_lits c \ w x = w' x" + shows "sat_clause w c = sat_clause w' c" + using assms + unfolding sat_clause_def var_lits_eq sat_lit_same + by (smt (verit) List.finite_set Max_ge dual_order.trans image_subset_iff list.set_map sat_lit_same set_subset_Cons) + +lemma le_var_lits_in: + assumes "y \ set ys" "v \ var_lit y" + shows "v \ var_lits ys" + using assms unfolding var_lits_eq + by (metis List.finite_set Max_ge dual_order.trans imageI insertCI list.set(2) list.set_map) + +lemma sat_cmsxor_same: + assumes "\x. x \ var_lits xs \ w x = w' x" + shows "sat_cmsxor w xs = sat_cmsxor w' xs" + using assms +proof (induction xs) + case Nil + then show ?case + unfolding sat_cmsxor_def + by auto +next + case ih:(Cons x xs) + have 1: "sat_lit w x = sat_lit w' x" + apply (intro sat_lit_same) + using ih(2) + by (metis le_var_lits_in list.set_intros(1)) + have 2: "sat_cmsxor w xs = sat_cmsxor w' xs" + apply (intro ih(1)) + using ih(2) + by (smt (verit) List.finite_set Max_ge_iff empty_not_insert insert_iff list.set(2) list.simps(9) var_lits_eq) + show ?case + unfolding sat_cmsxor_cons + using 1 2 by presburger +qed + +(* linear *) +lemma sat_cmsxor_split: + assumes u: "var_lits xs < u" "var_lits ys < u" + assumes w': "w' = (\x. if x = u then \ sat_cmsxor w xs else w x)" + shows " + (sat_cmsxor w (xs @ ys) = + (sat_cmsxor w' (Pos u # xs) \ + sat_cmsxor w' (Neg u # ys)))" +proof - + have xs: "sat_cmsxor w' xs = sat_cmsxor w xs" + apply (intro sat_cmsxor_same) + using u unfolding w' by auto + have ys: "sat_cmsxor w' ys = sat_cmsxor w ys" + apply (intro sat_cmsxor_same) + using u unfolding w' by auto + + show ?thesis + unfolding sat_cmsxor_append sat_cmsxor_cons xs ys + unfolding w' by (auto simp add: sat_lit_def) +qed + +(* split an XOR constraint into chunks of at most k+3 literals *) +fun split_xor ::"nat \ cmsxor \ cmsxor list \ nat \ cmsxor list \ nat" + where "split_xor k xs (acc,u) = ( + if length xs \ k + 3 then (xs # acc, u) + else ( + let xs1 = take (k + 2) xs in + let xs2 = drop (k + 2) xs in + split_xor k (Neg u # xs2) ((Pos u # xs1) # acc, u+1) + ) + )" + +declare split_xor.simps[simp del] + +lemma split_xor_bound: + assumes "split_xor k xs (acc,u) = (acc',u')" + shows "u \ u'" + using assms +proof (induction "length xs" arbitrary: xs acc u acc' u' rule: less_induct) + case less + have " length xs \ k + 3 \ \ ( length xs \ k + 3)" by auto + moreover { + assume "length xs \ k + 3" + then have "u \ u'" + using less(2) split_xor.simps by auto + } + moreover { + assume s: "\ ( length xs \ k + 3)" + then have l: "length (Neg u # drop (Suc (Suc k)) xs) < length xs" + by auto + have "Suc u \ u'" + using s less(2) + unfolding split_xor.simps[of k xs] + using less(1)[OF l] by auto + then have "u \ u'" by auto + } + ultimately show ?case by auto +qed + +lemma var_lits_append: + shows "var_lits xs \ var_lits (xs @ ys)" + "var_lits ys \ var_lits (xs @ ys)" + unfolding var_lits_eq + by auto + +lemma fold_max_eq: + assumes "i \ u" + shows "fold max ls u = max u (fold max ls (i::nat))" + using assms + apply (induction ls arbitrary: i) + subgoal by clarsimp + apply clarsimp + by (smt (verit) List.finite_set Max.set_eq_fold Max_ge_iff empty_iff insert_iff list.set(2) max.orderI max_def pre_arith_simps(3)) + +(* We can be more precise here that the number of solutions + is preserved exactly, but for UNSAT this is not needed *) +lemma split_xor_sound: + assumes "sat_cmsxor w xs" "\x. x \ set acc \ sat_cmsxor w x" + assumes u: "var_lits xs < u" "\x. x \ set acc \ var_lits x < u" + assumes "split_xor k xs (acc,u) = (acc',u')" + obtains w' where + "\x. x < u \ w x = w' x" + "\x. x \ set acc' \ sat_cmsxor w' x" + "\x. x \ set acc' \ var_lits x < u'" + using assms +proof (induction "length xs" arbitrary: w xs acc u acc' u' thesis rule: less_induct) + case less + have " length xs \ k + 3 \ \ ( length xs \ k + 3)" by auto + moreover { + assume "length xs \ k + 3" + then have *: "acc' = xs # acc" + using less(7) split_xor.simps + by auto + then have + "\x. x < u \ w x = w x" + "\x. x \ set acc' \ sat_cmsxor w x" + "\x. x \ set acc' \ var_lits x < u'" + subgoal by meson + subgoal using less + by (metis * set_ConsD) + using less + by (metis "*" order_trans_rules(22) set_ConsD split_xor_bound) + } + moreover { + assume s: "\ (length xs \ k + 3)" + define xs1 where xs1:"xs1 = take (k + 2) xs" + define xs2 where xs2:"xs2 = drop (k + 2) xs" + have sp: "split_xor k (Neg u # xs2) ((Pos u # xs1) # acc, u+1) = (acc',u')" + by (metis less(7) s split_xor.simps xs1 xs2) + have l: "length (Neg u # xs2) < length xs" + using s xs2 by auto + + have xs: "xs = xs1 @ xs2" by (simp add: xs1 xs2) + + define w' where w': "w' = + (\x. if x = u then \ sat_cmsxor w xs1 else w x)" + + have vl: "var_lits xs1 < u" "var_lits xs2 < u" + apply (metis less(5) order_trans_rules(21) var_lits_append(1) xs) + by (metis less(5) order_trans_rules(21) var_lits_append(2) xs) + + from sat_cmsxor_split[OF this w'] + have satws1: "sat_cmsxor w' (Pos u # xs1)" + and satws2: "sat_cmsxor w' (Neg u # xs2)" + using less(3) xs by auto + + have satacc: "\x. x \ set ((Pos u # xs1) # acc) \ + sat_cmsxor w' x" + by (metis less(4) less(6) not_less sat_cmsxor_same satws1 set_ConsD w') + + have v1: "var_lits (Neg u # xs2) < u + 1" + unfolding var_lits_def + apply (simp add: var_lit_def) + using vl var_lits_def fold_max_eq + by (metis le_add2 le_add_same_cancel2 less_Suc_eq max.absorb3) + + have "fold max (map var_lit xs1) u < Suc u" + using vl var_lits_def + by (smt (verit, best) List.finite_set Max.set_eq_fold Max_ge_iff dual_order.trans empty_iff insert_iff lessI less_or_eq_imp_le list.set(2) not_less) + moreover have "\x. x \ set acc \ + fold max (map var_lit x) 0 < Suc u" + by (metis less(6) less_SucI var_lits_def) + ultimately have v2:"\x. x \ set ((Pos u # xs1) # acc) \ var_lits x < u + 1" + unfolding var_lits_def + by (auto simp add: var_lit_def) + + obtain w'' where + w'': "\x. x < u + 1 \ w' x = w'' x" + "\x. x \ set acc' \ sat_cmsxor w'' x" + "\x. x \ set acc' \ var_lits x < u'" + using less(1)[OF l _ satws2 satacc v1 v2 sp] + by auto + + have "\x. x < u \ w x = w'' x" + using w''(1) + unfolding w' + using less_Suc_eq by fastforce + + then have "\w''. ( + (\x. x < u \ w x = w'' x) \ + (\x. x \ set acc' \ sat_cmsxor w'' x) \ + (\x. x \ set acc' \ var_lits x < u'))" + using w''(2-3) by auto + } + ultimately show ?case + using less(2) + by (metis (mono_tags, lifting)) +qed + +definition split_xors ::"nat \ nat \ cmsxor list \ cmsxor list" +where "split_xors k u xs = fst (fold (split_xor k) xs ([],u))" + +lemma split_xors_sound: + assumes "\x. x \ set xs \ sat_cmsxor w x" + "\x. x \ set acc \ sat_cmsxor w x" + assumes u: "\x. x \ set xs \ var_lits x < u" + "\x. x \ set acc \ var_lits x < u" + assumes "fold (split_xor k) xs (acc,u) = (acc',u')" + obtains w' where + "\x. x < u \ w x = w' x" + "\x. x \ set acc' \ sat_cmsxor w' x" + "\x. x \ set acc' \ var_lits x < u'" + using assms +proof (induction xs arbitrary: w acc u acc' u') + case Nil + then show ?case + by auto +next + case ih:(Cons x xs) + obtain acc'' u'' where x: "split_xor k x (acc, u) = (acc'',u'')" + by fastforce + from split_xor_sound[OF _ _ _ _ this] + obtain w'' where + w'': "\x. x < u \ w x = w'' x" + "\x. x \ set acc'' \ sat_cmsxor w'' x" + "\x. x \ set acc'' \ var_lits x < u''" + by (smt (verit, del_insts) ih(4) ih(5) ih(6) ih.prems(2) list.set_intros(1)) + have rw: "fold (split_xor k) xs (acc'',u'') = (acc', u')" + using ih(7) x by auto + have 1: "\x. x \ set xs \sat_cmsxor w'' x" + by (metis basic_trans_rules(22) ih(3) ih(5) list.set_intros(2) not_less sat_cmsxor_same w''(1)) + have 2: "\x. x \ set xs \ var_lits x < u''" + by (meson ih(5) list.set_intros(2) order_trans_rules(22) split_xor_bound x) + show ?case + using ih(1)[OF _ 1 w''(2) 2 w''(3) rw] + by (smt (verit, best) basic_trans_rules(22) ih(2) split_xor_bound w''(1) x) +qed + +(* maximum variable occuring in the whole formula *) +definition var_fml :: "fml \ nat" + where "var_fml f = + max (fold max (map var_lits (fst f)) 0) + (fold max (map var_lits (snd f)) 0)" + +lemma var_fml_eq: + "var_fml f = + max (Max (set (0 # map var_lits (fst f)))) + (Max (set (0 # map var_lits (snd f))))" + unfolding var_fml_def Max.set_eq_fold + by auto + +definition split_fml ::" nat \ fml \ fml" + where "split_fml k f = ( + let u = var_fml f + 1 in + (fst f, (split_xors k u (snd f))) + )" + +lemma var_lits_var_fml: + shows "\x. x \ set (snd F) \ var_lits x \ var_fml F" + "\x. x \ set (fst F) \ var_lits x \ var_fml F" + unfolding var_fml_eq + subgoal + apply clarsimp + by (meson List.finite_set Max_ge finite_imageI finite_insert image_subset_iff max.coboundedI2 subset_insertI) + apply clarsimp + by (meson List.finite_set Max_ge finite_imageI finite_insert image_subset_iff max.coboundedI1 subset_insertI) + +lemma split_fml_satisfies: + assumes "sat_fml w F" + obtains w' where "sat_fml w' (split_fml k F)" +proof - + obtain acc' u' where + *: "fold (split_xor k) (snd F) ([], var_fml F + 1) = (acc',u')" + by fastforce + have 1:"\x. x \ set (snd F) \ sat_cmsxor w x" + using assms unfolding sat_fml_def by auto + have 2:"\x. x \ set (snd F) \ var_lits x < var_fml F + 1" + using var_lits_var_fml + by (meson less_add_one order_le_less_trans) + from split_xors_sound[OF 1 _ _ 2 *] + obtain w' where + w': "\x. x < var_fml F + 1 \ w x = w' x" + "\x. x \ set acc' \ sat_cmsxor w' x" + "\x. x \ set acc' \ var_lits x < u'" + using "2" by auto + have "\x. x \ set (fst F) \ sat_clause w' x" + by (metis assms less_add_one order_trans_rules(21) sat_fml_def sat_lits_same var_lits_var_fml(2) w'(1)) + + then have "sat_fml w' (split_fml k F)" + unfolding split_fml_def Let_def split_xors_def * + by (auto simp add: sat_fml_def w'(2)) + thus ?thesis + using that by auto +qed + +lemma split_fml_sols: + assumes "sols (split_fml k F) = {}" + shows "sols F = {}" + using assms + using split_fml_satisfies unfolding sols_def + by (metis Collect_empty_eq) + +definition blast_xors :: "cmsxor list \ clause list" + where "blast_xors xors = concat (map (\x. xor_clauses x True) xors)" + +definition blast_fml :: "fml \ clause list" + where "blast_fml f = + fst f @ blast_xors (snd f)" + +lemma sat_clauses_concat: + "sat_clauses w (concat xs) \ + (\x \ set xs. sat_clauses w x)" + unfolding sat_clauses_def + by auto + +lemma blast_xors_sound: + assumes "(\x. x \ set xors \ sat_cmsxor w x)" + shows "sat_clauses w (blast_xors xors)" + unfolding blast_xors_def sat_clauses_concat + by (auto simp add: assms sols_xor_clauses) + +lemma blast_fml_sound: + assumes "sat_fml w F" + shows "sat_fml w (blast_fml F,[])" + unfolding blast_fml_def sat_fml_def + apply clarsimp + using assms blast_xors_sound sat_clauses_def sat_fml_def by blast + +definition blast_split_fml :: "fml \ clause list" + where "blast_split_fml f = blast_fml (split_fml 1 f)" + +lemma blast_split_fml_sols: + assumes "sols (blast_split_fml F,[]) = {}" + shows "sols F = {}" + by (metis Collect_empty_eq assms blast_fml_sound blast_split_fml_def sols_def split_fml_sols) + +definition certcheck_blast::" + (clause list \ bool) \ + fml \ nat list \ + real \ real \ + ((nat \ bool) list \ + (nat \ (nat \ (nat \ bool) list \ (nat \ bool) list))) \ + (nat \ nat \ (bool list \ bool)) \ + String.literal + nat" + where "certcheck_blast check_unsat F S \ \ m0ms = + certcheck (check_unsat \ blast_split_fml) F S \ \ m0ms" + +(* Just for completeness, we re-state the main theorems *) +corollary certcheck_blast_sound: + assumes "\F. check_unsat F \ sols (F, []) = {}" + assumes "0 < \" "\ < 1" + assumes "0 < \" + assumes "distinct S" + shows " + measure_pmf.prob + (map_pmf (\r. certcheck_blast check_unsat F S \ \ (f r) r) + (random_seed_xors (find_t \) (length S))) + {c. \ isl c \ + real (projr c) \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} \ \" + unfolding certcheck_blast_def + apply (intro CertCheck_CNF_XOR.certcheck_sound[OF _ assms(2-5)]) + using assms(1) unfolding Let_def + using blast_split_fml_sols by auto + +corollary certcheck_blast_promise_complete: + assumes "\F. check_unsat F \ sols (F, []) = {}" + assumes "0 < \" "\ < 1" + assumes "0 < \" + assumes "distinct S" + assumes r: "\r. + r \ set_pmf (random_seed_xors (find_t \) (length S)) \ + \isl (certcheck_blast check_unsat F S \ \ (f r) r)" + shows " + measure_pmf.prob + (map_pmf (\r. certcheck_blast check_unsat F S \ \ (f r) r) + (random_seed_xors (find_t \) (length S))) + {c. real (projr c) \ + {real (card (proj (set S) (sols F))) / (1 + \).. + (1 + \) * real (card (proj (set S) (sols F)))}} \ 1 - \" + unfolding certcheck_blast_def + apply (intro CertCheck_CNF_XOR.certcheck_promise_complete[OF _ assms(2-5)]) + using assms(1) unfolding Let_def + using blast_split_fml_sols assms(6) unfolding certcheck_blast_def by auto + +subsection \ Export code for a SML implementation. \ + +definition real_of_int :: "integer \ real" + where "real_of_int n = real (nat_of_integer n)" + +definition real_mult :: "real \ real \ real" + where "real_mult n m = n * m" + +definition real_div :: "real \ real \ real" + where "real_div n m = n / m" + +definition real_plus :: "real \ real \ real" + where "real_plus n m = n + m" + +definition real_minus :: "real \ real \ real" + where "real_minus n m = n - m" + +declare [[code abort: fix_t]] + +(* Sample code export. + Helper Isabelle converters, followed by exporting the actual code *) +export_code + length + nat_of_integer int_of_integer + integer_of_nat integer_of_int + real_of_int real_mult real_div real_plus real_minus + quotient_of + + Pos Neg + CertCheck_CNF_XOR.appmc.compute_thresh + find_t certcheck + certcheck_blast + in SML + +end diff --git a/thys/Approximate_Model_Counting/ROOT b/thys/Approximate_Model_Counting/ROOT new file mode 100644 --- /dev/null +++ b/thys/Approximate_Model_Counting/ROOT @@ -0,0 +1,18 @@ +chapter AFP + +session Approximate_Model_Counting = Frequency_Moments + + options [timeout = 600] + sessions + Concentration_Inequalities + Monad_Normalisation + theories + ApproxMCPreliminaries + RandomXOR + RandomXORHashFamily + ApproxMCCore + ApproxMCCoreAnalysis + CertCheck + CertCheck_CNF_XOR + document_files + "root.tex" + "root.bib" diff --git a/thys/Approximate_Model_Counting/RandomXOR.thy b/thys/Approximate_Model_Counting/RandomXOR.thy new file mode 100644 --- /dev/null +++ b/thys/Approximate_Model_Counting/RandomXOR.thy @@ -0,0 +1,1634 @@ +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 + Frequency_Moments.Product_PMF_Ext + 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 + +(* A random XOR can also be sampled as a + map |V| \ bool + a coin flip *) +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 + +(* An assignment is a subset \ of V + i.e., those variables assigned to true *) +fun satisfies_xor :: "('a set \ bool) \ 'a set \ bool" + where "satisfies_xor (x,b) \ = + even (card (\ \ x) + of_bool b) " + +(* +(* x_0 \ x_1 \ x_2 = 0 *) +value "satisfies_xor ({0,1,2},False) {0::nat}" +(* x_0 \ x_1 \ x_2 = 1 *) +value "satisfies_xor ({0,1,2},True) {0::nat}" +*) + +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 + +(* TODO: there is a more general version below *) +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) = + (\\<^sub>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 "... = (\\<^sub>aa\A. \\<^sub>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 "... = (\\<^sub>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 "... = (\\<^sub>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 + +(* 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 \ 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 + +(* + 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 \ \" "\ \ 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 V) + + 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 + +(* Split probability for two disjoint non-empty sets *) +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 + +(* Split probability for three disjoint non-empty sets *) +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))" + +(* The set of random XORs expressed in various ways*) +lemma random_xors_set: + assumes V:"finite V" + shows + "PiE_dflt {.. (\_. map_pmf Some (random_xor V))) = + {xors. dom xors = {.. + ran xors \ (Pow V) \ UNIV}" (is "?lhs = ?rhs") +proof - + have "?lhs = + {f. dom 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 = {.. ran xors \ (Pow V) \ UNIV}" +proof - + have "pmf_of_set + {xors. dom xors = {.. + ran xors \ (Pow V) \ UNIV} = + pmf_of_set + (PiE_dflt {.. (\_. map_pmf Some (random_xor V))))" + unfolding random_xors_set[OF V] by auto + also have "... = + Pi_pmf {..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 + +(* The XOR hash function from a mapping nat \ XOR *) +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 = {.. + 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 \ = {.. x = \ \ + (dom x = {.. + (\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 \ = {.. xors = \} = + PiE_dflt {..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 \ = {.. 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 {..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 x = Some True} = + the (\ x)}))" + by (subst measure_Pi_pmf_PiE_dflt) + (auto simp add: measure_map_pmf inj_vimage_image_eq) + also have "... = (\x 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 \ = {..': "dom \' = {..: "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 {..i. Some ` {xor. satisfies_xor xor {x. \ x = Some True} = the (\ i)}) + \ + PiE_dflt {..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 {..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 x = Some True} = the (\ x) \ + satisfies_xor xor {x. \' x = Some True} = the (\' x)}))" + by (subst measure_Pi_pmf_PiE_dflt) + (auto simp add: measure_map_pmf inj_vimage_image_eq) + also have "... = (\x: "dom \ = {..': "dom \' = {..'': "dom \'' = {..: "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 {..i. Some ` {xor. satisfies_xor xor {x. \ x = Some True} = the (\ i)}) + \ + PiE_dflt {..i. Some ` {xor. satisfies_xor xor {x. \' x = Some True} = the (\' i)}) + \ + PiE_dflt {..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 {..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 {.._. map_pmf Some (random_xor V)))"]) + apply (intro arg_cong[where f="PiE_dflt {..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: measure_map_pmf inj_vimage_image_eq) + moreover have "... = (\xRandom XOR hash family\ + +text \This section defines a hash family based on random XORs and proves + that this hash family is 3-universal. \ + +theory RandomXORHashFamily imports + RandomXOR +begin + +lemma finite_dom: + assumes "finite V" + shows "finite {w :: 'a \ bool. dom w = V}" +proof - + have *: "{w :: 'a \ bool. dom w = V} = + {w. dom w = V \ ran w \ {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 \ xors = \" + shows "dom xors = dom \" + 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 \ xors = \} = + indicat_real {\::nat \ bool. dom \ = {0.. / + real (card {\::nat \ bool. dom \ = {0..::nat \ bool. dom \ = {0... dom \ = {0.. ran \ \ {True, False}}" + by auto + have **: "card {\::nat \ bool. dom \ = {0.. = {.. dom \ \ {.. = {..dom \ = {.. atLeast0LessThan) + } + moreover { + assume *:"dom \ \ {.. set_pmf (random_xors V n) \ + \ \ xor_hash \ 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 \ xors = \} = 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 \ = V" + shows "prob_space.uniform_on + (random_xors V n) + (xor_hash i) {\. dom \ = {0..: "dom \ = V" + assumes \': "dom \' = V" + assumes neq: "\ \ \'" + shows " + 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 = \} * + measure_pmf.prob (random_xors V n) + {xors. + xor_hash \' xors = \'})" +proof - + have "dom \ = {.. dom \' = {.. + \(dom \ = {.. dom \' = {.. = {..' = {.. xors = \ \ xor_hash \' xors = \'} = 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 \ xors = \} = 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 \' xors = \'} = 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 \ \ {.. dom \' \ {.. set_pmf (random_xors V n) \ + \ = xor_hash \ x \ + \' = xor_hash \' x \ 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 \ xors = \} = 0 \ + measure_pmf.prob (random_xors V n) + {xors. + xor_hash \' xors = \'} = 0" + unfolding prob_random_xors_xor_hash_indicat_real[OF V] + by (metis * atLeast0LessThan div_0 indicator_simps(2) mem_Collect_eq) + moreover have " + measure_pmf.prob (random_xors V n) + {xors. + xor_hash \ xors = \ \ xor_hash \' xors = \'} = 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 \ b" "b \ c" "c \ a" + shows"(\\\{a, b, c}. f \) = f a * (f b * f c)" + using assms by auto + +lemma random_xors_xor_hash_three_indicat: + assumes V: "finite V" + 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 = \''} = + (measure_pmf.prob (random_xors V n) + {xors. + xor_hash \ xors = \} * + measure_pmf.prob (random_xors V n) + {xors. + xor_hash \' xors = \'} * + measure_pmf.prob (random_xors V n) + {xors. + xor_hash \'' xors = \''})" +proof - + have "dom \ = {.. dom \' = {.. dom \'' = {.. + \(dom \ = {.. dom \' = {.. dom \'' = {.. = {..' = {..'' = {.. xors = \ \ + xor_hash \' xors = \' \ + xor_hash \'' xors = \''} = 1 / 8 ^n" + apply (intro random_xors_xor_hash_three) + using V * \ \' \'' neq by auto + have 2:" + measure_pmf.prob (random_xors V n) + {xors. xor_hash \ xors = \} = 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 \' xors = \'} = 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 \'' xors = \''} = 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 \ \ {.. dom \' \ {.. dom \'' \ {.. set_pmf (random_xors V n) \ + \ = xor_hash \ x \ + \' = xor_hash \' x \ + \'' = xor_hash \'' x \ 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 \ xors = \} = 0 \ + measure_pmf.prob (random_xors V n) + {xors. + xor_hash \' xors = \'} = 0 \ + measure_pmf.prob (random_xors V n) + {xors. + xor_hash \'' xors = \''} = 0" + unfolding prob_random_xors_xor_hash_indicat_real[OF V] + by (metis * atLeast0LessThan div_0 indicator_simps(2) mem_Collect_eq) + moreover have " + measure_pmf.prob (random_xors V n) + {xors. + xor_hash \ xors = \ \ xor_hash \' xors = \' \ xor_hash \'' xors = \''} = 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 \ 3" "J \ {\. dom \ = V}" + shows " + measure_pmf.prob (random_xors V n) + {xors. \\\J. xor_hash \ xors = f \} = + (\\\J. + measure_pmf.prob (random_xors V n) + {xors. xor_hash \ xors = f \})" +proof - + have "card J = 0 \ card J = 1 \ card J = 2 \ 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 \ \' where J:"J = {\, \'}" and + \: "\ \ \'" "dom \ = V" "dom \' = V" + unfolding card_2_iff + using J + by force + have ?thesis unfolding J + by (auto simp add: random_xors_xor_hash_pair_indicat V \) + } + moreover { + assume "card J = 3" + then obtain \ \' \'' where J:"J = {\, \', \''}" and + \: "\ \ \'" "\' \ \''" "\'' \ \" + "dom \ = V" "dom \' = V" "dom \'' = V" + unfolding card_3_iff + using J + by force + have ?thesis unfolding J + by (auto simp add: random_xors_xor_hash_three_indicat V \ prod_3_expand[OF \(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 + (\_. Universal_Hash_Families_More_Independent_Families.discrete) xor_hash + {\. dom \ = 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 + {\::'a \ bool. dom \ = V} + {\::nat \ bool. dom \ = {0..::'a \ bool. dom \ = V} + {\::nat \ bool. dom \ = {0.. 0$ and $0 < +\delta \leq 1$. The algorithmic specification is further refined to a verified +certificate checker that can be used to validate the results of untrusted +{$\mathsf{ApproxMC}$} implementations (assuming access to trusted randomness). +} + +\tableofcontents + +% sane default for proof documents +\parindent 0pt\parskip 0.5ex + +\input{session} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document} diff --git a/thys/ROOTS b/thys/ROOTS --- a/thys/ROOTS +++ b/thys/ROOTS @@ -1,805 +1,806 @@ ABY3_Protocols ADS_Functor AI_Planning_Languages_Semantics AODV AOT AVL-Trees AWN Abortable_Linearizable_Modules Abs_Int_ITP2012 Abstract-Hoare-Logics Abstract-Rewriting Abstract_Completeness Abstract_Soundness Ackermanns_not_PR Actuarial_Mathematics Adaptive_State_Counting Affine_Arithmetic Aggregation_Algebras Akra_Bazzi Algebraic_Numbers Algebraic_VCs Allen_Calculus Amicable_Numbers Amortized_Complexity AnselmGod Applicative_Lifting +Approximate_Model_Counting Approximation_Algorithms Architectural_Design_Patterns Aristotles_Assertoric_Syllogistic Arith_Prog_Rel_Primes ArrowImpossibilityGS Attack_Trees Auto2_HOL Auto2_Imperative_HOL AutoFocus-Stream Automated_Stateful_Protocol_Verification Automatic_Refinement AxiomaticCategoryTheory BDD BD_Security_Compositional BNF_CC BNF_Operations BTree Balog_Szemeredi_Gowers Banach_Steinhaus Belief_Revision Bell_Numbers_Spivey BenOr_Kozen_Reif Berlekamp_Zassenhaus Bernoulli Bertrands_Postulate Bicategory BinarySearchTree Binary_Code_Imprimitive Binding_Syntax_Theory Binomial-Heaps Binomial-Queues BirdKMP Birkhoff_Finite_Distributive_Lattices Blue_Eyes Bondy Boolean_Expression_Checkers Boolos_Curious_Inference Boolos_Curious_Inference_Automated Bounded_Deducibility_Security Buchi_Complementation Budan_Fourier Buffons_Needle Buildings BytecodeLogicJmlTypes C2KA_DistributedSystems CAVA_Automata CAVA_LTL_Modelchecker CCS CHERI-C_Memory_Model CISC-Kernel Concentration_Inequalities CRDT CRYSTALS-Kyber CRYSTALS-Kyber_Security CSP_RefTK CVP_Hardness CYK CZH_Elementary_Categories CZH_Foundations CZH_Universal_Constructions CakeML CakeML_Codegen Call_Arity Card_Equiv_Relations Card_Multisets Card_Number_Partitions Card_Partitions Cardinality_Continuum Cartan_FP Case_Labeling Catalan_Numbers Category Category2 Category3 Catoids Cauchy Cayley_Hamilton Certification_Monads Ceva Chandy_Lamport Chebyshev_Polynomials Chord_Segments Circus Clean Clique_and_Monotone_Circuits ClockSynchInst Closest_Pair_Points CoCon CoSMeDis CoSMed CofGroups Coinductive Coinductive_Languages Collections Combinable_Wands Combinatorial_Enumeration_Algorithms Combinatorics_Words Combinatorics_Words_Graph_Lemma Combinatorics_Words_Lyndon CommCSL Commuting_Hermitian Comparison_Sort_Lower_Bound Compiling-Exceptions-Correctly Complete_Non_Orders Completeness Complex_Bounded_Operators Complex_Geometry Complx ComponentDependencies ConcurrentGC ConcurrentIMP Concurrent_Ref_Alg Concurrent_Revisions Conditional_Simplification Conditional_Transfer_Rule Consensus_Refined Constructive_Cryptography Constructive_Cryptography_CM Constructor_Funs Containers Cook_Levin CoreC++ Core_DOM Core_SC_DOM Correctness_Algebras Cotangent_PFD_Formula Count_Complex_Roots Coupledsim_Contrasim CryptHOL CryptoBasedCompositionalProperties Crypto_Standards CubicalCategories Cubic_Quartic_Equations DCR-ExecutionEquivalence DFS_Framework DOM_Components DPRM_Theorem DPT-SAT-Solver DataRefinementIBP Datatype_Order_Generator Decl_Sem_Fun_PL Decreasing-Diagrams Decreasing-Diagrams-II Dedekind_Real Deep_Learning Delta_System_Lemma Density_Compiler Dependent_SIFUM_Refinement Dependent_SIFUM_Type_Systems Depth-First-Search Derangements Deriving Descartes_Sign_Rule Design_Theory Dict_Construction Differential_Dynamic_Logic Differential_Game_Logic DigitsInBase Digit_Expansions Dijkstra_Shortest_Path Diophantine_Eqns_Lin_Hom Directed_Sets Dirichlet_L Dirichlet_Series DiscretePricing Discrete_Summation Disintegration DiskPaxos Distributed_Distinct_Elements Dominance_CHK DynamicArchitectures Dynamic_Tables E_Transcendental Earley_Parser Echelon_Form EdmondsKarp_Maxflow Edwards_Elliptic_Curves_Group Efficient-Mergesort Efficient_Weighted_Path_Order Elimination_Of_Repeated_Factors Elliptic_Curves_Group_Law Encodability_Process_Calculi Epistemic_Logic Equivalence_Relation_Enumeration Ergodic_Theory Error_Function Euler_MacLaurin Euler_Partition Euler_Polyhedron_Formula Eudoxus_Reals Eval_FO Example-Submission Executable_Randomized_Algorithms Expander_Graphs Extended_Finite_State_Machine_Inference Extended_Finite_State_Machines FFT FLP FOL-Fitting FOL_Axiomatic FOL_Harrison FOL_Seq_Calc1 FOL_Seq_Calc2 FOL_Seq_Calc3 FO_Theory_Rewriting FSM_Tests Factor_Algebraic_Polynomial Factored_Transition_System_Bounding Falling_Factorial_Sum Farkas FeatherweightJava Featherweight_OCL Fermat3_4 FileRefinement FinFun Finger-Trees Finite-Map-Extras Finite_Automata_HF Finite_Fields Finitely_Generated_Abelian_Groups First_Order_Terms First_Welfare_Theorem Fishburn_Impossibility Fisher_Yates Fishers_Inequality Fixed_Length_Vector Flow_Networks Floyd_Warshall Flyspeck-Tame FocusStreamsCaseStudies Forcing Formal_Puiseux_Series Formal_SSA Formula_Derivatives Foundation_of_geometry Fourier Free-Boolean-Algebra Free-Groups Frequency_Moments Fresh_Identifiers FunWithFunctions FunWithTilings Functional-Automata Functional_Ordered_Resolution_Prover Furstenberg_Topology GPU_Kernel_PL Gabow_SCC GaleStewart_Games Gale_Shapley Game_Based_Crypto Gauss-Jordan-Elim-Fun Gauss_Jordan Gauss_Sums Gaussian_Integers GenClock General-Triangle Generalized_Counting_Sort Generic_Deriving Generic_Join GewirthPGCProof Girth_Chromatic Given_Clause_Loops Go GoedelGod Goedel_HFSet_Semantic Goedel_HFSet_Semanticless Goedel_Incompleteness Goodstein_Lambda GraphMarkingIBP Graph_Saturation Graph_Theory Gray_Codes Green Groebner_Bases Groebner_Macaulay Gromov_Hyperbolicity Grothendieck_Schemes Group-Ring-Module HOL-CSP HOL-CSPM HOL-CSP_OpSem HOLCF-Prelude HRB-Slicing Hahn_Jordan_Decomposition Hales_Jewett Heard_Of Hello_World HereditarilyFinite Hermite Hermite_Lindemann Hidden_Markov_Models Higher_Order_Terms HoareForDivergence Hoare_Time Hood_Melville_Queue HotelKeyCards Huffman Hybrid_Logic Hybrid_Multi_Lane_Spatial_Logic Hybrid_Systems_VCs HyperCTL HyperHoareLogic Hyperdual Hypergraph_Basics Hypergraph_Colourings IEEE_Floating_Point IFC_Tracking IMAP-CRDT IMO2019 IMP2 IMP2_Binary_Heap IMP_Compiler IMP_Compiler_Reuse Interval_Analysis IO_Language_Conformance IP_Addresses Imperative_Insertion_Sort Implicational_Logic Impossible_Geometry IMP_Noninterference Incompleteness Incredible_Proof_Machine Independence_CH Inductive_Confidentiality Inductive_Inference InfPathElimination InformationFlowSlicing InformationFlowSlicing_Inter Integration Interpolation_Polynomials_HOL_Algebra Interpreter_Optimizations Interval_Arithmetic_Word32 Intro_Dest_Elim Involutions2Squares Iptables_Semantics Irrational_Series_Erdos_Straus Irrationality_J_Hancl Irrationals_From_THEBOOK IsaGeoCoq IsaNet Isabelle_C Isabelle_hoops Isabelle_Marries_Dirac Isabelle_Meta_Model Jacobson_Basic_Algebra Jinja JinjaDCI JinjaThreads JiveDataStoreModel Jordan_Hoelder Jordan_Normal_Form KAD Karatsuba KAT_and_DRA KBPs KD_Tree Key_Agreement_Strong_Adversaries Khovanskii_Theorem Kleene_Algebra Kneser_Cauchy_Davenport Knights_Tour Knot_Theory Knuth_Bendix_Order Knuth_Morris_Pratt KnuthMorrisPratt Koenigsberg_Friendship Kruskal Kuratowski_Closure_Complement LLL_Basis_Reduction LLL_Factorization LOFT LP_Duality LTL LTL_Master_Theorem LTL_Normal_Form LTL_to_DRA LTL_to_GBA Lam-ml-Normalization LambdaAuth LambdaMu Lambda_Free_EPO Lambda_Free_KBOs Lambda_Free_RPOs Lambert_Series Lambert_W Landau_Symbols Laplace_Transform Latin_Square LatticeProperties Launchbury Laws_of_Large_Numbers Lazy-Lists-II Lazy_Case Lehmer Lifting_Definition_Option Lifting_the_Exponent LightweightJava LinearQuantifierElim Linear_Inequalities Linear_Programming Linear_Recurrences Liouville_Numbers List-Index List-Infinite List_Interleaving List_Inversions List_Update LocalLexing Localization_Ring Locally-Nameless-Sigma Logging_Independent_Anonymity Lovasz_Local Lowe_Ontological_Argument Lower_Semicontinuous Lp Lucas_Theorem MDP-Algorithms MDP-Rewards MFMC_Countable MFODL_Monitor_Optimized MFOTL_Monitor MSO_Regex_Equivalence Markov_Models Marriage Martingales Mason_Stothers Matrices_for_ODEs Matrix Matrix_Tensor Matroids Max-Card-Matching Maximum_Segment_Sum Median_Method Median_Of_Medians_Selection Menger Mereology Mersenne_Primes Metalogic_ProofChecker MHComputation MiniML MiniSail Minimal_SSA Minkowskis_Theorem Minsky_Machines MLSS_Decision_Proc ML_Unification Modal_Logics_for_NTS Modular_Assembly_Kit_Security Modular_arithmetic_LLL_and_HNF_algorithms Monad_Memo_DP Monad_Normalisation MonoBoolTranAlgebra MonoidalCategory Monomorphic_Monad MuchAdoAboutTwo Multi_Party_Computation Multirelations Multirelations_Heterogeneous Multiset_Ordering_NPC Multitape_To_Singletape_TM Myhill-Nerode Name_Carrying_Type_Inference Nano_JSON Nash_Williams Nat-Interval-Logic Native_Word Nested_Multisets_Ordinals Network_Security_Policy_Verification Neumann_Morgenstern_Utility No_FTL_observers No_FTL_observers_Gen_Rel Nominal2 Nominal_Myhill_Nerode Noninterference_CSP Noninterference_Concurrent_Composition Noninterference_Generic_Unwinding Noninterference_Inductive_Unwinding Noninterference_Ipurge_Unwinding Noninterference_Sequential_Composition NormByEval Nullstellensatz Number_Theoretic_Transform Octonions OmegaCatoidsQuantales OpSets Open_Induction Optics Optimal_BST Orbit_Stabiliser Order_Lattice_Props Ordered_Resolution_Prover Ordinal Ordinal_Partitions Ordinals_and_Cardinals Ordinary_Differential_Equations PAC_Checker PAL PAPP_Impossibility PCF PLM POPLmark-deBruijn PSemigroupsConvolution Package_logic Padic_Field Padic_Ints Pairing_Heap Paraconsistency Parity_Game Partial_Function_MR Partial_Order_Reduction Password_Authentication_Protocol Pell Perfect_Fields Perfect-Number-Thm Perron_Frobenius Physical_Quantities Pi_Calculus Pi_Transcendental Planarity_Certificates Pluennecke_Ruzsa_Inequality Poincare_Bendixson Poincare_Disc Polygonal_Number_Theorem Polylog Polynomial_Crit_Geometry Polynomial_Factorization Polynomial_Interpolation Polynomials Pop_Refinement Posix-Lexing Possibilistic_Noninterference Power_Sum_Polynomials Pratt_Certificate Prefix_Free_Code_Combinators Presburger-Automata Prim_Dijkstra_Simple Prime_Distribution_Elementary Prime_Harmonic_Series Prime_Number_Theorem Priority_Queue_Braun Priority_Search_Trees Probabilistic_Noninterference Probabilistic_Prime_Tests Probabilistic_System_Zoo Probabilistic_Timed_Automata Probabilistic_While Probability_Inequality_Completeness Program-Conflict-Analysis Progress_Tracking Projective_Geometry Projective_Measurements Promela Proof_Strategy_Language PropResPI Propositional_Logic_Class Propositional_Proof_Systems Prpu_Maxflow PseudoHoops Psi_Calculi Ptolemys_Theorem Public_Announcement_Logic Q0_Metatheory Q0_Soundness QBF_Solver_Verification QHLProver QR_Decomposition Quantales Quantales_Converse Quantifier_Elimination_Hybrid Quasi_Borel_Spaces Quaternions Query_Optimization Quick_Sort_Cost RIPEMD-160-SPARK ROBDD RSAPSS Ramsey-Infinite Random_BSTs Random_Graph_Subgraph_Threshold Randomised_BSTs Randomised_Social_Choice Rank_Nullity_Theorem Real_Impl Real_Power Real_Time_Deque Recursion-Addition Recursion-Theory-I Refine_Imperative_HOL Refine_Monadic RefinementReactive Regex_Equivalence Region_Quadtrees Registers Regression_Test_Selection Regular-Sets Regular_Algebras Regular_Tree_Relations Relation_Algebra Relational-Incorrectness-Logic Relational_Cardinality Relational_Disjoint_Set_Forests Relational_Forests Relational_Method Relational_Minimum_Spanning_Trees Relational_Paths Rensets Rep_Fin_Groups ResiduatedTransitionSystem Residuated_Lattices Resolution_FOL Rewrite_Properties_Reduction Rewriting_Z Ribbon_Proofs Risk_Free_Lending Robbins-Conjecture Robinson_Arithmetic Root_Balanced_Tree Roth_Arithmetic_Progressions Routing Roy_Floyd_Warshall SATSolverVerification SCC_Bloemen_Sequential SC_DOM_Components SDS_Impossibility SIFPL SIFUM_Type_Systems SPARCv8 S_Finite_Measure_Monad Safe_Distance Safe_OCL Safe_Range_RC Saturation_Framework Saturation_Framework_Extensions Sauer_Shelah_Lemma Schutz_Spacetime Schwartz_Zippel Secondary_Sylow Security_Protocol_Refinement Selection_Heap_Sort SenSocialChoice Separata Separation_Algebra Separation_Logic_Imperative_HOL Separation_Logic_Unbounded SequentInvertibility Shadow_DOM Shadow_SC_DOM Shivers-CFA ShortestPath Show Sigma_Commit_Crypto Signature_Groebner Simpl Simple_Clause_Learning Simple_Firewall Simplex Simplicial_complexes_and_boolean_functions SimplifiedOntologicalArgument Skew_Heap Skip_Lists Slicing Sliding_Window_Algorithm Smith_Normal_Form Smooth_Manifolds Solidity Sophomores_Dream Sort_Encodings Source_Coding_Theorem SpecCheck Special_Function_Bounds Splay_Tree Sqrt_Babylonian Stable_Matching Stalnaker_Logic Standard_Borel_Spaces Statecharts Stateful_Protocol_Composition_and_Typing Stellar_Quorums Stern_Brocot Stewart_Apollonius Stirling_Formula Stochastic_Matrices Stone_Algebras Stone_Kleene_Relation_Algebras Stone_Relation_Algebras Store_Buffer_Reduction Stream-Fusion Stream_Fusion_Code StrictOmegaCategories Strong_Security Sturm_Sequences Sturm_Tarski Stuttering_Equivalence Subresultants Subset_Boolean_Algebras Sumcheck_Protocol SumSquares Sunflowers SuperCalc Suppes_Theorem Surprise_Paradox Symmetric_Polynomials Syntax_Independent_Logic Synthetic_Completeness Szemeredi_Regularity Szpilrajn TESL_Language TLA Tail_Recursive_Functions Tarskis_Geometry Taylor_Models Three_Circles Three_Squares Timed_Automata Topological_Semantics Topology TortoiseHare TsirelsonBound Transcendence_Series_Hancl_Rucki Transformer_Semantics Transition_Systems_and_Automata Transitive-Closure Transitive-Closure-II Transitive_Models Transport Treaps Tree-Automata Tree_Decomposition Tree_Enumeration Triangle Trie Turans_Graph_Theorem Twelvefold_Way Two_Generated_Word_Monoids_Intersection Tycon Types_Tableaus_and_Goedels_God Types_To_Sets_Extension UPF UPF_Firewall UTP Undirected_Graph_Theory Universal_Hash_Families Universal_Turing_Machine UpDown_Scheme VYDRA_MDL Valuation Van_Emde_Boas_Trees Van_der_Waerden VectorSpace VeriComp Verified-Prover Verified_SAT_Based_AI_Planning VerifyThis2018 VerifyThis2019 Vickrey_Clarke_Groves Virtual_Substitution VolpanoSmith WHATandWHERE_Security WOOT_Strong_Eventual_Consistency WebAssembly Weight_Balanced_Trees Weighted_Arithmetic_Geometric_Mean Weighted_Path_Order Well_Quasi_Orders Wetzels_Problem Wieferich_Kempner Winding_Number_Eval Word_Lib WorkerWrapper X86_Semantics XML Youngs_Inequality ZFC_in_HOL Zeckendorf Zeta_3_Irrational Zeta_Function pGCL Labeled_Transition_Systems Pushdown_Systems