*To*: Sven Schneider <svens at cs.tu-berlin.de>*Subject*: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 21 Nov 2007 11:12:25 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <Pine.SOC.4.64.0711201025050.557@fiesta>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <4741A956.6010208@cs.tu-berlin.de> <474299DE.8070305@in.tum.de> <Pine.SOC.4.64.0711201025050.557@fiesta>*User-agent*: Thunderbird 1.5 (X11/20060113)

Sven Schneider wrote: > Not being able to transform anything to code that involes sets or > functions seems to be a very strong restriction to me. > Even though > "card (dom x)" is just an example and changing it to "0" solves the > 'type arity'-Problem changing it does not solve my initial problem. Indeed, adding the following code setup, lemmas [code func del] = card_def lemma [code func]: "Collect P = project P UNIV" unfolding project_def by simp both card and dom turn executable (the latter only on finite types). The fact that there is no trivial solution to handle entities involving "infinity" (like functions and sets) at the same generality as HOL permits is due to the very nature of code generation. > Is there a list of what can/can't be executed and what will/will not be > made executable in the near future? If it is in the manual I missed it. There is an elaborate technical report on that: http://www4.in.tum.de/~haftmann/pdf/codegen_isabelle_haftmann_nipkow_16pp.pdf Pragmatically spoken, as long as you restrict to the FP fragment of HOL (class, datatype, executable constants specified by functions/definitions only involving datatype constructors or executable constants), code generation shall be possible. For specifications involving inherently logical constructs (set comprehension, ...), it may be possible to provide an executable model by means of particular code theorems. Florian

begin:vcard fn:Florian Haftmann n:Haftmann;Florian org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland email;internet:florian.haftmann at informatik.tu-muenchen.de title:M. Sc. tel;work:(++49 89) 289 - 17300 note;quoted-printable:PGP available: = =0D=0A= http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i= nformatik_tu_muenchen_de.pgp=0D=0A= x-mozilla-html:FALSE url:http://isabelle.in.tum.de/~haftmann version:2.1 end:vcard

**Attachment:
signature.asc**

**References**:**[isabelle] [Code-Generation] 'No type arity (..)' - Problem***From:*Sven Schneider

**Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem***From:*Tobias Nipkow

**Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem***From:*Sven Schneider

- Previous by Date: Re: [isabelle] discarding an assumption
- Next by Date: [isabelle] Knaster-Tarski fixed point theorem in HOL/Lattice/CompleteLattice
- Previous by Thread: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
- Next by Thread: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
- Cl-isabelle-users November 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list