# Theory DRA_Translate

section ‹Explore and Enumerate Nodes of Deterministic Rabin Automata›

theory DRA_Translate
imports DRA_Explicit
begin

subsection ‹Syntax›

(* TODO: this syntax has unnecessarily high inner binding strength, requiring extra parentheses
the regular let syntax correctly uses inner binding strength 0: ("(2_ =/ _)" 10) *)
no_syntax "_do_let" :: "[pttrn, 'a]  do_bind" ("(2let _ =/ _)" [1000, 13] 13)
syntax "_do_let" :: "[pttrn, 'a]  do_bind" ("(2let _ =/ _)" 13)

section ‹Image on Explicit Automata›

definition drae_image where "drae_image f A  drae (alphabete A) (f (initiale A))
((λ (p, a, q). (f p, a, f q)) ` transitione A) (map (map_prod (image f) (image f)) (conditione A))"

lemma drae_image_param[param]: "(drae_image, drae_image)  (S  T)  L, S drae_rel  L, T drae_rel"
unfolding drae_image_def by parametricity

lemma drae_image_id[simp]:  unfolding drae_image_def by auto
lemma drae_image_dra_drae: "drae_image f (dra_drae A) = drae
(alphabet A) (f (initial A))
( p  nodes A.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p})
(map (λ (P, Q). (f ` {p  nodes A. P p}, f ` {p  nodes A. Q p})) (condition A))"
unfolding dra_drae_def drae_image_def drae.simps Set.filter_def by force

section ‹Exploration and Translation›

definition trans_spec where
"trans_spec A f   p  nodes A.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p}"

definition trans_algo where
"trans_algo N L S f
FOREACH N (λ p T. do {
ASSERT (p  N);
FOREACH L (λ a T. do {
ASSERT (a  L);
let q = S a p;
ASSERT ((f p, a, f q)  T);
RETURN (insert (f p, a, f q) T) }
) T }
) {}"

lemma trans_algo_refine:
assumes "finite (nodes A)" "finite (alphabet A)" "inj_on f (nodes A)"
assumes "N = nodes A" "L = alphabet A" "S = transition A"
shows "(trans_algo N L S f, SPEC (HOL.eq (trans_spec A f)))  Id nres_rel"
unfolding trans_algo_def trans_spec_def assms(4-6)
proof (refine_vcg FOREACH_rule_insert_eq)
show "finite (nodes A)" using assms(1) by this
show "( p  nodes A.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p}) =
( p  nodes A.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p})" by rule
show "( p  {}.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p}) = {}" by simp
fix T x
assume 1: "T  nodes A" "x  nodes A" "x  T"
show "finite (alphabet A)" using assms(2) by this
show "( a  {}. f ` {x} × {a} × f ` {transition A a x})
( p  T.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p}) =
( p  T.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p})"
"( a  alphabet A. f ` {x} × {a} × f ` {transition A a x})
( p  T.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p}) =
( p  insert x T.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p})" by auto
fix Ta xa
assume 2: "Ta  alphabet A" "xa  alphabet A" "xa  Ta"
show "(f x, xa, f (transition A xa x))  ( a  Ta. f ` {x} × {a} × f ` {transition A a x})
( p  T.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p})"
using 1 2(3) assms(3) by (auto dest: inj_onD)
show "( a  insert xa Ta. f ` {x} × {a} × f ` {transition A a x})
( p  T.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p}) =
insert (f x, xa, f (transition A xa x)) (( a  Ta. f ` {x} × {a} × f ` {transition A a x})
( p  T.  a  alphabet A. f ` {p} × {a} × f ` {transition A a p}))"
by simp
qed

definition to_draei :: "('state, 'label) dra  ('state, 'label) dra"
where "to_draei  id"

(* TODO: make separate implementations for "dra_drae" and "op_set_enumerate ⤜ drae_image" *)
schematic_goal to_draei_impl:
fixes S :: "('statei × 'state) set"
assumes [simp]: "finite (nodes A)"
assumes [autoref_ga_rules]: "is_bounded_hashcode S seq bhc"
assumes [autoref_ga_rules]: "is_valid_def_hm_size TYPE('statei) hms"
assumes [autoref_rules]: "(seq, HOL.eq)  S  S  bool_rel"
assumes [autoref_rules]: "(Ai, A)  L, S drai_dra_rel"
shows "(?f :: ?'a, do {
let N = nodes A;
f  op_set_enumerate N;
ASSERT (dom f = N);
ASSERT (f (initial A)  None);
ASSERT ( a  alphabet A.  p  dom f. f (transition A a p)  None);
T  trans_algo N (alphabet A) (transition A) (λ x. the (f x));
RETURN (drae (alphabet A) ((λ x. the (f x)) (initial A)) T
(map (λ (P, Q). ((λ x. the (f x)) ` {p  N. P p}, (λ x. the (f x)) ` {p  N. Q p})) (condition A)))
})  ?R"
concrete_definition to_draei_impl uses to_draei_impl
lemma to_draei_impl_refine'':
fixes S :: "('statei × 'state) set"
assumes "finite (nodes A)"
assumes "is_bounded_hashcode S seq bhc"
assumes "is_valid_def_hm_size TYPE('statei) hms"
assumes "(seq, HOL.eq)  S  S  bool_rel"
assumes "(Ai, A)  L, S drai_dra_rel"
shows "(RETURN (to_draei_impl seq bhc hms Ai), do {
f  op_set_enumerate (nodes A);
RETURN (drae_image (the  f) (dra_drae A))
})  L, nat_rel draei_drae_rel nres_rel"
proof -
have 1: "finite (alphabet A)"
using drai_dra_param(2)[param_fo, OF assms(5)] list_set_rel_finite
unfolding finite_set_rel_def by auto
note to_draei_impl.refine[OF assms]
also have "(do {
let N = nodes A;
f  op_set_enumerate N;
ASSERT (dom f = N);
ASSERT (f (initial A)  None);
ASSERT ( a  alphabet A.  p  dom f. f (transition A a p)  None);
T  trans_algo N (alphabet A) (transition A) (λ x. the (f x));
RETURN (drae (alphabet A) ((λ x. the (f x)) (initial A)) T
(map (λ (P, Q). ((λ x. the (f x)) ` {p  N. P p}, (λ x. the (f x)) ` {p  N. Q p})) (condition A)))
}, do {
f  op_set_enumerate (nodes A);
T  SPEC (HOL.eq (trans_spec A (λ x. the (f x))));
RETURN (drae (alphabet A) ((λ x. the (f x)) (initial A)) T
(map (λ (P, Q). ((λ x. the (f x)) ` {p  nodes A. P p}, (λ x. the (f x)) ` {p  nodes A. Q p})) (condition A)))
})  Id nres_rel"
unfolding Let_def comp_apply op_set_enumerate_def using assms(1) 1
by (refine_vcg vcg0[OF trans_algo_refine]) (auto intro!: inj_on_map_the[unfolded comp_apply])
also have "(do {
f  op_set_enumerate (nodes A);
T  SPEC (HOL.eq (trans_spec A (λ x. the (f x))));
RETURN (drae (alphabet A) ((λ x. the (f x)) (initial A)) T
(map (λ (P, Q). ((λ x. the (f x)) ` {p  nodes A. P p}, (λ x. the (f x)) ` {p  nodes A. Q p})) (condition A)))
},  do {
f  op_set_enumerate (nodes A);
RETURN (drae_image (the  f) (dra_drae A))
})  Id nres_rel"
unfolding trans_spec_def drae_image_dra_drae by refine_vcg force
finally show ?thesis unfolding nres_rel_comp by simp
qed

(* TODO: generalize L *)
context
fixes Ai A
fixes seq bhc hms
fixes S :: "('statei × 'state) set"
assumes a: "finite (nodes A)"
assumes b: "is_bounded_hashcode S seq bhc"
assumes c: "is_valid_def_hm_size TYPE('statei) hms"
assumes d: "(seq, HOL.eq)  S  S  bool_rel"
assumes e: "(Ai, A)  Id, S drai_dra_rel"
begin

definition f' where "f'  SOME f'.
(to_draei_impl seq bhc hms Ai, drae_image (the  f') (dra_drae A))  Id, nat_rel draei_drae_rel
dom f' = nodes A  inj_on f' (nodes A)"

lemma 1: " f'. (to_draei_impl seq bhc hms Ai, drae_image (the  f') (dra_drae A))
Id, nat_rel draei_drae_rel  dom f' = nodes A  inj_on f' (nodes A)"
using to_draei_impl_refine''[
OF a b c d e,
unfolded op_set_enumerate_def bind_RES_RETURN_eq,
THEN nres_relD,
THEN RETURN_ref_SPECD]
by force

lemma f'_refine: "(to_draei_impl seq bhc hms Ai, drae_image (the  f') (dra_drae A))
Id, nat_rel draei_drae_rel" using someI_ex[OF 1, folded f'_def] by auto
lemma f'_dom: "dom f' = nodes A" using someI_ex[OF 1, folded f'_def] by auto
lemma f'_inj: "inj_on f' (nodes A)" using someI_ex[OF 1, folded f'_def] by auto

definition f where "f  the  f'"
definition g where "g = inv_into (nodes A) f"
lemma inj_f[intro!, simp]: "inj_on f (nodes A)"
using f'_inj f'_dom unfolding f_def by (simp add: inj_on_map_the)
lemma inj_g[intro!, simp]: "inj_on g (f ` nodes A)"
unfolding g_def by (simp add: inj_on_inv_into)

