src/HOL/Library/Fset.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 34976 06df18c9a091
child 36176 3fe7e97ccca8
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
haftmann@31807
     1
haftmann@31807
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@31807
     3
haftmann@31807
     4
header {* Executable finite sets *}
haftmann@31807
     5
haftmann@31849
     6
theory Fset
haftmann@31807
     7
imports List_Set
haftmann@31807
     8
begin
haftmann@31807
     9
haftmann@31846
    10
declare mem_def [simp]
haftmann@31846
    11
haftmann@31807
    12
subsection {* Lifting *}
haftmann@31807
    13
haftmann@31807
    14
datatype 'a fset = Fset "'a set"
haftmann@31807
    15
haftmann@31807
    16
primrec member :: "'a fset \<Rightarrow> 'a set" where
haftmann@31807
    17
  "member (Fset A) = A"
haftmann@31807
    18
haftmann@34048
    19
lemma member_inject [simp]:
haftmann@34048
    20
  "member A = member B \<Longrightarrow> A = B"
haftmann@34048
    21
  by (cases A, cases B) simp
haftmann@34048
    22
haftmann@31807
    23
lemma Fset_member [simp]:
haftmann@31807
    24
  "Fset (member A) = A"
haftmann@31807
    25
  by (cases A) simp
haftmann@31807
    26
haftmann@31807
    27
definition Set :: "'a list \<Rightarrow> 'a fset" where
haftmann@31807
    28
  "Set xs = Fset (set xs)"
haftmann@31807
    29
haftmann@31807
    30
lemma member_Set [simp]:
haftmann@31807
    31
  "member (Set xs) = set xs"
haftmann@31807
    32
  by (simp add: Set_def)
haftmann@31807
    33
haftmann@32880
    34
definition Coset :: "'a list \<Rightarrow> 'a fset" where
haftmann@32880
    35
  "Coset xs = Fset (- set xs)"
haftmann@32880
    36
haftmann@32880
    37
lemma member_Coset [simp]:
haftmann@32880
    38
  "member (Coset xs) = - set xs"
haftmann@32880
    39
  by (simp add: Coset_def)
haftmann@32880
    40
haftmann@32880
    41
code_datatype Set Coset
haftmann@32880
    42
haftmann@32880
    43
lemma member_code [code]:
haftmann@32880
    44
  "member (Set xs) y \<longleftrightarrow> List.member y xs"
haftmann@32880
    45
  "member (Coset xs) y \<longleftrightarrow> \<not> List.member y xs"
haftmann@32880
    46
  by (simp_all add: mem_iff fun_Compl_def bool_Compl_def)
haftmann@32880
    47
haftmann@32880
    48
lemma member_image_UNIV [simp]:
haftmann@32880
    49
  "member ` UNIV = UNIV"
haftmann@32880
    50
proof -
haftmann@32880
    51
  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B"
haftmann@32880
    52
  proof
haftmann@32880
    53
    fix A :: "'a set"
haftmann@32880
    54
    show "A = member (Fset A)" by simp
haftmann@32880
    55
  qed
haftmann@32880
    56
  then show ?thesis by (simp add: image_def)
haftmann@32880
    57
qed
haftmann@31807
    58
haftmann@31807
    59
haftmann@34048
    60
subsection {* Lattice instantiation *}
haftmann@34048
    61
haftmann@34048
    62
instantiation fset :: (type) boolean_algebra
haftmann@34048
    63
begin
haftmann@34048
    64
haftmann@34048
    65
definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@34048
    66
  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
haftmann@34048
    67
haftmann@34048
    68
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@34048
    69
  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
haftmann@34048
    70
haftmann@34048
    71
definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@34048
    72
  [simp]: "inf A B = Fset (member A \<inter> member B)"
haftmann@34048
    73
haftmann@34048
    74
definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@34048
    75
  [simp]: "sup A B = Fset (member A \<union> member B)"
haftmann@34048
    76
haftmann@34048
    77
