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.31  lemma subspace_add_closed [simp, intro!!]: 
    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.66    by (simp add: negate_eq1);
    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.143          by (simp! add: vs_add_mult_distrib2);
   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;