次の目標があります。
∀x ∈ {0,1,2,3,4,5}. P x
P 0この目標を、P 1、P 2、 、P 3の6 つのサブ目標に分割したいと思いP 4ますP 5。これは、 によって簡単に実行できapply autoます。しかし、これを行うために使用している関連するルールは何autoですか? 私の実際の目標は次のように見えるので、私は尋ねます：
∀x ∈ {0..<6}. P x
apply autoその目標を同じように分解することはありません（それは私に与えます
⋀x. 0 ≤ x ⟹ x < 6 ⟹ P x
代わりは）。
次のような補題を使用して、1 つのゴールを分割できます。
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
使用しているルールautoはballI(bounded all Introduction) です。これは に変形∀x ∈ S. P xしx ∈ S ==> P xます。
x ∈ {0,1,2,3,4,5}6 つの個別のサブゴールに変換する問題は別の問題です。基本的にauto、明示的な列挙を選言に変換してから分割します。
[simp]セットをより便利なバージョンのセットに変換するために補題を使用すると、非常に便利です。例えば{0..<6} = {0,1,2,3,4,5}