src/HOL/Real/HahnBanach/Linearform.thy
changeset 9035 371f023d3dbd
parent 9013 9dd0274f76af
child 9374 153853af318b
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Sun Jun 04 00:09:04 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Sun Jun 04 19:39:29 2000 +0200
     1.3 @@ -3,67 +3,67 @@
     1.4      Author:     Gertrud Bauer, TU Munich
     1.5  *)
     1.6  
     1.7 -header {* Linearforms *};
     1.8 +header {* Linearforms *}
     1.9  
    1.10 -theory Linearform = VectorSpace:;
    1.11 +theory Linearform = VectorSpace:
    1.12  
    1.13  text{* A \emph{linear form} is a function on a vector
    1.14 -space into the reals that is additive and multiplicative. *};
    1.15 +space into the reals that is additive and multiplicative. *}
    1.16  
    1.17  constdefs
    1.18    is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
    1.19    "is_linearform V f == 
    1.20        (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
    1.21 -      (ALL x: V. ALL a. f (a (*) x) = a * (f x))"; 
    1.22 +      (ALL x: V. ALL a. f (a (*) x) = a * (f x))" 
    1.23  
    1.24  lemma is_linearformI [intro]: 
    1.25    "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
    1.26      !! x c. x : V ==> f (c (*) x) = c * f x |]
    1.27 - ==> is_linearform V f";
    1.28 - by (unfold is_linearform_def) force;
    1.29 + ==> is_linearform V f"
    1.30 + by (unfold is_linearform_def) force
    1.31  
    1.32  lemma linearform_add [intro??]: 
    1.33 -  "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y";
    1.34 -  by (unfold is_linearform_def) fast;
    1.35 +  "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y"
    1.36 +  by (unfold is_linearform_def) fast
    1.37  
    1.38  lemma linearform_mult [intro??]: 
    1.39 -  "[| is_linearform V f; x:V |] ==>  f (a (*) x) = a * (f x)"; 
    1.40 -  by (unfold is_linearform_def) fast;
    1.41 +  "[| is_linearform V f; x:V |] ==>  f (a (*) x) = a * (f x)" 
    1.42 +  by (unfold is_linearform_def) fast
    1.43  
    1.44  lemma linearform_neg [intro??]:
    1.45    "[|  is_vectorspace V; is_linearform V f; x:V|] 
    1.46 -  ==> f (- x) = - f x";
    1.47 -proof -; 
    1.48 -  assume "is_linearform V f" "is_vectorspace V" "x:V"; 
    1.49 -  have "f (- x) = f ((- (#1::real)) (*) x)"; by (simp! add: negate_eq1);
    1.50 -  also; have "... = (- #1) * (f x)"; by (rule linearform_mult);
    1.51 -  also; have "... = - (f x)"; by (simp!);
    1.52 -  finally; show ?thesis; .;
    1.53 -qed;
    1.54 +  ==> f (- x) = - f x"
    1.55 +proof - 
    1.56 +  assume "is_linearform V f" "is_vectorspace V" "x:V"
    1.57 +  have "f (- x) = f ((- #1) (*) x)" by (simp! add: negate_eq1)
    1.58 +  also have "... = (- #1) * (f x)" by (rule linearform_mult)
    1.59 +  also have "... = - (f x)" by (simp!)
    1.60 +  finally show ?thesis .
    1.61 +qed
    1.62  
    1.63  lemma linearform_diff [intro??]: 
    1.64    "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
    1.65 -  ==> f (x - y) = f x - f y";  
    1.66 -proof -;
    1.67 -  assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
    1.68 -  have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1);
    1.69 -  also; have "... = f x + f (- y)"; 
    1.70 -    by (rule linearform_add) (simp!)+;
    1.71 -  also; have "f (- y) = - f y"; by (rule linearform_neg);
    1.72 -  finally; show "f (x - y) = f x - f y"; by (simp!);
    1.73 -qed;
    1.74 +  ==> f (x - y) = f x - f y"  
    1.75 +proof -
    1.76 +  assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"
    1.77 +  have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
    1.78 +  also have "... = f x + f (- y)" 
    1.79 +    by (rule linearform_add) (simp!)+
    1.80 +  also have "f (- y) = - f y" by (rule linearform_neg)
    1.81 +  finally show "f (x - y) = f x - f y" by (simp!)
    1.82 +qed
    1.83  
    1.84 -text{* Every linear form yields $0$ for the $\zero$ vector.*};
    1.85 +text{* Every linear form yields $0$ for the $\zero$ vector.*}
    1.86  
    1.87  lemma linearform_zero [intro??, simp]: 
    1.88 -  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = (#0::real)"; 
    1.89 -proof -; 
    1.90 -  assume "is_vectorspace V" "is_linearform V f";
    1.91 -  have "f 00 = f (00 - 00)"; by (simp!);
    1.92 -  also; have "... = f 00 - f 00"; 
    1.93 -    by (rule linearform_diff) (simp!)+;
    1.94 -  also; have "... = (#0::real)"; by simp;
    1.95 -  finally; show "f 00 = (#0::real)"; .;
    1.96 -qed; 
    1.97 +  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = #0" 
    1.98 +proof - 
    1.99 +  assume "is_vectorspace V" "is_linearform V f"
   1.100 +  have "f 00 = f (00 - 00)" by (simp!)
   1.101 +  also have "... = f 00 - f 00" 
   1.102 +    by (rule linearform_diff) (simp!)+
   1.103 +  also have "... = #0" by simp
   1.104 +  finally show "f 00 = #0" .
   1.105 +qed 
   1.106  
   1.107 -end;
   1.108 \ No newline at end of file
   1.109 +end
   1.110 \ No newline at end of file