summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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