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