(*  
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹Deterministic Transition Systems›

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

― ‹DTS are realised by functions›

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

subsection ‹Infinite Runs›

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

fun run_t :: "('q,'a) DTS → 'q → 'a word → ('q * 'a * 'q) word"
where
  "run_t δ q₀ w i = (run δ q₀ w i, w i, run δ q₀ w (Suc i))"

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

lemma run_{t_foldl}:
  "run_t Δ q₀ w i = (foldl Δ q₀ (map w [0..<i]), w i, foldl Δ q₀ (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₀ = {run δ q₀ w n | w n. range w ⊆ Σ}"

definition reach_t :: "'a set → ('b, 'a) DTS → 'b → ('b, 'a) transition set"
where
  "reach_t Σ δ q₀ = {run_t δ q₀ w n | w n. range w ⊆ Σ}"

lemma reach_foldl_def:
  assumes "Σ ≠ {}"
  shows "reach Σ δ q₀ = {foldl δ q₀ w | w. set w ⊆ Σ}"
proof -
  {
    fix w assume "set w ⊆ Σ"
    moreover
    obtain a where "a ∈ Σ"
      using ‹Σ ≠ {}› by blast
    ultimately
    have "foldl δ q₀ w = foldl δ q₀ (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₀ w = run δ q₀ 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₀ = {(foldl δ q₀ w, ν, foldl δ q₀ (w@[ν])) | w ν. set w ⊆ Σ ∧ ν ∈ Σ}" (is "?lhs = ?rhs")
proof (cases "Σ ≠ {}")
  case True
    show ?thesis
    proof
      {
        fix w ν assume "set w ⊆ Σ" "ν ∈ Σ"
        moreover
        obtain a where "a ∈ Σ"
          using ‹Σ ≠ {}› by blast
        moreover
        have "w = map (λn. if n < length w then w ! n else if n - length w = 0 then [ν] ! (n - length w) else a) [0..<length w]"
          by (simp add: nth_equalityI)  
        ultimately
        have "foldl δ q₀ w = foldl δ q₀ (prefix (length w) ((w @ [ν]) ⌢ (iter [a])))" 
          and"foldl δ q₀ (w @ [ν]) = foldl δ q₀ (prefix (length (w @ [ν])) ((w @ [ν]) ⌢ (iter [a])))" 
          and "range ((w @ [ν]) ⌢ (iter [a])) ⊆ Σ"
          by (simp_all only: prefix_conc_length conc_conc[symmetric] iter_def)
             (auto simp add: subsequence_def conc_def upt_Suc_append[OF le0])
        moreover
        have "((w @ [ν]) ⌢ (iter [a])) (length w) = ν"
          by (simp add: conc_def)
        ultimately
        have "∃w' n. (foldl δ q₀ w, ν, foldl δ q₀ (w @ [ν])) = run_t δ q₀ 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)
qed (simp add: reach_{t_def})

lemma reach_card_0:
  assumes "Σ ≠ {}"
  shows "infinite (reach Σ δ q₀) ⟷ card (reach Σ δ q₀) = 0"
proof -
  have "{run δ q₀ 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₀) ⟷ card (reach_t Σ δ q₀) = 0"
proof -
  have "{run_t δ q₀ 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₀ w) ⊆ reach Σ δ q₀" 
    and "range (run_t δ q₀ w) ⊆ reach_t Σ δ q₀"
  using assms unfolding reach_def reach_{t_def} by blast+

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

lemma run_{t_finite}:
  assumes "finite (reach Σ δ q₀)"
  assumes "finite Σ"
  assumes "range w ⊆ Σ"
  defines "r ≡ run_t δ q₀ w"
  shows "finite (range r)"
proof -
  let ?S = "(reach Σ δ q₀) × Σ × (reach Σ δ q₀)"
  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₀ = (if Σ ≠ [] then gen_dfs (λq. map (δ q) Σ) Set.insert (∈) {} [q₀] 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₀ = set (
    let
      start = map (λν. (q₀, ν, δ q₀ ν)) Σ;
      succ = λ(_, _, q). (map (λν. (q, ν, δ q ν)) Σ)
    in
      (list_dfs succ [] start))"

lemma Q_{L_reach}:
  assumes "finite (reach (set Σ) δ q₀)"
  shows "Q_L Σ δ q₀ = reach (set Σ) δ q₀"
proof (cases "Σ ≠ []")
  case True
    hence reach_redef: "reach (set Σ) δ q₀ = {foldl δ q₀ 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₀ w" "y ∈ set (map (δ x) Σ)"
      moreover
      then obtain ν where "y = δ x ν" and "ν ∈ set Σ"
        by auto
      ultimately
      have "y = foldl δ q₀ (w@[ν])" and "set (w@[ν]) ⊆ set Σ"
        by simp+
      hence "∃w'. set w' ⊆ set Σ ∧ y = foldl δ q₀ w'"
        by blast
    }
    note extend_run = this
    
    interpret DFS "λq. map (δ q) Σ" "λq. q ∈ reach (set Σ) δ q₀" "λS. S ⊆ reach (set Σ) δ q₀" Set.insert "(∈)" "{}" id
      apply (unfold_locales; auto simp add: 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₀ = foldl δ q₀ []"
      by simp+
    have list_all_init: "list_all (λq. q ∈ reach (set Σ) δ q₀) [q₀]"
      unfolding list_all_iff list.set reach_redef using Nil1 Nil2 by blast

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

    moreover

    have "reachable {q₀} ⊆ Q_L Σ δ q₀"
      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₀ ⊆ reach (set Σ) δ q₀"
      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+
qed (simp add: reach_def Q_{L_def})

lemma δ_{L_reach}: 
  assumes "finite (reach_t (set Σ) δ q₀)"
  shows "δ_L Σ δ q₀ = reach_t (set Σ) δ q₀"
proof -
  {
    fix x w y
    assume "set w ⊆ set Σ" "x = foldl δ q₀ w" "y ∈ set (map (δ x) Σ)"
    moreover
    then obtain ν where "y = δ x ν" and "ν ∈ set Σ"
      by auto
    ultimately
    have "y = foldl δ q₀ (w@[ν])" and "set (w@[ν]) ⊆ set Σ"
      by simp+
    hence "∃w'. set w' ⊆ set Σ ∧ y = foldl δ q₀ 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₀" "λS. set S ⊆ reach_t (set Σ) δ q₀" List.insert "λx xs. x ∈ set xs" "[]" id
    apply (unfold_locales; auto simp add: 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₀ = foldl δ q₀ []"
    by simp+
  have list_all_init: "list_all (λq. q ∈ reach_t (set Σ) δ q₀) (map (λν. (q₀, ν, δ q₀ ν)) Σ)"
    unfolding list_all_iff reach_{t_foldl_def} set_map image_def using Nil2 by fastforce
  
  let ?q₀ = "set (map (λν. (q₀, ν, δ q₀ ν)) Σ)"

  {
    fix q ν q'  
    assume "(q, ν, q') ∈ reach_t (set Σ) δ q₀"
    then obtain w where q_def: "q = foldl δ q₀ w" and q'_def: "q' = foldl δ q₀ (w@[ν])" 
      and "set w ⊆ set Σ" and "ν ∈ set Σ"
      unfolding reach_{t_foldl_def} by blast
    hence "(foldl δ q₀ w, ν, foldl δ q₀ (w@[ν])) ∈ reachable ?q₀"
    proof (induction w arbitrary: q q' ν rule: rev_induct)
      case (snoc ν' w)
        hence "(foldl δ q₀ w, ν', foldl δ q₀ (w@[ν'])) ∈ reachable ?q₀" (is "(?q, ν', ?q') ∈ _")
          and "∧q. δ q ν ∈ set (map (δ q) Σ)"
          and "ν ∈ set Σ"
          by simp+
        then obtain x₀ where 1: "(x₀, (?q, ν', ?q')) ∈ {(x, y). y ∈ set (?succs x)}^*" and 2: "x₀ ∈ ?q₀"
          unfolding reachable_def by auto
        moreover
        have 3: "((?q, ν', ?q'), (?q', ν, δ ?q' ν)) ∈ {(x, y). y ∈ set (?succs x)}"
          using snoc ‹∧q. δ q ν ∈ set (map (δ q) Σ)› by simp
        ultimately
        show ?case
          using rtrancl.rtrancl_into_rtrancl[OF 1 3] 2 unfolding reachable_def foldl_append foldl.simps  by auto
    qed (auto simp add: reachable_def)
    hence "(q, ν, q') ∈ reachable ?q₀"
      by (simp add: q_def q'_def)
  }
  hence "reach_t (set Σ) δ q₀ ⊆ reachable ?q₀"
    by auto
  moreover
  {
    fix y  
    assume "y ∈ reachable ?q₀" 
    then obtain x where "(x, y) ∈ {(x, y). y ∈ set (case x of (_, _, q) → map (λν. (q, ν, δ q ν)) Σ)}^*"
      and "x ∈ ?q₀"
      unfolding reachable_def by auto
    hence "y ∈ reach_t (set Σ) δ q₀"
    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₀ []) bs, b, foldl δ (foldl δ q₀ []) (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₀ ⊆ reach_t (set Σ) δ q₀"
     by blast
  ultimately
  have reachable_redef: "reachable ?q₀ = reach_t (set Σ) δ q₀"
    by blast

  moreover

  have "reachable ?q₀ ⊆ (δ_L Σ δ q₀)"
    using reachable_imp_dfs[OF _ list_all_init] unfolding δ_{L_def} reachable_redef list_dfs_def
    by (simp; blast)

  moreover

  have "δ_L Σ δ q₀ ⊆ reach_t (set Σ) δ q₀"
    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₀ = fst ` reach_t Σ δ q₀"
  unfolding reach_{t_def} reach_def image_def by fastforce

lemma finite_reach:
  "finite (reach_t Σ δ q₀) ==> finite (reach Σ δ q₀)"
  by (simp add: reach_reach_{t_fst})

lemma finite_reach_t:
  assumes "finite (reach Σ δ q₀)"
  assumes "finite Σ"
  shows "finite (reach_t Σ δ q₀)"
proof -
  have "reach_t Σ δ q₀ ⊆ reach Σ δ q₀ × Σ × reach Σ δ q₀"
    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₀)"
  shows "Q_L Σ δ q₀ = fst ` (δ_L Σ δ q₀)"
  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
  "δ₁ × δ₂ = (λ(q₁, q₂) ν. (δ₁ q₁ ν, δ₂ q₂ ν))"  

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

theorem finite_reach_simple_product:
  assumes "finite (reach Σ δ₁ q₁)"
  assumes "finite (reach Σ δ₂ q₂)"
  shows "finite (reach Σ (δ₁ × δ₂) (q₁, q₂))"
proof -
  have "reach Σ (δ₁ × δ₂) (q₁, q₂) ⊆ reach Σ δ₁ q₁ × reach Σ δ₂ q₂"
    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
  "Δ_\<times> δ_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 (Δ_\<times> δ_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₀ k
  defines "ρ ≡ run (Δ_\<times> δ_m) ι_m w"
  defines "ρ' ≡ run (δ_m k) q₀ w"
  assumes "ι_m k = Some q₀"
  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 Σ (Δ_\<times> δ_m) ι_m)"
  using assms(1,2) 
proof (induction "dom ι_m" arbitrary: ι_m) 
  case empty
    hence "ι_m = Map.empty"
      by auto
    hence "∧w i. run (Δ_\<times> δ_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 Σ (Δ_\<times> δ_m) (ι_m(k := None))))"

    have "(reach Σ (Δ_\<times> δ_m) ι_m) ⊆ f ` Reach"
    proof
      fix x
      assume "x ∈ reach Σ (Δ<sub>\</sub><times> δ<sub>m</sub>) ι<sub>m</sub>"
      then obtain w n where x_def: "x = run (Δ<sub>\</sub><times> δ<sub>m</sub>) ι<sub>m</sub> w n" and "range w ⊆ Σ"
        unfolding reach_def by blast
      {
        fix k'
        have "k' ∉ dom ι<sub>m</sub> ==> x k' = run (Δ<sub>\</sub><times> δ<sub>m</sub>) (ι<sub>m</sub>(k := None)) w n k'"
          unfolding x_def dom_def using product_run_None[of _ _ δ<sub>m</sub>] by simp
        moreover
        have "k' ∈ dom ι<sub>m</sub> - {k} ==> x k' = run (Δ<sub>\</sub><times> δ<sub>m</sub>) (ι<sub>m</sub>(k := None)) w n k'"
          unfolding x_def dom_def using product_run_Some[of _ _ _ δ<sub>m</sub>] by auto
        ultimately
        have "k' ≠ k ==> x k' = run (Δ<sub>\</sub><times> δ<sub>m</sub>) (ι<sub>m</sub>(k := None)) w n k'"
          by blast
      }
      hence "x(k := None) = run (Δ<sub>\</sub><times> δ<sub>m</sub>) (ι<sub>m</sub>(k := None)) w n"
        using product_run_None[of _ _ δ<sub>m</sub>] by auto
      moreover
      have "x k = Some (run (δ<sub>m</sub> k) (the (ι<sub>m</sub> k)) w n)"
        unfolding x_def using product_run_Some[of ι<sub>m</sub> k _ δ<sub>m</sub>] 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 (δ<sub>m</sub> k) (the (ι<sub>m</sub> k)) w n)› by auto 
      ultimately
      show "x ∈ f ` Reach"
         by simp
    qed
    moreover
    have "finite (reach Σ (Δ_\<times> δ_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 δ₁ δ₂ w q₁ q₂
  defines "ρ ≡ run_t (δ₁ × δ₂) (q₁, q₂) w"
  defines "ρ₁ ≡ run_t δ₁ q₁ w"
  defines "ρ₂ ≡ run_t δ₂ q₂ w"
  shows product_run_project_fst: "project_transition_fst (ρ i) = ρ₁ i" 
    and product_run_project_snd: "project_transition_snd (ρ i) = ρ₂ i"
    and product_run_embed_fst: "ρ i ∈ embed_transition_fst (ρ₁ i)"
    and product_run_embed_snd: "ρ i ∈ embed_transition_snd (ρ₂ i)"
  unfolding assms run_t.simps simple_product_run by simp_all

lemma 
  fixes δ₁ δ₂ w q₁ q₂
  defines "ρ ≡ run_t (δ₁ × δ₂) (q₁, q₂) w"
  defines "ρ₁ ≡ run_t δ₁ q₁ w"
  defines "ρ₂ ≡ run_t δ₂ q₂ w"
  assumes "finite (range ρ)"
  shows product_run_finite_fst: "finite (range ρ₁)"
    and product_run_finite_snd: "finite (range ρ₂)"
proof -
  have "∧k. project_transition_fst (ρ k) = ρ₁ k"
    and "∧k. project_transition_snd (ρ k) = ρ₂ k"
    unfolding assms product_run_project_fst product_run_project_snd by simp+
  hence "project_transition_fst ` range ρ = range ρ<sub>1</sub>"
    and "project_transition_snd ` range ρ = range ρ₂"
    using range_composition[symmetric, of project_transition_fst ρ]
    using range_composition[symmetric, of project_transition_snd ρ] by presburger+
  thus "finite (range ρ₁)" and "finite (range ρ₂)"
    using assms finite_imageI by metis+
qed

lemma 
  fixes δ₁ δ₂ w q₁ q₂
  defines "ρ ≡ run_t (δ₁ × δ₂) (q₁, q₂) w"
  defines "ρ₁ ≡ run_t δ₁ q₁ w"
  assumes "finite (range ρ)"
  shows product_run_project_limit_fst: "project_transition_fst ` limit ρ = limit ρ<sub>1</sub>"
    and product_run_embed_limit_fst: "limit ρ ⊆ ∪ (embed_transition_fst ` (limit ρ₁))"
proof -
  have "finite (range ρ₁)"
    using assms product_run_finite_fst 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. project_transition_fst (suffix i ρ k) = (suffix i ρ₁ k)"
    by (simp only: assms run_t.simps) (metis ρ₁_def product_run_project_fst suffix_nth) 
  hence "project_transition_fst ` range (suffix i ρ) = (range (suffix i ρ<sub>1</sub>))"
    using range_composition[symmetric, of "project_transition_fst" "suffix i ρ"] by presburger
  moreover
  have "∧k. (suffix i ρ k) ∈ embed_transition_fst (suffix i ρ<sub>1</sub> k)"
    using assms product_run_embed_fst by simp
  ultimately
  show "project_transition_fst ` limit ρ = limit ρ₁" 
    and "limit ρ ⊆ ∪ (embed_transition_fst ` (limit ρ₁))"
    by auto
qed 

lemma 
  fixes δ₁ δ₂ w q₁ q₂
  defines "ρ ≡ run_t (δ₁ × δ₂) (q₁, q₂) w"
  defines "ρ₂ ≡ run_t δ₂ q₂ w"
  assumes "finite (range ρ)"
  shows product_run_project_limit_snd: "project_transition_snd ` limit ρ = limit ρ<sub>2</sub>"
    and product_run_embed_limit_snd: "limit ρ ⊆ ∪ (embed_transition_snd ` (limit ρ₂))"
proof -
  have "finite (range ρ₂)"
    using assms product_run_finite_snd 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. project_transition_snd (suffix i ρ k) = (suffix i ρ₂ k)"
    by (simp only: assms run_t.simps) (metis ρ₂_def product_run_project_snd suffix_nth) 
  hence "project_transition_snd ` range ((suffix i ρ)) = (range (suffix i ρ<sub>2</sub>))"
    using range_composition[symmetric, of "project_transition_snd" "(suffix i ρ)"] by presburger
  moreover
  have "∧k. (suffix i ρ k) ∈ embed_transition_snd (suffix i ρ<sub>2</sub> k)"
    using assms product_run_embed_snd by simp
  ultimately
  show "project_transition_snd ` limit ρ = limit ρ₂" 
    and "limit ρ ⊆ ∪ (embed_transition_snd ` (limit ρ₂))"
    by auto
qed 

lemma 
  fixes δ₁ δ₂ w q₁ q₂
  defines "ρ ≡ run_t (δ₁ × δ₂) (q₁, q₂) w"
  defines "ρ₁ ≡ run_t δ₁ q₁ w"
  defines "ρ₂ ≡ run_t δ₂ q₂ w"
  assumes "finite (range ρ)"
  shows product_run_embed_limit_finiteness_fst: "limit ρ ∩ (∪ (embed_transition_fst ` S)) = {} ⟷ limit ρ<sub>1</sub> ∩ S = {}" (is "?thesis1")
    and product_run_embed_limit_finiteness_snd: "limit ρ ∩ (∪ (embed_transition_snd ` S')) = {} ⟷ limit ρ₂ ∩ 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
  "\<upharpoonleft>_x (S, S') = (∪(↿_x ` S), ∪(↿<sub>x</sub> ` S'))" 

fun project_pair :: "'a → (('a ⇀ 'b, 'c) transition set × ('a ⇀ 'b, 'c) transition set) → (('b, 'c) transition set × ('b, 'c) transition set)" (‹\⇃_{_}›)
where
  "\<downharpoonleft>_x (S, S') = (⇃_x ` S, ⇃<sub>x</sub> ` 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₀ 
  fixes x :: "'a"
  defines "ρ ≡ run_t (Δ_\<times> δ_m) ι_m w"
  defines "ρ' ≡ run_t (δ_m x) q₀ w"
  assumes "ι_m x = Some q₀"
  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₀ x
  defines "ρ ≡ run_t (Δ_\<times> δ_m) ι_m w"
  defines "ρ' ≡ run_t (δ_m x) q₀ w"
  assumes "ι_m x = Some q₀"
  assumes "finite (range ρ)"
  shows product_run_project_limit: "⇃_x ` limit ρ = limit ρ'" 
    and product_run_embed_limit: "limit ρ ⊆ ∪ (↿<sub>x</sub> ` (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 "⇃<sub>x</sub>" "(suffix i ρ)"] by presburger
  moreover
  have "∧k. (suffix i ρ k) ∈ ↿<sub>x</sub> (suffix i ρ' k)"
    using assms product_run_embed[of _ _ _ δ<sub>m</sub>] by simp
  ultimately
  show "⇃<sub>x</sub> ` limit ρ = limit ρ'" and "limit ρ ⊆ ∪ (↿_x ` (limit ρ'))"
    by auto
qed

lemma product_run_embed_limit_finiteness:
  fixes ι_m δ_m w q₀ k
  defines "ρ ≡ run_t (Δ_\<times> δ_m) ι_m w"
  defines "ρ' ≡ run_t (δ_m k) q₀ w"
  assumes "ι_m k = Some q₀"
  assumes "finite (range ρ)"
  shows "limit ρ ∩ (∪ (↿_k ` S)) = {} ⟷ limit ρ' ∩ S = {}"
  (is "?lhs ⟷ ?rhs")
proof -
  have "⇃<sub>k</sub> ` limit ρ ∩ S ≠ {} ⟶ limit ρ ∩ (∪ (↿_k ` S)) ≠ {}"
  proof
    assume "⇃<sub>k</sub> ` 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 ι<sub>m</sub> , 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') ∈ ∪ (↿<sub>k</sub> ` S)"
      using ‹(q, ν, q') ∈ S› by force
    ultimately
    show "limit ρ ∩ (∪ (↿_k ` S)) ≠ {}"
      by blast
  qed
  hence "?lhs ⟷ ⇃<sub>k</sub> ` 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 (↑Δ_\<times> δ_m) ι_m w i) k = None"
  by (transfer; insert product_run_None)

lemma product_abs_run_Some:
  "Mapping.lookup ι_m k = Some q₀ ==> Mapping.lookup (run (↑Δ_\<times> δ_m) ι_m w i) k = Some (run (δ_m k) q₀ 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 Σ (↑Δ_\<times> δ_m) ι_m)"
  using assms by (transfer; blast intro: finite_reach_product)

end