Executable_Set now based on Code_Set
authorhaftmann
Sun Jun 28 11:02:27 2009 +0200 (2009-06-28)
changeset 318477de0e20ca24d
parent 31846 89c37daebfdd
child 31848 e5ab21d14974
Executable_Set now based on Code_Set
src/HOL/Library/Code_Set.thy
src/HOL/Library/Executable_Set.thy
     1.1 --- a/src/HOL/Library/Code_Set.thy	Sun Jun 28 10:33:36 2009 +0200
     1.2 +++ b/src/HOL/Library/Code_Set.thy	Sun Jun 28 11:02:27 2009 +0200
     1.3 @@ -72,11 +72,11 @@
     1.4    "map f (Set xs) = Set (remdups (List.map f xs))"
     1.5    by (simp add: Set_def)
     1.6  
     1.7 -definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
     1.8 -  [simp]: "project P A = Fset (List_Set.project P (member A))"
     1.9 +definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.10 +  [simp]: "filter P A = Fset (List_Set.project P (member A))"
    1.11  
    1.12 -lemma project_Set [code]:
    1.13 -  "project P (Set xs) = Set (filter P xs)"
    1.14 +lemma filter_Set [code]:
    1.15 +  "filter P (Set xs) = Set (List.filter P xs)"
    1.16    by (simp add: Set_def project_set)
    1.17  
    1.18  definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
    1.19 @@ -119,10 +119,10 @@
    1.20    by (cases A, cases B) (simp add: eq set_eq)
    1.21  
    1.22  definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
    1.23 -  [simp]: "inter A B = Fset (List_Set.project (member A) (member B))"
    1.24 +  [simp]: "inter A B = Fset (project (member A) (member B))"
    1.25  
    1.26  lemma inter_project [code]:
    1.27 -  "inter A B = project (member A) B"
    1.28 +  "inter A B = filter (member A) B"
    1.29    by (simp add: inter)
    1.30  
    1.31  
    1.32 @@ -209,10 +209,10 @@
    1.33    by (simp add: List_Set.remove_def)
    1.34  declare remove_def [simp del]
    1.35  
    1.36 -lemma project_simp [simp]:
    1.37 -  "project P A = Fset {x \<in> member A. P x}"
    1.38 +lemma filter_simp [simp]:
    1.39 +  "filter P A = Fset {x \<in> member A. P x}"
    1.40    by (simp add: List_Set.project_def)
    1.41 -declare project_def [simp del]
    1.42 +declare filter_def [simp del]
    1.43  
    1.44  lemma inter_simp [simp]:
    1.45    "inter A B = Fset (member A \<inter> member B)"
     2.1 --- a/src/HOL/Library/Executable_Set.thy	Sun Jun 28 10:33:36 2009 +0200
     2.2 +++ b/src/HOL/Library/Executable_Set.thy	Sun Jun 28 11:02:27 2009 +0200
     2.3 @@ -5,251 +5,47 @@
     2.4  header {* Implementation of finite sets by lists *}
     2.5  
     2.6  theory Executable_Set
     2.7 -imports Main
     2.8 +imports Main Code_Set
     2.9  begin
    2.10  
    2.11 -subsection {* Definitional rewrites *}
    2.12 +subsection {* Derived set operations *}
    2.13 +
    2.14 +declare member [code] 
    2.15  
    2.16  definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    2.17    "subset = op \<le>"
    2.18  
    2.19  declare subset_def [symmetric, code unfold]
    2.20  
    2.21 -lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    2.22 -  unfolding subset_def subset_eq ..
    2.23 -
    2.24 -definition is_empty :: "'a set \<Rightarrow> bool" where
    2.25 -  "is_empty A \<longleftrightarrow> A = {}"
    2.26 +lemma [code]:
    2.27 +  "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    2.28 +  by (simp add: subset_def subset_eq)
    2.29  
    2.30  definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    2.31    [code del]: "eq_set = op ="
    2.32  
    2.33 -lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    2.34 -  unfolding eq_set_def by auto
    2.35 -
    2.36  (* FIXME allow for Stefan's code generator:
    2.37  declare set_eq_subset[code unfold]
    2.38  *)
    2.39  
    2.40  lemma [code]:
    2.41 -  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    2.42 -  unfolding bex_triv_one_point1 ..
    2.43 -
    2.44 -definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    2.45 -  "filter_set P xs = {x\<in>xs. P x}"
    2.46 -
    2.47 -declare filter_set_def[symmetric, code unfold] 
    2.48 -
    2.49 -
    2.50 -subsection {* Operations on lists *}
    2.51 -
    2.52 -subsubsection {* Basic definitions *}
    2.53 -
    2.54 -definition
    2.55 -  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    2.56 -  "flip f a b = f b a"
    2.57 -
    2.58 -definition
    2.59 -  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
    2.60 -  "member xs x \<longleftrightarrow> x \<in> set xs"
    2.61 -
    2.62 -definition
    2.63 -  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.64 -  "insertl x xs = (if member xs x then xs else x#xs)"
    2.65 -
    2.66 -lemma [code target: List]: "member [] y \<longleftrightarrow> False"
    2.67 -  and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
    2.68 -  unfolding member_def by (induct xs) simp_all
    2.69 -
    2.70 -fun
    2.71 -  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.72 -  "drop_first f [] = []"
    2.73 -| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
    2.74 -declare drop_first.simps [code del]
    2.75 -declare drop_first.simps [code target: List]
    2.76 +  "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    2.77 +  by (simp add: eq_set_def set_eq)
    2.78  
    2.79 -declare remove1.simps [code del]
    2.80 -lemma [code target: List]:
    2.81 -  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
    2.82 -proof (cases "member xs x")
    2.83 -  case False thus ?thesis unfolding member_def by (induct xs) auto
    2.84 -next
    2.85 -  case True
    2.86 -  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
    2.87 -  with True show ?thesis by simp
    2.88 -qed
    2.89 -
    2.90 -lemma member_nil [simp]:
    2.91 -  "member [] = (\<lambda>x. False)"
    2.92 -proof (rule ext)
    2.93 -  fix x
    2.94 -  show "member [] x = False" unfolding member_def by simp
    2.95 -qed
    2.96 +declare inter [code]
    2.97  
    2.98 -lemma member_insertl [simp]:
    2.99 -  "x \<in> set (insertl x xs)"
   2.100 -  unfolding insertl_def member_def mem_iff by simp
   2.101 -
   2.102 -lemma insertl_member [simp]:
   2.103 -  fixes xs x
   2.104 -  assumes member: "member xs x"
   2.105 -  shows "insertl x xs = xs"
   2.106 -  using member unfolding insertl_def by simp
   2.107 -
   2.108 -lemma insertl_not_member [simp]:
   2.109 -  fixes xs x
   2.110 -  assumes member: "\<not> (member xs x)"
   2.111 -  shows "insertl x xs = x # xs"
   2.112 -  using member unfolding insertl_def by simp
   2.113 -
   2.114 -lemma foldr_remove1_empty [simp]:
   2.115 -  "foldr remove1 xs [] = []"
   2.116 -  by (induct xs) simp_all
   2.117 +declare Inter_image_eq [symmetric, code]
   2.118 +declare Union_image_eq [symmetric, code]
   2.119  
   2.120  
   2.121 -subsubsection {* Derived definitions *}
   2.122 -
   2.123 -function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   2.124 -where
   2.125 -  "unionl [] ys = ys"
   2.126 -| "unionl xs ys = foldr insertl xs ys"
   2.127 -by pat_completeness auto
   2.128 -termination by lexicographic_order
   2.129 -
   2.130 -lemmas unionl_eq = unionl.simps(2)
   2.131 -
   2.132 -function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   2.133 -where
   2.134 -  "intersect [] ys = []"
   2.135 -| "intersect xs [] = []"
   2.136 -| "intersect xs ys = filter (member xs) ys"
   2.137 -by pat_completeness auto
   2.138 -termination by lexicographic_order
   2.139 -
   2.140 -lemmas intersect_eq = intersect.simps(3)
   2.141 -
   2.142 -function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   2.143 -where
   2.144 -  "subtract [] ys = ys"
   2.145 -| "subtract xs [] = []"
   2.146 -| "subtract xs ys = foldr remove1 xs ys"
   2.147 -by pat_completeness auto
   2.148 -termination by lexicographic_order
   2.149 +subsection {* Rewrites for primitive operations *}
   2.150  
   2.151 -lemmas subtract_eq = subtract.simps(3)
   2.152 -
   2.153 -function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   2.154 -where
   2.155 -  "map_distinct f [] = []"
   2.156 -| "map_distinct f xs = foldr (insertl o f) xs []"
   2.157 -by pat_completeness auto
   2.158 -termination by lexicographic_order
   2.159 -
   2.160 -lemmas map_distinct_eq = map_distinct.simps(2)
   2.161 -
   2.162 -function unions :: "'a list list \<Rightarrow> 'a list"
   2.163 -where
   2.164 -  "unions [] = []"
   2.165 -| "unions xs = foldr unionl xs []"
   2.166 -by pat_completeness auto
   2.167 -termination by lexicographic_order
   2.168 -
   2.169 -lemmas unions_eq = unions.simps(2)
   2.170 -
   2.171 -consts intersects :: "'a list list \<Rightarrow> 'a list"
   2.172 -primrec
   2.173 -  "intersects (x#xs) = foldr intersect xs x"
   2.174 -
   2.175 -definition
   2.176 -  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   2.177 -  "map_union xs f = unions (map f xs)"
   2.178 -
   2.179 -definition
   2.180 -  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   2.181 -  "map_inter xs f = intersects (map f xs)"
   2.182 +declare List_Set.project_def [symmetric, code unfold]
   2.183  
   2.184  
   2.185 -subsection {* Isomorphism proofs *}
   2.186 -
   2.187 -lemma iso_member:
   2.188 -  "member xs x \<longleftrightarrow> x \<in> set xs"
   2.189 -  unfolding member_def mem_iff ..
   2.190 -
   2.191 -lemma iso_insert:
   2.192 -  "set (insertl x xs) = insert x (set xs)"
   2.193 -  unfolding insertl_def iso_member by (simp add: insert_absorb)
   2.194 -
   2.195 -lemma iso_remove1:
   2.196 -  assumes distnct: "distinct xs"
   2.197 -  shows "set (remove1 x xs) = set xs - {x}"
   2.198 -  using distnct set_remove1_eq by auto
   2.199 -
   2.200 -lemma iso_union:
   2.201 -  "set (unionl xs ys) = set xs \<union> set ys"
   2.202 -  unfolding unionl_eq
   2.203 -  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
   2.204 -
   2.205 -lemma iso_intersect:
   2.206 -  "set (intersect xs ys) = set xs \<inter> set ys"
   2.207 -  unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
   2.208 -
   2.209 -definition
   2.210 -  subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   2.211 -  "subtract' = flip subtract"
   2.212 -
   2.213 -lemma iso_subtract:
   2.214 -  fixes ys
   2.215 -  assumes distnct: "distinct ys"
   2.216 -  shows "set (subtract' ys xs) = set ys - set xs"
   2.217 -    and "distinct (subtract' ys xs)"
   2.218 -  unfolding subtract'_def flip_def subtract_eq
   2.219 -  using distnct by (induct xs arbitrary: ys) auto
   2.220 -
   2.221 -lemma iso_map_distinct:
   2.222 -  "set (map_distinct f xs) = image f (set xs)"
   2.223 -  unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
   2.224 +subsection {* code generator setup *}
   2.225  
   2.226 -lemma iso_unions:
   2.227 -  "set (unions xss) = \<Union> set (map set xss)"
   2.228 -  unfolding unions_eq
   2.229 -proof (induct xss)
   2.230 -  case Nil show ?case by simp
   2.231 -next
   2.232 -  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
   2.233 -qed
   2.234 -
   2.235 -lemma iso_intersects:
   2.236 -  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
   2.237 -  by (induct xss) (simp_all add: Int_def iso_member, auto)
   2.238 -
   2.239 -lemma iso_UNION:
   2.240 -  "set (map_union xs f) = UNION (set xs) (set o f)"
   2.241 -  unfolding map_union_def iso_unions by simp
   2.242 -
   2.243 -lemma iso_INTER:
   2.244 -  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
   2.245 -  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
   2.246 -
   2.247 -definition
   2.248 -  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   2.249 -  "Blall = flip list_all"
   2.250 -definition
   2.251 -  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   2.252 -  "Blex = flip list_ex"
   2.253 -
   2.254 -lemma iso_Ball:
   2.255 -  "Blall xs f = Ball (set xs) f"
   2.256 -  unfolding Blall_def flip_def by (induct xs) simp_all
   2.257 -
   2.258 -lemma iso_Bex:
   2.259 -  "Blex xs f = Bex (set xs) f"
   2.260 -  unfolding Blex_def flip_def by (induct xs) simp_all
   2.261 -
   2.262 -lemma iso_filter:
   2.263 -  "set (filter P xs) = filter_set P (set xs)"
   2.264 -  unfolding filter_set_def by (induct xs) auto
   2.265 -
   2.266 -subsection {* code generator setup *}
   2.267 +text {* eliminate popular infixes *}
   2.268  
   2.269  ML {*
   2.270  nonfix inter;
   2.271 @@ -257,23 +53,33 @@
   2.272  nonfix subset;
   2.273  *}
   2.274  
   2.275 -subsubsection {* const serializations *}
   2.276 +text {* type @{typ "'a fset"} *}
   2.277 +
   2.278 +types_code
   2.279 +  fset ("(_/ list)")
   2.280 +
   2.281 +consts_code
   2.282 +  Set ("_")
   2.283 +
   2.284 +text {* primitive operations *}
   2.285 +
   2.286 +definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
   2.287 +  "flip f a b = f b a"
   2.288  
   2.289  consts_code
   2.290 -  "Set.empty" ("{*[]*}")
   2.291 -  insert ("{*insertl*}")
   2.292 -  is_empty ("{*null*}")
   2.293 -  "op \<union>" ("{*unionl*}")
   2.294 -  "op \<inter>" ("{*intersect*}")
   2.295 -  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
   2.296 -  image ("{*map_distinct*}")
   2.297 -  Union ("{*unions*}")
   2.298 -  Inter ("{*intersects*}")
   2.299 -  UNION ("{*map_union*}")
   2.300 -  INTER ("{*map_inter*}")
   2.301 -  Ball ("{*Blall*}")
   2.302 -  Bex ("{*Blex*}")
   2.303 -  filter_set ("{*filter*}")
   2.304 -  fold ("{* foldl o flip *}")
   2.305 +  "Set.empty"         ("{*Code_Set.empty*}")
   2.306 +  "List_Set.is_empty" ("{*Code_Set.is_empty*}")
   2.307 +  "Set.insert"        ("{*Code_Set.insert*}")
   2.308 +  "List_Set.remove"   ("{*Code_Set.remove*}")
   2.309 +  "Set.image"         ("{*Code_Set.map*}")
   2.310 +  "List_Set.project"  ("{*Code_Set.filter*}")
   2.311 +  "Ball"              ("{*flip Code_Set.forall*}")
   2.312 +  "Bex"               ("{*flip Code_Set.exists*}")
   2.313 +  "op \<union>"              ("{*Code_Set.union*}")
   2.314 +  "op \<inter>"              ("{*Code_Set.inter*}")
   2.315 +  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip subtract*}")
   2.316 +  "Set.Union"         ("{*Code_Set.union*}")
   2.317 +  "Set.Inter"         ("{*Code_Set.inter*}")
   2.318 +  fold                ("{*foldl o flip*}")
   2.319  
   2.320 -end
   2.321 +end
   2.322 \ No newline at end of file