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



Hi Tjark and Lars,

Am Donnerstag, den 07.02.2013, 12:18 +0100 schrieb Lars Noschinski:
> 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.

You need a congruence rule not for setsum but for {f k | k. k<  n} which
is conjunction. A simple solution is to rewrite the rule with the image
operator, it already has the correct fundef-cong rule installed:

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

   termination by lexicographic_order

With

  declare rev_conj_cong[fundef_cong]

your version also works.

 - Johannes










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