Elimination rule for finitely-bounded quantifiers

Question

I have the following goal:

∀x ∈ {0,1,2,3,4,5}. P x

I want to break this goal down into the six subgoals P 0, P 1, P 2, P 3, P 4 and P 5. This is easily done by apply auto. But what is the relevant rule that auto is using to do this? I ask because my actual goal looks more like this:

∀x ∈ {0..<6}. P x

and apply auto doesn't break that goal down in the same way (it gives me

⋀x. 0 ≤ x ⟹ x < 6 ⟹ P x

instead).

Answer 1

Using a [simp] lemma to transform sets into more convenient versions of the set is very convenient. E.g. {0..<6} = {0,1,2,3,4,5}

Answer 2

The rule that auto is using is ballI (bounded all introduction). This transforms ∀x ∈ S. P x into x ∈ S ==> P x.

The issue of transforming x ∈ {0,1,2,3,4,5} into 6 separate subgoals is a separate one. Basically, auto transforms the explicit enumeration into a disjunction and then splits that.

Answer 3

You could use a lemma such as the following to split out a single goal:

lemma expand_ballI: "⟦ (n :: nat) > 0; ∀x ∈ {0..< (n - 1)}. P x; P (n - 1) ⟧ ⟹ ∀x ∈ {0..< n}. P x"
  by (induct n, auto simp: less_Suc_eq)

which could then be repeatedly applied to your rule as follows:

lemma "∀x ∈ {0..< 6 :: nat}. P x"
  apply (rule expand_ballI, fastforce)+
  apply simp_all

resulting in the goals split out as follows:

goal (6 subgoals):
 1. P 0
 2. P (Suc 0)
 3. P 2
 4. P 3
 5. P 4
 6. P 5