section "List Inversion"

theory Inversion
imports "List-Index.List_Index"
begin

abbreviation "dist_perm xs ys ≡ distinct xs ∧ distinct ys ∧ set xs = set ys"

definition before_in :: "'a ⇒ 'a ⇒ 'a list ⇒ bool"
  ("(_ </ _/ in _)" [55,55,55] 55) where
"x < y in xs = (index xs x < index xs y ∧ y ∈ set xs)"

definition Inv :: "'a list ⇒ 'a list ⇒ ('a * 'a) set" where
"Inv xs ys = {(x,y). x < y in xs ∧ y < x in ys}"

lemma before_in_setD1: "x < y in xs ⟹ x : set xs"
by (metis index_conv_size_if_notin index_less before_in_def less_asym order_refl)

lemma before_in_setD2: "x < y in xs ⟹ y : set xs"
by (simp add: before_in_def)


lemma not_before_in:
  "x : set xs ⟹ y : set xs ⟹ ¬ x < y in xs ⟷ y < x in xs ∨ x=y"
by (metis index_eq_index_conv before_in_def less_asym linorder_neqE_nat)

lemma before_in_irefl: "x < x in xs = False"
by (meson before_in_setD2 not_before_in)

lemma no_before_inI[simp]: "x < y in xs ⟹ (¬ y < x in xs) = True"
by (metis before_in_setD1 not_before_in)

lemma finite_Invs[simp]:  "finite(Inv xs ys)"
apply(rule finite_subset[where B = "set xs × set ys"])
apply(auto simp add: Inv_def before_in_def)
apply(metis index_conv_size_if_notin index_less_size_conv less_asym)+
done

lemma Inv_id[simp]: "Inv xs xs = {}"
by(auto simp add: Inv_def before_in_def)

lemma card_Inv_sym: "card(Inv xs ys) = card(Inv ys xs)"
proof -
  have "Inv xs ys = (λ(x,y). (y,x)) ` Inv ys xs" by(auto simp: Inv_def)
  thus ?thesis by (metis card_image swap_inj_on)
qed

lemma Inv_tri_ineq:
  "dist_perm xs ys ⟹ dist_perm ys zs ⟹
  Inv xs zs ⊆ Inv xs ys Un Inv ys zs"
by(auto simp: Inv_def) (metis before_in_setD1 not_before_in)

lemma card_Inv_tri_ineq:
  "dist_perm xs ys ⟹ dist_perm ys zs ⟹
  card (Inv xs zs) ≤ card(Inv xs ys) + card (Inv ys zs)"
using card_mono[OF _ Inv_tri_ineq[of xs ys zs]]
by auto (metis card_Un_Int finite_Invs trans_le_add1)

end

(* Author: Tobias Nipkow *)

section "Swapping Adjacent Elements in a List"

theory Swaps
imports Inversion
begin

text‹Swap elements at index ‹n› and @{term "Suc n"}:›

definition "swap n xs =
  (if Suc n < size xs then xs[n := xs!Suc n, Suc n := xs!n] else xs)"

lemma length_swap[simp]: "length(swap i xs) = length xs"
by(simp add: swap_def)

lemma swap_id[simp]: "Suc n ≥ size xs ⟹ swap n xs = xs"
by(simp add: swap_def)

lemma distinct_swap[simp]:
  "distinct(swap i xs) = distinct xs"
by(simp add: swap_def)

lemma swap_Suc[simp]: "swap (Suc n) (a # xs) = a # swap n xs"
by(induction xs) (auto simp: swap_def)

lemma index_swap_distinct:
  "distinct xs ⟹ Suc n < length xs ⟹
  index (swap n xs) x =
  (if x = xs!n then Suc n else if x = xs!Suc n then n else index xs x)"
by(auto simp add: swap_def index_swap_if_distinct)

lemma set_swap[simp]: "set(swap n xs) = set xs"
by(auto simp add: swap_def set_conv_nth nth_list_update) metis

lemma nth_swap_id[simp]: "Suc i < length xs ⟹ swap i xs ! i = xs!(i+1)"
by(simp add: swap_def)

lemma before_in_swap:
 "dist_perm xs ys ⟹ Suc n < size xs ⟹
  x < y in (swap n xs) ⟷
  x < y in xs ∧ ¬ (x = xs!n ∧ y = xs!Suc n) ∨ x = xs!Suc n ∧ y = xs!n"
by(simp add:before_in_def index_swap_distinct)
  (metis Suc_lessD Suc_lessI index_less_size_conv index_nth_id less_Suc_eq n_not_Suc_n nth_index)

lemma Inv_swap: assumes "dist_perm xs ys"
shows "Inv xs (swap n ys) = 
  (if Suc n < size xs
   then if ys!n < ys!Suc n in xs
        then Inv xs ys ∪ {(ys!n, ys!Suc n)}
        else Inv xs ys - {(ys!Suc n, ys!n)}
   else Inv xs ys)"
proof-
  have "length xs = length ys" using assms by (metis distinct_card)
  with assms show ?thesis
    by(simp add: Inv_def set_eq_iff)
      (metis before_in_def not_before_in before_in_swap)
qed


text‹Perform a list of swaps, from right to left:›

abbreviation swaps where "swaps == foldr swap"

lemma swaps_inv[simp]:
  "set (swaps sws xs) = set xs ∧
  size(swaps sws xs) = size xs ∧
  distinct(swaps sws xs) = distinct xs"
by (induct sws arbitrary: xs) (simp_all add: swap_def)

