Re: [isabelle] executable multiset-extension
right, that's what I apparently failed to convey ;)
But maybe you, or others know tricks to make code generation work
automagically for each suitable instance?
On Thu, May 5, 2016, 10:36 Florian Haftmann <
florian.haftmann at informatik.tu-muenchen.de> wrote:
> Hi Christian,
> I will take care for this.
> Just one question: since the equation is guarded by preconditions, how
> do you apply it for code generation? By instantiating it to a specific
> relation and generation code for that instance only?
> Am 04.05.2016 um 15:24 schrieb Christian Sternagel:
> > 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.
> > cheers
> > chris
> PGP available:
This archive was generated by a fusion of
Pipermail (Mailman edition) and