如何让伊莎贝尔认识到一个明显的结论

Question

我试图证明在 isabelle 中集合的边界、内部和外部是不相交的。在我标记为“***”的那一行，c \<inter> d = {} 显然是根据块开头的假设从上一行得出的事实，那么我如何让伊莎贝尔理解这一点？

theory Scratch
imports
  "~~/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space"
  "~~/src/HOL/Probability/Sigma_Algebra"
begin

lemma boundary_disjoint: "disjoint {frontier S, interior S, interior (-S)}"
proof (rule disjointI)
  fix c d assume sets:
    "c \<in> {frontier S, interior S, interior (-S)}"
    "d \<in> {frontier S, interior S, interior (-S)}"
    and "c \<noteq> d"
  show "c \<inter> d = {}"
  proof cases
    assume "c = frontier S \<and> d = interior S"
    then show ?thesis using frontier_def by auto
  next
    assume "c = frontier S \<and> d = interior (-S)"
    have "closure S \<inter> interior (-S) = {}" by (simp add: closure_interior)
    hence "frontier S \<inter> interior (-S) = {}" using frontier_def by auto
    *** then show ?thesis by auto
  next

  qed
qed

end

Answer 1

在 Isar 中，您必须明确引用要使用的事实。如果你说你的目标来自上一行和你所做的局部假设，你应该给这个假设起一个名字，写assume A: "c = frontier S ∧ d = interior (-S)"，然后你可以用with A have ?thesis by auto.[=29来证明你的目标=]

为什么我写的是have而不是show？那么，还有一个问题。你做了一个 proof cases，但它使用了规则 (P ⟹ Q) ⟹ (¬P ⟹ Q) ⟹ Q，即它做了一种“P 是真还是假？”的大小写区分。这不是你想要的。

区分案例的一种方法是这样的：

from sets show "c ∩ d = {}"
  proof (elim singletonE insertE)

insertE 是 x ∈ insert y A 形式事实的消除规则，因为 {a,b,c} 只是 insert a (insert b (insert c A)) 的语法糖，这就是你想要的。 singletonE 类似，但专门针对 x ∈ {y}；使用 singletonE 而不是 insertE 意味着你不会得到像 x ∈ {}.

这样的假设的微不足道的案例

这为您提供了 9 个案例，其中 3 个案例由 simp_all 轻松解决。如果你想的话，剩下的你必须在 Isar 中证明自己，但它们也可以很容易地通过 auto 解决:

from sets and `c ≠ d` show "c ∩ d = {}"
  by (auto simp: frontier_def closure_def interior_closure)

如何让伊莎贝尔认识到一个明显的结论

how to get isabelle to recognize an obvious conclusion

isabelle