Theory DRA_Implement

section ‹Implementation of Deterministic Rabin Automata›

theory DRA_Implement
imports
  "DRA_Refine"
  "../../Basic/Implement"
begin

  datatype ('label, 'state) drai = drai
    (alphabeti: "'label list")
    (initiali: "'state")
    (transitioni: "'label ⇒ 'state ⇒ 'state")
    (conditioni: "'state rabin gen")

  definition drai_rel :: "('label1 × 'label2) set ⇒ ('state1 × 'state2) set ⇒
    (('label1, 'state1) drai × ('label2, 'state2) drai) set" where
    [to_relAPP]: "drai_rel L S ≡ {(A1, A2).
      (alphabeti A1, alphabeti A2) ∈ ⟨L⟩ list_rel ∧
      (initiali A1, initiali A2) ∈ S ∧
      (transitioni A1, transitioni A2) ∈ L → S → S ∧
      (conditioni A1, conditioni A2) ∈ ⟨rabin_rel S⟩ list_rel}"

  lemma drai_param[param]:
    "(drai, drai) ∈ ⟨L⟩ list_rel → S → (L → S → S) →
      ⟨rabin_rel S⟩ list_rel → ⟨L, S⟩ drai_rel"
    "(alphabeti, alphabeti) ∈ ⟨L, S⟩ drai_rel → ⟨L⟩ list_rel"
    "(initiali, initiali) ∈ ⟨L, S⟩ drai_rel → S"
    "(transitioni, transitioni) ∈ ⟨L, S⟩ drai_rel → L → S → S"
    "(conditioni, conditioni) ∈ ⟨L, S⟩ drai_rel → ⟨rabin_rel S⟩ list_rel"
    unfolding drai_rel_def fun_rel_def by auto

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

  lemma drai_dra_param[param, autoref_rules]:
    "(drai, dra) ∈ ⟨L⟩ list_set_rel → S → (L → S → S) →
      ⟨rabin_rel S⟩ list_rel → ⟨L, S⟩ drai_dra_rel"
    "(alphabeti, alphabet) ∈ ⟨L, S⟩ drai_dra_rel → ⟨L⟩ list_set_rel"
    "(initiali, initial) ∈ ⟨L, S⟩ drai_dra_rel → S"
    "(transitioni, transition) ∈ ⟨L, S⟩ drai_dra_rel → L → S → S"
    "(conditioni, condition) ∈ ⟨L, S⟩ drai_dra_rel → ⟨rabin_rel S⟩ list_rel"
    unfolding drai_dra_rel_def fun_rel_def by auto

  definition drai_dra :: "('label, 'state) drai ⇒ ('label, 'state) dra" where
    "drai_dra A ≡ dra (set (alphabeti A)) (initiali A) (transitioni A) (conditioni A)"
  definition drai_invar :: "('label, 'state) drai ⇒ bool" where
    "drai_invar A ≡ distinct (alphabeti A)"

  lemma drai_dra_id_param[param]: "(drai_dra, id) ∈ ⟨L, S⟩ drai_dra_rel → ⟨L, S⟩ dra_rel"
  proof
    fix Ai A
    assume 1: "(Ai, A) ∈ ⟨L, S⟩ drai_dra_rel"
    have 2: "drai_dra Ai = dra (set (alphabeti Ai)) (initiali Ai) (transitioni Ai) (conditioni Ai)"
      unfolding drai_dra_def by rule
    have 3: "id A = dra (id (alphabet A)) (initial A) (transition A) (condition A)" by simp
    show "(drai_dra Ai, id A) ∈ ⟨L, S⟩ dra_rel" unfolding 2 3 using 1 by parametricity
  qed

  lemma drai_dra_br: "⟨Id, Id⟩ drai_dra_rel = br drai_dra drai_invar"
  proof safe
    show "(A, B) ∈ ⟨Id, Id⟩ drai_dra_rel" if "(A, B) ∈ br drai_dra drai_invar"
      for A and B :: "('a, 'b) dra"
      using that unfolding drai_dra_rel_def drai_dra_def drai_invar_def
      by (auto simp: in_br_conv list_set_rel_def)
    show "(A, B) ∈ br drai_dra drai_invar" if "(A, B) ∈ ⟨Id, Id⟩ drai_dra_rel"
      for A and B :: "('a, 'b) dra"
    proof -
      have 1: "(drai_dra A, id B) ∈ ⟨Id, Id⟩ dra_rel" using that by parametricity
      have 2: "drai_invar A"
        using drai_dra_param(2 - 5)[param_fo, OF that]
        by (auto simp: in_br_conv list_set_rel_def drai_invar_def)
      show ?thesis using 1 2 unfolding in_br_conv by auto
    qed
  qed

end