src/HOL/Library/ExecutableSet.thy
author wenzelm
Thu Jun 14 23:04:39 2007 +0200 (2007-06-14)
changeset 23394 474ff28210c0
parent 22921 475ff421a6a3
permissions -rw-r--r--
tuned proofs;
berghofe@17632
     1
(*  Title:      HOL/Library/ExecutableSet.thy
berghofe@17632
     2
    ID:         $Id$
berghofe@17632
     3
    Author:     Stefan Berghofer, TU Muenchen
berghofe@17632
     4
*)
berghofe@17632
     5
berghofe@17632
     6
header {* Implementation of finite sets by lists *}
berghofe@17632
     7
berghofe@17632
     8
theory ExecutableSet
berghofe@17632
     9
imports Main
berghofe@17632
    10
begin
berghofe@17632
    11
wenzelm@22665
    12
subsection {* Definitional rewrites *}
haftmann@20597
    13
haftmann@20597
    14
instance set :: (eq) eq ..
haftmann@19791
    15
haftmann@21153
    16
lemma [code target: Set]:
haftmann@21385
    17
  "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
berghofe@17632
    18
  by blast
berghofe@17632
    19
haftmann@20597
    20
lemma [code func]:
haftmann@21572
    21
  "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
haftmann@21572
    22
  by blast
haftmann@21572
    23
haftmann@21572
    24
lemma [code func]:
haftmann@22177
    25
  "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
haftmann@22177
    26
  unfolding subset_def ..
haftmann@20597
    27
haftmann@21572
    28
lemma [code func]:
haftmann@22177
    29
  "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
haftmann@22177
    30
  by blast
haftmann@21572
    31
haftmann@21323
    32
lemma [code]:
haftmann@21323
    33
  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
haftmann@21323
    34
  unfolding bex_triv_one_point1 ..
berghofe@17632
    35
haftmann@21385
    36
definition
wenzelm@21404
    37
  filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
wenzelm@21404
    38
  "filter_set P xs = {x\<in>xs. P x}"
haftmann@20597
    39
haftmann@21385
    40
lemmas [symmetric, code inline] = filter_set_def
haftmann@21385
    41
haftmann@21385
    42
wenzelm@22665
    43
subsection {* Operations on lists *}
haftmann@19791
    44
wenzelm@22665
    45
subsubsection {* Basic definitions *}
haftmann@19791
    46
haftmann@19791
    47
definition
wenzelm@21404
    48
  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
haftmann@19791
    49
  "flip f a b = f b a"
wenzelm@21404
    50
wenzelm@21404
    51
definition
wenzelm@21404
    52
  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
haftmann@22350
    53
  "member xs x \<longleftrightarrow> x \<in> set xs"
wenzelm@21404
    54
wenzelm@21404
    55
definition
wenzelm@21404
    56
  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@19791
    57
  "insertl x xs = (if member xs x then xs else x#xs)"
haftmann@19791
    58
wenzelm@23394
    59
lemma [code target: List]: "member [] y \<longleftrightarrow> False"
haftmann@22350
    60
  and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
wenzelm@23394
    61
  unfolding member_def by (induct xs) simp_all
haftmann@19791
    62
haftmann@22177
    63
fun
haftmann@22177
    64
  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@19791
    65
  "drop_first f [] = []"
krauss@22492
    66
| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
haftmann@19791
    67
declare drop_first.simps [code del]
haftmann@19791
    68
declare drop_first.simps [code target: List]
haftmann@19791
    69
haftmann@19791
    70
declare remove1.simps [code del]
haftmann@19791
    71
lemma [code target: List]:
haftmann@19791
    72
  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
haftmann@19791
    73
proof (cases "member xs x")
haftmann@19791
    74
  case False thus ?thesis unfolding member_def by (induct xs) auto
haftmann@19791
    75
next
haftmann@19791
    76
  case True
haftmann@19791
    77
  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
haftmann@19791
    78
  with True show ?thesis by simp
haftmann@19791
    79
qed
haftmann@19791
    80
haftmann@19791
    81
lemma member_nil [simp]:
haftmann@19791
    82
  "member [] = (\<lambda>x. False)"
haftmann@19791
    83
proof
haftmann@19791
    84
  fix x
haftmann@19791
    85
  show "member [] x = False" unfolding member_def by simp
haftmann@19791
    86
qed
haftmann@19791
    87
haftmann@19791
    88
lemma member_insertl [simp]:
haftmann@19791
    89
  "x \<in> set (insertl x xs)"
haftmann@19791
    90
  unfolding insertl_def member_def mem_iff by simp
