避免匹配（λ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）

回答

相關問題