Theory QuasiBorel

(*  Title:   QuasiBorel.thy
    Author:  Yasuhiko Minamide, Michikazu Hirata, Tokyo Institute of Technology
*)

section ‹Quasi-Borel Spaces›
theory QuasiBorel
imports "StandardBorel"
begin

subsection ‹ Definitions ›

text ‹ We formalize quasi-Borel spaces introduced by Heunen et al.~\<^cite>‹"Heunen_2017"›.›

subsubsection ‹ Quasi-Borel Spaces›
definition qbs_closed1 :: "(real ⇒ 'a) set ⇒ bool"
  where "qbs_closed1 Mx ≡ (∀a ∈ Mx. ∀f ∈ real_borel →⇩M real_borel. a ∘ f ∈ Mx)"

definition qbs_closed2 :: "['a set, (real ⇒ 'a) set] ⇒ bool"
 where "qbs_closed2 X Mx ≡ (∀x ∈ X. (λr. x) ∈ Mx)"

definition qbs_closed3 :: "(real ⇒ 'a) set ⇒ bool"
 where "qbs_closed3 Mx ≡ (∀P::real ⇒ nat. ∀Fi::nat ⇒ real ⇒ 'a.
                          (∀i. P -` {i} ∈ sets real_borel)
                           ⟶ (∀i. Fi i ∈ Mx)
                           ⟶ (λr. Fi (P r) r) ∈ Mx)"

lemma separate_measurable:
  fixes P :: "real ⇒ nat"
  assumes "⋀i. P -` {i} ∈ sets real_borel"
  shows "P ∈ real_borel →⇩M nat_borel"
proof -
  have "P ∈ real_borel →⇩M count_space UNIV"
    by (auto simp add: assms measurable_count_space_eq_countable)
  thus ?thesis
    using measurable_cong_sets sets_borel_eq_count_space by blast
qed

lemma measurable_separate:
  fixes P :: "real ⇒ nat"
  assumes "P ∈ real_borel →⇩M nat_borel"
  shows "P -` {i} ∈ sets real_borel"
  by(rule measurable_sets_borel[OF assms borel_singleton[OF sets.empty_sets,of i]])

definition "is_quasi_borel X Mx ⟷ Mx ⊆ UNIV → X ∧ qbs_closed1 Mx ∧ qbs_closed2 X Mx ∧ qbs_closed3 Mx"

lemma is_quasi_borel_intro[simp]:
  assumes "Mx ⊆ UNIV → X"
      and "qbs_closed1 Mx" "qbs_closed2 X Mx" "qbs_closed3 Mx"
    shows "is_quasi_borel X Mx"
  using assms by(simp add: is_quasi_borel_def)

typedef 'a quasi_borel = "{(X::'a set, Mx). is_quasi_borel X Mx}"
proof
  show "(UNIV, UNIV) ∈ {(X::'a set, Mx). is_quasi_borel X Mx}"
    by (simp add: is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def)
qed

definition qbs_space :: "'a quasi_borel ⇒ 'a set" where
  "qbs_space X ≡ fst (Rep_quasi_borel X)"

definition qbs_Mx :: "'a quasi_borel ⇒ (real ⇒ 'a) set" where
  "qbs_Mx X ≡ snd (Rep_quasi_borel X)"

lemma qbs_decomp : 
"(qbs_space X,qbs_Mx X) ∈ {(X::'a set, Mx). is_quasi_borel X Mx}"
  by (simp add: qbs_space_def qbs_Mx_def Rep_quasi_borel[simplified])

lemma qbs_Mx_to_X[dest]:
  assumes "α ∈ qbs_Mx X"
  shows "α ∈ UNIV → qbs_space X"
        "α r ∈ qbs_space X"
  using qbs_decomp assms by(auto simp: is_quasi_borel_def)


lemma qbs_closed1I:
  assumes "⋀α f. α ∈ Mx ⟹ f ∈ real_borel →⇩M real_borel ⟹ α ∘ f ∈ Mx"
  shows "qbs_closed1 Mx"
  using assms by(simp add: qbs_closed1_def)

