[isabelle] Termination Proof


I was trying to prove termination for the following definition:
theory Termination
imports Nat Multiset Divides Datatype


inductive_set even :: "nat set" where
zero[intro!]: "0 ∈ even" |
step[intro!]: "n ∈ even ⟹ (Suc (Suc n)) ∈ even"

function (sequential) foo :: "nat ⇒ nat list" where
"foo 0             = [0]" |
"foo (Suc 0)       = [1]" |
"foo n = (case n ∈ even of
          True  ⇒ n # foo (n div 2) |
          False ⇒ n # foo (Suc n))"
by pat_completeness auto
apply (relation "measures [Suc, λn. n div 2]")
apply auto

I know I can change the definition slightly for foo to make it pass the
termination checker using the standard lexicographical measure.  I'm
learning about function package and specifically, how to write termination
proofs so I want to avoid the easy route here.  I'm following this
documentation in particular:

My understanding of the above proof attempt is that it will never work
because the well founded relation needs for the "n \<notin> even" case to
decrease or stay the same, but instead it gets larger in the recursive call.

I can also imagine a proof of termination based on the fact that if n is odd
then Suc n will be even and the next call to foo will cause the argument to
shrink by more than it grew.  Is it possible to write such a proof and lease
the termination checker?  Perhaps there is something that can be done with
the function domain in the same way partial functions are handled?  Advice
on how to get started with such a proof?  Perhaps there are examples of this
somewhere already?


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