src/HOL/Library/ExecutableSet.thy
author chaieb
Mon Jun 11 11:06:04 2007 +0200 (2007-06-11)
changeset 23315 df3a7e9ebadb
parent 22921 475ff421a6a3
child 23394 474ff28210c0
permissions -rw-r--r--
tuned Proof
     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
    60   [code target: List]: "member [] y \<longleftrightarrow> False"
    61   and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
    62 unfolding member_def by (induct xs) simp_all
    63 
    64 fun
    65   drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    66   "drop_first f [] = []"
    67 | "drop_first f (x#xs) = (if f x then xs else x # drop_first f xs)"
    68 declare drop_first.simps [code del]
    69 declare drop_first.simps [code target: List]
    70 
    71 declare remove1.simps [code del]
    72 lemma [code target: List]:
    73   "remove1 x xs = (if member xs x then drop_first (\<lambda>y. y = x) xs else xs)"
    74 proof (cases "member xs x")
    75   case False thus ?thesis unfolding member_def by (induct xs) auto
    76 next
    77   case True
    78   have "remove1 x xs = drop_first (\<lambda>y. y = x) xs" by (induct xs) simp_all
    79   with True show ?thesis by simp
    80 qed
    81 
    82 lemma member_nil [simp]:
    83   "member [] = (\<lambda>x. False)"
    84 proof
    85   fix x
    86   show "member [] x = False" unfolding member_def by simp
    87 qed
    88 
    89 lemma member_insertl [simp]:
    90   "x \<in> set (insertl x xs)"
    91   unfolding insertl_def member_def mem_iff by simp
    92 
    93 lemma insertl_member [simp]:
    94   fixes xs x
    95   assumes member: "member xs x"
    96   shows "insertl x xs = xs"
    97   using member unfolding insertl_def by simp
    98 
    99 lemma insertl_not_member [simp]:
   100   fixes xs x
   101   assumes member: "\<not> (member xs x)"
   102   shows "insertl x xs = x # xs"
   103   using member unfolding insertl_def by simp
   104 
   105 lemma foldr_remove1_empty [simp]:
   106   "foldr remove1 xs [] = []"
   107   by (induct xs) simp_all
   108 
   109 
   110 subsubsection {* Derived definitions *}
   111 
   112 function unionl :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   113 where
   114   "unionl [] ys = ys"
   115 | "unionl xs ys = foldr insertl xs ys"
   116 by pat_completeness auto
   117 termination by lexicographic_order
   118 
   119 lemmas unionl_def = unionl.simps(2)
   120 
   121 function intersect :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   122 where
   123   "intersect [] ys = []"
   124 | "intersect xs [] = []"
   125 | "intersect xs ys = filter (member xs) ys"
   126 by pat_completeness auto
   127 termination by lexicographic_order
   128 
   129 lemmas intersect_def = intersect.simps(3)
   130 
   131 function subtract :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   132 where
   133   "subtract [] ys = ys"
   134 | "subtract xs [] = []"
   135 | "subtract xs ys = foldr remove1 xs ys"
   136 by pat_completeness auto
   137 termination by lexicographic_order
   138 
   139 lemmas subtract_def = subtract.simps(3)
   140 
   141 function map_distinct :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   142 where
   143   "map_distinct f [] = []"
   144 | "map_distinct f xs = foldr (insertl o f) xs []"
   145 by pat_completeness auto
   146 termination by lexicographic_order
   147 
   148 lemmas map_distinct_def = map_distinct.simps(2)
   149 
   150 function unions :: "'a list list \<Rightarrow> 'a list"
   151 where
   152   "unions [] = []"
   153 | "unions xs = foldr unionl xs []"
   154 by pat_completeness auto
   155 termination by lexicographic_order
   156 
   157 lemmas unions_def = unions.simps(2)
   158 
   159 consts intersects :: "'a list list \<Rightarrow> 'a list"
   160 primrec
   161   "intersects (x#xs) = foldr intersect xs x"
   162 
   163 definition
   164   map_union :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   165   "map_union xs f = unions (map f xs)"
   166 
   167 definition
   168   map_inter :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
   169   "map_inter xs f = intersects (map f xs)"
   170 
   171 
   172 subsection {* Isomorphism proofs *}
   173 
   174 lemma iso_member:
   175   "member xs x \<longleftrightarrow> x \<in> set xs"
   176   unfolding member_def mem_iff ..
   177 
   178 lemma iso_insert:
   179   "set (insertl x xs) = insert x (set xs)"
   180   unfolding insertl_def iso_member by (simp add: Set.insert_absorb)
   181 
   182 lemma iso_remove1:
   183   assumes distnct: "distinct xs"
   184   shows "set (remove1 x xs) = set xs - {x}"
   185   using distnct set_remove1_eq by auto
   186 
   187 lemma iso_union:
   188   "set (unionl xs ys) = set xs \<union> set ys"
   189   unfolding unionl_def
   190   by (induct xs arbitrary: ys) (simp_all add: iso_insert)
   191 
   192 lemma iso_intersect:
   193   "set (intersect xs ys) = set xs \<inter> set ys"
   194   unfolding intersect_def Int_def by (simp add: Int_def iso_member) auto
   195 
   196 definition
   197   subtract' :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   198   "subtract' = flip subtract"
   199 
   200 lemma iso_subtract:
   201   fixes ys
   202   assumes distnct: "distinct ys"
   203   shows "set (subtract' ys xs) = set ys - set xs"
   204   and "distinct (subtract' ys xs)"
   205   unfolding subtract'_def flip_def subtract_def
   206   using distnct by (induct xs arbitrary: ys) auto
   207 
   208 lemma iso_map_distinct:
   209   "set (map_distinct f xs) = image f (set xs)"
   210   unfolding map_distinct_def by (induct xs) (simp_all add: iso_insert)
   211 
   212 lemma iso_unions:
   213   "set (unions xss) = \<Union> set (map set xss)"
   214 unfolding unions_def 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