# 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"
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'
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]
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"

lemma exp_qbs_Mx[simp]: "qbs_Mx (exp_qbs X Y) = exp_qbs_Mx X Y"

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)"
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›
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))))"
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"
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)))"
also have "... ∈ qbs_Mx Z"
proof -
have "(λr. ((α ∘ (fst ∘ β)) r, case_prod f ((α ∘ (fst ∘ β)) r, (snd ∘ β) r))) ∈ qbs_Mx (W ⨂⇩Q Y)"
have "fst ∘ (λr. (α (fst (β r)), f (α (fst (β r))) (snd (β r)))) = α ∘ (fst ∘ β)"
also have "... ∈ qbs_Mx W"
using qbs_decomp[of W] h
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))"
have "(λr. ((α ∘ (fst ∘ β)) r, (snd ∘ β) r)) ∈ qbs_Mx (W ⨂⇩Q X)"
have "fst ∘ (λr. (α (fst (β r)), snd (β r)))= α ∘ (fst ∘ β)"
also have "... ∈ qbs_Mx W"
using qbs_decomp[of W] h
finally show "fst ∘ (λr. (α (fst (β r)), snd (β r))) ∈ qbs_Mx W" .
next
show "snd ∘ (λr. (α (fst (β r)), snd (β r))) ∈ qbs_Mx X"
using h
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))))"
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)
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)
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))"
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)
finally show ?thesis
using qbs_Mx_is_morphisms by auto
next
case 2
then have "γ i = (λr. ?α2 (?β1 r) (α2 r))"
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)
finally show ?thesis
using qbs_Mx_is_morphisms by auto
qed
qed
ultimately show ?thesis
using qbs_decomp[of Z]
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)"
have 5: "⋀r. (Suc n, α r) = list_cons (a r) (n, α' r)"
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"
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"