Theory Random_List_Permutation

theory Random_List_Permutation
imports Probability_Misc Linorder_Relations
(*
  File:      Random_List.thy
  Authors:   Manuel Eberl

  Some facts about randomly permuted lists and how to obtain them by drawing i.i.d.
  priorities for every element.
*)
section ‹Randomly-permuted lists›
theory Random_List_Permutation
imports
  Probability_Misc
  Comparison_Sort_Lower_Bound.Linorder_Relations
begin

subsection ‹General facts about linear orderings›

text ‹
  We define the set of all linear orderings on a given set and show some properties about it.
›
definition linorders_on :: "'a set ⇒ ('a × 'a) set set" where
  "linorders_on A = {R. linorder_on A R}"
  
lemma linorders_on_empty [simp]: "linorders_on {} = {{}}"
  by (auto simp: linorders_on_def linorder_on_def refl_on_def)
    
lemma linorders_finite_nonempty:
  assumes "finite A"
  shows   "linorders_on A ≠ {}"
proof -
  from finite_distinct_list[OF assms] obtain xs where "set xs = A" "distinct xs" by blast
  hence "linorder_on A (linorder_of_list xs)" by auto
  thus ?thesis by (auto simp: linorders_on_def)
qed

text ‹
  There is an obvious bijection between permutations of a set (i.\,e.\ lists with all elements
  from that set without repetition) and linear orderings on it.
›
lemma bij_betw_linorders_on:
  assumes "finite A"
  shows   "bij_betw linorder_of_list (permutations_of_set A) (linorders_on A)"
  using bij_betw_linorder_of_list[of A] assms unfolding linorders_on_def by simp

lemma sorted_wrt_list_of_set_linorder_of_list [simp]:
  assumes "distinct xs"
  shows   "sorted_wrt_list_of_set (linorder_of_list xs) (set xs) = xs"
  by (rule sorted_wrt_list_of_set_eqI[of "set xs"]) (insert assms, auto)
    
lemma linorder_of_list_sorted_wrt_list_of_set [simp]:
  assumes "linorder_on A R" "finite A"
  shows   "linorder_of_list (sorted_wrt_list_of_set R A) = R"
proof -
  from assms(1) have subset: "R ⊆ A × A" by (auto simp: linorder_on_def refl_on_def)
  from assms and subset show ?thesis
    by (auto simp: linorder_of_list_def linorder_sorted_wrt_list_of_set sorted_wrt_linorder_index_le_iff)
qed

