src/HOL/Library/Executable_Set.thy
author haftmann
Mon Dec 07 14:54:01 2009 +0100 (2009-12-07)
changeset 34020 2573c794034c
parent 34008 src/HOL/Library/Crude_Executable_Set.thy@1ce58e8c02ee
child 34022 bb37c95f0b8e
permissions -rw-r--r--
merged Crude_Executable_Set into Executable_Set
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@33947
     9
imports List_Set
haftmann@33947
    10
begin
haftmann@33947
    11
haftmann@33947
    12
declare mem_def [code del]
haftmann@33947
    13
declare Collect_def [code del]
haftmann@33947
    14
declare insert_code [code del]
haftmann@33947
    15
declare vimage_code [code del]
haftmann@33947
    16
haftmann@33947
    17
subsection {* Set representation *}
haftmann@33947
    18
haftmann@33947
    19
setup {*
haftmann@33947
    20
  Code.add_type_cmd "set"
haftmann@33947
    21
*}
haftmann@33947
    22
haftmann@33947
    23
definition Set :: "'a list \<Rightarrow> 'a set" where
haftmann@33947
    24
  [simp]: "Set = set"
haftmann@33947
    25
haftmann@33947
    26
definition Coset :: "'a list \<Rightarrow> 'a set" where
haftmann@33947
    27
  [simp]: "Coset xs = - set xs"
haftmann@33947
    28
haftmann@33947
    29
setup {*
haftmann@33947
    30
  Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
haftmann@33947
    31
  #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
haftmann@33947
    32
  #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
haftmann@33947
    33
  #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
haftmann@33947
    34
*}
haftmann@33947
    35
haftmann@33947
    36
code_datatype Set Coset
haftmann@33947
    37
haftmann@34020
    38
consts_code
haftmann@34020
    39
  Coset ("\<module>Coset")
haftmann@34020
    40
  Set ("\<module>Set")
haftmann@34020
    41
attach {*
haftmann@34020
    42
  datatype 'a set = Set of 'a list | Coset of 'a list;
haftmann@34020
    43
*} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *}
haftmann@34020
    44
haftmann@33947
    45
haftmann@33947
    46
subsection {* Basic operations *}
haftmann@33947
    47
haftmann@33947
    48
lemma [code]:
haftmann@33947
    49
  "set xs = Set (remdups xs)"
haftmann@33947
    50
  by simp
haftmann@33947
    51
haftmann@33947
    52
lemma [code]:
haftmann@33947
    53
  "x \<in> Set xs \<longleftrightarrow> member x xs"
haftmann@33947
    54
  "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
haftmann@33947
    55
  by (simp_all add: mem_iff)
haftmann@33947
    56
haftmann@33947
    57
definition is_empty :: "'a set \<Rightarrow> bool" where
haftmann@33947
    58
  [simp]: "is_empty A \<longleftrightarrow> A = {}"
haftmann@33947
    59
haftmann@34020
    60
lemma [code_unfold]:
haftmann@33947
    61
  "A = {} \<longleftrightarrow> is_empty A"
haftmann@33947
    62
  by simp
haftmann@33947
    63
haftmann@33947
    64
definition empty :: "'a set" where
haftmann@33947
    65
  [simp]: "empty = {}"
haftmann@33947
    66
haftmann@34020
    67
lemma [code_unfold]:
haftmann@33947
    68
  "{} = empty"
haftmann@33947
    69
  by simp
haftmann@33947
    70
haftmann@34020
    71
lemma [code_unfold, code_inline del]:
haftmann@34020
    72
  "empty = Set []"
haftmann@34020
    73
  by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
haftmann@34020
    74
haftmann@33947
    75
setup {*
haftmann@33947
    76
  Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
haftmann@33947
    77
  #> Code.add_signature_cmd ("empty", "'a set")
haftmann@33947
    78
  #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
    79
  #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
    80
  #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
haftmann@33947
    81
  #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
    82
  #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
haftmann@33947
    83
  #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
haftmann@33947
    84
  #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
haftmann@33947
    85
*}
haftmann@33947
    86
haftmann@33947
    87
lemma is_empty_Set [code]:
haftmann@33947
    88
  "is_empty (Set xs) \<longleftrightarrow> null xs"
haftmann@33947
    89
  by (simp add: empty_null)
haftmann@33947
    90
haftmann@33947
    91
lemma empty_Set [code]:
haftmann@33947
    92
  "empty = Set []"
haftmann@33947
    93
  by simp
