[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
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)
but without too much success. I could have missed something though.
This archive was generated by a fusion of
Pipermail (Mailman edition) and