haftmann@19791
    91
haftmann@19791
    92
lemma insertl_member [simp]:
haftmann@19791
    93
  fixes xs x
haftmann@19791
    94
  assumes member: "member xs x"
haftmann@19791
    95
  shows "insertl x xs = xs"
haftmann@19791
    96
  using member unfolding insertl_def by simp
haftmann@19791
    97
haftmann@19791
    98
lemma insertl_not_member [simp]:
haftmann@19791
    99
  fixes xs x
haftmann@19791
   100
  assumes member: "\<not> (member xs x)"
haftmann@19791
   101
  shows "insertl x xs = x # xs"
haftmann@19791
   102
  using member unfolding insertl_def by simp
haftmann@19791
   103
haftmann@19791
   104
lemma foldr_remove1_empty [simp]:
haftmann@19791
   105
  "foldr remove1 xs [] = []"
haftmann@19791
   106
  by (induct xs) simp_all
haftmann@19791
   107
haftmann@19791
   108
wenzelm@22665
   109
subsubsection {* Derived definitions *}
haftmann@19791
   110
haftmann@20934
   111
function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
krauss@20523
   112
where
haftmann@19791
   113
  "unionl [] ys = ys"
krauss@20523
   114
| "unionl xs ys = foldr insertl xs ys"
krauss@20523
   115
by pat_completeness auto
krauss@21321
   116
termination by lexicographic_order
krauss@21321
   117
haftmann@19791
   118
lemmas unionl_def = unionl.simps(2)
haftmann@19791
   119
haftmann@20934
   120
function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
krauss@20523
   121
where
haftmann@19791
   122
  "intersect [] ys = []"
krauss@20523
   123
| "intersect xs [] = []"
krauss@20523
   124
| "intersect xs ys = filter (member xs) ys"
krauss@21321
   125
by pat_completeness auto
krauss@21321
   126
termination by lexicographic_order
krauss@21321
   127
haftmann@19791
   128
lemmas intersect_def = intersect.simps(3)
haftmann@19791
   129
haftmann@20934
   130
function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
krauss@20523
   131
where
haftmann@19791
   132
  "subtract [] ys = ys"
krauss@20523
   133
| "subtract xs [] = []"
krauss@20523
   134
| "subtract xs ys = foldr remove1 xs ys"
krauss@21321
   135
by pat_completeness auto
krauss@21321
   136
termination by lexicographic_order
krauss@21321
   137
haftmann@19791
   138
lemmas subtract_def = subtract.simps(3)
haftmann@19791
   139
haftmann@20934
   140
function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
krauss@20523
   141
where
haftmann@19791
   142
  "map_distinct f [] = []"
krauss@20523
   143
| "map_distinct f xs = foldr (insertl o f) xs []"
krauss@21321
   144
by pat_completeness auto
krauss@21321
   145
termination by lexicographic_order
krauss@21321
   146
haftmann@19791
   147
lemmas map_distinct_def = map_distinct.simps(2)
haftmann@19791
   148
haftmann@20934
   149
function unions :: "'a list list \<Rightarrow> 'a list"
krauss@20523
   150
where
haftmann@19791
   151
  "unions [] = []"
krauss@22492
   152
| "unions xs = foldr unionl xs []"
krauss@21321
   153
by pat_completeness auto
krauss@21321
   154
termination by lexicographic_order
krauss@21321
   155
haftmann@19791
   156
lemmas unions_def = unions.simps(2)
haftmann@19791
   157
haftmann@20934
   158
consts intersects :: "'a list list \<Rightarrow> 'a list"
haftmann@19791
   159
primrec
haftmann@19791
   160
  "intersects (x#xs) = foldr intersect xs x"
haftmann@19791
   161
haftmann@19791
   162
definition
wenzelm@21404
   163
  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
haftmann@19791
   164
  "map_union xs f = unions (map f xs)"
wenzelm@21404
   165
wenzelm@21404
   166
definition
wenzelm@21404
   167
  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
haftmann@19791
   168
  "map_inter xs f = intersects (map f xs)"
haftmann@19791
   169
haftmann@19791
   170
wenzelm@22665
   171
subsection {* Isomorphism proofs *}
haftmann@19791
   172
haftmann@19791
   173
lemma iso_member:
haftmann@22350
   174
  "member xs x \<longleftrightarrow> x \<in> set xs"
haftmann@19791
   175
  unfolding member_def mem_iff ..
haftmann@19791
   176
haftmann@19791
   177
lemma iso_insert:
haftmann@19791
   178
  "set (insertl x xs) = insert x (set xs)"
