author | wenzelm |
Tue, 25 May 2010 20:28:16 +0200 | |
changeset 37117 | 59cee8807c29 |
parent 37024 | e938a0b5286e |
child 37595 | 9591362629e3 |
permissions | -rw-r--r-- |
31807 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
||
4 |
header {* Relating (finite) sets and lists *} |
|
5 |
||
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
6 |
theory More_Set |
37023 | 7 |
imports Main More_List |
31807 | 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" |
|
37023 | 27 |
shows "B - A = Finite_Set.fold remove B A" |
31807 | 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 |
||
32880 | 55 |
lemma insert_set_compl: |
34977 | 56 |
"insert x (- set xs) = - set (removeAll x xs)" |
57 |
by auto |
|
31807 | 58 |
|
32880 | 59 |
lemma remove_set_compl: |
34977 | 60 |
"remove x (- set xs) = - set (List.insert x xs)" |
61 |
by (auto simp del: mem_def simp add: remove_def List.insert_def) |
|
32880 | 62 |
|
31807 | 63 |
lemma image_set: |
31846 | 64 |
"image f (set xs) = set (map f xs)" |
31807 | 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: |
|
37023 | 75 |
"set xs \<union> A = fold Set.insert xs A" |
31807 | 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 |
||
37023 | 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 |
||
31807 | 90 |
lemma minus_set: |
37023 | 91 |
"A - set xs = fold remove xs A" |
31807 | 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 |
||
37023 | 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 |
||
31807 | 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 |
||
37023 | 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 |
||
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
137 |
end |