src/HOL/Real/HahnBanach/Linearform.thy
changeset 7566 c5a3f980a7af
parent 7535 599d3414b51d
child 7656 2f18c0ffc348
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Tue Sep 21 17:30:55 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Tue Sep 21 17:31:20 1999 +0200
     1.3 @@ -1,3 +1,7 @@
     1.4 +(*  Title:      HOL/Real/HahnBanach/Linearform.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gertrud Bauer, TU Munich
     1.7 +*)
     1.8  
     1.9  theory Linearform = LinearSpace:;
    1.10  
    1.11 @@ -12,39 +16,41 @@
    1.12  lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
    1.13      !! x c. x : V ==> f (c [*] x) = c * f x |]
    1.14   ==> is_linearform V f";
    1.15 - by (unfold is_linearform_def, force);
    1.16 + by (unfold is_linearform_def) force;
    1.17  
    1.18 -lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
    1.19 - by (unfold is_linearform_def, auto);
    1.20 +lemma linearform_add_linear [intro!!]: 
    1.21 +  "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
    1.22 +  by (unfold is_linearform_def) auto;
    1.23  
    1.24 -lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==>  f (a [*] x) = a * (f x)"; 
    1.25 - by (unfold is_linearform_def, auto);
    1.26 +lemma linearform_mult_linear [intro!!]: 
    1.27 +  "[| is_linearform V f; x:V |] ==>  f (a [*] x) = a * (f x)"; 
    1.28 +  by (unfold is_linearform_def) auto;
    1.29  
    1.30 -lemma linearform_neg_linear:
    1.31 +lemma linearform_neg_linear [intro!!]:
    1.32    "[|  is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
    1.33  proof -; 
    1.34    assume "is_linearform V f" "is_vectorspace V" "x:V"; 
    1.35 -  have "f ([-] x) = f ((- 1r) [*] x)"; by (asm_simp add: vs_mult_minus_1);
    1.36 +  have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1);
    1.37    also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
    1.38 -  also; have "... = - (f x)"; by asm_simp;
    1.39 +  also; have "... = - (f x)"; by (simp!);
    1.40    finally; show ?thesis; .;
    1.41  qed;
    1.42  
    1.43 -lemma linearform_diff_linear: 
    1.44 +lemma linearform_diff_linear [intro!!]: 
    1.45    "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";  
    1.46  proof -;
    1.47    assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
    1.48    have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
    1.49 -  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+);
    1.50 +  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+;
    1.51    also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
    1.52 -  finally; show "f (x [-] y) = f x - f y"; by asm_simp;
    1.53 +  finally; show "f (x [-] y) = f x - f y"; by (simp!);
    1.54  qed;
    1.55  
    1.56 -lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
    1.57 +lemma linearform_zero [intro!!]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
    1.58  proof -; 
    1.59    assume "is_vectorspace V" "is_linearform V f";
    1.60 -  have "f <0> = f (<0> [-] <0>)"; by asm_simp;
    1.61 -  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+;
    1.62 +  have "f <0> = f (<0> [-] <0>)"; by (simp!);
    1.63 +  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+;
    1.64    also; have "... = 0r"; by simp;
    1.65    finally; show "f <0> = 0r"; .;
    1.66  qed;