추상 콜렉션 데이터 유형을 정의하는 방법은 무엇입니까?

Question

내 이론에는 4 가지 종류의 컬렉션이 있습니다.

lift_definition mybag_includes :: "'a mybag ⇒ 'a ⇒ bool" is 
    "(λxs x. mybag_count xs x > 0)" . 

lift_definition myseq_includes :: "'a myseq ⇒ 'a ⇒ bool" is 
    "(λxs x. myseq_count xs x > 0)" . 

lift_definition myset_includes :: "'a myset ⇒ 'a ⇒ bool" is 
    "(λxs x. myset_count xs x > 0)" . 

lift_definition myord_includes :: "'a myord ⇒ 'a ⇒ bool" is 
    "(λxs x. myord_count xs x > 0)" . 


lift_definition mybag_mybag_includes_all :: "'a mybag ⇒ 'a mybag ⇒ bool" is 
    "(λxs ys. mybag_for_all ys (mybag_includes xs))" . 

lift_definition mybag_myseq_includes_all :: "'a mybag ⇒ 'a myseq ⇒ bool" is 
    "(λxs ys. myseq_for_all ys (mybag_includes xs))" . 

(* ... and 14 more similar operations for other type combinations *) 

일부 테스트 케이스 :

value "mybag_myseq_includes_all (Abs_mybag {#1::nat,2,4,5,3,4#}) (Abs_myseq [1::nat,2])" 
value "mybag_myseq_includes_all (Abs_mybag {#1::nat,2,4,5,3,4#}) (Abs_myseq [1::nat,7])" 

을 나는이 수집 종류의 다형성 작업 ( includes 및 includes_all)를 정의 할 필요가

theory MyCollections 
    imports Main 
    "~~/src/HOL/Library/Dlist" 
    "~~/src/HOL/Library/Multiset" 
begin 

typedef 'a mybag = "UNIV :: 'a multiset set" .. (* not unique, not ordered *) 
typedef 'a myseq = "UNIV :: 'a list set" ..  (* not unique, ordered *) 
typedef 'a myset = "UNIV :: 'a set set" ..  (* unique, not ordered *) 
typedef 'a myord = "UNIV :: 'a dlist set" .. (* unique, ordered *) 

setup_lifting type_definition_mybag 
setup_lifting type_definition_myseq 
setup_lifting type_definition_myset 
setup_lifting type_definition_myord 

lift_definition mybag_count :: "'a mybag ⇒ 'a ⇒ nat" is "Multiset.count" . 
lift_definition myseq_count :: "'a myseq ⇒ 'a ⇒ nat" is "count_list" . 
lift_definition myset_count :: "'a myset ⇒ 'a ⇒ nat" is "(λxs x. if x ∈ xs then 1 else 0)" . 
lift_definition myord_count :: "'a myord ⇒ 'a ⇒ nat" is "(λxs x. if Dlist.member xs x then 1 else 0)" . 

lift_definition mybag_for_all :: "'a mybag ⇒ ('a ⇒ bool) ⇒ bool" is "Multiset.Ball" . 
lift_definition myseq_for_all :: "'a myseq ⇒ ('a ⇒ bool) ⇒ bool" is "(λxs f. list_all f xs)" . 
lift_definition myset_for_all :: "'a myset ⇒ ('a ⇒ bool) ⇒ bool" is "Ball" . 
lift_definition myord_for_all :: "'a myord ⇒ ('a ⇒ bool) ⇒ bool" is "(λxs f. list_all f (list_of_dlist xs))" . 

: 각 콜렉션 유형에 대해 나는 count 및 for_all 작업을 정의

문제는 이러한 작업이 구조적으로 동일하며 t를 복제하고 싶지 않다는 것입니다. 헛기침. 나는 추상적 인 집합 유형을 정의하려고 :

typedecl 'a mycol 
consts 
    mycol_count :: "'a mycol ⇒ 'a ⇒ nat" 
    mycol_for_all :: "'a mycol ⇒ ('a ⇒ bool) ⇒ bool" 

definition mycol_includes :: "'a mycol ⇒ 'a ⇒ bool" where 
    "mycol_includes xs x ≡ mycol_count xs x > 0" 

definition mycol_includes_all :: "'a mycol ⇒ 'a mycol ⇒ bool" where 
    "mycol_includes_all xs ys ≡ mycol_for_all xs (mycol_includes ys)" 

을하지만 어떻게 추상 하나에서 구체적인 수집 유형을 도출하는 아무 생각이 :

당신은 추상 컬렉션 형식을 axiomatized하면

typedef 'a mybag = "{xs :: 'a mycol. ???}" .. 
typedef 'a myseq = "{xs :: 'a mycol. ???}" .. 
typedef 'a myset = "{xs :: 'a mycol. ???}" .. 
typedef 'a myord = "{xs :: 'a mycol. ???}" .. 

Answer 1

, 당신은 할 수 없습니다 더 이상 로직 내부로 수정하십시오. 그래서 제안 된 접근 방식은 효과가 없습니다. 그러나 컨테이너 유형을 추상적으로 (유형 변수로) 남겨두면 이것이 가능합니다. 로케일을 사용하여 그렇게하는 것이 좋습니다.

locale container = 
    fixes count :: "'container => 'a => nat" 
    and for_all :: "'container => ('a => bool) => bool" 
begin 

definition "includes" where "includes C x <--> count C x > 0" 
definition includes_all where "includes_all C C' <--> for_all C (includes C')" 

end 

그런 다음 평소와 같이 다양한 컬렉션 유형을 정의하고 로켈 해석을 통해 일반적인 작업을 얻을 수 있습니다. 예를 들어,

interpretation mybag: container mybag_count mybag_forall . 

는 약어의 mybag.includes 및 mybag.includes_all를 생성한다. 또한 로케일 container에서 증명 된 모든 정리는 mybag으로 특수화되며 접두사는 mybag입니다.