我想证明伊莎贝尔中类似的引理
\n\nlemma assumes "y = (THE x. P x)" shows "P (THE x. P x)"\n我想这个假设意味着THE x. P x存在并且是明确定义的。所以这个引理也应该是正确的
lemma assumes "y = (THE x. P x)" shows "\xe2\x88\x83! x. P x"\n我不知道如何证明这一点，因为我已经查看了当我在 Isabelle 的查询框中输入“name: the”时出现的所有定理，但它们似乎没有用。我找不到THE两者的定义，也不知道如何定义它，尽管我对它的含义有一个直观的想法。我尝试过类似的事情，尽管我确信这是错误的
"(\xe2\x88\x83!x. P x) \xe2\x9f\xb9 THE x. P x = (SOME x. P x)"\n甚至可能没用，因为我也不知道如何定义SOME！
这是一个初学者的问题.
我正在阅读教程"在Isabelle/HOL中编程和证明".
我想打印"1 + 2"的结果.
所以我写道:
value "1 + 2"
这使:
"1 + (1 + 1)"
:: "'a"
我想看看结果,即"3".我怎么能在伊莎贝尔那里做到这一点？如果我在定理证明器中标准化"1 + 2",则显示结果3.我只想在伊莎贝尔做同样的事情.
请注意,我昨天开始使用Isabelle.
Isabelle中的“商型模式”是什么？
我在互联网上找不到任何解释。
如何在Agda中定义抽象类型.我们在Isabelle中使用typedecl这样做.
更准确地说,我想要Isabelle中以下代码的agda对应物:
typedecl A
谢谢
(注意:如果我可以摆脱下面显示的警告,那么我会说一些无关紧要的东西.作为提问的一部分,我也有一些看法.我想这有点问"为什么我错了"我在说什么？")
似乎用于bool运算符的6个符号应该已分配给语法类型类,并bool为这些类型类实例化.特别是这些:
~, &, |, \<not>, \<and>, \<or>.
因为术语的类型注释是HOL运算符的常见要求,所以我不认为必须bool为这6个运算符使用注释会是一个很大的负担.
我想为其他逻辑运算符重载这6个符号.没有应用程序的通常符号可能导致没有良好的符号解决方案.
在下面的示例源中,如果我可以摆脱警告,那么问题就解决了(除非我为自己设置一个陷阱):
definition natOP :: "nat => nat => nat" where
"natOP x y = x"
definition natlistOP :: "nat list => nat list => nat list" where
"natlistOP x y = x"
notation
natOP (infixr "&" 35)
notation
natlistOP (infixr "&" 35)
term "True & False"
term "2 & (2::nat)"
term "[2] & [(2::nat)]" (*
OUTPUT: Ambiguous input produces 3 parse trees:
...
Fortunately, …我正在寻找创建Eclipse PDE并需要与Isabelle进行通信.我确实找到一些出版物说Scala可以用来与Isabelle沟通.
我正在寻找一个如何使用Scala在Isabelle中创建证明的示例.
什么是real_of_int,real并且int在伊莎贝尔？它们听起来有点像类型,但通常类型都是类似的x ::real,这些都是类似的real x.
我无法证明以下陈述,
"S ((n*x)+(-x)) = S (n*x)*C (-x) + C (n*x)*S (-x)"
我注意到Isabelle写道:
S (real_of_int (int (n * x) + - int x)) =
S (real (n * x)) * C (real_of_int (- int x)) + C (real (n * x)) * S (real_of_int (- int x))
所以我希望能够理解这些意思.
是否存在Isabelle用户遵循的"通用"非正式算法,当他们试图证明某些事情未被立即证明auto或sledgehammer？如果auto需要额外的引理,由用户制定成功或者如果使用更好的一些其他证明方法,一种通用的方法.
一个相关的问题是:是否可能在某处找到一个表格,其中包含所有证明方法以及应用它们的上下文？当我阅读 编程和校对教程时,各种方法的描述(分别是某些方法的变体,例如许多变体auto)都散布在文本中,这不断让我回到文本和Isabelle代码之间(这也会导致忘记究竟用于什么),这导致工作效率非常低.
我想使用我的python程序访问Coq或Isabelle/HOL交互式定理证明器.有没有python包可用？请建议
Isabelle在证明陈述时是否支持自定义区分大小写？假设我想证明所有自然数的陈述n，但根据n是偶数还是奇数，证明完全不同。是否可以在证明中进行区分大小写，例如
proof(cases n)
assume "n mod 2 = 0"
<proof>
next assume "n mod 2 = 1"
<proof>
qed
到目前为止，我将引理/定理分为两个单独的部分（假定为n偶数/奇数），然后使用这些部分来证明所有自然数的陈述，但这似乎不是最佳解决方案。