author | haftmann |
Tue, 20 Sep 2011 21:47:52 +0200 | |
changeset 45012 | 060f76635bfe |
parent 44326 | 2b088d74beb3 |
child 45974 | 2b043ed911ac |
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 |
||
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
18 |
lemma comp_fun_idem_remove: |
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
19 |
"comp_fun_idem remove" |
31807 | 20 |
proof - |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
21 |
have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
22 |
show ?thesis by (simp only: comp_fun_idem_remove rem) |
31807 | 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 - |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
29 |
have rem: "remove = (\<lambda>x A. A - {x})" by (simp add: fun_eq_iff remove_def) |
31807 | 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 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
34 |
"project P A = {a \<in> A. P a}" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
35 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
36 |
lemma bounded_Collect_code [code_unfold_post]: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
37 |
"{x \<in> A. P x} = project P A" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
38 |
by (simp add: project_def) |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
39 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
40 |
definition product :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<times> 'b) set" where |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
41 |
"product A B = Sigma A (\<lambda>_. B)" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
42 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
43 |
hide_const (open) product |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
44 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
45 |
lemma [code_unfold_post]: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
46 |
"Sigma A (\<lambda>_. B) = More_Set.product A B" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
47 |
by (simp add: product_def) |
31807 | 48 |
|
49 |
||
50 |
subsection {* Basic set operations *} |
|
51 |
||
52 |
lemma is_empty_set: |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37024
diff
changeset
|
53 |
"is_empty (set xs) \<longleftrightarrow> List.null xs" |
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37024
diff
changeset
|
54 |
by (simp add: is_empty_def null_def) |
31807 | 55 |
|
56 |
lemma empty_set: |
|
57 |
"{} = set []" |
|
58 |
by simp |
|
59 |
||
32880 | 60 |
lemma insert_set_compl: |
34977 | 61 |
"insert x (- set xs) = - set (removeAll x xs)" |
62 |
by auto |
|
31807 | 63 |
|
32880 | 64 |
lemma remove_set_compl: |
34977 | 65 |
"remove x (- set xs) = - set (List.insert x xs)" |
44326 | 66 |
by (auto simp add: remove_def List.insert_def) |
32880 | 67 |
|
31807 | 68 |
lemma image_set: |
31846 | 69 |
"image f (set xs) = set (map f xs)" |
31807 | 70 |
by simp |
71 |
||
72 |
lemma project_set: |
|
73 |
"project P (set xs) = set (filter P xs)" |
|
74 |
by (auto simp add: project_def) |
|
75 |
||
76 |
||
77 |
subsection {* Functorial set operations *} |
|
78 |
||
79 |
lemma union_set: |
|
37023 | 80 |
"set xs \<union> A = fold Set.insert xs A" |
31807 | 81 |
proof - |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
82 |
interpret comp_fun_idem Set.insert |
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
83 |
by (fact comp_fun_idem_insert) |
31807 | 84 |
show ?thesis by (simp add: union_fold_insert fold_set) |
85 |
qed |
|
86 |
||
37023 | 87 |
lemma union_set_foldr: |
88 |
"set xs \<union> A = foldr Set.insert xs A" |
|
89 |
proof - |
|
90 |
have "\<And>x y :: 'a. insert y \<circ> insert x = insert x \<circ> insert y" |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
91 |
by auto |
37023 | 92 |
then show ?thesis by (simp add: union_set foldr_fold) |
93 |
qed |
|
94 |
||
31807 | 95 |
lemma minus_set: |
37023 | 96 |
"A - set xs = fold remove xs A" |
31807 | 97 |
proof - |
42871
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
98 |
interpret comp_fun_idem remove |
1c0b99f950d9
names of fold_set locales resemble name of characteristic property more closely
haftmann
parents:
42868
diff
changeset
|
99 |
by (fact comp_fun_idem_remove) |
31807 | 100 |
show ?thesis |
101 |
by (simp add: minus_fold_remove [of _ A] fold_set) |
|
102 |
qed |
|
103 |
||
37023 | 104 |
lemma minus_set_foldr: |
105 |
"A - set xs = foldr remove xs A" |
|
106 |
proof - |
|
107 |
have "\<And>x y :: 'a. remove y \<circ> remove x = remove x \<circ> remove y" |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
108 |
by (auto simp add: remove_def) |
37023 | 109 |
then show ?thesis by (simp add: minus_set foldr_fold) |
110 |
qed |
|
111 |
||
31807 | 112 |
|
113 |
subsection {* Derived set operations *} |
|
114 |
||
115 |
lemma member: |
|
116 |
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. a = x)" |
|
117 |
by simp |
|
118 |
||
119 |
lemma subset_eq: |
|
120 |
"A \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
121 |
by (fact subset_eq) |
|
122 |
||
123 |
lemma subset: |
|
124 |
"A \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> \<not> B \<subseteq> A" |
|
125 |
by (fact less_le_not_le) |
|
126 |
||
127 |
lemma set_eq: |
|
128 |
"A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
|
129 |
by (fact eq_iff) |
|
130 |
||
131 |
lemma inter: |
|
132 |
"A \<inter> B = project (\<lambda>x. x \<in> A) B" |
|
133 |
by (auto simp add: project_def) |
|
134 |
||
37023 | 135 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
136 |
subsection {* Theorems on relations *} |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
137 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
138 |
lemma product_code: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
139 |
"More_Set.product (set xs) (set ys) = set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
140 |
by (auto simp add: product_def) |
37023 | 141 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
142 |
lemma Id_on_set: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
143 |
"Id_on (set xs) = set [(x, x). x \<leftarrow> xs]" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
144 |
by (auto simp add: Id_on_def) |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
145 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
146 |
lemma set_rel_comp: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
147 |
"set xys O set yzs = set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
148 |
by (auto simp add: Bex_def) |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
149 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
150 |
lemma wf_set: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
151 |
"wf (set xs) = acyclic (set xs)" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44326
diff
changeset
|
152 |
by (simp add: wf_iff_acyclic_if_finite) |
37023 | 153 |
|
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
154 |
end |