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 "∃S∈sets real_borel. (S = {} ⟶ (∃α1∈qbs_Mx X. ?β2 = (λr. Inl (α1 r)))) ∧
                             (S = UNIV ⟶ (∃α2∈qbs_Mx Y. ?β2 = (λr. Inr (α2 r)))) ∧
                             (S ≠ {} ∧ S ≠ UNIV ⟶
                            (∃α1∈qbs_Mx X. ∃α2∈qbs_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:
   "S∈sets real_borel ∧ (S = {} ⟶ (∃α1∈qbs_Mx X. ?β2 = (λr. Inl (α1 r)))) ∧
                         (S = UNIV ⟶ (∃α2∈qbs_Mx Y. ?β2 = (λr. Inr (α2 r)))) ∧
                         (S ≠ {} ∧ S ≠ UNIV ⟶
                          (∃α1∈qbs_Mx X. ∃α2∈qbs_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:
         "α1∈qbs_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:
         "α2∈qbs_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:
          "α1∈qbs_Mx X ∧ α2∈qbs_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