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