*To*: Alexander Krauss <krauss at in.tum.de>*Subject*: Re: [isabelle] Induction rules of the function package*From*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Date*: Thu, 17 Sep 2009 11:14:39 +0200*Cc*: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <20090917103836.yv4ynsu5s84s0os0@mailbroy.in.tum.de>*References*: <20090917103836.yv4ynsu5s84s0os0@mailbroy.in.tum.de>*User-agent*: Thunderbird 2.0.0.17 (X11/20080925)

Hi Alex,

the induction rules that the function package generates for a function definitions are usually great. However, is always quantifies over all parameters of the function, even if they are just passed through all recursive calls. For some proofs, I would like not to have them quantified. Is there an option to the function package to declare such parameters to treat differently (like the for clause for inductive)?Currently, there is no such option. In fact, a for-clause would notsolve the problem completely, since even if an argument arguments doeschange in recursive calls, one would sometime like to see it eliminatedfrom the induction rule.

In suce a case, I usually project away the extra arguments manually(using something like [where P="%x y. Q y", standard]), which is notnice but works.

datatype 'a array = Array "'a list" primrec array_length :: "'a array => nat" where "array_length (Array a) = length a" function assoc_list_of_array_code :: "'a array => nat => (nat * 'a) list" where "assoc_list_of_array_code a n = (if array_length a < n then [] else ... # assoc_list_of_array_code a (n + 1))" by pat_completeness auto termination assoc_list_of_array_code by(relation "measure (%p. array_length (fst p) - snd p)") auto My desired induction rule is: (!!n. (n < array_length a ==> P (n + 1)) ==> P n) ==> P n

function assoc_list_of_array_code :: "'a array => nat => (nat * 'a) list" for a :: "'a array where "assoc_list_of_array_code a n = (if array_length a < n then [] else ... # assoc_list_of_array_code a (n + 1))" by pat_completeness auto termination assoc_list_of_array_code by(relation "%a. measure (%n. array_length a - n)") auto Anyway, I will have a look at your induct_scheme method. Cheers, Andreas

**Follow-Ups**:**Re: [isabelle] Induction rules of the function package***From:*Alexander Krauss

**References**:**Re: [isabelle] Induction rules of the function package***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] question about "fun"
- Next by Date: [isabelle] SBMF- Brazilian Symposium on Formal Methods - First Call for Satelite Events
- Previous by Thread: Re: [isabelle] Induction rules of the function package
- Next by Thread: Re: [isabelle] Induction rules of the function package
- Cl-isabelle-users September 2009 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