Isabelle等價於Haskell newtype嗎？

Question

我想創建一個新的數據類型形狀像一箇舊的，但（不像使用type_synonym）它應該被認爲是不同的其他理論。

我的激勵示例：我從列表中製作堆棧數據類型。我不希望我的其他理論看我stack S作爲list這麼我可以強制對我自己的簡化規則，但我已經找到了唯一的解決辦法是：

datatype 'a stk = S "'a list" 

... 

primrec index_of' :: "'a list => 'a => nat option" 
where "index_of' [] b = None" 
    | "index_of' (a # as) b = (
      if b = a then Some 0 
      else case index_of' as b of Some n => Some (Suc n) | None => None)" 

primrec index_of :: "'a stk => 'a => nat option" 
where "index_of (S as) x = index_of' as x" 

... 

lemma [simp]: "index_of' del v = Some m ==> m <= n ==> 
        index_of' (insert_at' del n v) v = Some m" 
<proof> 

lemma [simp]: "index_of del v = Some m ==> m <= n ==> 
        index_of (insert_at del n v) v = Some m" 
by (induction del, simp) 

它的工作原理，但這意味着我的理論膨脹並且充滿了過多的冗餘：每個函數都有第二個版本剝離構造函數，每個定理都有第二個版本（證明是總是by (induction del, simp)，這讓我感覺像一個符號我在某處做了太多工作）。

有沒有什麼可以幫到這裏？

Answer 1

您想使用typedef。

聲明

typedef 'a stack = "{xs :: 'a list. True}" 
    morphisms list_of_stack as_stack 
    by auto 

引入了一種新的類型，含有'a stack和'a list和一堆定理之間的所有列表，以及功能。這是他們的選擇（你可以在typedef命令後查看全部採用show_theorems）：

theorems: 
    as_stack_cases: (⋀y. ?x = as_stack y ⟹ y ∈ {xs. True} ⟹ ?P) ⟹ ?P 
    as_stack_inject: ?x ∈ {xs. True} ⟹ ?y ∈ {xs. True} ⟹ (as_stack ?x = as_stack ?y) = (?x = ?y) 
    as_stack_inverse: ?y ∈ {xs. True} ⟹ list_of_stack (as_stack ?y) = ?y 
    list_of_stack: list_of_stack ?x ∈ {xs. True} 
    list_of_stack_inject: (list_of_stack ?x = list_of_stack ?y) = (?x = ?y) 
    list_of_stack_inverse: as_stack (list_of_stack ?x) = ?x 
    type_definition_stack: type_definition list_of_stack as_stack {xs. True} 

的?x ∈ {xs. True}假設是相當枯燥這裏，但你可以在那裏指定所有列出的一個子集，例如如果你的堆棧永遠不是空的，並確保該屬性適用於所有類型的類型級別。

type_definition_stack定理與lifting包配合使用。該聲明之後

setup_lifting type_definition_stack 

您可以通過給他們的定義列表來定義的堆棧功能，並且還通過證明在清單方面的等價命題證明涉及棧定理;比手動轉換功能更容易。