# HG changeset patch # User haftmann # Date 1246280108 -7200 # Node ID 50b307148dab4a33d33fd73624842eb39854b9e8 # Parent cc7ddda02436d5126d5df69830aa4efb55c497cc# Parent f079b174e56a0d8b537510cbd1745c57759adb64 merged diff -r cc7ddda02436 -r 50b307148dab doc-src/Codegen/Thy/document/Introduction.tex --- a/doc-src/Codegen/Thy/document/Introduction.tex Sun Jun 28 22:51:29 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Mon Jun 29 14:55:08 2009 +0200 @@ -249,9 +249,9 @@ \hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\ \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\ \hspace*{0pt}dequeue (AQueue (v :~va) []) =\\ -\hspace*{0pt} ~(let {\char123}\\ +\hspace*{0pt} ~let {\char123}\\ \hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\ -\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys) );\\ +\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\ \hspace*{0pt}\\ \hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\ \hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\ diff -r cc7ddda02436 -r 50b307148dab doc-src/Codegen/Thy/document/Program.tex --- a/doc-src/Codegen/Thy/document/Program.tex Sun Jun 28 22:51:29 2009 +0200 +++ b/doc-src/Codegen/Thy/document/Program.tex Mon Jun 29 14:55:08 2009 +0200 @@ -966,9 +966,9 @@ \noindent% \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\ -\hspace*{0pt} ~(let {\char123}\\ +\hspace*{0pt} ~let {\char123}\\ \hspace*{0pt} ~~~(y :~ys) = rev xs;\\ -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys) );\\ +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\ \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);% \end{isamarkuptext}% \isamarkuptrue% diff -r cc7ddda02436 -r 50b307148dab doc-src/Codegen/Thy/examples/Example.hs --- a/doc-src/Codegen/Thy/examples/Example.hs Sun Jun 28 22:51:29 2009 +0200 +++ b/doc-src/Codegen/Thy/examples/Example.hs Mon Jun 29 14:55:08 2009 +0200 @@ -23,9 +23,9 @@ dequeue (AQueue [] []) = (Nothing, AQueue [] []); dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys); dequeue (AQueue (v : va) []) = - (let { + let { (y : ys) = rev (v : va); - } in (Just y, AQueue [] ys) ); + } in (Just y, AQueue [] ys); enqueue :: forall a. a -> Queue a -> Queue a; enqueue x (AQueue xs ys) = AQueue (x : xs) ys; diff -r cc7ddda02436 -r 50b307148dab src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Jun 28 22:51:29 2009 +0200 +++ b/src/HOL/IsaMakefile Mon Jun 29 14:55:08 2009 +0200 @@ -319,7 +319,7 @@ Library/Abstract_Rat.thy \ Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \ Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML \ - Library/Code_Set.thy Library/Convex_Euclidean_Space.thy \ + Library/Fset.thy Library/Convex_Euclidean_Space.thy \ Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \ Library/Executable_Set.thy Library/Infinite_Set.thy \ Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\ diff -r cc7ddda02436 -r 50b307148dab src/HOL/Library/Code_Set.thy --- a/src/HOL/Library/Code_Set.thy Sun Jun 28 22:51:29 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,169 +0,0 @@ - -(* Author: Florian Haftmann, TU Muenchen *) - -header {* Executable finite sets *} - -theory Code_Set -imports List_Set -begin - -lemma foldl_apply_inv: - assumes "\x. g (h x) = x" - shows "foldl f (g s) xs = g (foldl (\s x. h (f (g s) x)) s xs)" - by (rule sym, induct xs arbitrary: s) (simp_all add: assms) - -subsection {* Lifting *} - -datatype 'a fset = Fset "'a set" - -primrec member :: "'a fset \ 'a set" where - "member (Fset A) = A" - -lemma Fset_member [simp]: - "Fset (member A) = A" - by (cases A) simp - -definition Set :: "'a list \ 'a fset" where - "Set xs = Fset (set xs)" - -lemma member_Set [simp]: - "member (Set xs) = set xs" - by (simp add: Set_def) - -code_datatype Set - - -subsection {* Basic operations *} - -definition is_empty :: "'a fset \ bool" where - "is_empty A \ List_Set.is_empty (member A)" - -lemma is_empty_Set [code]: - "is_empty (Set xs) \ null xs" - by (simp add: is_empty_def is_empty_set) - -definition empty :: "'a fset" where - "empty = Fset {}" - -lemma empty_Set [code]: - "empty = Set []" - by (simp add: empty_def Set_def) - -definition insert :: "'a \ 'a fset \ 'a fset" where - "insert x A = Fset (Set.insert x (member A))" - -lemma insert_Set [code]: - "insert x (Set xs) = Set (List_Set.insert x xs)" - by (simp add: insert_def Set_def insert_set) - -definition remove :: "'a \ 'a fset \ 'a fset" where - "remove x A = Fset (List_Set.remove x (member A))" - -lemma remove_Set [code]: - "remove x (Set xs) = Set (remove_all x xs)" - by (simp add: remove_def Set_def remove_set) - -definition map :: "('a \ 'b) \ 'a fset \ 'b fset" where - "map f A = Fset (image f (member A))" - -lemma map_Set [code]: - "map f (Set xs) = Set (remdups (List.map f xs))" - by (simp add: map_def Set_def) - -definition project :: "('a \ bool) \ 'a fset \ 'a fset" where - "project P A = Fset (List_Set.project P (member A))" - -lemma project_Set [code]: - "project P (Set xs) = Set (filter P xs)" - by (simp add: project_def Set_def project_set) - -definition forall :: "('a \ bool) \ 'a fset \ bool" where - "forall P A \ Ball (member A) P" - -lemma forall_Set [code]: - "forall P (Set xs) \ list_all P xs" - by (simp add: forall_def Set_def ball_set) - -definition exists :: "('a \ bool) \ 'a fset \ bool" where - "exists P A \ Bex (member A) P" - -lemma exists_Set [code]: - "exists P (Set xs) \ list_ex P xs" - by (simp add: exists_def Set_def bex_set) - - -subsection {* Functorial operations *} - -definition union :: "'a fset \ 'a fset \ 'a fset" where - "union A B = Fset (member A \ member B)" - -lemma union_insert [code]: - "union (Set xs) A = foldl (\A x. insert x A) A xs" -proof - - have "foldl (\A x. Set.insert x A) (member A) xs = - member (foldl (\A x. Fset (Set.insert x (member A))) A xs)" - by (rule foldl_apply_inv) simp - then show ?thesis by (simp add: union_def union_set insert_def) -qed - -definition subtract :: "'a fset \ 'a fset \ 'a fset" where - "subtract A B = Fset (member B - member A)" - -lemma subtract_remove [code]: - "subtract (Set xs) A = foldl (\A x. remove x A) A xs" -proof - - have "foldl (\A x. List_Set.remove x A) (member A) xs = - member (foldl (\A x. Fset (List_Set.remove x (member A))) A xs)" - by (rule foldl_apply_inv) simp - then show ?thesis by (simp add: subtract_def minus_set remove_def) -qed - - -subsection {* Derived operations *} - -lemma member_exists [code]: - "member A y \ exists (\x. y = x) A" - by (simp add: exists_def mem_def) - -definition subfset_eq :: "'a fset \ 'a fset \ bool" where - "subfset_eq A B \ member A \ member B" - -lemma subfset_eq_forall [code]: - "subfset_eq A B \ forall (\x. member B x) A" - by (simp add: subfset_eq_def subset_eq forall_def mem_def) - -definition subfset :: "'a fset \ 'a fset \ bool" where - "subfset A B \ member A \ member B" - -lemma subfset_subfset_eq [code]: - "subfset A B \ subfset_eq A B \ \ subfset_eq B A" - by (simp add: subfset_def subfset_eq_def subset) - -lemma eq_fset_subfset_eq [code]: - "eq_class.eq A B \ subfset_eq A B \ subfset_eq B A" - by (cases A, cases B) (simp add: eq subfset_eq_def set_eq) - -definition inter :: "'a fset \ 'a fset \ 'a fset" where - "inter A B = Fset (List_Set.project (member A) (member B))" - -lemma inter_project [code]: - "inter A B = project (member A) B" - by (simp add: inter_def project_def inter) - - -subsection {* Misc operations *} - -lemma size_fset [code]: - "fset_size f A = 0" - "size A = 0" - by (cases A, simp) (cases A, simp) - -lemma fset_case_code [code]: - "fset_case f A = f (member A)" - by (cases A) simp - -lemma fset_rec_code [code]: - "fset_rec f A = f (member A)" - by (cases A) simp - -end diff -r cc7ddda02436 -r 50b307148dab src/HOL/Library/Executable_Set.thy --- a/src/HOL/Library/Executable_Set.thy Sun Jun 28 22:51:29 2009 +0200 +++ b/src/HOL/Library/Executable_Set.thy Mon Jun 29 14:55:08 2009 +0200 @@ -5,249 +5,43 @@ header {* Implementation of finite sets by lists *} theory Executable_Set -imports Main +imports Main Fset begin -subsection {* Definitional rewrites *} +subsection {* Derived set operations *} + +declare member [code] definition subset :: "'a set \ 'a set \ bool" where "subset = op \" declare subset_def [symmetric, code unfold] -lemma [code]: "subset A B \ (\x\A. x \ B)" - unfolding subset_def subset_eq .. - -definition is_empty :: "'a set \ bool" where - "is_empty A \ A = {}" +lemma [code]: + "subset A B \ (\x\A. x \ B)" + by (simp add: subset_def subset_eq) definition eq_set :: "'a set \ 'a set \ bool" where [code del]: "eq_set = op =" -lemma [code]: "eq_set A B \ A \ B \ B \ A" - unfolding eq_set_def by auto - (* FIXME allow for Stefan's code generator: declare set_eq_subset[code unfold] *) lemma [code]: - "a \ A \ (\x\A. x = a)" - unfolding bex_triv_one_point1 .. - -definition filter_set :: "('a \ bool) \ 'a set \ 'a set" where - "filter_set P xs = {x\xs. P x}" - -declare filter_set_def[symmetric, code unfold] - - -subsection {* Operations on lists *} - -subsubsection {* Basic definitions *} - -definition - flip :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where - "flip f a b = f b a" - -definition - member :: "'a list \ 'a \ bool" where - "member xs x \ x \ set xs" - -definition - insertl :: "'a \ 'a list \ 'a list" where - "insertl x xs = (if member xs x then xs else x#xs)" - -lemma [code target: List]: "member [] y \ False" - and [code target: List]: "member (x#xs) y \ y = x \ member xs y" - unfolding member_def by (induct xs) simp_all - -fun - drop_first :: "('a \ bool) \ 'a list \ '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 \ A \ B \ B \ 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 (\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 (\y. y = x) xs" by (induct xs) simp_all - with True show ?thesis by simp -qed - -lemma member_nil [simp]: - "member [] = (\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 \ 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: "\ (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 \ 'a list \ '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 \ 'a list \ '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 \ 'a list \ 'a list" -where - "subtract [] ys = ys" -| "subtract xs [] = []" -| "subtract xs ys = foldr remove1 xs ys" -by pat_completeness auto -termination by lexicographic_order - -lemmas subtract_eq = subtract.simps(3) - -function map_distinct :: "('a \ 'b) \ 'a list \ '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 \ '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 \ 'a list" -primrec - "intersects (x#xs) = foldr intersect xs x" - -definition - map_union :: "'a list \ ('a \ 'b list) \ 'b list" where - "map_union xs f = unions (map f xs)" - -definition - map_inter :: "'a list \ ('a \ 'b list) \ 'b list" where - "map_inter xs f = intersects (map f xs)" - - -subsection {* Isomorphism proofs *} - -lemma iso_member: - "member xs x \ x \ set xs" - unfolding member_def mem_iff .. +subsection {* Rewrites for primitive operations *} -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 \ set ys" - unfolding unionl_eq - by (induct xs arbitrary: ys) (simp_all add: iso_insert) - -lemma iso_intersect: - "set (intersect xs ys) = set xs \ set ys" - unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto - -definition - subtract' :: "'a list \ 'a list \ '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) +declare List_Set.project_def [symmetric, code unfold] -lemma iso_unions: - "set (unions xss) = \ 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)) = \ 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 \ ('a \ bool) \ bool" where - "Blall = flip list_all" -definition - Blex :: "'a list \ ('a \ bool) \ 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 *} @@ -257,23 +51,33 @@ nonfix subset; *} -subsubsection {* const serializations *} +definition flip :: "('a \ 'b \ 'c) \ 'b \ 'a \ 'c" where + "flip f a b = f b a" + +types_code + fset ("(_/ \fset)") +attach {* +datatype 'a fset = Set of 'a list; +*} + +consts_code + Set ("\Set") consts_code - "Set.empty" ("{*[]*}") - insert ("{*insertl*}") - is_empty ("{*null*}") - "op \" ("{*unionl*}") - "op \" ("{*intersect*}") - "op - \ 'a set \ 'a set \ '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" ("{*Fset.empty*}") + "List_Set.is_empty" ("{*Fset.is_empty*}") + "Set.insert" ("{*Fset.insert*}") + "List_Set.remove" ("{*Fset.remove*}") + "Set.image" ("{*Fset.map*}") + "List_Set.project" ("{*Fset.filter*}") + "Ball" ("{*flip Fset.forall*}") + "Bex" ("{*flip Fset.exists*}") + "op \" ("{*Fset.union*}") + "op \" ("{*Fset.inter*}") + "op - \ 'a set \ 'a set \ 'a set" ("{*flip Fset.subtract*}") + "Set.Union" ("{*Fset.Union*}") + "Set.Inter" ("{*Fset.Inter*}") + card ("{*Fset.card*}") + fold ("{*foldl o flip*}") -end +end \ No newline at end of file diff -r cc7ddda02436 -r 50b307148dab src/HOL/Library/Fset.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/Fset.thy Mon Jun 29 14:55:08 2009 +0200 @@ -0,0 +1,240 @@ + +(* Author: Florian Haftmann, TU Muenchen *) + +header {* Executable finite sets *} + +theory Fset +imports List_Set +begin + +lemma foldl_apply_inv: + assumes "\x. g (h x) = x" + shows "foldl f (g s) xs = g (foldl (\s x. h (f (g s) x)) s xs)" + by (rule sym, induct xs arbitrary: s) (simp_all add: assms) + +declare mem_def [simp] + + +subsection {* Lifting *} + +datatype 'a fset = Fset "'a set" + +primrec member :: "'a fset \ 'a set" where + "member (Fset A) = A" + +lemma Fset_member [simp]: + "Fset (member A) = A" + by (cases A) simp + +definition Set :: "'a list \ 'a fset" where + "Set xs = Fset (set xs)" + +lemma member_Set [simp]: + "member (Set xs) = set xs" + by (simp add: Set_def) + +code_datatype Set + + +subsection {* Basic operations *} + +definition is_empty :: "'a fset \ bool" where + [simp]: "is_empty A \ List_Set.is_empty (member A)" + +lemma is_empty_Set [code]: + "is_empty (Set xs) \ null xs" + by (simp add: is_empty_set) + +definition empty :: "'a fset" where + [simp]: "empty = Fset {}" + +lemma empty_Set [code]: + "empty = Set []" + by (simp add: Set_def) + +definition insert :: "'a \ 'a fset \ 'a fset" where + [simp]: "insert x A = Fset (Set.insert x (member A))" + +lemma insert_Set [code]: + "insert x (Set xs) = Set (List_Set.insert x xs)" + by (simp add: Set_def insert_set) + +definition remove :: "'a \ 'a fset \ 'a fset" where + [simp]: "remove x A = Fset (List_Set.remove x (member A))" + +lemma remove_Set [code]: + "remove x (Set xs) = Set (remove_all x xs)" + by (simp add: Set_def remove_set) + +definition map :: "('a \ 'b) \ 'a fset \ 'b fset" where + [simp]: "map f A = Fset (image f (member A))" + +lemma map_Set [code]: + "map f (Set xs) = Set (remdups (List.map f xs))" + by (simp add: Set_def) + +definition filter :: "('a \ bool) \ 'a fset \ 'a fset" where + [simp]: "filter P A = Fset (List_Set.project P (member A))" + +lemma filter_Set [code]: + "filter P (Set xs) = Set (List.filter P xs)" + by (simp add: Set_def project_set) + +definition forall :: "('a \ bool) \ 'a fset \ bool" where + [simp]: "forall P A \ Ball (member A) P" + +lemma forall_Set [code]: + "forall P (Set xs) \ list_all P xs" + by (simp add: Set_def ball_set) + +definition exists :: "('a \ bool) \ 'a fset \ bool" where + [simp]: "exists P A \ Bex (member A) P" + +lemma exists_Set [code]: + "exists P (Set xs) \ list_ex P xs" + by (simp add: Set_def bex_set) + +definition card :: "'a fset \ nat" where + [simp]: "card A = Finite_Set.card (member A)" + +lemma card_Set [code]: + "card (Set xs) = length (remdups xs)" +proof - + have "Finite_Set.card (set (remdups xs)) = length (remdups xs)" + by (rule distinct_card) simp + then show ?thesis by (simp add: Set_def card_def) +qed + + +subsection {* Derived operations *} + +lemma member_exists [code]: + "member A y \ exists (\x. y = x) A" + by simp + +definition subfset_eq :: "'a fset \ 'a fset \ bool" where + [simp]: "subfset_eq A B \ member A \ member B" + +lemma subfset_eq_forall [code]: + "subfset_eq A B \ forall (\x. member B x) A" + by (simp add: subset_eq) + +definition subfset :: "'a fset \ 'a fset \ bool" where + [simp]: "subfset A B \ member A \ member B" + +lemma subfset_subfset_eq [code]: + "subfset A B \ subfset_eq A B \ \ subfset_eq B A" + by (simp add: subset) + +lemma eq_fset_subfset_eq [code]: + "eq_class.eq A B \ subfset_eq A B \ subfset_eq B A" + by (cases A, cases B) (simp add: eq set_eq) + +definition inter :: "'a fset \ 'a fset \ 'a fset" where + [simp]: "inter A B = Fset (project (member A) (member B))" + +lemma inter_project [code]: + "inter A B = filter (member A) B" + by (simp add: inter) + + +subsection {* Functorial operations *} + +definition union :: "'a fset \ 'a fset \ 'a fset" where + [simp]: "union A B = Fset (member A \ member B)" + +lemma union_insert [code]: + "union (Set xs) A = foldl (\A x. insert x A) A xs" +proof - + have "foldl (\A x. Set.insert x A) (member A) xs = + member (foldl (\A x. Fset (Set.insert x (member A))) A xs)" + by (rule foldl_apply_inv) simp + then show ?thesis by (simp add: union_set) +qed + +definition subtract :: "'a fset \ 'a fset \ 'a fset" where + [simp]: "subtract A B = Fset (member B - member A)" + +lemma subtract_remove [code]: + "subtract (Set xs) A = foldl (\A x. remove x A) A xs" +proof - + have "foldl (\A x. List_Set.remove x A) (member A) xs = + member (foldl (\A x. Fset (List_Set.remove x (member A))) A xs)" + by (rule foldl_apply_inv) simp + then show ?thesis by (simp add: minus_set) +qed + +definition Inter :: "'a fset fset \ 'a fset" where + [simp]: "Inter A = Fset (Set.Inter (member ` member A))" + +lemma Inter_inter [code]: + "Inter (Set (A # As)) = foldl inter A As" +proof - + note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del] + have "foldl (op \) (member A) (List.map member As) = + member (foldl (\B A. Fset (member B \ A)) A (List.map member As))" + by (rule foldl_apply_inv) simp + then show ?thesis + by (simp add: Inter_set image_set inter_def_raw inter foldl_map) +qed + +definition Union :: "'a fset fset \ 'a fset" where + [simp]: "Union A = Fset (Set.Union (member ` member A))" + +lemma Union_union [code]: + "Union (Set As) = foldl union empty As" +proof - + note Union_image_eq [simp del] set_map [simp del] + have "foldl (op \) (member empty) (List.map member As) = + member (foldl (\B A. Fset (member B \ A)) empty (List.map member As))" + by (rule foldl_apply_inv) simp + then show ?thesis + by (simp add: Union_set image_set union_def_raw foldl_map) +qed + + +subsection {* Misc operations *} + +lemma size_fset [code]: + "fset_size f A = 0" + "size A = 0" + by (cases A, simp) (cases A, simp) + +lemma fset_case_code [code]: + "fset_case f A = f (member A)" + by (cases A) simp + +lemma fset_rec_code [code]: + "fset_rec f A = f (member A)" + by (cases A) simp + + +subsection {* Simplified simprules *} + +lemma is_empty_simp [simp]: + "is_empty A \ member A = {}" + by (simp add: List_Set.is_empty_def) +declare is_empty_def [simp del] + +lemma remove_simp [simp]: + "remove x A = Fset (member A - {x})" + by (simp add: List_Set.remove_def) +declare remove_def [simp del] + +lemma filter_simp [simp]: + "filter P A = Fset {x \ member A. P x}" + by (simp add: List_Set.project_def) +declare filter_def [simp del] + +lemma inter_simp [simp]: + "inter A B = Fset (member A \ member B)" + by (simp add: inter) +declare inter_def [simp del] + +declare mem_def [simp del] + + +hide (open) const is_empty empty insert remove map filter forall exists card + subfset_eq subfset inter union subtract Inter Union + +end diff -r cc7ddda02436 -r 50b307148dab src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Sun Jun 28 22:51:29 2009 +0200 +++ b/src/HOL/Library/Library.thy Mon Jun 29 14:55:08 2009 +0200 @@ -10,7 +10,6 @@ Char_ord Code_Char_chr Code_Integer - Code_Set Coinductive_List Commutative_Ring Continuity @@ -28,6 +27,7 @@ Formal_Power_Series Fraction_Field FrechetDeriv + Fset FuncSet Fundamental_Theorem_Algebra Infinite_Set diff -r cc7ddda02436 -r 50b307148dab src/HOL/Library/List_Set.thy --- a/src/HOL/Library/List_Set.thy Sun Jun 28 22:51:29 2009 +0200 +++ b/src/HOL/Library/List_Set.thy Mon Jun 29 14:55:08 2009 +0200 @@ -70,7 +70,7 @@ by (auto simp add: remove_def remove_all_def) lemma image_set: - "image f (set xs) = set (remdups (map f xs))" + "image f (set xs) = set (map f xs)" by simp lemma project_set: @@ -160,4 +160,7 @@ "A \ B = project (\x. x \ A) B" by (auto simp add: project_def) + +hide (open) const insert + end \ No newline at end of file diff -r cc7ddda02436 -r 50b307148dab src/HOL/MicroJava/BV/BVExample.thy --- a/src/HOL/MicroJava/BV/BVExample.thy Sun Jun 28 22:51:29 2009 +0200 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Jun 29 14:55:08 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/MicroJava/BV/BVExample.thy - ID: $Id$ Author: Gerwin Klein *) @@ -94,7 +93,7 @@ text {* Method and field lookup: *} lemma method_Object [simp]: - "method (E, Object) = empty" + "method (E, Object) = Map.empty" by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E]) lemma method_append [simp]: @@ -436,7 +435,7 @@ "some_elem = (%S. SOME x. x : S)" consts_code - "some_elem" ("hd") + "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)") text {* This code setup is just a demonstration and \emph{not} sound! *} @@ -455,7 +454,7 @@ (\(ss, w). let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) (ss, w)" - unfolding iter_def is_empty_def some_elem_def .. + unfolding iter_def List_Set.is_empty_def some_elem_def .. lemma JVM_sup_unfold [code]: "JVMType.sup S m n = lift2 (Opt.sup @@ -475,7 +474,6 @@ test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0 [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins" test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins" - ML BV.test1 ML BV.test2 diff -r cc7ddda02436 -r 50b307148dab src/HOL/Tools/dseq.ML --- a/src/HOL/Tools/dseq.ML Sun Jun 28 22:51:29 2009 +0200 +++ b/src/HOL/Tools/dseq.ML Mon Jun 29 14:55:08 2009 +0200 @@ -1,5 +1,4 @@ (* Title: HOL/Tools/dseq.ML - ID: $Id$ Author: Stefan Berghofer, TU Muenchen Sequences with recursion depth limit. diff -r cc7ddda02436 -r 50b307148dab src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Sun Jun 28 22:51:29 2009 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Jun 29 14:55:08 2009 +0200 @@ -378,7 +378,7 @@ end | compile_prems out_ts vs names ps gr = let - val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts)); + val vs' = distinct (op =) (flat (vs :: map term_vs out_ts)); val SOME (p, mode as SOME (Mode (_, js, _))) = select_mode_prem thy modes' vs' ps; val ps' = filter_out (equal p) ps; @@ -404,7 +404,9 @@ (compile_expr thy defs dep module false modes (mode, t) gr2) else - apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p]) + apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p, + str "of", str "Set", str "xs", str "=>", str "xs)"]) + (*this is a very strong assumption about the generated code!*) (invoke_codegen thy defs dep module true t gr2); val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3; in @@ -661,8 +663,10 @@ let val (call_p, gr') = mk_ind_call thy defs dep module true s T (ts1 @ ts2') names thyname k intrs gr in SOME ((if brack then parens else I) (Pretty.block - [str "DSeq.list_of", Pretty.brk 1, str "(", - conv_ntuple fs ots call_p, str ")"]), gr') + [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(", + conv_ntuple fs ots call_p, str "))"]), + (*this is a very strong assumption about the generated code!*) + gr') end else NONE end diff -r cc7ddda02436 -r 50b307148dab src/HOL/ex/Codegenerator_Candidates.thy --- a/src/HOL/ex/Codegenerator_Candidates.thy Sun Jun 28 22:51:29 2009 +0200 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Mon Jun 29 14:55:08 2009 +0200 @@ -8,7 +8,7 @@ Complex_Main AssocList Binomial - Code_Set + Fset Commutative_Ring Enum List_Prefix