lemma bij_betw_linorders_on':
  assumes "finite A"
  shows   "bij_betw (λR. sorted_wrt_list_of_set R A) (linorders_on A) (permutations_of_set A)"
  by (rule bij_betw_byWitness[where f' = linorder_of_list])
     (insert assms, auto simp: linorders_on_def permutations_of_set_def
        linorder_sorted_wrt_list_of_set)

lemma finite_linorders_on [intro]:
  assumes "finite A"
  shows   "finite (linorders_on A)"
proof -
  have "finite (permutations_of_set A)" by simp
  also have "?this ⟷ finite (linorders_on A)"
    using assms by (rule bij_betw_finite [OF bij_betw_linorders_on])
  finally show ?thesis .
qed


text ‹
  Next, we look at the ordering defined by a list that is permuted with some permutation
  function. For this, we first define the composition of a relation with a function.
›
definition map_relation :: "'a set ⇒ ('a ⇒ 'b) ⇒ ('b × 'b) set ⇒ ('a × 'a) set" where
  "map_relation A f R = {(x,y)∈A×A. (f x, f y) ∈ R}"

lemma index_distinct_eqI:
  assumes "distinct xs" "i < length xs" "xs ! i = x"
  shows   "index xs x = i"
  using assms by (induction xs arbitrary: i) (auto simp: nth_Cons split: nat.splits)
  
lemma index_permute_list:
  assumes "π permutes {..<length xs}" "distinct xs" "x ∈ set xs"
  shows   "index (permute_list π xs) x = inv π (index xs x)"
proof -
  have *: "inv π permutes {..<length xs}" by (rule permutes_inv) fact
  from assms show ?thesis
    using assms permutes_in_image[OF *]
    by (intro index_distinct_eqI) (simp_all add: permute_list_nth permutes_inverses)
qed

lemma linorder_of_list_permute:
  assumes "π permutes {..<length xs}" "distinct xs"
  shows   "linorder_of_list (permute_list π xs) =
             map_relation (set xs) ((!) xs ∘ inv π ∘ index xs) (linorder_of_list xs)"
proof -
  note * = permutes_inv[OF assms(1)]
  have less: "inv π i < length xs" if "i < length xs" for i
    using permutes_in_image[OF *] and that by simp
  from assms and * show ?thesis
    by (auto simp: linorder_of_list_def map_relation_def index_nth_id index_permute_list less)
qed


lemma inj_on_conv_Ex1: "inj_on f A ⟷ (∀y∈f`A. ∃!x∈A. y = f x)"
  by (auto simp: inj_on_def)

lemma bij_betw_conv_Ex1: "bij_betw f A B ⟷ (∀y∈B. ∃!x∈A. f x = y) ∧ B = f ` A"
  unfolding bij_betw_def inj_on_conv_Ex1 by (auto simp: eq_commute)

lemma permutesI:
  assumes "bij_betw f A A" "∀x. x ∉ A ⟶ f x = x"
  shows   "f permutes A"
  unfolding permutes_def
proof (intro conjI allI impI)
  fix y
  from assms have [simp]: "f x ∈ A ⟷ x ∈ A" for x
    by (auto simp: bij_betw_def)
  show "∃!x. f x = y"
  proof (cases "y ∈ A")
    case True
    also from assms have "A = f ` A" by (auto simp: bij_betw_def)
    finally obtain x where "x ∈ A" "y = f x" by auto
    with assms and ‹y ∈ A› show ?thesis
      by (intro ex1I[of _ x]) (auto simp: bij_betw_def dest: inj_onD)
  qed (insert assms, auto)
qed (insert assms, auto)

text ‹
  We now show the important lemma that any two linear orderings on a finite set can be
  mapped onto each other by a permutation.
›
lemma linorder_permutation_exists:
  assumes "finite A" "linorder_on A R" "linorder_on A R'"
  obtains π where "π permutes A" "R' = map_relation A π R"
proof -
  define xs where "xs = sorted_wrt_list_of_set R A"
  define ys where "ys = sorted_wrt_list_of_set R' A"
  have xs_ys: "distinct xs" "distinct ys" "set xs = A" "set ys = A"
    using assms by (simp_all add: linorder_sorted_wrt_list_of_set xs_def ys_def)
      
  from xs_ys have "mset ys = mset xs" by (simp add: set_eq_iff_mset_eq_distinct [symmetric])
  from mset_eq_permutation[OF this] guess π . note π = this
  define π' where "π' = (λx. if x ∉ A then x else xs ! inv π (index xs x))"
  have π': "π' permutes A"
  proof (rule permutesI)
    have "bij_betw ((!) xs ∘ inv π) {..<length xs} A"
      by (rule bij_betw_trans permutes_imp_bij permutes_inv π bij_betw_nth)+ (simp_all add: xs_ys)
    hence "bij_betw ((!) xs ∘ inv π ∘ index xs) A A"
      by (rule bij_betw_trans [rotated] bij_betw_index)+
         (insert bij_betw_index[of xs A "length xs"], simp_all add: xs_ys atLeast0LessThan)
    also have "bij_betw ((!) xs ∘ inv π ∘ index xs) A A ⟷ bij_betw π' A A"
      by (rule bij_betw_cong) (auto simp: π'_def)
    finally show  .
  qed (simp_all add: π'_def)
  
  from assms have "R' = linorder_of_list ys" by (simp add: ys_def)
  also from π have "ys = permute_list π xs" by simp
  also have "linorder_of_list (permute_list π xs) = 
               map_relation A ((!) xs ∘ inv π ∘ index xs) (linorder_of_list xs)"
    using π by (subst linorder_of_list_permute) (simp_all add: xs_ys)
  also from assms have "linorder_of_list xs = R" by (simp add: xs_def)
  finally have "R' = map_relation A ((!) xs ∘ inv π ∘ index xs) R" .
  also have "… = map_relation A π' R" by (auto simp: map_relation_def π'_def)
  finally show ?thesis using π' and that[of π'] by simp
qed

text ‹
  We now define the linear ordering defined by some priority function, i.\,e.\ a function
  that injectively associates priorities to every element such that elements with lower priority
  are smaller in the resulting ordering.
›
definition linorder_from_keys :: "'a set ⇒ ('a ⇒ 'b :: linorder) ⇒ ('a × 'a) set" where
  "linorder_from_keys A f = {(x,y)∈A×A. f x ≤ f y}"

lemma linorder_from_keys_permute:
  assumes "g permutes A"
  shows   "linorder_from_keys A (f ∘ g) = map_relation A g (linorder_from_keys A f)"
  using permutes_in_image[OF assms] by (auto simp: map_relation_def linorder_from_keys_def)
  
lemma linorder_on_linorder_from_keys [intro]:
  assumes "inj_on f A"
  shows   "linorder_on A (linorder_from_keys A f)"
  using assms by (auto simp: linorder_on_def refl_on_def antisym_def linorder_from_keys_def
                    trans_def total_on_def dest: inj_onD)

lemma linorder_from_keys_empty [simp]: "linorder_from_keys {} = (λ_. {})"
  by (simp add: linorder_from_keys_def fun_eq_iff)
    

text ‹
  We now show another important fact, namely that when we draw $n$ values i.\,i.\,d.\ uniformly
  from a non-trivial real interval, we almost surely get distinct values.
›
lemma emeasure_PiM_diagonal:
  fixes a b :: real
  assumes "x ∈ A" "y ∈ A" "x ≠ y"
  assumes "a < b" "finite A"
  defines "M ≡ uniform_measure lborel {a..b}"
  shows   "emeasure (PiM A (λ_. M)) {h∈A →E UNIV. h x = h y} = 0"
proof -
  from assms have M: "prob_space M" unfolding M_def
    by (intro prob_space_uniform_measure) auto
  then interpret product_prob_space "λ_. M" A
    unfolding product_prob_space_def product_prob_space_axioms_def product_sigma_finite_def
    by (auto simp: prob_space_imp_sigma_finite)
  from M interpret pair_sigma_finite M M by unfold_locales
  have [measurable]: "{h∈extensional {x, y}. h x = h y} ∈ sets (PiM {x, y} (λi. lborel))"
  proof -
    have "{h∈extensional {x,y}. h x = h y} = {h ∈ space (PiM {x, y} (λi. lborel)). h x = h y}"
      by (auto simp: extensional_def space_PiM)
    also have "... ∈ sets (PiM {x, y} (λi. lborel))"
      by measurable
    finally show ?thesis .
  qed
  have [simp]: "sets (PiM A (λ_. M)) = sets (PiM A (λ_. lborel))" for A :: "'a set"
    by (intro sets_PiM_cong refl) (simp_all add: M_def)
  have sets_M_M: "sets (M ⨂M M) = sets (borel ⨂M borel)"
    by (intro sets_pair_measure_cong) (auto simp: M_def)
  have [measurable]: "(λ(b, a). if b = a then 1 else 0) ∈ borel_measurable (M ⨂M M)"
    unfolding measurable_split_conv
    by (subst measurable_cong_sets[OF sets_M_M refl])
       (auto intro!: measurable_If measurable_const measurable_equality_set)
      
  have "{h∈A →E UNIV. h x = h y} = 
          (λh. restrict h {x, y}) -` {h∈extensional {x, y}. h x = h y} ∩ space (PiM A (λ_. M :: real measure))"
    by (auto simp: space_PiM PiE_def extensional_def M_def)
  also have "emeasure (PiM A (λ_. M)) … = 
               emeasure (distr (PiM A (λ_. M)) (PiM {x,y} (λ_. lborel :: real measure)) 
                 (λh. restrict h {x,y})) {h∈extensional {x, y}. h x = h y}"
  proof (rule emeasure_distr [symmetric])
    have "(λh. restrict h {x, y}) ∈ PiM A (λ_. lborel) →M PiM {x, y} (λ_. lborel)"
      using assms by (intro measurable_restrict_subset) auto
    also have "… = PiM A (λ_. M) →M PiM {x, y} (λ_. lborel)"
      by (intro sets_PiM_cong measurable_cong_sets refl) (simp_all add: M_def)
    finally show "(λh. restrict h {x, y}) ∈ …" .
  next
    show "{h∈extensional {x, y}. h x = h y} ∈ sets (PiM {x, y} (λ_. lborel))" by simp
  qed
  also have "distr (PiM A (λ_. M)) (PiM {x,y} (λ_. lborel :: real measure)) (λh. restrict h {x,y}) =
               distr (PiM A (λ_. M)) (PiM {x,y} (λ_. M)) (λh. restrict h {x,y})"
    by (intro distr_cong refl sets_PiM_cong) (simp_all add: M_def)
  also from assms have "… = PiM {x, y} (λi. M)" by (intro distr_restrict [symmetric]) auto
  also have "emeasure … {h∈extensional {x, y}. h x = h y} =
    nn_integral … (λh. indicator {h∈extensional {x, y}. h x = h y} h)"
    by (intro nn_integral_indicator [symmetric]) simp_all
  also have "… = nn_integral (PiM {x, y} (λi. M)) (λh. if h x = h y then 1 else 0)"
    by (intro nn_integral_cong) (auto simp add: indicator_def space_PiM PiE_def)
  also from ‹x ≠ y› have "… = (∫+ z. (if fst z = snd z then 1 else 0) ∂(M ⨂M M))"
    by (intro product_nn_integral_pair) auto
  also have "… = (∫+ x. (∫+y. (if x = y then 1 else 0) ∂M) ∂M)"
    by (subst M.nn_integral_fst [symmetric]) simp_all
  also have "… = (∫+ x. (∫+y. indicator {x} y ∂M) ∂M)" by (simp add: indicator_def eq_commute)
  also have "… = (∫+ x. emeasure M {x} ∂M)" by (subst nn_integral_indicator) (simp_all add: M_def)
  also have "… = (∫+ x. 0 ∂M)" unfolding M_def
    by (intro nn_integral_cong_AE refl AE_uniform_measureI) auto
  also have "… = 0" by simp
  finally show ?thesis .
qed      

lemma measurable_linorder_from_keys_restrict:
  assumes fin: "finite A"
  shows "linorder_from_keys A ∈ PiM A (λ_. borel :: real measure) →M count_space (Pow (A × A))"
  (is "_ : ?M →M _")
  apply (subst measurable_count_space_eq2)
  apply (auto simp add: fin linorder_from_keys_def)
proof -
  note fin[simp]
  fix R assume "R ⊆ A × A"
  then have "linorder_from_keys A -` {R} ∩ space ?M =
    {f ∈ space ?M. ∀x∈A. ∀y∈A. (x, y) ∈ R ⟷ f x ≤ f y}"
    by (auto simp add: linorder_from_keys_def set_eq_iff)
  also have "… ∈ sets ?M"
    by measurable
  finally show "linorder_from_keys A -` {R} ∩ space ?M ∈ sets ?M" .
qed

lemma measurable_count_space_extend:
  assumes "f ∈ measurable M (count_space A)" "A ⊆ B"
  shows   "f ∈ measurable M (count_space B)"
proof -
  note assms(1)
  also have "count_space A = restrict_space (count_space B) A"
    using assms(2) by (subst restrict_count_space) (simp_all add: Int_absorb2)
  finally show ?thesis by (simp add: measurable_restrict_space2_iff)
qed
  
lemma measurable_linorder_from_keys_restrict':
  assumes fin: "finite A" "A ⊆ B"
  shows "linorder_from_keys A ∈ PiM A (λ_. borel :: real measure) →M count_space (Pow (B × B))"
  apply (rule measurable_count_space_extend)
   apply (rule measurable_linorder_from_keys_restrict[OF assms(1)])
  using assms by auto
  

context
  fixes a b :: real and A :: "'a set" and M and B
  assumes fin: "finite A" and ab: "a < b" and B: "A ⊆ B"
  defines "M ≡ distr (PiM A (λ_. uniform_measure lborel {a..b})) 
                  (count_space (Pow (B × B))) (linorder_from_keys A)"
begin

lemma measurable_linorder_from_keys [measurable]: 
  "linorder_from_keys A ∈ PiM A (λ_. borel :: real measure) →M count_space (Pow (B × B))"
  by (rule measurable_linorder_from_keys_restrict') (auto simp: fin B)

text ‹
  The ordering defined by randomly-chosen priorities is almost surely linear:
›
theorem almost_everywhere_linorder: "AE R in M. linorder_on A R"
proof -
  define N where "N = PiM A (λ_. uniform_measure lborel {a..b})"
  have [simp]: "sets (PiM A (λ_. uniform_measure lborel {a..b})) = sets (PiM A (λ_. lborel))"
    by (intro sets_PiM_cong) simp_all
  let ?M_A = "(PiM A (λ_. lborel :: real measure))"
  have meas: "{h ∈ A →E UNIV. h i = h j} ∈ sets ?M_A"
    if [simp]: "i ∈ A" "j ∈ A" for i j
  proof -
    have "{h ∈ A →E UNIV. h i = h j} = {h ∈ space ?M_A. h i = h j}"
      by (auto simp: space_PiM)
    also have "... ∈ sets ?M_A"
      by measurable
    finally show ?thesis .
  qed
  define X :: "('a ⇒ real) set" where "X = (⋃x∈A. ⋃y∈A-{x}. {h∈A →E UNIV. h x = h y})"
  have "AE f in N. inj_on f A"
  proof (rule AE_I)
    show "{f ∈ space N. ¬ inj_on f A} ⊆ X"
      by (auto simp: inj_on_def X_def space_PiM N_def)
  next
    show "X ∈ sets N" unfolding X_def N_def
      using meas by (auto intro!: countable_finite fin sets.countable_UN')
  next
    have "emeasure N X ≤ (∑i∈A. emeasure N (⋃y∈A - {i}. {h ∈ A →E UNIV. h i = h y}))"
      unfolding X_def N_def using fin meas
      by (intro emeasure_subadditive_finite) 
         (auto simp: disjoint_family_on_def intro!: sets.countable_UN' countable_finite)
    also have "… ≤ (∑i∈A. ∑j∈A-{i}. emeasure N {h ∈ A →E UNIV. h i = h j})"
      unfolding N_def using fin meas
      by (intro emeasure_subadditive_finite sum_mono) 
         (auto simp: disjoint_family_on_def intro!: sets.countable_UN' countable_finite)
    also have "… = (∑i∈A. ∑j∈A-{i}. 0)" unfolding N_def using fin ab
      by (intro sum.cong refl emeasure_PiM_diagonal) auto
    also have "… = 0" by simp
    finally show "emeasure N X = 0" by simp
  qed
  hence "AE f in N. linorder_on A (linorder_from_keys A f)"
    by eventually_elim auto
  thus ?thesis unfolding M_def N_def
    by (subst AE_distr_iff) auto
qed

text ‹
  Furthermore, this is equivalent to choosing one of the $|A|!$ linear orderings uniformly
  at random.
›
theorem random_linorder_by_prios:
  "M = uniform_measure (count_space (Pow (B × B))) (linorders_on A)"
proof -
  from linorders_finite_nonempty[OF fin] obtain R where R: "linorder_on A R"
    by (auto simp: linorders_on_def)
  
  have *: "emeasure M {R} ≤ emeasure M {R'}" if "linorder_on A R" "linorder_on A R'" for R R'
  proof -
    define N where "N = PiM A (λ_. uniform_measure lborel {a..b})"
    from linorder_permutation_exists[OF fin that]
    obtain π where π: "π permutes A" "R' = map_relation A π R"
      by blast
    have "(λf. f ∘ π) ∈ PiM A (λ_. lborel :: real measure) →M PiM A (λ_. lborel :: real measure)"
      by (auto intro!: measurable_PiM_single' measurable_PiM_component_rev
          simp: comp_def permutes_in_image[OF π(1)] space_PiM PiE_def extensional_def)
    also have "… = N →M PiM A (λ_. lborel)"
      unfolding N_def by (intro measurable_cong_sets refl sets_PiM_cong) simp_all
    finally have [measurable]: "(λf. f ∘ π) ∈ …" .    
        
    have [simp]: "measurable N X = measurable (PiM A (λ_. lborel)) X" for X :: "('a × 'a) set measure"
      unfolding N_def by (intro measurable_cong_sets refl sets_PiM_cong) simp_all
    have [simp]: "measurable M X = measurable (count_space (Pow (B × B))) X" for X :: "('a × 'a) set measure"
      unfolding M_def by simp
      
    have M_eq: "M = distr N (count_space (Pow (B × B))) (linorder_from_keys A)"
      by (simp only: M_def N_def)
    also have "N = distr N (PiM A (λ_. lborel)) (λf. f ∘ π)"
      unfolding N_def by (rule PiM_uniform_measure_permute [symmetric]) fact+
    also have "distr … (count_space (Pow (B × B))) (linorder_from_keys A) = 
                 distr N (count_space (Pow (B × B))) (linorder_from_keys A ∘ (λf. f ∘ π)) "
      by (intro distr_distr) simp_all
    also have "… = distr N (count_space (Pow (B × B))) (map_relation A π ∘ linorder_from_keys A)"
      by (intro distr_cong refl) (auto simp: linorder_from_keys_permute[OF π(1)])
    also have "… = distr M (count_space (Pow (B × B))) (map_relation A π)"
      unfolding M_eq using B
      by (intro distr_distr [symmetric]) (auto simp: map_relation_def)
    finally have M_eq': "distr M (count_space (Pow (B × B))) (map_relation A π) = M" ..

    from that have subset': "R ⊆ B × B" "R' ⊆ B × B"
      using B by (auto simp: linorder_on_def refl_on_def)
    hence "emeasure M {R} ≤ emeasure M (map_relation A π -` {R'} ∩ space M)"
      using subset' by (intro emeasure_mono) (auto simp: M_def π )
    also have "… = emeasure (distr M (count_space (Pow (B × B))) (map_relation A π)) {R'} "
      by (rule emeasure_distr [symmetric]) (insert subset' B, auto simp: map_relation_def)
    also note M_eq'
    finally show ?thesis .
  qed
  have same_prob: "emeasure M {R'} = emeasure M {R}" if "linorder_on A R'" for R'
    using *[of R R'] and *[of R' R] and R and that by simp
  
  from ab have "prob_space M"
    unfolding M_def
    by (intro prob_space.prob_space_distr prob_space_PiM prob_space_uniform_measure) simp_all
  hence "1 = emeasure M (Pow (B × B))" 
    using prob_space.emeasure_space_1[OF ‹prob_space M›] by (simp add: M_def)
  also have "(Pow (B × B)) = linorders_on A ∪ ((Pow (B × B))-linorders_on A)"
    using B by (auto simp: linorders_on_def linorder_on_def refl_on_def)
  also have "emeasure M … = emeasure M (linorders_on A) + emeasure M (Pow (B × B)-linorders_on A)"
    using B by (subst plus_emeasure) (auto simp: M_def linorders_on_def linorder_on_def refl_on_def)
  also have "emeasure M (Pow (B × B)-linorders_on A) = 0" using almost_everywhere_linorder 
    by (subst (asm) AE_iff_measurable) (auto simp: linorders_on_def M_def)
  also from fin have "emeasure M (linorders_on A) = (∑R'∈linorders_on A. emeasure M {R'})"
    using B by (intro emeasure_eq_sum_singleton) 
               (auto simp: M_def  linorders_on_def linorder_on_def refl_on_def)
  also have "… = (∑R'∈linorders_on A. emeasure M {R})"
    by (rule sum.cong) (simp_all add: linorders_on_def same_prob)
  also from fin have "… = fact (card A) * emeasure M {R}"
    by (simp add: linorders_on_def card_finite_linorders)
  finally have [simp]: "emeasure M {R} = inverse (fact (card A))"
    by (simp add: inverse_ennreal_unique)
  
  show ?thesis
  proof (rule measure_eqI_countable_AE')
    show "sets M = Pow (Pow (B × B))"
      by (simp add: M_def)
  next
    from ‹finite A› show "countable (linorders_on A)"
      by (blast intro: countable_finite)
  next
    show "AE R in uniform_measure (count_space (Pow (B × B))) 
            (linorders_on A). R ∈ linorders_on A"
      by (rule AE_uniform_measureI) 
         (insert B, auto simp: linorders_on_def linorder_on_def refl_on_def)
  next
    fix R' assume R': "R' ∈ linorders_on A"
    have subset: "linorders_on A ⊆ Pow (B × B)"
      using B by (auto simp: linorders_on_def linorder_on_def refl_on_def)
    have "emeasure (uniform_measure (count_space (Pow (B × B))) 
           (linorders_on A)) {R'} = emeasure (count_space (Pow (B × B))) (linorders_on A ∩ {R'}) /
                                      emeasure (count_space (Pow (B × B))) (linorders_on A)"
      using R' B by (subst emeasure_uniform_measure) (auto simp: linorders_on_def linorder_on_def refl_on_def)
    also have "… = 1 / emeasure (count_space (Pow (B × B))) (linorders_on A)"
      using R' B by (subst emeasure_count_space) (auto simp: linorders_on_def linorder_on_def refl_on_def)
    also have "… = 1 / fact (card A)"
      using fin finite_linorders_on[of A]
      by (subst emeasure_count_space [OF subset])
         (auto simp: divide_ennreal [symmetric] linorders_on_def card_finite_linorders)
    also have "… = emeasure M {R}"
      by (simp add: field_simps divide_ennreal_def)
    also have "… = emeasure M {R'}"
      using R' by (intro same_prob [symmetric]) (auto simp: linorders_on_def)
    finally show "emeasure M {R'} = emeasure (uniform_measure (count_space (Pow (B × B))) 
                    (linorders_on A)) {R'}" ..
  next
    show "linorders_on A ⊆ Pow (B × B)"
      using B by (auto simp: linorders_on_def linorder_on_def refl_on_def)
  qed (auto simp: M_def linorders_on_def almost_everywhere_linorder)
qed

end
end