如何聲明一個不尊重排序約束的引理（使用OFCLASS）

Question

我該如何聲明Isabelle/HOL中不遵守排序約束的引理？

要解釋爲什麼這是有道理的，請看下面的例子理論：

theory Test 
imports Main 
begin 

class embeddable = 
    fixes embedding::"'a ⇒ nat" 
    assumes "inj embedding" 

lemma OFCLASS_I: 
    assumes "inj (embedding::'a⇒_)" 
    shows "OFCLASS('a::type,embeddable_class)" 
apply intro_classes by (fact assms) 

instantiation nat :: embeddable begin 
definition "embedding = id" 
instance 
    apply (rule OFCLASS_I) unfolding embedding_nat_def by simp 
end 

end 

這種理論定義了一個類型的類「嵌入」用一個類型參數「嵌入」。 （基本上，可嵌入類通過明確枚舉來表徵可數數字，但我選擇這只是一個非常簡單的例子。）

爲了簡化類型類的實例驗證，理論指出了一個輔助引理OFCLASS_I，它顯示目標的形式OFCLASS(...,embeddable)。這個引理可以用來解決instance產生的證明義務。

首先，我爲什麼要這麼做？ （在本理論，apply (rule OFCLASS_I)確實相同內建apply intro_classes，因此是無用的。）在更復雜的情況下，有兩個原因這樣的引理：

• 該引理可以給替代標準的一個實例類型的類，使後續的證明更簡單。
• 引理可用於自動化（ML級）實例。這裏使用intro_classes是有問題的，因爲intro_classes的子目標數量可能會根據之前執行的實例證明而有所不同。 （A引理如OFCLASS_I具有穩定的，良好控制的子目標。）

然而，上述理論沒有在伊莎貝爾/ HOL（均未2015或2016-RC1）工作，因爲引理不類型檢查。排序約束「embedding ::（_ :: embeddable => _）」不滿足。然而，這種類型的限制並不是邏輯必然性（它不是由邏輯內核強制執行，而是由更高級別執行）。

那麼，有沒有一種清楚的陳述上述理論的方法？ （我在答案中給出了一個稍微難看的解決方案，但我正在尋找更清潔的東西。）

Answer 1

以下是一個不同的解決方案，在證明引理之後不需要「清理」（this answer需要「修復」之後的排序約束）。

的思想是定義一個新的常數（embedding_UNCONSTRAINED在我的例子），其的一個副本的原始排序約束常數（embedding），除了沒有排序約束（使用下面的local_setup命令）。然後引理使用embedding_UNCONSTRAINED而不是embedding陳述。但通過添加屬性[unfolded embedding_UNCONSTRAINED_def]實際存儲的引理使用常量embedding沒有排序約束。

這種方法的缺點是，在引理的證明過程中，我們永遠不能明確地寫出包含embedding的任何術語（因爲這會增加不需要的排序約束）。但是如果我們需要聲明一個包含embedding的子目標，我們可以始終使用embedding_UNCONSTRAINED來表示它，然後使用例如unfolding embedding_UNCONSTRAINED將其轉換爲embedding。

theory Test 
imports Main 
begin 

class embeddable = 
    fixes embedding::"'a ⇒ nat" 
    assumes "inj embedding" 

(* This does roughly: 
    definition "embedding_UNCONSTRAINED == (embedding::('a::type)=>nat)" *) 
local_setup {* 
    Local_Theory.define ((@{binding embedding_UNCONSTRAINED},NoSyn),((@{binding embedding_UNCONSTRAINED_def},[]), 
     Const(@{const_name embedding},@{typ "'a ⇒ nat"}))) #> snd 
*} 

lemma OFCLASS_I [unfolded embedding_UNCONSTRAINED_def]: 
    assumes "inj (embedding_UNCONSTRAINED::'a⇒_)" 
    shows "OFCLASS('a::type,embeddable_class)" 
apply intro_classes by (fact assms[unfolded embedding_UNCONSTRAINED_def]) 

thm OFCLASS_I (* The theorem now uses "embedding", but without sort "embeddable" *) 

instantiation nat :: embeddable begin 
definition "embedding = id" 
instance 
    apply (rule OFCLASS_I) unfolding embedding_nat_def by simp 
end 

end 

Answer 2

可以在ML級別暫時禁用排序約束的檢查，然後再重新激活。 （請參閱下面的完整示例。）但是，該解決方案看起來非常像黑客。我們必須改變上下文中的排序約束，並記住在之後恢復它們。

theory Test 
imports Main 
begin 

class embeddable = 
    fixes embedding::"'a ⇒ nat" 
    assumes "inj embedding" 

ML {* 
    val consts_to_unconstrain = [@{const_name embedding}] 
    val consts_orig_constraints = map (Sign.the_const_constraint 
           @{theory}) consts_to_unconstrain 
*} 
setup {* 
    fold (fn c => fn thy => Sign.add_const_constraint (c,NONE) thy) consts_to_unconstrain 
*} 

lemma OFCLASS_I: 
    assumes "inj (embedding::'a⇒_)" 
    shows "OFCLASS('a::type,embeddable_class)" 
apply intro_classes by (fact assms) 

(* Recover stored type constraints *) 
setup {* 
    fold2 (fn c => fn T => fn thy => Sign.add_const_constraint 
      (c,SOME (Logic.unvarifyT_global T)) thy) 
       consts_to_unconstrain consts_orig_constraints 
*} 

instantiation nat :: embeddable begin 
definition "embedding = id" 
instance 
    apply (rule OFCLASS_I) unfolding embedding_nat_def by simp 
end 

end 

這個理論被Isabelle/HOL接受。該方法在更復雜的設置中工作（我已經使用過幾次），但我更喜歡更優雅的設置。