# Theory Preliminaries2

(*
Author:      Salomon Sickert
*)

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 i⇩1 i⇩2 where "⋀j. j ≥ i⇩1 ⟹ ∀x ∈ S. P x j"
and "⋀j. j ≥ i⇩2 ⟹ P x j"
unfolding MOST_nat_le by auto
hence "⋀j. j ≥ max i⇩1 i⇩2 ⟹ ∀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
*)

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 ∧ (∀x∈B. m x = (m (a := None)) x)"
by simp
thus ?thesis
by blast
qed

end


# Theory Mapping2

(*
Author:      Salomon Sickert
*)

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"

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 ∧ (∀k∈set ks. the (m k) ∈ set (V k))}}"
let ?r = "{m. dom m = set (k # ks) ∧ (∀k∈set (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 ∧ (∀k∈set ks. the (Mapping.lookup m k) ∈ set (V k))}}
= {m. Mapping.keys m = set (k # ks) ∧ (∀k∈set (k # ks). the (Mapping.lookup m k) ∈ set (V k))}"
by (transfer; blast)
thus ?case

end


# Theory DTS

(*
Author:      Salomon Sickert
*)

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 δ q⇩0 w 0 = q⇩0"
| "run δ q⇩0 w (Suc i) = δ (run δ q⇩0 w i) (w i)"

fun run⇩t :: "('q,'a) DTS ⇒ 'q ⇒ 'a word ⇒ ('q * 'a * 'q) word"
where
"run⇩t δ q⇩0 w i = (run δ q⇩0 w i, w i, run δ q⇩0 w (Suc i))"

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

lemma run⇩t_foldl:
"run⇩t Δ q⇩0 w i = (foldl Δ q⇩0 (map w [0..<i]), w i, foldl Δ q⇩0 (map w [0..<Suc i]))"
unfolding run⇩t.simps run_foldl ..

subsection ‹Reachable States and Transitions›

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

definition reach⇩t :: "'a set ⇒ ('b, 'a) DTS ⇒ 'b ⇒ ('b, 'a) transition set"
where
"reach⇩t Σ δ q⇩0 = {run⇩t δ q⇩0 w n | w n. range w ⊆ Σ}"

lemma reach_foldl_def:
assumes "Σ ≠ {}"
shows "reach Σ δ q⇩0 = {foldl δ q⇩0 w | w. set w ⊆ Σ}"
proof -
{
fix w assume "set w ⊆ Σ"
moreover
obtain a where "a ∈ Σ"
using ‹Σ ≠ {}› by blast
ultimately
have "foldl δ q⇩0 w = foldl δ q⇩0 (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 δ q⇩0 w = run δ q⇩0 w' n ∧ range w' ⊆ Σ"
unfolding run_foldl subsequence_def by blast
}
thus ?thesis
by (fastforce simp add: reach_def run_foldl)
qed

lemma reach⇩t_foldl_def:
"reach⇩t Σ δ q⇩0 = {(foldl δ q⇩0 w, ν, foldl δ q⇩0 (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]"
ultimately
have "foldl δ q⇩0 w = foldl δ q⇩0 (prefix (length w) ((w @ [ν]) ⌢ (iter [a])))"
and"foldl δ q⇩0 (w @ [ν]) = foldl δ q⇩0 (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) = ν"
ultimately
have "∃w' n. (foldl δ q⇩0 w, ν, foldl δ q⇩0 (w @ [ν])) = run⇩t δ q⇩0 w' n ∧ range w' ⊆ Σ"
by (metis run⇩t_foldl length_append_singleton subsequence_def)
}
thus "?lhs ⊇ ?rhs"
unfolding reach⇩t_def run⇩t.simps by blast
qed (unfold reach⇩t_def run⇩t_foldl, fastforce simp add: upt_Suc_append)

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

lemma reach⇩t_card_0:
assumes "Σ ≠ {}"
shows "infinite (reach⇩t Σ δ q⇩0) ⟷ card (reach⇩t Σ δ q⇩0) = 0"
proof -
have "{run⇩t δ q⇩0 w n | w n. range w ⊆ Σ} ≠ {}"
using assms by fast
thus ?thesis
unfolding reach⇩t_def card_eq_0_iff by blast
qed

subsubsection ‹Relation to runs›

lemma run_subseteq_reach:
assumes "range w ⊆ Σ"
shows "range (run δ q⇩0 w) ⊆ reach Σ δ q⇩0"
and "range (run⇩t δ q⇩0 w) ⊆ reach⇩t Σ δ q⇩0"
using assms unfolding reach_def reach⇩t_def by blast+

lemma limit_subseteq_reach:
assumes "range w ⊆ Σ"
shows "limit (run δ q⇩0 w) ⊆ reach Σ δ q⇩0"
and "limit (run⇩t δ q⇩0 w) ⊆ reach⇩t Σ δ q⇩0"
using run_subseteq_reach[OF assms] limit_in_range by fast+

lemma run⇩t_finite:
assumes "finite (reach Σ δ q⇩0)"
assumes "finite Σ"
assumes "range w ⊆ Σ"
defines "r ≡ run⇩t δ q⇩0 w"
shows "finite (range r)"
proof -
let ?S = "(reach Σ δ q⇩0) × Σ × (reach Σ δ q⇩0)"
have "⋀i. w i ∈ Σ" and "⋀i. set (map w [0..<i]) ⊆ Σ" and "Σ ≠ {}"
using ‹range w ⊆ Σ› by auto
hence "⋀n. r n ∈ ?S"
unfolding run⇩t.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 Q⇩L :: "'a list ⇒ ('b, 'a) DTS ⇒ 'b ⇒ 'b set"
where
"Q⇩L Σ δ q⇩0 = (if Σ ≠ [] then gen_dfs (λq. map (δ q) Σ) Set.insert (∈) {} [q⇩0] 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 Σ δ q⇩0 = set (
let
start = map (λν. (q⇩0, ν, δ q⇩0 ν)) Σ;
succ = λ(_, _, q). (map (λν. (q, ν, δ q ν)) Σ)
in
(list_dfs succ [] start))"

