src/HOL/Library/Fset.thy
author haftmann
Sat Jun 19 06:43:33 2010 +0200 (2010-06-19)
changeset 37468 a2a3b62fc819
parent 37024 e938a0b5286e
child 37473 013f78aed840
permissions -rw-r--r--
quickcheck for fsets
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@37024
     7
imports More_Set More_List
haftmann@31807
     8
begin
haftmann@31807
     9
haftmann@31807
    10
subsection {* Lifting *}
haftmann@31807
    11
haftmann@37468
    12
typedef (open) 'a fset = "UNIV :: 'a set set"
haftmann@37468
    13
  morphisms member Fset by rule+
haftmann@31807
    14
haftmann@37468
    15
lemma member_Fset [simp]:
haftmann@31807
    16
  "member (Fset A) = A"
haftmann@37468
    17
  by (rule Fset_inverse) rule
haftmann@34048
    18
haftmann@31807
    19
lemma Fset_member [simp]:
haftmann@31807
    20
  "Fset (member A) = A"
haftmann@37468
    21
  by (rule member_inverse)
haftmann@37468
    22
haftmann@37468
    23
declare member_inject [simp]
haftmann@37468
    24
haftmann@37468
    25
lemma Fset_inject [simp]:
haftmann@37468
    26
  "Fset A = Fset B \<longleftrightarrow> A = B"
haftmann@37468
    27
  by (simp add: Fset_inject)
haftmann@37468
    28
haftmann@37468
    29
declare mem_def [simp]
haftmann@31807
    30
haftmann@31807
    31
definition Set :: "'a list \<Rightarrow> 'a fset" where
haftmann@31807
    32
  "Set xs = Fset (set xs)"
haftmann@31807
    33
haftmann@31807
    34
lemma member_Set [simp]:
haftmann@31807
    35
  "member (Set xs) = set xs"
haftmann@31807
    36
  by (simp add: Set_def)
haftmann@31807
    37
haftmann@32880
    38
definition Coset :: "'a list \<Rightarrow> 'a fset" where
haftmann@32880
    39
  "Coset xs = Fset (- set xs)"
haftmann@32880
    40
haftmann@32880
    41
lemma member_Coset [simp]:
haftmann@32880
    42
  "member (Coset xs) = - set xs"
haftmann@32880
    43
  by (simp add: Coset_def)
haftmann@32880
    44
haftmann@32880
    45
code_datatype Set Coset
haftmann@32880
    46
haftmann@32880
    47
lemma member_code [code]:
haftmann@37023
    48
  "member (Set xs) = List.member xs"
haftmann@37023
    49
  "member (Coset xs) = Not \<circ> List.member xs"
haftmann@37023
    50
  by (simp_all add: expand_fun_eq mem_iff fun_Compl_def bool_Compl_def)
haftmann@32880
    51
haftmann@32880
    52
lemma member_image_UNIV [simp]:
haftmann@32880
    53
  "member ` UNIV = UNIV"
haftmann@32880
    54
proof -
haftmann@32880
    55
  have "\<And>A \<Colon> 'a set. \<exists>B \<Colon> 'a fset. A = member B"
haftmann@32880
    56
  proof
haftmann@32880
    57
    fix A :: "'a set"
haftmann@32880
    58
    show "A = member (Fset A)" by simp
haftmann@32880
    59
  qed
haftmann@32880
    60
  then show ?thesis by (simp add: image_def)
haftmann@32880
    61
qed
haftmann@31807
    62
haftmann@37468
    63
definition (in term_syntax)
haftmann@37468
    64
  setify :: "'a\<Colon>typerep list \<times> (unit \<Rightarrow> Code_Evaluation.term)
haftmann@37468
    65
    \<Rightarrow> 'a fset \<times> (unit \<Rightarrow> Code_Evaluation.term)" where
haftmann@37468
    66
  [code_unfold]: "setify xs = Code_Evaluation.valtermify Set {\<cdot>} xs"
haftmann@37468
    67
