Search code examples
mathdefinitionisabelleinduction

Are inductive definitions finitely generated in Isabelle?

Peter Aczel's classic paper An Introduction to Inductive Definitions

https://www.sciencedirect.com/science/article/pii/S0049237X08711200

says that, in an inductive definition,

a rule is a pair (X,x), where X is a set, called the set of premisses and x is the conclusion. The rule will usually be written X->x.

Now, this does not say anything about the finiteness of the set X.

Up to my memory, practical verification tasks involve only finite premise sets Xs, like the reflexive and transitive closure at

https://isabelle.in.tum.de/dist/Isabelle2017/doc/tutorial.pdf#page=124

I have two, related questions:

  1. Is it possible in Isabelle to use infinite premises?

  2. If yes, are there practical examples for that?

Solution

  • Yes, it has to be finite. How would you even write down an infinite set of rules?

    Of course, you have all the expressive power of HOL at your disposal, so you can write something like ‘∀x. f x ≤ f (x + 1)’, which corresponds to infinitely many clauses ‘f 0 ≤ f 1’, ‘f 1 ≤ f 2’, etc. in a sense, but that's still only one assumption.

    EDIT: In response to your comment, you could capture this example in Isabelle like this (if I understood it correctly)

    inductive acc :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" for lt where
  "(⋀x. lt x a ⟹ acc lt x) ⟹ acc lt a"

    Here, lt stands for ‘less than’ and represents some relation. This is actually pretty much what Wellfounded.acc (as in ‘accessible part’) from the Wellfounded theory in Isabelle/HOL does and how it is defined. A perhaps slightly nicer presentation would be this:

    context
  fixes lt :: "'a ⇒ 'a ⇒ bool" (infix "≺" 50)
begin

inductive acc :: "'a ⇒ bool" where
  "(⋀x. x ≺ a ⟹ acc x) ⟹ acc a"

end

    I only glanced over the article you linked, but it seems to me that what he discusses is less general than Isabelle's inductive predicates. It looks to me like he gives a way of defining inductive predicates P that take a single parameter, and all the production rules must be of the form (∀x∈A(a). P(x)) ⟹ P(a). This can easily be modelled in Isabelle, as you can see above.