theory Saturation imports Main begin subsection ‹Set operation closure for idempotent, associative, and commutative functions› lemma inv_to_set: "(∀ i < length ss. ss ! i ∈ S) ⟷ set ss ⊆ S" by (induct ss) (auto simp: nth_Cons split: nat.splits) lemma ac_comp_fun_commute: assumes "⋀ x y. f x y = f y x" and "⋀ x y z. f x (f y z) = f (f x y) z" shows "comp_fun_commute f" using assms unfolding comp_fun_commute_def by (auto simp: comp_def) fastforce lemma (in comp_fun_commute) fold_list_swap: "fold f xs (fold f ys y) = fold f ys (fold f xs y)" by (metis comp_fun_commute fold_commute fold_commute_apply) lemma (in comp_fun_commute) foldr_list_swap: "foldr f xs (foldr f ys y) = foldr f ys (foldr f xs y)" by (simp add: fold_list_swap foldr_conv_fold) lemma (in comp_fun_commute) foldr_to_fold: "foldr f xs = fold f xs" using comp_fun_commute foldr_fold[of _ f] by (auto simp: comp_def) lemma (in comp_fun_commute) fold_commute_f: "f x (foldr f xs y) = foldr f xs (f x y)" using comp_fun_commute unfolding foldr_to_fold by (auto simp: comp_def intro: fold_commute_apply) lemma closure_sound: assumes cl: "⋀ s t. s ∈ S ⟹ t ∈ S ⟹ f s t ∈ S" and com: "⋀ x y. f x y = f y x" and ass: "⋀ x y z. f x (f y z) = f (f x y) z" and fin: "set ss ⊆ S" "ss ≠ []" shows "fold f (tl ss) (hd ss) ∈ S" using assms(4-) proof (induct ss) case (Cons s ss) note IS = this show ?case proof (cases ss) case Nil then show ?thesis using IS by auto next case (Cons t ts) show ?thesis using IS assms(1) ac_comp_fun_commute[of f, OF com ass] unfolding Cons by (auto simp flip: comp_fun_commute.foldr_to_fold) (metis com comp_fun_commute.fold_commute_f) qed qed auto (* Writing a fold that does not take a base element may simplify the proves *) locale set_closure_oprator = fixes f assumes com [ac_simps]: "⋀ x y. f x y = f y x" and ass [ac_simps]: "⋀ x y z. f x (f y z) = f (f x y) z" and idem: "⋀ x. f x x = x" sublocale set_closure_oprator ⊆ comp_fun_idem using set_closure_oprator_axioms ac_comp_fun_commute by (auto simp: comp_fun_idem_def comp_fun_idem_axioms_def comp_def set_closure_oprator_def) context set_closure_oprator begin inductive_set closure for S where base [simp]: "s ∈ S ⟹ s ∈ closure S" | step [intro]: "s ∈ closure S ⟹ t ∈ closure S ⟹ f s t ∈ closure S" lemma closure_idem [simp]: "closure (closure S) = closure S" (is "?LS = ?RS") proof - {fix s assume "s ∈ ?LS" then have "s ∈ ?RS" by induct auto} moreover {fix s assume "s ∈ ?RS" then have "s ∈ ?LS" by induct auto} ultimately show ?thesis by blast qed lemma fold_dist: assumes "xs ≠ []" shows "f (fold f (tl xs) (hd xs)) t = fold f xs t" using assms proof (induct xs) case (Cons a xs) show ?case using Cons com ass fold_commute_f by (auto simp: comp_def foldr_to_fold) qed auto lemma closure_to_cons_list: assumes "s ∈ closure S" shows "∃ ss ≠ []. fold f (tl ss) (hd ss) = s ∧ (∀ i < length ss. ss ! i ∈ S)" using assms proof (induct) case (base s) then show ?case by (auto intro: exI[of _ "[s]"]) next case (step s t) then obtain ss ts where s: "fold f (tl ss) (hd ss) = s" and inv_s: "ss ≠ []" "∀ i < length ss. ss ! i ∈ S" and t: "fold f (tl ts) (hd ts) = t" and inv_t: "ts ≠ []" "∀ i < length ts. ts ! i ∈ S" by auto then show ?case by (auto simp: fold_dist nth_append intro!: exI[of _ "ss @ ts"]) (metis com fold_dist) qed lemma sound_fold: assumes "set ss ⊆ closure S" and "ss ≠ []" shows "fold f (tl ss) (hd ss) ∈ closure S" using assms using closure_sound[of "closure S" f] assms step by (auto simp add: com fun_left_comm) lemma closure_empty [simp]: "closure {} = {}" using closure_to_cons_list by auto lemma closure_mono: "S ⊆ T ⟹ closure S ⊆ closure T" proof fix s assume ass: "s ∈ closure S" then show "S ⊆ T ⟹ s ∈ closure T" by (induct) (auto simp: closure_to_cons_list) qed lemma closure_insert: "closure (insert x S) = {x} ∪ closure S ∪ {f x s | s. s ∈ closure S}" proof - {fix t assume ass: "t ∈ closure (insert x S)" "t ≠ x" "t ∉ closure S" from closure_to_cons_list[OF ass(1)] obtain ss where t: "fold f (tl ss) (hd ss) = t" and inv_t: "ss ≠ []" "∀ i < length ss. ss ! i ∈ insert x S" by auto then have mem: "x ∈ set ss" using ass(3) sound_fold[of ss] in_set_conv_nth by (force simp add: inv_to_set) have "∃ s. t = f x s ∧ s ∈ closure S" proof (cases "set ss = {x}") case True then show ?thesis using ass(2) t by (metis com finite.emptyI fold_dist fold_empty fold_insert_idem fold_set_fold idem inv_t(1)) next case False from False inv_t(1) mem obtain ts where split: "insert x (set ts) = set ss" "x ∉ set ts" "ts ≠ []" by auto (metis False List.finite_set Set.set_insert empty_set finite_insert finite_list) then have "∀ i < length ts. ts ! i ∈ S" using inv_t(2) split unfolding inv_to_set by auto moreover have "t = f x (Finite_Set.fold f (hd ts) (set (tl ts)))" using split t inv_t(1) by (metis List.finite_set com fold_dist fold_insert_idem2 fold_set_fold fun_left_idem idem) ultimately show ?thesis using sound_fold[OF _ split(3)] by (auto simp: foldr_to_fold fold_set_fold inv_to_set) force qed} then show ?thesis by (auto simp: fold_set_fold in_mono[OF closure_mono[OF subset_insertI[of S x]]]) qed lemma finite_S_finite_closure [intro]: "finite S ⟹ finite (closure S)" by (induct rule: finite.induct) (auto simp: closure_insert) end locale semilattice_closure_operator = cl: set_closure_oprator f for f :: "'a ⇒ 'a ⇒ 'a" + fixes less_eq e assumes neut_fun [simp]:"⋀ x. f e x = x" and neut_less [simp]: "⋀ x. less_eq e x" and sup_l: "⋀ x y. less_eq x (f x y)" and sup_r: "⋀ x y. less_eq y (f x y)" and upper_bound: "⋀ x y z. less_eq x z ⟹ less_eq y z ⟹ less_eq (f x y) z" and trans: "⋀ x y z. less_eq x y ⟹ less_eq y z ⟹ less_eq x z" and anti_sym: "⋀ x y. less_eq x y ⟹ less_eq y x ⟹ x = y" begin lemma unique_neut_elem [simp]: "f x y = e ⟷ x = e ∧ y = e" using neut_fun cl.fun_left_idem by (metis cl.com) abbreviation "closure S ≡ cl.closure S" lemma closure_to_cons_listE: assumes "s ∈ closure S" obtains ss where "ss ≠ []" "fold f ss e = s" "set ss ⊆ S" using cl.closure_to_cons_list[OF assms] cl.fold_dist by (auto simp: inv_to_set) (metis cl.com neut_fun) lemma sound_fold: assumes "set ss ⊆ closure S" "ss ≠ []" shows "fold f ss e ∈ closure S" using cl.sound_fold[OF assms] cl.fold_dist[OF assms(2)] by (metis cl.com neut_fun) abbreviation "supremum S ≡ Finite_Set.fold f e S" definition "smaller_subset x S ≡ {y. less_eq y x ∧ y ∈ S}" lemma smaller_subset_empty [simp]: "smaller_subset x {} = {}" by (auto simp: smaller_subset_def) lemma finite_smaller_subset [simp, intro]: "finite S ⟹ finite (smaller_subset x S)" by (auto simp: smaller_subset_def) lemma smaller_subset_mono: "smaller_subset x S ⊆ S" by (auto simp: smaller_subset_def) lemma sound_set_fold: assumes "set ss ⊆ closure S" and "ss ≠ []" shows "supremum (set ss) ∈ closure S" using sound_fold[OF assms] by (auto simp: cl.fold_set_fold) lemma supremum_neutral [simp]: assumes "finite S" and "supremum S = e" shows "S ⊆ {e}" using assms by (induct) auto lemma supremum_in_closure: assumes "finite S" and "R ⊆ closure S" and "R ≠ {}" shows "supremum R ∈ closure S" proof - obtain L where [simp]: "R = set L" using cl.finite_S_finite_closure[OF assms(1)] assms(2) finite_list by (metis infinite_super) then show ?thesis using sound_set_fold[of L S] assms by (cases L) auto qed lemma supremum_sound: assumes "finite S" shows "⋀ t. t ∈ S ⟹ less_eq t (supremum S)" using assms sup_l sup_r trans by induct (auto, blast) lemma supremum_sound_list: "∀ i < length ss. less_eq (ss ! i) (fold f ss e)" unfolding cl.fold_set_fold[symmetric] using supremum_sound[of "set ss"] by auto lemma smaller_subset_insert [simp]: "less_eq y x ⟹ smaller_subset x (insert y S) = insert y (smaller_subset x S)" "¬ less_eq y x ⟹ smaller_subset x (insert y S) = smaller_subset x S" by (auto simp: smaller_subset_def) lemma supremum_smaller_subset: assumes "finite S" shows "less_eq (supremum (smaller_subset x S)) x" using assms proof (induct) case (insert y F) then show ?case by (cases "less_eq y x") (auto simp: upper_bound) qed simp lemma pre_subset_eq_pos_subset [simp]: shows "smaller_subset x (closure S) = closure (smaller_subset x S)" (is "?LS = ?RS") proof - {fix s assume "s ∈ ?RS" then have "s ∈ ?LS" using upper_bound by induct (auto simp: smaller_subset_def)} moreover {fix s assume ass: "s ∈ ?LS" then have "s ∈ closure S" using smaller_subset_mono by auto then obtain ss where wit: "ss ≠ [] ∧ fold f ss e = s ∧ (set ss ⊆ S)" using closure_to_cons_listE by blast then have "∀ i < length ss. less_eq (ss ! i) x" using supremum_sound[of "set ss"] supremum_smaller_subset[of "set ss" x] unfolding cl.fold_set_fold[symmetric] by auto (metis ass local.trans mem_Collect_eq nth_mem smaller_subset_def) then have "s ∈ ?RS" using wit sound_fold[of ss] by (auto simp: smaller_subset_def) (metis (mono_tags, lifting) cl.closure.base inv_to_set mem_Collect_eq)} ultimately show ?thesis by blast qed lemma supremum_in_smaller_closure: assumes "finite S" shows "supremum (smaller_subset x S) ∈ {e} ∪ (closure S)" using supremum_in_closure[OF assms, of "smaller_subset x S"] by (metis UnI1 UnI2 cl.closure.base fold_empty singletonI smaller_subset_mono subset_iff) lemma supremum_subset_less_eq: assumes "finite S" and "R ⊆ S" shows "less_eq (supremum R) (supremum S)" using assms proof (induct arbitrary: R) case (insert x F) from insert(1, 2, 4) insert(3)[of "R - {x}"] have "less_eq (supremum (R - {x})) (f x (supremum F))" by (metis Diff_subset_conv insert_is_Un local.trans sup_r) then show ?case using insert(1, 2, 4) by auto (metis Diff_empty Diff_insert0 cl.fold_rec finite.insertI finite_subset sup_l upper_bound) qed (auto) lemma supremum_smaller_closure [simp]: assumes "finite S" shows "supremum (smaller_subset x (closure S)) = supremum (smaller_subset x S)" proof (cases "smaller_subset x S = {}") case [simp]: True show ?thesis by auto next case False have "smaller_subset x S ⊆ smaller_subset x (closure S)" unfolding pre_subset_eq_pos_subset by auto then have l: "less_eq (supremum (smaller_subset x S)) (supremum (smaller_subset x (closure S)))" using assms unfolding pre_subset_eq_pos_subset by (intro supremum_subset_less_eq) auto from False have "supremum (closure (smaller_subset x S)) ∈ closure S" using assms cl.closure_mono[OF smaller_subset_mono] using ‹smaller_subset x S ⊆ smaller_subset x (closure S)› by (auto simp add: assms intro!: supremum_in_closure) from closure_to_cons_listE[OF this] obtain ss where dec : "supremum (smaller_subset x (closure S)) = Finite_Set.fold f e (set ss)" and inv: "ss ≠ []" "set ss ⊆ S" by (auto simp: cl.fold_set_fold) force then have "set ss ⊆ smaller_subset x S" using supremum_sound[OF assms] using supremum_smaller_subset[OF assms] by (auto simp: smaller_subset_def) (metis List.finite_set assms cl.finite_S_finite_closure dec trans supremum_smaller_subset supremum_sound) then have "less_eq (supremum (smaller_subset x (closure S))) (supremum (smaller_subset x S))" using inv assms unfolding dec by (intro supremum_subset_less_eq) auto then show ?thesis using l anti_sym by auto qed end fun lift_f_total where "lift_f_total P f None _ = None" | "lift_f_total P f _ None = None" | "lift_f_total P f (Some s) (Some t) = (if P s t then Some (f s t) else None)" fun lift_less_eq_total where "lift_less_eq_total f _ None = True" | "lift_less_eq_total f None _ = False" | "lift_less_eq_total f (Some s) (Some t) = (f s t)" locale set_closure_partial_oprator = fixes P f assumes refl: "⋀ x. P x x" and sym: "⋀ x y. P x y ⟹ P y x" and dist: "⋀ x y z. P y z ⟹ P x (f y z) ⟹ P x y" and assP: "⋀ x y z. P x (f y z) ⟹ P y z ⟹ P (f x y) z" and com [ac_simps]: "⋀ x y. P x y ⟹ f x y = f y x" and ass [ac_simps]: "⋀ x y z. P x y ⟹ P y z ⟹ f x (f y z) = f (f x y) z" and idem: "⋀ x. f x x = x" begin lemma lift_f_total_com: "lift_f_total P f x y = lift_f_total P f y x" using com by (cases x; cases y) (auto simp: sym) lemma lift_f_total_ass: "lift_f_total P f x (lift_f_total P f y z) = lift_f_total P f (lift_f_total P f x y) z" proof (cases x) case [simp]: (Some s) show ?thesis proof (cases y) case [simp]: (Some t) show ?thesis proof (cases z) case [simp]: (Some u) show ?thesis by (auto simp add: ass dist[of t u s]) (metis com dist assP sym)+ qed auto qed auto qed auto lemma lift_f_total_idem: "lift_f_total P f x x = x" by (cases x) (auto simp: idem refl) lemma lift_f_totalE[elim]: assumes "lift_f_total P f s u = Some t" obtains v w where "s = Some v" "u = Some w" using assms by (cases s; cases u) auto lemma lift_set_closure_oprator: "set_closure_oprator (lift_f_total P f)" using lift_f_total_com lift_f_total_ass lift_f_total_idem by unfold_locales blast+ end sublocale set_closure_partial_oprator ⊆ lift_fun: set_closure_oprator "lift_f_total P f" by (simp add: lift_set_closure_oprator) context set_closure_partial_oprator begin abbreviation "lift_closure S ≡ lift_fun.closure (Some ` S)" inductive_set pred_closure for S where base [simp]: "s ∈ S ⟹ s ∈ pred_closure S" | step [intro]: "s ∈ pred_closure S ⟹ t ∈ pred_closure S ⟹ P s t ⟹ f s t ∈ pred_closure S" lemma pred_closure_to_some_lift_closure: assumes "s ∈ pred_closure S" shows "Some s ∈ lift_closure S" using assms proof (induct) case (step s t) then have "lift_f_total P f (Some s) (Some t) ∈ lift_closure S" by (intro lift_fun.closure.step) auto then show ?case using step(5) by (auto split: if_splits) qed auto lemma some_lift_closure_pred_closure: fixes t defines "s ≡ Some t" assumes "Some t ∈ lift_closure S" shows "t ∈ pred_closure S" using assms(2) unfolding assms(1)[symmetric] using assms(1) proof (induct arbitrary: t) case (step s u) from step(5) obtain v w where [simp]: "s = Some v" "u = Some w" by auto show ?case using step by (auto split: if_splits) qed auto lemma pred_closure_lift_closure: "pred_closure S = the ` (lift_closure S - {None})" (is "?LS = ?RS") proof {fix s assume "s ∈ ?LS" from pred_closure_to_some_lift_closure[OF this] have "s ∈ ?RS" by (metis DiffI empty_iff image_iff insertE option.distinct(1) option.sel)} then show "?LS ⊆ ?RS" by blast next {fix s assume ass: "s ∈ ?RS" then have "Some s ∈ lift_closure S" using option.collapse by fastforce from some_lift_closure_pred_closure[OF this] have "s ∈ ?LS" using option.collapse by auto} then show "?RS ⊆ ?LS" by blast qed lemma finite_S_finite_closure [simp, intro]: "finite S ⟹ finite (pred_closure S)" using finite_subset[of "Some ` pred_closure S" "lift_closure S"] using pred_closure_to_some_lift_closure lift_fun.finite_S_finite_closure[of "Some ` S"] by (auto simp add: pred_closure_lift_closure set_closure_partial_oprator_axioms) lemma closure_mono: assumes "S ⊆ T" shows "pred_closure S ⊆ pred_closure T" proof - have "Some ` S ⊆ Some ` T" using assms by auto from lift_fun.closure_mono[OF this] show ?thesis using pred_closure_to_some_lift_closure some_lift_closure_pred_closure set_closure_partial_oprator_axioms by fastforce qed lemma pred_closure_empty [simp]: "pred_closure {} = {}" using pred_closure_lift_closure by fastforce end locale semilattice_closure_partial_operator = cl: set_closure_partial_oprator P f for P and f :: "'a ⇒ 'a ⇒ 'a" + fixes less_eq e assumes neut_elm :"⋀ x. f e x = x" and neut_pred: "⋀ x. P e x" and neut_less: "⋀ x. less_eq e x" and pred_less: "⋀ x y z. less_eq x y ⟹ less_eq z y ⟹ P x z" and sup_l: "⋀ x y. P x y ⟹ less_eq x (f x y)" and sup_r: "⋀ x y. P x y ⟹ less_eq y (f x y)" and upper_bound: "⋀ x y z. less_eq x z ⟹ less_eq y z ⟹ less_eq (f x y) z" and trans: "⋀ x y z. less_eq x y ⟹ less_eq y z ⟹ less_eq x z" and anti_sym: "⋀ x y. less_eq x y ⟹ less_eq y x ⟹ x = y" begin abbreviation "lifted_less_eq ≡ lift_less_eq_total less_eq" abbreviation "lifted_fun ≡ lift_f_total P f" lemma lift_less_eq_None [simp]: "lifted_less_eq None y ⟷ y = None" by (cases y) auto lemma lift_less_eq_neut_elm [simp]: "lifted_fun (Some e) s = s" using neut_elm neut_pred by (cases s) auto lemma lift_less_eq_neut_less [simp]: "lifted_less_eq (Some e) s ⟷ True" using neut_less by (cases s) auto lemma lift_less_eq_sup_l [simp]: "lifted_less_eq x (lifted_fun x y) ⟷ True" using sup_l by (cases x; cases y) auto lemma lift_less_eq_sup_r [simp]: "lifted_less_eq y (lifted_fun x y) ⟷ True" using sup_r by (cases x; cases y) auto lemma lifted_less_eq_trans [trans]: "lifted_less_eq x y ⟹ lifted_less_eq y z ⟹ lifted_less_eq x z" using trans by (auto elim!: lift_less_eq_total.elims) lemma lifted_less_eq_anti_sym [trans]: "lifted_less_eq x y ⟹ lifted_less_eq y x ⟹ x = y" using anti_sym by (auto elim!: lift_less_eq_total.elims) lemma lifted_less_eq_upper: "lifted_less_eq x z ⟹ lifted_less_eq y z ⟹ lifted_less_eq (lifted_fun x y) z" using upper_bound pred_less by (auto elim!: lift_less_eq_total.elims) lemma semilattice_closure_operator_axioms: "semilattice_closure_operator_axioms (lift_f_total P f) (lift_less_eq_total less_eq) (Some e)" using lifted_less_eq_upper lifted_less_eq_trans lifted_less_eq_anti_sym by unfold_locales (auto elim!: lift_f_total.cases) end sublocale semilattice_closure_partial_operator ⊆ lift_ord: semilattice_closure_operator "lift_f_total P f" "lift_less_eq_total less_eq" "Some e" by (simp add: cl.lift_set_closure_oprator semilattice_closure_operator.intro semilattice_closure_operator_axioms) context semilattice_closure_partial_operator begin abbreviation "supremum ≡ lift_ord.supremum" abbreviation "smaller_subset ≡ lift_ord.smaller_subset" lemma supremum_impl: assumes "supremum (set (map Some ss)) = Some t" shows "foldr f ss e = t" using assms proof (induct ss arbitrary: t) case (Cons a ss) then show ?case by auto (metis cl.lift_f_totalE lift_f_total.simps(3) option.distinct(1) option.sel) qed auto lemma supremum_smaller_exists_unique: assumes "finite S" shows "∃! p. supremum (smaller_subset (Some t) (Some ` S)) = Some p" using assms proof (induct) case (insert x F) show ?case proof (cases "lifted_less_eq (Some x) (Some t)") case True obtain p where wit: "supremum (smaller_subset (Some t) (Some ` F)) = Some p" using insert by auto then have pred: "less_eq p t" "less_eq x t" using True insert(1) using lift_ord.supremum_smaller_subset by auto (metis finite_imageI lift_less_eq_total.simps(3)) show ?thesis using insert pred wit pred_less by auto next case False then show ?thesis using insert by auto qed qed auto lemma supremum_neut_or_in_closure: assumes "finite S" shows "the (supremum (smaller_subset (Some t) (Some ` S))) ∈ {e} ∪ cl.pred_closure S" using supremum_smaller_exists_unique[OF assms] using lift_ord.supremum_in_smaller_closure[of "Some ` S" "Some t"] assms by auto (metis cl.some_lift_closure_pred_closure option.sel) end (* At the moment we remove duplicates in each iteration, use data structure that can deal better with duplication i.e red black trees *) fun closure_impl where "closure_impl f [] = []" | "closure_impl f (x # S) = (let cS = closure_impl f S in remdups (x # cS @ map (f x) cS))" lemma (in set_closure_oprator) closure_impl [simp]: "set (closure_impl f S) = closure (set S)" by (induct S, auto simp: closure_insert Let_def) lemma (in set_closure_partial_oprator) closure_impl [simp]: "set (map the (removeAll None (closure_impl (lift_f_total P f) (map Some S)))) = pred_closure (set S)" using lift_set_closure_oprator set_closure_oprator.closure_impl pred_closure_lift_closure by auto end