避免匹配（λx.x）

考虑理论避免匹配（λx.x）

 
theory Scratch imports Main 
begin 

notepad 
begin 
    fix P and f g h :: "int ⇒ int" 
    assume prems: "P f" "P g" "P h" 
    assume comp: "⋀ f g. P f ⟹ P g ⟹ P (λ x. f (g x))" 

    have "P (λ x. f (g (h x)))" 
    sorry 
end 
end

显然引理可以从prems和comp显示。实际上，乍看之下，人们可以预料，它可以通过

by (intro prems comp)

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

我知道这是rule代表的有效行为。 intro。尽管如此，从务实的角度来看，我经常会遇到简化或引入规则，在与匹配的所有情况下，除匹配(λx. x)之外，这些规则都会非常有用。

有什么办法陈述comp让伊莎贝尔的匹配将不考虑一个解决方案，f或g是(λx. x)？

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

来源

2014-05-15 Joachim Breitner

在函数构成下的Isabelle属性库中有很多例子，例如HOLCF和Multivariate-Analysis中的连续性。它们都有一个通用组合规则，如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-15 09:28:14

HOLCF的连续性当然是我激励的例子。但是，如果有很多例子，那么我的第二个问题变得更加相关：为什么我们不能有一种不匹配'λx的方法。 x'？或者（也许更骇人听闻），如果第一个结果的目标没有在场所中修改，为什么不能'规则'回溯。 –

避免匹配（λx.x）

回答

相关问题