lemma swaps_eq_Nil_iff[simp]: "swaps acts xs = [] ⟷ xs = []"
by(induction acts)(auto simp: swap_def)

lemma swaps_map_Suc[simp]:
  "swaps (map Suc sws) (a # xs) = a # swaps sws xs"
by(induction sws arbitrary: xs) auto

lemma card_Inv_swaps_le:
  "distinct xs ⟹ card (Inv xs (swaps sws xs)) ≤ length sws"
by(induction sws) (auto simp: Inv_swap card_insert_if card_Diff_singleton_if)

lemma nth_swaps: "∀i∈set is. j < i ⟹ swaps is xs ! j = xs ! j"
by(induction "is")(simp_all add: swap_def)

lemma not_before0[simp]: "~ x < xs ! 0 in xs"
apply(cases "xs = []")
by(auto simp: before_in_def neq_Nil_conv)

lemma before_id[simp]: "⟦ distinct xs; i < size xs; j < size xs ⟧ ⟹
  xs ! i < xs ! j in xs ⟷ i < j"
by(simp add: before_in_def index_nth_id)

lemma before_swaps:
  "⟦ distinct is; ∀i∈set is. Suc i < size xs; distinct xs; i ∉ set is; i < j; j < size xs ⟧ ⟹
  swaps is xs ! i < swaps is xs ! j in xs"
apply(induction "is" arbitrary: i j)
 apply simp
apply(auto simp: swap_def nth_list_update)
done

lemma card_Inv_swaps:
  "⟦ distinct is; ∀i∈set is. Suc i < size xs; distinct xs ⟧ ⟹
  card(Inv xs (swaps is xs)) = length is"
apply(induction "is")
 apply simp
apply(simp add: Inv_swap before_swaps card_insert_if)
apply(simp add: Inv_def)
done

lemma swaps_eq_nth_take_drop: "i < length xs ⟹
    swaps [0..<i] xs = xs!i # take i xs @ drop (Suc i) xs"
apply(induction i arbitrary: xs)
apply (auto simp add: neq_Nil_conv swap_def drop_update_swap
  take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric])
done

lemma index_swaps_size: "distinct s ⟹
  index s q ≤ index (swaps sws s) q + length sws"
apply(induction sws arbitrary: s)
apply simp
 apply (fastforce simp: swap_def index_swap_if_distinct index_nth_id)
done

lemma index_swaps_last_size: "distinct s ⟹
  size s ≤ index (swaps sws s) (last s) + length sws + 1"
apply(cases "s = []")
 apply simp
using index_swaps_size[of s "last s" sws] by simp

end

(* Author: Tobias Nipkow *)

section "Deterministic Online and Offline Algorithms"

theory On_Off
imports Complex_Main
begin

