Theory Mojmir_Rabin_Impl

theory Mojmir_Rabin_Impl
imports Mojmir_Rabin
(*  
    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 q0 = [q0]"

fun nxt :: "'b set ⇒ ('a, 'b) DTS ⇒ 'a ⇒ ('a list, 'b) DTS"
where
  "nxt Σ δ q0 = (λqs ν. remdups_fwd ((filter (λq. ¬semi_mojmir_def.sink Σ δ q0 q) (map (λq. δ q ν) qs)) @ [q0]))" 

― ‹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 Σ δ q0 F (r, ν, _) = (∃q ∈ set r. let q' = δ q ν in (¬F q') ∧ semi_mojmir_def.sink Σ δ q0 q')"

fun merge_filt :: "('a, 'b) DTS ⇒ 'a ⇒ ('a ⇒ bool) ⇒ nat ⇒ ('a list, 'b) transition ⇒ bool"
where
  "merge_filt δ q0 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' = q0))"

fun succeed_filt :: "('a, 'b) DTS ⇒ 'a ⇒ ('a ⇒ bool) ⇒ nat ⇒ ('a list, 'b) transition ⇒ bool"
where
  "succeed_filt δ q0 F i (r, ν, _) = (∃q ∈ set r. let q' = δ q ν in rk r q = Some i  ∧ (¬F q ∨ q = q0) ∧ F q')" 

subsubsection ‹nxt Properties›

lemma nxt_run_distinct:
  "distinct (run (nxt Σ Δ q0) (init q0) w n)"
  by (cases n; simp del: remdups_fwd.simps; metis (no_types) remdups_fwd_distinct)

lemma nxt_run_reverse_step:
  fixes Σ δ q0 w
  defines "r ≡ run (nxt Σ δ q0) (init q0) w" 
  assumes "q ∈ set (r (Suc n))"
  assumes "q ≠ q0"
  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 Σ δ q0) (init q0) w n) ⟹ ¬semi_mojmir_def.sink Σ δ q0 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 Σ δ q0) (init q0) w"
  shows "q ∈ set (r n) ⟷ ¬sink q ∧ configuration q n ≠ {}"
proof (induction n arbitrary: q)
  case (Suc n)
    thus ?case
    proof (cases "q ≠ q0")
      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 ≠ q0] 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 Σ δ q0) (init q0) 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)) @ [q0])"

    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 = q0" 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 "q0 ∉ set (filter (λq. ¬sink q) (map (λq. δ q (w n)) (r n)))"
            using ‹p ∉ set zs ∪ set zs' ∪ {q}›  unfolding ‹p = q0 sink_def by simp
          hence "q0 ∉ (λ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 = q0 using configuration_step_eq_q0 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 = q0  ‹{q, p} ⊆ set [q←map (λq. δ q (w n)) (r n) @ [q0] . ¬ 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 = q0"; 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 = q0"; 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 Σ δ q0) (init q0) 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 Σ δ q0) (init q0) 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 Σ δ q0) (init q0) (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 Σ δ q0) (init q0) w)"
  using nxt_run_state_rank state_rank_step_foldl[unfolded run_foldl[symmetric]] unfolding comp_def by presburger  

definition (in semi_mojmir_def) QE
where
  "QE ≡ reach Σ (nxt Σ δ q0) (init q0)"

lemma (in semi_mojmir) finite_Q:
  "finite QE"
proof -
  {
    fix i fix w :: "nat ⇒ 'a" 
    assume "range w ⊆ Σ"
    then interpret : semi_mojmir Σ δ q0 w
      using finite_reach finite_Σ by (unfold_locales, blast)  
    have "set (run (nxt Σ δ q0) (init q0) w i) ⊆ {ℌ.token_run j i | j. j ≤ i}" (is "?S1 ⊆ _")
      using ℌ.nxt_run_configuration by auto
    also 
    have "… ⊆ reach Σ δ q0" (is "_ ⊆ ?S2")
      unfolding reach_def token_run.simps using ‹range w ⊆ Σ› by fastforce
    finally
    have "?S1 ⊆ ?S2" .
  }
  hence "set ` QE ⊆ Pow (reach Σ δ q0)"
    unfolding QE_def reach_def by blast
  hence "finite (set ` QE)"
    using finite_reach by (blast dest: finite_subset)
  moreover
  have "⋀xs. xs ∈ QE ⟹ distinct xs"
    unfolding QE_def reach_def using nxt_run_distinct by fastforce
  ultimately
  show "finite QE"
    using set_list by auto
qed

lemma (in mojmir_to_rabin_def) filt_equiv:
  "(rk x, ν, y) ∈ failR ⟷ fail_filt Σ δ q0 (λx. x ∈ F) (x, ν, y')"
  "(rk x, ν, y) ∈ succeedR i ⟷ succeed_filt δ q0 (λx. x ∈ F) i (x, ν, y')"
  "(rk x, ν, y) ∈ mergeR i ⟷ merge_filt δ q0 (λx. x ∈ F) i (x, ν, y')"
  by (simp add: failR_def succeedR_def mergeR_def del: rk.simps; metis (no_types, lifting) option.sel rk_facts(2))+

