src/HOL/List.thy
 author haftmann Sat Jun 15 17:19:23 2013 +0200 (2013-06-15) changeset 52379 7f864f2219a9 parent 52148 893b15200ec1 child 52380 3cc46b8cca5e permissions -rw-r--r--
selection operator smallest_prime_beyond
 wenzelm@13462  1 (* Title: HOL/List.thy  wenzelm@13462  2  Author: Tobias Nipkow  clasohm@923  3 *)  clasohm@923  4 wenzelm@13114  5 header {* The datatype of finite lists *}  wenzelm@13122  6 nipkow@15131  7 theory List  haftmann@51112  8 imports Presburger Code_Numeral Quotient ATP  nipkow@15131  9 begin  clasohm@923  10 wenzelm@13142  11 datatype 'a list =  wenzelm@13366  12  Nil ("[]")  wenzelm@13366  13  | Cons 'a "'a list" (infixr "#" 65)  clasohm@923  14 haftmann@34941  15 syntax  haftmann@34941  16  -- {* list Enumeration *}  wenzelm@35115  17  "_list" :: "args => 'a list" ("[(_)]")  haftmann@34941  18 haftmann@34941  19 translations  haftmann@34941  20  "[x, xs]" == "x#[xs]"  haftmann@34941  21  "[x]" == "x#[]"  haftmann@34941  22 wenzelm@35115  23 wenzelm@35115  24 subsection {* Basic list processing functions *}  nipkow@15302  25 nipkow@50548  26 primrec hd :: "'a list \ 'a" where  nipkow@50548  27 "hd (x # xs) = x"  nipkow@50548  28 nipkow@50548  29 primrec tl :: "'a list \ 'a list" where  nipkow@50548  30 "tl [] = []" |  nipkow@50548  31 "tl (x # xs) = xs"  nipkow@50548  32 nipkow@50548  33 primrec last :: "'a list \ 'a" where  nipkow@50548  34 "last (x # xs) = (if xs = [] then x else last xs)"  nipkow@50548  35 nipkow@50548  36 primrec butlast :: "'a list \ 'a list" where  nipkow@50548  37 "butlast []= []" |  nipkow@50548  38 "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"  nipkow@50548  39 nipkow@50548  40 primrec set :: "'a list \ 'a set" where  nipkow@50548  41 "set [] = {}" |  nipkow@50548  42 "set (x # xs) = insert x (set xs)"  nipkow@50548  43 nipkow@50548  44 definition coset :: "'a list \ 'a set" where  nipkow@50548  45 [simp]: "coset xs = - set xs"  nipkow@50548  46 nipkow@50548  47 primrec map :: "('a \ 'b) \ 'a list \ 'b list" where  nipkow@50548  48 "map f [] = []" |  nipkow@50548  49 "map f (x # xs) = f x # map f xs"  nipkow@50548  50 nipkow@50548  51 primrec append :: "'a list \ 'a list \ 'a list" (infixr "@" 65) where  nipkow@50548  52 append_Nil: "[] @ ys = ys" |  nipkow@50548  53 append_Cons: "(x#xs) @ ys = x # xs @ ys"  nipkow@50548  54 nipkow@50548  55 primrec rev :: "'a list \ 'a list" where  nipkow@50548  56 "rev [] = []" |  nipkow@50548  57 "rev (x # xs) = rev xs @ [x]"  nipkow@50548  58 nipkow@50548  59 primrec filter:: "('a \ bool) \ 'a list \ 'a list" where  nipkow@50548  60 "filter P [] = []" |  nipkow@50548  61 "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"  haftmann@34941  62 haftmann@34941  63 syntax  haftmann@34941  64  -- {* Special syntax for filter *}  wenzelm@35115  65  "_filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")  haftmann@34941  66 haftmann@34941  67 translations  haftmann@34941  68  "[x<-xs . P]"== "CONST filter (%x. P) xs"  haftmann@34941  69 haftmann@34941  70 syntax (xsymbols)  wenzelm@35115  71  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])")  haftmann@34941  72 syntax (HTML output)  wenzelm@35115  73  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])")  haftmann@34941  74 nipkow@50548  75 primrec fold :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b" where  nipkow@50548  76 fold_Nil: "fold f [] = id" |  nipkow@50548  77 fold_Cons: "fold f (x # xs) = fold f xs \ f x"  nipkow@50548  78 nipkow@50548  79 primrec foldr :: "('a \ 'b \ 'b) \ 'a list \ 'b \ 'b" where  nipkow@50548  80 foldr_Nil: "foldr f [] = id" |  nipkow@50548  81 foldr_Cons: "foldr f (x # xs) = f x \ foldr f xs"  nipkow@50548  82 nipkow@50548  83 primrec foldl :: "('b \ 'a \ 'b) \ 'b \ 'a list \ 'b" where  nipkow@50548  84 foldl_Nil: "foldl f a [] = a" |  nipkow@50548  85 foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"  nipkow@50548  86 nipkow@50548  87 primrec concat:: "'a list list \ 'a list" where  nipkow@50548  88 "concat [] = []" |  nipkow@50548  89 "concat (x # xs) = x @ concat xs"  nipkow@50548  90 nipkow@50548  91 definition (in monoid_add) listsum :: "'a list \ 'a" where  nipkow@50548  92 "listsum xs = foldr plus xs 0"  nipkow@50548  93 nipkow@50548  94 primrec drop:: "nat \ 'a list \ 'a list" where  nipkow@50548  95 drop_Nil: "drop n [] = []" |  nipkow@50548  96 drop_Cons: "drop n (x # xs) = (case n of 0 \ x # xs | Suc m \ drop m xs)"  haftmann@34941  97  -- {*Warning: simpset does not contain this definition, but separate  haftmann@34941  98  theorems for @{text "n = 0"} and @{text "n = Suc k"} *}  haftmann@34941  99 nipkow@50548  100 primrec take:: "nat \ 'a list \ 'a list" where  nipkow@50548  101 take_Nil:"take n [] = []" |  nipkow@50548  102 take_Cons: "take n (x # xs) = (case n of 0 \ [] | Suc m \ x # take m xs)"  haftmann@34941  103  -- {*Warning: simpset does not contain this definition, but separate  haftmann@34941  104  theorems for @{text "n = 0"} and @{text "n = Suc k"} *}  haftmann@34941  105 nipkow@50548  106 primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where  nipkow@50548  107 nth_Cons: "(x # xs) ! n = (case n of 0 \ x | Suc k \ xs ! k)"  haftmann@34941  108  -- {*Warning: simpset does not contain this definition, but separate  haftmann@34941  109  theorems for @{text "n = 0"} and @{text "n = Suc k"} *}  haftmann@34941  110 nipkow@50548  111 primrec list_update :: "'a list \ nat \ 'a \ 'a list" where  nipkow@50548  112 "list_update [] i v = []" |  nipkow@50548  113 "list_update (x # xs) i v =  nipkow@50548  114  (case i of 0 \ v # xs | Suc j \ x # list_update xs j v)"  clasohm@923  115 wenzelm@41229  116 nonterminal lupdbinds and lupdbind  nipkow@5077  117 clasohm@923  118 syntax  wenzelm@13366  119  "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")  wenzelm@13366  120  "" :: "lupdbind => lupdbinds" ("_")  wenzelm@13366  121  "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")  wenzelm@13366  122  "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)  nipkow@5077  123 clasohm@923  124 translations  wenzelm@35115  125  "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"  haftmann@34941  126  "xs[i:=x]" == "CONST list_update xs i x"  haftmann@34941  127 nipkow@50548  128 primrec takeWhile :: "('a \ bool) \ 'a list \ 'a list" where  nipkow@50548  129 "takeWhile P [] = []" |  nipkow@50548  130 "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"  nipkow@50548  131 nipkow@50548  132 primrec dropWhile :: "('a \ bool) \ 'a list \ 'a list" where  nipkow@50548  133 "dropWhile P [] = []" |  nipkow@50548  134 "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"  nipkow@50548  135 nipkow@50548  136 primrec zip :: "'a list \ 'b list \ ('a \ 'b) list" where  nipkow@50548  137 "zip xs [] = []" |  nipkow@50548  138 zip_Cons: "zip xs (y # ys) =  nipkow@50548  139  (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"  haftmann@34941  140  -- {*Warning: simpset does not contain this definition, but separate  haftmann@34941  141  theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}  haftmann@34941  142 nipkow@50548  143 primrec product :: "'a list \ 'b list \ ('a \ 'b) list" where  nipkow@50548  144 "product [] _ = []" |  nipkow@50548  145 "product (x#xs) ys = map (Pair x) ys @ product xs ys"  haftmann@49948  146 haftmann@49948  147 hide_const (open) product  haftmann@49948  148 nipkow@50548  149 primrec upt :: "nat \ nat \ nat list" ("(1[_.. 'a list \ 'a list" where  nipkow@50548  154 "insert x xs = (if x \ set xs then xs else x # xs)"  haftmann@34978  155 wenzelm@36176  156 hide_const (open) insert  wenzelm@36176  157 hide_fact (open) insert_def  haftmann@34978  158 nipkow@47122  159 primrec find :: "('a \ bool) \ 'a list \ 'a option" where  nipkow@50548  160 "find _ [] = None" |  nipkow@50548  161 "find P (x#xs) = (if P x then Some x else find P xs)"  nipkow@47122  162 nipkow@47122  163 hide_const (open) find  nipkow@47122  164 haftmann@51096  165 primrec those :: "'a option list \ 'a list option"  haftmann@51096  166 where  haftmann@51096  167 "those [] = Some []" |  haftmann@51096  168 "those (x # xs) = (case x of  haftmann@51096  169  None \ None  haftmann@51096  170 | Some y \ Option.map (Cons y) (those xs))"  haftmann@51096  171 nipkow@50548  172 primrec remove1 :: "'a \ 'a list \ 'a list" where  nipkow@50548  173 "remove1 x [] = []" |  nipkow@50548  174 "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"  nipkow@50548  175 nipkow@50548  176 primrec removeAll :: "'a \ 'a list \ 'a list" where  nipkow@50548  177 "removeAll x [] = []" |  nipkow@50548  178 "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"  nipkow@50548  179 nipkow@50548  180 primrec distinct :: "'a list \ bool" where  nipkow@50548  181 "distinct [] \ True" |  nipkow@50548  182 "distinct (x # xs) \ x \ set xs \ distinct xs"  nipkow@50548  183 nipkow@50548  184 primrec remdups :: "'a list \ 'a list" where  nipkow@50548  185 "remdups [] = []" |  nipkow@50548  186 "remdups (x # xs) = (if x \ set xs then remdups xs else x # remdups xs)"  nipkow@50548  187 nipkow@50548  188 primrec replicate :: "nat \ 'a \ 'a list" where  nipkow@50548  189 replicate_0: "replicate 0 x = []" |  nipkow@50548  190 replicate_Suc: "replicate (Suc n) x = x # replicate n x"  paulson@3342  191 wenzelm@13142  192 text {*  wenzelm@14589  193  Function @{text size} is overloaded for all datatypes. Users may  wenzelm@13366  194  refer to the list version as @{text length}. *}  wenzelm@13142  195 nipkow@50548  196 abbreviation length :: "'a list \ nat" where  nipkow@50548  197 "length \ size"  paulson@15307  198 haftmann@51173  199 definition enumerate :: "nat \ 'a list \ (nat \ 'a) list" where  haftmann@51173  200 enumerate_eq_zip: "enumerate n xs = zip [n.. 'a list" where  nipkow@50548  203 "rotate1 [] = []" |  nipkow@50548  204 "rotate1 (x # xs) = xs @ [x]"  nipkow@50548  205 nipkow@50548  206 definition rotate :: "nat \ 'a list \ 'a list" where  nipkow@50548  207 "rotate n = rotate1 ^^ n"  nipkow@50548  208 nipkow@50548  209 definition list_all2 :: "('a \ 'b \ bool) \ 'a list \ 'b list \ bool" where  nipkow@50548  210 "list_all2 P xs ys =  nipkow@50548  211  (length xs = length ys \ (\(x, y) \ set (zip xs ys). P x y))"  nipkow@50548  212 nipkow@50548  213 definition sublist :: "'a list => nat set => 'a list" where  nipkow@50548  214 "sublist xs A = map fst (filter (\p. snd p \ A) (zip xs [0.. 'a list list" where  nipkow@50548  217 "sublists [] = [[]]" |  nipkow@50548  218 "sublists (x#xs) = (let xss = sublists xs in map (Cons x) xss @ xss)"  nipkow@50548  219 nipkow@50548  220 primrec n_lists :: "nat \ 'a list \ 'a list list" where  nipkow@50548  221 "n_lists 0 xs = [[]]" |  nipkow@50548  222 "n_lists (Suc n) xs = concat (map (\ys. map (\y. y # ys) xs) (n_lists n xs))"  haftmann@49948  223 haftmann@49948  224 hide_const (open) n_lists  haftmann@49948  225 nipkow@40593  226 fun splice :: "'a list \ 'a list \ 'a list" where  nipkow@40593  227 "splice [] ys = ys" |  nipkow@40593  228 "splice xs [] = xs" |  nipkow@40593  229 "splice (x#xs) (y#ys) = x # y # splice xs ys"  haftmann@21061  230 nipkow@26771  231 text{*  nipkow@26771  232 \begin{figure}[htbp]  nipkow@26771  233 \fbox{  nipkow@26771  234 \begin{tabular}{l}  wenzelm@27381  235 @{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\  wenzelm@27381  236 @{lemma "length [a,b,c] = 3" by simp}\\  wenzelm@27381  237 @{lemma "set [a,b,c] = {a,b,c}" by simp}\\  wenzelm@27381  238 @{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\  wenzelm@27381  239 @{lemma "rev [a,b,c] = [c,b,a]" by simp}\\  wenzelm@27381  240 @{lemma "hd [a,b,c,d] = a" by simp}\\  wenzelm@27381  241 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\  wenzelm@27381  242 @{lemma "last [a,b,c,d] = d" by simp}\\  wenzelm@27381  243 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\  wenzelm@27381  244 @{lemma[source] "filter (\n::nat. n<2) [0,2,1] = [0,1]" by simp}\\  wenzelm@27381  245 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\  haftmann@46133  246 @{lemma "fold f [a,b,c] x = f c (f b (f a x))" by simp}\\  haftmann@47397  247 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\  haftmann@47397  248 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\  wenzelm@27381  249 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\  wenzelm@27381  250 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\  haftmann@51173  251 @{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\  haftmann@49948  252 @{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\  wenzelm@27381  253 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\  wenzelm@27381  254 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\  wenzelm@27381  255 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\  wenzelm@27381  256 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\  wenzelm@27381  257 @{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\  wenzelm@27381  258 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\  wenzelm@27381  259 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\  wenzelm@27381  260 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\  wenzelm@27381  261 @{lemma "distinct [2,0,1::nat]" by simp}\\  wenzelm@27381  262 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\  haftmann@34978  263 @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\  haftmann@35295  264 @{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\  nipkow@47122  265 @{lemma "List.find (%i::int. i>0) [0,0] = None" by simp}\\  nipkow@47122  266 @{lemma "List.find (%i::int. i>0) [0,1,0,2] = Some 1" by simp}\\  wenzelm@27381  267 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\  nipkow@27693  268 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\  wenzelm@27381  269 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\  wenzelm@27381  270 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\  wenzelm@27381  271 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\  haftmann@49948  272 @{lemma "sublists [a,b] = [[a, b], [a], [b], []]" by simp}\\  haftmann@49948  273 @{lemma "List.n_lists 2 [a,b,c] = [[a, a], [b, a], [c, a], [a, b], [b, b], [c, b], [a, c], [b, c], [c, c]]" by (simp add: eval_nat_numeral)}\\  blanchet@46440  274 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by simp}\\  blanchet@46440  275 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate_def eval_nat_numeral)}\\  nipkow@40077  276 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:eval_nat_numeral)}\\  nipkow@40077  277 @{lemma "[2..<5] = [2,3,4]" by (simp add:eval_nat_numeral)}\\  haftmann@47397  278 @{lemma "listsum [1,2,3::nat] = 6" by (simp add: listsum_def)}  nipkow@26771  279 \end{tabular}}  nipkow@26771  280 \caption{Characteristic examples}  nipkow@26771  281 \label{fig:Characteristic}  nipkow@26771  282 \end{figure}  blanchet@29927  283 Figure~\ref{fig:Characteristic} shows characteristic examples  nipkow@26771  284 that should give an intuitive understanding of the above functions.  nipkow@26771  285 *}  nipkow@26771  286 nipkow@24616  287 text{* The following simple sort functions are intended for proofs,  nipkow@24616  288 not for efficient implementations. *}  nipkow@24616  289 wenzelm@25221  290 context linorder  wenzelm@25221  291 begin  wenzelm@25221  292 haftmann@39915  293 inductive sorted :: "'a list \ bool" where  haftmann@39915  294  Nil [iff]: "sorted []"  haftmann@39915  295 | Cons: "\y\set xs. x \ y \ sorted xs \ sorted (x # xs)"  haftmann@39915  296 haftmann@39915  297 lemma sorted_single [iff]:  haftmann@39915  298  "sorted [x]"  haftmann@39915  299  by (rule sorted.Cons) auto  haftmann@39915  300 haftmann@39915  301 lemma sorted_many:  haftmann@39915  302  "x \ y \ sorted (y # zs) \ sorted (x # y # zs)"  haftmann@39915  303  by (rule sorted.Cons) (cases "y # zs" rule: sorted.cases, auto)  haftmann@39915  304 haftmann@39915  305 lemma sorted_many_eq [simp, code]:  haftmann@39915  306  "sorted (x # y # zs) \ x \ y \ sorted (y # zs)"  haftmann@39915  307  by (auto intro: sorted_many elim: sorted.cases)  haftmann@39915  308 haftmann@39915  309 lemma [code]:  haftmann@39915  310  "sorted [] \ True"  haftmann@39915  311  "sorted [x] \ True"  haftmann@39915  312  by simp_all  nipkow@24697  313 hoelzl@33639  314 primrec insort_key :: "('b \ 'a) \ 'b \ 'b list \ 'b list" where  nipkow@50548  315 "insort_key f x [] = [x]" |  nipkow@50548  316 "insort_key f x (y#ys) =  nipkow@50548  317  (if f x \ f y then (x#y#ys) else y#(insort_key f x ys))"  hoelzl@33639  318 haftmann@35195  319 definition sort_key :: "('b \ 'a) \ 'b list \ 'b list" where  nipkow@50548  320 "sort_key f xs = foldr (insort_key f) xs []"  hoelzl@33639  321 haftmann@40210  322 definition insort_insert_key :: "('b \ 'a) \ 'b \ 'b list \ 'b list" where  nipkow@50548  323 "insort_insert_key f x xs =  nipkow@50548  324  (if f x \ f  set xs then xs else insort_key f x xs)"  haftmann@40210  325 hoelzl@33639  326 abbreviation "sort \ sort_key (\x. x)"  hoelzl@33639  327 abbreviation "insort \ insort_key (\x. x)"  haftmann@40210  328 abbreviation "insort_insert \ insort_insert_key (\x. x)"  haftmann@35608  329 wenzelm@25221  330 end  wenzelm@25221  331 nipkow@24616  332 wenzelm@23388  333 subsubsection {* List comprehension *}  nipkow@23192  334 nipkow@24349  335 text{* Input syntax for Haskell-like list comprehension notation.  nipkow@24349  336 Typical example: @{text"[(x,y). x \ xs, y \ ys, x \ y]"},  nipkow@24349  337 the list of all pairs of distinct elements from @{text xs} and @{text ys}.  nipkow@24349  338 The syntax is as in Haskell, except that @{text"|"} becomes a dot  nipkow@24349  339 (like in Isabelle's set comprehension): @{text"[e. x \ xs, \]"} rather than  nipkow@24349  340 \verb![e| x <- xs, ...]!.  nipkow@24349  341 nipkow@24349  342 The qualifiers after the dot are  nipkow@24349  343 \begin{description}  nipkow@24349  344 \item[generators] @{text"p \ xs"},  nipkow@24476  345  where @{text p} is a pattern and @{text xs} an expression of list type, or  nipkow@24476  346 \item[guards] @{text"b"}, where @{text b} is a boolean expression.  nipkow@24476  347 %\item[local bindings] @ {text"let x = e"}.  nipkow@24349  348 \end{description}  nipkow@23240  349 nipkow@24476  350 Just like in Haskell, list comprehension is just a shorthand. To avoid  nipkow@24476  351 misunderstandings, the translation into desugared form is not reversed  nipkow@24476  352 upon output. Note that the translation of @{text"[e. x \ xs]"} is  nipkow@24476  353 optmized to @{term"map (%x. e) xs"}.  nipkow@23240  354 nipkow@24349  355 It is easy to write short list comprehensions which stand for complex  nipkow@24349  356 expressions. During proofs, they may become unreadable (and  nipkow@24349  357 mangled). In such cases it can be advisable to introduce separate  nipkow@24349  358 definitions for the list comprehensions in question. *}  nipkow@24349  359 wenzelm@46138  360 nonterminal lc_qual and lc_quals  nipkow@23192  361 nipkow@23192  362 syntax  wenzelm@46138  363  "_listcompr" :: "'a \ lc_qual \ lc_quals \ 'a list" ("[_ . __")  wenzelm@46138  364  "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ <- _")  wenzelm@46138  365  "_lc_test" :: "bool \ lc_qual" ("_")  wenzelm@46138  366  (*"_lc_let" :: "letbinds => lc_qual" ("let _")*)  wenzelm@46138  367  "_lc_end" :: "lc_quals" ("]")  wenzelm@46138  368  "_lc_quals" :: "lc_qual \ lc_quals \ lc_quals" (", __")  wenzelm@46138  369  "_lc_abs" :: "'a => 'b list => 'b list"  nipkow@23192  370 nipkow@24476  371 (* These are easier than ML code but cannot express the optimized  nipkow@24476  372  translation of [e. p<-xs]  nipkow@23192  373 translations  wenzelm@46138  374  "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"  wenzelm@46138  375  "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"  wenzelm@46138  376  => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"  wenzelm@46138  377  "[e. P]" => "if P then [e] else []"  wenzelm@46138  378  "_listcompr e (_lc_test P) (_lc_quals Q Qs)"  wenzelm@46138  379  => "if P then (_listcompr e Q Qs) else []"  wenzelm@46138  380  "_listcompr e (_lc_let b) (_lc_quals Q Qs)"  wenzelm@46138  381  => "_Let b (_listcompr e Q Qs)"  nipkow@24476  382 *)  nipkow@23240  383 nipkow@23279  384 syntax (xsymbols)  wenzelm@46138  385  "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _")  nipkow@23279  386 syntax (HTML output)  wenzelm@46138  387  "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _")  nipkow@24349  388 wenzelm@52143  389 parse_translation {*  wenzelm@46138  390  let  wenzelm@46138  391  val NilC = Syntax.const @{const_syntax Nil};  wenzelm@46138  392  val ConsC = Syntax.const @{const_syntax Cons};  wenzelm@46138  393  val mapC = Syntax.const @{const_syntax map};  wenzelm@46138  394  val concatC = Syntax.const @{const_syntax concat};  wenzelm@46138  395  val IfC = Syntax.const @{const_syntax If};  wenzelm@46138  396 wenzelm@46138  397  fun single x = ConsC $x$ NilC;  wenzelm@46138  398 wenzelm@46138  399  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)  wenzelm@46138  400  let  wenzelm@46138  401  (* FIXME proper name context!? *)  wenzelm@46138  402  val x =  wenzelm@46138  403  Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);  wenzelm@46138  404  val e = if opti then single e else e;  wenzelm@46138  405  val case1 = Syntax.const @{syntax_const "_case1"} $p$ e;  wenzelm@46138  406  val case2 =  wenzelm@46138  407  Syntax.const @{syntax_const "_case1"} $ wenzelm@46138  408  Syntax.const @{const_syntax dummy_pattern}$ NilC;  wenzelm@46138  409  val cs = Syntax.const @{syntax_const "_case2"} $case1$ case2;  traytel@51678  410  in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end;  wenzelm@46138  411 wenzelm@46138  412  fun abs_tr ctxt p e opti =  wenzelm@46138  413  (case Term_Position.strip_positions p of  wenzelm@46138  414  Free (s, T) =>  wenzelm@46138  415  let  wenzelm@46138  416  val thy = Proof_Context.theory_of ctxt;  wenzelm@46138  417  val s' = Proof_Context.intern_const ctxt s;  wenzelm@46138  418  in  wenzelm@46138  419  if Sign.declared_const thy s'  wenzelm@46138  420  then (pat_tr ctxt p e opti, false)  wenzelm@46138  421  else (Syntax_Trans.abs_tr [p, e], true)  wenzelm@46138  422  end  wenzelm@46138  423  | _ => (pat_tr ctxt p e opti, false));  wenzelm@46138  424 wenzelm@46138  425  fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $b, qs] =  wenzelm@46138  426  let  wenzelm@46138  427  val res =  wenzelm@46138  428  (case qs of  wenzelm@46138  429  Const (@{syntax_const "_lc_end"}, _) => single e  wenzelm@46138  430  | Const (@{syntax_const "_lc_quals"}, _)$ q $qs => lc_tr ctxt [e, q, qs]);  wenzelm@46138  431  in IfC$ b $res$ NilC end  wenzelm@46138  432  | lc_tr ctxt  wenzelm@46138  433  [e, Const (@{syntax_const "_lc_gen"}, _) $p$ es,  wenzelm@46138  434  Const(@{syntax_const "_lc_end"}, _)] =  wenzelm@46138  435  (case abs_tr ctxt p e true of  wenzelm@46138  436  (f, true) => mapC $f$ es  wenzelm@46138  437  | (f, false) => concatC $(mapC$ f $es))  wenzelm@46138  438  | lc_tr ctxt  wenzelm@46138  439  [e, Const (@{syntax_const "_lc_gen"}, _)$ p $es,  wenzelm@46138  440  Const (@{syntax_const "_lc_quals"}, _)$ q $qs] =  wenzelm@46138  441  let val e' = lc_tr ctxt [e, q, qs];  wenzelm@46138  442  in concatC$ (mapC $(fst (abs_tr ctxt p e' false))$ es) end;  wenzelm@46138  443 wenzelm@46138  444  in [(@{syntax_const "_listcompr"}, lc_tr)] end  nipkow@24349  445 *}  nipkow@23279  446 wenzelm@51272  447 ML_val {*  wenzelm@42167  448  let  wenzelm@42167  449  val read = Syntax.read_term @{context};  wenzelm@42167  450  fun check s1 s2 = read s1 aconv read s2 orelse error ("Check failed: " ^ quote s1);  wenzelm@42167  451  in  wenzelm@42167  452  check "[(x,y,z). b]" "if b then [(x, y, z)] else []";  wenzelm@42167  453  check "[(x,y,z). x\xs]" "map (\x. (x, y, z)) xs";  wenzelm@42167  454  check "[e x y. x\xs, y\ys]" "concat (map (\x. map (\y. e x y) ys) xs)";  wenzelm@42167  455  check "[(x,y,z). xb]" "if x < a then if b < x then [(x, y, z)] else [] else []";  wenzelm@42167  456  check "[(x,y,z). x\xs, x>b]" "concat (map (\x. if b < x then [(x, y, z)] else []) xs)";  wenzelm@42167  457  check "[(x,y,z). xxs]" "if x < a then map (\x. (x, y, z)) xs else []";  wenzelm@42167  458  check "[(x,y). Cons True x \ xs]"  wenzelm@42167  459  "concat (map (\xa. case xa of [] \ [] | True # x \ [(x, y)] | False # x \ []) xs)";  wenzelm@42167  460  check "[(x,y,z). Cons x [] \ xs]"  wenzelm@42167  461  "concat (map (\xa. case xa of [] \ [] | [x] \ [(x, y, z)] | x # aa # lista \ []) xs)";  wenzelm@42167  462  check "[(x,y,z). xb, x=d]"  wenzelm@42167  463  "if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []";  wenzelm@42167  464  check "[(x,y,z). xb, y\ys]"  wenzelm@42167  465  "if x < a then if b < x then map (\y. (x, y, z)) ys else [] else []";  wenzelm@42167  466  check "[(x,y,z). xxs,y>b]"  wenzelm@42167  467  "if x < a then concat (map (\x. if b < y then [(x, y, z)] else []) xs) else []";  wenzelm@42167  468  check "[(x,y,z). xxs, y\ys]"  wenzelm@42167  469  "if x < a then concat (map (\x. map (\y. (x, y, z)) ys) xs) else []";  wenzelm@42167  470  check "[(x,y,z). x\xs, x>b, yx. if b < x then if y < a then [(x, y, z)] else [] else []) xs)";  wenzelm@42167  472  check "[(x,y,z). x\xs, x>b, y\ys]"  wenzelm@42167  473  "concat (map (\x. if b < x then map (\y. (x, y, z)) ys else []) xs)";  wenzelm@42167  474  check "[(x,y,z). x\xs, y\ys,y>x]"  wenzelm@42167  475  "concat (map (\x. concat (map (\y. if x < y then [(x, y, z)] else []) ys)) xs)";  wenzelm@42167  476  check "[(x,y,z). x\xs, y\ys,z\zs]"  wenzelm@42167  477  "concat (map (\x. concat (map (\y. map (\z. (x, y, z)) zs) ys)) xs)"  wenzelm@42167  478  end;  wenzelm@42167  479 *}  wenzelm@42167  480 wenzelm@35115  481 (*  nipkow@24349  482 term "[(x,y). x\xs, let xx = x+x, y\ys, y \ xx]"  nipkow@23192  483 *)  nipkow@23192  484 wenzelm@42167  485 wenzelm@50422  486 ML {*  wenzelm@50422  487 (* Simproc for rewriting list comprehensions applied to List.set to set  wenzelm@50422  488  comprehension. *)  wenzelm@50422  489 wenzelm@50422  490 signature LIST_TO_SET_COMPREHENSION =  wenzelm@50422  491 sig  wenzelm@51717  492  val simproc : Proof.context -> cterm -> thm option  wenzelm@50422  493 end  wenzelm@50422  494 wenzelm@50422  495 structure List_to_Set_Comprehension : LIST_TO_SET_COMPREHENSION =  wenzelm@50422  496 struct  wenzelm@50422  497 wenzelm@50422  498 (* conversion *)  wenzelm@50422  499 wenzelm@50422  500 fun all_exists_conv cv ctxt ct =  wenzelm@50422  501  (case Thm.term_of ct of  wenzelm@50422  502  Const (@{const_name HOL.Ex}, _) $Abs _ =>  wenzelm@50422  503  Conv.arg_conv (Conv.abs_conv (all_exists_conv cv o #2) ctxt) ct  wenzelm@50422  504  | _ => cv ctxt ct)  wenzelm@50422  505 wenzelm@50422  506 fun all_but_last_exists_conv cv ctxt ct =  wenzelm@50422  507  (case Thm.term_of ct of  wenzelm@50422  508  Const (@{const_name HOL.Ex}, _)$ Abs (_, _, Const (@{const_name HOL.Ex}, _) $_) =>  wenzelm@50422  509  Conv.arg_conv (Conv.abs_conv (all_but_last_exists_conv cv o #2) ctxt) ct  wenzelm@50422  510  | _ => cv ctxt ct)  wenzelm@50422  511 wenzelm@50422  512 fun Collect_conv cv ctxt ct =  wenzelm@50422  513  (case Thm.term_of ct of  wenzelm@50422  514  Const (@{const_name Set.Collect}, _)$ Abs _ => Conv.arg_conv (Conv.abs_conv cv ctxt) ct  wenzelm@50422  515  | _ => raise CTERM ("Collect_conv", [ct]))  wenzelm@50422  516 wenzelm@50422  517 fun rewr_conv' th = Conv.rewr_conv (mk_meta_eq th)  wenzelm@50422  518 wenzelm@50422  519 fun conjunct_assoc_conv ct =  wenzelm@50422  520  Conv.try_conv  wenzelm@51315  521  (rewr_conv' @{thm conj_assoc} then_conv HOLogic.conj_conv Conv.all_conv conjunct_assoc_conv) ct  wenzelm@50422  522 wenzelm@50422  523 fun right_hand_set_comprehension_conv conv ctxt =  wenzelm@51315  524  HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv  wenzelm@50422  525  (Collect_conv (all_exists_conv conv o #2) ctxt))  wenzelm@50422  526 wenzelm@50422  527 wenzelm@50422  528 (* term abstraction of list comprehension patterns *)  wenzelm@50422  529 wenzelm@50422  530 datatype termlets = If | Case of (typ * int)  wenzelm@50422  531 wenzelm@51717  532 fun simproc ctxt redex =  wenzelm@50422  533  let  wenzelm@50422  534  val thy = Proof_Context.theory_of ctxt  wenzelm@50422  535  val set_Nil_I = @{thm trans} OF [@{thm set.simps(1)}, @{thm empty_def}]  wenzelm@50422  536  val set_singleton = @{lemma "set [a] = {x. x = a}" by simp}  wenzelm@50422  537  val inst_Collect_mem_eq = @{lemma "set A = {x. x : set A}" by simp}  wenzelm@50422  538  val del_refl_eq = @{lemma "(t = t & P) == P" by simp}  wenzelm@50422  539  fun mk_set T = Const (@{const_name List.set}, HOLogic.listT T --> HOLogic.mk_setT T)  wenzelm@50422  540  fun dest_set (Const (@{const_name List.set}, _) $xs) = xs  wenzelm@50422  541  fun dest_singleton_list (Const (@{const_name List.Cons}, _)  wenzelm@50422  542 $ t $(Const (@{const_name List.Nil}, _))) = t  wenzelm@50422  543  | dest_singleton_list t = raise TERM ("dest_singleton_list", [t])  wenzelm@50422  544  (* We check that one case returns a singleton list and all other cases  wenzelm@50422  545  return [], and return the index of the one singleton list case *)  wenzelm@50422  546  fun possible_index_of_singleton_case cases =  wenzelm@50422  547  let  wenzelm@50422  548  fun check (i, case_t) s =  wenzelm@50422  549  (case strip_abs_body case_t of  wenzelm@50422  550  (Const (@{const_name List.Nil}, _)) => s  wenzelm@50422  551  | _ => (case s of NONE => SOME i | SOME _ => NONE))  wenzelm@50422  552  in  wenzelm@50422  553  fold_index check cases NONE  wenzelm@50422  554  end  wenzelm@50422  555  (* returns (case_expr type index chosen_case) option *)  wenzelm@50422  556  fun dest_case case_term =  wenzelm@50422  557  let  wenzelm@50422  558  val (case_const, args) = strip_comb case_term  wenzelm@50422  559  in  wenzelm@50422  560  (case try dest_Const case_const of  wenzelm@50422  561  SOME (c, T) =>  wenzelm@50422  562  (case Datatype.info_of_case thy c of  wenzelm@50422  563  SOME _ =>  wenzelm@50422  564  (case possible_index_of_singleton_case (fst (split_last args)) of  wenzelm@50422  565  SOME i =>  wenzelm@50422  566  let  wenzelm@50422  567  val (Ts, _) = strip_type T  wenzelm@50422  568  val T' = List.last Ts  wenzelm@50422  569  in SOME (List.last args, T', i, nth args i) end  wenzelm@50422  570  | NONE => NONE)  wenzelm@50422  571  | NONE => NONE)  wenzelm@50422  572  | NONE => NONE)  wenzelm@50422  573  end  wenzelm@50422  574  (* returns condition continuing term option *)  wenzelm@50422  575  fun dest_if (Const (@{const_name If}, _)$ cond $then_t$ Const (@{const_name Nil}, _)) =  wenzelm@50422  576  SOME (cond, then_t)  wenzelm@50422  577  | dest_if _ = NONE  wenzelm@50422  578  fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1  wenzelm@50422  579  | tac ctxt (If :: cont) =  wenzelm@50422  580  Splitter.split_tac [@{thm split_if}] 1  wenzelm@50422  581  THEN rtac @{thm conjI} 1  wenzelm@50422  582  THEN rtac @{thm impI} 1  wenzelm@50422  583  THEN Subgoal.FOCUS (fn {prems, context, ...} =>  wenzelm@50422  584  CONVERSION (right_hand_set_comprehension_conv (K  wenzelm@51315  585  (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_TrueI})) Conv.all_conv  wenzelm@50422  586  then_conv  wenzelm@50422  587  rewr_conv' @{lemma "(True & P) = P" by simp})) context) 1) ctxt 1  wenzelm@50422  588  THEN tac ctxt cont  wenzelm@50422  589  THEN rtac @{thm impI} 1  wenzelm@50422  590  THEN Subgoal.FOCUS (fn {prems, context, ...} =>  wenzelm@50422  591  CONVERSION (right_hand_set_comprehension_conv (K  wenzelm@51315  592  (HOLogic.conj_conv (Conv.rewr_conv (List.last prems RS @{thm Eq_FalseI})) Conv.all_conv  wenzelm@50422  593  then_conv rewr_conv' @{lemma "(False & P) = False" by simp})) context) 1) ctxt 1  wenzelm@50422  594  THEN rtac set_Nil_I 1  wenzelm@50422  595  | tac ctxt (Case (T, i) :: cont) =  wenzelm@50422  596  let  wenzelm@50422  597  val info = Datatype.the_info thy (fst (dest_Type T))  wenzelm@50422  598  in  wenzelm@50422  599  (* do case distinction *)  wenzelm@50422  600  Splitter.split_tac [#split info] 1  wenzelm@50422  601  THEN EVERY (map_index (fn (i', _) =>  wenzelm@50422  602  (if i' < length (#case_rewrites info) - 1 then rtac @{thm conjI} 1 else all_tac)  wenzelm@50422  603  THEN REPEAT_DETERM (rtac @{thm allI} 1)  wenzelm@50422  604  THEN rtac @{thm impI} 1  wenzelm@50422  605  THEN (if i' = i then  wenzelm@50422  606  (* continue recursively *)  wenzelm@50422  607  Subgoal.FOCUS (fn {prems, context, ...} =>  wenzelm@50422  608  CONVERSION (Thm.eta_conversion then_conv right_hand_set_comprehension_conv (K  wenzelm@51315  609  ((HOLogic.conj_conv  wenzelm@51315  610  (HOLogic.eq_conv Conv.all_conv (rewr_conv' (List.last prems)) then_conv  wenzelm@50422  611  (Conv.try_conv (Conv.rewrs_conv (map mk_meta_eq (#inject info)))))  wenzelm@50422  612  Conv.all_conv)  wenzelm@50422  613  then_conv (Conv.try_conv (Conv.rewr_conv del_refl_eq))  wenzelm@50422  614  then_conv conjunct_assoc_conv)) context  wenzelm@51315  615  then_conv (HOLogic.Trueprop_conv (HOLogic.eq_conv Conv.all_conv (Collect_conv (fn (_, ctxt) =>  wenzelm@50422  616  Conv.repeat_conv  wenzelm@50422  617  (all_but_last_exists_conv  wenzelm@50422  618  (K (rewr_conv'  wenzelm@50422  619  @{lemma "(EX x. x = t & P x) = P t" by simp})) ctxt)) context)))) 1) ctxt 1  wenzelm@50422  620  THEN tac ctxt cont  wenzelm@50422  621  else  wenzelm@50422  622  Subgoal.FOCUS (fn {prems, context, ...} =>  wenzelm@50422  623  CONVERSION  wenzelm@50422  624  (right_hand_set_comprehension_conv (K  wenzelm@51315  625  (HOLogic.conj_conv  wenzelm@51315  626  ((HOLogic.eq_conv Conv.all_conv  wenzelm@50422  627  (rewr_conv' (List.last prems))) then_conv  wenzelm@50422  628  (Conv.rewrs_conv (map (fn th => th RS @{thm Eq_FalseI}) (#distinct info))))  wenzelm@50422  629  Conv.all_conv then_conv  wenzelm@50422  630  (rewr_conv' @{lemma "(False & P) = False" by simp}))) context then_conv  wenzelm@51314  631  HOLogic.Trueprop_conv  wenzelm@51315  632  (HOLogic.eq_conv Conv.all_conv  wenzelm@50422  633  (Collect_conv (fn (_, ctxt) =>  wenzelm@50422  634  Conv.repeat_conv  wenzelm@50422  635  (Conv.bottom_conv  wenzelm@50422  636  (K (rewr_conv'  wenzelm@50422  637  @{lemma "(EX x. P) = P" by simp})) ctxt)) context))) 1) ctxt 1  wenzelm@50422  638  THEN rtac set_Nil_I 1)) (#case_rewrites info))  wenzelm@50422  639  end  wenzelm@50422  640  fun make_inner_eqs bound_vs Tis eqs t =  wenzelm@50422  641  (case dest_case t of  wenzelm@50422  642  SOME (x, T, i, cont) =>  wenzelm@50422  643  let  wenzelm@52131  644  val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)  wenzelm@50422  645  val x' = incr_boundvars (length vs) x  wenzelm@50422  646  val eqs' = map (incr_boundvars (length vs)) eqs  wenzelm@50422  647  val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i  wenzelm@50422  648  val constr_t =  wenzelm@50422  649  list_comb  wenzelm@50422  650  (Const (constr_name, map snd vs ---> T), map Bound (((length vs) - 1) downto 0))  wenzelm@50422  651  val constr_eq = Const (@{const_name HOL.eq}, T --> T --> @{typ bool}) $constr_t$ x'  wenzelm@50422  652  in  wenzelm@50422  653  make_inner_eqs (rev vs @ bound_vs) (Case (T, i) :: Tis) (constr_eq :: eqs') body  wenzelm@50422  654  end  wenzelm@50422  655  | NONE =>  wenzelm@50422  656  (case dest_if t of  wenzelm@50422  657  SOME (condition, cont) => make_inner_eqs bound_vs (If :: Tis) (condition :: eqs) cont  wenzelm@50422  658  | NONE =>  wenzelm@50422  659  if eqs = [] then NONE (* no rewriting, nothing to be done *)  wenzelm@50422  660  else  wenzelm@50422  661  let  wenzelm@50422  662  val Type (@{type_name List.list}, [rT]) = fastype_of1 (map snd bound_vs, t)  wenzelm@50422  663  val pat_eq =  wenzelm@50422  664  (case try dest_singleton_list t of  wenzelm@50422  665  SOME t' =>  wenzelm@50422  666  Const (@{const_name HOL.eq}, rT --> rT --> @{typ bool}) $ wenzelm@50422  667  Bound (length bound_vs)$ t'  wenzelm@50422  668  | NONE =>  wenzelm@50422  669  Const (@{const_name Set.member}, rT --> HOLogic.mk_setT rT --> @{typ bool}) $ wenzelm@50422  670  Bound (length bound_vs)$ (mk_set rT $t))  wenzelm@50422  671  val reverse_bounds = curry subst_bounds  wenzelm@50422  672  ((map Bound ((length bound_vs - 1) downto 0)) @ [Bound (length bound_vs)])  wenzelm@50422  673  val eqs' = map reverse_bounds eqs  wenzelm@50422  674  val pat_eq' = reverse_bounds pat_eq  wenzelm@50422  675  val inner_t =  wenzelm@50422  676  fold (fn (_, T) => fn t => HOLogic.exists_const T$ absdummy T t)  wenzelm@50422  677  (rev bound_vs) (fold (curry HOLogic.mk_conj) eqs' pat_eq')  wenzelm@50422  678  val lhs = term_of redex  wenzelm@50422  679  val rhs = HOLogic.mk_Collect ("x", rT, inner_t)  wenzelm@50422  680  val rewrite_rule_t = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))  wenzelm@50422  681  in  wenzelm@50422  682  SOME  wenzelm@50422  683  ((Goal.prove ctxt [] [] rewrite_rule_t  wenzelm@50422  684  (fn {context, ...} => tac context (rev Tis))) RS @{thm eq_reflection})  wenzelm@50422  685  end))  wenzelm@50422  686  in  wenzelm@50422  687  make_inner_eqs [] [] [] (dest_set (term_of redex))  wenzelm@50422  688  end  wenzelm@50422  689 wenzelm@50422  690 end  wenzelm@50422  691 *}  bulwahn@41463  692 bulwahn@41463  693 simproc_setup list_to_set_comprehension ("set xs") = {* K List_to_Set_Comprehension.simproc *}  bulwahn@41463  694 haftmann@46133  695 code_datatype set coset  haftmann@46133  696 haftmann@46133  697 hide_const (open) coset  wenzelm@35115  698 haftmann@49948  699 haftmann@21061  700 subsubsection {* @{const Nil} and @{const Cons} *}  haftmann@21061  701 haftmann@21061  702 lemma not_Cons_self [simp]:  haftmann@21061  703  "xs \ x # xs"  nipkow@13145  704 by (induct xs) auto  wenzelm@13114  705 wenzelm@41697  706 lemma not_Cons_self2 [simp]:  wenzelm@41697  707  "x # xs \ xs"  wenzelm@41697  708 by (rule not_Cons_self [symmetric])  wenzelm@13114  709 wenzelm@13142  710 lemma neq_Nil_conv: "(xs \ []) = (\y ys. xs = y # ys)"  nipkow@13145  711 by (induct xs) auto  wenzelm@13114  712 wenzelm@13142  713 lemma length_induct:  haftmann@21061  714  "(\xs. \ys. length ys < length xs \ P ys \ P xs) \ P xs"  nipkow@17589  715 by (rule measure_induct [of length]) iprover  wenzelm@13114  716 haftmann@37289  717 lemma list_nonempty_induct [consumes 1, case_names single cons]:  haftmann@37289  718  assumes "xs \ []"  haftmann@37289  719  assumes single: "\x. P [x]"  haftmann@37289  720  assumes cons: "\x xs. xs \ [] \ P xs \ P (x # xs)"  haftmann@37289  721  shows "P xs"  haftmann@37289  722 using xs \ [] proof (induct xs)  haftmann@37289  723  case Nil then show ?case by simp  haftmann@37289  724 next  haftmann@37289  725  case (Cons x xs) show ?case proof (cases xs)  haftmann@37289  726  case Nil with single show ?thesis by simp  haftmann@37289  727  next  haftmann@37289  728  case Cons then have "xs \ []" by simp  haftmann@37289  729  moreover with Cons.hyps have "P xs" .  haftmann@37289  730  ultimately show ?thesis by (rule cons)  haftmann@37289  731  qed  haftmann@37289  732 qed  haftmann@37289  733 hoelzl@45714  734 lemma inj_split_Cons: "inj_on (\(xs, n). n#xs) X"  hoelzl@45714  735  by (auto intro!: inj_onI)  wenzelm@13114  736 haftmann@49948  737 haftmann@21061  738 subsubsection {* @{const length} *}  wenzelm@13114  739 wenzelm@13142  740 text {*  haftmann@21061  741  Needs to come before @{text "@"} because of theorem @{text  haftmann@21061  742  append_eq_append_conv}.  wenzelm@13142  743 *}  wenzelm@13114  744 wenzelm@13142  745 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"  nipkow@13145  746 by (induct xs) auto  wenzelm@13114  747 wenzelm@13142  748 lemma length_map [simp]: "length (map f xs) = length xs"  nipkow@13145  749 by (induct xs) auto  wenzelm@13114  750 wenzelm@13142  751 lemma length_rev [simp]: "length (rev xs) = length xs"  nipkow@13145  752 by (induct xs) auto  wenzelm@13114  753 wenzelm@13142  754 lemma length_tl [simp]: "length (tl xs) = length xs - 1"  nipkow@13145  755 by (cases xs) auto  wenzelm@13114  756 wenzelm@13142  757 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"  nipkow@13145  758 by (induct xs) auto  wenzelm@13114  759 wenzelm@13142  760 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \ [])"  nipkow@13145  761 by (induct xs) auto  wenzelm@13114  762 nipkow@23479  763 lemma length_pos_if_in_set: "x : set xs \ length xs > 0"  nipkow@23479  764 by auto  nipkow@23479  765 wenzelm@13114  766 lemma length_Suc_conv:  nipkow@13145  767 "(length xs = Suc n) = (\y ys. xs = y # ys \ length ys = n)"  nipkow@13145  768 by (induct xs) auto  wenzelm@13142  769 nipkow@14025  770 lemma Suc_length_conv:  nipkow@14025  771 "(Suc n = length xs) = (\y ys. xs = y # ys \ length ys = n)"  paulson@14208  772 apply (induct xs, simp, simp)  nipkow@14025  773 apply blast  nipkow@14025  774 done  nipkow@14025  775 wenzelm@25221  776 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"  wenzelm@25221  777  by (induct xs) auto  wenzelm@25221  778 haftmann@26442  779 lemma list_induct2 [consumes 1, case_names Nil Cons]:  haftmann@26442  780  "length xs = length ys \ P [] [] \  haftmann@26442  781  (\x xs y ys. length xs = length ys \ P xs ys \ P (x#xs) (y#ys))  haftmann@26442  782  \ P xs ys"  haftmann@26442  783 proof (induct xs arbitrary: ys)  haftmann@26442  784  case Nil then show ?case by simp  haftmann@26442  785 next  haftmann@26442  786  case (Cons x xs ys) then show ?case by (cases ys) simp_all  haftmann@26442  787 qed  haftmann@26442  788 haftmann@26442  789 lemma list_induct3 [consumes 2, case_names Nil Cons]:  haftmann@26442  790  "length xs = length ys \ length ys = length zs \ P [] [] [] \  haftmann@26442  791  (\x xs y ys z zs. length xs = length ys \ length ys = length zs \ P xs ys zs \ P (x#xs) (y#ys) (z#zs))  haftmann@26442  792  \ P xs ys zs"  haftmann@26442  793 proof (induct xs arbitrary: ys zs)  haftmann@26442  794  case Nil then show ?case by simp  haftmann@26442  795 next  haftmann@26442  796  case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)  haftmann@26442  797  (cases zs, simp_all)  haftmann@26442  798 qed  wenzelm@13114  799 kaliszyk@36154  800 lemma list_induct4 [consumes 3, case_names Nil Cons]:  kaliszyk@36154  801  "length xs = length ys \ length ys = length zs \ length zs = length ws \  kaliszyk@36154  802  P [] [] [] [] \ (\x xs y ys z zs w ws. length xs = length ys \  kaliszyk@36154  803  length ys = length zs \ length zs = length ws \ P xs ys zs ws \  kaliszyk@36154  804  P (x#xs) (y#ys) (z#zs) (w#ws)) \ P xs ys zs ws"  kaliszyk@36154  805 proof (induct xs arbitrary: ys zs ws)  kaliszyk@36154  806  case Nil then show ?case by simp  kaliszyk@36154  807 next  kaliszyk@36154  808  case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)  kaliszyk@36154  809 qed  kaliszyk@36154  810 krauss@22493  811 lemma list_induct2':  krauss@22493  812  "\ P [] [];  krauss@22493  813  \x xs. P (x#xs) [];  krauss@22493  814  \y ys. P [] (y#ys);  krauss@22493  815  \x xs y ys. P xs ys \ P (x#xs) (y#ys) \  krauss@22493  816  \ P xs ys"  krauss@22493  817 by (induct xs arbitrary: ys) (case_tac x, auto)+  krauss@22493  818 nipkow@22143  819 lemma neq_if_length_neq: "length xs \ length ys \ (xs = ys) == False"  nipkow@24349  820 by (rule Eq_FalseI) auto  wenzelm@24037  821 wenzelm@24037  822 simproc_setup list_neq ("(xs::'a list) = ys") = {*  nipkow@22143  823 (*  nipkow@22143  824 Reduces xs=ys to False if xs and ys cannot be of the same length.  nipkow@22143  825 This is the case if the atomic sublists of one are a submultiset  nipkow@22143  826 of those of the other list and there are fewer Cons's in one than the other.  nipkow@22143  827 *)  wenzelm@24037  828 wenzelm@24037  829 let  nipkow@22143  830 huffman@29856  831 fun len (Const(@{const_name Nil},_)) acc = acc  huffman@29856  832  | len (Const(@{const_name Cons},_) $_$ xs) (ts,n) = len xs (ts,n+1)  huffman@29856  833  | len (Const(@{const_name append},_) $xs$ ys) acc = len xs (len ys acc)  huffman@29856  834  | len (Const(@{const_name rev},_) $xs) acc = len xs acc  huffman@29856  835  | len (Const(@{const_name map},_)$ _ $xs) acc = len xs acc  nipkow@22143  836  | len t (ts,n) = (t::ts,n);  nipkow@22143  837 wenzelm@51717  838 val ss = simpset_of @{context};  wenzelm@51717  839 wenzelm@51717  840 fun list_neq ctxt ct =  nipkow@22143  841  let  wenzelm@24037  842  val (Const(_,eqT)$ lhs $rhs) = Thm.term_of ct;  nipkow@22143  843  val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);  nipkow@22143  844  fun prove_neq() =  nipkow@22143  845  let  nipkow@22143  846  val Type(_,listT::_) = eqT;  haftmann@22994  847  val size = HOLogic.size_const listT;  nipkow@22143  848  val eq_len = HOLogic.mk_eq (size$ lhs, size $rhs);  nipkow@22143  849  val neq_len = HOLogic.mk_Trueprop (HOLogic.Not$ eq_len);  wenzelm@51717  850  val thm = Goal.prove ctxt [] [] neq_len  wenzelm@51717  851  (K (simp_tac (put_simpset ss ctxt) 1));  haftmann@22633  852  in SOME (thm RS @{thm neq_if_length_neq}) end  nipkow@22143  853  in  wenzelm@23214  854  if m < n andalso submultiset (op aconv) (ls,rs) orelse  wenzelm@23214  855  n < m andalso submultiset (op aconv) (rs,ls)  nipkow@22143  856  then prove_neq() else NONE  nipkow@22143  857  end;  wenzelm@51717  858 in K list_neq end;  nipkow@22143  859 *}  nipkow@22143  860 nipkow@22143  861 nipkow@15392  862 subsubsection {* @{text "@"} -- append *}  wenzelm@13114  863 wenzelm@13142  864 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"  nipkow@13145  865 by (induct xs) auto  wenzelm@13114  866 wenzelm@13142  867 lemma append_Nil2 [simp]: "xs @ [] = xs"  nipkow@13145  868 by (induct xs) auto  nipkow@3507  869 wenzelm@13142  870 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \ ys = [])"  nipkow@13145  871 by (induct xs) auto  wenzelm@13114  872 wenzelm@13142  873 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \ ys = [])"  nipkow@13145  874 by (induct xs) auto  wenzelm@13114  875 wenzelm@13142  876 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"  nipkow@13145  877 by (induct xs) auto  wenzelm@13114  878 wenzelm@13142  879 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"  nipkow@13145  880 by (induct xs) auto  wenzelm@13114  881 blanchet@35828  882 lemma append_eq_append_conv [simp, no_atp]:  nipkow@24526  883  "length xs = length ys \ length us = length vs  berghofe@13883  884  ==> (xs@us = ys@vs) = (xs=ys \ us=vs)"  nipkow@24526  885 apply (induct xs arbitrary: ys)  paulson@14208  886  apply (case_tac ys, simp, force)  paulson@14208  887 apply (case_tac ys, force, simp)  nipkow@13145  888 done  wenzelm@13142  889 nipkow@24526  890 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =  nipkow@24526  891  (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"  nipkow@24526  892 apply (induct xs arbitrary: ys zs ts)  nipkow@44890  893  apply fastforce  nipkow@14495  894 apply(case_tac zs)  nipkow@14495  895  apply simp  nipkow@44890  896 apply fastforce  nipkow@14495  897 done  nipkow@14495  898 berghofe@34910  899 lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"  nipkow@13145  900 by simp  wenzelm@13142  901 wenzelm@13142  902 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \ x = y)"  nipkow@13145  903 by simp  wenzelm@13114  904 berghofe@34910  905 lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)"  nipkow@13145  906 by simp  wenzelm@13114  907 wenzelm@13142  908 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"  nipkow@13145  909 using append_same_eq [of _ _ "[]"] by auto  nipkow@3507  910 wenzelm@13142  911 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"  nipkow@13145  912 using append_same_eq [of "[]"] by auto  wenzelm@13114  913 blanchet@35828  914 lemma hd_Cons_tl [simp,no_atp]: "xs \ [] ==> hd xs # tl xs = xs"  nipkow@13145  915 by (induct xs) auto  wenzelm@13114  916 wenzelm@13142  917 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"  nipkow@13145  918 by (induct xs) auto  wenzelm@13114  919 wenzelm@13142  920 lemma hd_append2 [simp]: "xs \ [] ==> hd (xs @ ys) = hd xs"  nipkow@13145  921 by (simp add: hd_append split: list.split)  wenzelm@13114  922 wenzelm@13142  923 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"  nipkow@13145  924 by (simp split: list.split)  wenzelm@13114  925 wenzelm@13142  926 lemma tl_append2 [simp]: "xs \ [] ==> tl (xs @ ys) = tl xs @ ys"  nipkow@13145  927 by (simp add: tl_append split: list.split)  wenzelm@13114  928 wenzelm@13114  929 nipkow@14300  930 lemma Cons_eq_append_conv: "x#xs = ys@zs =  nipkow@14300  931  (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"  nipkow@14300  932 by(cases ys) auto  nipkow@14300  933 nipkow@15281  934 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =  nipkow@15281  935  (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"  nipkow@15281  936 by(cases ys) auto  nipkow@15281  937 nipkow@14300  938 wenzelm@13142  939 text {* Trivial rules for solving @{text "@"}-equations automatically. *}  wenzelm@13114  940 wenzelm@13114  941 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"  nipkow@13145  942 by simp  wenzelm@13114  943 wenzelm@13142  944 lemma Cons_eq_appendI:  nipkow@13145  945 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"  nipkow@13145  946 by (drule sym) simp  wenzelm@13114  947 wenzelm@13142  948 lemma append_eq_appendI:  nipkow@13145  949 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"  nipkow@13145  950 by (drule sym) simp  wenzelm@13114  951 wenzelm@13114  952 wenzelm@13142  953 text {*  nipkow@13145  954 Simplification procedure for all list equalities.  nipkow@13145  955 Currently only tries to rearrange @{text "@"} to see if  nipkow@13145  956 - both lists end in a singleton list,  nipkow@13145  957 - or both lists end in the same list.  wenzelm@13142  958 *}  wenzelm@13142  959 wenzelm@43594  960 simproc_setup list_eq ("(xs::'a list) = ys") = {*  wenzelm@13462  961  let  wenzelm@43594  962  fun last (cons as Const (@{const_name Cons}, _) $_$ xs) =  wenzelm@43594  963  (case xs of Const (@{const_name Nil}, _) => cons | _ => last xs)  wenzelm@43594  964  | last (Const(@{const_name append},_) $_$ ys) = last ys  wenzelm@43594  965  | last t = t;  wenzelm@43594  966   wenzelm@43594  967  fun list1 (Const(@{const_name Cons},_) $_$ Const(@{const_name Nil},_)) = true  wenzelm@43594  968  | list1 _ = false;  wenzelm@43594  969   wenzelm@43594  970  fun butlast ((cons as Const(@{const_name Cons},_) $x)$ xs) =  wenzelm@43594  971  (case xs of Const (@{const_name Nil}, _) => xs | _ => cons $butlast xs)  wenzelm@43594  972  | butlast ((app as Const (@{const_name append}, _)$ xs) $ys) = app$ butlast ys  wenzelm@43594  973  | butlast xs = Const(@{const_name Nil}, fastype_of xs);  wenzelm@43594  974   wenzelm@43594  975  val rearr_ss =  wenzelm@51717  976  simpset_of (put_simpset HOL_basic_ss @{context}  wenzelm@51717  977  addsimps [@{thm append_assoc}, @{thm append_Nil}, @{thm append_Cons}]);  wenzelm@43594  978   wenzelm@51717  979  fun list_eq ctxt (F as (eq as Const(_,eqT)) $lhs$ rhs) =  wenzelm@13462  980  let  wenzelm@43594  981  val lastl = last lhs and lastr = last rhs;  wenzelm@43594  982  fun rearr conv =  wenzelm@43594  983  let  wenzelm@43594  984  val lhs1 = butlast lhs and rhs1 = butlast rhs;  wenzelm@43594  985  val Type(_,listT::_) = eqT  wenzelm@43594  986  val appT = [listT,listT] ---> listT  wenzelm@43594  987  val app = Const(@{const_name append},appT)  wenzelm@43594  988  val F2 = eq $(app$lhs1$lastl)$ (app$rhs1$lastr)  wenzelm@43594  989  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));  wenzelm@51717  990  val thm = Goal.prove ctxt [] [] eq  wenzelm@51717  991  (K (simp_tac (put_simpset rearr_ss ctxt) 1));  wenzelm@43594  992  in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;  wenzelm@43594  993  in  wenzelm@43594  994  if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}  wenzelm@43594  995  else if lastl aconv lastr then rearr @{thm append_same_eq}  wenzelm@43594  996  else NONE  wenzelm@43594  997  end;  wenzelm@51717  998  in fn _ => fn ctxt => fn ct => list_eq ctxt (term_of ct) end;  wenzelm@13114  999 *}  wenzelm@13114  1000 wenzelm@13114  1001 haftmann@49948  1002 subsubsection {* @{const map} *}  wenzelm@13114  1003 haftmann@40210  1004 lemma hd_map:  haftmann@40210  1005  "xs \ [] \ hd (map f xs) = f (hd xs)"  haftmann@40210  1006  by (cases xs) simp_all  haftmann@40210  1007 haftmann@40210  1008 lemma map_tl:  haftmann@40210  1009  "map f (tl xs) = tl (map f xs)"  haftmann@40210  1010  by (cases xs) simp_all  haftmann@40210  1011 wenzelm@13142  1012 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"  nipkow@13145  1013 by (induct xs) simp_all  wenzelm@13114  1014 wenzelm@13142  1015 lemma map_ident [simp]: "map (\x. x) = (\xs. xs)"  nipkow@13145  1016 by (rule ext, induct_tac xs) auto  wenzelm@13114  1017 wenzelm@13142  1018 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"  nipkow@13145  1019 by (induct xs) auto  wenzelm@13114  1020 hoelzl@33639  1021 lemma map_map [simp]: "map f (map g xs) = map (f \ g) xs"  hoelzl@33639  1022 by (induct xs) auto  hoelzl@33639  1023 nipkow@35208  1024 lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)"  nipkow@35208  1025 apply(rule ext)  nipkow@35208  1026 apply(simp)  nipkow@35208  1027 done  nipkow@35208  1028 wenzelm@13142  1029 lemma rev_map: "rev (map f xs) = map f (rev xs)"  nipkow@13145  1030 by (induct xs) auto  wenzelm@13114  1031 nipkow@13737  1032 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"  nipkow@13737  1033 by (induct xs) auto  nipkow@13737  1034 krauss@44013  1035 lemma map_cong [fundef_cong]:  haftmann@40122  1036  "xs = ys \ (\x. x \ set ys \ f x = g x) \ map f xs = map g ys"  haftmann@40122  1037  by simp  wenzelm@13114  1038 wenzelm@13142  1039 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"  nipkow@13145  1040 by (cases xs) auto  wenzelm@13114  1041 wenzelm@13142  1042 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"  nipkow@13145  1043 by (cases xs) auto  wenzelm@13114  1044 paulson@18447  1045 lemma map_eq_Cons_conv:  nipkow@14025  1046  "(map f xs = y#ys) = (\z zs. xs = z#zs \ f z = y \ map f zs = ys)"  nipkow@13145  1047 by (cases xs) auto  wenzelm@13114  1048 paulson@18447  1049 lemma Cons_eq_map_conv:  nipkow@14025  1050  "(x#xs = map f ys) = (\z zs. ys = z#zs \ x = f z \ xs = map f zs)"  nipkow@14025  1051 by (cases ys) auto  nipkow@14025  1052 paulson@18447  1053 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]  paulson@18447  1054 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]  paulson@18447  1055 declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!]  paulson@18447  1056 nipkow@14111  1057 lemma ex_map_conv:  nipkow@14111  1058  "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"  paulson@18447  1059 by(induct ys, auto simp add: Cons_eq_map_conv)  nipkow@14111  1060 nipkow@15110  1061 lemma map_eq_imp_length_eq:  paulson@35510  1062  assumes "map f xs = map g ys"  haftmann@26734  1063  shows "length xs = length ys"  haftmann@26734  1064 using assms proof (induct ys arbitrary: xs)  haftmann@26734  1065  case Nil then show ?case by simp  haftmann@26734  1066 next  haftmann@26734  1067  case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto  paulson@35510  1068  from Cons xs have "map f zs = map g ys" by simp  haftmann@26734  1069  moreover with Cons have "length zs = length ys" by blast  haftmann@26734  1070  with xs show ?case by simp  haftmann@26734  1071 qed  haftmann@26734  1072   nipkow@15110  1073 lemma map_inj_on:  nipkow@15110  1074  "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]  nipkow@15110  1075  ==> xs = ys"  nipkow@15110  1076 apply(frule map_eq_imp_length_eq)  nipkow@15110  1077 apply(rotate_tac -1)  nipkow@15110  1078 apply(induct rule:list_induct2)  nipkow@15110  1079  apply simp  nipkow@15110  1080 apply(simp)  nipkow@15110  1081 apply (blast intro:sym)  nipkow@15110  1082 done  nipkow@15110  1083 nipkow@15110  1084 lemma inj_on_map_eq_map:  nipkow@15110  1085  "inj_on f (set xs Un set ys) \ (map f xs = map f ys) = (xs = ys)"  nipkow@15110  1086 by(blast dest:map_inj_on)  nipkow@15110  1087 wenzelm@13114  1088 lemma map_injective:  nipkow@24526  1089  "map f xs = map f ys ==> inj f ==> xs = ys"  nipkow@24526  1090 by (induct ys arbitrary: xs) (auto dest!:injD)  wenzelm@13114  1091 nipkow@14339  1092 lemma inj_map_eq_map[simp]: "inj f \ (map f xs = map f ys) = (xs = ys)"  nipkow@14339  1093 by(blast dest:map_injective)  nipkow@14339  1094 wenzelm@13114  1095 lemma inj_mapI: "inj f ==> inj (map f)"  nipkow@17589  1096 by (iprover dest: map_injective injD intro: inj_onI)  wenzelm@13114  1097 wenzelm@13114  1098 lemma inj_mapD: "inj (map f) ==> inj f"  paulson@14208  1099 apply (unfold inj_on_def, clarify)  nipkow@13145  1100 apply (erule_tac x = "[x]" in ballE)  paulson@14208  1101  apply (erule_tac x = "[y]" in ballE, simp, blast)  nipkow@13145  1102 apply blast  nipkow@13145  1103 done  wenzelm@13114  1104 nipkow@14339  1105 lemma inj_map[iff]: "inj (map f) = inj f"  nipkow@13145  1106 by (blast dest: inj_mapD intro: inj_mapI)  wenzelm@13114  1107 nipkow@15303  1108 lemma inj_on_mapI: "inj_on f (\(set  A)) \ inj_on (map f) A"  nipkow@15303  1109 apply(rule inj_onI)  nipkow@15303  1110 apply(erule map_inj_on)  nipkow@15303  1111 apply(blast intro:inj_onI dest:inj_onD)  nipkow@15303  1112 done  nipkow@15303  1113 kleing@14343  1114 lemma map_idI: "(\x. x \ set xs \ f x = x) \ map f xs = xs"  kleing@14343  1115 by (induct xs, auto)  wenzelm@13114  1116 nipkow@14402  1117 lemma map_fun_upd [simp]: "y \ set xs \ map (f(y:=v)) xs = map f xs"  nipkow@14402  1118 by (induct xs) auto  nipkow@14402  1119 nipkow@15110  1120 lemma map_fst_zip[simp]:  nipkow@15110  1121  "length xs = length ys \ map fst (zip xs ys) = xs"  nipkow@15110  1122 by (induct rule:list_induct2, simp_all)  nipkow@15110  1123 nipkow@15110  1124 lemma map_snd_zip[simp]:  nipkow@15110  1125  "length xs = length ys \ map snd (zip xs ys) = ys"  nipkow@15110  1126 by (induct rule:list_induct2, simp_all)  nipkow@15110  1127 haftmann@41505  1128 enriched_type map: map  nipkow@47122  1129 by (simp_all add: id_def)  nipkow@47122  1130 haftmann@49948  1131 declare map.id [simp]  haftmann@49948  1132 haftmann@49948  1133 haftmann@49948  1134 subsubsection {* @{const rev} *}  wenzelm@13114  1135 wenzelm@13142  1136 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"  nipkow@13145  1137 by (induct xs) auto  wenzelm@13114  1138 wenzelm@13142  1139 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"  nipkow@13145  1140 by (induct xs) auto  wenzelm@13114  1141 kleing@15870  1142 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"  kleing@15870  1143 by auto  kleing@15870  1144 wenzelm@13142  1145 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"  nipkow@13145  1146 by (induct xs) auto  wenzelm@13114  1147 wenzelm@13142  1148 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"  nipkow@13145  1149 by (induct xs) auto  wenzelm@13114  1150 kleing@15870  1151 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"  kleing@15870  1152 by (cases xs) auto  kleing@15870  1153 kleing@15870  1154 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"  kleing@15870  1155 by (cases xs) auto  kleing@15870  1156 blanchet@46439  1157 lemma rev_is_rev_conv [iff, no_atp]: "(rev xs = rev ys) = (xs = ys)"  haftmann@21061  1158 apply (induct xs arbitrary: ys, force)  paulson@14208  1159 apply (case_tac ys, simp, force)  nipkow@13145  1160 done  wenzelm@13114  1161 nipkow@15439  1162 lemma inj_on_rev[iff]: "inj_on rev A"  nipkow@15439  1163 by(simp add:inj_on_def)  nipkow@15439  1164 wenzelm@13366  1165 lemma rev_induct [case_names Nil snoc]:  wenzelm@13366  1166  "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"  berghofe@15489  1167 apply(simplesubst rev_rev_ident[symmetric])  nipkow@13145  1168 apply(rule_tac list = "rev xs" in list.induct, simp_all)  nipkow@13145  1169 done  wenzelm@13114  1170 wenzelm@13366  1171 lemma rev_exhaust [case_names Nil snoc]:  wenzelm@13366  1172  "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"  nipkow@13145  1173 by (induct xs rule: rev_induct) auto  wenzelm@13114  1174 wenzelm@13366  1175 lemmas rev_cases = rev_exhaust  wenzelm@13366  1176 nipkow@18423  1177 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"  nipkow@18423  1178 by(rule rev_cases[of xs]) auto  nipkow@18423  1179 wenzelm@13114  1180 haftmann@49948  1181 subsubsection {* @{const set} *}  wenzelm@13114  1182 nipkow@46698  1183 declare set.simps [code_post] --"pretty output"  nipkow@46698  1184 wenzelm@13142  1185 lemma finite_set [iff]: "finite (set xs)"  nipkow@13145  1186 by (induct xs) auto  wenzelm@13114  1187 wenzelm@13142  1188 lemma set_append [simp]: "set (xs @ ys) = (set xs \ set ys)"  nipkow@13145  1189 by (induct xs) auto  wenzelm@13114  1190 nipkow@17830  1191 lemma hd_in_set[simp]: "xs \ [] \ hd xs : set xs"  nipkow@17830  1192 by(cases xs) auto  oheimb@14099  1193 wenzelm@13142  1194 lemma set_subset_Cons: "set xs \ set (x # xs)"  nipkow@13145  1195 by auto  wenzelm@13114  1196 oheimb@14099  1197 lemma set_ConsD: "y \ set (x # xs) \ y=x \ y \ set xs"  oheimb@14099  1198 by auto  oheimb@14099  1199 wenzelm@13142  1200 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"  nipkow@13145  1201 by (induct xs) auto  wenzelm@13114  1202 nipkow@15245  1203 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"  nipkow@15245  1204 by(induct xs) auto  nipkow@15245  1205 wenzelm@13142  1206 lemma set_rev [simp]: "set (rev xs) = set xs"  nipkow@13145  1207 by (induct xs) auto  wenzelm@13114  1208 wenzelm@13142  1209 lemma set_map [simp]: "set (map f xs) = f(set xs)"  nipkow@13145  1210 by (induct xs) auto  wenzelm@13114  1211 wenzelm@13142  1212 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \ P x}"  nipkow@13145  1213 by (induct xs) auto  wenzelm@13114  1214 nipkow@32417  1215 lemma set_upt [simp]: "set[i.. \ys zs. xs = ys @ x # zs"  nipkow@18049  1220 proof (induct xs)  nipkow@26073  1221  case Nil thus ?case by simp  nipkow@26073  1222 next  nipkow@26073  1223  case Cons thus ?case by (auto intro: Cons_eq_appendI)  nipkow@26073  1224 qed  nipkow@26073  1225 haftmann@26734  1226 lemma in_set_conv_decomp: "x \ set xs \ (\ys zs. xs = ys @ x # zs)"  haftmann@26734  1227  by (auto elim: split_list)  nipkow@26073  1228 nipkow@26073  1229 lemma split_list_first: "x : set xs \ \ys zs. xs = ys @ x # zs \ x \ set ys"  nipkow@26073  1230 proof (induct xs)  nipkow@26073  1231  case Nil thus ?case by simp  nipkow@18049  1232 next  nipkow@18049  1233  case (Cons a xs)  nipkow@18049  1234  show ?case  nipkow@18049  1235  proof cases  nipkow@44890  1236  assume "x = a" thus ?case using Cons by fastforce  nipkow@18049  1237  next  nipkow@44890  1238  assume "x \ a" thus ?case using Cons by(fastforce intro!: Cons_eq_appendI)  nipkow@26073  1239  qed  nipkow@26073  1240 qed  nipkow@26073  1241 nipkow@26073  1242 lemma in_set_conv_decomp_first:  nipkow@26073  1243  "(x : set xs) = (\ys zs. xs = ys @ x # zs \ x \ set ys)"  haftmann@26734  1244  by (auto dest!: split_list_first)  nipkow@26073  1245 haftmann@40122  1246 lemma split_list_last: "x \ set xs \ \ys zs. xs = ys @ x # zs \ x \ set zs"  haftmann@40122  1247 proof (induct xs rule: rev_induct)  nipkow@26073  1248  case Nil thus ?case by simp  nipkow@26073  1249 next  nipkow@26073  1250  case (snoc a xs)  nipkow@26073  1251  show ?case  nipkow@26073  1252  proof cases  haftmann@40122  1253  assume "x = a" thus ?case using snoc by (metis List.set.simps(1) emptyE)  nipkow@26073  1254  next  nipkow@44890  1255  assume "x \ a" thus ?case using snoc by fastforce  nipkow@18049  1256  qed  nipkow@18049  1257 qed  nipkow@18049  1258 nipkow@26073  1259 lemma in_set_conv_decomp_last:  nipkow@26073  1260  "(x : set xs) = (\ys zs. xs = ys @ x # zs \ x \ set zs)"  haftmann@26734  1261  by (auto dest!: split_list_last)  nipkow@26073  1262 nipkow@26073  1263 lemma split_list_prop: "\x \ set xs. P x \ \ys x zs. xs = ys @ x # zs & P x"  nipkow@26073  1264 proof (induct xs)  nipkow@26073  1265  case Nil thus ?case by simp  nipkow@26073  1266 next  nipkow@26073  1267  case Cons thus ?case  nipkow@26073  1268  by(simp add:Bex_def)(metis append_Cons append.simps(1))  nipkow@26073  1269 qed  nipkow@26073  1270 nipkow@26073  1271 lemma split_list_propE:  haftmann@26734  1272  assumes "\x \ set xs. P x"  haftmann@26734  1273  obtains ys x zs where "xs = ys @ x # zs" and "P x"  haftmann@26734  1274 using split_list_prop [OF assms] by blast  nipkow@26073  1275 nipkow@26073  1276 lemma split_list_first_prop:  nipkow@26073  1277  "\x \ set xs. P x \  nipkow@26073  1278  \ys x zs. xs = ys@x#zs \ P x \ (\y \ set ys. \ P y)"  haftmann@26734  1279 proof (induct xs)  nipkow@26073  1280  case Nil thus ?case by simp  nipkow@26073  1281 next  nipkow@26073  1282  case (Cons x xs)  nipkow@26073  1283  show ?case  nipkow@26073  1284  proof cases  nipkow@26073  1285  assume "P x"  haftmann@40122  1286  thus ?thesis by simp (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)  nipkow@26073  1287  next  nipkow@26073  1288  assume "\ P x"  nipkow@26073  1289  hence "\x\set xs. P x" using Cons(2) by simp  nipkow@26073  1290  thus ?thesis using \ P x Cons(1) by (metis append_Cons set_ConsD)  nipkow@26073  1291  qed  nipkow@26073  1292 qed  nipkow@26073  1293 nipkow@26073  1294 lemma split_list_first_propE:  haftmann@26734  1295  assumes "\x \ set xs. P x"  haftmann@26734  1296  obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\y \ set ys. \ P y"  haftmann@26734  1297 using split_list_first_prop [OF assms] by blast  nipkow@26073  1298 nipkow@26073  1299 lemma split_list_first_prop_iff:  nipkow@26073  1300  "(\x \ set xs. P x) \  nipkow@26073  1301  (\ys x zs. xs = ys@x#zs \ P x \ (\y \ set ys. \ P y))"  haftmann@26734  1302 by (rule, erule split_list_first_prop) auto  nipkow@26073  1303 nipkow@26073  1304 lemma split_list_last_prop:  nipkow@26073  1305  "\x \ set xs. P x \  nipkow@26073  1306  \ys x zs. xs = ys@x#zs \ P x \ (\z \ set zs. \ P z)"  nipkow@26073  1307 proof(induct xs rule:rev_induct)  nipkow@26073  1308  case Nil thus ?case by simp  nipkow@26073  1309 next  nipkow@26073  1310  case (snoc x xs)  nipkow@26073  1311  show ?case  nipkow@26073  1312  proof cases  nipkow@26073  1313  assume "P x" thus ?thesis by (metis emptyE set_empty)  nipkow@26073  1314  next  nipkow@26073  1315  assume "\ P x"  nipkow@26073  1316  hence "\x\set xs. P x" using snoc(2) by simp  nipkow@44890  1317  thus ?thesis using \ P x snoc(1) by fastforce  nipkow@26073  1318  qed  nipkow@26073  1319 qed  nipkow@26073  1320 nipkow@26073  1321 lemma split_list_last_propE:  haftmann@26734  1322  assumes "\x \ set xs. P x"  haftmann@26734  1323  obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\z \ set zs. \ P z"  haftmann@26734  1324 using split_list_last_prop [OF assms] by blast  nipkow@26073  1325 nipkow@26073  1326 lemma split_list_last_prop_iff:  nipkow@26073  1327  "(\x \ set xs. P x) \  nipkow@26073  1328  (\ys x zs. xs = ys@x#zs \ P x \ (\z \ set zs. \ P z))"  haftmann@26734  1329 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)  nipkow@26073  1330 nipkow@26073  1331 lemma finite_list: "finite A ==> EX xs. set xs = A"  haftmann@26734  1332  by (erule finite_induct)  haftmann@26734  1333  (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))  paulson@13508  1334 kleing@14388  1335 lemma card_length: "card (set xs) \ length xs"  kleing@14388  1336 by (induct xs) (auto simp add: card_insert_if)  wenzelm@13114  1337 haftmann@26442  1338 lemma set_minus_filter_out:  haftmann@26442  1339  "set xs - {y} = set (filter (\x. \ (x = y)) xs)"  haftmann@26442  1340  by (induct xs) auto  paulson@15168  1341 wenzelm@35115  1342 haftmann@49948  1343 subsubsection {* @{const filter} *}  wenzelm@13114  1344 wenzelm@13142  1345 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"  nipkow@13145  1346 by (induct xs) auto  wenzelm@13114  1347 nipkow@15305  1348 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"  nipkow@15305  1349 by (induct xs) simp_all  nipkow@15305  1350 wenzelm@13142  1351 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\x. Q x \ P x) xs"  nipkow@13145  1352 by (induct xs) auto  wenzelm@13114  1353 nipkow@16998  1354 lemma length_filter_le [simp]: "length (filter P xs) \ length xs"  nipkow@16998  1355 by (induct xs) (auto simp add: le_SucI)  nipkow@16998  1356 nipkow@18423  1357 lemma sum_length_filter_compl:  nipkow@18423  1358  "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"  nipkow@18423  1359 by(induct xs) simp_all  nipkow@18423  1360 wenzelm@13142  1361 lemma filter_True [simp]: "\x \ set xs. P x ==> filter P xs = xs"  nipkow@13145  1362 by (induct xs) auto  wenzelm@13114  1363 wenzelm@13142  1364 lemma filter_False [simp]: "\x \ set xs. \ P x ==> filter P xs = []"  nipkow@13145  1365 by (induct xs) auto  wenzelm@13114  1366 nipkow@16998  1367 lemma filter_empty_conv: "(filter P xs = []) = (\x\set xs. \ P x)"  nipkow@24349  1368 by (induct xs) simp_all  nipkow@16998  1369 nipkow@16998  1370 lemma filter_id_conv: "(filter P xs = xs) = (\x\set xs. P x)"  nipkow@16998  1371 apply (induct xs)  nipkow@16998  1372  apply auto  nipkow@16998  1373 apply(cut_tac P=P and xs=xs in length_filter_le)  nipkow@16998  1374 apply simp  nipkow@16998  1375 done  wenzelm@13114  1376 nipkow@16965  1377 lemma filter_map:  nipkow@16965  1378  "filter P (map f xs) = map f (filter (P o f) xs)"  nipkow@16965  1379 by (induct xs) simp_all  nipkow@16965  1380 nipkow@16965  1381 lemma length_filter_map[simp]:  nipkow@16965  1382  "length (filter P (map f xs)) = length(filter (P o f) xs)"  nipkow@16965  1383 by (simp add:filter_map)  nipkow@16965  1384 wenzelm@13142  1385 lemma filter_is_subset [simp]: "set (filter P xs) \ set xs"  nipkow@13145  1386 by auto  wenzelm@13114  1387 nipkow@15246  1388 lemma length_filter_less:  nipkow@15246  1389  "\ x : set xs; ~ P x \ \ length(filter P xs) < length xs"  nipkow@15246  1390 proof (induct xs)  nipkow@15246  1391  case Nil thus ?case by simp  nipkow@15246  1392 next  nipkow@15246  1393  case (Cons x xs) thus ?case  nipkow@15246  1394  apply (auto split:split_if_asm)  nipkow@15246  1395  using length_filter_le[of P xs] apply arith  nipkow@15246  1396  done  nipkow@15246  1397 qed  wenzelm@13114  1398 nipkow@15281  1399 lemma length_filter_conv_card:  nipkow@15281  1400  "length(filter p xs) = card{i. i < length xs & p(xs!i)}"  nipkow@15281  1401 proof (induct xs)  nipkow@15281  1402  case Nil thus ?case by simp  nipkow@15281  1403 next  nipkow@15281  1404  case (Cons x xs)  nipkow@15281  1405  let ?S = "{i. i < length xs & p(xs!i)}"  nipkow@15281  1406  have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)  nipkow@15281  1407  show ?case (is "?l = card ?S'")  nipkow@15281  1408  proof (cases)  nipkow@15281  1409  assume "p x"  nipkow@15281  1410  hence eq: "?S' = insert 0 (Suc  ?S)"  nipkow@25162  1411  by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)  nipkow@15281  1412  have "length (filter p (x # xs)) = Suc(card ?S)"  wenzelm@23388  1413  using Cons p x by simp  nipkow@15281  1414  also have "\ = Suc(card(Suc  ?S))" using fin  huffman@44921  1415  by (simp add: card_image)  nipkow@15281  1416  also have "\ = card ?S'" using eq fin  nipkow@15281  1417  by (simp add:card_insert_if) (simp add:image_def)  nipkow@15281  1418  finally show ?thesis .  nipkow@15281  1419  next  nipkow@15281  1420  assume "\ p x"  nipkow@15281  1421  hence eq: "?S' = Suc  ?S"  nipkow@25162  1422  by(auto simp add: image_def split:nat.split elim:lessE)  nipkow@15281  1423  have "length (filter p (x # xs)) = card ?S"  wenzelm@23388  1424  using Cons \ p x by simp  nipkow@15281  1425  also have "\ = card(Suc  ?S)" using fin  huffman@44921  1426  by (simp add: card_image)  nipkow@15281  1427  also have "\ = card ?S'" using eq fin  nipkow@15281  1428  by (simp add:card_insert_if)  nipkow@15281  1429  finally show ?thesis .  nipkow@15281  1430  qed  nipkow@15281  1431 qed  nipkow@15281  1432 nipkow@17629  1433 lemma Cons_eq_filterD:  nipkow@17629  1434  "x#xs = filter P ys \  nipkow@17629  1435  \us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs"  wenzelm@19585  1436  (is "_ \ \us vs. ?P ys us vs")  nipkow@17629  1437 proof(induct ys)  nipkow@17629  1438  case Nil thus ?case by simp  nipkow@17629  1439 next  nipkow@17629  1440  case (Cons y ys)  nipkow@17629  1441  show ?case (is "\x. ?Q x")  nipkow@17629  1442  proof cases  nipkow@17629  1443  assume Py: "P y"  nipkow@17629  1444  show ?thesis  nipkow@17629  1445  proof cases  wenzelm@25221  1446  assume "x = y"  wenzelm@25221  1447  with Py Cons.prems have "?Q []" by simp  wenzelm@25221  1448  then show ?thesis ..  nipkow@17629  1449  next  wenzelm@25221  1450  assume "x \ y"  wenzelm@25221  1451  with Py Cons.prems show ?thesis by simp  nipkow@17629  1452  qed  nipkow@17629  1453  next  wenzelm@25221  1454  assume "\ P y"  nipkow@44890  1455  with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastforce  wenzelm@25221  1456  then have "?Q (y#us)" by simp  wenzelm@25221  1457  then show ?thesis ..  nipkow@17629  1458  qed  nipkow@17629  1459 qed  nipkow@17629  1460 nipkow@17629  1461 lemma filter_eq_ConsD:  nipkow@17629  1462  "filter P ys = x#xs \  nipkow@17629  1463  \us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs"  nipkow@17629  1464 by(rule Cons_eq_filterD) simp  nipkow@17629  1465 nipkow@17629  1466 lemma filter_eq_Cons_iff:  nipkow@17629  1467  "(filter P ys = x#xs) =  nipkow@17629  1468  (\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)"  nipkow@17629  1469 by(auto dest:filter_eq_ConsD)  nipkow@17629  1470 nipkow@17629  1471 lemma Cons_eq_filter_iff:  nipkow@17629  1472  "(x#xs = filter P ys) =  nipkow@17629  1473  (\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)"  nipkow@17629  1474 by(auto dest:Cons_eq_filterD)  nipkow@17629  1475 krauss@44013  1476 lemma filter_cong[fundef_cong]:  nipkow@17501  1477  "xs = ys \ (\x. x \ set ys \ P x = Q x) \ filter P xs = filter Q ys"  nipkow@17501  1478 apply simp  nipkow@17501  1479 apply(erule thin_rl)  nipkow@17501  1480 by (induct ys) simp_all  nipkow@17501  1481 nipkow@15281  1482 haftmann@26442  1483 subsubsection {* List partitioning *}  haftmann@26442  1484 haftmann@26442  1485 primrec partition :: "('a \ bool) \'a list \ 'a list \ 'a list" where  nipkow@50548  1486 "partition P [] = ([], [])" |  nipkow@50548  1487 "partition P (x # xs) =  nipkow@50548  1488  (let (yes, no) = partition P xs  nipkow@50548  1489  in if P x then (x # yes, no) else (yes, x # no))"  haftmann@26442  1490 haftmann@26442  1491 lemma partition_filter1:  haftmann@26442  1492  "fst (partition P xs) = filter P xs"  haftmann@26442  1493 by (induct xs) (auto simp add: Let_def split_def)  haftmann@26442  1494 haftmann@26442  1495 lemma partition_filter2:  haftmann@26442  1496  "snd (partition P xs) = filter (Not o P) xs"  haftmann@26442  1497 by (induct xs) (auto simp add: Let_def split_def)  haftmann@26442  1498 haftmann@26442  1499 lemma partition_P:  haftmann@26442  1500  assumes "partition P xs = (yes, no)"  haftmann@26442  1501  shows "(\p \ set yes. P p) \ (\p \ set no. \ P p)"  haftmann@26442  1502 proof -  haftmann@26442  1503  from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"  haftmann@26442  1504  by simp_all  haftmann@26442  1505  then show ?thesis by (simp_all add: partition_filter1 partition_filter2)  haftmann@26442  1506 qed  haftmann@26442  1507 haftmann@26442  1508 lemma partition_set:  haftmann@26442  1509  assumes "partition P xs = (yes, no)"  haftmann@26442  1510  shows "set yes \ set no = set xs"  haftmann@26442  1511 proof -  haftmann@26442  1512  from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"  haftmann@26442  1513  by simp_all  haftmann@26442  1514  then show ?thesis by (auto simp add: partition_filter1 partition_filter2)  haftmann@26442  1515 qed  haftmann@26442  1516 hoelzl@33639  1517 lemma partition_filter_conv[simp]:  hoelzl@33639  1518  "partition f xs = (filter f xs,filter (Not o f) xs)"  hoelzl@33639  1519 unfolding partition_filter2[symmetric]  hoelzl@33639  1520 unfolding partition_filter1[symmetric] by simp  hoelzl@33639  1521 hoelzl@33639  1522 declare partition.simps[simp del]  haftmann@26442  1523 wenzelm@35115  1524 haftmann@49948  1525 subsubsection {* @{const concat} *}  wenzelm@13114  1526 wenzelm@13142  1527 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"  nipkow@13145  1528 by (induct xs) auto  wenzelm@13114  1529 paulson@18447  1530 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\xs \ set xss. xs = [])"  nipkow@13145  1531 by (induct xss) auto  wenzelm@13114  1532 paulson@18447  1533 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\xs \ set xss. xs = [])"  nipkow@13145  1534 by (induct xss) auto  wenzelm@13114  1535 nipkow@24308  1536 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"  nipkow@13145  1537 by (induct xs) auto  wenzelm@13114  1538 nipkow@24476  1539 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"  nipkow@24349  1540 by (induct xs) auto  nipkow@24349  1541 wenzelm@13142  1542 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"  nipkow@13145  1543 by (induct xs) auto  wenzelm@13114  1544 wenzelm@13142  1545 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"  nipkow@13145  1546 by (induct xs) auto  wenzelm@13114  1547 wenzelm@13142  1548 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"  nipkow@13145  1549 by (induct xs) auto  wenzelm@13114  1550 bulwahn@40365  1551 lemma concat_eq_concat_iff: "\(x, y) \ set (zip xs ys). length x = length y ==> length xs = length ys ==> (concat xs = concat ys) = (xs = ys)"  bulwahn@40365  1552 proof (induct xs arbitrary: ys)  bulwahn@40365  1553  case (Cons x xs ys)  bulwahn@40365  1554  thus ?case by (cases ys) auto  bulwahn@40365  1555 qed (auto)  bulwahn@40365  1556 bulwahn@40365  1557 lemma concat_injective: "concat xs = concat ys ==> length xs = length ys ==> \(x, y) \ set (zip xs ys). length x = length y ==> xs = ys"  bulwahn@40365  1558 by (simp add: concat_eq_concat_iff)  bulwahn@40365  1559 wenzelm@13114  1560 haftmann@49948  1561 subsubsection {* @{const nth} *}  wenzelm@13114  1562 haftmann@29827  1563 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"  nipkow@13145  1564 by auto  wenzelm@13114  1565 haftmann@29827  1566 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"  nipkow@13145  1567 by auto  wenzelm@13114  1568 wenzelm@13142  1569 declare nth.simps [simp del]  wenzelm@13114  1570 nipkow@41842  1571 lemma nth_Cons_pos[simp]: "0 < n \ (x#xs) ! n = xs ! (n - 1)"  nipkow@41842  1572 by(auto simp: Nat.gr0_conv_Suc)  nipkow@41842  1573 wenzelm@13114  1574 lemma nth_append:  nipkow@24526  1575  "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"  nipkow@24526  1576 apply (induct xs arbitrary: n, simp)  paulson@14208  1577 apply (case_tac n, auto)  nipkow@13145  1578 done  wenzelm@13114  1579 nipkow@14402  1580 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"  wenzelm@25221  1581 by (induct xs) auto  nipkow@14402  1582 nipkow@14402  1583 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"  wenzelm@25221  1584 by (induct xs) auto  nipkow@14402  1585 nipkow@24526  1586 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"  nipkow@24526  1587 apply (induct xs arbitrary: n, simp)  paulson@14208  1588 apply (case_tac n, auto)  nipkow@13145  1589 done  wenzelm@13114  1590 noschinl@45841  1591 lemma nth_tl:  noschinl@45841  1592  assumes "n < length (tl x)" shows "tl x ! n = x ! Suc n"  noschinl@45841  1593 using assms by (induct x) auto  noschinl@45841  1594 nipkow@18423  1595 lemma hd_conv_nth: "xs \ [] \ hd xs = xs!0"  nipkow@18423  1596 by(cases xs) simp_all  nipkow@18423  1597 nipkow@18049  1598 nipkow@18049  1599 lemma list_eq_iff_nth_eq:  nipkow@24526  1600  "(xs = ys) = (length xs = length ys \ (ALL i set xs) = (\i < length xs. xs!i = x)"  nipkow@17501  1618 by(auto simp:set_conv_nth)  nipkow@17501  1619 haftmann@51160  1620 lemma nth_equal_first_eq:  haftmann@51160  1621  assumes "x \ set xs"  haftmann@51160  1622  assumes "n \ length xs"  haftmann@51160  1623  shows "(x # xs) ! n = x \ n = 0" (is "?lhs \ ?rhs")  haftmann@51160  1624 proof  haftmann@51160  1625  assume ?lhs  haftmann@51160  1626  show ?rhs  haftmann@51160  1627  proof (rule ccontr)  haftmann@51160  1628  assume "n \ 0"  haftmann@51160  1629  then have "n > 0" by simp  haftmann@51160  1630  with ?lhs have "xs ! (n - 1) = x" by simp  haftmann@51160  1631  moreover from n > 0 n \ length xs have "n - 1 < length xs" by simp  haftmann@51160  1632  ultimately have "\i set xs in_set_conv_nth [of x xs] show False by simp  haftmann@51160  1634  qed  haftmann@51160  1635 next  haftmann@51160  1636  assume ?rhs then show ?lhs by simp  haftmann@51160  1637 qed  haftmann@51160  1638 haftmann@51160  1639 lemma nth_non_equal_first_eq:  haftmann@51160  1640  assumes "x \ y"  haftmann@51160  1641  shows "(x # xs) ! n = y \ xs ! (n - 1) = y \ n > 0" (is "?lhs \ ?rhs")  haftmann@51160  1642 proof  haftmann@51160  1643  assume "?lhs" with assms have "n > 0" by (cases n) simp_all  haftmann@51160  1644  with ?lhs show ?rhs by simp  haftmann@51160  1645 next  haftmann@51160  1646  assume "?rhs" then show "?lhs" by simp  haftmann@51160  1647 qed  haftmann@51160  1648 nipkow@13145  1649 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"  nipkow@13145  1650 by (auto simp add: set_conv_nth)  wenzelm@13114  1651 wenzelm@13142  1652 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"  nipkow@13145  1653 by (auto simp add: set_conv_nth)  wenzelm@13114  1654 wenzelm@13114  1655 lemma all_nth_imp_all_set:  nipkow@13145  1656 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"  nipkow@13145  1657 by (auto simp add: set_conv_nth)  wenzelm@13114  1658 wenzelm@13114  1659 lemma all_set_conv_all_nth:  nipkow@13145  1660 "(\x \ set xs. P x) = (\i. i < length xs --> P (xs ! i))"  nipkow@13145  1661 by (auto simp add: set_conv_nth)  wenzelm@13114  1662 kleing@25296  1663 lemma rev_nth:  kleing@25296  1664  "n < size xs \ rev xs ! n = xs ! (length xs - Suc n)"  kleing@25296  1665 proof (induct xs arbitrary: n)  kleing@25296  1666  case Nil thus ?case by simp  kleing@25296  1667 next  kleing@25296  1668  case (Cons x xs)  kleing@25296  1669  hence n: "n < Suc (length xs)" by simp  kleing@25296  1670  moreover  kleing@25296  1671  { assume "n < length xs"  kleing@25296  1672  with n obtain n' where "length xs - n = Suc n'"  kleing@25296  1673  by (cases "length xs - n", auto)  kleing@25296  1674  moreover  kleing@25296  1675  then have "length xs - Suc n = n'" by simp  kleing@25296  1676  ultimately  kleing@25296  1677  have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp  kleing@25296  1678  }  kleing@25296  1679  ultimately  kleing@25296  1680  show ?case by (clarsimp simp add: Cons nth_append)  kleing@25296  1681 qed  wenzelm@13114  1682 nipkow@31159  1683 lemma Skolem_list_nth:  nipkow@31159  1684  "(ALL i (xs[i:=x])!j = (if i = j then x else xs!j)"  nipkow@24526  1709 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)  wenzelm@13114  1710 wenzelm@13142  1711 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"  nipkow@13145  1712 by (simp add: nth_list_update)  wenzelm@13114  1713 nipkow@24526  1714 lemma nth_list_update_neq [simp]: "i \ j ==> xs[i:=x]!j = xs!j"  nipkow@24526  1715 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)  wenzelm@13114  1716 nipkow@24526  1717 lemma list_update_id[simp]: "xs[i := xs!i] = xs"  nipkow@24526  1718 by (induct xs arbitrary: i) (simp_all split:nat.splits)  nipkow@24526  1719 nipkow@24526  1720 lemma list_update_beyond[simp]: "length xs \ i \ xs[i:=x] = xs"  nipkow@24526  1721 apply (induct xs arbitrary: i)  nipkow@17501  1722  apply simp  nipkow@17501  1723 apply (case_tac i)  nipkow@17501  1724 apply simp_all  nipkow@17501  1725 done  nipkow@17501  1726 nipkow@31077  1727 lemma list_update_nonempty[simp]: "xs[k:=x] = [] \ xs=[]"  nipkow@31077  1728 by(metis length_0_conv length_list_update)  nipkow@31077  1729 wenzelm@13114  1730 lemma list_update_same_conv:  nipkow@24526  1731 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"  nipkow@24526  1732 by (induct xs arbitrary: i) (auto split: nat.split)  wenzelm@13114  1733 nipkow@14187  1734 lemma list_update_append1:  nipkow@24526  1735  "i < size xs \ (xs @ ys)[i:=x] = xs[i:=x] @ ys"  nipkow@24526  1736 apply (induct xs arbitrary: i, simp)  nipkow@14187  1737 apply(simp split:nat.split)  nipkow@14187  1738 done  nipkow@14187  1739 kleing@15868  1740 lemma list_update_append:  nipkow@24526  1741  "(xs @ ys) [n:= x] =  kleing@15868  1742  (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"  nipkow@24526  1743 by (induct xs arbitrary: n) (auto split:nat.splits)  kleing@15868  1744 nipkow@14402  1745 lemma list_update_length [simp]:  nipkow@14402  1746  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"  nipkow@14402  1747 by (induct xs, auto)  nipkow@14402  1748 nipkow@31264  1749 lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"  nipkow@31264  1750 by(induct xs arbitrary: k)(auto split:nat.splits)  nipkow@31264  1751 nipkow@31264  1752 lemma rev_update:  nipkow@31264  1753  "k < length xs \ rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"  nipkow@31264  1754 by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)  nipkow@31264  1755 wenzelm@13114  1756 lemma update_zip:  nipkow@31080  1757  "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"  nipkow@24526  1758 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)  nipkow@24526  1759 nipkow@24526  1760 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"  nipkow@24526  1761 by (induct xs arbitrary: i) (auto split: nat.split)  wenzelm@13114  1762 wenzelm@13114  1763 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"  nipkow@13145  1764 by (blast dest!: set_update_subset_insert [THEN subsetD])  wenzelm@13114  1765 nipkow@24526  1766 lemma set_update_memI: "n < length xs \ x \ set (xs[n := x])"  nipkow@24526  1767 by (induct xs arbitrary: n) (auto split:nat.splits)  kleing@15868  1768 nipkow@31077  1769 lemma list_update_overwrite[simp]:  haftmann@24796  1770  "xs [i := x, i := y] = xs [i := y]"  nipkow@31077  1771 apply (induct xs arbitrary: i) apply simp  nipkow@31077  1772 apply (case_tac i, simp_all)  haftmann@24796  1773 done  haftmann@24796  1774 haftmann@24796  1775 lemma list_update_swap:  haftmann@24796  1776  "i \ i' \ xs [i := x, i' := x'] = xs [i' := x', i := x]"  haftmann@24796  1777 apply (induct xs arbitrary: i i')  haftmann@24796  1778 apply simp  haftmann@24796  1779 apply (case_tac i, case_tac i')  haftmann@24796  1780 apply auto  haftmann@24796  1781 apply (case_tac i')  haftmann@24796  1782 apply auto  haftmann@24796  1783 done  haftmann@24796  1784 haftmann@29827  1785 lemma list_update_code [code]:  haftmann@29827  1786  "[][i := y] = []"  haftmann@29827  1787  "(x # xs)[0 := y] = y # xs"  haftmann@29827  1788  "(x # xs)[Suc i := y] = x # xs[i := y]"  haftmann@29827  1789  by simp_all  haftmann@29827  1790 wenzelm@13114  1791 haftmann@49948  1792 subsubsection {* @{const last} and @{const butlast} *}  wenzelm@13114  1793 wenzelm@13142  1794 lemma last_snoc [simp]: "last (xs @ [x]) = x"  nipkow@13145  1795 by (induct xs) auto  wenzelm@13114  1796 wenzelm@13142  1797 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"  nipkow@13145  1798 by (induct xs) auto  wenzelm@13114  1799 nipkow@14302  1800 lemma last_ConsL: "xs = [] \ last(x#xs) = x"  huffman@44921  1801  by simp  nipkow@14302  1802 nipkow@14302  1803 lemma last_ConsR: "xs \ [] \ last(x#xs) = last xs"  huffman@44921  1804  by simp  nipkow@14302  1805 nipkow@14302  1806 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"  nipkow@14302  1807 by (induct xs) (auto)  nipkow@14302  1808 nipkow@14302  1809 lemma last_appendL[simp]: "ys = [] \ last(xs @ ys) = last xs"  nipkow@14302  1810 by(simp add:last_append)  nipkow@14302  1811 nipkow@14302  1812 lemma last_appendR[simp]: "ys \ [] \ last(xs @ ys) = last ys"  nipkow@14302  1813 by(simp add:last_append)  nipkow@14302  1814 noschinl@45841  1815 lemma last_tl: "xs = [] \ tl xs \ [] \last (tl xs) = last xs"  noschinl@45841  1816 by (induct xs) simp_all  noschinl@45841  1817 noschinl@45841  1818 lemma butlast_tl: "butlast (tl xs) = tl (butlast xs)"  noschinl@45841  1819 by (induct xs) simp_all  noschinl@45841  1820 nipkow@17762  1821 lemma hd_rev: "xs \ [] \ hd(rev xs) = last xs"  nipkow@17762  1822 by(rule rev_exhaust[of xs]) simp_all  nipkow@17762  1823 nipkow@17762  1824 lemma last_rev: "xs \ [] \ last(rev xs) = hd xs"  nipkow@17762  1825 by(cases xs) simp_all  nipkow@17762  1826 nipkow@17765  1827 lemma last_in_set[simp]: "as \ [] \ last as \ set as"  nipkow@17765  1828 by (induct as) auto  nipkow@17762  1829 wenzelm@13142  1830 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"  nipkow@13145  1831 by (induct xs rule: rev_induct) auto  wenzelm@13114  1832 wenzelm@13114  1833 lemma butlast_append:  nipkow@24526  1834  "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"  nipkow@24526  1835 by (induct xs arbitrary: ys) auto  wenzelm@13114  1836 wenzelm@13142  1837 lemma append_butlast_last_id [simp]:  nipkow@13145  1838 "xs \ [] ==> butlast xs @ [last xs] = xs"  nipkow@13145  1839 by (induct xs) auto  wenzelm@13114  1840 wenzelm@13142  1841 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"  nipkow@13145  1842 by (induct xs) (auto split: split_if_asm)  wenzelm@13114  1843 wenzelm@13114  1844 lemma in_set_butlast_appendI:  nipkow@13145  1845 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"  nipkow@13145  1846 by (auto dest: in_set_butlastD simp add: butlast_append)  wenzelm@13114  1847 nipkow@24526  1848 lemma last_drop[simp]: "n < length xs \ last (drop n xs) = last xs"  nipkow@24526  1849 apply (induct xs arbitrary: n)  nipkow@17501  1850  apply simp  nipkow@17501  1851 apply (auto split:nat.split)  nipkow@17501  1852 done  nipkow@17501  1853 noschinl@45841  1854 lemma nth_butlast:  noschinl@45841  1855  assumes "n < length (butlast xs)" shows "butlast xs ! n = xs ! n"  noschinl@45841  1856 proof (cases xs)  noschinl@45841  1857  case (Cons y ys)  noschinl@45841  1858  moreover from assms have "butlast xs ! n = (butlast xs @ [last xs]) ! n"  noschinl@45841  1859  by (simp add: nth_append)  noschinl@45841  1860  ultimately show ?thesis using append_butlast_last_id by simp  noschinl@45841  1861 qed simp  noschinl@45841  1862 huffman@30128  1863 lemma last_conv_nth: "xs\[] \ last xs = xs!(length xs - 1)"  nipkow@17589  1864 by(induct xs)(auto simp:neq_Nil_conv)  nipkow@17589  1865 huffman@30128  1866 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"  huffman@26584  1867 by (induct xs, simp, case_tac xs, simp_all)  huffman@26584  1868 nipkow@31077  1869 lemma last_list_update:  nipkow@31077  1870  "xs \ [] \ last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"  nipkow@31077  1871 by (auto simp: last_conv_nth)  nipkow@31077  1872 nipkow@31077  1873 lemma butlast_list_update:  nipkow@31077  1874  "butlast(xs[k:=x]) =  nipkow@31077  1875  (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"  nipkow@31077  1876 apply(cases xs rule:rev_cases)  nipkow@31077  1877 apply simp  nipkow@31077  1878 apply(simp add:list_update_append split:nat.splits)  nipkow@31077  1879 done  nipkow@31077  1880 haftmann@36851  1881 lemma last_map:  haftmann@36851  1882  "xs \ [] \ last (map f xs) = f (last xs)"  haftmann@36851  1883  by (cases xs rule: rev_cases) simp_all  haftmann@36851  1884 haftmann@36851  1885 lemma map_butlast:  haftmann@36851  1886  "map f (butlast xs) = butlast (map f xs)"  haftmann@36851  1887  by (induct xs) simp_all  haftmann@36851  1888 nipkow@40230  1889 lemma snoc_eq_iff_butlast:  nipkow@40230  1890  "xs @ [x] = ys \ (ys \ [] & butlast ys = xs & last ys = x)"  nipkow@40230  1891 by (metis append_butlast_last_id append_is_Nil_conv butlast_snoc last_snoc not_Cons_self)  nipkow@40230  1892 haftmann@24796  1893 haftmann@49948  1894 subsubsection {* @{const take} and @{const drop} *}  wenzelm@13114  1895 wenzelm@13142  1896 lemma take_0 [simp]: "take 0 xs = []"  nipkow@13145  1897 by (induct xs) auto  wenzelm@13114  1898 wenzelm@13142  1899 lemma drop_0 [simp]: "drop 0 xs = xs"  nipkow@13145  1900 by (induct xs) auto  wenzelm@13114  1901 wenzelm@13142  1902 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"  nipkow@13145  1903 by simp  wenzelm@13114  1904 wenzelm@13142  1905 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"  nipkow@13145  1906 by simp  wenzelm@13114  1907 wenzelm@13142  1908 declare take_Cons [simp del] and drop_Cons [simp del]  wenzelm@13114  1909 huffman@30128  1910 lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"  huffman@30128  1911  unfolding One_nat_def by simp  huffman@30128  1912 huffman@30128  1913 lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"  huffman@30128  1914  unfolding One_nat_def by simp  huffman@30128  1915 nipkow@15110  1916 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"  nipkow@15110  1917 by(clarsimp simp add:neq_Nil_conv)  nipkow@15110  1918 nipkow@14187  1919 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"  nipkow@14187  1920 by(cases xs, simp_all)  nipkow@14187  1921 huffman@26584  1922 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"  huffman@26584  1923 by (induct xs arbitrary: n) simp_all  huffman@26584  1924 nipkow@24526  1925 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"  nipkow@24526  1926 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)  nipkow@24526  1927 huffman@26584  1928 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"  huffman@26584  1929 by (cases n, simp, cases xs, auto)  huffman@26584  1930 huffman@26584  1931 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"  huffman@26584  1932 by (simp only: drop_tl)  huffman@26584  1933 nipkow@24526  1934 lemma nth_via_drop: "drop n xs = y#ys \ xs!n = y"  nipkow@24526  1935 apply (induct xs arbitrary: n, simp)  nipkow@14187  1936 apply(simp add:drop_Cons nth_Cons split:nat.splits)  nipkow@14187  1937 done  nipkow@14187  1938 nipkow@13913  1939 lemma take_Suc_conv_app_nth:  nipkow@24526  1940  "i < length xs \ take (Suc i) xs = take i xs @ [xs!i]"  nipkow@24526  1941 apply (induct xs arbitrary: i, simp)  paulson@14208  1942 apply (case_tac i, auto)  nipkow@13913  1943 done  nipkow@13913  1944 mehta@14591  1945 lemma drop_Suc_conv_tl:  nipkow@24526  1946  "i < length xs \ (xs!i) # (drop (Suc i) xs) = drop i xs"  nipkow@24526  1947 apply (induct xs arbitrary: i, simp)  mehta@14591  1948 apply (case_tac i, auto)  mehta@14591  1949 done  mehta@14591  1950 nipkow@24526  1951 lemma length_take [simp]: "length (take n xs) = min (length xs) n"  nipkow@24526  1952 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  nipkow@24526  1953 nipkow@24526  1954 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"  nipkow@24526  1955 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  nipkow@24526  1956 nipkow@24526  1957 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"  nipkow@24526  1958 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  nipkow@24526  1959 nipkow@24526  1960 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"  nipkow@24526  1961 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  wenzelm@13114  1962 wenzelm@13142  1963 lemma take_append [simp]:  nipkow@24526  1964  "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"  nipkow@24526  1965 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  wenzelm@13114  1966 wenzelm@13142  1967 lemma drop_append [simp]:  nipkow@24526  1968  "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"  nipkow@24526  1969 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  nipkow@24526  1970 nipkow@24526  1971 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"  nipkow@24526  1972 apply (induct m arbitrary: xs n, auto)  paulson@14208  1973 apply (case_tac xs, auto)  nipkow@15236  1974 apply (case_tac n, auto)  nipkow@13145  1975 done  wenzelm@13114  1976 nipkow@24526  1977 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"  nipkow@24526  1978 apply (induct m arbitrary: xs, auto)  paulson@14208  1979 apply (case_tac xs, auto)  nipkow@13145  1980 done  wenzelm@13114  1981 nipkow@24526  1982 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"  nipkow@24526  1983 apply (induct m arbitrary: xs n, auto)  paulson@14208  1984 apply (case_tac xs, auto)  nipkow@13145  1985 done  wenzelm@13114  1986 nipkow@24526  1987 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"  nipkow@24526  1988 apply(induct xs arbitrary: m n)  nipkow@14802  1989  apply simp  nipkow@14802  1990 apply(simp add: take_Cons drop_Cons split:nat.split)  nipkow@14802  1991 done  nipkow@14802  1992 nipkow@24526  1993 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"  nipkow@24526  1994 apply (induct n arbitrary: xs, auto)  paulson@14208  1995 apply (case_tac xs, auto)  nipkow@13145  1996 done  wenzelm@13114  1997 nipkow@24526  1998 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \ xs = [])"  nipkow@24526  1999 apply(induct xs arbitrary: n)  nipkow@15110  2000  apply simp  nipkow@15110  2001 apply(simp add:take_Cons split:nat.split)  nipkow@15110  2002 done  nipkow@15110  2003 nipkow@24526  2004 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"  nipkow@24526  2005 apply(induct xs arbitrary: n)  nipkow@15110  2006 apply simp  nipkow@15110  2007 apply(simp add:drop_Cons split:nat.split)  nipkow@15110  2008 done  nipkow@15110  2009 nipkow@24526  2010 lemma take_map: "take n (map f xs) = map f (take n xs)"  nipkow@24526  2011 apply (induct n arbitrary: xs, auto)  paulson@14208  2012 apply (case_tac xs, auto)  nipkow@13145  2013 done  wenzelm@13114  2014 nipkow@24526  2015 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"  nipkow@24526  2016 apply (induct n arbitrary: xs, auto)  paulson@14208  2017 apply (case_tac xs, auto)  nipkow@13145  2018 done  wenzelm@13114  2019 nipkow@24526  2020 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"  nipkow@24526  2021 apply (induct xs arbitrary: i, auto)  paulson@14208  2022 apply (case_tac i, auto)  nipkow@13145  2023 done  wenzelm@13114  2024 nipkow@24526  2025 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"  nipkow@24526  2026 apply (induct xs arbitrary: i, auto)  paulson@14208  2027 apply (case_tac i, auto)  nipkow@13145  2028 done  wenzelm@13114  2029 nipkow@24526  2030 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"  nipkow@24526  2031 apply (induct xs arbitrary: i n, auto)  paulson@14208  2032 apply (case_tac n, blast)  paulson@14208  2033 apply (case_tac i, auto)  nipkow@13145  2034 done  wenzelm@13114  2035 wenzelm@13142  2036 lemma nth_drop [simp]:  nipkow@24526  2037  "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"  nipkow@24526  2038 apply (induct n arbitrary: xs i, auto)  paulson@14208  2039 apply (case_tac xs, auto)  nipkow@13145  2040 done  nipkow@3507  2041 huffman@26584  2042 lemma butlast_take:  huffman@30128  2043  "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"  huffman@26584  2044 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)  huffman@26584  2045 huffman@26584  2046 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"  huffman@30128  2047 by (simp add: butlast_conv_take drop_take add_ac)  huffman@26584  2048 huffman@26584  2049 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"  huffman@26584  2050 by (simp add: butlast_conv_take min_max.inf_absorb1)  huffman@26584  2051 huffman@26584  2052 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"  huffman@30128  2053 by (simp add: butlast_conv_take drop_take add_ac)  huffman@26584  2054 bulwahn@46500  2055 lemma hd_drop_conv_nth: "n < length xs \ hd(drop n xs) = xs!n"  nipkow@18423  2056 by(simp add: hd_conv_nth)  nipkow@18423  2057 nipkow@35248  2058 lemma set_take_subset_set_take:  nipkow@35248  2059  "m <= n \ set(take m xs) <= set(take n xs)"  bulwahn@41463  2060 apply (induct xs arbitrary: m n)  bulwahn@41463  2061 apply simp  bulwahn@41463  2062 apply (case_tac n)  bulwahn@41463  2063 apply (auto simp: take_Cons)  bulwahn@41463  2064 done  nipkow@35248  2065 nipkow@24526  2066 lemma set_take_subset: "set(take n xs) \ set xs"  nipkow@24526  2067 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)  nipkow@24526  2068 nipkow@24526  2069 lemma set_drop_subset: "set(drop n xs) \ set xs"  nipkow@24526  2070 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)  nipkow@14025  2071 nipkow@35248  2072 lemma set_drop_subset_set_drop:  nipkow@35248  2073  "m >= n \ set(drop m xs) <= set(drop n xs)"  nipkow@35248  2074 apply(induct xs arbitrary: m n)  nipkow@35248  2075 apply(auto simp:drop_Cons split:nat.split)  nipkow@35248  2076 apply (metis set_drop_subset subset_iff)  nipkow@35248  2077 done  nipkow@35248  2078 nipkow@14187  2079 lemma in_set_takeD: "x : set(take n xs) \ x : set xs"  nipkow@14187  2080 using set_take_subset by fast  nipkow@14187  2081 nipkow@14187  2082 lemma in_set_dropD: "x : set(drop n xs) \ x : set xs"  nipkow@14187  2083 using set_drop_subset by fast  nipkow@14187  2084 wenzelm@13114  2085 lemma append_eq_conv_conj:  nipkow@24526  2086  "(xs @ ys = zs) = (xs = take (length xs) zs \ ys = drop (length xs) zs)"  nipkow@24526  2087 apply (induct xs arbitrary: zs, simp, clarsimp)  paulson@14208  2088 apply (case_tac zs, auto)  nipkow@13145  2089 done  wenzelm@13142  2090 nipkow@24526  2091 lemma take_add:  noschinl@42713  2092  "take (i+j) xs = take i xs @ take j (drop i xs)"  nipkow@24526  2093 apply (induct xs arbitrary: i, auto)  nipkow@24526  2094 apply (case_tac i, simp_all)  paulson@14050  2095 done  paulson@14050  2096 nipkow@14300  2097 lemma append_eq_append_conv_if:  nipkow@24526  2098  "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =  nipkow@14300  2099  (if size xs\<^isub>1 \ size ys\<^isub>1  nipkow@14300  2100  then xs\<^isub>1 = take (size xs\<^isub>1) ys\<^isub>1 \ xs\<^isub>2 = drop (size xs\<^isub>1) ys\<^isub>1 @ ys\<^isub>2  nipkow@14300  2101  else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \ drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)"  nipkow@24526  2102 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)  nipkow@14300  2103  apply simp  nipkow@14300  2104 apply(case_tac ys\<^isub>1)  nipkow@14300  2105 apply simp_all  nipkow@14300  2106 done  nipkow@14300  2107 nipkow@15110  2108 lemma take_hd_drop:  huffman@30079  2109  "n < length xs \ take n xs @ [hd (drop n xs)] = take (Suc n) xs"  nipkow@24526  2110 apply(induct xs arbitrary: n)  nipkow@15110  2111 apply simp  nipkow@15110  2112 apply(simp add:drop_Cons split:nat.split)  nipkow@15110  2113 done  nipkow@15110  2114 nipkow@17501  2115 lemma id_take_nth_drop:  nipkow@17501  2116  "i < length xs \ xs = take i xs @ xs!i # drop (Suc i) xs"  nipkow@17501  2117 proof -  nipkow@17501  2118  assume si: "i < length xs"  nipkow@17501  2119  hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto  nipkow@17501  2120  moreover  nipkow@17501  2121  from si have "take (Suc i) xs = take i xs @ [xs!i]"  nipkow@17501  2122  apply (rule_tac take_Suc_conv_app_nth) by arith  nipkow@17501  2123  ultimately show ?thesis by auto  nipkow@17501  2124 qed  nipkow@17501  2125   nipkow@17501  2126 lemma upd_conv_take_nth_drop:  nipkow@17501  2127  "i < length xs \ xs[i:=a] = take i xs @ a # drop (Suc i) xs"  nipkow@17501  2128 proof -  nipkow@17501  2129  assume i: "i < length xs"  nipkow@17501  2130  have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"  nipkow@17501  2131  by(rule arg_cong[OF id_take_nth_drop[OF i]])  nipkow@17501  2132  also have "\ = take i xs @ a # drop (Suc i) xs"  nipkow@17501  2133  using i by (simp add: list_update_append)  nipkow@17501  2134  finally show ?thesis .  nipkow@17501  2135 qed  nipkow@17501  2136 haftmann@24796  2137 lemma nth_drop':  haftmann@24796  2138  "i < length xs \ xs ! i # drop (Suc i) xs = drop i xs"  haftmann@24796  2139 apply (induct i arbitrary: xs)  haftmann@24796  2140 apply (simp add: neq_Nil_conv)  haftmann@24796  2141 apply (erule exE)+  haftmann@24796  2142 apply simp  haftmann@24796  2143 apply (case_tac xs)  haftmann@24796  2144 apply simp_all  haftmann@24796  2145 done  haftmann@24796  2146 wenzelm@13114  2147 haftmann@49948  2148 subsubsection {* @{const takeWhile} and @{const dropWhile} *}  wenzelm@13114  2149 hoelzl@33639  2150 lemma length_takeWhile_le: "length (takeWhile P xs) \ length xs"  hoelzl@33639  2151  by (induct xs) auto  hoelzl@33639  2152 wenzelm@13142  2153 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"  nipkow@13145  2154 by (induct xs) auto  wenzelm@13114  2155 wenzelm@13142  2156 lemma takeWhile_append1 [simp]:  nipkow@13145  2157 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"  nipkow@13145  2158 by (induct xs) auto  wenzelm@13114  2159 wenzelm@13142  2160 lemma takeWhile_append2 [simp]:  nipkow@13145  2161 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"  nipkow@13145  2162 by (induct xs) auto  wenzelm@13114  2163 wenzelm@13142  2164 lemma takeWhile_tail: "\ P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"  nipkow@13145  2165 by (induct xs) auto  wenzelm@13114  2166 hoelzl@33639  2167 lemma takeWhile_nth: "j < length (takeWhile P xs) \ takeWhile P xs ! j = xs ! j"  hoelzl@33639  2168 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto  hoelzl@33639  2169 hoelzl@33639  2170 lemma dropWhile_nth: "j < length (dropWhile P xs) \ dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"  hoelzl@33639  2171 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto  hoelzl@33639  2172 hoelzl@33639  2173 lemma length_dropWhile_le: "length (dropWhile P xs) \ length xs"  hoelzl@33639  2174 by (induct xs) auto  hoelzl@33639  2175 wenzelm@13142  2176 lemma dropWhile_append1 [simp]:  nipkow@13145  2177 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"  nipkow@13145  2178 by (induct xs) auto  wenzelm@13114  2179 wenzelm@13142  2180 lemma dropWhile_append2 [simp]:  nipkow@13145  2181 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"  nipkow@13145  2182 by (induct xs) auto  wenzelm@13114  2183 noschinl@45841  2184 lemma dropWhile_append3:  noschinl@45841  2185  "\ P y \dropWhile P (xs @ y # ys) = dropWhile P xs @ y # ys"  noschinl@45841  2186 by (induct xs) auto  noschinl@45841  2187 noschinl@45841  2188 lemma dropWhile_last:  noschinl@45841  2189  "x \ set xs \ \ P x \ last (dropWhile P xs) = last xs"  noschinl@45841  2190 by (auto simp add: dropWhile_append3 in_set_conv_decomp)  noschinl@45841  2191 noschinl@45841  2192 lemma set_dropWhileD: "x \ set (dropWhile P xs) \ x \ set xs"  noschinl@45841  2193 by (induct xs) (auto split: split_if_asm)  noschinl@45841  2194 krauss@23971  2195 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \ P x"  nipkow@13145  2196 by (induct xs) (auto split: split_if_asm)  wenzelm@13114  2197 nipkow@13913  2198 lemma takeWhile_eq_all_conv[simp]:  nipkow@13913  2199  "(takeWhile P xs = xs) = (\x \ set xs. P x)"  nipkow@13913  2200 by(induct xs, auto)  nipkow@13913  2201 nipkow@13913  2202 lemma dropWhile_eq_Nil_conv[simp]:  nipkow@13913  2203  "(dropWhile P xs = []) = (\x \ set xs. P x)"  nipkow@13913  2204 by(induct xs, auto)  nipkow@13913  2205 nipkow@13913  2206 lemma dropWhile_eq_Cons_conv:  nipkow@13913  2207  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \ P y)"  nipkow@13913  2208 by(induct xs, auto)  nipkow@13913  2209 nipkow@31077  2210 lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"  nipkow@31077  2211 by (induct xs) (auto dest: set_takeWhileD)  nipkow@31077  2212 nipkow@31077  2213 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"  nipkow@31077  2214 by (induct xs) auto  nipkow@31077  2215 hoelzl@33639  2216 lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \ f) xs)"  hoelzl@33639  2217 by (induct xs) auto  hoelzl@33639  2218 hoelzl@33639  2219 lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \ f) xs)"  hoelzl@33639  2220 by (induct xs) auto  hoelzl@33639  2221 hoelzl@33639  2222 lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"  hoelzl@33639  2223 by (induct xs) auto  hoelzl@33639  2224 hoelzl@33639  2225 lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"  hoelzl@33639  2226 by (induct xs) auto  hoelzl@33639  2227 hoelzl@33639  2228 lemma hd_dropWhile:  hoelzl@33639  2229  "dropWhile P xs \ [] \ \ P (hd (dropWhile P xs))"  hoelzl@33639  2230 using assms by (induct xs) auto  hoelzl@33639  2231 hoelzl@33639  2232 lemma takeWhile_eq_filter:  hoelzl@33639  2233  assumes "\ x. x \ set (dropWhile P xs) \ \ P x"  hoelzl@33639  2234  shows "takeWhile P xs = filter P xs"  hoelzl@33639  2235 proof -  hoelzl@33639  2236  have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)"  hoelzl@33639  2237  by simp  hoelzl@33639  2238  have B: "filter P (dropWhile P xs) = []"  hoelzl@33639  2239  unfolding filter_empty_conv using assms by blast  hoelzl@33639  2240  have "filter P xs = takeWhile P xs"  hoelzl@33639  2241  unfolding A filter_append B  hoelzl@33639  2242  by (auto simp add: filter_id_conv dest: set_takeWhileD)  hoelzl@33639  2243  thus ?thesis ..  hoelzl@33639  2244 qed  hoelzl@33639  2245 hoelzl@33639  2246 lemma takeWhile_eq_take_P_nth:  hoelzl@33639  2247  "\ \ i. \ i < n ; i < length xs \ \ P (xs ! i) ; n < length xs \ \ P (xs ! n) \ \  hoelzl@33639  2248  takeWhile P xs = take n xs"  hoelzl@33639  2249 proof (induct xs arbitrary: n)  hoelzl@33639  2250  case (Cons x xs)  hoelzl@33639  2251  thus ?case  hoelzl@33639  2252  proof (cases n)  hoelzl@33639  2253  case (Suc n') note this[simp]  hoelzl@33639  2254  have "P x" using Cons.prems(1)[of 0] by simp  hoelzl@33639  2255  moreover have "takeWhile P xs = take n' xs"  hoelzl@33639  2256  proof (rule Cons.hyps)  hoelzl@33639  2257  case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp  hoelzl@33639  2258  next case goal2 thus ?case using Cons by auto  hoelzl@33639  2259  qed  hoelzl@33639  2260  ultimately show ?thesis by simp  hoelzl@33639  2261  qed simp  hoelzl@33639  2262 qed simp  hoelzl@33639  2263 hoelzl@33639  2264 lemma nth_length_takeWhile:  hoelzl@33639  2265  "length (takeWhile P xs) < length xs \ \ P (xs ! length (takeWhile P xs))"  hoelzl@33639  2266 by (induct xs) auto  hoelzl@33639  2267 hoelzl@33639  2268 lemma length_takeWhile_less_P_nth:  hoelzl@33639  2269  assumes all: "\ i. i < j \ P (xs ! i)" and "j \ length xs"  hoelzl@33639  2270  shows "j \ length (takeWhile P xs)"  hoelzl@33639  2271 proof (rule classical)  hoelzl@33639  2272  assume "\ ?thesis"  hoelzl@33639  2273  hence "length (takeWhile P xs) < length xs" using assms by simp  hoelzl@33639  2274  thus ?thesis using all \ ?thesis nth_length_takeWhile[of P xs] by auto  hoelzl@33639  2275 qed  nipkow@31077  2276 nipkow@17501  2277 text{* The following two lemmmas could be generalized to an arbitrary  nipkow@17501  2278 property. *}  nipkow@17501  2279 nipkow@17501  2280 lemma takeWhile_neq_rev: "\distinct xs; x \ set xs\ \  nipkow@17501  2281  takeWhile (\y. y \ x) (rev xs) = rev (tl (dropWhile (\y. y \ x) xs))"  nipkow@17501  2282 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])  nipkow@17501  2283 nipkow@17501  2284 lemma dropWhile_neq_rev: "\distinct xs; x \ set xs\ \  nipkow@17501  2285  dropWhile (\y. y \ x) (rev xs) = x # rev (takeWhile (\y. y \ x) xs)"  nipkow@17501  2286 apply(induct xs)  nipkow@17501  2287  apply simp  nipkow@17501  2288 apply auto  nipkow@17501  2289 apply(subst dropWhile_append2)  nipkow@17501  2290 apply auto  nipkow@17501  2291 done  nipkow@17501  2292 nipkow@18423  2293 lemma takeWhile_not_last:  bulwahn@46500  2294  "distinct xs \ takeWhile (\y. y \ last xs) xs = butlast xs"  nipkow@18423  2295 apply(induct xs)  nipkow@18423  2296  apply simp  nipkow@18423  2297 apply(case_tac xs)  nipkow@18423  2298 apply(auto)  nipkow@18423  2299 done  nipkow@18423  2300 krauss@44013  2301 lemma takeWhile_cong [fundef_cong]:  krauss@18336  2302  "[| l = k; !!x. x : set l ==> P x = Q x |]  krauss@18336  2303  ==> takeWhile P l = takeWhile Q k"  nipkow@24349  2304 by (induct k arbitrary: l) (simp_all)  krauss@18336  2305 krauss@44013  2306 lemma dropWhile_cong [fundef_cong]:  krauss@18336  2307  "[| l = k; !!x. x : set l ==> P x = Q x |]  krauss@18336  2308  ==> dropWhile P l = dropWhile Q k"  nipkow@24349  2309 by (induct k arbitrary: l, simp_all)  krauss@18336  2310 wenzelm@13114  2311 haftmann@49948  2312 subsubsection {* @{const zip} *}  wenzelm@13114  2313 wenzelm@13142  2314 lemma zip_Nil [simp]: "zip [] ys = []"  nipkow@13145  2315 by (induct ys) auto  wenzelm@13114  2316 wenzelm@13142  2317 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"  nipkow@13145  2318 by simp  wenzelm@13114  2319 wenzelm@13142  2320 declare zip_Cons [simp del]  wenzelm@13114  2321 haftmann@36198  2322 lemma [code]:  haftmann@36198  2323  "zip [] ys = []"  haftmann@36198  2324  "zip xs [] = []"  haftmann@36198  2325  "zip (x # xs) (y # ys) = (x, y) # zip xs ys"  haftmann@36198  2326  by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+  haftmann@36198  2327 nipkow@15281  2328 lemma zip_Cons1:  nipkow@15281  2329  "zip (x#xs) ys = (case ys of [] \ [] | y#ys \ (x,y)#zip xs ys)"  nipkow@15281  2330 by(auto split:list.split)  nipkow@15281  2331 wenzelm@13142  2332 lemma length_zip [simp]:  krauss@22493  2333 "length (zip xs ys) = min (length xs) (length ys)"  krauss@22493  2334 by (induct xs ys rule:list_induct2') auto  wenzelm@13114  2335 haftmann@34978  2336 lemma zip_obtain_same_length:  haftmann@34978  2337  assumes "\zs ws n. length zs = length ws \ n = min (length xs) (length ys)  haftmann@34978  2338  \ zs = take n xs \ ws = take n ys \ P (zip zs ws)"  haftmann@34978  2339  shows "P (zip xs ys)"  haftmann@34978  2340 proof -  haftmann@34978  2341  let ?n = "min (length xs) (length ys)"  haftmann@34978  2342  have "P (zip (take ?n xs) (take ?n ys))"  haftmann@34978  2343  by (rule assms) simp_all  haftmann@34978  2344  moreover have "zip xs ys = zip (take ?n xs) (take ?n ys)"  haftmann@34978  2345  proof (induct xs arbitrary: ys)  haftmann@34978  2346  case Nil then show ?case by simp  haftmann@34978  2347  next  haftmann@34978  2348  case (Cons x xs) then show ?case by (cases ys) simp_all  haftmann@34978  2349  qed  haftmann@34978  2350  ultimately show ?thesis by simp  haftmann@34978  2351 qed  haftmann@34978  2352 wenzelm@13114  2353 lemma zip_append1:  krauss@22493  2354 "zip (xs @ ys) zs =  nipkow@13145  2355 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"  krauss@22493  2356 by (induct xs zs rule:list_induct2') auto  wenzelm@13114  2357 wenzelm@13114  2358 lemma zip_append2:  krauss@22493  2359 "zip xs (ys @ zs) =  nipkow@13145  2360 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"  krauss@22493  2361 by (induct xs ys rule:list_induct2') auto  wenzelm@13114  2362 wenzelm@13142  2363 lemma zip_append [simp]:  bulwahn@46500  2364  "[| length xs = length us |] ==>  nipkow@13145  2365 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"  nipkow@13145  2366 by (simp add: zip_append1)  wenzelm@13114  2367 wenzelm@13114  2368 lemma zip_rev:  nipkow@14247  2369 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"  nipkow@14247  2370 by (induct rule:list_induct2, simp_all)  wenzelm@13114  2371 hoelzl@33639  2372 lemma zip_map_map:  hoelzl@33639  2373  "zip (map f xs) (map g ys) = map (\ (x, y). (f x, g y)) (zip xs ys)"  hoelzl@33639  2374 proof (induct xs arbitrary: ys)  hoelzl@33639  2375  case (Cons x xs) note Cons_x_xs = Cons.hyps  hoelzl@33639  2376  show ?case  hoelzl@33639  2377  proof (cases ys)  hoelzl@33639  2378  case (Cons y ys')  hoelzl@33639  2379  show ?thesis unfolding Cons using Cons_x_xs by simp  hoelzl@33639  2380  qed simp  hoelzl@33639  2381 qed simp  hoelzl@33639  2382 hoelzl@33639  2383 lemma zip_map1:  hoelzl@33639  2384  "zip (map f xs) ys = map (\(x, y). (f x, y)) (zip xs ys)"  hoelzl@33639  2385 using zip_map_map[of f xs "\x. x" ys] by simp  hoelzl@33639  2386 hoelzl@33639  2387 lemma zip_map2:  hoelzl@33639  2388  "zip xs (map f ys) = map (\(x, y). (x, f y)) (zip xs ys)"  hoelzl@33639  2389 using zip_map_map[of "\x. x" xs f ys] by simp  hoelzl@33639  2390 nipkow@23096  2391 lemma map_zip_map:  hoelzl@33639  2392  "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"  hoelzl@33639  2393 unfolding zip_map1 by auto  nipkow@23096  2394 nipkow@23096  2395 lemma map_zip_map2:  hoelzl@33639  2396  "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"  hoelzl@33639  2397 unfolding zip_map2 by auto  nipkow@23096  2398 nipkow@31080  2399 text{* Courtesy of Andreas Lochbihler: *}  nipkow@31080  2400 lemma zip_same_conv_map: "zip xs xs = map (\x. (x, x)) xs"  nipkow@31080  2401 by(induct xs) auto  nipkow@31080  2402 wenzelm@13142  2403 lemma nth_zip [simp]:  nipkow@24526  2404 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"  nipkow@24526  2405 apply (induct ys arbitrary: i xs, simp)  nipkow@13145  2406 apply (case_tac xs)  nipkow@13145  2407  apply (simp_all add: nth.simps split: nat.split)  nipkow@13145  2408 done  wenzelm@13114  2409 wenzelm@13114  2410 lemma set_zip:  nipkow@13145  2411 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"  nipkow@31080  2412 by(simp add: set_conv_nth cong: rev_conj_cong)  wenzelm@13114  2413 hoelzl@33639  2414 lemma zip_same: "((a,b) \ set (zip xs xs)) = (a \ set xs \ a = b)"  hoelzl@33639  2415 by(induct xs) auto  hoelzl@33639  2416 wenzelm@13114  2417 lemma zip_update:  nipkow@31080  2418  "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"  nipkow@31080  2419 by(rule sym, simp add: update_zip)  wenzelm@13114  2420 wenzelm@13142  2421 lemma zip_replicate [simp]:  nipkow@24526  2422  "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"  nipkow@24526  2423 apply (induct i arbitrary: j, auto)  paulson@14208  2424 apply (case_tac j, auto)  nipkow@13145  2425 done  wenzelm@13114  2426 nipkow@19487  2427 lemma take_zip:  nipkow@24526  2428  "take n (zip xs ys) = zip (take n xs) (take n ys)"  nipkow@24526  2429 apply (induct n arbitrary: xs ys)  nipkow@19487  2430  apply simp  nipkow@19487  2431 apply (case_tac xs, simp)  nipkow@19487  2432 apply (case_tac ys, simp_all)  nipkow@19487  2433 done  nipkow@19487  2434 nipkow@19487  2435 lemma drop_zip:  nipkow@24526  2436  "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"  nipkow@24526  2437 apply (induct n arbitrary: xs ys)  nipkow@19487  2438  apply simp  nipkow@19487  2439 apply (case_tac xs, simp)  nipkow@19487  2440 apply (case_tac ys, simp_all)  nipkow@19487  2441 done  nipkow@19487  2442 hoelzl@33639  2443 lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \ fst) (zip xs ys)"  hoelzl@33639  2444 proof (induct xs arbitrary: ys)  hoelzl@33639  2445  case (Cons x xs) thus ?case by (cases ys) auto  hoelzl@33639  2446 qed simp  hoelzl@33639  2447 hoelzl@33639  2448 lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \ snd) (zip xs ys)"  hoelzl@33639  2449 proof (induct xs arbitrary: ys)  hoelzl@33639  2450  case (Cons x xs) thus ?case by (cases ys) auto  hoelzl@33639  2451 qed simp  hoelzl@33639  2452 krauss@22493  2453 lemma set_zip_leftD:  krauss@22493  2454  "(x,y)\ set (zip xs ys) \ x \ set xs"  krauss@22493  2455 by (induct xs ys rule:list_induct2') auto  krauss@22493  2456 krauss@22493  2457 lemma set_zip_rightD:  krauss@22493  2458  "(x,y)\ set (zip xs ys) \ y \ set ys"  krauss@22493  2459 by (induct xs ys rule:list_induct2') auto  wenzelm@13142  2460 nipkow@23983  2461 lemma in_set_zipE:  nipkow@23983  2462  "(x,y) : set(zip xs ys) \ (\ x : set xs; y : set ys \ \ R) \ R"  nipkow@23983  2463 by(blast dest: set_zip_leftD set_zip_rightD)  nipkow@23983  2464 haftmann@29829  2465 lemma zip_map_fst_snd:  haftmann@29829  2466  "zip (map fst zs) (map snd zs) = zs"  haftmann@29829  2467  by (induct zs) simp_all  haftmann@29829  2468 haftmann@29829  2469 lemma zip_eq_conv:  haftmann@29829  2470  "length xs = length ys \ zip xs ys = zs \ map fst zs = xs \ map snd zs = ys"  haftmann@29829  2471  by (auto simp add: zip_map_fst_snd)  haftmann@29829  2472 haftmann@51173  2473 lemma in_set_zip:  haftmann@51173  2474  "p \ set (zip xs ys) \ (\n. xs ! n = fst p \ ys ! n = snd p  haftmann@51173  2475  \ n < length xs \ n < length ys)"  haftmann@51173  2476  by (cases p) (auto simp add: set_zip)  haftmann@51173  2477 haftmann@51173  2478 lemma pair_list_eqI:  haftmann@51173  2479  assumes "map fst xs = map fst ys" and "map snd xs = map snd ys"  haftmann@51173  2480  shows "xs = ys"  haftmann@51173  2481 proof -  haftmann@51173  2482  from assms(1) have "length xs = length ys" by (rule map_eq_imp_length_eq)  haftmann@51173  2483  from this assms show ?thesis  haftmann@51173  2484  by (induct xs ys rule: list_induct2) (simp_all add: prod_eqI)  haftmann@51173  2485 qed  haftmann@51173  2486 wenzelm@35115  2487 haftmann@49948  2488 subsubsection {* @{const list_all2} *}  wenzelm@13114  2489 kleing@14316  2490 lemma list_all2_lengthD [intro?]:  kleing@14316  2491  "list_all2 P xs ys ==> length xs = length ys"  nipkow@24349  2492 by (simp add: list_all2_def)  haftmann@19607  2493 haftmann@19787  2494 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"  nipkow@24349  2495 by (simp add: list_all2_def)  haftmann@19607  2496 haftmann@19787  2497 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"  nipkow@24349  2498 by (simp add: list_all2_def)  haftmann@19607  2499 haftmann@19607  2500 lemma list_all2_Cons [iff, code]:  haftmann@19607  2501  "list_all2 P (x # xs) (y # ys) = (P x y \ list_all2 P xs ys)"  nipkow@24349  2502 by (auto simp add: list_all2_def)  wenzelm@13114  2503 wenzelm@13114  2504 lemma list_all2_Cons1:  nipkow@13145  2505 "list_all2 P (x # xs) ys = (\z zs. ys = z # zs \ P x z \ list_all2 P xs zs)"  nipkow@13145  2506 by (cases ys) auto  wenzelm@13114  2507 wenzelm@13114  2508 lemma list_all2_Cons2:  nipkow@13145  2509 "list_all2 P xs (y # ys) = (\z zs. xs = z # zs \ P z y \ list_all2 P zs ys)"  nipkow@13145  2510 by (cases xs) auto  wenzelm@13114  2511 huffman@45794  2512 lemma list_all2_induct  huffman@45794  2513  [consumes 1, case_names Nil Cons, induct set: list_all2]:  huffman@45794  2514  assumes P: "list_all2 P xs ys"  huffman@45794  2515  assumes Nil: "R [] []"  huffman@47640  2516  assumes Cons: "\x xs y ys.  huffman@47640  2517  \P x y; list_all2 P xs ys; R xs ys\ \ R (x # xs) (y # ys)"  huffman@45794  2518  shows "R xs ys"  huffman@45794  2519 using P  huffman@45794  2520 by (induct xs arbitrary: ys) (auto simp add: list_all2_Cons1 Nil Cons)  huffman@45794  2521 wenzelm@13142  2522 lemma list_all2_rev [iff]:  nipkow@13145  2523 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"  nipkow@13145  2524 by (simp add: list_all2_def zip_rev cong: conj_cong)  wenzelm@13114  2525 kleing@13863  2526 lemma list_all2_rev1:  kleing@13863  2527 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"  kleing@13863  2528 by (subst list_all2_rev [symmetric]) simp  kleing@13863  2529 wenzelm@13114  2530 lemma list_all2_append1:  nipkow@13145  2531 "list_all2 P (xs @ ys) zs =  nipkow@13145  2532 (EX us vs. zs = us @ vs \ length us = length xs \ length vs = length ys \  nipkow@13145  2533 list_all2 P xs us \ list_all2 P ys vs)"  nipkow@13145  2534 apply (simp add: list_all2_def zip_append1)  nipkow@13145  2535 apply (rule iffI)  nipkow@13145  2536  apply (rule_tac x = "take (length xs) zs" in exI)  nipkow@13145  2537  apply (rule_tac x = "drop (length xs) zs" in exI)  paulson@14208  2538  apply (force split: nat_diff_split simp add: min_def, clarify)  nipkow@13145  2539 apply (simp add: ball_Un)  nipkow@13145  2540 done  wenzelm@13114  2541 wenzelm@13114  2542 lemma list_all2_append2:  nipkow@13145  2543 "list_all2 P xs (ys @ zs) =  nipkow@13145  2544 (EX us vs. xs = us @ vs \ length us = length ys \ length vs = length zs \  nipkow@13145  2545 list_all2 P us ys \ list_all2 P vs zs)"  nipkow@13145  2546 apply (simp add: list_all2_def zip_append2)  nipkow@13145  2547 apply (rule iffI)  nipkow@13145  2548  apply (rule_tac x = "take (length ys) xs" in exI)  nipkow@13145  2549  apply (rule_tac x = "drop (length ys) xs" in exI)  paulson@14208  2550  apply (force split: nat_diff_split simp add: min_def, clarify)  nipkow@13145  2551 apply (simp add: ball_Un)  nipkow@13145  2552 done  wenzelm@13114  2553 kleing@13863  2554 lemma list_all2_append:  nipkow@14247  2555  "length xs = length ys \  nipkow@14247  2556  list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \ list_all2 P us vs)"  nipkow@14247  2557 by (induct rule:list_induct2, simp_all)  kleing@13863  2558 kleing@13863  2559 lemma list_all2_appendI [intro?, trans]:  kleing@13863  2560  "\ list_all2 P a b; list_all2 P c d \ \ list_all2 P (a@c) (b@d)"  nipkow@24349  2561 by (simp add: list_all2_append list_all2_lengthD)  kleing@13863  2562 wenzelm@13114  2563 lemma list_all2_conv_all_nth:  nipkow@13145  2564 "list_all2 P xs ys =  nipkow@13145  2565 (length xs = length ys \ (\i < length xs. P (xs!i) (ys!i)))"  nipkow@13145  2566 by (force simp add: list_all2_def set_zip)  wenzelm@13114  2567 berghofe@13883  2568 lemma list_all2_trans:  berghofe@13883  2569  assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"  berghofe@13883  2570  shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"  berghofe@13883  2571  (is "!!bs cs. PROP ?Q as bs cs")  berghofe@13883  2572 proof (induct as)  berghofe@13883  2573  fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"  berghofe@13883  2574  show "!!cs. PROP ?Q (x # xs) bs cs"  berghofe@13883  2575  proof (induct bs)  berghofe@13883  2576  fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"  berghofe@13883  2577  show "PROP ?Q (x # xs) (y # ys) cs"  berghofe@13883  2578  by (induct cs) (auto intro: tr I1 I2)  berghofe@13883  2579  qed simp  berghofe@13883  2580 qed simp  berghofe@13883  2581 kleing@13863  2582 lemma list_all2_all_nthI [intro?]:  kleing@13863  2583  "length a = length b \ (\n. n < length a \ P (a!n) (b!n)) \ list_all2 P a b"