# 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!
```
Yours,
Thomas.

On Tue, 27 May 2008, Andrei Popescu wrote:

```
```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&nbsp; typedecl B&nbsp; typedecl C

consts
&nbsp;u :: "A =&gt; C =&gt; B"
&nbsp;v :: "C =&gt; A"
&nbsp;w :: "C =&gt; B"
&nbsp;P :: "A =&gt; C =&gt; bool"
&nbsp;size :: "A =&gt; nat"

axioms conditional_decrease:
"P a c ==&gt; size (v c) &lt; size a"

function f :: "A =&gt; B set" where
"f a = {u a c| c. P a c&nbsp; &amp;&nbsp; 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|] ==&gt; ALL x. f_dom x"

while I would need something like:

f.context_sensitive_termination:
"[|wf ?R; !! a x c. P a c ==&gt; (v c, a) : ?R|] ==&gt; 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|] ==&gt; ALL x. f_dom x"

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

&nbsp;&nbsp; Andrei Popescu

```
```

```

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