# 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

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 ({|```