Email Gateway (Aug 19 2022 at 15:57): Email Gateway (Aug 19 2022 at 15:57):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 15:57):From: Ramana Kumar <rk436@cam.ac.uk>
I've only glanced at the paper briefly, so I'm probably wrong, but the
multi-set ordering in HOL4 (
https://github.com/HOL-Theorem-Prover/HOL/blob/master/src/bag/bagScript.sml#L2224)
looks similar. Then again, the comment there says it was "taken from [an]
Isabelle development", so is probably something you have seen before. In
particular, perhaps it doesn't cover the nested version you asked for.
Email Gateway (Aug 19 2022 at 15:57):From: Dmitriy Traytel <traytel@in.tum.de>
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
Last updated: Apr 19 2024 at 08:19 UTC