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