src/HOL/Library/Executable_Set.thy
author wenzelm
Mon Mar 17 22:34:26 2008 +0100 (2008-03-17)
changeset 26312 e9a65675e5e8
parent 25885 6fbc3f54f819
child 26816 e82229ee8f43
permissions -rw-r--r--
avoid rebinding of existing facts;
haftmann@23854
     1
(*  Title:      HOL/Library/Executable_Set.thy
haftmann@23854
     2
    ID:         $Id$
haftmann@23854
     3
    Author:     Stefan Berghofer, TU Muenchen
haftmann@23854
     4
*)
haftmann@23854
     5
haftmann@23854
     6
header {* Implementation of finite sets by lists *}
haftmann@23854
     7
haftmann@23854
     8
theory Executable_Set
haftmann@25595
     9
imports List
haftmann@23854
    10
begin
haftmann@23854
    11
haftmann@23854
    12
subsection {* Definitional rewrites *}
haftmann@23854
    13
haftmann@23854
    14
lemma [code target: Set]:
haftmann@23854
    15
  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
haftmann@23854
    16
  by blast
haftmann@23854
    17
haftmann@23854
    18
lemma [code]:
haftmann@23854
    19
  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
haftmann@23854
    20
  unfolding bex_triv_one_point1 ..
haftmann@23854
    21
haftmann@23854
    22
definition
haftmann@23854
    23
  filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@23854
    24
  "filter_set P xs = {x\<in>xs. P x}"
haftmann@23854
    25
haftmann@23854
    26
haftmann@23854
    27
subsection {* Operations on lists *}
haftmann@23854
    28
haftmann@23854
    29
subsubsection {* Basic definitions *}
haftmann@23854
    30
haftmann@23854
    31
definition
haftmann@23854
    32
  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
haftmann@23854
    33
  "flip f a b = f b a"
haftmann@23854
    34
haftmann@23854
    35
definition
haftmann@23854
    36
  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
haftmann@23854
    37
  "member xs x \<longleftrightarrow> x \<in> set xs"
haftmann@23854
    38
haftmann@23854
    39
definition
haftmann@23854
    40
  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@23854
    41
  "insertl x xs = (if member xs x then xs else x#xs)"
haftmann@23854
    42
haftmann@23854
    43
lemma [code target: List]: "member [] y \<longleftrightarrow> False"
haftmann@23854
    44
  and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
haftmann@23854
    45
  unfolding member_def by (induct xs) simp_all
haftmann@23854
    46
haftmann@23854
    47
fun
haftmann@23854
    48
  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@23854
    49
  "drop_first f [] = []"
haftmann@23854
    50
| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
haftmann@23854
    51
declare drop_first.simps [code del]
haftmann@23854
    52
declare drop_first.simps [code target: List]
haftmann@23854
    53
haftmann@23854
    54
declare remove1.simps [code del]
haftmann@23854
    55
lemma [code target: List]:
haftmann@23854
    56
  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
haftmann@23854
    57
proof (cases "member xs x")
haftmann@23854
    58
  case False thus ?thesis unfolding member_def by (induct xs) auto
haftmann@23854
    59
next
haftmann@23854
    60
  case True
haftmann@23854
    61
  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
haftmann@23854
    62
  with True show ?thesis by simp
haftmann@23854
    63
qed
haftmann@23854
    64
haftmann@23854
    65
lemma member_nil [simp]:
haftmann@23854
    66
  "member [] = (\<lambda>x. False)"
haftmann@23854
    67
proof
haftmann@23854
    68
  fix x
haftmann@23854
    69
  show "member [] x = False" unfolding member_def by simp
haftmann@23854
    70
qed
haftmann@23854
    71
haftmann@23854
    72
lemma member_insertl [simp]:
haftmann@23854
    73
  "x \<in> set (insertl x xs)"
haftmann@23854
    74
  unfolding insertl_def member_def mem_iff by simp
haftmann@23854
    75
haftmann@23854
    76
lemma insertl_member [simp]:
haftmann@23854
    77
  fixes xs x
haftmann@23854
    78
  assumes member: "member xs x"
haftmann@23854
    79
  shows "insertl x xs = xs"
haftmann@23854
    80
  using member unfolding insertl_def by simp
haftmann@23854
    81
haftmann@23854
    82
lemma insertl_not_member [simp]:
haftmann@23854
    83
  fixes xs x
haftmann@23854
    84
  assumes member: "\<not> (member xs x)"
haftmann@23854
    85
  shows "insertl x xs = x # xs"
haftmann@23854
    86
  using member unfolding insertl_def by simp
haftmann@23854
    87
haftmann@23854
    88
lemma foldr_remove1_empty [simp]:
haftmann@23854
    89
  "foldr remove1 xs [] = []"
haftmann@23854
    90
  by (induct xs) simp_all
haftmann@23854
    91
haftmann@23854
    92
haftmann@23854
    93
subsubsection {* Derived definitions *}
haftmann@23854
    94
haftmann@23854
    95
function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
haftmann@23854
    96
where
haftmann@23854
    97
  "unionl [] ys = ys"
