1.1 --- a/doc-src/Codegen/Thy/document/Introduction.tex Sun Jun 28 22:51:29 2009 +0200
1.2 +++ b/doc-src/Codegen/Thy/document/Introduction.tex Mon Jun 29 14:55:08 2009 +0200
1.3 @@ -249,9 +249,9 @@
1.4 \hspace*{0pt}dequeue (AQueue [] []) = (Nothing,~AQueue [] []);\\
1.5 \hspace*{0pt}dequeue (AQueue xs (y :~ys)) = (Just y,~AQueue xs ys);\\
1.6 \hspace*{0pt}dequeue (AQueue (v :~va) []) =\\
1.7 -\hspace*{0pt} ~(let {\char123}\\
1.8 +\hspace*{0pt} ~let {\char123}\\
1.9 \hspace*{0pt} ~~~(y :~ys) = rev (v :~va);\\
1.10 -\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys) );\\
1.11 +\hspace*{0pt} ~{\char125}~in (Just y,~AQueue [] ys);\\
1.12 \hspace*{0pt}\\
1.13 \hspace*{0pt}enqueue ::~forall a.~a -> Queue a -> Queue a;\\
1.14 \hspace*{0pt}enqueue x (AQueue xs ys) = AQueue (x :~xs) ys;\\
2.1 --- a/doc-src/Codegen/Thy/document/Program.tex Sun Jun 28 22:51:29 2009 +0200
2.2 +++ b/doc-src/Codegen/Thy/document/Program.tex Mon Jun 29 14:55:08 2009 +0200
2.3 @@ -966,9 +966,9 @@
2.4 \noindent%
2.5 \hspace*{0pt}strict{\char95}dequeue ::~forall a.~Queue a -> (a,~Queue a);\\
2.6 \hspace*{0pt}strict{\char95}dequeue (AQueue xs []) =\\
2.7 -\hspace*{0pt} ~(let {\char123}\\
2.8 +\hspace*{0pt} ~let {\char123}\\
2.9 \hspace*{0pt} ~~~(y :~ys) = rev xs;\\
2.10 -\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys) );\\
2.11 +\hspace*{0pt} ~{\char125}~in (y,~AQueue [] ys);\\
2.12 \hspace*{0pt}strict{\char95}dequeue (AQueue xs (y :~ys)) = (y,~AQueue xs ys);%
2.13 \end{isamarkuptext}%
2.14 \isamarkuptrue%
3.1 --- a/doc-src/Codegen/Thy/examples/Example.hs Sun Jun 28 22:51:29 2009 +0200
3.2 +++ b/doc-src/Codegen/Thy/examples/Example.hs Mon Jun 29 14:55:08 2009 +0200
3.3 @@ -23,9 +23,9 @@
3.4 dequeue (AQueue [] []) = (Nothing, AQueue [] []);
3.5 dequeue (AQueue xs (y : ys)) = (Just y, AQueue xs ys);
3.6 dequeue (AQueue (v : va) []) =
3.7 - (let {
3.8 + let {
3.9 (y : ys) = rev (v : va);
3.10 - } in (Just y, AQueue [] ys) );
3.11 + } in (Just y, AQueue [] ys);
3.12
3.13 enqueue :: forall a. a -> Queue a -> Queue a;
3.14 enqueue x (AQueue xs ys) = AQueue (x : xs) ys;
4.1 --- a/src/HOL/IsaMakefile Sun Jun 28 22:51:29 2009 +0200
4.2 +++ b/src/HOL/IsaMakefile Mon Jun 29 14:55:08 2009 +0200
4.3 @@ -319,7 +319,7 @@
4.4 Library/Abstract_Rat.thy \
4.5 Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy \
4.6 Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML \
4.7 - Library/Code_Set.thy Library/Convex_Euclidean_Space.thy \
4.8 + Library/Fset.thy Library/Convex_Euclidean_Space.thy \
4.9 Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
4.10 Library/Executable_Set.thy Library/Infinite_Set.thy \
4.11 Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\
5.1 --- a/src/HOL/Library/Code_Set.thy Sun Jun 28 22:51:29 2009 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,169 +0,0 @@
5.4 -
5.5 -(* Author: Florian Haftmann, TU Muenchen *)
5.6 -
5.7 -header {* Executable finite sets *}
5.8 -
5.9 -theory Code_Set
5.10 -imports List_Set
5.11 -begin
5.12 -
5.13 -lemma foldl_apply_inv:
5.14 - assumes "\<And>x. g (h x) = x"
5.15 - shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
5.16 - by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
5.17 -
5.18 -subsection {* Lifting *}
5.19 -
5.20 -datatype 'a fset = Fset "'a set"
5.21 -
5.22 -primrec member :: "'a fset \<Rightarrow> 'a set" where
5.23 - "member (Fset A) = A"
5.24 -
5.25 -lemma Fset_member [simp]:
5.26 - "Fset (member A) = A"
5.27 - by (cases A) simp
5.28 -
5.29 -definition Set :: "'a list \<Rightarrow> 'a fset" where
5.30 - "Set xs = Fset (set xs)"
5.31 -
5.32 -lemma member_Set [simp]:
5.33 - "member (Set xs) = set xs"
5.34 - by (simp add: Set_def)
5.35 -
5.36 -code_datatype Set
5.37 -
5.38 -
5.39 -subsection {* Basic operations *}
5.40 -
5.41 -definition is_empty :: "'a fset \<Rightarrow> bool" where
5.42 - "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
5.43 -
5.44 -lemma is_empty_Set [code]:
5.45 - "is_empty (Set xs) \<longleftrightarrow> null xs"
5.46 - by (simp add: is_empty_def is_empty_set)
5.47 -
5.48 -definition empty :: "'a fset" where
5.49 - "empty = Fset {}"
5.50 -
5.51 -lemma empty_Set [code]:
5.52 - "empty = Set []"
5.53 - by (simp add: empty_def Set_def)
5.54 -
5.55 -definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
5.56 - "insert x A = Fset (Set.insert x (member A))"
5.57 -
5.58 -lemma insert_Set [code]:
5.59 - "insert x (Set xs) = Set (List_Set.insert x xs)"
5.60 - by (simp add: insert_def Set_def insert_set)
5.61 -
5.62 -definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
5.63 - "remove x A = Fset (List_Set.remove x (member A))"
5.64 -
5.65 -lemma remove_Set [code]:
5.66 - "remove x (Set xs) = Set (remove_all x xs)"
5.67 - by (simp add: remove_def Set_def remove_set)
5.68 -
5.69 -definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
5.70 - "map f A = Fset (image f (member A))"
5.71 -
5.72 -lemma map_Set [code]:
5.73 - "map f (Set xs) = Set (remdups (List.map f xs))"
5.74 - by (simp add: map_def Set_def)
5.75 -
5.76 -definition project :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
5.77 - "project P A = Fset (List_Set.project P (member A))"
5.78 -
5.79 -lemma project_Set [code]:
5.80 - "project P (Set xs) = Set (filter P xs)"
5.81 - by (simp add: project_def Set_def project_set)
5.82 -
5.83 -definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
5.84 - "forall P A \<longleftrightarrow> Ball (member A) P"
5.85 -
5.86 -lemma forall_Set [code]:
5.87 - "forall P (Set xs) \<longleftrightarrow> list_all P xs"
5.88 - by (simp add: forall_def Set_def ball_set)
5.89 -
5.90 -definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
5.91 - "exists P A \<longleftrightarrow> Bex (member A) P"
5.92 -
5.93 -lemma exists_Set [code]:
5.94 - "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
5.95 - by (simp add: exists_def Set_def bex_set)
5.96 -
5.97 -
5.98 -subsection {* Functorial operations *}
5.99 -
5.100 -definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
5.101 - "union A B = Fset (member A \<union> member B)"
5.102 -
5.103 -lemma union_insert [code]:
5.104 - "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
5.105 -proof -
5.106 - have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
5.107 - member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
5.108 - by (rule foldl_apply_inv) simp
5.109 - then show ?thesis by (simp add: union_def union_set insert_def)
5.110 -qed
5.111 -
5.112 -definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
5.113 - "subtract A B = Fset (member B - member A)"
5.114 -
5.115 -lemma subtract_remove [code]:
5.116 - "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
5.117 -proof -
5.118 - have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
5.119 - member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
5.120 - by (rule foldl_apply_inv) simp
5.121 - then show ?thesis by (simp add: subtract_def minus_set remove_def)
5.122 -qed
5.123 -
5.124 -
5.125 -subsection {* Derived operations *}
5.126 -
5.127 -lemma member_exists [code]:
5.128 - "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
5.129 - by (simp add: exists_def mem_def)
5.130 -
5.131 -definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
5.132 - "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
5.133 -
5.134 -lemma subfset_eq_forall [code]:
5.135 - "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
5.136 - by (simp add: subfset_eq_def subset_eq forall_def mem_def)
5.137 -
5.138 -definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
5.139 - "subfset A B \<longleftrightarrow> member A \<subset> member B"
5.140 -
5.141 -lemma subfset_subfset_eq [code]:
5.142 - "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
5.143 - by (simp add: subfset_def subfset_eq_def subset)
5.144 -
5.145 -lemma eq_fset_subfset_eq [code]:
5.146 - "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
5.147 - by (cases A, cases B) (simp add: eq subfset_eq_def set_eq)
5.148 -
5.149 -definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
5.150 - "inter A B = Fset (List_Set.project (member A) (member B))"
5.151 -
5.152 -lemma inter_project [code]:
5.153 - "inter A B = project (member A) B"
5.154 - by (simp add: inter_def project_def inter)
5.155 -
5.156 -
5.157 -subsection {* Misc operations *}
5.158 -
5.159 -lemma size_fset [code]:
5.160 - "fset_size f A = 0"
5.161 - "size A = 0"
5.162 - by (cases A, simp) (cases A, simp)
5.163 -
5.164 -lemma fset_case_code [code]:
5.165 - "fset_case f A = f (member A)"
5.166 - by (cases A) simp
5.167 -
5.168 -lemma fset_rec_code [code]:
5.169 - "fset_rec f A = f (member A)"
5.170 - by (cases A) simp
5.171 -
5.172 -end
6.1 --- a/src/HOL/Library/Executable_Set.thy Sun Jun 28 22:51:29 2009 +0200
6.2 +++ b/src/HOL/Library/Executable_Set.thy Mon Jun 29 14:55:08 2009 +0200
6.3 @@ -5,249 +5,43 @@
6.4 header {* Implementation of finite sets by lists *}
6.5
6.6 theory Executable_Set
6.7 -imports Main
6.8 +imports Main Fset
6.9 begin
6.10
6.11 -subsection {* Definitional rewrites *}
6.12 +subsection {* Derived set operations *}
6.13 +
6.14 +declare member [code]
6.15
6.16 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
6.17 "subset = op \<le>"
6.18
6.19 declare subset_def [symmetric, code unfold]
6.20
6.21 -lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
6.22 - unfolding subset_def subset_eq ..
6.23 -
6.24 -definition is_empty :: "'a set \<Rightarrow> bool" where
6.25 - "is_empty A \<longleftrightarrow> A = {}"
6.26 +lemma [code]:
6.27 + "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
6.28 + by (simp add: subset_def subset_eq)
6.29
6.30 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
6.31 [code del]: "eq_set = op ="
6.32
6.33 -lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
6.34 - unfolding eq_set_def by auto
6.35 -
6.36 (* FIXME allow for Stefan's code generator:
6.37 declare set_eq_subset[code unfold]
6.38 *)
6.39
6.40 lemma [code]:
6.41 - "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
6.42 - unfolding bex_triv_one_point1 ..
6.43 + "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
6.44 + by (simp add: eq_set_def set_eq)
6.45
6.46 -definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
6.47 - "filter_set P xs = {x\<in>xs. P x}"
6.48 +declare inter [code]
6.49
6.50 -declare filter_set_def[symmetric, code unfold]
6.51 +declare Inter_image_eq [symmetric, code]
6.52 +declare Union_image_eq [symmetric, code]
6.53
6.54
6.55 -subsection {* Operations on lists *}
6.56 +subsection {* Rewrites for primitive operations *}
6.57
6.58 -subsubsection {* Basic definitions *}
6.59 +declare List_Set.project_def [symmetric, code unfold]
6.60
6.61 -definition
6.62 - flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
6.63 - "flip f a b = f b a"
6.64 -
6.65 -definition
6.66 - member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
6.67 - "member xs x \<longleftrightarrow> x \<in> set xs"
6.68 -
6.69 -definition
6.70 - insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
6.71 - "insertl x xs = (if member xs x then xs else x#xs)"
6.72 -
6.73 -lemma [code target: List]: "member [] y \<longleftrightarrow> False"
6.74 - and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
6.75 - unfolding member_def by (induct xs) simp_all
6.76 -
6.77 -fun
6.78 - drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
6.79 - "drop_first f [] = []"
6.80 -| "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
6.81 -declare drop_first.simps [code del]
6.82 -declare drop_first.simps [code target: List]
6.83 -
6.84 -declare remove1.simps [code del]
6.85 -lemma [code target: List]:
6.86 - "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
6.87 -proof (cases "member xs x")
6.88 - case False thus ?thesis unfolding member_def by (induct xs) auto
6.89 -next
6.90 - case True
6.91 - have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
6.92 - with True show ?thesis by simp
6.93 -qed
6.94 -
6.95 -lemma member_nil [simp]:
6.96 - "member [] = (\<lambda>x. False)"
6.97 -proof (rule ext)
6.98 - fix x
6.99 - show "member [] x = False" unfolding member_def by simp
6.100 -qed
6.101 -
6.102 -lemma member_insertl [simp]:
6.103 - "x \<in> set (insertl x xs)"
6.104 - unfolding insertl_def member_def mem_iff by simp
6.105 -
6.106 -lemma insertl_member [simp]:
6.107 - fixes xs x
6.108 - assumes member: "member xs x"
6.109 - shows "insertl x xs = xs"
6.110 - using member unfolding insertl_def by simp
6.111 -
6.112 -lemma insertl_not_member [simp]:
6.113 - fixes xs x
6.114 - assumes member: "\<not> (member xs x)"
6.115 - shows "insertl x xs = x # xs"
6.116 - using member unfolding insertl_def by simp
6.117 -
6.118 -lemma foldr_remove1_empty [simp]:
6.119 - "foldr remove1 xs [] = []"
6.120 - by (induct xs) simp_all
6.121 -
6.122 -
6.123 -subsubsection {* Derived definitions *}
6.124 -
6.125 -function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
6.126 -where
6.127 - "unionl [] ys = ys"
6.128 -| "unionl xs ys = foldr insertl xs ys"
6.129 -by pat_completeness auto
6.130 -termination by lexicographic_order
6.131 -
6.132 -lemmas unionl_eq = unionl.simps(2)
6.133 -
6.134 -function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
6.135 -where
6.136 - "intersect [] ys = []"
6.137 -| "intersect xs [] = []"
6.138 -| "intersect xs ys = filter (member xs) ys"
6.139 -by pat_completeness auto
6.140 -termination by lexicographic_order
6.141 -
6.142 -lemmas intersect_eq = intersect.simps(3)
6.143 -
6.144 -function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
6.145 -where
6.146 - "subtract [] ys = ys"
6.147 -| "subtract xs [] = []"
6.148 -| "subtract xs ys = foldr remove1 xs ys"
6.149 -by pat_completeness auto
6.150 -termination by lexicographic_order
6.151 -
6.152 -lemmas subtract_eq = subtract.simps(3)
6.153 -
6.154 -function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
6.155 -where
6.156 - "map_distinct f [] = []"
6.157 -| "map_distinct f xs = foldr (insertl o f) xs []"
6.158 -by pat_completeness auto
6.159 -termination by lexicographic_order
6.160 -
6.161 -lemmas map_distinct_eq = map_distinct.simps(2)
6.162 -
6.163 -function unions :: "'a list list \<Rightarrow> 'a list"
6.164 -where
6.165 - "unions [] = []"
6.166 -| "unions xs = foldr unionl xs []"
6.167 -by pat_completeness auto
6.168 -termination by lexicographic_order
6.169 -
6.170 -lemmas unions_eq = unions.simps(2)
6.171 -
6.172 -consts intersects :: "'a list list \<Rightarrow> 'a list"
6.173 -primrec
6.174 - "intersects (x#xs) = foldr intersect xs x"
6.175 -
6.176 -definition
6.177 - map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
6.178 - "map_union xs f = unions (map f xs)"
6.179 -
6.180 -definition
6.181 - map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
6.182 - "map_inter xs f = intersects (map f xs)"
6.183 -
6.184 -
6.185 -subsection {* Isomorphism proofs *}
6.186 -
6.187 -lemma iso_member:
6.188 - "member xs x \<longleftrightarrow> x \<in> set xs"
6.189 - unfolding member_def mem_iff ..
6.190 -
6.191 -lemma iso_insert:
6.192 - "set (insertl x xs) = insert x (set xs)"
6.193 - unfolding insertl_def iso_member by (simp add: insert_absorb)
6.194 -
6.195 -lemma iso_remove1:
6.196 - assumes distnct: "distinct xs"
6.197 - shows "set (remove1 x xs) = set xs - {x}"
6.198 - using distnct set_remove1_eq by auto
6.199 -
6.200 -lemma iso_union:
6.201 - "set (unionl xs ys) = set xs \<union> set ys"
6.202 - unfolding unionl_eq
6.203 - by (induct xs arbitrary: ys) (simp_all add: iso_insert)
6.204 -
6.205 -lemma iso_intersect:
6.206 - "set (intersect xs ys) = set xs \<inter> set ys"
6.207 - unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
6.208 -
6.209 -definition
6.210 - subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
6.211 - "subtract' = flip subtract"
6.212 -
6.213 -lemma iso_subtract:
6.214 - fixes ys
6.215 - assumes distnct: "distinct ys"
6.216 - shows "set (subtract' ys xs) = set ys - set xs"
6.217 - and "distinct (subtract' ys xs)"
6.218 - unfolding subtract'_def flip_def subtract_eq
6.219 - using distnct by (induct xs arbitrary: ys) auto
6.220 -
6.221 -lemma iso_map_distinct:
6.222 - "set (map_distinct f xs) = image f (set xs)"
6.223 - unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
6.224 -
6.225 -lemma iso_unions:
6.226 - "set (unions xss) = \<Union> set (map set xss)"
6.227 - unfolding unions_eq
6.228 -proof (induct xss)
6.229 - case Nil show ?case by simp
6.230 -next
6.231 - case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
6.232 -qed
6.233 -
6.234 -lemma iso_intersects:
6.235 - "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
6.236 - by (induct xss) (simp_all add: Int_def iso_member, auto)
6.237 -
6.238 -lemma iso_UNION:
6.239 - "set (map_union xs f) = UNION (set xs) (set o f)"
6.240 - unfolding map_union_def iso_unions by simp
6.241 -
6.242 -lemma iso_INTER:
6.243 - "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
6.244 - unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
6.245 -
6.246 -definition
6.247 - Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
6.248 - "Blall = flip list_all"
6.249 -definition
6.250 - Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
6.251 - "Blex = flip list_ex"
6.252 -
6.253 -lemma iso_Ball:
6.254 - "Blall xs f = Ball (set xs) f"
6.255 - unfolding Blall_def flip_def by (induct xs) simp_all
6.256 -
6.257 -lemma iso_Bex:
6.258 - "Blex xs f = Bex (set xs) f"
6.259 - unfolding Blex_def flip_def by (induct xs) simp_all
6.260 -
6.261 -lemma iso_filter:
6.262 - "set (filter P xs) = filter_set P (set xs)"
6.263 - unfolding filter_set_def by (induct xs) auto
6.264
6.265 subsection {* code generator setup *}
6.266
6.267 @@ -257,23 +51,33 @@
6.268 nonfix subset;
6.269 *}
6.270
6.271 -subsubsection {* const serializations *}
6.272 +definition flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
6.273 + "flip f a b = f b a"
6.274 +
6.275 +types_code
6.276 + fset ("(_/ \<module>fset)")
6.277 +attach {*
6.278 +datatype 'a fset = Set of 'a list;
6.279 +*}
6.280
6.281 consts_code
6.282 - "Set.empty" ("{*[]*}")
6.283 - insert ("{*insertl*}")
6.284 - is_empty ("{*null*}")
6.285 - "op \<union>" ("{*unionl*}")
6.286 - "op \<inter>" ("{*intersect*}")
6.287 - "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
6.288 - image ("{*map_distinct*}")
6.289 - Union ("{*unions*}")
6.290 - Inter ("{*intersects*}")
6.291 - UNION ("{*map_union*}")
6.292 - INTER ("{*map_inter*}")
6.293 - Ball ("{*Blall*}")
6.294 - Bex ("{*Blex*}")
6.295 - filter_set ("{*filter*}")
6.296 - fold ("{* foldl o flip *}")
6.297 + Set ("\<module>Set")
6.298
6.299 -end
6.300 +consts_code
6.301 + "Set.empty" ("{*Fset.empty*}")
6.302 + "List_Set.is_empty" ("{*Fset.is_empty*}")
6.303 + "Set.insert" ("{*Fset.insert*}")
6.304 + "List_Set.remove" ("{*Fset.remove*}")
6.305 + "Set.image" ("{*Fset.map*}")
6.306 + "List_Set.project" ("{*Fset.filter*}")
6.307 + "Ball" ("{*flip Fset.forall*}")
6.308 + "Bex" ("{*flip Fset.exists*}")
6.309 + "op \<union>" ("{*Fset.union*}")
6.310 + "op \<inter>" ("{*Fset.inter*}")
6.311 + "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{*flip Fset.subtract*}")
6.312 + "Set.Union" ("{*Fset.Union*}")
6.313 + "Set.Inter" ("{*Fset.Inter*}")
6.314 + card ("{*Fset.card*}")
6.315 + fold ("{*foldl o flip*}")
6.316 +
6.317 +end
6.318 \ No newline at end of file
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/Library/Fset.thy Mon Jun 29 14:55:08 2009 +0200
7.3 @@ -0,0 +1,240 @@
7.4 +
7.5 +(* Author: Florian Haftmann, TU Muenchen *)
7.6 +
7.7 +header {* Executable finite sets *}
7.8 +
7.9 +theory Fset
7.10 +imports List_Set
7.11 +begin
7.12 +
7.13 +lemma foldl_apply_inv:
7.14 + assumes "\<And>x. g (h x) = x"
7.15 + shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
7.16 + by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
7.17 +
7.18 +declare mem_def [simp]
7.19 +
7.20 +
7.21 +subsection {* Lifting *}
7.22 +
7.23 +datatype 'a fset = Fset "'a set"
7.24 +
7.25 +primrec member :: "'a fset \<Rightarrow> 'a set" where
7.26 + "member (Fset A) = A"
7.27 +
7.28 +lemma Fset_member [simp]:
7.29 + "Fset (member A) = A"
7.30 + by (cases A) simp
7.31 +
7.32 +definition Set :: "'a list \<Rightarrow> 'a fset" where
7.33 + "Set xs = Fset (set xs)"
7.34 +
7.35 +lemma member_Set [simp]:
7.36 + "member (Set xs) = set xs"
7.37 + by (simp add: Set_def)
7.38 +
7.39 +code_datatype Set
7.40 +
7.41 +
7.42 +subsection {* Basic operations *}
7.43 +
7.44 +definition is_empty :: "'a fset \<Rightarrow> bool" where
7.45 + [simp]: "is_empty A \<longleftrightarrow> List_Set.is_empty (member A)"
7.46 +
7.47 +lemma is_empty_Set [code]:
7.48 + "is_empty (Set xs) \<longleftrightarrow> null xs"
7.49 + by (simp add: is_empty_set)
7.50 +
7.51 +definition empty :: "'a fset" where
7.52 + [simp]: "empty = Fset {}"
7.53 +
7.54 +lemma empty_Set [code]:
7.55 + "empty = Set []"
7.56 + by (simp add: Set_def)
7.57 +
7.58 +definition insert :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
7.59 + [simp]: "insert x A = Fset (Set.insert x (member A))"
7.60 +
7.61 +lemma insert_Set [code]:
7.62 + "insert x (Set xs) = Set (List_Set.insert x xs)"
7.63 + by (simp add: Set_def insert_set)
7.64 +
7.65 +definition remove :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
7.66 + [simp]: "remove x A = Fset (List_Set.remove x (member A))"
7.67 +
7.68 +lemma remove_Set [code]:
7.69 + "remove x (Set xs) = Set (remove_all x xs)"
7.70 + by (simp add: Set_def remove_set)
7.71 +
7.72 +definition map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset" where
7.73 + [simp]: "map f A = Fset (image f (member A))"
7.74 +
7.75 +lemma map_Set [code]:
7.76 + "map f (Set xs) = Set (remdups (List.map f xs))"
7.77 + by (simp add: Set_def)
7.78 +
7.79 +definition filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
7.80 + [simp]: "filter P A = Fset (List_Set.project P (member A))"
7.81 +
7.82 +lemma filter_Set [code]:
7.83 + "filter P (Set xs) = Set (List.filter P xs)"
7.84 + by (simp add: Set_def project_set)
7.85 +
7.86 +definition forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
7.87 + [simp]: "forall P A \<longleftrightarrow> Ball (member A) P"
7.88 +
7.89 +lemma forall_Set [code]:
7.90 + "forall P (Set xs) \<longleftrightarrow> list_all P xs"
7.91 + by (simp add: Set_def ball_set)
7.92 +
7.93 +definition exists :: "('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> bool" where
7.94 + [simp]: "exists P A \<longleftrightarrow> Bex (member A) P"
7.95 +
7.96 +lemma exists_Set [code]:
7.97 + "exists P (Set xs) \<longleftrightarrow> list_ex P xs"
7.98 + by (simp add: Set_def bex_set)
7.99 +
7.100 +definition card :: "'a fset \<Rightarrow> nat" where
7.101 + [simp]: "card A = Finite_Set.card (member A)"
7.102 +
7.103 +lemma card_Set [code]:
7.104 + "card (Set xs) = length (remdups xs)"
7.105 +proof -
7.106 + have "Finite_Set.card (set (remdups xs)) = length (remdups xs)"
7.107 + by (rule distinct_card) simp
7.108 + then show ?thesis by (simp add: Set_def card_def)
7.109 +qed
7.110 +
7.111 +
7.112 +subsection {* Derived operations *}
7.113 +
7.114 +lemma member_exists [code]:
7.115 + "member A y \<longleftrightarrow> exists (\<lambda>x. y = x) A"
7.116 + by simp
7.117 +
7.118 +definition subfset_eq :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
7.119 + [simp]: "subfset_eq A B \<longleftrightarrow> member A \<subseteq> member B"
7.120 +
7.121 +lemma subfset_eq_forall [code]:
7.122 + "subfset_eq A B \<longleftrightarrow> forall (\<lambda>x. member B x) A"
7.123 + by (simp add: subset_eq)
7.124 +
7.125 +definition subfset :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> bool" where
7.126 + [simp]: "subfset A B \<longleftrightarrow> member A \<subset> member B"
7.127 +
7.128 +lemma subfset_subfset_eq [code]:
7.129 + "subfset A B \<longleftrightarrow> subfset_eq A B \<and> \<not> subfset_eq B A"
7.130 + by (simp add: subset)
7.131 +
7.132 +lemma eq_fset_subfset_eq [code]:
7.133 + "eq_class.eq A B \<longleftrightarrow> subfset_eq A B \<and> subfset_eq B A"
7.134 + by (cases A, cases B) (simp add: eq set_eq)
7.135 +
7.136 +definition inter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
7.137 + [simp]: "inter A B = Fset (project (member A) (member B))"
7.138 +
7.139 +lemma inter_project [code]:
7.140 + "inter A B = filter (member A) B"
7.141 + by (simp add: inter)
7.142 +
7.143 +
7.144 +subsection {* Functorial operations *}
7.145 +
7.146 +definition union :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
7.147 + [simp]: "union A B = Fset (member A \<union> member B)"
7.148 +
7.149 +lemma union_insert [code]:
7.150 + "union (Set xs) A = foldl (\<lambda>A x. insert x A) A xs"
7.151 +proof -
7.152 + have "foldl (\<lambda>A x. Set.insert x A) (member A) xs =
7.153 + member (foldl (\<lambda>A x. Fset (Set.insert x (member A))) A xs)"
7.154 + by (rule foldl_apply_inv) simp
7.155 + then show ?thesis by (simp add: union_set)
7.156 +qed
7.157 +
7.158 +definition subtract :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" where
7.159 + [simp]: "subtract A B = Fset (member B - member A)"
7.160 +
7.161 +lemma subtract_remove [code]:
7.162 + "subtract (Set xs) A = foldl (\<lambda>A x. remove x A) A xs"
7.163 +proof -
7.164 + have "foldl (\<lambda>A x. List_Set.remove x A) (member A) xs =
7.165 + member (foldl (\<lambda>A x. Fset (List_Set.remove x (member A))) A xs)"
7.166 + by (rule foldl_apply_inv) simp
7.167 + then show ?thesis by (simp add: minus_set)
7.168 +qed
7.169 +
7.170 +definition Inter :: "'a fset fset \<Rightarrow> 'a fset" where
7.171 + [simp]: "Inter A = Fset (Set.Inter (member ` member A))"
7.172 +
7.173 +lemma Inter_inter [code]:
7.174 + "Inter (Set (A # As)) = foldl inter A As"
7.175 +proof -
7.176 + note Inter_image_eq [simp del] set_map [simp del] set.simps [simp del]
7.177 + have "foldl (op \<inter>) (member A) (List.map member As) =
7.178 + member (foldl (\<lambda>B A. Fset (member B \<inter> A)) A (List.map member As))"
7.179 + by (rule foldl_apply_inv) simp
7.180 + then show ?thesis
7.181 + by (simp add: Inter_set image_set inter_def_raw inter foldl_map)
7.182 +qed
7.183 +
7.184 +definition Union :: "'a fset fset \<Rightarrow> 'a fset" where
7.185 + [simp]: "Union A = Fset (Set.Union (member ` member A))"
7.186 +
7.187 +lemma Union_union [code]:
7.188 + "Union (Set As) = foldl union empty As"
7.189 +proof -
7.190 + note Union_image_eq [simp del] set_map [simp del]
7.191 + have "foldl (op \<union>) (member empty) (List.map member As) =
7.192 + member (foldl (\<lambda>B A. Fset (member B \<union> A)) empty (List.map member As))"
7.193 + by (rule foldl_apply_inv) simp
7.194 + then show ?thesis
7.195 + by (simp add: Union_set image_set union_def_raw foldl_map)
7.196 +qed
7.197 +
7.198 +
7.199 +subsection {* Misc operations *}
7.200 +
7.201 +lemma size_fset [code]:
7.202 + "fset_size f A = 0"
7.203 + "size A = 0"
7.204 + by (cases A, simp) (cases A, simp)
7.205 +
7.206 +lemma fset_case_code [code]:
7.207 + "fset_case f A = f (member A)"
7.208 + by (cases A) simp
7.209 +
7.210 +lemma fset_rec_code [code]:
7.211 + "fset_rec f A = f (member A)"
7.212 + by (cases A) simp
7.213 +
7.214 +
7.215 +subsection {* Simplified simprules *}
7.216 +
7.217 +lemma is_empty_simp [simp]:
7.218 + "is_empty A \<longleftrightarrow> member A = {}"
7.219 + by (simp add: List_Set.is_empty_def)
7.220 +declare is_empty_def [simp del]
7.221 +
7.222 +lemma remove_simp [simp]:
7.223 + "remove x A = Fset (member A - {x})"
7.224 + by (simp add: List_Set.remove_def)
7.225 +declare remove_def [simp del]
7.226 +
7.227 +lemma filter_simp [simp]:
7.228 + "filter P A = Fset {x \<in> member A. P x}"
7.229 + by (simp add: List_Set.project_def)
7.230 +declare filter_def [simp del]
7.231 +
7.232 +lemma inter_simp [simp]:
7.233 + "inter A B = Fset (member A \<inter> member B)"
7.234 + by (simp add: inter)
7.235 +declare inter_def [simp del]
7.236 +
7.237 +declare mem_def [simp del]
7.238 +
7.239 +
7.240 +hide (open) const is_empty empty insert remove map filter forall exists card
7.241 + subfset_eq subfset inter union subtract Inter Union
7.242 +
7.243 +end
8.1 --- a/src/HOL/Library/Library.thy Sun Jun 28 22:51:29 2009 +0200
8.2 +++ b/src/HOL/Library/Library.thy Mon Jun 29 14:55:08 2009 +0200
8.3 @@ -10,7 +10,6 @@
8.4 Char_ord
8.5 Code_Char_chr
8.6 Code_Integer
8.7 - Code_Set
8.8 Coinductive_List
8.9 Commutative_Ring
8.10 Continuity
8.11 @@ -28,6 +27,7 @@
8.12 Formal_Power_Series
8.13 Fraction_Field
8.14 FrechetDeriv
8.15 + Fset
8.16 FuncSet
8.17 Fundamental_Theorem_Algebra
8.18 Infinite_Set
9.1 --- a/src/HOL/Library/List_Set.thy Sun Jun 28 22:51:29 2009 +0200
9.2 +++ b/src/HOL/Library/List_Set.thy Mon Jun 29 14:55:08 2009 +0200
9.3 @@ -70,7 +70,7 @@
9.4 by (auto simp add: remove_def remove_all_def)
9.5
9.6 lemma image_set:
9.7 - "image f (set xs) = set (remdups (map f xs))"
9.8 + "image f (set xs) = set (map f xs)"
9.9 by simp
9.10
9.11 lemma project_set:
9.12 @@ -160,4 +160,7 @@
9.13 "A \<inter> B = project (\<lambda>x. x \<in> A) B"
9.14 by (auto simp add: project_def)
9.15
9.16 +
9.17 +hide (open) const insert
9.18 +
9.19 end
9.20 \ No newline at end of file
10.1 --- a/src/HOL/MicroJava/BV/BVExample.thy Sun Jun 28 22:51:29 2009 +0200
10.2 +++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Jun 29 14:55:08 2009 +0200
10.3 @@ -1,5 +1,4 @@
10.4 (* Title: HOL/MicroJava/BV/BVExample.thy
10.5 - ID: $Id$
10.6 Author: Gerwin Klein
10.7 *)
10.8
10.9 @@ -94,7 +93,7 @@
10.10
10.11 text {* Method and field lookup: *}
10.12 lemma method_Object [simp]:
10.13 - "method (E, Object) = empty"
10.14 + "method (E, Object) = Map.empty"
10.15 by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E])
10.16
10.17 lemma method_append [simp]:
10.18 @@ -436,7 +435,7 @@
10.19 "some_elem = (%S. SOME x. x : S)"
10.20
10.21 consts_code
10.22 - "some_elem" ("hd")
10.23 + "some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)")
10.24
10.25 text {* This code setup is just a demonstration and \emph{not} sound! *}
10.26
10.27 @@ -455,7 +454,7 @@
10.28 (\<lambda>(ss, w).
10.29 let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
10.30 (ss, w)"
10.31 - unfolding iter_def is_empty_def some_elem_def ..
10.32 + unfolding iter_def List_Set.is_empty_def some_elem_def ..
10.33
10.34 lemma JVM_sup_unfold [code]:
10.35 "JVMType.sup S m n = lift2 (Opt.sup
10.36 @@ -475,7 +474,6 @@
10.37 test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0
10.38 [(Suc 0, 2, 8, Xcpt NullPointer)] append_ins"
10.39 test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins"
10.40 -
10.41 ML BV.test1
10.42 ML BV.test2
10.43
11.1 --- a/src/HOL/Tools/dseq.ML Sun Jun 28 22:51:29 2009 +0200
11.2 +++ b/src/HOL/Tools/dseq.ML Mon Jun 29 14:55:08 2009 +0200
11.3 @@ -1,5 +1,4 @@
11.4 (* Title: HOL/Tools/dseq.ML
11.5 - ID: $Id$
11.6 Author: Stefan Berghofer, TU Muenchen
11.7
11.8 Sequences with recursion depth limit.
12.1 --- a/src/HOL/Tools/inductive_codegen.ML Sun Jun 28 22:51:29 2009 +0200
12.2 +++ b/src/HOL/Tools/inductive_codegen.ML Mon Jun 29 14:55:08 2009 +0200
12.3 @@ -378,7 +378,7 @@
12.4 end
12.5 | compile_prems out_ts vs names ps gr =
12.6 let
12.7 - val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
12.8 + val vs' = distinct (op =) (flat (vs :: map term_vs out_ts));
12.9 val SOME (p, mode as SOME (Mode (_, js, _))) =
12.10 select_mode_prem thy modes' vs' ps;
12.11 val ps' = filter_out (equal p) ps;
12.12 @@ -404,7 +404,9 @@
12.13 (compile_expr thy defs dep module false modes
12.14 (mode, t) gr2)
12.15 else
12.16 - apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
12.17 + apfst (fn p => Pretty.breaks [str "DSeq.of_list", str "(case", p,
12.18 + str "of", str "Set", str "xs", str "=>", str "xs)"])
12.19 + (*this is a very strong assumption about the generated code!*)
12.20 (invoke_codegen thy defs dep module true t gr2);
12.21 val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
12.22 in
12.23 @@ -661,8 +663,10 @@
12.24 let val (call_p, gr') = mk_ind_call thy defs dep module true
12.25 s T (ts1 @ ts2') names thyname k intrs gr
12.26 in SOME ((if brack then parens else I) (Pretty.block
12.27 - [str "DSeq.list_of", Pretty.brk 1, str "(",
12.28 - conv_ntuple fs ots call_p, str ")"]), gr')
12.29 + [str "Set", Pretty.brk 1, str "(DSeq.list_of", Pretty.brk 1, str "(",
12.30 + conv_ntuple fs ots call_p, str "))"]),
12.31 + (*this is a very strong assumption about the generated code!*)
12.32 + gr')
12.33 end
12.34 else NONE
12.35 end
13.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy Sun Jun 28 22:51:29 2009 +0200
13.2 +++ b/src/HOL/ex/Codegenerator_Candidates.thy Mon Jun 29 14:55:08 2009 +0200
13.3 @@ -8,7 +8,7 @@
13.4 Complex_Main
13.5 AssocList
13.6 Binomial
13.7 - Code_Set
13.8 + Fset
13.9 Commutative_Ring
13.10 Enum
13.11 List_Prefix