--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy Mon Dec 29 13:23:53 2008 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,142 +0,0 @@
-(* Title: HOL/Real/HahnBanach/FunctionOrder.thy
- ID: $Id$
- Author: Gertrud Bauer, TU Munich
-*)
-
-header {* An order on functions *}
-
-theory FunctionOrder
-imports Subspace Linearform
-begin
-
-subsection {* The graph of a function *}
-
-text {*
- We define the \emph{graph} of a (real) function @{text f} with
- domain @{text F} as the set
- \begin{center}
- @{text "{(x, f x). x \<in> F}"}
- \end{center}
- So we are modeling partial functions by specifying the domain and
- the mapping function. We use the term ``function'' also for its
- graph.
-*}
-
-types 'a graph = "('a \<times> real) set"
-
-definition
- graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where
- "graph F f = {(x, f x) | x. x \<in> F}"
-
-lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
- unfolding graph_def by blast
-
-lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"
- unfolding graph_def by blast
-
-lemma graphE [elim?]:
- "(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C"
- unfolding graph_def by blast
-
-
-subsection {* Functions ordered by domain extension *}
-
-text {*
- A function @{text h'} is an extension of @{text h}, iff the graph of
- @{text h} is a subset of the graph of @{text h'}.
-*}
-
-lemma graph_extI:
- "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
- \<Longrightarrow> graph H h \<subseteq> graph H' h'"
- unfolding graph_def by blast
-
-lemma graph_extD1 [dest?]:
- "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
- unfolding graph_def by blast
-
-lemma graph_extD2 [dest?]:
- "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
- unfolding graph_def by blast
-
-
-subsection {* Domain and function of a graph *}
-
-text {*
- The inverse functions to @{text graph} are @{text domain} and @{text
- funct}.
-*}
-
-definition
- "domain" :: "'a graph \<Rightarrow> 'a set" where
- "domain g = {x. \<exists>y. (x, y) \<in> g}"
-
-definition
- funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" where
- "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
-
-text {*
- The following lemma states that @{text g} is the graph of a function
- if the relation induced by @{text g} is unique.
-*}
-
-lemma graph_domain_funct:
- assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
- shows "graph (domain g) (funct g) = g"
- unfolding domain_def funct_def graph_def
-proof auto (* FIXME !? *)
- fix a b assume g: "(a, b) \<in> g"
- from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
- from g show "\<exists>y. (a, y) \<in> g" ..
- from g show "b = (SOME y. (a, y) \<in> g)"
- proof (rule some_equality [symmetric])
- fix y assume "(a, y) \<in> g"
- with g show "y = b" by (rule uniq)
- qed
-qed
-
-
-subsection {* Norm-preserving extensions of a function *}
-
-text {*
- Given a linear form @{text f} on the space @{text F} and a seminorm
- @{text p} on @{text E}. The set of all linear extensions of @{text
- f}, to superspaces @{text H} of @{text F}, which are bounded by
- @{text p}, is defined as follows.
-*}
-
-definition
- norm_pres_extensions ::
- "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
- \<Rightarrow> 'a graph set" where
- "norm_pres_extensions E p F f
- = {g. \<exists>H h. g = graph H h
- \<and> linearform H h
- \<and> H \<unlhd> E
- \<and> F \<unlhd> H
- \<and> graph F f \<subseteq> graph H h
- \<and> (\<forall>x \<in> H. h x \<le> p x)}"
-
-lemma norm_pres_extensionE [elim]:
- "g \<in> norm_pres_extensions E p F f
- \<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h
- \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h
- \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C"
- unfolding norm_pres_extensions_def by blast
-
-lemma norm_pres_extensionI2 [intro]:
- "linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H
- \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
- \<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f"
- unfolding norm_pres_extensions_def by blast
-
-lemma norm_pres_extensionI: (* FIXME ? *)
- "\<exists>H h. g = graph H h
- \<and> linearform H h
- \<and> H \<unlhd> E
- \<and> F \<unlhd> H
- \<and> graph F f \<subseteq> graph H h
- \<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
- unfolding norm_pres_extensions_def by blast
-
-end