1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Relating (finite) sets and lists *} |
|
5 |
|
6 theory List_Set |
|
7 imports Main More_List |
|
8 begin |
|
9 |
|
10 subsection {* Various additional set functions *} |
|
11 |
|
12 definition is_empty :: "'a set \<Rightarrow> bool" where |
|
13 "is_empty A \<longleftrightarrow> A = {}" |
|
14 |
|
15 definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
16 "remove x A = A - {x}" |
|
17 |
|
18 lemma fun_left_comm_idem_remove: |
|
19 "fun_left_comm_idem remove" |
|
20 proof - |
|
21 have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def) |
|
22 show ?thesis by (simp only: fun_left_comm_idem_remove rem) |
|
23 qed |
|
24 |
|
25 lemma minus_fold_remove: |
|
26 assumes "finite A" |
|
27 shows "B - A = Finite_Set.fold remove B A" |
|
28 proof - |
|
29 have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def) |
|
30 show ?thesis by (simp only: rem assms minus_fold_remove) |
|
31 qed |
|
32 |
|
33 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
34 "project P A = {a\<in>A. P a}" |
|
35 |
|
36 |
|
37 subsection {* Basic set operations *} |
|
38 |
|
39 lemma is_empty_set: |
|
40 "is_empty (set xs) \<longleftrightarrow> null xs" |
|
41 by (simp add: is_empty_def null_empty) |
|
42 |
|
43 lemma ball_set: |
|
44 "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs" |
|
45 by (rule list_ball_code) |
|
46 |
|
47 lemma bex_set: |
|
48 "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs" |
|
49 by (rule list_bex_code) |
|
50 |
|
51 lemma empty_set: |
|
52 "{} = set []" |
|
53 by simp |
|
54 |
|
55 lemma insert_set_compl: |
|
56 "insert x (- set xs) = - set (removeAll x xs)" |
|
57 by auto |
|
58 |
|
59 lemma remove_set_compl: |
|
60 "remove x (- set xs) = - set (List.insert x xs)" |
|
61 by (auto simp del: mem_def simp add: remove_def List.insert_def) |
|
62 |
|
63 lemma image_set: |
|
64 "image f (set xs) = set (map f xs)" |
|
65 by simp |
|
66 |
|
67 lemma project_set: |
|
68 "project P (set xs) = set (filter P xs)" |
|
69 by (auto simp add: project_def) |
|
70 |
|
71 |
|
72 subsection {* Functorial set operations *} |
|
73 |
|
74 lemma union_set: |
|
75 "set xs \<union> A = fold Set.insert xs A" |
|
76 proof - |
|
77 interpret fun_left_comm_idem Set.insert |
|
78 by (fact fun_left_comm_idem_insert) |
|
79 show ?thesis by (simp add: union_fold_insert fold_set) |
|
80 qed |
|
81 |
|
82 lemma union_set_foldr: |
|
83 "set xs \<union> A = foldr Set.insert xs A" |
|
84 proof - |
|
85 have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y" |
|
86 by (auto intro: ext) |
|
87 then show ?thesis by (simp add: union_set foldr_fold) |
|
88 qed |
|
89 |
|
90 lemma minus_set: |
|
91 "A - set xs = fold remove xs A" |
|
92 proof - |
|
93 interpret fun_left_comm_idem remove |
|
94 by (fact fun_left_comm_idem_remove) |
|
95 show ?thesis |
|
96 by (simp add: minus_fold_remove [of _ A] fold_set) |
|
97 qed |
|
98 |
|
99 lemma minus_set_foldr: |
|
100 "A - set xs = foldr remove xs A" |
|
101 proof - |
|
102 have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y" |
|
103 by (auto simp add: remove_def intro: ext) |
|
104 then show ?thesis by (simp add: minus_set foldr_fold) |
|
105 qed |
|
106 |
|
107 |
|
108 subsection {* Derived set operations *} |
|
109 |
|
110 lemma member: |
|
111 "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)" |
|
112 by simp |
|
113 |
|
114 lemma subset_eq: |
|
115 "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
116 by (fact subset_eq) |
|
117 |
|
118 lemma subset: |
|
119 "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A" |
|
120 by (fact less_le_not_le) |
|
121 |
|
122 lemma set_eq: |
|
123 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
|
124 by (fact eq_iff) |
|
125 |
|
126 lemma inter: |
|
127 "A \<inter> B = project (\<lambda>x. x \<in> A) B" |
|
128 by (auto simp add: project_def) |
|
129 |
|
130 |
|
131 subsection {* Various lemmas *} |
|
132 |
|
133 lemma not_set_compl: |
|
134 "Not \<circ> set xs = - set xs" |
|
135 by (simp add: fun_Compl_def bool_Compl_def comp_def expand_fun_eq) |
|
136 |
|
137 end |
|