Theory DRA_Refine

section ‹Relations on Deterministic Rabin Automata›

theory DRA_Refine
imports
  "DRA"
  "../../Basic/Acceptance_Refine"
  "../../Transition_Systems/Transition_System_Refine"
begin

  definition dra_rel :: "('label1 × 'label2) set ⇒ ('state1 × 'state2) set ⇒
    (('label1, 'state1) dra × ('label2, 'state2) dra) set" where
    [to_relAPP]: "dra_rel L S ≡ {(A1, A2).
      (alphabet A1, alphabet A2) ∈ ⟨L⟩ set_rel ∧
      (initial A1, initial A2) ∈ S ∧
      (transition A1, transition A2) ∈ L → S → S ∧
      (condition A1, condition A2) ∈ ⟨rabin_rel S⟩ list_rel}"

  lemma dra_param[param]:
    "(dra, dra) ∈ ⟨L⟩ set_rel → S → (L → S → S) → ⟨rabin_rel S⟩ list_rel →
      ⟨L, S⟩ dra_rel"
    "(alphabet, alphabet) ∈ ⟨L, S⟩ dra_rel → ⟨L⟩ set_rel"
    "(initial, initial) ∈ ⟨L, S⟩ dra_rel → S"
    "(transition, transition) ∈ ⟨L, S⟩ dra_rel → L → S → S"
    "(condition, condition) ∈ ⟨L, S⟩ dra_rel → ⟨rabin_rel S⟩ list_rel"
    unfolding dra_rel_def fun_rel_def by auto

  lemma dra_rel_id[simp]: "⟨Id, Id⟩ dra_rel = Id" unfolding dra_rel_def using dra.expand by auto
  lemma dra_rel_comp[trans]:
    assumes [param]: "(A, B) ∈ ⟨L1, S1⟩ dra_rel" "(B, C) ∈ ⟨L2, S2⟩ dra_rel"
    shows "(A, C) ∈ ⟨L1 O L2, S1 O S2⟩ dra_rel"
  proof -
    have "(condition A, condition B) ∈ ⟨rabin_rel S1⟩ list_rel" by parametricity
    also have "(condition B, condition C) ∈ ⟨rabin_rel S2⟩ list_rel" by parametricity
    finally have 1: "(condition A, condition C) ∈ ⟨rabin_rel S1 O rabin_rel S2⟩ list_rel" by simp
    have 2: "rabin_rel S1 O rabin_rel S2 ⊆ rabin_rel (S1 O S2)" by (force simp: fun_rel_def)
    have 3: "(condition A, condition C) ∈ ⟨rabin_rel (S1 O S2)⟩ list_rel" using 1 2 list_rel_mono by blast
    have "(transition A, transition B) ∈ L1 → S1 → S1" by parametricity
    also have "(transition B, transition C) ∈ L2 → S2 → S2" by parametricity
    finally have 4: "(transition A, transition C) ∈ L1 O L2 → S1 O S2 → S1 O S2" by this
    show ?thesis
      unfolding dra_rel_def mem_Collect_eq prod.case set_rel_compp
      using 3 4
      using dra_param(2 - 5)[THEN fun_relD, OF assms(1)]
      using dra_param(2 - 5)[THEN fun_relD, OF assms(2)]
      by auto
  qed
  lemma dra_rel_converse[simp]: "(⟨L, S⟩ dra_rel)¯ = ⟨L¯, S¯⟩ dra_rel"
  proof -
    have 1: "⟨L⟩ set_rel = (⟨L¯⟩ set_rel)¯" by simp
    have 2: "⟨S⟩ set_rel = (⟨S¯⟩ set_rel)¯" by simp
    have 3: "L → S → S = (L¯ → S¯ → S¯)¯" by simp
    have 4: "⟨rabin_rel S⟩ list_rel = (⟨rabin_rel (S¯)⟩ list_rel)¯" by simp
    show ?thesis unfolding dra_rel_def unfolding 3 unfolding 1 2 4 by fastforce
  qed

  lemma dra_rel_eq: "(A, A) ∈ ⟨Id_on (alphabet A), Id_on (nodes A)⟩ dra_rel"
    unfolding dra_rel_def prod_rel_def using list_all2_same[to_set] by auto

  lemma enableds_param[param]: "(dra.enableds, dra.enableds) ∈ ⟨L, S⟩ dra_rel → S → ⟨L⟩ set_rel"
    unfolding dra.enableds_def Collect_mem_eq by parametricity
  lemma paths_param[param]: "(dra.paths, dra.paths) ∈ ⟨L, S⟩ dra_rel → S → ⟨⟨L⟩ list_rel⟩ set_rel"
    using enableds_param[param_fo] by parametricity
  lemma runs_param[param]: "(dra.runs, dra.runs) ∈ ⟨L, S⟩ dra_rel → S → ⟨⟨L⟩ stream_rel⟩ set_rel"
    using enableds_param[param_fo] by parametricity

  lemma reachable_param[param]: "(reachable, reachable) ∈ ⟨L, S⟩ dra_rel → S → ⟨S⟩ set_rel"
  proof -
    have 1: "reachable A p = (λ w. target A w p) ` dra.paths A p" for A :: "('label, 'state) dra" and p
      unfolding dra.reachable_alt_def dra.paths_def by auto
    show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity
  qed
  lemma nodes_param[param]: "(nodes, nodes) ∈ ⟨L, S⟩ dra_rel → ⟨S⟩ set_rel"
  proof -
    have 1: "nodes A = reachable A (initial A)" for A :: "('label, 'state) dra"
      unfolding dra.nodes_alt_def by simp
    show ?thesis unfolding 1 by parametricity
  qed

  lemma language_param[param]: "(language, language) ∈ ⟨L, S⟩ dra_rel → ⟨⟨L⟩ stream_rel⟩ set_rel"
  proof -
    have 1: "language A = (⋃ w ∈ dra.runs A (initial A).
      if cogen rabin (condition A) (initial A ## trace A w (initial A)) then {w} else {})"
      for A :: "('label, 'state) dra"
      unfolding dra.language_def dra.runs_def by auto
    show ?thesis unfolding 1 using enableds_param[param_fo] by parametricity
  qed

end