haftmann@37468
    68
notation fcomp (infixl "o>" 60)
haftmann@37468
    69
notation scomp (infixl "o\<rightarrow>" 60)
haftmann@37468
    70
haftmann@37468
    71
instantiation fset :: (random) random
haftmann@37468
    72
begin
haftmann@37468
    73
haftmann@37468
    74
definition
haftmann@37468
    75
  "Quickcheck.random i = Quickcheck.random i o\<rightarrow> (\<lambda>xs. Pair (setify xs))"
haftmann@37468
    76
haftmann@37468
    77
instance ..
haftmann@37468
    78
haftmann@37468
    79
end
haftmann@37468
    80
haftmann@37468
    81
no_notation fcomp (infixl "o>" 60)
haftmann@37468
    82
no_notation scomp (infixl "o\<rightarrow>" 60)
haftmann@37468
    83
haftmann@31807
    84
haftmann@34048
    85
subsection {* Lattice instantiation *}
haftmann@34048
    86
haftmann@34048
    87
instantiation fset :: (type) boolean_algebra
haftmann@34048
    88
begin
haftmann@34048
    89
haftmann@34048
    90
definition less_eq_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@34048
    91
  [simp]: "A \<le> B \<longleftrightarrow> member A \<subseteq> member B"
haftmann@34048
    92
haftmann@34048
    93
definition less_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@34048
    94
  [simp]: "A < B \<longleftrightarrow> member A \<subset> member B"
haftmann@34048
    95
haftmann@34048
    96
definition inf_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@34048
    97
  [simp]: "inf A B = Fset (member A \<inter> member B)"
haftmann@34048
    98
haftmann@34048
    99
definition sup_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@34048
   100
  [simp]: "sup A B = Fset (member A \<union> member B)"
haftmann@34048
   101
haftmann@34048
   102
definition bot_fset :: "'a fset" where
haftmann@34048
   103
  [simp]: "bot = Fset {}"
haftmann@34048
   104
haftmann@34048
   105
definition top_fset :: "'a fset" where
haftmann@34048
   106
  [simp]: "top = Fset UNIV"
haftmann@34048
   107
haftmann@34048
   108
definition uminus_fset :: "'a fset \<Rightarrow> 'a fset" where
haftmann@34048
   109
  [simp]: "- A = Fset (- (member A))"
haftmann@34048
   110
haftmann@34048
   111
definition minus_fset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@34048
   112
  [simp]: "A - B = Fset (member A - member B)"
haftmann@34048
   113
haftmann@34048
   114
instance proof
haftmann@34048
   115
qed auto
haftmann@34048
   116
haftmann@34048
   117
end
haftmann@34048
   118
haftmann@34048
   119
instantiation fset :: (type) complete_lattice
haftmann@34048
   120
begin
haftmann@34048
   121
haftmann@34048
   122
definition Inf_fset :: "'a fset set \<Rightarrow> 'a fset" where
haftmann@34048
   123
  [simp, code del]: "Inf_fset As = Fset (Inf (image member As))"
haftmann@34048
   124
haftmann@34048
   125
definition Sup_fset :: "'a fset set \<Rightarrow> 'a fset" where
haftmann@34048
   126
  [simp, code del]: "Sup_fset As = Fset (Sup (image member As))"
haftmann@34048
   127
haftmann@34048
   128
instance proof
haftmann@34048
   129
qed (auto simp add: le_fun_def le_bool_def)
haftmann@34048
   130
haftmann@34048
   131
end
haftmann@34048
   132
haftmann@37023
   133
haftmann@31807
   134
subsection {* Basic operations *}
haftmann@31807
   135
haftmann@31807
   136
definition is_empty :: "'a fset \<Rightarrow> bool" where
haftmann@37024
   137
  [simp]: "is_empty A \<longleftrightarrow> More_Set.is_empty (member A)"
haftmann@31807
   138
haftmann@31807
   139
lemma is_empty_Set [code]:
haftmann@31807
   140
  "is_empty (Set xs) \<longleftrightarrow> null xs"
