title: Non-terminating inductive predicates
body: <p>In the excellent <a href="https://isabelle.in.tum.de/doc/prog-prove.pdf" rel="nofollow noreferrer">Programming and Proving in Isabelle/HOL</a> it says</p>
  
  <blockquote>
    <p>[...] in contrast to recursive functions, there is no termination requirement
    for inductive definitions. (pdf p. 40)</p>
  </blockquote>
  
  <ol>
  <li>Does this mean there are inductive definitions where it's possible to have an infinitely deep derivation tree?</li>
  <li>What is an example of such a non-terminating derivation (preferably one with infinite height)? How do you 'construct' these?</li>
  <li>How are rule induction principles on these still sound?</li>
  </ol>