1

考虑理论

理论从头开始导入主要
开始

记事本
开始
  修复 P 和 fgh :: "int ⇒ int"
  假设前提：“P f”“P g”“P h”
  假设 comp: "⋀ f g. P f ⟹ P g ⟹ P (λ x. f (gx))"

  有“P(λx.f(g(hx)))”
    对不起
结尾
结尾

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

by (intro prems comp)

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

我知道这是rule代表的有效行为。intro. 然而，从实用的角度来看，我经常遇到简化或引入规则，这些规则在它们匹配的所有情况下都非常有用，除非它们匹配(λx. x)。

有什么办法可以comp说明 Isabelle 的匹配器不会考虑 where for gis的解决方案(λx. x)？

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

4

1 回答 1

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))
  *})
于 2014-05-15T09:28:14.157 回答