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

Tobias and Johannes, thank you for your responses.

Unfortunately I haven't had much success today using List.list_all2 or

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"
  "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).



On 29 November 2016 at 11:14, Tobias Nipkow <nipkow at> 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.