[isabelle] Termination of Recursive Function with Set Comprehension


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,

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