Есть ли эквивалент Изабеллы для нового типа Haskell?

Question

Я хочу создать новый тип данных, похожий на старый, но (в отличие от type_synonym) он должен быть распознан как отдельный в других теориях.

Мой мотивирующий пример: я делаю стековый тип данных из списков. Я не хочу, чтобы мои другие теории, чтобы увидеть мои stack с, как 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) 

Он работает, но это означает, что моя теория stack раздута и заполнена слишком избыточным избытком: каждая функция имеет вторую версию, отключающую конструктор, и каждая теорема имеет вторую версию (для которой доказательство всегда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 и кучей теорем. Вот выбор из них (вы можете просмотреть все с помощью show_theorems после команды typedef):

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 

вы можете определить функции на стеки, давая свое определение в терминах списков, а также доказательства теорем, связанных с стеки, доказав их эквивалентное утверждение в терминах списков; намного проще, чем ручное манипулирование функциями преобразования.