src/HOL/Real/HahnBanach/Linearform.thy
changeset 8703 816d8f6513be
parent 8203 2fcc6017cb72
child 9013 9dd0274f76af
     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Thu Apr 13 15:01:45 2000 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Apr 13 15:01:50 2000 +0200
     1.3 @@ -14,11 +14,11 @@
     1.4    is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
     1.5    "is_linearform V f == 
     1.6        (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
     1.7 -      (ALL x: V. ALL a. f (a <*> x) = a * (f x))"; 
     1.8 +      (ALL x: V. ALL a. f (a (*) x) = a * (f x))"; 
     1.9  
    1.10  lemma is_linearformI [intro]: 
    1.11    "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
    1.12 -    !! x c. x : V ==> f (c <*> x) = c * f x |]
    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  
    1.17 @@ -27,7 +27,7 @@
    1.18    by (unfold is_linearform_def) fast;
    1.19  
    1.20  lemma linearform_mult [intro??]: 
    1.21 -  "[| is_linearform V f; x:V |] ==>  f (a <*> x) = a * (f x)"; 
    1.22 +  "[| is_linearform V f; x:V |] ==>  f (a (*) x) = a * (f x)"; 
    1.23    by (unfold is_linearform_def) fast;
    1.24  
    1.25  lemma linearform_neg [intro??]:
    1.26 @@ -35,7 +35,7 @@
    1.27    ==> f (- x) = - f x";
    1.28  proof -; 
    1.29    assume "is_linearform V f" "is_vectorspace V" "x:V"; 
    1.30 -  have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
    1.31 +  have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);
    1.32    also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
    1.33    also; have "... = - (f x)"; by (simp!);
    1.34    finally; show ?thesis; .;
    1.35 @@ -56,14 +56,14 @@
    1.36  text{* Every linear form yields $0$ for the $\zero$ vector.*};
    1.37  
    1.38  lemma linearform_zero [intro??, simp]: 
    1.39 -  "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
    1.40 +  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r"; 
    1.41  proof -; 
    1.42    assume "is_vectorspace V" "is_linearform V f";
    1.43 -  have "f <0> = f (<0> - <0>)"; by (simp!);
    1.44 -  also; have "... = f <0> - f <0>"; 
    1.45 +  have "f 00 = f (00 - 00)"; by (simp!);
    1.46 +  also; have "... = f 00 - f 00"; 
    1.47      by (rule linearform_diff) (simp!)+;
    1.48    also; have "... = 0r"; by simp;
    1.49 -  finally; show "f <0> = 0r"; .;
    1.50 +  finally; show "f 00 = 0r"; .;
    1.51  qed; 
    1.52  
    1.53  end;
    1.54 \ No newline at end of file