|
1 |
|
2 (* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
|
4 header {* Relating (finite) sets and lists *} |
|
5 |
|
6 theory List_Set |
|
7 imports Main |
|
8 begin |
|
9 |
|
10 subsection {* Various additional list functions *} |
|
11 |
|
12 definition insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
13 "insert x xs = (if x \<in> set xs then xs else x # xs)" |
|
14 |
|
15 definition remove_all :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
16 "remove_all x xs = filter (Not o op = x) xs" |
|
17 |
|
18 |
|
19 subsection {* Various additional set functions *} |
|
20 |
|
21 definition is_empty :: "'a set \<Rightarrow> bool" where |
|
22 "is_empty A \<longleftrightarrow> A = {}" |
|
23 |
|
24 definition remove :: "'a \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
25 "remove x A = A - {x}" |
|
26 |
|
27 lemma fun_left_comm_idem_remove: |
|
28 "fun_left_comm_idem remove" |
|
29 proof - |
|
30 have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def) |
|
31 show ?thesis by (simp only: fun_left_comm_idem_remove rem) |
|
32 qed |
|
33 |
|
34 lemma minus_fold_remove: |
|
35 assumes "finite A" |
|
36 shows "B - A = fold remove B A" |
|
37 proof - |
|
38 have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: expand_fun_eq remove_def) |
|
39 show ?thesis by (simp only: rem assms minus_fold_remove) |
|
40 qed |
|
41 |
|
42 definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
43 "project P A = {a\<in>A. P a}" |
|
44 |
|
45 |
|
46 subsection {* Basic set operations *} |
|
47 |
|
48 lemma is_empty_set: |
|
49 "is_empty (set xs) \<longleftrightarrow> null xs" |
|
50 by (simp add: is_empty_def null_empty) |
|
51 |
|
52 lemma ball_set: |
|
53 "(\<forall>x\<in>set xs. P x) \<longleftrightarrow> list_all P xs" |
|
54 by (rule list_ball_code) |
|
55 |
|
56 lemma bex_set: |
|
57 "(\<exists>x\<in>set xs. P x) \<longleftrightarrow> list_ex P xs" |
|
58 by (rule list_bex_code) |
|
59 |
|
60 lemma empty_set: |
|
61 "{} = set []" |
|
62 by simp |
|
63 |
|
64 lemma insert_set: |
|
65 "Set.insert x (set xs) = set (insert x xs)" |
|
66 by (auto simp add: insert_def) |
|
67 |
|
68 lemma remove_set: |
|
69 "remove x (set xs) = set (remove_all x xs)" |
|
70 by (auto simp add: remove_def remove_all_def) |
|
71 |
|
72 lemma image_set: |
|
73 "image f (set xs) = set (remdups (map f xs))" |
|
74 by simp |
|
75 |
|
76 lemma project_set: |
|
77 "project P (set xs) = set (filter P xs)" |
|
78 by (auto simp add: project_def) |
|
79 |
|
80 |
|
81 subsection {* Functorial set operations *} |
|
82 |
|
83 lemma union_set: |
|
84 "set xs \<union> A = foldl (\<lambda>A x. Set.insert x A) A xs" |
|
85 proof - |
|
86 interpret fun_left_comm_idem Set.insert |
|
87 by (fact fun_left_comm_idem_insert) |
|
88 show ?thesis by (simp add: union_fold_insert fold_set) |
|
89 qed |
|
90 |
|
91 lemma minus_set: |
|
92 "A - set xs = foldl (\<lambda>A x. remove x A) A xs" |
|
93 proof - |
|
94 interpret fun_left_comm_idem remove |
|
95 by (fact fun_left_comm_idem_remove) |
|
96 show ?thesis |
|
97 by (simp add: minus_fold_remove [of _ A] fold_set) |
|
98 qed |
|
99 |
|
100 lemma Inter_set: |
|
101 "Inter (set (A # As)) = foldl (op \<inter>) A As" |
|
102 proof - |
|
103 have "finite (set (A # As))" by simp |
|
104 moreover have "fold (op \<inter>) UNIV (set (A # As)) = foldl (\<lambda>y x. x \<inter> y) UNIV (A # As)" |
|
105 by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) |
|
106 ultimately have "Inter (set (A # As)) = foldl (op \<inter>) UNIV (A # As)" |
|
107 by (simp only: Inter_fold_inter Int_commute) |
|
108 then show ?thesis by simp |
|
109 qed |
|
110 |
|
111 lemma Union_set: |
|
112 "Union (set As) = foldl (op \<union>) {} As" |
|
113 proof - |
|
114 have "fold (op \<union>) {} (set As) = foldl (\<lambda>y x. x \<union> y) {} As" |
|
115 by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) |
|
116 then show ?thesis |
|
117 by (simp only: Union_fold_union finite_set Un_commute) |
|
118 qed |
|
119 |
|
120 lemma INTER_set: |
|
121 "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) (f A) As" |
|
122 proof - |
|
123 have "finite (set (A # As))" by simp |
|
124 moreover have "fold (\<lambda>A. op \<inter> (f A)) UNIV (set (A # As)) = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)" |
|
125 by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) |
|
126 ultimately have "INTER (set (A # As)) f = foldl (\<lambda>B A. f A \<inter> B) UNIV (A # As)" |
|
127 by (simp only: INTER_fold_inter) |
|
128 then show ?thesis by simp |
|
129 qed |
|
130 |
|
131 lemma UNION_set: |
|
132 "UNION (set As) f = foldl (\<lambda>B A. f A \<union> B) {} As" |
|
133 proof - |
|
134 have "fold (\<lambda>A. op \<union> (f A)) {} (set As) = foldl (\<lambda>B A. f A \<union> B) {} As" |
|
135 by (rule fun_left_comm_idem.fold_set, unfold_locales, auto) |
|
136 then show ?thesis |
|
137 by (simp only: UNION_fold_union finite_set) |
|
138 qed |
|
139 |
|
140 |
|
141 subsection {* Derived set operations *} |
|
142 |
|
143 lemma member: |
|
144 "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)" |
|
145 by simp |
|
146 |
|
147 lemma subset_eq: |
|
148 "A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
149 by (fact subset_eq) |
|
150 |
|
151 lemma subset: |
|
152 "A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A" |
|
153 by (fact less_le_not_le) |
|
154 |
|
155 lemma set_eq: |
|
156 "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
|
157 by (fact eq_iff) |
|
158 |
|
159 lemma inter: |
|
160 "A \<inter> B = project (\<lambda>x. x \<in> A) B" |
|
161 by (auto simp add: project_def) |
|
162 |
|
163 end |