Theory QBS_Morphism

(*  Title:   QBS_Morphism.thy
    Author:  Michikazu Hirata, Tokyo Institute of Technology
*)
subsection ‹ Morphisms of Quasi-Borel Spaces ›
theory QBS_Morphism

imports
 "QuasiBorel"

begin

abbreviation qbs_morphism :: "['a quasi_borel, 'b quasi_borel] ⇒ ('a ⇒ 'b) set" (infixr ‹→Q› 60) where 
  "X →Q Y ≡ qbs_space (X ⇒Q Y)"

lemma qbs_morphismI: "(⋀α. α ∈ qbs_Mx X ⟹ f ∘ α ∈ qbs_Mx Y) ⟹ f ∈ X →Q Y"
  by(auto simp: exp_qbs_space)

lemma qbs_morphism_def: "X →Q Y = {f∈qbs_space X → qbs_space Y. ∀α ∈ qbs_Mx X. f ∘ α ∈ qbs_Mx Y}"
  unfolding exp_qbs_space
proof safe
  fix f x
  assume h:"x ∈ qbs_space X " "∀α∈qbs_Mx X. f ∘ α ∈ qbs_Mx Y"
  then have "(λr. x) ∈ qbs_Mx X"
    by simp
  hence "f ∘ (λr. x) ∈ qbs_Mx Y"
    using h by blast
  with qbs_Mx_to_X show "f x ∈ qbs_space Y"
    by auto
qed auto                     

lemma qbs_morphism_Mx:
  assumes "f ∈ X →Q Y" "α ∈ qbs_Mx X"
  shows "f ∘ α ∈ qbs_Mx Y"
  using assms by(auto simp: qbs_morphism_def)

lemma qbs_morphism_space:
  assumes "f ∈ X →Q Y" "x ∈ qbs_space X"
  shows "f x ∈ qbs_space Y"
  using assms by(auto simp: 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_compose_rev:
  assumes "f ∈ Y →Q Z" and "g ∈ X →Q Y"
  shows "(λx. f (g x)) ∈ X →Q Z"
  using qbs_morphism_comp[OF assms(2,1)] by(simp add: comp_def)

lemma qbs_morphism_compose:
  assumes "g ∈ X →Q Y" and "f ∈ Y →Q Z"
  shows "(λx. f (g x)) ∈ X →Q Z"
  using qbs_morphism_compose_rev[OF assms(2,1)] .

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] qbs_Mx_to_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_cong:
  assumes "⋀x. x ∈ qbs_space X ⟹ f x = g x"
  shows "f ∈ X →Q Y ⟷ g ∈ X →Q Y"
  using assms by(auto simp: qbs_morphism_cong'[of _ f g] qbs_morphism_cong'[of _ g f])

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

lemma qbs_morphism_from_empty: "qbs_space X = {} ⟹ f ∈ X →Q Y"
  by(auto intro!: qbs_morphismI simp: qbs_empty_equiv)

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 ≡ (λr.())"

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

lemma qbs_morphism_subD:
  assumes "f ∈ X →Q sub_qbs Y A"
  shows "f ∈ X →Q Y"
  using qbs_morphism_Mx[OF assms] by(auto intro!: qbs_morphismI simp: sub_qbs_Mx)

lemma qbs_morphism_subI1:
  assumes "f ∈ X →Q Y" "⋀x. x ∈ qbs_space X ⟹ f x ∈ A"
  shows "f ∈ X →Q sub_qbs Y A"
  using qbs_morphism_space[OF assms(1)] qbs_morphism_Mx[OF assms(1)] assms(2) qbs_Mx_to_X[of _ X]
  by(auto intro!: qbs_morphismI simp: sub_qbs_Mx)

lemma qbs_morphism_subI2:
  assumes "f ∈ X →Q Y"
  shows "f ∈ sub_qbs X A →Q Y"
  using qbs_morphism_Mx[OF assms] by(auto intro!: qbs_morphismI simp: sub_qbs_Mx)

corollary qbs_morphism_subsubI:
  assumes "f ∈  X →Q Y" "⋀x. x ∈ A ⟹ f x ∈ B"
  shows "f ∈ sub_qbs X A →Q sub_qbs Y B"
  by(rule qbs_morphism_subI1) (auto intro!: qbs_morphism_subI2 assms simp: sub_qbs_space)