definition rel where "rel  {(f p, p) |p. p  nodes A}"
lemma rel_alt_def: "rel = (br f (λ p. p  nodes A))¯"
unfolding rel_def by (auto simp: in_br_conv)
lemma rel_inv_def: "rel = br g (λ k. k  f ` nodes A)"
unfolding rel_alt_def g_def by (auto simp: in_br_conv)
lemma rel_domain[simp]:  unfolding rel_def by force
lemma rel_range[simp]:  unfolding rel_def by auto
lemma [intro!, simp]:  unfolding rel_inv_def by (simp add: bijective_alt)
lemma [simp]: "Id_on (f ` nodes A) O rel = rel" unfolding rel_def by auto
lemma [simp]: "rel O Id_on (nodes A) = rel" unfolding rel_def by auto

lemma [param]: "(f, f)  Id_on (Range rel)  Id_on (Domain rel)" unfolding rel_alt_def by auto
lemma [param]: "(g, g)  Id_on (Domain rel)  Id_on (Range rel)" unfolding rel_inv_def by auto
lemma [param]: "(id, f)  rel  Id_on (Domain rel)" unfolding rel_alt_def by (auto simp: in_br_conv)
lemma [param]: "(f, id)  Id_on (Range rel)  rel" unfolding rel_alt_def by (auto simp: in_br_conv)
lemma [param]: "(id, g)  Id_on (Domain rel)  rel" unfolding rel_inv_def by (auto simp: in_br_conv)
lemma [param]: "(g, id)  rel  Id_on (Range rel)" unfolding rel_inv_def by (auto simp: in_br_conv)

