5 |
5 |
6 header {* Linearforms *} |
6 header {* Linearforms *} |
7 |
7 |
8 theory Linearform = VectorSpace: |
8 theory Linearform = VectorSpace: |
9 |
9 |
10 text{* A \emph{linear form} is a function on a vector |
10 text {* |
11 space into the reals that is additive and multiplicative. *} |
11 A \emph{linear form} is a function on a vector space into the reals |
|
12 that is additive and multiplicative. |
|
13 *} |
12 |
14 |
13 constdefs |
15 constdefs |
14 is_linearform :: "['a::{plus, minus, zero} set, 'a => real] => bool" |
16 is_linearform :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool" |
15 "is_linearform V f == |
17 "is_linearform V f \<equiv> |
16 (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and> |
18 (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and> |
17 (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))" |
19 (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))" |
18 |
20 |
19 lemma is_linearformI [intro]: |
21 lemma is_linearformI [intro]: |
20 "[| !! x y. [| x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y; |
22 "(\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y) \<Longrightarrow> |
21 !! x c. x \<in> V ==> f (c \<cdot> x) = c * f x |] |
23 (\<And>x c. x \<in> V \<Longrightarrow> f (c \<cdot> x) = c * f x) |
22 ==> is_linearform V f" |
24 \<Longrightarrow> is_linearform V f" |
23 by (unfold is_linearform_def) force |
25 by (unfold is_linearform_def) blast |
24 |
26 |
25 lemma linearform_add [intro?]: |
27 lemma linearform_add [intro?]: |
26 "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y" |
28 "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y" |
27 by (unfold is_linearform_def) fast |
29 by (unfold is_linearform_def) blast |
28 |
30 |
29 lemma linearform_mult [intro?]: |
31 lemma linearform_mult [intro?]: |
30 "[| is_linearform V f; x \<in> V |] ==> f (a \<cdot> x) = a * (f x)" |
32 "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * (f x)" |
31 by (unfold is_linearform_def) fast |
33 by (unfold is_linearform_def) blast |
32 |
34 |
33 lemma linearform_neg [intro?]: |
35 lemma linearform_neg [intro?]: |
34 "[| is_vectorspace V; is_linearform V f; x \<in> V|] |
36 "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V |
35 ==> f (- x) = - f x" |
37 \<Longrightarrow> f (- x) = - f x" |
36 proof - |
38 proof - |
37 assume "is_linearform V f" "is_vectorspace V" "x \<in> V" |
39 assume "is_linearform V f" "is_vectorspace V" "x \<in> V" |
38 have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1) |
40 have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1) |
39 also have "... = (- #1) * (f x)" by (rule linearform_mult) |
41 also have "... = (- #1) * (f x)" by (rule linearform_mult) |
40 also have "... = - (f x)" by (simp!) |
42 also have "... = - (f x)" by (simp!) |
41 finally show ?thesis . |
43 finally show ?thesis . |
42 qed |
44 qed |
43 |
45 |
44 lemma linearform_diff [intro?]: |
46 lemma linearform_diff [intro?]: |
45 "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |] |
47 "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V |
46 ==> f (x - y) = f x - f y" |
48 \<Longrightarrow> f (x - y) = f x - f y" |
47 proof - |
49 proof - |
48 assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> V" |
50 assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> V" |
49 have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1) |
51 have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1) |
50 also have "... = f x + f (- y)" |
52 also have "... = f x + f (- y)" |
51 by (rule linearform_add) (simp!)+ |
53 by (rule linearform_add) (simp!)+ |
52 also have "f (- y) = - f y" by (rule linearform_neg) |
54 also have "f (- y) = - f y" by (rule linearform_neg) |
53 finally show "f (x - y) = f x - f y" by (simp!) |
55 finally show "f (x - y) = f x - f y" by (simp!) |
54 qed |
56 qed |
55 |
57 |
56 text{* Every linear form yields $0$ for the $\zero$ vector.*} |
58 text {* Every linear form yields @{text 0} for the @{text 0} vector. *} |
57 |
59 |
58 lemma linearform_zero [intro?, simp]: |
60 lemma linearform_zero [intro?, simp]: |
59 "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0" |
61 "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = #0" |
60 proof - |
62 proof - |
61 assume "is_vectorspace V" "is_linearform V f" |
63 assume "is_vectorspace V" "is_linearform V f" |
62 have "f 0 = f (0 - 0)" by (simp!) |
64 have "f 0 = f (0 - 0)" by (simp!) |
63 also have "... = f 0 - f 0" |
65 also have "... = f 0 - f 0" |
64 by (rule linearform_diff) (simp!)+ |
66 by (rule linearform_diff) (simp!)+ |
65 also have "... = #0" by simp |
67 also have "... = #0" by simp |
66 finally show "f 0 = #0" . |
68 finally show "f 0 = #0" . |
67 qed |
69 qed |
68 |
70 |
69 end |
71 end |