src/HOL/Library/Executable_Set.thy
author bulwahn
Tue Apr 05 09:38:28 2011 +0200 (2011-04-05)
changeset 42231 bc1891226d00
parent 40672 abd4e7358847
child 43363 eaf8b7f22d39
permissions -rw-r--r--
removing bounded_forall code equation for characters when loading Code_Char
     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 More_Set
    10 begin
    11 
    12 text {*
    13   This is just an ad-hoc hack which will rarely give you what you want.
    14   For the moment, whenever you need executable sets, consider using
    15   type @{text fset} from theory @{text Cset}.
    16 *}
    17 
    18 declare mem_def [code del]
    19 declare Collect_def [code del]
    20 declare insert_code [code del]
    21 declare vimage_code [code del]
    22 
    23 subsection {* Set representation *}
    24 
    25 setup {*
    26   Code.add_type_cmd "set"
    27 *}
    28 
    29 definition Set :: "'a list \<Rightarrow> 'a set" where
    30   [simp]: "Set = set"
    31 
    32 definition Coset :: "'a list \<Rightarrow> 'a set" where
    33   [simp]: "Coset xs = - set xs"
    34 
    35 setup {*
    36   Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
    37   #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
    38   #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
    39   #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
    40 *}
    41 
    42 code_datatype Set Coset
    43 
    44 consts_code
    45   Coset ("\<module>Coset")
    46   Set ("\<module>Set")
    47 attach {*
    48   datatype 'a set = Set of 'a list | Coset of 'a list;
    49 *} -- {* This assumes that there won't be a @{text Coset} without a @{text Set} *}
    50 
    51 
    52 subsection {* Basic operations *}
    53 
    54 lemma [code]:
    55   "set xs = Set (remdups xs)"
    56   by simp
    57 
    58 lemma [code]:
    59   "x \<in> Set xs \<longleftrightarrow> List.member xs x"
    60   "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
    61   by (simp_all add: member_def)
    62 
    63 definition is_empty :: "'a set \<Rightarrow> bool" where
    64   [simp]: "is_empty A \<longleftrightarrow> A = {}"
    65 
    66 lemma [code_unfold]:
    67   "A = {} \<longleftrightarrow> is_empty A"
    68   by simp
    69 
    70 definition empty :: "'a set" where
    71   [simp]: "empty = {}"
    72 
    73 lemma [code_unfold]:
    74   "{} = empty"
    75   by simp
    76 
    77 lemma [code_unfold, code_inline del]:
    78   "empty = Set []"
    79   by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
    80 
    81 setup {*
    82   Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
    83   #> Code.add_signature_cmd ("empty", "'a set")
    84   #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
    85   #> Code.add_signature_cmd ("More_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
    86   #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
    87   #> Code.add_signature_cmd ("More_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
    88   #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
    89   #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
    90   #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
    91 *}
    92 
    93 lemma is_empty_Set [code]:
    94   "is_empty (Set xs) \<longleftrightarrow> List.null xs"
    95   by (simp add: null_def)
    96 
    97 lemma empty_Set [code]:
    98   "empty = Set []"
    99   by simp
   100 
   101 lemma insert_Set [code]:
   102   "insert x (Set xs) = Set (List.insert x xs)"
   103   "insert x (Coset xs) = Coset (removeAll x xs)"
   104   by (simp_all add: set_insert)
   105 
   106 lemma remove_Set [code]:
   107   "remove x (Set xs) = Set (removeAll x xs)"
   108   "remove x (Coset xs) = Coset (List.insert x xs)"
   109   by (auto simp add: set_insert remove_def)
   110 
   111 lemma image_Set [code]:
   112   "image f (Set xs) = Set (remdups (map f xs))"
   113   by simp
   114 
   115 lemma project_Set [code]:
   116   "project P (Set xs) = Set (filter P xs)"
   117   by (simp add: project_set)
   118 
   119 lemma Ball_Set [code]:
   120   "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
   121   by (simp add: list_all_iff)
   122 
   123 lemma Bex_Set [code]:
   124   "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
   125   by (simp add: list_ex_iff)
   126 
   127 lemma card_Set [code]:
   128   "card (Set xs) = length (remdups xs)"
   129 proof -
   130   have "card (set (remdups xs)) = length (remdups xs)"
   131     by (rule distinct_card) simp
   132   then show ?thesis by simp
   133 qed
   134 
   135 
   136 subsection {* Derived operations *}
   137 
   138 definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   139   [simp]: "set_eq = op ="
   140 
   141 lemma [code_unfold]:
   142   "op = = set_eq"
   143   by simp
   144 
   145 definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   146   [simp]: "subset_eq = op \<subseteq>"
   147 
   148 lemma [code_unfold]:
   149   "op \<subseteq> = subset_eq"
   150   by simp
   151 
   152 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   153   [simp]: "subset = op \<subset>"
   154 
   155 lemma [code_unfold]:
   156   "op \<subset> = subset"
   157   by simp
   158 
   159 setup {*
   160   Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   161   #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   162   #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   163 *}
   164 
   165 lemma set_eq_subset_eq [code]:
   166   "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
   167   by auto
   168 
   169 lemma subset_eq_forall [code]:
   170   "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   171   by (simp add: subset_eq)
   172 
   173 lemma subset_subset_eq [code]:
   174   "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
   175   by (simp add: subset)
   176 
   177 
   178 subsection {* Functorial operations *}
   179 
   180 definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   181   [simp]: "inter = op \<inter>"
   182 
   183 lemma [code_unfold]:
   184   "op \<inter> = inter"
   185   by simp
   186 
   187 definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   188   [simp]: "subtract A B = B - A"
   189 
   190 lemma [code_unfold]:
   191   "B - A = subtract A B"
   192   by simp
   193 
   194 definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   195   [simp]: "union = op \<union>"
   196 
   197 lemma [code_unfold]:
   198   "op \<union> = union"
   199   by simp
   200 
   201 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
   202   [simp]: "Inf = Complete_Lattice.Inf"
   203 
   204 lemma [code_unfold]:
   205   "Complete_Lattice.Inf = Inf"
   206   by simp
   207 
   208 definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
   209   [simp]: "Sup = Complete_Lattice.Sup"
   210 
   211 lemma [code_unfold]:
   212   "Complete_Lattice.Sup = Sup"
   213   by simp
   214 
   215 definition Inter :: "'a set set \<Rightarrow> 'a set" where
   216   [simp]: "Inter = Inf"
   217 
   218 lemma [code_unfold]:
   219   "Inf = Inter"
   220   by simp
   221 
   222 definition Union :: "'a set set \<Rightarrow> 'a set" where
   223   [simp]: "Union = Sup"
   224 
   225 lemma [code_unfold]:
   226   "Sup = Union"
   227   by simp
   228 
   229 setup {*
   230   Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   231   #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   232   #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   233   #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
   234   #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
   235   #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
   236   #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
   237 *}
   238 
   239 lemma inter_project [code]:
   240   "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
   241   "inter A (Coset xs) = foldr remove xs A"
   242   by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
   243 
   244 lemma subtract_remove [code]:
   245   "subtract (Set xs) A = foldr remove xs A"
   246   "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
   247   by (auto simp add: minus_set_foldr)
   248 
   249 lemma union_insert [code]:
   250   "union (Set xs) A = foldr insert xs A"
   251   "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
   252   by (auto simp add: union_set_foldr)
   253 
   254 lemma Inf_inf [code]:
   255   "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
   256   "Inf (Coset []) = (bot :: 'a::complete_lattice)"
   257   by (simp_all add: Inf_UNIV Inf_set_foldr)
   258 
   259 lemma Sup_sup [code]:
   260   "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
   261   "Sup (Coset []) = (top :: 'a::complete_lattice)"
   262   by (simp_all add: Sup_UNIV Sup_set_foldr)
   263 
   264 lemma Inter_inter [code]:
   265   "Inter (Set xs) = foldr inter xs (Coset [])"
   266   "Inter (Coset []) = empty"
   267   unfolding Inter_def Inf_inf by simp_all
   268 
   269 lemma Union_union [code]:
   270   "Union (Set xs) = foldr union xs empty"
   271   "Union (Coset []) = Coset []"
   272   unfolding Union_def Sup_sup by simp_all
   273 
   274 hide_const (open) is_empty empty remove
   275   set_eq subset_eq subset inter union subtract Inf Sup Inter Union
   276 
   277 
   278 subsection {* Operations on relations *}
   279 
   280 text {* Initially contributed by Tjark Weber. *}
   281 
   282 lemma bounded_Collect_code [code_unfold]:
   283   "{x\<in>S. P x} = project P S"
   284   by (auto simp add: project_def)
   285 
   286 lemma Id_on_code [code]:
   287   "Id_on (Set xs) = Set [(x,x). x \<leftarrow> xs]"
   288   by (auto simp add: Id_on_def)
   289 
   290 lemma Domain_fst [code]:
   291   "Domain r = fst ` r"
   292   by (auto simp add: image_def Bex_def)
   293 
   294 lemma Range_snd [code]:
   295   "Range r = snd ` r"
   296   by (auto simp add: image_def Bex_def)
   297 
   298 lemma irrefl_code [code]:
   299   "irrefl r \<longleftrightarrow> (\<forall>(x, y)\<in>r. x \<noteq> y)"
   300   by (auto simp add: irrefl_def)
   301 
   302 lemma trans_def [code]:
   303   "trans r \<longleftrightarrow> (\<forall>(x, y1)\<in>r. \<forall>(y2, z)\<in>r. y1 = y2 \<longrightarrow> (x, z)\<in>r)"
   304   by (auto simp add: trans_def)
   305 
   306 definition "exTimes A B = Sigma A (%_. B)"
   307 
   308 lemma [code_unfold]:
   309   "Sigma A (%_. B) = exTimes A B"
   310   by (simp add: exTimes_def)
   311 
   312 lemma exTimes_code [code]:
   313   "exTimes (Set xs) (Set ys) = Set [(x,y). x \<leftarrow> xs, y \<leftarrow> ys]"
   314   by (auto simp add: exTimes_def)
   315 
   316 lemma rel_comp_code [code]:
   317   "(Set xys) O (Set yzs) = Set (remdups [(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
   318  by (auto simp add: Bex_def)
   319 
   320 lemma acyclic_code [code]:
   321   "acyclic r = irrefl (r^+)"
   322   by (simp add: acyclic_def irrefl_def)
   323 
   324 lemma wf_code [code]:
   325   "wf (Set xs) = acyclic (Set xs)"
   326   by (simp add: wf_iff_acyclic_if_finite)
   327 
   328 end