Theory DRA_Translate
section ‹Explore and Enumerate Nodes of Deterministic Rabin Automata›
theory DRA_Translate
imports DRA_Explicit
begin
subsection ‹Syntax›
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]: "drae_image id = id" 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"
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"
unfolding trans_algo_def by (autoref_monadic (plain))
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
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]: "Domain rel = f ` nodes A" unfolding rel_def by force
lemma rel_range[simp]: "Range rel = nodes A" unfolding rel_def by auto
lemma [intro!, simp]: "bijective rel" 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