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



Dear Mark,

For higher-order predicates, we only allow single variables or
constants as higher-order arguments.

This might be mentioned in the ITP 2009 paper, and this certainly
should be mentioned in my diploma thesis.

I could reformulate your inductive predicate as follows:
```
datatype D =
   DSingle nat | DMany "nat list"

inductive S_aux :: "nat â nat â bool"
and S :: "D â D â bool" where
 "S (DSingle x) (DSingle y) â S_aux x y" |
 "S (DSingle x) (DSingle (x+1))" |
 "list_all2 S_aux xs ys â S (DMany xs) (DMany ys)"


code_pred  [show_steps,  show_mode_inference,  show_invalid_clauses] S .

thm S.equation
```

So you can either use this definition and derive your introduction
rules from that, or you define it with your definition, introduce the
S_aux constant with the first introduction rule, and then derive the
introduction rules from my definition and annotate them with
code_pred_intro,

For code generation, you can then unfold the S_aux_i_o constant in the
S_i_o equation and you will get a recursive equation for S_i_o that
lazily enumerates all solutions.

Logically, there is no difference between your and my definition of S;
technically, the automatically derived induction rule probably looks
different, and hence, one definition might be better suited than the
other (but that's something you must find out).

Lukas

On Thu, Dec 1, 2016 at 8:22 AM, Mark Wassell <mpwassell at gmail.com> wrote:
> 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.