2020-04-07 13:35:47 (GMT)
In my formalization of superposition, I originally formalized literals as:
datatype literal = Lit (polarity: bool) (left: ‹term›) (right: ‹term›)
and I handled the symmetry of literals wherever needed (for example in the definition of rules). However I ran into some trouble in a couple of proofs where I had to reason about equivalent clauses. Therefore I'm now leaning towards a definition of literals as true unordered pairs:
typedef eql = ‹{E :: term multiset. size E = 2}›
datatype literal = Lit (polarity: bool) (eq: ‹eql›)
but typedefs can be a burden in proofs. Is there another way to define literals in a way that ensures equality of symmetric literals?
2020-04-07 13:43:12 (GMT)
In Isabelle, any custom type is a typedef ultimately. But if you used "quotient_type" instead, you'd surely end up with more convenient reasoning principles.
2020-04-07 13:44:1 (GMT)
In fact, unordered pairs are one of the two examples I use to show quotients in Lean.
2020-04-07 13:45:0 (GMT)
2020-04-07 13:45:32 (GMT)
Also, instead of a multiset of size 2, you can take a set of cardinality 1 or 2.
2020-04-07 13:45:38 (GMT)
Cardinality 1 means same element twice.
2020-04-07 13:45:52 (GMT)
Isn't there a type of unordered pairs in Isabelle?
2020-04-07 13:45:58 (GMT)
That's how unordered pairs are normally defined in maths.
2020-04-07 13:46:5 (GMT)
I'm not aware of any.
2020-04-07 13:46:13 (GMT)
(Answering Alex.)
2020-04-07 13:46:50 (GMT)
Okay, I'll try a quotient type and see if it's more convenient
2020-04-07 13:46:54 (GMT)
thanks
2020-04-07 13:47:15 (GMT)
But my recommendation would be to defined "unordered_pair" as its own thing, with that name.
2020-04-07 13:47:30 (GMT)
It's a general concept and somebody should define it some day.
2020-04-07 13:47:57 (GMT)
BTW I just grepped "unordered pair": 3 (irrelevant) hits in Isabelle, 0 hits in AFP.
2020-04-07 13:49:9 (GMT)
With underscores it gives more spurious hits. Nothing. Amazing.
2020-04-07 13:53:5 (GMT)
2020-04-07 13:58:40 (GMT)
that should do it!
2020-04-07 14:15:20 (GMT)
Argh, I should have searched case insensitively. Dammit. ;)