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