author | bulwahn |
Wed, 14 Dec 2011 16:30:32 +0100 | |
changeset 45873 | 37ffb8797a63 |
parent 45231 | d85a2fdc586c |
child 45975 | 5e78c499a7ff |
permissions | -rw-r--r-- |
34020 | 1 |
(* Title: HOL/Library/Executable_Set.thy |
2 |
Author: Stefan Berghofer, TU Muenchen |
|
33947 | 3 |
Author: Florian Haftmann, TU Muenchen |
4 |
*) |
|
5 |
||
6 |
header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *} |
|
7 |
||
34020 | 8 |
theory Executable_Set |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
9 |
imports More_Set |
33947 | 10 |
begin |
11 |
||
39141 | 12 |
text {* |
13 |
This is just an ad-hoc hack which will rarely give you what you want. |
|
14 |
For the moment, whenever you need executable sets, consider using |
|
43363 | 15 |
type @{text Cset.set} from theory @{text Cset}. |
39141 | 16 |
*} |
17 |
||
33947 | 18 |
declare mem_def [code del] |
19 |
declare Collect_def [code del] |
|
20 |
declare insert_code [code del] |
|
21 |
declare vimage_code [code del] |
|
22 |
||
23 |
subsection {* Set representation *} |
|
24 |
||
25 |
setup {* |
|
26 |
Code.add_type_cmd "set" |
|
27 |
*} |
|
28 |
||
29 |
definition Set :: "'a list \<Rightarrow> 'a set" where |
|
30 |
[simp]: "Set = set" |
|
31 |
||
32 |
definition Coset :: "'a list \<Rightarrow> 'a set" where |
|
33 |
[simp]: "Coset xs = - set xs" |
|
34 |
||
35 |
setup {* |
|
36 |
Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set") |
|
37 |
#> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set") |
|
38 |
#> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set") |
|
39 |
#> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool") |
|
40 |
*} |
|
41 |
||
42 |
code_datatype Set Coset |
|
43 |
||
44 |
||
45 |
subsection {* Basic operations *} |
|
46 |
||
47 |
lemma [code]: |
|
48 |
"set xs = Set (remdups xs)" |
|
49 |
by simp |
|
50 |
||
51 |
lemma [code]: |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37024
diff
changeset
|
52 |
"x \<in> Set xs \<longleftrightarrow> List.member xs x" |
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37024
diff
changeset
|
53 |
"x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x" |
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37024
diff
changeset
|
54 |
by (simp_all add: member_def) |
33947 | 55 |
|
56 |
definition is_empty :: "'a set \<Rightarrow> bool" where |
|
57 |
[simp]: "is_empty A \<longleftrightarrow> A = {}" |
|
58 |
||
34020 | 59 |
lemma [code_unfold]: |
33947 | 60 |
"A = {} \<longleftrightarrow> is_empty A" |
61 |
by simp |
|
62 |
||
63 |
definition empty :: "'a set" where |
|
64 |
[simp]: "empty = {}" |
|
65 |
||
34020 | 66 |
lemma [code_unfold]: |
33947 | 67 |
"{} = empty" |
68 |
by simp |
|
69 |
||
45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
45186
diff
changeset
|
70 |
lemma |
34020 | 71 |
"empty = Set []" |
72 |
by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *} |
|
73 |
||
33947 | 74 |
setup {* |
75 |
Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool") |
|
76 |
#> Code.add_signature_cmd ("empty", "'a set") |
|
77 |
#> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
78 |
#> Code.add_signature_cmd ("More_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set") |
33947 | 79 |
#> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set") |
37024
e938a0b5286e
renamed List_Set to the now more appropriate More_Set
haftmann
parents:
37023
diff
changeset
|
80 |
#> Code.add_signature_cmd ("More_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set") |
33947 | 81 |
#> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool") |
82 |
#> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool") |
|
83 |
#> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat") |
|
84 |
*} |
|
85 |
||
86 |
lemma is_empty_Set [code]: |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37024
diff
changeset
|
87 |
"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
|
88 |
by (simp add: null_def) |
33947 | 89 |
|
90 |
lemma empty_Set [code]: |
|
91 |
"empty = Set []" |
|
92 |
by simp |
|
93 |
||
94 |
lemma insert_Set [code]: |
|
34980 | 95 |
"insert x (Set xs) = Set (List.insert x xs)" |
96 |
"insert x (Coset xs) = Coset (removeAll x xs)" |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
97 |
by simp_all |
33947 | 98 |
|
99 |
lemma remove_Set [code]: |
|
34980 | 100 |
"remove x (Set xs) = Set (removeAll x xs)" |
101 |
"remove x (Coset xs) = Coset (List.insert x xs)" |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
102 |
by (auto simp add: remove_def) |
33947 | 103 |
|
104 |
lemma image_Set [code]: |
|
105 |
"image f (Set xs) = Set (remdups (map f xs))" |
|
106 |
by simp |
|
107 |
||
108 |
lemma project_Set [code]: |
|
109 |
"project P (Set xs) = Set (filter P xs)" |
|
110 |
by (simp add: project_set) |
|
111 |
||
112 |
lemma Ball_Set [code]: |
|
113 |
"Ball (Set xs) P \<longleftrightarrow> list_all P xs" |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37024
diff
changeset
|
114 |
by (simp add: list_all_iff) |
33947 | 115 |
|
116 |
lemma Bex_Set [code]: |
|
117 |
"Bex (Set xs) P \<longleftrightarrow> list_ex P xs" |
|
37595
9591362629e3
dropped ancient infix mem; refined code generation operations in List.thy
haftmann
parents:
37024
diff
changeset
|
118 |
by (simp add: list_ex_iff) |
33947 | 119 |
|
45120
717bc892e4d7
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
bulwahn
parents:
45012
diff
changeset
|
120 |
lemma |
717bc892e4d7
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
bulwahn
parents:
45012
diff
changeset
|
121 |
[code, code del]: "card S = card S" .. |
717bc892e4d7
removing code equation for card on finite types when loading the Executable_Set theory; should resolve a code generation issue with CoreC++
bulwahn
parents:
45012
diff
changeset
|
122 |
|
33947 | 123 |
lemma card_Set [code]: |
124 |
"card (Set xs) = length (remdups xs)" |
|
125 |
proof - |
|
126 |
have "card (set (remdups xs)) = length (remdups xs)" |
|
127 |
by (rule distinct_card) simp |
|
128 |
then show ?thesis by simp |
|
129 |
qed |
|
130 |
||
131 |
||
132 |
subsection {* Derived operations *} |
|
133 |
||
134 |
definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
135 |
[simp]: "set_eq = op =" |
|
136 |
||
34020 | 137 |
lemma [code_unfold]: |
33947 | 138 |
"op = = set_eq" |
139 |
by simp |
|
140 |
||
141 |
definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
142 |
[simp]: "subset_eq = op \<subseteq>" |
|
143 |
||
34020 | 144 |
lemma [code_unfold]: |
33947 | 145 |
"op \<subseteq> = subset_eq" |
146 |
by simp |
|
147 |
||
148 |
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
149 |
[simp]: "subset = op \<subset>" |
|
150 |
||
34020 | 151 |
lemma [code_unfold]: |
33947 | 152 |
"op \<subset> = subset" |
153 |
by simp |
|
154 |
||
155 |
setup {* |
|
156 |
Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
157 |
#> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
158 |
#> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool") |
|
159 |
*} |
|
160 |
||
161 |
lemma set_eq_subset_eq [code]: |
|
162 |
"set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A" |
|
163 |
by auto |
|
164 |
||
165 |
lemma subset_eq_forall [code]: |
|
166 |
"subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
167 |
by (simp add: subset_eq) |
|
168 |
||
169 |
lemma subset_subset_eq [code]: |
|
170 |
"subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A" |
|
171 |
by (simp add: subset) |
|
172 |
||
173 |
||
174 |
subsection {* Functorial operations *} |
|
175 |
||
176 |
definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
177 |
[simp]: "inter = op \<inter>" |
|
178 |
||
34020 | 179 |
lemma [code_unfold]: |
33947 | 180 |
"op \<inter> = inter" |
181 |
by simp |
|
182 |
||
183 |
definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
184 |
[simp]: "subtract A B = B - A" |
|
185 |
||
34020 | 186 |
lemma [code_unfold]: |
33947 | 187 |
"B - A = subtract A B" |
188 |
by simp |
|
189 |
||
190 |
definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
|
191 |
[simp]: "union = op \<union>" |
|
192 |
||
34020 | 193 |
lemma [code_unfold]: |
33947 | 194 |
"op \<union> = union" |
195 |
by simp |
|
196 |
||
197 |
definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
44860
56101fa00193
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents:
43363
diff
changeset
|
198 |
[simp]: "Inf = Complete_Lattices.Inf" |
33947 | 199 |
|
34020 | 200 |
lemma [code_unfold]: |
44860
56101fa00193
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents:
43363
diff
changeset
|
201 |
"Complete_Lattices.Inf = Inf" |
33947 | 202 |
by simp |
203 |
||
204 |
definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where |
|
44860
56101fa00193
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents:
43363
diff
changeset
|
205 |
[simp]: "Sup = Complete_Lattices.Sup" |
33947 | 206 |
|
34020 | 207 |
lemma [code_unfold]: |
44860
56101fa00193
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
haftmann
parents:
43363
diff
changeset
|
208 |
"Complete_Lattices.Sup = Sup" |
33947 | 209 |
by simp |
210 |
||
211 |
definition Inter :: "'a set set \<Rightarrow> 'a set" where |
|
212 |
[simp]: "Inter = Inf" |
|
213 |
||
34020 | 214 |
lemma [code_unfold]: |
33947 | 215 |
"Inf = Inter" |
216 |
by simp |
|
217 |
||
218 |
definition Union :: "'a set set \<Rightarrow> 'a set" where |
|
219 |
[simp]: "Union = Sup" |
|
220 |
||
34020 | 221 |
lemma [code_unfold]: |
33947 | 222 |
"Sup = Union" |
223 |
by simp |
|
224 |
||
225 |
setup {* |
|
226 |
Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
227 |
#> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
228 |
#> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set") |
|
229 |
#> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a") |
|
230 |
#> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a") |
|
231 |
#> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set") |
|
232 |
#> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set") |
|
233 |
*} |
|
234 |
||
235 |
lemma inter_project [code]: |
|
236 |
"inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)" |
|
37023 | 237 |
"inter A (Coset xs) = foldr remove xs A" |
238 |
by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr) |
|
33947 | 239 |
|
240 |
lemma subtract_remove [code]: |
|
37023 | 241 |
"subtract (Set xs) A = foldr remove xs A" |
33947 | 242 |
"subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)" |
37023 | 243 |
by (auto simp add: minus_set_foldr) |
33947 | 244 |
|
245 |
lemma union_insert [code]: |
|
37023 | 246 |
"union (Set xs) A = foldr insert xs A" |
33947 | 247 |
"union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)" |
37023 | 248 |
by (auto simp add: union_set_foldr) |
33947 | 249 |
|
250 |
lemma Inf_inf [code]: |
|
37023 | 251 |
"Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)" |
33947 | 252 |
"Inf (Coset []) = (bot :: 'a::complete_lattice)" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
253 |
by (simp_all add: Inf_set_foldr) |
33947 | 254 |
|
255 |
lemma Sup_sup [code]: |
|
37023 | 256 |
"Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)" |
33947 | 257 |
"Sup (Coset []) = (top :: 'a::complete_lattice)" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
258 |
by (simp_all add: Sup_set_foldr) |
33947 | 259 |
|
260 |
lemma Inter_inter [code]: |
|
37023 | 261 |
"Inter (Set xs) = foldr inter xs (Coset [])" |
33947 | 262 |
"Inter (Coset []) = empty" |
263 |
unfolding Inter_def Inf_inf by simp_all |
|
264 |
||
265 |
lemma Union_union [code]: |
|
37023 | 266 |
"Union (Set xs) = foldr union xs empty" |
33947 | 267 |
"Union (Coset []) = Coset []" |
268 |
unfolding Union_def Sup_sup by simp_all |
|
269 |
||
36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
wenzelm
parents:
34980
diff
changeset
|
270 |
hide_const (open) is_empty empty remove |
33947 | 271 |
set_eq subset_eq subset inter union subtract Inf Sup Inter Union |
272 |
||
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
273 |
|
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
274 |
subsection {* Operations on relations *} |
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
275 |
|
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
276 |
text {* Initially contributed by Tjark Weber. *} |
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
277 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
278 |
lemma [code]: |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
279 |
"Domain r = fst ` r" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
280 |
by (fact Domain_fst) |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
281 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
282 |
lemma [code]: |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
283 |
"Range r = snd ` r" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
284 |
by (fact Range_snd) |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
285 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
286 |
lemma [code]: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
287 |
"trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
288 |
by (fact trans_join) |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
289 |
|
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
290 |
lemma [code]: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
291 |
"irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
292 |
by (fact irrefl_distinct) |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
293 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
294 |
lemma [code]: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
295 |
"acyclic r \<longleftrightarrow> irrefl (r^+)" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
296 |
by (fact acyclic_irrefl) |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
297 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
298 |
lemma [code]: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
299 |
"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:
44860
diff
changeset
|
300 |
by (unfold Set_def) (fact product_code) |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
301 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
302 |
lemma [code]: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
303 |
"Id_on (Set xs) = Set [(x, x). x \<leftarrow> xs]" |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
304 |
by (unfold Set_def) (fact Id_on_set) |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
305 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
306 |
lemma [code]: |
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
307 |
"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:
44860
diff
changeset
|
308 |
by (unfold Set_def) (fact set_rel_comp) |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
309 |
|
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
310 |
lemma [code]: |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
311 |
"wf (Set xs) = acyclic (Set xs)" |
45012
060f76635bfe
tuned specification and lemma distribution among theories; tuned proofs
haftmann
parents:
44860
diff
changeset
|
312 |
by (unfold Set_def) (fact wf_set) |
38304
df7d5143db55
executable relation operations contributed by Tjark Weber
haftmann
parents:
37595
diff
changeset
|
313 |
|
33947 | 314 |
end |