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两者AB它会这样做,但是它将现有的重命名AAa,完全违背了引入引理的目的。

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 回答