Re: [isabelle] Termination of Recursive Function with Set Comprehension



Hi Tjark,

you are missing a congruence rule for setsum such as the following:

declare setsum_cong[fundef_cong]

However, this does not suffice because "∑{f k | k. k < n}" is an abbreviation for "setsum (%x. x) {u. ?k. u = f k & k < n}", i.e., you would need additional congruence rules for Collect, Ex and op &. If you rewrite the right-hand side to "(∑k | k < n. f k)", the above declaration should work, because "∑k | k < n. f k" is the same as "setsum (%k. f k) {k. k < n}", i.e., f is a direct argument to setsum.

Hope this helps,
Andreas

On 02/07/2013 12:08 PM, Tjark Weber wrote:
Hi,

Consider this (simplified) example of a recursive function whose
definition involves set comprehension:

   function (sequential) f :: "nat ⇒ nat" where
     "f 0 = 1"
   | "f n = ∑{f k | k. k < n}"
   by pat_completeness auto

How to prove termination? In particular,

   termination f
   apply (relation "measure id")

results in an unprovable goal.

Best regards,
Tjark







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