
diff -r 6a102f74ad0a -r fd019ac3485f src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 08 16:18:51 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 08 16:40:27 1999 +0200
@@ -3,10 +3,13 @@
     Author:     Gertrud Bauer, TU Munich
 *)
 
+
+header {* Subspaces *};
+
 theory Subspace = LinearSpace:;
 
 
-section {* subspaces *};
+subsection {* Subspaces *};
 
 constdefs
   is_subspace ::  "['a set, 'a set] => bool"
@@ -15,8 +18,9 @@
                        & a [*] x : U)";                            
 
 lemma subspaceI [intro]: 
-  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |]
-  \ ==> is_subspace U V";
+  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); 
+  ALL x:U. ALL a. a [*] x : U |]
+  ==> is_subspace U V";
   by (unfold is_subspace_def) simp;
 
 lemma "is_subspace U V ==> U ~= {}";
@@ -28,23 +32,27 @@
 lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
   by (unfold is_subspace_def) simp;
 
-lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V";
+lemma subspace_subsetD [simp, intro!!]: 
+  "[| is_subspace U V; x:U |]==> x:V";
   by (unfold is_subspace_def) force;
 
-lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
-  by (unfold is_subspace_def) simp;
-
-lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
+lemma subspace_add_closed [simp, intro!!]: 
+  "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
   by (unfold is_subspace_def) simp;
 
-lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
+lemma subspace_mult_closed [simp, intro!!]: 
+  "[| is_subspace U V; x: U |] ==> a [*] x: U";
+  by (unfold is_subspace_def) simp;
+
+lemma subspace_diff_closed [simp, intro!!]: 
+  "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
   by (unfold diff_def negate_def) simp;
 
-lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U";
- by (unfold negate_def) simp;
+lemma subspace_neg_closed [simp, intro!!]: 
+  "[| is_subspace U V; x: U |] ==> [-] x: U";
+  by (unfold negate_def) simp;
 
-
-theorem subspace_vs [intro!!]:
+lemma subspace_vs [intro!!]:
   "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
 proof -;
   assume "is_subspace U V" "is_vectorspace V";
@@ -65,7 +73,8 @@
   show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
 qed;
 
-lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
+lemma subspace_trans: 
+  "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
 proof; 
   assume "is_subspace U V" "is_subspace V W";
   show "<0> : U"; ..;
@@ -88,7 +97,9 @@
 qed;
 
 
-section {* linear closure *};
+
+subsection {* Linear closure *};
+
 
 constdefs
   lin :: "'a => 'a set"
@@ -106,7 +117,8 @@
   show "x = 1r [*] x"; by (simp!);
 qed;
 
-lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
+lemma lin_subspace [intro!!]: 
+  "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
 proof;
   assume "is_vectorspace V" "x:V";
   show "<0> : lin x"; 
@@ -126,7 +138,8 @@
     thus "x1 [+] x2 : lin x";
     proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
       fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
-      show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
+      show "x1 [+] x2 = (a1 + a2) [*] x"; 
+        by (simp! add: vs_add_mult_distrib2);
     qed;
   qed;
 
@@ -141,14 +154,17 @@
   qed; 
 qed;
 
-
-lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
+lemma lin_vs [intro!!]: 
+  "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
 proof (rule subspace_vs);
   assume "is_vectorspace V" "x:V";
   show "is_subspace (lin x) V"; ..;
 qed;
 
-section {* sum of two vectorspaces *};
+
+
+subsection {* Sum of two vectorspaces *};
+
 
 constdefs 
   vectorspace_sum :: "['a set, 'a set] => 'a set"
@@ -159,11 +175,14 @@
 
 lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
 
-lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
+lemma vs_sumI [intro!!]: 
+  "[| x: U; y:V; (t::'a) = x [+] y |] 
+  ==> (t::'a) : vectorspace_sum U V";
   by (unfold vectorspace_sum_def, intro CollectI bexI); 
 
 lemma subspace_vs_sum1 [intro!!]: 
-  "[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)";
+  "[| is_vectorspace U; is_vectorspace V |] 
+  ==> is_subspace U (vectorspace_sum U V)";
 proof; 
   assume "is_vectorspace U" "is_vectorspace V";
   show "<0> : U"; ..;
@@ -188,7 +207,6 @@
   ==> is_subspace (vectorspace_sum U V) E";
 proof; 
   assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
-
   show "<0> : vectorspace_sum U V";
   proof (intro vs_sumI);
     show "<0> : U"; ..;
@@ -202,24 +220,28 @@
     show "x:E"; by (simp!);
   qed;
   
-  show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
+  show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. 
+        x [+] y : vectorspace_sum U V";
   proof (intro ballI);
     fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
     thus "x [+] y : vectorspace_sum U V";
     proof (elim vs_sumE bexE, intro vs_sumI);
       fix ux vx uy vy; 
-      assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
+      assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" 
+             "y = uy [+] vy";
       show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
     qed (simp!)+;
   qed;
 
-  show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
+  show "ALL x:vectorspace_sum U V. ALL a. 
+        a [*] x : vectorspace_sum U V";
   proof (intro ballI allI);
     fix x a; assume "x:vectorspace_sum U V";
     thus "a [*] x : vectorspace_sum U V";
     proof (elim vs_sumE bexE, intro vs_sumI);
       fix a x u v; assume "u : U" "v : V" "x = u [+] v";
-      show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1);
+      show "a [*] x = (a [*] u) [+] (a [*] v)"; 
+        by (simp! add: vs_add_mult_distrib1);
     qed (simp!)+;
   qed;
 qed;
