title: Finite runs on a transition system
body: <p>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:</p>
  
  <pre><code>inductive finite_runs for R where         
  "(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"
  </code></pre>
  
  <p>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.</p>