Isabelle/HOLCF에서 부분 순서를 부여

Question

HOLCF의 Porder.thy에서 poset의 인스턴스를 list 데이터 유형으로 만들고 싶습니다. 다음과 같이 나의 시도는 다음과 같습니다

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