Create a gist now

Instantly share code, notes, and snippets.

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment