# HG changeset patch
# User haftmann
# Date 1246179747 -7200
# Node ID 7de0e20ca24d2e6a7d1e132cc4dde920b67beccc
# Parent  89c37daebfdd6e3a95512442b93c94d9a5abf9b3
Executable_Set now based on Code_Set

diff -r 89c37daebfdd -r 7de0e20ca24d src/HOL/Library/Code_Set.thy
--- a/src/HOL/Library/Code_Set.thy	Sun Jun 28 10:33:36 2009 +0200
+++ b/src/HOL/Library/Code_Set.thy	Sun Jun 28 11:02:27 2009 +0200
@@ -72,11 +72,11 @@
   "map f (Set xs) = Set (remdups (List.map f xs))"
   by (simp add: Set_def)
 
-definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "project P A = Fset (List_Set.project P (member A))"
+definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
+  [simp]: "filter P A = Fset (List_Set.project P (member A))"
 
-lemma project_Set [code]:
-  "project P (Set xs) = Set (filter P xs)"
+lemma filter_Set [code]:
+  "filter P (Set xs) = Set (List.filter P xs)"
   by (simp add: Set_def project_set)
 
 definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
@@ -119,10 +119,10 @@
   by (cases A, cases B) (simp add: eq set_eq)
 
 definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
-  [simp]: "inter A B = Fset (List_Set.project (member A) (member B))"
+  [simp]: "inter A B = Fset (project (member A) (member B))"
 
 lemma inter_project [code]:
-  "inter A B = project (member A) B"
+  "inter A B = filter (member A) B"
   by (simp add: inter)
 
 
@@ -209,10 +209,10 @@
   by (simp add: List_Set.remove_def)
 declare remove_def [simp del]
 
-lemma project_simp [simp]:
-  "project P A = Fset {x \<in> member A. P x}"
+lemma filter_simp [simp]:
+  "filter P A = Fset {x \<in> member A. P x}"
   by (simp add: List_Set.project_def)
-declare project_def [simp del]
+declare filter_def [simp del]
 
 lemma inter_simp [simp]:
   "inter A B = Fset (member A \<inter> member B)"
diff -r 89c37daebfdd -r 7de0e20ca24d src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Sun Jun 28 10:33:36 2009 +0200
+++ b/src/HOL/Library/Executable_Set.thy	Sun Jun 28 11:02:27 2009 +0200
@@ -5,251 +5,47 @@
 header {* Implementation of finite sets by lists *}
 
 theory Executable_Set
-imports Main
+imports Main Code_Set
 begin
 
-subsection {* Definitional rewrites *}
+subsection {* Derived set operations *}
+
+declare member [code] 
 
 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "subset = op \<le>"
 
 declare subset_def [symmetric, code unfold]
 
-lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
-  unfolding subset_def subset_eq ..
-
-definition is_empty :: "'a set \<Rightarrow> bool" where
-  "is_empty A \<longleftrightarrow> A = {}"
+lemma [code]:
+  "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+  by (simp add: subset_def subset_eq)
 
 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   [code del]: "eq_set = op ="
 
-lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
-  unfolding eq_set_def by auto
-
 (* FIXME allow for Stefan's code generator:
 declare set_eq_subset[code unfold]
 *)
 
 lemma [code]:
-  "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
-  unfolding bex_triv_one_point1 ..
-
-definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
-  "filter_set P xs = {x\<in>xs. P x}"
-
-declare filter_set_def[symmetric, code unfold] 
-
-
-subsection {* Operations on lists *}
-
-subsubsection {* Basic definitions *}
-
-definition
-  flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
-  "flip f a b = f b a"
-
-definition
-  member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
-  "member xs x \<longleftrightarrow> x \<in> set xs"
-
-definition
-  insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "insertl x xs = (if member xs x then xs else x#xs)"
-
-lemma [code target: List]: "member [] y \<longleftrightarrow> False"
-  and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
-  unfolding member_def by (induct xs) simp_all
-
-fun
-  drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "drop_first f [] = []"
-| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
-declare drop_first.simps [code del]
-declare drop_first.simps [code target: List]
+  "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+  by (simp add: eq_set_def set_eq)
 
-declare remove1.simps [code del]
-lemma [code target: List]:
-  "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
-proof (cases "member xs x")
-  case False thus ?thesis unfolding member_def by (induct xs) auto
-next
-  case True
-  have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
-  with True show ?thesis by simp
-qed
-
-lemma member_nil [simp]:
-  "member [] = (\<lambda>x. False)"
-proof (rule ext)
-  fix x
-  show "member [] x = False" unfolding member_def by simp
-qed
+declare inter [code]
 
-lemma member_insertl [simp]:
-  "x \<in> set (insertl x xs)"
-  unfolding insertl_def member_def mem_iff by simp
-
-lemma insertl_member [simp]:
-  fixes xs x
-  assumes member: "member xs x"
-  shows "insertl x xs = xs"
-  using member unfolding insertl_def by simp
-
-lemma insertl_not_member [simp]:
-  fixes xs x
-  assumes member: "\<not> (member xs x)"
-  shows "insertl x xs = x # xs"
-  using member unfolding insertl_def by simp
-
-lemma foldr_remove1_empty [simp]:
-  "foldr remove1 xs [] = []"
-  by (induct xs) simp_all
+declare Inter_image_eq [symmetric, code]
+declare Union_image_eq [symmetric, code]
 
 
-subsubsection {* Derived definitions *}
-
-function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "unionl [] ys = ys"
-| "unionl xs ys = foldr insertl xs ys"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas unionl_eq = unionl.simps(2)
-
-function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "intersect [] ys = []"
-| "intersect xs [] = []"
-| "intersect xs ys = filter (member xs) ys"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas intersect_eq = intersect.simps(3)
-
-function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-where
-  "subtract [] ys = ys"
-| "subtract xs [] = []"
-| "subtract xs ys = foldr remove1 xs ys"
-by pat_completeness auto
-termination by lexicographic_order
+subsection {* Rewrites for primitive operations *}
 
