src/HOL/Library/Code_Set.thy
author haftmann
Sun Jun 28 10:33:36 2009 +0200 (2009-06-28)
changeset 31846 89c37daebfdd
parent 31807 039893a9a77d
child 31847 7de0e20ca24d
permissions -rw-r--r--
added Inter, Union
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@31807
     6
theory Code_Set
haftmann@31807
     7
imports List_Set
haftmann@31807
     8
begin
haftmann@31807
     9
haftmann@31807
    10
lemma foldl_apply_inv:
haftmann@31807
    11
  assumes "\<And>x. g (h x) = x"
haftmann@31807
    12
  shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
haftmann@31807
    13
  by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
haftmann@31807
    14
haftmann@31846
    15
declare mem_def [simp]
haftmann@31846
    16
haftmann@31807
    17
subsection {* Lifting *}
haftmann@31807
    18
haftmann@31807
    19
datatype 'a fset = Fset "'a set"
haftmann@31807
    20
haftmann@31807
    21
primrec member :: "'a fset \<Rightarrow> 'a set" where
haftmann@31807
    22
  "member (Fset A) = A"
haftmann@31807
    23
haftmann@31807
    24
lemma Fset_member [simp]:
haftmann@31807
    25
  "Fset (member A) = A"
haftmann@31807
    26
  by (cases A) simp
haftmann@31807
    27
haftmann@31807
    28
definition Set :: "'a list \<Rightarrow> 'a fset" where
haftmann@31807
    29
  "Set xs = Fset (set xs)"
haftmann@31807
    30
haftmann@31807
    31
lemma member_Set [simp]:
haftmann@31807
    32
  "member (Set xs) = set xs"
haftmann@31807
    33
  by (simp add: Set_def)
haftmann@31807
    34
haftmann@31807
    35
code_datatype Set
haftmann@31807
    36
haftmann@31807
    37
haftmann@31807
    38
subsection {* Basic operations *}
haftmann@31807
    39
haftmann@31807
    40
