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



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.