Theory List_Space

(*
 Title:List_Space.thy
 Author: Tetsuya Sato
*)

theory List_Space
  imports
    "HOL-Analysis.Finite_Product_Measure"
    "Source_and_Sink_Algebras_Constructions"
    "Measurable_Isomorphism"
begin

section ‹ Measurable space of finite lists ›

text ‹ This entry introduces a measurable space of finite lists over a measurable space. The construction is inspired from Hirata's idea on list quasi-Borel spaces [Hirata et al., ITP 2023]. First, we construct countable coproduct space of product of n spaces. Then, we trasnsfer it to list space via bijections. ›

subsection ‹ miscellaneous lemmas ›

lemma measurable_pair_assoc[measurable]:
  shows "(λ((a, b), x). (a, b, x)) ∈ (A ⨂M B) ⨂M C →M A ⨂M B ⨂M C"
proof-
  have "(λ((a,b),x). (a,b,x)) = (λx. ((fst (fst x)),(snd (fst x)), snd x))"
    by auto
  also have "... ∈ (A ⨂M B) ⨂M C →M A ⨂M B ⨂M C"
    by measurable
  finally show "(λ((a, b), x). (a, b, x)) ∈ (A ⨂M B) ⨂M C →M A ⨂M B ⨂M C".
qed

lemma measurable_pair_assoc'[measurable]:
  shows "(λ((a, b), x, l). (a, b, x, l)) ∈ (A ⨂M B) ⨂M C ⨂M D →M A ⨂M B ⨂M C ⨂M D"
proof-
  have "(λ((a,b),x,l). (a,b,x,l)) = (λx. ((fst (fst x)),(snd (fst x)), (fst (snd x)), (snd (snd x))))"
    by auto
  also have "... ∈ (A ⨂M B) ⨂M C ⨂M D →M A ⨂M B ⨂M C ⨂M D"
    by measurable
  finally show "(λ((a, b), x, l). (a, b, x, l)) ∈ (A ⨂M B) ⨂M C ⨂M D →M A ⨂M B ⨂M C ⨂M D".
qed

subsection ‹ construction of list space ›

fun pair_to_list  :: "(nat × (nat ⇒ 'a)) ⇒ 'a list" where
  Zero: "pair_to_list (0,_) = []"
| Suc: "pair_to_list (Suc n,f) = (f 0) # pair_to_list (n, λ n. f (Suc n))"

fun list_to_pair  :: "'a list ⇒ (nat × (nat ⇒ 'a))" where
  Nil: "list_to_pair [] = (0,λ_.undefined)"
| Cons: "list_to_pair (x#xs) = (Suc (fst(list_to_pair xs)), λn. if n = 0 then x else (snd(list_to_pair xs))(n - 1))"

definition✐‹tag important› listM :: "'a measure ⇒ 'a list measure" where
  "listM M =
    initial_source (lists (space M)) {(list_to_pair, ⨿M n∈UNIV. ΠS i∈{..<n}. M)}"

lemma space_listM:
  shows "space (listM M) = (lists (space M))"
  by (auto simp: listM_def)

lemma lists_listM[measurable]:
  shows "lists (space M) ∈ sets (listM M)"
  by (metis sets.top space_listM)

lemma comp_list_to_list:
  shows "pair_to_list (list_to_pair xs) = xs"
  by(induction xs, auto)

lemma list_to_pair_function:
  shows "list_to_pair ∈ lists (space M) → space (⨿M n∈UNIV. ΠS i∈{..<n}. M)"
  unfolding space_prod_initial_source space_coprod_final_sink space_listM
proof(rule funcsetI)
  fix xs
  show "xs ∈ lists (space M)⟹ list_to_pair xs ∈ (SIGMA n:UNIV. {..<n} →E space M)"
  proof(induction xs)
    case Nil
    thus "list_to_pair [] ∈ (SIGMA n:UNIV. {..<n} →E space M)"
      unfolding PiE_def Sigma_def by auto
  next
    case (Cons x ys)
    hence propxys: "x ∈ (space M)" "ys ∈ lists (space M)"using Cons_in_lists_iff by auto
    from local.Cons obtain n f where propnf: "((list_to_pair ys) = (n,f))" "(n∈(UNIV :: nat set))" "(f ∈ {..<n} →E(space M))"
      unfolding Sigma_def by auto
    have "list_to_pair (x # ys) ∈ ({Suc n} × ({..<(Suc n)} →E(space M)))"
      using propxys propnf unfolding extensional_def PiE_def
      by(cases"n = 0",auto)
    also have "... ⊆ (SIGMA n:UNIV. {..<n} →E space M)"
      unfolding Sigma_def by(intro subsetI, blast)
    finally show "list_to_pair (x # ys) ∈ (SIGMA n:UNIV. {..<n} →E space M)".
  qed
qed

lemma list_to_pair_measurable:
  shows "list_to_pair ∈ (listM M) →M (⨿M n∈UNIV. ΠS i∈{..<n}. M)"
  unfolding listM_def using list_to_pair_function
  by (metis insertI1 measurable_initial_source1)

lemma comp_pair_to_pair:
  shows "(n,f) ∈ (SIGMA n:UNIV. {..<n} →E(space M)) ⟹ (list_to_pair (pair_to_list (n,f)) = (n,f))"
proof(induct n arbitrary: f)
  case 0
  thus ?case by auto
next
  case (Suc n)
  have "(Suc n, f) ∈ {(n,f) | n f. n∈ UNIV ∧ f ∈ {..<n} →E(space M)}"
    using Suc.prems by blast
  hence "(n, λ n. f (Suc n)) ∈ (SIGMA n:UNIV. {..<n} →E space M)"
    by (auto simp add: Sigma_def)
  hence in1: "list_to_pair (pair_to_list (n, λ n. f (Suc n))) =(n, λ n. f (Suc n))"
    by (auto simp add: Suc.hyps)
  thus ?case by auto
qed

lemma pair_to_list_function:
  shows "pair_to_list ∈ space (⨿M n∈UNIV. ΠS i∈{..<n}. M) → lists (space M)"
  unfolding space_prod_initial_source space_coprod_final_sink space_listM
proof
  fix x :: "(nat × _)" assume "x ∈ (SIGMA n:UNIV. {..<n} →E space M)"
  then obtain n f where x: "x = (n,f) ∧ (f ∈ {..<n} →E space M)"
    unfolding Sigma_def by auto
  have "⋀f. (f ∈ {..<n} →E space M) ⟹ pair_to_list (n,f) ∈ lists (space M)"
  proof(induction n)
    case 0
    thus ?case by auto
  next
    case (Suc n)
    hence "(f 0) ∈ space M" and "(λ n. f (Suc n))∈ {..<n} →E space M"
      and "⋀f. (f ∈ {..<n} →E space M) ⟹ pair_to_list (n,f) ∈ lists (space M)"
      by auto
    hence "pair_to_list (Suc n, f) ∈ lists (space M)"
      using lists.Cons by auto
    thus ?case by auto
  qed
  thus"pair_to_list x ∈ lists (space M)"using x by auto
qed

proposition pair_to_list_measurable:
  shows "pair_to_list ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M (listM M)"
  unfolding listM_def using pair_to_list_function
proof(rule measurable_initial_source2)
  have "list_to_pair ∈ lists (space M) → space (⨿M n∈UNIV. ΠS i∈{..<n}. M)"
    by (auto simp: list_to_pair_function)
  thus"∀(f, N)∈{(list_to_pair, (⨿M n∈UNIV. ΠS i∈{..<n}. M))}. f ∈ lists (space M) → space N"
    by blast
  have "(λx. list_to_pair (pair_to_list x)) ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M (⨿M n∈UNIV. ΠS i∈{..<n}. M)"
  proof(subst measurable_cong[where g ="id"])
    show "⋀w. w ∈ space (⨿M n∈UNIV. ΠS i∈{..<n}. M) ⟹ list_to_pair (pair_to_list w) = id w"
      unfolding space_prod_initial_source space_coprod_final_sink using comp_pair_to_pair by fastforce
  qed(auto)
  thus"∀(f, N)∈{(list_to_pair, (⨿M n∈UNIV. ΠS i∈{..<n}. M))}. (λx. f (pair_to_list x)) ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N"
    by blast
qed

proposition measurable_iff_list_and_pair:
  shows measurable_iff_pair_to_list: "⋀ f. (f ∈ (listM M) →M N) ⟷ (f o pair_to_list ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N)"
    and measurable_iff_list_to_pair: "⋀ f. (f o list_to_pair ∈ (listM M) →M N) ⟷ (f ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N)"
    and measurable_iff_pair_to_list2: "⋀ f. (f ∈ N →M (⨿M n∈UNIV. ΠS i∈{..<n}. M)) ⟷ (pair_to_list ∘ f∈ N →M listM M ∧ f ∈ space N → space (⨿M n∈UNIV. ΠS i∈{..<n}. M))"
    and measurable_iff_list_to_pair2: "⋀ f. (f ∈ N →M listM M) ⟷ (list_to_pair ∘ f ∈ N →M (⨿M n∈UNIV. ΠS i∈{..<n}. M) ∧ f ∈ space N → space (listM M))"
