Theory CoProduct_QuasiBorel
subsubsection ‹ Countable Coproduct Spaces ›
theory CoProduct_QuasiBorel
imports
"Product_QuasiBorel"
"Binary_CoProduct_QuasiBorel"
begin
definition coprod_qbs_Mx :: "['a set, 'a ⇒ 'b quasi_borel] ⇒ (real ⇒ 'a × 'b) set" where
"coprod_qbs_Mx I X ≡ { λr. (f r, α (f r) r) |f α. f ∈ real_borel →⇩M count_space I ∧ (∀i∈range f. α i ∈ qbs_Mx (X i))}"
lemma coprod_qbs_MxI:
assumes "f ∈ real_borel →⇩M count_space I"
and "⋀i. i ∈ range f ⟹ α i ∈ qbs_Mx (X i)"
shows "(λr. (f r, α (f r) r)) ∈ coprod_qbs_Mx I X"
using assms unfolding coprod_qbs_Mx_def by blast
definition coprod_qbs_Mx' :: "['a set, 'a ⇒ 'b quasi_borel] ⇒ (real ⇒ 'a × 'b) set" where
"coprod_qbs_Mx' I X ≡ { λr. (f r, α (f r) r) |f α. f ∈ real_borel →⇩M count_space I ∧ (∀i. (i ∈ range f ∨ qbs_space (X i) ≠ {}) ⟶ α i ∈ qbs_Mx (X i))}"
lemma coproduct_qbs_Mx_eq:
"coprod_qbs_Mx I X = coprod_qbs_Mx' I X"
proof auto
fix α
assume "α ∈ coprod_qbs_Mx I X"
then obtain f β where hfb:
"f ∈ real_borel →⇩M count_space I"
"⋀i. i ∈ range f ⟹ β i ∈ qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))"
unfolding coprod_qbs_Mx_def by blast
define β' where "β' ≡ (λi. if i ∈ range f then β i
else if qbs_space (X i) ≠ {} then (SOME γ. γ ∈ qbs_Mx (X i))
else β i)"
have 1:"α = (λr. (f r, β' (f r) r))"
by(simp add: hfb(3) β'_def)
have 2:"⋀i. qbs_space (X i) ≠ {} ⟹ β' i ∈ qbs_Mx (X i)"
proof -
fix i
assume hne:"qbs_space (X i) ≠ {}"
then obtain x where "x ∈ qbs_space (X i)" by auto
hence "(λr. x) ∈ qbs_Mx (X i)" by auto
thus "β' i ∈ qbs_Mx (X i)"
by(cases "i ∈ range f") (auto simp: β'_def hfb(2) hne intro!: someI2[where a="λr. x"])
qed
show "α ∈ coprod_qbs_Mx' I X"
using hfb(1,2) 1 2 by(auto simp: coprod_qbs_Mx'_def intro!: exI[where x=f] exI[where x=β'])
next
fix α
assume "α ∈ coprod_qbs_Mx' I X"
then obtain f β where hfb:
"f ∈ real_borel →⇩M count_space I" "⋀i. qbs_space (X i) ≠ {} ⟹ β i ∈ qbs_Mx (X i)"
"⋀i. i ∈ range f ⟹ β i ∈ qbs_Mx (X i)" "α = (λr. (f r, β (f r) r))"
unfolding coprod_qbs_Mx'_def by blast
show "α ∈ coprod_qbs_Mx I X"
by(auto simp: hfb(4) intro!: coprod_qbs_MxI[OF hfb(1) hfb(3)])
qed
definition coprod_qbs :: "['a set, 'a ⇒ 'b quasi_borel] ⇒ ('a × 'b) quasi_borel" where
"coprod_qbs I X ≡ Abs_quasi_borel (SIGMA i:I. qbs_space (X i), coprod_qbs_Mx I X)"
syntax
"_coprod_qbs" :: "pttrn ⇒ 'i set ⇒ 'a quasi_borel ⇒ ('i × 'a) quasi_borel" ("(3⨿⇩Q _∈_./ _)" 10)
translations
"⨿⇩Q x∈I. M" ⇌ "CONST coprod_qbs I (λx. M)"
lemma coprod_qbs_f[simp]: "coprod_qbs_Mx I X ⊆ UNIV → (SIGMA i:I. qbs_space (X i))"
by(fastforce simp: coprod_qbs_Mx_def dest: measurable_space)
lemma coprod_qbs_closed1: "qbs_closed1 (coprod_qbs_Mx I X)"
proof(rule qbs_closed1I)
fix α f
assume "α ∈ coprod_qbs_Mx I X"
and 1[measurable]: "f ∈ real_borel →⇩M real_borel"
then obtain β g where ha:
"⋀i. i ∈ range g ⟹ β i ∈ qbs_Mx (X i)" "α = (λr. (g r, β (g r) r))" and [measurable]:"g ∈ real_borel →⇩M count_space I"
by(fastforce simp: coprod_qbs_Mx_def)
then have "⋀i. i ∈ range g ⟹ β i ∘ f ∈ qbs_Mx (X i)"
by simp
thus "α ∘ f ∈ coprod_qbs_Mx I X"
by(auto intro!: coprod_qbs_MxI[where f="g ∘ f" and α="λi. β i ∘ f",simplified comp_def] simp: ha(2) comp_def)
qed
lemma coprod_qbs_closed2: "qbs_closed2 (SIGMA i:I. qbs_space (X i)) (coprod_qbs_Mx I X)"
proof(rule qbs_closed2I,auto)
fix i x
assume "i ∈ I" "x ∈ qbs_space (X i)"
then show "(λr. (i,x)) ∈ coprod_qbs_Mx I X"
by(auto simp: coprod_qbs_Mx_def intro!: exI[where x="λr. i"])
qed
lemma coprod_qbs_closed3:
"qbs_closed3 (coprod_qbs_Mx I X)"
proof(rule qbs_closed3I)
fix P Fi
assume h:"⋀i :: nat. P -` {i} ∈ sets real_borel"
"⋀i :: nat. Fi i ∈ coprod_qbs_Mx I X"
then have "∀i. ∃fi αi. Fi i = (λr. (fi r, αi (fi r) r)) ∧ fi ∈ real_borel →⇩M count_space I ∧ (∀j. (j ∈ range fi ∨ qbs_space (X j) ≠ {}) ⟶ αi j ∈ qbs_Mx (X j))"
by(auto simp: coproduct_qbs_Mx_eq coprod_qbs_Mx'_def)
then obtain fi where
"∀i. ∃αi. Fi i = (λr. (fi i r, αi (fi i r) r)) ∧ fi i ∈ real_borel →⇩M count_space I ∧ (∀j. (j ∈ range (fi i) ∨ qbs_space (X j) ≠ {}) ⟶ αi j ∈ qbs_Mx (X j))"
by(fastforce intro!: choice)
then obtain αi where
"∀i. Fi i = (λr. (fi i r, αi i (fi i r) r)) ∧ fi i ∈ real_borel →⇩M count_space I ∧ (∀j. (j ∈ range (fi i) ∨ qbs_space (X j) ≠ {}) ⟶ αi i j ∈ qbs_Mx (X j))"
by(fastforce intro!: choice)
then have hf:
"⋀i. Fi i = (λr. (fi i r, αi i (fi i r) r))" "⋀i. fi i ∈ real_borel →⇩M count_space I" "⋀i j. j ∈ range (fi i) ⟹ αi i j ∈ qbs_Mx (X j)" "⋀i j. qbs_space (X j) ≠ {} ⟹ αi i j ∈ qbs_Mx (X j)"
by auto
define f' where "f' ≡ (λr. fi (P r) r)"
define α' where "α' ≡ (λi r. αi (P r) i r)"
have 1:"(λr. Fi (P r) r) = (λr. (f' r, α' (f' r) r))"
by(simp add: α'_def f'_def hf)
have "f' ∈ real_borel →⇩M count_space I"
proof -
note [measurable] = separate_measurable[OF h(1)]
have "(λ(n,r). fi n r) ∈ count_space UNIV ⨂⇩M real_borel →⇩M count_space I"
by(auto intro!: measurable_pair_measure_countable1 simp: hf)
hence [measurable]:"(λ(n,r). fi n r) ∈ nat_borel ⨂⇩M real_borel →⇩M count_space I"
using measurable_cong_sets[OF sets_pair_measure_cong[OF sets_borel_eq_count_space],of real_borel real_borel]
by auto
thus ?thesis
using measurable_comp[of "λr. (P r, r)" _ _ "(λ(n,r). fi n r)"]
by(simp add: f'_def)
qed
moreover have "⋀i. i ∈ range f' ⟹ α' i ∈ qbs_Mx (X i)"
proof -
fix i
assume hi:"i ∈ range f'"
then obtain r where hr:
"i = fi (P r) r" by(auto simp: f'_def)
hence "i ∈ range (fi (P r))" by simp
hence "αi (P r) i ∈ qbs_Mx (X i)" by(simp add: hf)
hence "qbs_space (X i) ≠ {}"
by(auto simp: qbs_empty_equiv)
hence "⋀j. αi j i ∈ qbs_Mx (X i)"
by(simp add: hf(4))
then show "α' i ∈ qbs_Mx (X i)"
by(auto simp: α'_def h(1) intro!: qbs_closed3_dest[of P "λj. αi j i"])
qed
ultimately show "(λr. Fi (P r) r) ∈ coprod_qbs_Mx I X"
by(auto intro!: coprod_qbs_MxI simp: 1)
qed
lemma coprod_qbs_correct: "Rep_quasi_borel (coprod_qbs I X) = (SIGMA i:I. qbs_space (X i), coprod_qbs_Mx I X)"
unfolding coprod_qbs_def
using is_quasi_borel_intro[OF coprod_qbs_f coprod_qbs_closed1 coprod_qbs_closed2 coprod_qbs_closed3]
by(fastforce intro!: Abs_quasi_borel_inverse)
lemma coproduct_qbs_space[simp]: "qbs_space (coprod_qbs I X) = (SIGMA i:I. qbs_space (X i))"
by(simp add: coprod_qbs_correct qbs_space_def)
lemma coproduct_qbs_Mx[simp]: "qbs_Mx (coprod_qbs I X) = coprod_qbs_Mx I X"
by(simp add: coprod_qbs_correct qbs_Mx_def)
lemma ini_morphism:
assumes "j ∈ I"
shows "(λx. (j,x)) ∈ X j →⇩Q (⨿⇩Q i∈I. X i)"
by(fastforce intro!: qbs_morphismI exI[where x="λr. j"] simp: coprod_qbs_Mx_def comp_def assms)
lemma coprod_qbs_canonical1:
assumes "countable I"
and "⋀i. i ∈ I ⟹ f i ∈ X i →⇩Q Y"
shows "(λ(i,x). f i x) ∈ (⨿⇩Q i ∈I. X i) →⇩Q Y"
proof(rule qbs_morphismI)
fix α
assume "α ∈ qbs_Mx (coprod_qbs I X)"
then obtain β g where ha:
"⋀i. i ∈ range g ⟹ β i ∈ qbs_Mx (X i)" "α = (λr. (g r, β (g r) r))" and hg[measurable]:"g ∈ real_borel →⇩M count_space I"
by(fastforce simp: coprod_qbs_Mx_def)
define f' where "f' ≡ (λi r. f i (β i r))"
have "range g ⊆ I"
using measurable_space[OF hg] by auto
hence 1:"(⋀i. i ∈ range g ⟹ f' i ∈ qbs_Mx Y)"
using qbs_morphismE(3)[OF assms(2) ha(1),simplified comp_def]
by(auto simp: f'_def)
have "(λ(i, x). f i x) ∘ α = (λr. f' (g r) r)"
by(auto simp: ha(2) f'_def)
also have "... ∈ qbs_Mx Y"
by(auto intro!: qbs_closed3_dest2'[OF assms(1) hg,of f',OF 1])
finally show "(λ(i, x). f i x) ∘ α ∈ qbs_Mx Y " .
qed
lemma coprod_qbs_canonical1':
assumes "countable I"
and "⋀i. i ∈ I ⟹ (λx. f (i,x)) ∈ X i →⇩Q Y"
shows "f ∈ (⨿⇩Q i ∈I. X i) →⇩Q Y"
using coprod_qbs_canonical1[where f="curry f"] assms by(auto simp: curry_def)
text ‹ $\coprod_{i=0,1} X_i \cong X_1 + X_2$. ›
lemma coproduct_binary_coproduct:
"∃f g. f ∈ (⨿⇩Q i∈UNIV. if i then X else Y) →⇩Q X <+>⇩Q Y ∧ g ∈ X <+>⇩Q Y →⇩Q (⨿⇩Q i∈UNIV. if i then X else Y) ∧
g ∘ f = id ∧ f ∘ g = id"
proof(auto intro!: exI[where x="λ(b,z). if b then Inl z else Inr z"] exI[where x="case_sum (λz. (True,z)) (λz. (False,z))"])
show "(λ(b, z). if b then Inl z else Inr z) ∈ (⨿⇩Q i∈UNIV. if i then X else Y) →⇩Q X <+>⇩Q Y"
proof(rule qbs_morphismI)
fix α
assume " α ∈ qbs_Mx (⨿⇩Q i∈UNIV. if i then X else Y)"
then obtain f β where hf:
"α = (λr. (f r, β (f r) r))" "f ∈ real_borel →⇩M count_space UNIV" "⋀i. i ∈ range f ⟹ β i ∈ qbs_Mx (if i then X else Y)"
by(auto simp: coprod_qbs_Mx_def)
consider "range f = {True}" | "range f = {False}" | "range f = {True,False}"
by auto
thus "(λ(b, z). if b then Inl z else Inr z) ∘ α ∈ qbs_Mx (X <+>⇩Q Y)"
proof cases
case 1
then have "⋀r. f r = True"
by auto
then show ?thesis
using hf(3)
by(auto intro!: bexI[where x="{}"] bexI[where x="β True"] simp: copair_qbs_Mx_def split_beta' comp_def hf(1))
next
case 2
then have "⋀r. f r = False"
by auto
then show ?thesis
using hf(3)
by(auto intro!: bexI[where x="UNIV"] bexI[where x="β False"] simp: copair_qbs_Mx_def split_beta' comp_def hf(1))
next
case 3
then have 4:"f -` {True} ∈ sets real_borel"
using measurable_sets[OF hf(2)] by simp
have 5:"f -` {True} ≠ {} ∧ f -` {True} ≠ UNIV"
using 3
by (metis empty_iff imageE insertCI vimage_singleton_eq)
have 6:"β True ∈ qbs_Mx X" "β False ∈ qbs_Mx Y"
using hf(3)[of True] hf(3)[of False] by(auto simp: 3)
show ?thesis
apply(simp add: copair_qbs_Mx_def)
apply(intro bexI[OF _ 4])
apply(simp add: 5)
apply(intro bexI[OF _ 6(1)] bexI[OF _ 6(2)])
apply(auto simp add: hf(1) comp_def)
done
qed
qed
next
show "case_sum (Pair True) (Pair False) ∈ X <+>⇩Q Y →⇩Q (⨿⇩Q i∈UNIV. if i then X else Y)"
proof(rule qbs_morphismI)
fix α
assume "α ∈ qbs_Mx (X <+>⇩Q Y)"
then obtain S where hs:
"S ∈ sets real_borel" "S = {} ⟶ (∃ α1∈ qbs_Mx X. α = (λr. Inl (α1 r)))" "S = UNIV ⟶ (∃ α2∈ qbs_Mx Y. α = (λr. Inr (α2 r)))"
"(S ≠ {} ∧ S ≠ UNIV) ⟶ (∃ α1∈ qbs_Mx X. ∃ α2∈ qbs_Mx Y. α = (λr::real. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r))))"
by(auto simp: copair_qbs_Mx_def)
consider "S = {}" | "S = UNIV" | "S ≠ {} ∧ S ≠ UNIV" by auto
thus "case_sum (Pair True) (Pair False) ∘ α ∈ qbs_Mx (⨿⇩Q i∈UNIV. if i then X else Y)"
proof cases
case 1
then obtain α1 where ha:
"α1∈ qbs_Mx X" "α = (λr. Inl (α1 r))"
using hs(2) by auto
hence "case_sum (Pair True) (Pair False) ∘ α = (λr. (True, α1 r))"
by auto
thus ?thesis
by(auto intro!: coprod_qbs_MxI simp: ha)
next
case 2
then obtain α2 where ha:
"α2∈ qbs_Mx Y" "α = (λr. Inr (α2 r))"
using hs(3) by auto
hence "case_sum (Pair True) (Pair False) ∘ α = (λr. (False, α2 r))"
by auto
thus ?thesis
by(auto intro!: coprod_qbs_MxI simp: ha)
next
case 3
then obtain α1 α2 where ha:
"α1∈ qbs_Mx X" "α2∈ qbs_Mx Y" "α = (λr. (if (r ∈ S) then Inl (α1 r) else Inr (α2 r)))"
using hs(4) by auto
define f :: "real ⇒ bool" where "f ≡ (λr. r ∈ S)"
define α' where "α' ≡ (λi. if i then α1 else α2)"
have "case_sum (Pair True) (Pair False) ∘ α = (λr. (f r, α' (f r) r))"
by(auto simp: f_def α'_def ha(3))
thus ?thesis
using hs(1)
by(auto intro!: coprod_qbs_MxI simp: ha α'_def f_def)
qed
qed
next
show "(λ(b, z). if b then Inl z else Inr z) ∘ case_sum (Pair True) (Pair False) = id"
by (auto simp add: sum.case_eq_if )
qed
subsubsection ‹ Lists ›
abbreviation "list_of X ≡ ⨿⇩Q n∈(UNIV :: nat set). (Π⇩Q i∈{..<n}. X)"
abbreviation list_nil :: "nat × (nat ⇒ 'a)" where
"list_nil ≡ (0, λn. undefined)"
abbreviation list_cons :: "['a, nat × (nat ⇒ 'a)] ⇒ nat × (nat ⇒ 'a)" where
"list_cons x l ≡ (Suc (fst l), (λn. if n = 0 then x else (snd l) (n - 1)))"
definition list_head :: "nat × (nat ⇒ 'a) ⇒ 'a" where
"list_head l = snd l 0"
definition list_tail :: "nat × (nat ⇒ 'a) ⇒ nat × (nat ⇒ 'a)" where
"list_tail l = (fst l - 1, λm. (snd l) (Suc m))"
lemma list_simp1:
"list_nil ≠ list_cons x l"
by simp
lemma list_simp2:
assumes "list_cons a al = list_cons b bl"
shows "a = b" "al = bl"
proof -
have "a = snd (list_cons a al) 0"
"b = snd (list_cons b bl) 0"
by auto
thus "a = b"
by(simp add: assms)
next
have "fst al = fst bl"
using assms by simp
moreover have "snd al = snd bl"
proof
fix n
have "snd al n = snd (list_cons a al) (Suc n)"
by simp
also have "... = snd (list_cons b bl) (Suc n)"
by (simp add: assms)
also have "... = snd bl n"
by simp
finally show "snd al n = snd bl n" .
qed
ultimately show "al = bl"
by (simp add: prod.expand)
qed
lemma list_simp3:
shows "list_head (list_cons a l) = a"
by(simp add: list_head_def)
lemma list_simp4:
assumes "l ∈ qbs_space (list_of X)"
shows "list_tail (list_cons a l) = l"
using assms by(simp_all add: list_tail_def)
lemma list_decomp1:
assumes "l ∈ qbs_space (list_of X)"
shows "l = list_nil ∨
(∃a l'. a ∈ qbs_space X ∧ l' ∈ qbs_space (list_of X) ∧ l = list_cons a l')"
proof(cases l)
case hl:(Pair n f)
show ?thesis
proof(cases n)
case 0
then show ?thesis
using assms hl by simp
next
case hn:(Suc n')
define f' where "f' ≡ λm. f (Suc m)"
have "l = list_cons (f 0) (n',f')"
proof(simp add: hl hn, standard)
fix m
show "f m = (if m = 0 then f 0 else snd (n', f') (m - 1))"
using assms hl by(cases m; fastforce simp: f'_def)
qed
moreover have "(n', f') ∈ qbs_space (list_of X)"
proof(simp,rule PiE_I)
show "⋀x. x ∈ {..<n'} ⟹ f' x ∈ qbs_space X"
using assms hl hn by(fastforce simp: f'_def)
next
fix x
assume 1:"x ∉ {..<n'}"
thus " f' x = undefined"
using hl assms hn by(auto simp: f'_def)
qed
ultimately show ?thesis
using hl assms
by(auto intro!: exI[where x="f 0"] exI[where x="(n',λm. if m = 0 then undefined else f (Suc m))"])
qed
qed
lemma list_simp5:
assumes "l ∈ qbs_space (list_of X)"
and "l ≠ list_nil"
shows "l = list_cons (list_head l) (list_tail l)"
proof -
obtain a l' where hl:
"a ∈ qbs_space X" "l' ∈ qbs_space (list_of X)" "l = list_cons a l'"
using list_decomp1[OF assms(1)] assms(2) by blast
hence "list_head l = a" "list_tail l = l'"
using list_simp3 list_simp4 by auto
thus ?thesis
using hl(3) list_simp2 by auto
qed
lemma list_simp6:
"list_nil ∈ qbs_space (list_of X)"
by simp
lemma list_simp7:
assumes "a ∈ qbs_space X"
and "l ∈ qbs_space (list_of X)"
shows "list_cons a l ∈ qbs_space (list_of X)"
using assms by(fastforce simp: PiE_def extensional_def)
lemma list_destruct_rule:
assumes "l ∈ qbs_space (list_of X)"
"P list_nil"
and "⋀a l'. a ∈ qbs_space X ⟹ l' ∈ qbs_space (list_of X) ⟹ P (list_cons a l')"
shows "P l"
by(rule disjE[OF list_decomp1[OF assms(1)]]) (use assms in auto)
lemma list_induct_rule:
assumes "l ∈ qbs_space (list_of X)"
"P list_nil"
and "⋀a l'. a ∈ qbs_space X ⟹ l' ∈ qbs_space (list_of X) ⟹ P l' ⟹ P (list_cons a l')"
shows "P l"
proof(cases l)
case hl:(Pair n f)
then show ?thesis
using assms(1)
proof(induction n arbitrary: f l)
case 0
then show ?case
using assms(1,2) by simp
next
case ih:(Suc n)
then obtain a l' where hl:
"a ∈ qbs_space X" "l' ∈ qbs_space (list_of X)" "l = list_cons a l'"
using list_decomp1 by blast
have "P l'"
using ih hl(3)
by(auto intro!: ih(1)[OF _ hl(2),of "snd l'"])
from assms(3)[OF hl(1,2) this]
show ?case
by(simp add: hl(3))
qed
qed
fun from_list :: "'a list ⇒ nat × (nat ⇒ 'a)" where
"from_list [] = list_nil" |
"from_list (a#l) = list_cons a (from_list l)"
fun to_list' :: "nat ⇒ (nat ⇒ 'a) ⇒ 'a list" where
"to_list' 0 _ = []" |
"to_list' (Suc n) f = f 0 # to_list' n (λn. f (Suc n))"
definition to_list :: "nat × (nat ⇒ 'a) ⇒ 'a list" where
"to_list ≡ case_prod to_list'"
lemma to_list_simp1:
shows "to_list list_nil = []"
by(simp add: to_list_def)
lemma to_list_simp2:
assumes "l ∈ qbs_space (list_of X)"
shows "to_list (list_cons a l) = a # to_list l"
using assms by(auto simp:PiE_def to_list_def)
lemma from_list_length:
"fst (from_list l) = length l"
by(induction l, simp_all)
lemma from_list_in_list_of:
assumes "set l ⊆ qbs_space X"
shows "from_list l ∈ qbs_space (list_of X)"
using assms by(induction l) (auto simp: PiE_def extensional_def Pi_def)
lemma from_list_in_list_of':
shows "from_list l ∈ qbs_space (list_of (Abs_quasi_borel (UNIV,UNIV)))"
proof -
have "set l ⊆ qbs_space (Abs_quasi_borel (UNIV,UNIV))"
by(simp add: qbs_space_def Abs_quasi_borel_inverse[of "(UNIV,UNIV)",simplified is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def,simplified])
thus ?thesis
using from_list_in_list_of by blast
qed
lemma list_cons_in_list_of:
assumes "set (a#l) ⊆ qbs_space X"
shows "list_cons a (from_list l) ∈ qbs_space (list_of X)"
using from_list_in_list_of[OF assms] by simp
lemma from_list_to_list_ident:
"(to_list ∘ from_list) l = l"
by(induction l)
(simp add: to_list_def,simp add: to_list_simp2[OF from_list_in_list_of'])
lemma to_list_from_list_ident:
assumes "l ∈ qbs_space (list_of X)"
shows "(from_list ∘ to_list) l = l"
proof(rule list_induct_rule[OF assms])
fix a l'
assume h: "l' ∈ qbs_space (list_of X)"
and ih:"(from_list ∘ to_list) l' = l'"
show "(from_list ∘ to_list) (list_cons a l') = list_cons a l'"
by(auto simp add: to_list_simp2[OF h] ih[simplified])
qed (simp add: to_list_simp1)
definition rec_list' :: "'b ⇒ ('a ⇒ (nat × (nat ⇒ 'a)) ⇒ 'b ⇒ 'b) ⇒ (nat × (nat ⇒ 'a)) ⇒ 'b" where
"rec_list' t0 f l ≡ (rec_list t0 (λx l'. f x (from_list l')) (to_list l))"
lemma rec_list'_simp1:
"rec_list' t f list_nil = t"
by(simp add: rec_list'_def to_list_simp1)
lemma rec_list'_simp2:
assumes "l ∈ qbs_space (list_of X)"
shows "rec_list' t f (list_cons x l) = f x l (rec_list' t f l)"
by(simp add: rec_list'_def to_list_simp2[OF assms] to_list_from_list_ident[OF assms,simplified])
end