Theory Mojmir_Rabin_Impl
section ‹Executable Translation from Mojmir to Rabin Automata›
theory Mojmir_Rabin_Impl
imports Main "../Mojmir_Rabin"
begin
fun init :: "'a ⇒ 'a list"
where
"init q⇩0 = [q⇩0]"
fun nxt :: "'b set ⇒ ('a, 'b) DTS ⇒ 'a ⇒ ('a list, 'b) DTS"
where
"nxt Σ δ q⇩0 = (λqs ν. remdups_fwd ((filter (λq. ¬semi_mojmir_def.sink Σ δ q⇩0 q) (map (λq. δ q ν) qs)) @ [q⇩0]))"
fun rk :: "'a list ⇒ 'a ⇒ nat option"
where
"rk qs q = (let i = index qs q in if i ≠ length qs then Some i else None)"
fun fail_filt :: "'b set ⇒ ('a, 'b) DTS ⇒ 'a ⇒ ('a ⇒ bool) ⇒ ('a list, 'b) transition ⇒ bool"
where
"fail_filt Σ δ q⇩0 F (r, ν, _) = (∃q ∈ set r. let q' = δ q ν in (¬F q') ∧ semi_mojmir_def.sink Σ δ q⇩0 q')"
fun merge_filt :: "('a, 'b) DTS ⇒ 'a ⇒ ('a ⇒ bool) ⇒ nat ⇒ ('a list, 'b) transition ⇒ bool"
where
"merge_filt δ q⇩0 F i (r, ν, _) = (∃q ∈ set r. let q' = δ q ν in the (rk r q) < i ∧ ¬F q' ∧ ((∃q'' ∈ set r. q'' ≠ q ∧ δ q'' ν = q') ∨ q' = q⇩0))"
fun succeed_filt :: "('a, 'b) DTS ⇒ 'a ⇒ ('a ⇒ bool) ⇒ nat ⇒ ('a list, 'b) transition ⇒ bool"
where
"succeed_filt δ q⇩0 F i (r, ν, _) = (∃q ∈ set r. let q' = δ q ν in rk r q = Some i ∧ (¬F q ∨ q = q⇩0) ∧ F q')"
subsubsection ‹nxt Properties›
lemma nxt_run_distinct:
"distinct (run (nxt Σ Δ q⇩0) (init q⇩0) w n)"
by (cases n; simp del: remdups_fwd.simps; metis (no_types) remdups_fwd_distinct)
lemma nxt_run_reverse_step:
fixes Σ δ q⇩0 w
defines "r ≡ run (nxt Σ δ q⇩0) (init q⇩0) w"
assumes "q ∈ set (r (Suc n))"
assumes "q ≠ q⇩0"
shows "∃q' ∈ set (r n). δ q' (w n) = q"
using assms(2-3) unfolding r_def run.simps nxt.simps remdups_fwd_set by auto
lemma nxt_run_sink_free:
"q ∈ set (run (nxt Σ δ q⇩0) (init q⇩0) w n) ⟹ ¬semi_mojmir_def.sink Σ δ q⇩0 q"
by (induction n) (simp_all add: semi_mojmir_def.sink_def del: remdups_fwd.simps, blast)
subsubsection ‹rk Properties›
lemma rk_bounded:
"rk xs x = Some i ⟹ i < length xs"
by (simp add: Let_def) (metis index_conv_size_if_notin index_less_size_conv option.distinct(1) option.inject)
lemma rk_facts:
"x ∈ set xs ⟷ rk xs x ≠ None"
"x ∈ set xs ⟷ (∃i. rk xs x = Some i)"
using rk_bounded by (simp add: index_size_conv)+
lemma rk_split:
"y ∉ set xs ⟹ rk (xs @ y # zs) y = Some (length xs)"
by (induction xs) auto
lemma rk_split_card:
"y ∉ set xs ⟹ distinct xs ⟹ rk (xs @ y # zs) y = Some (card (set xs))"
using rk_split by (metis length_remdups_card_conv remdups_id_iff_distinct)
lemma rk_split_card_takeWhile:
assumes "x ∈ set xs"
assumes "distinct xs"
shows "rk xs x = Some (card (set (takeWhile (λy. y ≠ x) xs)))"
proof -
obtain ys zs where "xs = ys @ x # zs" and "x ∉ set ys"
using assms by (blast dest: split_list_first)
moreover
hence "distinct ys" and "ys = takeWhile (λy. y ≠ x) xs"
using takeWhile_foo assms by (simp, fast)
ultimately
show ?thesis
using rk_split_card by metis
qed
lemma take_rk:
assumes "distinct xs"
shows "set (take i xs) = {q. ∃j < i. rk xs q = Some j}"
(is "?rhs = ?lhs")
using assms
proof (induction i arbitrary: xs)
case (Suc i)
thus ?case
proof (induction xs)
case (Cons x xs)
have "set (take (Suc i) (x # xs)) = {x} ∪ set (take i xs)"
by simp
also
have "… = {x} ∪ {q. ∃j < i. rk xs q = Some j}"
using Cons by simp
finally
show ?case
by force
qed simp
qed simp
lemma drop_rk:
assumes "distinct xs"
shows "set (drop i xs) = {q. ∃j ≥ i. rk xs q = Some j}"
proof -
have "set xs = {q. ∃j. rk xs q = Some j}" (is "_ = ?U")
using rk_facts(2)[of _ xs] by blast
moreover
have "?U = {q. ∃j ≥ i. rk xs q = Some j} ∪ {q. ∃j < i. rk xs q = Some j}"
and "{} = {q. ∃j ≥ i. rk xs q = Some j} ∩ {q. ∃j < i. rk xs q = Some j}"
by auto
moreover
have "set xs = set (drop i xs) ∪ set (take i xs)"
and "{} = set (drop i xs) ∩ set (take i xs)"
by (metis assms append_take_drop_id inf_sup_aci(1,5) distinct_append set_append)+
ultimately
show ?thesis
using take_rk[OF assms] by blast
qed
subsubsection ‹Relation to (Semi) Mojmir Automata›
lemma (in semi_mojmir) nxt_run_configuration:
defines "r ≡ run (nxt Σ δ q⇩0) (init q⇩0) w"
shows "q ∈ set (r n) ⟷ ¬sink q ∧ configuration q n ≠ {}"
proof (induction n arbitrary: q)
case (Suc n)
thus ?case
proof (cases "q ≠ q⇩0")
case True
{
assume "q ∈ set (r (Suc n))"
hence "¬ sink q"
using r_def nxt_run_sink_free by metis
moreover
obtain q' where "q' ∈ set (r n)" and "δ q' (w n) = q"
using ‹q ∈ set (r (Suc n))› nxt_run_reverse_step[OF _ ‹q ≠ q⇩0›] unfolding r_def by blast
hence "configuration q (Suc n) ≠ {}" and "¬ sink q"
unfolding configuration_step_eq[OF True] Suc using True ‹¬ sink q› by auto
}
moreover
{
assume "¬sink q" and "configuration q (Suc n) ≠ {}"
then obtain q' where "configuration q' n ≠ {}" and "δ q' (w n) = q"
unfolding configuration_step_eq[OF True] by blast
moreover
hence "¬sink q'"
using ‹¬sink q› sink_rev_step assms by blast
ultimately
have "q' ∈ set (r n)"
unfolding Suc by blast
hence "q ∈ set (r (Suc n))"
using ‹δ q' (w n) = q› ‹¬sink q›
unfolding r_def run.simps set_filter comp_def remdups_fwd_set set_map set_append image_def
unfolding r_def[symmetric] by auto
}
ultimately
show ?thesis
by blast
qed (insert assms, auto simp add: r_def sink_def)
qed (insert assms, auto simp add: r_def sink_def)
lemma (in semi_mojmir) nxt_run_sorted:
defines "r ≡ run (nxt Σ δ q⇩0) (init q⇩0) w"
shows "sorted (map (λq. the (oldest_token q n)) (r n))"
proof (induction n)
case (Suc n)
let ?f_n = "λq. the (oldest_token q n)"
let ?f_Suc_n = "λq. the (oldest_token q (Suc n))"
let ?step = "filter (λq. ¬sink q) ((map (λq. δ q (w n)) (r n)) @ [q⇩0])"
have "⋀q p qs ps. remdups_fwd ?step = qs @ q # p # ps ⟹ ?f_Suc_n q ≤ ?f_Suc_n p"
proof -
fix q qs p ps
assume "remdups_fwd ?step = qs @ q # p # ps"
then obtain zs zs' zs'' where step_def: "?step = zs @ q # zs' @ p # zs''"
and "remdups_fwd zs = qs"
and "remdups_fwd_acc (set qs ∪ {q}) zs' = []"
and "remdups_fwd_acc (set qs ∪ {q, p}) zs'' = ps"
and "q ∉ set zs"
and "p ∉ set zs ∪ {q}"
unfolding remdups_fwd.simps remdups_fwd_split_exact_iff remdups_fwd_split_exact_iff[where ?ys = "[]", simplified] insert_commute
by auto
hence "p ∉ set zs ∪ set zs' ∪ {q}"
and "q ≠ p" unfolding remdups_fwd_acc_empty[symmetric] by auto
hence "p ∉ set zs ∪ set zs' ∪ set [q]"
by simp
hence "{q, p} ⊆ set ?step"
using step_def by simp
hence "¬ sink q" and "¬ sink p"
unfolding set_map set_filter by blast+
show "?f_Suc_n q ≤ ?f_Suc_n p"
proof (cases "zs'' = []")
case True
hence "p = q⇩0" and q_def: "filter (λq. ¬sink q) (map (λq. δ q (w n)) (r n)) = zs @ [q] @ zs'"
using step_def unfolding sink_def by simp+
hence "q⇩0 ∉ set (filter (λq. ¬sink q) (map (λq. δ q (w n)) (r n)))"
using ‹p ∉ set zs ∪ set zs' ∪ {q}› unfolding ‹p = q⇩0› sink_def by simp
hence "q⇩0 ∉ (λq. δ q (w n)) ` {q'. configuration q' n ≠ {}}"
using nxt_run_configuration bounded_w unfolding set_map set_filter r_def sink_def init.simps by blast
hence "configuration p (Suc n) = {Suc n}" using assms
unfolding ‹p = q⇩0› using configuration_step_eq_q⇩0 by blast
hence "?f_Suc_n p = Suc n"
using assms by force
moreover
have "q ∈ (λq. δ q (w n)) ` set (r n)"
using ‹p ∉ set zs ∪ set zs' ∪ {q}› image_set unfolding filter_map_split_iff[of "(λq. ¬ sink q)" "λq. δ q (w n)"]
by (metis (no_types, lifting) Un_insert_right ‹p = q⇩0› ‹{q, p} ⊆ set [q←map (λq. δ q (w n)) (r n) @ [q⇩0] . ¬ sink q]› append_Nil2 insert_iff insert_subset list.simps(15) mem_Collect_eq set_append set_filter)
hence "q ∈ (λq. δ q (w n)) ` {q'. configuration q' n ≠ {}}"
using nxt_run_configuration unfolding r_def by auto
hence "configuration q (Suc n) ≠ {}"
using configuration_step assms by blast
hence "?f_Suc_n q ≤ Suc n"
using assms oldest_token_bounded[of q "Suc n"]
by (simp del: configuration.simps)
ultimately
show "?f_Suc_n q ≤ ?f_Suc_n p"
by presburger
next
case False
hence X: "filter (λq. ¬sink q) (map (λq. δ q (w n)) (r n)) = zs @ [q] @ zs' @ [p] @ butlast zs''"
using step_def unfolding map_append filter_append sink_def apply simp
by (metis (no_types, lifting) butlast.simps(2) list.distinct(1) butlast_append append_is_Nil_conv butlast_snoc)
obtain qs' sq' sp' ps' ps'' where r_def': "r n = qs' @ sq' @ ps' @ sp' @ ps''"
and 1: "filter (λq. ¬sink q) (map (λq. δ q (w n)) qs') = zs"
and 2: "filter (λq. ¬sink q) (map (λq. δ q (w n)) sq') = [q]"
and 3: "filter (λq. ¬sink q) (map (λq. δ q (w n)) ps') = zs'"
and "filter (λq. ¬sink q) (map (λq. δ q (w n)) sp') = [p]"
and "filter (λq. ¬sink q) (map (λq. δ q (w n)) ps'') = butlast zs''"
using X unfolding filter_map_split_iff by (blast)
hence 21: "Set.filter (λq. ¬sink q) ((λq. δ q (w n)) ` set sq') = {q}"
and 41: "Set.filter (λq. ¬sink q) ((λq. δ q (w n)) ` set sp') = {p}"
by (metis filter_set image_set list.set(1) list.simps(15))+
from 21 obtain q' where "q' ∈ set sq'" and "¬ sink q'" and "q = δ q' (w n)"
using sink_rev_step(2)[OF ‹¬ sink q›, of _ n] by fastforce
from 41 obtain p' where "p' ∈ set sp'" and "¬ sink p'" and "p = δ p' (w n)"
using sink_rev_step(2)[OF ‹¬ sink p›, of _ n] by fastforce
from Suc have "?f_n q' ≤ ?f_n p'"
unfolding r_def' map_append sorted_append set_append set_map using ‹q' ∈ set sq'› ‹p' ∈ set sp'› by auto
moreover
{
have "oldest_token q' n ≠ None"
using nxt_run_configuration option.distinct(1) r_def r_def' ‹q' ∈ set sq'› ‹p' ∈ set sp'› set_append
unfolding init.simps oldest_token.simps by (metis UnCI)
moreover
hence "oldest_token q (Suc n) ≠ None"
using ‹q = δ q' (w n)› by (metis oldest_token.simps option.distinct(1) configuration_step_non_empty)
ultimately
obtain x y where x_def: "oldest_token q' n = Some x"
and y_def: "oldest_token q (Suc n) = Some y"
by blast
moreover
hence "x ≤ n" and "token_run x n = q'"
using oldest_token_bounded push_down_oldest_token_token_run assms by blast+
moreover
hence "token_run x (Suc n) = q"
using ‹q = δ q' (w n)› by (rule token_run_step)
ultimately
have "x ≥ y"
using oldest_token_monotonic_Suc assms by blast
moreover
{
have "⋀q''. q = δ q'' (w n) ⟹ q'' ∉ set qs'"
using ‹q ∉ set zs› unfolding ‹filter (λq. ¬sink q) (map (λq. δ q (w n)) qs') = zs›[symmetric] set_map set_filter apply simp using ‹¬ sink q› by blast
moreover
{
obtain us vs where 1: "map (λq. δ q (w n)) sq' = us @ [q] @ vs" and "∀u∈set us. sink u" and "[] = [q←vs . ¬ sink q]"
using ‹filter (λq. ¬sink q) (map (λq. δ q (w n)) sq') = [q]› unfolding filter_eq_Cons_iff by auto
moreover
hence "⋀q''. q'' ∈ (set us) ∪ (set vs) ⟹ sink q''"
by (metis UnE filter_empty_conv)
hence "q ∉ (set us) ∪ (set vs)"
using ‹¬ sink q› by blast
ultimately
have "⋀q''. q'' ∈ (set sq' - {q'}) ⟹ δ q'' (w n) ≠ q"
using 1 ‹q = δ q' (w n)› ‹q' ∈ set sq'› by (fastforce dest: split_list elim: map_splitE)
}
ultimately
have "⋀q''. q = δ q'' (w n) ⟹ configuration q'' n ≠ {} ⟹ q'' ∈ set (ps' @ sp' @ ps'') ∨ q'' = q'"
using nxt_run_configuration[of _ n] ‹¬ sink q› sink_rev_step
unfolding r_def'[unfolded r_def] set_append
by blast
moreover
have "⋀q''. q'' ∈ set (ps' @ sp' @ ps'') ⟹ x ≤ ?f_n q''"
using x_def using Suc unfolding r_def' map_append sorted_append set_append set_map using ‹q' ∈ set sq'› ‹p' ∈ set sp'›
apply (simp del: oldest_token.simps) by fastforce
moreover
have "⋀q''. q'' = q' ⟹ x ≤ ?f_n q''"
using x_def by simp
moreover
have "⋀q'' x. x ∈ configuration q'' n ⟹ the (oldest_token q'' n) ≤ x"
using assms by auto
ultimately
have "⋀z. z ∈ ⋃{configuration q' n |q'. q = δ q' (w n)} ⟹ x ≤ z"
by fastforce
}
hence "⋀z. z ∈ configuration q (Suc n) ⟹ x ≤ z"
unfolding configuration_step_eq_unified using ‹x ≤ n›
by (cases "q = q⇩0"; auto)
hence "x ≤ y"
using y_def Min.boundedI configuration_finite using push_down_oldest_token_configuration by presburger
ultimately
have "?f_n q' = ?f_Suc_n q"
using x_def y_def by fastforce
}
moreover
{
have "oldest_token p' n ≠ None"
using nxt_run_configuration oldest_token.simps option.distinct(1) r_def r_def' ‹q' ∈ set sq'› ‹p' ∈ set sp'› set_append
unfolding init.simps by (metis UnCI)
moreover
hence "oldest_token p (Suc n) ≠ None"
using ‹p = δ p' (w n)› by (metis oldest_token.simps option.distinct(1) configuration_step_non_empty)
ultimately
obtain x y where x_def: "oldest_token p' n = Some x"
and y_def: "oldest_token p (Suc n) = Some y"
by blast
moreover
hence "x ≤ n" and "token_run x n = p'"
using oldest_token_bounded push_down_oldest_token_token_run assms by blast+
moreover
hence "token_run x (Suc n) = p"
using ‹p = δ p' (w n)› assms token_run_step by simp
ultimately
have "x ≥ y"
using oldest_token_monotonic_Suc assms by blast
moreover
{
have "⋀q''. p = δ q'' (w n) ⟹ q'' ∉ set qs' ∪ set sq' ∪ set ps'"
using ‹p ∉ set zs ∪ set zs' ∪ set [q]› ‹¬ sink p› unfolding 1[symmetric] 2[symmetric] 3[symmetric] set_map set_filter by blast
moreover
{
obtain us vs where 1: "map (λq. δ q (w n)) sp' = us @ [p] @ vs" and "∀u∈set us. sink u" and "[] = [q←vs . ¬ sink q]"
using ‹filter (λq. ¬sink q) (map (λq. δ q (w n)) sp') = [p]› unfolding filter_eq_Cons_iff by auto
moreover
hence "⋀q''. q'' ∈ (set us) ∪ (set vs) ⟹ sink q''"
by (metis UnE filter_empty_conv)
hence "p ∉ (set us) ∪ (set vs)"
using ‹¬ sink p› by blast
ultimately
have "⋀q''. q'' ∈ (set sp' - {p'}) ⟹ δ q'' (w n) ≠ p"
using 1 ‹p = δ p' (w n)› ‹p' ∈ set sp'› by (fastforce dest: split_list elim: map_splitE)
}
ultimately
have "⋀q''. p = δ q'' (w n) ⟹ configuration q'' n ≠ {} ⟹ q'' ∈ set ps'' ∨ q'' = p'"
using nxt_run_configuration[of _ n] ‹¬ sink p›[THEN sink_rev_step(2)] unfolding r_def'[unfolded r_def] set_append
by blast
moreover
have "⋀q''. q'' ∈ set ps'' ⟹ x ≤ ?f_n q''"
using x_def using Suc unfolding r_def' map_append sorted_append set_append set_map using ‹q' ∈ set sq'› ‹p' ∈ set sp'›
apply (simp del: oldest_token.simps) by fastforce
moreover
have "⋀q''. q'' = p' ⟹ x ≤ ?f_n q''"
using x_def by simp
moreover
have "⋀q'' x. x ∈ configuration q'' n ⟹ the (oldest_token q'' n) ≤ x"
using assms by auto
ultimately
have "⋀z. z ∈ ⋃{configuration p' n |p'. p = δ p' (w n)} ⟹ x ≤ z"
by fastforce
}
hence "⋀z. z ∈ configuration p (Suc n) ⟹ x ≤ z"
unfolding configuration_step_eq_unified using ‹x ≤ n›
by (cases "p = q⇩0"; auto)
hence "x ≤ y"
using y_def Min.boundedI configuration_finite using push_down_oldest_token_configuration by presburger
ultimately
have "?f_n p' = ?f_Suc_n p"
using x_def y_def by fastforce
}
ultimately
show ?thesis
by presburger
qed
qed
hence "⋀x y xs ys. map ?f_Suc_n (remdups_fwd ?step) = xs @ [x, y] @ ys ⟹ x ≤ y"
by (auto elim: map_splitE simp del: remdups_fwd.simps)
hence "sorted (map ?f_Suc_n (remdups_fwd (?step)))"
using sorted_pre by metis
thus ?case
by (simp add: r_def sink_def)
qed (simp add: r_def)
lemma (in semi_mojmir) nxt_run_senior_states:
defines "r ≡ run (nxt Σ δ q⇩0) (init q⇩0) w"
assumes "¬sink q"
assumes "configuration q n ≠ {}"
shows "senior_states q n = set (takeWhile (λq'. q' ≠ q) (r n))"
(is "?lhs = ?rhs")
proof (rule set_eqI, rule)
fix q' assume q'_def: "q' ∈ senior_states q n"
then obtain x y where "oldest_token q' n = Some y" and "oldest_token q n = Some x" and "y < x"
using senior_states.simps using assms by blast
hence "the (oldest_token q' n) < the (oldest_token q n)"
by fastforce
moreover
hence "¬sink q'" and "configuration q' n ≠ {}"
using q'_def option.distinct(1) ‹oldest_token q' n = Some y›
oldest_token.simps using assms by (force, metis)
hence "q' ∈ set (r n)" and "q ∈ set (r n)"
using nxt_run_configuration assms by blast+
moreover
have "distinct (r n)"
unfolding r_def using nxt_run_distinct by fast
ultimately
obtain r' r'' r''' where r_alt_def: "r n = r' @ q' # r'' @ q # r'''"
using sorted_list[OF _ _ nxt_run_sorted] assms unfolding r_def by presburger
hence "q' ∈ set (r' @ q' # r'')"
by simp
thus "q' ∈ set (takeWhile (λq'. q' ≠ q) (r n))"
using ‹distinct (r n)› takeWhile_distinct[of "r' @ q' # r''" q r''' q'] unfolding r_alt_def by simp
next
fix q' assume q'_def: "q' ∈ set (takeWhile (λq'. q' ≠ q) (r n))"
moreover
hence "q' ∈ set (r n)"
by (blast dest: set_takeWhileD)+
hence 5: "¬ sink q'"
using nxt_run_configuration assms by simp
have "q ∈ set (r n)"
using nxt_run_configuration assms by blast+
ultimately
obtain r' r'' r''' where r_alt_def: "r n = r' @ q' # r'' @ q # r'''"
using takeWhile_split by metis
have "distinct (r n)"
unfolding r_def using nxt_run_distinct by fast
have 1: "the (oldest_token q' n) ≤ the (oldest_token q n)"
using nxt_run_sorted[of n, unfolded r_def[symmetric]] assms
unfolding r_alt_def map_append list.map
unfolding sorted_append by (simp del: oldest_token.simps)
have "q ≠ q'"
using ‹distinct (r n)› r_alt_def by auto
moreover
have 2: "oldest_token q' n ≠ None" and 3: "oldest_token q n ≠ None"
using assms ‹q' ∈ set (r n)› nxt_run_configuration by force+
ultimately
have 4: "the (oldest_token q' n) ≠ the (oldest_token q n)"
by (metis oldest_token_equal option.collapse)
show "q' ∈ senior_states q n"
using 1 2 3 4 5 assms by fastforce
qed
lemma (in semi_mojmir) nxt_run_state_rank:
"state_rank q n = rk (run (nxt Σ δ q⇩0) (init q⇩0) w n) q"
by (cases "¬sink q ∧ configuration q n ≠ {}", unfold state_rank.simps)
(metis nxt_run_senior_states rk_split_card_takeWhile nxt_run_distinct nxt_run_configuration, metis nxt_run_configuration rk_facts(1))
lemma (in semi_mojmir) nxt_foldl_state_rank:
"state_rank q n = rk (foldl (nxt Σ δ q⇩0) (init q⇩0) (map w [0..<n])) q"
unfolding nxt_run_state_rank run_foldl ..
lemma (in semi_mojmir) nxt_run_step_run:
"run step initial w = rk o (run (nxt Σ δ q⇩0) (init q⇩0) w)"
using nxt_run_state_rank state_rank_step_foldl[unfolded run_foldl[symmetric]] unfolding comp_def by presburger
definition (in semi_mojmir_def) Q⇩E
where
"Q⇩E ≡ reach Σ (nxt Σ δ q⇩0) (init q⇩0)"
lemma (in semi_mojmir) finite_Q:
"finite Q⇩E"
proof -
{
fix i fix w :: "nat ⇒ 'a"
assume "range w ⊆ Σ"
then interpret ℌ: semi_mojmir Σ δ q⇩0 w
using finite_reach finite_Σ by (unfold_locales, blast)
have "set (run (nxt Σ δ q⇩0) (init q⇩0) w i) ⊆ {ℌ.token_run j i | j. j ≤ i}" (is "?S1 ⊆ _")
using ℌ.nxt_run_configuration by auto
also
have "… ⊆ reach Σ δ q⇩0" (is "_ ⊆ ?S2")
unfolding reach_def token_run.simps using ‹range w ⊆ Σ› by fastforce
finally
have "?S1 ⊆ ?S2" .
}
hence "set ` Q⇩E ⊆ Pow (reach Σ δ q⇩0)"
unfolding Q⇩E_def reach_def by blast
hence "finite (set ` Q⇩E)"
using finite_reach by (blast dest: finite_subset)
moreover
have "⋀xs. xs ∈ Q⇩E ⟹ distinct xs"
unfolding Q⇩E_def reach_def using nxt_run_distinct by fastforce
ultimately
show "finite Q⇩E"
using set_list by auto
qed
lemma (in mojmir_to_rabin_def) filt_equiv:
"(rk x, ν, y) ∈ fail⇩R ⟷ fail_filt Σ δ q⇩0 (λx. x ∈ F) (x, ν, y')"
"(rk x, ν, y) ∈ succeed⇩R i ⟷ succeed_filt δ q⇩0 (λx. x ∈ F) i (x, ν, y')"
"(rk x, ν, y) ∈ merge⇩R i ⟷ merge_filt δ q⇩0 (λx. x ∈ F) i (x, ν, y')"
by (simp add: fail⇩R_def succeed⇩R_def merge⇩R_def del: rk.simps; metis (no_types, lifting) option.sel rk_facts(2))+
lemma fail_filt_eq:
"fail_filt Σ δ q⇩0 P (x, ν, y) ⟷ (rk x, ν, y') ∈ mojmir_to_rabin_def.fail⇩R Σ δ q⇩0 {x. P x}"
unfolding mojmir_to_rabin_def.filt_equiv(1)[where y' = y] by simp
lemma merge_filt_eq:
"merge_filt δ q⇩0 P i (x, ν, y) ⟷ (rk x, ν, y') ∈ mojmir_to_rabin_def.merge⇩R δ q⇩0 {x. P x} i"
unfolding mojmir_to_rabin_def.filt_equiv(3)[where y' = y] by simp
lemma succeed_filt_eq:
"succeed_filt δ q⇩0 P i (x, ν, y) ⟷ (rk x, ν, y') ∈ mojmir_to_rabin_def.succeed⇩R δ q⇩0 {x. P x} i"
unfolding mojmir_to_rabin_def.filt_equiv(2)[where y' = y] by simp
theorem (in mojmir_to_rabin) rabin_accept_iff_rabin_list_accept_rank:
"accepting_pair⇩R δ⇩ℛ q⇩ℛ (Acc⇩ℛ i) w ⟷ accepting_pair⇩R (nxt Σ δ q⇩0) (init q⇩0) ({t. fail_filt Σ δ q⇩0 (λx. x ∈ F) t} ∪ {t. merge_filt δ q⇩0 (λx. x ∈ F) i t}, {t. succeed_filt δ q⇩0 (λx. x ∈ F) i t}) w"
(is "accepting_pair⇩R δ⇩ℛ q⇩ℛ (?F, ?I) w ⟷ accepting_pair⇩R (nxt Σ δ q⇩0) (init q⇩0) (?F', ?I') w")
proof -
have "finite (reach⇩t Σ δ⇩ℛ q⇩ℛ)"
using wellformed_ℛ finite_Σ finite_reach⇩t by fast
moreover
have "finite (reach⇩t Σ (nxt Σ δ q⇩0) (init q⇩0))"
using finite_Q finite_Σ finite_reach⇩t by (auto simp add: Q⇩E_def)
moreover
have "run⇩t step initial w = (λ(x, ν, y). (rk x, ν, rk y)) o (run⇩t (nxt Σ δ q⇩0) (init q⇩0) w)"
using nxt_run_step_run by auto
moreover
note bounded_w filt_equiv
ultimately
show ?thesis
by (intro accepting_pair⇩R_abstract) auto
qed
subsection ‹Compute Rabin Automata List Representation›
fun mojmir_to_rabin_exec
where
"mojmir_to_rabin_exec Σ δ q⇩0 F = (
let
q⇩0' = init q⇩0;
δ' = δ⇩L Σ (nxt (set Σ) δ q⇩0) q⇩0';
max_rank = card (Set.filter (Not o semi_mojmir_def.sink (set Σ) δ q⇩0) (Q⇩L Σ δ q⇩0));
fail = Set.filter (fail_filt (set Σ) δ q⇩0 F) δ';
merge = (λi. Set.filter (merge_filt δ q⇩0 F i) δ');
succeed = (λi. Set.filter (succeed_filt δ q⇩0 F i) δ')
in
(δ', q⇩0', (λi. (fail ∪ (merge i), succeed i)) ` {0..<max_rank}))"
subsection ‹Code Generation›
declare semi_mojmir_def.sink_def [code]
fun index_option :: "nat ⇒ 'a list ⇒ 'a ⇒ nat option"
where
"index_option n [] y = None"
| "index_option n (x # xs) y = (if x = y then Some n else index_option (Suc n) xs y)"
declare rk.simps [code del]
lemma rk_eq_index_option [code]:
"rk xs x = index_option 0 xs x"
proof -
have A: "⋀n. x ∈ set xs ⟹ index xs x + n = the (index_option n xs x)"
and B: "⋀n. x ∉ set xs ⟷ index_option n xs x = None"
by (induction xs) (auto, metis add_Suc_right)
thus ?thesis
proof (cases "x ∈ set xs")
case True
moreover
hence "index xs x = the (index_option 0 xs x)"
using A[OF True, of 0] by simp
ultimately
show ?thesis
unfolding rk.simps by (metis (mono_tags, lifting) B True index_less_size_conv less_irrefl option.collapse)
qed simp
qed
export_code init nxt fail_filt succeed_filt merge_filt mojmir_to_rabin_exec checking
lemma (in mojmir) max_rank_card:
assumes "Σ = set Σ'"
shows "max_rank = card (Set.filter (Not o semi_mojmir_def.sink (set Σ') δ q⇩0) (Q⇩L Σ' δ q⇩0))"
unfolding max_rank_def Q⇩L_reach[OF finite_reach[unfolded ‹Σ = set Σ'›]]
by (simp add: Set.filter_def set_diff_eq assms(1))
theorem (in mojmir_to_rabin) exec_correct:
assumes "Σ = set Σ'"
shows "accept ⟷ accept⇩R_LTS (mojmir_to_rabin_exec Σ' δ q⇩0 (λx. x ∈ F)) w" (is "?lhs ⟷ ?rhs")
proof -
have F1: "finite (reach Σ (nxt Σ δ q⇩0) (init q⇩0))"
using finite_Q by (simp add: Q⇩E_def)
hence F2: "finite (reach⇩t Σ (nxt Σ δ q⇩0) (init q⇩0))"
using finite_Σ by (rule finite_reach⇩t)
let ?δ' = "δ⇩L Σ' (nxt Σ δ q⇩0) (init q⇩0)"
have δ'_Def: "?δ' = reach⇩t Σ (nxt Σ δ q⇩0) (init q⇩0)"
using δ⇩L_reach[OF F2[unfolded assms]] unfolding assms by simp
have 3: "snd (snd ((mojmir_to_rabin_exec Σ' δ q⇩0 (λx. x ∈ F))))
= {(({t. fail_filt Σ δ q⇩0 (λx. x ∈ F) t} ∪ {t. merge_filt δ q⇩0 (λx. x ∈ F) i t}) ∩ reach⇩t Σ (nxt Σ δ q⇩0) (init q⇩0),
{t. succeed_filt δ q⇩0 (λx. x ∈ F) i t} ∩ reach⇩t Σ (nxt Σ δ q⇩0) (init q⇩0)) | i. i < max_rank}"
unfolding assms mojmir_to_rabin_exec.simps Let_def fst_conv snd_conv set_map δ'_Def[unfolded assms] max_rank_card[OF assms, symmetric]
unfolding assms[symmetric] Set.filter_def by auto
have "?lhs ⟷ accept⇩R (δ⇩ℛ, q⇩ℛ, {(Acc⇩ℛ i) | i. i < max_rank}) w"
using mojmir_accept_iff_rabin_accept by blast
moreover
have "… ⟷ accept⇩R (nxt Σ δ q⇩0, init q⇩0, {({t. fail_filt Σ δ q⇩0 (λx. x ∈ F) t} ∪ {t. merge_filt δ q⇩0 (λx. x ∈ F) i t}, {t. succeed_filt δ q⇩0 (λx. x ∈ F) i t}) | i. i < max_rank}) w"
unfolding accept⇩R_def fst_conv snd_conv using rabin_accept_iff_rabin_list_accept_rank by blast
moreover
have "… ⟷ ?rhs"
apply (subst accept⇩R_restrict[OF bounded_w])
unfolding 3[unfolded mojmir_to_rabin_exec.simps Let_def snd_conv, symmetric] assms[symmetric] mojmir_to_rabin_exec.simps Let_def unfolding assms δ'_Def[unfolded assms]
unfolding accept⇩R_LTS[OF bounded_w[unfolded assms], symmetric, unfolded assms] by simp
ultimately
show ?thesis
by blast
qed
end