如何使用證明現場演繹的目標來證明其餘的

我定義了一個嚴格的順序語言環境如下：如何使用證明現場演繹的目標來證明其餘的

locale strict_order = 
fixes ls::"'a set ⇒ 'a set ⇒ bool" 
assumes 
    irrefl:"¬ ls a a" and 
    trans:"ls a c ∧ ls c g ⟹ ls a g" and 
    asym:"ls a c ⟹ ¬ ls c a"

然後，我宣佈一個類型strict_order

interpretation nest:strict_order "op ≪" 
proof 
fix a 
show "¬ a ≪ a" 
proof (rule contra, auto) 
    .... 
qed 
next 
fix a c g 
assume a:"a ≪ c ∧ c ≪ g" 
show " a ≪ g" 
proof - 
    (* uses the fact that ¬ a<<a *)

的解釋類型嵌套的證明「trans」屬性需要在解釋塊內部已經成功證明的某個「irrefl」屬性。我如何標籤和使用它？或者沒有辦法，只能將它移到解釋塊之外？

謝謝。

來源

2016-03-03 Faddou

安德烈亞斯ninja'd我，但這裏是我有兩個其他備註：1.'LS是C∧LS C G⟹LS一g'表達得更慣用爲'LS是C⟹LS C G⟹LS一個g'。這兩個語句在邏輯上是等價的，但是如果你做Isar證明或者想用OF來實例化這個定理，那麼第二個語句在Isabelle中更容易使用。 –

2.我在'show'語句的''a __「''中得到了'引入的固定類型變量：''b'的警告，所以你可能也會這樣做。發生這種情況時，爲固定變量提供顯式類型是一個好主意。要做到這一點，你可以在解釋中用'op«::'一套⇒_'替換你的'op«'，然後用'fix a ::''set'替換你的'fix a'''等等 –

你說得對，需要固定變量的類型。謝謝。 – Faddou

如果您使用show陳述事實，則可以將其命名爲have，例如show irrefl: "¬ a ≪ a"。但是，next會丟棄您迄今爲止證明的所有內容，因此您必須避免next。在概念上，接下來對應於關閉塊並打開新塊，即next實質上意味着} {。因此，你可以寫類似以下內容：

請注意，您只能關閉該塊後命名irreflexivity法，因爲你想要的固定a被推廣，這隻能從塊導出時發生。如果您使用的是Isabelle2016或更高版本，則可以使用for和if子句更簡潔地編寫案例。這爲您節省了所有樣板}和{。

proof 
    show irrefl: "¬ a ≪ a" for a 
    proof (rule contra, auto) .... qed 

    show "a ≪ g" if a: "a ≪ c ∧ c ≪ g" for a c g 
    proof - ... (* can reference irrefl *) qed 
qed

來源

2016-03-03 07:13:42

非常感謝。當下一個被移除時，它就像一個魅力。 – Faddou

如何使用證明現場演繹的目標來證明其餘的

回答

相關問題