src/HOL/Library/Executable_Set.thy
author bulwahn
Wed Oct 19 09:11:16 2011 +0200 (2011-10-19)
changeset 45186 645c6cac779e
parent 45120 717bc892e4d7
child 45231 d85a2fdc586c
permissions -rw-r--r--
removing old code generator setup for executable sets
     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 Cset.set} 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 
    45 subsection {* Basic operations *}
    46 
    47 lemma [code]:
    48   "set xs = Set (remdups xs)"
    49   by simp
    50 
    51 lemma [code]:
    52   "x \<in> Set xs \<longleftrightarrow> List.member xs x"
    53   "x \<in> Coset xs \<longleftrightarrow> \<not> List.member xs x"
    54   by (simp_all add: member_def)
    55 
    56 definition is_empty :: "'a set \<Rightarrow> bool" where
    57   [simp]: "is_empty A \<longleftrightarrow> A = {}"
    58 
    59 lemma [code_unfold]:
    60   "A = {} \<longleftrightarrow> is_empty A"
    61   by simp
    62 
    63 definition empty :: "'a set" where
    64   [simp]: "empty = {}"
    65 
    66 lemma [code_unfold]:
    67   "{} = empty"
    68   by simp
    69 
    70 lemma [code_unfold, code_inline del]:
    71   "empty = Set []"
    72   by simp -- {* Otherwise @{text \<eta>}-expansion produces funny things. *}
    73 
    74 setup {*
    75   Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
    76   #> Code.add_signature_cmd ("empty", "'a set")
    77   #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
    78   #> Code.add_signature_cmd ("More_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
    79   #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
    80   #> Code.add_signature_cmd ("More_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
    81   #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
    82   #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
    83   #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
    84 *}
    85 
    86 lemma is_empty_Set [code]:
    87   "is_empty (Set xs) \<longleftrightarrow> List.null xs"
    88   by (simp add: null_def)
    89 
    90 lemma empty_Set [code]:
    91   "empty = Set []"
    92   by simp
    93 
    94 lemma insert_Set [code]:
    95   "insert x (Set xs) = Set (List.insert x xs)"
    96   "insert x (Coset xs) = Coset (removeAll x xs)"
    97   by simp_all
    98 
    99 lemma remove_Set [code]:
   100   "remove x (Set xs) = Set (removeAll x xs)"
   101   "remove x (Coset xs) = Coset (List.insert x xs)"
   102   by (auto simp add: remove_def)
   103 
   104 lemma image_Set [code]:
   105   "image f (Set xs) = Set (remdups (map f xs))"
   106   by simp
   107 
   108 lemma project_Set [code]:
   109   "project P (Set xs) = Set (filter P xs)"
   110   by (simp add: project_set)
   111 
   112 lemma Ball_Set [code]:
   113   "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
   114   by (simp add: list_all_iff)
   115 
   116 lemma Bex_Set [code]:
   117   "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
   118   by (simp add: list_ex_iff)
   119 
   120 lemma
   121   [code, code del]: "card S = card S" ..
   122 
   123 lemma card_Set [code]:
   124   "card (Set xs) = length (remdups xs)"
   125 proof -
   126   have "card (set (remdups xs)) = length (remdups xs)"
   127     by (rule distinct_card) simp
   128   then show ?thesis by simp
   129 qed
   130 
   131 
   132 subsection {* Derived operations *}
   133 
   134 definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   135   [simp]: "set_eq = op ="
   136 
   137 lemma [code_unfold]:
   138   "op = = set_eq"
   139   by simp
   140 
   141 definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   142   [simp]: "subset_eq = op \<subseteq>"
   143 
   144 lemma [code_unfold]:
   145   "op \<subseteq> = subset_eq"
   146   by simp
   147 
   148 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   149   [simp]: "subset = op \<subset>"
   150 
   151 lemma [code_unfold]:
   152   "op \<subset> = subset"
   153   by simp
   154 
   155 setup {*
   156   Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   157   #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   158   #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   159 *}
   160 
   161 lemma set_eq_subset_eq [code]:
   162   "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
   163   by auto
   164 
   165 lemma subset_eq_forall [code]:
   166   "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   167   by (simp add: subset_eq)
   168 
   169 lemma subset_subset_eq [code]:
   170   "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
   171   by (simp add: subset)
   172 
   173 
   174 subsection {* Functorial operations *}
   175 
   176 definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   177   [simp]: "inter = op \<inter>"
   178 
   179 lemma [code_unfold]:
   180   "op \<inter> = inter"
   181   by simp
   182 
   183 definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   184   [simp]: "subtract A B = B - A"
   185 
   186 lemma [code_unfold]:
   187   "B - A = subtract A B"
   188   by simp
   189 
   190 definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   191   [simp]: "union = op \<union>"
   192 
   193 lemma [code_unfold]:
   194   "op \<union> = union"
   195   by simp
   196 
   197 definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
   198   [simp]: "Inf = Complete_Lattices.Inf"
   199 
   200 lemma [code_unfold]:
   201   "Complete_Lattices.Inf = Inf"
   202   by simp
   203 
   204 definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
   205   [simp]: "Sup = Complete_Lattices.Sup"
   206 
   207 lemma [code_unfold]:
   208   "Complete_Lattices.Sup = Sup"
   209   by simp
   210 
   211 definition Inter :: "'a set set \<Rightarrow> 'a set" where
   212   [simp]: "Inter = Inf"
   213 
   214 lemma [code_unfold]:
   215   "Inf = Inter"
   216   by simp
   217 
   218 definition Union :: "'a set set \<Rightarrow> 'a set" where
   219   [simp]: "Union = Sup"
   220 
   221 lemma [code_unfold]:
   222   "Sup = Union"
   223   by simp
   224 
   225 setup {*
   226   Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   227   #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   228   #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   229   #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
   230   #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
   231   #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
   232   #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
   233 *}
   234 
   235 lemma inter_project [code]:
   236   "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
   237   "inter A (Coset xs) = foldr remove xs A"
   238   by (simp add: inter project_def) (simp add: Diff_eq [symmetric] minus_set_foldr)
   239 
   240 lemma subtract_remove [code]:
   241   "subtract (Set xs) A = foldr remove xs A"
   242   "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
   243   by (auto simp add: minus_set_foldr)
   244 
   245 lemma union_insert [code]:
   246   "union (Set xs) A = foldr insert xs A"
   247   "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
   248   by (auto simp add: union_set_foldr)
   249 
   250 lemma Inf_inf [code]:
   251   "Inf (Set xs) = foldr inf xs (top :: 'a::complete_lattice)"
   252   "Inf (Coset []) = (bot :: 'a::complete_lattice)"
   253   by (simp_all add: Inf_set_foldr)
   254 
   255 lemma Sup_sup [code]:
   256   "Sup (Set xs) = foldr sup xs (bot :: 'a::complete_lattice)"
   257   "Sup (Coset []) = (top :: 'a::complete_lattice)"
   258   by (simp_all add: Sup_set_foldr)
   259 
   260 lemma Inter_inter [code]:
   261   "Inter (Set xs) = foldr inter xs (Coset [])"
   262   "Inter (Coset []) = empty"
   263   unfolding Inter_def Inf_inf by simp_all
   264 
   265 lemma Union_union [code]:
   266   "Union (Set xs) = foldr union xs empty"
   267   "Union (Coset []) = Coset []"
   268   unfolding Union_def Sup_sup by simp_all
   269 
   270 hide_const (open) is_empty empty remove
   271   set_eq subset_eq subset inter union subtract Inf Sup Inter Union
   272 
   273 
   274 subsection {* Operations on relations *}
   275 
   276 text {* Initially contributed by Tjark Weber. *}
   277 
   278 lemma [code]:
   279   "Domain r = fst ` r"
   280   by (fact Domain_fst)
   281 
   282 lemma [code]:
   283   "Range r = snd ` r"
   284   by (fact Range_snd)
   285 
   286 lemma [code]:
   287   "trans r \<longleftrightarrow> (\<forall>(x, y1) \<in> r. \<forall>(y2, z) \<in> r. y1 = y2 \<longrightarrow> (x, z) \<in> r)"
   288   by (fact trans_join)
   289 
   290 lemma [code]:
   291   "irrefl r \<longleftrightarrow> (\<forall>(x, y) \<in> r. x \<noteq> y)"
   292   by (fact irrefl_distinct)
   293 
   294 lemma [code]:
   295   "acyclic r \<longleftrightarrow> irrefl (r^+)"
   296   by (fact acyclic_irrefl)
   297 
   298 lemma [code]:
   299   "More_Set.product (Set xs) (Set ys) = Set [(x, y). x \<leftarrow> xs, y \<leftarrow> ys]"
   300   by (unfold Set_def) (fact product_code)
   301 
   302 lemma [code]:
   303   "Id_on (Set xs) = Set [(x, x). x \<leftarrow> xs]"
   304   by (unfold Set_def) (fact Id_on_set)
   305 
   306 lemma [code]:
   307   "Set xys O Set yzs = Set ([(fst xy, snd yz). xy \<leftarrow> xys, yz \<leftarrow> yzs, snd xy = fst yz])"
   308   by (unfold Set_def) (fact set_rel_comp)
   309 
   310 lemma [code]:
   311   "wf (Set xs) = acyclic (Set xs)"
   312   by (unfold Set_def) (fact wf_set)
   313 
   314 end