Theory Hull

(*  Title:      HOL/Hull.thy
    Author:     Amine Chaieb, University of Cambridge
    Author:     Jose Divasón <jose.divasonm at unirioja.es>
    Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
    Author:     Johannes Hölzl, VU Amsterdam
*)

theory Hull
  imports Main
begin

subsection A generic notion of the convex, affine, conic hull, or closed "hull".

definition hull :: "('a set  bool)  'a set  'a set"  (infixl "hull" 75)
  where "S hull s = {t. S t  s  t}"

lemma hull_same: "S s  S hull s = s"
  unfolding hull_def by auto

lemma hull_in: "(T. Ball T S  S (T))  S (S hull s)"
  unfolding hull_def Ball_def by auto

lemma hull_eq: "(T. Ball T S  S (T))  (S hull s) = s  S s"
  using hull_same[of S s] hull_in[of S s] by metis

lemma hull_hull [simp]: "S hull (S hull s) = S hull s"
  unfolding hull_def by blast

lemma hull_subset[intro]: "s  (S hull s)"
  unfolding hull_def by blast

lemma hull_mono: "s  t  (S hull s)  (S hull t)"
  unfolding hull_def by blast

lemma hull_antimono: "x. S x  T x  (T hull s)  (S hull s)"
  unfolding hull_def by blast

lemma hull_minimal: "s  t  S t  (S hull s)  t"
  unfolding hull_def by blast

lemma subset_hull: "S t  S hull s  t  s  t"
  unfolding hull_def by blast

lemma hull_UNIV [simp]: "S hull UNIV = UNIV"
  unfolding hull_def by auto

lemma hull_unique: "s  t  S t  (t'. s  t'  S t'  t  t')  (S hull s = t)"
  unfolding hull_def by auto

lemma hull_induct: "a  Q hull S; x. x S  P x; Q {x. P x}  P a"
  using hull_minimal[of S "{x. P x}" Q]
  by (auto simp add: subset_eq)

lemma hull_inc: "x  S  x  P hull S"
  by (metis hull_subset subset_eq)

lemma hull_Un_subset: "(S hull s)  (S hull t)  (S hull (s  t))"
  unfolding Un_subset_iff by (metis hull_mono Un_upper1 Un_upper2)

lemma hull_Un:
  assumes T: "T. Ball T S  S (T)"
  shows "S hull (s  t) = S hull (S hull s  S hull t)"
  apply (rule equalityI)
  apply (meson hull_mono hull_subset sup.mono)
  by (metis hull_Un_subset hull_hull hull_mono)

lemma hull_Un_left: "P hull (S  T) = P hull (P hull S  T)"
  apply (rule equalityI)
   apply (simp add: Un_commute hull_mono hull_subset sup.coboundedI2)
  by (metis Un_subset_iff hull_hull hull_mono hull_subset)

lemma hull_Un_right: "P hull (S  T) = P hull (S  P hull T)"
  by (metis hull_Un_left sup.commute)

lemma hull_insert:
   "P hull (insert a S) = P hull (insert a (P hull S))"
  by (metis hull_Un_right insert_is_Un)

lemma hull_redundant_eq: "a  (S hull s)  S hull (insert a s) = S hull s"
  unfolding hull_def by blast

lemma hull_redundant: "a  (S hull s)  S hull (insert a s) = S hull s"
  by (metis hull_redundant_eq)

end