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;
 wenzelm@31795 ` 1` ```(* Title: HOL/Hahn_Banach/Linearform.thy ``` wenzelm@7566 ` 2` ``` Author: Gertrud Bauer, TU Munich ``` wenzelm@7566 ` 3` ```*) ``` wenzelm@7535 ` 4` wenzelm@58889 ` 5` ```section \Linearforms\ ``` wenzelm@7535 ` 6` wenzelm@27612 ` 7` ```theory Linearform ``` wenzelm@31795 ` 8` ```imports Vector_Space ``` wenzelm@27612 ` 9` ```begin ``` wenzelm@7917 ` 10` wenzelm@58744 ` 11` ```text \ ``` wenzelm@61540 ` 12` ``` A \<^emph>\linear form\ is a function on a vector space into the reals that is ``` wenzelm@61540 ` 13` ``` additive and multiplicative. ``` wenzelm@58744 ` 14` ```\ ``` wenzelm@7535 ` 15` ballarin@29234 ` 16` ```locale linearform = ``` wenzelm@61076 ` 17` ``` fixes V :: "'a::{minus, plus, zero, uminus} set" and f ``` wenzelm@13515 ` 18` ``` assumes add [iff]: "x \ V \ y \ V \ f (x + y) = f x + f y" ``` wenzelm@13515 ` 19` ``` and mult [iff]: "x \ V \ f (a \ x) = a * f x" ``` wenzelm@7535 ` 20` ballarin@14254 ` 21` ```declare linearform.intro [intro?] ``` ballarin@14254 ` 22` wenzelm@13547 ` 23` ```lemma (in linearform) neg [iff]: ``` ballarin@27611 ` 24` ``` assumes "vectorspace V" ``` wenzelm@13547 ` 25` ``` shows "x \ V \ f (- x) = - f x" ``` wenzelm@10687 ` 26` ```proof - ``` ballarin@29234 ` 27` ``` interpret vectorspace V by fact ``` wenzelm@13515 ` 28` ``` assume x: "x \ V" ``` wenzelm@27612 ` 29` ``` then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1) ``` wenzelm@27612 ` 30` ``` also from x have "\ = (- 1) * (f x)" by (rule mult) ``` wenzelm@27612 ` 31` ``` also from x have "\ = - (f x)" by simp ``` wenzelm@9035 ` 32` ``` finally show ?thesis . ``` wenzelm@9035 ` 33` ```qed ``` wenzelm@7535 ` 34` wenzelm@13547 ` 35` ```lemma (in linearform) diff [iff]: ``` ballarin@27611 ` 36` ``` assumes "vectorspace V" ``` wenzelm@13547 ` 37` ``` shows "x \ V \ y \ V \ f (x - y) = f x - f y" ``` wenzelm@9035 ` 38` ```proof - ``` ballarin@29234 ` 39` ``` interpret vectorspace V by fact ``` wenzelm@13515 ` 40` ``` assume x: "x \ V" and y: "y \ V" ``` wenzelm@27612 ` 41` ``` then have "x - y = x + - y" by (rule diff_eq1) ``` wenzelm@27612 ` 42` ``` also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y) ``` wenzelm@58744 ` 43` ``` also have "f (- y) = - f y" using \vectorspace V\ y by (rule neg) ``` wenzelm@13515 ` 44` ``` finally show ?thesis by simp ``` wenzelm@9035 ` 45` ```qed ``` wenzelm@7535 ` 46` wenzelm@61539 ` 47` ```text \Every linear form yields \0\ for the \0\ vector.\ ``` wenzelm@7917 ` 48` wenzelm@13547 ` 49` ```lemma (in linearform) zero [iff]: ``` ballarin@27611 ` 50` ``` assumes "vectorspace V" ``` wenzelm@13547 ` 51` ``` shows "f 0 = 0" ``` wenzelm@10687 ` 52` ```proof - ``` ballarin@29234 ` 53` ``` interpret vectorspace V by fact ``` wenzelm@13515 ` 54` ``` have "f 0 = f (0 - 0)" by simp ``` wenzelm@58744 ` 55` ``` also have "\ = f 0 - f 0" using \vectorspace V\ by (rule diff) simp_all ``` wenzelm@13515 ` 56` ``` also have "\ = 0" by simp ``` wenzelm@13515 ` 57` ``` finally show ?thesis . ``` wenzelm@10687 ` 58` ```qed ``` wenzelm@7535 ` 59` wenzelm@10687 ` 60` ```end ```