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



Your solution should work. I though listrel1p was set up like that, but it is slightly different.

Tobias

On 29/11/2016 18:36, Mark Wassell 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




Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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