Theory Exponent_QuasiBorel

(*  Title:   Exponent_QuasiBorel.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)

subsection ‹Function Spaces›

theory Exponent_QuasiBorel
  imports "CoProduct_QuasiBorel"
begin

subsubsection ‹ Function Spaces  ›
definition exp_qbs_Mx :: "['a quasi_borel, 'b quasi_borel]  (real  'a => 'b) set" where
"exp_qbs_Mx X Y  {g :: real  'a  'b. case_prod g  Q Q X Q Y} "

definition exp_qbs :: "['a quasi_borel, 'b quasi_borel]  ('a  'b) quasi_borel" (infixr "Q" 61) where
"X Q Y  Abs_quasi_borel (X Q Y, exp_qbs_Mx X Y)"


lemma exp_qbs_f[simp]: "exp_qbs_Mx X Y  UNIV  (X :: 'a quasi_borel) Q (Y :: 'b quasi_borel)"
proof(auto intro!: qbs_morphismI)
  fix f α r
  assume h:"f  exp_qbs_Mx X Y"
           "α  qbs_Mx X"
  have "f r  α = (λy. case_prod f (r,y))  α"
    by auto
  also have "...  qbs_Mx Y"
    using qbs_morphism_Pair1'[of r "Q" "case_prod f" X Y] h
    by(auto simp: exp_qbs_Mx_def)
  finally show "f r  α  qbs_Mx Y" .
qed

lemma exp_qbs_closed1: "qbs_closed1 (exp_qbs_Mx X Y)"
proof(rule qbs_closed1I)
  fix a
  fix f
  assume h:"a  exp_qbs_Mx X Y"
           "f  real_borel M real_borel"
  have "a  f = (λr y. case_prod a (f r,y))" by auto
  moreover have "case_prod ...  Q Q X Q Y"
  proof -
    have "case_prod (λr y. case_prod a (f r,y)) = case_prod a  map_prod f id"
      by auto
    also have "...  Q Q X Q Y"
      using h
      by(auto intro!: qbs_morphism_comp qbs_morphism_map_prod simp: exp_qbs_Mx_def)
    finally show ?thesis .
  qed
  ultimately show "a  f  exp_qbs_Mx X Y"
    by (simp add: exp_qbs_Mx_def)
qed

