author | wenzelm |
Thu, 16 Feb 2012 22:53:24 +0100 | |
changeset 46507 | 1b24c24017dd |
parent 46146 | 6baea4fca6bd |
child 46884 | 154dc6ec0041 |
permissions | -rw-r--r-- |
31807 | 1 |
|
2 |
(* Author: Florian Haftmann, TU Muenchen *) |
|
3 |
||
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
4 |
header {* A dedicated set type which is executable on its finite part *} |
31807 | 5 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
6 |
theory Cset |
45990
b7b905b23b2a
incorporated More_Set and More_List into the Main body -- to be consolidated later
haftmann
parents:
45986
diff
changeset
|
7 |
imports Main |
31807 | 8 |
begin |
9 |
||
10 |
subsection {* Lifting *} |
|
11 |
||
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
12 |
typedef (open) 'a set = "UNIV :: 'a set set" |
44555 | 13 |
morphisms set_of Set by rule+ |
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
14 |
hide_type (open) set |
31807 | 15 |
|
44555 | 16 |
lemma set_of_Set [simp]: |
17 |
"set_of (Set A) = A" |
|
18 |
by (rule Set_inverse) rule |
|
19 |
||
20 |
lemma Set_set_of [simp]: |
|
21 |
"Set (set_of A) = A" |
|
22 |
by (fact set_of_inverse) |
|
23 |
||
24 |
definition member :: "'a Cset.set \<Rightarrow> 'a \<Rightarrow> bool" where |
|
25 |
"member A x \<longleftrightarrow> x \<in> set_of A" |
|
26 |
||
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
27 |
lemma member_Set [simp]: |
44555 | 28 |
"member (Set A) x \<longleftrightarrow> x \<in> A" |
29 |
by (simp add: member_def) |
|
37468 | 30 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
31 |
lemma Set_inject [simp]: |
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
32 |
"Set A = Set B \<longleftrightarrow> A = B" |
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
33 |
by (simp add: Set_inject) |
37468 | 34 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
35 |
lemma set_eq_iff: |
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
36 |
"A = B \<longleftrightarrow> member A = member B" |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
44563
diff
changeset
|
37 |
by (auto simp add: fun_eq_iff set_of_inject [symmetric] member_def) |
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
38 |
hide_fact (open) set_eq_iff |
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset
|
39 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
40 |
lemma set_eqI: |
37473 | 41 |
"member A = member B \<Longrightarrow> A = B" |
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
42 |
by (simp add: Cset.set_eq_iff) |
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
43 |
hide_fact (open) set_eqI |
37473 | 44 |
|
34048 | 45 |
subsection {* Lattice instantiation *} |
46 |
||
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
47 |
instantiation Cset.set :: (type) boolean_algebra |
34048 | 48 |
begin |
49 |
||
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
50 |
definition less_eq_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where |
44555 | 51 |
[simp]: "A \<le> B \<longleftrightarrow> set_of A \<subseteq> set_of B" |
34048 | 52 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
53 |
definition less_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where |
44555 | 54 |
[simp]: "A < B \<longleftrightarrow> set_of A \<subset> set_of B" |
34048 | 55 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
56 |
definition inf_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where |
44555 | 57 |
[simp]: "inf A B = Set (set_of A \<inter> set_of B)" |
34048 | 58 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
59 |
definition sup_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where |
44555 | 60 |
[simp]: "sup A B = Set (set_of A \<union> set_of B)" |
34048 | 61 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
62 |
definition bot_set :: "'a Cset.set" where |
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
63 |
[simp]: "bot = Set {}" |
34048 | 64 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
65 |
definition top_set :: "'a Cset.set" where |
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
66 |
[simp]: "top = Set UNIV" |
34048 | 67 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
68 |
definition uminus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set" where |
44555 | 69 |
[simp]: "- A = Set (- (set_of A))" |
34048 | 70 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
71 |
definition minus_set :: "'a Cset.set \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where |
44555 | 72 |
[simp]: "A - B = Set (set_of A - set_of B)" |
34048 | 73 |
|
74 |
instance proof |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
44563
diff
changeset
|
75 |
qed (auto intro!: Cset.set_eqI simp add: member_def) |
34048 | 76 |
|
77 |
end |
|
78 |
||
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
79 |
instantiation Cset.set :: (type) complete_lattice |
34048 | 80 |
begin |
81 |
||
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
82 |
definition Inf_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where |
44555 | 83 |
[simp]: "Inf_set As = Set (Inf (image set_of As))" |
34048 | 84 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
85 |
definition Sup_set :: "'a Cset.set set \<Rightarrow> 'a Cset.set" where |
44555 | 86 |
[simp]: "Sup_set As = Set (Sup (image set_of As))" |
34048 | 87 |
|
88 |
instance proof |
|
44555 | 89 |
qed (auto simp add: le_fun_def) |
34048 | 90 |
|
91 |
end |
|
92 |
||
44555 | 93 |
instance Cset.set :: (type) complete_boolean_algebra proof |
94 |
qed (unfold INF_def SUP_def, auto) |
|
95 |
||
37023 | 96 |
|
31807 | 97 |
subsection {* Basic operations *} |
98 |
||
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
99 |
abbreviation empty :: "'a Cset.set" where "empty \<equiv> bot" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
100 |
hide_const (open) empty |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
101 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
102 |
abbreviation UNIV :: "'a Cset.set" where "UNIV \<equiv> top" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
103 |
hide_const (open) UNIV |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
104 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
105 |
definition is_empty :: "'a Cset.set \<Rightarrow> bool" where |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
106 |
[simp]: "is_empty A \<longleftrightarrow> Set.is_empty (set_of A)" |
31807 | 107 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
108 |
definition insert :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where |
44555 | 109 |
[simp]: "insert x A = Set (Set.insert x (set_of A))" |
31807 | 110 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
111 |
definition remove :: "'a \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
112 |
[simp]: "remove x A = Set (Set.remove x (set_of A))" |
31807 | 113 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
114 |
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Cset.set \<Rightarrow> 'b Cset.set" where |
44555 | 115 |
[simp]: "map f A = Set (image f (set_of A))" |
31807 | 116 |
|
41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41372
diff
changeset
|
117 |
enriched_type map: map |
41372 | 118 |
by (simp_all add: fun_eq_iff image_compose) |
40604 | 119 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
120 |
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> 'a Cset.set" where |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
121 |
[simp]: "filter P A = Set (Set.project P (set_of A))" |
31807 | 122 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
123 |
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where |
44555 | 124 |
[simp]: "forall P A \<longleftrightarrow> Ball (set_of A) P" |
31807 | 125 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
126 |
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Cset.set \<Rightarrow> bool" where |
44555 | 127 |
[simp]: "exists P A \<longleftrightarrow> Bex (set_of A) P" |
31807 | 128 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
129 |
definition card :: "'a Cset.set \<Rightarrow> nat" where |
44555 | 130 |
[simp]: "card A = Finite_Set.card (set_of A)" |
43241 | 131 |
|
34048 | 132 |
context complete_lattice |
133 |
begin |
|
31807 | 134 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
135 |
definition Infimum :: "'a Cset.set \<Rightarrow> 'a" where |
44555 | 136 |
[simp]: "Infimum A = Inf (set_of A)" |
31807 | 137 |
|
40672
abd4e7358847
replaced misleading Fset/fset name -- these do not stand for finite sets
haftmann
parents:
40604
diff
changeset
|
138 |
definition Supremum :: "'a Cset.set \<Rightarrow> 'a" where |
44555 | 139 |
[simp]: "Supremum A = Sup (set_of A)" |
34048 | 140 |
|
141 |
end |
|
31807 | 142 |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
143 |
subsection {* More operations *} |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
144 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
145 |
text {* conversion from @{typ "'a list"} *} |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
146 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
147 |
definition set :: "'a list \<Rightarrow> 'a Cset.set" where |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
148 |
"set xs = Set (List.set xs)" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
149 |
hide_const (open) set |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
150 |
|
44558 | 151 |
definition coset :: "'a list \<Rightarrow> 'a Cset.set" where |
152 |
"coset xs = Set (- List.set xs)" |
|
153 |
hide_const (open) coset |
|
154 |
||
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
155 |
text {* conversion from @{typ "'a Predicate.pred"} *} |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
156 |
|
44555 | 157 |
definition pred_of_cset :: "'a Cset.set \<Rightarrow> 'a Predicate.pred" where |
158 |
[code del]: "pred_of_cset = Predicate.Pred \<circ> Cset.member" |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
159 |
|
44555 | 160 |
definition of_pred :: "'a Predicate.pred \<Rightarrow> 'a Cset.set" where |
161 |
"of_pred = Cset.Set \<circ> Collect \<circ> Predicate.eval" |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
162 |
|
44555 | 163 |
definition of_seq :: "'a Predicate.seq \<Rightarrow> 'a Cset.set" where |
164 |
"of_seq = of_pred \<circ> Predicate.pred_of_seq" |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
165 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
166 |
text {* monad operations *} |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
167 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
168 |
definition single :: "'a \<Rightarrow> 'a Cset.set" where |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
169 |
"single a = Set {a}" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
170 |
|
44555 | 171 |
definition bind :: "'a Cset.set \<Rightarrow> ('a \<Rightarrow> 'b Cset.set) \<Rightarrow> 'b Cset.set" (infixl "\<guillemotright>=" 70) where |
172 |
"A \<guillemotright>= f = (SUP x : set_of A. f x)" |
|
173 |
||
31807 | 174 |
|
31846 | 175 |
subsection {* Simplified simprules *} |
176 |
||
44555 | 177 |
lemma empty_simp [simp]: "member Cset.empty = bot" |
178 |
by (simp add: fun_eq_iff bot_apply) |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
179 |
|
44555 | 180 |
lemma UNIV_simp [simp]: "member Cset.UNIV = top" |
181 |
by (simp add: fun_eq_iff top_apply) |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
182 |
|
31846 | 183 |
lemma is_empty_simp [simp]: |
44555 | 184 |
"is_empty A \<longleftrightarrow> set_of A = {}" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
185 |
by (simp add: Set.is_empty_def) |
31846 | 186 |
declare is_empty_def [simp del] |
187 |
||
188 |
lemma remove_simp [simp]: |
|
44555 | 189 |
"remove x A = Set (set_of A - {x})" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
190 |
by (simp add: Set.remove_def) |
31846 | 191 |
declare remove_def [simp del] |
192 |
||
31847 | 193 |
lemma filter_simp [simp]: |
44555 | 194 |
"filter P A = Set {x \<in> set_of A. P x}" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
195 |
by (simp add: Set.project_def) |
31847 | 196 |
declare filter_def [simp del] |
31846 | 197 |
|
44555 | 198 |
lemma set_of_set [simp]: |
199 |
"set_of (Cset.set xs) = set xs" |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
200 |
by (simp add: set_def) |
44555 | 201 |
hide_fact (open) set_def |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
202 |
|
44558 | 203 |
lemma member_set [simp]: |
204 |
"member (Cset.set xs) = (\<lambda>x. x \<in> set xs)" |
|
205 |
by (simp add: fun_eq_iff member_def) |
|
206 |
hide_fact (open) member_set |
|
207 |
||
208 |
lemma set_of_coset [simp]: |
|
209 |
"set_of (Cset.coset xs) = - set xs" |
|
210 |
by (simp add: coset_def) |
|
211 |
hide_fact (open) coset_def |
|
212 |
||
213 |
lemma member_coset [simp]: |
|
214 |
"member (Cset.coset xs) = (\<lambda>x. x \<in> - set xs)" |
|
215 |
by (simp add: fun_eq_iff member_def) |
|
216 |
hide_fact (open) member_coset |
|
217 |
||
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
218 |
lemma set_simps [simp]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
219 |
"Cset.set [] = Cset.empty" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
220 |
"Cset.set (x # xs) = insert x (Cset.set xs)" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
221 |
by(simp_all add: Cset.set_def) |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
222 |
|
44555 | 223 |
lemma member_SUP [simp]: |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
224 |
"member (SUPR A f) = SUPR A (member \<circ> f)" |
44555 | 225 |
by (auto simp add: fun_eq_iff SUP_apply member_def, unfold SUP_def, auto) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
226 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
227 |
lemma member_bind [simp]: |
44555 | 228 |
"member (P \<guillemotright>= f) = SUPR (set_of P) (member \<circ> f)" |
229 |
by (simp add: bind_def Cset.set_eq_iff) |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
230 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
231 |
lemma member_single [simp]: |
44555 | 232 |
"member (single a) = (\<lambda>x. x \<in> {a})" |
233 |
by (simp add: single_def fun_eq_iff) |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
234 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
235 |
lemma single_sup_simps [simp]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
236 |
shows single_sup: "sup (single a) A = insert a A" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
237 |
and sup_single: "sup A (single a) = insert a A" |
44555 | 238 |
by (auto simp add: Cset.set_eq_iff single_def) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
239 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
240 |
lemma single_bind [simp]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
241 |
"single a \<guillemotright>= B = B a" |
44555 | 242 |
by (simp add: Cset.set_eq_iff SUP_insert single_def) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
243 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
244 |
lemma bind_bind: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
245 |
"(A \<guillemotright>= B) \<guillemotright>= C = A \<guillemotright>= (\<lambda>x. B x \<guillemotright>= C)" |
44555 | 246 |
by (simp add: bind_def, simp only: SUP_def image_image, simp) |
247 |
||
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
248 |
lemma bind_single [simp]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
249 |
"A \<guillemotright>= single = A" |
44555 | 250 |
by (simp add: Cset.set_eq_iff SUP_apply fun_eq_iff single_def member_def) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
251 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
252 |
lemma bind_const: "A \<guillemotright>= (\<lambda>_. B) = (if Cset.is_empty A then Cset.empty else B)" |
44555 | 253 |
by (auto simp add: Cset.set_eq_iff fun_eq_iff) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
254 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
255 |
lemma empty_bind [simp]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
256 |
"Cset.empty \<guillemotright>= f = Cset.empty" |
44555 | 257 |
by (simp add: Cset.set_eq_iff fun_eq_iff bot_apply) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
258 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
259 |
lemma member_of_pred [simp]: |
44555 | 260 |
"member (of_pred P) = (\<lambda>x. x \<in> {x. Predicate.eval P x})" |
261 |
by (simp add: of_pred_def fun_eq_iff) |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
262 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
263 |
lemma member_of_seq [simp]: |
44555 | 264 |
"member (of_seq xq) = (\<lambda>x. x \<in> {x. Predicate.member xq x})" |
265 |
by (simp add: of_seq_def eval_member) |
|
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
266 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
267 |
lemma eval_pred_of_cset [simp]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
268 |
"Predicate.eval (pred_of_cset A) = Cset.member A" |
44555 | 269 |
by (simp add: pred_of_cset_def) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
270 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
271 |
subsection {* Default implementations *} |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
272 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
273 |
lemma set_code [code]: |
44555 | 274 |
"Cset.set = (\<lambda>xs. fold insert xs Cset.empty)" |
275 |
proof (rule ext, rule Cset.set_eqI) |
|
276 |
fix xs :: "'a list" |
|
277 |
show "member (Cset.set xs) = member (fold insert xs Cset.empty)" |
|
278 |
by (simp add: fold_commute_apply [symmetric, where ?h = Set and ?g = Set.insert] |
|
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46133
diff
changeset
|
279 |
fun_eq_iff Cset.set_def union_set_fold [symmetric]) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
280 |
qed |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
281 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
282 |
lemma single_code [code]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
283 |
"single a = insert a Cset.empty" |
44555 | 284 |
by (simp add: Cset.single_def) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
285 |
|
44558 | 286 |
lemma compl_set [simp]: |
287 |
"- Cset.set xs = Cset.coset xs" |
|
288 |
by (simp add: Cset.set_def Cset.coset_def) |
|
289 |
||
290 |
lemma compl_coset [simp]: |
|
291 |
"- Cset.coset xs = Cset.set xs" |
|
292 |
by (simp add: Cset.set_def Cset.coset_def) |
|
293 |
||
294 |
lemma inter_project: |
|
295 |
"inf A (Cset.set xs) = Cset.set (List.filter (Cset.member A) xs)" |
|
296 |
"inf A (Cset.coset xs) = foldr Cset.remove xs A" |
|
297 |
proof - |
|
298 |
show "inf A (Cset.set xs) = Cset.set (List.filter (member A) xs)" |
|
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46133
diff
changeset
|
299 |
by (simp add: project_def Cset.set_def member_def) auto |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
300 |
have *: "\<And>x::'a. Cset.remove = (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of)" |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
301 |
by (simp add: fun_eq_iff Set.remove_def) |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
302 |
have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs = |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
303 |
fold Set.remove xs \<circ> set_of" |
44563 | 304 |
by (rule fold_commute) (simp add: fun_eq_iff) |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
305 |
then have "fold Set.remove xs (set_of A) = |
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
306 |
set_of (fold (\<lambda>x. Set \<circ> Set.remove x \<circ> set_of) xs A)" |
44558 | 307 |
by (simp add: fun_eq_iff) |
308 |
then have "inf A (Cset.coset xs) = fold Cset.remove xs A" |
|
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46133
diff
changeset
|
309 |
by (simp add: Diff_eq [symmetric] minus_set_fold *) |
44558 | 310 |
moreover have "\<And>x y :: 'a. Cset.remove y \<circ> Cset.remove x = Cset.remove x \<circ> Cset.remove y" |
45986
c9e50153e5ae
moved various set operations to theory Set (resp. Product_Type)
haftmann
parents:
45970
diff
changeset
|
311 |
by (auto simp add: Set.remove_def *) |
44558 | 312 |
ultimately show "inf A (Cset.coset xs) = foldr Cset.remove xs A" |
313 |
by (simp add: foldr_fold) |
|
314 |
qed |
|
315 |
||
44563 | 316 |
lemma union_insert: |
317 |
"sup (Cset.set xs) A = foldr Cset.insert xs A" |
|
318 |
"sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)" |
|
319 |
proof - |
|
320 |
have *: "\<And>x::'a. Cset.insert = (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of)" |
|
321 |
by (simp add: fun_eq_iff) |
|
322 |
have "set_of \<circ> fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs = |
|
323 |
fold Set.insert xs \<circ> set_of" |
|
324 |
by (rule fold_commute) (simp add: fun_eq_iff) |
|
325 |
then have "fold Set.insert xs (set_of A) = |
|
326 |
set_of (fold (\<lambda>x. Set \<circ> Set.insert x \<circ> set_of) xs A)" |
|
327 |
by (simp add: fun_eq_iff) |
|
328 |
then have "sup (Cset.set xs) A = fold Cset.insert xs A" |
|
46146
6baea4fca6bd
incorporated various theorems from theory More_Set into corpus
haftmann
parents:
46133
diff
changeset
|
329 |
by (simp add: union_set_fold *) |
44563 | 330 |
moreover have "\<And>x y :: 'a. Cset.insert y \<circ> Cset.insert x = Cset.insert x \<circ> Cset.insert y" |
331 |
by (auto simp add: *) |
|
332 |
ultimately show "sup (Cset.set xs) A = foldr Cset.insert xs A" |
|
333 |
by (simp add: foldr_fold) |
|
334 |
show "sup (Cset.coset xs) A = Cset.coset (List.filter (Not \<circ> member A) xs)" |
|
335 |
by (auto simp add: Cset.coset_def Cset.member_def) |
|
336 |
qed |
|
337 |
||
44558 | 338 |
lemma subtract_remove: |
339 |
"A - Cset.set xs = foldr Cset.remove xs A" |
|
340 |
"A - Cset.coset xs = Cset.set (List.filter (member A) xs)" |
|
341 |
by (simp_all only: diff_eq compl_set compl_coset inter_project) |
|
342 |
||
343 |
context complete_lattice |
|
344 |
begin |
|
345 |
||
346 |
lemma Infimum_inf: |
|
347 |
"Infimum (Cset.set As) = foldr inf As top" |
|
348 |
"Infimum (Cset.coset []) = bot" |
|
349 |
by (simp_all add: Inf_set_foldr) |
|
350 |
||
351 |
lemma Supremum_sup: |
|
352 |
"Supremum (Cset.set As) = foldr sup As bot" |
|
353 |
"Supremum (Cset.coset []) = top" |
|
354 |
by (simp_all add: Sup_set_foldr) |
|
355 |
||
356 |
end |
|
357 |
||
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
358 |
lemma of_pred_code [code]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
359 |
"of_pred (Predicate.Seq f) = (case f () of |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
360 |
Predicate.Empty \<Rightarrow> Cset.empty |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
361 |
| Predicate.Insert x P \<Rightarrow> Cset.insert x (of_pred P) |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
362 |
| Predicate.Join P xq \<Rightarrow> sup (of_pred P) (of_seq xq))" |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
44563
diff
changeset
|
363 |
by (auto split: seq.split simp add: Predicate.Seq_def of_pred_def Cset.set_eq_iff sup_apply eval_member [symmetric] member_def [symmetric]) |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
364 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
365 |
lemma of_seq_code [code]: |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
366 |
"of_seq Predicate.Empty = Cset.empty" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
367 |
"of_seq (Predicate.Insert x P) = Cset.insert x (of_pred P)" |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
368 |
"of_seq (Predicate.Join P xq) = sup (of_pred P) (of_seq xq)" |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
44563
diff
changeset
|
369 |
by (auto simp add: of_seq_def of_pred_def Cset.set_eq_iff) |
31846 | 370 |
|
44558 | 371 |
lemma bind_set: |
372 |
"Cset.bind (Cset.set xs) f = fold (sup \<circ> f) xs (Cset.set [])" |
|
46133
d9fe85d3d2cd
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r)
haftmann
parents:
45990
diff
changeset
|
373 |
by (simp add: Cset.bind_def SUP_set_fold) |
44558 | 374 |
hide_fact (open) bind_set |
375 |
||
376 |
lemma pred_of_cset_set: |
|
377 |
"pred_of_cset (Cset.set xs) = foldr sup (List.map Predicate.single xs) bot" |
|
378 |
proof - |
|
379 |
have "pred_of_cset (Cset.set xs) = Predicate.Pred (\<lambda>x. x \<in> set xs)" |
|
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
44563
diff
changeset
|
380 |
by (simp add: Cset.pred_of_cset_def) |
44558 | 381 |
moreover have "foldr sup (List.map Predicate.single xs) bot = \<dots>" |
45970
b6d0cff57d96
adjusted to set/pred distinction by means of type constructor `set`
haftmann
parents:
44563
diff
changeset
|
382 |
by (induct xs) (auto simp add: bot_pred_def intro: pred_eqI) |
44558 | 383 |
ultimately show ?thesis by simp |
384 |
qed |
|
385 |
hide_fact (open) pred_of_cset_set |
|
386 |
||
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
387 |
no_notation bind (infixl "\<guillemotright>=" 70) |
31849 | 388 |
|
43241 | 389 |
hide_const (open) is_empty insert remove map filter forall exists card |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
390 |
Inter Union bind single of_pred of_seq |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
391 |
|
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
392 |
hide_fact (open) set_def pred_of_cset_def of_pred_def of_seq_def single_def |
44555 | 393 |
bind_def empty_simp UNIV_simp set_simps member_bind |
43971
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
394 |
member_single single_sup_simps single_sup sup_single single_bind |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
395 |
bind_bind bind_single bind_const empty_bind member_of_pred member_of_seq |
892030194015
added operations to Cset with code equations in backing implementations
Andreas Lochbihler
parents:
43241
diff
changeset
|
396 |
eval_pred_of_cset set_code single_code of_pred_code of_seq_code |
31849 | 397 |
|
31807 | 398 |
end |