author | haftmann |
Mon, 29 Jun 2009 12:18:56 +0200 | |
changeset 31850 | e81d0f04ffdf |
parent 31847 | 7de0e20ca24d |
child 31998 | 2c7a24f74db9 |
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 |
||
31847 | 11 |
subsection {* Derived set operations *} |
12 |
||
13 |
declare member [code] |
|
23854 | 14 |
|
28522 | 15 |
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where |
16 |
"subset = op \<le>" |
|
17 |
||
18 |
declare subset_def [symmetric, code unfold] |
|
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 |
||
29107 | 27 |
(* FIXME allow for Stefan's code generator: |
28 |
declare set_eq_subset[code unfold] |
|
29 |
*) |
|
30 |
||
23854 | 31 |
lemma [code]: |
31847 | 32 |
"eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" |
33 |
by (simp add: eq_set_def set_eq) |
|
23854 | 34 |
|
31847 | 35 |
declare inter [code] |
23854 | 36 |
|
31847 | 37 |
declare Inter_image_eq [symmetric, code] |
38 |
declare Union_image_eq [symmetric, code] |
|
23854 | 39 |
|
40 |
||
31847 | 41 |
subsection {* Rewrites for primitive operations *} |
23854 | 42 |
|
31847 | 43 |
declare List_Set.project_def [symmetric, code unfold] |
23854 | 44 |
|
45 |
||
31847 | 46 |
subsection {* code generator setup *} |
23854 | 47 |
|
48 |
ML {* |
|
49 |
nonfix inter; |
|
50 |
nonfix union; |
|
51 |
nonfix subset; |
|
52 |
*} |
|
53 |
||
31847 | 54 |
definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where |
55 |
"flip f a b = f b a" |
|
23854 | 56 |
|
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
57 |
types_code |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
58 |
fset ("(_/ \<module>fset)") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
59 |
attach {* |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
60 |
datatype 'a fset = Set of 'a list; |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
61 |
*} |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
62 |
|
23854 | 63 |
consts_code |
31850
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
64 |
Set ("\<module>Set") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
65 |
|
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
66 |
consts_code |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
67 |
"Set.empty" ("{*Fset.empty*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
68 |
"List_Set.is_empty" ("{*Fset.is_empty*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
69 |
"Set.insert" ("{*Fset.insert*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
70 |
"List_Set.remove" ("{*Fset.remove*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
71 |
"Set.image" ("{*Fset.map*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
72 |
"List_Set.project" ("{*Fset.filter*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
73 |
"Ball" ("{*flip Fset.forall*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
74 |
"Bex" ("{*flip Fset.exists*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
75 |
"op \<union>" ("{*Fset.union*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
76 |
"op \<inter>" ("{*Fset.inter*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
77 |
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
78 |
"Set.Union" ("{*Fset.Union*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
79 |
"Set.Inter" ("{*Fset.Inter*}") |
e81d0f04ffdf
Executable_Set is now a simple wrapper around Fset
haftmann
parents:
31847
diff
changeset
|
80 |
card ("{*Fset.card*}") |
31847 | 81 |
fold ("{*foldl o flip*}") |
23854 | 82 |
|
31847 | 83 |
end |