Session LTL_to_DRA

Theory Preliminaries2

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Auxiliary Facts›

theory Preliminaries2
  imports Main "HOL-Library.Infinite_Set"
begin

subsection ‹Finite and Infinite Sets›

lemma finite_product:
  assumes fst: "finite (fst ` A)"
  and     snd: "finite (snd ` A)"
  shows   "finite A"
proof -
  have "A  (fst ` A) × (snd ` A)"
    by force
  thus ?thesis
    using snd fst finite_subset by blast
qed

subsection ‹Cofinite Filters›

lemma almost_all_commutative:
  "finite S  (x  S. i. P x (i::nat)) = (i. x  S. P x i)"
proof (induction rule: finite_induct) 
  case (insert x S)
    {
      assume "x  insert x S. i. P x i"
      hence "i. x  S. P x i" and "i. P x i"
        using insert by simp+
      then obtain i1 i2 where "j. j  i1  x  S. P x j"
        and "j. j  i2  P x j"
        unfolding MOST_nat_le by auto
      hence "j. j  max i1 i2  x  S  {x}. P x j"
        by simp
      hence "i. x  insert x S. P x i"
        unfolding MOST_nat_le by blast
    }
    moreover
    have "i. x  insert x S. P x i  x  insert x S. i. P x i"
      unfolding MOST_nat_le by auto
    ultimately
    show ?case 
      by blast
qed simp

lemma almost_all_commutative':
  "finite S  (x. x  S  i. P x (i::nat))  (i. x  S. P x i)"
  using almost_all_commutative by blast

fun index
where
  "index P = (if i. P i then Some (LEAST i. j  i. P j) else None)"

lemma index_properties: 
  fixes i :: nat
  shows "index P = Some i  0 < i  ¬ P (i - 1)"
    and "index P = Some i  j  i  P j"
proof -
  assume "index P = Some i"
  moreover
  hence i_def: "i = (LEAST i. j  i. P j)" and "i. P i"
    unfolding index.simps using option.distinct(2) option.sel 
    by (metis (erased, lifting))+
  then obtain i' where "j  i'.  P j"
    unfolding MOST_nat_le by blast
  ultimately
  show "j. j  i  P j"
    using LeastI[of "λi. j  i. P j"] by (metis i_def) 
  {
    assume "0 < i"
    then obtain j where "i = Suc j" and "j < i"
      using lessE by blast
    hence "j'. j' > j  P j'"
      using j. j  i  P j by force
    hence "¬ P j"
      using not_less_Least[OF j < i[unfolded i_def]] by (metis leI le_antisym)
    thus "¬ P (i - 1)"
      unfolding i = Suc j by simp
  }
qed

end

Theory Map2

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Auxiliary Map Facts›

theory Map2
  imports Main
begin 

lemma map_of_tabulate:  
  "map_of (map (λx. (x, f x)) xs) x  None  x  set xs"
  by (induct xs) auto

lemma map_of_tabulate_simp:
  "map_of (map (λx. (x, f x)) xs) x = (if x  set xs then Some (f x) else None)"
  by (metis (mono_tags, lifting) comp_eq_dest_lhs map_of_map_restrict restrict_map_def)

lemma dom_map_update:
  "dom (m (k  v)) = dom m  {k}"
  by simp

lemma map_equal:
  "dom m = dom m'  (x. x  dom m  m x = m' x)  m = m'"
  by fastforce

lemma map_reduce:
  assumes "dom m = {a}  B"
  shows "m'. dom m' = B  (x  B. m x = m' x)"
proof (cases "a  B")
  case True
    thus ?thesis
      using assms by (metis insert_absorb insert_is_Un)
next
  case False
    with assms have "dom (m (a := None)) = B  (xB. m x = (m (a := None)) x)"
      by simp
    thus ?thesis
      by blast
qed

end

Theory Mapping2

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Auxiliary Mapping Facts›

theory Mapping2
  imports Main Map2 "HOL-Library.Mapping"
begin 

lemma lookup_delete:
  "Mapping.lookup (Mapping.delete k m) k = None"
  by (transfer; simp) 

lemma lookup_tabulate:
  "Mapping.lookup (Mapping.tabulate xs f) x = (if x  set xs then Some (f x) else None)"
  by (transfer; insert map_of_tabulate_simp)

lemma lookup_tabulate_Some:
  "x  set xs  the (Mapping.lookup (Mapping.tabulate xs f) x) = f x" 
  by (simp add: lookup_tabulate)

lemma finite_keys_tabulate:
  "finite (Mapping.keys (Mapping.tabulate xs f))"
  by simp

lemma keys_empty_iff_map_empty:
  "Mapping.keys m = {}  m = Mapping.empty"
  by (transfer; simp)

lemma mapping_equal:
  "Mapping.keys m = Mapping.keys m'  (x. x  Mapping.keys m  Mapping.lookup m x = Mapping.lookup m' x)  m = m'"
  by (transfer; blast intro: map_equal)

fun mapping_generator :: "('a  'b list)  'a list  ('a, 'b) mapping set"
where
  "mapping_generator V [] = {Mapping.empty}"
| "mapping_generator V (k#ks) = {Mapping.update k v m | v m.  v  set (V k)  m  mapping_generator V ks}"

fun mapping_generator_list :: "('a  'b list)  'a list  ('a, 'b) mapping list"
where
  "mapping_generator_list V [] = [Mapping.empty]"
| "mapping_generator_list V (k#ks) = concat (map (λm. map (λv. Mapping.update k v m) (V k)) (mapping_generator_list V ks))"

lemma mapping_generator_code [code]:
  "mapping_generator V K = set (mapping_generator_list V K)"
  by (induction K) auto 

lemma mapping_generator_set_eq:
  "mapping_generator V K = {m. Mapping.keys m = set K  (k  (set K). the (Mapping.lookup m k)  set (V k))}"
