Re: [isabelle] executable multiset-extension



Hi Christian,

> But maybe you, or others know tricks to make code generation work
> automagically for each suitable instance?

there are different approaches to make it work.

a) Provide a locale (Âfunctorial styleÂ)

locale executable_mult =
  fixes r :: "'a => 'a => bool"
  assumes irrefl: "irrefl r" and trans: "trans r"
begin

lemma [code]
  "mult r = â"
  using irrefl trans â

end

interpretation executable_mult foo â

b) Provide an abstract type (Âdictionary passing styleÂ)

typedef 'a irrefl_trans = "{r. irrefl r & trans r}" â

setup_lifting â

definition "R = Abs_irrefl_trans r"

lemma [code abstract]:
  "Rep_irrefl_trans R = r" â

definition "mult_exec R = mult (Rep_irrefl_trans R)"

Depends on the particular application which one is preferrable.

Cheers,
	Florian

> 
> cheers
> 
> chris
> 
> 
> On Thu, May 5, 2016, 10:36 Florian Haftmann
> <florian.haftmann at informatik.tu-muenchen.de
> <mailto: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?
> 
>     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
> 

-- 

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.