haftmann@19791
   179
  unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
haftmann@19791
   180
haftmann@19791
   181
lemma iso_remove1:
haftmann@19791
   182
  assumes distnct: "distinct xs"
haftmann@19791
   183
  shows "set (remove1 x xs) = set xs - {x}"
haftmann@21385
   184
  using distnct set_remove1_eq by auto
haftmann@19791
   185
haftmann@19791
   186
lemma iso_union:
haftmann@19791
   187
  "set (unionl xs ys) = set xs \<union> set ys"
krauss@20523
   188
  unfolding unionl_def
haftmann@21385
   189
  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
haftmann@19791
   190
haftmann@19791
   191
lemma iso_intersect:
haftmann@19791
   192
  "set (intersect xs ys) = set xs \<inter> set ys"
haftmann@19791
   193
  unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
haftmann@19791
   194
haftmann@22177
   195
definition
haftmann@22177
   196
  subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
haftmann@22177
   197
  "subtract' = flip subtract"
haftmann@22177
   198
haftmann@19791
   199
lemma iso_subtract:
haftmann@19791
   200
  fixes ys
haftmann@19791
   201
  assumes distnct: "distinct ys"
haftmann@22177
   202
  shows "set (subtract' ys xs) = set ys - set xs"
wenzelm@23394
   203
    and "distinct (subtract' ys xs)"
haftmann@22177
   204
  unfolding subtract'_def flip_def subtract_def
haftmann@21385
   205
  using distnct by (induct xs arbitrary: ys) auto
haftmann@19791
   206
haftmann@19791
   207
lemma iso_map_distinct:
haftmann@19791
   208
  "set (map_distinct f xs) = image f (set xs)"
haftmann@19791
   209
  unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
haftmann@19791
   210
haftmann@19791
   211
lemma iso_unions:
haftmann@19791
   212
  "set (unions xss) = \<Union> set (map set xss)"
wenzelm@23394
   213
  unfolding unions_def
wenzelm@23394
   214
proof (induct xss)
haftmann@19791
   215
  case Nil show ?case by simp
haftmann@19791
   216
next
haftmann@19791
   217
  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
haftmann@19791
   218
qed
haftmann@19791
   219
haftmann@19791
   220
lemma iso_intersects:
haftmann@19791
   221
  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
haftmann@19791
   222
  by (induct xss) (simp_all add: Int_def iso_member, auto)
haftmann@19791
   223
haftmann@19791
   224
lemma iso_UNION:
haftmann@19791
   225
  "set (map_union xs f) = UNION (set xs) (set o f)"
haftmann@19791
   226
  unfolding map_union_def iso_unions by simp
haftmann@19791
   227
haftmann@19791
   228
lemma iso_INTER:
haftmann@19791
   229
  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
haftmann@19791
   230
  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
haftmann@19791
   231
haftmann@19791
   232
definition
wenzelm@21404
   233
  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
haftmann@19791
   234
  "Blall = flip list_all"
wenzelm@21404
   235
definition
wenzelm@21404
   236
  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
haftmann@19791
   237
  "Blex = flip list_ex"
haftmann@19791
   238
haftmann@19791
   239
lemma iso_Ball:
haftmann@19791
   240
  "Blall xs f = Ball (set xs) f"
haftmann@19791
   241
  unfolding Blall_def flip_def by (induct xs) simp_all
haftmann@19791
   242
haftmann@19791
   243
lemma iso_Bex:
haftmann@19791
   244
  "Blex xs f = Bex (set xs) f"
haftmann@19791
   245
  unfolding Blex_def flip_def by (induct xs) simp_all
haftmann@19791
   246
haftmann@21385
   247
lemma iso_filter:
haftmann@21385
   248
  "set (filter P xs) = filter_set P (set xs)"
haftmann@21385
   249
  unfolding filter_set_def by (induct xs) auto
haftmann@19791
   250
wenzelm@22665
   251
subsection {* code generator setup *}
haftmann@19791
   252
haftmann@21008
   253
ML {*
haftmann@21008
   254
nonfix inter;
haftmann@21008
   255
nonfix union;
haftmann@21875
   256
nonfix subset;
haftmann@21008
   257
*}
haftmann@21008
   258
haftmann@21191
   259
code_modulename SML
haftmann@21191
   260
  ExecutableSet List
haftmann@21385
   261
  Set List
haftmann@21385
   262
haftmann@21911
   263
code_modulename OCaml
haftmann@21911
   264
  ExecutableSet List
haftmann@21911
   265
  Set List
