小编Ben*_*ikt的帖子

Isabelle在证明陈述时是否支持自定义区分大小写？假设我想证明所有自然数的陈述n，但根据n是偶数还是奇数，证明完全不同。是否可以在证明中进行区分大小写，例如

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

到目前为止，我将引理/定理分为两个单独的部分（假定为n偶数/奇数），然后使用这些部分来证明所有自然数的陈述，但这似乎不是最佳解决方案。