# [isabelle] [Isabelle2007] Function termination measures

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.
`
TIA,
George

theory FunTerm imports Main begin
function tst1 :: "nat \<Rightarrow> nat"
and tst2 :: "nat \<Rightarrow> nat"
where
"tst1 n = (tst2 n) + 1"
| "tst2 n = n + 1"
by pat_completeness auto
fun tstMeasure :: "nat + nat => nat" where
"tstMeasure n =
(case n of Inl n1 \<Rightarrow> 1
| Inr n2 \<Rightarrow> 0
)"
termination tst1
apply(relation "measure tstMeasure")
apply(auto)
done
function tst1' :: "nat \<Rightarrow> nat"
and tst2' :: "nat \<Rightarrow> nat"
and tst3' :: "nat \<Rightarrow> nat"
where
"tst1' n = (tst2' n) + 1"
| "tst2' n = (tst3' n) + 1"
| "tst3' n = n + 1"
by pat_completeness auto
fun tstMeasure' :: "nat + nat + nat => nat" where
"tstMeasure' n =
(case n of Inl n1 \<Rightarrow> 2
| Inr n1 \<Rightarrow> (case n1 of Inl n2 \<Rightarrow> 1
| Inr n2 \<Rightarrow> 0
)
)"
termination tst1'
apply(relation "measure tstMeasure'")
apply(auto)
done
function t1 :: "nat \<Rightarrow> nat"
and t2 :: "nat \<Rightarrow> nat"
and t3 :: "nat \<Rightarrow> nat"
and t4 :: "nat \<Rightarrow> nat"
where
"t1 n = (t2 n) + 1"
| "t2 n = (t3 n) + 1"
| "t3 n = (t4 n) + 1"
| "t4 n = n + 1"
by pat_completeness auto
fun tMeasure :: "nat + nat + nat + nat \<Rightarrow> nat"
where
"tMeasure v = (case v of Inl x \<Rightarrow> 3
| Inr x \<Rightarrow> (case x of Inl y \<Rightarrow> 2
| Inr y \<Rightarrow> (case y of Inl z \<Rightarrow> 1
| Inr z \<Rightarrow> 0
)
)
)"
termination t1
apply(relation "measure tMeasure")
end

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