Theory Cond_Prob_Extensions

(* Theory: Cond_Prob_Extensions
   Author: Chelsea Edmonds *)

section ‹Conditional Probability Library Extensions ›

theory Cond_Prob_Extensions 
  imports 
    Prob_Events_Extras  
    Design_Theory.Multisets_Extras
begin

subsection ‹Miscellaneous Set and List Lemmas ›

lemma nth_image_tl: 
  assumes "xs  []"
  shows "nth xs ` {1..<length xs} = set(tl xs)"
proof -
  have "set (tl xs) = {(tl xs)!i | i. i < length (tl xs)}"
    using set_conv_nth by metis 
  then have "set (tl xs) = {xs! (Suc i) | i. i  < length xs - 1}"
    using nth_tl by fastforce 
  then have "set (tl xs) = {xs ! j | j. j > 0  j < length xs}"
    by (smt (verit, best) Collect_cong Suc_diff_1 Suc_less_eq assms length_greater_0_conv zero_less_Suc)
  thus ?thesis by auto
qed

lemma exists_list_card: 
  assumes "finite S"
  obtains xs where "set xs = S" and "length xs = card S"
  by (metis assms distinct_card finite_distinct_list)

lemma bij_betw_inter_empty: (* this is the only lemma needing the Multisets_Extras theory *)
  assumes "bij_betw f A B"
  assumes "A'  A"
  assumes "A''  A"
  assumes "A'  A'' = {}"
  shows "f ` A'  f ` A'' = {}"
  by (metis assms(1) assms(2) assms(3) assms(4) bij_betw_inter_subsets image_empty)


lemma bij_betw_image_comp_eq: 
  assumes "bij_betw g T S"
  shows "(F  g) ` T = F ` S"
  using assms bij_betw_imp_surj_on by (metis image_comp) 

lemma prod_card_image_set_eq: 
  assumes "bij_betw f {0..<card S} S"
  assumes "finite S"
  shows "(i  {n..<(card S)} . g (f i)) = (i  f ` {n..<card S} . g i)"
proof (cases "n  card S")
  case True
  then show ?thesis by simp
