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