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