# [isabelle] context-sensitive termination proof

Hello,
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
consts
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:
f.context_sensitive_termination:
"[|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.*