Search code examples
isabelle

Finite runs on a transition system

I want to write a predicate that would state that a transition system cannot have infinite runs from a state s. So consider the transition system is given by R, then the definition I have come up with is:

inductive finite_runs for R where         
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"

Is this the simplest way I can state this fact in Isabelle? In particular, I have browsed the Archive of Formal Proofs (the rewriting and labeled transition theories) but got no simpler solution.

Solution

  • There is Wellfounded.termip in the standard library. I think it should do exactly what you want.

    It is basically an abbreviation using Wellfounded.accp, which does the same thing but going ‘backwards’.