Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Hull.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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 \<open>A generic notion of the convex, affine, conic hull, or closed "hull".\<close>

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

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.