lemma map_qbs_morphism_f: "f ∈ X →Q map_qbs f X"
  by(auto intro!: qbs_morphismI simp: map_qbs_Mx)

lemma map_qbs_morphism_inverse_f:
  assumes "⋀x. x ∈ qbs_space X ⟹ g (f x) = x"
  shows "g ∈ map_qbs f X →Q X"
proof -
  { 
    fix α
    assume h:"α ∈ qbs_Mx X"
    from qbs_Mx_to_X[OF this] assms have "g ∘ (f ∘ α) = α"
      by auto
    with h have "g ∘ (f ∘ α) ∈ qbs_Mx X" by simp
  }
  thus ?thesis
    by(auto intro!: qbs_morphismI simp: map_qbs_Mx)
qed

lemma pair_qbs_morphismI:
  assumes "⋀α β. α ∈ qbs_Mx X ⟹ β ∈ qbs_Mx Y 
           ⟹ (λr. f (α r, β r)) ∈ qbs_Mx Z"
  shows "f ∈ (X ⨂Q Y) →Q Z"
  using assms by(fastforce intro!: qbs_morphismI simp: pair_qbs_Mx comp_def)

lemma pair_qbs_MxD:
  assumes "γ ∈ qbs_Mx (X ⨂Q Y)"
  obtains α β where "α ∈ qbs_Mx X" "β ∈ qbs_Mx Y" "γ = (λx. (α x, β x))"
  using assms by(auto simp: pair_qbs_Mx)

lemma pair_qbs_MxI:
  assumes "(λx. fst (γ x)) ∈ qbs_Mx X" and "(λx. snd (γ x)) ∈ qbs_Mx Y"
  shows "γ ∈ qbs_Mx (X ⨂Q Y)"
  using assms by(auto simp: pair_qbs_Mx comp_def)

lemma
  shows fst_qbs_morphism: "fst ∈ X ⨂Q Y →Q X"
    and snd_qbs_morphism: "snd ∈ X ⨂Q Y →Q Y"
  by(auto intro!: pair_qbs_morphismI simp: comp_def)

lemma qbs_morphism_pair_iff:
 "f ∈ X →Q Y ⨂Q Z ⟷ fst ∘ f ∈ X →Q Y ∧ snd ∘ f ∈ X →Q Z"
  by(auto intro!: qbs_morphism_comp fst_qbs_morphism snd_qbs_morphism)
    (auto dest: qbs_morphism_Mx intro!: qbs_morphismI simp: pair_qbs_Mx comp_assoc[symmetric])

lemma qbs_morphism_Pair:
  assumes "f ∈ Z →Q X"
      and "g ∈ Z →Q Y"
    shows "(λz. (f z, g z)) ∈ Z →Q X ⨂Q Y"
  unfolding qbs_morphism_pair_iff
  using assms by (auto simp: comp_def)

lemma qbs_morphism_curry: "curry ∈ exp_qbs (X ⨂Q Y) Z →Q exp_qbs X (exp_qbs Y Z)"
  by(auto intro!: qbs_morphismI simp: pair_qbs_Mx exp_qbs_Mx comp_def)  

corollary curry_preserves_morphisms:
  assumes "(λxy. f (fst xy) (snd xy)) ∈ X ⨂Q Y →Q Z"
  shows "f ∈ X →Q Y ⇒Q Z"
  using qbs_morphism_space[OF qbs_morphism_curry assms] by (auto simp: curry_def)

lemma qbs_morphism_eval:
 "(λfx. (fst fx) (snd fx)) ∈ (X ⇒Q Y) ⨂Q X →Q Y"
  by(auto intro!: qbs_morphismI simp: pair_qbs_Mx exp_qbs_Mx comp_def)