haftmann@23854
    98
| "unionl xs ys = foldr insertl xs ys"
haftmann@23854
    99
by pat_completeness auto
haftmann@23854
   100
termination by lexicographic_order
haftmann@23854
   101
wenzelm@26312
   102
lemmas unionl_eq = unionl.simps(2)
haftmann@23854
   103
haftmann@23854
   104
function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
haftmann@23854
   105
where
haftmann@23854
   106
  "intersect [] ys = []"
haftmann@23854
   107
| "intersect xs [] = []"
haftmann@23854
   108
| "intersect xs ys = filter (member xs) ys"
haftmann@23854
   109
by pat_completeness auto
haftmann@23854
   110
termination by lexicographic_order
haftmann@23854
   111
wenzelm@26312
   112
lemmas intersect_eq = intersect.simps(3)
haftmann@23854
   113
haftmann@23854
   114
function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
haftmann@23854
   115
where
haftmann@23854
   116
  "subtract [] ys = ys"
haftmann@23854
   117
| "subtract xs [] = []"
haftmann@23854
   118
| "subtract xs ys = foldr remove1 xs ys"
haftmann@23854
   119
by pat_completeness auto
haftmann@23854
   120
termination by lexicographic_order
haftmann@23854
   121
wenzelm@26312
   122
lemmas subtract_eq = subtract.simps(3)
haftmann@23854
   123
haftmann@23854
   124
function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
haftmann@23854
   125
where
haftmann@23854
   126
  "map_distinct f [] = []"
haftmann@23854
   127
| "map_distinct f xs = foldr (insertl o f) xs []"
haftmann@23854
   128
by pat_completeness auto
haftmann@23854
   129
termination by lexicographic_order
haftmann@23854
   130
wenzelm@26312
   131
lemmas map_distinct_eq = map_distinct.simps(2)
haftmann@23854
   132
haftmann@23854
   133
function unions :: "'a list list \<Rightarrow> 'a list"
haftmann@23854
   134
where
haftmann@23854
   135
  "unions [] = []"
haftmann@23854
   136
| "unions xs = foldr unionl xs []"
haftmann@23854
   137
by pat_completeness auto
haftmann@23854
   138
termination by lexicographic_order
haftmann@23854
   139
wenzelm@26312
   140
lemmas unions_eq = unions.simps(2)
haftmann@23854
   141
haftmann@23854
   142
consts intersects :: "'a list list \<Rightarrow> 'a list"
haftmann@23854
   143
primrec
haftmann@23854
   144
  "intersects (x#xs) = foldr intersect xs x"
haftmann@23854
   145
haftmann@23854
   146
definition
haftmann@23854
   147
  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
haftmann@23854
   148
  "map_union xs f = unions (map f xs)"
haftmann@23854
   149
haftmann@23854
   150
definition
haftmann@23854
   151
  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
haftmann@23854
   152
  "map_inter xs f = intersects (map f xs)"
haftmann@23854
   153
haftmann@23854
   154
haftmann@23854
   155
subsection {* Isomorphism proofs *}
haftmann@23854
   156
haftmann@23854
   157
lemma iso_member:
haftmann@23854
   158
  "member xs x \<longleftrightarrow> x \<in> set xs"
haftmann@23854
   159
  unfolding member_def mem_iff ..
haftmann@23854
   160
haftmann@23854
   161
lemma iso_insert:
haftmann@23854
   162
  "set (insertl x xs) = insert x (set xs)"
haftmann@23854
   163
  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
haftmann@23854
   164
haftmann@23854
   165
lemma iso_remove1:
haftmann@23854
   166
  assumes distnct: "distinct xs"
haftmann@23854
   167
  shows "set (remove1 x xs) = set xs - {x}"
haftmann@23854
   168
  using distnct set_remove1_eq by auto
haftmann@23854
   169
haftmann@23854
   170
lemma iso_union:
haftmann@23854
   171
  "set (unionl xs ys) = set xs \<union> set ys"
wenzelm@26312
   172
  unfolding unionl_eq
haftmann@23854
   173
  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
haftmann@23854
   174
haftmann@23854
   175
lemma iso_intersect:
haftmann@23854
   176
  "set (intersect xs ys) = set xs \<inter> set ys"
wenzelm@26312
   177
  unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
haftmann@23854
   178
haftmann@23854
   179
definition
haftmann@23854
   180
  subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@23854
   181
  "subtract' = flip subtract"
haftmann@23854
   182
haftmann@23854
   183
lemma iso_subtract:
haftmann@23854
   184
  fixes ys
haftmann@23854
   185
  assumes distnct: "distinct ys"
haftmann@23854
   186
  shows "set (subtract' ys xs) = set ys - set xs"
haftmann@23854
   187
    and "distinct (subtract' ys xs)"
wenzelm@26312
   188
  unfolding subtract'_def flip_def subtract_eq
haftmann@23854
   189
  using distnct by (induct xs arbitrary: ys) auto
haftmann@23854
   190
haftmann@23854
   191
