Theory Vardi

section ‹Vardi Systems›

(*<*)
theory Vardi
imports 
  Probabilistic_Hierarchy
begin
(*>*)

context notes [[bnf_internals]]
begin
  datatype ('a, 'b, 'k) var0 = PMF "('a × 'b) pmf" | BPS "('a × 'b) set['k]"
end

inductive var_eq :: "('a, 'b, 'k) var0 ⇒ ('a, 'b, 'k) var0 ⇒ bool" (infixl ‹∼› 65) where
  var_eq_reflp[intro]: "x ∼ x"
| [intro]: "PMF (return_pmf (a, x)) ∼ BPS (bsingleton (a, x))"
| [intro]: "BPS (bsingleton (a, x)) ∼ PMF (return_pmf (a, x))"

lemma var_eq_symp: "x ∼ y ⟹ y ∼ x"
  by (auto elim: var_eq.cases)

lemma var_eq_transp: "x ∼ y ⟹ y ∼ z ⟹ x ∼ z"
  by (auto elim!: var_eq.cases)

quotient_type ('a, 'b, 'k) var = "('a, 'b, 'k) var0" / "(∼)"
  by (auto intro: equivpI reflpI sympI transpI  var_eq_symp var_eq_transp)

lift_definition map_var  :: "('a ⇒ 'c) ⇒ ('b ⇒ 'd) ⇒ ('a, 'b, 'k) var ⇒ ('c, 'd, 'k) var"
  is map_var0
  by (auto elim!: var_eq.cases simp: map_bset_bsingleton)

lift_definition set1_var  :: "('a, 'b, 'k) var ⇒ 'a set"
  is set1_var0
  by (auto elim!: var_eq.cases)

lift_definition set2_var  :: "('a, 'b, 'k) var ⇒ 'b set"
  is set2_var0
  by (auto elim!: var_eq.cases)

inductive rel_var :: "('a ⇒ 'c ⇒ bool) ⇒ ('b ⇒ 'd ⇒ bool) ⇒ ('a, 'b, 'k) var ⇒ ('c, 'd, 'k) var ⇒ bool" for R S where
  "set1_var x ⊆ {(x, y). R x y} ⟹ set2_var x ⊆ {(x, y). S x y} ⟹
    rel_var R S (map_var fst fst x) (map_var snd snd x)"

abbreviation (input) "var0_of_gen_emb ≡ case_option (BPS bempty) PMF"
abbreviation (input) "var0_of_lts_emb ≡ BPS"

lift_definition var_of_gen_emb :: "('a × 'b) pmf option ⇒ ('a, 'b, 'k) var" is var0_of_gen_emb .
lift_definition var_of_lts_emb :: "('a × 'b) set['k] ⇒ ('a, 'b, 'k) var" is var0_of_lts_emb .

abbreviation "bisimilar_var ≡ bisimilar (λR. rel_var (=) R)"

lemma map_var0_eq_BPS_iff[simp]:
  "map_var0 f g z = BPS X ⟷ (∃Y. z = BPS Y ∧ map_bset (map_prod f g) Y = X)"
  by (cases z) auto

lemma map_var0_eq_PMF_iff[simp]:
  "map_var0 f g z = PMF p ⟷ (∃q. z = PMF q ∧ map_pmf (map_prod f g) q = p)"
  by (cases z) auto

lemma "bisimilar_lts s1 s2 x y ⟷ bisimilar_var (var_of_lts_emb o s1) (var_of_lts_emb o s2) x y"
  (is "_ ⟷ bisimilar_var (?emb1 o _) (?emb2 o _) _ _")
unfolding bisimilar_def o_apply proof safe
  fix R assume "R x y" and
    bis: "∀x y. R x y ⟶ rel_bset (rel_prod (=) R) (s1 x) (s2 y)"
  from ‹R x y› show "∃R. R x y ∧ (∀x y. R x y ⟶ rel_var (=) R (?emb1 (s1 x)) (?emb2 (s2 y)))"
  proof (intro exI[of _ R], safe)
    fix x y
    assume "R x y"
    with bis have *: "rel_bset (rel_prod (=) R) (s1 x) (s2 y)" by blast
    then obtain z where
      "set_bset z ⊆ {(x, y). rel_prod (=) R x y}" "map_bset fst z = s1 x" "map_bset snd z = s2 y"
      by (auto simp: bset.in_rel)
    then show "rel_var (=) R (?emb1 (s1 x)) (?emb2 (s2 y))"
      unfolding rel_var.simps by (transfer fixing: z)
        (force simp: bset.map_comp o_def split_beta prod_set_simps
        intro: exI[of _ "BPS (map_bset (λ((a,b),(c,d)). ((a,c),(b,d))) z)"])
  qed
