[isabelle] executable multiset-extension

Dear list,

as far as I can tell "mult" from "~~/src/HOL/Library/Multiset" does not
support code generation at the moment.

So maybe the attached theory (which I extracted from recent work on
IsaFoR) is of general interest.

Summary: The main (but not new, and maybe obvious) observation is that
we may always drop the common part of two multisets that should be
compared (I got the idea to use the converse of a finite well-founded
relation in the main induction proof by Vincent van Oostrom). Now, when
checking whether "(N, M) : mult r", instead of guessing an arbitrary
decomposition "M = I + A" and "N = I + B" such that "ALL b :# B. EX a :#
A. (b, a) : r" (which currently does not support code generation and
would lead to a worst-case exponential implementation), we may always
choose "A = M - M #Int N" and "B = N - M #Int N" (which supports code
generation and yields a worst-case quadratic implementation).

However, since the equivalence between my implementation and "mult r"
basically requires "r" to be irreflexive and transitive, we only obtain
executable code for specific "r" (or rather its predicate variant; see
the attached file) satisfying these requirements.



Attachment: Executable_Multiset_Extension.thy
Description: application/extension-thy

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