-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathideal_colim.casl
57 lines (55 loc) · 1.98 KB
/
ideal_colim.casl
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
logic CASL.SulFOL=
sorts Generic, RingElt, SimplePrime, SubSetOfRing
sorts SimplePrime < Generic; Generic < SubSetOfRing
op 0 : RingElt
op 1 : RingElt
op S : Generic
op __*__ : RingElt * RingElt -> RingElt
op __+__ : RingElt * RingElt -> RingElt
op __x__ : Generic * Generic -> Generic
pred IsIdeal : SubSetOfRing
pred IsPrime : Generic
pred __isIn__ : RingElt * SubSetOfRing
pred gcont : Generic * Generic
pred __generates__ : RingElt * Generic
forall I : SubSetOfRing . I in Generic <=> IsIdeal(I)
forall x : Generic . x x S = x
forall x : Generic . S x x = x
forall A, B : Generic.
gcont(A, B) <=> forall a : RingElt . a isIn A => a isIn B
forall x, y : RingElt . x + y = y + x
forall x, y, z : RingElt . (x + y) + z = x + (y + z)
forall x : RingElt . x + 0 = x /\ 0 + x = x
forall x : RingElt . exists x' : RingElt . x' + x = 0
forall x, y : RingElt . x * y = y * x
forall x, y, z : RingElt . (x * y) * z = x * (y * z)
forall x : RingElt . x * 1 = x /\ 1 * x = x
forall x, y, z : RingElt
. (x + y) * z = (x * z) + (y * z)
forall x, y, z : RingElt
. z * (x + y) = (z * x) + (z * y)
forall I : SubSetOfRing
. IsIdeal(I)
<=> forall a, b, c : RingElt
. ((a isIn I => a isIn S) /\ 0 isIn I)
/\ (a isIn I /\ c isIn S => c * a isIn I)
/\ (a isIn I /\ b isIn I /\
c isIn S /\ b + c = 0 => a + c isIn I)
forall a : RingElt; A : Generic
. a generates A
<=> forall c : RingElt
. c isIn A => exists d : RingElt . c = a * d
forall A, B : Generic; a, b : RingElt
. a isIn A /\ b isIn B => a * b isIn A x B
forall A, B, D : Generic
. (forall a, b : RingElt
. a isIn A /\ b isIn B => a * b isIn D)
=> gcont(A x B, D)
forall x, y : Generic
. gcont(x, y) <=> exists c : Generic . x = y x c
forall p : Generic . p in SimplePrime <=> IsPrime(p)
forall p : Generic
. IsPrime(p)
<=> (forall a, b : Generic
. gcont(a x b, p) => gcont(a, p) \/ gcont(b, p))
/\ not p = S