lemma Q⇩L_reach:
assumes "finite (reach (set Σ) δ q⇩0)"
shows "Q⇩L Σ δ q⇩0 = reach (set Σ) δ q⇩0"
proof (cases "Σ ≠ []")
case True
hence reach_redef: "reach (set Σ) δ q⇩0 = {foldl δ q⇩0 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 δ q⇩0 w" "y ∈ set (map (δ x) Σ)"
moreover
then obtain ν where "y = δ x ν" and "ν ∈ set Σ"
by auto
ultimately
have "y = foldl δ q⇩0 (w@[ν])" and "set (w@[ν]) ⊆ set Σ"
by simp+
hence "∃w'. set w' ⊆ set Σ ∧ y = foldl  δ q⇩0 w'"
by blast
}
note extend_run = this

interpret DFS "λq. map (δ q) Σ" "λq. q ∈ reach (set Σ) δ q⇩0" "λS. S ⊆ reach (set Σ) δ q⇩0" 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: "q⇩0 = foldl δ q⇩0 []"
by simp+
have list_all_init: "list_all (λq. q ∈ reach (set Σ) δ q⇩0) [q⇩0]"
unfolding list_all_iff list.set reach_redef using Nil1 Nil2 by blast

have "reach (set Σ) δ q⇩0 ⊆ reachable {q⇩0}"
proof rule
fix x
assume "x ∈ reach (set Σ) δ q⇩0"
then obtain w where x_def: "x = foldl δ q⇩0 w" and "set w ⊆ set Σ"
unfolding reach_redef by blast
hence "foldl δ q⇩0 w ∈ reachable {q⇩0}"
proof (induction w arbitrary: x rule: rev_induct)
case (snoc ν w)
hence "foldl δ q⇩0 w ∈ reachable {q⇩0}" and "δ (foldl δ q⇩0 w) ν ∈ set (map (δ (foldl δ q⇩0 w)) Σ)"
by simp+
thus ?case
thus "x ∈ reachable {q⇩0}"
qed
moreover
have "reachable {q⇩0} ⊆ reach (set Σ) δ q⇩0"
proof rule
fix x
assume "x ∈ reachable {q⇩0}"
hence "(q⇩0, x) ∈ {(x, y). y ∈ set (map (δ x) Σ)}⇧*"
unfolding reachable_def by blast
thus "x ∈ reach (set Σ) δ q⇩0"
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 {q⇩0} = reach (set Σ) δ q⇩0"
by blast

moreover

have "reachable {q⇩0} ⊆ Q⇩L Σ δ q⇩0"
using reachable_imp_dfs[OF _ list_all_init] unfolding list.set reachable_redef
unfolding  reach_redef Q⇩L_def using ‹Σ ≠ []› by auto

moreover

have "Q⇩L Σ δ q⇩0 ⊆ reach (set Σ) δ q⇩0"
using dfs_invariant[of "{}", OF _ list_all_init]
by (auto simp add: reach_redef Q⇩L_def)

