Theory Saturation

theory Saturation
  imports Main
begin

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

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 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: comp_fun_idem.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)

"closure S ≡ cl.closure S"">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)

"supremum S ≡ Finite_Set.fold f e S"">abbreviation "supremum S ≡ Finite_Set.fold f e S"
"smaller_subset x S ≡ {y. less_eq y x ∧ y ∈ 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)"


(* TODO rework *)
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

"lift_closure S ≡ lift_fun.closure (Some ` S)"">abbreviation "lift_closure S ≡ lift_fun.closure (Some ` S)"

forS">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

(* TODO RENAME *)
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

"lifted_less_eq ≡ lift_less_eq_total less_eq"">abbreviation "lifted_less_eq ≡ lift_less_eq_total less_eq"
"lifted_fun ≡ lift_f_total P f"">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

"supremum ≡ lift_ord.supremum"">abbreviation "supremum ≡ lift_ord.supremum"
"smaller_subset ≡ lift_ord.smaller_subset"">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