Theory Simple_Convergence_Graph

section ‹Simple Convergence Graphs›

text ‹This theory introduces a very simple implementation of convergence graphs that
      consists of a list of convergent classes represented as sets of traces.›

theory Simple_Convergence_Graph
imports Convergence_Graph 
begin

subsection ‹Basic Definitions›

type_synonym 'a simple_cg = "'a list fset list"

definition simple_cg_empty :: "'a simple_cg" where
  "simple_cg_empty = []"

(* collects all traces in the same convergent class set as ys *)
fun simple_cg_lookup :: "('a::linorder) simple_cg ⇒ 'a list ⇒ 'a list list" where
  "simple_cg_lookup xs ys = sorted_list_of_fset (finsert ys (foldl (|∪|) fempty (filter (λx . ys |∈| x) xs)))"

(* collects all traces (zs@ys'') such that there exists a prefix ys' of ys with (ys=ys'@ys'')
   and zs is in the same convergent class set as ys' *) 
fun simple_cg_lookup_with_conv :: "('a::linorder) simple_cg ⇒ 'a list ⇒ 'a list list" where
  "simple_cg_lookup_with_conv g ys = (let
      lookup_for_prefix = (λi . let
                                  pref = take i ys;
                                  suff = drop i ys;
                                  pref_conv = (foldl (|∪|) fempty (filter (λx . pref |∈| x) g))
                                in fimage (λ pref' . pref'@suff) pref_conv)
    in sorted_list_of_fset (finsert ys (foldl (λ cs i . lookup_for_prefix i |∪| cs) fempty [0..<Suc (length ys)])))"

fun simple_cg_insert' :: "('a::linorder) simple_cg ⇒ 'a list ⇒ 'a simple_cg" where
  "simple_cg_insert' xs ys = (case find (λx . ys |∈| x) xs
    of Some x ⇒ xs |
       None   ⇒ {|ys|}#xs)"


fun simple_cg_insert :: "('a::linorder) simple_cg ⇒ 'a list ⇒ 'a simple_cg" where
  "simple_cg_insert xs ys = foldl (λ xs' ys' . simple_cg_insert' xs' ys') xs (prefixes ys)"

fun simple_cg_initial :: "('a,'b::linorder,'c::linorder) fsm ⇒ ('b×'c) prefix_tree ⇒ ('b×'c) simple_cg" where
  "simple_cg_initial M1 T = foldl (λ xs' ys' . simple_cg_insert' xs' ys') simple_cg_empty (filter (is_in_language M1 (initial M1)) (sorted_list_of_sequences_in_tree T))"


subsection ‹Merging by Closure›

text ‹The following implementation of the merge operation follows the closure operation described
      by Simão et al. in Simão, A., Petrenko, A. and Yevtushenko, N. (2012), On reducing test length 
      for FSMs with extra states. Softw. Test. Verif. Reliab., 22: 435-454. https://doi.org/10.1002/stvr.452.
      That is, two traces u and v are merged by adding {u,v} to the list of convergent classes
      followed by computing the closure of the graph based on two operations: 
      (1) classes A and B can be merged if there exists some class C such that C contains some w1, w2
          and there exists some w such that A contains w1.w and B contains w2.w.
      (2) classes A and B can be merged if one is a subset of the other.›


(* classes x1 and x2 can be merged via class x if there exist α, β in x and some suffix γ
   such that x1 contains α@γ and x2 contains β@γ *)
fun can_merge_by_suffix :: "'a list fset ⇒ 'a list fset ⇒ 'a list fset ⇒ bool" where
  "can_merge_by_suffix x x1 x2 = (∃ α β γ . α |∈| x ∧ β |∈| x ∧ α@γ |∈| x1 ∧ β@γ |∈| x2)"

lemma can_merge_by_suffix_code[code] : 
  "can_merge_by_suffix x x1 x2 = 
    (∃ ys ∈ fset x . 
      ∃ ys1 ∈ fset x1 . 
        is_prefix ys ys1 ∧ 
        (∃ ys' ∈ fset x . ys'@(drop (length ys) ys1) |∈| x2))"
  (is "?P1 = ?P2")
proof 
  show "?P1 ⟹ ?P2"
    by (metis append_eq_conv_conj can_merge_by_suffix.elims(2) is_prefix_prefix) 
  show "?P2 ⟹ ?P1"
    by (metis append_eq_conv_conj can_merge_by_suffix.elims(3) is_prefix_prefix)
qed



