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



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.