type_synonym ('s,'r,'a) alg_off = "'s ⇒ 'r list ⇒ 'a list"
type_synonym ('s,'is,'r,'a) alg_on = "('s ⇒ 'is) * ('s * 'is ⇒ 'r ⇒ 'a * 'is)"

locale On_Off =
fixes step :: "'state ⇒ 'request ⇒ 'answer ⇒ 'state"
fixes t :: "'state ⇒ 'request ⇒ 'answer ⇒ nat"
fixes wf :: "'state ⇒ 'request list ⇒ bool"
begin

fun T :: "'state ⇒ 'request list ⇒ 'answer list ⇒ nat" where
"T s [] [] = 0" |
"T s (r#rs) (a#as) = t s r a + T (step s r a) rs as"

definition Step ::
  "('state , 'istate, 'request, 'answer)alg_on
   ⇒ 'state * 'istate ⇒ 'request ⇒ 'state * 'istate"
where
"Step A s r = (let (a,is') = snd A s r in (step (fst s) r a, is'))"

fun config' :: "('state,'is,'request,'answer) alg_on  ⇒ ('state*'is) ⇒ 'request list  
    ⇒ ('state * 'is)" where
"config' A s []  = s" |
"config' A s (r#rs) = config' A (Step A s r) rs"

lemma config'_snoc: "config' A s (rs@[r]) = Step A (config' A s rs) r"
apply(induct rs arbitrary: s) by simp_all

lemma config'_append2: "config' A s (xs@ys) = config' A (config' A s xs) ys"
apply(induct xs arbitrary: s) by simp_all

lemma config'_induct: "P (fst init) ⟹ (⋀s q a. P s ⟹ P (step s q a))
     ⟹ P (fst (config' A init rs))"
apply (induct rs arbitrary: init) by(simp_all add: Step_def split: prod.split)

abbreviation config where
"config A s0 rs == config' A (s0, fst A s0) rs" 
 

lemma config_snoc: "config A s (rs@[r]) = Step A (config A s rs) r"
using config'_snoc by metis

lemma config_append: "config A s (xs@ys) = config' A (config A s xs) ys"
using config'_append2 by metis

lemma config_induct: "P s0 ⟹ (⋀s q a. P s ⟹ P (step s q a)) ⟹ P (fst (config A s0 qs))"
using config'_induct[of P "(s0, fst A s0)" ] by auto

fun T_on' :: "('state,'is,'request,'answer) alg_on ⇒ ('state*'is) ⇒ 'request list ⇒  nat" where
"T_on' A s [] = 0" |
"T_on' A s (r#rs) = (t (fst s) r (fst (snd A s r))) + T_on' A (Step A s r) rs"

lemma T_on'_append: "T_on' A s (xs@ys) = T_on' A s xs + T_on' A (config' A s xs) ys"
apply(induct xs arbitrary: s) by simp_all   

abbreviation T_on'' :: "('state,'is,'request,'answer) alg_on ⇒ 'state ⇒ 'request list ⇒ nat" where
  "T_on'' A s rs == T_on' A (s,fst A s) rs" 

lemma T_on_append: "T_on'' A s (xs@ys) = T_on'' A s xs + T_on' A (config A s xs) ys"
by(rule T_on'_append)  

abbreviation "T_on_n A s0 xs n == T_on' A (config A s0 (take n xs)) [xs!n]" 

lemma T_on__as_sum: "T_on'' A s0 rs = sum (T_on_n A s0 rs) {..<length rs} "
apply(induct rs rule: rev_induct)
  by(simp_all add: T_on'_append  nth_append)



fun off2 :: "('state,'is,'request,'answer) alg_on ⇒ ('state * 'is,'request,'answer) alg_off" where
"off2 A s [] = []" |
"off2 A s (r#rs) = fst (snd A s r) # off2 A (Step A s r) rs"


abbreviation off :: "('state,'is,'request,'answer) alg_on ⇒ ('state,'request,'answer) alg_off" where
"off A s0 ≡ off2 A (s0, fst A s0)"


abbreviation T_off :: "('state,'request,'answer) alg_off ⇒ 'state ⇒ 'request list ⇒ nat" where
"T_off A s0 rs == T s0 rs (A s0 rs)"



abbreviation T_on :: "('state,'is,'request,'answer) alg_on ⇒ 'state ⇒ 'request list ⇒ nat" where
"T_on A == T_off (off A)"



lemma T_on_on': "T_off (λs0. (off2 A (s0, x))) s0 qs = T_on' A (s0,x) qs"
apply(induct qs arbitrary: s0 x) 
  by(simp_all add: Step_def split: prod.split)

lemma T_on_on'': "T_on A s0 qs = T_on'' A s0 qs"
using T_on_on'[where x="fst A s0", of s0 qs A] by(auto)

lemma T_on_as_sum: "T_on A s0 rs = sum (T_on_n A s0 rs) {..<length rs} "
using T_on__as_sum T_on_on'' by metis



definition T_opt :: "'state ⇒ 'request list ⇒ nat" where
"T_opt s rs = Inf {T s rs as | as. size as = size rs}"

definition compet :: "('state,'is,'request,'answer) alg_on ⇒ real ⇒ 'state set ⇒ bool" where
"compet A c S = (∀s∈S. ∃b ≥ 0. ∀rs. wf s rs ⟶ real(T_on A s rs) ≤ c * T_opt s rs + b)"

lemma length_off[simp]: "length(off2 A s rs) = length rs"
by (induction rs arbitrary: s) (auto split: prod.split)

lemma compet_mono: assumes "compet A c S0" and "c ≤ c'"
shows "compet A c' S0"
proof (unfold compet_def, auto)
  let ?compt = "λs0 rs b (c::real). T_on A s0 rs ≤ c * T_opt s0 rs + b"
  fix s0 assume "s0 ∈ S0"
  with assms(1) obtain b where "b ≥ 0" and 1: "∀rs. wf s0 rs ⟶ ?compt s0 rs b c"
    by(auto simp: compet_def)
  have "∀rs.  wf s0 rs ⟶ ?compt s0 rs b c'"
  proof safe
    fix rs
    assume wf: "wf s0 rs"
    from 1 wf have "?compt s0 rs b c" by blast
    thus "?compt s0 rs b c'"
      using 1 mult_right_mono[OF assms(2) of_nat_0_le_iff[of "T_opt s0 rs"]]
      by arith
  qed
  thus "∃b≥0. ∀rs.  wf s0 rs ⟶ ?compt s0 rs b c'" using ‹b≥0› by(auto)
qed

lemma competE: fixes c :: real
assumes "compet A c S0" "c ≥ 0" "∀s0 rs. size(aoff s0 rs) = length rs" "s0∈S0"
shows "∃b≥0. ∀rs. wf s0 rs ⟶ T_on A s0 rs ≤ c * T_off aoff s0 rs + b"
proof -
  from assms(1,4) obtain b where "b≥0" and
    1: "∀rs.  wf s0 rs ⟶ T_on A s0 rs ≤ c * T_opt s0 rs + b"
    by(auto simp add: compet_def)
  { fix rs
    assume "wf s0 rs"
    then have 2: "real(T_on A s0 rs) ≤ c * Inf {T s0 rs as | as. size as = size rs} + b"
      (is "_ ≤ _ * real(Inf ?T) + _")
      using 1 by(auto simp add: T_opt_def)
    have "Inf ?T ≤ T_off aoff s0 rs"
      using assms(3) by (intro cInf_lower) auto
    from mult_left_mono[OF of_nat_le_iff[THEN iffD2, OF this] assms(2)]
    have "T_on A s0 rs ≤ c * T_off aoff s0 rs + b" using 2 by arith
  }
  thus ?thesis using ‹b≥0› by(auto simp: compet_def)
qed

end

end

(*  Title:       Definition of Expectation and Distribution of uniformly distributed bit vectors
    Author:      Max Haslbeck
*)

section "Probability Theory"

theory Prob_Theory
imports "HOL-Probability.Probability"
begin

lemma integral_map_pmf[simp]:
  fixes f::"real ⇒ real"
  shows "(∫x. f x ∂(map_pmf g M)) = (∫x. f (g x) ∂M)"
   unfolding map_pmf_rep_eq
 using integral_distr[of g "(measure_pmf M)" "(count_space UNIV)" f] by auto


subsection "function ‹E›"

definition E :: "real pmf ⇒ real"  where
  "E M = (∫x. x ∂ measure_pmf M)"

translations
  "∫ x. f ∂M" <= "CONST lebesgue_integral M (λx. f)"

notation (latex output) E  ("E[_]" [1] 100)

lemma E_const[simp]: "E (return_pmf a) = a"
unfolding E_def
unfolding return_pmf.rep_eq
by (simp add: integral_return)

lemma E_null[simp]: "E (return_pmf 0) = 0"
by auto

lemma E_finite_sum: "finite (set_pmf X) ⟹ E X = (∑x∈(set_pmf X). pmf X x * x)"
  unfolding E_def by (subst integral_measure_pmf) simp_all

lemma E_of_const: "E(map_pmf (λx. y) (X::real pmf)) = y" by auto

lemma E_nonneg:
  shows "(∀x∈set_pmf X. 0≤ x) ⟹ 0 ≤ E X"
unfolding E_def
using integral_nonneg by (simp add: AE_measure_pmf_iff integral_nonneg_AE)

lemma E_nonneg_fun: fixes f::"'a⇒real"
  shows "(∀x∈set_pmf X. 0≤f x) ⟹ 0 ≤ E (map_pmf f X)"
using E_nonneg by auto

lemma E_cong:
  fixes f::"'a ⇒ real"
  shows "finite (set_pmf X) ⟹ (∀x∈ set_pmf X. (f x) = (u x)) ⟹ E (map_pmf f X) = E (map_pmf u X)"
unfolding E_def integral_map_pmf apply(rule integral_cong_AE)
apply(simp add: integrable_measure_pmf_finite)+
by (simp add: AE_measure_pmf_iff)

lemma E_mono3:
  fixes f::"'a ⇒ real"
  shows " integrable (measure_pmf X) f ⟹  integrable (measure_pmf X) u ⟹ (∀x∈ set_pmf X. (f x) ≤ (u x)) ⟹ E (map_pmf f X) ≤ E (map_pmf u X)"
unfolding E_def integral_map_pmf apply(rule integral_mono_AE)
by (auto simp add: AE_measure_pmf_iff)

lemma E_mono2:
  fixes f::"'a ⇒ real"
  shows "finite (set_pmf X) ⟹ (∀x∈ set_pmf X. (f x) ≤ (u x)) ⟹ E (map_pmf f X) ≤ E (map_pmf u X)"
unfolding E_def integral_map_pmf apply(rule integral_mono_AE)
apply(simp add: integrable_measure_pmf_finite)+
by (simp add: AE_measure_pmf_iff)

lemma E_linear_diff2: "finite (set_pmf A) ⟹ E (map_pmf f A) - E (map_pmf g A) = E (map_pmf (λx. (f x) - (g x)) A)"
unfolding E_def integral_map_pmf apply(rule Bochner_Integration.integral_diff[of "measure_pmf A" f g, symmetric])
 by (simp_all add: integrable_measure_pmf_finite)

lemma E_linear_plus2: "finite (set_pmf A) ⟹ E (map_pmf f A) + E (map_pmf g A) = E (map_pmf (λx. (f x) + (g x)) A)"
unfolding E_def integral_map_pmf apply(rule Bochner_Integration.integral_add[of "measure_pmf A" f g, symmetric])
 by (simp_all add: integrable_measure_pmf_finite)

lemma E_linear_sum2: "finite (set_pmf D) ⟹ E(map_pmf (λx. (∑i<up. f i x)) D)
      = (∑i<(up::nat). E(map_pmf (f i) D))"
unfolding E_def integral_map_pmf apply(rule Bochner_Integration.integral_sum) by (simp add: integrable_measure_pmf_finite)

lemma E_linear_sum_allg: "finite (set_pmf D) ⟹ E(map_pmf (λx. (∑i∈ A. f i x)) D)
      = (∑i∈ (A::'a set). E(map_pmf (f i) D))"
unfolding E_def integral_map_pmf apply(rule Bochner_Integration.integral_sum) by (simp add: integrable_measure_pmf_finite)

lemma E_finite_sum_fun: "finite (set_pmf X) ⟹
    E (map_pmf f X) = (∑x∈set_pmf X. pmf X x * f x)"
proof -
  assume finite: "finite (set_pmf X)"
  have "E (map_pmf f X) = (∫x. f x ∂measure_pmf X)"
      unfolding E_def by auto
  also have "… = (∑x∈set_pmf X. pmf X x * f x)"
    by (subst integral_measure_pmf) (auto simp add: finite)
  finally show ?thesis .
qed

lemma E_bernoulli: "0≤p ⟹ p≤1 ⟹
        E (map_pmf f (bernoulli_pmf p)) = p*(f True) + (1-p)*(f False)"
unfolding E_def by (auto)


subsection "function ‹bv›"

  fun bv:: "nat ⇒ bool list pmf" where
  "bv 0 = return_pmf []"
| "bv (Suc n) =  do {
                    (xs::bool list) ← bv n;
                    (x::bool) ← (bernoulli_pmf 0.5);
                    return_pmf (x#xs)
                  }"

lemma bv_finite: "finite (bv n)"
by (induct  n) auto

lemma len_bv_n: "∀xs ∈ set_pmf (bv n). length xs = n"
apply(induct n) by auto

lemma bv_set: "set_pmf (bv n) = {x::bool list. length x = n}"
proof (induct n)
  case (Suc n)
  then have "set_pmf (bv (Suc n)) = (⋃x∈{x. length x = n}. {True # x, False # x})"
    by(simp add: set_pmf_bernoulli UNIV_bool)
  also have "… = {x#xs| x xs. length xs = n}" by auto
  also have "… = {x. length x = Suc n} " using Suc_length_conv by fastforce
  finally show ?case .
qed (simp)

lemma len_not_in_bv: "length xs  ≠ n ⟹ xs ∉ set_pmf (bv n)"
by(auto simp: len_bv_n)

lemma not_n_bv_0: "length xs ≠ n ⟹ pmf (bv n) xs = 0"
by (simp add: len_not_in_bv pmf_eq_0_set_pmf)

lemma bv_comp_bernoulli: "n < l
        ⟹ map_pmf (λy. y!n) (bv l) = bernoulli_pmf (5 / 10)"
proof (induct n arbitrary: l)
  case 0
  then obtain m where "l = Suc m" by (metis Suc_pred)
  then show "map_pmf (λy. y!0) (bv l) =  bernoulli_pmf (5 / 10)" by (auto simp: map_pmf_def bind_return_pmf bind_assoc_pmf bind_return_pmf')
next
  case (Suc n)
  then have "0 < l" by auto
  then obtain m where lsm: "l = Suc m" by (metis Suc_pred)
  with Suc(2) have nltm: "n < m" by auto

  from lsm have "map_pmf (λy. y ! Suc n) (bv l)
       =  map_pmf (λx. x!n) (bind_pmf (bv m) (λt. (return_pmf t)))" by (auto simp: map_bind_pmf)
also
  have "… =  map_pmf (λx. x!n) (bv m)" by (auto simp: bind_return_pmf')
also
  have "… = bernoulli_pmf (5 / 10)" by (auto simp add: Suc(1)[of m, OF nltm])
finally
  show ?case .
qed

lemma pmf_2elemlist: "pmf (bv (Suc 0)) ([x]) = pmf (bv 0) [] * pmf (bernoulli_pmf (5 / 10)) x"
  unfolding bv.simps(2)[where n=0] pmf_bind pmf_return
  apply (subst integral_measure_pmf[where A="{[]}"])
  apply (auto) by (cases x) auto

lemma pmf_moreelemlist: "pmf (bv (Suc n)) (x#xs) = pmf (bv n) xs * pmf (bernoulli_pmf (5 / 10)) x"
  unfolding bv.simps(2) pmf_bind pmf_return
  apply (subst integral_measure_pmf[where A="{xs}"])
  apply auto apply (cases x) apply(auto)
  apply (meson indicator_simps(2) list.inject singletonD)
  apply (meson indicator_simps(2) list.inject singletonD)
  apply (cases x) by(auto)

lemma list_pmf: "length xs = n ⟹ pmf (bv n) xs = (1 / 2)^n"
proof(induct n arbitrary: xs)
  case 0
  then have "xs = []" by auto
  then show "pmf (bv 0) xs = (1 / 2) ^ 0" by(auto)
next
  case (Suc n xs)
  then obtain a as where split: "xs = a#as" by (metis Suc_length_conv)
  have "length as = n" using Suc(2) split by auto
  with Suc(1) have 1: "pmf (bv n) as = (1 / 2) ^ n" by auto

  from split pmf_moreelemlist[where n=n and x=a and xs=as] have
    "pmf (bv (Suc n)) xs = pmf (bv n) as * pmf (bernoulli_pmf (5 / 10)) a" by auto
  then have "pmf (bv (Suc n)) xs = (1 / 2) ^ n * 1 / 2" using 1 by auto
  then show "pmf (bv (Suc n)) xs = (1 / 2) ^ Suc n" by auto
qed

lemma bv_0_notlen: "pmf (bv n) xs = 0 ⟹ length xs ≠ n "
by(auto simp: list_pmf)

lemma "length xs > n ⟹ pmf (bv n) xs = 0"
proof (induct n arbitrary: xs)
  case (Suc n xs)
  then obtain a as where split: "xs = a#as" by (metis Suc_length_conv Suc_lessE)
  have "length as > n" using Suc(2) split by auto
  with Suc(1) have 1: "pmf (bv n) as = 0" by auto
  from split pmf_moreelemlist[where n=n and x=a and xs=as] have
    "pmf (bv (Suc n)) xs = pmf (bv n) as * pmf (bernoulli_pmf (5 / 10)) a" by auto
  then have "pmf (bv (Suc n)) xs = 0 * 1 / 2" using 1 by auto
  then show "pmf (bv (Suc n)) xs = 0" by auto
qed simp

lemma map_hd_list_pmf: "map_pmf hd (bv (Suc n)) = bernoulli_pmf (5 / 10)"
  by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf')

lemma map_tl_list_pmf: "map_pmf tl (bv (Suc n)) = bv n"
  by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf' )


subsection "function ‹flip›"

fun flip :: "nat ⇒ bool list ⇒ bool list" where
  "flip _ [] = []"
| "flip 0 (x#xs) = (¬x)#xs"
| "flip (Suc n) (x#xs) = x#(flip n xs)"

lemma flip_length[simp]: "length (flip i xs) = length xs"
apply(induct xs arbitrary: i) apply(simp) apply(case_tac i) by(simp_all)

lemma flip_out_of_bounds: "y ≥ length X ⟹ flip y X = X"
apply(induct X arbitrary: y)
proof -
  case (Cons X Xs)
  hence "y > 0" by auto
  with Cons obtain y' where y1: "y = Suc y'" and y2: "y' ≥ length Xs" by (metis Suc_pred' length_Cons not_less_eq_eq)
  then have "flip y (X # Xs) = X#(flip y' Xs)" by auto
  moreover from Cons y2 have "flip y' Xs = Xs" by auto
  ultimately show ?case by auto
qed simp

lemma flip_other: "y < length X ⟹ z < length X ⟹ z ≠ y ⟹ flip z X ! y = X ! y"
apply(induct y arbitrary: X z)
apply(simp) apply (metis flip.elims neq0_conv nth_Cons_0)
proof (case_tac z, goal_cases)
  case (1 y X z)
  then obtain a as where "X=a#as" using length_greater_0_conv by (metis (full_types) flip.elims)
  with 1(5) show ?case by(simp)
next
  case (2 y X z z')
  from 2 have 3: "z' ≠ y" by auto
  from 2(2) have "length X > 0" by auto
  then obtain a as where aas: "X = a#as" by (metis (full_types) flip.elims length_greater_0_conv)
  then have a: "flip (Suc z') X ! Suc y = flip z' as ! y"
    and b : "(X ! Suc y) = (as !  y)" by auto
  from 2(2) aas have 1: "y < length as" by auto
  from 2(3,5) aas have f2: "z' < length as" by auto
  note c=2(1)[OF 1 f2 3]

  have "flip z X ! Suc y = flip (Suc z') X ! Suc y" using 2 by auto
  also have "… = flip z' as ! y" by (rule a)
  also have "… = as ! y" by (rule c)
  also have "… = (X ! Suc y)" by (rule b[symmetric])
  finally show "flip z X ! Suc y = (X ! Suc y)" .
qed

lemma flip_itself: "y < length X ⟹ flip y X ! y = (¬ X ! y)"
apply(induct y arbitrary: X)
apply(simp) apply (metis flip.elims nth_Cons_0 old.nat.distinct(2))
proof -
  fix y
  fix X::"bool list"
  assume iH: "(⋀X. y < length X ⟹ flip y X ! y = (¬ X ! y))"
  assume len: "Suc y < length X"
  from len have "y < length X" by auto
  from len have "length X > 0" by auto
  then obtain z zs where zzs: "X = z#zs" by (metis (full_types) flip.elims length_greater_0_conv)
  then have a: "flip (Suc y) X ! Suc y = flip y zs ! y"
    and b : "(¬ X ! Suc y) = (¬ zs !  y)" by auto
  from len zzs have "y < length zs" by auto
  note c=iH[OF this]
  from a b c show "flip (Suc y) X ! Suc y = (¬ X ! Suc y)" by auto
qed

lemma flip_twice: "flip i (flip i b) = b"
proof (cases "i < length b")
  case True
  then have A: "i < length (flip i b)" by simp
  show ?thesis apply(simp add: list_eq_iff_nth_eq) apply(clarify)
  proof (goal_cases)
    case (1 j)
    then show ?case
      apply(cases "i=j")
        using flip_itself[OF A] flip_itself[OF True] apply(simp)
        using flip_other True 1 by auto
  qed
qed (simp add: flip_out_of_bounds)

lemma flipidiflip: "y < length X ⟹ e < length X  ⟹ flip e X ! y = (if e=y then ~ (X ! y) else X ! y)"
apply(cases "e=y")
apply(simp add: flip_itself)
by(simp add: flip_other)

lemma bernoulli_Not: "map_pmf Not (bernoulli_pmf (1 / 2)) = (bernoulli_pmf (1 / 2))"
apply(rule pmf_eqI)
proof (case_tac i, goal_cases)
  case (1 i)
  then have "pmf (map_pmf Not (bernoulli_pmf (1 / 2))) i =
    pmf (map_pmf Not (bernoulli_pmf (1 / 2))) (Not False)" by auto
  also have "… = pmf (bernoulli_pmf (1 / 2)) False" apply (rule pmf_map_inj') apply(rule injI) by auto
  also have "… = pmf (bernoulli_pmf (1 / 2)) i" by auto
  finally show ?case .
next
  case (2 i)
  then have "pmf (map_pmf Not (bernoulli_pmf (1 / 2))) i =
    pmf (map_pmf Not (bernoulli_pmf (1 / 2))) (Not True)" by auto
  also have "… = pmf (bernoulli_pmf (1 / 2)) True" apply (rule pmf_map_inj') apply(rule injI) by auto
  also have "… = pmf (bernoulli_pmf (1 / 2)) i" by auto
  finally show ?case .
qed

lemma inv_flip_bv: "map_pmf (flip i) (bv n) = (bv n)"
proof(induct n arbitrary: i)
   case (Suc n i)
   note iH=this
   have "bind_pmf (bv n) (λx. bind_pmf (bernoulli_pmf (1 / 2)) (λxa. map_pmf (flip i) (return_pmf (xa # x))))
    = bind_pmf (bernoulli_pmf (1 / 2)) (λxa .bind_pmf (bv n) (λx. map_pmf (flip i) (return_pmf (xa # x))))"
    by(rule bind_commute_pmf)
   also have "… = bind_pmf (bernoulli_pmf (1 / 2)) (λxa . bind_pmf (bv n) (λx. return_pmf (xa # x)))"
   proof (cases i)
    case 0
    then have "bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. map_pmf (flip i) (return_pmf (xa # x))))
        = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. return_pmf ((¬ xa) # x)))" by auto
    also have "…  = bind_pmf (bv n) (λx. bind_pmf (bernoulli_pmf (1 / 2)) (λxa. return_pmf ((¬ xa) # x)))"
      by(rule bind_commute_pmf)
    also have "…
        = bind_pmf (bv n) (λx. bind_pmf (map_pmf Not (bernoulli_pmf (1 / 2))) (λxa. return_pmf (xa # x)))"
              by(auto simp add: bind_map_pmf)
    also have "… = bind_pmf (bv n) (λx. bind_pmf (bernoulli_pmf (1 / 2)) (λxa. return_pmf (xa # x)))" by (simp only: bernoulli_Not)
    also have "… = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. return_pmf (xa # x)))"
      by(rule bind_commute_pmf)
    finally show ?thesis .
   next
    case (Suc i')
    have "bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. map_pmf (flip i) (return_pmf (xa # x))))
        = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. return_pmf (xa # flip i' x)))" unfolding Suc by(simp)
    also have "… = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (map_pmf (flip i') (bv n)) (λx. return_pmf (xa # x)))"
        by(auto simp add: bind_map_pmf)
    also have "… =  bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. return_pmf (xa # x)))"
        using iH[of "i'"] by simp
    finally show ?thesis .
   qed
   also have "… = bind_pmf (bv n) (λx. bind_pmf (bernoulli_pmf (1 / 2)) (λxa. return_pmf (xa # x)))"
    by(rule bind_commute_pmf)
   finally show ?case by(simp add: map_pmf_def bind_assoc_pmf)
qed simp


subsection "Example for pmf"

definition "twocoins =
                do {
                    x ← (bernoulli_pmf 0.4);
                    y ← (bernoulli_pmf 0.5);
                    return_pmf (x ∨ y)
                  }"

lemma experiment0_7: "pmf twocoins True = 0.7"
unfolding twocoins_def
  unfolding pmf_bind pmf_return
  apply (subst integral_measure_pmf[where A="{True, False}"])
  by auto

subsection "Sum Distribution"

definition "Sum_pmf p Da Db = (bernoulli_pmf p) ⤜ (%b. if b then map_pmf Inl Da else map_pmf Inr Db )"

lemma b0: "bernoulli_pmf 0 = return_pmf False"
apply(rule pmf_eqI) apply(case_tac i)
  by(simp_all)
lemma b1: "bernoulli_pmf 1 = return_pmf True"
apply(rule pmf_eqI) apply(case_tac i)
  by(simp_all)


lemma Sum_pmf_0: "Sum_pmf 0 Da Db = map_pmf Inr Db"
unfolding Sum_pmf_def
apply(rule pmf_eqI)
  by(simp add: b0 bind_return_pmf)

lemma Sum_pmf_1: "Sum_pmf 1 Da Db = map_pmf Inl Da"
unfolding Sum_pmf_def
apply(rule pmf_eqI)
  by(simp add: b1 bind_return_pmf)


definition "Proj1_pmf D = map_pmf (%a. case a of Inl e ⇒ e) (cond_pmf D {f. (∃e. Inl e = f)})"


lemma A: "(case_sum (λe. e) (λa. undefined)) (Inl e) = e"
  by(simp)

lemma B: "inj (case_sum (λe. e) (λa. undefined))"
  oops

lemma none: "p >0 ⟹ p < 1 ⟹ (set_pmf (bernoulli_pmf p ⤜
          (λb. if b then map_pmf Inl Da else map_pmf Inr Db))
          ∩ {f. (∃e. Inl e = f)}) ≠ {}"
    apply(simp add: UNIV_bool)
      using set_pmf_not_empty by fast
lemma none2: "p >0 ⟹ p < 1 ⟹  (set_pmf (bernoulli_pmf p ⤜
          (λb. if b then map_pmf Inl Da else map_pmf Inr Db))
          ∩ {f. (∃e. Inr e = f)}) ≠ {}"
    apply(simp add: UNIV_bool)
      using set_pmf_not_empty by fast

lemma C: "set_pmf (Proj1_pmf (Sum_pmf 0.5 Da Db)) = set_pmf Da"
proof -
  show ?thesis
    unfolding Sum_pmf_def Proj1_pmf_def
    apply(simp add: )
    using none[of "0.5" Da Db] apply(simp add: set_cond_pmf UNIV_bool)
      by force
qed

thm integral_measure_pmf

thm pmf_cond pmf_cond[OF none]

lemma proj1_pmf: assumes "p>0" "p<1" shows "Proj1_pmf (Sum_pmf p Da Db) =  Da"
proof -

  have kl: "⋀e. pmf (map_pmf Inr Db) (Inl e) = 0"
    apply(simp only: pmf_eq_0_set_pmf)
    apply(simp) by blast

  have ll: "measure_pmf.prob
           (bernoulli_pmf p ⤜
            (λb. if b then map_pmf Inl Da else map_pmf Inr Db))
           {f. ∃e. Inl e = f} = p"
       using assms
     apply(simp add: integral_pmf[symmetric] pmf_bind)
     apply(subst Bochner_Integration.integral_add)
      using integrable_pmf apply fast
      using integrable_pmf apply fast
        by(simp add: integral_pmf)

  have E: "(cond_pmf
       (bernoulli_pmf p ⤜
        (λb. if b then map_pmf Inl Da else map_pmf Inr Db))
       {f. ∃e. Inl e = f}) =
    map_pmf Inl Da"
    apply(rule pmf_eqI)
      apply(subst pmf_cond)
      using none[of p Da Db] assms apply (simp)
       using assms apply(auto)
          apply(subst pmf_bind)
          apply(simp add: kl ll )
          apply(simp only: pmf_eq_0_set_pmf) by auto

  have ID: "case_sum (λe. e) (λa. undefined) ∘ Inl = id"
    by fastforce
  show ?thesis
    unfolding Sum_pmf_def Proj1_pmf_def
    apply(simp only: E)
    apply(simp add: pmf.map_comp ID)
  done

qed


definition "Proj2_pmf D = map_pmf (%a. case a of Inr e ⇒ e) (cond_pmf D {f. (∃e. Inr e = f)})"

lemma proj2_pmf: assumes "p>0" "p<1" shows "Proj2_pmf (Sum_pmf p Da Db) =  Db"
proof -

  have kl: "⋀e. pmf (map_pmf Inl Da) (Inr e) = 0"
    apply(simp only: pmf_eq_0_set_pmf)
    apply(simp) by blast

  have ll: "measure_pmf.prob
           (bernoulli_pmf p ⤜
            (λb. if b then map_pmf Inl Da else map_pmf Inr Db))
           {f. ∃e. Inr e = f} = 1-p"
       using assms
     apply(simp add: integral_pmf[symmetric] pmf_bind)
     apply(subst Bochner_Integration.integral_add)
      using integrable_pmf apply fast
      using integrable_pmf apply fast
        by(simp add: integral_pmf)

  have E: "(cond_pmf
       (bernoulli_pmf p ⤜
        (λb. if b then map_pmf Inl Da else map_pmf Inr Db))
       {f. ∃e. Inr e = f}) =
    map_pmf Inr Db"
    apply(rule pmf_eqI)
      apply(subst pmf_cond)
      using none2[of p Da Db] assms apply (simp)
       using assms apply(auto)
          apply(subst pmf_bind)
          apply(simp add: kl ll )
          apply(simp only: pmf_eq_0_set_pmf) by auto

  have ID: "case_sum (λe. undefined) (λa. a) ∘ Inr = id"
    by fastforce
  show ?thesis
    unfolding Sum_pmf_def Proj2_pmf_def
    apply(simp only: E)
    apply(simp add: pmf.map_comp ID)
  done

qed




definition "invSum invA invB D x i == invA (Proj1_pmf D) x i ∧ invB (Proj2_pmf D) x i"


lemma invSum_split: "p>0 ⟹ p<1 ⟹ invA Da x i ⟹ invB Db x i ⟹ invSum invA invB (Sum_pmf p Da Db) x i"
by(simp add: invSum_def proj1_pmf proj2_pmf)

term "(%a. case a of Inl e ⇒ Inl (fa e) | Inr e ⇒ Inr (fb e))"
definition "f_on2 fa fb = (%a. case a of Inl e ⇒ map_pmf Inl (fa e) | Inr e ⇒ map_pmf Inr (fb e))"

term "bind_pmf"


lemma Sum_bind_pmf: assumes a: "bind_pmf Da fa = Da'" and b: "bind_pmf Db fb = Db'"
  shows "bind_pmf (Sum_pmf p Da Db) (f_on2 fa fb)
              = Sum_pmf p Da' Db'"
proof -
  { fix x
  have "(if x then map_pmf Inl Da else map_pmf Inr Db) ⤜
                 case_sum (λe. map_pmf Inl (fa e))
                  (λe. map_pmf Inr (fb e))
            =
        (if x then map_pmf Inl Da ⤜ case_sum (λe. map_pmf Inl (fa e))
                  (λe. map_pmf Inr (fb e))
              else map_pmf Inr Db ⤜ case_sum (λe. map_pmf Inl (fa e))
                  (λe. map_pmf Inr (fb e)))"
                  apply(simp) done
  also
    have "… = (if x then map_pmf Inl (bind_pmf Da fa) else map_pmf Inr (bind_pmf Db fb))"
      by(auto simp add: map_pmf_def bind_assoc_pmf bind_return_pmf)
  also
    have "… = (if x then map_pmf Inl Da' else map_pmf Inr Db')"
      using a b by simp
  finally
    have "(if x then map_pmf Inl Da else map_pmf Inr Db) ⤜
                 case_sum (λe. map_pmf Inl (fa e))
                  (λe. map_pmf Inr (fb e)) = (if x then map_pmf Inl Da' else map_pmf Inr Db')" .
  } note gr=this



  show ?thesis
    unfolding Sum_pmf_def f_on2_def
    apply(rule pmf_eqI)
    apply(case_tac i)
    by(simp_all add: bind_return_pmf bind_assoc_pmf gr)
qed

definition "sum_map_pmf fa fb = (%a. case a of Inl e ⇒ Inl (fa e) | Inr e ⇒ Inr (fb e))"

lemma Sum_map_pmf: assumes a: "map_pmf fa Da = Da'" and b: "map_pmf fb Db = Db'"
  shows "map_pmf (sum_map_pmf fa fb) (Sum_pmf p Da Db)
              = Sum_pmf p Da' Db'"
proof -
  have "map_pmf (sum_map_pmf fa fb) (Sum_pmf p Da Db)
        = bind_pmf (Sum_pmf p Da Db) (f_on2 (λx. return_pmf (fa x)) (λx. return_pmf (fb x)))"
        using a b
  unfolding map_pmf_def sum_map_pmf_def f_on2_def
    by(auto simp add: bind_return_pmf sum.case_distrib)
also
  have "… = Sum_pmf p Da' Db'"
 using assms[unfolded map_pmf_def]
 by(rule Sum_bind_pmf )
finally
  show ?thesis .
qed



end