Search code examples
isabelleinductionnon-termination

Non-terminating inductive predicates

In the excellent Programming and Proving in Isabelle/HOL it says

[...] in contrast to recursive functions, there is no termination requirement for inductive definitions. (pdf p. 40)

  1. Does this mean there are inductive definitions where it's possible to have an infinitely deep derivation tree?
  2. What is an example of such a non-terminating derivation (preferably one with infinite height)? How do you 'construct' these?
  3. How are rule induction principles on these still sound?
Solution
    1. No. You need coinductive predicates for that.
    2. Not existing.
    3. If you look at the induction principle, you'll find that they have an additional premise. For example, "even n". That means, before you can even apply the induction principle, you'll need to know that you have a finite derivation at hand.