# 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.*