definition is_empty :: "'a fset \<Rightarrow> bool" where
haftmann@31846
    41
  [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
haftmann@31807
    42
haftmann@31807
    43
lemma is_empty_Set [code]:
haftmann@31807
    44
  "is_empty (Set xs) \<longleftrightarrow> null xs"
haftmann@31846
    45
  by (simp add: is_empty_set)
haftmann@31807
    46
haftmann@31807
    47
definition empty :: "'a fset" where
haftmann@31846
    48
  [simp]: "empty = Fset {}"
haftmann@31807
    49
haftmann@31807
    50
lemma empty_Set [code]:
haftmann@31807
    51
  "empty = Set []"
haftmann@31846
    52
  by (simp add: Set_def)
haftmann@31807
    53
haftmann@31807
    54
definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
    55
  [simp]: "insert x A = Fset (Set.insert x (member A))"
haftmann@31807
    56
haftmann@31807
    57
lemma insert_Set [code]:
haftmann@31807
    58
  "insert x (Set xs) = Set (List_Set.insert x xs)"
haftmann@31846
    59
  by (simp add: Set_def insert_set)
haftmann@31807
    60
haftmann@31807
    61
definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
    62
  [simp]: "remove x A = Fset (List_Set.remove x (member A))"
haftmann@31807
    63
haftmann@31807
    64
lemma remove_Set [code]:
haftmann@31807
    65
  "remove x (Set xs) = Set (remove_all x xs)"
haftmann@31846
    66
  by (simp add: Set_def remove_set)
haftmann@31807
    67
haftmann@31807
    68
definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
haftmann@31846
    69
  [simp]: "map f A = Fset (image f (member A))"
haftmann@31807
    70
haftmann@31807
    71
lemma map_Set [code]:
haftmann@31807
    72
  "map f (Set xs) = Set (remdups (List.map f xs))"
haftmann@31846
    73
  by (simp add: Set_def)
haftmann@31807
    74
haftmann@31807
    75
definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
    76
  [simp]: "project P A = Fset (List_Set.project P (member A))"
haftmann@31807
    77
haftmann@31807
    78
lemma project_Set [code]:
haftmann@31807
    79
  "project P (Set xs) = Set (filter P xs)"
haftmann@31846
    80
  by (simp add: Set_def project_set)
haftmann@31807
    81
haftmann@31807
    82
definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
    83
  [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
haftmann@31807
    84
haftmann@31807
    85
lemma forall_Set [code]:
haftmann@31807
    86
  "forall P (Set xs) \<longleftrightarrow> list_all P xs"
haftmann@31846
    87
  by (simp add: Set_def ball_set)
haftmann@31807
    88
haftmann@31807
    89
definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
    90
  [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
haftmann@31807
    91
haftmann@31807
    92
lemma exists_Set [code]:
haftmann@31807
    93
  "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
haftmann@31846
    94
  by (simp add: Set_def bex_set)
haftmann@31846
    95
haftmann@31846
    96
haftmann@31846
    97
subsection {* Derived operations *}
haftmann@31846
    98
haftmann@31846
    99
lemma member_exists [code]:
haftmann@31846
   100
  "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
haftmann@31846
   101
  by simp
haftmann@31846
   102
haftmann@31846
   103
definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
   104
  [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
haftmann@31846
   105
haftmann@31846
   106
lemma subfset_eq_forall [code]:
haftmann@31846
   107
  "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
haftmann@31846
   108
  by (simp add: subset_eq)
haftmann@31846
   109
haftmann@31846
   110
definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
haftmann@31846
   111
  [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B"
haftmann@31846
   112
haftmann@31846
   113
lemma subfset_subfset_eq [code]:
haftmann@31846
   114
  "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
haftmann@31846
   115
  by (simp add: subset)
haftmann@31846
   116
haftmann@31846
   117
lemma eq_fset_subfset_eq [code]:
haftmann@31846
   118
  "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
haftmann@31846
   119
  by (cases A, cases B) (simp add: eq set_eq)
haftmann@31846
   120
haftmann@31846
   121
definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
   122
  [simp]: "inter A B = Fset (List_Set.project (member A) (member B))"
haftmann@31846
   123
haftmann@31846
   124
lemma inter_project [code]:
haftmann@31846
   125
  "inter A B = project (member A) B"
haftmann@31846
   126
  by (simp add: inter)
haftmann@31807
   127
haftmann@31807
   128
haftmann@31807
   129
subsection {* Functorial operations *}
haftmann@31807
   130
haftmann@31807
   131
definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
   132
  [simp]: "union A B = Fset (member A \<union> member B)"
haftmann@31807
   133
haftmann@31807
   134
lemma union_insert [code]:
haftmann@31807
   135
  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
haftmann@31807
   136
proof -
haftmann@31807
   137
  have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
haftmann@31807
   138
    member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
haftmann@31807
   139
    by (rule foldl_apply_inv) simp
haftmann@31846
   140
  then show ?thesis by (simp add: union_set)
haftmann@31807
   141
qed
haftmann@31807
   142
haftmann@31807
   143
definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
haftmann@31846
   144
  [simp]: "subtract A B = Fset (member B - member A)"
haftmann@31807
   145
haftmann@31807
   146
lemma subtract_remove [code]:
haftmann@31807
   147
  "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
haftmann@31807
   148
proof -
haftmann@31807
   149
  have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
haftmann@31807
   150
    member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
haftmann@31807
   151
    by (rule foldl_apply_inv) simp
haftmann@31846
   152
  then show ?thesis by (simp add: minus_set)
haftmann@31807
   153
qed
haftmann@31807
   154
haftmann@31846
   155
definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where
haftmann@31846
   156
  [simp]: "Inter A = Fset (Set.Inter (member ` member A))"
haftmann@31807
   157
haftmann@31846
   158
lemma Inter_inter [code]:
haftmann@31846
   159
  "Inter (Set (A # As)) = foldl inter A As"
haftmann@31846
   160
proof -
haftmann@31846
   161
  note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del]
haftmann@31846
   162
  have "foldl (op \<inter>) (member A) (List.map member As) = 
haftmann@31846
   163
    member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))"
haftmann@31846
   164
    by (rule foldl_apply_inv) simp
haftmann@31846
   165
  then show ?thesis
haftmann@31846
   166
    by (simp add: Inter_set image_set inter_def_raw inter foldl_map)
haftmann@31846
   167
qed
haftmann@31807
   168
haftmann@31846
   169
definition Union :: "'a fset fset \<Rightarrow> 'a fset" where
haftmann@31846
   170
  [simp]: "Union A = Fset (Set.Union (member ` member A))"
haftmann@31807
   171
haftmann@31846
   172
lemma Union_union [code]:
haftmann@31846
   173
  "Union (Set As) = foldl union empty As"
haftmann@31846
   174
proof -
haftmann@31846
   175
  note Union_image_eq [simp del] set_map [simp del]
haftmann@31846
   176
  have "foldl (op \<union>) (member empty) (List.map member As) = 
haftmann@31846
   177
    member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
haftmann@31846
   178
    by (rule foldl_apply_inv) simp
haftmann@31846
   179
  then show ?thesis
haftmann@31846
   180
    by (simp add: Union_set image_set union_def_raw foldl_map)
haftmann@31846
   181
qed
haftmann@31807
   182
haftmann@31807
   183
haftmann@31807
   184
subsection {* Misc operations *}
haftmann@31807
   185
haftmann@31807
   186
lemma size_fset [code]:
haftmann@31807
   187
  "fset_size f A = 0"
haftmann@31807
   188
  "size A = 0"
haftmann@31807
   189
  by (cases A, simp) (cases A, simp)
haftmann@31807
   190
haftmann@31807
   191
lemma fset_case_code [code]:
haftmann@31807
   192
  "fset_case f A = f (member A)"
haftmann@31807
   193
  by (cases A) simp
haftmann@31807
   194
haftmann@31807
   195
lemma fset_rec_code [code]:
haftmann@31807
   196
  "fset_rec f A = f (member A)"
haftmann@31807
   197
  by (cases A) simp
haftmann@31807
   198
haftmann@31846
   199
haftmann@31846
   200
subsection {* Simplified simprules *}
haftmann@31846
   201
haftmann@31846
   202
lemma is_empty_simp [simp]:
haftmann@31846
   203
  "is_empty A \<longleftrightarrow> member A = {}"
haftmann@31846
   204
  by (simp add: List_Set.is_empty_def)
haftmann@31846
   205
declare is_empty_def [simp del]
haftmann@31846
   206
haftmann@31846
   207
lemma remove_simp [simp]:
haftmann@31846
   208
  "remove x A = Fset (member A - {x})"
haftmann@31846
   209
  by (simp add: List_Set.remove_def)
haftmann@31846
   210
declare remove_def [simp del]
haftmann@31846
   211
haftmann@31846
   212
lemma project_simp [simp]:
haftmann@31846
   213
  "project P A = Fset {x \<in> member A. P x}"
haftmann@31846
   214
  by (simp add: List_Set.project_def)
haftmann@31846
   215
declare project_def [simp del]
haftmann@31846
   216
haftmann@31846
   217
lemma inter_simp [simp]:
haftmann@31846
   218
  "inter A B = Fset (member A \<inter> member B)"
haftmann@31846
   219
  by (simp add: inter)
haftmann@31846
   220
declare inter_def [simp del]
haftmann@31846
   221
haftmann@31846
   222
declare mem_def [simp del]
haftmann@31846
   223
haftmann@31807
   224
end