proof-
  have A: "∀x∈space (⨿M n∈UNIV. ΠS i∈{..<n}. M). list_to_pair (pair_to_list x) = x"
    and B: "∀y∈space (listM M). pair_to_list (list_to_pair y) = y"
    unfolding space_coprod_final_sink space_prod_initial_source
    using comp_list_to_list comp_pair_to_pair by auto
  show "⋀ f. (f ∈ (listM M) →M N) ⟷ (f o pair_to_list ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N)"
    and "⋀ f. (f o list_to_pair ∈ (listM M) →M N) ⟷ (f ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N)"
    and "⋀ f. (f ∈ N →M (⨿M n∈UNIV. ΠS i∈{..<n}. M)) ⟷ (pair_to_list ∘ f∈ N →M listM M ∧ f ∈ space N → space (⨿M n∈UNIV. ΠS i∈{..<n}. M))"
    and "⋀ f. (f ∈ N →M listM M) ⟷ (list_to_pair ∘ f ∈ N →M (⨿M n∈UNIV. ΠS i∈{..<n}. M) ∧ f ∈ space N → space (listM M))"
    using measurable_isomorphism_iff[of pair_to_list"⨿M n∈UNIV. ΠS i∈{..<n}. M" "(listM M)"list_to_pair _ N,OF pair_to_list_measurable list_to_pair_measurable A B] by blast+
qed

proposition measurable_iff_list_and_pair_plus:
  shows measurable_iff_pair_to_list_plus: "⋀ f. (f ∈ K ⨂M (listM M) →M N) ⟷ (f o (λ q. ((fst q),pair_to_list (snd q))) ∈ K ⨂M (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N)"
    and measurable_iff_list_to_pair_plus: "⋀ f. (f ∈ K ⨂M (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N) ⟷ (f o (λ p. ((fst p), list_to_pair (snd p))) ∈ K ⨂M (listM M) →M N)"
proof-
  have 1: "(λ q. ((fst q),pair_to_list (snd q))) ∈ K ⨂M (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M K ⨂M listM M"
    using pair_to_list_measurable by measurable
  have 2: "⋀f. (λ p. ((fst p), list_to_pair (snd p))) ∈ K ⨂M listM M →M K ⨂M (⨿M n∈UNIV. ΠS i∈{..<n}. M)"
    using list_to_pair_measurable by measurable
  have 3: "∀x∈space (K ⨂M (⨿M n∈UNIV. ΠS i∈{..<n}. M)).(fst (fst x, pair_to_list (snd x)), list_to_pair (snd (fst x, pair_to_list (snd x)))) = x"
    by(auto simp add: comp_pair_to_pair comp_def space_pair_measure space_prod_initial_source space_coprod_final_sink)
  have 4: "∀y∈space (K ⨂M listM M).(fst (fst y, list_to_pair (snd y)), pair_to_list (snd (fst y, list_to_pair (snd y)))) = y"
    by(auto simp add: comp_list_to_list comp_def space_pair_measure space_prod_initial_source space_coprod_final_sink)
  show "⋀f. (f ∈ K ⨂M listM M →M N) ⟷ (f ∘ (λq. (fst q, pair_to_list (snd q))) ∈ K ⨂M (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N)"
    by(rule measurable_isomorphism_iff [OF 1 2 3 4])
  show "⋀ f. (f ∈ K ⨂M (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M N) ⟷ (f o (λ p. ((fst p), list_to_pair (snd p))) ∈ K ⨂M (listM M) →M N)"
    by(rule measurable_isomorphism_iff [OF 1 2 3 4])
qed

lemma measurable_iff_on_list:
  shows "⋀ f. (f ∈ (listM M) →M N) ⟷ (∀ n∈UNIV. (f o pair_to_list o coProj n) ∈ (ΠS i∈{..<n}. M) →M N)"
  by(auto simp add: measurable_iff_pair_to_list coprod_measurable_iff[THEN sym])


subsection‹measurability of functions defined inductively on lists›

subsubsection ‹ Measurability of @{term Cons} ›

definition shift_prod :: "'a ⇒ (nat ⇒ 'a) ⇒ (nat ⇒ 'a)" where
  "shift_prod x f = (λ m. if m = 0 then x else f(m - 1))"

lemma shift_prod_function:
  shows "(λ (x,xs).(shift_prod x xs)) ∈ space M × (ΠE i∈{..<n}. space M) → (ΠE i∈{..<(Suc n)}. space M)"
proof(clarify)
  fix x f assume x: "x ∈ (space M)" and f: "f ∈ {..<n} →E space M"
  thus"shift_prod x f ∈ {..<Suc n} →E space M"
    unfolding shift_prod_def
  proof(induction n)
    case 0
    thus ?case by(intro PiE_I, auto)
  next
    case (Suc n)
    assume f: "f ∈ {..<Suc n} →E space M"
    show "(λm. if m = 0 then x else f (m - 1)) ∈ {..<Suc (Suc n)} →E space M"
    proof(intro PiE_I)
      fix m
      show "m ∈ {..<Suc (Suc n)} ⟹ (if m = 0 then x else f (m - 1)) ∈ space M"
        using PiE_mem[OF f,where x ="m - 1"] x by auto
      show "m ∉ {..<Suc (Suc n)} ⟹ (if m = 0 then x else f (m - 1)) = undefined"
        using PiE_arb[OF f,where x ="m - 1"] x by auto
    qed
  qed
qed

lemma shift_prod_measurable:
  shows "(λ (x,xs).(shift_prod x xs)) ∈ M ⨂M (prod_initial_source {..<n} (λ_.M)) →M (prod_initial_source {..<(Suc n)} (λ_.M))"
  unfolding prod_initial_source_def
proof(rule measurable_initial_source2)
  show "(λa. case a of (x, xs) ⇒ shift_prod x xs) ∈ space (M ⨂M initial_source ({..<n} →E space M) {(λf. f i, M) |i. i ∈ {..<n}}) → {..<Suc n} →E space M"
    unfolding space_pair_measure by (metis shift_prod_function space_initial_source)
  show "∀(f, Ma)∈{(λf. f i, M) |i. i ∈ {..<Suc n}}. f ∈ ({..<Suc n} →E space M) → space Ma"
    by blast
  show "∀(f, Ma)∈{(λf. f i, M) |i. i ∈ {..<Suc n}}.
 (λx. f (case x of (x, xs) ⇒ shift_prod x xs)) ∈ M ⨂M initial_source ({..<n} →E space M) {(λf. f i, M) |i. i ∈ {..<n}} →M Ma"
  proof(intro ballI, elim exE conjE CollectE)
    fix x :: "((nat ⇒ 'a) ⇒ 'a) × 'a measure" and i assume x: "x = (λf. f i, M)" and i: "i ∈ {..<Suc n}"
    show "case x of (f, N) ⇒ (λx. f (case x of (x, xs) ⇒ shift_prod x xs)) ∈ M ⨂M initial_source ({..<n} →E space M) {(λf. f i, M) |i. i ∈ {..<n}} →M N"
    proof(cases"i = 0")
      case True
      hence *: "case x of (f, N) ⇒ (λx. f (case x of (x, xs) ⇒ shift_prod x xs)) = fst"
        by (auto simp: case_prod_unfold shift_prod_def x i)
      thus ?thesis
        by (auto simp: x)
    next
      case False
      hence *: "(case x of (f, N) ⇒ (λx. f (case x of (x, xs) ⇒ shift_prod x xs))) = (λ xa. xa(i - 1)) o snd"
        by (auto simp: case_prod_unfold comp_def shift_prod_def x i)
      have "(λ xa. xa(i - 1)) ∈ initial_source ({..<n} →E space M) {(λf. f i, M) |i. i ∈ {..<n}} →M M"
      proof(intro measurable_initial_source1)
        show **: "((λ xa. xa(i - 1)),M) ∈ {(λf. f i, M) |i. i ∈ {..<n}}"
          using False i by auto
        show "(λxa. xa (i - 1)) ∈ ({..<n} →E space M) → space M"
          using i ** by fastforce
      qed
      thus ?thesis
        using * x by force
    qed
  qed
qed

lemma shift_prod_measurable':
  assumes "x ∈ (space M)"
  shows "(shift_prod x) ∈ (prod_initial_source {..<n} (λ_.M)) →M (prod_initial_source {..<(Suc n)} (λ_.M))"
  using measurable_Pair2[OF shift_prod_measurable assms] by auto

definition shift_list :: "'a measure ⇒ 'a ⇒ nat × (nat ⇒ 'a) ⇒ nat × (nat ⇒ 'a)" where
  "shift_list M x =
    coTuple (UNIV :: nat set)
    (λ n :: nat. (space (prod_initial_source {..<n} (λ_.M))))
    (λ n :: nat. coProj (Suc n) o (shift_prod x))"

lemma shift_list_def2:
  shows "shift_list M x (n, f) = (Suc n, shift_prod x f)"
  unfolding shift_list_def shift_prod_def coTuple_def coProj_def by auto

lemma shift_list_measurable:
  shows "(λ (x,(n,f)). (shift_list M x (n,f))) ∈ (M ⨂M (⨿M n∈UNIV. ΠS i∈{..<n}. M)) →M (⨿M n∈UNIV. ΠS i∈{..<n}. M)"
proof(subst measurable_iff_dist_law_A)
  show "countable (UNIV :: nat set)"
    by auto
  show "(λ(x, n, f). shift_list M x (n, f)) ∘ dist_law_A UNIV (λn. ΠS _∈{..<n}. M) M ∈ (⨿M i∈UNIV. M ⨂M (ΠS _∈{..<i}. M)) →M (⨿M n∈UNIV. ΠS _∈{..<n}. M)"
  proof(subst coprod_measurable_iff,intro ballI)
    fix i :: nat assume "i∈UNIV"
    thus "(λ(x, n, f). shift_list M x (n, f)) ∘ dist_law_A UNIV (λn. ΠS _∈{..<n}. M) M ∘ coProj i ∈ M ⨂M (ΠS _∈{..<i}. M) →M (⨿M n∈UNIV. ΠS _∈{..<n}. M)"
      using shift_prod_measurable[of M i ] coProj_measurable[of"Suc i"UNIV"(λ i. (ΠS _∈{..<i}. M))"]
      by(subst measurable_cong, unfold coTuple_def shift_list_def dist_law_A_def shift_prod_def coProj_def, blast,auto)
  qed
qed

lemma shift_list_measurable':
  assumes "x ∈ (space M)"
  shows "(shift_list M x) ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M (⨿M n∈UNIV. ΠS i∈{..<n}. M)"
  using measurable_Pair2[OF shift_list_measurable[of M] assms] by auto

lemma measurable_Cons[measurable]:
  shows "(λ (x,xs). x # xs) ∈ M ⨂M (listM M) →M (listM M)"
proof-
  {
    fix x fix xs :: "_ list"
    have "x # xs = (pair_to_list o (λ (x,(n,f)). (shift_list M x (n,f)))) (x, list_to_pair xs)"
      unfolding shift_list_def coTuple_def  shift_prod_def
      by(induction xs ,auto simp add: comp_list_to_list coProj_def)
  }
  hence *: "(λ (x,xs). x # xs) = (pair_to_list o (λ (x,(n,f)). (shift_list M x (n,f)))) o (λ (x,xs :: _list). (x, list_to_pair xs))"
    by (auto simp: cond_case_prod_eta)
  show ?thesis
    using list_to_pair_measurable pair_to_list_measurable shift_list_measurable
    by(unfold *, measurable)
qed

lemma listM_Nil[measurable]:
  shows "Nil ∈ space (listM M)"
  unfolding listM_def space_initial_source by auto

lemma measurable_Cons'[measurable]:
  shows "x ∈ space M ⟹ Cons x ∈ (listM M) →M (listM M)"
  using measurable_Pair2 by auto

subsubsection ‹ Measurability of @{term"(λp. [p])"}, the unit of list monad. ›

lemma measurable_unit_ListM[measurable]:
  shows "(λp. [p]) ∈ M →M listM M"
  by measurable

subsubsection ‹ Measurability of @{term rec_list} ›

text ‹Since the notion of measurable functions does not support higher-order functions in general,
  the following theorems for measurability of@{term rec_list} are restricted. ›

lemma measurable_rec_list_func2':
  fixes T :: "'a ⇒ ('b ⇒ 'd)"
    and F :: "'a ⇒ 'c ⇒ 'c list ⇒ ('b ⇒ 'd) ⇒ ('b ⇒ 'd)"
  assumes "(λ(a,b). T a b) ∈ K ⨂M L →M N "
    and "⋀i g. (λ ((a, q), l). g a q l) ∈ (K ⨂M L) ⨂M (ΠS i∈{..<i}. M) →M N
 ⟹ (λ((a,b),x,l). (F a x ((pair_to_list o (coProj i)) l)) (λq. (g a q l)) b) ∈ (K ⨂M L) ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
    (*The condition is bit too strong*)
  shows "(λ((a,b),xs). (rec_list (T a) (F a)) xs b) ∈ (K ⨂M L) ⨂M (listM M) →M N"
proof(subst measurable_iff_pair_to_list_plus,subst measurable_iff_dist_laws)
  show "countable (UNIV :: nat set)"by auto
  show "(λ((a, b), xs). rec_list (T a) (F a) xs b) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ dist_law_A UNIV (λn. ΠS i∈{..<n}. M) (K ⨂M L)
 ∈ (⨿M i∈UNIV. (K ⨂M L) ⨂M (ΠS i∈{..<i}. M)) →M N"
    unfolding dist_law_A_def2
  proof(subst coprod_measurable_iff, intro ballI)
    fix i :: nat assume i: "i ∈ UNIV"
    show "(λ((a, b), xs). rec_list (T a) (F a) xs b) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj i ∈ (K ⨂M L) ⨂M (ΠS i∈{..<i}. M) →M N"
    proof(induction i)
      case 0
      have "((λa. case a of (a, b) ⇒ (case a of (a, b) ⇒ λxs. rec_list (T a) (F a) xs b) b) ∘ (λq. (fst q, pair_to_list (snd q))) ∘
 (λp. (fst (snd p), fst p, snd (snd p))) ∘
 coProj 0) = ((λ (a,b). T a b) o fst)"
        by (auto simp: coProj_def )
      also have "... ∈ (K ⨂M L) ⨂M (ΠS i∈{..<0}. M) →M N"
        using assms(1) by auto
      finally show ?case .
    next
      case (Suc i)
      have "((λa. case a of (a, b) ⇒ (case a of (a, b) ⇒ λxs. rec_list (T a) (F a) xs b) b) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj (Suc i)) = ((λ((a,b),x,l). (F a) x ((pair_to_list o (coProj i)) l) (rec_list (T a) (F a) ((pair_to_list o (coProj i)) l)) b) o (λ ((a,b),l). ((a,b),l 0,λn. l(Suc n))))"
        using List.list.rec(2)
        by (auto simp: coProj_def)
      also have "... ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M N"
      proof(rule measurable_comp)
        show "(λ((a, b), l). ((a, b), l 0, λn. l (Suc n))) ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M (K ⨂M L) ⨂M M ⨂M (ΠS i∈{..<i}. M)"
        proof(intro measurable_pair)
          have 1: "(λ l. l (0 :: nat)) ∈ (ΠS i∈{..<Suc i}. M) →M M"using
              measurable_prod_initial_source_projections by measurable
          have "fst ∘ (snd ∘ (λ((a, b), l). ((a, b), l 0, λn. l (Suc n)))) = (λ l. l 0) o snd"by auto
          also have "... ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M M"
            using 1 by auto
          finally show "fst ∘ (snd ∘ (λ((a, b), l). ((a, b), l 0, λn. l (Suc n)))) ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M M".

          have "snd ∘ (snd ∘ (λ((a, b), l). ((a, b), l 0, λn. l (Suc n)))) = (λ l. λn. l (Suc n)) o snd"by auto
          also have "... ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<i}. M)"
            using measurable_projection_shift by measurable
          finally show "snd ∘ (snd ∘ (λ((a, b), l). ((a, b), l 0, λn. l (Suc n)))) ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<i}. M)".

          have "fst ∘ (fst ∘ (λ((a, b), l). ((a, b), l 0, λn. l (Suc n)))) = fst ∘ fst"by auto
          also have "... ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M K"by auto
          finally show "fst ∘ (fst ∘ (λ((a, b), l). ((a, b), l 0, λn. l (Suc n)))) ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M K".
          have "snd ∘ (fst ∘ (λ((a, b), l). ((a, b), l 0, λn. l (Suc n)))) = snd ∘ fst"by auto
          also have "... ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M L"by auto
          finally show "snd ∘ (fst ∘ (λ((a, b), l). ((a, b), l 0, λn. l (Suc n)))) ∈ (K ⨂M L) ⨂M (ΠS i∈{..<Suc i}. M) →M L".
        qed

        show "(λ((a, b), x, l). F a x ((pair_to_list ∘ coProj i) l) (rec_list (T a) (F a) ((pair_to_list ∘ coProj i) l)) b)
 ∈ (K ⨂M L) ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
        proof(intro assms(2)[of"λ a b l. (rec_list (T a) (F a) ((pair_to_list ∘ coProj i) l)) b"i])
          have "(λ((a, q), l). rec_list (T a) (F a) ((pair_to_list ∘ coProj i) l) q) = (λa. case a of (a, b) ⇒ (case a of (a, b) ⇒ λxs. rec_list (T a) (F a) xs b) b) ∘ (λq. (fst q, pair_to_list (snd q))) ∘
(λp. (fst (snd p), fst p, snd (snd p))) ∘
coProj i"
            by (auto simp: coProj_def)
          also have "... ∈ (K ⨂M L) ⨂M (ΠS i∈{..<i}. M) →M N"using Suc by measurable
          finally show "(λ((a, q), l). rec_list (T a) (F a) ((pair_to_list ∘ coProj i) l) q) ∈ (K ⨂M L) ⨂M (ΠS i∈{..<i}. M) →M N".
        qed
      qed
      finally show ?case .
    qed
  qed
qed

