避免匹配 (λx.x)

Question

考虑理论

理论从头开始导入主要 开始 记事本 开始 修复 P 和 f g h :: "int ⇒ int" 假设前提：“P f”“P g”“P h” 假设 comp：“⋀ f g. P f ⟹ P g ⟹ P (λ x. f (g x))” 有“P(λx.f(g(hx)))” 对不起 结尾 结束

显然，引理可以从prems 和comp 显示。事实上，乍一看，人们会期望它可以通过

by (intro prems comp)

但这只是循环。原因是comp 与目标的一种可能统一是f = (λa. a) 和g = (λ x. f (g (h x)))（使用apply (rule comp) 可以看出）并且没有取得任何进展。

我了解这是rule reps 的有效行为。 intro。尽管如此，从实用的角度来看，我经常遇到简化或引入规则，这些规则在匹配(λx. x) 时匹配除了的所有情况下都非常有用。

有什么方法可以声明comp，以便Isabelle 的匹配器不考虑f 或g 是(λx. x) 的解决方案？

如果不是，为什么不是这样的技术和/或理论原因是什么？

Answer 1

Isabelle 库中有许多在函数组合下封闭的属性示例，例如 HOLCF 和多变量分析中的连续性。它们都有一个通用的组合规则，如comp，但comp 从未在规则应用程序中使用，正是因为与%x. x 匹配。相反，只使用专门的实例，您可以使用THEN 属性获取这些实例。在您的示例中，这可能如下所示：

have "P (%x. f (g (h x)))"
  by(rule prems prems[THEN comp])+

如果您只是在寻找单个方法表达式来证明这一点，您可以利用 , 回溯，即，

have "P (%x. f (g (h x)))"
  by(rule prems|rule comp, rule prems)+

或者，您可以编写自己的 rule 或 intros 包装器，丢弃结果序列的头部。

have "P (%x. f (g (h x)))"
  apply(tactic {*
    REPEAT_FIRST (resolve_tac @{thms prems} ORELSE' 
                  (fn i => snd o Seq.chop 1 o resolve_tac @{thms comp} i))
  *})