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.9  theory Subspace = LinearSpace:;
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.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.22  lemma "is_subspace U V ==> U ~= {}";
1.23    by (unfold is_subspace_def) force;
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.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.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.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.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.58 -lemma subspace_neg_closed [simp]: "[| is_subspace U V; x: U |] ==> [-] x: U";
1.59 - by (unfold negate_def) asm_simp;
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.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.82  qed;
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.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.122 @@ -89,39 +94,45 @@
1.123    "lin x == {y. ? a. y = a [*] x}";
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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.302  section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
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.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.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.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.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.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.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.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.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.470  end;