ultimately
show ?thesis
using ‹Σ ≠ []› dfs_invariant[of "{}", OF _ list_all_init] by simp+

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

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

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

have Nil1: "set [] ⊆ set Σ" and Nil2: "q⇩0 = foldl δ q⇩0 []"
by simp+
have list_all_init: "list_all (λq. q ∈ reach⇩t (set Σ) δ q⇩0) (map (λν. (q⇩0, ν, δ q⇩0 ν)) Σ)"
unfolding list_all_iff reach⇩t_foldl_def set_map image_def using Nil2 by fastforce

let ?q⇩0 = "set (map (λν. (q⇩0, ν, δ q⇩0 ν)) Σ)"

{
fix q ν q'
assume "(q, ν, q') ∈ reach⇩t (set Σ) δ q⇩0"
then obtain w where q_def: "q = foldl δ q⇩0 w" and q'_def: "q' = foldl δ q⇩0 (w@[ν])"
and "set w ⊆ set Σ" and "ν ∈ set Σ"
unfolding reach⇩t_foldl_def by blast
hence "(foldl δ q⇩0 w, ν, foldl δ q⇩0 (w@[ν])) ∈ reachable ?q⇩0"
proof (induction w arbitrary: q q' ν rule: rev_induct)
case (snoc ν' w)
hence "(foldl δ q⇩0 w, ν', foldl δ q⇩0 (w@[ν'])) ∈ reachable ?q⇩0" (is "(?q, ν', ?q') ∈ _")
and "⋀q. δ q ν ∈ set (map (δ q) Σ)"
and "ν ∈ set Σ"
by simp+
then obtain x⇩0 where 1: "(x⇩0, (?q, ν', ?q')) ∈ {(x, y). y ∈ set (?succs x)}⇧*" and 2: "x⇩0 ∈ ?q⇩0"
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
hence "(q, ν, q') ∈ reachable ?q⇩0"
}
hence "reach⇩t (set Σ) δ q⇩0 ⊆ reachable ?q⇩0"
by auto
moreover
{
fix y
assume "y ∈ reachable ?q⇩0"
then obtain x where "(x, y) ∈ {(x, y). y ∈ set (case x of (_, _, q) ⇒ map (λν. (q, ν, δ q ν)) Σ)}⇧*"
and "x ∈ ?q⇩0"
unfolding reachable_def by auto
hence "y ∈ reach⇩t (set Σ) δ q⇩0"
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 δ q⇩0 []) bs, b, foldl δ (foldl δ q⇩0 []) (bs @ [b])) | bs b. set bs ⊆ set Σ ∧ b ∈ set Σ}"
using base by (metis (no_types) Nil2 list_all_init reach⇩t_foldl_def)
thus ?case
unfolding reach⇩t_foldl_def by auto
next
case (step x' y')
thus ?case using succsr_def succsr_isNode by blast
qed
}
hence "reachable ?q⇩0 ⊆ reach⇩t (set Σ) δ q⇩0"
by blast
ultimately
have reachable_redef: "reachable ?q⇩0 = reach⇩t (set Σ) δ q⇩0"
by blast

moreover

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

moreover

have "δ⇩L Σ δ q⇩0 ⊆ reach⇩t (set Σ) δ q⇩0"
using dfs_invariant[of "[]", OF _ list_all_init]
by (auto simp add: reach⇩t_foldl_def δ⇩L_def list_dfs_def)

ultimately
show ?thesis
by simp
qed

lemma reach_reach⇩t_fst:
"reach Σ δ q⇩0 = fst  reach⇩t Σ δ q⇩0"
unfolding reach⇩t_def reach_def image_def by fastforce

lemma finite_reach:
"finite (reach⇩t Σ δ q⇩0) ⟹ finite (reach Σ δ q⇩0)"

lemma finite_reach⇩t:
assumes "finite (reach Σ δ q⇩0)"
assumes "finite Σ"
shows "finite (reach⇩t Σ δ q⇩0)"
proof -
have "reach⇩t Σ δ q⇩0 ⊆ reach Σ δ q⇩0 × Σ × reach Σ δ q⇩0"
unfolding reach⇩t_def reach_def run⇩t.simps by blast
thus ?thesis
using assms finite_subset by blast
qed

lemma Q⇩L_eq_δ⇩L:
assumes "finite (reach⇩t (set Σ) δ q⇩0)"
shows "Q⇩L Σ δ q⇩0 = fst  (δ⇩L Σ δ q⇩0)"
unfolding set_map δ⇩L_reach[OF assms] Q⇩L_reach[OF finite_reach[OF assms]] reach_reach⇩t_fst ..

