*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Code generation for predicates with variable number of premises*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Tue, 29 Nov 2016 12:14:18 +0100*In-reply-to*: <CAK0o7caJGdiF2t8OtCrfvfnXyhjnpqxj_cTz8MVqDbTTRnC2PA@mail.gmail.com>*References*: <CAK0o7caJGdiF2t8OtCrfvfnXyhjnpqxj_cTz8MVqDbTTRnC2PA@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.5.0

listrel1p :: "('a â 'a â bool) â 'a list â 'a list â bool" for exactly this purpose in List.thy. You could now write listrel1p (Î(x,y). S (DSingle x) (DSingle y)) xs ys

Tobias On 29/11/2016 11:36, Mark Wassell wrote:

Hello Andreas and Isabelle list, Thank you for your help with my last question. I have a follow up question: I would like to be able to generate code for inductive predicates that have clauses with variable number of premises that mention the inductive predicate being defined. A simple case: datatype D = DSingle nat | DMany "nat list" inductive S :: "D â D â bool" where "S (DSingle x) (DSingle x)" | "List.list_all (Î(x,y). S (DSingle x) (DSingle y)) (zip xs ys) â S (DMany xs) (DMany ys)" For this I would like to generate a function S_i_o. Intuitively this should be possible. However the mode inference for S is only passing i->i->bool as a valid mode. My rough understanding of how mode inference works (for example from "Turning inductive into equational specifications") indicates i->o->bool is consistent. However I can see that the appearance of 'zip xs ys' is mixing known data (the xs) with unknown data (ys). Also its possible that List.list_all is being considered as a side condition where, I believe, all variables need to be known. So my question is this: Why doesn't it infer i->o->bool where according to the mode inference rules it should? One solution is to by-pass this completely and define the predicate as: inductive S' :: "D â D â bool" where "S' (DSingle x) (DSingle x)" | "S' (DMany []) (DMany [])" | "S' (DMany xs) (DMany ys) ==> S' (DSingle x) (DSingle y) ==> S' (DMany (x#xs)) (DMany (y#ys))" However I would like to see if it can be made to work without doing this. I have also tried to define a version of list_all as an inductive predicate and also a list_all_pair, as in inductive T :: "D â D â bool" where "T (DSingle x) (DSingle x)" | "list_all_pair (Îx y. T (DSingle x) (DSingle y)) xs ys â T (DMany xs) (DMany ys)" but without too much success. I could have missed something though. Cheers Mark

**Attachment:
smime.p7s**

**Follow-Ups**:

**References**:**[isabelle] Code generation for predicates with variable number of premises***From:*Mark Wassell

- Previous by Date: Re: [isabelle] Code generation for predicates with variable number of premises
- Next by Date: [isabelle] New AFP article: Complx
- Previous by Thread: Re: [isabelle] Code generation for predicates with variable number of premises
- Next by Thread: Re: [isabelle] Code generation for predicates with variable number of premises
- Cl-isabelle-users November 2016 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