haftmann@31846
   141
  by (simp add: is_empty_set)
haftmann@31807
   142
haftmann@34048
   143
lemma empty_Set [code]:
haftmann@34048
   144
  "bot = Set []"
haftmann@37468
   145
  by (simp add: Set_def)
haftmann@31807
   146
haftmann@34048
   147
lemma UNIV_Set [code]:
haftmann@34048
   148
  "top = Coset []"
haftmann@37468
   149
  by (simp add: Coset_def)
haftmann@31807
   150
haftmann@31807
   151
definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
   152
  [simp]: "insert x A = Fset (Set.insert x (member A))"
haftmann@31807
   153
haftmann@31807
   154
lemma insert_Set [code]:
haftmann@34976
   155
  "insert x (Set xs) = Set (List.insert x xs)"
haftmann@34976
   156
  "insert x (Coset xs) = Coset (removeAll x xs)"
haftmann@37023
   157
  by (simp_all add: Set_def Coset_def)
haftmann@31807
   158
haftmann@31807
   159
definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@37024
   160
  [simp]: "remove x A = Fset (More_Set.remove x (member A))"
haftmann@31807
   161
haftmann@31807
   162
lemma remove_Set [code]:
haftmann@34976
   163
  "remove x (Set xs) = Set (removeAll x xs)"
haftmann@34976
   164
  "remove x (Coset xs) = Coset (List.insert x xs)"
haftmann@34976
   165
  by (simp_all add: Set_def Coset_def remove_set_compl)
haftmann@37024
   166
    (simp add: More_Set.remove_def)
haftmann@31807
   167
haftmann@31807
   168
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
haftmann@31846
   169
  [simp]: "map f A = Fset (image f (member A))"
haftmann@31807
   170
haftmann@31807
   171
lemma map_Set [code]:
haftmann@31807
   172
  "map f (Set xs) = Set (remdups (List.map f xs))"
haftmann@31846
   173
  by (simp add: Set_def)
haftmann@31807
   174
haftmann@31847
   175
definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@37024
   176
  [simp]: "filter P A = Fset (More_Set.project P (member A))"
haftmann@31807
   177
haftmann@31847
   178
lemma filter_Set [code]:
haftmann@31847
   179
  "filter P (Set xs) = Set (List.filter P xs)"
haftmann@31846
   180
  by (simp add: Set_def project_set)
haftmann@31807
   181
haftmann@31807
   182
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
   183
  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
haftmann@31807
   184
haftmann@31807
   185
lemma forall_Set [code]:
haftmann@31807
   186
  "forall P (Set xs) \<longleftrightarrow> list_all P xs"
haftmann@31846
   187
  by (simp add: Set_def ball_set)
haftmann@31807
   188
haftmann@31807
   189
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
   190
  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
haftmann@31807
   191
haftmann@31807
   192
lemma exists_Set [code]:
haftmann@31807
   193
  "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
haftmann@31846
   194
  by (simp add: Set_def bex_set)
haftmann@31846
   195
haftmann@31849
   196
definition card :: "'a fset \<Rightarrow> nat" where
haftmann@31849
   197
  [simp]: "card A = Finite_Set.card (member A)"
haftmann@31849
   198
haftmann@31849
   199
lemma card_Set [code]:
haftmann@31849
   200
  "card (Set xs) = length (remdups xs)"
haftmann@31849
   201
proof -
haftmann@31849
   202
  have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
haftmann@31849
   203
    by (rule distinct_card) simp
haftmann@37023
   204
  then show ?thesis by (simp add: Set_def)
haftmann@31849
   205
qed
haftmann@31849
   206
haftmann@37023
   207
lemma compl_Set [simp, code]:
haftmann@37023
   208
  "- Set xs = Coset xs"
haftmann@37023
   209
  by (simp add: Set_def Coset_def)
haftmann@37023
   210
haftmann@37023
   211
lemma compl_Coset [simp, code]:
haftmann@37023
   212
  "- Coset xs = Set xs"
