1 (* Title: HOL/Quotient_Examples/FSet.thy |
1 (* Title: HOL/Quotient_Examples/FSet.thy |
2 Author: Cezary Kaliszyk, TU Munich |
2 Author: Cezary Kaliszyk, TU Munich |
3 Author: Christian Urban, TU Munich |
3 Author: Christian Urban, TU Munich |
4 |
4 |
5 A reasoning infrastructure for the type of finite sets. |
5 Type of finite sets. |
6 *) |
6 *) |
7 |
7 |
8 theory FSet |
8 theory FSet |
9 imports Quotient_List |
9 imports Quotient_List |
10 begin |
10 begin |
11 |
11 |
12 text {* Definiton of List relation and the quotient type *} |
12 text {* Definiton of the list equivalence relation *} |
13 |
13 |
14 fun |
14 fun |
15 list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50) |
15 list_eq :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" (infix "\<approx>" 50) |
16 where |
16 where |
17 "list_eq xs ys = (set xs = set ys)" |
17 "list_eq xs ys = (set xs = set ys)" |
20 shows "equivp list_eq" |
20 shows "equivp list_eq" |
21 unfolding equivp_reflp_symp_transp |
21 unfolding equivp_reflp_symp_transp |
22 unfolding reflp_def symp_def transp_def |
22 unfolding reflp_def symp_def transp_def |
23 by auto |
23 by auto |
24 |
24 |
|
25 text {* Fset type *} |
|
26 |
25 quotient_type |
27 quotient_type |
26 'a fset = "'a list" / "list_eq" |
28 'a fset = "'a list" / "list_eq" |
27 by (rule list_eq_equivp) |
29 by (rule list_eq_equivp) |
28 |
30 |
29 text {* Raw definitions of membership, sublist, cardinality, |
31 text {* |
30 intersection |
32 Definitions of membership, sublist, cardinality, |
|
33 intersection etc over lists |
31 *} |
34 *} |
32 |
35 |
33 definition |
36 definition |
34 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
37 memb :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" |
35 where |
38 where |
71 (if (rsp_fold f) then |
81 (if (rsp_fold f) then |
72 if a \<in> set xs then ffold_raw f z xs |
82 if a \<in> set xs then ffold_raw f z xs |
73 else f a (ffold_raw f z xs) |
83 else f a (ffold_raw f z xs) |
74 else z)" |
84 else z)" |
75 |
85 |
76 text {* Composition Quotient *} |
86 |
|
87 |
|
88 lemma set_finter_raw[simp]: |
|
89 shows "set (finter_raw xs ys) = set xs \<inter> set ys" |
|
90 by (induct xs) (auto simp add: memb_def) |
|
91 |
|
92 lemma set_fminus_raw[simp]: |
|
93 shows "set (fminus_raw xs ys) = (set xs - set ys)" |
|
94 by (induct ys arbitrary: xs) (auto) |
|
95 |
|
96 |
|
97 |
|
98 section {* Quotient composition lemmas *} |
77 |
99 |
78 lemma list_all2_refl1: |
100 lemma list_all2_refl1: |
79 shows "(list_all2 op \<approx>) r r" |
101 shows "(list_all2 op \<approx>) r r" |
80 by (rule list_all2_refl) (metis equivp_def fset_equivp) |
102 by (rule list_all2_refl) (metis equivp_def fset_equivp) |
81 |
103 |
149 using a c pred_compI by simp |
171 using a c pred_compI by simp |
150 qed |
172 qed |
151 qed |
173 qed |
152 |
174 |
153 |
175 |
154 lemma set_finter_raw[simp]: |
|
155 "set (finter_raw xs ys) = set xs \<inter> set ys" |
|
156 by (induct xs) (auto simp add: memb_def) |
|
157 |
|
158 lemma set_fminus_raw[simp]: |
|
159 "set (fminus_raw xs ys) = (set xs - set ys)" |
|
160 by (induct ys arbitrary: xs) (auto) |
|
161 |
|
162 |
|
163 text {* Respectfulness *} |
176 text {* Respectfulness *} |
164 |
177 |
165 lemma append_rsp[quot_respect]: |
178 lemma append_rsp[quot_respect]: |
166 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append" |
179 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) append append" |
167 by (simp) |
180 by simp |
168 |
181 |
169 lemma sub_list_rsp[quot_respect]: |
182 lemma sub_list_rsp[quot_respect]: |
170 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
183 shows "(op \<approx> ===> op \<approx> ===> op =) sub_list sub_list" |
171 by (auto simp add: sub_list_def) |
184 by (auto simp add: sub_list_def) |
172 |
185 |
208 |
221 |
209 lemma fcard_raw_rsp[quot_respect]: |
222 lemma fcard_raw_rsp[quot_respect]: |
210 shows "(op \<approx> ===> op =) fcard_raw fcard_raw" |
223 shows "(op \<approx> ===> op =) fcard_raw fcard_raw" |
211 by (simp add: fcard_raw_def) |
224 by (simp add: fcard_raw_def) |
212 |
225 |
213 |
|
214 |
|
215 lemma not_memb_nil: |
|
216 shows "\<not> memb x []" |
|
217 by (simp add: memb_def) |
|
218 |
|
219 lemma memb_cons_iff: |
|
220 shows "memb x (y # xs) = (x = y \<or> memb x xs)" |
|
221 by (induct xs) (auto simp add: memb_def) |
|
222 |
|
223 lemma memb_absorb: |
|
224 shows "memb x xs \<Longrightarrow> x # xs \<approx> xs" |
|
225 by (induct xs) (auto simp add: memb_def) |
|
226 |
|
227 lemma none_memb_nil: |
|
228 "(\<forall>x. \<not> memb x xs) = (xs \<approx> [])" |
|
229 by (simp add: memb_def) |
|
230 |
226 |
231 |
227 |
232 lemma memb_commute_ffold_raw: |
228 lemma memb_commute_ffold_raw: |
233 "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))" |
229 "rsp_fold f \<Longrightarrow> h \<in> set b \<Longrightarrow> ffold_raw f z b = f h (ffold_raw f z (removeAll h b))" |
234 apply (induct b) |
230 apply (induct b) |
300 |
296 |
301 lemma [quot_respect]: |
297 lemma [quot_respect]: |
302 shows "(op = ===> op \<approx> ===> op \<approx>) filter filter" |
298 shows "(op = ===> op \<approx> ===> op \<approx>) filter filter" |
303 by auto |
299 by auto |
304 |
300 |
305 text {* Distributive lattice with bot *} |
301 |
306 |
302 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" |
307 lemma append_inter_distrib: |
303 begin |
|
304 |
|
305 quotient_definition |
|
306 "bot :: 'a fset" is "[] :: 'a list" |
|
307 |
|
308 abbreviation |
|
309 fempty ("{||}") |
|
310 where |
|
311 "{||} \<equiv> bot :: 'a fset" |
|
312 |
|
313 quotient_definition |
|
314 "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)" |
|
315 is |
|
316 "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" |
|
317 |
|
318 abbreviation |
|
319 f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) |
|
320 where |
|
321 "xs |\<subseteq>| ys \<equiv> xs \<le> ys" |
|
322 |
|
323 definition |
|
324 less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" |
|
325 where |
|
326 "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)" |
|
327 |
|
328 abbreviation |
|
329 fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) |
|
330 where |
|
331 "xs |\<subset>| ys \<equiv> xs < ys" |
|
332 |
|
333 quotient_definition |
|
334 "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
335 is |
|
336 "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
337 |
|
338 abbreviation |
|
339 funion (infixl "|\<union>|" 65) |
|
340 where |
|
341 "xs |\<union>| ys \<equiv> sup xs (ys::'a fset)" |
|
342 |
|
343 quotient_definition |
|
344 "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
345 is |
|
346 "finter_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
347 |
|
348 abbreviation |
|
349 finter (infixl "|\<inter>|" 65) |
|
350 where |
|
351 "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)" |
|
352 |
|
353 quotient_definition |
|
354 "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
355 is |
|
356 "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
357 |
|
358 lemma append_finter_raw_distrib: |
308 "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)" |
359 "x @ (finter_raw y z) \<approx> finter_raw (x @ y) (x @ z)" |
309 apply (induct x) |
360 apply (induct x) |
310 apply (auto) |
361 apply (auto) |
311 done |
362 done |
312 |
|
313 instantiation fset :: (type) "{bounded_lattice_bot, distrib_lattice, minus}" |
|
314 begin |
|
315 |
|
316 quotient_definition |
|
317 "bot :: 'a fset" is "[] :: 'a list" |
|
318 |
|
319 abbreviation |
|
320 fempty ("{||}") |
|
321 where |
|
322 "{||} \<equiv> bot :: 'a fset" |
|
323 |
|
324 quotient_definition |
|
325 "less_eq_fset \<Colon> ('a fset \<Rightarrow> 'a fset \<Rightarrow> bool)" |
|
326 is |
|
327 "sub_list \<Colon> ('a list \<Rightarrow> 'a list \<Rightarrow> bool)" |
|
328 |
|
329 abbreviation |
|
330 f_subset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subseteq>|" 50) |
|
331 where |
|
332 "xs |\<subseteq>| ys \<equiv> xs \<le> ys" |
|
333 |
|
334 definition |
|
335 less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" |
|
336 where |
|
337 "xs < ys \<equiv> xs \<le> ys \<and> xs \<noteq> (ys::'a fset)" |
|
338 |
|
339 abbreviation |
|
340 fsubset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<subset>|" 50) |
|
341 where |
|
342 "xs |\<subset>| ys \<equiv> xs < ys" |
|
343 |
|
344 quotient_definition |
|
345 "sup :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
346 is |
|
347 "append :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
348 |
|
349 abbreviation |
|
350 funion (infixl "|\<union>|" 65) |
|
351 where |
|
352 "xs |\<union>| ys \<equiv> sup xs (ys::'a fset)" |
|
353 |
|
354 quotient_definition |
|
355 "inf :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
356 is |
|
357 "finter_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
358 |
|
359 abbreviation |
|
360 finter (infixl "|\<inter>|" 65) |
|
361 where |
|
362 "xs |\<inter>| ys \<equiv> inf xs (ys::'a fset)" |
|
363 |
|
364 quotient_definition |
|
365 "minus :: 'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
|
366 is |
|
367 "fminus_raw :: 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
368 |
363 |
369 instance |
364 instance |
370 proof |
365 proof |
371 fix x y z :: "'a fset" |
366 fix x y z :: "'a fset" |
372 show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x" |
367 show "x |\<subset>| y \<longleftrightarrow> x |\<subseteq>| y \<and> \<not> y |\<subseteq>| x" |
379 show "x |\<inter>| y |\<subseteq>| x" |
374 show "x |\<inter>| y |\<subseteq>| x" |
380 by (descending) (simp add: sub_list_def memb_def[symmetric]) |
375 by (descending) (simp add: sub_list_def memb_def[symmetric]) |
381 show "x |\<inter>| y |\<subseteq>| y" |
376 show "x |\<inter>| y |\<subseteq>| y" |
382 by (descending) (simp add: sub_list_def memb_def[symmetric]) |
377 by (descending) (simp add: sub_list_def memb_def[symmetric]) |
383 show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" |
378 show "x |\<union>| (y |\<inter>| z) = x |\<union>| y |\<inter>| (x |\<union>| z)" |
384 by (descending) (rule append_inter_distrib) |
379 by (descending) (rule append_finter_raw_distrib) |
385 next |
380 next |
386 fix x y z :: "'a fset" |
381 fix x y z :: "'a fset" |
387 assume a: "x |\<subseteq>| y" |
382 assume a: "x |\<subseteq>| y" |
388 assume b: "y |\<subseteq>| z" |
383 assume b: "y |\<subseteq>| z" |
389 show "x |\<subseteq>| z" using a b |
384 show "x |\<subseteq>| z" using a b |
593 lemma memb_card_not_0: |
588 lemma memb_card_not_0: |
594 assumes a: "memb a A" |
589 assumes a: "memb a A" |
595 shows "\<not>(fcard_raw A = 0)" |
590 shows "\<not>(fcard_raw A = 0)" |
596 proof - |
591 proof - |
597 have "\<not>(\<forall>x. \<not> memb x A)" using a by auto |
592 have "\<not>(\<forall>x. \<not> memb x A)" using a by auto |
598 then have "\<not>A \<approx> []" using none_memb_nil[of A] by simp |
593 then have "\<not>A \<approx> []" by (simp add: memb_def) |
599 then show ?thesis using fcard_raw_0[of A] by simp |
594 then show ?thesis using fcard_raw_0[of A] by simp |
600 qed |
595 qed |
601 |
596 |
602 |
597 |
603 |
598 |
604 section {* fmap *} |
599 section {* ? *} |
605 |
600 |
606 (* there is another fmap section below *) |
|
607 |
|
608 lemma map_append: |
|
609 "map f (xs @ ys) \<approx> (map f xs) @ (map f ys)" |
|
610 by simp |
|
611 |
|
612 lemma memb_append: |
|
613 "memb x (xs @ ys) \<longleftrightarrow> memb x xs \<or> memb x ys" |
|
614 by (induct xs) (simp_all add: not_memb_nil memb_cons_iff) |
|
615 |
601 |
616 lemma fset_raw_strong_cases: |
602 lemma fset_raw_strong_cases: |
617 obtains "xs = []" |
603 obtains "xs = []" |
618 | x ys where "\<not> memb x ys" and "xs \<approx> x # ys" |
604 | x ys where "\<not> memb x ys" and "xs \<approx> x # ys" |
619 proof (induct xs arbitrary: x ys) |
605 proof (induct xs arbitrary: x ys) |
685 lemma cons_delete_list_eq2: |
671 lemma cons_delete_list_eq2: |
686 shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)" |
672 shows "list_eq2 (a # (removeAll a A)) (if memb a A then A else a # A)" |
687 apply (induct A) |
673 apply (induct A) |
688 apply (simp add: memb_def list_eq2_refl) |
674 apply (simp add: memb_def list_eq2_refl) |
689 apply (case_tac "memb a (aa # A)") |
675 apply (case_tac "memb a (aa # A)") |
690 apply (simp_all only: memb_cons_iff) |
676 apply (simp_all only: memb_def) |
691 apply (case_tac [!] "a = aa") |
677 apply (case_tac [!] "a = aa") |
692 apply (simp_all) |
678 apply (simp_all) |
693 apply (case_tac "memb a A") |
679 apply (case_tac "memb a A") |
694 apply (auto simp add: memb_def)[2] |
680 apply (auto simp add: memb_def)[2] |
695 apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
681 apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6)) |
783 |
769 |
784 text {* fset *} |
770 text {* fset *} |
785 |
771 |
786 lemma fset_simps[simp]: |
772 lemma fset_simps[simp]: |
787 "fset {||} = ({} :: 'a set)" |
773 "fset {||} = ({} :: 'a set)" |
788 "fset (finsert (h :: 'a) t) = insert h (fset t)" |
774 "fset (finsert (x :: 'a) S) = insert x (fset S)" |
789 by (lifting set.simps) |
775 by (lifting set.simps) |
790 |
776 |
791 lemma in_fset: |
777 lemma fin_fset: |
792 "x \<in> fset S \<equiv> x |\<in>| S" |
778 "x \<in> fset S \<longleftrightarrow> x |\<in>| S" |
793 by (lifting memb_def[symmetric]) |
779 by (lifting memb_def[symmetric]) |
794 |
780 |
795 lemma none_fin_fempty: |
781 lemma none_fin_fempty: |
796 "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}" |
782 "(\<forall>x. x |\<notin>| S) \<longleftrightarrow> S = {||}" |
797 by (lifting none_memb_nil) |
783 by (descending) (simp add: memb_def) |
798 |
784 |
799 lemma fset_cong: |
785 lemma fset_cong: |
800 "S = T \<longleftrightarrow> fset S = fset T" |
786 "S = T \<longleftrightarrow> fset S = fset T" |
801 by (lifting list_eq.simps) |
787 by (lifting list_eq.simps) |
802 |
788 |
947 "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T" |
933 "inj f \<Longrightarrow> fmap f S = fmap f T \<longleftrightarrow> S = T" |
948 by (lifting inj_map_eq_iff) |
934 by (lifting inj_map_eq_iff) |
949 |
935 |
950 lemma fmap_funion: |
936 lemma fmap_funion: |
951 shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T" |
937 shows "fmap f (S |\<union>| T) = fmap f S |\<union>| fmap f T" |
952 by (lifting map_append) |
938 by (descending) (simp) |
953 |
939 |
954 lemma fin_funion: |
940 lemma fin_funion: |
955 shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T" |
941 shows "x |\<in>| S |\<union>| T \<longleftrightarrow> x |\<in>| S \<or> x |\<in>| T" |
956 by (lifting memb_append) |
942 by (descending) (simp add: memb_def) |
957 |
|
958 |
943 |
959 section {* fset *} |
944 section {* fset *} |
960 |
945 |
961 lemma fin_set: |
946 lemma fin_set: |
962 shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset xs" |
947 shows "x |\<in>| xs \<longleftrightarrow> x \<in> fset xs" |