proof (induction K)
  case (Cons k ks)
    let ?l = "{m(k  v) |v m. v  set (V k)   m  {m. dom m = set ks  (kset ks. the (m k)  set (V k))}}"
    let ?r = "{m. dom m = set (k # ks)  (kset (k # ks). the (m k)  set (V k))}"

    have "?l  ?r"
      by fastforce
    moreover
    {
      fix m 
      assume "m  ?r" 
      hence "dom m = set (k#ks)" 
        and "k  set (k#ks). the (m k)  set (V k)" 
        and "k'  set (k#ks). m k  None"
        by auto   
      moreover
      then obtain m' where "dom m' = set ks"
        and "x  set ks. m x = m' x"
        using map_reduce[of m k "set ks"] by auto
      ultimately
      have "the (m k)  set (V k)"
        and "dom m' = set ks" 
        and "k  (set ks). the (m' k)  set (V k)"
        and "m = m'(k  the (m k))"
        apply (simp, blast, auto) 
        apply (insert map_equal[of m "m'(k  the (m k))"])
        apply (unfold dom_map_update ‹dom m = set (k#ks) ‹dom m' = set ks)
        by fastforce
      moreover
      hence "m  set (map (λv. m'(k  v)) (V k))"
        by simp
      ultimately
      have "m  ?l"
        using ‹dom m = set (k#ks) by blast       
    }
    ultimately
    have "{Mapping.update k v m |v m. v  set (V k)  m  {m. Mapping.keys m = set ks  (kset ks. the (Mapping.lookup m k)  set (V k))}} 
      = {m. Mapping.keys m = set (k # ks)  (kset (k # ks). the (Mapping.lookup m k)  set (V k))}" 
      by (transfer; blast)
    thus ?case
      by (simp add: Cons)
qed (force simp add: keys_empty_iff_map_empty)

end

Theory DTS

(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Deterministic Transition Systems›

theory DTS
  imports Main "HOL-Library.Omega_Words_Fun" "Auxiliary/Mapping2" KBPs.DFS
begin

― ‹DTS are realised by functions›

type_synonym ('a, 'b) DTS = "'a  'b  'a"
type_synonym ('a, 'b) transition = "('a × 'b × 'a)"

subsection ‹Infinite Runs›

fun run :: "('q,'a) DTS  'q  'a word  'q word"
where
  "run δ q0 w 0 = q0"
| "run δ q0 w (Suc i) = δ (run δ q0 w i) (w i)"

fun runt :: "('q,'a) DTS  'q  'a word  ('q * 'a * 'q) word"
where
  "runt δ q0 w i = (run δ q0 w i, w i, run δ q0 w (Suc i))"

lemma run_foldl:
  "run Δ q0 w i = foldl Δ q0 (map w [0..<i])"
  by (induction i; simp)

lemma runt_foldl:
  "runt Δ q0 w i = (foldl Δ q0 (map w [0..<i]), w i, foldl Δ q0 (map w [0..<Suc i]))"
  unfolding runt.simps run_foldl ..

subsection ‹Reachable States and Transitions›

definition reach :: "'a set  ('b, 'a) DTS  'b  'b set"
where
  "reach Σ δ q0 = {run δ q0 w n | w n. range w  Σ}"

definition reacht :: "'a set  ('b, 'a) DTS  'b  ('b, 'a) transition set"
where
  "reacht Σ δ q0 = {runt δ q0 w n | w n. range w  Σ}"

lemma reach_foldl_def:
  assumes "Σ  {}"
  shows "reach Σ δ q0 = {foldl δ q0 w | w. set w  Σ}"
proof -
  {
    fix w assume "set w  Σ"
    moreover
    obtain a where "a  Σ"
      using Σ  {} by blast
    ultimately
    have "foldl δ q0 w = foldl δ q0 (prefix (length w) (w  (iter [a])))" 
      and "range (w  (iter [a]))  Σ"
      by (unfold prefix_conc_length, auto simp add: iter_def conc_def) 
    hence "w' n. foldl δ q0 w = run δ q0 w' n  range w'  Σ"
      unfolding run_foldl subsequence_def by blast
  }
  thus ?thesis
    by (fastforce simp add: reach_def run_foldl)
qed

lemma reacht_foldl_def:
  "reacht Σ δ q0 = {(foldl δ q0 w, ν, foldl δ q0 (w@[ν])) | w ν. set w  Σ  ν  Σ}" (is "?lhs = ?rhs")
proof (cases "Σ  {}")
  case True
    show ?thesis
    proof
      {
        fix w ν assume "set w  Σ" "ν  Σ"
        moreover
        obtain a where "a  Σ"
          using Σ  {} by blast
        moreover
        have "w = map (λn. if n < length w then w ! n else if n - length w = 0 then [ν] ! (n - length w) else a) [0..<length w]"
          by (simp add: nth_equalityI)  
        ultimately
        have "foldl δ q0 w = foldl δ q0 (prefix (length w) ((w @ [ν])  (iter [a])))" 
          and"foldl δ q0 (w @ [ν]) = foldl δ q0 (prefix (length (w @ [ν])) ((w @ [ν])  (iter [a])))" 
          and "range ((w @ [ν])  (iter [a]))  Σ"
          by (simp_all only: prefix_conc_length conc_conc[symmetric] iter_def)
             (auto simp add: subsequence_def conc_def upt_Suc_append[OF le0])
        moreover
        have "((w @ [ν])  (iter [a])) (length w) = ν"
          by (simp add: conc_def)
        ultimately
        have "w' n. (foldl δ q0 w, ν, foldl δ q0 (w @ [ν])) = runt δ q0 w' n  range w'  Σ"
          by (metis runt_foldl length_append_singleton subsequence_def)
      }
      thus "?lhs  ?rhs"
        unfolding reacht_def runt.simps by blast
    qed (unfold reacht_def runt_foldl, fastforce simp add: upt_Suc_append)
qed (simp add: reacht_def)

lemma reach_card_0:
  assumes "Σ  {}"
  shows "infinite (reach Σ δ q0)  card (reach Σ δ q0) = 0"
proof -
  have "{run δ q0 w n | w n. range w  Σ}  {}"
    using assms by fast
  thus ?thesis
    unfolding reach_def card_eq_0_iff by auto
qed

lemma reacht_card_0:
  assumes "Σ  {}"
  shows "infinite (reacht Σ δ q0)  card (reacht Σ δ q0) = 0"
proof -
  have "{runt δ q0 w n | w n. range w  Σ}  {}"
    using assms by fast
  thus ?thesis
    unfolding reacht_def card_eq_0_iff by blast
qed

subsubsection ‹Relation to runs›

lemma run_subseteq_reach:
  assumes "range w  Σ"
  shows "range (run δ q0 w)  reach Σ δ q0" 
    and "range (runt δ q0 w)  reacht Σ δ q0"
  using assms unfolding reach_def reacht_def by blast+

lemma limit_subseteq_reach:
  assumes "range w  Σ"
  shows "limit (run δ q0 w)  reach Σ δ q0"
    and "limit (runt δ q0 w)  reacht Σ δ q0"
  using run_subseteq_reach[OF assms] limit_in_range by fast+

lemma runt_finite:
  assumes "finite (reach Σ δ q0)"
  assumes "finite Σ"
  assumes "range w  Σ"
  defines "r  runt δ q0 w"
  shows "finite (range r)"
proof -
  let ?S = "(reach Σ δ q0) × Σ × (reach Σ δ q0)"
  have "i. w i  Σ" and "i. set (map w [0..<i])  Σ" and "Σ  {}"
    using ‹range w  Σ by auto 
  hence "n. r n  ?S"
    unfolding runt.simps run_foldl reach_foldl_def[OF Σ  {}] r_def by blast
  hence "range r  ?S" and "finite ?S"
    using assms by blast+
  thus "finite (range r)"
    by (blast dest: finite_subset)
qed

subsubsection ‹Compute reach Using DFS›

definition QL :: "'a list  ('b, 'a) DTS  'b  'b set"
where
  "QL Σ δ q0 = (if Σ  [] then gen_dfs (λq. map (δ q) Σ) Set.insert (∈) {} [q0] else {})"

definition list_dfs :: "(('a, 'b) transition  ('a, 'b) transition list)  ('a, 'b) transition list => ('a, 'b) transition list => ('a, 'b) transition list"
where
  "list_dfs succ S start  gen_dfs succ List.insert (λx xs. x  set xs) S start"

definition δL :: "'a list  ('b, 'a) DTS  'b  ('b, 'a) transition set"
where
  "δL Σ δ q0 = set ( 
    let 
      start = map (λν. (q0, ν, δ q0 ν)) Σ; 
      succ = λ(_, _, q). (map (λν. (q, ν, δ q ν)) Σ)
    in 
      (list_dfs succ [] start))"

lemma QL_reach:
  assumes "finite (reach (set Σ) δ q0)"
  shows "QL Σ δ q0 = reach (set Σ) δ q0"
proof (cases "Σ  []")
  case True
    hence reach_redef: "reach (set Σ) δ q0 = {foldl δ q0 w | w. set w  set Σ}"
      using reach_foldl_def[of "set Σ"] unfolding set_empty[of Σ, symmetric] by force
  
    {
      fix x w y
      assume "set w  set Σ" "x = foldl δ q0 w" "y  set (map (δ x) Σ)"
      moreover
      then obtain ν where "y = δ x ν" and "ν  set Σ"
        by auto
      ultimately
      have "y = foldl δ q0 (w@[ν])" and "set (w@[ν])  set Σ"
        by simp+
      hence "w'. set w'  set Σ  y = foldl  δ q0 w'"
        by blast
    }
    note extend_run = this
    
    interpret DFS "λq. map (δ q) Σ" "λq. q  reach (set Σ) δ q0" "λS. S  reach (set Σ) δ q0" Set.insert "(∈)" "{}" id
      apply (unfold_locales; auto simp add: member_rec reach_redef list_all_iff elim: extend_run)
      apply (metis extend_run image_eqI set_map)
      apply (metis assms[unfolded reach_redef])
      done

    have Nil1: "set []  set Σ" and Nil2: "q0 = foldl δ q0 []"
      by simp+
    have list_all_init: "list_all (λq. q  reach (set Σ) δ q0) [q0]"
      unfolding list_all_iff list.set reach_redef using Nil1 Nil2 by blast

    have "reach (set Σ) δ q0  reachable {q0}"
    proof rule
      fix x 
      assume "x  reach (set Σ) δ q0"
      then obtain w where x_def: "x = foldl δ q0 w" and "set w  set Σ"
        unfolding reach_redef by blast
      hence "foldl δ q0 w  reachable {q0}"
      proof (induction w arbitrary: x rule: rev_induct)
        case (snoc ν w)
          hence "foldl δ q0 w  reachable {q0}" and "δ (foldl δ q0 w) ν  set (map (δ (foldl δ q0 w)) Σ)"
            by simp+
          thus ?case
            by (simp add: rtrancl.rtrancl_into_rtrancl reachable_def)
      qed (simp add: reachable_def)
      thus "x  reachable {q0}"
        by (simp add: x_def)
    qed
    moreover
    have "reachable {q0}  reach (set Σ) δ q0"
    proof rule
      fix x 
      assume "x  reachable {q0}"
      hence "(q0, x)  {(x, y). y  set (map (δ x) Σ)}*"
        unfolding reachable_def by blast
      thus "x  reach (set Σ) δ q0"
        apply (induction)
        apply (insert reach_redef Nil1 Nil2; blast)
        apply (metis r_into_rtrancl succsr_def succsr_isNode) 
        done
    qed
    ultimately
    have reachable_redef: "reachable {q0} = reach (set Σ) δ q0"
      by blast

    moreover

    have "reachable {q0}  QL Σ δ q0"
      using reachable_imp_dfs[OF _ list_all_init] unfolding list.set reachable_redef
      unfolding  reach_redef QL_def using Σ  [] by auto

    moreover

    have "QL Σ δ q0  reach (set Σ) δ q0"
      using dfs_invariant[of "{}", OF _ list_all_init] 
      by (auto simp add: reach_redef QL_def)

    ultimately
    show ?thesis
      using Σ  [] dfs_invariant[of "{}", OF _ list_all_init] by simp+
qed (simp add: reach_def QL_def)

lemma δL_reach: 
  assumes "finite (reacht (set Σ) δ q0)"
  shows L Σ δ q0 = reacht (set Σ) δ q0"
proof -
  {
    fix x w y
    assume "set w  set Σ" "x = foldl δ q0 w" "y  set (map (δ x) Σ)"
    moreover
    then obtain ν where "y = δ x ν" and "ν  set Σ"
      by auto
    ultimately
    have "y = foldl δ q0 (w@[ν])" and "set (w@[ν])  set Σ"
      by simp+
    hence "w'. set w'  set Σ  y = foldl  δ q0 w'"
      by blast
  }
  note extend_run = this

  let ?succs = "λ(_, _, q). (map (λν. (q, ν, δ q ν)) Σ)"

  interpret DFS "λ(_, _, q). (map (λν. (q, ν, δ q ν)) Σ)" "λt. t  reacht (set Σ) δ q0" "λS. set S  reacht (set Σ) δ q0" List.insert "λx xs. x  set xs" "[]" id
    apply (unfold_locales; auto simp add: member_rec reacht_foldl_def list_all_iff elim: extend_run)
    apply (metis extend_run image_eqI set_map)
    using  assms unfolding reacht_foldl_def by simp

  have Nil1: "set []  set Σ" and Nil2: "q0 = foldl δ q0 []"
    by simp+
  have list_all_init: "list_all (λq. q  reacht (set Σ) δ q0) (map (λν. (q0, ν, δ q0 ν)) Σ)"
    unfolding list_all_iff reacht_foldl_def set_map image_def using Nil2 by fastforce
  
  let ?q0 = "set (map (λν. (q0, ν, δ q0 ν)) Σ)"

  {
    fix q ν q'  
    assume "(q, ν, q')  reacht (set Σ) δ q0"
    then obtain w where q_def: "q = foldl δ q0 w" and q'_def: "q' = foldl δ q0 (w@[ν])" 
      and "set w  set Σ" and "ν  set Σ"
      unfolding reacht_foldl_def by blast
    hence "(foldl δ q0 w, ν, foldl δ q0 (w@[ν]))  reachable ?q0"
    proof (induction w arbitrary: q q' ν rule: rev_induct)
      case (snoc ν' w)
        hence "(foldl δ q0 w, ν', foldl δ q0 (w@[ν']))  reachable ?q0" (is "(?q, ν', ?q')  _")
          and "q. δ q ν  set (map (δ q) Σ)"
          and "ν  set Σ"
          by simp+
        then obtain x0 where 1: "(x0, (?q, ν', ?q'))  {(x, y). y  set (?succs x)}*" and 2: "x0  ?q0"
          unfolding reachable_def by auto
        moreover
        have 3: "((?q, ν', ?q'), (?q', ν, δ ?q' ν))  {(x, y). y  set (?succs x)}"
          using snoc q. δ q ν  set (map (δ q) Σ) by simp
        ultimately
        show ?case
          using rtrancl.rtrancl_into_rtrancl[OF 1 3] 2 unfolding reachable_def foldl_append foldl.simps  by auto
    qed (auto simp add: reachable_def)
    hence "(q, ν, q')  reachable ?q0"
      by (simp add: q_def q'_def)
  }
  hence "reacht (set Σ) δ q0  reachable ?q0"
    by auto
  moreover
  {
    fix y  
    assume "y  reachable ?q0" 
    then obtain x where "(x, y)  {(x, y). y  set (case x of (_, _, q)  map (λν. (q, ν, δ q ν)) Σ)}*"
      and "x  ?q0"
      unfolding reachable_def by auto
    hence "y  reacht (set Σ) δ q0"
    proof induction
      case base
        have "p ps. list_all p ps = (pa. pa  set ps  p pa)"
          by (meson list_all_iff)
        hence "x  {(foldl δ (foldl δ q0 []) bs, b, foldl δ (foldl δ q0 []) (bs @ [b])) | bs b. set bs  set Σ  b  set Σ}"
          using base by (metis (no_types) Nil2 list_all_init reacht_foldl_def)
        thus ?case
          unfolding reacht_foldl_def by auto
    next
      case (step x' y')
        thus ?case using succsr_def succsr_isNode by blast
    qed
  }
  hence "reachable ?q0  reacht (set Σ) δ q0"
     by blast
  ultimately
  have reachable_redef: "reachable ?q0 = reacht (set Σ) δ q0"
    by blast

  moreover

  have "reachable ?q0  (δL Σ δ q0)"
    using reachable_imp_dfs[OF _ list_all_init] unfolding δL_def reachable_redef list_dfs_def
    by (simp; blast)

  moreover

  have L Σ δ q0  reacht (set Σ) δ q0"
    using dfs_invariant[of "[]", OF _ list_all_init] 
    by (auto simp add: reacht_foldl_def δL_def list_dfs_def)

  ultimately
  show ?thesis 
    by simp
qed

lemma reach_reacht_fst:
  "reach Σ δ q0 = fst ` reacht Σ δ q0"
  unfolding reacht_def reach_def image_def by fastforce

lemma finite_reach:
  "finite (reacht Σ δ q0)  finite (reach Σ δ q0)"
  by (simp add: reach_reacht_fst)

lemma finite_reacht:
  assumes "finite (reach Σ δ q0)"
  assumes "finite Σ"
  shows "finite (reacht Σ δ q0)"
proof -
  have "reacht Σ δ q0  reach Σ δ q0 × Σ × reach Σ δ q0"
    unfolding reacht_def reach_def runt.simps by blast
  thus ?thesis
    using assms finite_subset by blast
qed

lemma QL_eq_δL:
  assumes "finite (reacht (set Σ) δ q0)"
  shows "QL Σ δ q0 = fst ` (δL Σ δ q0)"
  unfolding set_map δL_reach[OF assms] QL_reach[OF finite_reach[OF assms]] reach_reacht_fst ..

subsection ‹Product of DTS› 

fun simple_product :: "('a, 'c) DTS  ('b, 'c) DTS  ('a × 'b, 'c) DTS" ("_ × _")
where
  "δ1 × δ2 = (λ(q1, q2) ν. (δ1 q1 ν, δ2 q2 ν))"  

lemma simple_product_run:
  fixes δ1 δ2 w q1 q2
  defines "ρ  run (δ1 × δ2) (q1, q2) w"
  defines "ρ1  run δ1 q1 w"
  defines "ρ2  run δ2 q2 w"
  shows "ρ i = (ρ1 i, ρ2 i)"
  by (induction i) (insert assms, auto)

theorem finite_reach_simple_product:
  assumes "finite (reach Σ δ1 q1)"
  assumes "finite (reach Σ δ2 q2)"
  shows "finite (reach Σ (δ1 × δ2) (q1, q2))"
proof -
  have "reach Σ (δ1 × δ2) (q1, q2)  reach Σ δ1 q1 × reach Σ δ2 q2"
    unfolding reach_def simple_product_run by blast
  thus ?thesis
    using assms finite_subset by blast
qed

subsection ‹(Generalised) Product of DTS›

fun product :: "('a  ('b, 'c) DTS)  ('a  'b, 'c) DTS" ("Δ×")
where
  "Δ× δm = (λq ν. (λx. case q x of None  None | Some y  Some (δm x y ν)))"  

lemma product_run_None:
  fixes ιm δm w
  defines "ρ  run (Δ× δm) ιm w"
  assumes "ιm k = None"
  shows "ρ i k = None"
  by (induction i) (insert assms, auto)

lemma product_run_Some:
  fixes ιm δm w q0 k
  defines "ρ  run (Δ× δm) ιm w"
  defines "ρ'  run (δm k) q0 w"
  assumes "ιm k = Some q0"
  shows "ρ i k = Some (ρ' i)"
  by (induction i) (insert assms, auto)

theorem finite_reach_product:
  assumes "finite (dom ιm)"
  assumes "x. x  dom ιm  finite (reach Σ (δm x) (the (ιm x)))"
  shows "finite (reach Σ (Δ× δm) ιm)"
  using assms(1,2) 
proof (induction "dom ιm" arbitrary: ιm) 
  case empty
    hence "ιm = Map.empty"
      by auto
    hence "w i. run (Δ× δm) ιm w i = (λx. None)"
      using product_run_None by fast
    thus ?case
      unfolding reach_def by simp
next 
  case (insert k K)
    define f where "f = (λ(q :: 'b, m :: 'a  'b). m(k := Some q))"
    define Reach where "Reach = (reach Σ (δm k) (the (ιm k))) × ((reach Σ (Δ× δm) (ιm(k := None))))"

    have "(reach Σ (Δ× δm) ιm)  f ` Reach"
    proof
      fix x
      assume "x  reach Σ (Δ× δm) ιm"
      then obtain w n where x_def: "x = run (Δ× δm) ιm w n" and "range w  Σ"
        unfolding reach_def by blast
      {
        fix k'
        have "k'  dom ιm  x k' = run (Δ× δm) (ιm(k := None)) w n k'"
          unfolding x_def dom_def using product_run_None[of _ _ δm] by simp
        moreover
        have "k'  dom ιm - {k}  x k' = run (Δ× δm) (ιm(k := None)) w n k'"
          unfolding x_def dom_def using product_run_Some[of _ _ _ δm] by auto
        ultimately
        have "k'  k  x k' = run (Δ× δm) (ιm(k := None)) w n k'"
          by blast
      }
      hence "x(k := None) = run (Δ× δm) (ιm(k := None)) w n"
        using product_run_None[of _ _ δm] by auto
      moreover
      have "x k = Some (run (δm k) (the (ιm k)) w n)"
        unfolding x_def using product_run_Some[of ιm k _ δm] insert.hyps(4) by force 
      ultimately
      have "(the (x k), x(k := None))  Reach"
        unfolding Reach_def reach_def using ‹range w  Σ by auto
      moreover
      have "x = f (the (x k), x(k := None))"
        unfolding f_def using x k = Some (run (δm k) (the (ιm k)) w n) by auto 
      ultimately
      show "x  f ` Reach"
         by simp
    qed
    moreover
    have "finite (reach Σ (Δ× δm) (ιm (k := None)))"
      using insert insert(3)[of "ιm (k:=None)"] by auto 
    hence "finite Reach"
      using insert Reach_def by blast
    hence "finite (f ` Reach)"
      .. 
    ultimately
    show ?case
      by (rule finite_subset)
qed

subsection ‹Simple Product Construction Helper Functions and Lemmas›

fun embed_transition_fst :: "('a, 'c) transition  ('a × 'b, 'c) transition set"
where
  "embed_transition_fst (q, ν, q') = {((q, x), ν, (q', y)) | x y. True}"

fun embed_transition_snd :: "('b, 'c) transition  ('a × 'b, 'c) transition set"
where
  "embed_transition_snd (q, ν, q') = {((x, q), ν, (y, q')) | x y. True}"

lemma embed_transition_snd_unfold:
  "embed_transition_snd t = {((x, fst t), fst (snd t), (y, snd (snd t))) | x y. True}"
  unfolding embed_transition_snd.simps[symmetric] by simp

fun project_transition_fst :: "('a × 'b, 'c) transition  ('a, 'c) transition" 
where
  "project_transition_fst (x, ν, y) = (fst x, ν, fst y)"

fun project_transition_snd :: "('a × 'b, 'c) transition  ('b, 'c) transition" 
where
  "project_transition_snd (x, ν, y) = (snd x, ν, snd y)"

lemma
  fixes δ1 δ2 w q1 q2
  defines "ρ  runt (δ1 × δ2) (q1, q2) w"
  defines "ρ1  runt δ1 q1 w"
  defines "ρ2  runt δ2 q2 w"
  shows product_run_project_fst: "project_transition_fst (ρ i) = ρ1 i" 
    and product_run_project_snd: "project_transition_snd (ρ i) = ρ2 i"
    and product_run_embed_fst: "ρ i  embed_transition_fst (ρ1 i)"
    and product_run_embed_snd: "ρ i  embed_transition_snd (ρ2 i)"
  unfolding assms runt.simps simple_product_run by simp_all

lemma 
  fixes δ1 δ2 w q1 q2
  defines "ρ  runt (δ1 × δ2) (q1, q2) w"
  defines "ρ1  runt δ1 q1 w"
  defines "ρ2  runt δ2 q2 w"
  assumes "finite (range ρ)"
  shows product_run_finite_fst: "finite (range ρ1)"
    and product_run_finite_snd: "finite (range ρ2)"
proof -
  have "k. project_transition_fst (ρ k) = ρ1 k"
    and "k. project_transition_snd (ρ k) = ρ2 k"
    unfolding assms product_run_project_fst product_run_project_snd by simp+
  hence "project_transition_fst ` range ρ = range ρ1"
    and "project_transition_snd ` range ρ = range ρ2"
    using range_composition[symmetric, of project_transition_fst ρ]
    using range_composition[symmetric, of project_transition_snd ρ] by presburger+
  thus "finite (range ρ1)" and "finite (range ρ2)"
    using assms finite_imageI by metis+
qed

lemma 
  fixes δ1 δ2 w q1 q2
  defines "ρ  runt (δ1 × δ2) (q1, q2) w"
  defines "ρ1  runt δ1 q1 w"
  assumes "finite (range ρ)"
  shows product_run_project_limit_fst: "project_transition_fst ` limit ρ = limit ρ1"
    and product_run_embed_limit_fst: "limit ρ   (embed_transition_fst ` (limit ρ1))"
proof -
  have "finite (range ρ1)"
    using assms product_run_finite_fst by metis

  then obtain i where "limit ρ = range (suffix i ρ)" and "limit ρ1 = range (suffix i ρ1)"
    using common_range_limit assms by metis
  moreover
  have "k. project_transition_fst (suffix i ρ k) = (suffix i ρ1 k)"
    by (simp only: assms runt.simps) (metis ρ1_def product_run_project_fst suffix_nth) 
  hence "project_transition_fst ` range (suffix i ρ) = (range (suffix i ρ1))"
    using range_composition[symmetric, of "project_transition_fst" "suffix i ρ"] by presburger
  moreover
  have "k. (suffix i ρ k)  embed_transition_fst (suffix i ρ1 k)"
    using assms product_run_embed_fst by simp
  ultimately
  show "project_transition_fst ` limit ρ = limit ρ1" 
    and "limit ρ   (embed_transition_fst ` (limit ρ1))"
    by auto
qed 

lemma 
  fixes δ1 δ2 w q1 q2
  defines "ρ  runt (δ1 × δ2) (q1, q2) w"
  defines "ρ2  runt δ2 q2 w"
  assumes "finite (range ρ)"
  shows product_run_project_limit_snd: "project_transition_snd ` limit ρ = limit ρ2"
    and product_run_embed_limit_snd: "limit ρ   (embed_transition_snd ` (limit ρ2))"
proof -
  have "finite (range ρ2)"
    using assms product_run_finite_snd by metis

  then obtain i where "limit ρ = range (suffix i ρ)" and "limit ρ2 = range (suffix i ρ2)"
    using common_range_limit assms by metis
  moreover
  have "k. project_transition_snd (suffix i ρ k) = (suffix i ρ2 k)"
    by (simp only: assms runt.simps) (metis ρ2_def product_run_project_snd suffix_nth) 
  hence "project_transition_snd ` range ((suffix i ρ)) = (range (suffix i ρ2))"
    using range_composition[symmetric, of "project_transition_snd" "(suffix i ρ)"] by presburger
  moreover
  have "k. (suffix i ρ k)  embed_transition_snd (suffix i ρ2 k)"
    using assms product_run_embed_snd by simp
  ultimately
  show "project_transition_snd ` limit ρ = limit ρ2" 
    and "limit ρ   (embed_transition_snd ` (limit ρ2))"
    by auto
qed 

lemma 
  fixes δ1 δ2 w q1 q2
  defines "ρ  runt (δ1 × δ2) (q1, q2) w"
  defines "ρ1  runt δ1 q1 w"
  defines "ρ2  runt δ2 q2 w"
  assumes "finite (range ρ)"
  shows product_run_embed_limit_finiteness_fst: "limit ρ  ( (embed_transition_fst ` S)) = {}  limit ρ1  S = {}" (is "?thesis1")
    and product_run_embed_limit_finiteness_snd: "limit ρ  ( (embed_transition_snd ` S')) = {}  limit ρ2  S' = {}" (is "?thesis2")
proof -
  show ?thesis1
    using assms product_run_project_limit_fst by fastforce
  show ?thesis2
    using assms product_run_project_limit_snd by fastforce
qed

subsection ‹Product Construction Helper Functions and Lemmas›

fun embed_transition :: "'a  ('b, 'c) transition  ('a  'b, 'c) transition set" ("↿⇩_")
where
  "↿⇩x (q, ν, q') = {(m, ν, m') | m m'. m x = Some q  m' x = Some q'}"

fun project_transition :: "'a  ('a  'b, 'c) transition  ('b, 'c) transition" ("⇃⇩_")
where
  "⇃⇩x (m, ν, m') = (the (m x), ν, the (m' x))"

fun embed_pair :: "'a  (('b, 'c) transition set × ('b, 'c) transition set)  (('a  'b, 'c) transition set × ('a  'b, 'c) transition set)" ("_")
where
  "x (S, S') = ((↿⇩x ` S), (↿⇩x ` S'))" 

fun project_pair :: "'a  (('a  'b, 'c) transition set × ('a  'b, 'c) transition set)  (('b, 'c) transition set × ('b, 'c) transition set)" ("_")
where
  "x (S, S') = (⇃⇩x ` S, ⇃⇩x ` S')" 

lemma embed_transition_unfold:
  "embed_transition x t = {(m, fst (snd t), m') | m m'. m x = Some (fst t)  m' x = Some (snd (snd t))}"
  unfolding embed_transition.simps[symmetric] by simp

lemma
  fixes ιm δm w q0 
  fixes x :: "'a"
  defines "ρ  runt (Δ× δm) ιm w"
  defines "ρ'  runt (δm x) q0 w"
  assumes "ιm x = Some q0"
  shows product_run_project: "⇃⇩x (ρ i) = ρ' i" 
    and product_run_embed: "ρ i  ↿⇩x (ρ' i)"
  using assms product_run_Some[of _ _ _ δm] by simp+

lemma 
  fixes ιm δm w q0 x
  defines "ρ  runt (Δ× δm) ιm w"
  defines "ρ'  runt (δm x) q0 w"
  assumes "ιm x = Some q0"
  assumes "finite (range ρ)"
  shows product_run_project_limit: "⇃⇩x ` limit ρ = limit ρ'" 
    and product_run_embed_limit: "limit ρ   (↿⇩x ` (limit ρ'))"
proof -
  have "k. ⇃⇩x (ρ k) = ρ' k"
    using assms product_run_embed[of _ _ _ δm] by simp
  hence "⇃⇩x ` range ρ = range ρ'"
    using range_composition[symmetric, of "⇃⇩x" ρ] by presburger
  hence "finite (range ρ')"
    using assms finite_imageI by metis

  then obtain i where "limit ρ = range (suffix i ρ)" and "limit ρ' = range (suffix i ρ')"
    using common_range_limit assms by metis
  moreover  
  have "k. ⇃⇩x (suffix i ρ k) = (suffix i ρ' k)"
    using assms product_run_embed[of _ _ _ δm] by simp
  hence "⇃⇩x ` range ((suffix i ρ)) = (range (suffix i ρ'))"
    using range_composition[symmetric, of "⇃⇩x" "(suffix i  ρ)"] by presburger
  moreover
  have "k. (suffix i ρ k)  ↿⇩x (suffix i ρ' k)"
    using assms product_run_embed[of _ _ _ δm] by simp
  ultimately
  show "⇃⇩x ` limit ρ = limit ρ'" and "limit ρ   (↿⇩x ` (limit ρ'))"
    by auto
qed

lemma product_run_embed_limit_finiteness:
  fixes ιm δm w q0 k
  defines "ρ  runt (Δ× δm) ιm w"
  defines "ρ'  runt (δm k) q0 w"
  assumes "ιm k = Some q0"
  assumes "finite (range ρ)"
  shows "limit ρ  ( (↿⇩k ` S)) = {}  limit ρ'  S = {}"
  (is "?lhs  ?rhs")
proof -
  have "⇃⇩k ` limit ρ  S  {}  limit ρ  ( (↿⇩k ` S))  {}"
  proof
    assume "⇃⇩k ` limit ρ  S  {}"
    then obtain q ν q' where "(q, ν, q')  ⇃⇩k ` limit ρ" and "(q, ν, q')  S"
      by auto
    moreover
    have "m ν m' i. (m, ν, m') = ρ i  p p'. m k = Some p  m' k = Some p'" 
      using assms product_run_Some[of ιm , OF assms(3)] by auto
    hence "m ν m'. (m, ν, m')  limit ρ  p p'. m k = Some p  m' k = Some p'" 
      using limit_in_range by fast
    ultimately
    obtain m m' where "m k = Some q" and "m' k = Some q'" and "(m, ν, m')  limit ρ"
      by auto
    moreover
    hence "(m, ν, m')   (↿⇩k ` S)"
      using (q, ν, q')  S by force
    ultimately
    show "limit ρ  ( (↿⇩k ` S))  {}"
      by blast
  qed
  hence "?lhs  ⇃⇩k ` limit ρ  S = {}"
    by auto
  also
  have "  ?rhs"
    using assms product_run_project_limit[of _ _ _ δm] by simp
  finally
  show ?thesis
    by simp
qed

subsection ‹Transfer Rules›

context includes lifting_syntax
begin

lemma product_parametric [transfer_rule]:
  "((A ===> B ===> C ===> B) ===> (A ===> rel_option B) ===> C ===> A ===> rel_option B) product product"
  by (auto simp add: rel_fun_def rel_option_iff split: option.split)

lemma run_parametric [transfer_rule]:
  "((A ===> B ===> A) ===> A ===> ((=) ===> B) ===> (=) ===> A) run run"
proof -
  {
    fix δ δ' q q' n w 
    fix w' :: "nat  'd" 
    assume "(A ===> B ===> A) δ δ'" "A q q'" "((=) ===> B) w w'" 
    hence "A (run δ q w n) (run δ' q' w' n)"
      by (induction n) (simp_all add: rel_fun_def)
  }
  thus ?thesis
    by blast
qed

lemma reach_parametric [transfer_rule]:
  assumes "bi_total B"
  assumes "bi_unique B"
  shows "(rel_set B ===> (A ===> B ===> A) ===> A ===> rel_set A) reach reach"
proof standard+
  fix Σ Σ' δ δ' q q'
  assume "rel_set B Σ Σ'" "(A ===> B ===> A) δ δ'" "A q q'"

  {
    fix z 
    assume "z  reach Σ δ q"
    then obtain w n where "z = run δ q w n" and "range w  Σ"
      unfolding reach_def by auto
    
    define w' where "w' n = (SOME x. B (w n) x)" for n
    
    have "n. w n  Σ"
      using ‹range w  Σ by blast
    hence "n. w' n  Σ'"
      using assms ‹rel_set B Σ Σ' by (simp add: w'_def bi_unique_def rel_set_def; metis someI) 
    hence "run δ' q' w' n  reach Σ' δ' q'"
      unfolding reach_def by auto
     
    moreover

    have "A z (run δ' q' w' n)"
      apply (unfold z = run δ q w n)
      apply (insert A q q' (A ===> B ===> A) δ δ' assms(1))  
      apply (induction n) 
      apply (simp_all add: rel_fun_def bi_total_def w'_def) 
      by (metis tfl_some)  

    ultimately

    have "z'  reach Σ' δ' q'. A z z'"
      by blast
  }

  moreover
  
  {
    fix z 
    assume "z  reach Σ' δ' q'"
    then obtain w n where "z = run δ' q' w n" and "range w  Σ'"
      unfolding reach_def by auto
    
    define w' where "w' n = (SOME x. B x (w n))" for n
    
    have "n. w n  Σ'"
      using ‹range w  Σ' by blast
    hence "n. w' n  Σ"
      using assms ‹rel_set B Σ Σ' by (simp add: w'_def bi_unique_def rel_set_def; metis someI)
    hence "run δ q w' n  reach Σ δ q"
      unfolding reach_def by auto
     
    moreover

    have "A (run δ q w' n) z"
      apply (unfold z = run δ' q' w n)
      apply (insert A q q' (A ===> B ===> A) δ δ' assms(1))  
      apply (induction n) 
      apply (simp_all add: rel_fun_def bi_total_def w'_def) 
      by (metis tfl_some)  

    ultimately

    have "z'  reach Σ δ q. A z' z"
      by blast
  }
  ultimately
  show "rel_set A (reach Σ δ q) (reach Σ' δ' q')"
    unfolding rel_set_def by blast
qed

end

subsection ‹Lift to Mapping›

lift_definition product_abs :: "('a  ('b, 'c) DTS)  (('a, 'b) mapping, 'c) DTS" ("↑Δ×") is product 
  parametric product_parametric .

lemma product_abs_run_None:
  "Mapping.lookup ιm k = None  Mapping.lookup (run (↑Δ× δm) ιm w i) k = None"
  by (transfer; insert product_run_None)

lemma product_abs_run_Some:
  "Mapping.lookup ιm k = Some q0  Mapping.lookup (run (↑Δ× δm) ιm w i) k = Some (run (δm k) q0 w i)"
  by (transfer; insert product_run_Some)

theorem finite_reach_product_abs:
  assumes "finite (Mapping.keys ιm)"
  assumes "x. x  (Mapping.keys ιm)  finite (reach Σ (δm x) (the (Mapping.lookup ιm x)))"
  shows "finite (reach Σ (↑Δ× δm) ιm)"
  using assms by (transfer; blast intro: finite_reach_product)

end

Theory Semi_Mojmir

(*
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Mojmir Automata (Without Final States)›

theory Semi_Mojmir
  imports Main "Auxiliary/Preliminaries2" DTS
begin

subsection ‹Definitions›

locale semi_mojmir_def =
  fixes
    ― ‹Alphapet›
    Σ :: "'a set"
  fixes
    ― ‹Transition Function›
    δ :: "('b, 'a) DTS"
  fixes
    ― ‹Initial State›
    q0 :: "'b"
  fixes
    ― ‹$\omega$-Word›
    w :: "'a word"
begin

definition sink :: "'b  bool"
where
  "sink q  (q0  q)  (ν  Σ. δ q ν = q)"

declare sink_def [code]

fun token_run :: "nat  nat  'b"
where
  "token_run x n = run δ q0 (suffix x w) (n - x)"

fun configuration :: "'b  nat  nat set"
where
  "configuration q n = {x. x  n  token_run x n = q}"

fun oldest_token :: "'b  nat  nat option"
where
  "oldest_token q n = (if configuration q n  {} then Some (Min (configuration q n)) else None)"

fun senior :: "nat  nat  nat"
where
  "senior x n = the (oldest_token (token_run x n) n)"

fun older_seniors :: "nat  nat  nat set"
where
  "older_seniors x n = {s. y. s = senior y n  s < senior x n  ¬ sink (token_run s n)}"

fun rank :: "nat  nat  nat option"
where
  "rank x n =
    (if x  n  ¬sink (token_run x n) then Some (card (older_seniors x n)) else None)"

fun senior_states :: "'b  nat  'b set"
where
  "senior_states q n =
    {p. x y. oldest_token p n = Some y  oldest_token q n = Some x  y < x  ¬ sink p}"

fun state_rank :: "'b  nat  nat option"
where
  "state_rank q n = (if configuration q n  {}  ¬sink q then Some (card (senior_states q n)) else None)"

definition max_rank :: "nat"
where
  "max_rank = card (reach Σ δ q0 - {q. sink q})"

subsubsection ‹Iterative Computation of State-Ranks›

fun initial :: "'b  nat option"
where
  "initial q = (if q = q0 then Some 0 else None)"

fun pre_ranks :: "('b  nat option)  'a  'b  nat set"
where
  "pre_ranks r ν q = {i . q'. r q' = Some i  q = δ q' ν}  (if q = q0 then {max_rank} else {})"

fun step :: "('b  nat option)  'a  ('b  nat option)"
where
  "step r ν q = (
    if
      ¬sink q  pre_ranks r ν q  {}
    then
      Some (card {q'. ¬sink q'  pre_ranks r ν q'  {}  Min (pre_ranks r ν q') < Min (pre_ranks r ν q)})
    else
      None)"

subsubsection ‹Properties of Tokens›

definition token_squats :: "nat  bool"
where
  "token_squats x = (n. ¬sink (token_run x n))"

end

locale semi_mojmir = semi_mojmir_def +
  assumes
    ― ‹The alphabet is finite. Non-emptiness is derived from well-formed w›
    finite_Σ: "finite Σ"
  assumes
    ― ‹The set of reachable states is finite›
    finite_reach: "finite (reach Σ δ q0)"
  assumes
    ― ‹w only contains letters from the alphabet›
    bounded_w: "range w  Σ"
begin

lemma nonempty_Σ: "Σ  {}"
  using bounded_w by blast

lemma bounded_w': "w i  Σ"
  using bounded_w by blast

― ‹Naming Scheme:

This theory uses the following naming scheme to consistently name variables.

* Tokens: x, y, z
* Time: n, m
* Rank: i, j, k
* States: p, q›

lemma sink_rev_step:
  "¬sink q  q = δ q' ν  ν  Σ  ¬sink q'"
  "¬sink q  q = δ q' (w i)  ¬sink q'"
  using bounded_w' by (force simp only: sink_def)+

subsection ‹Token Run›

lemma token_stays_in_sink:
  assumes "sink q"
  assumes "token_run x n = q"
  shows "token_run x (n + m) = q"
proof (cases "x  n")
  case True
    show ?thesis
    proof (induction m)
      case 0
        show ?case
          using assms(2) by simp
    next
      case (Suc m)
        have "x  n + m"
          using True by simp
        moreover
        have "x. w x  Σ"
          using bounded_w by auto
        ultimately
        have "t. token_run x (n + m)  = q  token_run x (n + m + 1) = q"
          using ‹sink q[unfolded sink_def] upt_add_eq_append[OF le0, of "n + m" 1]
          using Suc_diff_le by simp
        with Suc show ?case
          by simp
    qed
qed (insert assms, simp add: sink_def)

lemma token_is_not_in_sink:
  "token_run x n  A  token_run x (Suc n)  A  ¬sink (token_run x n)"
  by (metis Suc_eq_plus1 token_stays_in_sink)

lemma token_run_intial_state:
  "token_run x x = q0"
  by simp

lemma token_run_P:
  assumes "¬ P (token_run x n)"
  assumes "P (token_run x (Suc (n + m)))"
  shows "m'  m. ¬ P (token_run x (n + m'))  P (token_run x (Suc (n + m')))"
  using assms by (induction m) (simp_all, metis add_Suc_right le_Suc_eq)

lemma token_run_merge_Suc:
  assumes "x  n"
  assumes "y  n"
  assumes "token_run x n = token_run y n"
  shows "token_run x (Suc n) = token_run y (Suc n)"
proof -
  have "run δ q0 (suffix x w) (Suc (n - x)) = run δ q0 (suffix y w) (Suc (n - y))"
    using assms by fastforce
  thus ?thesis
    using Suc_diff_le assms(1,2) by force
qed

lemma token_run_merge:
  "x  n; y  n; token_run x n = token_run y n  token_run x (n + m) = token_run y (n + m)"
  using token_run_merge_Suc[of x _ y] by (induction m) auto

lemma token_run_mergepoint:
  assumes "x < y"
  assumes "token_run x (y + n) = token_run y (y + n)"
  obtains m where "x  (Suc m)" and "y  (Suc m)"
    and "y = Suc m  token_run x m  token_run y m"
    and "token_run x (Suc m) = token_run y (Suc m)"
  using assms by (induction n)
    ((metis add_0_iff le_Suc_eq le_add1 less_imp_Suc_add),
     (metis add_Suc_right le_add1 less_or_eq_imp_le order_trans))

subsubsection ‹Step Lemmas›

lemma token_run_step:
  assumes "x  n"
  assumes "token_run x n = q'"
  assumes "q = δ q' (w n)"
  shows "token_run x (Suc n) = q"
  using assms unfolding token_run.simps Suc_diff_le[OF x  n] by force

lemma token_run_step':
  "x  n  token_run x (Suc n) = δ (token_run x n) (w n)"
  using token_run_step by simp

subsection ‹Configuration›

subsubsection ‹Properties›

lemma configuration_distinct:
  "q  q'  configuration q n  configuration q' n = {}"
  by auto

lemma configuration_finite:
  "finite (configuration q n)"
  by simp

lemma configuration_non_empty:
  "x  n  configuration (token_run x n) n  {}"
  by fastforce

lemma configuration_token:
  "x  n  x  configuration (token_run x n) n"
  by fastforce

lemmas configuration_Max_in = Max_in[OF configuration_finite]
lemmas configuration_Min_in = Min_in[OF configuration_finite]

subsubsection ‹Monotonicity›

lemma configuration_monotonic_Suc:
  "x  n  configuration (token_run x n) n  configuration (token_run x (Suc n)) (Suc n)"
proof
  fix y
  assume "y  configuration (token_run x n) n"
  hence "y  n" and "token_run x n = token_run y n"
    by simp_all
  moreover
  assume "x  n"
  ultimately
  have "token_run x (Suc n) = token_run y (Suc n)"
    using token_run_merge_Suc by blast
  thus "y  configuration (token_run x (Suc n)) (Suc n)"
    using configuration_token y  n by simp
qed

subsubsection ‹Pull-Up and Push-Down›

lemma pull_up_token_run_tokens:
  "x  n; y  n; token_run x n = token_run y n  q. x  configuration q n  y  configuration q n"
  by force

lemma push_down_configuration_token_run:
  "x  configuration q n; y  configuration q n  x  n  y  n  token_run x n = token_run y n"
  by simp

subsubsection ‹Step Lemmas›

lemma configuration_step:
  "x  configuration q' n  q = δ q' (w n)  x  configuration q (Suc n)"
  using Suc_diff_le by simp

lemma configuration_step_non_empty:
  "configuration q' n  {}  q = δ q' (w n)  configuration q (Suc n)  {}"
  by (blast dest: configuration_step)

lemma configuration_rev_step':
  assumes "x  Suc n"
  assumes "x  configuration q (Suc n)"
  obtains q' where "q = δ q' (w n)" and "x  configuration q' n"
  using assms Suc_diff_le by force

lemma configuration_rev_step'':
  assumes "x  configuration q0 (Suc n)"
  shows "x = Suc n  (q'. q0 = δ q' (w n)  x  configuration q' n)"
  using assms configuration_rev_step' by metis

lemma configuration_step_eq_q0:
  "configuration q0 (Suc n) = {Suc n}  {configuration q' n | q'. q0 = δ q' (w n)}"
  apply rule using configuration_rev_step'' apply fast using configuration_step[of _ _ n q0] by fastforce

lemma configuration_rev_step:
  assumes "q  q0"
  assumes "x  configuration q (Suc n)"
  obtains q' where "q = δ q' (w n)" and "x  configuration q' n"
  using configuration_rev_step'[OF _ assms(2)] assms by fastforce

lemma configuration_step_eq:
  assumes "q  q0"
  shows "configuration q (Suc n) = {configuration q' n | q'. q = δ q' (w n)}"
  using configuration_rev_step[OF assms, of _ n] configuration_step by auto

lemma configuration_step_eq_unified:
  shows "configuration q (Suc n) = {configuration q' n | q'. q = δ q' (w n)}  (if q = q0 then {Suc n} else {}) "
  using configuration_step_eq configuration_step_eq_q0 by force

subsection ‹Oldest Token›

subsubsection ‹Properties›

lemma oldest_token_always_def:
  "i. i  x  oldest_token (token_run x n) n = Some i"
proof (cases "x  n")
  case False
    let ?q = "token_run x n"
    from False have "n  configuration ?q n" and "configuration ?q n  {}"
      by auto
    then obtain i where "i  n" and "oldest_token ?q n = Some i"
      by (metis Min.coboundedI oldest_token.simps configuration_finite)
    moreover
    hence "i  x"
      using False by linarith
    ultimately
    show ?thesis
      by blast
qed fastforce

lemma oldest_token_bounded:
  "oldest_token q n = Some x  x  n"
  by (metis oldest_token.simps configuration_Min_in option.distinct(1) option.inject push_down_configuration_token_run)

lemma oldest_token_distinct:
  "q  q'  oldest_token q n = Some i  oldest_token q' n = Some j  i  j"
  by (metis configuration_Min_in configuration_distinct disjoint_iff_not_equal option.distinct(1) oldest_token.simps option.sel)

lemma oldest_token_equal:
  "oldest_token q n = Some i  oldest_token q' n = Some i  q = q'"
  using oldest_token_distinct by blast

subsubsection ‹Monotonicity›

lemma oldest_token_monotonic_Suc:
  assumes "x  n"
  assumes "oldest_token (token_run x n) n = Some i"
  assumes "oldest_token (token_run x (Suc n)) (Suc n) = Some j"
  shows "i  j"
proof -
  from assms have "i = Min (configuration (token_run x n) n)"
    and "j = Min (configuration (token_run x (Suc n)) (Suc n))"
    by (metis oldest_token.elims option.discI option.sel)+
  thus ?thesis
    using Min_antimono[OF configuration_monotonic_Suc[OF assms(1)] configuration_non_empty[OF assms(1)] configuration_finite] by blast
qed

subsubsection ‹Pull-Up and Push-Down›

lemma push_down_oldest_token_configuration:
  "oldest_token q n = Some x  x  configuration q n"
  by (metis configuration_Min_in oldest_token.simps option.distinct(2) option.inject)

lemma push_down_oldest_token_token_run:
  "oldest_token q n = Some x  token_run x n = q"
  using push_down_oldest_token_configuration configuration.simps by blast

subsection ‹Senior Token›

subsubsection ‹Properties›

lemma senior_le_token:
  "senior x n  x"
  using oldest_token_always_def[of x n] by fastforce

lemma senior_token_run:
  "senior x n = senior y n  token_run x n = token_run y n"
  by (metis oldest_token_always_def oldest_token_distinct option.sel senior.simps)

text ‹The senior of a token is always in the same state›

lemma senior_same_state:
  "token_run (senior x n) n = token_run x n"
proof -
  have X: "{t. t  n  token_run t n = token_run x n}  {}"
    by (cases "x  n") auto
  show ?thesis
    using Min_in[OF _ X] by force
qed

lemma senior_senior:
  "senior (senior x n) n = senior x n"
  using senior_same_state senior_token_run by blast

subsubsection ‹Monotonicity›

lemma senior_monotonic_Suc:
  "x  n  senior x n  senior x (Suc n)"
  by (metis oldest_token_always_def oldest_token_monotonic_Suc option.sel senior.simps)

subsubsection ‹Pull-Up and Push-Down›

lemma pull_up_configuration_senior:
  "x  configuration q n; y  configuration q n  senior x n = senior y n"
  by force

lemma push_down_senior_tokens:
  "x  n; y  n; senior x n = senior y n  q. x  configuration q n  y  configuration q n"
  using senior_token_run pull_up_token_run_tokens by blast

subsection ‹Set of Older Seniors›

subsubsection ‹Properties›

lemma older_seniors_cases_subseteq [case_names le ge]:
  assumes "older_seniors x n  older_seniors y n  P"
  assumes "older_seniors x n  older_seniors y n  P"
  shows "P" using assms by fastforce

lemma older_seniors_cases_subset [case_names less equal greater]:
  assumes "older_seniors x n  older_seniors y n  P"
  assumes "older_seniors x n = older_seniors y n  P"
  assumes "older_seniors x n  older_seniors y n  P"
  shows "P" using assms older_seniors_cases_subseteq by blast

lemma older_seniors_finite:
  "finite (older_seniors x n)"
  by fastforce

lemma older_seniors_older:
  "y  older_seniors x n  y < x"
  using less_le_trans[OF _ senior_le_token, of y x n] by force

lemma older_seniors_senior_simp:
  "older_seniors (senior x n) n = older_seniors x n"
  unfolding older_seniors.simps senior_senior ..

lemma older_seniors_not_self_referential:
  "senior x n  older_seniors x n"
  by simp

lemma older_seniors_not_self_referential_2:
  "x  older_seniors x n"
  using older_seniors_older older_seniors_not_self_referential less_not_refl by blast

lemma older_seniors_subset:
  "y  older_seniors x n  older_seniors y n  older_seniors x n"
  using older_seniors_not_self_referential_2 by (cases rule: older_seniors_cases_subset) blast+

lemma older_seniors_subset_2:
  assumes "¬ sink (token_run x n)"
  assumes "older_seniors x n  older_seniors y n"
  shows "senior x n  older_seniors y n"
proof -
  have "senior x n < senior y n"
    using assms(2) by fastforce
  thus ?thesis
    using assms(1)[unfolded senior_same_state[symmetric, of x n]]
    unfolding older_seniors.simps by blast
qed

lemmas older_seniors_Max_in = Max_in[OF older_seniors_finite]
lemmas older_seniors_Min_in = Min_in[OF older_seniors_finite]
lemmas older_seniors_Max_coboundedI = Max.coboundedI[OF older_seniors_finite]
lemmas older_seniors_Min_coboundedI = Min.coboundedI[OF older_seniors_finite]
lemmas older_seniors_card_mono = card_mono[OF older_seniors_finite]
lemmas older_seniors_psubset_card_mono = psubset_card_mono[OF older_seniors_finite]

lemma older_seniors_recursive:
  fixes x n
  defines "os  older_seniors x n"
  assumes "os  {}"
  shows "os = {Max os}  older_seniors (Max os) n"
  (is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
  proof
    fix x
    assume "x  ?lhs"
    show "x  ?rhs"
    proof (cases "x = Max os")
      case False
        hence "x < Max os"
          by (metis older_seniors_Max_coboundedI os_def x  os dual_order.order_iff_strict)
        moreover
        obtain y' where "Max os = senior y' n"
          using older_seniors_Max_in assms(2)
          unfolding os_def older_seniors.simps by blast
        ultimately
        have "x < senior (Max os) n"
          using senior_senior by presburger
        moreover
        from x  ?lhs obtain y where "x = senior y n" and "¬ sink (token_run x n)"
          unfolding os_def older_seniors.simps by blast
        ultimately
        show ?thesis
          unfolding older_seniors.simps by blast
    qed blast
  qed
next
  show "?lhs  ?rhs"
    using older_seniors_subset older_seniors_Max_in assms(2)
    unfolding os_def by blast
qed

lemma older_seniors_recursive_card:
  fixes x n
  defines "os  older_seniors x n"
  assumes "os  {}"
  shows "card os = Suc (card (older_seniors (Max os) n))"
  by (metis older_seniors_recursive assms Un_empty_left Un_insert_left card_insert_disjoint older_seniors_finite older_seniors_not_self_referential_2)

lemma older_seniors_card:
  "card (older_seniors x n) = card (older_seniors y n)  older_seniors x n = older_seniors y n"
  by (metis less_not_refl older_seniors_cases_subset older_seniors_psubset_card_mono)

lemma older_seniors_card_le:
  "card (older_seniors x n) < card (older_seniors y n)  older_seniors x n  older_seniors y n"
  by (metis card_mono card_psubset not_le older_seniors_cases_subseteq older_seniors_finite psubset_card_mono)

lemma older_seniors_card_less:
  "card (older_seniors x n)  card (older_seniors y n)  older_seniors x n  older_seniors y n"
   by (metis not_le older_seniors_card_mono older_seniors_cases_subseteq older_seniors_psubset_card_mono subset_not_subset_eq)

subsubsection ‹Monotonicity›

lemma older_seniors_monotonic_Suc:
  assumes "x  n"
  shows "older_seniors x n  older_seniors x (Suc n)"
proof
  fix y
  assume "y  older_seniors x (Suc n)"
  then obtain ox where "y = senior ox (Suc n)"
    and "y < senior x (Suc n)"
    and "¬ sink (token_run y (Suc n))"
    unfolding older_seniors.simps by blast

  hence "y = senior y n"
    using senior_senior senior_le_token senior_monotonic_Suc assms
    by (metis add.commute add.left_commute dual_order.order_iff_strict linear not_add_less1 not_less le_iff_add)
  moreover
  have "y < senior x n"
    using assms less_le_trans[OF y < senior x (Suc n) senior_monotonic_Suc]
    by blast
  moreover
  have "¬ sink (token_run y n)"
    using ¬ sink (token_run y (Suc n)) token_stays_in_sink
    unfolding Suc_eq_plus1 by metis

  ultimately
  show "y  older_seniors x n"
    unfolding older_seniors.simps by blast
qed

lemma older_seniors_monotonic:
  "x  n  older_seniors x n  older_seniors x (n + m)"
  by (induction m) (simp, metis older_seniors_monotonic_Suc add_Suc_right dual_order.trans trans_le_add1)

lemma older_seniors_stable:
  "x  n  older_seniors x n = older_seniors x (n + m + m')  older_seniors x n = older_seniors x (n + m)"
  by (induction m') (simp, unfold set_eq_subset, metis dual_order.trans le_add1 older_seniors_monotonic)

lemma card_older_seniors_monotonic:
  "x  n  card (older_seniors x n)  card (older_seniors x (n + m))"
  using older_seniors_monotonic older_seniors_card_mono by meson

subsubsection ‹Pull-Up and Push-Down›

lemma pull_up_senior_older_seniors:
  "senior x n = senior y n  older_seniors x n = older_seniors y n"
  unfolding older_seniors.simps senior.simps senior_token_run by presburger

lemma pull_up_senior_older_seniors_less:
  "senior x n < senior y n  older_seniors x n  older_seniors y n"
  by force

lemma pull_up_senior_older_seniors_less_2:
  assumes "¬ sink (token_run x n)"
  assumes "senior x n < senior y n"
  shows "older_seniors x n  older_seniors y n"
proof -
  from assms have "senior x n  older_seniors y n"
    unfolding senior_same_state[of x n, symmetric] older_seniors.simps by blast
  thus ?thesis
    using older_seniors_not_self_referential pull_up_senior_older_seniors_less[OF assms(2)] by blast
qed

lemma pull_up_senior_older_seniors_le:
  "senior x n  senior y n  older_seniors x n  older_seniors y n"
  using pull_up_senior_older_seniors pull_up_senior_older_seniors_less
  unfolding dual_order.order_iff_strict by blast

lemma push_down_older_seniors_senior:
  assumes "¬ sink (token_run x n)"
  assumes "¬ sink (token_run y n)"
  assumes "older_seniors x n = older_seniors y n"
  shows "senior x n = senior y n"
  using assms by (cases "senior x n" " senior y n" rule: linorder_cases) (fast dest: pull_up_senior_older_seniors_less_2)+

subsubsection ‹Tower Lemma›

lemma older_seniors_tower'':
  assumes "x  n"
  assumes "y  n"
  assumes "¬sink (token_run x n)"
  assumes "¬sink (token_run y n)"
  assumes "older_seniors x n = older_seniors x (Suc n)"
  assumes "older_seniors y n  older_seniors x n"
  shows "older_seniors y n = older_seniors y (Suc n)"
proof
  {
    fix s
    assume "s  older_seniors y n" and "older_seniors y n  older_seniors x n"
    hence "s  older_seniors x n"
      using assms by blast
    hence "¬sink (token_run s (Suc n))" and "z. s = senior z (Suc n)"
      unfolding assms by simp+
    moreover
    have "senior y n  senior y (Suc n)"
    proof (rule ccontr)
      assume "¬senior y n  senior y (Suc n)"
      moreover
      have "senior y n  n"
        by (metis assms(2) senior_le_token le_trans)
      ultimately
      have "z. senior y n  senior z (Suc n)"
        using token_run_merge_Suc[unfolded senior_token_run[symmetric], OF y  n]
        by (metis senior_senior le_refl)
      hence "senior y n  older_seniors x (Suc n)"
        using assms by simp
      moreover
      have "senior y n  older_seniors x n"
        using assms ‹older_seniors y n  older_seniors x n older_seniors_subset_2 by meson
      ultimately
      show False
        unfolding assms ..
    qed
    hence "s < senior y (Suc n)"
      using s  older_seniors y n by fastforce
    ultimately
    have "s  older_seniors y (Suc n)"
      unfolding older_seniors.simps by blast
  }
  moreover
  {
    fix s
    assume "s  older_seniors y n" and "older_seniors y n = older_seniors x n"
    moreover
    hence "senior y n = senior x n"
      using assms(3-4) push_down_older_seniors_senior by blast
    hence "senior y (Suc n) = senior x (Suc n)"
      using token_run_merge_Suc[OF assms(2,1)] unfolding senior_token_run by blast
    ultimately
    have "s  older_seniors y (Suc n)"
      by (metis assms(5) older_seniors_senior_simp)
  }
  ultimately
  show "older_seniors y n  older_seniors y (Suc n)"
    using assms by blast
qed (metis older_seniors_monotonic_Suc assms(2))

lemma older_seniors_tower''2:
  assumes "x  n"
  assumes "y  n"
  assumes "¬sink (token_run x (n + m))"
  assumes "¬sink (token_run y (n + m))"
  assumes "older_seniors x n = older_seniors x (n + m)"
  assumes "older_seniors y n  older_seniors x n"
  shows "older_seniors y n = older_seniors y (n + m)"
  using assms
proof (induction m arbitrary: n)
  case (Suc m)
    have "¬sink (token_run x (n + m))" and "¬sink (token_run y (n + m))"
      using ¬sink (token_run x (n + Suc m)) ¬sink (token_run y (n + Suc m))
      using token_stays_in_sink[of _ _ "n + m" 1]
      unfolding Suc_eq_plus1 add.assoc[symmetric] by metis+
    moreover
    have "older_seniors x n = older_seniors x (n + m)"
      using Suc.prems(5) older_seniors_stable[OF x  n]
      unfolding Suc_eq_plus1 add.assoc by blast
    moreover
    hence "older_seniors x (n + m) = older_seniors x (Suc (n + m))"
      unfolding Suc.prems add_Suc_right ..
    ultimately
    have "older_seniors y n = older_seniors y (n + m)"
      using Suc by meson
    also
    have " = older_seniors y (Suc (n + m))"
      using older_seniors_tower''[OF _ _ ¬sink (token_run x (n + m)) ¬sink (token_run y (n + m)) ‹older_seniors x (n + m) = older_seniors x (Suc (n + m))] Suc
      by (metis ‹older_seniors x n = older_seniors x (n + m) add.commute add.left_commute calculation le_iff_add)
    finally
    show ?case
      unfolding add_Suc_right .
qed simp

lemma older_seniors_tower':
  assumes "y  older_seniors x n"
  assumes "older_seniors x n = older_seniors x (Suc n)"
  shows "older_seniors y n = older_seniors y (Suc n)"
  (is "?lhs = ?rhs")
  using assms
proof (induction "card (older_seniors x n)" arbitrary: x y)
  case 0
    hence "older_seniors x n = {}"
      using older_seniors_finite card_eq_0_iff by metis
    thus ?case
      using "0.prems" by blast
next
  case (Suc c)
    let ?os = "older_seniors x n"
    have "?os  {}"
      using Suc.prems(1) by blast

    hence "y = Max ?os  y  older_seniors (Max ?os) n"
      using Suc.prems(1) older_seniors_recursive by blast
    moreover
    have "older_seniors (Max ?os) n = older_seniors (Max ?os) (Suc n)"
      using Suc.prems(2) older_seniors_recursive ?os  {} older_seniors_not_self_referential_2
      by (metis Un_empty_left Un_insert_left insert_ident)
    moreover
    {
      fix s
      assume "s  older_seniors (Max ?os) n"
      moreover
      from Suc.hyps(2) have "card (older_seniors (Max ?os) n) = c"
        unfolding older_seniors_recursive_card[OF ?os  {}] by blast
      ultimately
      have "older_seniors s n = older_seniors s (Suc n)"
        by (metis Suc.hyps(1) ‹older_seniors (Max ?os) n = older_seniors (Max ?os) (Suc n))
    }
    ultimately
    show ?case
      by blast
qed

lemma older_seniors_tower:
  "x  n; y  older_seniors x n; older_seniors x n = older_seniors x (n + m)  older_seniors y n = older_seniors y (n + m)"
proof (induction m)
  case (Suc m)
    hence "older_seniors x n = older_seniors x (n + m)"
      using older_seniors_monotonic older_seniors_monotonic_Suc subset_antisym
      by (metis Nat.add_0_right add.assoc add_Suc_shift trans_le_add1)
    hence "older_seniors y n = older_seniors y (n + m)"
      using Suc.IH[OF Suc.prems(1,2)] by blast
    also
    have " = older_seniors y (n + Suc m)"
      using older_seniors_tower'[of y x "n + m"] Suc.prems unfolding add_Suc_right
      by (metis ‹older_seniors x n = older_seniors x (n + m))
    finally
    show ?case .
qed simp

subsection ‹Rank›

subsubsection ‹Properties›

lemma rank_None_before:
  "x > n  rank x n = None"
  by simp

lemma rank_None_Suc:
  assumes "x  n"
  assumes "rank x n = None"
  shows "rank x (Suc n) = None"
proof -
  have "sink (token_run x n)"
    using assms by (metis option.distinct(1) rank.simps)
  hence "sink (token_run x (Suc n))"
    using token_stays_in_sink by (metis (erased, hide_lams) Suc_leD le_Suc_ex not_less_eq_eq)
  thus ?thesis
    by simp
qed

lemma rank_Some_time:
  "rank x n = Some j  x  n"
  by (metis option.distinct(1) rank.simps)

lemma rank_Some_sink:
  "rank x n = Some j  ¬sink (token_run x n)"
  by fastforce

lemma rank_Some_card:
  "rank x n = Some j  card (older_seniors x n) = j"
  by (metis option.distinct(1) option.inject rank.simps)

lemma rank_initial:
  "i. rank x x = Some i"
  unfolding rank.simps sink_def by force

lemma rank_continuous:
  assumes "rank x n = Some i"
  assumes "rank x (n + m) = Some j"
  assumes "m'  m"
  shows "k. rank x (n + m') = Some k"
  using assms
proof (induction m arbitrary: j m')
  case (Suc m)
    thus ?case
    proof (cases "m' = Suc m")
      case False
        with Suc.prems have "m'  m"
          by linarith
        moreover
        obtain j' where "rank x (n + m) = Some j'"
          using Suc.prems(1,2) rank_Some_time rank_None_Suc
          by (metis add_Suc_right add_lessD1 not_less rank.simps)
        ultimately
        show ?thesis
          using Suc.IH[OF Suc.prems(1)] by blast
    qed simp
qed simp

lemma rank_token_squats:
  "token_squats x  x  n  i. rank x n = Some i"
  unfolding token_squats_def by simp

lemma rank_older_seniors_bounded:
  assumes "y  older_seniors x n"
  assumes "rank x n = Some j"
  shows "j' < j. rank y n = Some j'"
proof -
  from assms(1) have "¬sink (token_run y n)"
    by simp
  moreover
  from assms have "y  n"
    by (metis dual_order.trans linear not_less older_seniors_older option.distinct(1) rank.simps)
  moreover
  have "older_seniors y n  older_seniors x n"
    using older_seniors_subset assms(1) by presburger
  hence "card (older_seniors y n) < card (older_seniors x n)"
    by (rule older_seniors_psubset_card_mono)
  ultimately
  show ?thesis
    using rank_Some_card[OF assms(2)] rank.simps by meson
qed

subsubsection ‹Bounds›

lemma max_rank_lowerbound:
  "0 < max_rank"
proof -
  obtain a where "a  Σ"
    using nonempty_Σ by blast
  hence "range (λ_. a)  Σ" and "q0 = run δ q0 (λ_. a) 0"
    by auto
  hence "q0  reach Σ δ q0"
    unfolding reach_def by blast
  thus ?thesis
    using reach_card_0[OF nonempty_Σ] finite_reach max_rank_def sink_def by force
qed

lemma older_seniors_card_bounded:
  assumes "¬sink (token_run x n)" and "x  n"
  shows "card (older_seniors x n) < card (reach Σ δ q0 - {q. sink q})"
  (is "card ?S4 < card ?S0")
proof -
  let ?S1 = "{token_run x n | x n. True} - {q. sink q}"
  let ?S2 = "(λq. the (oldest_token q n)) ` ?S1"
  let ?S3 = "{s. x. s = senior x n  ¬(sink (token_run s n))}"

  have "?S1  ?S0"
    unfolding reach_def token_run.simps using bounded_w by fastforce
  hence "finite ?S1" and C1: "card ?S1  card ?S0"
    using finite_reach card_mono finite_subset
   apply (simp add: finite_subset) by (metis {token_run x n |x n. True} - Collect sink  reach Σ δ q0 - Collect sink› card_mono finite_Diff local.finite_reach)
  hence "finite ?S2" and C2: "card ?S2  card ?S1"
    using finite_imageI card_image_le by blast+
  moreover
  have "?S3  ?S2"
  proof
    fix s
    assume "s  ?S3"
    hence "s = senior s n" and "¬sink (token_run s n)"
      using senior_senior by fastforce+
    thus "s  ?S2"
      by auto
  qed
  ultimately
  have "finite ?S3" and C3: "card ?S3  card ?S2"
    using card_mono finite_subset by blast+
  moreover
  have "senior x n  ?S3" and "senior x n  ?S4" and "?S4  ?S3"
    using assms older_seniors_not_self_referential senior_same_state by auto
  hence "?S4  ?S3"
    by blast
  ultimately
  have "finite ?S4" and C4: "card ?S4 < card ?S3"
    using psubset_card_mono finite_subset by blast+
  show ?thesis
    using C1 C2 C3 C4 by linarith
qed

lemma rank_upper_bound:
  "rank x n = Some i  i < max_rank"
  using older_seniors_card_bounded unfolding max_rank_def
  by (fast dest: rank_Some_card rank_Some_time rank_Some_sink )

lemma rank_range:
  "i. range (rank x)  {None}  Some ` {0..<i}"
proof
  {
    fix i_option
    assume "i_option  range (rank x)"
    hence "i_option  {None}  Some ` {0..<max_rank}"
    proof (cases i_option)
      case (Some i)
        hence "i  {0..<max_rank}"
          using i_option  range (rank x) rank_upper_bound by force
        thus ?thesis
          using Some by blast
    qed blast
  }
  thus "range (rank x)  ({None}  Some ` {0..<max_rank})" ..
qed

subsubsection ‹Monotonicity›

lemma rank_monotonic:
  "rank x n = Some i; rank x (n + m) = Some j  i  j"
  using card_older_seniors_monotonic rank_Some_card rank_Some_time by metis

subsubsection ‹Pull-Up and Push-Down›

lemma pull_up_senior_rank:
  "x  n; y  n; senior x n = senior y n  rank x n = rank y n"
  by (metis senior_token_run rank.simps pull_up_senior_older_seniors)

lemma pull_up_configuration_rank:
  "x  configuration q n; y  configuration q n  rank x n = rank y n"
  by force

lemma push_down_rank_older_seniors:
  "rank x n = rank y n; rank x n = Some i  older_seniors x n = older_seniors y n"
  by (metis older_seniors_card option.distinct(2) option.sel rank.simps)

lemma push_down_rank_senior:
  "rank x n = rank y n; rank x n = Some i  senior x n = senior y n"
  by (metis push_down_rank_older_seniors push_down_older_seniors_senior option.distinct(1) rank.elims)

lemma push_down_rank_tokens:
  "rank x n = rank y n; rank x n = Some i  (q. x  configuration q n  y  configuration q n)"
  by (metis push_down_senior_tokens rank_Some_time push_down_rank_senior)

subsubsection ‹Pulled-Up Lemmas›

lemma rank_senior_senior:
  "x  n  rank (senior x n) n = rank x n"
  by (metis le_iff_add add.commute add.left_commute pull_up_senior_rank senior_le_token senior_senior)

subsubsection ‹Stable Rank›

definition stable_rank :: "nat  nat  bool"
where
  "stable_rank x i = (n. rank x n = Some i)"

lemma stable_rank_unique:
  assumes "stable_rank x i"
  assumes "stable_rank x j"
  shows "i = j"
proof -
  from assms obtain n m where "n'. n'  n  rank x n' = Some i"
    and "m'. m'  m  rank x m' = Some j"
    unfolding stable_rank_def MOST_nat_le by blast
  hence "rank x (n + m) = Some i" and "rank x (n + m) = Some j"
    by (metis add.commute le_add1)+
  thus ?thesis
    by simp
qed

lemma stable_rank_equiv_token_squats:
  "token_squats x = (i. stable_rank x i)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  define ranks where "ranks = {j | j n. rank x n = Some j}"
  hence "ranks  {0..<max_rank}" and "the (rank x x)  ranks"
    using rank_upper_bound rank_initial[of x] unfolding ranks_def by fastforce+ (* Takes roughly 10s *)
  hence "finite ranks" and "ranks  {}"
    using finite_reach finite_atLeastAtMost infinite_super by fast+

  define i where "i = Min ranks"
  obtain n where "rank x n = Some i"
    using Min_in[OF ‹finite ranks ranks  {}]
    unfolding i_def ranks_def by blast

  have "j. j  ranks  j  i"
    using Min_in[OF ‹finite ranks ranks  {}] unfolding i_def
    by (metis Min.coboundedI ‹finite ranks)
  hence "m j. rank x (n + m) = Some j  j  i"
    unfolding ranks_def by blast
  moreover
  have "m j. rank x (n + m) = Some j  j  i"
    using rank_monotonic[OF ‹rank x n = Some i] by blast
  moreover
  have "m. j. rank x (n + m) = Some j"
    using rank_token_squats[OF ?lhs] rank_Some_time[OF ‹rank x n = Some i] by simp
  ultimately
  have "m. rank x (n + m) = Some i"
    by (metis le_antisym)
  thus ?rhs
    unfolding stable_rank_def MOST_nat_le by (metis le_iff_add)
next
  assume ?rhs
  thus ?lhs
    unfolding token_squats_def stable_rank_def MOST_nat_le
    by (metis le_add2 rank_Some_sink token_stays_in_sink)
qed

lemma stable_rank_same_tokens:
  assumes "stable_rank x i"
  assumes "stable_rank y j"
  assumes "x  configuration q n"
  assumes "y  configuration q n"
  shows "i = j"
proof -
  from assms(1) obtain n_i where "n_i  n" and "t  n_i. rank x t = Some i"
    unfolding stable_rank_def MOST_nat_le by (metis linear order_trans)
  moreover
  from assms(2) obtain n_j where "n_j  n" and "t  n_j. rank y t = Some j"
    unfolding stable_rank_def MOST_nat_le by (metis linear order_trans)
  moreover
  define m where "m = max n_i n_j"
  ultimately
  have "rank x m = Some i" and "rank y m = Some j"
    by (metis max.bounded_iff order_refl)+
  moreover
  have "m  n"
    by (metis n  n_j le_trans max.cobounded2 m_def)
  have "q'. x  configuration q' m  y  configuration q' m"
    using push_down_configuration_token_run[OF assms(3,4)]
    using token_run_merge[of x n y]
    using pull_up_token_run_tokens[of x m y]
    using m  n[unfolded le_iff_add] by force
  ultimately
  show ?thesis
    using pull_up_configuration_rank by (metis option.inject)
qed

subsubsection ‹Tower Lemma›

lemma rank_tower:
  assumes "i  j"
  assumes "rank x n = Some j"
  assumes "rank x (n + m) = Some j"
  assumes "rank y n = Some i"
  shows "rank y (n + m) = Some i"
proof (cases i j rule: linorder_cases)
  case less
    {
      hence "card (older_seniors (senior y n) n) < card (older_seniors x n)"
        using assms rank_Some_card senior_same_state by force
      hence "senior y n  older_seniors x n"
        by (metis older_seniors_card_le rank_Some_sink assms(4) older_seniors_senior_simp older_seniors_subset_2)
      moreover
      have "older_seniors x n = older_seniors x (n + m)"
        by (metis assms(2,3) rank_Some_card rank_Some_time card_subset_eq[OF older_seniors_finite] older_seniors_monotonic)
      ultimately
      have "older_seniors (senior y n) n = older_seniors (senior y n) (n + m)" and "senior y n  older_seniors x (n + m)"
        using older_seniors_tower rank_Some_time assms(2) by blast+
    }
    moreover
    have "rank (senior y n) n = Some i"
      by (metis assms(4) rank_Some_time rank_senior_senior)
    ultimately
    have "rank (senior y n) (n + m) = Some i"
      by (metis rank_older_seniors_bounded[OF _ assms(3)] rank_Some_card)
    moreover
    have "senior y n  n"
      by (metis ‹rank (senior y n) n = Some i rank_Some_time)
    hence "senior y n  configuration (token_run y (n + m)) (n + m)"
      by (metis (full_types) token_run_merge[OF _ rank_Some_time[OF assms(4)] senior_same_state] configuration_token trans_le_add1)
    ultimately
    show ?thesis
      by (metis pull_up_configuration_rank le_iff_add add.assoc assms(4) configuration_token rank_Some_time)
next
  case equal
    hence "x  n" and "y  n" and "token_run x n = token_run y n"
      using assms(2-4) push_down_rank_tokens by force+
    moreover
    hence "token_run x (n + m) = token_run y (n + m)"
      using token_run_merge by blast
    ultimately
    show ?thesis
      by (metis assms(3) equal rank_senior_senior senior_token_run le_iff_add add.assoc)
qed (insert i  j, linarith)

lemma stable_rank_alt_def:
  "rank x n = Some j  stable_rank x j  (m  n. rank x m = Some j)"
  (is "?rhs  ?lhs")
proof
  assume ?rhs
  then obtain m' where "m  m'. rank x m = Some j"
    unfolding stable_rank_def MOST_nat_le by blast
  moreover
  hence "rank x n = Some j" and "rank x m' = Some j"
    using ?rhs by blast+
  {
    fix m
    assume "n  n + m" and "n + m < m'"
    then obtain j' where "rank x (n + m) = Some j'"
      by (metis ?rhs stable_rank_equiv_token_squats rank_Some_time rank_token_squats trans_le_add1)
    moreover
    hence "j'  j"
      using ‹rank x n = Some j rank_monotonic by blast
    moreover
    have "j  j'"
      using ‹rank x (n + m) = Some j' ‹rank x m' = Some j  n + m < m' rank_monotonic
      by (metis add_Suc_right less_imp_Suc_add)
    ultimately
    have "rank x (n + m) = Some j"
      by simp
  }
  ultimately
  show ?lhs
    by (metis le_add_diff_inverse not_le)
qed (unfold stable_rank_def MOST_nat_le, blast)

lemma stable_rank_tower:
  assumes "j  i"
  assumes "rank x n = Some j"
  assumes "rank y n = Some i"
  assumes "stable_rank y i"
  shows "stable_rank x j"
  using assms rank_tower[OF j  i] stable_rank_alt_def[of y n i]
  unfolding stable_rank_def[of x j, unfolded MOST_nat_le] by (metis le_Suc_ex)

subsection ‹Senior States›

lemma senior_states_initial:
  "senior_states q 0 = {}"
  by simp

lemma senior_states_cases_subseteq [case_names le ge]:
  assumes "senior_states p n  senior_states q n  P"
  assumes "senior_states p n  senior_states q n  P"
  shows "P" using assms by force

lemma senior_states_cases_subset [case_names less equal greater]:
  assumes "senior_states p n  senior_states q n  P"
  assumes "senior_states p n = senior_states q n  P"
  assumes "senior_states p n  senior_states q n  P"
  shows "P" using assms senior_states_cases_subseteq by blast

lemma senior_states_finite:
  "finite (senior_states q n)"
  by fastforce

lemmas senior_states_card_mono = card_mono[OF senior_states_finite]
lemmas senior_states_psubset_card_mono = psubset_card_mono[OF senior_states_finite]

lemma senior_states_card:
  "card (senior_states p n) = card (senior_states q n)  senior_states p n = senior_states q n"
  by (metis less_not_refl senior_states_cases_subset senior_states_psubset_card_mono)

lemma senior_states_card_le:
  "card (senior_states p n) < card (senior_states q n)  senior_states p n  senior_states q n"
  by (metis card_mono not_less senior_states_cases_subseteq senior_states_finite senior_states_psubset_card_mono subset_not_subset_eq)

lemma senior_states_card_less:
  "card (senior_states p n)  card (senior_states q n)  senior_states p n  senior_states q n"
  by (metis card_mono card_seteq senior_states_cases_subseteq senior_states_finite)

lemma senior_states_older_seniors:
  "(λy. token_run y n) ` older_seniors x n = senior_states (token_run x n) n"
  (is "?lhs = ?rhs")
proof -
  have "?lhs = {q'. ost ot. q' = token_run ost n  ost = senior ot n  ost < senior x n  ¬ sink q'}"
    by auto
  also
  have " = {q'. t ot. oldest_token q' n = Some t  t = senior ot n  t < senior x n  ¬ sink q'}"
    unfolding senior.simps by (metis (erased, hide_lams) oldest_token_always_def push_down_oldest_token_token_run option.sel)
  also
  have " = {q'. t. oldest_token q' n = Some t  t < senior x n  ¬ sink q'}"
    by auto
  also
  have " = ?rhs"
    unfolding senior_states.simps senior.simps by (metis (erased, hide_lams) oldest_token_always_def option.sel)
  finally
  show "?lhs = ?rhs"
    .
qed

lemma card_older_senior_senior_states:
  assumes "x  configuration q n"
  shows "card (older_seniors x n) = card (senior_states q n)"
  (is "?lhs = ?rhs")
proof -
  have "inj_on (λt. token_run t n) (older_seniors x n)"
    unfolding inj_on_def using senior_same_state
    by (fastforce simp del: token_run.simps)
  moreover
  have "token_run x n = q"
    using assms by simp
  ultimately
  show "?lhs = ?rhs"
    using card_image[of "(λt. token_run t n)" "older_seniors x n"]
    unfolding senior_states_older_seniors by presburger
qed

subsection ‹Rank of States›

subsubsection ‹Alternative Definitions›

lemma state_rank_eq_rank:
  "state_rank q n = (case oldest_token q n of None  None | Some t  rank t n) "
  (is "?lhs = ?rhs")
proof (cases "oldest_token q n")
  case (None)
    thus ?thesis
      by (metis not_Some_eq oldest_token.elims option.simps(4) state_rank.elims)
next
  case (Some x)
    hence "?lhs = (if ¬sink q then Some (card (older_seniors x n)) else None)"
      by (metis emptyE push_down_oldest_token_configuration[OF Some] card_older_senior_senior_states state_rank.simps)
    also
    have " = rank x n"
      using oldest_token_bounded[OF Some] push_down_oldest_token_token_run[OF Some] by auto
    also
    have " = ?rhs"
      using Some by force
    finally
    show ?thesis .
qed

lemma state_rank_eq_rank_SOME:
  "state_rank q n = (if configuration q n  {} then rank (SOME x. x  configuration q n) n else None)"
proof (cases "oldest_token q n")
  case (Some x)
    thus ?thesis
      unfolding state_rank_eq_rank Some option.simps(5)
      by (metis Some ex_in_conv pull_up_configuration_rank push_down_oldest_token_configuration someI_ex)
qed (unfold state_rank_eq_rank; metis not_Some_eq oldest_token.elims option.simps(4))

lemma rank_eq_state_rank:
  "x  n  rank x n = state_rank (token_run x n) n"
  unfolding state_rank_eq_rank_SOME[of "token_run x n"]
  by (metis all_not_in_conv configuration_token pull_up_configuration_rank someI_ex)

subsubsection ‹Pull-Up and Push-Down›

lemma pull_up_configuration_state_rank:
  "configuration q n = {}  state_rank q n = None"
  by force

lemma push_down_state_rank_tokens:
  "state_rank q n = Some i  configuration q n  {}"
  by (metis not_Some_eq state_rank.elims)

lemma push_down_state_rank_configuration_None:
  "state_rank q n = None  ¬sink q  configuration q n = {}"
  unfolding state_rank.simps by (metis option.distinct(1))

lemma push_down_state_rank_oldest_token:
  "state_rank q n = Some i  x. oldest_token q n = Some x"
  by (metis oldest_token.elims state_rank.elims)

lemma push_down_state_rank_token_run:
  "state_rank q n = Some i  x. token_run x n = q  x  n"
  by (blast dest: push_down_state_rank_oldest_token push_down_oldest_token_token_run oldest_token_bounded)

subsubsection ‹Properties›

lemma state_rank_distinct:
  assumes distinct: "p  q"
  assumes ranked_1: "state_rank p n = Some i"
  assumes ranked_2: "state_rank q n = Some j"
  shows "i  j"
proof
  assume "i = j"
  obtain x y where "x  configuration p n" and "y  configuration q n"
    using assms push_down_state_rank_tokens by blast
  hence "rank x n = Some i" and "rank y n = Some j"
    using assms pull_up_configuration_rank unfolding state_rank_eq_rank_SOME
    by (metis all_not_in_conv someI_ex)+
  hence "x  configuration q n"
    using y  configuration q n push_down_rank_tokens
    unfolding i = j by auto
  hence "p = q"
    using x  configuration p n by fastforce
  thus "False"
    using distinct by blast
qed

lemma state_rank_initial_state:
  obtains i where "state_rank q0 n = Some i"
  unfolding state_rank.simps sink_def by fastforce

lemma state_rank_sink:
  "sink q  state_rank q n = None"
  by simp

lemma state_rank_upper_bound:
  "state_rank q n = Some i  i < max_rank"
  by (metis option.simps(5) rank_upper_bound push_down_state_rank_oldest_token state_rank_eq_rank)

lemma state_rank_range:
  "state_rank q n  {None}  Some ` {0..<max_rank}"
  by (cases "state_rank q n") (simp add: state_rank_upper_bound[of q n])+

lemma state_rank_None:
  "¬sink q  state_rank q n = None  oldest_token q n = None"
  by simp

lemma state_rank_Some:
  "¬sink q  (i. state_rank q n = Some i)  (j. oldest_token q n = Some j)"
  by simp

lemma state_rank_oldest_token:
  assumes "state_rank p n = Some i"
  assumes "state_rank q n = Some j"
  assumes "oldest_token p n = Some x"
  assumes "oldest_token q n = Some y"
  shows "i < j  x < y"
proof -
  have "configuration p n  {}" and "configuration q n  {}"
    using assms(3,4) by (metis oldest_token.simps option.distinct(1))+
  moreover
  have "¬sink p" and "¬sink q"
    using assms(1,2) state_rank_sink by auto
  ultimately
  have i_def: "i = card (senior_states p n)" and j_def: "j = card (senior_states q n)"
    using assms(1,2) option.sel by simp_all
  hence "i < j  senior_states p n  senior_states q n"
    using senior_states_card_le by presburger
  also
  with assms(3,4) have "  x < y"
  proof (cases rule: senior_states_cases_subset[of p n q])
    case equal
      thus ?thesis
        using assms state_rank_distinct i_def j_def
        by (metis less_irrefl option.sel)
  qed auto
  ultimately
  show ?thesis
    by meson
qed

lemma state_rank_oldest_token_le:
  assumes "state_rank p n = Some i"
  assumes "state_rank q n = Some j"
  assumes "oldest_token p n = Some x"
  assumes "oldest_token q n = Some y"
  shows "i  j  x  y"
  using state_rank_oldest_token[OF assms] assms state_rank_distinct oldest_token_equal
  by (cases "x = y") ((metis option.sel order_refl), (metis le_eq_less_or_eq option.inject))

lemma state_rank_in_function_set:
  shows "(λq. state_rank q t)  {f. (x. x  reach Σ δ q0  f x = None) 
      (x. x  reach Σ δ q0  f x  {None}  Some ` {0..<max_rank})}"
proof -
  {
    fix x
    assume "x  reach Σ δ q0"
    hence "token. x  token_run token t"
      unfolding reach_def token_run.simps using bounded_w by fastforce
    hence "state_rank x t = None"
      using pull_up_configuration_state_rank by auto
  }
  with state_rank_range show ?thesis
    by blast
qed

subsection ‹Step Function›

fun pre_oldest_tokens :: "'b  nat  nat set"
where
  "pre_oldest_tokens q n = {x. q'. oldest_token q' n = Some x  q = δ q' (w n)}  (if q = q0 then {Suc n} else {})"

lemma pre_oldest_configuration_range:
  "pre_oldest_tokens q n  {0..Suc n}"
proof -
  have "{x. q'. oldest_token q' n = Some x  q = δ q' (w n)}  {0..n}"
    (is "?lhs  ?rhs")
  proof
    fix x
    assume "x  ?lhs"
    then obtain q' where "oldest_token q' n = Some x"
      by blast
    thus "x  ?rhs"
      unfolding atLeastAtMost_iff using oldest_token_bounded[of q' n x] by blast
  qed
  thus ?thesis
    by (cases "q = q0") fastforce+
qed

lemma pre_oldest_configuration_finite:
  "finite (pre_oldest_tokens q n)"
  using pre_oldest_configuration_range finite_atLeastAtMost by (rule finite_subset)

lemmas pre_oldest_configuration_Min_in = Min_in[OF pre_oldest_configuration_finite]

lemma pre_oldest_configuration_obtain:
  assumes "x  pre_oldest_tokens q n - {Suc n}"
  obtains q' where "oldest_token q' n = Some x" and "q = δ q' (w n)"
  using assms by (cases "q = q0", auto)

lemma pre_oldest_configuration_element:
  assumes "oldest_token q' n = Some ot"
  assumes "q = δ q' (w n)"
  shows "ot  pre_oldest_tokens q n"
proof
  show "ot  {ot. q'. oldest_token q' n = Some ot  q = δ q' (w n)}"
    (is "_  ?A")
    using assms by blast
  show "?A  pre_oldest_tokens q n"
    by simp
qed

lemma pre_oldest_configuration_initial_state:
  "Suc n  pre_oldest_tokens q n  q = q0"
  using oldest_token_bounded[of _ n "Suc n"]
  by (cases "q = q0") auto

lemma pre_oldest_configuration_initial_state_2:
  "q = q0  Suc n  pre_oldest_tokens q n"
  by fastforce

lemma pre_oldest_configuration_tokens:
  "pre_oldest_tokens q n  {}  configuration q (Suc n)  {}"
  (is "?lhs  ?rhs")
proof
  assume ?lhs
  then obtain ot where ot_def: "ot  pre_oldest_tokens q n"
    by blast
  thus ?rhs
  proof (cases "ot = Suc n")
    case True
      thus ?thesis
    using pre_oldest_configuration_initial_state configuration_non_empty[of "Suc n" "Suc n"] ot  pre_oldest_tokens q n unfolding token_run_intial_state  by blast
  next
    case False
      then obtain q' where "oldest_token q' n = Some ot" and "q = δ q' (w n)"
        using ot_def pre_oldest_configuration_obtain by blast
      moreover
      hence "configuration q' n  {}"
        by (metis oldest_token.simps option.distinct(2))
      ultimately
      show ?rhs
        by (elim configuration_step_non_empty)
  qed
next
  assume ?rhs
  then obtain token where "token  configuration q (Suc n)" and "token  Suc n" and "token_run token (Suc n) = q"
    by auto
  moreover
  {
    assume "token  n"
    then obtain q' where "token_run token n = q'" and "q = δ q' (w n)"
      using ‹token_run token (Suc n) = q unfolding token_run.simps Suc_diff_le[OF token  n] by fastforce
    then obtain ot where "oldest_token q' n = Some ot"
      using oldest_token_always_def by blast
    with q = δ q' (w n) have ?lhs
      using pre_oldest_configuration_element by blast
  }
  ultimately
  show ?lhs
    using pre_oldest_configuration_initial_state_2 by fastforce
qed

lemma oldest_token_rec:
  "oldest_token q (Suc n) = (if pre_oldest_tokens q n  {} then Some (Min (pre_oldest_tokens q n)) else None)"
proof (cases "oldest_token q (Suc n)")
  case (Some ot)
    moreover
    hence "ot  configuration q (Suc n)"
      by (rule push_down_oldest_token_configuration)
    hence "configuration q (Suc n)  {}"
      by blast
    hence "pre_oldest_tokens q n  {}"
      unfolding pre_oldest_configuration_tokens .
    let ?ot = "Min (pre_oldest_tokens q n)"
    {
      {
        {
          assume "ot < Suc n"
          hence "ot  Suc n"
            by blast
          then obtain q' where "ot  configuration q' n" and "q = δ q' (w n)"
            using configuration_rev_step' ot  configuration q (Suc n) by metis
          {
            fix token
            assume "token  configuration q' n"
            hence "token  configuration q (Suc n)"
              using q = δ q' (w n) by (rule configuration_step)
            hence "ot  token"
              using Some by (metis Min.coboundedI ‹configuration q (Suc n)  {} configuration_finite oldest_token.simps option.inject)
          }
          hence "Min (configuration q' n) = ot"
            by (metis Min_eqI ot  configuration q' n configuration_finite)
          hence "oldest_token q' n = Some ot"
            using ot  configuration q' n unfolding oldest_token.simps by auto
          hence "ot  pre_oldest_tokens q n"
            using q = δ q' (w n) by (rule pre_oldest_configuration_element)
        }
        moreover
        {
          assume "ot = Suc n"
          moreover
          hence "q = q0"
            using Some by (metis push_down_oldest_token_token_run token_run_intial_state)
          ultimately
          have "ot  pre_oldest_tokens q n"
            by simp
        }
        ultimately
        have "ot  pre_oldest_tokens q n"
          using Some[THEN oldest_token_bounded] by linarith
      }
      moreover
      {
        fix ot' q'
        assume "oldest_token q' n = Some ot'" and "q = δ q' (w n)"
        moreover
        hence "ot'  configuration q (Suc n)"
          using push_down_oldest_token_configuration configuration_step by blast
        hence "ot  ot'"
          using Some by (metis Min.coboundedI ‹configuration q (Suc n)  {} configuration_finite oldest_token.simps option.inject)
      }
      hence "y. y  pre_oldest_tokens q n - {Suc n}  ot  y"
        using pre_oldest_configuration_obtain by metis
      hence "y. y  pre_oldest_tokens q n  ot  y"
        using Some[THEN oldest_token_bounded] by force
      ultimately
      have "?ot = ot"
        using Min_eqI[OF pre_oldest_configuration_finite, of q n ot] by fast
    }
    ultimately
    show ?thesis
      unfolding pre_oldest_configuration_tokens oldest_token.simps
      by (metis ‹configuration q (Suc n)  {})
qed (unfold pre_oldest_configuration_tokens oldest_token.simps, metis option.distinct(2))

lemma pre_ranks_range:
  "pre_ranks (λq. state_rank q n) ν q   {0..max_rank}"
proof -
  have "{i | q' i. state_rank q' n = Some i  q = δ q' ν}  {0..max_rank}"
    using state_rank_upper_bound by fastforce
  thus ?thesis
    by auto
qed

lemma pre_ranks_finite:
  "finite (pre_ranks (λq. state_rank q n) ν q)"
  using pre_ranks_range finite_atLeastAtMost by (rule finite_subset)

lemmas pre_ranks_Min_in = Min_in[OF pre_ranks_finite]

lemma pre_ranks_state_obtain:
  assumes "rq  pre_ranks r ν q - {max_rank}"
  obtains q' where "r q' = Some rq" and "q = δ q' ν"
  using assms by (cases "q = q0", auto)

lemma pre_ranks_element:
  assumes "state_rank q' n = Some r"
  assumes "q = δ q' (w n)"
  shows "r  pre_ranks (λq. state_rank q n) (w n) q"
proof
  show "r  {i. q'. (λq. state_rank q n) q' = Some i  q = δ q' (w n)}"
    (is "_  ?A")
    using assms by blast
  show "?A  pre_ranks (λq. state_rank q n) (w n) q"
    by simp
qed

lemma pre_ranks_initial_state:
  "max_rank  pre_ranks (λq. state_rank q n) ν q  q = q0"
  using state_rank_upper_bound by (cases "q = q0") auto

lemma pre_ranks_initial_state_2:
  "q = q0  max_rank  pre_ranks r ν q"
  by fastforce

lemma pre_ranks_tokens:
  assumes "¬sink q"
  shows "pre_ranks (λq. state_rank q n) (w n) q  {}  configuration q (Suc n)  {}"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  thus ?rhs
  proof (cases "q  q0")
    case True
      hence "{i. q'. state_rank q' n = Some i  q = δ q' (w n)}  {}"
        using ?lhs by simp
      then obtain q' where "state_rank q' n  None" and "q = δ q' (w n)"
        by blast
      moreover
      hence "configuration q' n  {}"
        unfolding state_rank.simps by meson
      ultimately
      show ?rhs
        by (elim configuration_step_non_empty)
  qed auto
next
  assume ?rhs
  then obtain token where "token  configuration q (Suc n)" and "token  Suc n" and "token_run token (Suc n) = q"
    by auto
  moreover
  {
    assume "token  n"
    then obtain q' where "token_run token n = q'" and "q = δ q' (w n)"
      using ‹token_run token (Suc n) = q unfolding token_run.simps Suc_diff_le[OF token  n] by fastforce
    hence "¬sink q'"
      using ¬sink q sink_rev_step bounded_w by blast
    then obtain r where "state_rank q' n = Some r"
      using ¬sink q configuration_non_empty[OF token  n] unfolding ‹token_run token n = q' by simp
    with q = δ q' (w n) have ?lhs
      using pre_ranks_element by blast
  }
  ultimately
  show ?lhs
    by fastforce
qed

lemma pre_ranks_pre_oldest_token_Min_state_special:
  assumes "¬sink q"
  assumes "configuration q (Suc n)  {}"
  shows "Min (pre_ranks (λq. state_rank q n) (w n) q) = max_rank  Min (pre_oldest_tokens q n) = Suc n"
  (is "?lhs  ?rhs")
proof
  from assms have "pre_oldest_tokens q n  {}"
    and "pre_ranks  (λq. state_rank q n) (w n) q  {}"
    using pre_ranks_tokens pre_oldest_configuration_tokens by simp_all

  {
    assume ?lhs
    have "q = q0"
      apply (rule ccontr)
      using state_rank_upper_bound pre_ranks_Min_in[OF ‹pre_ranks (λq. state_rank q n) (w n) q  {}] ?lhs
      by auto
    moreover
    {
      fix q'
      assume "q = δ q' (w n)"
      hence "¬sink q'"
        using ¬sink q bounded_w unfolding sink_def
        using calculation by blast
      {
        fix i
        assume "state_rank q' n = Some i"
        hence "False"
          using q = δ q' (w n)
        using Min.coboundedI[OF pre_ranks_finite, of _ n "(w n)" q]
        unfolding ?lhs using state_rank_upper_bound[of q' n] by fastforce
      }
      hence "state_rank q' n = None"
        by fastforce
      hence "oldest_token q' n = None"
        using ¬sink q' by (metis state_rank_None)
    }
    hence "{ot. q'. oldest_token q' n = Some ot  q = δ q' (w n)} = {}"
      by fastforce
    ultimately
    show "?rhs"
      by auto
  }

  {
    assume ?rhs
    {
      fix q'
      assume "q = δ q' (w n)"
      have "state_rank q' n = None"
      proof (cases "oldest_token q' n")
        case (Some t)
          hence "t  n"
            using oldest_token_bounded[of q' n] by blast
          moreover
          have "Suc n  t"
            using q = δ q' (w n)
            using Min.coboundedI[OF pre_oldest_configuration_finite, of _ q n]
            unfolding ?rhs using ‹oldest_token q' n = Some t by auto
          ultimately
          have "False"
            by linarith
          thus ?thesis
            ..
      qed (unfold state_rank_eq_rank, auto)
    }
    hence X: "{i. q'.  (λq. state_rank q n) q' = Some i  q = δ q' (w n)} = {}"
      by fastforce

    have "q = q0"
      apply (rule ccontr)
      using ‹pre_ranks (λq. state_rank q n) (w n) q  {}
      unfolding pre_ranks.simps X by simp
    hence "pre_ranks (λq. state_rank q n) (w n) q = {max_rank}"
      unfolding pre_ranks.simps X by force
    thus ?lhs
      by fastforce
  }
qed

lemma pre_ranks_pre_oldest_token_Min_state:
  assumes "¬sink q"
  assumes "q = δ q' (w n)"
  assumes "configuration q (Suc n)  {}"
  defines "min_r  Min (pre_ranks (λq. state_rank q n) (w n) q)"
  defines "min_ot  Min (pre_oldest_tokens q n)"
  shows "state_rank q' n = Some min_r  oldest_token q' n = Some min_ot"
  (is "?lhs  ?rhs")
proof
  from assms have "pre_oldest_tokens q n  {}" and "¬sink q'"
    and "pre_ranks (λq. state_rank q n) (w n) q  {}"
    using pre_ranks_tokens pre_oldest_configuration_tokens bounded_w unfolding sink_def
    by (simp_all, metis rangeI subset_iff)

  {
    assume ?lhs
    thus ?rhs
    proof (cases min_r max_rank rule: linorder_cases)
      case less
        then obtain ot where "oldest_token q' n = Some ot"
           by (metis push_down_state_rank_oldest_token ?lhs)
        moreover
        {
          {
            fix q'' ot''
            assume "q = δ q'' (w n)"
            assume "oldest_token q'' n = Some ot''"
            moreover
            have "¬sink q''"
              using q = δ q'' (w n) assms unfolding sink_def
              by (metis rangeI subset_eq bounded_w)
            then obtain r'' where "state_rank q'' n = Some r''"
              using ‹oldest_token q'' n = Some ot'' by (metis state_rank_Some)
            moreover
            hence "r''  pre_ranks (λq. state_rank q n) (w n) q" (* Move to special lemma *)
              using q = δ q'' (w n) unfolding pre_ranks.simps by blast
            then have "min_r  r''"
              unfolding min_r_def by (metis Min.coboundedI pre_ranks_finite)
            ultimately
            have "ot  ot''"
              using state_rank_oldest_token_le[OF ?lhs _ ‹oldest_token q' n = Some ot] by blast
          }
          hence "x. x  {ot. q'. oldest_token q' n = Some ot  q = δ q' (w n)}  ot  x"
            by blast
          moreover
          have "ot  Suc n"
            using oldest_token_bounded[OF ‹oldest_token q' n = Some ot] by simp
          ultimately
          have "x. x  pre_oldest_tokens q n  ot  x"
            unfolding pre_oldest_tokens.simps apply (cases "q0 = q") apply auto done
          hence "ot  min_ot"
            unfolding min_ot_def
            unfolding Min_ge_iff[OF pre_oldest_configuration_finite ‹pre_oldest_tokens q n  {}, of ot]
             by simp
        }
        moreover
        have "ot  min_ot"
          using Min.coboundedI[OF pre_oldest_configuration_finite] pre_oldest_configuration_element
          unfolding min_ot_def by (metis assms(2) calculation(1))
        ultimately
        show ?thesis
          by simp
    qed (insert not_less, blast intro: state_rank_upper_bound less_imp_le_nat)+
  }

  {
    assume ?rhs
    thus ?lhs
    proof (cases min_ot "Suc n" rule: linorder_cases)
      case less
        then obtain r where "state_rank q' n = Some r"
          using ?rhs ¬sink q' by (metis state_rank_Some)
        moreover
        {
          {
            fix r''
            assume "r''  pre_ranks (λq. state_rank q n) (w n) q - {max_rank}"
            then obtain q'' where "state_rank q'' n = Some r''"
              and "q = δ q'' (w n)"
              using pre_ranks_state_obtain by blast
            moreover
            then obtain ot'' where "oldest_token q'' n = Some ot''"
               using push_down_state_rank_oldest_token by fastforce
            moreover
            hence "min_ot  ot''"
              using q = δ q'' (w n) pre_oldest_configuration_element Min.coboundedI pre_oldest_configuration_finite
              unfolding min_ot_def by metis
            ultimately
            have "r  r''"
              using state_rank_oldest_token_le[OF ‹state_rank q' n = Some r _ ?rhs] by blast
          }
          moreover
          have "r  max_rank"
            using state_rank_upper_bound[OF ‹state_rank q' n = Some r] by linarith
          ultimately
          have "x. x   pre_ranks (λq. state_rank q n) (w n) q  r  x"
            unfolding pre_ranks.simps apply (cases "q0 = q") apply auto done
          hence "r  min_r"
            unfolding min_r_def Min_ge_iff[OF pre_ranks_finite ‹pre_ranks (λq. state_rank q n) (w n) q  {}]
            by simp
        }
        moreover
        have "r  min_r"
          using Min.coboundedI[OF pre_ranks_finite] pre_ranks_element
          unfolding min_r_def by (metis assms(2) calculation(1))
        ultimately
        show ?thesis
          by simp
    qed (insert not_less, blast intro: oldest_token_bounded Suc_lessD)+
  }
qed

lemma Min_pre_ranks_pre_oldest_tokens:
  fixes n
  defines "r  (λq. state_rank q n)"
  assumes "configuration p (Suc n)  {}"
      and "configuration q (Suc n)  {}"
  assumes "¬sink q"
      and "¬sink p"
  shows "Min (pre_ranks r (w n) p) < Min (pre_ranks r (w n) q)  Min (pre_oldest_tokens p n) < Min (pre_oldest_tokens q n)"
  (is "?lhs  ?rhs")
proof
  have pre_ranks_Min: "x ν. (x < Min (pre_ranks r (w n) q)) = (a  pre_ranks r (w n) q. x < a)"
    using assms pre_ranks_finite Min.bounded_iff pre_ranks_tokens by simp
  have pre_oldest_configuration_Min: "x. (x < Min (pre_oldest_tokens q n)) = (apre_oldest_tokens q n. x < a)"
    using assms pre_oldest_configuration_finite Min.bounded_iff pre_oldest_configuration_tokens by simp
  have "x. w x  Σ"
    using bounded_w by auto

  {
    let ?min_i = "Min (pre_ranks r (w n) p)"
    let ?min_j = "Min (pre_ranks r (w n) q)"

    assume ?lhs

    have "?min_i  pre_ranks r (w n) p" and "?min_j  pre_ranks r (w n) q"
      using Min_in[OF pre_ranks_finite] assms pre_ranks_tokens by presburger+
    hence "?min_i  max_rank" and "?min_j  max_rank"
      using pre_ranks_range atLeastAtMost_iff unfolding r_def by blast+
    with ?lhs have "?min_i  max_rank"
      by linarith
    then obtain p' i' where "i' = ?min_i" and "r p' = Some i'" and "p = δ p' (w n)"
      using ?min_i  pre_ranks r (w n) p apply (cases "p = q0") apply auto[1] by fastforce
    then obtain ot' where "oldest_token p' n = Some ot'"
      unfolding assms by (metis push_down_state_rank_oldest_token)
    have "state_rank p' n = Some ?min_i"
      using i' = ?min_i r p' = Some i' unfolding assms by simp
    hence "ot' = Min (pre_oldest_tokens p n)"
      using pre_ranks_pre_oldest_token_Min_state[OF ¬sink p p = δ p' (w n) ‹configuration p (Suc n)  {}] ‹oldest_token p' n = Some ot'
      unfolding r_def by (metis option.inject)
    moreover
    have "ot' < Suc n"
    proof (cases ot' "Suc n" rule: linorder_cases)
      case equal
        hence "?min_i = max_rank"
          using pre_ranks_pre_oldest_token_Min_state_special[of p n, OF ¬sink p ‹configuration p (Suc n)  {}] assms
          unfolding ot' = Min (pre_oldest_tokens p n) by simp
        thus ?thesis
          using ?min_i  max_rank› by simp
    next
      case greater
        moreover
        have "ot'  {0..Suc n}"
          using ‹oldest_token p' n = Some ot'[THEN oldest_token_bounded] by fastforce
        ultimately
        show ?thesis
          by simp
    qed simp
    moreover
    {
      fix otq
      assume "otq  pre_oldest_tokens q n - {Suc n}"
      then obtain q' where "oldest_token q' n = Some otq" and "q = δ q' (w n)"
        using pre_oldest_configuration_obtain by blast
      moreover
      hence "¬sink q'"
        using ¬sink q x. w x  Σ unfolding sink_def by auto
      then obtain rq where "state_rank q' n = Some rq"
        unfolding assms state_rank.simps using ‹oldest_token q' n = Some otq
        by (metis oldest_token.simps option.distinct(2))
      moreover
      hence "rq  pre_ranks r (w n) q"
        using q = δ q' (w n)
        unfolding pre_ranks.simps assms by blast
      hence "?min_j  rq"
        using Min.coboundedI[OF pre_ranks_finite] unfolding assms by blast
      hence "?min_i < rq"
        using ?lhs by linarith
      hence "ot' < otq"
        using state_rank_oldest_token[OF ‹state_rank p' n = Some ?min_i ‹state_rank q' n = Some rq ‹oldest_token p' n = Some ot' ‹oldest_token q' n = Some otq]
        unfolding assms by simp
    }
    ultimately
    show ?rhs
      using pre_oldest_configuration_Min by blast
  }

  {
    define ot_p where "ot_p = Min (pre_oldest_tokens p n)"
    define ot_q where "ot_q = Min (pre_oldest_tokens q n)"
    assume ?rhs
    hence "ot_p < ot_q"
      unfolding ot_p_def ot_q_def .

    have "oldest_token p (Suc n) = Some ot_p" and "oldest_token q (Suc n) = Some ot_q"
      unfolding ot_p_def ot_q_def oldest_token_rec pre_oldest_configuration_tokens by (metis assms)+

   (* Min oldest ⟷ Min rank *)
    define min_rp where "min_rp = Min (pre_ranks r (w n) p)"
    hence "min_rp  pre_ranks r (w n) p"
      using pre_ranks_Min_in assms pre_ranks_tokens by simp
    hence *: "min_rp < max_rank"
    proof (cases min_rp max_rank rule: linorder_cases)
      case equal
        hence "ot_p = Suc n"
          using pre_ranks_pre_oldest_token_Min_state_special[of p n, OF _ ‹configuration p (Suc n)  {}] assms
          unfolding ot_p_def min_rp_def by simp
        moreover
        have "Min (pre_oldest_tokens q n)  pre_oldest_tokens q n"
          using Min_in[OF pre_oldest_configuration_finite ] assms pre_oldest_configuration_tokens by presburger
        hence "ot_q  {0..Suc n}"
          using pre_oldest_configuration_range[of q n]
          unfolding ot_q_def by blast
        hence "ot_q  Suc n"
          by simp
        ultimately
        show ?thesis
          using ot_p < ot_q by simp
    next
      case greater
        moreover
        have "min_rp  {0..max_rank}"
          using pre_ranks_range min_rp  pre_ranks r (w n) p
          unfolding r_def ..
        ultimately
        show ?thesis
          by simp
    qed simp
    moreover
    from * have "min_rp  pre_ranks r (w n) p - {max_rank}"
      using min_rp  pre_ranks r (w n) p by simp
    then obtain p' where "r p' = Some min_rp" and "p = δ p' (w n)"
      using pre_ranks_state_obtain by blast
    hence "oldest_token p' n = Some ot_p"
      using pre_ranks_pre_oldest_token_Min_state[OF ¬sink p p = δ p' (w n) ‹configuration p (Suc n)  {}]
      unfolding r_def[symmetric] min_rp_def[symmetric] ot_p_def[symmetric] by (metis r_def)
    {
      fix rq
      assume "rq  pre_ranks r (w n) q - {max_rank}"
      then obtain q' where q': "r q' = Some rq" "q = δ q' (w n)"
        using pre_ranks_state_obtain by blast
      moreover
      from q' obtain ot_q' where ot_q': "oldest_token q' n = Some ot_q'"
        unfolding assms by (metis push_down_state_rank_oldest_token)
      moreover
      from ot_q' have "ot_q'  pre_oldest_tokens q n"
        using q = δ q' (w n)
        unfolding pre_oldest_tokens.simps by blast
      hence "ot_q  ot_q'"
        unfolding ot_q_def
        by (rule Min.coboundedI[OF pre_oldest_configuration_finite])
      hence "ot_p < ot_q'"
        using ot_p < ot_q by linarith
      ultimately
      have "min_rp < rq"
        using state_rank_oldest_token r p' = Some min_rp ‹oldest_token p' n = Some ot_p
        unfolding assms by blast
    }
    ultimately
    show ?lhs
      using pre_ranks_Min unfolding min_rp_def by blast
  }
qed

subsubsection ‹Definition of initial and step›

lemma state_rank_initial:
  "state_rank q 0 = initial q"
  using state_rank_initial_state by force

lemma state_rank_step:
  "state_rank q (Suc n) = step (λq. state_rank q n) (w n) q"
  (is "?lhs = ?rhs")
proof (cases "sink q")
  case False
    {
      assume "configuration q (Suc n) = {}"
      hence ?thesis
        using False pull_up_configuration_state_rank pre_ranks_tokens
        unfolding step.simps by presburger
    }
    moreover
    {
      assume "configuration q (Suc n)  {}"
      hence "?lhs = Some (card (senior_states q (Suc n)))"
        using False unfolding state_rank.simps by presburger
      also
      have " = ?rhs"
      proof -
        let ?r = "λq. state_rank q n"
        have "{q'. ¬sink q'  pre_ranks ?r (w n) q'  {}  Min (pre_ranks ?r (w n) q') < Min (pre_ranks ?r (w n) q)} = senior_states q (Suc n)"
          (is "?S = ?S'")
        proof (rule set_eqI)
          fix q'
          have "q'  ?S  ¬sink q'  configuration q' (Suc n)  {}  Min (pre_ranks  ?r (w n) q') < Min (pre_ranks ?r (w n) q)"
            using pre_ranks_tokens by blast
          also
          have "  ¬sink q'  configuration q' (Suc n)  {}  Min (pre_oldest_tokens q' n) < Min (pre_oldest_tokens q n)"
            by (metis ‹configuration q (Suc n)  {} ¬sink q Min_pre_ranks_pre_oldest_tokens)
          also
          have "  ¬sink q'  (x y. oldest_token q' (Suc n) = Some y  oldest_token q (Suc n) = Some x  y < x)"
            unfolding oldest_token_rec by (metis pre_oldest_configuration_tokens ‹configuration q (Suc n)  {} option.distinct(2) option.sel)
          finally
          show "q'  ?S  q'  ?S'"
            unfolding senior_states.simps by blast
        qed
        thus ?thesis
          using ¬sink q ‹configuration q (Suc n)  {}
          unfolding step.simps pre_ranks_tokens[OF ¬sink q] by presburger
      qed
      finally
      have ?thesis .
    }
    ultimately
    show ?thesis
      by blast
qed auto

lemma state_rank_step_foldl:
  "(λq. state_rank q n) = foldl step initial (map w [0..<n])"
  by (induction n) (unfold state_rank_initial state_rank_step, simp_all)

end

end

Theory Mojmir

(*
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Mojmir Automata›

theory Mojmir
  imports Main Semi_Mojmir
begin

subsection ‹Definitions›

locale mojmir_def = semi_mojmir_def +
  fixes
    ― ‹Final States›
    F :: "'b set"
begin

definition token_succeeds :: "nat  bool"
where
  "token_succeeds x = (n. token_run x n  F)"

definition token_fails :: "nat  bool"
where
  "token_fails x = (n. sink (token_run x n)  token_run x n  F)"

definition accept :: "bool" ("acceptM")
where
  "accept  (x. token_succeeds x)"

definition fail :: "nat set"
where
  "fail = {x. token_fails x}"

definition merge :: "nat  (nat × nat) set"
where
  "merge i = {(x, y) | x y n j. j < i
     (token_run x n  token_run y n  rank y n  None  y = Suc n)
     token_run x (Suc n) = token_run y (Suc n)
     token_run x (Suc n)  F
     rank x n = Some j}"

definition succeed :: "nat  nat set"
where
  "succeed i = {x. n. rank x n = Some i
     token_run x n  F - {q0}
     token_run x (Suc n)  F}"

definition smallest_accepting_rank :: "nat option"
where
  "smallest_accepting_rank  (if accept then
    Some (LEAST i. finite fail  finite (merge i)  infinite (succeed i)) else None)"

definition fail_t :: "nat set"
where
  "fail_t = {n. q q'. state_rank q n  None  q' = δ q (w n)  q'  F  sink q'}"

definition merge_t :: "nat  nat set"
where
  "merge_t i = {n. q q' j. state_rank q n = Some j  j < i  q' = δ q (w n)  q'  F 
    ((q''. q''  q  q' = δ q'' (w n)  state_rank q'' n  None)  q' = q0)}"

definition succeed_t :: "nat  nat set"
where
  "succeed_t i = {n. q. state_rank q n = Some i  q  F - {q0}  δ q (w n)  F}"

fun "𝒮"
where
  "𝒮 n = F  {q. (j  the smallest_accepting_rank. state_rank q n = Some j)}"

end

locale mojmir = semi_mojmir + mojmir_def +
  assumes
    ― ‹All states reachable from final states are also final›
    wellformed_F: "q ν. q  F  δ q ν  F"
begin

lemma token_stays_in_final_states:
  "token_run x n  F  token_run x (n + m)  F"
proof (induction m)
  case (Suc m)
    thus ?case
    proof (cases "n + m < x")
      case False
        hence "n + m  x"
          by arith
        then obtain j where "n + m = x + j"
          using le_Suc_ex by blast
        hence "δ (token_run x (n + m)) (suffix x w j) = token_run x (n + (Suc m))"
          unfolding suffix_def by fastforce
        thus ?thesis
          using wellformed_F Suc suffix_nth by (metis (no_types, hide_lams))
    qed fastforce
qed simp

lemma token_run_enter_final_states:
  assumes "token_run x n  F"
  shows "m  x. token_run x m  F - {q0}  token_run x (Suc m)  F"
proof (cases "x  n")
  case True
    then obtain n' where "token_run x (x + n')  F"
      using assms by force
    hence "m. token_run x (x + m)  F - {q0}  token_run x (x + Suc m)  F"
      by (induction n') ((metis (erased, hide_lams) token_stays_in_final_states token_run_intial_state  Diff_iff Nat.add_0_right Suc_eq_plus1 insertCI ), blast)
    thus ?thesis
      by (metis add_Suc_right le_add1)
next
  case False
    hence "token_run x x  F - {q0}" and "token_run x (Suc x)  F"
      using assms wellformed_F by simp_all
    thus ?thesis
      by blast
qed

subsection ‹Token Properties›

subsubsection ‹Alternative Definitions›

lemma token_succeeds_alt_def:
  "token_succeeds x = (n. token_run x n  F)"
  unfolding token_succeeds_def MOST_nat_le le_iff_add
  using token_stays_in_final_states by blast

lemma token_fails_alt_def:
  "token_fails x = (n. sink (token_run x n)  token_run x n  F)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain n where "sink (token_run x n)" and "token_run x n  F"
    using token_fails_def by blast
  hence "m  n. sink (token_run x m)" and "m  n. token_run x m  F"
    using token_stays_in_sink unfolding le_iff_add by auto
  thus ?rhs
    unfolding MOST_nat_le by blast
qed (unfold MOST_nat_le token_fails_def, blast)

lemma token_fails_alt_def_2:
  "token_fails x  ¬token_succeeds x  ¬token_squats x"
  by (metis add.commute token_fails_def token_squats_def token_stays_in_final_states token_stays_in_sink token_succeeds_def)

subsubsection ‹Properties›

lemma token_succeeds_run_merge:
  "x  n  y  n  token_run x n = token_run y n  token_succeeds x  token_succeeds y"
  using token_run_merge token_stays_in_final_states add.commute unfolding token_succeeds_def by metis

lemma token_squats_run_merge:
  "x  n  y  n  token_run x n = token_run y n  token_squats x  token_squats y"
  using token_run_merge token_stays_in_sink add.commute unfolding token_squats_def by metis

subsubsection ‹Pulled-Up Lemmas›

lemma configuration_token_succeeds:
  "x  configuration q n; y  configuration q n  token_succeeds x = token_succeeds y"
  using token_succeeds_run_merge push_down_configuration_token_run by meson

lemma configuration_token_squats:
  "x  configuration q n; y  configuration q n  token_squats x = token_squats y"
  using token_squats_run_merge push_down_configuration_token_run by meson

subsection ‹Mojmir Acceptance›

lemma Mojmir_reject:
  "¬ accept  (x. ¬token_succeeds x)"
  unfolding accept_def Alm_all_def by blast

lemma mojmir_accept_alt_def:
  "accept  finite {x. ¬token_succeeds x}"
  using Inf_many_def Mojmir_reject by blast

lemma mojmir_accept_initial:
  "q0  F  accept"
  unfolding accept_def MOST_nat_le token_succeeds_def
  using token_run_intial_state by metis

subsection ‹Equivalent Acceptance Conditions›

subsubsection ‹Token-Based Definitions›

lemma merge_token_succeeds:
  assumes "(x, y)  merge i"
  shows "token_succeeds x  token_succeeds y"
proof -
  obtain n j j' where "token_run x (Suc n) = token_run y (Suc n)"
    and "rank x n = Some j" and "rank y n = Some j'  y = Suc n"
    using assms unfolding merge_def by blast
  hence "x  Suc n" and "y  Suc n"
    using rank_Some_time le_Suc_eq by blast+
  then obtain q where "x  configuration q (Suc n)" and "y  configuration q (Suc n)"
    using ‹token_run x (Suc n) = token_run y (Suc n) pull_up_token_run_tokens by blast
  thus ?thesis
    using configuration_token_succeeds by blast
qed

lemma merge_subset:
   "i  j  merge i  merge j"
proof
  assume "i  j"
  fix p
  assume "p  merge i"
  then obtain x y n k where "p = (x, y)" and "k < i" and "token_run x n  token_run y n  rank y n  None  y = Suc n"
    and "token_run x (Suc n) = token_run y (Suc n)" and "token_run x (Suc n)  F" and "rank x n = Some k"
    unfolding merge_def by blast
  moreover
  hence "k < j"
    using i  j by simp
  ultimately
  have "(x, y)  merge j"
    unfolding merge_def by blast
  thus "p  merge j"
    using p = (x, y) by simp
qed

lemma merge_finite:
  "i  j  finite (merge j)  finite (merge i)"
  using merge_subset by (blast intro: rev_finite_subset)

lemma merge_finite':
  "i < j  finite (merge j)  finite (merge i)"
  using merge_finite[of i j] by force

lemma succeed_membership:
  "token_succeeds x  (i. x  succeed i)"
  (is "?lhs  ?rhs")
proof
  assume ?lhs
  then obtain m where "token_run x m  F"
    unfolding token_succeeds_alt_def MOST_nat_le by blast
  then obtain n where 1: "token_run x n  F - {q0}"
    and 2: "token_run x (Suc n)  F" and "x  n"
    using token_run_enter_final_states by blast
  moreover
  hence "¬sink (token_run x n)"
  proof (cases "token_run x n  q0")
    case True
      hence "token_run x n  F"
        using ‹token_run x n  F - {q0} by blast
      thus ?thesis
        using ‹token_run x (Suc n)  F token_stays_in_sink unfolding Suc_eq_plus1 by metis
  qed (simp add: sink_def)
  then obtain i where "rank x n = Some i"
    using x  n by fastforce
  ultimately
  show ?rhs
    unfolding succeed_def by blast
qed (unfold token_succeeds_def succeed_def, blast)

lemma stable_rank_succeed:
  assumes "infinite (succeed i)"
      and "x  succeed i"
      and "q0  F"
  shows "¬stable_rank x i"
proof
  assume "stable_rank x i"
  then obtain n where "n'  n. rank x n' = Some i"
    unfolding stable_rank_def MOST_nat_le by rule

  from assms(2) obtain m where "token_run x m  F"
    and "token_run x (Suc m)  F"
    and "rank x m = Some i"
    using assms(3) unfolding succeed_def by force

  obtain y where "y > max n m" and "y  succeed i"
    using assms(1) unfolding infinite_nat_iff_unbounded by blast

  then obtain m' where "token_run y m'  F"
    and "token_run y (Suc m')  F"
    and "rank y m' = Some i"
    using assms(3) unfolding succeed_def by force

  moreover

  ― ‹token has still rank i at m'›
  have "m'  n"
    using rank_Some_time[OF ‹rank y m' = Some i] y > max n m by force
  hence "rank x m' = Some i"
    using  n'  n. rank x n' = Some i by blast

  moreover

  ― ‹but x and y are not in the same state›
  have "m'  Suc m"
    using rank_Some_time[OF ‹rank y m' = Some i] y > max n m by force
  hence "token_run x m'  F"
    using token_stays_in_final_states[OF ‹token_run x (Suc m)  F]
    unfolding le_iff_add by fast
  with ‹token_run y m'  F have "token_run y m'  token_run x m'"
    by metis

  ultimately

  show "False"
    using push_down_rank_tokens by force
qed

lemma stable_rank_bounded:
  assumes stable: "stable_rank x j"
  assumes inf: "infinite (succeed i)"
  assumes "q0  F"
  shows "j < i"
proof -
  from stable obtain m where "m'  m. rank x m' = Some j"
    unfolding stable_rank_def MOST_nat_le by rule
  from inf obtain y where "y  m" and "y  succeed i"
    unfolding infinite_nat_iff_unbounded_le by meson
  then obtain n where "rank y n = Some i"
    unfolding succeed_def MOST_nat_le by blast

  moreover

  hence "n  y"
    by (rule rank_Some_time)
  hence "rank x n = Some j"
    using m'  m. rank x m' = Some j y  m by fastforce

  ultimately

  ― ‹In the case @{term "i  j"}, the token y has also to stabilise with @{term i} at @{term n}.›
  have "i  j  stable_rank y i"
    using stable by (blast intro: stable_rank_tower)
  thus "j < i"
    using stable_rank_succeed[OF inf y  succeed i q0  F] by linarith
qed

― ‹Relation to Mojmir Acceptance›

lemma mojmir_accept_token_set_def1:
  assumes "accept"
  shows "i < max_rank. finite fail  finite (merge i)  infinite (succeed i)  (j < i. finite (succeed j))"
proof (rule+)
  define i where "i = (LEAST k. infinite (succeed k))"

  from assms have "infinite {t. token_succeeds t}"
    unfolding mojmir_accept_alt_def by force

  moreover

  have "{x. token_succeeds x} = {succeed i | i. i < max_rank}"
    (is "?lhs = ?rhs")
  proof -
    have "?lhs = {succeed i | i. True}"
      using succeed_membership by blast
    also
    have " = ?rhs"
    proof
      show "  ?rhs"
      proof
        fix x
        assume "x  {succeed i |i. True}"
        then obtain i where "x  succeed i"
          by blast
        moreover
        ― ‹Obtain upper bound for succeed ranks›
        have "u. u  max_rank  succeed u = {}"
          unfolding succeed_def using rank_upper_bound by fastforce
        ultimately
        show "x  {succeed i |i. i < max_rank}"
          by (cases "i < max_rank") (blast, simp)
      qed
    qed blast
    finally
    show ?thesis .
  qed

  ultimately

  have "j. infinite (succeed j)"
    by force
  hence "infinite (succeed i)" and "j. j < i  finite (succeed j)"
    unfolding i_def by (metis LeastI_ex, metis not_less_Least)
  hence fin_succeed_ranks: "finite ({succeed j | j. j < i})"
    by auto

  ― ‹@{term i} is bounded by @{term max_rank}
  {
    obtain x where "x  succeed i"
      using ‹infinite (succeed i) by fastforce
    then obtain n where "rank x n = Some i"
      unfolding succeed_def by blast
    thus "i < max_rank"
      by (rule rank_upper_bound)
  }

  define S where "S = {(x, y). token_succeeds x  token_succeeds y}"

  have "finite (merge i  S)"
  proof (rule finite_product)
    {
      fix x y
      assume "(x, y)  (merge i  S)"

      then obtain n k k'' where "k < i"
        and "rank x n = Some k"
        and "rank y n = Some k''  y = Suc n"
        and "token_run x (Suc n)  F"
        and "token_run x (Suc n) = token_run y (Suc n)"
        and "token_succeeds x"
        unfolding merge_def S_def by fast

      then obtain m where "token_run x (Suc n + m)  F"
        and "token_run x (Suc (Suc n + m))  F"
        by (metis Suc_eq_plus1 add.commute token_run_P[of "λq. q  F"] token_stays_in_final_states token_succeeds_def)

      moreover

      have "x  Suc n" and "y  Suc n" and "x  Suc n + m" and "y  Suc n + m"
        using rank_Some_time ‹rank x n = Some k ‹rank y n = Some k''  y = Suc n by fastforce+

      hence "token_run y (Suc n + m)  F" and "token_run y (Suc (Suc n + m))  F"
        using ‹token_run x (Suc n + m)  F ‹token_run x (Suc (Suc n + m))  F ‹token_run x (Suc n) = token_run y (Suc n)
        using token_run_merge token_run_merge_Suc by metis+

      moreover

      have "¬sink (token_run x (Suc n + m))"
        using ‹token_run x (Suc n + m)  F ‹token_run x (Suc(Suc n + m))  F
        using token_is_not_in_sink by blast

      ― ‹Obtain rank used to enter final›
      obtain k' where "rank x (Suc n + m) = Some k'"
        using ¬sink (token_run x (Suc n + m)) x  Suc n + m by fastforce

      moreover

      hence "rank y (Suc n + m) = Some k'"
        by (metis x  Suc n + m y  Suc n + m token_run_merge x  Suc n y  Suc n
                  ‹token_run x (Suc n) = token_run y (Suc n) pull_up_token_run_tokens
                  pull_up_configuration_rank[of x _ "Suc n + m" y])

      moreover

      ― ‹Rank used to enter final states is strictly bounded by i›
      have "k' < i"
        using ‹rank x (Suc n + m) = Some k' rank_monotonic[OF ‹rank x n = Some k] k < i
        unfolding add_Suc_shift by fastforce

      ultimately

      have "x  {succeed j | j. j < i}" and "y  {succeed j | j. j < i}"
        unfolding succeed_def by blast+
    }
    hence "fst ` (merge i  S)  {succeed j | j. j < i}" and "snd ` (merge i  S)  {succeed j | j. j < i}"
      by force+
    thus "finite (fst ` (merge i  S))" and "finite (snd ` (merge i  S))"
      using finite_subset[OF _ fin_succeed_ranks] by meson+
  qed

  moreover

  have "finite (merge i  (UNIV - S))"
  proof -
    obtain l where l_def: "x  l. token_succeeds x"
      using assms unfolding accept_def MOST_nat_le by blast
    {
      fix x y
      assume "(x, y)  merge i  (UNIV - S)"
      hence "¬token_succeeds x  ¬token_succeeds y"
        unfolding S_def by simp
      hence "¬token_succeeds x  ¬token_succeeds y"
        using merge_token_succeeds (x, y)  merge i  (UNIV - S) by blast
      hence "x < l" and "y < l"
        by (metis l_def le_eq_less_or_eq linear)+
    }
    hence "merge i  (UNIV - S)  {0..l} × {0..l}"
      by fastforce
    thus ?thesis
      using finite_subset by blast
  qed

  ultimately

  have "finite (merge i)"
    by (metis Int_Diff Un_Diff_Int finite_UnI inf_top_right)
  moreover
  have "finite fail"
    by (metis assms mojmir_accept_alt_def fail_def token_fails_alt_def_2 infinite_nat_iff_unbounded_le mem_Collect_eq)
  ultimately
  show "finite fail  finite (merge i)  infinite (succeed i)  (j < i. finite (succeed j))"
    using ‹infinite (succeed i) j. j < i  finite (succeed j) by blast
qed

lemma mojmir_accept_token_set_def2:
  assumes "finite fail"
      and "finite (merge i)"
      and "infinite (succeed i)"
  shows "accept"
proof (rule ccontr, cases "q0  F")
  case True
    assume "¬ accept"
    moreover
    have "finite {x. ¬token_succeeds x  ¬token_squats x}"
      using ‹finite fail› unfolding fail_def token_fails_alt_def_2[symmetric] .
    moreover
    have X: "{x. ¬ token_succeeds x} = {x. ¬ token_succeeds x  token_squats x}  {x. ¬ token_succeeds x  ¬ token_squats x}"
      by blast
    ultimately
    have inf: "infinite {x. ¬token_succeeds x  token_squats x}"
      unfolding mojmir_accept_alt_def X by blast

    ― ‹Obtain j, where j is the rank used by infinitely many configuration stabilising and not succeeding›
    have "{x. ¬token_succeeds x  token_squats x} = {x. j < i. ¬token_succeeds x  token_squats x  stable_rank x j}"
      using stable_rank_bounded ‹infinite (succeed i) q0  F
      unfolding stable_rank_equiv_token_squats by metis
    also
    have " = {{x.  ¬token_succeeds x  token_squats x  stable_rank x j} | j. j < i}"
      by blast
    finally
    obtain j where "j < i" and "infinite {t. ¬token_succeeds t  token_squats t  stable_rank t j}"
      (is "infinite ?S")
      using inf by force

    ― ‹Obtain such a token x›
    then obtain x where "¬token_succeeds x" and "token_squats x" and "stable_rank x j"
      unfolding infinite_nat_iff_unbounded_le by blast
    then obtain n where "m  n. rank x m = Some j"
      unfolding stable_rank_def MOST_nat_le by blast

    ― ‹All configuration with same stable rank are bought at some n with rank smaller i›
    have "{(x, y) | y. y > n  stable_rank y j}  merge i"
      (is "?lhs  ?rhs")
    proof
      fix p
      assume "p  ?lhs"
      then obtain y where "p = (x, y)" and "y > n" and "stable_rank y j"
        by blast
      hence "x < y" and "x  y"
        using rank_Some_time n'n. rank x n' = Some j by fastforce+

      moreover

      ― ‹Obtain a time n'' where x and y have the same rank›
      obtain n'' where "rank x n'' = Some j" and "rank y n'' = Some j"
        using n'n. rank x n' = Some j ‹stable_rank y j
        unfolding stable_rank_def MOST_nat_le by (metis add.commute le_add2)
      hence "token_run x n'' = token_run y n''" and "y  n''"
        using push_down_rank_tokens rank_Some_time[OF ‹rank y n'' = Some j] by simp_all

      ― ‹Obtain the time n' where x merges y and proof all necessary properties›
      then obtain n' where "token_run x n'  token_run y n'  y = Suc n'"
        and "token_run x (Suc n') = token_run y (Suc n')" and "y  Suc n'"
        using token_run_mergepoint[OF x < y] le_add_diff_inverse by metis

      moreover

      hence "(j'. rank y n' = Some j')  y = Suc n'"
        using ‹stable_rank y j stable_rank_equiv_token_squats rank_token_squats
        unfolding le_Suc_eq by blast

      moreover

      have "rank x n' = Some j"
        using n'n. rank x n' = Some j y  Suc n' y > n by fastforce

      moreover

      have "token_run x (Suc n')  F"
        using ¬ token_succeeds x token_succeeds_def by blast

      ultimately
      show "p  ?rhs"
        unfolding merge_def p = (x, y)
        using j < i by blast
    qed

    moreover

    ― ‹However, x merges infinitely many configuration›
    hence "infinite {(x, y) | y. y > n  stable_rank y j}"
      (is "infinite ?S'")
    proof -
      {
        {
          fix y
          assume "stable_rank y j" and "y > n"
          then obtain n' where "rank y n' = Some j"
            unfolding stable_rank_def MOST_nat_le by blast
          moreover
          hence "y  n'"
            by (rule rank_Some_time)
          hence "n' > n"
            using y > n by arith
          hence "rank x n' = Some j"
            using n'  n. rank x n' = Some j by simp
          ultimately
          have "¬token_succeeds y"
            by (metis ¬token_succeeds x configuration_token_succeeds push_down_rank_tokens)
        }
        hence "{y | y. y > n  stable_rank y j} = {y | y. token_squats y  ¬token_succeeds y  stable_rank y j   y > n}"
          (is "_ = ?S''")
          using stable_rank_equiv_token_squats by blast
        moreover
        have "finite {y | y. token_squats y  ¬token_succeeds y  stable_rank y j   y  n}"
          (is "finite ?S'''")
          by simp
        moreover
        have "?S = ?S''  ?S'''"
          by auto
        ultimately
        have "infinite {y | y. y > n  stable_rank y j}"
          using ‹infinite ?S by simp
      }
      moreover
      have "{x} × {y. y > n  stable_rank y j} = ?S'"
        by auto
      ultimately
      show ?thesis
        by (metis empty_iff finite_cartesian_productD2 singletonI)
    qed

    ultimately

    have "infinite (merge i)"
      by (rule infinite_super)
    with ‹finite (merge i) show "False"
      by blast
qed (blast intro: mojmir_accept_initial)

theorem mojmir_accept_iff_token_set_accept:
  "accept  (i < max_rank. finite fail  finite (merge i)  infinite (succeed i))"
  using mojmir_accept_token_set_def1 mojmir_accept_token_set_def2 by blast

theorem mojmir_accept_iff_token_set_accept2:
  "accept  (i < max_rank. finite fail  finite (merge i)  infinite (succeed i)  (j < i. finite (merge j)  finite (succeed j)))"
  using mojmir_accept_token_set_def1 mojmir_accept_token_set_def2 merge_finite' by blast

subsubsection ‹Time-Based Definitions›

― ‹Proof Rules›

lemma finite_monotonic_image:
  fixes A B :: "nat set"
  assumes "i. i  A  i  f i"
  assumes "f ` A = B"
  shows "finite A  finite B"
proof
  assume "finite B"
  thus "finite A"
  proof (cases "B  {}")
    case True
      hence "i. i  A  i  Max B"
        by (metis assms Max_ge_iff ‹finite B imageI)
      thus "finite A"
        unfolding finite_nat_set_iff_bounded_le by blast
  qed (metis assms(2) image_is_empty)
qed (metis assms(2) finite_imageI)

lemma finite_monotonic_image_pairs:
  fixes A :: "(nat × nat) set"
  fixes B :: "nat set"
  assumes "i. i  A  (fst i)  f i + c"
  assumes "i. i  A  (snd i)  f i + d"
  assumes "f ` A = B"
  shows "finite A  finite B"
proof
  assume "finite B"
  thus "finite A"
  proof (cases "B  {}")
    case True
      hence "i. i  A  fst i  Max B + c  snd i  Max B + d"
        by (metis assms Max_ge_iff ‹finite B imageI le_diff_conv)
      thus "finite A"
        using finite_product[of A] unfolding finite_nat_set_iff_bounded_le by blast
  qed (metis assms(3) finite.emptyI image_is_empty)
qed (metis assms(3) finite_imageI)

lemma token_time_finite_rule:
  fixes A B :: "nat set"
  assumes unique:  "x y z. P x y  P x z  y = z"
      and existsA: "x. x  A  (y. P x y)"
      and existsB: "y. y  B  (x. P x y)"
      and inA:     "x y. P x y  x  A"
      and inB:     "x y. P x y  y  B"
      and mono:    "x y. P x y  x  y"
  shows "finite A  finite B"
proof (rule finite_monotonic_image)
  let ?f = "(λx. if x  A then The (P x) else undefined)"

  {
    fix x
    assume "x  A"
    then obtain y where "P x y" and "y = ?f x"
      using existsA the_equality unique by metis
    thus "x  ?f x"
      using mono by blast
  }

  {
    fix y
    have "y  ?f ` A  (x. x  A  y = The (P x))"
      unfolding image_def by force
    also
    have "  (x. P x y)"
      by (metis inA existsA unique the_equality)
    also
    have "  y  B"
      using inB existsB by blast
    finally
    have "y  ?f ` A  y  B"
      .
  }
  thus "?f ` A = B"
    by blast
qed

lemma token_time_finite_pair_rule:
  fixes A :: "(nat × nat) set"
  fixes B :: "nat set"
  assumes unique:  "x y z. P x y  P x z  y = z"
      and existsA: "x. x  A  (y. P x y)"
      and existsB: "y. y  B  (x. P x y)"
      and inA:     "x y. P x y  x  A"
      and inB:     "x y. P x y  y  B"
      and mono:    "x y. P x y  fst x  y + c  snd x  y + d"
  shows "finite A  finite B"
proof (rule finite_monotonic_image_pairs)
  let ?f = "(λx. if x  A then The (P x) else undefined)"

  {
    fix x
    assume "x  A"
    then obtain y where "P x y" and "y = ?f x"
      using existsA the_equality unique by metis
    thus "fst x  ?f x + c" and "snd x  ?f x + d"
      using mono by blast+
  }

  {
    fix y
    have "y  ?f ` A  (x. x  A  y = The (P x))"
      unfolding image_def by force
    also
    have "  (x. P x y)"
      by (metis inA existsA unique the_equality)
    also
    have "  y  B"
      using inB existsB by blast
    finally
    have "y  ?f ` A  y  B"
      .
  }
  thus "?f ` A = B"
    by blast
qed

― ‹Correspondence Between Token- and Time-Based Definitions›

lemma fail_t_inclusion:
  assumes "x  n"
  assumes "¬sink (token_run x n)"
  assumes "sink (token_run x (Suc n))"
  assumes "token_run x (Suc n)  F"
  shows "n  fail_t"
proof -
  define q q' where "q = token_run x n" and "q' = token_run x (Suc n)"
  hence *: "¬sink q" "sink q'" and "q'  F"
    using assms by blast+
  moreover
  from * have **: "state_rank q n  None"
    unfolding q_def by (metis oldest_token_always_def option.distinct(1) state_rank_None)
  moreover
  from ** have "q' = δ q (w n)"
    unfolding q_def q'_def using assms(1) token_run_step' by blast
  ultimately
  show "n  fail_t"
    unfolding fail_t_def by blast
qed

lemma merge_t_inclusion:
  assumes "x  n"
  assumes "(j'. token_run x n  token_run y n  y  n  state_rank (token_run y n) n = Some j')  y = Suc n"
  assumes "token_run x (Suc n) = token_run y (Suc n)"
  assumes "token_run x (Suc n)  F"
  assumes "state_rank (token_run x n) n = Some j"
  assumes "j < i"
  shows "n  merge_t i"
proof -
  define q q' q''
    where "q = token_run x n"
      and "q' = token_run x (Suc n)"
      and "q'' = token_run y n"
  have "y  Suc n"
    using assms(2) by linarith
  hence "(q' = δ q'' (w n)  state_rank q'' n  None  q''  q)  q' = q0"
    unfolding q_def q'_def q''_def using assms(2-3)
    by (cases "y = Suc n") ((metis token_run_intial_state), (metis option.distinct(1) token_run_step))
  moreover
  have "state_rank q n = Some j  j < i  q' = δ q (w n)  q'  F"
    unfolding q_def q'_def using token_run_step[OF assms(1)] assms(4-6) by blast
  ultimately
  show "n  merge_t i"
    unfolding merge_t_def by blast
qed

lemma succeed_t_inclusion:
  assumes "rank x n = Some i"
  assumes "token_run x n  F - {q0}"
  assumes "token_run x (Suc n)  F"
  shows "n  succeed_t i"
proof -
  define q where "q = token_run x n"
  hence "state_rank q n = Some i" and "q  F - {q0}" and "δ q (w n)  F"
    using token_run_step' rank_Some_time[OF assms(1)] assms rank_eq_state_rank by auto
  thus "n  succeed_t i"
    unfolding succeed_t_def by blast
qed

lemma finite_fail_t:
  "finite fail = finite fail_t"
proof (rule token_time_finite_rule)
  let ?P = "(λx n. x  n
     ¬sink (token_run x n)
     sink (token_run x (Suc n))
     token_run x (Suc n)  F)"

  {
    fix x
    have "¬sink (token_run x x)"
      unfolding sink_def by simp

    assume "x  fail"
    hence "token_fails x"
      unfolding fail_def ..
    moreover
    then obtain y'' where "sink (token_run x (Suc (x + y'')))"
      unfolding token_fails_alt_def MOST_nat
      using ¬ sink (token_run x x) less_add_Suc2 by blast
    then obtain y' where "¬sink (token_run x (x + y'))" and "sink (token_run x (Suc (x + y')))"
      using token_run_P[of "λq. sink q", OF ¬sink (token_run x x)] by blast
    ultimately
    show "y. ?P x y"
      using token_fails_alt_def_2 token_succeeds_def by (metis le_add1)
  }

  {
    fix y
    assume "y  fail_t"
    then obtain q q' i where "state_rank q y = Some i" and "q' = δ q (w y)" and "q'  F" and "sink q'"
      unfolding fail_t_def by blast
    moreover
    then obtain x where "token_run x y = q" and "x  y"
      by (blast dest: push_down_state_rank_token_run)
    moreover
    hence "token_run x (Suc y) = q'"
      using token_run_step[OF _ _ q' = δ q (w y)] by blast
    ultimately
    show "x. ?P x y"
      by (metis option.distinct(1) state_rank_sink)
  }

  {
    fix x y
    assume "?P x y"
    thus "x  fail" and "x  y" and "y  fail_t"
      unfolding fail_def using token_fails_def fail_t_inclusion by blast+
  }

  ― ‹Uniqueness›
  {
    fix x y z
    assume "?P x y" and "?P x z"
    from ?P x y have "¬sink (token_run x y)" and "sink (token_run x (Suc y))"
      by blast+
    moreover
    from ?P x z have "¬sink (token_run x z)" and "sink (token_run x (Suc z))"
      by blast+
    ultimately
    show "y = z"
      using token_stays_in_sink
      by (cases y z rule: linorder_cases, simp_all)
         (metis (no_types, lifting) Suc_leI le_add_diff_inverse)+
  }
qed

lemma finite_succeed_t':
  assumes "q0  F"
  shows "finite (succeed i) = finite (succeed_t i)"
proof (rule token_time_finite_rule)
  let ?P = "(λx n. x  n
     state_rank (token_run x n) n = Some i
     (token_run x n)  F - {q0}
     (token_run x (Suc n))  F)"

  {
    fix x
    assume "x  succeed i"
    then obtain y where "token_run x y  F - {q0}" and "token_run x (Suc y)  F" and "rank x y = Some i"
       unfolding succeed_def by force
    moreover
    hence "rank (senior x y) y = Some i"
      using rank_Some_time[THEN rank_senior_senior] by presburger
    hence "state_rank (token_run x y) y = Some i"
      unfolding state_rank_eq_rank senior.simps by (metis oldest_token_always_def option.sel option.simps(5))
    ultimately
    show "y. ?P x y"
      using rank_Some_time by blast
  }

  {
    fix y
    assume "y  succeed_t i"
    then obtain q where "state_rank q y = Some i" and "q  F - {q0}" and "(δ q (w y))  F"
      unfolding succeed_t_def by blast
    moreover
    then obtain x where "q = token_run x y" and "x  y"
      by (metis oldest_token_bounded push_down_oldest_token_token_run push_down_state_rank_oldest_token)
    moreover
    hence "token_run x (Suc y)  F"
      using token_run_step (δ q (w y))  F by simp
    ultimately
    show "x. ?P x y"
      by meson
  }

  {
    fix x y
    assume "?P x y"
    thus "x  y" and "x  succeed i" and "y  succeed_t i"
      unfolding succeed_def using rank_eq_state_rank[of x y] succeed_t_inclusion
      by (metis (mono_tags, lifting) mem_Collect_eq)+
  }

  ― ‹Uniqueness›
  {
    fix x y z
    assume "?P x y" and "?P x z"
    from ?P x y have "token_run x y  F" and "token_run x (Suc y)  F"
      using q0  F by auto
    moreover
    from ?P x z have "token_run x z  F" and "token_run x (Suc z)  F"
      using q0  F by auto
    ultimately
    show "y = z"
      using token_stays_in_final_states
      by (cases y z rule: linorder_cases, simp_all)
         (metis le_Suc_ex less_Suc_eq_le not_le)+
  }
qed

lemma initial_in_F_token_run:
  assumes "q0  F"
  shows "token_run x y  F"
  using assms token_stays_in_final_states[of _ 0] by fastforce

lemma finite_succeed_t'':
  assumes "q0  F"
  shows "finite (succeed i) = finite (succeed_t i)"
  (is "?lhs = ?rhs")
proof
  have "succeed_t i = {n. state_rank q0 n = Some i}"
    unfolding succeed_t_def using initial_in_F_token_run assms wellformed_F by auto
  also
  have "... = {n. rank n n = Some i}"
    unfolding rank_eq_state_rank[OF order_refl] token_run_intial_state ..
  finally
  have succeed_t_alt_def: "succeed_t i = {n. rank n n = Some i  token_run n n = q0}"
    by simp

  have succeed_alt_def: "succeed i = {x. n. rank x n = Some i  token_run x n = q0}"
    unfolding succeed_def using initial_in_F_token_run[OF assms] by auto

  {
    assume ?lhs
    moreover
    have "succeed_t i  succeed i"
      unfolding succeed_t_alt_def succeed_alt_def by blast
    ultimately
    show ?rhs
      by (rule rev_finite_subset)
  }

  {
    assume ?rhs
    then obtain U where U_def: "x. x  succeed_t i  U  x"
      unfolding finite_nat_set_iff_bounded_le by blast
    {
      fix x
      assume "x  succeed i"
      then obtain n where "rank x n = Some i" and "token_run x n = q0"
        unfolding succeed_alt_def by blast
      moreover
      hence "x  n"
        by (blast dest: rank_Some_time)
      moreover
      hence "rank n n = Some i"
        using ‹rank x n = Some i ‹token_run x n = q0
        by (metis order_refl token_run_intial_state[of n] pull_up_token_run_tokens pull_up_configuration_rank)
      hence "n  succeed_t i"
        unfolding succeed_t_alt_def by simp
      ultimately
      have "U  x"
        using U_def by fastforce
    }
    thus ?lhs
      unfolding finite_nat_set_iff_bounded_le by blast
  }
qed

lemma finite_succeed_t:
  "finite (succeed i) = finite (succeed_t i)"
  using finite_succeed_t' finite_succeed_t'' by blast

lemma finite_merge_t:
  "finite (merge i) = finite (merge_t i)"
proof (rule token_time_finite_pair_rule)
  let ?P = "(λ(x, y) n. j. x  n
     ((j'. token_run x n  token_run y n  y  n  state_rank (token_run y n) n = Some j')  y = Suc n)
     token_run x (Suc n) = token_run y (Suc n)
     token_run x (Suc n)  F
     state_rank (token_run x n) n = Some j
     j < i)"

  {
    fix x
    assume "x  merge i"
    then obtain t t' n j where 1: "x = (t, t')"
      and 3: "(j'. token_run t n  token_run t' n  rank t' n = Some j')   t' = Suc n"
      and 4: "token_run t (Suc n) = token_run t' (Suc n)"
      and 5: "token_run t (Suc n)  F"
      and 6: "rank t n = Some j"
      and 7:  "j < i"
      unfolding merge_def by blast
    moreover
    hence 8: "t  n" and 9: "t'  Suc n"
      using rank_Some_time le_Suc_eq by blast+
    moreover
    hence 10: "state_rank (token_run t n) n = Some j"
      using ‹rank t n = Some j rank_eq_state_rank by metis
    ultimately
    show "y. ?P x y"
    proof (cases "t' = Suc n")
      case False
        hence "t'  n"
          using t'  Suc n by simp
        with 1 3 4 5 7 8 10 show ?thesis
          unfolding rank_eq_state_rank[OF t'  n] by blast
    qed blast
  }

  {
    fix y
    assume "y  merge_t i"
    then obtain q q' j where 1: "state_rank q y = Some j"
      and 2: "j < i"
      and 3: "q' = δ q (w y)"
      and 4: "q'  F"
      and 5: "(q''. q' = δ q'' (w y)  state_rank q'' y  None  q''  q)  q' = q0"
      unfolding merge_t_def by blast

    then obtain t where 6: "q = token_run t y" and 7: "t  y"
      using push_down_state_rank_token_run by metis
    hence 8: "q' = token_run t (Suc y)"
      unfolding q' = δ q (w y) using token_run_step by simp

    {
      assume "q' = q0"
      hence "token_run t (Suc y) = token_run (Suc y) (Suc y)"
        unfolding 8 by simp
      moreover
      then obtain x where "x = (t, Suc y)"
        by simp
      ultimately
      have "?P x y"
        using 1 2 3 4 5 7 unfolding 6 8 by force
      hence "x. ?P x y"
        by blast
    }
    moreover
    {
      assume "q'  q0"
      then obtain q'' j' where 9: "q' = δ q'' (w y)"
        and "state_rank q'' y = Some j'"
        and "q''  q"
        using 5 by blast
      moreover
      then obtain t' where 12: "q'' = token_run t' y" and "t'  y"
        by (blast dest: push_down_state_rank_token_run)
      moreover
      hence "token_run t (Suc y) = token_run t' (Suc y)"
        using 8 9 token_run_step by presburger
      moreover
      have "token_run t y  token_run t' y"
        using q''  q unfolding 6 12 ..
      moreover
      then obtain x where "x = (t, t')"
        by simp