43146
|
1 |
(* Author: Florian Haftmann, TU Muenchen *)
|
|
2 |
|
|
3 |
header {* Canonical implementation of sets by distinct lists *}
|
|
4 |
|
|
5 |
theory Dlist_Cset
|
43241
|
6 |
imports Dlist List_Cset
|
43146
|
7 |
begin
|
|
8 |
|
|
9 |
definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
|
43241
|
10 |
"Set dxs = List_Cset.set (list_of_dlist dxs)"
|
43146
|
11 |
|
|
12 |
definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
|
43241
|
13 |
"Coset dxs = List_Cset.coset (list_of_dlist dxs)"
|
43146
|
14 |
|
|
15 |
code_datatype Set Coset
|
|
16 |
|
|
17 |
declare member_code [code del]
|
43241
|
18 |
declare List_Cset.is_empty_set [code del]
|
|
19 |
declare List_Cset.empty_set [code del]
|
|
20 |
declare List_Cset.UNIV_set [code del]
|
43146
|
21 |
declare insert_set [code del]
|
|
22 |
declare remove_set [code del]
|
|
23 |
declare compl_set [code del]
|
|
24 |
declare compl_coset [code del]
|
|
25 |
declare map_set [code del]
|
|
26 |
declare filter_set [code del]
|
|
27 |
declare forall_set [code del]
|
|
28 |
declare exists_set [code del]
|
|
29 |
declare card_set [code del]
|
|
30 |
declare inter_project [code del]
|
|
31 |
declare subtract_remove [code del]
|
|
32 |
declare union_insert [code del]
|
|
33 |
declare Infimum_inf [code del]
|
|
34 |
declare Supremum_sup [code del]
|
|
35 |
|
|
36 |
lemma Set_Dlist [simp]:
|
|
37 |
"Set (Dlist xs) = Cset.Set (set xs)"
|
|
38 |
by (rule Cset.set_eqI) (simp add: Set_def)
|
|
39 |
|
|
40 |
lemma Coset_Dlist [simp]:
|
|
41 |
"Coset (Dlist xs) = Cset.Set (- set xs)"
|
|
42 |
by (rule Cset.set_eqI) (simp add: Coset_def)
|
|
43 |
|
|
44 |
lemma member_Set [simp]:
|
|
45 |
"Cset.member (Set dxs) = List.member (list_of_dlist dxs)"
|
|
46 |
by (simp add: Set_def member_set)
|
|
47 |
|
|
48 |
lemma member_Coset [simp]:
|
|
49 |
"Cset.member (Coset dxs) = Not \<circ> List.member (list_of_dlist dxs)"
|
|
50 |
by (simp add: Coset_def member_set not_set_compl)
|
|
51 |
|
|
52 |
lemma Set_dlist_of_list [code]:
|
43241
|
53 |
"List_Cset.set xs = Set (dlist_of_list xs)"
|
43146
|
54 |
by (rule Cset.set_eqI) simp
|
|
55 |
|
|
56 |
lemma Coset_dlist_of_list [code]:
|
43241
|
57 |
"List_Cset.coset xs = Coset (dlist_of_list xs)"
|
43146
|
58 |
by (rule Cset.set_eqI) simp
|
|
59 |
|
|
60 |
lemma is_empty_Set [code]:
|
|
61 |
"Cset.is_empty (Set dxs) \<longleftrightarrow> Dlist.null dxs"
|
|
62 |
by (simp add: Dlist.null_def List.null_def member_set)
|
|
63 |
|
|
64 |
lemma bot_code [code]:
|
|
65 |
"bot = Set Dlist.empty"
|
|
66 |
by (simp add: empty_def)
|
|
67 |
|
|
68 |
lemma top_code [code]:
|
|
69 |
"top = Coset Dlist.empty"
|
|
70 |
by (simp add: empty_def)
|
|
71 |
|
|
72 |
lemma insert_code [code]:
|
|
73 |
"Cset.insert x (Set dxs) = Set (Dlist.insert x dxs)"
|
|
74 |
"Cset.insert x (Coset dxs) = Coset (Dlist.remove x dxs)"
|
|
75 |
by (simp_all add: Dlist.insert_def Dlist.remove_def member_set not_set_compl)
|
|
76 |
|
|
77 |
lemma remove_code [code]:
|
|
78 |
"Cset.remove x (Set dxs) = Set (Dlist.remove x dxs)"
|
|
79 |
"Cset.remove x (Coset dxs) = Coset (Dlist.insert x dxs)"
|
|
80 |
by (auto simp add: Dlist.insert_def Dlist.remove_def member_set not_set_compl)
|
|
81 |
|
|
82 |
lemma member_code [code]:
|
|
83 |
"Cset.member (Set dxs) = Dlist.member dxs"
|
|
84 |
"Cset.member (Coset dxs) = Not \<circ> Dlist.member dxs"
|
|
85 |
by (simp_all add: member_def)
|
|
86 |
|
|
87 |
lemma compl_code [code]:
|
|
88 |
"- Set dxs = Coset dxs"
|
|
89 |
"- Coset dxs = Set dxs"
|
|
90 |
by (rule Cset.set_eqI, simp add: member_set not_set_compl)+
|
|
91 |
|
|
92 |
lemma map_code [code]:
|
|
93 |
"Cset.map f (Set dxs) = Set (Dlist.map f dxs)"
|
|
94 |
by (rule Cset.set_eqI) (simp add: member_set)
|
|
95 |
|
|
96 |
lemma filter_code [code]:
|
|
97 |
"Cset.filter f (Set dxs) = Set (Dlist.filter f dxs)"
|
|
98 |
by (rule Cset.set_eqI) (simp add: member_set)
|
|
99 |
|
|
100 |
lemma forall_Set [code]:
|
|
101 |
"Cset.forall P (Set xs) \<longleftrightarrow> list_all P (list_of_dlist xs)"
|
|
102 |
by (simp add: member_set list_all_iff)
|
|
103 |
|
|
104 |
lemma exists_Set [code]:
|
|
105 |
"Cset.exists P (Set xs) \<longleftrightarrow> list_ex P (list_of_dlist xs)"
|
|
106 |
by (simp add: member_set list_ex_iff)
|
|
107 |
|
|
108 |
lemma card_code [code]:
|
|
109 |
"Cset.card (Set dxs) = Dlist.length dxs"
|
|
110 |
by (simp add: length_def member_set distinct_card)
|
|
111 |
|
|
112 |
lemma inter_code [code]:
|
|
113 |
"inf A (Set xs) = Set (Dlist.filter (Cset.member A) xs)"
|
|
114 |
"inf A (Coset xs) = Dlist.foldr Cset.remove xs A"
|
|
115 |
by (simp_all only: Set_def Coset_def foldr_def inter_project list_of_dlist_filter)
|
|
116 |
|
|
117 |
lemma subtract_code [code]:
|
|
118 |
"A - Set xs = Dlist.foldr Cset.remove xs A"
|
|
119 |
"A - Coset xs = Set (Dlist.filter (Cset.member A) xs)"
|
|
120 |
by (simp_all only: Set_def Coset_def foldr_def subtract_remove list_of_dlist_filter)
|
|
121 |
|
|
122 |
lemma union_code [code]:
|
|
123 |
"sup (Set xs) A = Dlist.foldr Cset.insert xs A"
|
|
124 |
"sup (Coset xs) A = Coset (Dlist.filter (Not \<circ> Cset.member A) xs)"
|
|
125 |
by (simp_all only: Set_def Coset_def foldr_def union_insert list_of_dlist_filter)
|
|
126 |
|
|
127 |
context complete_lattice
|
|
128 |
begin
|
|
129 |
|
|
130 |
lemma Infimum_code [code]:
|
|
131 |
"Infimum (Set As) = Dlist.foldr inf As top"
|
|
132 |
by (simp only: Set_def Infimum_inf foldr_def inf.commute)
|
|
133 |
|
|
134 |
lemma Supremum_code [code]:
|
|
135 |
"Supremum (Set As) = Dlist.foldr sup As bot"
|
|
136 |
by (simp only: Set_def Supremum_sup foldr_def sup.commute)
|
|
137 |
|
|
138 |
end
|
|
139 |
|
|
140 |
end
|