src/HOL/Real/HahnBanach/Subspace.thy

                        & 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";
-  by (unfold is_subspace_def) (simp!);
+  by (unfold is_subspace_def) simp;
 
 lemma "is_subspace U V ==> U ~= {}";
   by (unfold is_subspace_def) force;
 
 lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
-  by (unfold is_subspace_def) (simp!);;
+  by (unfold is_subspace_def) simp;;
 
 lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
-  by (unfold is_subspace_def) (simp!);
+  by (unfold is_subspace_def) simp;
 
 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!);
+  by (unfold is_subspace_def) simp;
 
 lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
-  by (unfold is_subspace_def) (simp!);
+  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!);
+  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!);
+ by (unfold negate_def) simp;
 
 
 theorem subspace_vs [intro!!]:
   "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
 proof -;
-  assume "is_subspace U V";
-  assume "is_vectorspace V";
-  assume "is_subspace U V";
+  assume "is_subspace U V" "is_vectorspace V";
   show ?thesis;
   proof; 
     show "<0>:U"; ..;
     show "ALL x:U. ALL a. a [*] x : U"; by (simp!);
     show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!);

 
 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"; ..;
+
   have "U <= V"; ..;
   also; have "V <= W"; ..;
   finally; show "U <= W"; .;
+
   show "ALL x:U. ALL y:U. x [+] y : U"; 
   proof (intro ballI);
     fix x y; assume "x:U" "y:U";
     show "x [+] y : U"; by (simp!);
   qed;
+
   show "ALL x:U. ALL a. a [*] x : U";
   proof (intro ballI allI);
     fix x a; assume "x:U";
     show "a [*] x : U"; by (simp!);
   qed;

 constdefs
   lin :: "'a => 'a set"
   "lin x == {y. ? a. y = a [*] x}";
 
 lemma linD: "x : lin v = (? a::real. x = a [*] v)";
+  by (unfold lin_def) force;
+
+lemma linI [intro!!]: "a [*] x0 : lin x0";
   by (unfold lin_def) force;
 
 lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
 proof (unfold lin_def, intro CollectI exI);
   assume "is_vectorspace V" "x:V";

 constdefs 
   vectorspace_sum :: "['a set, 'a set] => 'a set"
   "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
 
 lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
-  by (unfold vectorspace_sum_def) (simp!);
+  by (unfold vectorspace_sum_def) simp;
 
 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";
   by (unfold vectorspace_sum_def, intro CollectI bexI); 

 
   show "<0> : vectorspace_sum U V";
   proof (intro vs_sumI);
     show "<0> : U"; ..;
     show "<0> : V"; ..;