next
  case False
  then show ?thesis using assms 
  proof (induct "card S" arbitrary: S)
    case 0
    then show ?case by auto
  next
    case (Suc x)
    then have nlt: "n < Suc x" by simp
    then have split: "{n..<Suc x} = {n..<x}  {x}" by auto
    then have "f ` {n..<Suc x} = f ` ({n..< x}  {x})" by simp
    then have fsplit: "f ` {n..<Suc x} = f ` {n..< x}  {f x}"
      by simp 
    have "{n..<x}  {0..<card S}"
      using Suc(2)  by auto 
    moreover have "{x}  {0..<card S}" using Suc(2) by auto
    moreover have "{n..< x}  {x} = {}" by auto
    ultimately have finter: "f ` {n..< x}  {f x} = {}" using Suc.prems(2) Suc.prems(1) 
       bij_betw_inter_empty[of f "{0..<card S}" S "{n..< x}" "{x}"] by auto
    have "(i = n..<Suc x. g (f i)) = (i = n..<x. g (f i)) * g (f( x))" using nlt by simp
    moreover have "(xf ` {n..<Suc x}. g x) = (if ` {n..< x}. g i) * g (f x)" using finter fsplit
      by (simp add: Groups.mult_ac(2))
    moreover have "(if ` {n..< x}. g i) = (i = n..<x. g (f i))"
    proof -
      let ?S' = "f ` {0..<x}"
      have "{0..<x}  {0..<card S}" using Suc(2) by auto
      then have bij: "bij_betw f {0..<x} ?S'" using Suc.prems(2)
        using bij_betw_subset by blast 
      moreover have "card ?S' = x" using bij_betw_same_card[of f "{0..<x}" ?S'] bij by auto
      moreover have "finite ?S'" using finite_subset by auto 
      ultimately show ?thesis
        by (metis bij_betw_subset ivl_subset less_eq_nat.simps(1) order_refl prod.reindex_bij_betw)  
    qed 
    ultimately show ?case using Suc(2) by auto
  qed
qed

lemma set_take_distinct_elem_not: 
  assumes "distinct xs"
  assumes "i < length xs"
  shows "xs ! i  set (take i xs)"
  by (metis assms(1) assms(2) distinct_take id_take_nth_drop not_distinct_conv_prefix)

subsection ‹ Conditional Probability Basics ›
context prob_space
begin

text ‹Abbreviation to mirror mathematical notations ›

abbreviation cond_prob_ev :: "'a set  'a set  real" ("𝒫'(_ | _')")  where 
"𝒫(B | A)   𝒫(x in M. (x  B) ¦ (x  A))"

lemma cond_prob_inter: "𝒫(B | A) = 𝒫(ω in M. (ω  B  A)) / 𝒫(ω in M. (ω  A))"
  using cond_prob_def by auto

lemma cond_prob_ev_def: 
  assumes "A  events" "B  events"
  shows "𝒫(B | A) = prob (A  B) / prob A"
proof -
  have a: "𝒫(B | A) = 𝒫(ω in M. (ω  B  A)) / 𝒫(ω in M. (ω  A))"
    using cond_prob_inter by auto
  also have "... = prob {w  space M . w  B  A} / prob {w  space M . w  A}"
    by auto
  finally show ?thesis using assms
    by (simp add: Collect_conj_eq a inf_commute)
qed

lemma measurable_in_ev:
  assumes "A  events"
  shows "Measurable.pred M (λ x . x  A)"
  using assms by auto

lemma measure_uniform_measure_eq_cond_prob_ev:
  assumes "A  events" "B  events"
  shows "𝒫(A | B) =𝒫(x in uniform_measure M {xspace M. x  B}. x  A)"
  using assms measurable_in_ev measure_uniform_measure_eq_cond_prob by auto

lemma measure_uniform_measure_eq_cond_prob_ev2:
  assumes "A  events" "B  events"
  shows "𝒫(A | B) = measure (uniform_measure M {xspace M. x  B}) A"
  using measure_uniform_measure_eq_cond_prob_ev assms
  by (metis Int_def sets.Int_space_eq1 space_uniform_measure) 

lemma measure_uniform_measure_eq_cond_prob_ev3:
  assumes "A  events" "B  events"
  shows "𝒫(A | B) = measure (uniform_measure M B) A"
  using measure_uniform_measure_eq_cond_prob_ev assms  Int_def sets.Int_space_eq1 space_uniform_measure
  by metis (* Slow *)

lemma prob_space_cond_prob_uniform:
  assumes "prob ({xspace M. Q x}) > 0"
  shows "prob_space (uniform_measure M {xspace M. Q x})"
  using assms by (intro prob_space_uniform_measure) (simp_all add: emeasure_eq_measure)

lemma prob_space_cond_prob_event:
  assumes "prob B > 0"
  shows "prob_space (uniform_measure M B)"
  using assms by (intro prob_space_uniform_measure) (simp_all add: emeasure_eq_measure)

text‹Note this case shouldn't be used. Conditional probability should have > 0 assumption›
lemma cond_prob_empty: "𝒫(B | {}) = 0" 
  using cond_prob_inter[of B "{}"] by auto

lemma cond_prob_space:  "𝒫(A | space M) = 𝒫(w in M . w  A)"
proof -
  have p1: "prob {ω  space M. ω  space M} = 1"
    by (simp add: prob_space) 
  have " w. w  space M  w  A  (space M)  w  A" by auto
  then have "prob {ω  space M. ω  A  space M} = 𝒫(w in M . w  A)"
    by meson 
  then show ?thesis using cond_prob_inter[of  A "space M"] p1 by auto
qed

lemma cond_prob_space_ev: assumes "A  events" shows "𝒫(A | space M) = prob A"
  using cond_prob_space assms
  by (metis Int_commute Int_def measure_space_inter sets.top) 

lemma cond_prob_UNIV: "𝒫(A | UNIV) = 𝒫(w in M . w  A)"
proof -
  have p1: "prob {ω  space M. ω  UNIV} = 1"
    by (simp add: prob_space) 
  have " w. w  space M  w  A  UNIV  w  A" by auto
  then have "prob {ω  space M. ω  A  UNIV} = 𝒫(w in M . w  A)"
    by meson 
  then show ?thesis using cond_prob_inter[of A UNIV] p1 by auto
qed

lemma cond_prob_UNIV_ev: "A  events  𝒫(A | UNIV) = prob A"
  using cond_prob_UNIV 
  by (metis Int_commute Int_def measure_space_inter sets.top)

lemma cond_prob_neg: 
  assumes "A  events" "B  events"
  assumes "prob A >0"
  shows "𝒫((space M - B) | A) = 1 - 𝒫(B | A)"
proof -
  have negB: "space M - B  events" using assms by auto 
  have "prob ((space M - B)  A) = prob A - prob (B  A)"
    by (simp add: Diff_Int_distrib2 assms(1) assms(2) finite_measure_Diff sets.Int)
  then have "𝒫((space M - B) | A) = (prob A - prob (B  A))/prob A" 
    using cond_prob_ev_def[of A "space M - B"] assms negB by (simp add: Int_commute) 
  also have "... = ((prob A)/prob A) - ((prob (B  A))/prob A)" by (simp add: field_simps)
  also have "... = 1 - ((prob (B  A))/prob A)" using assms(3) by (simp add: field_simps)
  finally show "𝒫((space M - B) | A) = 1 - 𝒫(B | A)" using cond_prob_ev_def[of A B] assms
    by (simp add: inf_commute) 
qed

subsection ‹Bayes Theorem ›


lemma prob_intersect_A: 
  assumes "A  events" "B  events"
  shows "prob (A  B) = prob A * 𝒫(B | A)"
  using cond_prob_ev_def assms apply simp
  by (metis Int_lower1 finite_measure_mono measure_le_0_iff)

lemma prob_intersect_B: 
  assumes "A  events" "B  events"
  shows "prob (A  B) = prob B * 𝒫(A | B)"
  using cond_prob_ev_def assms 
  by (simp_all add: inf_commute)(metis Int_lower2 finite_measure_mono measure_le_0_iff)

theorem Bayes_theorem: 
  assumes "A  events" "B  events"
  shows "prob B * 𝒫(A | B) = prob A * 𝒫(B |A)" 
  using prob_intersect_A prob_intersect_B assms by simp

corollary Bayes_theorem_div: 
  assumes "A  events" "B  events"
  shows "𝒫(A | B) = (prob A * 𝒫(B |A))/(prob B)"
  using assms Bayes_theorem
  by (metis cond_prob_ev_def prob_intersect_A) 

lemma cond_prob_dual_intersect: 
  assumes "A  events" "B  events" "C  events"
  assumes "prob C  0"
  shows "𝒫(A | (B  C)) = 𝒫(A  B | C)/ 𝒫(B | C)" (is "?LHS = ?RHS")
proof - 
  have "B  C  events" using assms by auto
  then have lhs: "?LHS = prob (A  B  C)/prob (B  C)" 
    using assms cond_prob_ev_def[of "B  C" "A"] inf_commute inf_left_commute  by (metis)
  have "A  B  events" using assms by auto
  then have "𝒫(A  B | C) = prob (A  B  C) / prob C" 
    using assms cond_prob_ev_def[of "C" "A  B"] inf_commute by (metis)
  moreover have "𝒫(B | C) = prob (B  C)/prob C" using cond_prob_ev_def[of "C" "B"] assms inf_commute by metis
  ultimately have "?RHS = (prob (A  B  C) / prob C)/( prob (B  C)/prob C)"
    by simp
  also have "... = (prob (A  B  C) / prob C)*( prob (C)/prob (B  C))" by simp
  also have "... = prob (A  B  C)/prob (B C)" using assms(4) by simp
  finally show ?thesis using lhs by simp
qed


lemma cond_prob_ev_double: 
  assumes "A  events" "B  events" "C  events"
  assumes "prob C > 0"
  shows "𝒫(x in (uniform_measure M C). (x  A) ¦ (x  B)) =  𝒫(A | (B  C))"
proof - 
  let ?M = "uniform_measure M C"
  interpret cps: prob_space "?M" using assms(4) prob_space_cond_prob_event by auto
  have probne: "prob C  0" using assms(4) by auto
  have ev: "cps.events = events" using sets_uniform_measure by auto
  have iev: "A  B  events" using assms(1) assms(2) by simp
  have 0: "𝒫(x in (uniform_measure M C). (x  A) ¦ (x  B)) = cps.cond_prob_ev A B" by simp
  also have 1: "... = (measure ?M (A  B))/(measure ?M B)" using cond_prob_ev_def assms(1) assms(2) ev
    by (metis Int_commute cps.cond_prob_ev_def)
  also have 2: "... = 𝒫((A  B) | C)/(measure ?M B)" 
    using measure_uniform_measure_eq_cond_prob_ev3[of "A  B" "C"] assms(3) iev by auto
  also have 3: "... = 𝒫((A  B) | C)/ 𝒫(B | C)" using measure_uniform_measure_eq_cond_prob_ev3[of "B" "C"] assms(3) assms(2) by auto
  also have 4: "... = 𝒫(A | (B  C))" 
    using cond_prob_dual_intersect[of "A" "B" "C"] assms(1) assms(2) assms(3) probne by presburger 
  finally show ?thesis using 1 2 3 4 by presburger
qed

lemma cond_prob_inter_set_lt: 
  assumes "A  events" "B  events" "AS  events"
  assumes "finite AS"
  shows "𝒫((A  (AS)) | B)  𝒫(A|B)" (is "?LHS  ?RHS")
using measure_uniform_measure_eq_cond_prob_ev finite_measure_mono 
proof (cases "AS = {}")
  case True
  then have "(A  (AS)) = A" by simp
  then show ?thesis by simp
next
  case False
  then have "(AS)  events" using assms(3) assms(4) Inter_event_ss by simp
  then have "(A  (AS))  events" using assms by simp
  then have "?LHS = prob (A  (AS)  B)/prob B" 
    using assms cond_prob_ev_def[of "B" "(A  (AS))"] inf_commute by metis
  moreover have "prob (A  (AS)  B)  prob (A  B)" using finite_measure_mono
    assms(1) inf_commute inf_left_commute by (metis assms(2) inf_sup_ord(1) sets.Int) 
  ultimately show ?thesis using cond_prob_ev_def[of "B" "A"]
    by (simp add: assms(1) assms(2) divide_right_mono inf_commute) 
qed

subsection ‹Conditional Probability Multiplication Rule ›
text ‹Many list and indexed variations of this lemma ›

lemma prob_cond_Inter_List:  
  assumes "xs  []"
  assumes " A. A  set xs  A  events"
  shows "prob ((set xs)) = prob (hd xs) * (i = 1..<(length xs) . 
    𝒫((xs ! i) | ((set (take i xs )))))"
  using assms(1) assms(2) 