lemma iso_map_distinct:
haftmann@23854
   192
  "set (map_distinct f xs) = image f (set xs)"
wenzelm@26312
   193
  unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
haftmann@23854
   194
haftmann@23854
   195
lemma iso_unions:
haftmann@23854
   196
  "set (unions xss) = \<Union> set (map set xss)"
wenzelm@26312
   197
  unfolding unions_eq
haftmann@23854
   198
proof (induct xss)
haftmann@23854
   199
  case Nil show ?case by simp
haftmann@23854
   200
next
haftmann@23854
   201
  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
haftmann@23854
   202
qed
haftmann@23854
   203
haftmann@23854
   204
lemma iso_intersects:
haftmann@23854
   205
  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
haftmann@23854
   206
  by (induct xss) (simp_all add: Int_def iso_member, auto)
haftmann@23854
   207
haftmann@23854
   208
lemma iso_UNION:
haftmann@23854
   209
  "set (map_union xs f) = UNION (set xs) (set o f)"
haftmann@23854
   210
  unfolding map_union_def iso_unions by simp
haftmann@23854
   211
haftmann@23854
   212
lemma iso_INTER:
haftmann@23854
   213
  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
haftmann@23854
   214
  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
haftmann@23854
   215
haftmann@23854
   216
definition
haftmann@23854
   217
  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
haftmann@23854
   218
  "Blall = flip list_all"
haftmann@23854
   219
definition
haftmann@23854
   220
  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
haftmann@23854
   221
  "Blex = flip list_ex"
haftmann@23854
   222
haftmann@23854
   223
lemma iso_Ball:
haftmann@23854
   224
  "Blall xs f = Ball (set xs) f"
haftmann@23854
   225
  unfolding Blall_def flip_def by (induct xs) simp_all
haftmann@23854
   226
haftmann@23854
   227
lemma iso_Bex:
haftmann@23854
   228
  "Blex xs f = Bex (set xs) f"
haftmann@23854
   229
  unfolding Blex_def flip_def by (induct xs) simp_all
haftmann@23854
   230
haftmann@23854
   231
lemma iso_filter:
haftmann@23854
   232
  "set (filter P xs) = filter_set P (set xs)"
haftmann@23854
   233
  unfolding filter_set_def by (induct xs) auto
haftmann@23854
   234
haftmann@23854
   235
subsection {* code generator setup *}
haftmann@23854
   236
haftmann@23854
   237
ML {*
haftmann@23854
   238
nonfix inter;
haftmann@23854
   239
nonfix union;
haftmann@23854
   240
nonfix subset;
haftmann@23854
   241
*}
haftmann@23854
   242
haftmann@23854
   243
subsubsection {* type serializations *}
haftmann@23854
   244
haftmann@23854
   245
types_code
haftmann@23854
   246
  set ("_ list")
haftmann@23854
   247
attach (term_of) {*
haftmann@23854
   248
fun term_of_set f T [] = Const ("{}", Type ("set", [T]))
haftmann@23854
   249
  | term_of_set f T (x :: xs) = Const ("insert",
haftmann@23854
   250
      T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
haftmann@23854
   251
*}
haftmann@23854
   252
attach (test) {*
berghofe@25885
   253
fun gen_set' aG aT i j = frequency
berghofe@25885
   254
  [(i, fn () =>
berghofe@25885
   255
      let
berghofe@25885
   256
        val (x, t) = aG j;
berghofe@25885
   257
        val (xs, ts) = gen_set' aG aT (i-1) j
berghofe@25885
   258
      in
berghofe@25885
   259
        (x :: xs, fn () => Const ("insert",
berghofe@25885
   260
           aT --> Type ("set", [aT]) --> Type ("set", [aT])) $ t () $ ts ())
berghofe@25885
   261
      end),
berghofe@25885
   262
   (1, fn () => ([], fn () => Const ("{}", Type ("set", [aT]))))] ()
berghofe@25885
   263
and gen_set aG aT i = gen_set' aG aT i i;
haftmann@23854
   264
*}
haftmann@23854
   265
haftmann@23854
   266
haftmann@23854
   267
subsubsection {* const serializations *}
haftmann@23854
   268
haftmann@23854
   269
consts_code
haftmann@23854
   270
  "{}" ("{*[]*}")
haftmann@23854
   271
  insert ("{*insertl*}")
haftmann@23854
   272
  "op \<union>" ("{*unionl*}")
haftmann@23854
   273
  "op \<inter>" ("{*intersect*}")
haftmann@23854
   274
  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
haftmann@23854
   275
  image ("{*map_distinct*}")
haftmann@23854
   276
  Union ("{*unions*}")
haftmann@23854
   277
  Inter ("{*intersects*}")
haftmann@23854
   278
  UNION ("{*map_union*}")
haftmann@23854
   279
  INTER ("{*map_inter*}")
haftmann@23854
   280
  Ball ("{*Blall*}")
haftmann@23854
   281
  Bex ("{*Blex*}")
haftmann@23854
   282
  filter_set ("{*filter*}")
haftmann@23854
   283
haftmann@23854
   284
end