src/HOL/Real/HahnBanach/Subspace.thy
 changeset 7978 1b99ee57d131 parent 7927 b50446a33c16 child 8169 77b3bc101de5
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 29 19:24:20 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 29 20:18:34 1999 +0200
1.3 @@ -17,15 +17,15 @@
1.4
1.5  constdefs
1.6    is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
1.7 -  "is_subspace U V ==  U ~= {}  & U <= V
1.8 -     &  (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
1.9 +  "is_subspace U V == U ~= {} & U <= V
1.10 +     & (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
1.11
1.12  lemma subspaceI [intro]:
1.13 -  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x + y : U);
1.14 +  "[| <0> : U; U <= V; ALL x:U. ALL y:U. (x + y : U);
1.15    ALL x:U. ALL a. a <*> x : U |]
1.16    ==> is_subspace U V";
1.17  proof (unfold is_subspace_def, intro conjI);
1.18 -  assume "<0>:U"; thus "U ~= {}"; by fast;
1.19 +  assume "<0> : U"; thus "U ~= {}"; by fast;
1.20  qed (simp+);
1.21
1.22  lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
1.23 @@ -35,28 +35,28 @@
1.24    by (unfold is_subspace_def) simp;
1.25
1.26  lemma subspace_subsetD [simp, intro!!]:
1.27 -  "[| is_subspace U V; x:U |]==> x:V";
1.28 +  "[| is_subspace U V; x:U |] ==> x:V";
1.29    by (unfold is_subspace_def) force;
1.30
1.32 -  "[| is_subspace U V; x: U; y: U |] ==> x + y : U";
1.33 +  "[| is_subspace U V; x:U; y:U |] ==> x + y : U";
1.34    by (unfold is_subspace_def) simp;
1.35
1.36  lemma subspace_mult_closed [simp, intro!!]:
1.37 -  "[| is_subspace U V; x: U |] ==> a <*> x: U";
1.38 +  "[| is_subspace U V; x:U |] ==> a <*> x : U";
1.39    by (unfold is_subspace_def) simp;
1.40
1.41  lemma subspace_diff_closed [simp, intro!!]:
1.42 -  "[| is_subspace U V; is_vectorspace V; x: U; y: U |]
1.43 -  ==> x - y: U";
1.44 +  "[| is_subspace U V; is_vectorspace V; x:U; y:U |]
1.45 +  ==> x - y : U";
1.46    by (simp! add: diff_eq1 negate_eq1);
1.47
1.48  text {* Similar as for linear spaces, the existence of the
1.49 -zero element in every subspace follws from the non-emptyness
1.50 -of the subspace and vector space laws.*};
1.51 +zero element in every subspace follows from the non-emptiness
1.52 +of the carrier set and by vector space laws.*};
1.53
1.54  lemma zero_in_subspace [intro !!]:
1.55 -  "[| is_subspace U V; is_vectorspace V |] ==> <0>:U";
1.56 +  "[| is_subspace U V; is_vectorspace V |] ==> <0> : U";
1.57  proof -;
1.58    assume "is_subspace U V" and v: "is_vectorspace V";
1.59    have "U ~= {}"; ..;
1.60 @@ -72,11 +72,11 @@
1.61  qed;
1.62
1.63  lemma subspace_neg_closed [simp, intro!!]:
1.64 -  "[| is_subspace U V; is_vectorspace V; x: U |] ==> - x: U";
1.65 +  "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U";
1.67
1.68  text_raw {* \medskip *};
1.69 -text {* Further derived laws: Every subspace is a vector space. *};
1.70 +text {* Further derived laws: every subspace is a vector space. *};
1.71
1.72  lemma subspace_vs [intro!!]:
1.73    "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
1.74 @@ -84,7 +84,7 @@
1.75    assume "is_subspace U V" "is_vectorspace V";
1.76    show ?thesis;
1.77    proof;
1.78 -    show "<0>:U"; ..;
1.79 +    show "<0> : U"; ..;
1.80      show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
1.81      show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
1.82      show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
1.83 @@ -134,26 +134,26 @@
1.84
1.85  subsection {* Linear closure *};
1.86
1.87 -text {* The \emph{linear closure} of a vector $x$ is the set of all
1.88 -multiples of $x$. *};
1.89 +text {* The \emph{linear closure} of a vector $x$ is the set of all
1.90 +scalar multiples of $x$. *};
1.91
1.92  constdefs
1.93    lin :: "'a => 'a set"
1.94 -  "lin x == {y. EX a. y = a <*> x}";
1.95 +  "lin x == {a <*> x | a. True}";
1.96
1.97  lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
1.98 -  by (unfold lin_def) force;
1.99 +  by (unfold lin_def) fast;
1.100
1.101  lemma linI [intro!!]: "a <*> x0 : lin x0";
1.102 -  by (unfold lin_def) force;
1.103 +  by (unfold lin_def) fast;
1.104
1.105  text {* Every vector is contained in its linear closure. *};
1.106
1.107 -lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
1.108 -proof (unfold lin_def, intro CollectI exI);
1.109 +lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
1.110 +proof (unfold lin_def, intro CollectI exI conjI);
1.111    assume "is_vectorspace V" "x:V";
1.112    show "x = 1r <*> x"; by (simp!);
1.113 -qed;
1.114 +qed simp;
1.115
1.116  text {* Any linear closure is a subspace. *};
1.117
1.118 @@ -162,12 +162,12 @@
1.119  proof;
1.120    assume "is_vectorspace V" "x:V";
1.121    show "<0> : lin x";
1.122 -  proof (unfold lin_def, intro CollectI exI);
1.123 +  proof (unfold lin_def, intro CollectI exI conjI);
1.124      show "<0> = 0r <*> x"; by (simp!);
1.125 -  qed;
1.126 +  qed simp;
1.127
1.128    show "lin x <= V";
1.129 -  proof (unfold lin_def, intro subsetI, elim CollectE exE);
1.130 +  proof (unfold lin_def, intro subsetI, elim CollectE exE conjE);
1.131      fix xa a; assume "xa = a <*> x";
1.132      show "xa:V"; by (simp!);
1.133    qed;
1.134 @@ -176,21 +176,23 @@
1.135    proof (intro ballI);
1.136      fix x1 x2; assume "x1 : lin x" "x2 : lin x";
1.137      thus "x1 + x2 : lin x";
1.138 -    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
1.139 +    proof (unfold lin_def, elim CollectE exE conjE,
1.140 +      intro CollectI exI conjI);
1.141        fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
1.142        show "x1 + x2 = (a1 + a2) <*> x";
1.144 -    qed;
1.145 +    qed simp;
1.146    qed;
1.147
1.148    show "ALL xa:lin x. ALL a. a <*> xa : lin x";
1.149    proof (intro ballI allI);
1.150      fix x1 a; assume "x1 : lin x";
1.151      thus "a <*> x1 : lin x";
1.152 -    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
1.153 +    proof (unfold lin_def, elim CollectE exE conjE,
1.154 +      intro CollectI exI conjI);
1.155        fix a1; assume "x1 = a1 <*> x";
1.156        show "a <*> x1 = (a * a1) <*> x"; by (simp!);
1.157 -    qed;
1.158 +    qed simp;
1.159    qed;
1.160  qed;
1.161
1.162 @@ -213,7 +215,7 @@
1.163  instance set :: (plus) plus; by intro_classes;
1.164
1.165  defs vs_sum_def:
1.166 -  "U + V == {x. EX u:U. EX v:V. x = u + v}";(***
1.167 +  "U + V == {u + v | u v. u:U & v:V}"; (***
1.168
1.169  constdefs
1.170    vs_sum ::
1.171 @@ -223,13 +225,13 @@
1.172
1.173  lemma vs_sumD:
1.174    "x: U + V = (EX u:U. EX v:V. x = u + v)";
1.175 -  by (unfold vs_sum_def) simp;
1.176 +    by (unfold vs_sum_def) fast;
1.177
1.178  lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
1.179
1.180  lemma vs_sumI [intro!!]:
1.181    "[| x:U; y:V; t= x + y |] ==> t : U + V";
1.182 -  by (unfold vs_sum_def, intro CollectI bexI);
1.183 +  by (unfold vs_sum_def) fast;
1.184
1.185  text{* $U$ is a subspace of $U + V$. *};
1.186
1.187 @@ -287,7 +289,7 @@
1.188      qed (simp!)+;
1.189    qed;
1.190
1.191 -  show "ALL x: U + V. ALL a. a <*> x : U + V";
1.192 +  show "ALL x : U + V. ALL a. a <*> x : U + V";
1.193    proof (intro ballI allI);
1.194      fix x a; assume "x : U + V";
1.195      thus "a <*> x : U + V";
1.196 @@ -348,10 +350,11 @@
1.197    qed;
1.198  qed;
1.199
1.200 -text {* An application of the previous lemma will be used in the
1.201 -proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$
1.202 -of the direct sum of a vectorspace $H$ and the linear closure of
1.203 -$x_0$ the components $y \in H$ and $a$ are unique. *};
1.204 +text {* An application of the previous lemma will be used in the proof
1.205 +of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any
1.206 +element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and
1.207 +the linear closure of $x_0$ the components $y \in H$ and $a$ are
1.208 +uniquely determined. *};
1.209
1.210  lemma decomp_H0:
1.211    "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
1.212 @@ -370,9 +373,9 @@
1.213      proof;
1.214        show "H Int lin x0 <= {<0>}";
1.215        proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
1.216 -        fix x; assume "x:H" "x:lin x0";
1.217 +        fix x; assume "x:H" "x : lin x0";
1.218          thus "x = <0>";
1.219 -        proof (unfold lin_def, elim CollectE exE);
1.220 +        proof (unfold lin_def, elim CollectE exE conjE);
1.221            fix a; assume "x = a <*> x0";
1.222            show ?thesis;
1.223            proof (rule case_split);
1.224 @@ -388,8 +391,9 @@
1.225         qed;
1.226        qed;
1.227        show "{<0>} <= H Int lin x0";
1.228 -      proof (intro subsetI, elim singletonE, intro IntI, simp+);
1.229 -        show "<0> : H"; ..;
1.230 +      proof (intro subsetI, elim singletonE, intro IntI,
1.231 +        (simp only:)+);
1.232 +        show "<0>:H"; ..;
1.233          from lin_vs; show "<0> : lin x0"; ..;
1.234        qed;
1.235      qed;
1.236 @@ -404,20 +408,20 @@
1.237    qed;
1.238  qed;
1.239
1.240 -text {* Since for an element $y + a \mult x_0$ of the direct sum
1.241 +text {* Since for any element $y + a \mult x_0$ of the direct sum
1.242  of a vectorspace $H$ and the linear closure of $x_0$ the components
1.243 -$y\in H$ and $a$ are unique, follows from $y\in H$ the fact that
1.244 +$y\in H$ and $a$ are unique, it follows from $y\in H$ that
1.245  $a = 0$.*};
1.246
1.247  lemma decomp_H0_H:
1.248 -  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E;
1.249 +  "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
1.250    x0 ~= <0> |]
1.251    ==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
1.252  proof (rule, unfold split_paired_all);
1.253 -  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E"
1.254 +  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
1.255      "x0 ~= <0>";
1.256    have h: "is_vectorspace H"; ..;
1.257 -  fix y a; presume t1: "t = y + a <*> x0" and "y : H";
1.258 +  fix y a; presume t1: "t = y + a <*> x0" and "y:H";
1.259    have "y = t & a = 0r";
1.260      by (rule decomp_H0) (assumption | (simp!))+;
1.261    thus "(y, a) = (t, 0r)"; by (simp!);
1.262 @@ -428,14 +432,14 @@
1.263  $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
1.264
1.265  lemma h0_definite:
1.266 -  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
1.267 +  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
1.268                  in (h y) + a * xi);
1.269    x = y + a <*> x0; is_vectorspace E; is_subspace H E;
1.270    y:H; x0 ~: H; x0:E; x0 ~= <0> |]
1.271    ==> h0 x = h y + a * xi";
1.272  proof -;
1.273    assume
1.274 -    "h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
1.275 +    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
1.276                 in (h y) + a * xi)"
1.277      "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
1.278      "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
1.279 @@ -443,25 +447,25 @@
1.280      by (simp! add: vs_sum_def lin_def) force+;
1.281    have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
1.282    proof;
1.283 -    show "EX xa. ((%(y, a). x = y + a <*> x0 & y:H) xa)";
1.284 +    show "EX xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
1.285        by (force!);
1.286    next;
1.287      fix xa ya;
1.288 -    assume "(%(y,a). x = y + a <*> x0 & y : H) xa"
1.289 -           "(%(y,a). x = y + a <*> x0 & y : H) ya";
1.290 +    assume "(\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
1.291 +           "(\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
1.292      show "xa = ya"; ;
1.293      proof -;
1.294        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya";
1.295          by (rule Pair_fst_snd_eq [RS iffD2]);
1.296 -      have x: "x = (fst xa) + (snd xa) <*> x0 & (fst xa) : H";
1.297 +      have x: "x = fst xa + snd xa <*> x0 & fst xa : H";
1.298          by (force!);
1.299 -      have y: "x = (fst ya) + (snd ya) <*> x0 & (fst ya) : H";
1.300 +      have y: "x = fst ya + snd ya <*> x0 & fst ya : H";
1.301          by (force!);
1.302        from x y; show "fst xa = fst ya & snd xa = snd ya";
1.303          by (elim conjE) (rule decomp_H0, (simp!)+);
1.304      qed;
1.305    qed;
1.306 -  hence eq: "(SOME (y, a). (x = y + a <*> x0 & y:H)) = (y, a)";
1.307 +  hence eq: "(SOME (y, a). x = y + a <*> x0 & y:H) = (y, a)";
1.308      by (rule select1_equality) (force!);
1.309    thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
1.310  qed;