Re: [isabelle] [Isabelle2007] Function termination measures



George Karabotsos wrote:
Hello all,

I am a bit confused with function termination. In particular on the manner the sum of types for mutually recursive functions are defined.

For example consider the attached toy theory (although none of them is mutually recursive I believe they illustrate my confusion). Can someone show me how I can prove termination for the quartet t1,t2,t3,and t4 functions? I know it can be proven using lexicographic_order. However, I am more interested in proving termination via a measure function in order to additionally understand how the summation of the types is packaged together.

The function package builds a balanced tree for the sum types: If you have four functions with argument types T1,... T4, then you have to provide a relation over the nested sum type

(T1 + T2) + (T3 + T4)

but your relation is on

T1 + T2 + T3 + T4

which is synonymous for

T1 + (T2 + (T3 + T4))  .

You can check what kind of relation you have to give by writing

termination
proof

Then the "proof" command applies the rule which is also applied by the "relation" method, but without instantiating the relation. You can then, say, enable "show types"...

Hope this helps,
Alex





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