ring.als

sig Element {}

one sig Ring{
	elements: set Element,
	zero: one elements,
	un: one elements,
	add: elements -> elements -> one elements,
	mult: elements -> elements -> one elements,
	neg: elements -> one elements
}

fact NoRedundantElements{
	all e: Element | e in Ring.elements
}

fact AddZero{
	all a: Ring.elements | Ring.add [a] [Ring.zero] = a
	all a: Ring.elements | Ring.add [Ring.zero] [a] = a
}

fact AddAssociative{
	all a, b, c: Ring.elements | Ring.add [a] [Ring.add [b] [c]] = Ring.add [Ring.add [a] [b]] [c]
}

fact AddCommutative{
	all a, b: Ring.elements | Ring.add [a] [b] = Ring.add [b] [a]
}

fact Neg{
	all a: Ring.elements | Ring.add [a] [Ring.neg [a]] = Ring.zero
}

fact MultAssociative{
	all a, b, c: Ring.elements | Ring.mult [a] [Ring.mult [b] [c]] = Ring.mult [Ring.mult [a] [b]] [c]
}

// Commutative Ring!
fact MultCommutative{
	all a, b: Ring.elements | Ring.mult [a] [b] = Ring.mult [b] [a]
}

fact MultDistributive{
	all a, b, c: Ring.elements | Ring.mult [a] [Ring.add [b] [c]] = Ring.add [Ring.mult [a] [b]] [Ring.mult [a] [c]]
}

fact MultUn{
	all a: Ring.elements | Ring.mult [a] [Ring.un] = a
}

// run {}

pred isIdeal(i: set Element){
	Ring.zero in i
	all a, b: i | Ring.add [a] [b] in i
	all a:i , c: Ring.elements | Ring.mult [c] [a] in i
}

//run {some i: set Element | isIdeal [i]}

assert main{
	all i: set Element, a: set Element, b: set Element |
	((i in a+b) and
	isIdeal[i] and
	isIdeal[a] and
	isIdeal[b]) implies
	((i in a) or (i in b))
}

//check main for 10 //valid

assert main2{
	all i: set Element, a: set Element, b: set Element, c: set Element |
	((i in a+b+c) and
	isIdeal[i] and
	isIdeal[a] and
	isIdeal[b] and
	isIdeal[c]) implies
	((i in a) or (i in b) or (i in c))
}

check main2 for 8