Таможенные различия в доказательствах

Question

Поддерживает ли Изабель пользовательские различия в регистрах утверждений? Допустим, я хочу доказать утверждение для всех натуральных чисел n, но доказательство совершенно другое в зависимости от того, n четный или нечетный. Можно ли провести такое различие в доказательстве, например

 proof(cases n) 
   assume "n mod 2 = 0"
   <proof>
   next assume "n mod 2 = 1"
   <proof>
qed

Пока что я разделил бы лемму / теорему на две отдельные части (предполагая n четное / нечетное), а затем используйте эти части для доказательства утверждения для всех натуральных чисел, но это не является оптимальным решением.

Answer 1

В Isabelle2017 вы можете легко доказать специальные правила разграничения падежей, например:

lemma "P (n::nat)"
proof -
  consider (odd) "odd n" | (even) "even n" by auto
  then show ?thesis
  proof cases
    case odd
    then show ?thesis sorry
  next
    case even
    then show ?thesis sorry
  qed
qed

Answer 2

Возможно, вы можете попробовать следующее:

proof -
   have "your statement" when "n mod 2 = 0"
   <proof>
   moreover
   have "your statement" when "n mod 2 = 1"
   <proof>
   ultimately
   show "your statement"
     by <some tactic>
qed