感應證明與三個基本案例（伊莎貝爾）

Question

我想能夠證明一個聲明在n（nat類型）上的歸納。它由一個條件組成，前提條件的前提條件是n> = 2。前提條件爲假的條件總是如此。所以我想證明n = 0，n = 1和n = 2的情況都與主要歸納步驟分開。是否有可能通過誘導基地情況下，像下面做一個證明：

lemma "P (n::nat) --> Q" 
    proof (induct n) 
    case 0 
    show ?case sorry 
    next 
    case 1 
    show ?case sorry 
    next 
    case 2 
    show ?case sorry 
    next 
    case (Suc n) 
    show ?case sorry 
    qed 

因爲它的立場，這似乎並沒有工作。我可以通過歸納證明"P (n+2) --> Q"，但它不會是一個強有力的聲明。我正在考慮將案件分成"n=0"，"n=1"和"n>=2"，並通過歸納證明最後一個案例。

Answer 1

最徹底的方法可能是證明了你想要的那種感應的定製感應規則是這樣的：

lemma nat_0_1_2_induct [case_names 0 1 2 step]: 
    assumes "P 0" "P 1" "P 2" "⋀n. n ≥ 2 ⟹ P n ⟹ P (Suc n)" 
    shows "P n" 
proof (induction n rule: less_induct) 
    case (less n) 
    show ?case using assms(4)[OF _ less.IH[of "n - 1"]] 
    by (cases "n ≤ 2") (insert assms(1-3), auto simp: eval_nat_numeral le_Suc_eq) 
qed 

lemma "P (n::nat) ⟶ Q" 
proof (induction n rule: nat_0_1_2_induct) 

理論上，induction_schema方法也是非常有用的，證明這種定製感應規則，但在這種情況下，它不會有很大的幫助：

lemma nat_0_1_2_induct [case_names 0 1 2 step]: 
    "P 0 ⟹ P 1 ⟹ P 2 ⟹ (⋀n. n ≥ 2 ⟹ P n ⟹ P (Suc n)) ⟹ P n" 
proof (induction_schema, goal_cases complete wf terminate) 
    case (complete P n) 
    thus ?case by (cases n) force+ 
next 
    show "wf (Wellfounded.measure id)" by (rule wf_measure) 
qed simp_all 

你也可以使用less_induct直接，然後做基礎的情況下誘導工序內的情況區分。