lemma to_draei_impl_refine':
"(to_draei_impl seq bhc hms Ai, to_draei A)  Id_on (alphabet A), rel draei_dra_rel"
proof -
have 1: "(draei_drae (to_draei_impl seq bhc hms Ai), id (drae_image f (dra_drae A)))
Id, nat_rel drae_rel" using f'_refine[folded f_def] by parametricity
have 2: "(draei_drae (to_draei_impl seq bhc hms Ai), id (drae_image f (dra_drae A)))
Id_on (alphabet A), Id_on (f ` nodes A) drae_rel"
using 1 unfolding drae_rel_def dra_drae_def drae_image_def by auto

have 3: "wft (alphabet A) (nodes A) (transitione (dra_drae A))"
using wft_transitions unfolding dra_drae_def drae.sel by this
have 4: "(wft (alphabet A) (f ` nodes A) (transitione (drae_image f (dra_drae A))),
wft (alphabet A) (id ` nodes A) (transitione (drae_image id (dra_drae A))))  bool_rel"
using dra_rel_eq by parametricity auto
have 5: "wft (alphabet A) (f ` nodes A) (transitione (drae_image f (dra_drae A)))" using 3 4 by simp

have "(drae_dra (draei_drae (to_draei_impl seq bhc hms Ai)), drae_dra (id (drae_image f (dra_drae A))))
Id_on (alphabet A), Id_on (f ` nodes A) dra_rel" using 2 5 by parametricity auto
also have "(drae_dra (id (drae_image f (dra_drae A))), drae_dra (id (drae_image id (dra_drae A))))
Id_on (alphabet A), rel dra_rel" using dra_rel_eq 3 by parametricity auto
also have "drae_dra (id (drae_image id (dra_drae A))) = (drae_dra  dra_drae) A" by simp
also have "(, id A)  Id_on (alphabet A), Id_on (nodes A) dra_rel" by parametricity
also have "id A = to_draei A" unfolding to_draei_def by simp
finally show ?thesis unfolding draei_dra_rel_def by simp
qed

end

context
begin

interpretation autoref_syn by this

lemma to_draei_impl_refine[autoref_rules]:
fixes S :: "('statei × 'state) set"
assumes "SIDE_PRECOND (finite (nodes A))"
assumes "SIDE_GEN_ALGO (is_bounded_hashcode S seq bhc)"
assumes "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('statei) hms)"
assumes "GEN_OP seq HOL.eq (S  S  bool_rel)"
assumes "(Ai, A)  Id, S drai_dra_rel"
shows "(to_draei_impl seq bhc hms Ai,
(OP to_draei ::: Id, S drai_dra_rel
Id_on (alphabet A), rel Ai A seq bhc hms draei_dra_rel) \$ A)
Id_on (alphabet A), rel Ai A seq bhc hms draei_dra_rel"
using to_draei_impl_refine' assms unfolding autoref_tag_defs by this

end

end