问如何在伊莎贝尔中使用conjunct1证明"(∀x. P)∧q⟹∀x. P“？
EN

Stack Overflow用户

提问于 2014-12-12 12:56:49

回答 1查看 129关注 0票数 2

我想证明这一点：

lemma
  assumes 0: "(∀x. P) ∧ Q"
  shows "∀x. P"
proof -
  show ?thesis using 0 by (rule conjunct1)
qed

我得到了：

Failed to apply initial proof method⌂:
using this:
  (∀x. P) ∧ Q
goal (1 subgoal):
 1. ∀x. P

我应该在我的证据中改变什么？

回答已采纳

发布于 2014-12-12 13:25:13

类型推断妨碍了你。如果在这两种情况下都修复了x的类型，即

lemma
  assumes 0: "(∀(x::nat). P) ∧ Q"
  shows "∀(x::nat). P"
proof -
  show ?thesis using 0 by (rule conjunct1)
qed

它起作用了。

如果没有此类型注释，则Isabelle将推断出第一个类型为x的'a，即类型变量，而第二个x则得到一个不同的类型变量。

票数 3

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/27444161

复制

相似问题

问如何在伊莎贝尔中使用conjunct1证明"(∀x. P)∧q⟹∀x. P“？EN