definition bot_fset :: "'a fset" where
haftmann@34048
    78
  [simp]: "bot = Fset {}"
haftmann@34048
    79
haftmann@34048
    80
definition top_fset :: "'a fset" where
haftmann@34048
    81
  [simp]: "top = Fset UNIV"
haftmann@34048
    82
haftmann@34048
    83
definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" where
haftmann@34048
    84
  [simp]: "- A = Fset (- (member A))"
haftmann@34048
    85
haftmann@34048
    86
definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@34048
    87
  [simp]: "A - B = Fset (member A - member B)"
haftmann@34048
    88
haftmann@34048
    89
instance proof
haftmann@34048
    90
qed auto
haftmann@34048
    91
haftmann@34048
    92
end
haftmann@34048
    93
haftmann@34048
    94
instantiation fset :: (type) complete_lattice
haftmann@34048
    95
begin
haftmann@34048
    96
haftmann@34048
    97
definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where
haftmann@34048
    98
  [simp, code del]: "Inf_fset As = Fset (Inf (image member As))"
haftmann@34048
    99
haftmann@34048
   100
definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where
haftmann@34048
   101
  [simp, code del]: "Sup_fset As = Fset (Sup (image member As))"
haftmann@34048
   102
haftmann@34048
   103
instance proof
haftmann@34048
   104
qed (auto simp add: le_fun_def le_bool_def)
haftmann@34048
   105
haftmann@34048
   106
end
haftmann@34048
   107
haftmann@31807
   108
subsection {* Basic operations *}
haftmann@31807
   109
haftmann@31807
   110
