author | haftmann |
Wed, 23 Sep 2009 11:34:21 +0200 | |
changeset 32700 | e743ca6e97e7 |
parent 32647 | e54f47f9e28b |
parent 32683 | 7c1fe854ca6a |
child 32702 | 457135bdd596 |
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 |
|
32683
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
15 |
definition empty :: "'a set" where |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
16 |
"empty = {}" |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
17 |
|
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
18 |
declare empty_def [symmetric, code_unfold] |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
19 |
|
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
20 |
definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
21 |
"inter = op \<inter>" |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
22 |
|
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
23 |
declare inter_def [symmetric, code_unfold] |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
24 |
|
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
25 |
definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
26 |
"union = op \<union>" |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
27 |
|
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
28 |
declare union_def [symmetric, code_unfold] |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
29 |
|
28522 | 30 |
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
31 |
"subset = op \<le>" |
|
32 |
||
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31850
diff
changeset
|
33 |
declare subset_def [symmetric, code_unfold] |
28522 | 34 |
|
31847 | 35 |
lemma [code]: |
36 |
"subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" |
|
37 |
by (simp add: subset_def subset_eq) |
|
28522 | 38 |
|
39 |
definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
|
40 |
[code del]: "eq_set = op =" |
|
41 |
||
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
42 |
(*declare eq_set_def [symmetric, code_unfold]*) |
29107 | 43 |
|
23854 | 44 |
lemma [code]: |
31847 | 45 |
"eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
46 |
by (simp add: eq_set_def set_eq) |
|
23854 | 47 |
|
31847 | 48 |
declare inter [code] |
23854 | 49 |
|
32606
b5c3a8a75772
INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents:
32587
diff
changeset
|
50 |
declare Inter_image_eq [symmetric, code_unfold] |
b5c3a8a75772
INTER and UNION are mere abbreviations for INFI and SUPR
haftmann
parents:
32587
diff
changeset
|
51 |
declare Union_image_eq [symmetric, code_unfold] |
23854 | 52 |
|
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31850
diff
changeset
|
53 |
declare List_Set.project_def [symmetric, code_unfold] |
23854 | 54 |
|
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
55 |
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
|
56 |
"Inter = Complete_Lattice.Inter" |
23854 | 57 |
|
32587
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
58 |
declare Inter_def [symmetric, code_unfold] |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
59 |
|
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
60 |
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
|
61 |
"Union = Complete_Lattice.Union" |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
62 |
|
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
63 |
declare Union_def [symmetric, code_unfold] |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
64 |
|
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
65 |
|
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
66 |
subsection {* Code generator setup *} |
23854 | 67 |
|
68 |
ML {* |
|
69 |
nonfix inter; |
|
70 |
nonfix union; |
|
71 |
nonfix subset; |
|
72 |
*} |
|
73 |
||
31847 | 74 |
definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where |
75 |
"flip f a b = f b a" |
|
23854 | 76 |
|
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
77 |
types_code |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
78 |
fset ("(_/ \<module>fset)") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
79 |
attach {* |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
80 |
datatype 'a fset = Set of 'a list; |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
81 |
*} |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
82 |
|
23854 | 83 |
consts_code |
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
84 |
Set ("\<module>Set") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
85 |
|
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
86 |
consts_code |
32683
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
87 |
"empty" ("{*Fset.empty*}") |
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
88 |
"List_Set.is_empty" ("{*Fset.is_empty*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
89 |
"Set.insert" ("{*Fset.insert*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
90 |
"List_Set.remove" ("{*Fset.remove*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
91 |
"Set.image" ("{*Fset.map*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
92 |
"List_Set.project" ("{*Fset.filter*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
93 |
"Ball" ("{*flip Fset.forall*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
94 |
"Bex" ("{*flip Fset.exists*}") |
32683
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
95 |
"union" ("{*Fset.union*}") |
7c1fe854ca6a
inter and union are mere abbreviations for inf and sup
haftmann
parents:
32606
diff
changeset
|
96 |
"inter" ("{*Fset.inter*}") |
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
97 |
"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
|
98 |
"Union" ("{*Fset.Union*}") |
caa5ada96a00
Inter and Union are mere abbreviations for Inf and Sup
haftmann
parents:
32139
diff
changeset
|
99 |
"Inter" ("{*Fset.Inter*}") |
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
100 |
card ("{*Fset.card*}") |
31847 | 101 |
fold ("{*foldl o flip*}") |
23854 | 102 |
|
32647 | 103 |
hide (open) const subset eq_set Inter Union flip |
104 |
||
31847 | 105 |
end |