61 |
61 |
62 lemma sub_list_empty: |
62 lemma sub_list_empty: |
63 "sub_list [] x" |
63 "sub_list [] x" |
64 by (simp add: sub_list_def) |
64 by (simp add: sub_list_def) |
65 |
65 |
66 instantiation fset :: (type) bot |
66 primrec |
|
67 finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
68 where |
|
69 "finter_raw [] l = []" |
|
70 | "finter_raw (h # t) l = |
|
71 (if memb h l then h # (finter_raw t l) else finter_raw t l)" |
|
72 |
|
73 lemma not_memb_nil: |
|
74 shows "\<not> memb x []" |
|
75 by (simp add: memb_def) |
|
76 |
|
77 lemma memb_cons_iff: |
|
78 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
|
79 by (induct xs) (auto simp add: memb_def) |
|
80 |
|
81 lemma memb_finter_raw: |
|
82 "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys" |
|
83 apply (induct xs) |
|
84 apply (simp add: not_memb_nil) |
|
85 apply (simp add: finter_raw.simps) |
|
86 apply (simp add: memb_cons_iff) |
|
87 apply auto |
|
88 done |
|
89 |
|
90 lemma [quot_respect]: |
|
91 "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw" |
|
92 by (simp add: memb_def[symmetric] memb_finter_raw) |
|
93 |
|
94 |
|
95 lemma sub_list_append_left: |
|
96 "sub_list x (x @ y)" |
|
97 by (simp add: sub_list_def) |
|
98 |
|
99 lemma sub_list_append_right: |
|
100 "sub_list y (x @ y)" |
|
101 by (simp add: sub_list_def) |
|
102 |
|
103 lemma sub_list_inter_left: |
|
104 shows "sub_list (finter_raw x y) x" |
|
105 by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) |
|
106 |
|
107 lemma sub_list_inter_right: |
|
108 shows "sub_list (finter_raw x y) y" |
|
109 by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) |
|
110 |
|
111 lemma sub_list_list_eq: |
|
112 "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y" |
|
113 unfolding sub_list_def list_eq.simps by blast |
|
114 |
|
115 lemma sub_list_append: |
|
116 "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x" |
|
117 unfolding sub_list_def by auto |
|
118 |
|
119 lemma sub_list_inter: |
|
120 "sub_list x y \<Longrightarrow> sub_list x z \<Longrightarrow> sub_list x (finter_raw y z)" |
|
121 by (simp add: sub_list_def memb_def[symmetric] memb_finter_raw) |
|
122 |
|
123 lemma append_inter_distrib: |
|
124 "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)" |
|
125 apply (induct x) |
|
126 apply simp |
|
127 apply simp |
|
128 apply (rule conjI) |
|
129 apply (simp_all add: memb_def) |
|
130 apply (simp add: memb_def[symmetric] memb_finter_raw) |
|
131 apply (simp add: memb_def) |
|
132 apply auto |
|
133 done |
|
134 |
|
135 instantiation fset :: (type) "{bot,distrib_lattice}" |
67 begin |
136 begin |
68 |
137 |
69 quotient_definition |
138 quotient_definition |
70 "bot :: 'a fset" is "[] :: 'a list" |
139 "bot :: 'a fset" is "[] :: 'a list" |
71 |
140 |
90 |
159 |
91 abbreviation |
160 abbreviation |
92 f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) |
161 f_subset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) |
93 where |
162 where |
94 "xs |\<subset>| ys \<equiv> xs < ys" |
163 "xs |\<subset>| ys \<equiv> xs < ys" |
|
164 |
|
165 quotient_definition |
|
166 "sup \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)" |
|
167 is |
|
168 "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
|
169 |
|
170 abbreviation |
|
171 funion (infixl "|\<union>|" 65) |
|
172 where |
|
173 "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys" |
|
174 |
|
175 quotient_definition |
|
176 "inf \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)" |
|
177 is |
|
178 "finter_raw \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
|
179 |
|
180 abbreviation |
|
181 finter (infixl "|\<inter>|" 65) |
|
182 where |
|
183 "xs |\<inter>| ys \<equiv> inf (xs :: 'a fset) ys" |
95 |
184 |
96 instance |
185 instance |
97 proof |
186 proof |
98 fix x y z :: "'a fset" |
187 fix x y z :: "'a fset" |
99 show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)" |
188 show "(x |\<subset>| y) = (x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x)" |
100 unfolding less_fset by (lifting sub_list_not_eq) |
189 unfolding less_fset by (lifting sub_list_not_eq) |
101 show "x |\<subseteq>| x" by (lifting sub_list_refl) |
190 show "x |\<subseteq>| x" by (lifting sub_list_refl) |
102 show "{||} |\<subseteq>| x" by (lifting sub_list_empty) |
191 show "{||} |\<subseteq>| x" by (lifting sub_list_empty) |
|
192 show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left) |
|
193 show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right) |
|
194 show "x |\<inter>| y |\<subseteq>| x" by (lifting sub_list_inter_left) |
|
195 show "x |\<inter>| y |\<subseteq>| y" by (lifting sub_list_inter_right) |
|
196 show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" by (lifting append_inter_distrib) |
103 next |
197 next |
104 fix x y z :: "'a fset" |
198 fix x y z :: "'a fset" |
105 assume a: "x |\<subseteq>| y" |
199 assume a: "x |\<subseteq>| y" |
106 assume b: "y |\<subseteq>| z" |
200 assume b: "y |\<subseteq>| z" |
107 show "x |\<subseteq>| z" using a b by (lifting sub_list_trans) |
201 show "x |\<subseteq>| z" using a b by (lifting sub_list_trans) |
108 qed |
|
109 end |
|
110 |
|
111 lemma sub_list_append_left: |
|
112 "sub_list x (x @ y)" |
|
113 by (simp add: sub_list_def) |
|
114 |
|
115 lemma sub_list_append_right: |
|
116 "sub_list y (x @ y)" |
|
117 by (simp add: sub_list_def) |
|
118 |
|
119 lemma sub_list_list_eq: |
|
120 "sub_list x y \<Longrightarrow> sub_list y x \<Longrightarrow> list_eq x y" |
|
121 unfolding sub_list_def list_eq.simps by blast |
|
122 |
|
123 lemma sub_list_append: |
|
124 "sub_list y x \<Longrightarrow> sub_list z x \<Longrightarrow> sub_list (y @ z) x" |
|
125 unfolding sub_list_def by auto |
|
126 |
|
127 instantiation fset :: (type) "semilattice_sup" |
|
128 begin |
|
129 |
|
130 quotient_definition |
|
131 "sup \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset)" |
|
132 is |
|
133 "(op @) \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> 'a list)" |
|
134 |
|
135 abbreviation |
|
136 funion (infixl "|\<union>|" 65) |
|
137 where |
|
138 "xs |\<union>| ys \<equiv> sup (xs :: 'a fset) ys" |
|
139 |
|
140 instance |
|
141 proof |
|
142 fix x y :: "'a fset" |
|
143 show "x |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_left) |
|
144 show "y |\<subseteq>| x |\<union>| y" by (lifting sub_list_append_right) |
|
145 next |
202 next |
146 fix x y :: "'a fset" |
203 fix x y :: "'a fset" |
147 assume a: "x |\<subseteq>| y" |
204 assume a: "x |\<subseteq>| y" |
148 assume b: "y |\<subseteq>| x" |
205 assume b: "y |\<subseteq>| x" |
149 show "x = y" using a b by (lifting sub_list_list_eq) |
206 show "x = y" using a b by (lifting sub_list_list_eq) |
150 next |
207 next |
151 fix x y z :: "'a fset" |
208 fix x y z :: "'a fset" |
152 assume a: "y |\<subseteq>| x" |
209 assume a: "y |\<subseteq>| x" |
153 assume b: "z |\<subseteq>| x" |
210 assume b: "z |\<subseteq>| x" |
154 show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append) |
211 show "y |\<union>| z |\<subseteq>| x" using a b by (lifting sub_list_append) |
|
212 next |
|
213 fix x y z :: "'a fset" |
|
214 assume a: "x |\<subseteq>| y" |
|
215 assume b: "x |\<subseteq>| z" |
|
216 show "x |\<subseteq>| y |\<inter>| z" using a b by (lifting sub_list_inter) |
155 qed |
217 qed |
|
218 |
156 end |
219 end |
157 |
220 |
158 section {* Empty fset, Finsert and Membership *} |
221 section {* Empty fset, Finsert and Membership *} |
159 |
222 |
160 quotient_definition |
223 quotient_definition |
195 lemma nil_not_cons: |
258 lemma nil_not_cons: |
196 shows "\<not> ([] \<approx> x # xs)" |
259 shows "\<not> ([] \<approx> x # xs)" |
197 and "\<not> (x # xs \<approx> [])" |
260 and "\<not> (x # xs \<approx> [])" |
198 by auto |
261 by auto |
199 |
262 |
200 lemma not_memb_nil: |
|
201 shows "\<not> memb x []" |
|
202 by (simp add: memb_def) |
|
203 |
|
204 lemma no_memb_nil: |
263 lemma no_memb_nil: |
205 "(\<forall>x. \<not> memb x xs) = (xs = [])" |
264 "(\<forall>x. \<not> memb x xs) = (xs = [])" |
206 by (simp add: memb_def) |
265 by (simp add: memb_def) |
207 |
266 |
208 lemma none_memb_nil: |
267 lemma none_memb_nil: |
209 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
268 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
210 by (simp add: memb_def) |
269 by (simp add: memb_def) |
211 |
|
212 lemma memb_cons_iff: |
|
213 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
|
214 by (induct xs) (auto simp add: memb_def) |
|
215 |
270 |
216 lemma memb_consI1: |
271 lemma memb_consI1: |
217 shows "memb x (x # xs)" |
272 shows "memb x (x # xs)" |
218 by (simp add: memb_def) |
273 by (simp add: memb_def) |
219 |
274 |
488 |
543 |
489 lemma [quot_respect]: |
544 lemma [quot_respect]: |
490 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
545 "(op = ===> op = ===> op \<approx> ===> op =) ffold_raw ffold_raw" |
491 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
546 by (simp add: memb_def[symmetric] ffold_raw_rsp_pre) |
492 |
547 |
493 primrec |
|
494 finter_raw :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
495 where |
|
496 "finter_raw [] l = []" |
|
497 | "finter_raw (h # t) l = |
|
498 (if memb h l then h # (finter_raw t l) else finter_raw t l)" |
|
499 |
|
500 lemma finter_raw_empty: |
548 lemma finter_raw_empty: |
501 "finter_raw l [] = []" |
549 "finter_raw l [] = []" |
502 by (induct l) (simp_all add: not_memb_nil) |
550 by (induct l) (simp_all add: not_memb_nil) |
503 |
551 |
504 lemma memb_finter_raw: |
|
505 "memb x (finter_raw xs ys) \<longleftrightarrow> memb x xs \<and> memb x ys" |
|
506 apply (induct xs) |
|
507 apply (simp add: not_memb_nil) |
|
508 apply (simp add: finter_raw.simps) |
|
509 apply (simp add: memb_cons_iff) |
|
510 apply auto |
|
511 done |
|
512 |
|
513 lemma [quot_respect]: |
|
514 "(op \<approx> ===> op \<approx> ===> op \<approx>) finter_raw finter_raw" |
|
515 by (simp add: memb_def[symmetric] memb_finter_raw) |
|
516 |
|
517 section {* Constants on the Quotient Type *} |
552 section {* Constants on the Quotient Type *} |
518 |
553 |
519 quotient_definition |
554 quotient_definition |
520 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
555 "fdelete :: 'a fset \<Rightarrow> 'a \<Rightarrow> 'a fset" |
521 is "delete_raw" |
556 is "delete_raw" |