Re: [isabelle] nested multiset ordering?
I don't have an answer to your question, but two related remarks.
1) If you deal with nested multisets, a good way to define those is to
use the new datatypes as follows (in Isabelle2014, in the development
version drop the "_new"):
datatype_new 'a nested_multiset = Elem 'a | Nest "'a nested_multiset
You will get many conveniences including induction and primitive
recursion using this representation.
2) Concerning plain (nonnested) multisets: the definition of the
ordering that we have in Isabelle (the one Ramana pointed to in HOL4) is
neither of the classic ones (Dershowitz--Manna, Huet--Oppen). The
equivalences are not hard to prove, but if you happen to need them you
can reuse a proof that we (Jasmin and me) made in an ongoing
formalization of Bachmair and Ganzingers chapter "Resolution Theorem
Proving" in the Handbook of Automated Reasoning:
At some point, much of the linked theory will migrate to
On 28.09.2014 17:19, Lawrence Paulson wrote:
I wonder whether anybody is aware of a formalisation (in any system) of the nested multiset ordering, as described in the classic paper "Proving Termination With Multiset Orderings”?
There is, I believe, a connection with the ordinal epsilon-0.
This archive was generated by a fusion of
Pipermail (Mailman edition) and