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

src/HOL/Real/HahnBanach/Linearform.thy

changeset 27611 | 2c01c0bdb385 |

parent 25762 | c03e9d04b3e4 |

child 27612 | d3eb431db035 |

1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:02:10 2008 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy Tue Jul 15 16:50:09 2008 +0200 1.3 @@ -20,9 +20,10 @@ 1.4 declare linearform.intro [intro?] 1.5 1.6 lemma (in linearform) neg [iff]: 1.7 - includes vectorspace 1.8 + assumes "vectorspace V" 1.9 shows "x \<in> V \<Longrightarrow> f (- x) = - f x" 1.10 proof - 1.11 + interpret vectorspace [V] by fact 1.12 assume x: "x \<in> V" 1.13 hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1) 1.14 also from x have "... = (- 1) * (f x)" by (rule mult) 1.15 @@ -31,9 +32,10 @@ 1.16 qed 1.17 1.18 lemma (in linearform) diff [iff]: 1.19 - includes vectorspace 1.20 + assumes "vectorspace V" 1.21 shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y" 1.22 proof - 1.23 + interpret vectorspace [V] by fact 1.24 assume x: "x \<in> V" and y: "y \<in> V" 1.25 hence "x - y = x + - y" by (rule diff_eq1) 1.26 also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y) 1.27 @@ -44,9 +46,10 @@ 1.28 text {* Every linear form yields @{text 0} for the @{text 0} vector. *} 1.29 1.30 lemma (in linearform) zero [iff]: 1.31 - includes vectorspace 1.32 + assumes "vectorspace V" 1.33 shows "f 0 = 0" 1.34 proof - 1.35 + interpret vectorspace [V] by fact 1.36 have "f 0 = f (0 - 0)" by simp 1.37 also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all 1.38 also have "\<dots> = 0" by simp