# Theory DRA_Explicit

```section ‹Explicit Deterministic Rabin Automata›

theory DRA_Explicit
imports DRA_Nodes
begin

datatype ('label, 'state) drae = drae
(alphabete: "'label set")
(initiale: "'state")
(transitione: "('state × 'label × 'state) set")
(conditione: "('state set × 'state set) list")

definition drae_rel where
[to_relAPP]: "drae_rel L S ≡ {(A⇩1, A⇩2).
(alphabete A⇩1, alphabete A⇩2) ∈ ⟨L⟩ set_rel ∧
(initiale A⇩1, initiale A⇩2) ∈ S ∧
(transitione A⇩1, transitione A⇩2) ∈ ⟨S ×⇩r L ×⇩r S⟩ set_rel ∧
(conditione A⇩1, conditione A⇩2) ∈ ⟨⟨S⟩ set_rel ×⇩r ⟨S⟩ set_rel⟩ list_rel}"

lemma drae_param[param, autoref_rules]:
"(drae, drae) ∈ ⟨L⟩ set_rel → S → ⟨S ×⇩r L ×⇩r S⟩ set_rel →
⟨⟨S⟩ set_rel ×⇩r ⟨S⟩ set_rel⟩ list_rel → ⟨L, S⟩ drae_rel"
"(alphabete, alphabete) ∈ ⟨L, S⟩ drae_rel → ⟨L⟩ set_rel"
"(initiale, initiale) ∈ ⟨L, S⟩ drae_rel → S"
"(transitione, transitione) ∈ ⟨L, S⟩ drae_rel → ⟨S ×⇩r L ×⇩r S⟩ set_rel"
"(conditione, conditione) ∈ ⟨L, S⟩ drae_rel → ⟨⟨S⟩ set_rel ×⇩r ⟨S⟩ set_rel⟩ list_rel"
unfolding drae_rel_def by auto

lemma drae_rel_id[simp]: "⟨Id, Id⟩ drae_rel = Id" unfolding drae_rel_def using drae.expand by auto
lemma drae_rel_comp[simp]: "⟨L⇩1 O L⇩2, S⇩1 O S⇩2⟩ drae_rel = ⟨L⇩1, S⇩1⟩ drae_rel O ⟨L⇩2, S⇩2⟩ drae_rel"
proof safe
fix A B
assume 1: "(A, B) ∈ ⟨L⇩1 O L⇩2, S⇩1 O S⇩2⟩ drae_rel"
obtain a b c d where 2:
"(alphabete A, a) ∈ ⟨L⇩1⟩ set_rel" "(a, alphabete B) ∈ ⟨L⇩2⟩ set_rel"
"(initiale A, b) ∈ S⇩1" "(b, initiale B) ∈ S⇩2"
"(transitione A, c) ∈ ⟨S⇩1 ×⇩r L⇩1 ×⇩r S⇩1⟩ set_rel" "(c, transitione B) ∈ ⟨S⇩2 ×⇩r L⇩2 ×⇩r S⇩2⟩ set_rel"
"(conditione A, d) ∈ ⟨⟨S⇩1⟩ set_rel ×⇩r ⟨S⇩1⟩ set_rel⟩ list_rel"
"(d, conditione B) ∈ ⟨⟨S⇩2⟩ set_rel ×⇩r ⟨S⇩2⟩ set_rel⟩ list_rel"
using 1 unfolding drae_rel_def prod_rel_compp set_rel_compp by auto
show "(A, B) ∈ ⟨L⇩1, S⇩1⟩ drae_rel O ⟨L⇩2, S⇩2⟩ drae_rel"
proof
show "(A, drae a b c d) ∈ ⟨L⇩1, S⇩1⟩ drae_rel" using 2 unfolding drae_rel_def by auto
show "(drae a b c d, B) ∈ ⟨L⇩2, S⇩2⟩ drae_rel" using 2 unfolding drae_rel_def by auto
qed
next
show "(A, C) ∈ ⟨L⇩1 O L⇩2, S⇩1 O S⇩2⟩ drae_rel"
if "(A, B) ∈ ⟨L⇩1, S⇩1⟩ drae_rel" "(B, C) ∈ ⟨L⇩2, S⇩2⟩ drae_rel" for A B C
using that unfolding drae_rel_def prod_rel_compp set_rel_compp by auto
qed

(* TODO: why do we need all this setup? can't i_of_rel do the trick? *)
consts i_drae_scheme :: "interface ⇒ interface ⇒ interface"

context
begin

interpretation autoref_syn by this

lemma drae_scheme_itype[autoref_itype]:
"drae ::⇩i ⟨L⟩⇩i i_set →⇩i S →⇩i ⟨⟨S, ⟨L, S⟩⇩i i_prod⟩⇩i i_prod⟩⇩i i_set →⇩i
⟨⟨⟨S⟩⇩i i_set, ⟨S⟩⇩i i_set⟩⇩i i_prod⟩⇩i i_list →⇩i ⟨L, S⟩⇩i i_drae_scheme"
"alphabete ::⇩i ⟨L, S⟩⇩i i_drae_scheme →⇩i ⟨L⟩⇩i i_set"
"initiale ::⇩i ⟨L, S⟩⇩i i_drae_scheme →⇩i S"
"transitione ::⇩i ⟨L, S⟩⇩i i_drae_scheme →⇩i ⟨⟨S, ⟨L, S⟩⇩i i_prod⟩⇩i i_prod⟩⇩i i_set"
"conditione ::⇩i ⟨L, S⟩⇩i i_drae_scheme →⇩i ⟨⟨⟨S⟩⇩i i_set, ⟨S⟩⇩i i_set⟩⇩i i_prod⟩⇩i i_list"
by auto

end

datatype ('label, 'state) draei = draei
(alphabetei: "'label list")
(initialei: "'state")
(transitionei: "('state × 'label × 'state) list")
(conditionei: "('state list × 'state list) list")

definition draei_rel where
[to_relAPP]: "draei_rel L S ≡ {(A⇩1, A⇩2).
(alphabetei A⇩1, alphabetei A⇩2) ∈ ⟨L⟩ list_rel ∧
(initialei A⇩1, initialei A⇩2) ∈ S ∧
(transitionei A⇩1, transitionei A⇩2) ∈ ⟨S ×⇩r L ×⇩r S⟩ list_rel ∧
(conditionei A⇩1, conditionei A⇩2) ∈ ⟨⟨S⟩ list_rel ×⇩r ⟨S⟩ list_rel⟩ list_rel}"

lemma draei_param[param, autoref_rules]:
"(draei, draei) ∈ ⟨L⟩ list_rel → S → ⟨S ×⇩r L ×⇩r S⟩ list_rel →
⟨⟨S⟩ list_rel ×⇩r ⟨S⟩ list_rel⟩ list_rel → ⟨L, S⟩ draei_rel"
"(alphabetei, alphabetei) ∈ ⟨L, S⟩ draei_rel → ⟨L⟩ list_rel"
"(initialei, initialei) ∈ ⟨L, S⟩ draei_rel → S"
"(transitionei, transitionei) ∈ ⟨L, S⟩ draei_rel → ⟨S ×⇩r L ×⇩r S⟩ list_rel"
"(conditionei, conditionei) ∈ ⟨L, S⟩ draei_rel → ⟨⟨S⟩ list_rel ×⇩r ⟨S⟩ list_rel⟩ list_rel"
unfolding draei_rel_def by auto

definition draei_drae_rel where
[to_relAPP]: "draei_drae_rel L S ≡ {(A⇩1, A⇩2).
(alphabetei A⇩1, alphabete A⇩2) ∈ ⟨L⟩ list_set_rel ∧
(initialei A⇩1, initiale A⇩2) ∈ S ∧
(transitionei A⇩1, transitione A⇩2) ∈ ⟨S ×⇩r L ×⇩r S⟩ list_set_rel ∧
(conditionei A⇩1, conditione A⇩2) ∈ ⟨⟨S⟩ list_set_rel ×⇩r ⟨S⟩ list_set_rel⟩ list_rel}"

lemmas [autoref_rel_intf] = REL_INTFI[of draei_drae_rel i_drae_scheme]

lemma draei_drae_param[param, autoref_rules]:
"(draei, drae) ∈ ⟨L⟩ list_set_rel → S → ⟨S ×⇩r L ×⇩r S⟩ list_set_rel →
⟨⟨S⟩ list_set_rel ×⇩r ⟨S⟩ list_set_rel⟩ list_rel → ⟨L, S⟩ draei_drae_rel"
"(alphabetei, alphabete) ∈ ⟨L, S⟩ draei_drae_rel → ⟨L⟩ list_set_rel"
"(initialei, initiale) ∈ ⟨L, S⟩ draei_drae_rel → S"
"(transitionei, transitione) ∈ ⟨L, S⟩ draei_drae_rel → ⟨S ×⇩r L ×⇩r S⟩ list_set_rel"
"(conditionei, conditione) ∈ ⟨L, S⟩ draei_drae_rel → ⟨⟨S⟩ list_set_rel ×⇩r ⟨S⟩ list_set_rel⟩ list_rel"
unfolding draei_drae_rel_def by auto

definition draei_drae where
"draei_drae A ≡ drae (set (alphabetei A)) (initialei A)
(set (transitionei A)) (map (map_prod set set) (conditionei A))"

lemma draei_drae_id_param[param]: "(draei_drae, id) ∈ ⟨L, S⟩ draei_drae_rel → ⟨L, S⟩ drae_rel"
proof
fix Ai A
assume 1: "(Ai, A) ∈ ⟨L, S⟩ draei_drae_rel"
have 2: "draei_drae Ai = drae (set (alphabetei Ai)) (initialei Ai)
(set (transitionei Ai)) (map (map_prod set set) (conditionei Ai))" unfolding draei_drae_def by rule
have 3: "id A = drae (id (alphabete A)) (initiale A)
(id (transitione A)) (map (map_prod id id) (conditione A))" by simp
show "(draei_drae Ai, id A) ∈ ⟨L, S⟩ drae_rel" unfolding 2 3 using 1 by parametricity
qed

abbreviation "transitions L S s ≡ ⋃ a ∈ L. ⋃ p ∈ S. {p} × {a} × {s a p}"
abbreviation "succs T a p ≡ the_elem ((T `` {p}) `` {a})"

definition wft :: "'label set ⇒ 'state set ⇒ ('state × 'label × 'state) set ⇒ bool" where
"wft L S T ≡ ∀ a ∈ L. ∀ p ∈ S. is_singleton ((T `` {p}) `` {a})"

lemma wft_param[param]:
assumes "bijective S" "bijective L"
shows "(wft, wft) ∈ ⟨L⟩ set_rel → ⟨S⟩ set_rel → ⟨S ×⇩r L ×⇩r S⟩ set_rel → bool_rel"
using assms unfolding wft_def by parametricity

lemma wft_transitions: "wft L S (transitions L S s)" unfolding wft_def is_singleton_def by auto

definition dra_drae where "dra_drae A ≡ drae (alphabet A) (initial A)
(transitions (alphabet A) (nodes A) (transition A))
(map (λ (P, Q). (Set.filter P (nodes A), Set.filter Q (nodes A))) (condition A))"
definition drae_dra where "drae_dra A ≡ dra (alphabete A) (initiale A)
(succs (transitione A)) (map (λ (I, F). (λ p. p ∈ I, λ p. p ∈ F)) (conditione A))"

lemma set_rel_Domain_Range[intro!, simp]: "(Domain A, Range A) ∈ ⟨A⟩ set_rel" unfolding set_rel_def by auto

lemma dra_drae_param[param]: "(dra_drae, dra_drae) ∈ ⟨L, S⟩ dra_rel → ⟨L, S⟩ drae_rel"
unfolding dra_drae_def by parametricity
lemma drae_dra_param[param]:
assumes "bijective L" "bijective S"
assumes "wft (Range L) (Range S) (transitione B)"
assumes [param]: "(A, B) ∈ ⟨L, S⟩ drae_rel"
shows "(drae_dra A, drae_dra B) ∈ ⟨L, S⟩ dra_rel"
proof -
have 1: "(wft (Domain L) (Domain S) (transitione A), wft (Range L) (Range S) (transitione B)) ∈ bool_rel"
using assms(1, 2) by parametricity auto
have 2: "wft (Domain L) (Domain S) (transitione A)" using assms(3) 1 by simp
show ?thesis
using assms(1 - 3) 2 assms(2)[unfolded bijective_alt]
unfolding drae_dra_def wft_def
by parametricity force+
qed

lemma succs_transitions_param[param]:
"(succs ∘ transitions L S, id) ∈ (Id_on L → Id_on S → Id_on S) → (Id_on L → Id_on S → Id_on S)"
proof
fix f g
assume 1[param]: "(f, g) ∈ Id_on L → Id_on S → Id_on S"
show "((succs ∘ transitions L S) f, id g) ∈ Id_on L → Id_on S → Id_on S"
proof safe
fix a p
assume 2: "a ∈ L" "p ∈ S"
have "(succs ∘ transitions L S) f a p = succs (transitions L S f) a p" by simp
also have "(transitions L S f `` {p}) `` {a} = {f a p}" using 2 by auto
also have "the_elem … = f a p" by simp
also have "(…, g a p) ∈ Id_on S" using 2 by parametricity auto
finally show "(succs ∘ transitions L S) f a p = id g a p" by simp
show "id g a p ∈ S" using 1[param_fo] 2 by simp
qed
qed
lemma drae_dra_dra_drae_param[param]:
"((drae_dra ∘ dra_drae) A, id A) ∈ ⟨Id_on (alphabet A), Id_on (nodes A)⟩ dra_rel"
proof -
have [param]: "(λ (P, Q). (λ p. p ∈ Set.filter P (nodes A), λ p. p ∈ Set.filter Q (nodes A)), id) ∈
pred_rel (Id_on (nodes A)) ×⇩r pred_rel (Id_on (nodes A)) → rabin_rel (Id_on (nodes A))"
unfolding fun_rel_def Id_on_def by auto
have "(drae_dra ∘ dra_drae) A = dra (alphabet A) (initial A)
((succs ∘ transitions (alphabet A) (nodes A)) (transition A))
(map (λ (P, Q). (λ p. p ∈ Set.filter P (nodes A), λ p. p ∈ Set.filter Q (nodes A))) (condition A))"
unfolding drae_dra_def dra_drae_def by auto
also have "(…, dra (alphabet A) (initial A) (id (transition A)) (map id (condition A))) ∈
⟨Id_on (alphabet A), Id_on (nodes A)⟩ dra_rel" using dra_rel_eq by parametricity auto
also have "dra (alphabet A) (initial A) (id (transition A)) (map id (condition A)) = id A" by simp
finally show ?thesis by this
qed

definition draei_dra_rel where
[to_relAPP]: "draei_dra_rel L S ≡ {(Ae, A). (drae_dra (draei_drae Ae), A) ∈ ⟨L, S⟩ dra_rel}"
lemma draei_dra_id[param]: "(drae_dra ∘ draei_drae, id) ∈ ⟨L, S⟩ draei_dra_rel → ⟨L, S⟩ dra_rel"
unfolding draei_dra_rel_def by auto

(*
schematic_goal drae_dra_impl: "(?f, drae_dra) ∈ ⟨Id, Id⟩ draei_drae_rel → ⟨Id, Id⟩ drai_dra_rel"
unfolding drae_dra_def by (autoref (trace))
concrete_definition drae_dra_impl uses drae_dra_impl
*)

end```