proof (induct xs rule: rev_nonempty_induct)
  case (single x)
  then show ?case by auto
next
  case (snoc x xs)
  have "xs  []"
    by (simp add: snoc.hyps(1)) 
  then have inev: "((set xs))  events" using events_inter
    by (simp add: snoc.prems) 
  have len: "(length (xs @ [x])) = length xs + 1" by auto
  have last_p: "𝒫(x | ((set xs))) = 
    𝒫((xs @ [x]) ! length xs |  (set (take (length xs) (xs @ [x]))))"
    by auto
  have "prob ( (set (xs @ [x]))) = prob (x  ((set xs)))"
    by auto
  also have "... = prob ((set xs)) * 𝒫(x | ((set xs)))" 
    using prob_intersect_B snoc.prems inev by simp 
  also have "... = prob (hd xs) * (i = 1..<length xs. 𝒫(xs ! i |  (set (take i xs)))) * 
      𝒫(x | ((set xs)))"
    using snoc.hyps snoc.prems by auto
  finally have "prob ( (set (xs @ [x]))) = prob (hd (xs @[x])) * 
      (i = 1..<length xs. 𝒫((xs @ [x]) ! i |  (set (take i (xs @ [x]))))) *  𝒫(x | ((set xs)))" 
    using nth_append[of xs "[x]"] nth_take by (simp add: snoc.hyps(1)) 
  then show ?case using last_p by auto
qed

