src/HOL/Library/Executable_Set.thy
author hoelzl
Tue Jul 19 14:37:49 2011 +0200 (2011-07-19)
changeset 43922 c6f35921056e
parent 43363 eaf8b7f22d39
child 44860 56101fa00193
permissions -rw-r--r--
add nat => enat coercion
haftmann@34020
     1
(*  Title:      HOL/Library/Executable_Set.thy
haftmann@34020
     2
    Author:     Stefan Berghofer, TU Muenchen
haftmann@33947
     3
    Author:     Florian Haftmann, TU Muenchen
haftmann@33947
     4
*)
haftmann@33947
     5
haftmann@33947
     6
header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
haftmann@33947
     7
haftmann@34020
     8
theory Executable_Set
haftmann@37024
     9
imports More_Set
haftmann@33947
    10
begin
haftmann@33947
    11
haftmann@39141
    12
text {*
haftmann@39141
    13
  This is just an ad-hoc hack which will rarely give you what you want.
haftmann@39141
    14
  For the moment, whenever you need executable sets, consider using
haftmann@43363
    15
  type @{text Cset.set} from theory @{text Cset}.
haftmann@39141
    16
*}
haftmann@39141
    17
haftmann@33947
    18
declare mem_def [code del]
haftmann@33947
    19
declare Collect_def [code del]
haftmann@33947
    20
declare insert_code [code del]
haftmann@33947
    21
declare vimage_code [code del]
haftmann@33947
    22
haftmann@33947
    23
subsection {* Set representation *}
haftmann@33947
    24
haftmann@33947
    25
setup {*
haftmann@33947
    26
  Code.add_type_cmd "set"
haftmann@33947
    27
*}
haftmann@33947
    28
haftmann@33947
    29
definition Set :: "'a list \<Rightarrow> 'a set" where
haftmann@33947
    30
  [simp]: "Set = set"
haftmann@33947
    31
haftmann@33947
    32
definition Coset :: "'a list \<Rightarrow> 'a set" where
haftmann@33947
    33
  [simp]: "Coset xs = - set xs"
haftmann@33947
    34
haftmann@33947
    35
setup {*
haftmann@33947
    36
  Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
haftmann@33947
    37
  #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
haftmann@33947
    38
  #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
haftmann@33947
    39
  #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
haftmann@33947
    40
*}
haftmann@33947
    41
haftmann@33947
    42
code_datatype Set Coset
haftmann@33947
    43
haftmann@34020
    44
consts_code
haftmann@34020
    45
  Coset ("\<module>Coset")
haftmann@34020
    46
  Set ("\<module>Set")
haftmann@34020
    47
attach {*
haftmann@34020
    48
  datatype 'a set = Set of 'a list | Coset of 'a list;
haftmann@34020
    49
*} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *}
haftmann@34020
    50
haftmann@33947
    51
haftmann@33947
    52
subsection {* Basic operations *}
haftmann@33947
    53
haftmann@33947
    54
lemma [code]:
haftmann@33947
    55
  "set xs = Set (remdups xs)"
haftmann@33947
    56
  by simp
haftmann@33947
    57
haftmann@33947
    58
lemma [code]:
haftmann@37595
    59
  "x \<in> Set xs \<longleftrightarrow> List.member xs x"
haftmann@37595
    60
  "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
haftmann@37595
    61
  by (simp_all add: member_def)
haftmann@33947
    62
haftmann@33947
    63
definition is_empty :: "'a set \<Rightarrow> bool" where
haftmann@33947
    64
  [simp]: "is_empty A \<longleftrightarrow> A = {}"
haftmann@33947
    65
haftmann@34020
    66
lemma [code_unfold]:
haftmann@33947
    67
  "A = {} \<longleftrightarrow> is_empty A"
haftmann@33947
    68
  by simp
haftmann@33947
    69
haftmann@33947
    70
definition empty :: "'a set" where
haftmann@33947
    71
  [simp]: "empty = {}"
haftmann@33947
    72
haftmann@34020
    73
lemma [code_unfold]:
haftmann@33947
    74
  "{} = empty"
haftmann@33947
    75
  by simp
haftmann@33947
    76
haftmann@34020
    77
lemma [code_unfold, code_inline del]:
haftmann@34020
    78
  "empty = Set []"
haftmann@34020
    79
  by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
haftmann@34020
    80
haftmann@33947
    81
