Re: [isabelle] context-sensitive termination proof



Andrei,

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
Alex


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

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

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




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