Skip to content

Instantly share code, notes, and snippets.

@ashiato45 ashiato45/ring.als
Created Feb 19, 2017

Embed
What would you like to do?
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
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.