lemma measurable_rec_list_func2:
  fixes T :: "'a ⇒ ('b ⇒ 'd)"
    and F :: "'a ⇒ 'c ⇒ 'c list ⇒ ('b ⇒ 'd) ⇒ ('b ⇒ 'd)"
  assumes "(λ(a,b). T a b) ∈ K ⨂M L →M N "
    and "⋀i g. (λ (a, q, l). g a q l) ∈ K ⨂M L ⨂M (ΠS i∈{..<i}. M) →M N
 ⟹ (λ(a,b,x,l). (F a x ((pair_to_list o (coProj i)) l)) (λq. (g a q l)) b) ∈ K ⨂M L ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
    (*The condition is bit too strong*)
  shows "(λ(a,b,xs). (rec_list (T a) (F a)) xs b) ∈ K ⨂M L ⨂M (listM M) →M N"
proof-
  {
    fix i :: nat and g
    assume g: "(λ ((a, q), l). g a q l) ∈ (K ⨂M L) ⨂M (ΠS i∈{..<i}. M) →M N"
    have "(λ (a, q, l). g a q l) = (λ ((a, q), l). g a q l) o (λ (a, q, l). ((a, q), l))"
      by auto
    also have "... ∈ K ⨂M L ⨂M (ΠS i∈{..<i}. M) →M N"
      using g by measurable
    finally have g2: "(λ(a, q, l). g a q l) ∈ K ⨂M L ⨂M (ΠS i∈{..<i}. M) →M N".

    hence m: "(λ(a,b,x,l). (F a x ((pair_to_list o (coProj i)) l)) (λq. (g a q l)) b) ∈ K ⨂M L ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
      using assms(2) by measurable
    have "(λ((a,b),x,l). (F a x ((pair_to_list o (coProj i)) l)) (λq. (g a q l)) b) = ((λ(a,b,x,l). (F a x ((pair_to_list o (coProj i)) l)) (λq. (g a q l)) b)) o (λ((a,b),x,l).(a,b,x,l))"by auto
    also have "... ∈ (K ⨂M L) ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
      using m by measurable
    finally have F: "(λ((a, b), x, l). F a x ((pair_to_list ∘ coProj i) l) (λq. g a q l) b) ∈ (K ⨂M L) ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N".
  }
  note 2 = this
  have 3: "(λ((a,b),xs). (rec_list (T a) (F a)) xs b) ∈ (K ⨂M L) ⨂M (listM M) →M N"
    by(rule measurable_rec_list_func2'[OF assms(1) 2],auto)
  have "(λ(a,b,xs). (rec_list (T a) (F a)) xs b) = (λ((a,b),xs). (rec_list (T a) (F a)) xs b) o (λ(a,b,xs).((a,b),xs))"
    by auto
  also have "... ∈ K ⨂M L ⨂M (listM M) →M N"using 3 by measurable
  finally show "(λ(a, b, xs). rec_list (T a) (F a) xs b) ∈ K ⨂M L ⨂M listM M →M N".
qed

lemma measurable_rec_list'_func:
  fixes T :: "('c ⇒ 'd)"
    and F :: "'b ⇒ 'b list ⇒ ('c ⇒ 'd) ⇒ ('c ⇒ 'd)"
  assumes "T ∈ K →M N "
    and "⋀i g. g ∈ K ⨂M (ΠS i∈{..<i}. M) →M N
 ⟹ (λp. (F (fst (snd p)) (pair_to_list (coProj i(snd (snd (p))))) (λq. (g (q,snd (snd (p)))))) (fst p)) ∈ K ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
    (*The condition is bit too strong*)
  shows "(λp. (rec_list T F) (snd p) (fst p)) ∈ K ⨂M (listM M) →M N"
proof(subst measurable_iff_pair_to_list_plus,subst measurable_iff_dist_laws)
  show "countable (UNIV :: nat set)"by auto
  show "(λp. rec_list T F (snd p) (fst p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ dist_law_A UNIV (λn. ΠS i∈{..<n}. M) K ∈ (⨿M i∈UNIV. K ⨂M (ΠS i∈{..<i}. M)) →M N"
    unfolding dist_law_A_def2
  proof(subst coprod_measurable_iff, intro ballI)
    fix i :: nat assume "i ∈ UNIV"
    show "(λp. rec_list T F (snd p) (fst p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj i ∈ K ⨂M (ΠS i∈{..<i}. M) →M N"
    proof(induction i)
      case 0
      {
        fix p :: "(_ × (nat⇒_))" assume "p ∈ space (K ⨂M (ΠS i∈{..<0}. M))"

        hence "(snd p) = (λ n. undefined)"
          unfolding space_pair_measure space_prod_initial_source by auto
        hence "((λp. rec_list T F (snd p) (fst p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj 0) p = T (fst p)"
          by (auto simp: case_prod_beta comp_def coProj_def)
      }note * = this
      thus ?case
        by(subst measurable_cong[OF *],auto intro: assms measurable_compose)
    next
      case (Suc i)
      have eq1: "(λp. (rec_list T F (pair_to_list (i,(snd p)))) (fst p)) = (λp. rec_list T F (snd p) (fst p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj i"
        by (auto simp: coProj_def comp_def)
      also have "... ∈ K ⨂M (ΠS i∈{..<i}. M) →M N"using local.Suc by blast
      finally have meas1: "(λp. (rec_list T F (pair_to_list (i,(snd p)))) (fst p)) ∈ K ⨂M (ΠS i∈{..<i}. M) →M N".
      {
        fix p :: "(_ × (nat⇒_))" assume "p ∈ space (K ⨂M (ΠS i∈{..<Suc i}. M))"
        hence "(pair_to_list (Suc i,snd p)) = ((snd p 0) # (pair_to_list (i,λn. (snd p)(Suc n))))"
          by auto
        hence "((λp. rec_list T F (snd p) (fst p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj (Suc i)) p =
 rec_list T F ((snd p 0) # (pair_to_list (i,λn. (snd p)(Suc n))))(fst p)
 "
          by (auto simp: coProj_def)
        also have "... = F (snd p 0) (pair_to_list (i,λn. (snd p)(Suc n))) (rec_list T F (pair_to_list (i,λn. (snd p)(Suc n)))) (fst p)"
          by auto
        finally have "((λp. rec_list T F (snd p) (fst p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj (Suc i)) p = ((λp. F (fst (snd p)) (pair_to_list (coProj i (snd (snd p)))) (λq. rec_list T F (pair_to_list (i, snd (q, snd (snd p)))) (fst (q, snd (snd p)))) (fst p)) o (λ p. (fst p,snd p 0, λn. (snd p)(Suc n)))) p"
          by (auto simp: coProj_def)
      }note * = this
      show ?case
      proof(subst measurable_cong[OF *])
        show "⋀ w. w ∈ space (K ⨂M (ΠS i∈{..<Suc i}. M)) ⟹ w ∈ space (K ⨂M (ΠS i∈{..<Suc i}. M))"by auto
        show "(λp. F (fst (snd p)) (pair_to_list (coProj i (snd (snd p)))) (λq. rec_list T F (pair_to_list (i, snd (q, snd (snd p)))) (fst (q, snd (snd p)))) (fst p)) ∘ (λp. (fst p, snd p 0, λn. snd p (Suc n)))
 ∈ K ⨂M (ΠS i∈{..<Suc i}. M) →M N"
        proof(rule measurable_comp)
          show "(λp. F (fst (snd p)) (pair_to_list (coProj i (snd (snd p)))) (λq. rec_list T F (pair_to_list (i, snd (q, snd (snd p)))) (fst (q, snd (snd p)))) (fst p)) ∈ K ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
            using assms(2)[OF meas1] by auto
          show "(λp. (fst p, snd p 0, λn. snd p (Suc n))) ∈ K ⨂M (ΠS i∈{..<Suc i}. M) →M K ⨂M M ⨂M (ΠS i∈{..<i}. M) "
          proof(intro measurable_pair)
            have eq1: "fst ∘ (snd ∘ (λp. (fst p, snd p 0, λn. snd p (Suc n)))) = (λp. p 0) o snd"by auto
            have eq2: "snd ∘ (snd ∘ (λp. (fst p, snd p 0, λn. snd p (Suc n)))) = (λp. λn. p (Suc n)) o snd"by auto
            show "fst ∘ (λp. (fst p, snd p 0, λn. snd p (Suc n))) ∈ K ⨂M (ΠS i∈{..<Suc i}. M) →M K"by(auto simp: comp_def)
            show "fst ∘ (snd ∘ (λp. (fst p, snd p 0, λn. snd p (Suc n)))) ∈ K ⨂M (ΠS i∈{..<Suc i}. M) →M M"
              by(subst eq1, auto intro: measurable_comp measurable_prod_initial_source_projections)
            show "snd ∘ (snd ∘ (λp. (fst p, snd p 0, λn. snd p (Suc n)))) ∈ K ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<i}. M)"
            proof(subst eq2,rule measurable_comp)
              show "snd ∈ K ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<Suc i}. M)"by auto
              show "(λp n. p (Suc n)) ∈ (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<i}. M)"
                by(rule measurable_prod_initial_sourceI,unfold space_prod_initial_source, auto intro :measurable_prod_initial_source_projections)
            qed
          qed
        qed
      qed
    qed
  qed
qed

lemma measurable_rec_list''_func:
  fixes T :: "('c ⇒ 'd)"
    and F :: "'b ⇒ 'b list ⇒ ('c ⇒ 'd) ⇒ ('c ⇒ 'd)"
  assumes "T ∈ K →M N"
    and "⋀i g. (λ(q,v). g q v) ∈ K ⨂M (ΠS i∈{..<i}. M) →M N
 ⟹ (λ(x,y,xs). (F y (pair_to_list (coProj i xs)) (λq. (g q xs))) x) ∈ K ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
  shows "(λ(x,xs). (rec_list T F) xs x) ∈ K ⨂M (listM M) →M N"
proof-
  {
    fix i :: nat and g assume "g ∈ K ⨂M (ΠS i∈{..<i}. M) →M N"
    hence "(λx. F (fst (snd x)) (pair_to_list (coProj i (snd (snd x)))) (λq. g (q, snd (snd x))) (fst x)) ∈ K ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"
      using assms(2)[of"(λq xs. g (q, xs))"] by (auto simp: case_prod_beta')
  }
  hence "⋀i g. g ∈ K ⨂M (ΠS i∈{..<i}. M) →M N ⟹ (λx. F (fst (snd x)) (pair_to_list (coProj i (snd (snd x)))) (λq. g (q, snd (snd x))) (fst x)) ∈ K ⨂M M ⨂M (ΠS i∈{..<i}. M) →M N"by auto
  thus ?thesis using assms(1) measurable_rec_list'_func by measurable
qed

lemma measurable_rec_list':
  assumes "F ∈ (N ⨂M M ⨂M (listM M) →M N)"
  shows "(λp. (rec_list (fst p) (λ y xs x. F(x,y,xs)) (snd p))) ∈ N ⨂M (listM M) →M N"
proof(subst measurable_iff_list_and_pair_plus, subst measurable_iff_dist_laws measurable_iff_dist_laws)
  show "countable (UNIV :: nat set)"by auto
  show "(λp. rec_list (fst p) (λy xs x. F (x, y, xs)) (snd p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ dist_law_A UNIV (λn. ΠS i∈{..<n}. M) N ∈ (⨿M i∈UNIV. N ⨂M (ΠS i∈{..<i}. M)) →M N"
    unfolding dist_law_A_def2
  proof(subst coprod_measurable_iff, intro ballI)
    fix i :: nat assume "i ∈ UNIV"
    show "(λp. rec_list (fst p) (λy xs x. F (x, y, xs)) (snd p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj i ∈ N ⨂M (ΠS i∈{..<i}. M) →M N"
    proof(induction i)
      case 0
      {
        fix p :: "(_ × (nat⇒_))" assume "p ∈ space (N ⨂M (ΠS i∈{..<0}. M))"
        hence "(snd p) = (λ n. undefined)"
          unfolding space_pair_measure space_prod_initial_source by auto
        hence "((λp. rec_list (fst p) (λy xs x. F (x, y, xs)) (snd p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj 0) p = fst p"
          by (auto simp: case_prod_beta comp_def coProj_def)
      }note * = this
      show ?case
        by(subst measurable_cong[OF *],auto)
    next
      case (Suc i)
      define X where "X = (λp. rec_list (fst p) (λy xs x. F (x, y, xs)) (snd p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj i"
      hence X[measurable]: "X ∈ N ⨂M (ΠS i∈{..<i}. M) →M N"
        by (auto simp: local.Suc)
      {
        fix p :: "(_ × (nat⇒_))" assume "p ∈ space (N ⨂M (ΠS i∈{..<Suc i}. M))"
        hence
          "((λp. rec_list (fst p) (λy xs x. F (x, y, xs)) (snd p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj (Suc i)) p
 = rec_list (fst p) (λy xs x. F (x, y, xs)) (pair_to_list (Suc i, snd p))"
          by (auto simp: case_prod_beta comp_def coProj_def)
        also have "... =F(((λp. rec_list (fst p) (λy xs x. F (x, y, xs)) (snd p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj i)(fst p , λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n)))"
          by(auto simp: case_prod_beta comp_def coProj_def)
        also have "... = (F o (λ p. (X (fst p , λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n))))) p"
          unfolding X_def by auto
        finally have "((λp. rec_list (fst p) (λy xs x. F (x, y, xs)) (snd p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj (Suc i)) p = (F o (λ p. (X (fst p , λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n))))) p".
      }note * = this

      show "(λp. rec_list (fst p) (λy xs x. F (x, y, xs)) (snd p)) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ (λp. (fst (snd p), fst p, snd (snd p))) ∘ coProj (Suc i) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M N"
      proof(subst measurable_cong[OF *])
        show "⋀w. w ∈ space (N ⨂M (ΠS i∈{..<Suc i}. M)) ⟹ w ∈ space (N ⨂M (ΠS i∈{..<Suc i}. M))"by auto
        show "F ∘ (λp. (X (fst p, λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n)))) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M N"
        proof(intro measurable_comp)
          show "F ∈ (N ⨂M M ⨂M (listM M) →M N)"by (auto simp: assms(1))
          show "(λp. (X (fst p, λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n)))) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M N ⨂M M ⨂M listM M"
          proof(intro measurable_pair)
            have "fst ∘ (snd ∘ (λp. (X (fst p, λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n))))) = (λp. p 0) o snd"by auto
            also have "... ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M M"
            proof(rule measurable_comp)
              show "snd ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<Suc i}. M)"by auto
              show "(λp. p 0) ∈ (ΠS i∈{..<Suc i}. M) →M M"
                unfolding prod_initial_source_def by(rule measurable_initial_source1,auto)
            qed
            finally show "fst ∘ (snd ∘ (λp. (X (fst p, λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n))))) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M M".

            have "snd ∘ (snd ∘ (λp. (X (fst p, λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n))))) = (λp. pair_to_list (i, λn. p (Suc n))) o snd"by auto
            also have "... ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M listM M"
            proof(rule measurable_comp)
              show "snd ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<Suc i}. M)"by auto
              have "(λp. pair_to_list (i, λn. p (Suc n))) = pair_to_list o (coProj i) o (λp. (λn. p (Suc n)))"
                by(auto simp: comp_def coProj_def)
              also have "... ∈ (ΠS i∈{..<Suc i}. M) →M listM M"
              proof(subst measurable_iff_prod_initial_source,intro measurable_comp)
                show "(λp n. if n = 0 then fst p else snd p (n - 1)) ∈ M ⨂M (ΠS i∈{..<i}. M) →M (ΠS i∈{..<Suc i}. M)"
                  by(auto simp: measurable_integrate_prod_initial_source_Suc_n)
                show "pair_to_list ∈ (⨿M n∈UNIV. ΠS i∈{..<n}. M) →M (listM M)"
                  by(auto simp: pair_to_list_measurable)
                show "coProj i ∈(ΠS i∈{..<i}. M) →M (⨿M n∈UNIV. ΠS i∈{..<n}. M)"
                  by auto
                show "(λp n. p (Suc n)) ∈ (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<i}. M)"
                  by(auto simp: measurable_projection_shift)
              qed
              finally show "(λp. pair_to_list (i, λn. p (Suc n))) ∈ (ΠS i∈{..<Suc i}. M) →M listM M".
            qed
            finally show "snd ∘ (snd ∘ (λp. (X (fst p, λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n))))) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M listM M".
            have "fst ∘ (λp. (X (fst p, λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n)))) = X o (λp. (fst p, λn. snd p (Suc n)))"by auto
            also have "... ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M N"
            proof(rule measurable_comp)
              show "X ∈ N ⨂M (ΠS i∈{..<i}. M) →M N"by(auto simp: X)
              show "(λp. (fst p, λn. snd p (Suc n))) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M N ⨂M (ΠS i∈{..<i}. M)"
              proof(rule measurable_pair)
                show "fst ∘ (λp. (fst p, λn. snd p (Suc n))) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M N"
                  by (auto simp: measurable_cong_simp)
                have "snd ∘ (λp. (fst p, λn. snd p (Suc n))) = (λp n. p (Suc n)) o snd"by auto
                also have "... ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<i}. M)"
                proof(rule measurable_comp)
                  show "snd ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<Suc i}. M)"by auto
                  show "(λp n. p (Suc n)) ∈ (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<i}. M)"
                    by(auto simp: measurable_projection_shift)
                qed
                finally show "snd ∘ (λp. (fst p, λn. snd p (Suc n))) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M (ΠS i∈{..<i}. M)".
              qed
            qed
            finally show "fst ∘ (λp. (X (fst p, λn. snd p (Suc n)), snd p 0, pair_to_list (i, λn. snd p (Suc n)))) ∈ N ⨂M (ΠS i∈{..<Suc i}. M) →M N".
          qed
        qed
      qed
    qed
  qed
qed

lemma measurable_rec_list'2:
  assumes "(λp. (F (fst (snd p)) (snd (snd p)) (fst p))) ∈ (N ⨂M M ⨂M (listM M) →M N)"
  shows "(λp. (rec_list (fst p) F (snd p))) ∈ N ⨂M (listM M) →M N"
  using measurable_rec_list'[OF assms] by auto

lemma measurable_rec_list:
  assumes "F ∈ (N ⨂M M ⨂M (listM M) →M N)"
    and "T ∈ space N"
  shows "rec_list T (λ y xs x. F(x,y,xs)) ∈ (listM M) →M N"
proof-
  have "rec_list T (λ y xs x. F(x,y,xs)) = (λp. (rec_list (fst p) (λ y xs x. F(x,y,xs)) (snd p))) o (λ r.(T, r))"
    by auto
  also have "... ∈ (listM M) →M N"
    using measurable_rec_list' assms by measurable
  finally show ?thesis .
qed

lemma measurable_rec_list2:
  assumes "(λp. (F (fst (snd p)) (snd (snd p)) (fst p))) ∈ (N ⨂M M ⨂M (listM M) →M N)"
    and "T ∈ space N"
  shows "rec_list T F ∈ (listM M) →M N"
  using measurable_rec_list[OF assms] by auto

lemma measurable_rec_list''':
  assumes "(λ(x,y,xs). F x y xs) ∈ N ⨂M M ⨂M (listM M) →M N"
    and "T ∈ space N"
  shows "rec_list T (λ y xs x. F x y xs) ∈ (listM M) →M N"
  using measurable_rec_list[OF assms] by fastforce

subsubsection ‹ Measurability of @{term case_list} ›

lemma measurable_case_list[measurable(raw)]:
  assumes [measurable]:"(λp. (F (fst p) (snd p))) ∈ M ⨂M (listM M) →M N "
    and "T ∈ space N"
  shows "case_list T F ∈ (listM M) →M N"
proof(subst measurable_iff_list_and_pair, subst coprod_measurable_iff, rule ballI)
  note [measurable] = measurable_decompose_prod_initial_source_Suc_n
  fix i :: nat assume i: "i ∈ UNIV"
  show "case_list T F ∘ pair_to_list ∘ coProj i ∈ (ΠS i∈{..<i}. M) →M N"
    unfolding comp_def coProj_def
  proof(induction i)
    case 0
    thus "(λx. case pair_to_list (0, x) of [] ⇒ T | z # zs ⇒ F z zs) ∈ (ΠS i∈{..<0}. M) →M N"
      using assms(2) by auto
  next
    case (Suc i)
    {
      fix y assume "y ∈ space (ΠS i∈{..<Suc i}. M)"
      then obtain z zs where pair: "pair_to_list (Suc i, y) = z # zs" and z : "z = y 0" and zs: "zs = pair_to_list(i, (λn :: nat. y(Suc n)))"
        by auto
      hence "(λx. case pair_to_list (Suc i, x) of [] ⇒ T | z # zs ⇒ F z zs) y = F z zs"
        by auto
      also have "... = ((λp. (F (fst p) (snd p))) o (λ p. ((fst p),(pair_to_list o (coProj i))(snd p))) o (λ f. (f 0, (λ n. f (Suc n))))) y"
        by (auto simp: z zs coProj_def)
      finally have "(case pair_to_list (Suc i, y) of [] ⇒ T | z # zs ⇒ F z zs) = ((λp. F (fst p) (snd p)) ∘ (λp. (fst p, (pair_to_list ∘ coProj i) (snd p))) ∘ (λf. (f 0, λn. f (Suc n)))) y".
    }note * = this
    show ?case
      unfolding coProj_def
    proof(subst measurable_cong[OF *])
      show "⋀w. w ∈ space (ΠS i∈{..<Suc i}. M) ⟹ w ∈ space (ΠS i∈{..<Suc i}. M)"
        by auto
      show "(λp. F (fst p) (snd p)) ∘ (λp. (fst p, (pair_to_list ∘ coProj i) (snd p))) ∘ (λf. (f 0, λn. f (Suc n))) ∈ (ΠS i∈{..<Suc i}. M) →M N"
        unfolding comp_def using pair_to_list_measurable assms by measurable
    qed
  qed
qed

lemma measurable_case_list2[measurable]:
  assumes [measurable]:"(λ(x,b,bl). g x b bl) ∈ N ⨂M L ⨂M (listM L) →M M"
    and [measurable]:"a ∈ N →M M"
  shows "(λ(x,xs). case_list (a x) (g x) xs) ∈ N ⨂M (listM L) →M M"
proof(subst measurable_iff_list_and_pair_plus, subst measurable_iff_dist_laws)
  note [measurable] = pair_to_list_measurable list_to_pair_measurable dist_law_A_measurable measurable_projection_shift
  show "countable (UNIV :: nat set)"
    by auto
  show "(λ(x, y). case_list (a x) (g x) y) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ dist_law_A UNIV (λn. ΠS i∈{..<n}. L) N ∈ (⨿M i∈UNIV. N ⨂M (ΠS i∈{..<i}. L)) →M M"
  proof(subst coprod_measurable_iff,rule ballI)
    fix i :: nat assume i: "i ∈ (UNIV :: nat set)"
    show "(λ(x, y). case_list (a x) (g x) y) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ dist_law_A UNIV (λn. ΠS i∈{..<n}. L) N ∘ coProj i ∈ N ⨂M (ΠS i∈{..<i}. L) →M M"
    proof(induction i)
      case 0
      {
        fix w :: "'a × (nat ⇒ 'b)" assume "w ∈ space (N ⨂M (ΠS i∈{..<0}. L))"
        have "((λb. case b of (x, []) ⇒ a x | (x, a # b) ⇒ g x a b) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ dist_law_A UNIV (λn. ΠS i∈{..<n}. L) N ∘ coProj 0) w = (a (fst w))"
          unfolding comp_def coProj_def dist_law_A_def2 pair_to_list.simps by auto
      }note * = this
      show ?case
        using assms by(subst measurable_cong[OF *],measurable)
    next
      case (Suc i)
      {
        fix w :: "'a × (nat ⇒ 'b)" assume "w ∈ space (N ⨂M (ΠS i∈{..<Suc i}. L))"
        have "((λb. case b of (x, []) ⇒ a x | (x, a # b) ⇒ g x a b) ∘ (λq. (fst q, pair_to_list (snd q))) ∘ dist_law_A UNIV (λn. ΠS i∈{..<n}. L) N ∘ coProj (Suc i)) w = ((λ(x,b,bl). g x b bl) ∘ (λ w. (fst w, (((snd w) 0) , (pair_to_list (i, λ n. (snd w)(Suc n))))))) w "
          unfolding comp_def coProj_def dist_law_A_def2 pair_to_list.simps by auto
      }note * = this
      show ?case
      proof(subst measurable_cong[OF *])
        show "⋀w. w ∈ space (N ⨂M (ΠS i∈{..<Suc i}. L)) ⟹ w ∈ space (N ⨂M (ΠS i∈{..<Suc i}. L))"
          by auto
        show "(λ(x, xa, y). g x xa y) ∘ (λw. (fst w, snd w 0, pair_to_list (i, λn. snd w (Suc n)))) ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M M"
        proof(rule measurable_comp)
          show "(λw. (fst w, snd w 0, pair_to_list (i, λn. snd w (Suc n)))) ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M N ⨂M (L ⨂M (listM L))"
          proof(intro measurable_pair)
            show "fst ∘ (λw. (fst w, snd w 0, pair_to_list (i, λn. snd w (Suc n)))) ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M N"
              by(auto simp: comp_def)
            have "(λx. snd x 0) = ((λf. f 0) o snd)"
              by auto
            also have "... ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M L"
              by(auto intro: measurable_comp measurable_prod_initial_source_projections)
            finally have "(λx. snd x 0) ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M L".
            thus"fst ∘ (snd ∘ (λw. (fst w, snd w 0, pair_to_list (i, λn. snd w (Suc n))))) ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M L"
              unfolding comp_def prod_initial_source_def using pair_to_list_measurable[of L] by auto
            have "(λx. pair_to_list (i, λn. snd x (Suc n))) = pair_to_list o (coProj i) o (λ f. λn. f (Suc n)) o snd"
              by(auto simp: comp_def coProj_def)
            also have "... ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M (listM L)"
            proof(intro measurable_comp)
              show "coProj i ∈ (ΠS i∈{..<i}. L) →M ((⨿M i∈UNIV. ΠS i∈{..<i}. L))"
                by auto
            qed(auto)
            finally have "(λx. pair_to_list (i, λn. snd x (Suc n))) ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M listM L".
            thus"snd ∘ (snd ∘ (λw. (fst w, snd w 0, pair_to_list (i, λn. snd w (Suc n))))) ∈ N ⨂M (ΠS i∈{..<Suc i}. L) →M listM L"
              unfolding comp_def by auto
          qed
          show "(λ(x, xa, y). g x xa y) ∈ N ⨂M L ⨂M listM L →M M"
            by (auto simp: assms)
        qed
      qed
    qed
  qed
qed

lemma measurable_case_list':
  assumes "(λ(x,b,bl). g x b bl) ∈ N ⨂M L ⨂M (listM L) →M M"
    and "a ∈ N →M M"
    and "l ∈ N →M listM L"
  shows "(λx. case_list (a x) (g x) (l x)) ∈ N →M M"
  using measurable_case_list2 assms by measurable

subsubsection ‹ Measurability of @{term foldr} ›

lemma measurable_foldr:
  assumes "(λ (x,y). F x y) ∈ (N ⨂M M →M N)"
  shows "(λ (T,xs). foldr (λ x y. F y x) xs T) ∈ N ⨂M (listM M) →M N"
proof-
  have 1: "(λ (x ,y , xs). (λ y xs x. F x y) y xs x) ∈ N ⨂M M ⨂M listM M →M N"
    using assms by measurable
  {
    fix T xs
    have "(foldr (λ x y. F y x) xs T) = (rec_list T (λ y xs x. F x y) xs)"
      by(induction xs,auto)
  }
  hence "(λ (T,xs). foldr (λ x y. F y x) xs T) = (λ (T,xs). (rec_list T (λ y xs x. (λ (x ,y , xs). (λ y xs x. F x y) y xs x)(x,y,xs)) xs))"
    by auto
  also have "... ∈ N ⨂M (listM M) →M N"
    using measurable_rec_list'[OF 1 ] by measurable
  finally show ?thesis .
qed

subsubsection ‹ Measurability of @{term append} ›

lemma measurable_append[measurable]:
  shows "(λ (xs,ys). xs @ ys) ∈ (listM M) ⨂M (listM M) →M (listM M)"
proof-
  {
    fix xs ys :: "'a list"
    have "xs @ ys = (rec_list ys (λx xs ys. x # ys)) xs"
      by(induction xs,auto)
  }
  hence "(λ (xs :: 'a list,ys :: 'a list). xs @ ys) = (λp. rec_list (fst p) (λx xs ys. x # ys) (snd p)) o (λ(xs, ys). (ys, xs))"
    by auto
  also have "... ∈ (listM M) ⨂M (listM M) →M (listM M)"
    using measurable_rec_list'2 by measurable
  finally show ?thesis .
qed

subsubsection ‹ Measurability of @{term rev} ›

lemma measurable_rev[measurable]:
  shows "rev ∈ (listM M) →M (listM M)"
proof-
  note [measurable] = measurable_pair listM_Nil
  have "rev = (λ xs :: 'a list. rec_list [] (λy xs x. (((λ(xs, ys). xs @ ys)o (λp. (fst p,[fst (snd p)]))) (x, y, xs))) xs)"
    by (auto simp add: rev_def)
  also have "... ∈ listM M →M listM M"
    by(rule measurable_rec_list,measurable)
  finally show ?thesis .
qed

subsubsection ‹ Measurability of @{term concat}, that is, the bind of the list monad›

lemma measurable_concat[measurable]:
  shows "concat ∈ listM (listM M) →M (listM M)"
proof-
  note [measurable] = measurable_append listM_Nil
  have "concat = (λ xs :: 'a list list. rec_list [] (λy xs x. (((λ(xs, ys). xs @ ys) o (λp. (fst (snd p), fst p))) (x, y, xs))) xs)"
    by (auto simp add: concat_def comp_def)
  also have "... ∈ listM (listM M) →M listM M"
    by(rule measurable_rec_list,measurable)
  finally show ?thesis .
qed

subsubsection ‹ Measurability of @{term map}, the functor part of the list monad›

lemma measurable_map[measurable]:
  assumes [measurable]: "f ∈ M →M N "
  shows "(map f) ∈ (listM M) →M (listM N)"
proof-
  note [measurable] = measurable_pair listM_Nil
  {
    fix xs  :: "'a list"
    have "map f xs = (rec_list [] (λx xs ys. (f x) # ys)) xs"
      by(induction xs,auto)
  }
  hence "(map f) = (λp. (rec_list [] (λy' xs' x'. ((λ (x,xs). x # xs) o (λp. (f (fst (snd p)), fst p))) (x', y', xs')) p))"
    by auto
  also have "... ∈ listM M →M listM N"
    by(rule measurable_rec_list, measurable)
  finally show ?thesis.
qed

subsubsection ‹ Measurability of @{term length} ›

lemma measurable_length[measurable]:
  shows "length ∈ listM M →M count_space (UNIV :: nat set)"
proof -
  {
    fix xs :: "'a list"
    have "length xs = (rec_list 0 (λy xs x. (Suc o fst) (x, y ,xs))) xs "
      by(induction xs,auto)
  }
  hence "length = (λ xs :: 'a list.(rec_list 0 (λy xs x :: nat. (Suc o fst) (x, y ,xs)) xs))"
    by auto
  also have "... ∈ listM M →M count_space UNIV"
    by(rule measurable_rec_list, auto)
  finally show ?thesis .
qed

lemma sets_listM_length[measurable]:
  shows "{xs. xs ∈ space (listM M) ∧ length xs = n} ∈ sets (listM M)"
  by measurable

subsubsection ‹ Measurability of @{term foldl} ›

lemma measurable_foldl [measurable]:
  assumes [measurable]:"(λ(x,y). F y x) ∈ (M ⨂M N →M N)"
  shows "(λ (T,xs). foldl F T xs) ∈ N ⨂M (listM M) →M N"
proof(subst foldl_conv_foldr)
  have "(λ(T, xs). foldr (λx y. F y x) (rev xs) T) = (λ(T, xs). foldr (λx y. F y x) xs T) o (λ(T, xs). (T, rev xs))"
    by auto
  also have "... ∈ N ⨂M listM M →M N"
    using measurable_foldr by measurable
  finally show "(λ(T, xs). foldr (λx y. F y x) (rev xs) T) ∈ N ⨂M listM M →M N".
qed

subsubsection ‹ Measurability of @{term fold} ›

lemma measurable_fold [measurable]:
  assumes [measurable]: "(λ(x,y). F x y) ∈ (M ⨂M N→M N)"
  shows "(λ (T,xs). fold F xs T) ∈ N ⨂M (listM M) →M N"
proof-
  have "(λ (T,xs). fold F xs T) = (λ (T,xs). foldr F xs T) o (λ (T,xs). (T, rev xs))"
    by (auto simp add: foldr_conv_fold)
  also have "... ∈ N ⨂M listM M →M N"
    using measurable_foldr by measurable
  finally show "(λ(T, xs). fold F xs T) ∈ N ⨂M listM M →M N".
qed

subsubsection ‹ Measurability of @{term drop} ›

lemma measurable_drop[measurable]:
  shows "drop n ∈ listM M →M listM M"
proof-
  have "(λa. []) ∈ space (PiM UNIV (λa. listM M))"
    using listM_Nil space_PiM by fastforce
  with measurable_rec_list''' listM_Nil space_PiM
  show ?thesis unfolding drop_def by measurable
qed

lemma measurable_drop'[measurable]:
  shows "(λ (n,xs). drop n xs) ∈ count_space (UNIV :: nat set) ⨂M listM M →M listM M"
  by measurable

subsubsection ‹ Measurability of @{term take} ›

lemma measurable_take[measurable]:
  shows "take n ∈ listM M →M listM M"
proof-
  have "(λ (n,xs). take n xs) = (λ (n,xs). rev (drop (length xs - n) (rev xs)))"
    by (metis rev_swap rev_take)
  also have "... ∈ count_space (UNIV :: nat set) ⨂M listM M →M listM M"
    using measurable_drop by measurable
  finally show ?thesis by measurable
qed

lemma measurable_take'[measurable]:
  shows "(λ (n,xs). take n xs) ∈ count_space (UNIV :: nat set) ⨂M listM M →M listM M"
  by measurable

subsubsection ‹ Measurability of @{term nth} plus a default value ›

text ‹ Since the {@term undefined} is harmful to prove measurability, we introduce the total function version of @{term nth} that returns a fixed default value when the nth element is not found. ›

primrec nth_total  :: "'a ⇒ 'a list ⇒ nat ⇒ 'a" where
  "nth_total d [] n = d" |
  "nth_total d (x # xs) n = (case n of 0 ⇒ x | Suc k ⇒ nth_total d xs k)"

value"nth_total (15 :: nat) [] (0 :: nat)  :: nat"
value"nth_total (15 :: nat) [1] (0 :: nat)  :: nat"
value"nth_total (15 :: nat) [1,2,3] (0 :: nat)  :: nat"
value"nth_total (15 :: nat) [1,2,3] (1 :: nat)  :: nat"
value"nth_total (15 :: nat) [1,2,3] (2 :: nat)  :: nat"
value"nth_total (15 :: nat) [1,2,3] (3 :: nat)  :: nat"
  (* value"nth [] (0 :: nat)  :: nat" *)
value"nth [1] (0 :: nat)  :: nat"
value"nth [1,2,3] (0 :: nat)  :: nat"
value"nth [1,2,3] (1 :: nat)  :: nat"
value"nth [1,2,3] (2 :: nat)  :: nat"
  (* value"nth [1,2,3] (3 :: nat)  :: nat"*)

text ‹ The total version @{term nth_total} is the same as @{term nth} if the nth element exists and otherwise it returns the default value.  ›

lemma cong_nth_total_nth:
  shows "((n :: nat) < length xs ∧ 0 < length xs) ⟹ nth_total d xs n = nth xs n"
proof(induction xs arbitrary :n)
  case Nil
  thus ?case by auto
next
  case (Cons a xs)
  show "nth_total d (a # xs) n = (a # xs) ! n"
  proof(cases"n=0")
    case True
    thus ?thesis by auto
  next
    case False
    hence 1: "n = Suc (n-1)" and 3: "n-1 < length xs"
      using Cons(2) by auto
    hence 2: "nth_total d xs (n-1) = xs ! (n-1)"
      using Cons(1) by fastforce
    thus ?thesis unfolding nth_total.simps(2) nth.simps
      by (metis"2"Nitpick.case_nat_unfold)
  qed
qed

lemma cong_nth_total_default:
  shows "¬((n :: nat) < length xs ∧ 0 < length xs) ⟹ nth_total d xs n = d"
proof(induction xs arbitrary :n)
  case Nil
  thus ?case by auto
next
  case (Cons a xs)
  hence "0 < length (a # xs)" by auto
  then obtain m where n: "n = Suc m"
    using Cons.prems not0_implies_Suc by force
  thus ?case unfolding n nth_total.simps using Cons.IH[of m]
    using Cons.prems n by auto
qed

lemma nth_total_def2:
  shows " nth_total d xs n = (if (n < length xs ∧ 0 < length xs) then xs ! n else d)"
  using cong_nth_total_nth cong_nth_total_default by (metis (no_types))

context
  fixes d
begin

primrec nth_total'  :: "'a list ⇒ nat ⇒ 'a" where
  "nth_total' [] n = d" |
  "nth_total' (x # xs) n = (case n of 0 ⇒ x | Suc k ⇒ nth_total' xs k)"

lemma measurable_nth_total':
  assumes d: "d ∈ space M"
  shows "(λ (n,xs). nth_total' xs n) ∈ (count_space UNIV) ⨂M listM M →M M"
  unfolding nth_total'_def using assms
  by(intro  measurable_rec_list''_func, auto simp add: d)

lemma nth_total_nth_total':
  shows "nth_total d xs n = nth_total' xs n"
proof(induction xs arbitrary: n)
  case Nil
  thus ?case by auto
next
  case (Cons a xs)
  thus ?case unfolding nth_total'.simps nth_total.simps
    by meson
qed

end (*end of context*)

lemma measurable_nth_total[measurable]:
  assumes "d ∈ space M"
  shows "(λ (n,xs). nth_total d xs n) ∈ (count_space UNIV) ⨂M listM M →M M"
  by (auto simp: measurable_nth_total'[OF assms] nth_total_nth_total')

subsubsection ‹ Definition and Measurability of list insert. ›

definition list_insert  :: "'a ⇒ 'a list ⇒ nat ⇒ 'a list" where
  "list_insert x xs i = (take i xs) @ [x] @ (drop i xs)"

value"list_insert (15 :: nat) [] (0 :: nat)  :: nat list"
value"list_insert (15 :: nat) [] (1 :: nat)  :: nat list"
value"list_insert (15 :: nat) [1,2,3] (0 :: nat) :: nat list"
value"list_insert (15 :: nat) [1,2,3] (1 :: nat)  :: nat list"
value"list_insert (15 :: nat) [1,2,3] (2 :: nat) :: nat list"
value"list_insert (15 :: nat) [1,2,3] (3 :: nat) :: nat list"
value"list_insert (15 :: nat) [1,2,3] (4 :: nat) :: nat list"

lemma measurable_list_insert[measurable]:
  fixes n :: nat
  shows "(λ (d,xs). list_insert d xs n) ∈ M ⨂M listM M →M listM M"
  unfolding list_insert_def by measurable

primrec list_insert'  :: "'a ⇒ 'a list ⇒ nat ⇒ 'a list" where
  "list_insert' d [] n = [d]"
| "list_insert' d (x # xs) n = (case n of 0 ⇒ d # (x # xs) | Suc k ⇒ x # (list_insert' d xs k))"

lemma list_insert'_is_list_insert:
  shows "list_insert' x xs i = list_insert x xs i"
proof(induction xs arbitrary: x i)
  case Nil
  thus ?case unfolding list_insert_def by auto
next
  case (Cons a xs)
  thus ?case
  proof(cases"i = 0")
    case True
    thus ?thesis unfolding list_insert_def list_insert'.simps(2) take.simps(2) drop.simps(2) by auto
  next
    case False
    then obtain j :: nat where i: "i = Suc j"
      using not0_implies_Suc by auto
    thus ?thesis unfolding i list_insert_def list_insert'.simps(2) take.simps(2) drop.simps(2) using Cons
      using list_insert_def by fastforce
  qed
qed


definition list_exclude :: "nat⇒ 'a list ⇒ 'a list" where
  "list_exclude n xs = ((take n xs) @ (drop (Suc n) xs))"

value"list_exclude (0 :: nat) [] :: nat list"
value"list_exclude (0 :: nat) [1,2] :: nat list"
value"list_exclude (1 :: nat) [1,2] :: nat list"
value"list_exclude (2 :: nat) [1,2] :: nat list"

lemma measurable_list_exclude[measurable]:
  shows "list_exclude n ∈ listM M →M listM M"
  unfolding list_exclude_def by measurable

lemma insert_exclude:
  shows "n < length xs ⟹ xs ≠ [] ⟹ list_insert' (nth_total d xs n) (list_exclude n xs) n = xs"
  unfolding list_exclude_def
proof(induction xs arbitrary : d n)
  case Nil
  thus ?case by auto
next
  case (Cons a xs)
  thus "n < length (a # xs) ⟹ a # xs ≠ [] ⟹ list_insert' (nth_total d (a # xs) n) (take n (a # xs) @ drop (Suc n) (a # xs)) n = a # xs"
  proof(cases"xs = []")
    case True
    then have q: "a # xs = [a]" and "n = 0"
      using Cons by auto
    thus ?thesis
      by auto
  next
    case False
    thus "n < length (a # xs) ⟹ list_insert' (nth_total d (a # xs) n) (take n (a # xs) @ drop (Suc n) (a # xs)) n = a # xs"
    proof(induction n)
      case 0
      then obtain b ys where xs: "xs = b # ys"
        using list_to_pair.cases by auto
      thus ?case
        by auto
    next
      case (Suc n)
      have  "n < length xs"
        using Suc by auto
      thus ?case
        using False Cons(1) by auto
    qed
  qed
qed

subsubsection ‹ Measurability of @{term list_update}›

lemma update_insert_exclude:
  shows "n < length xs ⟹ xs ≠ [] ⟹ list_update xs n x = list_insert' x (list_exclude n xs) n"
proof(induction xs arbitrary : x n)
  case Nil
  thus ?case by auto
next
  case (Cons a xs)
  thus "n < length (a # xs) ⟹(a # xs) ≠ [] ⟹ list_update (a # xs) n x = list_insert' x (list_exclude n (a # xs)) n"
  proof(cases"xs = []")
    case True
    with Cons have q: "a # xs = [a]" and q2: "n = 0"by auto
    show ?thesis unfolding q q2 list_exclude_def by auto
  next
    case False
    thus "n < length (a # xs) ⟹(a # xs) ≠ [] ⟹ list_update (a # xs) n x = list_insert' x (list_exclude n (a # xs)) n"
    proof(induction n)
      case 0
      then obtain b ys where xs: "xs = b # ys"
        using list_to_pair.cases by auto
      show ?case unfolding xs list_exclude_def by auto
    next
      case (Suc n)
      have nn: "n < length xs"using Suc by auto
      thus ?case unfolding list_exclude_def list_insert'.simps(2) take.simps(2) drop.simps(2) list_update.simps(2)
        using Cons(1)
        by (metis Cons_eq_appendI False list_exclude_def list_insert'.simps(2) old.nat.simps(5))
    qed
  qed
qed

lemma list_update_def2:
  shows "list_update xs n x = If (n < length xs ∧ xs ≠ []) (list_insert' x (list_exclude n xs) n) xs"
proof(cases"(n < length xs ∧ xs ≠ [])")
  case True
  thus ?thesis by(subst update_insert_exclude,auto)
qed (auto simp: list_update_beyond)

lemma measurable_list_update[measurable]:
  shows "(λ (x,xs). list_update xs (n :: nat) x) ∈ M ⨂M (listM M) →M (listM M)"
proof-
  have 1 : "(λx. length (snd x)) ∈  (M ⨂M listM M) →M (count_space UNIV)"
    by auto
  have "(λx. snd x ≠ []) = (λxs. (length xs ≠ 0)) o snd"
    by auto
  also have "... ∈ (M ⨂M listM M) →M (count_space (UNIV :: bool set))"
    by measurable
  finally have "Measurable.pred (M ⨂M listM M) (λx. snd x ≠ [])".
  thus ?thesis
    unfolding  list_insert'_is_list_insert list_update_def2
    using 1 by auto
qed

subsubsection ‹ Measurability of @{term zip}›

lemma measurable_zip[measurable]:
  shows "(λ(xs,ys). (zip xs ys)) ∈ (listM M) ⨂M (listM N) →M (listM (M ⨂M N))"
  unfolding zip_def
  by(rule measurable_rec_list''_func,auto)

subsubsection ‹ Measurability of @{term map2}›

lemma measurable_map2[measurable]:
  assumes [measurable]: "(λ(x,y). f x y) ∈ M ⨂M M' →M N "
  shows "(λ(xs,ys). map2 f xs ys) ∈ (listM M) ⨂M (listM M') →M (listM N)"
  by auto

end