haftmann@21911
   266
haftmann@21385
   267
code_modulename Haskell
haftmann@21385
   268
  ExecutableSet List
haftmann@21385
   269
  Set List
haftmann@20934
   270
haftmann@21063
   271
definition [code inline]:
haftmann@20934
   272
  "empty_list = []"
haftmann@20934
   273
haftmann@20934
   274
lemma [code func]:
haftmann@20934
   275
  "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
haftmann@20934
   276
haftmann@20934
   277
lemma [code func]:
haftmann@20934
   278
  "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
haftmann@20934
   279
haftmann@20934
   280
lemma [code func]:
haftmann@20934
   281
  "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
haftmann@20934
   282
haftmann@21385
   283
lemma [code func]:
haftmann@22177
   284
  "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
haftmann@20934
   285
haftmann@20934
   286
lemma [code func]:
haftmann@20934
   287
  "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
haftmann@20934
   288
haftmann@20934
   289
lemma [code func]:
haftmann@22744
   290
  "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
haftmann@22744
   291
haftmann@22744
   292
lemma [code func]:
haftmann@22744
   293
  "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
haftmann@22744
   294
haftmann@22744
   295
lemma [code func]:
haftmann@20934
   296
  "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
haftmann@20934
   297
haftmann@20934
   298
lemma [code func]:
haftmann@20934
   299
  "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
haftmann@20934
   300
haftmann@20934
   301
lemma [code func]:
haftmann@20934
   302
  "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
haftmann@20934
   303
haftmann@20934
   304
lemma [code func]:
haftmann@20934
   305
  "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
haftmann@20934
   306
haftmann@21385
   307
lemma [code func]:
haftmann@21385
   308
  "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
haftmann@21385
   309
haftmann@22744
   310
haftmann@20934
   311
code_abstype "'a set" "'a list" where
haftmann@21115
   312
  "{}" \<equiv> empty_list
haftmann@20934
   313
  insert \<equiv> insertl
haftmann@20934
   314
  "op \<union>" \<equiv> unionl
haftmann@20934
   315
  "op \<inter>" \<equiv> intersect
haftmann@22177
   316
  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
haftmann@20934
   317
  image \<equiv> map_distinct
haftmann@20934
   318
  Union \<equiv> unions
haftmann@20934
   319
  Inter \<equiv> intersects
haftmann@20934
   320
  UNION \<equiv> map_union
haftmann@20934
   321
  INTER \<equiv> map_inter
haftmann@20934
   322
  Ball \<equiv> Blall
haftmann@20934
   323
  Bex \<equiv> Blex
haftmann@21385
   324
  filter_set \<equiv> filter
haftmann@20934
   325
haftmann@20934
   326
wenzelm@22665
   327
subsubsection {* type serializations *}
haftmann@19791
   328
berghofe@17632
   329
types_code
berghofe@17632
   330
  set ("_ list")
berghofe@17632
   331
attach (term_of) {*
berghofe@17632
   332
fun term_of_set f T [] = Const ("{}", Type ("set", [T]))
berghofe@17632
   333
  | term_of_set f T (x :: xs) = Const ("insert",
berghofe@17632
   334
      T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
berghofe@17632
   335
*}
berghofe@17632
   336
attach (test) {*
berghofe@17632
   337
fun gen_set' aG i j = frequency
berghofe@17632
   338
  [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] ()
berghofe@17632
   339
and gen_set aG i = gen_set' aG i i;
berghofe@17632
   340
*}
berghofe@17632
   341
haftmann@19791
   342
wenzelm@22665
   343
subsubsection {* const serializations *}
haftmann@18702
   344
berghofe@17632
   345
consts_code
haftmann@22921
   346
  "{}" ("{*[]*}")
haftmann@22921
   347
  insert ("{*insertl*}")
haftmann@22921
   348
  "op \<union>" ("{*unionl*}")
haftmann@22921
   349
  "op \<inter>" ("{*intersect*}")
haftmann@22921
   350
  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
haftmann@22921
   351
  image ("{*map_distinct*}")
haftmann@22921
   352
  Union ("{*unions*}")
haftmann@22921
   353
  Inter ("{*intersects*}")
haftmann@22921
   354
  UNION ("{*map_union*}")
haftmann@22921
   355
  INTER ("{*map_inter*}")
haftmann@22921
   356
  Ball ("{*Blall*}")
haftmann@22921
   357
  Bex ("{*Blex*}")
haftmann@22921
   358
  filter_set ("{*filter*}")
berghofe@17632
   359
berghofe@17632
   360
end