*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Code generation for predicates with variable number of premises*From*: Mark Wassell <mpwassell at gmail.com>*Date*: Tue, 29 Nov 2016 10:36:03 +0000

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

**Follow-Ups**:**Re: [isabelle] Code generation for predicates with variable number of premises***From:*Johannes Hölzl

**Re: [isabelle] Code generation for predicates with variable number of premises***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Isabelle2016-1-RC3 available for testing
- Next by Date: Re: [isabelle] Code generation for predicates with variable number of premises
- Previous by Thread: Re: [isabelle] [ExternalEmail] [isabelle-dev] afp-2016-1 branch
- Next by Thread: Re: [isabelle] Code generation for predicates with variable number of premises
- Cl-isabelle-users November 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list