next
  fix R assume "R x y" and
    bis: "∀x y. R x y ⟶ rel_var (=) R (?emb1 (s1 x)) (?emb2 (s2 y))"
  from ‹R x y› show "∃R. R x y ∧ (∀x y. R x y ⟶ rel_bset (rel_prod (=) R) (s1 x) (s2 y))"
  proof (intro exI[of _ R], safe)
    fix x y
    assume "R x y"
    with bis have "rel_var (=) R (?emb1 (s1 x)) (?emb2 (s2 y))" by blast
    then obtain z where *:
      "set1_var z ⊆ {(x, y). x = y}" "set2_var z ⊆ {(x, y). R x y}"
      "?emb1 (s1 x) = map_var fst fst z" "?emb2 (s2 y) = map_var snd snd z"
      by (auto simp: rel_var.simps)
    then show "rel_bset (rel_prod (=) R) (s1 x) (s2 y)"
      by (transfer fixing: s1 s2) (fastforce simp: bset.in_rel bset.map_comp o_def map_pmf_eq_return_pmf_iff
        split_beta[abs_def] map_prod_def subset_eq split_beta prod_set_defs elim!: var_eq.cases
        intro: exI[of _ "map_bset (λ((a,b),(c,d)). ((a,c),(b,d))) z" for z]
          exI[of _ "bsingleton ((a,c),(b,d))" for a b c d])
  qed
qed

lemma "bisimilar_gen s1 s2 x y ⟷ bisimilar_var (var_of_gen_emb o s1) (var_of_gen_emb o s2) x y"
  (is "_ ⟷ bisimilar_var (?emb1 o _) (?emb2 o _) _ _")
unfolding bisimilar_def o_apply proof safe
  fix R assume "R x y" and
    bis: "∀x y. R x y ⟶ rel_option (rel_pmf (rel_prod (=) R)) (s1 x) (s2 y)"
  from ‹R x y› show "∃R. R x y ∧ (∀x y. R x y ⟶ rel_var (=) R (?emb1 (s1 x)) (?emb2 (s2 y)))"
  proof (intro exI[of _ R], safe)
    fix x y
    assume "R x y"
    with bis have *: "rel_option (rel_pmf (rel_prod (=) R)) (s1 x) (s2 y)" by blast
    then show "rel_var (=) R (?emb1 (s1 x)) (?emb2 (s2 y))"
    proof (cases "s1 x" "s2 y" rule: option.exhaust[case_product option.exhaust])
      case None_None then show ?thesis unfolding rel_var.simps
        by (transfer fixing: s1 s2) (auto simp: bempty.rep_eq intro!: exI[of _ "BPS bempty"])
    next
      case (Some_Some p q)
      with * obtain z where
        "set_pmf z ⊆ {(x, y). rel_prod (=) R x y}" "map_pmf fst z = p" "map_pmf snd z = q"
        by (auto simp: pmf.in_rel)
      with Some_Some show ?thesis unfolding rel_var.simps
        by (transfer fixing: s1 s2 z) (force simp: pmf.map_comp o_def split_beta prod_set_simps
          intro: exI[of _ "PMF (map_pmf (λ((a,b),(c,d)). ((a,c),(b,d))) z)"])
    qed auto
  qed
next
  fix R assume "R x y" and
    bis: "∀x y. R x y ⟶ rel_var (=) R (?emb1 (s1 x)) (?emb2 (s2 y))"
  from ‹R x y› show "∃R. R x y ∧ (∀x y. R x y ⟶
     rel_option (rel_pmf (rel_prod (=) R)) (s1 x) (s2 y))"
  proof (intro exI[of _ R], safe)
    fix x y
    assume "R x y"
    with bis have "rel_var (=) R (?emb1 (s1 x)) (?emb2 (s2 y))" by blast
    then obtain z where *:
        "set1_var z ⊆ {(x, y). x = y}" "set2_var z ⊆ {(x, y). R x y}"
        "?emb1 (s1 x) = map_var fst fst z" "?emb2 (s2 y) = map_var snd snd z"
        by (auto simp: rel_var.simps)
    then show "rel_option (rel_pmf (rel_prod (=) R)) (s1 x) (s2 y)"
    proof (cases "s1 x" "s2 y" rule: option.exhaust[case_product option.exhaust])
      case Some_None
      with * show ?thesis by transfer (auto simp: bempty.rep_eq elim!: var_eq.cases)
    next
      case None_Some
      with * show ?thesis by transfer (auto elim!: var_eq.cases)
    next
      case (Some_Some p q)
      with * show ?thesis
        by transfer (fastforce simp: subset_eq split_beta prod_set_defs
          elim!: var_eq.cases intro!: rel_pmf_reflI)
    qed simp
  qed
qed

(*<*)
end
(*>*)