lemma prob_cond_Inter_index:  
  fixes n :: nat
  assumes "n > 0"
  assumes "F ` {0..<n}  events"
  shows "prob ( (F `{0..<n} )) = prob (F 0) * (i  {1..<n} . 
    𝒫(F i | ( (F`{0..<i}))))"
proof -
  define xs where "xs  map F [0..<n]"
  have "prob ((set xs)) = prob (hd xs) * (i = 1..<(length xs) . 
    𝒫((xs ! i) | ((set (take i xs )))))" using xs_def assms prob_cond_Inter_List[of xs] by auto
  then have "prob ((set xs)) = prob (hd xs) * (i  {1..<n} . 𝒫((xs ! i) | ((set (take i xs )))))" 
    using xs_def by auto
  moreover have "hd xs = F 0" 
    unfolding xs_def by (simp add: assms(1) hd_map) 
  moreover have " i. i  {1..<n}  F ` {0..<i} = set (take i xs )"
    by (metis atLeastLessThan_iff atLeastLessThan_upt image_set less_or_eq_imp_le plus_nat.add_0 
        take_map take_upt xs_def)
  ultimately show ?thesis using xs_def by auto
qed

lemma prob_cond_Inter_index_compl: 
  fixes n :: nat
  assumes "n > 0"
  assumes "F ` {0..<n}  events"
  shows "prob ( x  {0..<n} . space M - F x) = prob (space M - F 0) * (i  {1..<n} . 
    𝒫(space M - F i | ( j {0..<i}. space M - F j)))"
proof -
  define G where "G  λ i. space M - F i"
  then have "G ` {0..<n}  events" using assms(2) by auto
  then show ?thesis using prob_cond_Inter_index[of n G] G_def
    using assms(1) by blast  
qed


lemma prob_cond_Inter_take_cond:
  assumes "xs  []"
  assumes "set xs  events"
  assumes "S  events"
  assumes "S  {}"
  assumes "finite S"
  assumes "prob (S) > 0"
  shows "𝒫(((set xs)) | ( S)) = (i = 0..<(length xs) .  𝒫((xs ! i) | ((set (take i xs )  S))))"
proof -
  define M' where "M' = uniform_measure M (S)"
  interpret cps: prob_space M' using prob_space_cond_prob_event M'_def assms(6) by auto
  have len: "length xs > 0" using assms(1) by simp
  have cps_ev: "cps.events = events" using sets_uniform_measure M'_def by auto
  have sevents: "S  events" using assms(3) assms(4) Inter_event_ss assms(5) by auto
  have fin: "finite (set xs)" by auto
  then have xevents: "(set xs)  events" using assms(1) assms(2) Inter_event_ss by blast
  then have peq: "𝒫(((set xs)) | ( S)) = cps.prob ( (set xs))" 
    using measure_uniform_measure_eq_cond_prob_ev3[of "(set xs)" "S"] sevents M'_def
    by blast
  then have "cps.prob ( (set xs)) = cps.prob (hd xs) * (i = 1..<(length xs) . 
    cps.cond_prob_ev (xs ! i) ((set (take i xs ))))" using assms cps.prob_cond_Inter_List cps_ev 
    by blast
  moreover have "cps.prob (hd xs) = 𝒫((xs ! 0) | ((set (take 0 xs )  S)))"
  proof -
    have ev: "hd xs  events" using assms(2) len by auto
    then have "cps.prob (hd xs) = 𝒫(hd xs | S)" 
      using ev sevents measure_uniform_measure_eq_cond_prob_ev3[of "hd xs" "S"] M'_def by presburger
    then show ?thesis using len by (simp add: hd_conv_nth)
  qed
  moreover have "i. i > 0  i < length xs  
    cps.cond_prob_ev (xs ! i) ((set (take i xs ))) = 𝒫((xs ! i) | ((set (take i xs )  S)))"
  proof -
    fix i assume igt: "i > 0" and ilt: "i <length xs"
    then have "set (take i xs)  events" using assms(2)
      by (meson set_take_subset subset_trans) 
    moreover have "set (take i xs)  {}" using len igt ilt by auto
    ultimately have "((set (take i xs )))  events"
      using Inter_event_ss fin by auto
    moreover have "xs ! i  events" using assms(2)
      using nth_mem subset_iff igt ilt by blast
    moreover have "((set (take i xs )  S)) = ((set (take i xs )))  (S)"
      by (simp add: Inf_union_distrib) 
    ultimately show "cps.cond_prob_ev (xs ! i) ((set (take i xs ))) = 𝒫((xs ! i) | ((set (take i xs )  S)))"
      using sevents cond_prob_ev_double[of "xs ! i" "((set (take i xs )))" "S"] assms(6) M'_def by presburger 
  qed
  ultimately have eq: "cps.prob ( (set xs)) = 𝒫((xs ! 0) | ((set (take 0 xs )  S))) * (i  {1..<(length xs)} . 
    𝒫((xs ! i) | ((set (take i xs )  S))))" by simp
  moreover have "{1..<length xs} = {0..<length xs} - {0}"
    by (simp add: atLeast1_lessThan_eq_remove0 lessThan_atLeast0)
  moreover have "finite {0..<length xs}" by auto
  moreover have "0  {0..<length xs}"by (simp add: assms(1)) 
  ultimately have "𝒫((xs ! 0) | ((set (take 0 xs )  S))) * (i  {1..<(length xs)} . 
    𝒫((xs ! i) | ((set (take i xs )  S)))) = (i  {0..<(length xs)} . 
    𝒫((xs ! i) | ((set (take i xs )  S))))" using prod.remove[of "{0..<length xs}" "0" "λ i. 𝒫((xs ! i) | ((set (take i xs )  S)))"]
    by presburger
  then have "cps.prob ( (set xs)) = (i  {0..<(length xs)} . 
    𝒫((xs ! i) | ((set (take i xs )  S))))" using eq by simp
  then show ?thesis using peq by auto
qed

lemma prob_cond_Inter_index_cond_set:
  fixes n :: nat
  assumes "n > 0"
  assumes "finite E"
  assumes "E  {}"
  assumes "E  events"
  assumes "F ` {0..<n}  events"
  assumes "prob (E) > 0"
  shows "𝒫(((F ` {0..<n})) | (E)) = (i  {0..<n}.  𝒫(F i | (((F ` {0..<i})  E))))"
