Доказательство по индукции с тремя базовыми случаями (Изабель)

Я хочу иметь возможность доказать утверждение индукцией по 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" по индукции, но это было бы не столь сильное утверждение. Я рассматриваю случай, разделенный на _3 _, _ 4_ и "n>=2", и доказываю только последний случай по индукции.


induction isabelle isar
person IIM    schedule 29.12.2016    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Самый простой способ - это, вероятно, доказать собственное правило индукции для того типа индукции, который вам нужен, например:

lemma nat_0_1induction_schemainduct [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_1induction_schemainduct)

Теоретически метод 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 напрямую, а затем провести различие между регистрами на этапе индукции для базовых случаев.

person Manuel Eberl    schedule 29.12.2016