haftmann@33947
    94
haftmann@33947
    95
lemma insert_Set [code]:
haftmann@33947
    96
  "insert x (Set xs) = Set (List_Set.insert x xs)"
haftmann@33947
    97
  "insert x (Coset xs) = Coset (remove_all x xs)"
haftmann@33947
    98
  by (simp_all add: insert_set insert_set_compl)
haftmann@33947
    99
haftmann@33947
   100
lemma remove_Set [code]:
haftmann@33947
   101
  "remove x (Set xs) = Set (remove_all x xs)"
haftmann@33947
   102
  "remove x (Coset xs) = Coset (List_Set.insert x xs)"
haftmann@33947
   103
  by (simp_all add:remove_set remove_set_compl)
haftmann@33947
   104
haftmann@33947
   105
lemma image_Set [code]:
haftmann@33947
   106
  "image f (Set xs) = Set (remdups (map f xs))"
haftmann@33947
   107
  by simp
haftmann@33947
   108
haftmann@33947
   109
lemma project_Set [code]:
haftmann@33947
   110
  "project P (Set xs) = Set (filter P xs)"
haftmann@33947
   111
  by (simp add: project_set)
haftmann@33947
   112
haftmann@33947
   113
lemma Ball_Set [code]:
haftmann@33947
   114
  "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
haftmann@33947
   115
  by (simp add: ball_set)
haftmann@33947
   116
haftmann@33947
   117
lemma Bex_Set [code]:
haftmann@33947
   118
  "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
haftmann@33947
   119
  by (simp add: bex_set)
haftmann@33947
   120
haftmann@33947
   121
lemma card_Set [code]:
haftmann@33947
   122
  "card (Set xs) = length (remdups xs)"
haftmann@33947
   123
proof -
haftmann@33947
   124
  have "card (set (remdups xs)) = length (remdups xs)"
haftmann@33947
   125
    by (rule distinct_card) simp
haftmann@33947
   126
  then show ?thesis by simp
haftmann@33947
   127
qed
haftmann@33947
   128
haftmann@33947
   129
haftmann@33947
   130
subsection {* Derived operations *}
haftmann@33947
   131
haftmann@33947
   132
definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
haftmann@33947
   133
  [simp]: "set_eq = op ="
haftmann@33947
   134
haftmann@34020
   135
lemma [code_unfold]:
haftmann@33947
   136
  "op = = set_eq"
haftmann@33947
   137
  by simp
haftmann@33947
   138
haftmann@33947
   139
definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
haftmann@33947
   140
  [simp]: "subset_eq = op \<subseteq>"
haftmann@33947
   141
haftmann@34020
   142
lemma [code_unfold]:
haftmann@33947
   143
  "op \<subseteq> = subset_eq"
haftmann@33947
   144
  by simp
haftmann@33947
   145
haftmann@33947
   146
definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
haftmann@33947
   147
  [simp]: "subset = op \<subset>"
haftmann@33947
   148
haftmann@34020
   149
lemma [code_unfold]:
haftmann@33947
   150
  "op \<subset> = subset"
haftmann@33947
   151
  by simp
haftmann@33947
   152
haftmann@33947
   153
setup {*
haftmann@33947
   154
  Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
haftmann@33947
   155
  #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
haftmann@33947
   156
  #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
haftmann@33947
   157
*}
haftmann@33947
   158
haftmann@33947
   159
lemma set_eq_subset_eq [code]:
haftmann@33947
   160
  "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
haftmann@33947
   161
  by auto
haftmann@33947
   162
haftmann@33947
   163
lemma subset_eq_forall [code]:
haftmann@33947
   164
  "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
haftmann@33947
   165
  by (simp add: subset_eq)
haftmann@33947
   166
haftmann@33947
   167
lemma subset_subset_eq [code]:
haftmann@33947
   168
  "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
haftmann@33947
   169
  by (simp add: subset)
haftmann@33947
   170
haftmann@33947
   171
haftmann@33947
   172
subsection {* Functorial operations *}
haftmann@33947
   173
haftmann@33947
   174
definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@33947
   175
  [simp]: "inter = op \<inter>"
haftmann@33947
   176
haftmann@34020
   177
lemma [code_unfold]:
haftmann@33947
   178
  "op \<inter> = inter"
haftmann@33947
   179
  by simp
haftmann@33947
   180
haftmann@33947
   181
definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@33947
   182
  [simp]: "subtract A B = B - A"
haftmann@33947
   183
