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 = {fqbs_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. aqbs_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. bqbs_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 iI. (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 iI. 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 iI. 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 iI. 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 iI. (M i)) Q (ΠQ jJ. (M j)) Q (ΠQ iIJ. (M i))"
proof(rule qbs_morphismI)
  fix α
  assume h:"α  qbs_Mx ((ΠQ iI. (M i)) Q (ΠQ jJ. (M j)))"
  show "merge I J  α  qbs_Mx (ΠQ iIJ. (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 iI. 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