(* 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⇩_{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]" by (simp add: nth_equalityI) 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) = ν" by (simp add: conc_def) 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) qed (simp add: reach⇩_{t}_def) 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 by (simp add: rtrancl.rtrancl_into_rtrancl reachable_def) qed (simp add: reachable_def) thus "x ∈ reachable {q⇩_{0}}" by (simp add: x_def) 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+ qed (simp add: reach_def Q⇩_{L}_def) 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 qed (auto simp add: reachable_def) hence "(q, ν, q') ∈ reachable ?q⇩_{0}" by (simp add: q_def q'_def) } 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})" by (simp add: reach_reach⇩_{t}_fst) 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