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
"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
by(relation "%a. measure (%n. array_length a - n)") auto
Looks reasonable. I'll think about it.
This archive was generated by a fusion of
Pipermail (Mailman edition) and