lemma exp_qbs_closed2: "qbs_closed2 (X Q Y) (exp_qbs_Mx X Y)"
  by(auto intro!: qbs_closed2I qbs_morphism_snd'' simp: exp_qbs_Mx_def split_beta')

lemma exp_qbs_closed3:"qbs_closed3 (exp_qbs_Mx X Y)"
proof(rule qbs_closed3I)
  fix P :: "real  nat"
  fix Fi :: "nat  real  _"
  assume h:"i. P -` {i}  sets real_borel"
           "i. Fi i  exp_qbs_Mx X Y"
  show "(λr. Fi (P r) r)  exp_qbs_Mx X Y"
    unfolding exp_qbs_Mx_def
  proof(auto intro!: qbs_morphismI)
    fix α β
    assume h':"α  pair_qbs_Mx Q X "
    have 1:"i. (λ(r,x). Fi i r x)  α  qbs_Mx Y"
      using qbs_morphismE(3)[OF h(2)[simplified exp_qbs_Mx_def,simplified]] h'
      by(simp add: exp_qbs_Mx_def)
    have 2:"i. (P  (λr. fst (α r)))  -` {i}  sets real_borel"
      using separate_measurable[OF h(1)] h'
      by(auto intro!: measurable_separate simp: pair_qbs_Mx_def comp_def)
    show "(λ(r, y). Fi (P r) r y)  α  qbs_Mx Y"
      using qbs_closed3_dest[OF 2,of "λi. (λ(r,x). Fi i r x)  α",OF 1]
      by(simp add: comp_def split_beta')
  qed
qed


lemma exp_qbs_correct: "Rep_quasi_borel (exp_qbs X Y) = (X Q Y, exp_qbs_Mx X Y)"
  unfolding exp_qbs_def
  by(auto intro!: Abs_quasi_borel_inverse exp_qbs_f simp: exp_qbs_closed1 exp_qbs_closed2 exp_qbs_closed3)

lemma exp_qbs_space[simp]: "qbs_space (exp_qbs X Y) = X Q Y"
  by(simp add: qbs_space_def exp_qbs_correct)

lemma exp_qbs_Mx[simp]: "qbs_Mx (exp_qbs X Y) = exp_qbs_Mx X Y"
  by(simp add: qbs_Mx_def exp_qbs_correct)


lemma qbs_exp_morphismI:
  assumes "α β. α  qbs_Mx X 
                 β  pair_qbs_Mx real_quasi_borel Y 
                 (λ(r,x). (f  α) r x)  β  qbs_Mx Z"
   shows "f  X Q exp_qbs Y Z"
  using assms
  by(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def comp_def)

definition qbs_eval :: "(('a  'b) × 'a)   'b" where
"qbs_eval a  (fst a) (snd a)"

lemma qbs_eval_morphism:
  "qbs_eval  (exp_qbs X Y) Q X Q Y"
proof(rule qbs_morphismI,simp)
  fix f
  assume "f  pair_qbs_Mx (exp_qbs X Y) X"
  let ?f1 = "fst  f"
  let ?f2 = "snd  f"
  define g :: "real  real × _" 
    where "g  λr.(r,?f2 r)"
  have "g  qbs_Mx (real_quasi_borel Q X)"
  proof(auto simp add: pair_qbs_Mx_def)
    have "fst  g = id" by(auto simp add: g_def comp_def)
    thus "fst  g  real_borel M real_borel" by(auto simp add: measurable_ident)
  next
    have "snd  g = ?f2" by(auto simp add: g_def)
    thus "snd  g  qbs_Mx X" 
      using f  pair_qbs_Mx (exp_qbs X Y) X pair_qbs_Mx_def by auto
  qed
  moreover have "?f1  exp_qbs_Mx X Y"
    using f  pair_qbs_Mx (exp_qbs X Y) X
    by(simp add: pair_qbs_Mx_def)
  ultimately have "(λ(r,x). (?f1 r x))  g  qbs_Mx Y"
    by (auto simp add: exp_qbs_Mx_def qbs_morphism_def)
       (metis (mono_tags, lifting) case_prod_conv comp_apply cond_case_prod_eta)
  moreover have "(λ(r,x). (?f1 r x))  g = qbs_eval  f" 
    by(auto simp add: case_prod_unfold g_def qbs_eval_def)
  ultimately show "qbs_eval  f  qbs_Mx Y" by simp
qed

lemma curry_morphism:
 "curry  exp_qbs (X Q Y) Z Q exp_qbs X (exp_qbs Y Z)"
proof(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def)
  fix k α α'
  assume h:"(λ(r, xy). k r xy)  Q Q X Q Y Q Z"
           "α  pair_qbs_Mx Q X"
           "α'  pair_qbs_Mx Q Y"
  define β where
   "β  (λr. (fst (α (fst (α' r))),(snd (α (fst (α' r))), snd (α' r))))"
  have "(λ(x, y). ((λ(x, y). (curry  k) x y)  α) x y)  α' = (λ(r, xy). k r xy)  β"
    by(simp add: curry_def split_beta' comp_def β_def)
  also have "...  qbs_Mx Z"
  proof -
    have "β  qbs_Mx (Q Q X Q Y)"
      using h(2,3) qbs_closed1_dest[of _ _ "(λx. fst (α' x))"]
      by(auto simp: pair_qbs_Mx_def β_def comp_def)
    thus ?thesis
      using h by auto
  qed
  finally show "(λ(x, y). ((λ(x, y). (curry  k) x y)  α) x y)  α'  qbs_Mx Z" .
qed

lemma curry_preserves_morphisms:
  assumes "f  X Q Y Q Z"
  shows "curry f  X Q exp_qbs Y Z"
  by(rule qbs_morphismE(2)[OF curry_morphism,simplified,OF assms])

lemma uncurry_morphism:
 "case_prod  exp_qbs X (exp_qbs Y Z) Q exp_qbs (X Q Y) Z"
proof(auto intro!: qbs_morphismI simp: exp_qbs_Mx_def)
  fix k α
  assume h:"(λ(x, y). k x y)  Q Q X Q exp_qbs Y Z"
           "α  pair_qbs_Mx Q (X Q Y)"
  have "(λ(x, y). (case_prod  k) x y)  α = (λ(r,y). k (fst (α r)) (fst (snd (α r))) y)  (λr. (r,snd (snd (α r))))"
    by(simp add: split_beta' comp_def)
  also have "...  qbs_Mx Z"
  proof(rule qbs_morphismE(3)[where X="Q Q Y"])
    have "(λr. k (fst (α r)) (fst (snd (α r)))) = (λ(x, y). k x y)  (λr. (fst (α r),fst (snd (α r))))"
      by auto
    also have "...  qbs_Mx (exp_qbs Y Z)"
      apply(rule qbs_morphismE(3)[where X="Q Q X"])
      using h(2) by(auto simp: h(1) pair_qbs_Mx_def comp_def)
    finally show " (λ(r, y). k (fst (α r)) (fst (snd (α r))) y)  Q Q Y Q Z"
      by(simp add: exp_qbs_Mx_def)
  next
    show "(λr. (r, snd (snd (α r))))  qbs_Mx (Q Q Y)"
      using h(2) by(simp add: pair_qbs_Mx_def comp_def)
  qed
  finally show "(λ(x, y). (case_prod  k) x y)  α  qbs_Mx Z" .
qed

lemma uncurry_preserves_morphisms:
  assumes "f  X Q exp_qbs Y Z"
  shows "case_prod f  X Q Y Q Z"
 by(rule qbs_morphismE(2)[OF uncurry_morphism,simplified,OF assms])

lemma arg_swap_morphism:
  assumes "f  X Q exp_qbs Y Z"
  shows "(λy x. f x y)  Y Q exp_qbs X Z"
  using curry_preserves_morphisms[OF qbs_morphism_pair_swap[OF uncurry_preserves_morphisms[OF assms]]]
  by simp

lemma exp_qbs_comp_morphism:
  assumes "f  W Q exp_qbs X Y"
      and "g  W Q exp_qbs Y Z"
    shows "(λw. g w  f w)  W Q exp_qbs X Z"
proof(rule qbs_exp_morphismI)
  fix α β
  assume h: "α  qbs_Mx W"
            "β  pair_qbs_Mx Q X"
  have "(λ(r, x). ((λw. g w  f w)  α) r x)  β= case_prod g  (λr. ((α  (fst  β)) r, case_prod f ((α  (fst  β)) r, (snd  β) r)))"
    by(simp add: split_beta' comp_def)
  also have "...  qbs_Mx Z"
  proof -
    have "(λr. ((α  (fst  β)) r, case_prod f ((α  (fst  β)) r, (snd  β) r)))  qbs_Mx (W Q Y)"
    proof(auto simp add: pair_qbs_Mx_def)
      have "fst  (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) = α  (fst  β)"
        by (simp add: comp_def)
      also have "...  qbs_Mx W"
        using qbs_decomp[of W] h
        by(simp add: pair_qbs_Mx_def qbs_closed1_def)
      finally show "fst  (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r))))  qbs_Mx W" .
    next
      have [simp]:"snd  (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) =  case_prod f  (λr. ((α  (fst  β)) r, (snd  β) r))"
        by(simp add: comp_def)
      have "(λr. ((α  (fst  β)) r, (snd  β) r))  qbs_Mx (W Q X)"
      proof(auto simp add: pair_qbs_Mx_def)
        have "fst  (λr. (α (fst (β r)), snd (β r)))= α  (fst  β)"
          by (simp add: comp_def)
        also have "...  qbs_Mx W"
          using qbs_decomp[of W] h
          by(simp add: pair_qbs_Mx_def qbs_closed1_def)
        finally show "fst  (λr. (α (fst (β r)), snd (β r)))  qbs_Mx W" .
      next
        show "snd  (λr. (α (fst (β r)), snd (β r)))  qbs_Mx X"
          using h
          by(simp add: pair_qbs_Mx_def comp_def)
      qed
      hence "case_prod f  (λr. ((α  (fst  β)) r, (snd  β) r))  qbs_Mx Y"
        using uncurry_preserves_morphisms[OF assms(1)] by auto
      thus "snd  (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r))))  qbs_Mx Y"
        by simp
    qed
    thus ?thesis
      using uncurry_preserves_morphisms[OF assms(2)]
      by auto
  qed
  finally show "(λ(r, x). ((λw. g w  f w)  α) r x)  β  qbs_Mx Z" .
qed

lemma case_sum_morphism:
 "case_prod case_sum  exp_qbs X Z Q exp_qbs Y Z  Q exp_qbs (X <+>Q Y) Z"
proof(rule qbs_exp_morphismI)
  fix α β
  assume h0:"α  qbs_Mx (exp_qbs X Z Q exp_qbs Y Z)"
            "β  pair_qbs_Mx Q (X <+>Q Y)"
  let ?α1 = "fst  α"
  let ?α2 = "snd  α"
  let ?β1 = "fst  β"
  let ?β2 = "snd  β"
  have h:"?α1  exp_qbs_Mx X Z"
         "?α2  exp_qbs_Mx Y Z"
         "?β1  real_borel M real_borel"
         "?β2  copair_qbs_Mx X Y"
    using h0 by (auto simp add: pair_qbs_Mx_def)
  hence "Ssets real_borel. (S = {}  (α1qbs_Mx X. ?β2 = (λr. Inl (α1 r)))) 
                             (S = UNIV  (α2qbs_Mx Y. ?β2 = (λr. Inr (α2 r)))) 
                             (S  {}  S  UNIV 
                            (α1qbs_Mx X. α2qbs_Mx Y. ?β2 = (λr. if r  S then Inl (α1 r) else Inr (α2 r))))"
    by(simp add: copair_qbs_Mx_def)
  then obtain S :: "real set" where hs:
   "Ssets real_borel  (S = {}  (α1qbs_Mx X. ?β2 = (λr. Inl (α1 r)))) 
                         (S = UNIV  (α2qbs_Mx Y. ?β2 = (λr. Inr (α2 r)))) 
                         (S  {}  S  UNIV 
                          (α1qbs_Mx X. α2qbs_Mx Y. ?β2 = (λr. if r  S then Inl (α1 r) else Inr (α2 r))))"
    by auto
  show "(λ(r, x). ((λ(x, y). case_sum x y)  α) r x)  β  qbs_Mx Z"
  proof -
    have "(λ(r, x). ((λ(x, y). case_sum x y)  α) r x)  β = (λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r))"
          (is "?lhs = ?rhs")
      by(auto simp: split_beta' comp_def) (metis comp_apply)
    also have "...  qbs_Mx Z"
         (is "?f  _")
    proof -
      consider "S = {}" | "S = UNIV" | "S  {}  S  UNIV" by auto
      then show ?thesis
      proof cases
        case 1
        then obtain α1 where h1:
         "α1qbs_Mx X  ?β2 = (λr. Inl (α1 r))"
          using hs by auto
        then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) = (λr. ?α1 (?β1 r) (α1 r))"
          by simp
        also have "... = case_prod ?α1  (λr. (?β1 r,α1 r))"
          by auto
        also have "...  Q Q Z"
          apply(rule qbs_morphism_comp[of _ _ "Q Q X"])
           apply(rule qbs_morphism_tuple)
          using h(3)
            apply blast
          using qbs_Mx_is_morphisms h1
           apply blast
          using qbs_Mx_is_morphisms[of "Q Q X"] h(1)
          by (simp add: exp_qbs_Mx_def)
        finally show ?thesis
          using qbs_Mx_is_morphisms by auto
      next
        case 2
        then obtain α2 where h2:
         "α2qbs_Mx Y  ?β2 = (λr. Inr (α2 r))"
          using hs by auto
        then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) = (λr. ?α2 (?β1 r) (α2 r))"
          by simp
        also have "... = case_prod ?α2  (λr. (?β1 r,α2 r))"
          by auto
        also have "...  Q Q Z"
          apply(rule qbs_morphism_comp[of _ _ "Q Q Y"])
           apply(rule qbs_morphism_tuple)
          using h(3)
            apply blast
          using qbs_Mx_is_morphisms h2
           apply blast
          using qbs_Mx_is_morphisms[of "Q Q Y"] h(2)
          by (simp add: exp_qbs_Mx_def)
        finally show ?thesis
          using qbs_Mx_is_morphisms by auto
      next
        case 3
        then obtain α1 α2 where h3:
          "α1qbs_Mx X  α2qbs_Mx Y  ?β2 = (λr. if r  S then Inl (α1 r) else Inr (α2 r))"
          using hs by auto
        define P :: "real  nat"
          where "P  (λr. if r  S then 0 else 1)"
        define γ :: "nat  real  _"
          where "γ  (λn r. if n = 0 then ?α1 (?β1 r) (α1 r) else ?α2 (?β1 r) (α2 r))"
        then have "(λr. case_sum (?α1 (?β1 r)) (?α2 (?β1 r)) (?β2 r)) =(λr. γ (P r) r)"
          by(auto simp add: P_def γ_def h3)
        also have "...  qbs_Mx Z"
        proof -
          have "i. P -` {i}  sets real_borel"
            using hs borel_comp[of S] by(simp add: P_def)
          moreover have"i. γ i  qbs_Mx Z"
          proof
            fix i :: nat
            consider "i = 0" | "i  0" by auto
            then show "γ i  qbs_Mx Z"
            proof cases
              case 1
              then have "γ i = (λr. ?α1 (?β1 r) (α1 r))"
                by(simp add: γ_def)
              also have "... = case_prod ?α1  (λr. (?β1 r,α1 r))"
                by auto
              also have "...  Q Q Z"
                apply(rule qbs_morphism_comp[of _ _ "Q Q X"])
                 apply(rule qbs_morphism_tuple)
                using h(3)
                  apply blast
                using qbs_Mx_is_morphisms h3
                 apply blast
                using qbs_Mx_is_morphisms[of "Q Q X"] h(1)
                by (simp add: exp_qbs_Mx_def)
              finally show ?thesis
                using qbs_Mx_is_morphisms by auto
            next
              case 2
              then have "γ i = (λr. ?α2 (?β1 r) (α2 r))"
                by(simp add: γ_def)
              also have "... = case_prod ?α2  (λr. (?β1 r,α2 r))"
                by auto
              also have "...  Q Q Z"
                apply(rule qbs_morphism_comp[of _ _ "Q Q Y"])
                 apply(rule qbs_morphism_tuple)
                using h(3)
                  apply blast
                using qbs_Mx_is_morphisms h3
                 apply blast
                using qbs_Mx_is_morphisms[of "Q Q Y"] h(2)
                by (simp add: exp_qbs_Mx_def)
              finally show ?thesis
                using qbs_Mx_is_morphisms by auto
            qed
          qed
          ultimately show ?thesis
            using qbs_decomp[of Z]
            by(simp add: qbs_closed3_def)
        qed
        finally show ?thesis .
      qed
    qed
    finally show ?thesis .
  qed
qed


lemma not_qbs_morphism:
 "Not  𝔹Q Q 𝔹Q"
  by(auto intro!: bool_qbs_morphism)

lemma or_qbs_morphism:
 "(∨)  𝔹Q Q exp_qbs 𝔹Q 𝔹Q"
  by(auto intro!: bool_qbs_morphism)

lemma and_qbs_morphism:
 "(∧)  𝔹Q Q exp_qbs 𝔹Q 𝔹Q"
  by(auto intro!: bool_qbs_morphism)

lemma implies_qbs_morphism:
 "(⟶)  𝔹Q Q 𝔹Q Q 𝔹Q"
  by(auto intro!: bool_qbs_morphism)


lemma less_nat_qbs_morphism:
 "(<)  Q Q exp_qbs Q 𝔹Q"
  by(auto intro!: nat_qbs_morphism)

lemma less_real_qbs_morphism:
 "(<)  Q Q exp_qbs Q 𝔹Q"
proof(rule curry_preserves_morphisms[where f="(λ(z :: real × real). fst z < snd z)",simplified curry_def,simplified])
  have "(λz. fst z < snd z)  real_borel M real_borel M bool_borel"
    using borel_measurable_pred_less[OF measurable_fst measurable_snd,simplified measurable_cong_sets[OF refl sets_borel_eq_count_space[symmetric],of "borel M borel"]]
    by simp
  thus "(λz. fst z < snd z)  Q Q Q Q 𝔹Q"
    by auto
qed


lemma rec_list_morphism':
 "rec_list'  qbs_space (exp_qbs Y (exp_qbs (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) (exp_qbs (list_of X) Y)))"
  apply(simp,rule curry_preserves_morphisms[where f="λyf. rec_list' (fst yf) (snd yf)",simplified curry_def, simplified])
  apply(rule arg_swap_morphism)
proof(rule coprod_qbs_canonical1')
  fix n
  show "(λx y. rec_list' (fst y) (snd y) (n, x))  (ΠQ i{..<n}. X) Q exp_qbs (Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y"
  proof(induction n)
    case 0
    show ?case
    proof(rule curry_preserves_morphisms[of " (λ(x,y). rec_list' (fst y) (snd y) (0, x))", simplified],rule qbs_morphismI)
      fix α
      assume h:"α  qbs_Mx ((ΠQ i{..<0::nat}. X) Q Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)))"
      have "r. fst (α r) = (λn. undefined)"
      proof -
        fix r
        have "i. (λr. fst (α r) i) = (λr. undefined)"
          using h by(auto simp: exp_qbs_Mx_def prod_qbs_Mx_def pair_qbs_Mx_def comp_def split_beta')
        thus "fst (α r) = (λn. undefined)"
          by(fastforce dest: fun_cong)
      qed
      hence "(λ(x, y). rec_list' (fst y) (snd y) (0, x))  α = (λx. fst (snd (α x)))"
        by(auto simp: rec_list'_simp1 comp_def split_beta')
      also have "...  qbs_Mx Y"
        using h by(auto simp: pair_qbs_Mx_def comp_def)
      finally show "(λ(x, y). rec_list' (fst y) (snd y) (0, x))  α  qbs_Mx Y" .
    qed
  next
    case ih:(Suc n)
    show ?case
    proof(rule qbs_morphismI)
      fix α
      assume h:"α  qbs_Mx (ΠQ i{..<Suc n}. X)"
      define α' where "α'  (λr. snd (list_tail (Suc n, α r)))"
      define a where "a  (λr. α r 0)"
      then have ha:"a  qbs_Mx X"
        using h by(auto simp: prod_qbs_Mx_def)
      have 1:"α'  qbs_Mx (ΠQ i{..<n}. X)"
        using h by(fastforce simp: prod_qbs_Mx_def list_tail_def α'_def)
      hence 2: "r. (n, α' r)  qbs_space (list_of X)"
        using qbs_Mx_to_X[of α'] by fastforce
      have 3: "r. (Suc n, α r)  qbs_space (list_of X)"
        using qbs_Mx_to_X[of α] h by fastforce
      have 4: "r. (n, α' r) = list_tail (Suc n, α r)"
        by(simp add: list_tail_def α'_def)
      have 5: "r. (Suc n, α r) = list_cons (a r) (n, α' r)"
        unfolding a_def by(simp add: list_simp5[OF 3,simplified 4[symmetric],simplified list_head_def]) auto
      have 6: "(λr. (n, α' r))  qbs_Mx (list_of X)"
        using 1 by(auto intro!: coprod_qbs_MxI)

      have "(λx y. rec_list' (fst y) (snd y) (Suc n, x))  α = (λr y. rec_list' (fst y) (snd y) (Suc n, α r))"
        by auto
      also have "... = (λr y. snd y (a r) (n, α' r) (rec_list' (fst y) (snd y) (n, α' r)))"
        by(simp only: 5 rec_list'_simp2[OF 2])
      also have "...  qbs_Mx (exp_qbs (Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y)"
      proof -
        have "(λ(r,y). snd y (a r) (n, α' r) (rec_list' (fst y) (snd y) (n, α' r))) = (λ(y,x1,x2,x3). y x1 x2 x3)  (λ(r,y). (snd y, a r, (n, α' r), rec_list' (fst y) (snd y) (n, α' r)))"
          by auto
        also have "...  Q Q (Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Q Y"
        proof(rule qbs_morphism_comp[where Y="exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) Q X Q list_of X Q Y"])
          show "(λ(r, y). (snd y, a r, (n, α' r), rec_list' (fst y) (snd y) (n, α' r)))  Q Q Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) Q X Q list_of X Q Y"
          proof(auto simp: split_beta' intro!: qbs_morphism_tuple[OF qbs_morphism_snd''[OF snd_qbs_morphism] qbs_morphism_tuple[of "λ(r, y). a r" "Q Q Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))" X], OF _ qbs_morphism_tuple[of "λ(r,y).  (n, α' r)"],of "list_of X" "λ(r,y). rec_list' (fst y) (snd y) (n, α' r)",simplified split_beta'])
            show "(λx. a (fst x))  Q Q Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) Q X"
              using ha qbs_Mx_is_morphisms[of X] qbs_morphism_fst''[of a "Q" X] by auto
          next
            show "(λx. (n, α' (fst x)))  Q Q Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) Q list_of X"
              using qbs_morphism_fst''[of "λr. (n, α' r)" "Q" "list_of X"] qbs_Mx_is_morphisms[of "list_of X"] 6 by auto
          next
            show "(λx. rec_list' (fst (snd x)) (snd (snd x)) (n, α' (fst x)))  Q Q Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) Q Y"
              using qbs_morphismE(3)[OF ih 1, simplified comp_def]  uncurry_preserves_morphisms[of "(λx y. rec_list' (fst y) (snd y) (n, α' x))" "Q" "Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))" Y] qbs_Mx_is_morphisms[of "exp_qbs (Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y"]
              by(fastforce simp: split_beta')
          qed
        next
          show "(λ(y, x1, x2, x3). y x1 x2 x3)  exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) Q X Q list_of X Q Y Q Y"
          proof(rule qbs_morphismI)
            fix β
            assume "β  qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)) Q X Q list_of X Q Y)"
            then have " β1 β2 β3 β4. β = (λr. (β1 r, β2 r, β3 r, β4 r))  β1  qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)))  β2  qbs_Mx X  β3  qbs_Mx (list_of X)  β4  qbs_Mx Y"
              by(auto intro!: exI[where x="fst  β"] exI[where x="fst  snd  β"] exI[where x="fst  snd  snd  β"] exI[where x="snd  snd  snd  β"] simp:pair_qbs_Mx_def comp_def) 
            then obtain β1 β2 β3 β4 where hb:
             "β = (λr. (β1 r, β2 r, β3 r, β4 r))" "β1  qbs_Mx (exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y)))" "β2  qbs_Mx X" "β3  qbs_Mx (list_of X)" "β4  qbs_Mx Y"
              by auto
            hence hbq:"(λ(((r,x1),x2),x3). β1 r x1 x2 x3)  ((Q Q X) Q list_of X) Q Y Q Y"
              by(simp add: exp_qbs_Mx_def) (meson uncurry_preserves_morphisms)
            have "(λ(y, x1, x2, x3). y x1 x2 x3)  β = (λ(((r,x1),x2),x3). β1 r x1 x2 x3)  (λr. (((r,β2 r), β3 r), β4 r))"
              by(auto simp: hb(1))
            also have "...  Q Q Y"
              using hb(2-5)
              by(auto intro!: qbs_morphism_comp[OF qbs_morphism_tuple[OF qbs_morphism_tuple[OF qbs_morphism_tuple[OF qbs_morphism_ident']]] hbq] simp: qbs_Mx_is_morphisms)
            finally show "(λ(y, x1, x2, x3). y x1 x2 x3)  β  qbs_Mx Y"
              by(simp add: qbs_Mx_is_morphisms)
          qed
        qed
        finally show ?thesis
          by(simp add: exp_qbs_Mx_def)
      qed
      finally show "(λx y. rec_list' (fst y) (snd y) (Suc n, x))  α  qbs_Mx (exp_qbs (Y Q exp_qbs X (exp_qbs (list_of X) (exp_qbs Y Y))) Y)" .
    qed
  qed
qed simp


end