src/HOL/Library/ExecutableSet.thy
author wenzelm
Thu Jun 14 23:04:39 2007 +0200 (2007-06-14)
changeset 23394 474ff28210c0
parent 22921 475ff421a6a3
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Library/ExecutableSet.thy
     2     ID:         $Id$
     3     Author:     Stefan Berghofer, TU Muenchen
     4 *)
     5 
     6 header {* Implementation of finite sets by lists *}
     7 
     8 theory ExecutableSet
     9 imports Main
    10 begin
    11 
    12 subsection {* Definitional rewrites *}
    13 
    14 instance set :: (eq) eq ..
    15 
    16 lemma [code target: Set]:
    17   "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    18   by blast
    19 
    20 lemma [code func]:
    21   "(A\<Colon>'a\<Colon>eq set) = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
    22   by blast
    23 
    24 lemma [code func]:
    25   "(A\<Colon>'a\<Colon>eq set) \<subseteq> B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
    26   unfolding subset_def ..
    27 
    28 lemma [code func]:
    29   "(A\<Colon>'a\<Colon>eq set) \<subset> B \<longleftrightarrow> A \<subseteq> B \<and> A \<noteq> B"
    30   by blast
    31 
    32 lemma [code]:
    33   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
    34   unfolding bex_triv_one_point1 ..
    35 
    36 definition
    37   filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
    38   "filter_set P xs = {x\<in>xs. P x}"
    39 
    40 lemmas [symmetric, code inline] = filter_set_def
    41 
    42 
    43 subsection {* Operations on lists *}
    44 
    45 subsubsection {* Basic definitions *}
    46 
    47 definition
    48   flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c" where
    49   "flip f a b = f b a"
    50 
    51 definition
    52   member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
    53   "member xs x \<longleftrightarrow> x \<in> set xs"
    54 
    55 definition
    56   insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    57   "insertl x xs = (if member xs x then xs else x#xs)"
    58 
    59 lemma [code target: List]: "member [] y \<longleftrightarrow> False"
    60   and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
    61   unfolding member_def by (induct xs) simp_all
    62 
    63 fun
    64   drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    65   "drop_first f [] = []"
    66 | "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
    67 declare drop_first.simps [code del]
    68 declare drop_first.simps [code target: List]
    69 
    70 declare remove1.simps [code del]
    71 lemma [code target: List]:
    72   "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
    73 proof (cases "member xs x")
    74   case False thus ?thesis unfolding member_def by (induct xs) auto
    75 next
    76   case True
    77   have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
    78   with True show ?thesis by simp
    79 qed
    80 
    81 lemma member_nil [simp]:
    82   "member [] = (\<lambda>x. False)"
    83 proof
    84   fix x
    85   show "member [] x = False" unfolding member_def by simp
    86 qed
    87 
    88 lemma member_insertl [simp]:
    89   "x \<in> set (insertl x xs)"
    90   unfolding insertl_def member_def mem_iff by simp
    91 
    92 lemma insertl_member [simp]:
    93   fixes xs x
    94   assumes member: "member xs x"
    95   shows "insertl x xs = xs"
    96   using member unfolding insertl_def by simp
    97 
    98 lemma insertl_not_member [simp]:
    99   fixes xs x
   100   assumes member: "\<not> (member xs x)"
   101   shows "insertl x xs = x # xs"
   102   using member unfolding insertl_def by simp
   103 
   104 lemma foldr_remove1_empty [simp]:
   105   "foldr remove1 xs [] = []"
   106   by (induct xs) simp_all
   107 
   108 
   109 subsubsection {* Derived definitions *}
   110 
   111 function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   112 where
   113   "unionl [] ys = ys"
   114 | "unionl xs ys = foldr insertl xs ys"
   115 by pat_completeness auto
   116 termination by lexicographic_order
   117 
   118 lemmas unionl_def = unionl.simps(2)
   119 
   120 function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   121 where
   122   "intersect [] ys = []"
   123 | "intersect xs [] = []"
   124 | "intersect xs ys = filter (member xs) ys"
   125 by pat_completeness auto
   126 termination by lexicographic_order
   127 
   128 lemmas intersect_def = intersect.simps(3)
   129 
   130 function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   131 where
   132   "subtract [] ys = ys"
   133 | "subtract xs [] = []"
   134 | "subtract xs ys = foldr remove1 xs ys"
   135 by pat_completeness auto
   136 termination by lexicographic_order
   137 
   138 lemmas subtract_def = subtract.simps(3)
   139 
   140 function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   141 where
   142   "map_distinct f [] = []"
   143 | "map_distinct f xs = foldr (insertl o f) xs []"
   144 by pat_completeness auto
   145 termination by lexicographic_order
   146 
   147 lemmas map_distinct_def = map_distinct.simps(2)
   148 
   149 function unions :: "'a list list \<Rightarrow> 'a list"
   150 where
   151   "unions [] = []"
   152 | "unions xs = foldr unionl xs []"
   153 by pat_completeness auto
   154 termination by lexicographic_order
   155 
   156 lemmas unions_def = unions.simps(2)
   157 
   158 consts intersects :: "'a list list \<Rightarrow> 'a list"
   159 primrec
   160   "intersects (x#xs) = foldr intersect xs x"
   161 
   162 definition
   163   map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   164   "map_union xs f = unions (map f xs)"
   165 
   166 definition
   167   map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   168   "map_inter xs f = intersects (map f xs)"
   169 
   170 
   171 subsection {* Isomorphism proofs *}
   172 
   173 lemma iso_member:
   174   "member xs x \<longleftrightarrow> x \<in> set xs"
   175   unfolding member_def mem_iff ..
   176 
   177 lemma iso_insert:
   178   "set (insertl x xs) = insert x (set xs)"
   179   unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
   180 
   181 lemma iso_remove1:
   182   assumes distnct: "distinct xs"
   183   shows "set (remove1 x xs) = set xs - {x}"
   184   using distnct set_remove1_eq by auto
   185 
   186 lemma iso_union:
   187   "set (unionl xs ys) = set xs \<union> set ys"
   188   unfolding unionl_def
   189   by (induct xs arbitrary: ys) (simp_all add: iso_insert)
   190 
   191 lemma iso_intersect:
   192   "set (intersect xs ys) = set xs \<inter> set ys"
   193   unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
   194 
   195 definition
   196   subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   197   "subtract' = flip subtract"
   198 
   199 lemma iso_subtract:
   200   fixes ys
   201   assumes distnct: "distinct ys"
   202   shows "set (subtract' ys xs) = set ys - set xs"
   203     and "distinct (subtract' ys xs)"
   204   unfolding subtract'_def flip_def subtract_def
   205   using distnct by (induct xs arbitrary: ys) auto
   206 
   207 lemma iso_map_distinct:
   208   "set (map_distinct f xs) = image f (set xs)"
   209   unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
   210 
   211 lemma iso_unions:
   212   "set (unions xss) = \<Union> set (map set xss)"
   213   unfolding unions_def
   214 proof (induct xss)
   215   case Nil show ?case by simp
   216 next
   217   case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)
   218 qed
   219 
   220 lemma iso_intersects:
   221   "set (intersects (xs#xss)) = \<Inter> set (map set (xs#xss))"
   222   by (induct xss) (simp_all add: Int_def iso_member, auto)
   223 
   224 lemma iso_UNION:
   225   "set (map_union xs f) = UNION (set xs) (set o f)"
   226   unfolding map_union_def iso_unions by simp
   227 
   228 lemma iso_INTER:
   229   "set (map_inter (x#xs) f) = INTER (set (x#xs)) (set o f)"
   230   unfolding map_inter_def iso_intersects by (induct xs) (simp_all add: iso_member, auto)
   231 
   232 definition
   233   Blall :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   234   "Blall = flip list_all"
   235 definition
   236   Blex :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   237   "Blex = flip list_ex"
   238 
   239 lemma iso_Ball:
   240   "Blall xs f = Ball (set xs) f"
   241   unfolding Blall_def flip_def by (induct xs) simp_all
   242 
   243 lemma iso_Bex:
   244   "Blex xs f = Bex (set xs) f"
   245   unfolding Blex_def flip_def by (induct xs) simp_all
   246 
   247 lemma iso_filter:
   248   "set (filter P xs) = filter_set P (set xs)"
   249   unfolding filter_set_def by (induct xs) auto
   250 
   251 subsection {* code generator setup *}
   252 
   253 ML {*
   254 nonfix inter;
   255 nonfix union;
   256 nonfix subset;
   257 *}
   258 
   259 code_modulename SML
   260   ExecutableSet List
   261   Set List
   262 
   263 code_modulename OCaml
   264   ExecutableSet List
   265   Set List
   266 
   267 code_modulename Haskell
   268   ExecutableSet List
   269   Set List
   270 
   271 definition [code inline]:
   272   "empty_list = []"
   273 
   274 lemma [code func]:
   275   "insert (x \<Colon> 'a\<Colon>eq) = insert x" ..
   276 
   277 lemma [code func]:
   278   "(xs \<Colon> 'a\<Colon>eq set) \<union> ys = xs \<union> ys" ..
   279 
   280 lemma [code func]:
   281   "(xs \<Colon> 'a\<Colon>eq set) \<inter> ys = xs \<inter> ys" ..
   282 
   283 lemma [code func]:
   284   "(op -) (xs \<Colon> 'a\<Colon>eq set) = (op -) (xs \<Colon> 'a\<Colon>eq set)" ..
   285 
   286 lemma [code func]:
   287   "image (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq) = image f" ..
   288 
   289 lemma [code func]:
   290   "Union (xss \<Colon> 'a\<Colon>eq set set) = Union xss" ..
   291 
   292 lemma [code func]:
   293   "Inter (xss \<Colon> 'a\<Colon>eq set set) = Inter xss" ..
   294 
   295 lemma [code func]:
   296   "UNION xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = UNION xs f" ..
   297 
   298 lemma [code func]:
   299   "INTER xs (f \<Colon> 'a \<Rightarrow> 'b\<Colon>eq set) = INTER xs f" ..
   300 
   301 lemma [code func]:
   302   "Ball (xs \<Colon> 'a\<Colon>type set) = Ball xs" ..
   303 
   304 lemma [code func]:
   305   "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
   306 
   307 lemma [code func]:
   308   "filter_set P (xs \<Colon> 'a\<Colon>type set) = filter_set P xs" ..
   309 
   310 
   311 code_abstype "'a set" "'a list" where
   312   "{}" \<equiv> empty_list
   313   insert \<equiv> insertl
   314   "op \<union>" \<equiv> unionl
   315   "op \<inter>" \<equiv> intersect
   316   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" \<equiv> subtract'
   317   image \<equiv> map_distinct
   318   Union \<equiv> unions
   319   Inter \<equiv> intersects
   320   UNION \<equiv> map_union
   321   INTER \<equiv> map_inter
   322   Ball \<equiv> Blall
   323   Bex \<equiv> Blex
   324   filter_set \<equiv> filter
   325 
   326 
   327 subsubsection {* type serializations *}
   328 
   329 types_code
   330   set ("_ list")
   331 attach (term_of) {*
   332 fun term_of_set f T [] = Const ("{}", Type ("set", [T]))
   333   | term_of_set f T (x :: xs) = Const ("insert",
   334       T --> Type ("set", [T]) --> Type ("set", [T])) $ f x $ term_of_set f T xs;
   335 *}
   336 attach (test) {*
   337 fun gen_set' aG i j = frequency
   338   [(i, fn () => aG j :: gen_set' aG (i-1) j), (1, fn () => [])] ()
   339 and gen_set aG i = gen_set' aG i i;
   340 *}
   341 
   342 
   343 subsubsection {* const serializations *}
   344 
   345 consts_code
   346   "{}" ("{*[]*}")
   347   insert ("{*insertl*}")
   348   "op \<union>" ("{*unionl*}")
   349   "op \<inter>" ("{*intersect*}")
   350   "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
   351   image ("{*map_distinct*}")
   352   Union ("{*unions*}")
   353   Inter ("{*intersects*}")
   354   UNION ("{*map_union*}")
   355   INTER ("{*map_inter*}")
   356   Ball ("{*Blall*}")
   357   Bex ("{*Blex*}")
   358   filter_set ("{*filter*}")
   359 
   360 end