-    show "(<0>::'a) = <0> [+] <0>"; 
-      by (simp!);
+    show "(<0>::'a) = <0> [+] <0>"; by (simp!);
   qed;
   
   show "vectorspace_sum U V <= E";
   proof (intro subsetI, elim vs_sumE bexE);
     fix x u v; assume "u : U" "v : V" "x = u [+] v";

 qed;
 
 
 section {* special case: 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"; 
+  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;
+  
+  show "u1 = u2";
+  proof (rule vs_add_minus_eq);
+    show "u1 [-] u2 = <0>"; by (rule Int_singletonD [OF _ u u']); 
+  qed (rule);
+
+  show "v1 = v2";
+  proof (rule vs_add_minus_eq [RS sym]);
+    show "v2 [-] v1 = <0>"; by (rule Int_singletonD [OF _ v' v]); 
+  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 |]
   ==> y1 = y2 & a1 = a2";
 proof;
-  assume "is_vectorspace E" "is_subspace H E"
-         "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
+  assume "is_vectorspace E" and h: "is_subspace H E"
+     and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
          "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
-  have h: "is_vectorspace H"; ..;
-  have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0";
-    by (simp! add: vs_add_diff_swap);
-  also; have "... = (a2 - a1) [*] x0";
-    by (rule vs_diff_mult_distrib2 [RS sym]);
-  finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
-
-  have y: "y1 [-] y2 : H"; by (simp!);
-  have x: "(a2 - a1) [*] x0 : lin x0"; by (simp! add: lin_def) force; 
-  from eq y x; have y': "y1 [-] y2 : lin x0"; by simp;
-  from eq y x; have x': "(a2 - a1) [*] x0 : H"; by simp;
-
-  have int: "H Int (lin x0) = {<0>}"; 
-  proof;
-    show "H Int lin x0 <= {<0>}"; 
-    proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
-      fix x; assume "x:H" "x:lin x0"; 
-      thus "x = <0>";
-      proof (unfold lin_def, elim CollectE exE);
-        fix a; assume "x = a [*] x0";
-        show ?thesis;
-        proof (rule case [of "a = 0r"]);
-          assume "a = 0r"; show ?thesis; by (simp!);
-        next;
-          assume "a ~= 0r"; 
-          have "(rinv a) [*] a [*] x0 : H"; 
-            by (rule vs_mult_closed [OF h]) (simp!);
-          also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
-          finally; have "x0 : H"; .;
-          thus ?thesis; by contradiction;
-        qed;
-     qed;
+
+  have c: "y1 = y2 & a1 [*] x0 = a2 [*] x0";
+  proof (rule decomp); 
+    show "a1 [*] x0 : lin x0"; ..; 
+    show "a2 [*] x0 : lin x0"; ..;
+    show "H Int (lin x0) = {<0>}"; 
+    proof;
+      show "H Int lin x0 <= {<0>}"; 
+      proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
+        fix x; assume "x:H" "x:lin x0"; 
+        thus "x = <0>";
+        proof (unfold lin_def, elim CollectE exE);
+          fix a; assume "x = a [*] x0";
+          show ?thesis;
+          proof (rule case_split [of "a = 0r"]);
+            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!);
+            also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
+            finally; have "x0 : H"; .;
+            thus ?thesis; by contradiction;
+          qed;
+       qed;
+      qed;
+      show "{<0>} <= H Int lin x0";
+      proof (intro subsetI, elim singletonE, intro IntI, simp+);
+        show "<0> : H"; ..;
+        from lin_vs; show "<0> : lin x0"; ..;
+      qed;
     qed;
-    show "{<0>} <= H Int lin x0";
-    proof (intro subsetI, elim singletonE, intro IntI, simp+);
-      show "<0> : H"; ..;
-      from lin_vs; show "<0> : lin x0"; ..;
-    qed;
-  qed;
-
-  from h; show "y1 = y2";
-  proof (rule vs_add_minus_eq);
-    show "y1 [-] y2 = <0>"; 
-      by (rule Int_singletonD [OF int y y']); 
-  qed;
- 
-  show "a1 = a2";
-  proof (rule real_add_minus_eq [RS sym]);
-    show "a2 - a1 = 0r";
-    proof (rule vs_mult_zero_uniq);
-      show "(a2 - a1) [*] x0 = <0>";  by (rule Int_singletonD [OF int x' x]);
-    qed;
-  qed;
-qed;
-
- 
+    show "is_subspace (lin x0) E"; ..;
+  qed;
+  
+  from c; show "y1 = y2"; by simp;
+  
+  show  "a1 = a2"; 
+  proof (rule vs_mult_right_cancel [RS iffD1]);
+    from c; show "a1 [*] x0 = a2 [*] x0"; by simp; 
+  qed;
+qed;
+
 lemma decomp1: 
   "[| 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>";
   have h: "is_vectorspace H"; ..;
   fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
   have "y = t & a = 0r"; 
-    by (rule decomp4) (assumption+, (simp!)); 
+    by (rule decomp4) (assumption | (simp!))+; 
   thus "(y, a) = (t, 0r)"; by (simp!);
 qed (simp!)+;
-
 
 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> |]
   ==> 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)";
-  assume "x = y [+] a [*] x0";
-  assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
+                    in (h y) + a * xi)"
+         "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+;
   have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
-  proof;
+  proof%%;
     show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
       by (force!);
   next;
     fix xa ya;
     assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"

     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!)+);
+      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!);
-  thus "h0 x = h y + a * xi"; 
-    by (simp! add: Let_def);
-qed;
-
+  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;