src/HOL/Real/HahnBanach/Linearform.thy
 changeset 29234 60f7fb56f8cd parent 27612 d3eb431db035
```     1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Sun Dec 14 18:45:51 2008 +0100
1.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Mon Dec 15 18:12:52 2008 +0100
1.3 @@ -1,5 +1,4 @@
1.4  (*  Title:      HOL/Real/HahnBanach/Linearform.thy
1.5 -    ID:         \$Id\$
1.6      Author:     Gertrud Bauer, TU Munich
1.7  *)
1.8
1.9 @@ -14,8 +13,8 @@
1.10    that is additive and multiplicative.
1.11  *}
1.12
1.13 -locale linearform = var V + var f +
1.14 -  constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set"
1.15 +locale linearform =
1.16 +  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
1.17    assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
1.18      and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
1.19
1.20 @@ -25,7 +24,7 @@
1.21    assumes "vectorspace V"
1.22    shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
1.23  proof -
1.24 -  interpret vectorspace [V] by fact
1.25 +  interpret vectorspace V by fact
1.26    assume x: "x \<in> V"
1.27    then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
1.28    also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
1.29 @@ -37,7 +36,7 @@
1.30    assumes "vectorspace V"
1.31    shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
1.32  proof -
1.33 -  interpret vectorspace [V] by fact
1.34 +  interpret vectorspace V by fact
1.35    assume x: "x \<in> V" and y: "y \<in> V"
1.36    then have "x - y = x + - y" by (rule diff_eq1)
1.37    also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
1.38 @@ -51,7 +50,7 @@
1.39    assumes "vectorspace V"
1.40    shows "f 0 = 0"
1.41  proof -
1.42 -  interpret vectorspace [V] by fact
1.43 +  interpret vectorspace V by fact
1.44    have "f 0 = f (0 - 0)" by simp
1.45    also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
1.46    also have "\<dots> = 0" by simp
```