isabelle - 有没有办法命名和引用 Isabelle apply-scripts 中的假设？

Question

Isabelle (2021) 中是否有任何方法可以引用旧应用样式证明中的假设？

特别是，我有兴趣将假设用作OF运算符中的事实，以便我可以（假设地）做：

apply(rule R[OF assm1  assm4])

, where assm1andassm4应该指当前证明状态下的第 1 和第 4 假设。

很多时候，我可以安排当前子目标的假设，使其R[OF assm1 assm4]与子目标相同。但是，我无法完成证明，因为我不知道如何引用assm1 assm4等。似乎只允许使用全局定理名称OF。

我什至尝试subgoal_tac在假设上使用该方法，但它似乎没有为事实命名的选项。

最后，我必须使用自动脚本，例如simp，对于如此明显的事情，这有点不透明。顺便说一句，这是为了学习目的。我尝试设置simp_trace，但仍然无法在不使用的情况下复制效果simp。

而且，

如果没有办法参考假设，这是策略的限制还是自然演绎的根本限制？（即是R[OF assm1 assm4]不是与自然演绎不兼容的改写方式？）

标签： isabelle

Answer 1

重点是 Isar 是你可以命名假设......

第一个低级解决方案是使用drule（或frule保持假设）。

这是一个例子：

lemma
  assumes ‹⋀x y. P x ⟹ Q y ⟹ R z› ‹P x› ‹Q y›
  shows ‹R z›
  using assms(2-) apply -
  apply (drule assms(1))
  apply assumption
  apply assumption
  done

有关销毁/消除/介绍规则的详细信息，请参阅第5 章。

第二种解决方案是subgoal：

lemma
  assumes ‹⋀x y. P x ⟹ Q y ⟹ R z› ‹P x› ‹Q y›
  shows ‹R z›
  using assms(2-) apply -
  subgoal premises p
    by (rule assms(1)[OF p])
  done

但是如果你有非常深的嵌套，这会产生难以阅读的校样。

第三个也是最好的解决方案是使用 Isar 证明……</p>

这是一个完全避免使用名称的版本：

lemma
  assumes ‹⋀x y. P x ⟹ Q y ⟹ R z› ‹P x› ‹Q y›
  shows ‹R z›
  using assms apply -
  apply (elim meta_allE[of _ x])
  apply (elim meta_allE[of _ y])
  apply (drule cut_rl)
   apply assumption  
  apply (drule cut_rl)
   apply assumption  
  apply assumption
  done

你可以看到这是多么丑陋，以及为什么你应该避免这种情况。