theory Saturation
imports Main
begin
locale closure_under_fun =
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"
begin
forS">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 comp_fun_commute_f [simp]:
"comp_fun_commute f"
using ass com unfolding comp_fun_commute_def by (auto simp: comp_def) fastforce
lemma comp_fun_idem_f [simp]:
"comp_fun_idem f"
using idem ass unfolding comp_fun_idem_def comp_fun_idem_axioms_def
by (auto simp: comp_def)
lemma foldr_to_fold:
"foldr f xs = fold f xs"
using com ass foldr_fold[of _ f] by (auto simp: comp_def) metis
lemma fold_commute_f:
"f x (foldr f xs y) = foldr f xs (f x y)"
using com ass unfolding foldr_to_fold
by (auto simp: comp_def intro!: fold_commute_apply) fastforce
lemma foldr_to_Finite_Set_fold:
"foldr f xs t = Finite_Set.fold f t (set xs)"
proof (induct xs)
case (Cons x xs) then show ?case
by (cases "x ∈ set xs") (auto simp: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_f])
qed auto
lemma foldr_dist:
assumes "xs ≠ []"
shows " f (foldr f (tl xs) (hd xs)) t = foldr f xs t" using assms
proof (induct xs)
case (Cons a xs)
show ?case using Cons com ass fold_commute_f[symmetric]
by (auto simp: comp_def) metis
qed auto
lemma closure_to_cons_list:
assumes "s ∈ closure S"
shows "∃ ss ≠ []. foldr 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: "foldr f (tl ss) (hd ss) = s" and inv_s: "ss ≠ []" "∀ i < length ss. ss ! i ∈ S" and
t: "foldr f (tl ts) (hd ts) = t" and inv_t: "ts ≠ []" "∀ i < length ts. ts ! i ∈ S"
by auto
then show ?case by (auto simp: foldr_dist nth_append intro!: exI[of _ "ss @ ts"])
(smt ass com comp_apply foldr_Cons foldr_append foldr_dist list.exhaust_sel self_append_conv2)
qed
lemma cons_list_to_closure:
assumes "∀ i < length ss. ss ! i ∈ S" and "ss ≠ []"
shows "foldr f (tl ss) (hd ss) ∈ closure S" using assms
proof (induct ss)
case (Cons s ss) note IS = this show ?case
proof (cases ss)
case Nil
then show ?thesis using IS(2) by auto
next
case (Cons t ts)
then have t: "foldr f (tl (s # ss)) (hd (s # ss)) = f s (foldr f ts t)"
using com fold_commute_f by auto
show ?thesis using IS unfolding t unfolding Cons
by (auto intro!: step) fastforce
qed
qed auto
lemma closure_empty [simp]:
"closure {} = {}"
using closure_to_cons_list by auto
lemma closure_mono:
assumes "S ⊆ T"
shows "closure S ⊆ closure T"
proof
fix s assume ass: "s ∈ closure S"
then show "s ∈ closure T" using closure_to_cons_list[OF ass] cons_list_to_closure
by (meson assms subset_eq)
qed
lemma inv_to_set [simp]:
"(∀ i < length ss. ss ! i ∈ S) ⟷ set ss ⊆ S"
by (induct ss) (auto simp: nth_Cons split: nat.splits)
lemma closure_insert [simp]:
"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: "foldr 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) cons_list_to_closure[of ss] by (metis in_set_conv_nth insertE)
have "∃ s. t = f x s ∧ s ∈ closure S"
proof (cases "set ss = {x}")
case True then show ?thesis using ass(2) t
by (cases ss) (auto simp: comp_fun_idem.fold_insert_idem2 idem foldr_to_Finite_Set_fold dest!: subset_singletonD)
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
by (auto simp: foldr_to_Finite_Set_fold) (metis List.finite_set com comp_fun_idem.fold_insert_idem
comp_fun_idem.fold_insert_idem2 comp_fun_idem_f idem inv_t(1) list.exhaust_sel list.simps(15))
ultimately show ?thesis using cons_list_to_closure[OF _ split(3)]
by (auto simp: foldr_to_Finite_Set_fold)
qed}
then show ?thesis
by (auto simp: foldr_to_Finite_Set_fold in_mono[OF closure_mono[OF subset_insertI[of S x]]] intro!: step)
qed
lemma finite_S_finite_closure:
"finite S ⟹ finite (closure S)"
by (induct rule: finite.induct) auto
end
locale closure_under_pred_fun =
fixes f P
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
forS">inductive_set closure for S where
base [simp]: "s ∈ S ⟹ s ∈ closure S"
| step [intro]: "s ∈ closure S ⟹ t ∈ closure S ⟹ P s t ⟹ f s t ∈ closure S"
fun total_f where
"total_f None _ = None"
| "total_f _ None = None"
| "total_f (Some s) (Some t) = (if P s t then Some (f s t) else None)"
lemma total_f_com:
"total_f x y = total_f y x"
using com by (cases x; cases y) (auto simp: sym)
lemma total_f_ass:
"total_f x (total_f y z) = total_f (total_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 total_f_idem:
"total_f x x = x"
by (cases x) (auto simp: idem refl)
lemma total_fE[elim]:
assumes "total_f s u = Some t"
obtains v w where "s = Some v" "u = Some w"
using assms by (cases s; cases u) auto
interpretation l: closure_under_fun "total_f"
using total_f_com total_f_ass total_f_idem by unfold_locales blast+
abbreviation "tclosure S ≡ l.closure (Some ` S)"
lemma pclosure_subset_tclosure:
assumes "s ∈ closure S"
shows "Some s ∈ tclosure S" using assms
proof (induct)
case (step s t)
then have "total_f (Some s) (Some t) ∈ tclosure S"
by (intro l.closure.step) auto
then show ?case using step(5)
by (auto split: if_splits)
qed auto
lemma def_impl_tclosure_subset_pclosure:
fixes t defines "s ≡ Some t"
assumes "s ∈ tclosure S"
shows "the s ∈ closure S" using assms(2, 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 finite_S_finite_closure:
"finite S ⟹ finite (closure S)"
using finite_subset[of "Some ` closure S" "tclosure S"]
using pclosure_subset_tclosure l.finite_S_finite_closure[of "Some ` S"]
by auto (metis (mono_tags, lifting) Option.these_def Some_image_these_eq finite_imageI image_subset_iff these_image_Some_eq)
lemma closure_mono:
assumes "S ⊆ T"
shows "closure S ⊆ closure T"
proof -
have "Some ` S ⊆ Some ` T" using assms by auto
from l.closure_mono[OF this] show ?thesis
using pclosure_subset_tclosure def_impl_tclosure_subset_pclosure closure_under_pred_fun_axioms
by fastforce
qed
lemma closure_empty_set [simp]:
"closure {} = {}"
using pclosure_subset_tclosure by fastforce
end
end