equal
deleted
inserted
replaced
7 |
7 |
8 theory VectorSpace = Bounds + Aux:; |
8 theory VectorSpace = Bounds + Aux:; |
9 |
9 |
10 subsection {* Signature *}; |
10 subsection {* Signature *}; |
11 |
11 |
12 text {* For the definition of real vector spaces a type $\alpha$ is |
12 text {* For the definition of real vector spaces a type $\alpha$ |
13 considered, on which the operations addition and real scalar |
13 of the sort $\idt{plus}, \idt{minus}$ is considered, on which a |
14 multiplication are defined, and which has an zero element.*}; |
14 real scalar multiplication $\mult$ is defined, and which has an zero |
|
15 element $\zero$.*}; |
15 |
16 |
16 consts |
17 consts |
17 (*** |
18 (*** |
18 sum :: "['a, 'a] => 'a" (infixl "+" 65) |
19 sum :: "['a, 'a] => 'a" (infixl "+" 65) |
19 ***) |
20 ***) |
22 |
23 |
23 syntax (symbols) |
24 syntax (symbols) |
24 prod :: "[real, 'a] => 'a" (infixr "\<prod>" 70) |
25 prod :: "[real, 'a] => 'a" (infixr "\<prod>" 70) |
25 zero :: 'a ("\<zero>"); |
26 zero :: 'a ("\<zero>"); |
26 |
27 |
27 text {* The unary and binary minus can be considered as |
28 (* text {* The unary and binary minus can be considered as |
28 abbreviations: *}; |
29 abbreviations: *}; |
|
30 *) |
29 |
31 |
30 (*** |
32 (*** |
31 constdefs |
33 constdefs |
32 negate :: "'a => 'a" ("- _" [100] 100) |
34 negate :: "'a => 'a" ("- _" [100] 100) |
33 "- x == (- 1r) <*> x" |
35 "- x == (- 1r) <*> x" |
35 "x - y == x + - y"; |
37 "x - y == x + - y"; |
36 ***) |
38 ***) |
37 |
39 |
38 subsection {* Vector space laws *}; |
40 subsection {* Vector space laws *}; |
39 |
41 |
40 text {* A \emph{vector space} is a non-empty set $V$ of elements |
42 text {* A \emph{vector space} is a non-empty set $V$ of elements from |
41 from $\alpha$ with the following vector space laws: |
43 $\alpha$ with the following vector space laws: The set $V$ is closed |
42 The set $V$ is closed under addition and scalar multiplication, |
44 under addition and scalar multiplication, addition is associative |
43 addition is associative and commutative. $\minus x$ is the inverse |
45 and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition |
44 of $x$ w.~r.~t.~addition and $\zero$ is the neutral element of |
46 and $\zero$ is the neutral element of addition. Addition and |
45 addition. |
47 multiplication are distributive; scalar multiplication is |
46 Addition and multiplication are distributive. |
48 associative and the real $1$ is the neutral element of scalar |
47 Scalar multiplication is associative and the real $1$ is the neutral |
49 multiplication. |
48 element of scalar multiplication. |
|
49 *}; |
50 *}; |
50 |
51 |
51 constdefs |
52 constdefs |
52 is_vectorspace :: "('a::{plus,minus}) set => bool" |
53 is_vectorspace :: "('a::{plus,minus}) set => bool" |
53 "is_vectorspace V == V ~= {} |
54 "is_vectorspace V == V ~= {} |