diff -r 60c795d6bd9e -r c186279eecea src/HOL/Real/HahnBanach/Linearform.thy --- a/src/HOL/Real/HahnBanach/Linearform.thy Sat Dec 16 21:41:14 2000 +0100 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Sat Dec 16 21:41:51 2000 +0100 @@ -7,63 +7,65 @@ theory Linearform = VectorSpace: -text{* A \emph{linear form} is a function on a vector -space into the reals that is additive and multiplicative. *} +text {* + A \emph{linear form} is a function on a vector space into the reals + that is additive and multiplicative. +*} constdefs - is_linearform :: "['a::{plus, minus, zero} set, 'a => real] => bool" - "is_linearform V f == + is_linearform :: "'a::{plus, minus, zero} set \ ('a \ real) \ bool" + "is_linearform V f \ (\x \ V. \y \ V. f (x + y) = f x + f y) \ - (\x \ V. \a. f (a \ x) = a * (f x))" + (\x \ V. \a. f (a \ x) = a * (f x))" -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 +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) blast -lemma linearform_add [intro?]: - "[| is_linearform V f; x \ V; y \ V |] ==> f (x + y) = f x + f y" - by (unfold is_linearform_def) fast +lemma linearform_add [intro?]: + "is_linearform V f \ x \ V \ y \ V \ f (x + y) = f x + f y" + by (unfold is_linearform_def) blast -lemma linearform_mult [intro?]: - "[| is_linearform V f; x \ V |] ==> f (a \ x) = a * (f x)" - by (unfold is_linearform_def) fast +lemma linearform_mult [intro?]: + "is_linearform V f \ x \ V \ f (a \ x) = a * (f x)" + by (unfold is_linearform_def) blast lemma linearform_neg [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" + "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 ((- #1) \ x)" by (simp! add: negate_eq1) also have "... = (- #1) * (f x)" by (rule linearform_mult) also have "... = - (f x)" by (simp!) finally show ?thesis . qed -lemma linearform_diff [intro?]: - "[| is_vectorspace V; is_linearform V f; x \ V; y \ V |] - ==> f (x - y) = f x - f y" +lemma linearform_diff [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" + assume "is_vectorspace V" "is_linearform V f" "x \ V" "y \ V" have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1) - also have "... = f x + f (- y)" + also have "... = f x + f (- y)" by (rule linearform_add) (simp!)+ also have "f (- y) = - f y" by (rule linearform_neg) finally show "f (x - y) = f x - f y" by (simp!) qed -text{* Every linear form yields $0$ for the $\zero$ vector.*} +text {* Every linear form yields @{text 0} for the @{text 0} vector. *} -lemma linearform_zero [intro?, simp]: - "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0" -proof - - assume "is_vectorspace V" "is_linearform V f" +lemma linearform_zero [intro?, simp]: + "is_vectorspace V \ is_linearform V f \ f 0 = #0" +proof - + assume "is_vectorspace V" "is_linearform V f" have "f 0 = f (0 - 0)" by (simp!) - also have "... = f 0 - f 0" + also have "... = f 0 - f 0" by (rule linearform_diff) (simp!)+ also have "... = #0" by simp finally show "f 0 = #0" . -qed +qed -end \ No newline at end of file +end