# [isabelle] Proving termination of a recursive function

Hi,
I've been getting into Isabelle recently, and I have a problem with
function termination: I have a recursive data type, and a function
checking some property of it, but I'm not sure how to approach the
termination proof:
~~~~
theory MinimalExample
imports Main "~~/src/HOL/Library/FSet" Map
begin
datatype ThreadId = UserThread nat
datatype POR = POR "ThreadId fset" "ThreadId fset" "ThreadId â POR"
function
por_well_formed :: "POR â bool"
where
"por_well_formed por â (case por of (POR runnable todo done) â
( todo |â| runnable
â dom done â fset runnable
â fset todo â dom done = {})
â (â p â ran done. por_well_formed p))"
by auto
termination sorry
end
~~~~
My informal termination argument goes like this: because POR is data,
not codata, there can't be an infinite sequence POR1 -> POR2 -> POR3
-> ... (following the links in the map). This means that the recursive
case in por_well_formed will terminate. However, I'm not sure how to
formalise that.
Any suggestions for this in particular, or termination proofs in
general, would be greatly appreciated.
--
Michael Walker (http://www.barrucadu.co.uk)

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