summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Library/ExecutableSet.thy

author | haftmann |

Mon, 18 Dec 2006 08:21:31 +0100 | |

changeset 21875 | 5df10a17644e |

parent 21572 | 7442833ea2b6 |

child 21911 | e29bcab0c81c |

permissions | -rw-r--r-- |

explicit nonfix declaration for ML "subset"

(* Title: HOL/Library/ExecutableSet.thy ID: $Id$ Author: Stefan Berghofer, TU Muenchen *) header {* Implementation of finite sets by lists *} theory ExecutableSet imports Main begin section {* Definitional rewrites *} instance set :: (eq) eq .. definition minus_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" where "minus_set xs ys = ys - xs" lemma [code inline]: "op - = (\<lambda>xs ys. minus_set ys xs)" unfolding minus_set_def .. definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where "subset = op \<subseteq>" lemmas [symmetric, code inline] = subset_def definition strict_subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where "strict_subset = op \<subset>" lemmas [symmetric, code inline] = strict_subset_def lemma [code target: Set]: "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" by blast lemma [code func]: "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" by blast lemma [code func]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)" unfolding subset_def Set.subset_def .. lemma [code func]: "strict_subset A B \<longleftrightarrow> subset A B \<and> A \<noteq> B" unfolding subset_def strict_subset_def by blast 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}" lemmas [symmetric, code inline] = filter_set_def section {* Operations on lists *} subsection {* 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 = (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 = False" and [code target: List]: "member (x#xs) y = (y = x \<or> member xs y)" unfolding member_def by (induct xs) simp_all consts drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" primrec "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] 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 fix x show "member [] x = False" unfolding member_def by simp qed 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 subsection {* 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_def = 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_def = 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 lemmas subtract_def = 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_def = 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_def = 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)" section {* Isomorphism proofs *} lemma iso_member: "member xs x = (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: Set.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_def by (induct xs arbitrary: ys) (simp_all add: iso_insert) lemma iso_intersect: "set (intersect xs ys) = set xs \<inter> set ys" unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto lemma iso_subtract: fixes ys assumes distnct: "distinct ys" shows "set (subtract xs ys) = minus_set (set xs) (set ys)" and "distinct (subtract xs ys)" unfolding subtract_def minus_set_def using distnct by (induct xs arbitrary: ys) auto lemma iso_map_distinct: "set (map_distinct f xs) = image f (set xs)" unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert) lemma iso_unions: "set (unions xss) = \<Union> set (map set xss)" unfolding unions_def 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 section {* code generator setup *} ML {* nonfix inter; nonfix union; nonfix subset; *} code_modulename SML ExecutableSet List Set List code_modulename Haskell ExecutableSet List Set List definition [code inline]: "empty_list = []" lemma [code func]: "insert (x \<Colon> 'a\<Colon>eq) = insert x" .. lemma [code func]: "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" .. lemma [code func]: "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" .. lemma [code func]: "minus_set xs = minus_set (xs \<Colon> 'a\<Colon>eq set)" .. lemma [code func]: "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" .. lemma [code func]: "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" .. lemma [code func]: "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" .. lemma [code func]: "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" .. lemma [code func]: "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" .. lemma [code func]: "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" .. code_abstype "'a set" "'a list" where "{}" \<equiv> empty_list insert \<equiv> insertl "op \<union>" \<equiv> unionl "op \<inter>" \<equiv> intersect minus_set \<equiv> subtract image \<equiv> map_distinct Union \<equiv> unions Inter \<equiv> intersects UNION \<equiv> map_union INTER \<equiv> map_inter Ball \<equiv> Blall Bex \<equiv> Blex filter_set \<equiv> filter code_gen "{}" insert "op \<union>" "op \<inter>" minus_set image Union Inter UNION INTER Ball Bex filter_set (SML -) subsection {* type serializations *} types_code set ("_ list") attach (term_of) {* fun term_of_set f T [] = Const ("{}", Type ("set", [T])) | term_of_set f T (x :: xs) = Const ("insert", T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs; *} attach (test) {* fun gen_set' aG i j = frequency [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] () and gen_set aG i = gen_set' aG i i; *} subsection {* const serializations *} consts_code "{}" ("[]") "insert" ("{*insertl*}") "op Un" ("{*unionl*}") "op Int" ("{*intersect*}") "HOL.minus" :: "'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*}") end