Re: [isabelle] nested multiset ordering?



Hi Larry,

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 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: https://bitbucket.org/jasmin_blanchette/superformal/src/tip/thys/Multiset_More.thy. At some point, much of the linked theory will migrate to src/HOL/Library/Multiset.

Dmitriy

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”?

http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.145.8728

There is, I believe, a connection with the ordinal epsilon-0.

Larry Paulson








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.