Re: [isabelle] Induction rules of the function package



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 not solve the problem completely, since even if an argument arguments does change in recursive calls, one would sometime like to see it eliminated from the induction rule.
That is right, but a for clause would also help in proving compatibility for overlapping patterns, because already the function graph definition could use the for clause. Then, reasoning on the graph becomes easier and the termination proof as well, because one would not need to code the functional dependency on the fixed parameters into the relation.

In suce a case, I usually project away the extra arguments manually (using something like [where P="%x y. Q y", standard]), which is not nice but works.
I also use that trick to derive my own induction rules. However, this does not work, if one of the fixed parameters is used in some guard to the recursive call. Here is a concrete example:

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

I obtain it by instantiating P in assoc_list_of_array_code.induct to "%a' n. a = a' --> P n" and doing some more manipulations.

If you have some time somewhen you might consider such a for clause as a feature request. Here is what I think would be a nice definition:

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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.