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