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