@@ -233,17 +255,25 @@
 qed;
 
 
-section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
+
+subsection {* A special case *}
+
 
-lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; U Int V = {<0>}; 
-  u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] 
+text {* direct sum of a vectorspace and a linear closure of a vector 
+*};
+
+lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
+  U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] 
   ==> u1 = u2 & v1 = v2"; 
 proof; 
-  assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  "U Int V = {<0>}" 
-         "u1:U" "u2:U" "v1:V" "v2:V" "u1 [+] v1 = u2 [+] v2"; 
+  assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
+    "U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V" 
+    "u1 [+] v1 = u2 [+] v2"; 
   have eq: "u1 [-] u2 = v2 [-] v1"; by (simp! add: vs_add_diff_swap);
-  have u: "u1 [-] u2 : U"; by (simp!); with eq; have v': "v2 [-] v1 : U"; by simp; 
-  have v: "v2 [-] v1 : V"; by (simp!); with eq; have u': "u1 [-] u2 : V"; by simp;
+  have u: "u1 [-] u2 : U"; by (simp!); 
+  with eq; have v': "v2 [-] v1 : U"; by simp; 
+  have v: "v2 [-] v1 : V"; by (simp!); 
+  with eq; have u': "u1 [-] u2 : V"; by simp;
   
   show "u1 = u2";
   proof (rule vs_add_minus_eq);
@@ -256,8 +286,8 @@
   qed (rule);
 qed;
 
-lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
-  x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
+lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
+  x0 ~: H; x0 :E; x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
   ==> y1 = y2 & a1 = a2";
 proof;
   assume "is_vectorspace E" and h: "is_subspace H E"
@@ -281,7 +311,8 @@
             assume "a = 0r"; show ?thesis; by (simp!);
           next;
             assume "a ~= 0r"; 
-            from h; have "(rinv a) [*] a [*] x0 : H"; by (rule subspace_mult_closed) (simp!);
+            from h; have "(rinv a) [*] a [*] x0 : H"; 
+              by (rule subspace_mult_closed) (simp!);
             also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
             finally; have "x0 : H"; .;
             thus ?thesis; by contradiction;
@@ -306,10 +337,11 @@
 qed;
 
 lemma decomp1: 
-  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] 
+  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |]
   ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
 proof (rule, unfold split_paired_all);
-  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
+  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" 
+    "x0 ~= <0>";
   have h: "is_vectorspace H"; ..;
   fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
   have "y = t & a = 0r"; 
@@ -320,17 +352,17 @@
 lemma decomp3:
   "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
                 in (h y) + a * xi);
-      x = y [+] a [*] x0; 
-      is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
+  x = y [+] a [*] x0; is_vectorspace E; is_subspace H E;    
+  y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   ==> h0 x = h y + a * xi";
 proof -;  
   assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
                     in (h y) + a * xi)"
-         "x = y [+] a [*] x0"
-         "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
-
+         "x = y [+] a [*] x0" "is_vectorspace E" "is_subspace H E" 
+         "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
   have "x : vectorspace_sum H (lin x0)"; 
-    by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
+    by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) 
+       force+;
   have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
   proof%%;
     show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
@@ -343,15 +375,17 @@
     proof -;
       show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
         by (rule Pair_fst_snd_eq [RS iffD2]);
-      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!);
-      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!);
-      from x y; show "fst xa = fst ya & snd xa = snd ya"; by (elim conjE) (rule decomp4, (simp!)+);
+      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; 
+        by (force!);
+      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; 
+        by (force!);
+      from x y; show "fst xa = fst ya & snd xa = snd ya"; 
+        by (elim conjE) (rule decomp4, (simp!)+);
     qed;
   qed;
-  hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; by (rule select1_equality) (force!);
+  hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; 
+    by (rule select1_equality) (force!);
   thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
 qed;
 
-end;
-
-
+end;
\ No newline at end of file