setup {*
haftmann@33947
    82
  Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
haftmann@33947
    83
  #> Code.add_signature_cmd ("empty", "'a set")
haftmann@33947
    84
  #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@37024
    85
  #> Code.add_signature_cmd ("More_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
    86
  #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
haftmann@37024
    87
  #> Code.add_signature_cmd ("More_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
    88
  #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
haftmann@33947
    89
  #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
haftmann@33947
    90
  #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
haftmann@33947
    91
*}
haftmann@33947
    92
haftmann@33947
    93
lemma is_empty_Set [code]:
haftmann@37595
    94
  "is_empty (Set xs) \<longleftrightarrow> List.null xs"
haftmann@37595
    95
  by (simp add: null_def)
haftmann@33947
    96
haftmann@33947
    97
lemma empty_Set [code]:
haftmann@33947
    98
  "empty = Set []"
haftmann@33947
    99
  by simp
haftmann@33947
   100
haftmann@33947
   101
lemma insert_Set [code]:
haftmann@34980
   102
  "insert x (Set xs) = Set (List.insert x xs)"
haftmann@34980
   103
  "insert x (Coset xs) = Coset (removeAll x xs)"
haftmann@34980
   104
  by (simp_all add: set_insert)
haftmann@33947
   105
haftmann@33947
   106
lemma remove_Set [code]:
haftmann@34980
   107
  "remove x (Set xs) = Set (removeAll x xs)"
haftmann@34980
   108
  "remove x (Coset xs) = Coset (List.insert x xs)"
haftmann@34980
   109
  by (auto simp add: set_insert remove_def)
haftmann@33947
   110
haftmann@33947
   111
lemma image_Set [code]:
haftmann@33947
   112
  "image f (Set xs) = Set (remdups (map f xs))"
haftmann@33947
   113
  by simp
haftmann@33947
   114
haftmann@33947
   115
lemma project_Set [code]:
haftmann@33947
   116
  "project P (Set xs) = Set (filter P xs)"
haftmann@33947
   117
  by (simp add: project_set)
haftmann@33947
   118
haftmann@33947
   119
lemma Ball_Set [code]:
haftmann@33947
   120
  "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
haftmann@37595
   121
  by (simp add: list_all_iff)
haftmann@33947
   122
haftmann@33947
   123
lemma Bex_Set [code]:
haftmann@33947
   124
  "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
haftmann@37595
   125
  by (simp add: list_ex_iff)
haftmann@33947
   126
haftmann@33947
   127
lemma card_Set [code]:
haftmann@33947
   128
  "card (Set xs) = length (remdups xs)"
haftmann@33947
   129
proof -
haftmann@33947
   130
  have "card (set (remdups xs)) = length (remdups xs)"
haftmann@33947
   131
    by (rule distinct_card) simp
haftmann@33947
   132
  then show ?thesis by simp
haftmann@33947
   133
qed
haftmann@33947
   134
haftmann@33947
   135
haftmann@33947
   136
subsection {* Derived operations *}
haftmann@33947
   137
haftmann@33947
   138
definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
haftmann@33947
   139
  [simp]: "set_eq = op ="
haftmann@33947
   140
haftmann@34020
   141
lemma [code_unfold]:
haftmann@33947
   142
  "op = = set_eq"
haftmann@33947
   143
  by simp
haftmann@33947
   144
haftmann@33947
   145
definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
haftmann@33947
   146
  [simp]: "subset_eq = op \<subseteq>"
haftmann@33947
   147
haftmann@34020
   148
lemma [code_unfold]:
haftmann@33947
   149
  "op \<subseteq> = subset_eq"
haftmann@33947
   150
  by simp
haftmann@33947
   151
haftmann@33947
   152
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
haftmann@33947
   153
  [simp]: "subset = op \<subset>"
haftmann@33947
   154
haftmann@34020
   155
lemma [code_unfold]:
haftmann@33947
   156
  "op \<subset> = subset"
haftmann@33947
   157
  by simp
haftmann@33947
   158
haftmann@33947
   159
setup {*
haftmann@33947
   160
  Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
haftmann@33947
   161
  #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
haftmann@33947
   162
  #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
haftmann@33947
   163
*}
haftmann@33947
   164
haftmann@33947
   165
lemma set_eq_subset_eq [code]:
haftmann@33947
   166
  "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
haftmann@33947
   167
  by auto
haftmann@33947
   168
