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.25    by (simp add: diff_def);
    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.74  lemma vs_add_assoc [simp]:  
    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.82  lemma vs_add_left_commute [simp]:
    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.99  theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute;
   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.121  lemma vs_add_mult_distrib1: 
   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.126  lemma vs_add_mult_distrib2: 
   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.145 -  by (asm_simp add: diff_def negate_def vs_add_mult_distrib1);
   1.146 +  by (simp! add: diff_def negate_def vs_add_mult_distrib1);
   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.172      by (rule vs_add_mult_distrib2);
   1.173    also; have "... = x [+] (- 1r) [*] x";
   1.174 -    by asm_simp;
   1.175 +    by (simp!);
   1.176    also; have "... = x [-] x";
   1.177      by (rule vs_add_mult_minus_1_eq_diff);
   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.213      by (simp only: vs_add_minus_eq_diff);
   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.218 -  by (asm_simp add: vs_add_minus_eq_diff); 
   1.219 +  by (simp! add: vs_add_minus_eq_diff); 
   1.220  
   1.221  lemma vs_add_minus_left [simp]: "[| is_vectorspace V; x:V |] ==> [-] x [+]  x = <0>";
   1.222 -  by (asm_simp add: vs_add_minus_eq_diff); 
   1.223 +  by (simp! add: vs_add_minus_eq_diff); 
   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.239 -  by (asm_simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
   1.240 +  by (simp! add: vs_add_assoc [RS sym] del: vs_add_commute); 
   1.241  
   1.242  lemma vs_minus_add_cancel [simp]: "[| is_vectorspace V; x:V; y:V |] ==>  [-] x [+] (x [+] y) = y"; 
   1.243 -  by (asm_simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
   1.244 +  by (simp! add: vs_add_assoc [RS sym] del: vs_add_commute); 
   1.245  
   1.246  lemma vs_minus_add_distrib [simp]:  
   1.247    "[| is_vectorspace V; x:V; y:V|] ==>  [-] (x [+] y) = [-] x [+] [-] y";
   1.248 -  by (unfold negate_def, asm_simp add: vs_add_mult_distrib1);
   1.249 +  by (unfold negate_def, simp! add: vs_add_mult_distrib1);
   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.259  lemma vs_add_left_cancel:
   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.271      by (rule vs_add_assoc);
   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.288  lemma vs_add_right_cancel: 
   1.289    "[| is_vectorspace V; x:V; y:V; z:V |] ==>  (y [+] x = z [+] x) = (y = z)";  
   1.290 -  by (asm_simp only: vs_add_commute vs_add_left_cancel);
   1.291 +  by (simp! only: vs_add_commute vs_add_left_cancel);
   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.295 -  by (asm_simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
   1.296 +  by (simp! del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]);
   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.367        by (rule vs_add_assoc); 
   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.422      by (simp add: vs_add_ac diff_def);
   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