# Theory DRA_Refine

section ‹Relations on Deterministic Rabin Automata›

theory DRA_Refine
imports
"DRA"

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