algebra.why 1.47 KB
Newer Older
1
2
3

theory Assoc
  type t
4
  logic op t t : t
5
  axiom Assoc : forall x y z : t. op (op x y) z = op x (op y z)
6
7
8
9
end

theory Comm
  type t
10
  logic op t t : t
11
  axiom Comm : forall x y : t. op x y = op y x
12
13
14
15
end

theory AC
  type t
16
  logic op t t : t
17
18
19
20
21
22
23
24
25
  clone Assoc with type t = t, logic op = op
  clone Comm  with type t = t, logic op = op
end

theory Group
  type t
       
  logic unit : t
       
26
27
  logic op t t : t
  logic inv t : t
28
       
29
  axiom Unit_def : forall x:t. op x unit = x
30
31
32

  clone Assoc with type t = t, logic op = op

33
  axiom Inv_def : forall x:t. op x (inv x) = unit
34
35
36
37
38
39
40
41
42
43
end

theory CommutativeGroup
  clone export Group
  clone Comm with type t = t, logic op = op
end

theory Ring
  type t
  logic zero : t
44
45
46
  logic (+) t t : t
  logic (-_) t : t
  logic (*) t t : t
47
48
49
50
51
52
53
54

  clone CommutativeGroup with type t = t,
                              logic unit = zero,
                              logic op = (+),
                              logic inv = (-_)

  clone Assoc with type t = t, logic op = (*)

55
  axiom Mul_distr: forall x y z : t. x * (y + z) = x * y + x * z
56

57
  logic (-) (x y : t) : t = x + -y
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
end

theory CommutativeRing
  clone export Ring
  clone Comm with type t = t, logic op = (*)
end

theory UnitaryCommutativeRing
  clone export CommutativeRing
  logic one : t
  axiom Unitary : forall x:t. one * x = x
end

theory Field
  clone export UnitaryCommutativeRing 
73
  logic inv t : t
74
  axiom Inverse : forall x:t. x <> zero -> x * inv x = one
75
  logic (/) (x y : t) : t = x * inv y
76
end