Re: [isabelle] context-sensitive termination proof

The function package does build up context information for you.

The algorithm for doing so involves using congruence rules, in a similar manner to the use of congruence rules in the simplifier. Essentially these congruence rules define the assumptions that may be made while rewriting inner contexts of the goals.

You seem to need to exploit the fact that P a c holds for the right hand side of the conjunction to matter. I suspect that declaring conj_cong[fundef_cong] before defining your recursive function may add the necessary fact to the termination rule.

This is a powerful technique - we have managed to use it to define what are essentially recursive imperative programs and state their termination property in terms of progressive state transformation. We had to add a great many rules to the set, but we got there. Good luck!


On Tue, 27 May 2008, Andrei Popescu wrote:


I am having trouble proving termination of a function whose recursive call argument decreases conditionally, in a context which is essentially the following:

typedecl A  typedecl B  typedecl C

 u :: "A => C => B"
 v :: "C => A"
 w :: "C => B"
 P :: "A => C => bool"
 size :: "A => nat"

axioms conditional_decrease:
"P a c ==> size (v c) < size a"

function f :: "A => B set" where
"f a = {u a c| c. P a c  &  w c : f (v c)}"

The only tool I see available for proving termination of f is the lemma

f.termination: "[|wf ?R; !! a x c. (v c, a) : ?R|] ==> ALL x. f_dom x"

while I would need something like:

"[|wf ?R; !! a x c. P a c ==> (v c, a) : ?R|] ==> ALL x. f_dom x"

or rather

"[|wf (?R Int {(v c,a)| a c. P a c}); !! a x c. (v c, a) : ?R|] ==> ALL x. f_dom x"

Thanks in advance for any hint on how to handle this.

   Andrei Popescu

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