src/HOL/Hahn_Banach/Linearform.thy
 author wenzelm Sat Nov 04 15:24:40 2017 +0100 (20 months ago) changeset 67003 49850a679c2c parent 61540 f92bf6674699 permissions -rw-r--r--
more robust sorted_entries;
```     1 (*  Title:      HOL/Hahn_Banach/Linearform.thy
```
```     2     Author:     Gertrud Bauer, TU Munich
```
```     3 *)
```
```     4
```
```     5 section \<open>Linearforms\<close>
```
```     6
```
```     7 theory Linearform
```
```     8 imports Vector_Space
```
```     9 begin
```
```    10
```
```    11 text \<open>
```
```    12   A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
```
```    13   additive and multiplicative.
```
```    14 \<close>
```
```    15
```
```    16 locale linearform =
```
```    17   fixes V :: "'a::{minus, plus, zero, uminus} set" and f
```
```    18   assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
```
```    19     and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
```
```    20
```
```    21 declare linearform.intro [intro?]
```
```    22
```
```    23 lemma (in linearform) neg [iff]:
```
```    24   assumes "vectorspace V"
```
```    25   shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
```
```    26 proof -
```
```    27   interpret vectorspace V by fact
```
```    28   assume x: "x \<in> V"
```
```    29   then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
```
```    30   also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
```
```    31   also from x have "\<dots> = - (f x)" by simp
```
```    32   finally show ?thesis .
```
```    33 qed
```
```    34
```
```    35 lemma (in linearform) diff [iff]:
```
```    36   assumes "vectorspace V"
```
```    37   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
```
```    38 proof -
```
```    39   interpret vectorspace V by fact
```
```    40   assume x: "x \<in> V" and y: "y \<in> V"
```
```    41   then have "x - y = x + - y" by (rule diff_eq1)
```
```    42   also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
```
```    43   also have "f (- y) = - f y" using \<open>vectorspace V\<close> y by (rule neg)
```
```    44   finally show ?thesis by simp
```
```    45 qed
```
```    46
```
```    47 text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close>
```
```    48
```
```    49 lemma (in linearform) zero [iff]:
```
```    50   assumes "vectorspace V"
```
```    51   shows "f 0 = 0"
```
```    52 proof -
```
```    53   interpret vectorspace V by fact
```
```    54   have "f 0 = f (0 - 0)" by simp
```
```    55   also have "\<dots> = f 0 - f 0" using \<open>vectorspace V\<close> by (rule diff) simp_all
```
```    56   also have "\<dots> = 0" by simp
```
```    57   finally show ?thesis .
```
```    58 qed
```
```    59
```
```    60 end
```