1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Crude_Executable_Set.thy	Fri Dec 04 11:03:54 2009 +0100
     1.3 @@ -0,0 +1,259 @@
     1.4 +(*  Title:      HOL/Library/Crude_Executable_Set.thy
     1.5 +    Author:     Florian Haftmann, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* A crude implementation of finite sets by lists -- avoid using this at any cost! *}
     1.9 +
    1.10 +theory Crude_Executable_Set
    1.11 +imports List_Set
    1.12 +begin
    1.13 +
    1.14 +declare mem_def [code del]
    1.15 +declare Collect_def [code del]
    1.16 +declare insert_code [code del]
    1.17 +declare vimage_code [code del]
    1.18 +
    1.19 +subsection {* Set representation *}
    1.20 +
    1.21 +setup {*
    1.22 +  Code.add_type_cmd "set"
    1.23 +*}
    1.24 +
    1.25 +definition Set :: "'a list \<Rightarrow> 'a set" where
    1.26 +  [simp]: "Set = set"
    1.27 +
    1.28 +definition Coset :: "'a list \<Rightarrow> 'a set" where
    1.29 +  [simp]: "Coset xs = - set xs"
    1.30 +
    1.31 +setup {*
    1.32 +  Code.add_signature_cmd ("Set", "'a list \<Rightarrow> 'a set")
    1.33 +  #> Code.add_signature_cmd ("Coset", "'a list \<Rightarrow> 'a set")
    1.34 +  #> Code.add_signature_cmd ("set", "'a list \<Rightarrow> 'a set")
    1.35 +  #> Code.add_signature_cmd ("op \<in>", "'a \<Rightarrow> 'a set \<Rightarrow> bool")
    1.36 +*}
    1.37 +
    1.38 +code_datatype Set Coset
    1.39 +
    1.40 +
    1.41 +subsection {* Basic operations *}
    1.42 +
    1.43 +lemma [code]:
    1.44 +  "set xs = Set (remdups xs)"
    1.45 +  by simp
    1.46 +
    1.47 +lemma [code]:
    1.48 +  "x \<in> Set xs \<longleftrightarrow> member x xs"
    1.49 +  "x \<in> Coset xs \<longleftrightarrow> \<not> member x xs"
    1.50 +  by (simp_all add: mem_iff)
    1.51 +
    1.52 +definition is_empty :: "'a set \<Rightarrow> bool" where
    1.53 +  [simp]: "is_empty A \<longleftrightarrow> A = {}"
    1.54 +
    1.55 +lemma [code_inline]:
    1.56 +  "A = {} \<longleftrightarrow> is_empty A"
    1.57 +  by simp
    1.58 +
    1.59 +definition empty :: "'a set" where
    1.60 +  [simp]: "empty = {}"
    1.61 +
    1.62 +lemma [code_inline]:
    1.63 +  "{} = empty"
    1.64 +  by simp
    1.65 +
    1.66 +setup {*
    1.67 +  Code.add_signature_cmd ("is_empty", "'a set \<Rightarrow> bool")
    1.68 +  #> Code.add_signature_cmd ("empty", "'a set")
    1.69 +  #> Code.add_signature_cmd ("insert", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
    1.70 +  #> Code.add_signature_cmd ("List_Set.remove", "'a \<Rightarrow> 'a set \<Rightarrow> 'a set")
    1.71 +  #> Code.add_signature_cmd ("image", "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b set")
    1.72 +  #> Code.add_signature_cmd ("List_Set.project", "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set")
    1.73 +  #> Code.add_signature_cmd ("Ball", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
    1.74 +  #> Code.add_signature_cmd ("Bex", "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool")
    1.75 +  #> Code.add_signature_cmd ("card", "'a set \<Rightarrow> nat")
    1.76 +*}
    1.77 +
    1.78 +lemma is_empty_Set [code]:
    1.79 +  "is_empty (Set xs) \<longleftrightarrow> null xs"
    1.80 +  by (simp add: empty_null)
    1.81 +
    1.82 +lemma empty_Set [code]:
    1.83 +  "empty = Set []"
    1.84 +  by simp
    1.85 +
    1.86 +lemma insert_Set [code]:
    1.87 +  "insert x (Set xs) = Set (List_Set.insert x xs)"
    1.88 +  "insert x (Coset xs) = Coset (remove_all x xs)"
    1.89 +  by (simp_all add: insert_set insert_set_compl)
    1.90 +
    1.91 +lemma remove_Set [code]:
    1.92 +  "remove x (Set xs) = Set (remove_all x xs)"
    1.93 +  "remove x (Coset xs) = Coset (List_Set.insert x xs)"
    1.94 +  by (simp_all add:remove_set remove_set_compl)
    1.95 +
    1.96 +lemma image_Set [code]:
    1.97 +  "image f (Set xs) = Set (remdups (map f xs))"
    1.98 +  by simp
    1.99 +
   1.100 +lemma project_Set [code]:
   1.101 +  "project P (Set xs) = Set (filter P xs)"
   1.102 +  by (simp add: project_set)
   1.103 +
   1.104 +lemma Ball_Set [code]:
   1.105 +  "Ball (Set xs) P \<longleftrightarrow> list_all P xs"
   1.106 +  by (simp add: ball_set)
   1.107 +
   1.108 +lemma Bex_Set [code]:
   1.109 +  "Bex (Set xs) P \<longleftrightarrow> list_ex P xs"
   1.110 +  by (simp add: bex_set)
   1.111 +
   1.112 +lemma card_Set [code]:
   1.113 +  "card (Set xs) = length (remdups xs)"
   1.114 +proof -
   1.115 +  have "card (set (remdups xs)) = length (remdups xs)"
   1.116 +    by (rule distinct_card) simp
   1.117 +  then show ?thesis by simp
   1.118 +qed
   1.119 +
   1.120 +
   1.121 +subsection {* Derived operations *}
   1.122 +
   1.123 +definition set_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.124 +  [simp]: "set_eq = op ="
   1.125 +
   1.126 +lemma [code_inline]:
   1.127 +  "op = = set_eq"
   1.128 +  by simp
   1.129 +
   1.130 +definition subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.131 +  [simp]: "subset_eq = op \<subseteq>"
   1.132 +
   1.133 +lemma [code_inline]:
   1.134 +  "op \<subseteq> = subset_eq"
   1.135 +  by simp
   1.136 +
   1.137 +definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   1.138 +  [simp]: "subset = op \<subset>"
   1.139 +
   1.140 +lemma [code_inline]:
   1.141 +  "op \<subset> = subset"
   1.142 +  by simp
   1.143 +
   1.144 +setup {*
   1.145 +  Code.add_signature_cmd ("set_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   1.146 +  #> Code.add_signature_cmd ("subset_eq", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   1.147 +  #> Code.add_signature_cmd ("subset", "'a set \<Rightarrow> 'a set \<Rightarrow> bool")
   1.148 +*}
   1.149 +
   1.150 +lemma set_eq_subset_eq [code]:
   1.151 +  "set_eq A B \<longleftrightarrow> subset_eq A B \<and> subset_eq B A"
   1.152 +  by auto
   1.153 +
   1.154 +lemma subset_eq_forall [code]:
   1.155 +  "subset_eq A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
   1.156 +  by (simp add: subset_eq)
   1.157 +
   1.158 +lemma subset_subset_eq [code]:
   1.159 +  "subset A B \<longleftrightarrow> subset_eq A B \<and> \<not> subset_eq B A"
   1.160 +  by (simp add: subset)
   1.161 +
   1.162 +
   1.163 +subsection {* Functorial operations *}
   1.164 +
   1.165 +definition inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   1.166 +  [simp]: "inter = op \<inter>"
   1.167 +
   1.168 +lemma [code_inline]:
   1.169 +  "op \<inter> = inter"
   1.170 +  by simp
   1.171 +
   1.172 +definition subtract :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   1.173 +  [simp]: "subtract A B = B - A"
   1.174 +
   1.175 +lemma [code_inline]:
   1.176 +  "B - A = subtract A B"
   1.177 +  by simp
   1.178 +
   1.179 +definition union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   1.180 +  [simp]: "union = op \<union>"
   1.181 +
   1.182 +lemma [code_inline]:
   1.183 +  "op \<union> = union"
   1.184 +  by simp
   1.185 +
   1.186 +definition Inf :: "'a::complete_lattice set \<Rightarrow> 'a" where
   1.187 +  [simp]: "Inf = Complete_Lattice.Inf"
   1.188 +
   1.189 +lemma [code_inline]:
   1.190 +  "Complete_Lattice.Inf = Inf"
   1.191 +  by simp
   1.192 +
   1.193 +definition Sup :: "'a::complete_lattice set \<Rightarrow> 'a" where
   1.194 +  [simp]: "Sup = Complete_Lattice.Sup"
   1.195 +
   1.196 +lemma [code_inline]:
   1.197 +  "Complete_Lattice.Sup = Sup"
   1.198 +  by simp
   1.199 +
   1.200 +definition Inter :: "'a set set \<Rightarrow> 'a set" where
   1.201 +  [simp]: "Inter = Inf"
   1.202 +
   1.203 +lemma [code_inline]:
   1.204 +  "Inf = Inter"
   1.205 +  by simp
   1.206 +
   1.207 +definition Union :: "'a set set \<Rightarrow> 'a set" where
   1.208 +  [simp]: "Union = Sup"
   1.209 +
   1.210 +lemma [code_inline]:
   1.211 +  "Sup = Union"
   1.212 +  by simp
   1.213 +
   1.214 +setup {*
   1.215 +  Code.add_signature_cmd ("inter", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   1.216 +  #> Code.add_signature_cmd ("subtract", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   1.217 +  #> Code.add_signature_cmd ("union", "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set")
   1.218 +  #> Code.add_signature_cmd ("Inf", "'a set \<Rightarrow> 'a")
   1.219 +  #> Code.add_signature_cmd ("Sup", "'a set \<Rightarrow> 'a")
   1.220 +  #> Code.add_signature_cmd ("Inter", "'a set set \<Rightarrow> 'a set")
   1.221 +  #> Code.add_signature_cmd ("Union", "'a set set \<Rightarrow> 'a set")
   1.222 +*}
   1.223 +
   1.224 +lemma inter_project [code]:
   1.225 +  "inter A (Set xs) = Set (List.filter (\<lambda>x. x \<in> A) xs)"
   1.226 +  "inter A (Coset xs) = foldl (\<lambda>A x. remove x A) A xs"
   1.227 +  by (simp add: inter project_def, simp add: Diff_eq [symmetric] minus_set)
   1.228 +
   1.229 +lemma subtract_remove [code]:
   1.230 +  "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
   1.231 +  "subtract (Coset xs) A = Set (List.filter (\<lambda>x. x \<in> A) xs)"
   1.232 +  by (auto simp add: minus_set)
   1.233 +
   1.234 +lemma union_insert [code]:
   1.235 +  "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
   1.236 +  "union (Coset xs) A = Coset (List.filter (\<lambda>x. x \<notin> A) xs)"
   1.237 +  by (auto simp add: union_set)
   1.238 +
   1.239 +lemma Inf_inf [code]:
   1.240 +  "Inf (Set xs) = foldl inf (top :: 'a::complete_lattice) xs"
   1.241 +  "Inf (Coset []) = (bot :: 'a::complete_lattice)"
   1.242 +  by (simp_all add: Inf_Univ bot_def [symmetric] Inf_set_fold)
   1.243 +
   1.244 +lemma Sup_sup [code]:
   1.245 +  "Sup (Set xs) = foldl sup (bot :: 'a::complete_lattice) xs"
   1.246 +  "Sup (Coset []) = (top :: 'a::complete_lattice)"
   1.247 +  by (simp_all add: Sup_Univ top_def [symmetric] Sup_set_fold)
   1.248 +
   1.249 +lemma Inter_inter [code]:
   1.250 +  "Inter (Set xs) = foldl inter (Coset []) xs"
   1.251 +  "Inter (Coset []) = empty"
   1.252 +  unfolding Inter_def Inf_inf by simp_all
   1.253 +
   1.254 +lemma Union_union [code]:
   1.255 +  "Union (Set xs) = foldl union empty xs"
   1.256 +  "Union (Coset []) = Coset []"
   1.257 +  unfolding Union_def Sup_sup by simp_all
   1.258 +
   1.259 +hide (open) const is_empty empty remove
   1.260 +  set_eq subset_eq subset inter union subtract Inf Sup Inter Union
   1.261 +
   1.262 +end