lemma qbs_closed1_dest[simp]:
  assumes "α ∈ qbs_Mx X"
      and "f ∈ real_borel →⇩M real_borel"
    shows "α ∘ f ∈ qbs_Mx X"
  using assms qbs_decomp by (auto simp add: is_quasi_borel_def qbs_closed1_def)

lemma qbs_closed2I:
  assumes "⋀x. x ∈ X ⟹ (λr. x) ∈ Mx"
  shows "qbs_closed2 X Mx"
  using assms by(simp add: qbs_closed2_def)

lemma qbs_closed2_dest[simp]:
  assumes "x ∈ qbs_space X"
  shows "(λr. x) ∈ qbs_Mx X"
  using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed2_def)

lemma qbs_closed3I:
  assumes "⋀(P :: real ⇒ nat) Fi. (⋀i. P -` {i} ∈ sets real_borel) ⟹ (⋀i. Fi i ∈ Mx)
                  ⟹ (λr. Fi (P r) r) ∈ Mx"
  shows "qbs_closed3 Mx"
  using assms by(auto simp: qbs_closed3_def)

lemma qbs_closed3I':
  assumes "⋀(P :: real ⇒ nat) Fi. P ∈ real_borel →⇩M nat_borel ⟹ (⋀i. Fi i ∈ Mx)
                  ⟹ (λr. Fi (P r) r) ∈ Mx"
  shows "qbs_closed3 Mx"
  using assms by(auto intro!: qbs_closed3I simp: separate_measurable)

lemma qbs_closed3_dest[simp]:
  fixes P::"real ⇒ nat" and Fi :: "nat ⇒ real ⇒ _"
  assumes "⋀i. P -` {i} ∈ sets real_borel"
      and "⋀i. Fi i ∈ qbs_Mx X"
    shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
  using assms qbs_decomp[of X] by (auto simp add: is_quasi_borel_def qbs_closed3_def)

lemma qbs_closed3_dest':
  fixes P::"real ⇒ nat" and Fi :: "nat ⇒ real ⇒ _"
  assumes "P ∈ real_borel →⇩M nat_borel"
      and "⋀i. Fi i ∈ qbs_Mx X"
    shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
  using qbs_closed3_dest[OF measurable_separate[OF assms(1)] assms(2)] .

lemma qbs_closed3_dest2:
  assumes "countable I"
 and [measurable]: "P ∈ real_borel →⇩M count_space I"
      and "⋀i. i ∈ I ⟹ Fi i ∈ qbs_Mx X"
    shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
