*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*: Wed, 30 Nov 2016 07:38:11 +0100*In-reply-to*: <CAK0o7cZXe8P5CVXtNuVSFA+Mqp+xhckRyZLwBHDbkWX6AqYxrw@mail.gmail.com>*References*: <CAK0o7caJGdiF2t8OtCrfvfnXyhjnpqxj_cTz8MVqDbTTRnC2PA@mail.gmail.com> <768c603c-83db-7d88-4bde-e97f8abefd4d@in.tum.de> <CAK0o7cZXe8P5CVXtNuVSFA+Mqp+xhckRyZLwBHDbkWX6AqYxrw@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:45.0) Gecko/20100101 Thunderbird/45.5.0

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

Tobias and Johannes, thank you for your responses. Unfortunately I haven't had much success today using List.list_all2 or listrel1p. I am a little puzzled as to how these were going to work as mode inference would have needed to 'pass though' these functions to make use of the mode information for S (DSingle x) (DSingle y) occurrence inside the function. I am thinking that I might need to have an equivalent of List.list_all2 defined as an inductive predicate so that mode information for this can be used in the mode inference of S. For example: inductive list_all2_ind :: "('a â 'b â bool) â 'a list â 'b list â bool" where "list_all2_ind P [] []" | "list_all2_ind P xs ys â P x y â list_all2_ind P (x#xs) (y#ys)" When I do code_pred for list_all2_ind it does tell me that the mode (i -> o -> bool) -> i -> o -> bool is consistent (the elimination rule for this being called list_all2_ind_FioB_i_o). Cheers Mark On 29 November 2016 at 11:14, Tobias Nipkow <nipkow at in.tum.de> wrote:The predicate compiller cannot invert arbitrary functions or expressions, that would be magic. You need to be explicit about how ys is computed from xs. Your current specification is not even a function, for any xs, my suitable ys exist because zip will truncate longer ys's. You have to phrase your precondition in terms of relations that have the right mode (or via functions that compute the ys's, but that will not be possible because that involves S again. However, there is the predefined predicate 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 That should be executable. In the end, you should formulate the precondition in the most abstract style (eg via quantifiers) and prove the listrel1p version as a consequence for code generation. 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**

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

**Re: [isabelle] Code generation for predicates with variable number of premises***From:*Tobias Nipkow

**Re: [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: Re: [isabelle] [ExternalEmail] [isabelle-dev] afp-2016-1 branch
- Previous by Thread: Re: [isabelle] Code generation for predicates with variable number of premises
- Next by Thread: [isabelle] New AFP article: Complx
- 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