3

考虑以下愚蠢的例子

theory meta_all
imports Main
begin

lemma strict_subset: "⟦ A ⊂ B ⟧ ⟹ ∃a ∈ B. a ∉ A"
apply(blast)
done

lemma strict_subset2: "∀A B. A ⊂ B ⟶ (∃a ∈ B. a ∉ A)"
apply(blast)
done

lemma "¬ (∃A. A ⊂ A)"
apply(rule notI)
apply(erule exE)

接下来我想使用strict_subset引理并替换A两者A，B它会这样做，但是它将现有的重命名A为Aa，完全违背了引入引理的目的。

apply(insert strict_subset [where A="A" and B="A"])

如果我使用派生引理strict_subset2，一切都会很好，所以我相信我的推理是合理的。

apply(insert strict_subset2)
apply(erule_tac x="A" in allE, erule_tac x="A" in allE)
apply(drule mp, assumption)
apply(erule bexE, erule notE, assumption)
done

end

关键是大多数标准引理都是形式strict_subset而不是形式strict_subset2，伊莎贝尔的制造者不可能让我strict_subset2先自己制作，所以，我一定做错了什么。

我想明白为什么A要改名？我认为这与打字系统有关，因为我认为我还看到了只要类型完全正确，元通用量化就不是问题的例子。

另一个问题是我是否可以以A某种方式阻止重命名？

当然，很可能这两个问题实际上都与真正正确的答案无关，因为我对伊莎贝尔还是很陌生。

PS。是否也可以从 Isabelle 那里获得漂亮的符号？

4

3 回答 3

3

这只是一个狭隘的技术答案，并没有提出这种实验路径是否有意义的问题。

在你的情况下

apply(insert strict_subset [where A="A" and B="A"])

有问题的子目标是：

⋀A. A ⊂ A ⟹ False

但是局部边界（绿色）A是子目标的所谓“参数”，这意味着它隐藏在目标上下文中。使用是strict_subset [where A="A" and B="A"]指证明文本的上下文，而不是证明目标。所以你会得到不同的 (free, undeclared) A，这也通过证明者输出中的特殊突出显示来表示。

有一组特殊的（非常老式的）策略允许潜入隐式目标上下文并进行一些实例化。这是一个例子：

apply(cut_tac A = A and B = A in strict_subset)

现在您在目标状态中拥有了绿色实例A，但由于规则的形式以及这种奇怪的工作方式，它也被分成了太多的子目标cut_tac。

请注意，基本上有以下类别的 Isabelle/Isar 证明方法：

  • 结构化 Isar 证明步骤：特别是rule

  • 带有推理方向指示的弱结构化步骤：erule, drule,frule

  • 允许使用参数进入隐含目标上下文的旧式策略模拟：rule_tac, erule_tac, drule_tac,frule_tac

PS：您可以将 Isabelle/jEdit 中的 unicode 输出复制粘贴到此文本编辑器中。

于 2013-03-12T22:19:38.603 回答
1

我认为您应该更改apply (insert strict_subset)为apply (drule strict_subset). 那么你的证明可以通过 完成apply simp。

（该insert foo方法foo作为附加假设添加，并带有它带来的元量词。您想要的是该drule foo方法，它根据蕴涵削弱了您的一个假设foo。）

于 2013-03-12T21:37:42.890 回答
1

结构化证明避免了所描述的命名问题，还允许您执行单步推理：

lemma  "¬ (∃A :: 'a set. A ⊂ A)"
proof
   assume "∃A :: 'a set. A ⊂ A"
   then obtain A :: "'a set" where "A ⊂ A" ..          (* by (rule exE) *)
   then have "∃a ∈ A. a ∉ A" by (rule strict_subset)
   then obtain a where "a ∉ A" "a ∈ A" ..              (* by (rule bexE) *)
   then show False ..                                  (* by (rule notE) *)
qed

..是一样的by rule。您可以using [[rule_trace]]在证明步骤之前使用（和 find_theorems）来确定正在使用哪个规则rule。

这种结构使证明中发生的事情更加明显。当然，apply 风格肯定具有更多的探索性（这就是为什么我在尝试寻找证明时经常更喜欢它的原因），但结构化证明给你更多的控制权。

于 2013-03-29T09:04:22.637 回答