3 Author: Gertrud Bauer, TU Munich |
3 Author: Gertrud Bauer, TU Munich |
4 *) |
4 *) |
5 |
5 |
6 header {* Linearforms *}; |
6 header {* Linearforms *}; |
7 |
7 |
8 theory Linearform = LinearSpace:; |
8 theory Linearform = VectorSpace:; |
|
9 |
|
10 text{* A \emph{linearform} is a function on a vector |
|
11 space into the reals that is linear w.~r.~t.~addition and skalar |
|
12 multiplikation. *}; |
9 |
13 |
10 constdefs |
14 constdefs |
11 is_linearform :: "['a set, 'a => real] => bool" |
15 is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" |
12 "is_linearform V f == |
16 "is_linearform V f == |
13 (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) & |
17 (ALL x: V. ALL y: V. f (x + y) = f x + f y) & |
14 (ALL x: V. ALL a. f (a [*] x) = a * (f x))"; |
18 (ALL x: V. ALL a. f (a <*> x) = a * (f x))"; |
15 |
19 |
16 lemma is_linearformI [intro]: |
20 lemma is_linearformI [intro]: |
17 "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y; |
21 "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y; |
18 !! x c. x : V ==> f (c [*] x) = c * f x |] |
22 !! x c. x : V ==> f (c <*> x) = c * f x |] |
19 ==> is_linearform V f"; |
23 ==> is_linearform V f"; |
20 by (unfold is_linearform_def) force; |
24 by (unfold is_linearform_def) force; |
21 |
25 |
22 lemma linearform_add_linear [intro!!]: |
26 lemma linearform_add_linear [intro!!]: |
23 "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y"; |
27 "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y"; |
24 by (unfold is_linearform_def) auto; |
28 by (unfold is_linearform_def) fast; |
25 |
29 |
26 lemma linearform_mult_linear [intro!!]: |
30 lemma linearform_mult_linear [intro!!]: |
27 "[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)"; |
31 "[| is_linearform V f; x:V |] ==> f (a <*> x) = a * (f x)"; |
28 by (unfold is_linearform_def) auto; |
32 by (unfold is_linearform_def) fast; |
29 |
33 |
30 lemma linearform_neg_linear [intro!!]: |
34 lemma linearform_neg_linear [intro!!]: |
31 "[| is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x"; |
35 "[| is_vectorspace V; is_linearform V f; x:V|] |
|
36 ==> f (- x) = - f x"; |
32 proof -; |
37 proof -; |
33 assume "is_linearform V f" "is_vectorspace V" "x:V"; |
38 assume "is_linearform V f" "is_vectorspace V" "x:V"; |
34 have "f ([-] x) = f ((- 1r) [*] x)"; by (unfold negate_def) simp; |
39 have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1); |
35 also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear); |
40 also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear); |
36 also; have "... = - (f x)"; by (simp!); |
41 also; have "... = - (f x)"; by (simp!); |
37 finally; show ?thesis; .; |
42 finally; show ?thesis; .; |
38 qed; |
43 qed; |
39 |
44 |
40 lemma linearform_diff_linear [intro!!]: |
45 lemma linearform_diff_linear [intro!!]: |
41 "[| is_vectorspace V; is_linearform V f; x:V; y:V |] |
46 "[| is_vectorspace V; is_linearform V f; x:V; y:V |] |
42 ==> f (x [-] y) = f x - f y"; |
47 ==> f (x - y) = f x - f y"; |
43 proof -; |
48 proof -; |
44 assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"; |
49 assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"; |
45 have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def); |
50 have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1); |
46 also; have "... = f x + f ([-] y)"; |
51 also; have "... = f x + f (- y)"; |
47 by (rule linearform_add_linear) (simp!)+; |
52 by (rule linearform_add_linear) (simp!)+; |
48 also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear); |
53 also; have "f (- y) = - f y"; by (rule linearform_neg_linear); |
49 finally; show "f (x [-] y) = f x - f y"; by (simp!); |
54 finally; show "f (x - y) = f x - f y"; by (simp!); |
50 qed; |
55 qed; |
|
56 |
|
57 text{* Every linearform yields $0$ for the $\zero$ vector.*}; |
51 |
58 |
52 lemma linearform_zero [intro!!, simp]: |
59 lemma linearform_zero [intro!!, simp]: |
53 "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; |
60 "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; |
54 proof -; |
61 proof -; |
55 assume "is_vectorspace V" "is_linearform V f"; |
62 assume "is_vectorspace V" "is_linearform V f"; |
56 have "f <0> = f (<0> [-] <0>)"; by (simp!); |
63 have "f <0> = f (<0> - <0>)"; by (simp!); |
57 also; have "... = f <0> - f <0>"; |
64 also; have "... = f <0> - f <0>"; |
58 by (rule linearform_diff_linear) (simp!)+; |
65 by (rule linearform_diff_linear) (simp!)+; |
59 also; have "... = 0r"; by simp; |
66 also; have "... = 0r"; by simp; |
60 finally; show "f <0> = 0r"; .; |
67 finally; show "f <0> = 0r"; .; |
61 qed; |
68 qed; |