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