(* Author: Salomon Sickert License: BSD *) section ‹Executable Translation from Mojmir to Rabin Automata› theory Mojmir_Rabin_Impl imports Main "../Mojmir_Rabin" begin ― ‹Ranking functions are stored as lists sorted ascending by the state rank› 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}]))" ― ‹Recompute the rank from the list› 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)" ― ‹Instead of computing the whole sets for fail, merge, and succeed, we define filters (a.k.a. characteristic functions)› 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) (* Slow *) 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› ― ‹Setup missing equations for code generator› declare semi_mojmir_def.sink_def [code] ― ‹Drop computation of length by different code equation› 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 ― ‹Check Code Export› 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