src/HOL/Real/HahnBanach/FunctionOrder.thy
changeset 10687 c186279eecea
parent 9969 4753185f1dd2
child 11472 d08d4e17a5f6
     1.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sat Dec 16 21:41:14 2000 +0100
     1.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Sat Dec 16 21:41:51 2000 +0100
     1.3 @@ -9,75 +9,82 @@
     1.4  
     1.5  subsection {* The graph of a function *}
     1.6  
     1.7 -text{* We define the \emph{graph} of a (real) function $f$ with
     1.8 -domain $F$ as the set 
     1.9 -\[
    1.10 -\{(x, f\ap x). \ap x \in F\}
    1.11 -\]
    1.12 -So we are modeling partial functions by specifying the domain and 
    1.13 -the mapping function. We use the term ``function'' also for its graph.
    1.14 +text {*
    1.15 +  We define the \emph{graph} of a (real) function @{text f} with
    1.16 +  domain @{text F} as the set
    1.17 +  \begin{center}
    1.18 +  @{text "{(x, f x). x \<in> F}"}
    1.19 +  \end{center}
    1.20 +  So we are modeling partial functions by specifying the domain and
    1.21 +  the mapping function. We use the term ``function'' also for its
    1.22 +  graph.
    1.23  *}
    1.24  
    1.25  types 'a graph = "('a * real) set"
    1.26  
    1.27  constdefs
    1.28 -  graph :: "['a set, 'a => real] => 'a graph "
    1.29 -  "graph F f == {(x, f x) | x. x \<in> F}" 
    1.30 +  graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph "
    1.31 +  "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
    1.32  
    1.33 -lemma graphI [intro?]: "x \<in> F ==> (x, f x) \<in> graph F f"
    1.34 -  by (unfold graph_def, intro CollectI exI) force
    1.35 +lemma graphI [intro?]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
    1.36 +  by (unfold graph_def, intro CollectI exI) blast
    1.37  
    1.38 -lemma graphI2 [intro?]: "x \<in> F ==> \<exists>t\<in> (graph F f). t = (x, f x)"
    1.39 -  by (unfold graph_def, force)
    1.40 +lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t\<in> (graph F f). t = (x, f x)"
    1.41 +  by (unfold graph_def) blast
    1.42  
    1.43 -lemma graphD1 [intro?]: "(x, y) \<in> graph F f ==> x \<in> F"
    1.44 -  by (unfold graph_def, elim CollectE exE) force
    1.45 +lemma graphD1 [intro?]: "(x, y) \<in> graph F f \<Longrightarrow> x \<in> F"
    1.46 +  by (unfold graph_def) blast
    1.47  
    1.48 -lemma graphD2 [intro?]: "(x, y) \<in> graph H h ==> y = h x"
    1.49 -  by (unfold graph_def, elim CollectE exE) force 
    1.50 +lemma graphD2 [intro?]: "(x, y) \<in> graph H h \<Longrightarrow> y = h x"
    1.51 +  by (unfold graph_def) blast
    1.52 +
    1.53  
    1.54  subsection {* Functions ordered by domain extension *}
    1.55  
    1.56 -text{* A function $h'$ is an extension of $h$, iff the graph of 
    1.57 -$h$ is a subset of the graph of $h'$.*}
    1.58 +text {* A function @{text h'} is an extension of @{text h}, iff the
    1.59 +  graph of @{text h} is a subset of the graph of @{text h'}. *}
    1.60  
    1.61 -lemma graph_extI: 
    1.62 -  "[| !! x. x \<in> H ==> h x = h' x; H <= H'|]
    1.63 -  ==> graph H h <= graph H' h'"
    1.64 -  by (unfold graph_def, force)
    1.65 +lemma graph_extI:
    1.66 +  "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
    1.67 +  \<Longrightarrow> graph H h \<subseteq> graph H' h'"
    1.68 +  by (unfold graph_def) blast
    1.69  
    1.70 -lemma graph_extD1 [intro?]: 
    1.71 -  "[| graph H h <= graph H' h'; x \<in> H |] ==> h x = h' x"
    1.72 -  by (unfold graph_def, force)
    1.73 +lemma graph_extD1 [intro?]:
    1.74 +  "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
    1.75 +  by (unfold graph_def) blast
    1.76  
    1.77 -lemma graph_extD2 [intro?]: 
    1.78 -  "[| graph H h <= graph H' h' |] ==> H <= H'"
    1.79 -  by (unfold graph_def, force)
    1.80 +lemma graph_extD2 [intro?]:
    1.81 +  "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
    1.82 +  by (unfold graph_def) blast
    1.83  
    1.84  subsection {* Domain and function of a graph *}
    1.85  
    1.86 -text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and 
    1.87 -$\idt{funct}$.*}
    1.88 +text {*
    1.89 +  The inverse functions to @{text graph} are @{text domain} and
    1.90 +  @{text funct}.
    1.91 +*}
    1.92  
    1.93  constdefs
    1.94 -  domain :: "'a graph => 'a set" 
    1.95 -  "domain g == {x. \<exists>y. (x, y) \<in> g}"
    1.96 +  domain :: "'a graph \<Rightarrow> 'a set"
    1.97 +  "domain g \<equiv> {x. \<exists>y. (x, y) \<in> g}"
    1.98  
    1.99 -  funct :: "'a graph => ('a => real)"
   1.100 -  "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)"
   1.101 +  funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
   1.102 +  "funct g \<equiv> \<lambda>x. (SOME y. (x, y) \<in> g)"
   1.103  
   1.104  
   1.105 -text {* The following lemma states that $g$ is the graph of a function
   1.106 -if the relation induced by $g$ is unique. *}
   1.107 +text {*
   1.108 +  The following lemma states that @{text g} is the graph of a function
   1.109 +  if the relation induced by @{text g} is unique.
   1.110 +*}
   1.111  
   1.112 -lemma graph_domain_funct: 
   1.113 -  "(!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y) 
   1.114 -  ==> graph (domain g) (funct g) = g"
   1.115 +lemma graph_domain_funct:
   1.116 +  "(\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y)
   1.117 +  \<Longrightarrow> graph (domain g) (funct g) = g"
   1.118  proof (unfold domain_def funct_def graph_def, auto)
   1.119    fix a b assume "(a, b) \<in> g"
   1.120    show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
   1.121    show "\<exists>y. (a, y) \<in> g" ..
   1.122 -  assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y"
   1.123 +  assume uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
   1.124    show "b = (SOME y. (a, y) \<in> g)"
   1.125    proof (rule some_equality [symmetric])
   1.126      fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
   1.127 @@ -88,47 +95,49 @@
   1.128  
   1.129  subsection {* Norm-preserving extensions of a function *}
   1.130  
   1.131 -text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on 
   1.132 -$E$. The set of all linear extensions of $f$, to superspaces $H$ of 
   1.133 -$F$, which are bounded by $p$, is defined as follows. *}
   1.134 -
   1.135 +text {*
   1.136 +  Given a linear form @{text f} on the space @{text F} and a seminorm
   1.137 +  @{text p} on @{text E}. The set of all linear extensions of @{text
   1.138 +  f}, to superspaces @{text H} of @{text F}, which are bounded by
   1.139 +  @{text p}, is defined as follows.
   1.140 +*}
   1.141  
   1.142  constdefs
   1.143 -  norm_pres_extensions :: 
   1.144 -    "['a::{plus, minus, zero} set, 'a  => real, 'a set, 'a => real] 
   1.145 -    => 'a graph set"
   1.146 -    "norm_pres_extensions E p F f 
   1.147 -    == {g. \<exists>H h. graph H h = g 
   1.148 -                \<and> is_linearform H h 
   1.149 +  norm_pres_extensions ::
   1.150 +    "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
   1.151 +    \<Rightarrow> 'a graph set"
   1.152 +    "norm_pres_extensions E p F f
   1.153 +    \<equiv> {g. \<exists>H h. graph H h = g
   1.154 +                \<and> is_linearform H h
   1.155                  \<and> is_subspace H E
   1.156                  \<and> is_subspace F H
   1.157 -                \<and> graph F f <= graph H h
   1.158 -                \<and> (\<forall>x \<in> H. h x <= p x)}"
   1.159 -                       
   1.160 -lemma norm_pres_extension_D:  
   1.161 +                \<and> graph F f \<subseteq> graph H h
   1.162 +                \<and> (\<forall>x \<in> H. h x \<le> p x)}"
   1.163 +
   1.164 +lemma norm_pres_extension_D:
   1.165    "g \<in> norm_pres_extensions E p F f
   1.166 -  ==> \<exists>H h. graph H h = g 
   1.167 -            \<and> is_linearform H h 
   1.168 +  \<Longrightarrow> \<exists>H h. graph H h = g
   1.169 +            \<and> is_linearform H h
   1.170              \<and> is_subspace H E
   1.171              \<and> is_subspace F H
   1.172 -            \<and> graph F f <= graph H h
   1.173 -            \<and> (\<forall>x \<in> H. h x <= p x)"
   1.174 -  by (unfold norm_pres_extensions_def) force
   1.175 +            \<and> graph F f \<subseteq> graph H h
   1.176 +            \<and> (\<forall>x \<in> H. h x \<le> p x)"
   1.177 +  by (unfold norm_pres_extensions_def) blast
   1.178  
   1.179 -lemma norm_pres_extensionI2 [intro]:  
   1.180 -  "[| is_linearform H h; is_subspace H E; is_subspace F H;
   1.181 -  graph F f <= graph H h; \<forall>x \<in> H. h x <= p x |]
   1.182 -  ==> (graph H h \<in> norm_pres_extensions E p F f)"
   1.183 - by (unfold norm_pres_extensions_def) force
   1.184 +lemma norm_pres_extensionI2 [intro]:
   1.185 +  "is_linearform H h \<Longrightarrow> is_subspace H E \<Longrightarrow> is_subspace F H \<Longrightarrow>
   1.186 +  graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
   1.187 +  \<Longrightarrow> (graph H h \<in> norm_pres_extensions E p F f)"
   1.188 + by (unfold norm_pres_extensions_def) blast
   1.189  
   1.190 -lemma norm_pres_extensionI [intro]:  
   1.191 -  "\<exists>H h. graph H h = g 
   1.192 -         \<and> is_linearform H h    
   1.193 +lemma norm_pres_extensionI [intro]:
   1.194 +  "\<exists>H h. graph H h = g
   1.195 +         \<and> is_linearform H h
   1.196           \<and> is_subspace H E
   1.197           \<and> is_subspace F H
   1.198 -         \<and> graph F f <= graph H h
   1.199 -         \<and> (\<forall>x \<in> H. h x <= p x)
   1.200 -  ==> g \<in> norm_pres_extensions E p F f"
   1.201 -  by (unfold norm_pres_extensions_def) force
   1.202 +         \<and> graph F f \<subseteq> graph H h
   1.203 +         \<and> (\<forall>x \<in> H. h x \<le> p x)
   1.204 +  \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
   1.205 +  by (unfold norm_pres_extensions_def) blast
   1.206  
   1.207 -end
   1.208 \ No newline at end of file
   1.209 +end