-lemmas subtract_eq = subtract.simps(3)
-
-function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
-where
-  "map_distinct f [] = []"
-| "map_distinct f xs = foldr (insertl o f) xs []"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas map_distinct_eq = map_distinct.simps(2)
-
-function unions :: "'a list list \<Rightarrow> 'a list"
-where
-  "unions [] = []"
-| "unions xs = foldr unionl xs []"
-by pat_completeness auto
-termination by lexicographic_order
-
-lemmas unions_eq = unions.simps(2)
-
-consts intersects :: "'a list list \<Rightarrow> 'a list"
-primrec
-  "intersects (x#xs) = foldr intersect xs x"
-
-definition
-  map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
-  "map_union xs f = unions (map f xs)"
-
-definition
-  map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
-  "map_inter xs f = intersects (map f xs)"
+declare List_Set.project_def [symmetric, code unfold]
 
 
-subsection {* Isomorphism proofs *}
-
-lemma iso_member:
-  "member xs x \<longleftrightarrow> x \<in> set xs"
-  unfolding member_def mem_iff ..
-
-lemma iso_insert:
-  "set (insertl x xs) = insert x (set xs)"
-  unfolding insertl_def iso_member by (simp add: insert_absorb)
-
-lemma iso_remove1:
-  assumes distnct: "distinct xs"
-  shows "set (remove1 x xs) = set xs - {x}"
-  using distnct set_remove1_eq by auto
-
-lemma iso_union:
-  "set (unionl xs ys) = set xs \<union> set ys"
-  unfolding unionl_eq
-  by (induct xs arbitrary: ys) (simp_all add: iso_insert)
-
-lemma iso_intersect:
-  "set (intersect xs ys) = set xs \<inter> set ys"
-  unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
-
-definition
-  subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "subtract' = flip subtract"
-
-lemma iso_subtract:
-  fixes ys
-  assumes distnct: "distinct ys"
-  shows "set (subtract' ys xs) = set ys - set xs"
-    and "distinct (subtract' ys xs)"
-  unfolding subtract'_def flip_def subtract_eq
-  using distnct by (induct xs arbitrary: ys) auto
-
-lemma iso_map_distinct:
-  "set (map_distinct f xs) = image f (set xs)"
-  unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
+subsection {* code generator setup *}
 
-lemma iso_unions:
-  "set (unions xss) = \<Union> set (map set xss)"
-  unfolding unions_eq
-proof (induct xss)
-  case Nil show ?case by simp
-next
-  case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
-qed
-
-lemma iso_intersects:
-  "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
-  by (induct xss) (simp_all add: Int_def iso_member, auto)
-
-lemma iso_UNION:
-  "set (map_union xs f) = UNION (set xs) (set o f)"
-  unfolding map_union_def iso_unions by simp
-
-lemma iso_INTER:
-  "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
-  unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
-
-definition
-  Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "Blall = flip list_all"
-definition
-  Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
-  "Blex = flip list_ex"
-
-lemma iso_Ball:
-  "Blall xs f = Ball (set xs) f"
-  unfolding Blall_def flip_def by (induct xs) simp_all
-
-lemma iso_Bex:
-  "Blex xs f = Bex (set xs) f"
-  unfolding Blex_def flip_def by (induct xs) simp_all
-
-lemma iso_filter:
-  "set (filter P xs) = filter_set P (set xs)"
-  unfolding filter_set_def by (induct xs) auto
-
-subsection {* code generator setup *}
+text {* eliminate popular infixes *}
 
 ML {*
 nonfix inter;
@@ -257,23 +53,33 @@
 nonfix subset;
 *}
 
-subsubsection {* const serializations *}
+text {* type @{typ "'a fset"} *}
+
+types_code
+  fset ("(_/ list)")
+
+consts_code
+  Set ("_")
+
+text {* primitive operations *}
+
+definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
+  "flip f a b = f b a"
 
 consts_code
-  "Set.empty" ("{*[]*}")
-  insert ("{*insertl*}")
-  is_empty ("{*null*}")
-  "op \<union>" ("{*unionl*}")
-  "op \<inter>" ("{*intersect*}")
-  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
-  image ("{*map_distinct*}")
-  Union ("{*unions*}")
-  Inter ("{*intersects*}")
-  UNION ("{*map_union*}")
-  INTER ("{*map_inter*}")
-  Ball ("{*Blall*}")
-  Bex ("{*Blex*}")
-  filter_set ("{*filter*}")
-  fold ("{* foldl o flip *}")
+  "Set.empty"         ("{*Code_Set.empty*}")
+  "List_Set.is_empty" ("{*Code_Set.is_empty*}")
+  "Set.insert"        ("{*Code_Set.insert*}")
+  "List_Set.remove"   ("{*Code_Set.remove*}")
+  "Set.image"         ("{*Code_Set.map*}")
+  "List_Set.project"  ("{*Code_Set.filter*}")
+  "Ball"              ("{*flip Code_Set.forall*}")
+  "Bex"               ("{*flip Code_Set.exists*}")
+  "op \<union>"              ("{*Code_Set.union*}")
+  "op \<inter>"              ("{*Code_Set.inter*}")
+  "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip subtract*}")
+  "Set.Union"         ("{*Code_Set.union*}")
+  "Set.Inter"         ("{*Code_Set.inter*}")
+  fold                ("{*foldl o flip*}")
 
-end
+end
\ No newline at end of file