lemma fail_filt_eq: 
  "fail_filt Σ δ q0 P (x, ν, y) ⟷ (rk x, ν, y') ∈ mojmir_to_rabin_def.failR Σ δ q0 {x. P x}"
  unfolding mojmir_to_rabin_def.filt_equiv(1)[where y' = y] by simp

lemma merge_filt_eq: 
  "merge_filt δ q0 P i (x, ν, y) ⟷ (rk x, ν, y') ∈ mojmir_to_rabin_def.mergeR δ q0 {x. P x} i"
  unfolding mojmir_to_rabin_def.filt_equiv(3)[where y' = y] by simp

lemma succeed_filt_eq: 
  "succeed_filt δ q0 P i (x, ν, y) ⟷ (rk x, ν, y') ∈ mojmir_to_rabin_def.succeedR δ q0 {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_pairR δ q (Acc i) w ⟷ accepting_pairR (nxt Σ δ q0) (init q0) ({t. fail_filt Σ δ q0 (λx. x ∈ F) t} ∪ {t. merge_filt δ q0 (λx. x ∈ F) i t}, {t. succeed_filt δ q0 (λx. x ∈ F) i t}) w"
  (is "accepting_pairR δ q (?F, ?I) w ⟷ accepting_pairR (nxt Σ δ q0) (init q0) (?F', ?I') w")
proof -
  have "finite (reacht Σ δ q)"
    using wellformed_ℛ finite_Σ finite_reacht by fast
  moreover
  have "finite (reacht Σ (nxt Σ δ q0) (init q0))"
    using finite_Q finite_Σ finite_reacht by (auto simp add: QE_def) 
  moreover
  have "runt step initial w = (λ(x, ν, y). (rk x, ν, rk y)) o (runt (nxt Σ δ q0) (init q0) w)"
    using nxt_run_step_run by auto
  moreover
  note bounded_w filt_equiv 
  ultimately
  show ?thesis
    by (intro accepting_pairR_abstract) auto
qed

subsection ‹Compute Rabin Automata List Representation›

fun mojmir_to_rabin_exec
where
  "mojmir_to_rabin_exec Σ δ q0 F = (
    let 
      q0' = init q0;
      δ' = δL Σ (nxt (set Σ) δ q0) q0';
      max_rank = card (Set.filter (Not o semi_mojmir_def.sink (set Σ) δ q0) (QL Σ δ q0));
      fail = Set.filter (fail_filt (set Σ) δ q0 F) δ';
      merge = (λi. Set.filter (merge_filt δ q0 F i) δ');
      succeed = (λi. Set.filter (succeed_filt δ q0 F i) δ')
    in
      (δ', q0', (λ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 Σ') δ q0) (QL Σ' δ q0))"
  unfolding max_rank_def QL_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 ⟷ acceptR_LTS (mojmir_to_rabin_exec Σ' δ q0 (λx. x ∈ F)) w" (is "?lhs ⟷ ?rhs")
proof -
 have F1: "finite (reach Σ (nxt Σ δ q0) (init q0))"
    using finite_Q by (simp add: QE_def)
  hence F2: "finite (reacht Σ (nxt Σ δ q0) (init q0))"
    using finite_Σ by (rule finite_reacht)

  let ?δ' = L Σ' (nxt Σ δ q0) (init q0)"
  have δ'_Def: "?δ' = reacht Σ (nxt Σ δ q0) (init q0)"
    using δL_reach[OF F2[unfolded assms]] unfolding  assms  by simp
 
  have 3: "snd (snd ((mojmir_to_rabin_exec Σ' δ q0 (λx. x ∈ F)))) 
    = {(({t. fail_filt Σ δ q0 (λx. x ∈ F) t} ∪ {t. merge_filt δ q0 (λx. x ∈ F) i t}) ∩ reacht Σ (nxt Σ δ q0) (init q0), 
        {t. succeed_filt δ q0 (λx. x ∈ F) i t}  ∩ reacht Σ (nxt Σ δ q0) (init q0)) | 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 ⟷ acceptR, q, {(Acc i) | i. i < max_rank}) w"
    using mojmir_accept_iff_rabin_accept by blast

  moreover

  have "… ⟷ acceptR (nxt Σ δ q0, init q0, {({t. fail_filt Σ δ q0 (λx. x ∈ F) t} ∪ {t. merge_filt δ q0 (λx. x ∈ F) i t}, {t. succeed_filt δ q0 (λx. x ∈ F) i t}) | i. i < max_rank}) w"
    unfolding acceptR_def fst_conv snd_conv using rabin_accept_iff_rabin_list_accept_rank by blast 
 
  moreover 

  have "… ⟷ ?rhs"
    apply (subst acceptR_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 acceptR_LTS[OF bounded_w[unfolded assms], symmetric, unfolded assms] by simp
  
  ultimately
 
  show ?thesis
    by blast
qed

end