haftmann@33947
   169
lemma subset_eq_forall [code]:
haftmann@33947
   170
  "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
haftmann@33947
   171
  by (simp add: subset_eq)
haftmann@33947
   172
haftmann@33947
   173
lemma subset_subset_eq [code]:
haftmann@33947
   174
  "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
haftmann@33947
   175
  by (simp add: subset)
haftmann@33947
   176
haftmann@33947
   177
haftmann@33947
   178
subsection {* Functorial operations *}
haftmann@33947
   179
haftmann@33947
   180
definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@33947
   181
  [simp]: "inter = op \<inter>"
haftmann@33947
   182
haftmann@34020
   183
lemma [code_unfold]:
haftmann@33947
   184
  "op \<inter> = inter"
haftmann@33947
   185
  by simp
haftmann@33947
   186
haftmann@33947
   187
definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@33947
   188
  [simp]: "subtract A B = B - A"
haftmann@33947
   189
haftmann@34020
   190
lemma [code_unfold]:
haftmann@33947
   191
  "B - A = subtract A B"
haftmann@33947
   192
  by simp
haftmann@33947
   193
haftmann@33947
   194
definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@33947
   195
  [simp]: "union = op \<union>"
haftmann@33947
   196
haftmann@34020
   197
lemma [code_unfold]:
haftmann@33947
   198
  "op \<union> = union"
haftmann@33947
   199
  by simp
haftmann@33947
   200
haftmann@33947
   201
definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
haftmann@33947
   202
  [simp]: "Inf = Complete_Lattice.Inf"
haftmann@33947
   203
haftmann@34020
   204
lemma [code_unfold]:
haftmann@33947
   205
  "Complete_Lattice.Inf = Inf"
haftmann@33947
   206
  by simp
haftmann@33947
   207
haftmann@33947
   208
definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
haftmann@33947
   209
  [simp]: "Sup = Complete_Lattice.Sup"
haftmann@33947
   210
haftmann@34020
   211
lemma [code_unfold]:
haftmann@33947
   212
  "Complete_Lattice.Sup = Sup"
haftmann@33947
   213
  by simp
haftmann@33947
   214
haftmann@33947
   215
definition Inter :: "'a set set \<Rightarrow> 'a set" where
haftmann@33947
   216
  [simp]: "Inter = Inf"
haftmann@33947
   217
haftmann@34020
   218
lemma [code_unfold]:
haftmann@33947
   219
  "Inf = Inter"
haftmann@33947
   220
  by simp
haftmann@33947
   221
haftmann@33947
   222
definition Union :: "'a set set \<Rightarrow> 'a set" where
haftmann@33947
   223
  [simp]: "Union = Sup"
haftmann@33947
   224
haftmann@34020
   225
lemma [code_unfold]:
haftmann@33947
   226
  "Sup = Union"
haftmann@33947
   227
  by simp
haftmann@33947
   228
haftmann@33947
   229
setup {*
haftmann@33947
   230
  Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
   231
  #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
   232
  #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
   233
  #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
haftmann@33947
   234
  #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
haftmann@33947
   235
  #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
haftmann@33947
   236
  #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
haftmann@33947
   237
*}
haftmann@33947
   238
haftmann@33947
   239
lemma inter_project [code]:
haftmann@33947
   240
  "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
haftmann@37023
   241
  "inter A (Coset xs) = foldr remove xs A"
haftmann@37023
   242
  by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
haftmann@33947
   243
haftmann@33947
   244
lemma subtract_remove [code]:
haftmann@37023
   245
  "subtract (Set xs) A = foldr remove xs A"
haftmann@33947
   246
  "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
haftmann@37023
   247
  by (auto simp add: minus_set_foldr)
haftmann@33947
   248
haftmann@33947
   249
lemma union_insert [code]:
haftmann@37023
   250
  "union (Set xs) A = foldr insert xs A"
haftmann@33947
   251
  "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
haftmann@37023
   252
  by (auto simp add: union_set_foldr)
haftmann@33947
   253
haftmann@33947
   254
lemma Inf_inf [code]:
haftmann@37023
   255
  "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
haftmann@33947
   256
  "Inf (Coset []) = (bot :: 'a::complete_lattice)"
haftmann@37023
   257
  by (simp_all add: Inf_UNIV Inf_set_foldr)
haftmann@33947
   258
haftmann@33947
   259
