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 

您可以通过给他们的定义列表来定义的堆栈功能，并且还通过证明在清单方面的等价命题证明涉及栈定理;比手动转换功能更容易。