|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
univGen.ml
Sprache: 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.19Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
|
|
|
|
|