haftmann@34020
   184
lemma [code_unfold]:
haftmann@33947
   185
  "B - A = subtract A B"
haftmann@33947
   186
  by simp
haftmann@33947
   187
haftmann@33947
   188
definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
haftmann@33947
   189
  [simp]: "union = op \<union>"
haftmann@33947
   190
haftmann@34020
   191
lemma [code_unfold]:
haftmann@33947
   192
  "op \<union> = union"
haftmann@33947
   193
  by simp
haftmann@33947
   194
haftmann@33947
   195
definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
haftmann@33947
   196
  [simp]: "Inf = Complete_Lattice.Inf"
haftmann@33947
   197
haftmann@34020
   198
lemma [code_unfold]:
haftmann@33947
   199
  "Complete_Lattice.Inf = Inf"
haftmann@33947
   200
  by simp
haftmann@33947
   201
haftmann@33947
   202
definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
haftmann@33947
   203
  [simp]: "Sup = Complete_Lattice.Sup"
haftmann@33947
   204
haftmann@34020
   205
lemma [code_unfold]:
haftmann@33947
   206
  "Complete_Lattice.Sup = Sup"
haftmann@33947
   207
  by simp
haftmann@33947
   208
haftmann@33947
   209
definition Inter :: "'a set set \<Rightarrow> 'a set" where
haftmann@33947
   210
  [simp]: "Inter = Inf"
haftmann@33947
   211
haftmann@34020
   212
lemma [code_unfold]:
haftmann@33947
   213
  "Inf = Inter"
haftmann@33947
   214
  by simp
haftmann@33947
   215
haftmann@33947
   216
definition Union :: "'a set set \<Rightarrow> 'a set" where
haftmann@33947
   217
  [simp]: "Union = Sup"
haftmann@33947
   218
haftmann@34020
   219
lemma [code_unfold]:
haftmann@33947
   220
  "Sup = Union"
haftmann@33947
   221
  by simp
haftmann@33947
   222
haftmann@33947
   223
setup {*
haftmann@33947
   224
  Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
   225
  #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
   226
  #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
haftmann@33947
   227
  #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
haftmann@33947
   228
  #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
haftmann@33947
   229
  #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
haftmann@33947
   230
  #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
haftmann@33947
   231
*}
haftmann@33947
   232
haftmann@33947
   233
lemma inter_project [code]:
haftmann@33947
   234
  "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
haftmann@33947
   235
  "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
haftmann@33947
   236
  by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set)
haftmann@33947
   237
haftmann@33947
   238
lemma subtract_remove [code]:
haftmann@33947
   239
  "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
haftmann@33947
   240
  "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
haftmann@33947
   241
  by (auto simp add: minus_set)
haftmann@33947
   242
haftmann@33947
   243
lemma union_insert [code]:
haftmann@33947
   244
  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
haftmann@33947
   245
  "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
haftmann@33947
   246
  by (auto simp add: union_set)
haftmann@33947
   247
haftmann@33947
   248
lemma Inf_inf [code]:
haftmann@33947
   249
  "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
haftmann@33947
   250
  "Inf (Coset []) = (bot :: 'a::complete_lattice)"
haftmann@34008
   251
  by (simp_all add: Inf_UNIV Inf_set_fold)
haftmann@33947
   252
haftmann@33947
   253
lemma Sup_sup [code]:
haftmann@33947
   254
  "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
haftmann@33947
   255
  "Sup (Coset []) = (top :: 'a::complete_lattice)"
haftmann@34008
   256
  by (simp_all add: Sup_UNIV Sup_set_fold)
haftmann@33947
   257
haftmann@33947
   258
lemma Inter_inter [code]:
haftmann@33947
   259
  "Inter (Set xs) = foldl inter (Coset []) xs"
haftmann@33947
   260
  "Inter (Coset []) = empty"
haftmann@33947
   261
  unfolding Inter_def Inf_inf by simp_all
haftmann@33947
   262
haftmann@33947
   263
lemma Union_union [code]:
haftmann@33947
   264
  "Union (Set xs) = foldl union empty xs"
haftmann@33947
   265
  "Union (Coset []) = Coset []"
haftmann@33947
   266
  unfolding Union_def Sup_sup by simp_all
haftmann@33947
   267
haftmann@33947
   268
hide (open) const is_empty empty remove
haftmann@33947
   269
  set_eq subset_eq subset inter union subtract Inf Sup Inter Union
haftmann@33947
   270
haftmann@33947
   271
end