src/HOL/Library/Executable_Set.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 34980 6676fd863e02
child 36176 3fe7e97ccca8
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
     1 (*  Title:      HOL/Library/Executable_Set.thy
     2     Author:     Stefan Berghofer, TU Muenchen
     3     Author:     Florian Haftmann, TU Muenchen
     4 *)
     5 
     6 header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
     7 
     8 theory Executable_Set
     9 imports List_Set
    10 begin
    11 
    12 declare mem_def [code del]
    13 declare Collect_def [code del]
    14 declare insert_code [code del]
    15 declare vimage_code [code del]
    16 
    17 subsection {* Set representation *}
    18 
    19 setup {*
    20   Code.add_type_cmd "set"
    21 *}
    22 
    23 definition Set :: "'a list \<Rightarrow> 'a set" where
    24   [simp]: "Set = set"
    25 
    26 definition Coset :: "'a list \<Rightarrow> 'a set" where
    27   [simp]: "Coset xs = - set xs"
    28 
    29 setup {*
    30   Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
    31   #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
    32   #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
    33   #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
    34 *}
    35 
    36 code_datatype Set Coset
    37 
    38 consts_code
    39   Coset ("\<module>Coset")
    40   Set ("\<module>Set")
    41 attach {*
    42   datatype 'a set = Set of 'a list | Coset of 'a list;
    43 *} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *}
    44 
    45 
    46 subsection {* Basic operations *}
    47 
    48 lemma [code]:
    49   "set xs = Set (remdups xs)"
    50   by simp
    51 
    52 lemma [code]:
    53   "x \<in> Set xs \<longleftrightarrow> member x xs"
    54   "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
    55   by (simp_all add: mem_iff)
    56 
    57 definition is_empty :: "'a set \<Rightarrow> bool" where
    58   [simp]: "is_empty A \<longleftrightarrow> A = {}"
    59 
    60 lemma [code_unfold]:
    61   "A = {} \<longleftrightarrow> is_empty A"
    62   by simp
    63 
    64 definition empty :: "'a set" where
    65   [simp]: "empty = {}"
    66 
    67 lemma [code_unfold]:
    68   "{} = empty"
    69   by simp
    70 
    71 lemma [code_unfold, code_inline del]:
    72   "empty = Set []"
    73   by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
    74 
    75 setup {*
    76   Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
    77   #> Code.add_signature_cmd ("empty", "'a set")
    78   #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
    79   #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
    80   #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
    81   #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
    82   #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
    83   #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
    84   #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
    85 *}
    86 
    87 lemma is_empty_Set [code]:
    88   "is_empty (Set xs) \<longleftrightarrow> null xs"
    89   by (simp add: empty_null)
    90 
    91 lemma empty_Set [code]:
    92   "empty = Set []"
    93   by simp
    94 
    95 lemma insert_Set [code]:
    96   "insert x (Set xs) = Set (List.insert x xs)"
    97   "insert x (Coset xs) = Coset (removeAll x xs)"
    98   by (simp_all add: set_insert)
    99 
   100 lemma remove_Set [code]:
   101   "remove x (Set xs) = Set (removeAll x xs)"
   102   "remove x (Coset xs) = Coset (List.insert x xs)"
   103   by (auto simp add: set_insert remove_def)
   104 
   105 lemma image_Set [code]:
   106   "image f (Set xs) = Set (remdups (map f xs))"
   107   by simp
   108 
   109 lemma project_Set [code]:
   110   "project P (Set xs) = Set (filter P xs)"
   111   by (simp add: project_set)
   112 
   113 lemma Ball_Set [code]:
   114   "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
   115   by (simp add: ball_set)
   116 
   117 lemma Bex_Set [code]:
   118   "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
   119   by (simp add: bex_set)
   120 
   121 lemma card_Set [code]:
   122   "card (Set xs) = length (remdups xs)"
   123 proof -
   124   have "card (set (remdups xs)) = length (remdups xs)"
   125     by (rule distinct_card) simp
   126   then show ?thesis by simp
   127 qed
   128 
   129 
   130 subsection {* Derived operations *}
   131 
   132 definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   133   [simp]: "set_eq = op ="
   134 
   135 lemma [code_unfold]:
   136   "op = = set_eq"
   137   by simp
   138 
   139 definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   140   [simp]: "subset_eq = op \<subseteq>"
   141 
   142 lemma [code_unfold]:
   143   "op \<subseteq> = subset_eq"
   144   by simp
   145 
   146 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   147   [simp]: "subset = op \<subset>"
   148 
   149 lemma [code_unfold]:
   150   "op \<subset> = subset"
   151   by simp
   152 
   153 setup {*
   154   Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   155   #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   156   #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   157 *}
   158 
   159 lemma set_eq_subset_eq [code]:
   160   "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
   161   by auto
   162 
   163 lemma subset_eq_forall [code]:
   164   "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   165   by (simp add: subset_eq)
   166 
   167 lemma subset_subset_eq [code]:
   168   "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
   169   by (simp add: subset)
   170 
   171 
   172 subsection {* Functorial operations *}
   173 
   174 definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   175   [simp]: "inter = op \<inter>"
   176 
   177 lemma [code_unfold]:
   178   "op \<inter> = inter"
   179   by simp
   180 
   181 definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   182   [simp]: "subtract A B = B - A"
   183 
   184 lemma [code_unfold]:
   185   "B - A = subtract A B"
   186   by simp
   187 
   188 definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   189   [simp]: "union = op \<union>"
   190 
   191 lemma [code_unfold]:
   192   "op \<union> = union"
   193   by simp
   194 
   195 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
   196   [simp]: "Inf = Complete_Lattice.Inf"
   197 
   198 lemma [code_unfold]:
   199   "Complete_Lattice.Inf = Inf"
   200   by simp
   201 
   202 definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
   203   [simp]: "Sup = Complete_Lattice.Sup"
   204 
   205 lemma [code_unfold]:
   206   "Complete_Lattice.Sup = Sup"
   207   by simp
   208 
   209 definition Inter :: "'a set set \<Rightarrow> 'a set" where
   210   [simp]: "Inter = Inf"
   211 
   212 lemma [code_unfold]:
   213   "Inf = Inter"
   214   by simp
   215 
   216 definition Union :: "'a set set \<Rightarrow> 'a set" where
   217   [simp]: "Union = Sup"
   218 
   219 lemma [code_unfold]:
   220   "Sup = Union"
   221   by simp
   222 
   223 setup {*
   224   Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   225   #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   226   #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   227   #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
   228   #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
   229   #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
   230   #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
   231 *}
   232 
   233 lemma inter_project [code]:
   234   "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
   235   "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
   236   by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set)
   237 
   238 lemma subtract_remove [code]:
   239   "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
   240   "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
   241   by (auto simp add: minus_set)
   242 
   243 lemma union_insert [code]:
   244   "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   245   "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
   246   by (auto simp add: union_set)
   247 
   248 lemma Inf_inf [code]:
   249   "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
   250   "Inf (Coset []) = (bot :: 'a::complete_lattice)"
   251   by (simp_all add: Inf_UNIV Inf_set_fold)
   252 
   253 lemma Sup_sup [code]:
   254   "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
   255   "Sup (Coset []) = (top :: 'a::complete_lattice)"
   256   by (simp_all add: Sup_UNIV Sup_set_fold)
   257 
   258 lemma Inter_inter [code]:
   259   "Inter (Set xs) = foldl inter (Coset []) xs"
   260   "Inter (Coset []) = empty"
   261   unfolding Inter_def Inf_inf by simp_all
   262 
   263 lemma Union_union [code]:
   264   "Union (Set xs) = foldl union empty xs"
   265   "Union (Coset []) = Coset []"
   266   unfolding Union_def Sup_sup by simp_all
   267 
   268 hide (open) const is_empty empty remove
   269   set_eq subset_eq subset inter union subtract Inf Sup Inter Union
   270 
   271 end