src/HOL/Real/HahnBanach/LinearSpace.thy
 changeset 7566 c5a3f980a7af parent 7535 599d3414b51d child 7656 2f18c0ffc348
```     1.1 --- a/src/HOL/Real/HahnBanach/LinearSpace.thy	Tue Sep 21 17:30:55 1999 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/LinearSpace.thy	Tue Sep 21 17:31:20 1999 +0200
1.3 @@ -1,5 +1,9 @@
1.4 +(*  Title:      HOL/Real/HahnBanach/LinearSpace.thy
1.5 +    ID:         \$Id\$
1.6 +    Author:     Gertrud Bauer, TU Munich
1.7 +*)
1.8
1.9 -theory LinearSpace = Main + RealAbs + Bounds + Aux:;
1.10 +theory LinearSpace = Bounds + Aux:;
1.11
1.12
1.13  section {* vector spaces *};
1.14 @@ -7,7 +11,7 @@
1.15  consts
1.16    sum	:: "['a, 'a] => 'a"                      (infixl "[+]" 65)
1.17    prod  :: "[real, 'a] => 'a"                    (infixr "[*]" 70)
1.18 -  zero   :: "'a"                                 ("<0>");
1.19 +  zero  :: 'a                                    ("<0>");
1.20
1.21  constdefs
1.22    negate :: "'a => 'a"                           ("[-] _" [100] 100)
1.23 @@ -41,7 +45,7 @@
1.24  lemma vs_add_minus_eq_diff: "x [+] [-] y = x [-] y";
1.26
1.27 -lemma vs_I:
1.28 +lemma vsI [intro]:
1.29    "[| <0>:V; \
1.30    \      ALL x: V. ALL a::real. a [*] x: V; \
1.31    \      ALL x: V. ALL y: V. x [+] y = y [+] x; \
1.32 @@ -53,43 +57,49 @@
1.33    \      ALL x: V. ALL a::real. ALL b::real. (a + b) [*] x = a [*] x [+] b [*] x; \
1.34    \      ALL x: V. ALL a::real. ALL b::real. (a * b) [*] x = a [*] b [*] x; \
1.35    \      ALL x: V. 1r [*] x = x |] ==> is_vectorspace V";
1.36 -  by (unfold is_vectorspace_def) auto;
1.37 +proof (unfold is_vectorspace_def, intro conjI ballI allI);
1.38 +  fix x y z; assume "x:V" "y:V" "z:V";
1.39 +  assume "ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z =  x [+] (y [+] z)";
1.40 +  thus "x [+] y [+] z =  x [+] (y [+] z)"; by (elim bspec[elimify]);
1.41 +qed force+;
1.42
1.43 -lemma zero_in_vs [simp, dest]: "is_vectorspace V ==> <0>:V";
1.44 -  by (unfold is_vectorspace_def) asm_simp;
1.45 +
1.46
1.47 -lemma vs_not_empty: "is_vectorspace V ==> (V ~= {})";
1.48 +lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
1.49 +  by (unfold is_vectorspace_def) (simp!);
1.50 +
1.51 +lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})";
1.52    by (unfold is_vectorspace_def) fast;
1.53
1.54 -lemma vs_add_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V";
1.55 -  by (unfold is_vectorspace_def) asm_simp;
1.56 +lemma vs_add_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V";
1.57 +  by (unfold is_vectorspace_def) (simp!);
1.58
1.59 -lemma vs_mult_closed [simp]: "[| is_vectorspace V; x: V |] ==> a [*] x: V";
1.60 -  by (unfold is_vectorspace_def) asm_simp;
1.61 +lemma vs_mult_closed [simp, intro!!]: "[| is_vectorspace V; x: V |] ==> a [*] x: V";
1.62 +  by (unfold is_vectorspace_def) (simp!);
1.63
1.64 -lemma vs_diff_closed [simp]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
1.65 -  by (unfold diff_def negate_def) asm_simp;
1.66 +lemma vs_diff_closed [simp, intro!!]: "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V";
1.67 +  by (unfold diff_def negate_def) (simp!);
1.68
1.69 -lemma vs_neg_closed  [simp]: "[| is_vectorspace V; x: V |] ==>  [-] x: V";
1.70 -  by (unfold negate_def) asm_simp;
1.71 +lemma vs_neg_closed  [simp, intro!!]: "[| is_vectorspace V; x: V |] ==>  [-] x: V";
1.72 +  by (unfold negate_def) (simp!);
1.73
1.75    "[| is_vectorspace V; x: V; y: V; z: V|] ==> x [+] y [+] z =  x [+] (y [+] z)";
1.76    by (unfold is_vectorspace_def) fast;
1.77
1.78  lemma vs_add_commute [simp]: "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y";
1.79 -  by (unfold is_vectorspace_def) asm_simp;
1.80 +  by (unfold is_vectorspace_def) (simp!);
1.81
1.83    "[| is_vectorspace V; x:V; y:V; z:V |] ==> x [+] (y [+] z) = y [+] (x [+] z)";
1.84  proof -;
1.85    assume vs: "is_vectorspace V" "x:V" "y:V" "z:V";
1.86    have "x [+] (y [+] z) = (x [+] y) [+] z";
1.87 -    by (asm_simp only: vs_add_assoc);
1.88 +    by (simp! only: vs_add_assoc);
1.89    also; have "... = (y [+] x) [+] z";
1.90 -    by (asm_simp only: vs_add_commute);
1.91 +    by (simp! only: vs_add_commute);
1.92    also; have "... = y [+] (x [+] z)";
1.93 -    by (asm_simp only: vs_add_assoc);
1.94 +    by (simp! only: vs_add_assoc);
1.95    finally; show ?thesis; .;
1.96  qed;
1.97
1.98 @@ -97,44 +107,44 @@
1.100
1.101  lemma vs_diff_self [simp]: "[| is_vectorspace V; x:V |] ==>  x [-] x = <0>";
1.102 -  by (unfold is_vectorspace_def) asm_simp;
1.103 +  by (unfold is_vectorspace_def) (simp!);
1.104
1.105  lemma vs_add_zero_left [simp]: "[| is_vectorspace V; x:V |] ==>  <0> [+] x = x";
1.106 -  by (unfold is_vectorspace_def) asm_simp;
1.107 +  by (unfold is_vectorspace_def) (simp!);
1.108
1.109  lemma vs_add_zero_right [simp]: "[| is_vectorspace V; x:V |] ==>  x [+] <0> = x";
1.110  proof -;
1.111    assume vs: "is_vectorspace V" "x:V";
1.112    have "x [+] <0> = <0> [+] x";
1.113 -    by asm_simp;
1.114 +    by (simp!);
1.115    also; have "... = x";
1.116 -    by asm_simp;
1.117 +    by (simp!);
1.118    finally; show ?thesis; .;
1.119  qed;
1.120
1.122    "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [+] y) = a [*] x [+] a [*] y";
1.123 -  by (unfold is_vectorspace_def) asm_simp;
1.124 +  by (unfold is_vectorspace_def) (simp!);
1.125
1.127    "[| is_vectorspace V; x:V |] ==>  (a + b) [*] x = a [*] x [+] b [*] x";
1.128 -  by (unfold is_vectorspace_def) asm_simp;
1.129 +  by (unfold is_vectorspace_def) (simp!);
1.130
1.131  lemma vs_mult_assoc: "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)";
1.132 -  by (unfold is_vectorspace_def) asm_simp;
1.133 +  by (unfold is_vectorspace_def) (simp!);
1.134
1.135  lemma vs_mult_assoc2 [simp]: "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x";
1.136 -  by (asm_simp only: vs_mult_assoc);
1.137 +  by (simp! only: vs_mult_assoc);
1.138
1.139  lemma vs_mult_1 [simp]: "[| is_vectorspace V; x:V |] ==> 1r [*] x = x";
1.140 -  by (unfold is_vectorspace_def) asm_simp;
1.141 +  by (unfold is_vectorspace_def) (simp!);
1.142
1.143  lemma vs_diff_mult_distrib1:
1.144    "[| is_vectorspace V; x:V; y:V |] ==> a [*] (x [-] y) = a [*] x [-] a [*] y";
1.147
1.148  lemma vs_minus_eq: "[| is_vectorspace V; x:V |] ==> - b [*] x = [-] (b [*] x)";
1.149 -  by (asm_simp add: negate_def);
1.150 +  by (simp! add: negate_def);
1.151
1.152  lemma vs_diff_mult_distrib2:
1.153    "[| is_vectorspace V; x:V |] ==> (a - b) [*] x = a [*] x [-] (b [*] x)";
1.154 @@ -142,7 +152,7 @@
1.155    assume "is_vectorspace V" "x:V";
1.156    have " (a - b) [*] x = (a + - b ) [*] x"; by (unfold real_diff_def, simp);
1.157    also; have "... = a [*] x [+] (- b) [*] x"; by (rule vs_add_mult_distrib2);
1.158 -  also; have "... = a [*] x [+] [-] (b [*] x)"; by (asm_simp add: vs_minus_eq);
1.159 +  also; have "... = a [*] x [+] [-] (b [*] x)"; by (simp! add: vs_minus_eq);
1.160    also; have "... = a [*] x [-] (b [*] x)"; by (unfold diff_def, simp);
1.161    finally; show ?thesis; .;
1.162  qed;
1.163 @@ -151,17 +161,17 @@
1.164  proof -;
1.165    assume vs: "is_vectorspace V" "x:V";
1.166    have  "0r [*] x = (1r - 1r) [*] x";
1.167 -    by (asm_simp only: real_diff_self);
1.168 +    by (simp! only: real_diff_self);
1.169    also; have "... = (1r + - 1r) [*] x";
1.170      by simp;
1.171    also; have "... =  1r [*] x [+] (- 1r) [*] x";
1.173    also; have "... = x [+] (- 1r) [*] x";
1.174 -    by asm_simp;
1.175 +    by (simp!);
1.176    also; have "... = x [-] x";
1.178    also; have "... = <0>";
1.179 -    by asm_simp;
1.180 +    by (simp!);
1.181    finally; show ?thesis; .;
1.182  qed;
1.183
1.184 @@ -169,40 +179,40 @@
1.185  proof -;
1.186    assume vs: "is_vectorspace V";
1.187    have "a [*] <0> = a [*] (<0> [-] (<0>::'a))";
1.188 -    by (asm_simp);
1.189 +    by (simp!);
1.190    also; from zero_in_vs [of V]; have "... =  a [*] <0> [-] a [*] <0>";
1.191 -    by (asm_simp only: vs_diff_mult_distrib1);
1.192 +    by (simp! only: vs_diff_mult_distrib1);
1.193    also; have "... = <0>";
1.194 -    by asm_simp;
1.195 +    by (simp!);
1.196    finally; show ?thesis; .;
1.197  qed;
1.198
1.199  lemma vs_minus_mult_cancel [simp]:  "[| is_vectorspace V; x:V |] ==>  (- a) [*] [-] x = a [*] x";
1.200 -  by (unfold negate_def) asm_simp;
1.201 +  by (unfold negate_def) (simp!);
1.202
1.203  lemma vs_add_minus_left_eq_diff: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] y = y [-] x";
1.204  proof -;
1.205    assume vs: "is_vectorspace V";
1.206 -  assume x: "x:V"; hence nx: "[-] x:V"; by asm_simp;
1.207 +  assume x: "x:V"; hence nx: "[-] x:V"; by (simp!);
1.208    assume y: "y:V";
1.209    have "[-] x [+] y = y [+] [-] x";
1.210 -    by (asm_simp add: vs_add_commute [RS sym, of V "[-] x"]);
1.211 +    by (simp! add: vs_add_commute [RS sym, of V "[-] x"]);
1.212    also; have "... = y [-] x";
1.214    finally; show ?thesis; .;
1.215  qed;
1.216
1.217  lemma vs_add_minus [simp]: "[| is_vectorspace V; x:V|] ==> x [+] [-] x = <0>";
1.220
1.221  lemma vs_add_minus_left [simp]: "[| is_vectorspace V; x:V |] ==> [-] x [+]  x = <0>";
1.224
1.225  lemma vs_minus_minus [simp]: "[| is_vectorspace V; x:V|] ==> [-] [-] x = x";
1.226 -  by (unfold negate_def) asm_simp;
1.227 +  by (unfold negate_def) (simp!);
1.228
1.229  lemma vs_minus_zero [simp]: "[| is_vectorspace (V::'a set)|] ==>  [-] (<0>::'a) = <0>";
1.230 -  by (unfold negate_def) asm_simp;
1.231 +  by (unfold negate_def) (simp!);
1.232
1.233  lemma vs_minus_zero_iff [simp]:
1.234    "[| is_vectorspace V; x:V|] ==>  ([-] x = <0>) = (x = <0>)" (concl is "?L = ?R");
1.235 @@ -226,20 +236,20 @@
1.236  qed;
1.237
1.238  lemma vs_add_minus_cancel [simp]:  "[| is_vectorspace V; x:V; y:V|] ==>  x [+] ([-] x [+] y) = y";
1.241
1.242  lemma vs_minus_add_cancel [simp]: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] (x [+] y) = y";
1.245
1.247    "[| is_vectorspace V; x:V; y:V|] ==>  [-] (x [+] y) = [-] x [+] [-] y";
1.250
1.251  lemma vs_diff_zero [simp]: "[| is_vectorspace V; x:V |] ==> x [-] <0> = x";
1.252 -  by (unfold diff_def) asm_simp;
1.253 +  by (unfold diff_def) (simp!);
1.254
1.255  lemma vs_diff_zero_right [simp]: "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x";
1.256 -  by (unfold diff_def) asm_simp;
1.257 +  by (unfold diff_def) (simp!);
1.258
1.260    "[|is_vectorspace V; x:V; y:V; z:V|] ==> (x [+] y = x [+] z) = (y = z)"
1.261 @@ -248,35 +258,34 @@
1.262    assume vs: "is_vectorspace V" and x: "x:V" and y: "y:V" and z: "z:V";
1.263    assume l: ?L;
1.264    have "y = <0> [+] y";
1.265 -    by asm_simp;
1.266 +    by (simp!);
1.267    also; have "... = [-] x [+] x [+] y";
1.268 -    by asm_simp;
1.269 +    by (simp!);
1.270    also; from vs vs_neg_closed x y ; have "... = [-] x [+] (x [+] y)";
1.272    also; have "...  = [-] x [+] (x [+] z)";
1.273 -    by (asm_simp only: l);
1.274 +    by (simp! only: l);
1.275    also; from vs vs_neg_closed x z; have "... = [-] x [+] x [+] z";
1.276      by (rule vs_add_assoc [RS sym]);
1.277    also; have "... = z";
1.278 -    by asm_simp;
1.279 +    by (simp!);
1.280    finally; show ?R;.;
1.281  next;
1.282    assume ?R;
1.283 -  show ?L;
1.284 -    by force;
1.285 +  thus ?L; by force;
1.286  qed;
1.287
1.289    "[| is_vectorspace V; x:V; y:V; z:V |] ==>  (y [+] x = z [+] x) = (y = z)";
1.292
1.293  lemma vs_add_assoc_cong [tag FIXME simp]: "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] \
1.294  \   ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)";
1.297
1.298  lemma vs_mult_left_commute:
1.299    "[| is_vectorspace V; x:V; y:V; z:V |] ==>  x [*] y [*] z = y [*] x [*] z";
1.300 -  by (asm_simp add: real_mult_commute);
1.301 +  by (simp! add: real_mult_commute);
1.302
1.303  lemma vs_mult_left_cancel:
1.304    "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==>  (a [*] x = a [*] y) = (x = y)"
1.305 @@ -288,20 +297,20 @@
1.306    assume a: "a ~= 0r";
1.307    assume l: ?L;
1.308    have "x = 1r [*] x";
1.309 -    by (asm_simp);
1.310 +    by (simp!);
1.311    also; have "... = (rinv a * a) [*] x";
1.312 -    by (asm_simp);
1.313 +    by (simp!);
1.314    also; have "... = rinv a [*] (a [*] x)";
1.315 -    by (asm_simp only: vs_mult_assoc);
1.316 +    by (simp! only: vs_mult_assoc);
1.317    also; have "... = rinv a [*] (a [*] y)";
1.318 -    by (asm_simp only: l);
1.319 +    by (simp! only: l);
1.320    also; have "... = y";
1.321 -    by (asm_simp);
1.322 +    by (simp!);
1.323    finally; show ?R;.;
1.324  next;
1.325    assume ?R;
1.326    show ?L;
1.327 -    by (asm_simp);
1.328 +    by (simp!);
1.329  qed;
1.330
1.331  lemma vs_eq_diff_eq:
1.332 @@ -310,32 +319,32 @@
1.333  proof -;
1.334    assume vs: "is_vectorspace V";
1.335    assume x: "x:V";
1.336 -  assume y: "y:V"; hence n: "[-] y:V"; by asm_simp;
1.337 +  assume y: "y:V"; hence n: "[-] y:V"; by (simp!);
1.338    assume z: "z:V";
1.339    show "?L = ?R";
1.340    proof;
1.341      assume l: ?L;
1.342      have "x [+] y = z [-] y [+] y";
1.343 -      by (asm_simp add: l);
1.344 +      by (simp! add: l);
1.345      also; have "... = z [+] [-] y [+] y";
1.346 -      by (asm_simp only: vs_add_minus_eq_diff);
1.347 +      by (simp! only: vs_add_minus_eq_diff);
1.348      also; from vs z n y; have "... = z [+] ([-] y [+] y)";
1.349 -      by (asm_simp only: vs_add_assoc);
1.350 +      by (simp! only: vs_add_assoc);
1.351      also; have "... = z [+] <0>";
1.352 -      by (asm_simp only: vs_add_minus_left);
1.353 +      by (simp! only: vs_add_minus_left);
1.354      also; have "... = z";
1.355 -      by (asm_simp only: vs_add_zero_right);
1.356 +      by (simp! only: vs_add_zero_right);
1.357      finally; show ?R;.;
1.358    next;
1.359      assume r: ?R;
1.360      have "z [-] y = (x [+] y) [-] y";
1.361 -      by (asm_simp only: r);
1.362 +      by (simp! only: r);
1.363      also; have "... = x [+] y [+] [-] y";
1.364 -      by (asm_simp only: vs_add_minus_eq_diff);
1.365 +      by (simp! only: vs_add_minus_eq_diff);
1.366     also; from vs x y n; have "... = x [+] (y [+] [-] y)";
1.368      also; have "... = x";
1.369 -      by (asm_simp);
1.370 +      by (simp!);
1.371      finally; show ?L; by (rule sym);
1.372    qed;
1.373  qed;
1.374 @@ -343,19 +352,19 @@
1.375  lemma vs_add_minus_eq_minus: "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x";
1.376  proof -;
1.377    assume vs: "is_vectorspace V";
1.378 -  assume x: "x:V"; hence n: "[-] x : V"; by (asm_simp);
1.379 +  assume x: "x:V"; hence n: "[-] x : V"; by (simp!);
1.380    assume y: "y:V";
1.381    assume xy: "<0> = x [+] y";
1.382    from vs n; have "[-] x = [-] x [+] <0>";
1.383 -    by asm_simp;
1.384 +    by (simp!);
1.385    also; have "... = [-] x [+] (x [+] y)";
1.386 -    by (asm_simp);
1.387 +    by (simp!);
1.388    also; from vs n x y; have "... = [-] x [+] x [+] y";
1.389      by (rule vs_add_assoc [RS sym]);
1.390    also; from vs x y; have "... = (x [+] [-] x) [+] y";
1.391 -    by (simp);
1.392 +    by simp;
1.393    also; from vs y; have "... = y";
1.394 -    by (asm_simp);
1.395 +    by (simp!);
1.396    finally; show ?thesis;
1.397      by (rule sym);
1.398  qed;
1.399 @@ -366,10 +375,10 @@
1.400    have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp);
1.401    also; have "... = <0>"; .;
1.402    finally; have e: "<0> = x [+] [-] y"; by (rule sym);
1.403 -  have "x = [-] [-] x"; by asm_simp;
1.404 +  have "x = [-] [-] x"; by (simp!);
1.405    also; from _ _ _ e; have "[-] x = [-] y";
1.406 -    by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) asm_simp+;
1.407 -  also; have "[-] ... = y"; by asm_simp;
1.408 +    by (rule vs_add_minus_eq_minus [RS sym, of V x "[-] y"]) (simp!)+;
1.409 +  also; have "[-] ... = y"; by (simp!);
1.410    finally; show "x = y"; .;
1.411  qed;
1.412
1.413 @@ -377,12 +386,12 @@
1.414    "[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] ==> a [-] c = d [-] b";
1.415  proof -;
1.416    assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" and eq: "a [+] b = c [+] d";
1.417 -  have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (asm_simp add: vs_add_left_cancel);
1.418 +  have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; by (simp! add: vs_add_left_cancel);
1.419    also; have "... = d"; by (rule vs_minus_add_cancel);
1.420    finally; have eq: "[-] c [+] (a [+] b) = d"; .;
1.421    from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b";
1.423 -  also; from eq; have "...  = d [+] [-] b"; by (asm_simp add: vs_add_right_cancel);
1.424 +  also; from eq; have "...  = d [+] [-] b"; by (simp! add: vs_add_right_cancel);
1.425    also; have "... = d [-] b"; by (simp add : diff_def);
1.426    finally; show "a [-] c = d [-] b"; .;
1.427  qed;
1.428 @@ -393,10 +402,10 @@
1.429  proof (rule classical);
1.430    assume "is_vectorspace V" "x:V" "a [*] x = <0>" "x ~= <0>";
1.431    assume "a ~= 0r";
1.432 -  have "x = (rinv a * a) [*] x"; by asm_simp;
1.433 +  have "x = (rinv a * a) [*] x"; by (simp!);
1.434    also; have "... = (rinv a) [*] (a [*] x)"; by (rule vs_mult_assoc);
1.435 -  also; have "... = (rinv a) [*] <0>"; by asm_simp;
1.436 -  also; have "... = <0>"; by asm_simp;
1.437 +  also; have "... = (rinv a) [*] <0>"; by (simp!);
1.438 +  also; have "... = <0>"; by (simp!);
1.439    finally; have "x = <0>"; .;
1.440    thus "a = 0r"; by contradiction;
1.441  qed;
1.442 @@ -407,33 +416,33 @@
1.443  proof -;
1.444    assume vs: "is_vectorspace V";
1.445    assume x: "x:V";
1.446 -  assume y: "y:V"; hence n: "[-] y:V"; by (asm_simp);
1.447 -  assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
1.448 +  assume y: "y:V"; hence n: "[-] y:V"; by (simp!);
1.449 +  assume z: "z:V"; hence xz: "x [+] z: V"; by (simp!);
1.450    assume u: "u:V";
1.451    show "?L = ?R";
1.452    proof;
1.453      assume l: ?L;
1.454      from vs u; have "u = <0> [+] u";
1.455 -      by asm_simp;
1.456 +      by (simp!);
1.457      also; from vs y vs_neg_closed u; have "... = [-] y [+] y [+] u";
1.458 -      by asm_simp;
1.459 +      by (simp!);
1.460      also; from vs n y u; have "... = [-] y [+] (y [+] u)";
1.461 -      by (asm_simp only: vs_add_assoc);
1.462 +      by (simp! only: vs_add_assoc);
1.463      also; have "... = [-] y [+] (x [+] (y [+] z))";
1.464 -      by (asm_simp only: l);
1.465 +      by (simp! only: l);
1.466      also; have "... = [-] y [+] (y [+] (x [+] z))";
1.467 -      by (asm_simp only: vs_add_left_commute);
1.468 +      by (simp! only: vs_add_left_commute);
1.469      also; from vs n y xz; have "... = [-] y [+] y [+] (x [+] z)";
1.470 -      by (asm_simp only: vs_add_assoc);
1.471 +      by (simp! only: vs_add_assoc);
1.472      also; have "... = (x [+] z)";
1.473 -      by (asm_simp);
1.474 +      by (simp!);
1.475      finally; show ?R; by (rule sym);
1.476    next;
1.477      assume r: ?R;
1.478      have "x [+] (y [+] z) = y [+] (x [+] z)";
1.479 -      by (asm_simp only: vs_add_left_commute [of V x y z]);
1.480 +      by (simp! only: vs_add_left_commute [of V x y z]);
1.481      also; have "... = y [+] u";
1.482 -      by (asm_simp only: r);
1.483 +      by (simp! only: r);
1.484      finally; show ?L; .;
1.485    qed;
1.486  qed;
1.487 @@ -445,41 +454,41 @@
1.488    assume vs: "is_vectorspace V";
1.489    assume x: "x:V";
1.490    assume y: "y:V";
1.491 -  assume z: "z:V"; hence xz: "x [+] z: V"; by (asm_simp);
1.492 -  hence nz: "[-] z: V"; by (asm_simp);
1.493 +  assume z: "z:V"; hence xz: "x [+] z: V"; by (simp!);
1.494 +  hence nz: "[-] z: V"; by (simp!);
1.495    show "?L = ?R";
1.496    proof;
1.497      assume l: ?L;
1.498 -    have n: "<0>:V"; by (asm_simp);
1.499 +    have n: "<0>:V"; by (simp!);
1.500      have "y [+] <0> = y";
1.501 -      by (asm_simp only: vs_add_zero_right);
1.502 +      by (simp! only: vs_add_zero_right);
1.503      also; have "... =  x [+] (y [+] z)";
1.504 -      by (asm_simp only: l);
1.505 +      by (simp! only: l);
1.506      also; have "... = y [+] (x [+] z)";
1.507 -      by (asm_simp only: vs_add_left_commute);
1.508 +      by (simp! only: vs_add_left_commute);
1.509      finally; have "y [+] <0> = y [+] (x [+] z)"; .;
1.510      with vs y n xz; have "<0> = x [+] z";
1.511        by (rule vs_add_left_cancel [RS iffD1]);
1.512      with vs x z; have "z = [-] x";
1.513 -      by (asm_simp only: vs_add_minus_eq_minus);
1.514 +      by (simp! only: vs_add_minus_eq_minus);
1.515      then; show ?R;
1.516 -      by (asm_simp);
1.517 +      by (simp!);
1.518    next;
1.519      assume r: ?R;
1.520      have "x [+] (y [+] z) = [-] z [+] (y [+] z)";
1.521 -      by (asm_simp only: r);
1.522 +      by (simp! only: r);
1.523      also; from vs nz y z; have "... = y [+] ([-] z [+] z)";
1.524 -       by (asm_simp only: vs_add_left_commute);
1.525 +       by (simp! only: vs_add_left_commute);
1.526      also; have "... = y [+] <0>";
1.527 -      by (asm_simp);
1.528 +      by (simp!);
1.529      also; have "... = y";
1.530 -      by (asm_simp);
1.531 +      by (simp!);
1.532      finally; show ?L; .;
1.533    qed;
1.534  qed;
1.535
1.536  lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'";
1.537 -  by (asm_simp);
1.538 +  by (simp!);
1.539
1.540
1.541  end;
1.542 \ No newline at end of file
```