spmf_of_set {..The following is a deterministic version. It returns the lexicographically minimal monic
+irreducible polynomial. Note that contrary to the randomized algorithm, the run time of the
+deterministic algorithm may be exponential (w.r.t. to the size of the field and degree of the
+polynomial).\
+
+fun find_irreducible_poly :: "nat \ nat \ nat list"
+ where "find_irreducible_poly p n = (let f = enum_monic_poly (mod_ring p) n in
+ f (while ((\k. \rabin_test (mod_ring p) (f k))) (\x. x + 1) 0))"
+
+definition cost :: "('a \ nat) option \ enat"
+ where "cost x = (case x of None \ \ | Some (_,r) \ enat r)"
+
+lemma cost_tick: "cost (map_option (\(x, c). (x, Suc c)) c) = eSuc (cost c)"
+ by (cases c) (auto simp:cost_def eSuc_enat)
+
+context
+ fixes n p :: nat
+ assumes p_prime: "Factorial_Ring.prime p"
+ assumes n_gt_0: "n > 0"
+begin
+
+private definition S where "S = {f. monic_poly (ring_of (mod_ring p)) f \ degree f = n }"
+private definition T where "T = {f. monic_irreducible_poly (ring_of (mod_ring p)) f \ degree f = n}"
+
+lemmas field_c = mod_ring_is_field_c[OF p_prime]
+lemmas enum_c = mod_ring_is_enum_c[where n="p"]
+
+interpretation finite_field "ring_of (mod_ring p)"
+ unfolding finite_field_def finite_field_axioms_def
+ by (intro mod_ring_is_field conjI mod_ring_finite p_prime)
+
+private lemmas field_ops = field_cD[OF field_c]
+
+private lemma S_fin: "finite S"
+ unfolding S_def
+ using enum_monic_poly[OF field_c enum_c, where d="n"]
+ bij_betw_finite by auto
+
+private lemma T_sub_S: "T \ S"
+ unfolding S_def T_def monic_irreducible_poly_def by auto
+
+private lemma T_card_gt_0: "real (card T) > 0"
+proof -
+ have "0 < real (order (ring_of (mod_ring p))) ^ n / (2 * real n)"
+ using n_gt_0 finite_field_min_order by (intro divide_pos_pos) (simp_all)
+ also have "... \ real (card T)" unfolding T_def by (intro card_irred_gt_0 n_gt_0)
+ finally show "real (card T) > 0" by auto
+qed
+
+private lemma S_card_gt_0: "real (card S) > 0"
+proof -
+ have "0 < card T" using T_card_gt_0 by simp
+ also have "... \ card S" by (intro card_mono T_sub_S S_fin)
+ finally have "0 < card S" by simp
+ thus ?thesis by simp
+qed
+
+private lemma S_ne: "S \ {}" using S_card_gt_0 by auto
+
+private lemma sample_irreducible_poly_step_aux:
+ "do {
+ k \ spmf_of_set {.. spmf_of_set S;
+ if monic_irreducible_poly (ring_of (mod_ring p)) poly
+ then return_spmf (poly,c)
+ else x
+ }"
+ (is "?L = ?R")
+proof -
+ have "order (ring_of (mod_ring p)) = p"
+ unfolding Finite_Fields_Mod_Ring_Code.mod_ring_def Coset.order_def ring_of_def by simp
+ hence 0:"spmf_of_set S = map_spmf (enum_monic_poly (mod_ring p) n) (spmf_of_set {..
spmf_of_set S; if rabin_test (mod_ring p) f then return_spmf (f,c) else x}"
+ unfolding 0 bind_map_spmf by (simp add:Let_def comp_def)
+ also have "... = ?R"
+ using set_spmf_of_set_finite[OF S_fin]
+ by (intro bind_spmf_cong refl if_cong rabin_test field_c enum_c) (simp add:S_def)
+ finally show ?thesis by simp
+qed
+
+private lemma sample_irreducible_poly_step:
+ "sample_irreducible_poly p n =
+ do {
+ poly \ spmf_of_set S;
+ if monic_irreducible_poly (ring_of (mod_ring p)) poly
+ then return_spmf (poly,1)
+ else tick_spmf (sample_irreducible_poly p n)
+ }"
+ by (subst sample_irreducible_poly.simps) (simp add:sample_irreducible_poly_step_aux)
+
+private lemma sample_irreducible_poly_aux_1:
+ "ord_spmf (=) (map_spmf fst (sample_irreducible_poly p n)) (spmf_of_set T)"
+proof (induction rule:sample_irreducible_poly.fixp_induct)
+ case 1 thus ?case by simp
+next
+ case 2 thus ?case by simp
+next
+ case (3 rec)
+ let ?f = "monic_irreducible_poly (ring_of (mod_ring p))"
+
+ have "real (card (S\-{x. ?f x})) = real (card (S - T))"
+ unfolding S_def T_def by (intro arg_cong[where f="card"] arg_cong[where f="of_nat"]) (auto)
+ also have "... = real (card S - card T)"
+ by (intro arg_cong[where f="of_nat"] card_Diff_subset T_sub_S finite_subset[OF T_sub_S S_fin])
+ also have "... = real (card S) - card T"
+ by (intro of_nat_diff card_mono S_fin T_sub_S)
+ finally have 0:"real (card (S\-{x. ?f x})) = real (card S) - card T" by simp
+
+ have S_card_gt_0: "real (card S) > 0" using S_ne S_fin by auto
+
+ have "do {f \ spmf_of_set S;if ?f f then return_spmf f else spmf_of_set T} = spmf_of_set T"
+ (is "?L = ?R")
+ proof (rule spmf_eqI)
+ fix i
+ have "spmf ?L i = spmf (pmf_of_set S \(\x. if ?f x then return_spmf x else spmf_of_set T)) i"
+ unfolding spmf_of_pmf_pmf_of_set[OF S_fin S_ne, symmetric] spmf_of_pmf_def
+ by (simp add:bind_spmf_def bind_map_pmf)
+ also have "... = (\x. (if ?f x then of_bool (x=i) else spmf (spmf_of_set T) i) \pmf_of_set S)"
+ unfolding pmf_bind if_distrib if_distribR pmf_return_spmf indicator_def by (simp cong:if_cong)
+ also have "... = (\x \ S. (if ?f x then of_bool (x = i) else spmf (spmf_of_set T) i))/card S"
+ by (subst integral_pmf_of_set[OF S_ne S_fin]) simp
+ also have "... = (of_bool (i \ T) + spmf (spmf_of_set T) i*real (card (S\-{x. ?f x})))/card S"
+ using S_fin S_ne
+ by (subst sum.If_cases[OF S_fin]) (simp add:of_bool_def T_def monic_irreducible_poly_def S_def)
+ also have "... = (of_bool (i \ T)*(1 + real (card (S\-{x. ?f x}))/real (card T)))/card S"
+ unfolding spmf_of_set indicator_def by (simp add:algebra_simps)
+ also have "... = (of_bool (i \ T)*(real (card S)/real (card T)))/card S"
+ using T_card_gt_0 unfolding 0 by (simp add:field_simps)
+ also have "... = of_bool (i \ T)/real (card T)"
+ using S_card_gt_0 by (simp add:field_simps)
+ also have "... = spmf ?R i"
+ unfolding spmf_of_set by simp
+ finally show "spmf ?L i = spmf ?R i"
+ by simp
+ qed
+ hence "ord_spmf (=)
+ (spmf_of_set S \ (\x. if ?f x then return_spmf x else spmf_of_set T)) (spmf_of_set T)"
+ by simp
+ moreover have "ord_spmf (=)
+ (do { poly \ spmf_of_set S; if ?f poly then return_spmf poly else map_spmf fst (rec p n)})
+ (do { poly \ spmf_of_set S; if ?f poly then return_spmf poly else spmf_of_set T})"
+ using 3 by (intro bind_spmf_mono') simp_all
+ ultimately have "ord_spmf (=) (spmf_of_set S \
+ (\x. if ?f x then return_spmf x else map_spmf fst (rec p n))) (spmf_of_set T)"
+ using spmf.leq_trans by force
+ thus ?case unfolding sample_irreducible_poly_step_aux map_spmf_bind_spmf
+ by (simp add:comp_def if_distribR if_distrib spmf.map_comp case_prod_beta cong:if_cong)
+qed
+
+lemma cost_sample_irreducible_poly:
+ "(\\<^sup>+x. cost x \sample_irreducible_poly p n) \ 2*real n" (is "?L \ ?R")
+proof -
+ let ?f = "monic_irreducible_poly (ring_of (mod_ring p))"
+ let ?a = "(\t. measure (sample_irreducible_poly p n) {\. enat t < cost \})"
+ let ?b = "(\t. measure (sample_irreducible_poly p n) {\. enat t \ cost \})"
+
+ define \ where "\ = measure (pmf_of_set S) {x. ?f x}"
+ have \_le_1: "\ \ 1" unfolding \_def by simp
+
+ have "1 / (2* real n) = (card S / (2 * real n)) / card S"
+ using S_card_gt_0 by (simp add:algebra_simps)
+ also have "... = (real (order (ring_of (mod_ring p)))^n / (2 * real n)) / card S"
+ unfolding S_def bij_betw_same_card[OF enum_monic_poly[OF field_c enum_c, where d="n"],symmetric]
+ by simp
+ also have "... \ card T / card S"
+ unfolding T_def by (intro divide_right_mono card_irred_gt_0 n_gt_0) auto
+ also have "... = \"
+ unfolding \_def measure_pmf_of_set[OF S_ne S_fin]
+ by (intro arg_cong2[where f="(/)"] refl arg_cong[where f="of_nat"] arg_cong[where f="card"])
+ (auto simp: S_def T_def monic_irreducible_poly_def)
+ finally have \_lb: "1/ (2*real n) \ \"
+ by simp
+ have "0 < 1/ (2*real n)" using n_gt_0 by simp
+ also have "... \ \" using \_lb by simp
+ finally have \_gt_0: "\ > 0" by simp
+
+ have a_step_aux: "norm (a * b) \ 1" if "norm a \ 1" "norm b \ 1" for a b :: real
+ using that by (simp add:abs_mult mult_le_one)
+
+ have b_eval: "?b t = (\x. (if ?f x then of_bool(t \ 1) else
+ measure (sample_irreducible_poly p n) {\. enat t \ eSuc (cost \)}) \pmf_of_set S)"
+ (is "?L1 = ?R1") for t
+ proof -
+ have "?b t = measure (bind_spmf (spmf_of_set S) (\x. if ?f x then return_spmf (x,1) else
+ tick_spmf (sample_irreducible_poly p n))) {\. enat t \ cost \}"
+ by (subst sample_irreducible_poly_step) simp
+ also have "... = measure (bind_pmf (pmf_of_set S) (\x. if ?f x then return_spmf (x,1) else
+ tick_spmf (sample_irreducible_poly p n))) {\. enat t \ cost \}"
+ unfolding spmf_of_pmf_pmf_of_set[OF S_fin S_ne, symmetric]
+ by (simp add:spmf_of_pmf_def bind_map_pmf bind_spmf_def)
+ also have "... = (\x. (if ?f x then of_bool(t \ 1) else
+ measure (tick_spmf (sample_irreducible_poly p n)) {\. enat t \ cost \}) \pmf_of_set S)"
+ unfolding measure_bind_pmf if_distrib if_distribR emeasure_return_pmf
+ by (simp add:indicator_def cost_def comp_def cong:if_cong)
+ also have "... = ?R1"
+ unfolding measure_map_pmf vimage_def
+ by (intro arg_cong2[where f="integral\<^sup>L"] refl ext if_cong arg_cong2[where f="measure"])
+ (auto simp add:vimage_def cost_tick eSuc_enat[symmetric])
+ finally show ?thesis by simp
+ qed
+
+ have b_eval_2: "?b t = 1 - (1-\)^t" for t
+ proof (induction t)
+ case 0
+ have "?b 0 = 0" unfolding b_eval by (simp add:enat_0 cong:if_cong )
+ thus ?case by simp
+ next
+ case (Suc t)
+ have "?b (Suc t) = (\x. (if ?f x then 1 else ?b t) \pmf_of_set S)"
+ unfolding b_eval[of "Suc t"]
+ by (intro arg_cong2[where f="integral\<^sup>L"] if_cong arg_cong2[where f="measure"])
+ (auto simp add: eSuc_enat[symmetric])
+ also have "... = (\x. indicator {x. ?f x} x + ?b t * indicator {x. \?f x} x \pmf_of_set S)"
+ by (intro Bochner_Integration.integral_cong) (auto simp:algebra_simps)
+ also have "... = (\x. indicator {x. ?f x} x \pmf_of_set S) +
+ (\x. ?b t * indicator {x. \?f x} x \pmf_of_set S)"
+ by (intro Bochner_Integration.integral_add measure_pmf.integrable_const_bound[where B="1"]
+ AE_pmfI a_step_aux) auto
+ also have "... = \ + ?b t * measure (pmf_of_set S) {x. \?f x}" unfolding \_def by simp
+ also have "... = \ + (1-\) * ?b t"
+ unfolding \_def
+ by (subst measure_pmf.prob_compl[symmetric]) (auto simp:Compl_eq_Diff_UNIV Collect_neg_eq)
+ also have "... = 1 - (1-\)^Suc t"
+ unfolding Suc by (simp add:algebra_simps)
+ finally show ?case by simp
+ qed
+
+ hence a_eval: "?a t = (1-\)^t" for t
+ proof -
+ have "?a t = 1 - ?b t"
+ by (simp add: measure_pmf.prob_compl[symmetric] Compl_eq_Diff_UNIV[symmetric]
+ Collect_neg_eq[symmetric] not_le)
+ also have "... = (1-\)^t"
+ unfolding b_eval_2 by simp
+ finally show ?thesis by simp
+ qed
+
+ have "?L = (\