Re: [isabelle] Induction rules of the function package



Andreas Lochbihler wrote:
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

Looks reasonable. I'll think about it.

Cheers,
Alex





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