我想证明伊莎贝尔中类似的引理
\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！
我最近在Prolog中使用谓词#=/2看到了一个程序.我在SWI prolog网站上查看了它,并将其定义为
算术表达式X等于Y.当对整数进行推理时,将#=/2替换为/ 2以获得更一般的关系.
我不明白的是,#=/2可以更"通用",因为它只适用于整数.
我在 Isabelle 中遇到了一个使用以下规则的自然演绎问题集classical：
( \\<not> A ==> A) ==>A\n我更习惯使用“排中律”（excluded_middle）和“归谬法”（ccontr）。
我假设这classical与上述两者相同，但我无法从中证明它们中的任何一个，也无法证明lemma "A \xe2\x88\x92\xe2\x86\x92 \xc2\xac \xc2\xac A"问题集中的哪个。我不认为我只是误解了这个规则，因为我成功地使用它lemma "\xc2\xac \xc2\xac A \xe2\x88\x92\xe2\x86\x92 A"从问题集中证明了。有人可以给我一些使用此规则的提示/策略/演示吗？
什么是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))
所以我希望能够理解这些意思.