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



On 07.02.2013 12:08, Tjark Weber wrote:
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")

I think you need a congruence rule for Setsum/setsum. A quick grep for "fundef_cong" does not find any predefined rule. See the section on Higher-Order Recursion in the documentation of the function package.

  -- Lars





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