# 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 :: "('label⇩1 × 'label⇩2) set ⇒ ('state⇩1 × 'state⇩2) set ⇒
(('label⇩1, 'state⇩1) drai × ('label⇩2, 'state⇩2) drai) set" where
[to_relAPP]: "drai_rel L S ≡ {(A⇩1, A⇩2).
(alphabeti A⇩1, alphabeti A⇩2) ∈ ⟨L⟩ list_rel ∧
(initiali A⇩1, initiali A⇩2) ∈ S ∧
(transitioni A⇩1, transitioni A⇩2) ∈ L → S → S ∧
(conditioni A⇩1, conditioni A⇩2) ∈ ⟨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 :: "('label⇩1 × 'label⇩2) set ⇒ ('state⇩1 × 'state⇩2) set ⇒
(('label⇩1, 'state⇩1) drai × ('label⇩2, 'state⇩2) dra) set" where
[to_relAPP]: "drai_dra_rel L S ≡ {(A⇩1, A⇩2).
(alphabeti A⇩1, alphabet A⇩2) ∈ ⟨L⟩ list_set_rel ∧
(initiali A⇩1, initial A⇩2) ∈ S ∧
(transitioni A⇩1, transition A⇩2) ∈ L → S → S ∧
(conditioni A⇩1, condition A⇩2) ∈ ⟨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```