# Re: [isabelle] executable multiset-extension

```See now

http://isabelle.in.tum.de/repos/isabelle/rev/f2177f5d2aed
http://isabelle.in.tum.de/repos/isabelle/rev/40134ddec3bf

Florian

Am 05.05.2016 um 10:35 schrieb Florian Haftmann:
> 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?
>
> Cheers,
> 	Florian
>
> 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:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

```

Attachment: signature.asc
Description: OpenPGP digital signature

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