src/HOL/Library/Fset.thy
author haftmann
Thu May 20 16:35:54 2010 +0200 (2010-05-20)
changeset 37023 efc202e1677e
parent 36176 3fe7e97ccca8
child 37024 e938a0b5286e
permissions -rw-r--r--
added theory More_List
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@37023
     7
imports List_Set More_List
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@37023
    44
  "member (Set xs) = List.member xs"
haftmann@37023
    45
  "member (Coset xs) = Not \<circ> List.member xs"
haftmann@37023
    46
  by (simp_all add: expand_fun_eq 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@37023
   108
haftmann@31807
   109
subsection {* Basic operations *}
haftmann@31807
   110
haftmann@31807
   111
definition is_empty :: "'a fset \<Rightarrow> bool" where
haftmann@31846
   112
  [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
haftmann@31807
   113
haftmann@31807
   114
lemma is_empty_Set [code]:
haftmann@31807
   115
  "is_empty (Set xs) \<longleftrightarrow> null xs"
haftmann@31846
   116
  by (simp add: is_empty_set)
haftmann@31807
   117
haftmann@34048
   118
lemma empty_Set [code]:
haftmann@34048
   119
  "bot = Set []"
haftmann@34048
   120
  by simp
haftmann@31807
   121
haftmann@34048
   122
lemma UNIV_Set [code]:
haftmann@34048
   123
  "top = Coset []"
haftmann@34048
   124
  by simp
haftmann@31807
   125
haftmann@31807
   126
definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
   127
  [simp]: "insert x A = Fset (Set.insert x (member A))"
haftmann@31807
   128
haftmann@31807
   129
lemma insert_Set [code]:
haftmann@34976
   130
  "insert x (Set xs) = Set (List.insert x xs)"
haftmann@34976
   131
  "insert x (Coset xs) = Coset (removeAll x xs)"
haftmann@37023
   132
  by (simp_all add: Set_def Coset_def)
haftmann@31807
   133
haftmann@31807
   134
definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
   135
  [simp]: "remove x A = Fset (List_Set.remove x (member A))"
haftmann@31807
   136
haftmann@31807
   137
lemma remove_Set [code]:
haftmann@34976
   138
  "remove x (Set xs) = Set (removeAll x xs)"
haftmann@34976
   139
  "remove x (Coset xs) = Coset (List.insert x xs)"
haftmann@34976
   140
  by (simp_all add: Set_def Coset_def remove_set_compl)
haftmann@34976
   141
    (simp add: List_Set.remove_def)
haftmann@31807
   142
haftmann@31807
   143
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
haftmann@31846
   144
  [simp]: "map f A = Fset (image f (member A))"
haftmann@31807
   145
haftmann@31807
   146
lemma map_Set [code]:
haftmann@31807
   147
  "map f (Set xs) = Set (remdups (List.map f xs))"
haftmann@31846
   148
  by (simp add: Set_def)
haftmann@31807
   149
haftmann@31847
   150
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31847
   151
  [simp]: "filter P A = Fset (List_Set.project P (member A))"
haftmann@31807
   152
haftmann@31847
   153
lemma filter_Set [code]:
haftmann@31847
   154
  "filter P (Set xs) = Set (List.filter P xs)"
haftmann@31846
   155
  by (simp add: Set_def project_set)
haftmann@31807
   156
haftmann@31807
   157
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
   158
  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
haftmann@31807
   159
haftmann@31807
   160
lemma forall_Set [code]:
haftmann@31807
   161
  "forall P (Set xs) \<longleftrightarrow> list_all P xs"
haftmann@31846
   162
  by (simp add: Set_def ball_set)
haftmann@31807
   163
haftmann@31807
   164
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
   165
  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
haftmann@31807
   166
haftmann@31807
   167
lemma exists_Set [code]:
haftmann@31807
   168
  "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
haftmann@31846
   169
  by (simp add: Set_def bex_set)
haftmann@31846
   170
haftmann@31849
   171
definition card :: "'a fset \<Rightarrow> nat" where
haftmann@31849
   172
  [simp]: "card A = Finite_Set.card (member A)"
haftmann@31849
   173
haftmann@31849
   174
lemma card_Set [code]:
haftmann@31849
   175
  "card (Set xs) = length (remdups xs)"
haftmann@31849
   176
proof -
haftmann@31849
   177
  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
haftmann@31849
   178
    by (rule distinct_card) simp
haftmann@37023
   179
  then show ?thesis by (simp add: Set_def)
haftmann@31849
   180
qed
haftmann@31849
   181
haftmann@37023
   182
lemma compl_Set [simp, code]:
haftmann@37023
   183
  "- Set xs = Coset xs"
haftmann@37023
   184
  by (simp add: Set_def Coset_def)
haftmann@37023
   185
haftmann@37023
   186
lemma compl_Coset [simp, code]:
haftmann@37023
   187
  "- Coset xs = Set xs"
haftmann@37023
   188
  by (simp add: Set_def Coset_def)
haftmann@37023
   189
haftmann@31846
   190
haftmann@31846
   191
subsection {* Derived operations *}
haftmann@31846
   192
haftmann@31846
   193
lemma subfset_eq_forall [code]:
haftmann@34048
   194
  "A \<le> B \<longleftrightarrow> forall (member B) A"
haftmann@31846
   195
  by (simp add: subset_eq)
haftmann@31846
   196
haftmann@31846
   197
lemma subfset_subfset_eq [code]:
haftmann@34048
   198
  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
haftmann@34048
   199
  by (fact less_le_not_le)
haftmann@31846
   200
haftmann@31846
   201
lemma eq_fset_subfset_eq [code]:
haftmann@34048
   202
  "eq_class.eq A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
haftmann@31846
   203
  by (cases A, cases B) (simp add: eq set_eq)
haftmann@31846
   204
haftmann@31807
   205
haftmann@31807
   206
subsection {* Functorial operations *}
haftmann@31807
   207
haftmann@32880
   208
lemma inter_project [code]:
haftmann@34048
   209
  "inf A (Set xs) = Set (List.filter (member A) xs)"
haftmann@37023
   210
  "inf A (Coset xs) = foldr remove xs A"
haftmann@31807
   211
proof -
haftmann@34048
   212
  show "inf A (Set xs) = Set (List.filter (member A) xs)"
haftmann@32880
   213
    by (simp add: inter project_def Set_def)
haftmann@37023
   214
  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member)"
haftmann@37023
   215
    by (simp add: expand_fun_eq)
haftmann@37023
   216
  have "member \<circ> fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs =
haftmann@37023
   217
    fold List_Set.remove xs \<circ> member"
haftmann@37023
   218
    by (rule fold_apply) (simp add: expand_fun_eq)
haftmann@37023
   219
  then have "fold List_Set.remove xs (member A) = 
haftmann@37023
   220
    member (fold (\<lambda>x. Fset \<circ> List_Set.remove x \<circ> member) xs A)"
haftmann@37023
   221
    by (simp add: expand_fun_eq)
haftmann@37023
   222
  then have "inf A (Coset xs) = fold remove xs A"
haftmann@37023
   223
    by (simp add: Diff_eq [symmetric] minus_set *)
haftmann@37023
   224
  moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
haftmann@37023
   225
    by (auto simp add: List_Set.remove_def * intro: ext)
haftmann@37023
   226
  ultimately show "inf A (Coset xs) = foldr remove xs A"
haftmann@37023
   227
    by (simp add: foldr_fold)
haftmann@31807
   228
qed
haftmann@31807
   229
haftmann@31807
   230
lemma subtract_remove [code]:
haftmann@37023
   231
  "A - Set xs = foldr remove xs A"
haftmann@34048
   232
  "A - Coset xs = Set (List.filter (member A) xs)"
haftmann@37023
   233
  by (simp_all only: diff_eq compl_Set compl_Coset inter_project)
haftmann@32880
   234
haftmann@32880
   235
lemma union_insert [code]:
haftmann@37023
   236
  "sup (Set xs) A = foldr insert xs A"
haftmann@34048
   237
  "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
haftmann@32880
   238
proof -
haftmann@37023
   239
  have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
haftmann@37023
   240
    by (simp add: expand_fun_eq)
haftmann@37023
   241
  have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
haftmann@37023
   242
    fold Set.insert xs \<circ> member"
haftmann@37023
   243
    by (rule fold_apply) (simp add: expand_fun_eq)
haftmann@37023
   244
  then have "fold Set.insert xs (member A) =
haftmann@37023
   245
    member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
haftmann@37023
   246
    by (simp add: expand_fun_eq)
haftmann@37023
   247
  then have "sup (Set xs) A = fold insert xs A"
haftmann@37023
   248
    by (simp add: union_set *)
haftmann@37023
   249
  moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
haftmann@37023
   250
    by (auto simp add: * intro: ext)
haftmann@37023
   251
  ultimately show "sup (Set xs) A = foldr insert xs A"
haftmann@37023
   252
    by (simp add: foldr_fold)
haftmann@34048
   253
  show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
haftmann@32880
   254
    by (auto simp add: Coset_def)
haftmann@31807
   255
qed
haftmann@31807
   256
haftmann@34048
   257
context complete_lattice
haftmann@34048
   258
begin
haftmann@31807
   259
haftmann@34048
   260
definition Infimum :: "'a fset \<Rightarrow> 'a" where
haftmann@34048
   261
  [simp]: "Infimum A = Inf (member A)"
haftmann@31807
   262
haftmann@34048
   263
lemma Infimum_inf [code]:
haftmann@37023
   264
  "Infimum (Set As) = foldr inf As top"
haftmann@34048
   265
  "Infimum (Coset []) = bot"
haftmann@37023
   266
  by (simp_all add: Inf_set_foldr Inf_UNIV)
haftmann@31807
   267
haftmann@34048
   268
definition Supremum :: "'a fset \<Rightarrow> 'a" where
haftmann@34048
   269
  [simp]: "Supremum A = Sup (member A)"
haftmann@34048
   270
haftmann@34048
   271
lemma Supremum_sup [code]:
haftmann@37023
   272
  "Supremum (Set As) = foldr sup As bot"
haftmann@34048
   273
  "Supremum (Coset []) = top"
haftmann@37023
   274
  by (simp_all add: Sup_set_foldr Sup_UNIV)
haftmann@34048
   275
haftmann@34048
   276
end
haftmann@31807
   277
haftmann@31807
   278
haftmann@31807
   279
subsection {* Misc operations *}
haftmann@31807
   280
haftmann@31807
   281
lemma size_fset [code]:
haftmann@31807
   282
  "fset_size f A = 0"
haftmann@31807
   283
  "size A = 0"
haftmann@31807
   284
  by (cases A, simp) (cases A, simp)
haftmann@31807
   285
haftmann@31807
   286
lemma fset_case_code [code]:
haftmann@31807
   287
  "fset_case f A = f (member A)"
haftmann@31807
   288
  by (cases A) simp
haftmann@31807
   289
haftmann@31807
   290
lemma fset_rec_code [code]:
haftmann@31807
   291
  "fset_rec f A = f (member A)"
haftmann@31807
   292
  by (cases A) simp
haftmann@31807
   293
haftmann@31846
   294
haftmann@31846
   295
subsection {* Simplified simprules *}
haftmann@31846
   296
haftmann@31846
   297
lemma is_empty_simp [simp]:
haftmann@31846
   298
  "is_empty A \<longleftrightarrow> member A = {}"
haftmann@31846
   299
  by (simp add: List_Set.is_empty_def)
haftmann@31846
   300
declare is_empty_def [simp del]
haftmann@31846
   301
haftmann@31846
   302
lemma remove_simp [simp]:
haftmann@31846
   303
  "remove x A = Fset (member A - {x})"
haftmann@31846
   304
  by (simp add: List_Set.remove_def)
haftmann@31846
   305
declare remove_def [simp del]
haftmann@31846
   306
haftmann@31847
   307
lemma filter_simp [simp]:
haftmann@31847
   308
  "filter P A = Fset {x \<in> member A. P x}"
haftmann@31846
   309
  by (simp add: List_Set.project_def)
haftmann@31847
   310
declare filter_def [simp del]
haftmann@31846
   311
haftmann@31846
   312
declare mem_def [simp del]
haftmann@31846
   313
haftmann@31849
   314
wenzelm@36176
   315
hide_const (open) is_empty insert remove map filter forall exists card
haftmann@34048
   316
  Inter Union
haftmann@31849
   317
haftmann@31807
   318
end