summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Real/HahnBanach/Linearform.thy

changeset 7566 | c5a3f980a7af |

parent 7535 | 599d3414b51d |

child 7656 | 2f18c0ffc348 |

--- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Sep 21 17:30:55 1999 +0200 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Sep 21 17:31:20 1999 +0200 @@ -1,3 +1,7 @@ +(* Title: HOL/Real/HahnBanach/Linearform.thy + ID: $Id$ + Author: Gertrud Bauer, TU Munich +*) theory Linearform = LinearSpace:; @@ -12,39 +16,41 @@ lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y; !! x c. x : V ==> f (c [*] x) = c * f x |] ==> is_linearform V f"; - by (unfold is_linearform_def, force); + by (unfold is_linearform_def) force; -lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y"; - by (unfold is_linearform_def, auto); +lemma linearform_add_linear [intro!!]: + "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y"; + by (unfold is_linearform_def) auto; -lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)"; - by (unfold is_linearform_def, auto); +lemma linearform_mult_linear [intro!!]: + "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)"; + by (unfold is_linearform_def) auto; -lemma linearform_neg_linear: +lemma linearform_neg_linear [intro!!]: "[| is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x"; proof -; assume "is_linearform V f" "is_vectorspace V" "x:V"; - have "f ([-] x) = f ((- 1r) [*] x)"; by (asm_simp add: vs_mult_minus_1); + have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1); also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear); - also; have "... = - (f x)"; by asm_simp; + also; have "... = - (f x)"; by (simp!); finally; show ?thesis; .; qed; -lemma linearform_diff_linear: +lemma linearform_diff_linear [intro!!]: "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y"; proof -; assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"; have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def); - also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+); + also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+; also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear); - finally; show "f (x [-] y) = f x - f y"; by asm_simp; + finally; show "f (x [-] y) = f x - f y"; by (simp!); qed; -lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; +lemma linearform_zero [intro!!]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; proof -; assume "is_vectorspace V" "is_linearform V f"; - have "f <0> = f (<0> [-] <0>)"; by asm_simp; - also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+; + have "f <0> = f (<0> [-] <0>)"; by (simp!); + also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+; also; have "... = 0r"; by simp; finally; show "f <0> = 0r"; .; qed;