proof -
  have 0:"I ≠ {}"
    using measurable_empty_iff[of "count_space I" P real_borel] assms(2)
    by fastforce
  define P' where "P' ≡ to_nat_on I ∘ P"
  define Fi' where "Fi' ≡ Fi ∘ (from_nat_into I)"
  have 1:"P' ∈ real_borel →⇩M nat_borel"
    by(simp add: P'_def)
  have 2:"⋀i. Fi' i ∈ qbs_Mx X"
    using assms(3) from_nat_into[OF 0] by(simp add: Fi'_def)
  have "(λr. Fi' (P' r) r) ∈ qbs_Mx X"
    using 1 2 measurable_separate by auto
  thus ?thesis
    using from_nat_into_to_nat_on[OF assms(1)] measurable_space[OF assms(2)]
    by(auto simp: Fi'_def P'_def)
qed

lemma qbs_closed3_dest2':
  assumes "countable I"
 and [measurable]: "P ∈ real_borel →⇩M count_space I"
      and "⋀i. i ∈ range P ⟹ Fi i ∈ qbs_Mx X"
    shows "(λr. Fi (P r) r) ∈ qbs_Mx X"
proof -
  have 0:"range P ∩ I = range P"
    using measurable_space[OF assms(2)] by auto
  have 1:"P ∈ real_borel →⇩M count_space (range P)"
    using restrict_count_space[of I "range P"] measurable_restrict_space2[OF _ assms(2),of "range P"]
    by(simp add: 0)
  have 2:"countable (range P)"
    using countable_Int2[OF assms(1),of "range P"]
    by(simp add: 0)
  show ?thesis
    by(auto intro!: qbs_closed3_dest2[OF 2 1 assms(3)])
qed

lemma qbs_space_Mx:
 "qbs_space X = {α x |x α. α ∈ qbs_Mx X}"
proof auto
  fix x
  assume 1:"x ∈ qbs_space X"
  show "∃xa α. x = α xa ∧ α ∈ qbs_Mx X"
    by(auto intro!: exI[where x=0] exI[where x="(λr. x)"] simp: 1)
qed

lemma qbs_space_eq_Mx:
  assumes "qbs_Mx X = qbs_Mx Y"
  shows "qbs_space X = qbs_space Y"
  by(simp add: qbs_space_Mx assms)

lemma qbs_eqI:
  assumes "qbs_Mx X = qbs_Mx Y"
  shows "X = Y"
  by (metis Rep_quasi_borel_inverse prod.exhaust_sel qbs_Mx_def qbs_space_def assms qbs_space_eq_Mx[OF assms])


subsubsection ‹ Morphism of Quasi-Borel Spaces ›
definition qbs_morphism :: "['a quasi_borel, 'b quasi_borel] ⇒ ('a ⇒ 'b) set" (infixr "→⇩Q" 60) where 
  "X →⇩Q Y ≡ {f ∈ qbs_space X → qbs_space Y. ∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx Y}"

lemma qbs_morphismI:
  assumes "⋀α. α ∈ qbs_Mx X ⟹ f ∘ α ∈ qbs_Mx Y"
  shows "f ∈ X →⇩Q Y"
proof -
  have "f ∈ qbs_space X → qbs_space Y"
  proof
    fix x
    assume "x ∈ qbs_space X "
    then have "(λr. x) ∈ qbs_Mx X"
      by simp
    hence "f ∘ (λr. x) ∈ qbs_Mx Y"
      using assms by blast
    thus "f x ∈ qbs_space Y"
      by auto
  qed
  thus ?thesis
    using assms by(simp add: qbs_morphism_def)
qed

lemma qbs_morphismE[dest]:
  assumes "f ∈ X →⇩Q Y"
  shows "f ∈ qbs_space X → qbs_space Y"
        "⋀x. x ∈ qbs_space X ⟹ f x ∈ qbs_space Y"
        "⋀α. α ∈ qbs_Mx X ⟹ f ∘ α ∈ qbs_Mx Y"
  using assms by(auto simp add: qbs_morphism_def)

lemma qbs_morphism_ident[simp]:
   "id ∈ X →⇩Q X"
  by(auto intro: qbs_morphismI)

lemma qbs_morphism_ident'[simp]:
   "(λx. x) ∈ X →⇩Q X"
  using qbs_morphism_ident by(simp add: id_def)


lemma qbs_morphism_comp:
  assumes "f ∈ X →⇩Q Y" "g ∈ Y →⇩Q Z"
  shows "g ∘ f ∈ X →⇩Q Z"
  using assms by (simp add: comp_assoc Pi_def qbs_morphism_def)

lemma qbs_morphism_cong:
  assumes "⋀x. x ∈ qbs_space X ⟹ f x = g x"
      and "f ∈ X →⇩Q Y"
    shows "g ∈ X →⇩Q Y"
proof(rule qbs_morphismI)
  fix α
  assume 1:"α ∈ qbs_Mx X"
  have "g ∘ α = f ∘ α"
  proof
    fix x
    have "α x ∈ qbs_space X"
      using 1 qbs_decomp[of X] by auto
    thus "(g ∘ α) x = (f ∘ α) x"
      using assms(1) by simp
  qed
  thus "g ∘ α ∈ qbs_Mx Y"
    using 1 assms(2) by(simp add: qbs_morphism_def)
qed

lemma qbs_morphism_const:
  assumes "y ∈ qbs_space Y"
  shows "(λ_. y) ∈ X →⇩Q Y"
  using assms by (auto intro: qbs_morphismI)


subsubsection ‹ Empty Space ›
definition empty_quasi_borel  :: "'a quasi_borel" where
"empty_quasi_borel ≡ Abs_quasi_borel ({},{})"

lemma eqb_correct: "Rep_quasi_borel empty_quasi_borel = ({}, {})"
  using Abs_quasi_borel_inverse
  by(auto simp add: Abs_quasi_borel_inverse empty_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)

lemma eqb_space[simp]: "qbs_space empty_quasi_borel = {}"
  by(simp add: qbs_space_def eqb_correct)

lemma eqb_Mx[simp]: "qbs_Mx empty_quasi_borel = {}"
  by(simp add: qbs_Mx_def eqb_correct)

lemma qbs_empty_equiv :"qbs_space X = {} ⟷ qbs_Mx X = {}"
proof(auto)
  fix x
  assume "qbs_Mx X = {}"
     and h:"x ∈ qbs_space X"
  have "(λr. x) ∈ qbs_Mx X"
    using h by simp
  thus "False" using ‹qbs_Mx X = {}› by simp
qed

lemma empty_quasi_borel_iff:
  "qbs_space X = {} ⟷ X = empty_quasi_borel"
  by(auto intro!: qbs_eqI)

subsubsection ‹ Unit Space ›
definition unit_quasi_borel :: "unit quasi_borel" ("1⇩Q") where
"unit_quasi_borel ≡ Abs_quasi_borel (UNIV,UNIV)"

lemma uqb_correct: "Rep_quasi_borel unit_quasi_borel = (UNIV,UNIV)"
  using Abs_quasi_borel_inverse
  by(auto simp add: unit_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)

lemma uqb_space[simp]: "qbs_space unit_quasi_borel = {()}"
  by(simp add: qbs_space_def UNIV_unit uqb_correct)

lemma uqb_Mx[simp]: "qbs_Mx unit_quasi_borel = {λr. ()}"
  by(auto simp add: qbs_Mx_def uqb_correct)

lemma unit_quasi_borel_terminal:
 "∃! f. f ∈ X →⇩Q unit_quasi_borel"
  by(fastforce simp: qbs_morphism_def)

definition to_unit_quasi_borel :: "'a ⇒ unit" ("!⇩Q") where
"to_unit_quasi_borel ≡ (λ_.())"

lemma to_unit_quasi_borel_morphism :
 "!⇩Q ∈ X →⇩Q unit_quasi_borel"
  by(auto simp add: to_unit_quasi_borel_def qbs_morphism_def)

subsubsection ‹ Subspaces ›
definition sub_qbs :: "['a quasi_borel, 'a set] ⇒ 'a quasi_borel" where
"sub_qbs X U ≡ Abs_quasi_borel (qbs_space X ∩ U,{f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X})"

lemma sub_qbs_closed:
  "qbs_closed1 {f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X}"
  "qbs_closed2 (qbs_space X ∩ U) {f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X}"
  "qbs_closed3 {f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X}"
  unfolding qbs_closed1_def qbs_closed2_def qbs_closed3_def by auto

lemma sub_qbs_correct[simp]: "Rep_quasi_borel (sub_qbs X U) = (qbs_space X ∩ U,{f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X})"
  by(simp add: Abs_quasi_borel_inverse sub_qbs_def sub_qbs_closed)

lemma sub_qbs_space[simp]: "qbs_space (sub_qbs X U) = qbs_space X ∩ U"
  by(simp add: qbs_space_def)

lemma sub_qbs_Mx[simp]: "qbs_Mx (sub_qbs X U) = {f ∈ UNIV → qbs_space X ∩ U. f ∈ qbs_Mx X}"
  by(simp add: qbs_Mx_def)

lemma sub_qbs:
  assumes "U ⊆ qbs_space X"
  shows "(qbs_space (sub_qbs X U), qbs_Mx (sub_qbs X U)) = (U, {f ∈ UNIV → U. f ∈ qbs_Mx X})"
  using assms by auto


subsubsection ‹ Image Spaces ›
definition map_qbs :: "['a ⇒ 'b] ⇒ 'a quasi_borel ⇒ 'b quasi_borel" where
"map_qbs f X = Abs_quasi_borel (f ` (qbs_space X),{β. ∃α∈ qbs_Mx X. β = f ∘ α})"

lemma map_qbs_f:
 "{β. ∃α∈ qbs_Mx X. β = f ∘ α} ⊆ UNIV → f ` (qbs_space X)"
  by fastforce

lemma map_qbs_closed1:
 "qbs_closed1 {β. ∃α∈ qbs_Mx X. β = f ∘ α}"
  unfolding qbs_closed1_def
  using qbs_closed1_dest by(fastforce simp: comp_def)

lemma map_qbs_closed2:
 "qbs_closed2 (f ` (qbs_space X)) {β. ∃α∈ qbs_Mx X. β = f ∘ α}"
  unfolding qbs_closed2_def by fastforce

lemma map_qbs_closed3:
 "qbs_closed3 {β. ∃α∈ qbs_Mx X. β = f ∘ α}"
proof(auto simp add: qbs_closed3_def)
  fix P Fi
  assume h:"∀i::nat. P -` {i} ∈ sets real_borel"
           "∀i::nat. ∃α∈qbs_Mx X. Fi i = f ∘ α"
  then obtain αi
    where ha: "∀i::nat. αi i ∈ qbs_Mx X ∧  Fi i = f ∘ (αi i)"
    by metis
  hence 1:"(λr. αi (P r) r) ∈ qbs_Mx X"
    using h(1) by fastforce
  show "∃α∈qbs_Mx X. (λr. Fi (P r) r) = f ∘ α"
    by(auto intro!: bexI[where x="(λr. αi (P r) r)"] simp add: 1 ha comp_def)
qed

lemma map_qbs_correct[simp]:
 "Rep_quasi_borel (map_qbs f X) = (f ` (qbs_space X),{β. ∃α∈ qbs_Mx X. β = f ∘ α})"
  unfolding map_qbs_def
  by(simp add: Abs_quasi_borel_inverse map_qbs_f map_qbs_closed1 map_qbs_closed2 map_qbs_closed3)

lemma map_qbs_space[simp]:
 "qbs_space (map_qbs f X) = f ` (qbs_space X)"
  by(simp add: qbs_space_def)

lemma map_qbs_Mx[simp]:
 "qbs_Mx (map_qbs f X) = {β. ∃α∈ qbs_Mx X. β = f ∘ α}"
  by(simp add: qbs_Mx_def)


inductive_set generating_Mx :: "'a set ⇒ (real ⇒ 'a) set ⇒ (real ⇒ 'a) set"
  for X :: "'a set" and Mx :: "(real ⇒ 'a) set"
  where
    Basic: "α ∈ Mx ⟹ α ∈ generating_Mx X Mx"
  | Const: "x ∈ X ⟹ (λr. x) ∈ generating_Mx X Mx"
  | Comp : "f ∈ real_borel →⇩M real_borel ⟹ α ∈ generating_Mx X Mx ⟹ α ∘ f ∈ generating_Mx X Mx"
  | Part : "(⋀i. Fi i ∈ generating_Mx X Mx) ⟹ P ∈ real_borel →⇩M nat_borel ⟹ (λr. Fi (P r) r) ∈ generating_Mx X Mx"

lemma generating_Mx_to_space:
  assumes "Mx ⊆ UNIV → X"
  shows "generating_Mx X Mx ⊆ UNIV → X"
proof
  fix α
  assume "α ∈ generating_Mx X Mx"
  then show "α ∈ UNIV → X"
   by(induct rule: generating_Mx.induct) (use assms in auto)
qed

lemma generating_Mx_closed1:
 "qbs_closed1 (generating_Mx X Mx)"
  by (simp add: generating_Mx.Comp qbs_closed1I)

lemma generating_Mx_closed2:
 "qbs_closed2 X (generating_Mx X Mx)"
  by (simp add: generating_Mx.Const qbs_closed2I)

lemma generating_Mx_closed3:
 "qbs_closed3 (generating_Mx X Mx)"
  by(simp add: qbs_closed3I' generating_Mx.Part)

lemma generating_Mx_Mx:
 "generating_Mx (qbs_space X) (qbs_Mx X) = qbs_Mx X"
proof auto
  fix α
  assume "α ∈ generating_Mx (qbs_space X) (qbs_Mx X)"
  then show "α ∈ qbs_Mx X"
    by(rule generating_Mx.induct) (auto intro!: qbs_closed1_dest[simplified comp_def] simp: qbs_closed3_dest')
next
  fix α
  assume "α ∈ qbs_Mx X"
  then show "α ∈ generating_Mx (qbs_space X) (qbs_Mx X)" ..
qed


subsubsection ‹ Ordering of Quasi-Borel Spaces ›

instantiation quasi_borel :: (type) order_bot
begin

inductive less_eq_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ bool" where
  "qbs_space X ⊂ qbs_space Y ⟹ less_eq_quasi_borel X Y"
| "qbs_space X = qbs_space Y ⟹ qbs_Mx Y ⊆ qbs_Mx X ⟹ less_eq_quasi_borel X Y"

lemma le_quasi_borel_iff:
 "X ≤ Y ⟷ (if qbs_space X = qbs_space Y then qbs_Mx Y ⊆ qbs_Mx X else qbs_space X ⊂ qbs_space Y)"
  by(auto elim: less_eq_quasi_borel.cases intro: less_eq_quasi_borel.intros)

definition less_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ bool" where
 "less_quasi_borel X Y ⟷ (X ≤ Y ∧ ¬ Y ≤ X)"

definition bot_quasi_borel :: "'a quasi_borel" where
 "bot_quasi_borel = empty_quasi_borel"

instance
proof
  show "bot ≤ a" for a :: "'a quasi_borel"
    using qbs_empty_equiv
    by(auto simp add: le_quasi_borel_iff bot_quasi_borel_def)
qed (auto simp: le_quasi_borel_iff less_quasi_borel_def split: if_split_asm intro: qbs_eqI)
end

definition inf_quasi_borel :: "['a quasi_borel, 'a quasi_borel] ⇒ 'a quasi_borel" where
"inf_quasi_borel X X' = Abs_quasi_borel (qbs_space X ∩ qbs_space X', qbs_Mx X ∩ qbs_Mx X')"

lemma inf_quasi_borel_correct: "Rep_quasi_borel (inf_quasi_borel X X') = (qbs_space X ∩ qbs_space X', qbs_Mx X ∩ qbs_Mx X')"
  by(fastforce intro!: Abs_quasi_borel_inverse
     simp: inf_quasi_borel_def is_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def)

lemma inf_qbs_space[simp]: "qbs_space (inf_quasi_borel X X') = qbs_space X ∩ qbs_space X'"
  by (simp add: qbs_space_def inf_quasi_borel_correct)

lemma inf_qbs_Mx[simp]: "qbs_Mx (inf_quasi_borel X X') = qbs_Mx X ∩ qbs_Mx X'"
  by(simp add: qbs_Mx_def inf_quasi_borel_correct)

definition max_quasi_borel :: "'a set ⇒ 'a quasi_borel" where
"max_quasi_borel X = Abs_quasi_borel (X, UNIV → X)"

lemma max_quasi_borel_correct: "Rep_quasi_borel (max_quasi_borel X) = (X, UNIV → X)"
  by(fastforce intro!: Abs_quasi_borel_inverse
   simp: max_quasi_borel_def qbs_closed1_def qbs_closed2_def qbs_closed3_def is_quasi_borel_def)

lemma max_qbs_space[simp]: "qbs_space (max_quasi_borel X) = X"
  by(simp add: qbs_space_def max_quasi_borel_correct)

lemma max_qbs_Mx[simp]: "qbs_Mx (max_quasi_borel X) = UNIV → X"
  by(simp add: qbs_Mx_def max_quasi_borel_correct)

instantiation quasi_borel :: (type) semilattice_sup
begin

definition sup_quasi_borel :: "'a quasi_borel ⇒ 'a quasi_borel ⇒ 'a quasi_borel" where
"sup_quasi_borel X Y ≡ (if qbs_space X = qbs_space Y      then inf_quasi_borel X Y
                        else if qbs_space X ⊂ qbs_space Y then Y
                        else if qbs_space Y ⊂ qbs_space X then X
                        else max_quasi_borel (qbs_space X ∪ qbs_space Y))"


instance
proof
  fix X Y :: "'a quasi_borel"
  let ?X = "qbs_space X"
  let ?Y = "qbs_space Y"
  consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
    by auto
  then show "X ≤ X ⊔ Y"
  proof(cases)
    case 1
    show ?thesis
      unfolding sup_quasi_borel_def
      by(rule less_eq_quasi_borel.intros(2),simp_all add: 1)
  next
    case 2
    then show ?thesis
      unfolding sup_quasi_borel_def
      by (simp add: less_eq_quasi_borel.intros(1))
  next
    case 3
    then show ?thesis
      unfolding sup_quasi_borel_def
      by auto
  next
    case 4
    then show ?thesis
      unfolding sup_quasi_borel_def
      by(auto simp: less_eq_quasi_borel.intros(1))
  qed
next
  fix X Y :: "'a quasi_borel"
  let ?X = "qbs_space X"
  let ?Y = "qbs_space Y"
  consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
    by auto
  then show "Y ≤ X ⊔ Y"
  proof(cases)
    case 1
    show ?thesis
      unfolding sup_quasi_borel_def
      by(rule less_eq_quasi_borel.intros(2)) (simp_all add: 1)
  next
    case 2
    then show ?thesis
      unfolding sup_quasi_borel_def
      by auto
  next
    case 3
    then show ?thesis
      unfolding sup_quasi_borel_def
      by (auto simp add: less_eq_quasi_borel.intros(1))
  next
    case 4
    then show ?thesis
      unfolding sup_quasi_borel_def
      by(auto simp: less_eq_quasi_borel.intros(1))
  qed
next
  fix X Y Z :: "'a quasi_borel"
  assume h:"X ≤ Z" "Y ≤ Z"
  let ?X = "qbs_space X"
  let ?Y = "qbs_space Y"
  let ?Z = "qbs_space Z"
  consider "?X = ?Y" | "?X ⊂ ?Y" | "?Y ⊂ ?X" | "?X ⊂ ?X ∪ ?Y ∧ ?Y ⊂ ?X ∪ ?Y"
    by auto
  then show "sup X Y ≤ Z"
  proof cases
    case 1
    show ?thesis
      unfolding sup_quasi_borel_def
      apply(simp add: 1,rule less_eq_quasi_borel.cases[OF h(1)])
       apply(rule less_eq_quasi_borel.intros(1))
       apply auto[1]
      apply auto
      apply(rule less_eq_quasi_borel.intros(2))
       apply(simp add: 1)
      by(rule less_eq_quasi_borel.cases[OF h(2)]) (auto simp: 1)
  next
    case 2
    then show ?thesis
      unfolding sup_quasi_borel_def
      using h(2) by auto
  next
    case 3
    then show ?thesis
      unfolding sup_quasi_borel_def
      using h(1) by auto
  next
    case 4
    then have [simp]:"?X ≠ ?Y" "~ (?X ⊂ ?Y)" "~ (?Y ⊂ ?X)"
      by auto
    have [simp]:"?X ⊆ ?Z" "?Y ⊆ ?Z"
      by (metis h(1) dual_order.order_iff_strict less_eq_quasi_borel.cases)
         (metis h(2) dual_order.order_iff_strict less_eq_quasi_borel.cases)
    then consider "?X ∪ ?Y = ?Z" | "?X ∪ ?Y ⊂ ?Z"
      by blast
    then show ?thesis
      unfolding sup_quasi_borel_def
      apply cases
       apply simp
       apply(rule less_eq_quasi_borel.intros(2))
        apply simp
       apply auto[1]
      by(simp add: less_eq_quasi_borel.intros(1))
  qed
qed
end

end