proof -
  define M' where "M' = uniform_measure M (E)"
  interpret cps: prob_space M' using prob_space_cond_prob_event M'_def assms(6) by auto
  have cps_ev: "cps.events = events" using sets_uniform_measure M'_def by auto
  have sevents: "((E))  events" using assms(6) assms(2) assms(3) assms(4) Inter_event_ss by auto
  have fin: "finite (F ` {0..<n})" by auto
  then have xevents: "(F ` {0..<n})  events" using assms Inter_event_ss by auto
  then have peq: "𝒫(((F ` {0..<n})) | ( E)) = cps.prob ( (F ` {0..<n}))" 
    using measure_uniform_measure_eq_cond_prob_ev3[of "(F ` {0..<n})" "E"] sevents M'_def
    by blast
  moreover have "F `{0..<n}  cps.events" using cps_ev assms(5) by force 
  ultimately have "cps.prob ( (F ` {0..<n})) = cps.prob (F 0) * (i = 1..<n . 
    cps.cond_prob_ev (F i) ((F ` {0..<i})))" 
    using assms(1) cps.prob_cond_Inter_index[of n F] by blast
  moreover have "cps.prob (F 0) = 𝒫((F 0) | (E))"
  proof -
    have ev: "F 0  events" using assms(1) assms(5) by auto
    then show ?thesis 
      using ev sevents measure_uniform_measure_eq_cond_prob_ev3[of "F 0" "E"] M'_def by presburger
  qed
  moreover have "i. i > 0  i < n  
    cps.cond_prob_ev (F i) ((F ` {0..<i})) = 𝒫((F i) | (((F ` {0..<i})  E)))"
  proof -
    fix i assume igt: "i > 0" and ilt: "i <n"
    then have "((F ` {0..<i}))  events"
      using assms subset_trans igt Inter_event_ss fin by auto
    moreover have "F i  events" using assms 
      using subset_iff igt ilt by simp
    moreover have "(((F ` {0..<i})  (E))) = (((F ` {0..<i})))  ((E))"
      by (simp add: Inf_union_distrib) 
    ultimately show "cps.cond_prob_ev (F i) ((F ` {0..<i})) = 𝒫((F i) | (((F ` {0..<i})  E)))"
      using sevents cond_prob_ev_double[of "F i" "(((F ` {0..<i})))" "E"] assms M'_def by presburger 
  qed
  ultimately have eq: "cps.prob ( (F ` {0..<n})) = 𝒫((F 0) | (E)) * (i  {1..<n} . 
    𝒫((F i) | (((F ` {0..<i})  E))))" by simp
  moreover have "{1..<n} = {0..<n} - {0}"
    by (simp add: atLeast1_lessThan_eq_remove0 lessThan_atLeast0)
  ultimately have "𝒫((F 0) | (E)) * (i  {1..<n} .  𝒫((F i) | (((F ` {0..<i})  E)))) = 
      (i  {0..<n} . 𝒫((F i) | (((F ` {0..<i})  E))))" using assms(1) 
    prod.remove[of "{0..<n}" "0" "λ i. 𝒫((F i) | (((F `{0..<i})  E)))"] by fastforce
  then show ?thesis using peq eq by auto
qed

lemma prob_cond_Inter_index_cond_compl_set:
  fixes n :: nat
  assumes "n > 0"
  assumes "finite E"
  assumes "E  {}"
  assumes "E  events"
  assumes "F ` {0..<n}  events"
  assumes "prob (E) > 0"
  shows "𝒫((((-) (space M) ` F ` {0..<n})) | (E)) = 
    (i = 0..<n .  𝒫((space M - F i) | (((-) (space M) ` F ` {0..<i}  E))))"
proof -
  define G where "G  λ i. (space M - F i)"
  then have "G ` {0..<n}  events" using assms(5) by auto
  then have "𝒫(((G ` {0..<n})) | (E)) = (i  {0..<n}.  𝒫(G i | (((G ` {0..<i})  E))))"
    using prob_cond_Inter_index_cond_set[of n E G] assms by blast
  moreover have "((-) (space M) ` F ` {0..<n}) = (G ` {0..<n})"  unfolding G_def by auto
  moreover have " i. i  {0..<n}  𝒫((space M - F i) | (((-) (space M) ` F ` {0..<i}  E))) = 
    𝒫(G i | (((G ` {0..<i})  E)))" 
  proof -
    fix i assume iin: "i  {0..<n}"
    have "(-) (space M) ` F ` {0..<i} =  G ` {0..<i}" unfolding G_def using iin by auto
    then show "𝒫((space M - F i) | (((-) (space M) ` F ` {0..<i}  E))) = 
    𝒫(G i | (((G ` {0..<i})  E)))" unfolding G_def by auto
  qed
  ultimately show ?thesis  by auto
qed

lemma prob_cond_Inter_index_cond:
  fixes n :: nat
  assumes "n > 0"
  assumes "n < m"
  assumes "F ` {0..<m}  events"
  assumes "prob (j  {n..<m}. F j) > 0"
  shows "𝒫(((F ` {0..<n})) | (j {n..<m} . F j)) = (i  {0..<n}.  𝒫(F i | (((F ` {0..<i})  (F ` {n..<m})))))"
proof -
  let ?E = "F ` {n..<m}"
  have "F ` {0..<n}  events" using assms(2) assms(3) by auto
  moreover have "?E  events" using assms(2) assms(3) by auto
  moreover have "prob(?E) > 0" using assms(4) by simp
  moreover have "?E  {}" using assms(2) by simp
  ultimately show ?thesis using prob_cond_Inter_index_cond_set[of n "?E" F] assms(1) by blast
qed


lemma prob_cond_Inter_index_cond_compl:
  fixes n :: nat
  assumes "n > 0"
  assumes "n < m"
  assumes "F ` {0..<m}  events"
  assumes "prob (j  {n..<m}. F j) > 0"
  shows "𝒫((((-) (space M) ` F ` {0..<n})) | (( F ` {n..<m}))) = 
    (i = 0..<n .  𝒫((space M - F i) | (((-) (space M) ` F ` {0..<i}  (F ` {n..<m})))))"
proof -
  define G where "G  λ i. if (i < n) then (space M - F i) else F i"
  then have "G ` {0..<m}  events" using assms(3) by auto
  moreover have "prob (j  {n..<m}. G j) > 0" using G_def assms(4) by simp
  ultimately have "𝒫(((G ` {0..<n})) | (( G ` {n..<m}))) = (i  {0..<n}.  𝒫(G i | (((G ` {0..<i})  (G ` {n..<m})))))"
    using prob_cond_Inter_index_cond[of n m G] assms(1) assms(2) by blast
  moreover have "((-) (space M) ` F ` {0..<n}) = (G ` {0..<n})"  unfolding G_def by auto
  moreover have meq: "( F ` {n..<m}) = ( G ` {n..<m})" unfolding G_def by auto
  moreover have " i. i  {0..<n}  𝒫((space M - F i) | (((-) (space M) ` F ` {0..<i}  (F ` {n..<m})))) = 
    𝒫(G i | (((G ` {0..<i})  (G ` {n..<m}))))" 
  proof -
    fix i assume iin: "i  {0..<n}"
    then have "(space M - F i) = G i" unfolding G_def by auto
    moreover have "(-) (space M) ` F ` {0..<i} =  G ` {0..<i}" unfolding G_def using iin by auto
    ultimately show "𝒫((space M - F i) | (((-) (space M) ` F ` {0..<i}  (F ` {n..<m})))) = 
    𝒫(G i | (((G ` {0..<i})  (G ` {n..<m}))))" using meq by auto
  qed
  ultimately show ?thesis  by auto
qed

lemma prob_cond_Inter_take_cond_neg:
  assumes "xs  []"
  assumes "set xs  events"
  assumes "S  events"
  assumes "S  {}"
  assumes "finite S"
  assumes "prob (S) > 0"
  shows "𝒫((((-) (space M) ` (set xs))) | ( S)) = 
    (i = 0..<(length xs) .  𝒫((space M - xs ! i) | (((-) (space M) ` (set (take i xs ))  S))))"
proof -
  define ys where "ys = map ((-) (space M)) xs"
  have set: "((-) (space M) ` (set xs)) = set (ys)"
    using ys_def by simp
  then have "set ys  events"
    by (metis assms(2) image_subset_iff sets.compl_sets subsetD)
  moreover have "ys  []" using ys_def assms(1) by simp
  ultimately have "𝒫((set ys) | (S)) = 
      (i = 0..<(length ys) .  𝒫((ys ! i) | ((set (take i ys )  S))))"
    using prob_cond_Inter_take_cond assms by auto
  moreover have len: "length ys = length xs" using ys_def by auto
  moreover have "i. i < length xs  ys ! i = space M - xs ! i" using ys_def nth_map len by auto
  moreover have "i. i < length xs  set (take i ys) = (-) (space M) ` set (take i xs)" 
    using ys_def take_map len by (metis set_map) 
  ultimately show ?thesis using set by auto
qed

lemma prob_cond_Inter_List_Index:  
  assumes "xs  []"
  assumes "set xs  events"
  shows "prob ((set xs)) = prob (hd xs) * (i = 1..<(length xs) . 
    𝒫((xs ! i) | ( j  {0..<i} . xs ! j)))"
proof -
  have " i. i < length xs  set (take i xs) = ((!) xs ` {0..<i})"
    by (metis nat_less_le nth_image)
  thus ?thesis using prob_cond_Inter_List[of xs] assms by auto
qed

lemma obtains_prob_cond_Inter_index: (* added obtains *)
  assumes " S  {}"
  assumes "S  events"
  assumes "finite S"
  obtains xs where "set xs = S" and "length xs = card S" and 
    "prob (S) = prob (hd xs) * (i = 1..<(length xs) . 𝒫((xs ! i) | ( j  {0..<i} . xs ! j)))"
  using assms prob_cond_Inter_List_Index exists_list_card 
  by (metis (no_types, lifting) set_empty2) 

lemma obtain_list_index: 
  assumes "bij_betw g {0..<card S} S"
  assumes "finite S"
  obtains xs where "set xs = S" and " i . i  {0..<card S}  g i = xs ! i" and "distinct xs"
proof -
  let ?xs = "map g [0..<card S]" 
  have seq: "g ` {0..<card S} = S" using assms(1)
    by (simp add: bij_betw_imp_surj_on) 
  then have set_eq: "set ?xs = S"
    by simp 
  moreover have " i . i  {0..<card S}  g i = ?xs ! i" 
    by auto
  moreover have leneq: "length ?xs = card S" using seq by auto
  moreover have "distinct ?xs" using set_eq leneq
    by (simp add: card_distinct) 
  ultimately show ?thesis
    using that by blast 
qed

lemma prob_cond_inter_fn:  
  assumes "bij_betw g {0..<card S} S"
  assumes "finite S"
  assumes "S  {}"
  assumes "S  events"
  shows "prob (S) = prob (g 0) * (i  {1..<(card S)} . 𝒫(g i | ((g ` {0..<i}))))"
proof -
  obtain xs where seq: "set xs = S" and geq: " i . i  {0..<card S}  g i = xs ! i" and "distinct xs"
    using obtain_list_index assms by auto
  then have len:  "length xs = card S" by (metis distinct_card) 
  then have "prob (S) = prob (hd xs) * (i  {1..<(length xs)} . 𝒫((xs ! i) | ( j  {0..<i} . xs ! j)))"
    using prob_cond_Inter_List_Index[of xs] assms(3) assms(4) seq by auto
  then have "prob (S) = prob (hd xs) * (i  {1..<card S} . 𝒫(g i | ( j  {0..<i} . g j)))"
    using geq len by auto
  moreover have "hd xs = g 0" 
  proof -
    have "length xs > 0" using seq assms(3) by auto 
    then have "hd xs = xs ! 0"
      by (simp add: hd_conv_nth) 
    then show ?thesis using geq len
      using 0 < length xs by auto 
  qed
  ultimately show ?thesis by simp
qed

lemma prob_cond_inter_obtain_fn: 
  assumes " S  {}"
  assumes "S  events"
  assumes "finite S"
  obtains f where "bij_betw f {0..<card S} S"  and 
    "prob (S) = prob (f 0) * (i  {1..<(card S)} . 𝒫(f i | ((f ` {0..<i}))))"
proof -
  obtain f where "bij_betw f {0..<card S} S"
    using assms(3) ex_bij_betw_nat_finite by blast 
  then show ?thesis using that prob_cond_inter_fn assms by auto
qed 


lemma prob_cond_inter_obtain_fn_compl: 
  assumes " S  {}"
  assumes "S  events"
  assumes "finite S"
  obtains f where "bij_betw f {0..<card S} S" and "prob (((-) (space M) ` S)) = 
     prob (space M - f 0) * (i  {1..<(card S)} . 𝒫(space M - f i | (((-) (space M) ` f ` {0..<i}))))"
proof -
  let ?c = "(-) (space M)"
  obtain f where bb: "bij_betw f {0..<card S} S"
    using assms(3) ex_bij_betw_nat_finite by blast 
  moreover have bij: "bij_betw ?c S ((-) (space M) ` S)"
    using bij_betw_compl_sets_rev assms(2) by auto
  ultimately have "bij_betw (?c  f) {0..<card S} (?c ` S)"
    using bij_betw_comp_iff by blast 
  moreover have "?c ` S  {}" using assms(1) by auto
  moreover have "finite (?c ` S )" using assms(3) by auto
  moreover have "?c ` S  events" using assms(2) by auto
  moreover have "card S = card (?c ` S)" using bij
    by (simp add: bij_betw_same_card)  
  ultimately have "prob ((?c ` S)) = prob ((?c  f) 0) * 
    (i  {1..<(card S)} . 𝒫((?c  f) i | (((?c  f) ` {0..<i}))))"
    using prob_cond_inter_fn[of "(?c  f)" "(?c ` S)"] by auto
  then have "prob ((?c ` S)) = prob (space M - (f 0)) * 
    (i  {1..<(card S)} . 𝒫(space M -  (f i) | (((?c  f) ` {0..<i}))))" by simp
  then show ?thesis using that bb by simp
qed 

lemma prob_cond_Inter_index_cond_fn:
  assumes "I  {}"
  assumes "finite I"
  assumes "finite E"
  assumes "E  {}"
  assumes "E  events"
  assumes "F ` I  events"
  assumes "prob (E) > 0"
  assumes bb: "bij_betw g {0..<card I} I"
  shows "𝒫(((F ` g ` {0..<card I})) | (E)) = 
    (i  {0..<card I}.  𝒫(F (g i) | (((F ` g` {0..<i})  E))))"
proof -
  let ?n = "card I"
  have eq: "F ` I = (F  g) ` {0..<card I}" using bij_betw_image_comp_eq bb  by metis
  moreover have "0 < ?n" using assms(1) assms(2) by auto
  ultimately have "𝒫( ((F  g) ` {0..<card I}) |  E) = 
      (i = 0..<?n. 𝒫(F (g i) |  ((F  g) ` {0..<i}  E)))"
    using prob_cond_Inter_index_cond_set[of ?n E "(F  g)"] assms(3) assms(4) assms(5) assms(6) 
      assms(7) by auto
  moreover have " i. i  {0..<?n}  (F  g) ` {0..<i} = F ` g ` {0..<i}" using image_comp by auto
  ultimately have "𝒫( (F ` g ` {0..<card I}) |  E) = (i = 0..<?n. 𝒫(F (g i) |  (F ` g ` {0..<i}  E)))" 
    using image_comp[of F g "{0..<card I}"] by auto
  then show ?thesis using eq bb assms by blast
qed

lemma prob_cond_Inter_index_cond_obtains:
  assumes "I  {}"
  assumes "finite I"
  assumes "finite E"
  assumes "E  {}"
  assumes "E  events"
  assumes "F ` I  events"
  assumes "prob (E) > 0"
  obtains g where "bij_betw g {0..<card I} I" and  "𝒫(((F ` g ` {0..<card I})) | (E)) = 
    (i  {0..<card I}.  𝒫(F (g i) | (((F ` g` {0..<i})  E))))"
proof -
  obtain g where bb: "bij_betw g {0..<card I} I" using assms(2) ex_bij_betw_nat_finite by auto
  then show thesis using assms prob_cond_Inter_index_cond_fn[of I E F g] that by blast
qed

lemma prob_cond_Inter_index_cond_compl_fn:
  assumes "I  {}"
  assumes "finite I"
  assumes "finite E"
  assumes "E  {}"
  assumes "E  events"
  assumes "F ` I  events"
  assumes "prob (E) > 0"
  assumes bb: "bij_betw g {0..<card I} I"
  shows "𝒫((Aj  I . space M - F Aj) | (E)) = 
    (i  {0..<card I}.  𝒫(space M - F (g i) | ((((λAj. space M - F Aj) ` g ` {0..<i})  E))))"
proof -
  let ?n = "card I"
  let ?G = "λ i. space M - F i"
  have eq: "?G ` I = (?G  g) ` {0..<card I}" using bij_betw_image_comp_eq bb by metis
  then have "(?G  g) ` {0..<card I}   events" using assms(5)
    by (metis assms(6) compl_subset_in_events image_image) 
  moreover have "0 < ?n" using assms(1) assms(2) by auto
  ultimately have "𝒫( ((?G  g) ` {0..<card I}) |  E) = (i = 0..<?n. 𝒫(?G (g i) |  ((?G  g) ` {0..<i}  E)))"
    using prob_cond_Inter_index_cond_set[of ?n E "(?G  g)"] assms(3) assms(4) assms(5) assms(6) 
      assms(7) by auto
  moreover have " i. i  {0..<?n}  (?G  g) ` {0..<i} = ?G ` g ` {0..<i}" using image_comp by auto
  ultimately have "𝒫( (?G ` I) |  E) = (i = 0..<?n. 𝒫(?G (g i) |  (?G ` g ` {0..<i}  E)))" 
    using image_comp[of ?G g "{0..<card I}"] eq by auto
  then show ?thesis using bb by blast
qed

lemma prob_cond_Inter_index_cond_compl_obtains:
  assumes "I  {}"
  assumes "finite I"
  assumes "finite E"
  assumes "E  {}"
  assumes "E  events"
  assumes "F ` I  events"
  assumes "prob (E) > 0"
  obtains g where "bij_betw g {0..<card I} I" and "𝒫((Aj  I . space M - F Aj) | (E)) = 
    (i  {0..<card I}.  𝒫(space M - F (g i) | ((((λAj. space M - F Aj) ` g ` {0..<i})  E))))"
proof -
  let ?n = "card I"
  let ?G = "λ i. space M - F i"
  obtain g where bb: "bij_betw g {0..<?n} I" using assms(2) ex_bij_betw_nat_finite by auto
  then show ?thesis using assms prob_cond_Inter_index_cond_compl_fn[of I E F g] that by blast
qed

lemma prob_cond_inter_index_fn2: 
  assumes "F ` S  events"
  assumes "finite S"
  assumes "card S > 0"
  assumes "bij_betw g {0..<card S} S"
  shows "prob ((F `S)) = prob (F (g 0)) * (i  {1..<(card S)} . 𝒫(F (g i) | ((F ` g ` {0..<i}))))"
proof -
  have 1: "F ` S = (F  g) ` {0..<card S}" using assms(4) bij_betw_image_comp_eq  by metis
  moreover have "prob (((F  g) ` {0..<card S})) = 
      prob (F (g 0)) * (i  {1..<(card S)} . 𝒫(F (g i) | ((F ` g ` {0..<i}))))"
    using 1 prob_cond_Inter_index[of "card S" "F  g"] assms(3) assms(1) by auto
  ultimately show ?thesis using assms(4)
    by metis
qed 

lemma prob_cond_inter_index_fn: 
  assumes "F ` S  events"
  assumes "finite S"
  assumes "S  {}"
  assumes "bij_betw g {0..<card S} S"
  shows "prob ((F `S)) = prob (F (g 0)) * (i  {1..<(card S)} . 𝒫(F (g i) | ((F ` g ` {0..<i}))))"
proof -
  have "card S > 0" using assms(3) assms(2)
    by (simp add: card_gt_0_iff) 
  moreover have "(F  g) ` {0..<card S}  events" using assms(1) assms(4)
    using  bij_betw_imp_surj_on by (metis image_comp) 
  ultimately have "prob (((F  g) ` {0..<card S})) = 
      prob (F (g 0)) * (i  {1..<(card S)} . 𝒫(F (g i) | ((F ` g ` {0..<i}))))"
    using prob_cond_Inter_index[of "card S" "F  g"] by auto
  moreover have "F ` S = (F  g) ` {0..<card S}" using assms(4) 
    using bij_betw_imp_surj_on image_comp by (metis) 
  ultimately show ?thesis using assms(4) by presburger 
qed 

lemma prob_cond_inter_index_obtain_fn: 
  assumes "F ` S  events"
  assumes "finite S"
  assumes "S  {}"
  obtains g where "bij_betw g {0..<card S} S"  and 
    "prob ((F `S)) = prob (F (g 0)) * (i  {1..<(card S)} . 𝒫(F (g i) | ((F ` g ` {0..<i}))))"
proof -
  obtain f where bb: "bij_betw f {0..<card S} S"
    using assms(2) ex_bij_betw_nat_finite by blast 
  then show ?thesis using prob_cond_inter_index_fn that assms by blast 
qed 

lemma prob_cond_inter_index_fn_compl: 
  assumes " S  {}"
  assumes "F ` S  events"
  assumes "finite S"
  assumes "bij_betw f {0..<card S} S"
  shows "prob (((-) (space M) ` F ` S)) = prob (space M - F (f 0)) * 
    (i  {1..<(card S)} . 𝒫(space M - F (f i) | (((-) (space M) ` F ` f ` {0..<i}))))"
proof -
  define G where "G  λ i. space M - F i"
  then have "G ` S  events" using G_def assms(2) by auto
  then have "prob ( (G ` S)) = prob (G (f 0)) * (i = 1..<card S. 𝒫(G (f i) |  (G ` f ` {0..<i})))"
    using prob_cond_inter_index_fn[of G S] assms by auto
  moreover have "(((-) (space M) ` F ` S)) = (iS. space M - F i)" by auto
  ultimately show ?thesis unfolding G_def by auto
qed


lemma prob_cond_inter_index_obtain_fn_compl: 
  assumes " S  {}"
  assumes "F ` S  events"
  assumes "finite S"
  obtains f where "bij_betw f {0..<card S} S"  and 
    "prob (((-) (space M) ` F ` S)) = prob (space M - F (f 0)) * 
      (i  {1..<(card S)} . 𝒫(space M - F (f i) | (((-) (space M) ` F ` f ` {0..<i}))))"
proof -
  obtain f where bb: "bij_betw f {0..<card S} S"
    using assms(3) ex_bij_betw_nat_finite by blast 
  then show ?thesis using prob_cond_inter_index_fn_compl[of S F f] assms that by blast
qed

lemma prob_cond_Inter_take: 
  assumes " S  {}"
  assumes "S  events"
  assumes "finite S"
  obtains xs where "set xs = S" and "length xs = card S" and 
    "prob (S) = prob (hd xs) * (i = 1..<(length xs) . 𝒫((xs ! i) | ((set (take i xs )))))"
  using assms prob_cond_Inter_List exists_list_card 
  by (metis (no_types, lifting) set_empty2 subset_code(1)) 


lemma prob_cond_Inter_set_bound: 
  assumes " A  {}"
  assumes "A  events"
  assumes "finite A"
  assumes " Ai . f Ai  0  f Ai  1"
  assumes "Ai S. Ai  A  S  A - {Ai}  S  {}  𝒫(Ai | (S))  f Ai"
  assumes " Ai. Ai  A  prob Ai  f Ai"
  shows "prob (A)  (a'  A .  f a')"
proof - 
  obtain xs where eq: "set xs = A" and seq: "length xs = card A" and
    pA: "prob (A) = prob (hd xs) * (i = 1..<(length xs) . 𝒫((xs ! i) | ( j  {0..<i} . xs ! j)))"
    using assms obtains_prob_cond_Inter_index[of A] by blast
  then have dis: "distinct xs" using card_distinct
    by metis 
  then have "hd xs  A" using eq hd_in_set assms(1) by auto
  then have "prob (hd xs)  (f (hd xs))" using assms(6) by blast
  have " i. i  {1..<(length xs)}  𝒫((xs ! i) | ( j  {0..<i} . xs ! j))  f (xs ! i)"
  proof -
    fix i assume "i  {1..<length xs}"
    then have ilb: "i  1" and iub: "i < length xs" by auto
    then have xsin: "xs ! i  A" using eq by auto
    define S where "S = (λ j. xs ! j) ` {0..<i}"
    then have "S = set (take i xs)"
      by (simp add: iub less_or_eq_imp_le nth_image)
    then have "xs ! i  S" using dis set_take_distinct_elem_not iub by simp
    then have "S  A - {(xs ! i)}"
      using S = set (take i xs) eq set_take_subset by fastforce 
    moreover have "S  {}" using S_def ilb by (simp) 
    moreover have "𝒫((xs ! i) | ( j  {0..<i} . xs ! j)) = 𝒫((xs ! i) | ( Aj  S . Aj))" 
      using S_def by auto
    ultimately show "𝒫((xs ! i) | ( j  {0..<i} . xs ! j))  f (xs ! i)"
      using assms(5) xsin by auto
  qed
  then have "(i = 1..<(length xs) . 𝒫((xs ! i) | ( j  {0..<i} . xs ! j)))  
    (i = 1..<(length xs) . f (xs ! i))"
    by (meson assms(4) prod_mono)
  moreover have "(i = 1..<(length xs) . f (xs ! i)) = (a  A - {hd xs} . f a)"
  proof -
    have ne: "xs  []" using assms(1) eq by auto
    have "A = (λ j. xs ! j) ` {0..<length xs}" using eq
      by (simp add: nth_image) 
    have "A - {hd xs} = set (tl xs) " using dis
      by (metis Diff_insert_absorb distinct.simps(2) eq list.exhaust_sel list.set(2) ne)
    also have "... = (λ j. xs ! j) ` {1..<length xs}" using nth_image_tl ne by auto
    finally have Ahdeq: "A - {hd xs} = (λ j. xs ! j) ` {1..<length xs}" by simp
    have io: "inj_on (nth xs) {1..<length xs}" using inj_on_nth dis
      by (metis atLeastLessThan_iff) 
    have "(i = 1..<(length xs) . f (xs ! i)) = (i  {1..<(length xs)} . f (xs ! i))" by simp
    also have "... = (i  (λ j. xs ! j) ` {1..<length xs} . f i)" 
      using io by (simp add: prod.reindex_cong) 
    finally show ?thesis using Ahdeq
      using (i = 1..<length xs. f (xs ! i)) = prod f ((!) xs ` {1..<length xs}) by presburger 
  qed
  ultimately have "prob (A)  f (hd xs) * (a  A - {hd xs} . f a)"
    using pA f (hd xs)  prob (hd xs) assms(4) ordered_comm_semiring_class.comm_mult_left_mono
    by (simp add: mult_mono' prod_nonneg)  
  then show ?thesis
    by (metis hd xs  A assms(3) prod.remove) 
qed
end

end