src/HOL/Real/HahnBanach/Linearform.thy
 author wenzelm Fri Sep 10 17:28:51 1999 +0200 (1999-09-10) changeset 7535 599d3414b51d child 7566 c5a3f980a7af permissions -rw-r--r--
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);
 wenzelm@7535 ` 1` wenzelm@7535 ` 2` ```theory Linearform = LinearSpace:; ``` wenzelm@7535 ` 3` wenzelm@7535 ` 4` ```section {* linearforms *}; ``` wenzelm@7535 ` 5` wenzelm@7535 ` 6` ```constdefs ``` wenzelm@7535 ` 7` ``` is_linearform :: "['a set, 'a => real] => bool" ``` wenzelm@7535 ` 8` ``` "is_linearform V f == ``` wenzelm@7535 ` 9` ``` (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) & ``` wenzelm@7535 ` 10` ``` (ALL x: V. ALL a. f (a [*] x) = a * (f x))"; ``` wenzelm@7535 ` 11` wenzelm@7535 ` 12` ```lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y; ``` wenzelm@7535 ` 13` ``` !! x c. x : V ==> f (c [*] x) = c * f x |] ``` wenzelm@7535 ` 14` ``` ==> is_linearform V f"; ``` wenzelm@7535 ` 15` ``` by (unfold is_linearform_def, force); ``` wenzelm@7535 ` 16` wenzelm@7535 ` 17` ```lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y"; ``` wenzelm@7535 ` 18` ``` by (unfold is_linearform_def, auto); ``` wenzelm@7535 ` 19` wenzelm@7535 ` 20` ```lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)"; ``` wenzelm@7535 ` 21` ``` by (unfold is_linearform_def, auto); ``` wenzelm@7535 ` 22` wenzelm@7535 ` 23` ```lemma linearform_neg_linear: ``` wenzelm@7535 ` 24` ``` "[| is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x"; ``` wenzelm@7535 ` 25` ```proof -; ``` wenzelm@7535 ` 26` ``` assume "is_linearform V f" "is_vectorspace V" "x:V"; ``` wenzelm@7535 ` 27` ``` have "f ([-] x) = f ((- 1r) [*] x)"; by (asm_simp add: vs_mult_minus_1); ``` wenzelm@7535 ` 28` ``` also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear); ``` wenzelm@7535 ` 29` ``` also; have "... = - (f x)"; by asm_simp; ``` wenzelm@7535 ` 30` ``` finally; show ?thesis; .; ``` wenzelm@7535 ` 31` ```qed; ``` wenzelm@7535 ` 32` wenzelm@7535 ` 33` ```lemma linearform_diff_linear: ``` wenzelm@7535 ` 34` ``` "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y"; ``` wenzelm@7535 ` 35` ```proof -; ``` wenzelm@7535 ` 36` ``` assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"; ``` wenzelm@7535 ` 37` ``` have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def); ``` wenzelm@7535 ` 38` ``` also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+); ``` wenzelm@7535 ` 39` ``` also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear); ``` wenzelm@7535 ` 40` ``` finally; show "f (x [-] y) = f x - f y"; by asm_simp; ``` wenzelm@7535 ` 41` ```qed; ``` wenzelm@7535 ` 42` wenzelm@7535 ` 43` ```lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; ``` wenzelm@7535 ` 44` ```proof -; ``` wenzelm@7535 ` 45` ``` assume "is_vectorspace V" "is_linearform V f"; ``` wenzelm@7535 ` 46` ``` have "f <0> = f (<0> [-] <0>)"; by asm_simp; ``` wenzelm@7535 ` 47` ``` also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+; ``` wenzelm@7535 ` 48` ``` also; have "... = 0r"; by simp; ``` wenzelm@7535 ` 49` ``` finally; show "f <0> = 0r"; .; ``` wenzelm@7535 ` 50` ```qed; ``` wenzelm@7535 ` 51` wenzelm@7535 ` 52` ```end; ``` wenzelm@7535 ` 53`