第一个伊莎贝尔例子

【问题标题】：First Isabelle example第一个伊莎贝尔例子
【发布时间】：2019-10-07 03:23:59
【问题描述】：

一直试图在 YouTube 上重现 Mohamed Abouelwafa 的第三篇教程中的简短示例，但无法克服解析错误。 Mohamed 展示了如何将双右箭头输入为 == 但这似乎不适用于我的 Isabelle 2019，因此我使用 Symbols/Arrow 来获取它。除此之外，我想不出任何东西，但仍然无法让它发挥作用。无论我尝试过什么，它都无法解析。帮助任何人？谢谢！

theory example
imports FOL
begin

lemma ex1: "⟦ A; B ⟧ ⟹  A ⋀ B" 
  apply (rule conjI)
  apply assumption
  apply assumption
  done

end

【问题讨论】：

标签： isabelle

【解决方案1】：

当我将您的代码复制到 Isabelle 时，我发现似乎是一个错字：“A ⋀ B”而不是“A ∧ B”

它们在 StackOverflow 上看起来非常相似，但在 Isabelle 中前者要大得多，并且不适合使用。

当我将其更改为后一个符号∧时，解析错误消失了，证明成功完成。如果您开始输入\and，它将允许您从下拉菜单中选择正确的符号。

我希望这会有所帮助:)

【讨论】：

谢谢，确实如此！视频没有说要使用哪一个，所以我很困惑，以为它们是一样的。是时候开始真正使用伊莎贝尔了。寻找归纳证明示例的最佳位置是什么，例如 1+2+...+n = n(n+1)/2 或类似的？再次感谢您！