Re: [isabelle] context-sensitive termination proof


I am having trouble proving termination of a function whose recursive call argument decreases conditionally, in a context which is essentially the following:
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:

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

You need to add a congruence rule (here: conj_cong for the conjunction) to the definition. See the attached theory (and the function tutorial for some more explanation on congruence rules).

Hope this helps

theory Scratch imports Main
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"

declare conj_cong[fundef_cong]

function f :: "A => B set" where 
"f a = {u a c| c. P a c  \<and>  w c : f (v c)}"
by auto

by (relation "measure size") (auto simp: conditional_decrease)

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