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

src/HOL/Real/HahnBanach/Linearform.thy

changeset 7535 | 599d3414b51d |

child 7566 | c5a3f980a7af |

1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Fri Sep 10 17:28:51 1999 +0200 1.3 @@ -0,0 +1,53 @@ 1.4 + 1.5 +theory Linearform = LinearSpace:; 1.6 + 1.7 +section {* linearforms *}; 1.8 + 1.9 +constdefs 1.10 + is_linearform :: "['a set, 'a => real] => bool" 1.11 + "is_linearform V f == 1.12 + (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) & 1.13 + (ALL x: V. ALL a. f (a [*] x) = a * (f x))"; 1.14 + 1.15 +lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y; 1.16 + !! x c. x : V ==> f (c [*] x) = c * f x |] 1.17 + ==> is_linearform V f"; 1.18 + by (unfold is_linearform_def, force); 1.19 + 1.20 +lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y"; 1.21 + by (unfold is_linearform_def, auto); 1.22 + 1.23 +lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)"; 1.24 + by (unfold is_linearform_def, auto); 1.25 + 1.26 +lemma linearform_neg_linear: 1.27 + "[| is_vectorspace V; is_linearform V f; x:V|] ==> 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 (asm_simp add: vs_mult_minus_1); 1.31 + also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear); 1.32 + also; have "... = - (f x)"; by asm_simp; 1.33 + finally; show ?thesis; .; 1.34 +qed; 1.35 + 1.36 +lemma linearform_diff_linear: 1.37 + "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y"; 1.38 +proof -; 1.39 + assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"; 1.40 + have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def); 1.41 + also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+); 1.42 + also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear); 1.43 + finally; show "f (x [-] y) = f x - f y"; by asm_simp; 1.44 +qed; 1.45 + 1.46 +lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 1.47 +proof -; 1.48 + assume "is_vectorspace V" "is_linearform V f"; 1.49 + have "f <0> = f (<0> [-] <0>)"; by asm_simp; 1.50 + also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+; 1.51 + also; have "... = 0r"; by simp; 1.52 + finally; show "f <0> = 0r"; .; 1.53 +qed; 1.54 + 1.55 +end; 1.56 +