subsection ‹Product of DTS›

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

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

theorem finite_reach_simple_product:
assumes "finite (reach Σ δ⇩1 q⇩1)"
assumes "finite (reach Σ δ⇩2 q⇩2)"
shows "finite (reach Σ (δ⇩1 × δ⇩2) (q⇩1, q⇩2))"
proof -
have "reach Σ (δ⇩1 × δ⇩2) (q⇩1, q⇩2) ⊆ reach Σ δ⇩1 q⇩1 × reach Σ δ⇩2 q⇩2"
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 q⇩0 k
defines "ρ ≡ run (Δ⇩× δ⇩m) ι⇩m w"
defines "ρ' ≡ run (δ⇩m k) q⇩0 w"
assumes "ι⇩m k = Some q⇩0"
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 q⇩1 q⇩2
defines "ρ ≡ run⇩t (δ⇩1 × δ⇩2) (q⇩1, q⇩2) w"
defines "ρ⇩1 ≡ run⇩t δ⇩1 q⇩1 w"
defines "ρ⇩2 ≡ run⇩t δ⇩2 q⇩2 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 run⇩t.simps simple_product_run by simp_all

lemma
fixes δ⇩1 δ⇩2 w q⇩1 q⇩2
defines "ρ ≡ run⇩t (δ⇩1 × δ⇩2) (q⇩1, q⇩2) w"
defines "ρ⇩1 ≡ run⇩t δ⇩1 q⇩1 w"
defines "ρ⇩2 ≡ run⇩t δ⇩2 q⇩2 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 q⇩1 q⇩2
defines "ρ ≡ run⇩t (δ⇩1 × δ⇩2) (q⇩1, q⇩2) w"
defines "ρ⇩1 ≡ run⇩t δ⇩1 q⇩1 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 run⇩t.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 q⇩1 q⇩2
defines "ρ ≡ run⇩t (δ⇩1 × δ⇩2) (q⇩1, q⇩2) w"
defines "ρ⇩2 ≡ run⇩t δ⇩2 q⇩2 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 run⇩t.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 q⇩1 q⇩2
defines "ρ ≡ run⇩t (δ⇩1 × δ⇩2) (q⇩1, q⇩2) w"
defines "ρ⇩1 ≡ run⇩t δ⇩1 q⇩1 w"
defines "ρ⇩2 ≡ run⇩t δ⇩2 q⇩2 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 q⇩0
fixes x :: "'a"
defines "ρ ≡ run⇩t (Δ⇩× δ⇩m) ι⇩m w"
defines "ρ' ≡ run⇩t (δ⇩m x) q⇩0 w"
assumes "ι⇩m x = Some q⇩0"
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 q⇩0 x
defines "ρ ≡ run⇩t (Δ⇩× δ⇩m) ι⇩m w"
defines "ρ' ≡ run⇩t (δ⇩m x) q⇩0 w"
assumes "ι⇩m x = Some q⇩0"
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 q⇩0 k
defines "ρ ≡ run⇩t (Δ⇩× δ⇩m) ι⇩m w"
defines "ρ' ≡ run⇩t (δ⇩m k) q⇩0 w"
assumes "ι⇩m k = Some q⇩0"
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 q⇩0 ⟹ Mapping.lookup (run (↑Δ⇩× δ⇩m) ι⇩m w i) k = Some (run (δ⇩m k) q⇩0 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
*)

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›
q⇩0 :: "'b"
fixes
― ‹$\omega$-Word›
w :: "'a word"
begin

definition sink :: "'b ⇒ bool"
where
"sink q ≡ (q⇩0 ≠ q) ∧ (∀ν ∈ Σ. δ q ν = q)"

declare sink_def [code]

fun token_run :: "nat ⇒ nat ⇒ 'b"
where
"token_run x n = run δ q⇩0 (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 Σ δ q⇩0 - {q. sink q})"

subsubsection ‹Iterative Computation of State-Ranks›

fun initial :: "'b ⇒ nat option"
where
"initial q = (if q = q⇩0 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 = q⇩0 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 Σ δ q⇩0)"
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 = q⇩0"
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 δ q⇩0 (suffix x w) (Suc (n - x)) = run δ q⇩0 (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)

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 q⇩0 (Suc n)"
shows "x = Suc n ∨ (∃q'. q⇩0 = δ q' (w n) ∧ x ∈ configuration q' n)"
using assms configuration_rev_step' by metis

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

