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