Предоставление списка частичного заказа в Isabelle/HOLCF

Question

Я хотел бы сделать список datatype экземпляром poset из Porder.thy в HOLCF. Моя попытка выглядит следующим образом:

theory Scratch 
imports Porder Representable 
begin 

datatype 'a myList = 
    Nil | 
    Cons 'a "'a myList" 

instantiation myList :: (below) below 
begin 
    definition below_list_def: 
    "(x ⊑ y) = (case x of Nil ⇒ True | 
    Cons a xs ⇒ (case y of Nil ⇒ False | 
    Cons b ys ⇒ a ⊑ b ∧ xs ⊑ ys))" 
    instance .. 
end 

Я понимаю, что «определение» не поддерживает рекурсивное определение я использую, и я должен использовать что-то вроде «удовольствие» или «fixrec». Однако я не знаю, как использовать эти команды в этом контексте. Каждый пример, который я нашел в Интернете для создания экземпляра po, использует нерекурсивный тип данных. Каков наилучший способ сделать рекурсивный тип данных экземпляром ниже и po?

Answer 1

В этом локальном контексте вы можете использовать fun, вы должны просто указать ему правильное имя, то есть имя функции, суффикс которой «_» и имя типа экземпляра, в данном случае below_myList.

Тогда ваш пример переписывает на:

instantiation myList :: (below) below 
begin 
    fun below_myList where 
    "Nil ⊑ xs = True" 
    | "Cons x xs ⊑ Nil = False" 
    | "Cons x xs ⊑ Cons y ys = (x ⊑ y ∧ xs ⊑ ys)" 
    instance .. 
end 

lemma "Nil ⊑ Nil" 
    by simp