# [isabelle] termination of mutually recursive functions

*To*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] termination of mutually recursive functions
*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>
*Date*: Wed, 07 Sep 2011 16:17:34 +0300
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:6.0) Gecko/20110812 Thunderbird/6.0

Hello,
I have the following recursive function definitions:
consts const_a:: "'a"
function
A_fun :: "nat => 'b"
and B_fun :: "int => 'd"
and C_fun :: "bool => 'f"
and D_fun :: "bool => 'g"
and E_fun :: "nat => 'j"
where
"A_fun x = const_a" |
"B_fun y = const_a" |
"C_fun y = const_a" |
"D_fun y = const_a" |
"E_fun y = const_a"
apply pat_completeness
by auto
termination
apply (relation "test_rel")
sorry
function
A_f :: "nat => 'b"
and B_f :: "int => 'd"
and C_f :: "bool => 'f"
where
"A_f x = const_a" |
"B_f y = const_a" |
"C_f y = const_a"
apply pat_completeness
by auto
termination
apply (relation "test_rel")
sorry
The first collection of functions needs a termination relation of the type

` (((nat + int) + bool + bool + nat) * ((nat + int) + bool + bool +
``nat)) set
`and the second collection needs a termination relation of the type
((nat + int + bool) * (nat + int + bool)) set

`The question is why in the first case the first two types (nat and int)
``are grouped
`together and in the second case they are not? What is the general rule
for type of the termination relation?
Best regards,
Viorel Preoteasa

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