lemma configuration_rev_step:
assumes "q ≠ q⇩0"
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 ≠ q⇩0"
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 = q⇩0 then {Suc n} else {}) "
using configuration_step_eq configuration_step_eq_q⇩0 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
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)"

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]
moreover
have "older_seniors x n = older_seniors x (n + m)"
using Suc.prems(5) older_seniors_stable[OF ‹x ≤ n›]
moreover
hence "older_seniors x (n + m) = older_seniors x (Suc (n + m))"
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
finally
show ?case
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
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
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 "q⇩0 = run δ q⇩0 (λ_. a) 0"
by auto
hence "q⇩0 ∈ reach Σ δ q⇩0"
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 Σ δ q⇩0 - {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 Σ δ q⇩0 - 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"

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"
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
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
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
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
ultimately
have "rank x (n + m) = Some j"
by simp
}
ultimately
show ?lhs
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 q⇩0 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 Σ δ q⇩0 ⟶ f x = None) ∧
(∀x. x ∈ reach Σ δ q⇩0 ⟶ f x ∈ {None} ∪ Some  {0..<max_rank})}"
proof -
{
fix x
assume "x ∉ reach Σ δ q⇩0"
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 = q⇩0 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 = q⇩0") 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 = q⇩0", 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 = q⇩0"
using oldest_token_bounded[of _ n "Suc n"]
by (cases "q = q⇩0") auto

lemma pre_oldest_configuration_initial_state_2:
"q = q⇩0 ⟹ 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 = q⇩0"
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 "r⇩q ∈ pre_ranks r ν q - {max_rank}"
obtains q' where "r q' = Some r⇩q" and "q = δ q' ν"
using assms by (cases "q = q⇩0", 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 = q⇩0"
using state_rank_upper_bound by (cases "q = q⇩0") auto

lemma pre_ranks_initial_state_2:
"q = q⇩0 ⟹ 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 ≠ q⇩0")
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 = q⇩0"
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 = q⇩0"
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 "q⇩0 = 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 "q⇩0 = 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)) = (∀a∈pre_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 = q⇩0") apply auto 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 ot⇩q
assume "ot⇩q ∈ pre_oldest_tokens q n - {Suc n}"
then obtain q' where "oldest_token q' n = Some ot⇩q" 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 r⇩q where "state_rank q' n = Some r⇩q"
unfolding assms state_rank.simps using ‹oldest_token q' n = Some ot⇩q›
by (metis oldest_token.simps option.distinct(2))
moreover
hence "r⇩q ∈ pre_ranks r (w n) q"
using ‹q = δ q' (w n)›
unfolding pre_ranks.simps assms by blast
hence "?min_j ≤ r⇩q"
using Min.coboundedI[OF pre_ranks_finite] unfolding assms by blast
hence "?min_i < r⇩q"
using ‹?lhs› by linarith
hence "ot' < ot⇩q"
using state_rank_oldest_token[OF ‹state_rank p' n = Some ?min_i› ‹state_rank q' n = Some r⇩q› ‹oldest_token p' n = Some ot'› ‹oldest_token q' n = Some ot⇩q›]
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_r⇩p where "min_r⇩p = Min (pre_ranks r (w n) p)"
hence "min_r⇩p ∈ pre_ranks r (w n) p"
using pre_ranks_Min_in assms pre_ranks_tokens by simp
hence *: "min_r⇩p < max_rank"
proof (cases min_r⇩p 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_r⇩p_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_r⇩p ∈ {0..max_rank}"
using pre_ranks_range ‹min_r⇩p ∈ pre_ranks r (w n) p›
unfolding r_def ..
ultimately
show ?thesis
by simp
qed simp
moreover
from * have "min_r⇩p ∈ pre_ranks r (w n) p - {max_rank}"
using ‹min_r⇩p ∈ pre_ranks r (w n) p› by simp
then obtain p' where "r p' = Some min_r⇩p" 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_r⇩p_def[symmetric] ot_p_def[symmetric] by (metis r_def)
{
fix r⇩q
assume "r⇩q ∈ pre_ranks r (w n) q - {max_rank}"
then obtain q' where q': "r q' = Some r⇩q" "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_r⇩p < r⇩q"
using state_rank_oldest_token ‹r p' = Some min_r⇩p› ‹oldest_token p' n = Some ot_p›
unfolding assms by blast
}
ultimately
show ?lhs
using pre_ranks_Min unfolding min_r⇩p_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
*)

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