fun prefixes_in_list_helper :: "'a ⇒ 'a list list ⇒ (bool × 'a list list) ⇒ bool × 'a list list" where
  "prefixes_in_list_helper x [] res = res" |
  "prefixes_in_list_helper x ([]#yss) res = prefixes_in_list_helper x yss (True, snd res)" |
  "prefixes_in_list_helper x ((y#ys)#yss) res = 
    (if x = y then prefixes_in_list_helper x yss (fst res, ys # snd res)
              else prefixes_in_list_helper x yss res)"

fun prefixes_in_list :: "'a list ⇒ 'a list ⇒ 'a list list ⇒ 'a list list ⇒ 'a list list" where
  "prefixes_in_list [] prev yss res = (if List.member yss [] then prev#res else res)" |
  "prefixes_in_list (x#xs) prev yss res = (let
    (b,yss') = prefixes_in_list_helper x yss (False,[])
   in if b then prefixes_in_list xs (prev@[x]) yss' (prev # res)
           else prefixes_in_list xs (prev@[x]) yss' res)"

fun prefixes_in_set :: "('a::linorder) list ⇒ 'a list fset ⇒ 'a list list" where
  "prefixes_in_set xs yss = prefixes_in_list xs [] (sorted_list_of_fset yss) []"

value "prefixes_in_list [1::nat,2,3,4,5] [] 
                        [ [1,2,3], [1,2,4], [1,3], [], [1], [1,5,3], [2,5] ] []"

value "prefixes_in_list_helper (1::nat) 
                               [ [1,2,3], [1,2,4], [1,3], [], [1], [1,5,3], [2,5] ]
                               (False,[])"

lemma prefixes_in_list_helper_prop :
shows "fst (prefixes_in_list_helper x yss res) = (fst res ∨ [] ∈ list.set yss)" (is ?P1)
  and "list.set (snd (prefixes_in_list_helper x yss res)) = list.set (snd res) ∪ {ys . x#ys ∈ list.set yss}" (is ?P2)
proof -
  have "?P1 ∧ ?P2"
  proof (induction yss arbitrary: res)
    case Nil
    then show ?case by auto
  next
    case (Cons ys yss)
    show ?case proof (cases ys)
      case Nil
      then show ?thesis 
        using Cons.IH by auto
    next
      case (Cons y ys')
      show ?thesis proof (cases "x = y")
        case True
        have *: "prefixes_in_list_helper x (ys # yss) res = prefixes_in_list_helper y yss (fst res, ys' # snd res)"
          unfolding Cons True by auto
        show ?thesis 
          using Cons.IH[of "(fst res, ys' # snd res)"]
          unfolding * 
          unfolding Cons
          unfolding True 
          by auto
      next
        case False
        then have *: "prefixes_in_list_helper x (ys # yss) res = prefixes_in_list_helper x yss res"
          unfolding Cons by auto

        show ?thesis 
          unfolding * 
          unfolding Cons
          using Cons.IH[of res] False
          by force 
      qed
    qed
  qed
  then show ?P1 and ?P2 by blast+
qed

lemma prefixes_in_list_prop :
shows "list.set (prefixes_in_list xs prev yss res) = list.set res ∪ {prev@ys | ys . ys ∈ list.set (prefixes xs) ∧ ys ∈ list.set yss}"
proof (induction xs arbitrary: prev yss res)
  case Nil
  show ?case 
    unfolding prefixes_in_list.simps List.member_def prefixes_set by auto
next
  case (Cons x xs)

  obtain b yss' where "prefixes_in_list_helper x yss (False,[]) = (b,yss')"
    using prod.exhaust by metis
  then have "b = ([] ∈ list.set yss)"
        and "list.set yss' = {ys . x#ys ∈ list.set yss}"
    using prefixes_in_list_helper_prop[of x yss "(False,[])"] 
    by auto

  show ?case proof (cases b)
    case True
    then have *: "prefixes_in_list (x#xs) prev yss res = prefixes_in_list xs (prev@[x]) yss' (prev # res)"
      using ‹prefixes_in_list_helper x yss (False,[]) = (b,yss')› by auto
    show ?thesis 
      unfolding *
      unfolding Cons ‹list.set yss' = {ys . x#ys ∈ list.set yss}›
      using True unfolding ‹b = ([] ∈ list.set yss)›
      by auto
  next
    case False
    then have *: "prefixes_in_list (x#xs) prev yss res = prefixes_in_list xs (prev@[x]) yss' res"
      using ‹prefixes_in_list_helper x yss (False,[]) = (b,yss')› by auto

    show ?thesis 
      unfolding *
      unfolding Cons ‹list.set yss' = {ys . x#ys ∈ list.set yss}›
      using False unfolding ‹b = ([] ∈ list.set yss)›
      by auto
  qed
qed

lemma prefixes_in_set_prop :
  "list.set (prefixes_in_set xs yss) = list.set (prefixes xs) ∩ fset yss"
  unfolding prefixes_in_set.simps
  unfolding prefixes_in_list_prop
  by auto

(* alternative implementation of merging *)
(*
lemma can_merge_by_suffix_code[code] : 
  "can_merge_by_suffix x x1 x2 = 
    (∃ ys1 ∈ fset x1 . list_ex (λys . ys |∈| x ∧ (∃ ys' ∈ fset x . ys'@(drop (length ys) ys1) |∈| x2)) 
                               (prefixes ys1))"
  (is "?P1 = ?P2")
proof 
  show "?P1 ⟹ ?P2" 
  proof -
    assume "?P1"
    then obtain α β γ where "α |∈| x" and "β |∈| x" and "α@γ |∈| x1" and "β@γ |∈| x2"
      by auto

    have "α@γ ∈ fset x1" using ‹α@γ |∈| x1› notin_fset by metis
    moreover have "α ∈ list.set (prefixes (α@γ))" by (simp add: prefixes_take_iff) 
    moreover note ‹α |∈| x›
    moreover have "∃ ys'' ∈ fset x . ys''@(drop (length α) (α@γ)) |∈| x2"
      using ‹β@γ |∈| x2› ‹β |∈| x›
      by (metis append_eq_conv_conj notin_fset)
    ultimately show "?P2" 
      unfolding list_ex_iff by blast
  qed

  show "?P2 ⟹ ?P1"
  proof -
    assume "?P2"
    then obtain ys1 ys ys' where "ys1 ∈ fset x1" 
                             and "ys ∈ list.set (prefixes ys1)" 
                             and "ys |∈| x" 
                             and "ys' ∈ fset x" 
                             and "ys'@(drop (length ys) ys1) |∈| x2"
      unfolding list_ex_iff by blast
    then show "?P1"
      by (metis append_take_drop_id can_merge_by_suffix.elims(3) notin_fset prefixes_take_iff) 
  qed
qed
*)
  


lemma can_merge_by_suffix_validity :
  assumes "observable M1" and "observable M2"
  and     "⋀ u v . u |∈| x ⟹ v |∈| x ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ u v . u |∈| x1 ⟹ v |∈| x1 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ u v . u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "can_merge_by_suffix x x1 x2"
  and     "u |∈| (x1 |∪| x2)"
  and     "v |∈| (x1 |∪| x2)"
  and     "u ∈ L M1" and "u ∈ L M2" 
shows "converge M1 u v ∧ converge M2 u v"
proof -
  obtain α β γ where "α |∈| x" and "β |∈| x" and "α@γ |∈| x1" and "β@γ |∈| x2"
    using ‹can_merge_by_suffix x x1 x2› by auto

  consider "u |∈| x1" | "u |∈| x2" 
    using ‹u |∈| (x1 |∪| x2)› by blast
  then show ?thesis proof cases
    case 1

    then have "converge M1 u (α@γ)" and "converge M2 u (α@γ)"
      using ‹u |∈| (x1 |∪| x2)› assms(4)[OF _ ‹α@γ |∈| x1› assms(9,10)] 
      by blast+
    then have "(α@γ) ∈ L M1" and "(α@γ) ∈ L M2"
      by auto
    then have "α ∈ L M1" and "α ∈ L M2"
      using language_prefix by metis+
    then have "converge M1 α β" and "converge M2 α β"
      using assms(3) ‹α |∈| x› ‹β |∈| x›
      by blast+
    have "converge M1 (α@γ) (β@γ)" 
      using ‹converge M1 α β›
      by (meson ‹α @ γ ∈ L M1› assms(1) converge.simps converge_append) 
    then have "β@γ ∈ L M1"
      by auto
    have "converge M2 (α@γ) (β@γ)" 
      using ‹converge M2 α β›
      by (meson ‹α @ γ ∈ L M2› assms(2) converge.simps converge_append)   
    then have "β@γ ∈ L M2"
      by auto

    consider (11) "v |∈| x1" | (12) "v |∈| x2" 
      using ‹v |∈| (x1 |∪| x2)› by blast
    then show ?thesis proof cases
      case 11
      show ?thesis
        using "1" "11" assms(10) assms(4) assms(9) by blast 
    next
      case 12
      then have "converge M1 v (β@γ)" and "converge M2 v (β@γ)"
        using assms(5)[OF ‹β@γ |∈| x2› _ ‹β@γ ∈ L M1› ‹β@γ ∈ L M2›] 
        by auto
      then show ?thesis 
        using ‹converge M1 (α@γ) (β@γ)› ‹converge M2 (α@γ) (β@γ)› ‹converge M1 u (α@γ)› ‹converge M2 u (α@γ)› 
        by auto
    qed 
  next
    case 2

    then have "converge M1 u (β@γ)" and "converge M2 u (β@γ)"
      using ‹u |∈| (x1 |∪| x2)› assms(5)[OF _ ‹β@γ |∈| x2› assms(9,10)] 
      by blast+
    then have "(β@γ) ∈ L M1" and "(β@γ) ∈ L M2"
      by auto
    then have "β ∈ L M1" and "β ∈ L M2"
      using language_prefix by metis+
    then have "converge M1 α β" and "converge M2 α β"
      using assms(3)[OF ‹β |∈| x› ‹α |∈| x›]
      by auto
    have "converge M1 (α@γ) (β@γ)" 
        using ‹converge M1 α β›
        using ‹β @ γ ∈ L M1› ‹β ∈ L M1› assms(1) converge_append converge_append_language_iff by blast
    then have "α@γ ∈ L M1"
      by auto
    have "converge M2 (α@γ) (β@γ)" 
      using ‹converge M2 α β› 
      using ‹β @ γ ∈ L M2› ‹β ∈ L M2› assms(2) converge_append converge_append_language_iff by blast
    then have "α@γ ∈ L M2"
      by auto
      

    consider (21) "v |∈| x1" | (22) "v |∈| x2" 
      using ‹v |∈| (x1 |∪| x2)› by blast
    then show ?thesis proof cases
      case 22
      show ?thesis
        using "2" "22" assms(10) assms(5) assms(9) by blast 
    next
      case 21
      then have "converge M1 v (α@γ)" and "converge M2 v (α@γ)"
        using assms(4)[OF ‹α@γ |∈| x1› _ ‹α@γ ∈ L M1› ‹α@γ ∈ L M2›] 
        by auto
      then show ?thesis 
        using ‹converge M1 (α@γ) (β@γ)› ‹converge M2 (α@γ) (β@γ)›  ‹converge M1 u (β@γ)› ‹converge M2 u (β@γ)› 
        by auto
    qed 
  qed
qed


fun simple_cg_closure_phase_1_helper' :: "'a list fset ⇒ 'a list fset ⇒ 'a simple_cg ⇒ (bool × 'a list fset × 'a simple_cg)" where
  "simple_cg_closure_phase_1_helper' x x1 xs = 
    (let (x2s,others) = separate_by (can_merge_by_suffix x x1) xs;
         x1Union      = foldl (|∪|) x1 x2s
      in (x2s ≠ [],x1Union,others))"  

lemma simple_cg_closure_phase_1_helper'_False :
  "¬fst (simple_cg_closure_phase_1_helper' x x1 xs) ⟹ simple_cg_closure_phase_1_helper' x x1 xs = (False,x1,xs)"
  unfolding simple_cg_closure_phase_1_helper'.simps Let_def separate_by.simps
  by (simp add: filter_empty_conv) 


lemma simple_cg_closure_phase_1_helper'_True :
  assumes "fst (simple_cg_closure_phase_1_helper' x x1 xs)" 
shows "length (snd (snd (simple_cg_closure_phase_1_helper' x x1 xs))) < length xs"
proof -
  have "snd (snd (simple_cg_closure_phase_1_helper' x x1 xs)) = filter (λx2 . ¬ (can_merge_by_suffix x x1 x2)) xs"
    by auto
  moreover have "filter (λx2 . (can_merge_by_suffix x x1 x2)) xs ≠ []"
    using assms unfolding simple_cg_closure_phase_1_helper'.simps Let_def separate_by.simps
    by fastforce
  ultimately show ?thesis 
    using filter_not_all_length[of "can_merge_by_suffix x x1" xs]
    by metis
qed

lemma simple_cg_closure_phase_1_helper'_length :
  "length (snd (snd (simple_cg_closure_phase_1_helper' x x1 xs))) ≤ length xs"
  by auto

lemma simple_cg_closure_phase_1_helper'_validity_fst :
  assumes "observable M1" and "observable M2"
  and     "⋀ u v . u |∈| x ⟹ v |∈| x ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ u v . u |∈| x1 ⟹ v |∈| x1 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ x2 u v . x2 ∈ list.set xs ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "u |∈| fst (snd (simple_cg_closure_phase_1_helper' x x1 xs))"
  and     "v |∈| fst (snd (simple_cg_closure_phase_1_helper' x x1 xs))"
  and     "u ∈ L M1" and "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
proof -

  have *:"⋀ w . w |∈| fst (snd (simple_cg_closure_phase_1_helper' x x1 xs)) ⟹ w |∈| x1 ∨ (∃ x2 . x2 ∈ list.set xs ∧ w |∈| x2 ∧ can_merge_by_suffix x x1 x2)"
  proof -
    fix w assume "w |∈| fst (snd (simple_cg_closure_phase_1_helper' x x1 xs))"
    then have "w |∈| ffUnion (fset_of_list (x1#(filter (can_merge_by_suffix x x1) xs)))"
      using foldl_funion_fsingleton[where xs="(filter (can_merge_by_suffix x x1) xs)"]
      by auto

    then obtain x2 where "w |∈| x2"
                     and "x2 |∈| fset_of_list (x1#(filter (can_merge_by_suffix x x1) xs))"
      using ffUnion_fmember_ob
      by metis
    then consider "x2=x1" | "x2 ∈ list.set (filter (can_merge_by_suffix x x1) xs)"
      by (meson fset_of_list_elem set_ConsD) 
    then show "w |∈| x1 ∨ (∃ x2 . x2 ∈ list.set xs ∧ w |∈| x2 ∧ can_merge_by_suffix x x1 x2)"
      using ‹w |∈| x2› by (cases; auto)
  qed

  consider "u |∈| x1" | "(∃ x2 . x2 ∈ list.set xs ∧ u |∈| x2 ∧ can_merge_by_suffix x x1 x2)"
    using *[OF assms(6)] by blast
  then show ?thesis proof cases
    case 1
    
    consider (a) "v |∈| x1" | (b) "(∃ x2 . x2 ∈ list.set xs ∧ v |∈| x2 ∧ can_merge_by_suffix x x1 x2)"
      using *[OF assms(7)] by blast
    then show ?thesis proof cases
      case a
      then show ?thesis using assms(4)[OF 1 _ assms(8,9)] by auto
    next
      case b
      then obtain x2v where "x2v ∈ list.set xs" and "v |∈| x2v" and "can_merge_by_suffix x x1 x2v"
        using *[OF assms(6)] 
        by blast

      then have "u |∈| x1 |∪| x2v" and "v |∈| x1 |∪| x2v"
        using 1 by auto

      show ?thesis
        using can_merge_by_suffix_validity[OF assms(1,2), of x x1 x2v, OF assms(3,4) assms(5)[OF ‹x2v ∈ list.set xs›] ‹can_merge_by_suffix x x1 x2v› ‹u |∈| x1 |∪| x2v› ‹v |∈| x1 |∪| x2v› assms(8,9)]
        by blast
    qed    
  next
    case 2
    then obtain x2u where "x2u ∈ list.set xs" and "u |∈| x2u" and "can_merge_by_suffix x x1 x2u"
      using *[OF assms(6)] 
      by blast
    then have "u |∈| x1 |∪| x2u"
      by auto

    consider (a) "v |∈| x1" | (b) "(∃ x2 . x2 ∈ list.set xs ∧ v |∈| x2 ∧ can_merge_by_suffix x x1 x2)"
      using *[OF assms(7)] by blast
    then show ?thesis proof cases
      case a
      then have "v |∈| x1 |∪| x2u"
        by auto
      show ?thesis
        using can_merge_by_suffix_validity[OF assms(1,2), of x x1 x2u, OF assms(3,4) assms(5)[OF ‹x2u ∈ list.set xs›] ‹can_merge_by_suffix x x1 x2u› ‹u |∈| x1 |∪| x2u› ‹v |∈| x1 |∪| x2u› assms(8,9)]  
        by blast
    next 
      case b
      
      then obtain x2v where "x2v ∈ list.set xs" and "v |∈| x2v" and "can_merge_by_suffix x x1 x2v"
        using *[OF assms(6)] 
        by blast
      then have "v |∈| x1 |∪| x2v"
        by auto

      have "⋀ v . v |∈| x1 |∪| x2u ⟹ converge M1 u v ∧ converge M2 u v"
        using can_merge_by_suffix_validity[OF assms(1,2), of x x1 x2u, OF assms(3,4) assms(5)[OF ‹x2u ∈ list.set xs›] ‹can_merge_by_suffix x x1 x2u› ‹u |∈| x1 |∪| x2u› _ assms(8,9)]
        by blast
      have "⋀ u . u |∈| x1 |∪| x2v ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
        using can_merge_by_suffix_validity[OF assms(1,2), of x x1 x2v, OF assms(3,4) assms(5)[OF ‹x2v ∈ list.set xs›] ‹can_merge_by_suffix x x1 x2v› _ ‹v |∈| x1 |∪| x2v›]
        by blast

      obtain αv βv γv where "αv |∈| x" and "βv |∈| x" and "αv@γv |∈| x1" and "βv@γv |∈| x2v"
        using ‹can_merge_by_suffix x x1 x2v› by auto

      show ?thesis
        using ‹⋀u. ⟦u |∈| x1 |∪| x2v; u ∈ L M1; u ∈ L M2⟧ ⟹ converge M1 u v ∧ converge M2 u v› ‹⋀v. v |∈| x1 |∪| x2u ⟹ converge M1 u v ∧ converge M2 u v› ‹αv @ γv |∈| x1› by fastforce
    qed
  qed
qed


lemma simple_cg_closure_phase_1_helper'_validity_snd :
  assumes "⋀ x2 u v . x2 ∈ list.set xs ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "x2 ∈ list.set (snd (snd (simple_cg_closure_phase_1_helper' x x1 xs)))"
  and     "u |∈| x2"
  and     "v |∈| x2"
  and     "u ∈ L M1" and "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
proof -
  have "list.set (snd (snd (simple_cg_closure_phase_1_helper' x x1 xs))) ⊆ list.set xs"
    by auto
  then show ?thesis
    using assms by blast  
qed


fun simple_cg_closure_phase_1_helper :: "'a list fset ⇒ 'a simple_cg ⇒ (bool × 'a simple_cg) ⇒ (bool × 'a simple_cg)" where
  "simple_cg_closure_phase_1_helper x [] (b,done) = (b,done)" |
  "simple_cg_closure_phase_1_helper x (x1#xs) (b,done) = (let (hasChanged,x1',xs') = simple_cg_closure_phase_1_helper' x x1 xs
                                    in simple_cg_closure_phase_1_helper x xs' (b ∨ hasChanged, x1' # done))"


lemma simple_cg_closure_phase_1_helper_validity :
  assumes "observable M1" and "observable M2"
  and     "⋀ u v . u |∈| x ⟹ v |∈| x ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ x2 u v . x2 ∈ list.set don ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ x2 u v . x2 ∈ list.set xss ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "x2 ∈ list.set (snd (simple_cg_closure_phase_1_helper x xss (b,don)))"
  and     "u |∈| x2"
  and     "v |∈| x2"
  and     "u ∈ L M1" and "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
  using assms(4,5,6)
proof (induction "length xss" arbitrary: xss don b rule: less_induct)
  case less
  show ?case proof (cases xss)
    case Nil
    then have "x2 ∈ list.set don"
      using less.prems(3) by auto
    then show ?thesis 
      using less.prems(1) assms(7,8,9,10)
      by blast 
  next
    case (Cons x1 xs)
    obtain b' x1' xs' where "simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')"
      using prod.exhaust by metis
    then have "simple_cg_closure_phase_1_helper x xss (b,don) = simple_cg_closure_phase_1_helper x xs' (b ∨ b', x1' # don)"
      unfolding Cons by auto


    have *:"⋀ u v . u |∈| x1 ⟹ v |∈| x1 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
      using less.prems(2)[of x1] unfolding Cons
      by (meson list.set_intros(1)) 

    have **:"⋀ x2 u v . x2 ∈ list.set xs ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
      using less.prems(2) unfolding Cons
      by (meson list.set_intros(2)) 

    have ***:"⋀ u v. u |∈| x1' ⟹ v |∈| x1' ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
      using simple_cg_closure_phase_1_helper'_validity_fst[of M1 M2 x x1 xs _ _, OF assms(1,2,3) * **, of "λ a b c . a"]
      unfolding ‹simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')› fst_conv snd_conv
      by blast

    have "length xs' < length xss"
      using simple_cg_closure_phase_1_helper'_length[of x x1 xs]
      unfolding ‹simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')› Cons by auto

    have "(⋀x2 u v. x2 ∈ list.set (x1' # don) ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
      using *** less.prems(1)
      by (metis set_ConsD) 

    have "xs' = snd (snd (simple_cg_closure_phase_1_helper' x x1 xs))"
      using ‹simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')› by auto
    have "(⋀x2 u v. x2 ∈ list.set xs' ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
      using simple_cg_closure_phase_1_helper'_validity_snd[of xs' M1]
      unfolding ‹xs' = snd (snd (simple_cg_closure_phase_1_helper' x x1 xs))›
      using ** simple_cg_closure_phase_1_helper'_validity_snd by blast 

    have "x2 ∈ list.set (snd (simple_cg_closure_phase_1_helper x xs' (b ∨ b', x1' # don)))"
      using less.prems(3) unfolding ‹simple_cg_closure_phase_1_helper x xss (b,don) = simple_cg_closure_phase_1_helper x xs' (b ∨ b', x1' # don)› .
    then show ?thesis
      using less.hyps[OF ‹length xs' < length xss› ‹(⋀x2 u v. x2 ∈ list.set (x1' # don) ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)› ‹(⋀x2 u v. x2 ∈ list.set xs' ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)›, of "x1'#don" "λ a b c . a" "λ a b c . a"]
      by force
  qed
qed



lemma simple_cg_closure_phase_1_helper_length :
  "length (snd (simple_cg_closure_phase_1_helper x xss (b,don))) ≤ length xss + length don"
proof (induction "length xss" arbitrary: xss b don rule: less_induct)
  case less
  show ?case proof (cases xss)
    case Nil
    then show ?thesis by auto
  next
    case (Cons x1 xs)
    obtain b' x1' xs' where "simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')"
      using prod.exhaust by metis
    then have "simple_cg_closure_phase_1_helper x xss (b,don) = simple_cg_closure_phase_1_helper x xs' (b ∨ b', x1' # don)"
      unfolding Cons by auto
    
    have "length xs' < length xss"
      using simple_cg_closure_phase_1_helper'_length[of x x1 xs]
      unfolding ‹simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')› Cons by auto
    then have "length (snd (simple_cg_closure_phase_1_helper x xs' (b ∨ b', x1'#don))) ≤ length xs' + length (x1'#don)"
      using less[of xs'] unfolding Cons by blast
    moreover have "length xs' + length (x1'#don) ≤ length xss + length don"
      using simple_cg_closure_phase_1_helper'_length[of x x1 xs]
      unfolding ‹simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')› snd_conv Cons by auto
    ultimately show ?thesis
      unfolding ‹simple_cg_closure_phase_1_helper x xss (b,don) = simple_cg_closure_phase_1_helper x xs' (b ∨ b', x1' # don)› 
      by presburger
  qed
qed 


lemma simple_cg_closure_phase_1_helper_True :
  assumes "fst (simple_cg_closure_phase_1_helper x xss (False,don))" 
  and     "xss ≠ []"
shows "length (snd (simple_cg_closure_phase_1_helper x xss (False,don))) < length xss + length don"
  using assms
proof (induction "length xss" arbitrary: xss don rule: less_induct)
  case less
  show ?case proof (cases xss)
    case Nil
    then show ?thesis using less.prems(2) by auto
  next
    case (Cons x1 xs)
    obtain b' x1' xs' where "simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')"
      using prod.exhaust by metis
    then have "simple_cg_closure_phase_1_helper x xss (False,don) = simple_cg_closure_phase_1_helper x xs' (b', x1' # don)"
      unfolding Cons by auto

    show ?thesis proof (cases b')
      case True
      then have "length xs' < length xs"
        using simple_cg_closure_phase_1_helper'_True[of x x1 xs]
        unfolding ‹simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')› fst_conv snd_conv
        by blast
      then have "length (snd (simple_cg_closure_phase_1_helper x xs' (b', x1' # don))) < length xss + length don"
        using simple_cg_closure_phase_1_helper_length[of x xs' b' "x1'#don"]
        unfolding Cons
        by auto
      then show ?thesis 
        unfolding ‹simple_cg_closure_phase_1_helper x xss (False,don) = simple_cg_closure_phase_1_helper x xs' (b', x1' # don)› .
    next
      case False
      then have "simple_cg_closure_phase_1_helper x xss (False,don) = simple_cg_closure_phase_1_helper x xs' (False, x1' # don)"
        using ‹simple_cg_closure_phase_1_helper x xss (False,don) = simple_cg_closure_phase_1_helper x xs' (b', x1' # don)› 
        by auto
      then have "fst (simple_cg_closure_phase_1_helper x xs' (False, x1' # don))"
        using less.prems(1) by auto

      have "length xs' < length xss"
        using simple_cg_closure_phase_1_helper'_length[of x x1 xs]
        unfolding ‹simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')› Cons by auto

      have "xs' ≠ []"
        using ‹simple_cg_closure_phase_1_helper' x x1 xs = (b',x1',xs')› False
        by (metis ‹fst (simple_cg_closure_phase_1_helper x xs' (False, x1' # don))› simple_cg_closure_phase_1_helper.simps(1) fst_eqD)
  
      show ?thesis 
        using less.hyps[OF ‹length xs' < length xss› ‹fst (simple_cg_closure_phase_1_helper x xs' (False, x1' # don))› ‹xs' ≠ []›] ‹length xs' < length xss›
        unfolding ‹simple_cg_closure_phase_1_helper x xss (False,don) = simple_cg_closure_phase_1_helper x xs' (False, x1' # don)› 
        unfolding Cons 
        by auto
    qed
  qed
qed



(* closure operation (1) *)
fun simple_cg_closure_phase_1 :: "'a simple_cg ⇒ (bool × 'a simple_cg)" where
  "simple_cg_closure_phase_1 xs = foldl (λ (b,xs) x. let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xs"

lemma simple_cg_closure_phase_1_validity :
  assumes "observable M1" and "observable M2"
  and     "⋀ x2 u v . x2 ∈ list.set xs ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "x2 ∈ list.set (snd (simple_cg_closure_phase_1 xs))"
  and     "u |∈| x2"
  and     "v |∈| x2"
  and     "u ∈ L M1" and "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
proof -

  have "⋀ xss x2 u v . (⋀ x2 u v . x2 ∈ list.set xss ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v) ⟹ x2 ∈ list.set (snd (foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss)) ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  proof -
    fix xss x2 u v
    assume "⋀ x2 u v . x2 ∈ list.set xss ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
    and    "x2 ∈ list.set (snd (foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss))"
    and    "u |∈| x2"
    and    "v |∈| x2"
    and    "u ∈ L M1" 
    and    "u ∈ L M2"

    then show "converge M1 u v ∧ converge M2 u v"
    proof (induction xss arbitrary: x2 u v rule: rev_induct)
      case Nil
      then have "x2 ∈ list.set xs"
        by auto
      then show ?case 
        using Nil.prems(3,4,5,6) assms(3) by blast
    next
      case (snoc x xss)

      obtain b xss' where "(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss) = (b,xss')"
        using prod.exhaust by metis
      moreover obtain b' xss'' where "simple_cg_closure_phase_1_helper x xss' (False,[]) = (b',xss'')"
        using prod.exhaust by metis
      ultimately have *:"(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) (xss@[x])) = (b∨b',xss'')"
        by auto

      have "(⋀u v. u |∈| x ⟹ v |∈| x ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
        using snoc.prems(1)
        by (metis append_Cons list.set_intros(1) list_set_sym) 
      moreover have "(⋀x2 u v. x2 ∈ list.set [] ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
        by auto
      moreover have "(⋀x2 u v. x2 ∈ list.set xss' ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
      proof -
        have "(⋀x2 u v. x2 ∈ list.set xss ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)" 
          using snoc.prems(1)
          by (metis (no_types, lifting) append_Cons append_Nil2 insertCI list.simps(15) list_set_sym)
        then show "(⋀x2 u v. x2 ∈ list.set xss' ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
          using snoc.IH
          unfolding ‹(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss) = (b,xss')› snd_conv
          by blast
      qed
      ultimately have "(⋀x2 u v. x2 ∈ list.set xss'' ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
        using simple_cg_closure_phase_1_helper_validity[OF assms(1,2), of x "[]" xss' _ False]
        unfolding ‹simple_cg_closure_phase_1_helper x xss' (False,[]) = (b',xss'')› snd_conv
        by blast
      then show ?case
        using snoc.prems(2,3,4,5,6)
        unfolding *  snd_conv
        by blast 
    qed
  qed

  then show ?thesis
    using assms(3,4,5,6,7,8)
    unfolding simple_cg_closure_phase_1.simps
    by blast
qed

lemma simple_cg_closure_phase_1_length_helper :
  "length (snd (foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss)) ≤ length xs"
proof (induction xss rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x xss)

  obtain b xss' where "(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss) = (b,xss')"
    using prod.exhaust by metis
  moreover obtain b' xss'' where "simple_cg_closure_phase_1_helper x xss' (False,[]) = (b',xss'')"
    using prod.exhaust by metis
  ultimately have *:"(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) (xss@[x])) = (b∨b',xss'')"
    by auto

  have "length xss' ≤ length xs"
    using snoc.IH
    unfolding ‹(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss) = (b,xss')›
    by auto
  moreover have "length xss'' ≤ length xss'"
    using simple_cg_closure_phase_1_helper_length[of x xss' False "[]"]
    unfolding ‹simple_cg_closure_phase_1_helper x xss' (False,[]) = (b',xss'')›
    by auto
  ultimately show ?case
    unfolding * snd_conv
    by simp
qed

lemma simple_cg_closure_phase_1_length : 
  "length (snd (simple_cg_closure_phase_1 xs)) ≤ length xs"
  using simple_cg_closure_phase_1_length_helper by auto

lemma simple_cg_closure_phase_1_True :
  assumes "fst (simple_cg_closure_phase_1 xs)" 
  shows "length (snd (simple_cg_closure_phase_1 xs)) < length xs"
proof -
  have "⋀ xss . fst (foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss) ⟹ length (snd (foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss)) < length xs"
  proof -
    fix xss
    assume "fst (foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss)"
    then show "length (snd (foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss)) < length xs"
    proof (induction xss rule: rev_induct)
      case Nil
      then show ?case by auto
    next
      case (snoc x xss)

      obtain b xss' where "(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss) = (b,xss')"
        using prod.exhaust by metis
      moreover obtain b' xss'' where "simple_cg_closure_phase_1_helper x xss' (False,[]) = (b',xss'')"
        using prod.exhaust by metis
      ultimately have "(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) (xss@[x])) = (b∨b',xss'')"
        by auto

      consider b | b'
        using snoc.prems
        unfolding ‹(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) (xss@[x])) = (b∨b',xss'')› fst_conv
        by blast
      then show ?case proof cases
        case 1
        then have "length xss' < length xs"
          using snoc.IH 
          unfolding ‹(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) xss) = (b,xss')› fst_conv snd_conv
          by auto
        moreover have "length xss'' ≤ length xss'"
          using simple_cg_closure_phase_1_helper_length[of x xss' False "[]"]
          unfolding ‹simple_cg_closure_phase_1_helper x xss' (False,[]) = (b',xss'')›
          by auto
        ultimately show ?thesis
          unfolding ‹(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) (xss@[x])) = (b∨b',xss'')› snd_conv
          by simp
      next
        case 2
        have "length xss' ≤ length xs"
          using simple_cg_closure_phase_1_length_helper[of xss xs]
          by (metis ‹foldl (λ(b, xs) x. let (b', xs') = simple_cg_closure_phase_1_helper x xs (False, []) in (b ∨ b', xs')) (False, xs) xss = (b, xss')› simple_cg_closure_phase_1_length_helper snd_conv)
        moreover have "length xss'' < length xss'"
        proof -
          have "xss' ≠ []"
            using "2" ‹simple_cg_closure_phase_1_helper x xss' (False, []) = (b', xss'')› by auto
          then show ?thesis
            using simple_cg_closure_phase_1_helper_True[of x xss' "[]"] 2
            unfolding ‹simple_cg_closure_phase_1_helper x xss' (False,[]) = (b',xss'')› fst_conv snd_conv 
            by auto
        qed
        ultimately show ?thesis
          unfolding ‹(foldl (λ (b,xs) x . let (b',xs') = simple_cg_closure_phase_1_helper x xs (False,[]) in (b∨b',xs')) (False,xs) (xss@[x])) = (b∨b',xss'')› snd_conv
          by simp
      qed 
    qed
  qed
  then show ?thesis
    using assms by auto
qed




fun can_merge_by_intersection :: "'a list fset ⇒ 'a list fset ⇒ bool" where
  "can_merge_by_intersection x1 x2 = (∃ α . α |∈| x1 ∧ α |∈| x2)"

lemma can_merge_by_intersection_code[code] : 
  "can_merge_by_intersection x1 x2 = (∃ α ∈ fset x1 . α |∈| x2)"
  unfolding can_merge_by_intersection.simps
  by metis


lemma can_merge_by_intersection_validity :
  assumes "⋀ u v . u |∈| x1 ⟹ v |∈| x1 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ u v . u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "can_merge_by_intersection x1 x2"
  and     "u |∈| (x1 |∪| x2)"
  and     "v |∈| (x1 |∪| x2)"
  and     "u ∈ L M1"
  and     "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
proof -
  obtain α where "α |∈| x1" and "α |∈| x2" 
    using assms(3) by auto

  have "converge M1 u α ∧ converge M2 u α"
    using ‹α |∈| x1› ‹α |∈| x2› assms(1,2,4,6,7) by blast
  moreover have "converge M1 v α ∧ converge M2 v α"
    by (metis (no_types, opaque_lifting) ‹α |∈| x1› ‹α |∈| x2› assms(1) assms(2) assms(5) calculation converge.simps funion_iff)
  ultimately show ?thesis
    by simp
qed


fun simple_cg_closure_phase_2_helper :: "'a list fset ⇒ 'a simple_cg ⇒ (bool × 'a list fset × 'a simple_cg)" where
  "simple_cg_closure_phase_2_helper x1 xs = 
    (let (x2s,others) = separate_by (can_merge_by_intersection x1) xs;
         x1Union      = foldl (|∪|) x1 x2s
      in (x2s ≠ [],x1Union,others))"  

lemma simple_cg_closure_phase_2_helper_length :
  "length (snd (snd (simple_cg_closure_phase_2_helper x1 xs))) ≤ length xs"
  by auto

lemma simple_cg_closure_phase_2_helper_validity_fst :
  assumes "⋀ u v . u |∈| x1 ⟹ v |∈| x1 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ x2 u v . x2 ∈ list.set xs ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "u |∈| fst (snd (simple_cg_closure_phase_2_helper x1 xs))"
  and     "v |∈| fst (snd (simple_cg_closure_phase_2_helper x1 xs))"
  and     "u ∈ L M1"
  and     "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
proof -

  have *:"⋀ w . w |∈| fst (snd (simple_cg_closure_phase_2_helper x1 xs)) ⟹ w |∈| x1 ∨ (∃ x2 . x2 ∈ list.set xs ∧ w |∈| x2 ∧ can_merge_by_intersection x1 x2)"
  proof -
    fix w assume "w |∈| fst (snd (simple_cg_closure_phase_2_helper x1 xs))"
    then have "w |∈| ffUnion (fset_of_list (x1#(filter (can_merge_by_intersection x1) xs)))"
      using foldl_funion_fsingleton[where xs="(filter (can_merge_by_intersection x1) xs)"]
      by auto

    then obtain x2 where "w |∈| x2"
                     and "x2 |∈| fset_of_list (x1#(filter (can_merge_by_intersection x1) xs))"
      using ffUnion_fmember_ob
      by metis
    then consider "x2=x1" | "x2 ∈ list.set (filter (can_merge_by_intersection x1) xs)"
      by (meson fset_of_list_elem set_ConsD) 
    then show "w |∈| x1 ∨ (∃ x2 . x2 ∈ list.set xs ∧ w |∈| x2 ∧ can_merge_by_intersection x1 x2)"
      using ‹w |∈| x2› by (cases; auto)
  qed

  consider "u |∈| x1" | "(∃ x2 . x2 ∈ list.set xs ∧ u |∈| x2 ∧ can_merge_by_intersection x1 x2)"
    using *[OF assms(3)] by blast
  then show ?thesis proof cases
    case 1

    consider (a) "v |∈| x1" | (b) "(∃ x2 . x2 ∈ list.set xs ∧ v |∈| x2 ∧ can_merge_by_intersection x1 x2)"
      using *[OF assms(4)] by blast
    then show ?thesis proof cases
      case a
      then show ?thesis using assms(1)[OF 1 _ assms(5,6)] by auto
    next
      case b
      then obtain x2v where "x2v ∈ list.set xs" and "v |∈| x2v" and "can_merge_by_intersection x1 x2v"
        using *[OF assms(3)] 
        by blast
      show ?thesis 
        using can_merge_by_intersection_validity[of x1 M1 M2 x2v, OF assms(1) assms(2)[OF ‹x2v ∈ list.set xs›] ‹can_merge_by_intersection x1 x2v›]
        using 1 ‹v |∈| x2v› assms(5,6)
        by blast
    qed    
  next
    case 2
    then obtain x2u where "x2u ∈ list.set xs" and "u |∈| x2u" and "can_merge_by_intersection x1 x2u"
      using *[OF assms(3)] 
      by blast
    obtain αu where "αu |∈| x1" and "αu |∈| x2u"
      using ‹can_merge_by_intersection x1 x2u› by auto

    consider (a) "v |∈| x1" | (b) "(∃ x2 . x2 ∈ list.set xs ∧ v |∈| x2 ∧ can_merge_by_intersection x1 x2)"
      using *[OF assms(4)] by blast
    then show ?thesis proof cases
      case a

      show ?thesis 
        using can_merge_by_intersection_validity[of x1 M1 M2 x2u, OF assms(1) assms(2)[OF ‹x2u ∈ list.set xs›] ‹can_merge_by_intersection x1 x2u›]
        using ‹u |∈| x2u› a assms(5,6)
        by blast
    next 
      case b
      
      then obtain x2v where "x2v ∈ list.set xs" and "v |∈| x2v" and "can_merge_by_intersection x1 x2v"
        using *[OF assms(4)] 
        by blast
      obtain αv where "αv |∈| x1" and "αv |∈| x2v"
        using ‹can_merge_by_intersection x1 x2v› by auto

      have "⋀ v . v |∈| x1 |∪| x2u ⟹ converge M1 u v ∧ converge M2 u v"
        using can_merge_by_intersection_validity[of x1 M1 M2 x2u, OF assms(1) assms(2)[OF ‹x2u ∈ list.set xs›] ‹can_merge_by_intersection x1 x2u› _ _ assms(5,6)] ‹u |∈| x2u›
        by blast
      have "⋀ u . u |∈| x1 |∪| x2v ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
        using can_merge_by_intersection_validity[of x1 M1 M2 x2v, OF assms(1) assms(2)[OF ‹x2v ∈ list.set xs›] ‹can_merge_by_intersection x1 x2v› ] ‹v |∈| x2v›
        by blast


      show ?thesis
        using ‹⋀u. ⟦u |∈| x1 |∪| x2v; u ∈ L M1; u ∈ L M2⟧ ⟹ converge M1 u v ∧ converge M2 u v› ‹⋀v. v |∈| x1 |∪| x2u ⟹ converge M1 u v ∧ converge M2 u v› ‹αu |∈| x1› by fastforce
    qed
  qed
qed


lemma simple_cg_closure_phase_2_helper_validity_snd :
  assumes "⋀ x2 u v . x2 ∈ list.set xs ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "x2 ∈ list.set (snd (snd (simple_cg_closure_phase_2_helper x1 xs)))"
  and     "u |∈| x2"
  and     "v |∈| x2"
  and     "u ∈ L M1"
  and     "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
proof -
  have "list.set (snd (snd (simple_cg_closure_phase_2_helper x1 xs))) ⊆ list.set xs"
    by auto
  then show ?thesis
    using assms by blast 
qed

lemma simple_cg_closure_phase_2_helper_True :
  assumes "fst (simple_cg_closure_phase_2_helper x xs)" 
shows "length (snd (snd (simple_cg_closure_phase_2_helper x xs))) < length xs"
proof -
  have "snd (snd (simple_cg_closure_phase_2_helper x xs)) = filter (λx2 . ¬ (can_merge_by_intersection x x2)) xs"
    by auto
  moreover have "filter (λx2 . (can_merge_by_intersection x x2)) xs ≠ []"
    using assms unfolding simple_cg_closure_phase_1_helper'.simps Let_def separate_by.simps
    by fastforce
  ultimately show ?thesis 
    using filter_not_all_length[of "can_merge_by_intersection x" xs]
    by metis
qed


function simple_cg_closure_phase_2' :: "'a simple_cg ⇒ (bool × 'a simple_cg) ⇒ (bool × 'a simple_cg)" where
  "simple_cg_closure_phase_2' [] (b,done) = (b,done)" |                                 
  "simple_cg_closure_phase_2' (x#xs) (b,done) = (let (hasChanged,x',xs') = simple_cg_closure_phase_2_helper x xs
    in if hasChanged then simple_cg_closure_phase_2' xs' (True,x'#done)
                     else simple_cg_closure_phase_2' xs (b,x#done))"
  by pat_completeness auto
termination
proof -
  {
    fix xa :: "(bool × 'a list fset × 'a simple_cg)"
    fix x xs b don xb y xaa ya
    assume "xa = simple_cg_closure_phase_2_helper x xs" 
    and    "(xb, y) = xa" 
    and    "(xaa, ya) = y" 
    and    xb
  
    have "length ya < Suc (length xs)"
      using simple_cg_closure_phase_2_helper_True[of x xs] ‹xb›
      unfolding ‹xa = simple_cg_closure_phase_2_helper x xs›[symmetric]
      unfolding ‹(xb, y) = xa›[symmetric] ‹(xaa, ya) = y›[symmetric]
      unfolding fst_conv snd_conv
      by auto
  
    then have "((ya, True, xaa # don), x # xs, b, don) ∈ measure (λ(xs, bd). length xs)"
      by auto
  }
  then show ?thesis
    apply (relation "measure (λ (xs,bd) . length xs)")
    by force+
qed


lemma simple_cg_closure_phase_2'_validity :
  assumes "⋀ x2 u v . x2 ∈ list.set don ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "⋀ x2 u v . x2 ∈ list.set xss ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "x2 ∈ list.set (snd (simple_cg_closure_phase_2' xss (b,don)))"
  and     "u |∈| x2"
  and     "v |∈| x2"
  and     "u ∈ L M1"
  and     "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
  using assms(1,2,3)
proof (induction "length xss" arbitrary: xss b don rule: less_induct)
  case less
  show ?case proof (cases xss)
    case Nil
    show ?thesis using less.prems(3) less.prems(1)[OF _ assms(4,5,6,7)] unfolding Nil 
      by auto
  next
    case (Cons x xs)
    obtain hasChanged x' xs' where "simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')"
      using prod.exhaust by metis

    show ?thesis proof (cases hasChanged)
      case True
      then have "simple_cg_closure_phase_2' xss (b,don) = simple_cg_closure_phase_2' xs' (True,x'#don)"
        using ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')›
        unfolding Cons  
        by auto

      have *:"(⋀u v. u |∈| x ⟹ v |∈| x ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)" and 
           **:"(⋀x2 u v. x2 ∈ list.set xs ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
        using less.prems(2) unfolding Cons
        by (meson list.set_intros)+

      have "length xs' < length xss"
        unfolding Cons 
        using simple_cg_closure_phase_2_helper_True[of x xs] True
        unfolding ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')› fst_conv snd_conv
        by auto
      moreover have "(⋀x2 u v. x2 ∈ list.set (x' # don) ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"  
        using simple_cg_closure_phase_2_helper_validity_fst[of x M1 M2 xs, OF * **, of "λ a b c . a"] 
        using less.prems(1)
        unfolding ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')› fst_conv snd_conv
        using set_ConsD[of _ x' don] 
        by blast 
      moreover have "(⋀x2 u v. x2 ∈ list.set xs' ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
        using simple_cg_closure_phase_2_helper_validity_snd[of xs M1 M2 _ x, OF **, of "λ a b c . a"]
        unfolding ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')› fst_conv snd_conv
        by blast
      moreover have "x2 ∈ list.set (snd (simple_cg_closure_phase_2' xs' (True, x' # don)))"
        using less.prems(3) unfolding ‹simple_cg_closure_phase_2' xss (b,don) = simple_cg_closure_phase_2' xs' (True,x'#don)› .
      ultimately show ?thesis 
        using less.hyps[of xs' "x'#don"]
        by blast
    next
      case False
      then have "simple_cg_closure_phase_2' xss (b,don) = simple_cg_closure_phase_2' xs (b,x#don)"
        using ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')›
        unfolding Cons  
        by auto

      have "length xs < length xss"
        unfolding Cons by auto
      moreover have "(⋀x2 u v. x2 ∈ list.set (x # don) ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
        using less.prems(1,2) unfolding Cons
        by (metis list.set_intros(1) set_ConsD) 
      moreover have "(⋀x2 u v. x2 ∈ list.set xs ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
        using less.prems(2) unfolding Cons
        by (metis list.set_intros(2))
      moreover have "x2 ∈ list.set (snd (simple_cg_closure_phase_2' xs (b, x # don)))"
        using less.prems(3)
        unfolding ‹simple_cg_closure_phase_2' xss (b,don) = simple_cg_closure_phase_2' xs (b,x#don)›
        unfolding Cons .
      ultimately show ?thesis 
        using less.hyps[of xs "x#don" b]
        by blast
    qed
  qed
qed


lemma simple_cg_closure_phase_2'_length :
  "length (snd (simple_cg_closure_phase_2' xss (b,don))) ≤ length xss + length don"
proof (induction "length xss" arbitrary: xss b don rule: less_induct)
  case less
  show ?case proof (cases xss)
    case Nil
    then show ?thesis by auto
  next
    case (Cons x xs)
    obtain hasChanged x' xs' where "simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')"
      using prod.exhaust by metis

    show ?thesis proof (cases hasChanged)
      case True
      then have "simple_cg_closure_phase_2' xss (b,don) = simple_cg_closure_phase_2' xs' (True,x'#don)"
        using ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')›
        unfolding Cons  
        by auto
      have "length xs' < length xss"
        using simple_cg_closure_phase_2_helper_True[of x xs] True
        unfolding ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')› snd_conv fst_conv
        unfolding Cons
        by auto

      then show ?thesis
        using less.hyps[of xs' True "x'#don"] 
        unfolding ‹simple_cg_closure_phase_2' xss (b,don) = simple_cg_closure_phase_2' xs' (True,x'#don)› 
        unfolding Cons by auto
    next
      case False 
      then have "simple_cg_closure_phase_2' xss (b,don) = simple_cg_closure_phase_2' xs (b,x#don)"
        using ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')›
        unfolding Cons  
        by auto

      show ?thesis
        using less.hyps[of xs b "x#don"]
        unfolding ‹simple_cg_closure_phase_2' xss (b,don) = simple_cg_closure_phase_2' xs (b,x#don)›
        unfolding Cons
        by auto
    qed
  qed
qed


lemma simple_cg_closure_phase_2'_True :
  assumes "fst (simple_cg_closure_phase_2' xss (False,don))" 
  and     "xss ≠ []"
shows "length (snd (simple_cg_closure_phase_2' xss (False,don))) < length xss + length don"
  using assms
proof (induction "length xss" arbitrary: xss don rule: less_induct)
  case less
  show ?case proof (cases xss)
    case Nil
    then show ?thesis 
      using less.prems(2) by auto
  next
    case (Cons x xs)
    obtain hasChanged x' xs' where "simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')"
      using prod.exhaust by metis

    show ?thesis proof (cases hasChanged)
      case True
      then have "simple_cg_closure_phase_2' xss (False,don) = simple_cg_closure_phase_2' xs' (True,x'#don)"
        using ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')›
        unfolding Cons  
        by auto
      have "length xs' < length xs"
        using simple_cg_closure_phase_2_helper_True[of x xs] True
        unfolding ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')› snd_conv fst_conv
        unfolding Cons
        by auto
      moreover have "length (snd (simple_cg_closure_phase_2' xs' (True,x'#don))) ≤ length xs' + length (x'#don)"
        using simple_cg_closure_phase_2'_length by metis
      ultimately show ?thesis
        unfolding ‹simple_cg_closure_phase_2' xss (False,don) = simple_cg_closure_phase_2' xs' (True,x'#don)›
        unfolding Cons
        by auto
    next
      case False 
      then have "simple_cg_closure_phase_2' xss (False,don) = simple_cg_closure_phase_2' xs (False,x#don)"
        using ‹simple_cg_closure_phase_2_helper x xs = (hasChanged,x',xs')›
        unfolding Cons  
        by auto

      have "xs ≠ []"
        using ‹simple_cg_closure_phase_2' xss (False, don) = simple_cg_closure_phase_2' xs (False, x # don)› less.prems(1) by auto

      show ?thesis
        using less.hyps[of xs "x#don", OF _ _ ‹xs ≠ []›]
        using less.prems(1)
        unfolding ‹simple_cg_closure_phase_2' xss (False,don) = simple_cg_closure_phase_2' xs (False,x#don)›
        unfolding Cons
        by auto
    qed
  qed
qed


(* closure operation (2) *)
fun simple_cg_closure_phase_2 :: "'a simple_cg ⇒ (bool × 'a simple_cg)" where
  "simple_cg_closure_phase_2 xs = simple_cg_closure_phase_2' xs (False,[])" 


lemma simple_cg_closure_phase_2_validity :
  assumes "⋀ x2 u v . x2 ∈ list.set xss ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "x2 ∈ list.set (snd (simple_cg_closure_phase_2 xss))"
  and     "u |∈| x2"
  and     "v |∈| x2"
  and     "u ∈ L M1"
  and     "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
  using assms(2)
  unfolding simple_cg_closure_phase_2.simps
  using simple_cg_closure_phase_2'_validity[OF _ assms(1) _ assms(3,4,5,6), of "[]" xss "λ a b c . a" False] 
  by auto

lemma simple_cg_closure_phase_2_length :
  "length (snd (simple_cg_closure_phase_2 xss)) ≤ length xss"
  unfolding simple_cg_closure_phase_2.simps
  using simple_cg_closure_phase_2'_length[of xss False "[]"] 
  by auto

lemma simple_cg_closure_phase_2_True :
  assumes "fst (simple_cg_closure_phase_2 xss)" 
shows "length (snd (simple_cg_closure_phase_2 xss)) < length xss"
proof -
  have "xss ≠ []"
    using assms by auto
  then show ?thesis
    using simple_cg_closure_phase_2'_True[of xss "[]"] assms by auto
qed



function simple_cg_closure :: "'a simple_cg ⇒ 'a simple_cg" where
  "simple_cg_closure g = (let (hasChanged1,g1) = simple_cg_closure_phase_1 g;
                       (hasChanged2,g2) = simple_cg_closure_phase_2 g1
     in if hasChanged1 ∨ hasChanged2
        then simple_cg_closure g2
        else g2)"
  by pat_completeness auto
termination
proof -
  {
    fix g :: "'a simple_cg"
    fix x hasChanged1 g1 xb hasChanged2 g2
    assume "x = simple_cg_closure_phase_1 g" 
           "(hasChanged1, g1) = x" 
           "xb = simple_cg_closure_phase_2 g1" 
           "(hasChanged2, g2) = xb" 
           "hasChanged1 ∨ hasChanged2"
  
    then have "simple_cg_closure_phase_1 g = (hasChanged1, g1)"
          and "simple_cg_closure_phase_2 g1 = (hasChanged2, g2)"
      by auto
  
    have "length g1 ≤ length g"
      using ‹simple_cg_closure_phase_1 g = (hasChanged1, g1)›
      using simple_cg_closure_phase_1_length[of g] 
      by auto 
    have "length g2 ≤ length g1"
      using ‹simple_cg_closure_phase_2 g1 = (hasChanged2, g2)›
      using simple_cg_closure_phase_2_length[of g1] 
      by auto
    
  
    consider hasChanged1 | hasChanged2
      using ‹hasChanged1 ∨ hasChanged2› by blast
    then have "length g2 < length g"
    proof cases
      case 1
      then have "length g1 < length g"
        using ‹simple_cg_closure_phase_1 g = (hasChanged1, g1)›
        using simple_cg_closure_phase_1_True[of g]
        by auto
      then show ?thesis
        using ‹length g2 ≤ length g1›
        by linarith
    next
      case 2
      then have "length g2 < length g1"
        using ‹simple_cg_closure_phase_2 g1 = (hasChanged2, g2)›
        using simple_cg_closure_phase_2_True[of g1]
        by auto
      then show ?thesis
        using ‹length g1 ≤ length g›
        by linarith
    qed
    then have "(g2, g) ∈ measure length"
      by auto
  }
  then show ?thesis by (relation "measure length"; force)
qed


lemma simple_cg_closure_validity :
  assumes "observable M1" and "observable M2"
  and     "⋀ x2 u v . x2 ∈ list.set g ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "x2 ∈ list.set (simple_cg_closure g)"
  and     "u |∈| x2"
  and     "v |∈| x2"
  and     "u ∈ L M1"
  and     "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
  using assms(3,4)
proof (induction "length g" arbitrary: g rule: less_induct)
  case less

  obtain hasChanged1 hasChanged2 g1 g2 where "simple_cg_closure_phase_1 g = (hasChanged1, g1)"
                                         and "simple_cg_closure_phase_2 g1 = (hasChanged2, g2)"
    using prod.exhaust by metis

  have "length g1 ≤ length g"
    using ‹simple_cg_closure_phase_1 g = (hasChanged1, g1)›
    using simple_cg_closure_phase_1_length[of g] 
    by auto 
  have "length g2 ≤ length g1"
    using ‹simple_cg_closure_phase_2 g1 = (hasChanged2, g2)›
    using simple_cg_closure_phase_2_length[of g1] 
    by auto

  have "(⋀x2 u v. x2 ∈ list.set g2 ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
  proof -
    have "(⋀x2 u v. x2 ∈ list.set g1 ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
      using simple_cg_closure_phase_1_validity[OF assms(1,2), of g]
      using less.prems(1)
      unfolding ‹simple_cg_closure_phase_1 g = (hasChanged1, g1)› snd_conv 
      by blast
    then show "(⋀x2 u v. x2 ∈ list.set g2 ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
      using simple_cg_closure_phase_2_validity[of g1]
      unfolding ‹simple_cg_closure_phase_2 g1 = (hasChanged2, g2)› snd_conv
      by blast
  qed 

  show ?thesis proof (cases "hasChanged1 ∨ hasChanged2")
    case True
    then consider hasChanged1 | hasChanged2
      by blast
    then have "length g2 < length g"
    proof cases
      case 1
      then have "length g1 < length g"
        using ‹simple_cg_closure_phase_1 g = (hasChanged1, g1)›
        using simple_cg_closure_phase_1_True[of g]
        by auto
      then show ?thesis
        using ‹length g2 ≤ length g1›
        by linarith
    next
      case 2
      then have "length g2 < length g1"
        using ‹simple_cg_closure_phase_2 g1 = (hasChanged2, g2)›
        using simple_cg_closure_phase_2_True[of g1]
        by auto
      then show ?thesis
        using ‹length g1 ≤ length g›
        by linarith
    qed
    moreover have "x2 ∈ list.set (simple_cg_closure g2)"
      using less.prems(2)
      using ‹simple_cg_closure_phase_1 g = (hasChanged1, g1)› ‹simple_cg_closure_phase_2 g1 = (hasChanged2, g2)› True
      by auto
    moreover note ‹(⋀x2 u v. x2 ∈ list.set g2 ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)›
    ultimately show ?thesis 
      using less.hyps[of g2]
      by blast      
  next
    case False
    then have "(simple_cg_closure g) = g2"
      using ‹simple_cg_closure_phase_1 g = (hasChanged1, g1)› ‹simple_cg_closure_phase_2 g1 = (hasChanged2, g2)› 
      by auto
    show ?thesis 
      using less.prems(2)
      using ‹(⋀x2 u v. x2 ∈ list.set g2 ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)› assms(5,6,7,8)
      unfolding ‹(simple_cg_closure g) = g2›
      by blast
  qed
qed


(* when inserting α this also for all α1@α2 = α and β in [α1] inserts β@α2 -- extremely inefficient *)
fun simple_cg_insert_with_conv :: "('a::linorder) simple_cg ⇒ 'a list ⇒ 'a simple_cg" where
  "simple_cg_insert_with_conv g ys = (let
      insert_for_prefix = (λ g i . let
                                    pref = take i ys;
                                    suff = drop i ys;
                                    pref_conv = simple_cg_lookup g pref
                                  in foldl (λ g' ys' . simple_cg_insert' g' (ys'@suff)) g pref_conv);
      g' = simple_cg_insert g ys;
      g'' = foldl insert_for_prefix g' [0..<length ys]
  in simple_cg_closure g'')"


fun simple_cg_merge :: "'a simple_cg ⇒ 'a list ⇒ 'a list ⇒ 'a simple_cg" where
  "simple_cg_merge g ys1 ys2 = simple_cg_closure ({|ys1,ys2|}#g)"

lemma simple_cg_merge_validity :
  assumes "observable M1" and "observable M2"
  and     "converge M1 u' v' ∧ converge M2 u' v'"
  and     "⋀ x2 u v . x2 ∈ list.set g ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
  and     "x2 ∈ list.set (simple_cg_merge g u' v')"
  and     "u |∈| x2"
  and     "v |∈| x2"
  and     "u ∈ L M1"
  and     "u ∈ L M2"
shows "converge M1 u v ∧ converge M2 u v"
proof -
  have "(⋀x2 u v. x2 ∈ list.set ({|u',v'|}#g) ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
  proof -
    fix x2 u v assume "x2 ∈ list.set ({|u',v'|}#g)" and "u |∈| x2" and "v |∈| x2" and "u ∈ L M1" and "u ∈ L M2"
    then consider "x2 = {|u',v'|}" | "x2 ∈ list.set g"
      by auto
    then show "converge M1 u v ∧ converge M2 u v" proof cases
      case 1
      then have "u ∈ {u',v'}" and "v ∈ {u',v'}"
        using ‹u |∈| x2› ‹v |∈| x2› by auto
      then show ?thesis 
        using assms(3) 
        by (cases "u = u'"; cases "v = v'"; auto)
    next
      case 2
      then show ?thesis 
        using assms(4) ‹u |∈| x2› ‹v |∈| x2› ‹u ∈ L M1› ‹u ∈ L M2›
        by blast
    qed
  qed
  moreover have "x2 ∈ list.set (simple_cg_closure ({|u',v'|}#g))"  
    using assms(5) by auto
  ultimately show ?thesis
    using simple_cg_closure_validity[OF assms(1,2) _ _ assms(6,7,8,9)]
    by blast
qed
  



subsection ‹Invariants›


lemma simple_cg_lookup_iff :
  "β ∈ list.set (simple_cg_lookup G α) ⟷ (β = α ∨ (∃ x . x ∈ list.set G ∧ α |∈| x ∧ β |∈| x))"
proof (induction G rule: rev_induct)
  case Nil
  then show ?case by auto
next
  case (snoc x G)
  show ?case proof (cases "α |∈| x ∧ β |∈| x")
    case True
    then have "β ∈ list.set (simple_cg_lookup (G@[x]) α)"
      unfolding simple_cg_lookup.simps
      unfolding sorted_list_of_set_set
      by simp
    then show ?thesis 
      using True by auto
  next
    case False
    have "β ∈ list.set (simple_cg_lookup (G@[x]) α) = (β = α ∨ (β ∈ list.set (simple_cg_lookup G α)))"
    proof -
      consider "α |∉| x" | "β |∉| x"
        using False by blast
      then show "β ∈ list.set (simple_cg_lookup (G@[x]) α) = (β = α ∨ (β ∈ list.set (simple_cg_lookup G α)))"
      proof cases
        case 1
        then show ?thesis  
          unfolding simple_cg_lookup.simps
          unfolding sorted_list_of_set_set 
          by auto
      next
        case 2
        then have "β ∉ list.set (sorted_list_of_fset x)"
          by simp          
        then have "(β ∈ list.set (simple_cg_lookup (G@[x]) α)) = (β ∈ Set.insert α (list.set (simple_cg_lookup G α)))"
          unfolding simple_cg_lookup.simps
          unfolding sorted_list_of_set_set 
          by auto
        then show ?thesis 
          by (induction G; auto)
      qed 
    qed
    moreover have "(∃ x' . x' ∈ list.set (G@[x]) ∧ α |∈| x' ∧ β |∈| x') = (∃ x . x ∈ list.set G ∧ α |∈| x ∧ β |∈| x)"
      using False by auto
    ultimately show ?thesis
      using snoc.IH
      by blast
  qed
qed


lemma simple_cg_insert'_invar :
  "convergence_graph_insert_invar M1 M2 simple_cg_lookup simple_cg_insert'"
proof -
  have "⋀ G γ α β . γ ∈ L M1 ⟹
          γ ∈ L M2 ⟹
          (⋀α . α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup G α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup G α) ⟶ converge M1 α β ∧ converge M2 α β)) ⟹
          α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup (simple_cg_insert' G γ) α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup (simple_cg_insert' G γ) α) ⟶ converge M1 α β ∧ converge M2 α β)"
  proof 
    fix G γ α 
    assume "γ ∈ L M1"
    and    "γ ∈ L M2"
    and  *:"(⋀α . α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup G α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup G α) ⟶ converge M1 α β ∧ converge M2 α β))"
    and    "α ∈ L M1" 
    and    "α ∈ L M2"

    show "α ∈ list.set (simple_cg_lookup (simple_cg_insert' G γ) α)"
      unfolding simple_cg_lookup.simps
      unfolding sorted_list_of_set_set 
      by auto


    have "⋀ β . β ∈ list.set (simple_cg_lookup (simple_cg_insert' G γ) α) ⟹ converge M1 α β ∧ converge M2 α β"
    proof -
      fix β
      assume **: "β ∈ list.set (simple_cg_lookup (simple_cg_insert' G γ) α)"
      show "converge M1 α β ∧ converge M2 α β"

    proof (cases "β ∈ list.set (simple_cg_lookup G α)")
      case True
      then show ?thesis 
        using *[OF ‹α ∈ L M1› ‹α ∈ L M2›]
        by presburger 
    next
      case False

      show ?thesis proof (cases "find ((|∈|) γ) G")
        case None
        then have "(simple_cg_insert' G γ) = {|γ|}#G" 
          by auto

        have "α = γ ∧ β = γ"
          using False ‹β ∈ list.set (simple_cg_lookup (simple_cg_insert' G γ) α)› 
          unfolding ‹(simple_cg_insert' G γ) = {|γ|}#G›
          by (metis fsingleton_iff set_ConsD simple_cg_lookup_iff)
        then show ?thesis
          using ‹γ ∈ L M1› ‹γ ∈ L M2› by auto
      next
        case (Some x)
        then have "(simple_cg_insert' G γ) = G" 
          by auto
        then show ?thesis 
          using *[OF ‹α ∈ L M1› ‹α ∈ L M2›] **
          by presburger
        qed
      qed
    qed
    then show "(∀ β . β ∈ list.set (simple_cg_lookup (simple_cg_insert' G γ) α) ⟶ converge M1 α β ∧ converge M2 α β)"
      by blast
  qed
  then show ?thesis
    unfolding convergence_graph_insert_invar_def convergence_graph_lookup_invar_def
    by blast
qed


lemma simple_cg_insert'_foldl_helper:
  assumes "list.set xss ⊆ L M1 ∩ L M2"
  and     "(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
shows     "(⋀α β. β ∈ list.set (simple_cg_lookup (foldl (λ xs' ys' . simple_cg_insert' xs' ys') G xss) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
  using ‹list.set xss ⊆ L M1 ∩ L M2›
proof (induction xss rule: rev_induct)
  case Nil
  then show ?case 
    using ‹(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)›
    by auto
next
  case (snoc x xs)

  have "x ∈ L M1" and "x ∈ L M2"
    using snoc.prems by auto
  
  have "list.set xs ⊆ L M1 ∩ L M2"
    using snoc.prems by auto
  then have *:"(⋀α β. β ∈ list.set (simple_cg_lookup (foldl (λ xs' ys'. simple_cg_insert' xs' ys') G xs) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
    using snoc.IH
    by blast

  have **:"(foldl (λ xs' ys'. simple_cg_insert' xs' ys') G (xs@[x])) = simple_cg_insert' (foldl (λ xs' ys' . simple_cg_insert' xs' ys') G xs) x"
    by auto        

  show ?case 
    using snoc.prems(1,2,3) * ‹x ∈ L M1› ‹x ∈ L M2›
    unfolding **
    using simple_cg_insert'_invar[of M1 M2]
    unfolding convergence_graph_insert_invar_def convergence_graph_lookup_invar_def
    using simple_cg_lookup_iff 
    by blast
qed


lemma simple_cg_insert_invar :                  
  "convergence_graph_insert_invar M1 M2 simple_cg_lookup simple_cg_insert"
proof -

  have "⋀ G γ α β . γ ∈ L M1 ⟹
          γ ∈ L M2 ⟹
          (⋀α . α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup G α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup G α) ⟶ converge M1 α β ∧ converge M2 α β)) ⟹
          α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup (simple_cg_insert G γ) α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup (simple_cg_insert G γ) α) ⟶ converge M1 α β ∧ converge M2 α β)"
  proof 
    fix G γ α 
    assume "γ ∈ L M1"
    and    "γ ∈ L M2"
    and  *:"(⋀α . α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup G α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup G α) ⟶ converge M1 α β ∧ converge M2 α β))"
    and    "α ∈ L M1" 
    and    "α ∈ L M2"

    show "α ∈ list.set (simple_cg_lookup (simple_cg_insert G γ) α)" 
      unfolding simple_cg_lookup.simps
      unfolding sorted_list_of_set_set 
      by auto

    note simple_cg_insert'_foldl_helper[of "prefixes γ" M1 M2]
    moreover have "list.set (prefixes γ) ⊆ L M1 ∩ L M2"
      by (metis (no_types, lifting) IntI ‹γ ∈ L M1› ‹γ ∈ L M2› language_prefix prefixes_set_ob subsetI) 
    ultimately show "(∀ β . β ∈ list.set (simple_cg_lookup (simple_cg_insert G γ) α) ⟶ converge M1 α β ∧ converge M2 α β)"      
      using ‹α ∈ L M1› ‹α ∈ L M2›
      by (metis "*" simple_cg_insert.simps) 
  qed
  then show ?thesis
    unfolding convergence_graph_insert_invar_def convergence_graph_lookup_invar_def
    by blast
qed


lemma simple_cg_closure_invar_helper :
  assumes "observable M1" and "observable M2"
  and     "(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
  and     "β ∈ list.set (simple_cg_lookup (simple_cg_closure G) α)"
  and     "α ∈ L M1" and "α ∈ L M2"
shows "converge M1 α β ∧ converge M2 α β"
proof (cases "β = α")
  case True
  then show ?thesis using assms(5,6) by auto 
next
  case False
  show ?thesis 
  proof 
  
    obtain x where "x ∈ list.set (simple_cg_closure G)" and "α |∈| x" and "β |∈| x"
      using False ‹β ∈ list.set (simple_cg_lookup (simple_cg_closure G) α)› unfolding simple_cg_lookup_iff
      by blast
  
    have "⋀ x2 u v . x2 ∈ list.set G ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v"
      using ‹(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)› 
      unfolding simple_cg_lookup_iff
      by blast
  
  
  
    have "(⋀x2 u v. x2 ∈ list.set G ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
      using ‹(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)› 
      unfolding simple_cg_lookup_iff by blast
    then show "converge M1 α β"
      using ‹α |∈| x› ‹β |∈| x› ‹x ∈ list.set (simple_cg_closure G)› assms(1) assms(2) assms(5) assms(6) simple_cg_closure_validity by blast
  
    have "(⋀x2 u v. x2 ∈ list.set G ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
      using ‹(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)› 
      unfolding simple_cg_lookup_iff by blast
    then show "converge M2 α β"
      using ‹α |∈| x› ‹β |∈| x› ‹x ∈ list.set (simple_cg_closure G)› assms(1) assms(2) assms(5) assms(6) simple_cg_closure_validity by blast    
  qed
qed



lemma simple_cg_merge_invar :
  assumes "observable M1" and "observable M2"
shows "convergence_graph_merge_invar M1 M2 simple_cg_lookup simple_cg_merge"
proof -

  have "⋀ G γ γ' α β.
       converge M1 γ γ' ⟹
       converge M2 γ γ' ⟹
       (⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β) ⟹
       β ∈ list.set (simple_cg_lookup (simple_cg_merge G γ γ') α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β"
  proof -
    fix G γ γ' α β
    assume "converge M1 γ γ'"
           "converge M2 γ γ'"
           "(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
           "β ∈ list.set (simple_cg_lookup (simple_cg_merge G γ γ') α)"
           "α ∈ L M1" 
           "α ∈ L M2"
    show "converge M1 α β ∧ converge M2 α β"
    proof (cases "β = α")
      case True
      then show ?thesis using ‹α ∈ L M1› ‹α ∈ L M2› by auto
    next
      case False
      then obtain x where "x ∈ list.set (simple_cg_merge G γ γ')" and "α |∈| x" and "β |∈| x"
        using ‹β ∈ list.set (simple_cg_lookup (simple_cg_merge G γ γ') α)› unfolding simple_cg_lookup_iff
        by blast
  
      have "(⋀x2 u v. x2 ∈ list.set G ⟹ u |∈| x2 ⟹ v |∈| x2 ⟹ u ∈ L M1 ⟹ u ∈ L M2 ⟹ converge M1 u v ∧ converge M2 u v)"
        using ‹(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)› 
        unfolding simple_cg_lookup_iff by blast
      then show ?thesis
        using simple_cg_merge_validity[OF assms(1,2) _ _ ‹x ∈ list.set (simple_cg_merge G γ γ')› ‹α |∈| x› ‹β |∈| x› ‹α ∈ L M1› ‹α ∈ L M2›] 
              ‹converge M1 γ γ'› ‹converge M2 γ γ'›
        by blast
    qed
  qed
  then show ?thesis 
    unfolding convergence_graph_merge_invar_def convergence_graph_lookup_invar_def
    unfolding simple_cg_lookup_iff
    by metis
qed


lemma simple_cg_empty_invar :
  "convergence_graph_lookup_invar M1 M2 simple_cg_lookup simple_cg_empty"
  unfolding convergence_graph_lookup_invar_def simple_cg_empty_def 
  by auto


lemma simple_cg_initial_invar :
  assumes "observable M1"
  shows "convergence_graph_initial_invar M1 M2 simple_cg_lookup simple_cg_initial"
proof -

  have "⋀ T . (L M1 ∩ set T = (L M2 ∩ set T)) ⟹ finite_tree T ⟹ (⋀α β. β ∈ list.set (simple_cg_lookup (simple_cg_initial M1 T) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
  proof -
    fix T assume "(L M1 ∩ set T = (L M2 ∩ set T))" and "finite_tree T"
    then have "list.set (filter (is_in_language M1 (initial M1)) (sorted_list_of_sequences_in_tree T)) ⊆ L M1 ∩ L M2"
      unfolding is_in_language_iff[OF assms fsm_initial]
      using sorted_list_of_sequences_in_tree_set[OF ‹finite_tree T›]
      by auto 
    moreover have "(⋀α β. β ∈ list.set (simple_cg_lookup simple_cg_empty α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
      using simple_cg_empty_invar
      unfolding convergence_graph_lookup_invar_def
      by blast
    ultimately show "(⋀α β. β ∈ list.set (simple_cg_lookup (simple_cg_initial M1 T) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
      using simple_cg_insert'_foldl_helper[of "(filter (is_in_language M1 (initial M1)) (sorted_list_of_sequences_in_tree T))" M1 M2]
      unfolding simple_cg_initial.simps
      by blast
  qed
  then show ?thesis
    unfolding convergence_graph_initial_invar_def convergence_graph_lookup_invar_def
    using simple_cg_lookup_iff by blast
qed


lemma simple_cg_insert_with_conv_invar :                  
  assumes "observable M1"
  assumes "observable M2"
  shows  "convergence_graph_insert_invar M1 M2 simple_cg_lookup simple_cg_insert_with_conv"
proof -
  have "⋀ G γ α β . γ ∈ L M1 ⟹
          γ ∈ L M2 ⟹
          (⋀α . α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup G α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup G α) ⟶ converge M1 α β ∧ converge M2 α β)) ⟹
          α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup (simple_cg_insert_with_conv G γ) α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup (simple_cg_insert_with_conv G γ) α) ⟶ converge M1 α β ∧ converge M2 α β)"
  proof 
    fix G ys α 
    assume "ys ∈ L M1"
    and    "ys ∈ L M2"
    and  *:"(⋀α . α ∈ L M1 ⟹ α ∈ L M2 ⟹ α ∈ list.set (simple_cg_lookup G α) ∧ (∀ β . β ∈ list.set (simple_cg_lookup G α) ⟶ converge M1 α β ∧ converge M2 α β))"
    and    "α ∈ L M1" 
    and    "α ∈ L M2"

    show "α ∈ list.set (simple_cg_lookup (simple_cg_insert_with_conv G ys) α)"
      using simple_cg_lookup_iff by blast
      

    have "⋀ β . β ∈ list.set (simple_cg_lookup (simple_cg_insert_with_conv G ys) α) ⟹ converge M1 α β ∧ converge M2 α β"
    proof -
      fix β
      assume "β ∈ list.set (simple_cg_lookup (simple_cg_insert_with_conv G ys) α)"
  
      define insert_for_prefix where insert_for_prefix: 
        "insert_for_prefix = (λ g i . let
                                      pref = take i ys;
                                      suff = drop i ys;
                                      pref_conv = simple_cg_lookup g pref
                                    in foldl (λ g' ys' . simple_cg_insert' g' (ys'@suff)) g pref_conv)"
      define g' where g': "g' = simple_cg_insert G ys"
      define g'' where g'': "g'' = foldl insert_for_prefix g' [0..<length ys]"
  
      have "simple_cg_insert_with_conv G ys = simple_cg_closure g''"
        unfolding simple_cg_insert_with_conv.simps g'' g' insert_for_prefix Let_def by force
  
      have g'_invar: "(⋀α β. β ∈ list.set (simple_cg_lookup g' α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
        using g' *
        using simple_cg_insert_invar ‹ys ∈ L M1› ‹ys ∈ L M2›
        unfolding convergence_graph_insert_invar_def convergence_graph_lookup_invar_def
        by blast
  
      have insert_for_prefix_invar: "⋀ i g . (⋀α β. β ∈ list.set (simple_cg_lookup g α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β) ⟹ (⋀α β. β ∈ list.set (simple_cg_lookup (insert_for_prefix g i) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
      proof -
        fix i g assume "(⋀α β. β ∈ list.set (simple_cg_lookup g α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
  
        define pref where pref: "pref = take i ys"
        define suff where suff: "suff = drop i ys"
        let ?pref_conv = "simple_cg_lookup g pref"
  
        have "insert_for_prefix g i = foldl (λ g' ys' . simple_cg_insert' g' (ys'@suff)) g ?pref_conv"
          unfolding insert_for_prefix pref suff Let_def by force
  
        have "ys = pref @ suff"
          unfolding pref suff by auto
        then have "pref ∈ L M1" and "pref ∈ L M2"
          using ‹ys ∈ L M1› ‹ys ∈ L M2› language_prefix by metis+
  
        have insert_step_invar: "⋀ ys' pc G . list.set pc ⊆ list.set (simple_cg_lookup g pref) ⟹ ys' ∈ list.set pc ⟹
                        (⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β) ⟹ 
                        (⋀α β. β ∈ list.set (simple_cg_lookup (simple_cg_insert' G (ys'@suff)) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
        proof -
          fix ys' pc G
          assume "list.set pc ⊆ list.set (simple_cg_lookup g pref)" 
             and "ys' ∈ list.set pc"
             and "(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
          then have "converge M1 pref ys'" and "converge M2 pref ys'"
            using ‹⋀β α. β ∈ list.set (simple_cg_lookup g α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β› 
            using ‹pref ∈ L M1› ‹pref ∈ L M2›
            by blast+
  
          have "(ys'@suff) ∈ L M1"
            using ‹converge M1 pref ys'›
            using ‹ys = pref @ suff› ‹ys ∈ L M1› assms(1) converge_append_language_iff by blast
          moreover have "(ys'@suff) ∈ L M2"
            using ‹converge M2 pref ys'›
            using ‹ys = pref @ suff› ‹ys ∈ L M2› assms(2) converge_append_language_iff by blast
          ultimately show "(⋀α β. β ∈ list.set (simple_cg_lookup (simple_cg_insert' G (ys'@suff)) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
            using ‹(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)›
            using simple_cg_insert'_invar[of M1 M2]
            unfolding convergence_graph_insert_invar_def convergence_graph_lookup_invar_def
            using simple_cg_lookup_iff by blast
        qed
  
        have insert_foldl_invar: "⋀ pc G . list.set pc ⊆ list.set (simple_cg_lookup g pref) ⟹ 
                        (⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β) ⟹ 
                        (⋀α β. β ∈ list.set (simple_cg_lookup (foldl (λ g' ys' . simple_cg_insert' g' (ys'@suff)) G pc) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)" 
        proof -
          fix pc G assume "list.set pc ⊆ list.set (simple_cg_lookup g pref)" 
                     and "(⋀α β. β ∈ list.set (simple_cg_lookup G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
  
          then show "(⋀α β. β ∈ list.set (simple_cg_lookup (foldl (λ g' ys' . simple_cg_insert' g' (ys'@suff)) G pc) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
          proof (induction pc rule: rev_induct)
            case Nil
            then show ?case by auto
          next
            case (snoc a pc)

            have **:"(foldl (λg' ys'. simple_cg_insert' g' (ys' @ suff)) G (pc @ [a]))
                   = simple_cg_insert' (foldl (λg' ys'. simple_cg_insert' g' (ys' @ suff)) G pc) (a@suff)"
              unfolding foldl_append by auto
            have "list.set pc ⊆ list.set (simple_cg_lookup g pref)"
              using snoc.prems(4) by auto 
            then have *: "(⋀α β. β ∈ list.set (simple_cg_lookup (foldl (λ g' ys' . simple_cg_insert' g' (ys'@suff)) G pc) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
              using snoc.IH
              using snoc.prems(5) by blast  
            
            have "a ∈ list.set (pc @ [a])" by auto
            then show ?case 
              using snoc.prems(1,2,3)
              unfolding **
              using insert_step_invar[OF snoc.prems(4), of a "(foldl (λ g' ys' . simple_cg_insert' g' (ys'@suff)) G pc)", OF _  *]
              by blast
          qed
        qed
        
        show "(⋀α β. β ∈ list.set (simple_cg_lookup (insert_for_prefix g i) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
          using insert_foldl_invar[of ?pref_conv g, OF _ ‹(⋀α β. β ∈ list.set (simple_cg_lookup g α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)›]
          unfolding ‹insert_for_prefix g i = foldl (λ g' ys' . simple_cg_insert' g' (ys'@suff)) g ?pref_conv›
          by blast
      qed
  
      have insert_for_prefix_foldl_invar: "⋀ ns . (⋀α β. β ∈ list.set (simple_cg_lookup (foldl insert_for_prefix g' ns) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
      proof -
        fix ns show "(⋀α β. β ∈ list.set (simple_cg_lookup (foldl insert_for_prefix g' ns) α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
        proof (induction ns rule: rev_induct)
          case Nil
          then show ?case using g'_invar by auto
        next
          case (snoc a ns)
          show ?case 
            using snoc.prems          
            using insert_for_prefix_invar [OF snoc.IH]
            by auto
        qed
      qed
  
      show ‹converge M1 α β ∧ converge M2 α β› 
        using ‹β ∈ list.set (simple_cg_lookup (simple_cg_insert_with_conv G ys) α)›
        unfolding ‹simple_cg_insert_with_conv G ys = simple_cg_closure g''› g''
        using insert_for_prefix_foldl_invar[of _ "[0..<length ys]" _]
        using simple_cg_closure_invar_helper[OF assms, of "(foldl insert_for_prefix g' [0..<length ys])", OF insert_for_prefix_foldl_invar[of _ "[0..<length ys]" _]]
        using ‹α ∈ L M1› ‹α ∈ L M2› by blast
    qed
    then show "(∀ β . β ∈ list.set (simple_cg_lookup (simple_cg_insert_with_conv G ys) α) ⟶ converge M1 α β ∧ converge M2 α β)"
      by blast
  qed

  then show ?thesis
    unfolding convergence_graph_insert_invar_def convergence_graph_lookup_invar_def
    by blast
qed



lemma simple_cg_lookup_with_conv_from_lookup_invar:
  assumes "observable M1" and "observable M2"
  and "convergence_graph_lookup_invar M1 M2 simple_cg_lookup G"
shows "convergence_graph_lookup_invar M1 M2 simple_cg_lookup_with_conv G"
proof -

  have "(⋀ α β. β ∈ list.set (simple_cg_lookup_with_conv G α) ⟹ α ∈ L M1 ⟹ α ∈ L M2 ⟹ converge M1 α β ∧ converge M2 α β)"
  proof -
    fix ys β assume "β ∈ list.set (simple_cg_lookup_with_conv G ys)" and "ys ∈ L M1" and "ys ∈ L M2"

    define lookup_for_prefix where lookup_for_prefix:
      "lookup_for_prefix = (λi . let
                                  pref = take i ys;
                                  suff = drop i ys;
                                  pref_conv = (foldl (|∪|) fempty (filter (λx . pref |∈| x) G))
                                in fimage (λ pref' . pref'@suff) pref_conv)"


    have "⋀ ns . β ∈ list.set (sorted_list_of_fset (finsert ys (foldl (λ cs i . lookup_for_prefix i |∪| cs) fempty ns))) ⟹ converge M1 ys β ∧ converge M2 ys β"
    proof -
      fix ns assume "β ∈ list.set (sorted_list_of_fset (finsert ys (foldl (λ cs i . lookup_for_prefix i |∪| cs) fempty ns)))"
      then show "converge M1 ys β ∧ converge M2 ys β"
      proof (induction ns rule: rev_induct)
        case Nil
        then show ?case using ‹ys ∈ L M1› ‹ys ∈ L M2› by auto
      next
        case (snoc a ns)

        have "list.set (sorted_list_of_fset (finsert ys (foldl (λ cs i . lookup_for_prefix i |∪| cs) fempty (ns@[a])))) =
                (fset (lookup_for_prefix a) ∪ list.set (sorted_list_of_fset (finsert ys (foldl (λ cs i . lookup_for_prefix i |∪| cs) fempty ns))))"
          by auto
        then consider "β ∈ fset (lookup_for_prefix a)" | "β ∈ list.set (sorted_list_of_fset (finsert ys (foldl (λ cs i . lookup_for_prefix i |∪| cs) fempty ns)))"
          using snoc.prems by auto
        then show ?case proof cases
          case 1
          define pref where pref: "pref = take a ys"
          define suff where suff: "suff = drop a ys"
          define pref_conv where pref_conv: "pref_conv = (foldl (|∪|) fempty (filter (λx . pref |∈| x) G))"
                                
          have "lookup_for_prefix a = fimage (λ pref' . pref'@suff) pref_conv"
            unfolding lookup_for_prefix pref suff pref_conv
            by metis
          then have "β ∈ list.set (map (λ pref' . pref'@suff) (sorted_list_of_fset (finsert pref (foldl (|∪|) {||} (filter ((|∈|) pref) G)))))"
            using 1 unfolding pref_conv by auto
          then obtain γ where "γ ∈ list.set (simple_cg_lookup G pref)"
                          and "β = γ@suff"
            unfolding simple_cg_lookup.simps
            by (meson set_map_elem)
          then have "converge M1 γ pref" and "converge M2 γ pref"
            using ‹convergence_graph_lookup_invar M1 M2 simple_cg_lookup G›
            unfolding convergence_graph_lookup_invar_def
            by (metis ‹ys ∈ L M1› ‹ys ∈ L M2› append_take_drop_id converge_sym language_prefix pref)+
          then show ?thesis
            by (metis ‹⋀thesis. (⋀γ. ⟦γ ∈ list.set (simple_cg_lookup G pref); β = γ @ suff⟧ ⟹ thesis) ⟹ thesis› ‹ys ∈ L M1› ‹ys ∈ L M2› append_take_drop_id assms(1) assms(2) assms(3) converge_append converge_append_language_iff convergence_graph_lookup_invar_def language_prefix pref suff) 
        next
          case 2
          then show ?thesis using snoc.IH by blast
        qed
      qed
    qed

    then show "converge M1 ys β ∧ converge M2 ys β"
      using ‹β ∈ list.set (simple_cg_lookup_with_conv G ys)›  
      unfolding simple_cg_lookup_with_conv.simps Let_def lookup_for_prefix sorted_list_of_set_set
      by blast 
  qed
  moreover have "⋀ α . α ∈ list.set (simple_cg_lookup_with_conv G α)"
    unfolding simple_cg_lookup_with_conv.simps by auto
  ultimately show ?thesis
    unfolding convergence_graph_lookup_invar_def 
    by blast
qed

lemma simple_cg_lookup_from_lookup_invar_with_conv:
  assumes "convergence_graph_lookup_invar M1 M2 simple_cg_lookup_with_conv G"
shows "convergence_graph_lookup_invar M1 M2 simple_cg_lookup G"
proof -

  have "⋀ α β. β ∈ list.set (simple_cg_lookup G α) ⟹ β ∈ list.set (simple_cg_lookup_with_conv G α)"
  proof -

    fix α β assume "β ∈ list.set (simple_cg_lookup G α)"

    define lookup_for_prefix where lookup_for_prefix:
      "lookup_for_prefix = (λi . let
                                  pref = take i α;
                                  suff = drop i α;
                                  pref_conv = simple_cg_lookup G pref
                                in map (λ pref' . pref'@suff) pref_conv)"

    have "lookup_for_prefix (length α) = simple_cg_lookup G α"
      unfolding lookup_for_prefix by auto
    moreover have "list.set (lookup_for_prefix (length α)) ⊆ list.set (simple_cg_lookup_with_conv G α)"
      unfolding simple_cg_lookup_with_conv.simps lookup_for_prefix Let_def sorted_list_of_set_set by auto
    ultimately show "β ∈ list.set (simple_cg_lookup_with_conv G α)"
      using ‹β ∈ list.set (simple_cg_lookup G α)›
      by (metis subsetD)
  qed

  then show ?thesis
    using assms
    unfolding convergence_graph_lookup_invar_def
    using simple_cg_lookup_iff by blast    
qed


lemma simple_cg_lookup_invar_with_conv_eq :
  assumes "observable M1" and "observable M2" 
  shows "convergence_graph_lookup_invar M1 M2 simple_cg_lookup_with_conv G = convergence_graph_lookup_invar M1 M2 simple_cg_lookup G"
  using simple_cg_lookup_with_conv_from_lookup_invar[OF assms] simple_cg_lookup_from_lookup_invar_with_conv[of M1 M2]
  by blast


lemma simple_cg_insert_invar_with_conv :    
  assumes "observable M1" and "observable M2"
shows "convergence_graph_insert_invar M1 M2 simple_cg_lookup_with_conv simple_cg_insert"
  using simple_cg_insert_invar[of M1 M2] 
  unfolding convergence_graph_insert_invar_def 
  unfolding simple_cg_lookup_invar_with_conv_eq[OF assms]
  .

lemma simple_cg_merge_invar_with_conv :
  assumes "observable M1" and "observable M2"
shows "convergence_graph_merge_invar M1 M2 simple_cg_lookup_with_conv simple_cg_merge"
  using simple_cg_merge_invar[OF assms] 
  unfolding convergence_graph_merge_invar_def 
  unfolding simple_cg_lookup_invar_with_conv_eq[OF assms]
  .

lemma simple_cg_initial_invar_with_conv :
  assumes "observable M1" and "observable M2"
  shows "convergence_graph_initial_invar M1 M2 simple_cg_lookup_with_conv simple_cg_initial"
  using simple_cg_initial_invar[OF assms(1), of M2] 
  unfolding convergence_graph_initial_invar_def 
  unfolding simple_cg_lookup_invar_with_conv_eq[OF assms]
  .


end