isabelle - 无法获取变量

Question

我试图证明我提出的以下简单定理:

A point is on the boundary iff any small enough ball around that point contains points both in S and out of S.

下面我已经成功地向前移动了，但我被困在向后的方向上。

使用相同的方法在最后一步失败了，目标已经接近但还没有完全实现，我不知道在这里该怎么做:

lemma frontier_ball: "x ∈ frontier S ⟷
  (∃r>0. (∀δ>0. δ<r ⟶ ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})))"
  (is "?lhs = ?rhs")
proof
  {
    assume "?lhs"
    hence "x ∉ interior S ∧ x ∉ interior (-S)" by (auto simp: frontier_def interior_complement)
    hence "∀δ>0. ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})" by (auto simp: mem_interior)
    then have "?rhs" by (simp add: Orderings.no_top_class.gt_ex)
  }
  {
    assume "¬?lhs"
    hence "x ∈ interior S ∨ x ∈ interior (-S)" by (auto simp: frontier_def interior_complement)
    hence "∃δ>0. ball x δ ∩ S = {} ∨ ball x δ ∩ -S = {}" by (auto simp: mem_interior)
    then have "¬?rhs" by (simp add: subset_ball)
  }
qed

我试图告诉 isabelle 如何获取这样的增量，但它卡在获取步骤上:

lemma frontier_ball: "x ∈ frontier S ⟷
  (∃r>0. (∀δ>0. δ<r ⟶ ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})))"
  (is "?lhs = ?rhs")
proof
  {
    assume "?lhs"
    hence "x ∉ interior S ∧ x ∉ interior (-S)" by (auto simp: frontier_def interior_complement)
    hence "∀δ>0. ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})" by (auto simp: mem_interior)
    then have "?rhs" by (simp add: Orderings.no_top_class.gt_ex)
  }
  {
    fix r::real
    assume "¬?lhs ∧ r>0"
    hence "x ∈ interior S ∨ x ∈ interior (-S)" by (auto simp: frontier_def interior_complement)
    then obtain r2 where "r2>0" and "ball x r2 ∩ S = {} ∨ ball x r2 ∩ -S = {}" by (auto simp: mem_interior)
    then obtain δ where "δ>0 ∧ δ<r ∧ δ<r2" by auto

  }
qed

任何指针都会很棒!

Answer 1

好吧，你可以构造这样一个δ。如果您有r > 0和r2 > 0你想要一些δ满足0 < δ ≤ r2和0 < δ < r ，为什么不直接使用 min r2 (r/2) ？您可以定义 δ是这样，然后你就可以证明你想要的属性:

    def δ ≡ "min r2 (r/2)"
    with r2 A have δ: "δ > 0" "δ < r" "δ ≤ r2" by auto
    with r2 have δ': "ball x δ ∩ S = {} ∨ ball x r2 ∩ -S = {}" using subset_ball[OF δ(3)] by auto

或者，更直接一点:

lemma frontier_ball: "(x :: 'a :: {metric_space}) ∈ frontier S ⟷
  (∃r>0. (∀δ>0. δ<r ⟶ ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})))"
  (is "?lhs = ?rhs")
proof -
  {
    assume "?lhs"
    hence "x ∉ interior S ∧ x ∉ interior (-S)" by (auto simp: frontier_def interior_complement)
    hence "∀δ>0. ((ball x δ) ∩ S ≠ {} ∧ (ball x δ) ∩ -S ≠ {})" by (auto simp: mem_interior)
    then have "?rhs" by (simp add: Orderings.no_top_class.gt_ex)
  }
  moreover
  {
    assume lhs: "¬?lhs"
    {
      fix r :: real assume r: "r > 0"
      from lhs have "x ∈ interior S ∨ x ∈ interior (-S)" 
        by (auto simp: frontier_def interior_complement)
      then obtain δ where "δ > 0" "ball x δ ∩ S = {} ∨ ball x δ ∩ -S = {}" 
        by (auto simp: mem_interior)
      with r have "min δ (r/2) > 0" "min δ (r/2) < r" 
        "ball x (min δ (r/2)) ∩ S = {} ∨ ball x (min δ (r/2)) ∩ -S = {}" using subset_ball by auto
      hence "∃δ>0. δ < r ∧ (ball x δ ∩ S = {} ∨ ball x δ ∩ -S = {})" by blast
    }
    hence "¬?rhs" by blast
  }
  ultimately show ?thesis by blast
qed

郑重声明，我会避免做类似 assume "A ∧ B" 的事情。做assume "A" "B"反而。这为您提供了两个可以直接使用的事实，而不是用 HOL 连词将它们包裹在一个事实中。