如何確保類型變量的實例化不同

在Isabelle中，有沒有一種方法可以確保區域設置或命題中兩個類型變量的實例化不同？如何確保類型變量的實例化不同

對於一個具體的例子，我想推理一個複合實體沒有提交到一個具體的表示。爲此，我定義一個類成分，具有一定的操作他們：

class Component = fixes oper :: "'a ⇒ 'a"

我還定義了一個綜合，它具有相同的操作，通過將它們逐分量加選擇的組件解除：

class Composite = Component (* + ... *) 

locale ComponentAccess = 
    fixes set :: "'c :: Composite ⇒ 'a :: Component ⇒ 'c" 
    and get :: "'c ⇒ 'a" 
    assumes (* e.g. *) "get (set c a) = a" 
    and "set c (get c) = c" 
    and "oper (set c1 a1) = set (oper c1) (oper a2)"

現在我想說明一些公理成對組合，如：

locale CompositeAxioms = 
    a: ComponentAccess set get + b: ComponentAccess set' get' 
    for set :: "'c :: Composite ⇒ 'a1 :: Component ⇒ 'c" 
    and get :: "'c ⇒ 'a1" 
    and set' :: "'c ⇒ 'a2 :: Component ⇒ 'c" 
    and get' :: "'c ⇒ 'a2" + 
    assumes set_disj_commut: "set' (set c a1) a2 = set (set' c a2) a1"

然而，上述法律是唯一明智的，如果'a1和'a2被實例化爲不同類型。否則，我們平凡得難以預料的後果，如恢復組件設置：

lemma 
    fixes set get 
    assumes "CompositeAxioms set get set get" 
    shows "set (set c a1) a2 = set (set c a2) a1" 
using assms CompositeAxioms.set_disj_commut by blast

在上述地區，它的假設，是否有確保'a1和'a2總是實例化不同類型的方法嗎？

更新（說明）。其實，只有在set和set'不同的情況下，「法律」纔有意義。但是，我不得不比較兩種不同類型的函數，我認爲這是不可能的。由於我在類型類中定義了get/set操作，並使用排序約束來確保組合具有某些組件，因此我的get和set組件的類型始終不相同。因此，這個問題。

來源

2015-07-20 Ferd

您可以在Isabelle/HOL中表達兩種類型，它們通過使用類型反映作爲術語而不同。爲此，這些類型必須是可表示的，即實例化類typerep。 HOL中的大多數類型都這樣做。然後，你可以寫

TYPEREP('a) ~= TYPEREP('b)

來表達'a和'b只能被實例化不同類型。但是，TYPEREP通常僅用於內部目的（特別是在代碼生成器中），所以沒有可用的推理基礎結構，我不知道如何利用這種假設。

無論如何，我想知道爲什麼你想制定這樣的約束。如果用戶實例化您的區域CompositeAxioms，且兩個組件都相同（並且保持交換法則爲set和set'），則用戶必須顯示交換法則。如果他可以，那麼set功能有點奇怪，但健全性不受影響。此外，像TYPEREP('a) ~= TYPEREP('b)這樣的區域設置假設會不必要地限制您的開發的一般性，對set和get使用具有不同實例的相同表示類型可能是非常明智的。

來源

2015-07-21 07:44:24

安德烈亞斯，TYPEREP似乎工作，很高興知道這一點。感謝您詳細解釋爲什麼這是一個奇怪的限制。事實上，試圖確保交換不能適用於同一部件的組成部分，看起來似乎衝上去了。感謝讓我意識到這一點。 – Ferd

如何確保類型變量的實例化不同

回答

相關問題