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



Dear Mark,

There is already

 list_all2 :: "('a â 'b â bool) â 'a list â 'b list â bool"

I'm not sure if this has the right setup.

But be aware that there is a difference btw

(1)  list_all (%(x, y). P x y) (zip xs ys) and
(2)  list_all2 P xs ys

While (1) allows xs and ys to have different length, and P only needs
to hold on the smaller length, (2) enforces that both lists have the
same length.

 - Johannes


Am Dienstag, den 29.11.2016, 10:36 +0000 schrieb Mark Wassell:
> 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.