definition is_empty :: "'a fset \<Rightarrow> bool" where
haftmann@31846
   111
  [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
haftmann@31807
   112
haftmann@31807
   113
lemma is_empty_Set [code]:
haftmann@31807
   114
  "is_empty (Set xs) \<longleftrightarrow> null xs"
haftmann@31846
   115
  by (simp add: is_empty_set)
haftmann@31807
   116
haftmann@34048
   117
lemma empty_Set [code]:
haftmann@34048
   118
  "bot = Set []"
haftmann@34048
   119
  by simp
haftmann@31807
   120
haftmann@34048
   121
lemma UNIV_Set [code]:
haftmann@34048
   122
  "top = Coset []"
haftmann@34048
   123
  by simp
haftmann@31807
   124
haftmann@31807
   125
definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
   126
  [simp]: "insert x A = Fset (Set.insert x (member A))"
haftmann@31807
   127
haftmann@31807
   128
lemma insert_Set [code]:
haftmann@34976
   129
  "insert x (Set xs) = Set (List.insert x xs)"
haftmann@34976
   130
  "insert x (Coset xs) = Coset (removeAll x xs)"
haftmann@34976
   131
  by (simp_all add: Set_def Coset_def set_insert)
haftmann@31807
   132
haftmann@31807
   133
definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
   134
  [simp]: "remove x A = Fset (List_Set.remove x (member A))"
haftmann@31807
   135
haftmann@31807
   136
lemma remove_Set [code]:
haftmann@34976
   137
  "remove x (Set xs) = Set (removeAll x xs)"
haftmann@34976
   138
  "remove x (Coset xs) = Coset (List.insert x xs)"
haftmann@34976
   139
  by (simp_all add: Set_def Coset_def remove_set_compl)
haftmann@34976
   140
    (simp add: List_Set.remove_def)
haftmann@31807
   141
haftmann@31807
   142
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
haftmann@31846
   143
  [simp]: "map f A = Fset (image f (member A))"
haftmann@31807
   144
haftmann@31807
   145
lemma map_Set [code]:
haftmann@31807
   146
  "map f (Set xs) = Set (remdups (List.map f xs))"
haftmann@31846
   147
  by (simp add: Set_def)
haftmann@31807
   148
haftmann@31847
   149
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31847
   150
  [simp]: "filter P A = Fset (List_Set.project P (member A))"
haftmann@31807
   151
haftmann@31847
   152
lemma filter_Set [code]:
haftmann@31847
   153
  "filter P (Set xs) = Set (List.filter P xs)"
haftmann@31846
   154
  by (simp add: Set_def project_set)
haftmann@31807
   155
haftmann@31807
   156
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
   157
  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
haftmann@31807
   158
haftmann@31807
   159
lemma forall_Set [code]:
haftmann@31807
   160
  "forall P (Set xs) \<longleftrightarrow> list_all P xs"
haftmann@31846
   161
  by (simp add: Set_def ball_set)
haftmann@31807
   162
haftmann@31807
   163
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
   164
  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
haftmann@31807
   165
haftmann@31807
   166
lemma exists_Set [code]:
haftmann@31807
   167
  "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
haftmann@31846
   168
  by (simp add: Set_def bex_set)
haftmann@31846
   169
haftmann@31849
   170
definition card :: "'a fset \<Rightarrow> nat" where
haftmann@31849
   171
  [simp]: "card A = Finite_Set.card (member A)"
haftmann@31849
   172
haftmann@31849
   173
lemma card_Set [code]:
haftmann@31849
   174
  "card (Set xs) = length (remdups xs)"
haftmann@31849
   175
proof -
haftmann@31849
   176
  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
haftmann@31849
   177
    by (rule distinct_card) simp
haftmann@31849
   178
  then show ?thesis by (simp add: Set_def card_def)
haftmann@31849
   179
qed
haftmann@31849
   180
haftmann@31846
   181
haftmann@31846
   182
subsection {* Derived operations *}
haftmann@31846
   183
haftmann@31846
   184
lemma subfset_eq_forall [code]:
haftmann@34048
   185
  "A \<le> B \<longleftrightarrow> forall (member B) A"
haftmann@31846
   186
  by (simp add: subset_eq)
haftmann@31846
   187
haftmann@31846
   188
lemma subfset_subfset_eq [code]:
haftmann@34048
   189
  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
haftmann@34048
   190
  by (fact less_le_not_le)
haftmann@31846
   191
haftmann@31846
   192
lemma eq_fset_subfset_eq [code]:
haftmann@34048
   193
  "eq_class.eq A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
haftmann@31846
   194
  by (cases A, cases B) (simp add: eq set_eq)
haftmann@31846
   195
haftmann@31807
   196
haftmann@31807
   197
subsection {* Functorial operations *}
haftmann@31807
   198
haftmann@32880
   199
lemma inter_project [code]:
haftmann@34048
   200
  "inf A (Set xs) = Set (List.filter (member A) xs)"
haftmann@34048
   201
  "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
haftmann@31807
   202
proof -
haftmann@34048
   203
  show "inf A (Set xs) = Set (List.filter (member A) xs)"
haftmann@32880
   204
    by (simp add: inter project_def Set_def)
haftmann@32880
   205
  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
haftmann@32880
   206
    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
haftmann@34976
   207
    by (rule foldl_apply) (simp add: expand_fun_eq)
haftmann@34048
   208
  then show "inf A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
haftmann@32880
   209
    by (simp add: Diff_eq [symmetric] minus_set)
haftmann@31807
   210
qed
haftmann@31807
   211
haftmann@31807
   212
lemma subtract_remove [code]:
haftmann@34048
   213
  "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
haftmann@34048
   214
  "A - Coset xs = Set (List.filter (member A) xs)"
haftmann@31807
   215
proof -
haftmann@31807
   216
  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
haftmann@31807
   217
    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
haftmann@34976
   218
    by (rule foldl_apply) (simp add: expand_fun_eq)
haftmann@34048
   219
  then show "A - Set xs = foldl (\<lambda>A x. remove x A) A xs"
haftmann@32880
   220
    by (simp add: minus_set)
haftmann@34048
   221
  show "A - Coset xs = Set (List.filter (member A) xs)"
haftmann@32880
   222
    by (auto simp add: Coset_def Set_def)
haftmann@32880
   223
qed
haftmann@32880
   224
haftmann@32880
   225
lemma union_insert [code]:
haftmann@34048
   226
  "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
haftmann@34048
   227
  "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
haftmann@32880
   228
proof -
haftmann@32880
   229
  have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
haftmann@32880
   230
    member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
haftmann@34976
   231
    by (rule foldl_apply) (simp add: expand_fun_eq)
haftmann@34048
   232
  then show "sup (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
haftmann@32880
   233
    by (simp add: union_set)
haftmann@34048
   234
  show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
haftmann@32880
   235
    by (auto simp add: Coset_def)
haftmann@31807
   236
qed
haftmann@31807
   237
haftmann@34048
   238
context complete_lattice
haftmann@34048
   239
begin
haftmann@31807
   240
haftmann@34048
   241
definition Infimum :: "'a fset \<Rightarrow> 'a" where
haftmann@34048
   242
  [simp]: "Infimum A = Inf (member A)"
haftmann@31807
   243
haftmann@34048
   244
lemma Infimum_inf [code]:
haftmann@34048
   245
  "Infimum (Set As) = foldl inf top As"
haftmann@34048
   246
  "Infimum (Coset []) = bot"
haftmann@34048
   247
  by (simp_all add: Inf_set_fold Inf_UNIV)
haftmann@31807
   248
haftmann@34048
   249
definition Supremum :: "'a fset \<Rightarrow> 'a" where
haftmann@34048
   250
  [simp]: "Supremum A = Sup (member A)"
haftmann@34048
   251
haftmann@34048
   252
lemma Supremum_sup [code]:
haftmann@34048
   253
  "Supremum (Set As) = foldl sup bot As"
haftmann@34048
   254
  "Supremum (Coset []) = top"
haftmann@34048
   255
  by (simp_all add: Sup_set_fold Sup_UNIV)
haftmann@34048
   256
haftmann@34048
   257
end
haftmann@31807
   258
haftmann@31807
   259
haftmann@31807
   260
subsection {* Misc operations *}
haftmann@31807
   261
haftmann@31807
   262
lemma size_fset [code]:
haftmann@31807
   263
  "fset_size f A = 0"
haftmann@31807
   264
  "size A = 0"
haftmann@31807
   265
  by (cases A, simp) (cases A, simp)
haftmann@31807
   266
haftmann@31807
   267
lemma fset_case_code [code]:
haftmann@31807
   268
  "fset_case f A = f (member A)"
haftmann@31807
   269
  by (cases A) simp
haftmann@31807
   270
haftmann@31807
   271
lemma fset_rec_code [code]:
haftmann@31807
   272
  "fset_rec f A = f (member A)"
haftmann@31807
   273
  by (cases A) simp
haftmann@31807
   274
haftmann@31846
   275
haftmann@31846
   276
subsection {* Simplified simprules *}
haftmann@31846
   277
haftmann@31846
   278
lemma is_empty_simp [simp]:
haftmann@31846
   279
  "is_empty A \<longleftrightarrow> member A = {}"
haftmann@31846
   280
  by (simp add: List_Set.is_empty_def)
haftmann@31846
   281
declare is_empty_def [simp del]
haftmann@31846
   282
haftmann@31846
   283
lemma remove_simp [simp]:
haftmann@31846
   284
  "remove x A = Fset (member A - {x})"
haftmann@31846
   285
  by (simp add: List_Set.remove_def)
haftmann@31846
   286
declare remove_def [simp del]
haftmann@31846
   287
haftmann@31847
   288
lemma filter_simp [simp]:
haftmann@31847
   289
  "filter P A = Fset {x \<in> member A. P x}"
haftmann@31846
   290
  by (simp add: List_Set.project_def)
haftmann@31847
   291
declare filter_def [simp del]
haftmann@31846
   292
haftmann@31846
   293
declare mem_def [simp del]
haftmann@31846
   294
haftmann@31849
   295
haftmann@34048
   296
hide (open) const is_empty insert remove map filter forall exists card
haftmann@34048
   297
  Inter Union
haftmann@31849
   298
haftmann@31807
   299
end