haftmann@37023
   213
  by (simp add: Set_def Coset_def)
haftmann@37023
   214
haftmann@31846
   215
haftmann@31846
   216
subsection {* Derived operations *}
haftmann@31846
   217
haftmann@31846
   218
lemma subfset_eq_forall [code]:
haftmann@34048
   219
  "A \<le> B \<longleftrightarrow> forall (member B) A"
haftmann@31846
   220
  by (simp add: subset_eq)
haftmann@31846
   221
haftmann@31846
   222
lemma subfset_subfset_eq [code]:
haftmann@34048
   223
  "A < B \<longleftrightarrow> A \<le> B \<and> \<not> B \<le> (A :: 'a fset)"
haftmann@34048
   224
  by (fact less_le_not_le)
haftmann@31846
   225
haftmann@37468
   226
instantiation fset :: (type) eq
haftmann@37468
   227
begin
haftmann@37468
   228
haftmann@37468
   229
definition
haftmann@37468
   230
  "eq_fset A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
haftmann@37468
   231
haftmann@37468
   232
instance proof
haftmann@37468
   233
qed (simp add: eq_fset_def set_eq [symmetric])
haftmann@37468
   234
haftmann@37468
   235
end
haftmann@31846
   236
haftmann@31807
   237
haftmann@31807
   238
subsection {* Functorial operations *}
haftmann@31807
   239
haftmann@32880
   240
lemma inter_project [code]:
haftmann@34048
   241
  "inf A (Set xs) = Set (List.filter (member A) xs)"
haftmann@37023
   242
  "inf A (Coset xs) = foldr remove xs A"
haftmann@31807
   243
proof -
haftmann@34048
   244
  show "inf A (Set xs) = Set (List.filter (member A) xs)"
haftmann@32880
   245
    by (simp add: inter project_def Set_def)
haftmann@37024
   246
  have *: "\<And>x::'a. remove = (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member)"
haftmann@37023
   247
    by (simp add: expand_fun_eq)
haftmann@37024
   248
  have "member \<circ> fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs =
haftmann@37024
   249
    fold More_Set.remove xs \<circ> member"
haftmann@37023
   250
    by (rule fold_apply) (simp add: expand_fun_eq)
haftmann@37024
   251
  then have "fold More_Set.remove xs (member A) = 
haftmann@37024
   252
    member (fold (\<lambda>x. Fset \<circ> More_Set.remove x \<circ> member) xs A)"
haftmann@37023
   253
    by (simp add: expand_fun_eq)
haftmann@37023
   254
  then have "inf A (Coset xs) = fold remove xs A"
haftmann@37023
   255
    by (simp add: Diff_eq [symmetric] minus_set *)
haftmann@37023
   256
  moreover have "\<And>x y :: 'a. Fset.remove y \<circ> Fset.remove x = Fset.remove x \<circ> Fset.remove y"
haftmann@37024
   257
    by (auto simp add: More_Set.remove_def * intro: ext)
haftmann@37023
   258
  ultimately show "inf A (Coset xs) = foldr remove xs A"
haftmann@37023
   259
    by (simp add: foldr_fold)
haftmann@31807
   260
qed
haftmann@31807
   261
haftmann@31807
   262
lemma subtract_remove [code]:
haftmann@37023
   263
  "A - Set xs = foldr remove xs A"
haftmann@34048
   264
  "A - Coset xs = Set (List.filter (member A) xs)"
haftmann@37023
   265
  by (simp_all only: diff_eq compl_Set compl_Coset inter_project)
haftmann@32880
   266
haftmann@32880
   267
lemma union_insert [code]:
haftmann@37023
   268
  "sup (Set xs) A = foldr insert xs A"
haftmann@34048
   269
  "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
haftmann@32880
   270
proof -
haftmann@37023
   271
  have *: "\<And>x::'a. insert = (\<lambda>x. Fset \<circ> Set.insert x \<circ> member)"
haftmann@37023
   272
    by (simp add: expand_fun_eq)
