*To*: Lukas Bulwahn <lukas.bulwahn at gmail.com>, Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Code generation for predicates with variable number of premises*From*: Mark Wassell <mpwassell at gmail.com>*Date*: Thu, 1 Dec 2016 07:22:49 +0000*In-reply-to*: <CAKXUXMzz+aXOKRKXvVjST1TEfObKzPQZ0QNAuYdAfrwM=B5_4A@mail.gmail.com>*References*: <CAK0o7caJGdiF2t8OtCrfvfnXyhjnpqxj_cTz8MVqDbTTRnC2PA@mail.gmail.com> <768c603c-83db-7d88-4bde-e97f8abefd4d@in.tum.de> <CAK0o7cZXe8P5CVXtNuVSFA+Mqp+xhckRyZLwBHDbkWX6AqYxrw@mail.gmail.com> <CAKXUXMzz+aXOKRKXvVjST1TEfObKzPQZ0QNAuYdAfrwM=B5_4A@mail.gmail.com>

Hi, Thank you for your help. If I add the following to the end of your Listall2.thy datatype D = DSingle nat | DMany "nat list" inductive S :: "D â D â bool" where "S (DSingle x) (DSingle (x+1))" | "list_all2 (Îx y. S (DSingle x) (DSingle y)) xs ys â S (DMany xs) (DMany ys)" code_pred [show_steps, show_mode_inference, show_invalid_clauses] S . I don't get the mode of (i->o->bool) which is the one that I am after. I see in the output that (o => i => bool) => o => i => bool is inferred for list_all2 however clause 2 of S violates i->o->bool. Is it ok to use the predicate that I am defining in the occurrence of list_all2? I am passing to list_all2 the function (Îx y. S (DSingle x) (DSingle y)) I am also getting the following at the end of the output: exception Fail raised (line 74 of "~~/src/HOL/Tools/Predicate_ Compile/predicate_compile_proof.ML"): prove_param: No valid parameter term. Cheers Mark On 30 November 2016 at 07:28, Lukas Bulwahn <lukas.bulwahn at gmail.com> wrote: > Dear Mark, > > you actually do not need to define a new constant, but can set up the > predicate compiler to use list_all2. To see how, look at the attached > theory file. > > If you are wondering why this predicate compiler setup for list_all2 > in is not provided by the default HOL-Main setup (what also crossed my > mind going though the example), this is due to historic circumstances: > I developed the predicate compiler in 2009-2012; the new datatype > package, which defines list_all2, was developed since 2012. Until now, > no one has considered to set up the predicate compiler for the > constants defined by the new datatype package. > > To find out that listrel1p is not the same as list_all2, you can > invoke quickcheck on the proposition `listrel1p R xs ys = list_all2 R > xs ys` and you will get a counterexample. > > Lukas > > On Tue, Nov 29, 2016 at 6:36 PM, Mark Wassell <mpwassell at gmail.com> 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 > >>> > >>> > >> >

**Follow-Ups**:**Re: [isabelle] Code generation for predicates with variable number of premises***From:*Lukas Bulwahn

- Next by Date: 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 December 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