src/HOL/Real/HahnBanach/Linearform.thy
changeset 7808 fd019ac3485f
parent 7656 2f18c0ffc348
child 7917 5e5b9813cce7
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 08 16:18:51 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 08 16:40:27 1999 +0200
     1.3 @@ -3,9 +3,9 @@
     1.4      Author:     Gertrud Bauer, TU Munich
     1.5  *)
     1.6  
     1.7 -theory Linearform = LinearSpace:;
     1.8 +header {* Linearforms *};
     1.9  
    1.10 -section {* linearforms *};
    1.11 +theory Linearform = LinearSpace:;
    1.12  
    1.13  constdefs
    1.14    is_linearform :: "['a set, 'a => real] => bool" 
    1.15 @@ -13,7 +13,8 @@
    1.16        (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) &
    1.17        (ALL x: V. ALL a. f (a [*] x) = a * (f x))"; 
    1.18  
    1.19 -lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
    1.20 +lemma is_linearformI [intro]: 
    1.21 +  "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
    1.22      !! x c. x : V ==> f (c [*] x) = c * f x |]
    1.23   ==> is_linearform V f";
    1.24   by (unfold is_linearform_def) force;
    1.25 @@ -30,30 +31,33 @@
    1.26    "[|  is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
    1.27  proof -; 
    1.28    assume "is_linearform V f" "is_vectorspace V" "x:V"; 
    1.29 -  have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1);
    1.30 +  have "f ([-] x) = f ((- 1r) [*] x)"; by (unfold negate_def) simp;
    1.31    also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
    1.32    also; have "... = - (f x)"; by (simp!);
    1.33    finally; show ?thesis; .;
    1.34  qed;
    1.35  
    1.36  lemma linearform_diff_linear [intro!!]: 
    1.37 -  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";  
    1.38 +  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
    1.39 +  ==> f (x [-] y) = f x - f y";  
    1.40  proof -;
    1.41    assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
    1.42    have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
    1.43 -  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+;
    1.44 +  also; have "... = f x + f ([-] y)"; 
    1.45 +    by (rule linearform_add_linear) (simp!)+;
    1.46    also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
    1.47    finally; show "f (x [-] y) = f x - f y"; by (simp!);
    1.48  qed;
    1.49  
    1.50 -lemma linearform_zero [intro!!, simp]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
    1.51 +lemma linearform_zero [intro!!, simp]: 
    1.52 +  "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
    1.53  proof -; 
    1.54    assume "is_vectorspace V" "is_linearform V f";
    1.55    have "f <0> = f (<0> [-] <0>)"; by (simp!);
    1.56 -  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+;
    1.57 +  also; have "... = f <0> - f <0>"; 
    1.58 +    by (rule linearform_diff_linear) (simp!)+;
    1.59    also; have "... = 0r"; by simp;
    1.60    finally; show "f <0> = 0r"; .;
    1.61  qed; 
    1.62  
    1.63 -end;
    1.64 -
    1.65 +end;
    1.66 \ No newline at end of file