# Theory Convergence_Graph

```section ‹Convergence Graphs›

text ‹This theory introduces the invariants required for the initialisation, insertion, lookup, and
merge operations on convergence graphs.›

theory Convergence_Graph
imports Convergence "../Prefix_Tree"
begin

lemma after_distinguishes_diverge :
assumes "observable M1"
and     "observable M2"
and     "minimal M1"
and     "minimal M2"
and     "α ∈ L M1"
and     "β ∈ L M1"
and     "γ ∈ set (after T1 α) ∩ set (after T1 β)"
and     "distinguishes M1 (after_initial M1 α) (after_initial M1 β) γ"
and     "L M1 ∩ set T1 = L M2 ∩ set T1"
shows "¬converge M2 α β"
proof
have "γ ≠ []"
using assms(5,6,8)
by (metis after_distinguishes_language append_Nil2 assms(1))
then have "α ∈ set T1" and "β ∈ set T1"
using assms(7) after_set_Cons[of γ]
by auto

assume "converge M2 α β"
moreover have "α ∈ L M2"
using assms(5,9) ‹α ∈ set T1› by blast
moreover have "β ∈ L M2"
using assms(6,9) ‹β ∈ set T1› by blast
ultimately have "(after_initial M2 α) = (after_initial M2 β)"
using convergence_minimal[OF assms(4,2)]
by blast
then have "α@γ ∈ L M2 = (β@γ ∈ L M2)"
using ‹converge M2 α β› assms(2) converge_append_language_iff by blast
moreover have "(α@γ ∈ L M1) ≠ (β@γ ∈ L M1)"
using after_distinguishes_language[OF assms(1,5,6,8)] .
moreover have "α@γ ∈ set T1" and "β@γ ∈ set T1"
using assms(7) unfolding after_set
by (metis IntE append_Nil2 assms(5) assms(6) calculation(2) insertE mem_Collect_eq)+
ultimately show False
using assms(9)
by blast
qed

subsection ‹Required Invariants on Convergence Graphs›

definition convergence_graph_lookup_invar :: "('a,'b,'c) fsm ⇒ ('e,'b,'c) fsm ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
'd ⇒
bool"
where
"convergence_graph_lookup_invar M1 M2 cg_lookup G = (∀ α .  α ∈ L M1 ⟶ α ∈ L M2 ⟶ α ∈ list.set (cg_lookup G α) ∧ (∀ β . β ∈ list.set (cg_lookup G α) ⟶ converge M1 α β ∧ converge M2 α β))"

lemma convergence_graph_lookup_invar_simp:
assumes "convergence_graph_lookup_invar M1 M2 cg_lookup G"
and     "α ∈ L M1" and "α ∈ L M2"
and     "β ∈ list.set (cg_lookup G α)"
shows "converge M1 α β" and "converge M2 α β"
using assms unfolding convergence_graph_lookup_invar_def by blast+

definition convergence_graph_initial_invar :: "('a,'b,'c) fsm ⇒ ('e,'b,'c) fsm ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
(('a,'b,'c) fsm ⇒ ('b×'c) prefix_tree ⇒ 'd) ⇒
bool"
where
"convergence_graph_initial_invar M1 M2 cg_lookup cg_initial = (∀ T . (L M1 ∩ set T = (L M2 ∩ set T)) ⟶ finite_tree T ⟶ convergence_graph_lookup_invar M1 M2 cg_lookup (cg_initial M1 T))"

definition convergence_graph_insert_invar :: "('a,'b,'c) fsm ⇒ ('e,'b,'c) fsm ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
('d ⇒ ('b×'c) list ⇒ 'd) ⇒
bool"
where
"convergence_graph_insert_invar M1 M2 cg_lookup cg_insert = (∀ G γ . γ ∈ L M1 ⟶ γ ∈ L M2 ⟶ convergence_graph_lookup_invar M1 M2 cg_lookup G ⟶ convergence_graph_lookup_invar M1 M2 cg_lookup (cg_insert G γ))"

definition convergence_graph_merge_invar :: "('a,'b,'c) fsm ⇒ ('e,'b,'c) fsm ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list list) ⇒
('d ⇒ ('b×'c) list ⇒ ('b×'c) list ⇒ 'd) ⇒
bool"
where
"convergence_graph_merge_invar M1 M2 cg_lookup cg_merge = (∀ G γ γ'. converge M1 γ γ' ⟶ converge M2 γ γ' ⟶ convergence_graph_lookup_invar M1 M2 cg_lookup G ⟶ convergence_graph_lookup_invar M1 M2 cg_lookup (cg_merge G γ γ'))"

end```