У меня следующая цель:
∀x ∈ {0,1,2,3,4,5}. P x
Я хочу разбить эту цель на шесть подцелей P 0, P 1, P 2, P 3, P 4 и P 5. apply auto это легко делает. Но какое соответствующее правило auto использует для этого? Я спрашиваю, потому что моя настоящая цель выглядит примерно так:
∀x ∈ {0..<6}. P x
и apply auto не разрушает эту цель таким же образом (это дает мне
⋀x. 0 ≤ x ⟹ x < 6 ⟹ P x
вместо).
Очень удобно использовать [simp] лемму для преобразования множеств в более удобные версии множества. Например. {0..<6} = {0,1,2,3,4,5}
Правило, которое использует auto, - ballI (ограничено все введение). Это преобразует ∀x ∈ S. P x в x ∈ S ==> P x.
Отдельно стоит вопрос о преобразовании x ∈ {0,1,2,3,4,5} в 6 отдельных подцелей. По сути, auto преобразует явное перечисление в дизъюнкцию, а затем разбивает его.
Вы можете использовать следующую лемму, чтобы выделить одну цель:
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)
который затем может быть повторно применен к вашему правилу следующим образом:
lemma "∀x ∈ {0..< 6 :: nat}. P x"
apply (rule expand_ballI, fastforce)+
apply simp_all
В результате цели разделились следующим образом:
goal (6 subgoals):
1. P 0
2. P (Suc 0)
3. P 2
4. P 3
5. P 4
6. P 5