corollary qbs_morphism_app:
  assumes "f ∈ X →Q (Y ⇒Q Z)" "g ∈ X →Q Y"
  shows "(λx. (f x) (g x)) ∈ X →Q Z"
  by(rule qbs_morphism_cong'[where f="(λfx. (fst fx) (snd fx)) ∘ (λx. (f x, g x))",OF _ qbs_morphism_comp[OF qbs_morphism_Pair[OF assms] qbs_morphism_eval]]) auto

ML_file ‹qbs.ML›

attribute_setup qbs = ‹
  Attrib.add_del Qbs.qbs_add Qbs.qbs_del›
 "declaration of qbs rule"

method_setup qbs = ‹ Scan.lift (Scan.succeed (METHOD o Qbs.qbs_tac))›

simproc_setup qbs ("x ∈ qbs_space X") = ‹K Qbs.simproc›

declare
  fst_qbs_morphism[qbs]
  snd_qbs_morphism[qbs]
  qbs_morphism_const[qbs]
  qbs_morphism_ident[qbs]
  qbs_morphism_ident'[qbs]
  qbs_morphism_curry[qbs]

lemma [qbs]:
  shows qbs_morphism_Pair1: "Pair ∈ X →Q Y ⇒Q (X ⨂Q Y)"
  by(auto intro!: qbs_morphismI simp: exp_qbs_Mx pair_qbs_Mx comp_def)

lemma qbs_morphism_case_prod[qbs]: "case_prod ∈ exp_qbs X (exp_qbs Y Z) →Q exp_qbs (X ⨂Q Y) Z"
  by(fastforce intro!: qbs_morphismI simp: exp_qbs_Mx pair_qbs_Mx comp_def split_beta')

lemma uncurry_preserves_morphisms:
  assumes [qbs]:"(λx y. f (x,y)) ∈ X →Q Y ⇒Q Z"
  shows "f ∈ X ⨂Q Y →Q Z"
  by(rule qbs_morphism_cong'[where f="case_prod (λx y. f (x,y))"],simp) qbs

lemma qbs_morphism_comp'[qbs]:"comp ∈ Y ⇒Q Z →Q (X ⇒Q Y) ⇒Q X ⇒Q Z"
  by(auto intro!: qbs_morphismI simp: exp_qbs_Mx)

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 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"
  using assms by qbs

lemma arg_swap_morphism_map_qbs1:
  assumes "g ∈ exp_qbs W (exp_qbs X Y) →Q Z"
  shows "(λk. g (k ∘ f)) ∈ exp_qbs (map_qbs f W) (exp_qbs X Y) →Q Z"
  using assms map_qbs_morphism_f by qbs

lemma qbs_morphism_map_prod[qbs]: "map_prod ∈ X ⇒Q Y →Q (W ⇒Q Z) ⇒Q (X ⨂Q W) ⇒Q (Y ⨂Q Z)"
  by(auto intro!: qbs_morphismI simp: exp_qbs_Mx pair_qbs_Mx map_prod_def comp_def case_prod_beta')

lemma qbs_morphism_pair_swap:
  assumes "f ∈ X ⨂Q Y →Q Z"
  shows "(λ(x,y). f (y,x)) ∈ Y ⨂Q X →Q Z"
  using assms by simp

lemma
  shows qbs_morphism_pair_assoc1: "(λ((x,y),z). (x,(y,z))) ∈ (X ⨂Q Y) ⨂Q Z →Q X ⨂Q (Y ⨂Q Z)"
    and qbs_morphism_pair_assoc2: "(λ(x,(y,z)). ((x,y),z)) ∈ X ⨂Q (Y ⨂Q Z) →Q (X ⨂Q Y) ⨂Q Z"
  by simp_all

lemma Inl_qbs_morphism[qbs]: "Inl ∈ X →Q X ⨁Q Y"
  by(auto intro!: qbs_morphismI bexI[where x="{}"] simp: copair_qbs_Mx copair_qbs_Mx_def comp_def)

lemma Inr_qbs_morphism[qbs]: "Inr ∈ Y →Q X ⨁Q Y"
  by(auto intro!: qbs_morphismI bexI[where x="UNIV"] simp: copair_qbs_Mx copair_qbs_Mx_def comp_def)

lemma case_sum_qbs_morphism[qbs]: "case_sum ∈ X ⇒Q Z →Q (Y ⇒Q Z) ⇒Q (X ⨁Q Y ⇒Q Z)"
  by(auto intro!: qbs_morphismI qbs_Mx_indicat simp: copair_qbs_Mx copair_qbs_Mx_def exp_qbs_Mx case_sum_if)

lemma map_sum_qbs_morphism[qbs]: "map_sum ∈ X ⇒Q Y →Q (X' ⇒Q Y') ⇒Q (X ⨁Q X' ⇒Q Y ⨁Q Y')"
proof(rule qbs_morphismI)
  fix α
  assume "α ∈ qbs_Mx (X ⇒Q Y)"
  then have ha[measurable]: "∀(k :: real ⇒ real)∈borel_measurable borel. ∀a∈qbs_Mx X. (λr. α (k r) (a r)) ∈ qbs_Mx Y"
    by (auto simp: exp_qbs_Mx)
  show "map_sum ∘ α ∈ qbs_Mx ((X' ⇒Q Y') ⇒Q X ⨁Q X' ⇒Q Y ⨁Q Y')"
    unfolding exp_qbs_Mx
  proof safe
    fix β b and f g :: "real ⇒ real"
    assume h[measurable]: "∀(k :: real ⇒ real)∈borel_measurable borel. ∀b∈qbs_Mx X'. (λr. β (k r) (b r)) ∈ qbs_Mx Y'"
         "f ∈ borel_measurable borel" "g ∈ borel_measurable borel"
     and b: "b ∈ qbs_Mx (X ⨁Q X')"  
    show "(λr. (map_sum ∘ α) (f (g r)) (β (g r)) (b r)) ∈ qbs_Mx (Y ⨁Q Y')"
    proof(rule copair_qbs_MxD[OF b])
      fix a
      assume "a ∈ qbs_Mx X" "b = (λr. Inl (a r))"
      with ha show "(λr. (map_sum ∘ α) (f (g r)) (β (g r)) (b r)) ∈ qbs_Mx (Y ⨁Q Y')"
        by(auto simp: copair_qbs_Mx copair_qbs_Mx_def intro!: bexI[where x="{}"])
    next
      fix a
      assume "a ∈ qbs_Mx X'" "b = (λr. Inr (a r))"
      with h(1) show "(λr. (map_sum ∘ α) (f (g r)) (β (g r)) (b r)) ∈ qbs_Mx (Y ⨁Q Y')"
        by(auto simp: copair_qbs_Mx copair_qbs_Mx_def intro!: bexI[where x="UNIV"])
    next
      fix S a a'
      assume "S ∈ sets borel" "S ≠ {}" "S ≠ UNIV" "a ∈ qbs_Mx X" "a' ∈ qbs_Mx X'" "b = (λr. if r ∈ S then Inl (a r) else Inr (a' r))"
      with h ha show "(λr. (map_sum ∘ α) (f (g r)) (β (g r)) (b r)) ∈ qbs_Mx (Y ⨁Q Y')"
        by simp (fastforce simp: copair_qbs_Mx copair_qbs_Mx_def intro!: bexI[where x=S])
    qed
  qed
qed

lemma qbs_morphism_component_singleton[qbs]:
  assumes "i ∈ I"
  shows "(λx. x i) ∈ (ΠQ i∈I. (M i)) →Q M i"
  by(auto intro!: qbs_morphismI simp: comp_def assms PiQ_Mx)

lemma qbs_morphism_component_singleton':
  assumes "f ∈ Y →Q (ΠQ i∈I. X i)" "g ∈ Z →Q Y" "i ∈ I"
  shows "(λx. f (g x) i) ∈ Z →Q X i"
  by(auto intro!: qbs_morphism_compose[OF assms(2)] qbs_morphism_compose[OF assms(1)] qbs_morphism_component_singleton assms)

lemma product_qbs_canonical1:
  assumes "⋀i. i ∈ I ⟹ f i ∈ Y →Q X i"
      and "⋀i. i ∉ I ⟹ f i = (λy. undefined)"
    shows "(λy i. f i y) ∈ Y →Q (ΠQ i∈I. X i)"
  using assms qbs_morphism_Mx[OF assms(1)] by(auto intro!: qbs_morphismI simp: PiQ_Mx comp_def)

lemma product_qbs_canonical2:
  assumes "⋀i. i ∈ I ⟹ f i ∈ Y →Q X i"
          "⋀i. i ∉ I ⟹ f i = (λy. undefined)"
          "g ∈ Y →Q (ΠQ i∈I. X i)"
          "⋀i. i ∈ I ⟹ f i = (λx. x i) ∘ g"
      and "y ∈ qbs_space Y"
    shows "g y = (λi. f i y)"
proof(intro ext)
  fix i
  show "g y i = f i y"
  proof(cases "i ∈ I")
    case True
    then show ?thesis
      using assms(4)[of i] by simp
  next
    case False
    with qbs_morphism_space[OF assms(3)] assms(2,3,5) show ?thesis
      by(auto simp: PiQ_Mx PiQ_space)
  qed
qed

lemma merge_qbs_morphism:
 "merge I J ∈ (ΠQ i∈I. (M i)) ⨂Q (ΠQ j∈J. (M j)) →Q (ΠQ i∈I∪J. (M i))"
proof(rule qbs_morphismI)
  fix α
  assume h:"α ∈ qbs_Mx ((ΠQ i∈I. (M i)) ⨂Q (ΠQ j∈J. (M j)))"
  show "merge I J ∘ α ∈ qbs_Mx (ΠQ i∈I∪J. (M i))"
  proof -
    {
      fix i
      assume "i ∈ I ∪ J"
      then consider "i ∈ I" | "i ∈ I ∧ i ∈ J" | "i ∉ I ∧ i ∈ J"
        by auto
      hence "(λr. (merge I J ∘ α) r i) ∈ qbs_Mx (M i)"
        by cases (insert h, auto simp: merge_def split_beta' pair_qbs_Mx PiQ_Mx)
    }
    thus ?thesis
      by(auto simp: PiQ_Mx) (auto simp: merge_def split_beta')
  qed
qed

lemma ini_morphism[qbs]:
  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: coPiQ_Mx_def comp_def assms coPiQ_Mx)

lemma coPiQ_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 (coPiQ 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 ∈ borel →M count_space I"
    by(fastforce simp: coPiQ_Mx_def coPiQ_Mx)
  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_morphism_Mx[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 coPiQ_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 coPiQ_canonical1[where f="curry f"] assms by(auto simp: curry_def)

lemma None_qbs[qbs]: "None ∈ qbs_space (option_qbs X)"
  by(simp add: option_qbs_space)

lemma Some_qbs[qbs]: "Some ∈ X →Q option_qbs X"
proof -
  have 1: "Some = (λx. case x of Inl y ⇒ Some y | Inr y ⇒ None) ∘ Inl"
    by standard auto
  show ?thesis
    unfolding option_qbs_def
    by(rule qbs_morphism_cong'[OF _ qbs_morphism_comp[OF Inl_qbs_morphism map_qbs_morphism_f]]) (simp add: 1)
qed

lemma case_option_qbs_morphism[qbs]: "case_option ∈ qbs_space (Y ⇒Q (X ⇒Q Y) ⇒Q option_qbs X ⇒Q Y)"
proof(rule curry_preserves_morphisms[OF arg_swap_morphism])
  have "(λx y. case x of None ⇒ fst y | Some z ⇒ snd y z) = (λx y. case x of Inr _ ⇒ fst y | Inl z ⇒ snd y z) ∘ (λz. case z of Some x ⇒ Inl x | None ⇒ Inr ())"
    by standard+ (simp add: option.case_eq_if)
  also have "... ∈ option_qbs X →Q Y ⨂Q (X ⇒Q Y) ⇒Q Y"
    unfolding option_qbs_def by(rule qbs_morphism_comp[OF  map_qbs_morphism_inverse_f]) (auto simp: copair_qbs_space)
  finally show " (λx y. case x of None ⇒ fst y | Some x ⇒ snd y x) ∈ option_qbs X →Q Y ⨂Q (X ⇒Q Y) ⇒Q Y" .
qed

lemma rec_option_qbs_morphism[qbs]: "rec_option ∈ qbs_space (Y ⇒Q (X ⇒Q Y) ⇒Q option_qbs X ⇒Q Y)"
proof -
  have [simp]: "rec_option = case_option"
    by standard+ (metis option.case_eq_if option.exhaust_sel option.simps(6) option.simps(7)) 
  show ?thesis by simp
qed

lemma bind_option_qbs_morphism[qbs]: "(⤜) ∈ qbs_space (option_qbs X ⇒Q (X ⇒Q option_qbs Y) ⇒Q option_qbs Y)"
  by(simp add: Option.bind_def)

lemma Let_qbs_morphism[qbs]: "Let ∈ X ⇒Q (X ⇒Q Y) ⇒Q Y"
proof -
  have [simp]:"Let = (λx f. f x)" by standard+ auto
  show ?thesis by simp
qed

end