lemma Sup_sup [code]:
haftmann@37023
   260
  "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
haftmann@33947
   261
  "Sup (Coset []) = (top :: 'a::complete_lattice)"
haftmann@37023
   262
  by (simp_all add: Sup_UNIV Sup_set_foldr)
haftmann@33947
   263
haftmann@33947
   264
lemma Inter_inter [code]:
haftmann@37023
   265
  "Inter (Set xs) = foldr inter xs (Coset [])"
haftmann@33947
   266
  "Inter (Coset []) = empty"
haftmann@33947
   267
  unfolding Inter_def Inf_inf by simp_all
haftmann@33947
   268
haftmann@33947
   269
lemma Union_union [code]:
haftmann@37023
   270
  "Union (Set xs) = foldr union xs empty"
haftmann@33947
   271
  "Union (Coset []) = Coset []"
haftmann@33947
   272
  unfolding Union_def Sup_sup by simp_all
haftmann@33947
   273
wenzelm@36176
   274
hide_const (open) is_empty empty remove
haftmann@33947
   275
  set_eq subset_eq subset inter union subtract Inf Sup Inter Union
haftmann@33947
   276
haftmann@38304
   277
haftmann@38304
   278
subsection {* Operations on relations *}
haftmann@38304
   279
haftmann@38304
   280
text {* Initially contributed by Tjark Weber. *}
haftmann@38304
   281
haftmann@38304
   282
lemma bounded_Collect_code [code_unfold]:
haftmann@38304
   283
  "{x\<in>S. P x} = project P S"
haftmann@38304
   284
  by (auto simp add: project_def)
haftmann@38304
   285
haftmann@38304
   286
lemma Id_on_code [code]:
haftmann@38304
   287
  "Id_on (Set xs) = Set [(x,x). x \<leftarrow> xs]"
haftmann@38304
   288
  by (auto simp add: Id_on_def)
haftmann@38304
   289
haftmann@38304
   290
lemma Domain_fst [code]:
haftmann@38304
   291
  "Domain r = fst ` r"
haftmann@38304
   292
  by (auto simp add: image_def Bex_def)
haftmann@38304
   293
haftmann@38304
   294
lemma Range_snd [code]:
haftmann@38304
   295
  "Range r = snd ` r"
haftmann@38304
   296
  by (auto simp add: image_def Bex_def)
haftmann@38304
   297
haftmann@38304
   298
lemma irrefl_code [code]:
haftmann@38304
   299
  "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
haftmann@38304
   300
  by (auto simp add: irrefl_def)
haftmann@38304
   301
haftmann@38304
   302
lemma trans_def [code]:
haftmann@38304
   303
  "trans r \<longleftrightarrow> (\<forall>(x, y1)\<in>r. \<forall>(y2, z)\<in>r. y1 = y2 \<longrightarrow> (x, z)\<in>r)"
haftmann@38304
   304
  by (auto simp add: trans_def)
haftmann@38304
   305
haftmann@38304
   306
definition "exTimes A B = Sigma A (%_. B)"
haftmann@38304
   307
haftmann@38304
   308
lemma [code_unfold]:
haftmann@38304
   309
  "Sigma A (%_. B) = exTimes A B"
haftmann@38304
   310
  by (simp add: exTimes_def)
haftmann@38304
   311
haftmann@38304
   312
lemma exTimes_code [code]:
haftmann@38304
   313
  "exTimes (Set xs) (Set ys) = Set [(x,y). x \<leftarrow> xs, y \<leftarrow> ys]"
haftmann@38304
   314
  by (auto simp add: exTimes_def)
haftmann@38304
   315
haftmann@38304
   316
lemma rel_comp_code [code]:
haftmann@38304
   317
  "(Set xys) O (Set yzs) = Set (remdups [(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
haftmann@38304
   318
 by (auto simp add: Bex_def)
haftmann@38304
   319
haftmann@38304
   320
lemma acyclic_code [code]:
haftmann@38304
   321
  "acyclic r = irrefl (r^+)"
haftmann@38304
   322
  by (simp add: acyclic_def irrefl_def)
haftmann@38304
   323
haftmann@38304
   324
lemma wf_code [code]:
haftmann@38304
   325
  "wf (Set xs) = acyclic (Set xs)"
haftmann@38304
   326
  by (simp add: wf_iff_acyclic_if_finite)
haftmann@38304
   327
haftmann@33947
   328
end