src/HOL/Library/Executable_Set.thy
author nipkow
Mon Dec 15 10:16:38 2008 +0100 (2008-12-15)
changeset 29110 476c46e99ada
parent 29107 e70b9c2bee14
child 30304 d8e4cd2ac2a1
permissions -rw-r--r--
flipped fold implementation
     1 (*  Title:      HOL/Library/Executable_Set.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 *)
     5 
     6 header {* Implementation of finite sets by lists *}
     7 
     8 theory Executable_Set
     9 imports Plain "~~/src/HOL/List"
    10 begin
    11 
    12 subsection {* Definitional rewrites *}
    13 
    14 definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    15   "subset = op \<le>"
    16 
    17 declare subset_def [symmetric, code unfold]
    18 
    19 lemma [code]: "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    20   unfolding subset_def subset_eq ..
    21 
    22 definition is_empty :: "'a set \<Rightarrow> bool" where
    23   "is_empty A \<longleftrightarrow> A = {}"
    24 
    25 definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
    26   [code del]: "eq_set = op ="
    27 
    28 lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    29   unfolding eq_set_def by auto
    30 
    31 (* FIXME allow for Stefan's code generator:
    32 declare set_eq_subset[code unfold]
    33 *)
    34 
    35 lemma [code]:
    36   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    37   unfolding bex_triv_one_point1 ..
    38 
    39 definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    40   "filter_set P xs = {x\<in>xs. P x}"
    41 
    42 declare filter_set_def[symmetric, code unfold] 
    43 
    44 
    45 subsection {* Operations on lists *}
    46 
    47 subsubsection {* Basic definitions *}
    48 
    49 definition
    50   flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    51   "flip f a b = f b a"
    52 
    53 definition
    54   member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
    55   "member xs x \<longleftrightarrow> x \<in> set xs"
    56 
    57 definition
    58   insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    59   "insertl x xs = (if member xs x then xs else x#xs)"
    60 
    61 lemma [code target: List]: "member [] y \<longleftrightarrow> False"
    62   and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
    63   unfolding member_def by (induct xs) simp_all
    64 
    65 fun
    66   drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    67   "drop_first f [] = []"
    68 | "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
    69 declare drop_first.simps [code del]
    70 declare drop_first.simps [code target: List]
    71 
    72 declare remove1.simps [code del]
    73 lemma [code target: List]:
    74   "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
    75 proof (cases "member xs x")
    76   case False thus ?thesis unfolding member_def by (induct xs) auto
    77 next
    78   case True
    79   have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
    80   with True show ?thesis by simp
    81 qed
    82 
    83 lemma member_nil [simp]:
    84   "member [] = (\<lambda>x. False)"
    85 proof (rule ext)
    86   fix x
    87   show "member [] x = False" unfolding member_def by simp
    88 qed
    89 
    90 lemma member_insertl [simp]:
    91   "x \<in> set (insertl x xs)"
    92   unfolding insertl_def member_def mem_iff by simp
    93 
    94 lemma insertl_member [simp]:
    95   fixes xs x
    96   assumes member: "member xs x"
    97   shows "insertl x xs = xs"
    98   using member unfolding insertl_def by simp
    99 
   100 lemma insertl_not_member [simp]:
   101   fixes xs x
   102   assumes member: "\<not> (member xs x)"
   103   shows "insertl x xs = x # xs"
   104   using member unfolding insertl_def by simp
   105 
   106 lemma foldr_remove1_empty [simp]:
   107   "foldr remove1 xs [] = []"
   108   by (induct xs) simp_all
   109 
   110 
   111 subsubsection {* Derived definitions *}
   112 
   113 function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   114 where
   115   "unionl [] ys = ys"
   116 | "unionl xs ys = foldr insertl xs ys"
   117 by pat_completeness auto
   118 termination by lexicographic_order
   119 
   120 lemmas unionl_eq = unionl.simps(2)
   121 
   122 function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   123 where
   124   "intersect [] ys = []"
   125 | "intersect xs [] = []"
   126 | "intersect xs ys = filter (member xs) ys"
   127 by pat_completeness auto
   128 termination by lexicographic_order
   129 
   130 lemmas intersect_eq = intersect.simps(3)
   131 
   132 function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   133 where
   134   "subtract [] ys = ys"
   135 | "subtract xs [] = []"
   136 | "subtract xs ys = foldr remove1 xs ys"
   137 by pat_completeness auto
   138 termination by lexicographic_order
   139 
   140 lemmas subtract_eq = subtract.simps(3)
   141 
   142 function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   143 where
   144   "map_distinct f [] = []"
   145 | "map_distinct f xs = foldr (insertl o f) xs []"
   146 by pat_completeness auto
   147 termination by lexicographic_order
   148 
   149 lemmas map_distinct_eq = map_distinct.simps(2)
   150 
   151 function unions :: "'a list list \<Rightarrow> 'a list"
   152 where
   153   "unions [] = []"
   154 | "unions xs = foldr unionl xs []"
   155 by pat_completeness auto
   156 termination by lexicographic_order
   157 
   158 lemmas unions_eq = unions.simps(2)
   159 
   160 consts intersects :: "'a list list \<Rightarrow> 'a list"
   161 primrec
   162   "intersects (x#xs) = foldr intersect xs x"
   163 
   164 definition
   165   map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   166   "map_union xs f = unions (map f xs)"
   167 
   168 definition
   169   map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   170   "map_inter xs f = intersects (map f xs)"
   171 
   172 
   173 subsection {* Isomorphism proofs *}
   174 
   175 lemma iso_member:
   176   "member xs x \<longleftrightarrow> x \<in> set xs"
   177   unfolding member_def mem_iff ..
   178 
   179 lemma iso_insert:
   180   "set (insertl x xs) = insert x (set xs)"
   181   unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
   182 
   183 lemma iso_remove1:
   184   assumes distnct: "distinct xs"
   185   shows "set (remove1 x xs) = set xs - {x}"
   186   using distnct set_remove1_eq by auto
   187 
   188 lemma iso_union:
   189   "set (unionl xs ys) = set xs \<union> set ys"
   190   unfolding unionl_eq
   191   by (induct xs arbitrary: ys) (simp_all add: iso_insert)
   192 
   193 lemma iso_intersect:
   194   "set (intersect xs ys) = set xs \<inter> set ys"
   195   unfolding intersect_eq Int_def by (simp add: Int_def iso_member) auto
   196 
   197 definition
   198   subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   199   "subtract' = flip subtract"
   200 
   201 lemma iso_subtract:
   202   fixes ys
   203   assumes distnct: "distinct ys"
   204   shows "set (subtract' ys xs) = set ys - set xs"
   205     and "distinct (subtract' ys xs)"
   206   unfolding subtract'_def flip_def subtract_eq
   207   using distnct by (induct xs arbitrary: ys) auto
   208 
   209 lemma iso_map_distinct:
   210   "set (map_distinct f xs) = image f (set xs)"
   211   unfolding map_distinct_eq by (induct xs) (simp_all add: iso_insert)
   212 
   213 lemma iso_unions:
   214   "set (unions xss) = \<Union> set (map set xss)"
   215   unfolding unions_eq
   216 proof (induct xss)
   217   case Nil show ?case by simp
   218 next
   219   case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
   220 qed
   221 
   222 lemma iso_intersects:
   223   "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
   224   by (induct xss) (simp_all add: Int_def iso_member, auto)
   225 
   226 lemma iso_UNION:
   227   "set (map_union xs f) = UNION (set xs) (set o f)"
   228   unfolding map_union_def iso_unions by simp
   229 
   230 lemma iso_INTER:
   231   "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
   232   unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
   233 
   234 definition
   235   Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   236   "Blall = flip list_all"
   237 definition
   238   Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   239   "Blex = flip list_ex"
   240 
   241 lemma iso_Ball:
   242   "Blall xs f = Ball (set xs) f"
   243   unfolding Blall_def flip_def by (induct xs) simp_all
   244 
   245 lemma iso_Bex:
   246   "Blex xs f = Bex (set xs) f"
   247   unfolding Blex_def flip_def by (induct xs) simp_all
   248 
   249 lemma iso_filter:
   250   "set (filter P xs) = filter_set P (set xs)"
   251   unfolding filter_set_def by (induct xs) auto
   252 
   253 subsection {* code generator setup *}
   254 
   255 ML {*
   256 nonfix inter;
   257 nonfix union;
   258 nonfix subset;
   259 *}
   260 
   261 subsubsection {* const serializations *}
   262 
   263 consts_code
   264   "{}" ("{*[]*}")
   265   insert ("{*insertl*}")
   266   is_empty ("{*null*}")
   267   "op \<union>" ("{*unionl*}")
   268   "op \<inter>" ("{*intersect*}")
   269   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
   270   image ("{*map_distinct*}")
   271   Union ("{*unions*}")
   272   Inter ("{*intersects*}")
   273   UNION ("{*map_union*}")
   274   INTER ("{*map_inter*}")
   275   Ball ("{*Blall*}")
   276   Bex ("{*Blex*}")
   277   filter_set ("{*filter*}")
   278   fold ("{* foldl o flip *}")
   279 
   280 end