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
```