Re: [isabelle] Code generation for predicates with variable number of premises



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
> >>>
> >>>
> >>
>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.