[isabelle] termination of mutually recursive functions



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.