Re: [isabelle] Code generation for predicates with variable number of premises
- 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> <email@example.com> <CAK0o7cZXe8P5CVXtNuVSFA+Mqp+xhckRyZLwBHDbkWX6AqYxrw@mail.gmail.com> <CAKXUXMzz+aXOKRKXvVjST1TEfObKzPQZ0QNAuYdAfrwM=B5_4A@mail.gmail.com>
Thank you for your help. If I add the following to the end of your
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
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)
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.
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.
> 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
> > would have needed to 'pass though' these functions to make use of the
> > 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
> > 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
> > 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
> >> that would be magic. You need to be explicit about how ys is computed
> >> 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
> >> 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
> >> 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
> >> 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
> >>> "Turning inductive into equational specifications") indicates
> >>> is
> >>> consistent. However I can see that the appearance of 'zip xs ys' is
> >>> 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'
> >>> (x#xs)) (DMany (y#ys))"
> >>> However I would like to see if it can be made to work without doing
> >>> 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
This archive was generated by a fusion of
Pipermail (Mailman edition) and