# Theory Mojmir

theory Mojmir
imports Semi_Mojmir
```(*
Author:      Salomon Sickert
*)

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" ("accept⇩M")
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 - {q⇩0}
∧ 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' = q⇩0)}"

definition succeed_t :: "nat ⇒ nat set"
where
"succeed_t i = {n. ∃q. state_rank q n = Some i ∧ q ∉ F - {q⇩0} ∧ δ 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 - {q⇩0} ∧ 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 - {q⇩0} ∧ 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
next
case False
hence "token_run x x ∉ F - {q⇩0}" 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)"
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:
"q⇩0 ∈ 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 - {q⇩0}"
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 ≠ q⇩0")
case True
hence "token_run x n ∉ F"
using ‹token_run x n ∉ F - {q⇩0}› by blast
thus ?thesis
using ‹token_run x (Suc n) ∈ F› token_stays_in_sink unfolding Suc_eq_plus1 by metis
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 "q⇩0 ∉ 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›]
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 "q⇩0 ∉ 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› ‹q⇩0 ∉ 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›

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 "q⇩0 ∉ 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)› ‹q⇩0 ∉ 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›
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' = q⇩0"
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 - {q⇩0}"
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 - {q⇩0}" 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)
}
qed

lemma finite_succeed_t':
assumes "q⇩0 ∉ 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 - {q⇩0}
∧ (token_run x (Suc n)) ∈ F)"

{
fix x
assume "x ∈ succeed i"
then obtain y where "token_run x y ∉ F - {q⇩0}" 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 - {q⇩0}" 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 ‹q⇩0 ∉ F› by auto
moreover
from ‹?P x z› have "token_run x z ∉ F" and "token_run x (Suc z) ∈ F"
using ‹q⇩0 ∉ 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 "q⇩0 ∈ F"
shows "token_run x y ∈ F"
using assms token_stays_in_final_states[of _ 0] by fastforce

lemma finite_succeed_t'':
assumes "q⇩0 ∈ F"
shows "finite (succeed i) = finite (succeed_t i)"
(is "?lhs = ?rhs")
proof
have "succeed_t i = {n. state_rank q⇩0 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 = q⇩0}"
by simp

have succeed_alt_def: "succeed i = {x. ∃n. rank x n = Some i ∧ token_run x n = q⇩0}"
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 = q⇩0"
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 = q⇩0›
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' = q⇩0"
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' = q⇩0"
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' ≠ q⇩0"
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
ultimately
have "?P x y"
using 1 2 4 7 unfolding 6 8 by fast
hence "∃x. ?P x y"
by blast
}
ultimately
show "∃x. ?P x y"
by blast
}

{
fix x y
assume "?P x y"
then obtain t t' j where 1: "x = (t, t')"
and 3: "t ≤ y"
and 4: "(∃j'. token_run t y ≠ token_run t' y ∧ t' ≤ y ∧ state_rank (token_run t' y) y = Some j') ∨ t' = Suc y"
and 5: "token_run t (Suc y) = token_run t' (Suc y)"
and 6: "token_run t (Suc y) ∉ F"
and 7: "state_rank (token_run t y) y = Some j"
and 8: "j < i"
by blast

thus "x ∈ merge i"
proof (cases "t' = Suc y")
case False
hence "t' ≤ y"
using 4 by blast
thus ?thesis
using 1 3 4 5 6 7 8 unfolding merge_def
unfolding rank_eq_state_rank[OF ‹t' ≤ y›, symmetric] rank_eq_state_rank[OF ‹t ≤ y›, symmetric]
by blast
qed (unfold rank_eq_state_rank[OF ‹t ≤ y›, symmetric] merge_def, blast)

show "y ∈ merge_t i" and "fst x ≤ y + 0 ∧ snd x ≤ y + 1"
using merge_t_inclusion ‹?P x y› by force+
}

― ‹Uniqueness›
{
fix x y z
assume "?P x y" and "?P x z"
then obtain t t' where "x = (t, t')"
by blast
from ‹?P x y›[unfolded ‹x = (t, t')›] have y1: "t ≤ y"
and y2: "(token_run t y ≠ token_run t' y ∧ t' ≤ y) ∨ t' = Suc y"
and y3: "token_run t (Suc y) = token_run t' (Suc y)" by blast+
moreover
from ‹?P x z›[unfolded ‹x = (t, t')›] have z1: "t ≤ z"
and z2: "(token_run t z ≠ token_run t' z ∧ t' ≤ z) ∨ t' = Suc z"
and z3: "token_run t (Suc z) = token_run t' (Suc z)" by blast+
moreover
have y4: "t' ≤ Suc y" and z4: "t' ≤ Suc z"
using y2 z2 by linarith+
ultimately
show "y = z"
proof (cases y z rule: linorder_cases)
case less
then obtain d where "Suc y + d = z"
thus ?thesis
using y1 y2 z2 token_run_merge[OF _ y4 y3] by auto
next
case greater
then obtain d where "Suc z + d = y"
thus ?thesis
using z1 y2 z2 token_run_merge[OF _ z4 z3] by auto
qed
}
qed

subsubsection ‹Relation to Mojmir Acceptance›

lemma token_iff_time_accept:
shows "(finite fail ∧ finite (merge i) ∧ infinite (succeed i) ∧ (∀j < i. finite (succeed j)))
= (finite fail_t ∧ finite (merge_t i) ∧ infinite (succeed_t i) ∧ (∀j < i. finite (succeed_t j)))"
unfolding finite_fail_t finite_merge_t finite_succeed_t by simp

subsection ‹Succeeding Tokens (Alternative Definition)›

definition stable_rank_at :: "nat ⇒ nat ⇒ bool"
where
"stable_rank_at x n ≡ ∃i. ∀m ≥ n. rank x m = Some i"

lemma stable_rank_at_ge:
"n ≤ m ⟹ stable_rank_at x n ⟹ stable_rank_at x m"
unfolding stable_rank_at_def by fastforce

lemma stable_rank_equiv:
"(∃i. stable_rank x i) = (∃n. stable_rank_at x n)"
unfolding stable_rank_def MOST_nat_le stable_rank_at_def by blast

lemma smallest_accepting_rank_properties:
assumes "smallest_accepting_rank = Some i"
shows "accept" "finite fail" "finite (merge i)" "infinite (succeed i)" "∀j < i. finite (succeed j)" "i < max_rank"
proof -
from assms show "accept"
unfolding smallest_accepting_rank_def using option.distinct(1) by metis
then obtain i' where "finite fail" and "finite (merge i')" and "infinite (succeed i')"
and "∀j < i'. finite (succeed j)" and "i' < max_rank"
unfolding mojmir_accept_iff_token_set_accept2 by blast
moreover
hence "⋀y. finite fail ∧ finite (merge y) ∧ infinite (succeed y) ⟶ i' ≤ y"
using not_le by blast
ultimately
have "(LEAST i. finite fail ∧ finite (merge i) ∧ infinite (succeed i)) = i'"
using le_antisym unfolding Least_def by (blast dest: the_equality[of _ i'])
hence "i' = i"
using ‹smallest_accepting_rank = Some i› ‹accept› unfolding smallest_accepting_rank_def by simp
thus "finite fail" and "finite (merge i)" and "infinite (succeed i)"
and "∀j < i. finite (succeed j)" and "i < max_rank"
using ‹finite fail› ‹finite (merge i')› ‹infinite (succeed i')›
using ‹∀j < i'. finite (succeed j)› ‹i' < max_rank› by simp+
qed

lemma token_smallest_accepting_rank:
assumes "smallest_accepting_rank = Some i"
shows "∀⇩∞n. ∀x. token_succeeds x ⟷ (x > n ∨ (∃j ≥ i. rank x n = Some j) ∨ token_run x n ∈ F)"
proof -
from assms have "accept" "finite fail" "infinite (succeed i)" "∀j < i. finite (succeed j)"
using smallest_accepting_rank_properties by blast+

then obtain n⇩1 where n⇩1_def: "∀x ≥ n⇩1. token_succeeds x"
unfolding accept_def MOST_nat_le by blast
define n⇩2 where "n⇩2 = Suc (Max (fail_t ∪ ⋃{succeed_t j | j. j < i}))" (is "_ = Suc (Max ?S)")
define n⇩3 where "n⇩3 = Max ({LEAST m. stable_rank_at x m | x. x < n⇩1 ∧ token_squats x})" (is "_ = Max ?S'")
define n where "n = Max {n⇩1, n⇩2, n⇩3}"

have "finite ?S" and "finite ?S'"
using ‹finite fail› ‹∀j < i. finite (succeed j)›
unfolding finite_fail_t finite_succeed_t by fastforce+

{
fix x
assume "x < n⇩1" "token_squats x"
hence "(LEAST m. stable_rank_at x m) ∈ ?S'" (is "?m ∈ _")
by blast
hence "?m ≤ n⇩3"
using Max.coboundedI[OF ‹finite ?S'›] n⇩3_def by simp
moreover
obtain k where "stable_rank x k"
using ‹x < n⇩1› ‹token_squats x› stable_rank_equiv_token_squats by blast
hence "stable_rank_at x ?m"
by (metis stable_rank_equiv LeastI)
ultimately
have "stable_rank_at x n⇩3"
by (rule stable_rank_at_ge)
hence "∃i. ∀m' ≥ n. rank x m' = Some i"
unfolding n_def stable_rank_at_def by fastforce
}
note Stable = this

have "⋀m j. j < i ⟹ m ∈ succeed_t j ⟹ m < n"
using Max.coboundedI[OF ‹finite ?S›] unfolding n_def n⇩2_def by fastforce
hence Succeed: "⋀m j x. n ≤ m ⟹ token_run x m ∉ F - {q⇩0} ⟹ token_run x (Suc m) ∈ F ⟹ rank x m = Some j ⟹ i ≤ j"
by (metis not_le succeed_t_inclusion)

have "⋀m. m ∈ fail_t ⟹ m < n"
using Max.coboundedI[OF ‹finite ?S›] unfolding n_def n⇩2_def by fastforce
hence Fail: "⋀m x. n ≤ m ⟹ x ≤ m ⟹ sink (token_run x m) ∨ ¬sink (token_run x (Suc m)) ∨ ¬token_run x (Suc m) ∉ F"
using fail_t_inclusion by fastforce

{
fix m x
assume "m ≥ n" "m ≥ x"
moreover
{
assume "token_succeeds x" "token_run x m ∉ F"
then obtain m' where "x ≤ m'" and "token_run x m' ∉ F - {q⇩0}" and "token_run x (Suc m') ∈ F"
using token_run_enter_final_states unfolding token_succeeds_def by meson
moreover
hence "¬sink (token_run x m')"
by (metis Diff_empty Diff_insert0 ‹token_run x m ∉ F› initial_in_F_token_run token_is_not_in_sink)
ultimately
obtain j' where "rank x m' = Some j'"
by simp
moreover
have "m ≤ m'"
by (metis ‹token_run x m ∉ F› token_stays_in_final_states[OF ‹token_run x (Suc m') ∈ F›] add_Suc_right add_Suc_shift less_imp_Suc_add not_le)
moreover
hence "m' ≥ n"
using ‹x ≤ m› ‹m ≥ n› by simp
hence "j' ≥ i"
using Succeed[OF _ ‹token_run x m' ∉ F - {q⇩0}› ‹token_run x (Suc m') ∈ F› ‹rank x m' = Some j'›] by blast
moreover
obtain k where "rank x x = Some k"
using rank_initial[of x] by blast
ultimately
obtain j where "rank x m = Some j"
by (metis rank_continuous[OF ‹rank x x = Some k›, of "m' - x"] ‹x ≤ m'› ‹x ≤ m› diff_le_mono le_add_diff_inverse)
hence "∃j ≥ i. rank x m = Some j"
using rank_monotonic ‹rank x m' = Some j'› ‹j' ≥ i› ‹m ≤ m'›[THEN le_Suc_ex]
}
moreover
{
assume "¬token_succeeds x"
hence "⋀m. token_run x m ∉ F"
unfolding token_succeeds_def by blast
moreover
have "¬(∃j ≥ i. rank x m = Some j)"
proof (cases "token_squats x")
case True
have "x < n⇩1"
using ‹¬token_succeeds x› n⇩1_def by (metis not_le)
then obtain k where "∀m' ≥ n. rank x m' = Some k"
using Stable[OF _ True] by blast
moreover
hence "stable_rank x k"
unfolding stable_rank_def MOST_nat_le by blast
moreover
have "q⇩0 ∉ F"
by (metis ‹⋀m. token_run x m ∉ F› initial_in_F_token_run)
ultimately
― ‹Hence the rank is smaller than i›
have "k < i" and "rank x m = Some k"
using stable_rank_bounded ‹infinite (succeed i)› ‹n ≤ m› by blast+
thus ?thesis
by simp
next
case False
― ‹Then token is already in a sink›
have "sink (token_run x m)"
proof (rule ccontr)
assume "¬sink (token_run x m)"
moreover
obtain m' where "m < m'" and "sink (token_run x m')"
by (metis False token_squats_def le_add2 not_le not_less_eq_eq token_stays_in_sink)
ultimately
obtain m'' where "m ≤ m''" and  "¬sink (token_run x m'')" and "sink (token_run x (Suc m''))"
thus False
by (metis Fail ‹⋀m. token_run x m ∉ F› ‹n ≤ m› ‹x ≤ m› le_trans)
qed
― ‹Hence there is no rank›
thus ?thesis
by simp
qed
ultimately
have "¬(∃j ≥ i. rank x m = Some j) ∧ token_run x m ∉ F"
by blast
}
ultimately
have "(∃j ≥ i. rank x m = Some j) ∨ token_run x m ∈ F ⟷ token_succeeds x"
by (cases "token_succeeds x") (blast, simp)
}
moreover
― ‹By definition of n all tokens @{term "⋀x. x ≥ n"} succeed›
have "⋀m x. m ≥ n ⟹ ¬x ≤ m ⟹ token_succeeds x"
using n_def n⇩1_def by force
ultimately
show ?thesis
unfolding MOST_nat_le not_le[symmetric] by blast
qed

lemma succeeding_states:
assumes "smallest_accepting_rank = Some i"
shows "∀⇩∞n. ∀q. ((∃x ∈ configuration q n. token_succeeds x) ⟶ q ∈ 𝒮 n) ∧ (q ∈ 𝒮 n ⟶ (∀x ∈ configuration q n. token_succeeds x))"
proof -
obtain n where n_def: "⋀m x. m ≥ n ⟹ token_succeeds x = (x > m ∨ (∃j ≥ i. rank x m = Some j) ∨ token_run x m ∈ F)"
using token_smallest_accepting_rank[OF assms] unfolding MOST_nat_le by auto
{
fix m q
assume "m ≥ n" "q ∉ F" "∃x ∈ configuration q m. token_succeeds x"
moreover
then obtain x where "token_run x m = q" and "x ≤ m" and "token_succeeds x"
by auto
ultimately
have "∃j ≥ i. rank x m = Some j"
using n_def by simp
hence "∃j ≥ i. state_rank q m = Some j"
using rank_eq_state_rank ‹x ≤ m› ‹token_run x m = q› by metis
}
moreover
{
fix m q x
assume "m ≥ n" "x ∈ configuration q m"
hence "x ≤ m" and "token_run x m = q"
by simp+
moreover
assume "q ∈ 𝒮 m"
hence "(∃j ≥ i. state_rank q m = Some j) ∨ q ∈ F"
using assms by fastforce
ultimately
have "(∃j ≥ i. rank x m = Some j) ∨ q ∈ F"
using rank_eq_state_rank by presburger
hence "token_succeeds x"
unfolding n_def[OF ‹m ≥ n›] ‹token_run x m = q› by presburger
}
ultimately
show ?thesis
unfolding MOST_nat_le 𝒮.simps assms option.sel by blast
qed

end

end
```