# Theory DTS

theory DTS
imports Omega_Words_Fun Mapping2 DFS
```(*
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
```