抽象コレクションのデータ型を定義する方法は？

Question

私の理論には4種類のコレクションがあります。私はcountとfor_all操作を定義し、各コレクション型の場合：

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])" 

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))" . 

私はこれらのコレクション型のための多型事業（includesとincludes_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です。