haftmann@37023
   273
  have "member \<circ> fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs =
haftmann@37023
   274
    fold Set.insert xs \<circ> member"
haftmann@37023
   275
    by (rule fold_apply) (simp add: expand_fun_eq)
haftmann@37023
   276
  then have "fold Set.insert xs (member A) =
haftmann@37023
   277
    member (fold (\<lambda>x. Fset \<circ> Set.insert x \<circ> member) xs A)"
haftmann@37023
   278
    by (simp add: expand_fun_eq)
haftmann@37023
   279
  then have "sup (Set xs) A = fold insert xs A"
haftmann@37023
   280
    by (simp add: union_set *)
haftmann@37023
   281
  moreover have "\<And>x y :: 'a. Fset.insert y \<circ> Fset.insert x = Fset.insert x \<circ> Fset.insert y"
haftmann@37023
   282
    by (auto simp add: * intro: ext)
haftmann@37023
   283
  ultimately show "sup (Set xs) A = foldr insert xs A"
haftmann@37023
   284
    by (simp add: foldr_fold)
haftmann@34048
   285
  show "sup (Coset xs) A = Coset (List.filter (Not \<circ> member A) xs)"
haftmann@32880
   286
    by (auto simp add: Coset_def)
haftmann@31807
   287
qed
haftmann@31807
   288
haftmann@34048
   289
context complete_lattice
haftmann@34048
   290
begin
haftmann@31807
   291
haftmann@34048
   292
definition Infimum :: "'a fset \<Rightarrow> 'a" where
haftmann@34048
   293
  [simp]: "Infimum A = Inf (member A)"
haftmann@31807
   294
haftmann@34048
   295
lemma Infimum_inf [code]:
haftmann@37023
   296
  "Infimum (Set As) = foldr inf As top"
haftmann@34048
   297
  "Infimum (Coset []) = bot"
haftmann@37023
   298
  by (simp_all add: Inf_set_foldr Inf_UNIV)
haftmann@31807
   299
haftmann@34048
   300
definition Supremum :: "'a fset \<Rightarrow> 'a" where
haftmann@34048
   301
  [simp]: "Supremum A = Sup (member A)"
haftmann@34048
   302
haftmann@34048
   303
lemma Supremum_sup [code]:
haftmann@37023
   304
  "Supremum (Set As) = foldr sup As bot"
haftmann@34048
   305
  "Supremum (Coset []) = top"
haftmann@37023
   306
  by (simp_all add: Sup_set_foldr Sup_UNIV)
haftmann@34048
   307
haftmann@34048
   308
end
haftmann@31807
   309
haftmann@31807
   310
haftmann@31846
   311
subsection {* Simplified simprules *}
haftmann@31846
   312
haftmann@31846
   313
lemma is_empty_simp [simp]:
haftmann@31846
   314
  "is_empty A \<longleftrightarrow> member A = {}"
haftmann@37024
   315
  by (simp add: More_Set.is_empty_def)
haftmann@31846
   316
declare is_empty_def [simp del]
haftmann@31846
   317
haftmann@31846
   318
lemma remove_simp [simp]:
haftmann@31846
   319
  "remove x A = Fset (member A - {x})"
haftmann@37024
   320
  by (simp add: More_Set.remove_def)
haftmann@31846
   321
declare remove_def [simp del]
haftmann@31846
   322
haftmann@31847
   323
lemma filter_simp [simp]:
haftmann@31847
   324
  "filter P A = Fset {x \<in> member A. P x}"
haftmann@37024
   325
  by (simp add: More_Set.project_def)
haftmann@31847
   326
declare filter_def [simp del]
haftmann@31846
   327
haftmann@31846
   328
declare mem_def [simp del]
haftmann@31846
   329
haftmann@31849
   330
haftmann@37468
   331
hide_const (open) setify is_empty insert remove map filter forall exists card
haftmann@34048
   332
  Inter Union
haftmann@31849
   333
haftmann@31807
   334
end