author | haftmann |
Fri, 18 Sep 2009 14:09:38 +0200 | |
changeset 32606 | b5c3a8a75772 |
parent 32587 | caa5ada96a00 |
child 32647 | e54f47f9e28b |
child 32683 | 7c1fe854ca6a |
permissions | -rw-r--r-- |
23854 | 1 |
(* Title: HOL/Library/Executable_Set.thy |
2 |
Author: Stefan Berghofer, TU Muenchen |
|
3 |
*) |
|
4 |
||
5 |
header {* Implementation of finite sets by lists *} |
|
6 |
||
7 |
theory Executable_Set |
|
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
8 |
imports Main Fset |
23854 | 9 |
begin |
10 |
||
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
11 |
subsection {* Preprocessor setup *} |
31847 | 12 |
|
13 |
declare member [code] |
|
23854 | 14 |
|
28522 | 15 |
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
16 |
"subset = op \<le>" |
|
17 |
||
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31850
diff
changeset
|
18 |
declare subset_def [symmetric, code_unfold] |
28522 | 19 |
|
31847 | 20 |
lemma [code]: |
21 |
"subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
22 |
by (simp add: subset_def subset_eq) |
|
28522 | 23 |
|
24 |
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
25 |
[code del]: "eq_set = op =" |
|
26 |
||
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
27 |
(*declare eq_set_def [symmetric, code_unfold]*) |
29107 | 28 |
|
23854 | 29 |
lemma [code]: |
31847 | 30 |
"eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
31 |
by (simp add: eq_set_def set_eq) |
|
23854 | 32 |
|
31847 | 33 |
declare inter [code] |
23854 | 34 |
|
32606
b5c3a8a75772
INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents:
32587
diff
changeset
|
35 |
declare Inter_image_eq [symmetric, code_unfold] |
b5c3a8a75772
INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents:
32587
diff
changeset
|
36 |
declare Union_image_eq [symmetric, code_unfold] |
23854 | 37 |
|
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31850
diff
changeset
|
38 |
declare List_Set.project_def [symmetric, code_unfold] |
23854 | 39 |
|
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
40 |
definition Inter :: "'a set set \<Rightarrow> 'a set" where |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
41 |
"Inter = Complete_Lattice.Inter" |
23854 | 42 |
|
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
43 |
declare Inter_def [symmetric, code_unfold] |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
44 |
|
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
45 |
definition Union :: "'a set set \<Rightarrow> 'a set" where |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
46 |
"Union = Complete_Lattice.Union" |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
47 |
|
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
48 |
declare Union_def [symmetric, code_unfold] |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
49 |
|
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
50 |
|
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
51 |
subsection {* Code generator setup *} |
23854 | 52 |
|
53 |
ML {* |
|
54 |
nonfix inter; |
|
55 |
nonfix union; |
|
56 |
nonfix subset; |
|
57 |
*} |
|
58 |
||
31847 | 59 |
definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where |
60 |
"flip f a b = f b a" |
|
23854 | 61 |
|
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
62 |
types_code |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
63 |
fset ("(_/ \<module>fset)") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
64 |
attach {* |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
65 |
datatype 'a fset = Set of 'a list; |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
66 |
*} |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
67 |
|
23854 | 68 |
consts_code |
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
69 |
Set ("\<module>Set") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
70 |
|
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
71 |
consts_code |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
72 |
"Set.empty" ("{*Fset.empty*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
73 |
"List_Set.is_empty" ("{*Fset.is_empty*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
74 |
"Set.insert" ("{*Fset.insert*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
75 |
"List_Set.remove" ("{*Fset.remove*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
76 |
"Set.image" ("{*Fset.map*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
77 |
"List_Set.project" ("{*Fset.filter*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
78 |
"Ball" ("{*flip Fset.forall*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
79 |
"Bex" ("{*flip Fset.exists*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
80 |
"op \<union>" ("{*Fset.union*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
81 |
"op \<inter>" ("{*Fset.inter*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
82 |
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}") |
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
83 |
"Union" ("{*Fset.Union*}") |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
84 |
"Inter" ("{*Fset.Inter*}") |
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
85 |
card ("{*Fset.card*}") |
31847 | 86 |
fold ("{*foldl o flip*}") |
23854 | 87 |
|
31847 | 88 |
end |