-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathprime.pp.tex
104 lines (104 loc) · 7.08 KB
/
prime.pp.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
\begin{hetcasl}
\KW{library} \Id{prime}\\
\\
\KW{logic} \SId{CASL}\\
{\small{}\KW{\%\%}PRIME IDEAS OVER CDR\Ax{-}s AS A BLEND}\\
\\
\SPEC \=\SIdIndex{IdealsOfRing} \Ax{=}\\
\> \SORT \=\Id{RingElt}\\
\>\> {\small{}\KW{\%\%} sort of Ring Elements}\\
\> \SORT \=\Id{SubSetOfRing}\\
\>\> {\small{}\KW{\%\%} sort of parts of this ring}\\
\> \PRED \=\Id{IsIdeal} \Ax{:} \Id{SubSetOfRing}\\
\>\> {\small{}\KW{\%\%} when a subset is an ideal}\\
\> \OP \=\Ax{0} \Ax{:} \Id{RingElt}\\
\> \OP \=\Ax{1} \Ax{:} \Id{RingElt}\\
\> \OP \=\Ax{\_\_}\Ax{*}\Ax{\_\_} \Ax{:} \=\Id{RingElt} \Ax{\times} \Id{RingElt} \Ax{\rightarrow} \Id{RingElt}\\
\> \OP \=\Ax{\_\_}\Ax{+}\Ax{\_\_} \Ax{:} \=\Id{RingElt} \Ax{\times} \Id{RingElt} \Ax{\rightarrow} \Id{RingElt}\\
\> \PRED \=\Ax{\_\_}\Id{isIn}\Ax{\_\_} \Ax{:} \=\Id{RingElt} \Ax{\times} \Id{SubSetOfRing}\\
\> \SORT \=\Id{Ideal} \Ax{=} \=\{\Id{I} \Ax{:} \Id{SubSetOfRing} \Ax{\bullet} \Id{IsIdeal}(\Id{I})\}\\
\> \OP \=\Id{R} \Ax{:} \Id{Ideal}\\
\>\> {\small{}\KW{\%\%} the Ring as an ideal}\\
\> \OP \=\Ax{\_\_}\Ax{**}\Ax{\_\_} \Ax{:} \=\Id{Ideal} \Ax{\times} \Id{Ideal} \Ax{\rightarrow} \Id{Ideal}, \Id{unit} \Id{R}\\
\>\> {\small{}\KW{\%\%}Definition of the predicate of contention}\\
\> \PRED \=\Ax{\_\_}\Id{issubsetOf}\Ax{\_\_} \Ax{:} \=\Id{Ideal} \Ax{\times} \Id{Ideal}\\
\> \Ax{\forall} \=\Id{A}, \Id{B} \Ax{:} \Id{Ideal} \\
\> \Ax{\bullet} \=\Id{A} \Id{issubsetOf} \Id{B} \Ax{\Leftrightarrow} \=\Ax{\forall} \Id{a} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{a} \Id{isIn} \Id{A} \Ax{\Rightarrow} \=\Id{a} \Id{isIn} \Id{B}\\
\> \\
\> {\small{}\KW{\%\%} axiomatization of a commutative Ring with unity}\\
\> \Ax{\forall} \Id{x} \Ax{:} \Id{RingElt}; \=\Id{y} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{x} \Ax{+} \Id{y} \Ax{=} \=\Id{y} \Ax{+} \Id{x}\\
\> \Ax{\forall} \Id{x} \Ax{:} \Id{RingElt}; \Id{y} \Ax{:} \Id{RingElt}; \=\Id{z} \Ax{:} \Id{RingElt} \\
\> \Ax{\bullet} \=(\=\Id{x} \Ax{+} \Id{y}) \Ax{+} \Id{z} \Ax{=} \=\Id{x} \Ax{+} (\=\Id{y} \Ax{+} \Id{z})\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{x} \Ax{+} \Ax{0} \Ax{=} \Id{x} \Ax{\wedge} \=\Ax{0} \Ax{+} \Id{x} \Ax{=} \Id{x}\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Ax{\exists} \Id{x'} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{x'} \Ax{+} \Id{x} \Ax{=} \Ax{0}\\
\> \Ax{\forall} \Id{x} \Ax{:} \Id{RingElt}; \=\Id{y} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{x} \Ax{*} \Id{y} \Ax{=} \=\Id{y} \Ax{*} \Id{x}\\
\> \Ax{\forall} \Id{x} \Ax{:} \Id{RingElt}; \Id{y} \Ax{:} \Id{RingElt}; \=\Id{z} \Ax{:} \Id{RingElt} \Ax{\bullet} \=(\=\Id{x} \Ax{*} \Id{y}) \Ax{*} \Id{z} \Ax{=} \=\Id{x} \Ax{*} (\=\Id{y} \Ax{*} \Id{z})\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{x} \Ax{*} \Ax{1} \Ax{=} \Id{x} \Ax{\wedge} \=\Ax{1} \Ax{*} \Id{x} \Ax{=} \Id{x}\\
\> \Ax{\forall} \=\Id{x}, \Id{y}, \Id{z} \Ax{:} \Id{RingElt} \Ax{\bullet} \=(\=\Id{x} \Ax{+} \Id{y}) \Ax{*} \Id{z} \Ax{=} \=(\=\Id{x} \Ax{*} \Id{z}) \Ax{+} (\=\Id{y} \Ax{*} \Id{z})\\
\> \Ax{\forall} \=\Id{x}, \Id{y}, \Id{z} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{z} \Ax{*} (\=\Id{x} \Ax{+} \Id{y}) \Ax{=} \=(\=\Id{z} \Ax{*} \Id{x}) \Ax{+} (\=\Id{z} \Ax{*} \Id{y})\\
\> \\
\> {\small{}\KW{\%\%}axioms for Ideal}\\
\> \Ax{\forall} \=\Id{I} \Ax{:} \Id{SubSetOfRing} \\
\> \Ax{\bullet} \=\Id{IsIdeal}(\Id{I}) \\
\>\> \Ax{\Leftrightarrow} \=\Ax{\forall} \Id{a}, \Id{b}, \Id{c} \Ax{:} \Id{RingElt} \\
\>\>\> \Ax{\bullet} \=(\=(\=\Id{a} \Id{isIn} \Id{I} \Ax{\Rightarrow} \=\Id{a} \Id{isIn} \Id{R}) \Ax{\wedge} \=\Ax{0} \Id{isIn} \Id{I}) \\
\>\>\>\> \Ax{\wedge} (\=\Id{a} \Id{isIn} \Id{I} \Ax{\wedge} \=\Id{c} \Id{isIn} \Id{R} \Ax{\Rightarrow} \=\Id{c} \Ax{*} \Id{a} \Id{isIn} \Id{I}) \\
\>\>\>\> \Ax{\wedge} (\=\Id{a} \Id{isIn} \Id{I} \Ax{\wedge} \=\Id{b} \Id{isIn} \Id{I} \Ax{\wedge} \=\Id{c} \Id{isIn} \Id{R} \Ax{\wedge} \=\Id{b} \Ax{+} \Id{c} \Ax{=} \Ax{0} \\
\>\>\>\>\> \Ax{\Rightarrow} \=\Id{a} \Ax{+} \Id{c} \Id{isIn} \Id{I})\\
\> \\
\> {\small{}\KW{\%\%} Definition of the product of ideals without subindexes}\\
\> \Ax{\forall} \=\Id{A}, \Id{B} \Ax{:} \Id{Ideal} \\
\> \Ax{\bullet} \=\Ax{\forall} \Id{a}, \Id{b} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{a} \Id{isIn} \Id{A} \Ax{\wedge} \=\Id{b} \Id{isIn} \Id{B} \Ax{\Rightarrow} \=\Id{a} \Ax{*} \Id{b} \Id{isIn} \=\Id{A} \Ax{**} \Id{B}\\
\> \Ax{\bullet} \=\Ax{\forall} \Id{D} \Ax{:} \Id{Ideal} \\
\>\> \Ax{\bullet} \=(\=\Ax{\forall} \Id{a}, \Id{b} \Ax{:} \Id{RingElt} \Ax{\bullet} \=\Id{a} \Id{isIn} \Id{A} \Ax{\wedge} \=\Id{b} \Id{isIn} \Id{B} \Ax{\Rightarrow} \=\Id{a} \Ax{*} \Id{b} \Id{isIn} \Id{D}) \\
\>\>\> \Ax{\Rightarrow} \=\Id{A} \Ax{**} \Id{B} \Id{issubsetOf} \Id{D}\\
\KW{end}\\
\\
\\
{\small{}\KW{\%\%}\Ax{\%}axioms defining a very simple version of the integers\Ax{,}}\\
{\small{}\KW{\%\%}\Ax{\%}considered with an operation \Ax{*} with neutral element\Ax{,}}\\
{\small{}\KW{\%\%}\Ax{\%} a binary relation \Ax{|}\Ax{|} \Ax{(}upside\Ax{-}down divisibility relation\Ax{)}}\\
{\small{}\KW{\%\%}\Ax{\%} and a primality axiom\Ax{.}}\\
\SPEC \=\SIdIndex{SimpleInt} \Ax{=}\\
\> \SORT \Id{SimpleElem}\\
\> \OPS \=\Ax{1} \Ax{:} \Id{SimpleElem};\\
\>\> \Ax{\_\_}\Id{x}\Ax{\_\_} \Ax{:} \=\Id{SimpleElem} \Ax{\times} \Id{SimpleElem} \Ax{\rightarrow} \Id{SimpleElem}, \\
\>\> \Id{unit} \Ax{1}\\
\> \PREDS \=\Ax{\_\_}\Ax{||}\Ax{\_\_} \Ax{:} \=\Id{SimpleElem} \Ax{\times} \Id{SimpleElem};\\
\>\> \Id{IsPrime} \Ax{:} \Id{SimpleElem}\\
\>\> {\small{}\KW{\%}\KW{Def\_upsidedownDivisilityRelation}\Ax{\%}}\\
\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{SimpleElem} \Ax{\bullet} \=\Id{x} \Ax{||} \Id{y} \Ax{\Leftrightarrow} \=\Ax{\exists} \Id{c} \Ax{:} \Id{SimpleElem} \Ax{\bullet} \=\Id{x} \Ax{=} \=\Id{y} \Id{x} \Id{c}\\
\> \\
\> {\small{}\KW{\%\%} subsort of primes}\\
\> \SORT \=\Id{SimplePrime} \Ax{=} \=\{\Id{p} \Ax{:} \Id{SimpleElem} \Ax{\bullet} \Id{IsPrime}(\Id{p})\}\\
\> \Ax{\forall} \=\Id{p} \Ax{:} \Id{SimpleElem} \\
\> \Ax{\bullet} \=\Id{IsPrime}(\Id{p}) \\
\>\> \Ax{\Leftrightarrow} \=(\=\Ax{\forall} \Id{a}, \Id{b} \Ax{:} \Id{SimpleElem} \Ax{\bullet} \=\Id{a} \Id{x} \Id{b} \Ax{||} \Id{p} \Ax{\Rightarrow} \=\Id{a} \Ax{||} \Id{p} \Ax{\vee} \=\Id{b} \Ax{||} \Id{p}) \Ax{\wedge} \Ax{\neg} \=\Id{p} \Ax{=} \Ax{1}\\
\> {\small{}\KW{\%}\KW{Def\_primality}\Ax{\%}}\\
\KW{end}\\
\\
\\
{\small{}\KW{\%\%}\Ax{\%} Generic space}\\
\SPEC \=\SIdIndex{Gen} \Ax{=}\\
\> \SORT \Id{Generic}\\
\> \OPS \=\Id{S} \Ax{:} \Id{Generic};\\
\>\> \Ax{\_\_}\Id{gpr}\Ax{\_\_} \Ax{:} \=\Id{Generic} \Ax{\times} \Id{Generic} \Ax{\rightarrow} \Id{Generic}, \Id{unit} \Id{S}\\
\> \PRED \=\Id{gcont} \Ax{:} \=\Id{Generic} \Ax{\times} \Id{Generic}\\
\KW{end}\\
\\
\VIEW \=\SId{I1} \Ax{:} \\
\> \SId{Gen} \KW{to} \SId{IdealsOfRing} \Ax{=} \\
\> \Id{Generic} \Ax{\mapsto} \Id{Ideal}, \Id{S} \Ax{\mapsto} \Id{R}, \Ax{\_\_}\Id{gpr}\Ax{\_\_} \Ax{\mapsto} \=\Ax{\_\_}\Ax{**}\Ax{\_\_}, \\
\> \Id{gcont} \Ax{\mapsto} \=\Ax{\_\_}\Id{issubsetOf}\Ax{\_\_}\\
\KW{end}\\
\\
\VIEW \=\SId{I2} \Ax{:} \\
\> \SId{Gen} \KW{to} \SId{SimpleInt} \Ax{=} \\
\> \Id{Generic} \Ax{\mapsto} \Id{SimpleElem}, \Id{S} \Ax{\mapsto} \Ax{1}, \Ax{\_\_}\Id{gpr}\Ax{\_\_} \Ax{\mapsto} \=\Ax{\_\_}\Id{x}\Ax{\_\_}, \\
\> \Id{gcont} \Ax{\mapsto} \=\Ax{\_\_}\Ax{||}\Ax{\_\_}\\
\KW{end}\\
\\
\SPEC \=\SIdIndex{Colimit} \Ax{=}\\
\> \KW{combine} \=\Id{I1}, \Id{I2}\\
\KW{end}
\end{hetcasl}