src/HOL/Real/HahnBanach/Subspace.thy
changeset 7566 c5a3f980a7af
parent 7535 599d3414b51d
child 7567 62384a807775
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 17:30:55 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Tue Sep 21 17:31:20 1999 +0200
     1.3 @@ -1,3 +1,7 @@
     1.4 +(*  Title:      HOL/Real/HahnBanach/Subspace.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gertrud Bauer, TU Munich
     1.7 +*)
     1.8  
     1.9  theory Subspace = LinearSpace:;
    1.10  
    1.11 @@ -10,74 +14,75 @@
    1.12       &  (ALL x:U. ALL y:U. ALL a. x [+] y : U                          
    1.13                         & a [*] x : U)";                            
    1.14  
    1.15 -lemma subspace_I: 
    1.16 +lemma subspaceI [intro]: 
    1.17    "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |]
    1.18    \ ==> is_subspace U V";
    1.19 -  by (unfold is_subspace_def) blast;
    1.20 +  by (unfold is_subspace_def) (simp!);
    1.21  
    1.22  lemma "is_subspace U V ==> U ~= {}";
    1.23    by (unfold is_subspace_def) force;
    1.24  
    1.25 -lemma zero_in_subspace: "is_subspace U V ==> <0>:U";
    1.26 +lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
    1.27 +  by (unfold is_subspace_def) (simp!);;
    1.28 +
    1.29 +lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
    1.30 +  by (unfold is_subspace_def) (simp!);
    1.31 +
    1.32 +lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V";
    1.33    by (unfold is_subspace_def) force;
    1.34  
    1.35 -lemma subspace_subset: "is_subspace U V ==> U <= V";
    1.36 -  by (unfold is_subspace_def) fast;
    1.37 +lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
    1.38 +  by (unfold is_subspace_def) (simp!);
    1.39  
    1.40 -lemma subspace_subset2 [simp]: "[| is_subspace U V; x:U |]==> x:V";
    1.41 -  by (unfold is_subspace_def) fast;
    1.42 -
    1.43 -lemma subspace_add_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
    1.44 -  by (unfold is_subspace_def) asm_simp;
    1.45 +lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
    1.46 +  by (unfold is_subspace_def) (simp!);
    1.47  
    1.48 -lemma subspace_mult_closed [simp]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
    1.49 -  by (unfold is_subspace_def) asm_simp;
    1.50 +lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
    1.51 +  by (unfold diff_def negate_def) (simp!);
    1.52  
    1.53 -lemma subspace_diff_closed [simp]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
    1.54 -  by (unfold diff_def negate_def) asm_simp;
    1.55 +lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U";
    1.56 + by (unfold negate_def) (simp!);
    1.57  
    1.58 -lemma subspace_neg_closed [simp]: "[| is_subspace U V; x: U |] ==> [-] x: U";
    1.59 - by (unfold negate_def) asm_simp;
    1.60  
    1.61  theorem subspace_vs [intro!!]:
    1.62    "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
    1.63  proof -;
    1.64 -  presume "U <= V";
    1.65 +  assume "is_subspace U V";
    1.66    assume "is_vectorspace V";
    1.67    assume "is_subspace U V";
    1.68    show ?thesis;
    1.69 -  proof (rule vs_I);
    1.70 -    show "<0>:U"; by (rule zero_in_subspace);
    1.71 -    show "ALL x:U. ALL a. a [*] x : U"; by asm_simp;
    1.72 -    show "ALL x:U. ALL y:U. x [+] y : U"; by asm_simp;
    1.73 -  qed (asm_simp add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
    1.74 -next;
    1.75 -  assume "is_subspace U V";
    1.76 -  show "U <= V"; by (rule subspace_subset);
    1.77 +  proof; 
    1.78 +    show "<0>:U"; ..;
    1.79 +    show "ALL x:U. ALL a. a [*] x : U"; by (simp!);
    1.80 +    show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!);
    1.81 +  qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
    1.82  qed;
    1.83  
    1.84 -lemma subspace_refl: "is_vectorspace V ==> is_subspace V V";
    1.85 -proof (unfold is_subspace_def, intro conjI); 
    1.86 +lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
    1.87 +proof; 
    1.88    assume "is_vectorspace V";
    1.89 -  show "<0> : V"; by (rule zero_in_vs [of V], assumption);
    1.90 -  show "V <= V"; by (simp);
    1.91 -  show "ALL x::'a:V. ALL y::'a:V. ALL a::real. x [+] y : V & a [*] x : V"; by (asm_simp);
    1.92 +  show "<0> : V"; ..;
    1.93 +  show "V <= V"; ..;
    1.94 +  show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!);
    1.95 +  show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
    1.96  qed;
    1.97  
    1.98  lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
    1.99 -proof (rule subspace_I); 
   1.100 +proof; 
   1.101    assume "is_subspace U V" "is_subspace V W";
   1.102 -  show "<0> : U"; by (rule zero_in_subspace);;
   1.103 -  from subspace_subset [of U] subspace_subset [of V]; show uw: "U <= W"; by force;
   1.104 +  show "<0> : U"; ..;
   1.105 +  have "U <= V"; ..;
   1.106 +  also; have "V <= W"; ..;
   1.107 +  finally; show "U <= W"; .;
   1.108    show "ALL x:U. ALL y:U. x [+] y : U"; 
   1.109    proof (intro ballI);
   1.110      fix x y; assume "x:U" "y:U";
   1.111 -    show "x [+] y : U"; by (rule subspace_add_closed);
   1.112 +    show "x [+] y : U"; by (simp!);
   1.113    qed;
   1.114    show "ALL x:U. ALL a. a [*] x : U";
   1.115    proof (intro ballI allI);
   1.116      fix x a; assume "x:U";
   1.117 -    show "a [*] x : U"; by (rule subspace_mult_closed);
   1.118 +    show "a [*] x : U"; by (simp!);
   1.119    qed;
   1.120  qed;
   1.121  
   1.122 @@ -89,39 +94,45 @@
   1.123    "lin x == {y. ? a. y = a [*] x}";
   1.124  
   1.125  lemma linD: "x : lin v = (? a::real. x = a [*] v)";
   1.126 -  by (unfold lin_def) fast;
   1.127 +  by (unfold lin_def) force;
   1.128  
   1.129  lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
   1.130  proof (unfold lin_def, intro CollectI exI);
   1.131    assume "is_vectorspace V" "x:V";
   1.132 -  show "x = 1r [*] x"; by (asm_simp);
   1.133 +  show "x = 1r [*] x"; by (simp!);
   1.134  qed;
   1.135  
   1.136 -lemma lin_subspace: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
   1.137 -proof (rule subspace_I);
   1.138 +lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
   1.139 +proof;
   1.140    assume "is_vectorspace V" "x:V";
   1.141    show "<0> : lin x"; 
   1.142    proof (unfold lin_def, intro CollectI exI);
   1.143 -    show "<0> = 0r [*] x"; by asm_simp;
   1.144 +    show "<0> = 0r [*] x"; by (simp!);
   1.145    qed;
   1.146 +
   1.147    show "lin x <= V";
   1.148 -  proof (unfold lin_def, intro subsetI, elim CollectD [elimify] exE); 
   1.149 -    fix xa a; assume "xa = a [*] x"; show "xa:V"; by asm_simp;
   1.150 +  proof (unfold lin_def, intro subsetI, elim CollectE exE); 
   1.151 +    fix xa a; assume "xa = a [*] x"; 
   1.152 +    show "xa:V"; by (simp!);
   1.153    qed;
   1.154 +
   1.155    show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; 
   1.156    proof (intro ballI);
   1.157 -    fix x1 x2; assume "x1 : lin x" "x2 : lin x"; show "x1 [+] x2 : lin x";
   1.158 -    proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
   1.159 +    fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
   1.160 +    thus "x1 [+] x2 : lin x";
   1.161 +    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);   (* FIXME !? *)
   1.162        fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
   1.163 -      show "x1 [+] x2 = (a1 + a2) [*] x"; by (asm_simp add: vs_add_mult_distrib2);
   1.164 +      show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
   1.165      qed;
   1.166    qed;
   1.167 +
   1.168    show "ALL xa:lin x. ALL a. a [*] xa : lin x"; 
   1.169    proof (intro ballI allI);
   1.170 -    fix x1 a; assume "x1 : lin x"; show "a [*] x1 : lin x";
   1.171 -    proof (unfold lin_def, elim CollectD [elimify] exE, intro CollectI exI);
   1.172 +    fix x1 a; assume "x1 : lin x"; 
   1.173 +    thus "a [*] x1 : lin x";
   1.174 +    proof (-, unfold lin_def, elim CollectE exE, intro CollectI exI);
   1.175        fix a1; assume "x1 = a1 [*] x";
   1.176 -      show "a [*] x1 = (a * a1) [*] x"; by asm_simp;
   1.177 +      show "a [*] x1 = (a * a1) [*] x"; by (simp!);
   1.178      qed;
   1.179    qed; 
   1.180  qed;
   1.181 @@ -130,7 +141,7 @@
   1.182  lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
   1.183  proof (rule subspace_vs);
   1.184    assume "is_vectorspace V" "x:V";
   1.185 -  show "is_subspace (lin x) V"; by (rule lin_subspace);
   1.186 +  show "is_subspace (lin x) V"; ..;
   1.187  qed;
   1.188  
   1.189  section {* sum of two vectorspaces *};
   1.190 @@ -140,159 +151,181 @@
   1.191    "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
   1.192  
   1.193  lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
   1.194 -  by (unfold vectorspace_sum_def) fast;
   1.195 +  by (unfold vectorspace_sum_def) (simp!);
   1.196  
   1.197 -lemma vs_sum_I: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
   1.198 +lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
   1.199 +
   1.200 +lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
   1.201    by (unfold vectorspace_sum_def, intro CollectI bexI); 
   1.202  
   1.203  lemma subspace_vs_sum1 [intro!!]: 
   1.204    "[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)";
   1.205 -proof (rule subspace_I);
   1.206 +proof; 
   1.207    assume "is_vectorspace U" "is_vectorspace V";
   1.208 -  show "<0> : U"; by (rule zero_in_vs);
   1.209 +  show "<0> : U"; ..;
   1.210    show "U <= vectorspace_sum U V";
   1.211 -  proof (intro subsetI vs_sum_I);
   1.212 +  proof (intro subsetI vs_sumI);
   1.213    fix x; assume "x:U";
   1.214 -    show "x = x [+] <0>"; by asm_simp;
   1.215 -    show "<0> : V"; by asm_simp;
   1.216 +    show "x = x [+] <0>"; by (simp!);
   1.217 +    show "<0> : V"; by (simp!);
   1.218    qed;
   1.219    show "ALL x:U. ALL y:U. x [+] y : U"; 
   1.220    proof (intro ballI);
   1.221 -    fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by asm_simp;
   1.222 +    fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!);
   1.223    qed;
   1.224    show "ALL x:U. ALL a. a [*] x : U"; 
   1.225    proof (intro ballI allI);
   1.226 -    fix x a; assume "x:U"; show "a [*] x : U"; by asm_simp;
   1.227 +    fix x a; assume "x:U"; show "a [*] x : U"; by (simp!);
   1.228    qed;
   1.229  qed;
   1.230  
   1.231 -lemma vs_sum_subspace: 
   1.232 -  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_subspace (vectorspace_sum U V) E";
   1.233 -proof (rule subspace_I);
   1.234 -  assume u: "is_subspace U E" and v: "is_subspace V E" and e: "is_vectorspace E";
   1.235 +lemma vs_sum_subspace [intro!!]: 
   1.236 +  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   1.237 +  ==> is_subspace (vectorspace_sum U V) E";
   1.238 +proof; 
   1.239 +  assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
   1.240  
   1.241    show "<0> : vectorspace_sum U V";
   1.242 -  by (intro vs_sum_I, rule vs_add_zero_left [RS sym], 
   1.243 -      rule zero_in_subspace, rule zero_in_subspace, rule zero_in_vs); 
   1.244 -
   1.245 +  proof (intro vs_sumI);
   1.246 +    show "<0> : U"; ..;
   1.247 +    show "<0> : V"; ..;
   1.248 +    show "(<0>::'a) = <0> [+] <0>"; 
   1.249 +      by (simp!);
   1.250 +  qed;
   1.251 +  
   1.252    show "vectorspace_sum U V <= E";
   1.253 -  proof (intro subsetI, elim vs_sumD [RS iffD1, elimify] bexE);
   1.254 +  proof (intro subsetI, elim vs_sumE bexE);
   1.255      fix x u v; assume "u : U" "v : V" "x = u [+] v";
   1.256 -    show "x:E"; by (asm_simp);
   1.257 +    show "x:E"; by (simp!);
   1.258    qed;
   1.259    
   1.260    show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
   1.261 -  proof (intro ballI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
   1.262 -    fix x y ux vx uy vy; assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
   1.263 -    show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by asm_simp;
   1.264 -  qed asm_simp+;
   1.265 +  proof (intro ballI);
   1.266 +    fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
   1.267 +    thus "x [+] y : vectorspace_sum U V";
   1.268 +    proof (elim vs_sumE bexE, intro vs_sumI);
   1.269 +      fix ux vx uy vy; 
   1.270 +      assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
   1.271 +      show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
   1.272 +    qed (simp!)+;
   1.273 +  qed;
   1.274  
   1.275    show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
   1.276 -  proof (intro ballI allI, elim vs_sumD [RS iffD1, elimify] bexE, intro vs_sum_I);
   1.277 -    fix a x u v; assume "u : U" "v : V" "x = u [+] v";
   1.278 -    show "a [*] x = (a [*] u) [+] (a [*] v)"; by (asm_simp add: vs_add_mult_distrib1 [OF e]);
   1.279 -  qed asm_simp+;
   1.280 +  proof (intro ballI allI);
   1.281 +    fix x a; assume "x:vectorspace_sum U V";
   1.282 +    thus "a [*] x : vectorspace_sum U V";
   1.283 +    proof (elim vs_sumE bexE, intro vs_sumI);
   1.284 +      fix a x u v; assume "u : U" "v : V" "x = u [+] v";
   1.285 +      show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1);
   1.286 +    qed (simp!)+;
   1.287 +  qed;
   1.288  qed;
   1.289  
   1.290 -lemma vs_sum_vs: 
   1.291 -  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] ==> is_vectorspace (vectorspace_sum U V)";
   1.292 -  by (rule subspace_vs [OF vs_sum_subspace]);
   1.293 +lemma vs_sum_vs [intro!!]: 
   1.294 +  "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   1.295 +  ==> is_vectorspace (vectorspace_sum U V)";
   1.296 +proof (rule subspace_vs);
   1.297 +  assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
   1.298 +  show "is_subspace (vectorspace_sum U V) E"; ..;
   1.299 +qed;
   1.300  
   1.301  
   1.302  section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
   1.303  
   1.304 -
   1.305 -lemma lemma4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
   1.306 +lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
   1.307    x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
   1.308    ==> y1 = y2 & a1 = a2";
   1.309  proof;
   1.310    assume "is_vectorspace E" "is_subspace H E"
   1.311           "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
   1.312           "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
   1.313 -  have h: "is_vectorspace H"; by (rule subspace_vs);
   1.314 -  have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0"; 
   1.315 -    by (rule vs_add_diff_swap) asm_simp+;
   1.316 +  have h: "is_vectorspace H"; ..;
   1.317 +  have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0";
   1.318 +    by (simp! add: vs_add_diff_swap);
   1.319    also; have "... = (a2 - a1) [*] x0";
   1.320      by (rule vs_diff_mult_distrib2 [RS sym]);
   1.321    finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
   1.322  
   1.323 -  have y: "y1 [-] y2 : H"; by asm_simp;
   1.324 -  have x: "(a2 - a1) [*] x0 : lin x0"; by (asm_simp add: lin_def) force; 
   1.325 -  from y; have y': "y1 [-] y2 : lin x0"; by (simp only: eq x);
   1.326 -  from x; have x': "(a2 - a1) [*] x0 : H"; by (simp only: eq [RS sym] y);
   1.327 +  have y: "y1 [-] y2 : H"; by (simp!);
   1.328 +  have x: "(a2 - a1) [*] x0 : lin x0"; by (simp! add: lin_def) force; 
   1.329 +  from eq y x; have y': "y1 [-] y2 : lin x0"; by simp;
   1.330 +  from eq y x; have x': "(a2 - a1) [*] x0 : H"; by simp;
   1.331  
   1.332    have int: "H Int (lin x0) = {<0>}"; 
   1.333    proof;
   1.334      show "H Int lin x0 <= {<0>}"; 
   1.335 -    proof (intro subsetI, unfold lin_def, elim IntE CollectD[elimify] exE,
   1.336 -      rule singleton_iff[RS iffD2]);
   1.337 -      fix x a; assume "x : H" and ax0: "x = a [*] x0";
   1.338 -      show "x = <0>";
   1.339 -      proof (rule case [of "a=0r"]);
   1.340 -        assume "a = 0r"; show ?thesis; by asm_simp;
   1.341 -      next;
   1.342 -        assume "a ~= 0r"; 
   1.343 -        have "(rinv a) [*] a [*] x0 : H"; 
   1.344 -          by (rule vs_mult_closed [OF h]) asm_simp;
   1.345 -        also; have "(rinv a) [*] a [*] x0 = x0"; by asm_simp;
   1.346 -        finally; have "x0 : H"; .;
   1.347 -        thus ?thesis; by contradiction;
   1.348 -      qed;
   1.349 +    proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
   1.350 +      fix x; assume "x:H" "x:lin x0"; 
   1.351 +      thus "x = <0>";
   1.352 +      proof (-, unfold lin_def, elim CollectE exE);
   1.353 +        fix a; assume "x = a [*] x0";
   1.354 +        show ?thesis;
   1.355 +        proof (rule case [of "a = 0r"]);
   1.356 +          assume "a = 0r"; show ?thesis; by (simp!);
   1.357 +        next;
   1.358 +          assume "a ~= 0r"; 
   1.359 +          have "(rinv a) [*] a [*] x0 : H"; 
   1.360 +            by (rule vs_mult_closed [OF h]) (simp!);
   1.361 +          also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
   1.362 +          finally; have "x0 : H"; .;
   1.363 +          thus ?thesis; by contradiction;
   1.364 +        qed;
   1.365 +     qed;
   1.366      qed;
   1.367 -    show "{<0>} <= H Int lin x0"; 
   1.368 -    proof (intro subsetI, elim singletonD[elimify], intro IntI, asm_simp+);
   1.369 -      show "<0> : H"; by (rule zero_in_vs [OF h]);
   1.370 -      show "<0> : lin x0"; by (rule zero_in_vs [OF lin_vs]);
   1.371 +    show "{<0>} <= H Int lin x0";
   1.372 +    proof (intro subsetI, elim singletonE, intro IntI, simp+);
   1.373 +      show "<0> : H"; ..;
   1.374 +      from lin_vs; show "<0> : lin x0"; ..;
   1.375      qed;
   1.376    qed;
   1.377  
   1.378    from h; show "y1 = y2";
   1.379    proof (rule vs_add_minus_eq);
   1.380 -    show "y1 [-] y2 = <0>";
   1.381 -      by (rule Int_singeltonD [OF int y y']); 
   1.382 +    show "y1 [-] y2 = <0>"; 
   1.383 +      by (rule Int_singletonD [OF int y y']); 
   1.384    qed;
   1.385   
   1.386    show "a1 = a2";
   1.387    proof (rule real_add_minus_eq [RS sym]);
   1.388      show "a2 - a1 = 0r";
   1.389      proof (rule vs_mult_zero_uniq);
   1.390 -      show "(a2 - a1) [*] x0 = <0>";  by (rule Int_singeltonD [OF int x' x]);
   1.391 +      show "(a2 - a1) [*] x0 = <0>";  by (rule Int_singletonD [OF int x' x]);
   1.392      qed;
   1.393    qed;
   1.394  qed;
   1.395  
   1.396   
   1.397 -lemma lemma1: 
   1.398 +lemma decomp1: 
   1.399    "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] 
   1.400    ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
   1.401  proof (rule, unfold split_paired_all);
   1.402    assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
   1.403 -  have h: "is_vectorspace H"; by (rule subspace_vs);
   1.404 +  have h: "is_vectorspace H"; ..;
   1.405    fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
   1.406    have "y = t & a = 0r"; 
   1.407 -    by (rule lemma4) (assumption+, asm_simp); 
   1.408 -  thus "(y, a) = (t, 0r)"; by asm_simp;
   1.409 -qed asm_simp+;
   1.410 +    by (rule decomp4) (assumption+, (simp!)); 
   1.411 +  thus "(y, a) = (t, 0r)"; by (simp!);
   1.412 +qed (simp!)+;
   1.413  
   1.414  
   1.415 -lemma lemma3: "!! x0 h xi x y a H. [| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
   1.416 -                            in (h y) + a * xi);
   1.417 -                  x = y [+] a [*] x0; 
   1.418 -                  is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   1.419 +lemma decomp3:
   1.420 +  "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
   1.421 +                in (h y) + a * xi);
   1.422 +      x = y [+] a [*] x0; 
   1.423 +      is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   1.424    ==> h0 x = h y + a * xi";
   1.425  proof -;  
   1.426 -  fix x0 h xi x y a H;
   1.427    assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
   1.428 -                            in (h y) + a * xi)";
   1.429 +                    in (h y) + a * xi)";
   1.430    assume "x = y [+] a [*] x0";
   1.431    assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
   1.432  
   1.433    have "x : vectorspace_sum H (lin x0)"; 
   1.434 -    by (asm_simp add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
   1.435 +    by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
   1.436    have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
   1.437    proof;
   1.438 -    show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
   1.439 -      by (asm_simp, rule exI, force);
   1.440 +    show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
   1.441 +      by (force!);
   1.442    next;
   1.443      fix xa ya;
   1.444      assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
   1.445 @@ -300,18 +333,18 @@
   1.446      show "xa = ya"; ;
   1.447      proof -;
   1.448        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
   1.449 -        by(rule Pair_fst_snd_eq [RS iffD2]);
   1.450 -      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by force;
   1.451 -      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by force;
   1.452 +        by (rule Pair_fst_snd_eq [RS iffD2]);
   1.453 +      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!);
   1.454 +      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!);
   1.455        from x y; show "fst xa = fst ya & snd xa = snd ya"; 
   1.456 -        by (elim conjE) (rule lemma4, asm_simp+);
   1.457 +        by (elim conjE) (rule decomp4, (simp!)+);
   1.458      qed;
   1.459    qed;
   1.460    hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; 
   1.461 -    by (rule select1_equality, force);
   1.462 +    by (rule select1_equality) (force!);
   1.463    thus "h0 x = h y + a * xi"; 
   1.464 -    by (asm_simp add: Let_def);
   1.465 -qed;  
   1.466 +    by (simp! add: Let_def);
   1.467 +qed;
   1.468  
   1.469  
   1.470  end;