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