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