[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: 

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.