Theory Saturation

theory Saturation
  imports Main

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

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}
  {fix s assume "s  ?RS" then have "s  ?LS" by induct auto}
  ultimately show ?thesis by blast

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]"])
  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)

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"
  fix s assume ass: "s  closure S"
  then show "S  T  s  closure T"
    by (induct) (auto simp: closure_to_cons_list)

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))
      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
  then show ?thesis
    by (auto simp: fold_set_fold in_mono[OF closure_mono[OF subset_insertI[of S x]]])

lemma finite_S_finite_closure [intro]:
  "finite S  finite (closure S)"
  by (induct rule: finite.induct) (auto simp: closure_insert)


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"

lemma unique_neut_elem [simp]:
  "f x y = e  x = e  y = e"
  using neut_fun cl.fun_left_idem
  by (metis

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

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)}
  {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

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


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"

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+


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")
  {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
  {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

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

lemma pred_closure_empty [simp]:
  "pred_closure {} = {}"
  using pred_closure_lift_closure by fastforce

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"

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)


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

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
    case False then show ?thesis
      using insert by auto 
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)


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