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

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