src/HOL/List.thy
 author hoelzl Thu Nov 12 17:21:48 2009 +0100 (2009-11-12) changeset 33639 603320b93668 parent 33593 ef54e2108b74 child 33640 0d82107dc07a permissions -rw-r--r--
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
 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@33593  8 imports Plain Presburger ATP_Linkup Recdef  haftmann@31055  9 uses ("Tools/list_code.ML")  nipkow@15131  10 begin  clasohm@923  11 wenzelm@13142  12 datatype 'a list =  wenzelm@13366  13  Nil ("[]")  wenzelm@13366  14  | Cons 'a "'a list" (infixr "#" 65)  clasohm@923  15 nipkow@15392  16 subsection{*Basic list processing functions*}  nipkow@15302  17 clasohm@923  18 consts  wenzelm@13366  19  filter:: "('a => bool) => 'a list => 'a list"  wenzelm@13366  20  concat:: "'a list list => 'a list"  wenzelm@13366  21  foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"  wenzelm@13366  22  foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"  wenzelm@13366  23  hd:: "'a list => 'a"  wenzelm@13366  24  tl:: "'a list => 'a list"  wenzelm@13366  25  last:: "'a list => 'a"  wenzelm@13366  26  butlast :: "'a list => 'a list"  wenzelm@13366  27  set :: "'a list => 'a set"  wenzelm@13366  28  map :: "('a=>'b) => ('a list => 'b list)"  nipkow@23096  29  listsum :: "'a list => 'a::monoid_add"  wenzelm@13366  30  list_update :: "'a list => nat => 'a => 'a list"  wenzelm@13366  31  take:: "nat => 'a list => 'a list"  wenzelm@13366  32  drop:: "nat => 'a list => 'a list"  wenzelm@13366  33  takeWhile :: "('a => bool) => 'a list => 'a list"  wenzelm@13366  34  dropWhile :: "('a => bool) => 'a list => 'a list"  wenzelm@13366  35  rev :: "'a list => 'a list"  wenzelm@13366  36  zip :: "'a list => 'b list => ('a * 'b) list"  nipkow@15425  37  upt :: "nat => nat => nat list" ("(1[_.. 'a list"  nipkow@15110  39  remove1 :: "'a => 'a list => 'a list"  nipkow@27693  40  removeAll :: "'a => 'a list => 'a list"  wenzelm@13366  41  "distinct":: "'a list => bool"  wenzelm@13366  42  replicate :: "nat => 'a => 'a list"  nipkow@19390  43  splice :: "'a list \ 'a list \ 'a list"  nipkow@15302  44 clasohm@923  45 nipkow@13146  46 nonterminals lupdbinds lupdbind  nipkow@5077  47 clasohm@923  48 syntax  wenzelm@13366  49  -- {* list Enumeration *}  wenzelm@13366  50  "@list" :: "args => 'a list" ("[(_)]")  clasohm@923  51 wenzelm@13366  52  -- {* Special syntax for filter *}  nipkow@23279  53  "@filter" :: "[pttrn, 'a list, bool] => 'a list" ("(1[_<-_./ _])")  clasohm@923  54 wenzelm@13366  55  -- {* list update *}  wenzelm@13366  56  "_lupdbind":: "['a, 'a] => lupdbind" ("(2_ :=/ _)")  wenzelm@13366  57  "" :: "lupdbind => lupdbinds" ("_")  wenzelm@13366  58  "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds" ("_,/ _")  wenzelm@13366  59  "_LUpdate" :: "['a, lupdbinds] => 'a" ("_/[(_)]" [900,0] 900)  nipkow@5077  60 clasohm@923  61 translations  wenzelm@13366  62  "[x, xs]" == "x#[xs]"  wenzelm@13366  63  "[x]" == "x#[]"  nipkow@23279  64  "[x<-xs . P]"== "filter (%x. P) xs"  clasohm@923  65 wenzelm@13366  66  "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"  wenzelm@13366  67  "xs[i:=x]" == "list_update xs i x"  nipkow@5077  68 nipkow@5427  69 wenzelm@12114  70 syntax (xsymbols)  nipkow@23279  71  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])")  kleing@14565  72 syntax (HTML output)  nipkow@23279  73  "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\_ ./ _])")  paulson@3342  74 paulson@3342  75 wenzelm@13142  76 text {*  wenzelm@14589  77  Function @{text size} is overloaded for all datatypes. Users may  wenzelm@13366  78  refer to the list version as @{text length}. *}  wenzelm@13142  79 wenzelm@19363  80 abbreviation  wenzelm@21404  81  length :: "'a list => nat" where  wenzelm@19363  82  "length == size"  nipkow@15302  83 berghofe@5183  84 primrec  paulson@15307  85  "hd(x#xs) = x"  paulson@15307  86 berghofe@5183  87 primrec  paulson@15307  88  "tl([]) = []"  paulson@15307  89  "tl(x#xs) = xs"  paulson@15307  90 berghofe@5183  91 primrec  paulson@15307  92  "last(x#xs) = (if xs=[] then x else last xs)"  paulson@15307  93 berghofe@5183  94 primrec  paulson@15307  95  "butlast []= []"  paulson@15307  96  "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"  paulson@15307  97 berghofe@5183  98 primrec  paulson@15307  99  "set [] = {}"  paulson@15307  100  "set (x#xs) = insert x (set xs)"  paulson@15307  101 berghofe@5183  102 primrec  paulson@15307  103  "map f [] = []"  paulson@15307  104  "map f (x#xs) = f(x)#map f xs"  paulson@15307  105 wenzelm@25221  106 primrec  haftmann@25559  107  append :: "'a list \ 'a list \ 'a list" (infixr "@" 65)  haftmann@25559  108 where  haftmann@25559  109  append_Nil:"[] @ ys = ys"  haftmann@25559  110  | append_Cons: "(x#xs) @ ys = x # xs @ ys"  paulson@15307  111 berghofe@5183  112 primrec  paulson@15307  113  "rev([]) = []"  paulson@15307  114  "rev(x#xs) = rev(xs) @ [x]"  paulson@15307  115 berghofe@5183  116 primrec  paulson@15307  117  "filter P [] = []"  paulson@15307  118  "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"  paulson@15307  119 berghofe@5183  120 primrec  paulson@15307  121  foldl_Nil:"foldl f a [] = a"  paulson@15307  122  foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"  paulson@15307  123 paulson@8000  124 primrec  paulson@15307  125  "foldr f [] a = a"  paulson@15307  126  "foldr f (x#xs) a = f x (foldr f xs a)"  paulson@15307  127 berghofe@5183  128 primrec  paulson@15307  129  "concat([]) = []"  paulson@15307  130  "concat(x#xs) = x @ concat(xs)"  paulson@15307  131 berghofe@5183  132 primrec  nipkow@23096  133 "listsum [] = 0"  nipkow@23096  134 "listsum (x # xs) = x + listsum xs"  nipkow@23096  135 nipkow@23096  136 primrec  paulson@15307  137  drop_Nil:"drop n [] = []"  paulson@15307  138  drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"  paulson@15307  139  -- {*Warning: simpset does not contain this definition, but separate  paulson@15307  140  theorems for @{text "n = 0"} and @{text "n = Suc k"} *}  paulson@15307  141 berghofe@5183  142 primrec  paulson@15307  143  take_Nil:"take n [] = []"  paulson@15307  144  take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"  paulson@15307  145  -- {*Warning: simpset does not contain this definition, but separate  paulson@15307  146  theorems for @{text "n = 0"} and @{text "n = Suc k"} *}  paulson@15307  147 haftmann@29822  148 primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where  haftmann@29822  149  nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"  paulson@15307  150  -- {*Warning: simpset does not contain this definition, but separate  paulson@15307  151  theorems for @{text "n = 0"} and @{text "n = Suc k"} *}  paulson@15307  152 berghofe@5183  153 primrec  paulson@15307  154  "[][i:=v] = []"  paulson@15307  155  "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"  paulson@15307  156 paulson@15307  157 primrec  paulson@15307  158  "takeWhile P [] = []"  paulson@15307  159  "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"  paulson@15307  160 berghofe@5183  161 primrec  paulson@15307  162  "dropWhile P [] = []"  paulson@15307  163  "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"  paulson@15307  164 berghofe@5183  165 primrec  paulson@15307  166  "zip xs [] = []"  paulson@15307  167  zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"  paulson@15307  168  -- {*Warning: simpset does not contain this definition, but separate  paulson@15307  169  theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}  paulson@15307  170 nipkow@5427  171 primrec  nipkow@15425  172  upt_0: "[i..<0] = []"  nipkow@15425  173  upt_Suc: "[i..<(Suc j)] = (if i <= j then [i.. distinct xs)"  paulson@15307  178 berghofe@5183  179 primrec  paulson@15307  180  "remdups [] = []"  paulson@15307  181  "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"  paulson@15307  182 berghofe@5183  183 primrec  paulson@15307  184  "remove1 x [] = []"  paulson@15307  185  "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"  paulson@15307  186 nipkow@15110  187 primrec  nipkow@27693  188  "removeAll x [] = []"  nipkow@27693  189  "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"  nipkow@27693  190 nipkow@27693  191 primrec  paulson@15307  192  replicate_0: "replicate 0 x = []"  paulson@15307  193  replicate_Suc: "replicate (Suc n) x = x # replicate n x"  paulson@15307  194 haftmann@21061  195 definition  wenzelm@21404  196  rotate1 :: "'a list \ 'a list" where  wenzelm@21404  197  "rotate1 xs = (case xs of [] \ [] | x#xs \ xs @ [x])"  wenzelm@21404  198 wenzelm@21404  199 definition  wenzelm@21404  200  rotate :: "nat \ 'a list \ 'a list" where  haftmann@30971  201  "rotate n = rotate1 ^^ n"  wenzelm@21404  202 wenzelm@21404  203 definition  wenzelm@21404  204  list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where  haftmann@28562  205  [code del]: "list_all2 P xs ys =  haftmann@21061  206  (length xs = length ys \ (\(x, y) \ set (zip xs ys). P x y))"  wenzelm@21404  207 wenzelm@21404  208 definition  wenzelm@21404  209  sublist :: "'a list => nat set => 'a list" where  wenzelm@21404  210  "sublist xs A = map fst (filter (\p. snd p \ A) (zip xs [0..n::nat. n<2) [0,2,1] = [0,1]" by simp}\\  wenzelm@27381  231 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\  wenzelm@27381  232 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\  wenzelm@27381  233 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\  wenzelm@27381  234 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\  wenzelm@27381  235 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\  wenzelm@27381  236 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\  wenzelm@27381  237 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\  wenzelm@27381  238 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\  wenzelm@27381  239 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\  wenzelm@27381  240 @{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\  wenzelm@27381  241 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\  wenzelm@27381  242 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\  wenzelm@27381  243 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\  wenzelm@27381  244 @{lemma "distinct [2,0,1::nat]" by simp}\\  wenzelm@27381  245 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\  wenzelm@27381  246 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\  nipkow@27693  247 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\  wenzelm@27381  248 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\  wenzelm@27381  249 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\  wenzelm@27381  250 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\  wenzelm@27381  251 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\  wenzelm@27381  252 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\  wenzelm@27381  253 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\  wenzelm@27381  254 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\  wenzelm@27381  255 @{lemma "listsum [1,2,3::nat] = 6" by simp}  nipkow@26771  256 \end{tabular}}  nipkow@26771  257 \caption{Characteristic examples}  nipkow@26771  258 \label{fig:Characteristic}  nipkow@26771  259 \end{figure}  blanchet@29927  260 Figure~\ref{fig:Characteristic} shows characteristic examples  nipkow@26771  261 that should give an intuitive understanding of the above functions.  nipkow@26771  262 *}  nipkow@26771  263 nipkow@24616  264 text{* The following simple sort functions are intended for proofs,  nipkow@24616  265 not for efficient implementations. *}  nipkow@24616  266 wenzelm@25221  267 context linorder  wenzelm@25221  268 begin  wenzelm@25221  269 wenzelm@25221  270 fun sorted :: "'a list \ bool" where  nipkow@24697  271 "sorted [] \ True" |  nipkow@24697  272 "sorted [x] \ True" |  haftmann@25062  273 "sorted (x#y#zs) \ x <= y \ sorted (y#zs)"  nipkow@24697  274 hoelzl@33639  275 primrec insort_key :: "('b \ 'a) \ 'b \ 'b list \ 'b list" where  hoelzl@33639  276 "insort_key f x [] = [x]" |  hoelzl@33639  277 "insort_key f x (y#ys) = (if f x \ f y then (x#y#ys) else y#(insort_key f x ys))"  hoelzl@33639  278 hoelzl@33639  279 primrec sort_key :: "('b \ 'a) \ 'b list \ 'b list" where  hoelzl@33639  280 "sort_key f [] = []" |  hoelzl@33639  281 "sort_key f (x#xs) = insort_key f x (sort_key f xs)"  hoelzl@33639  282 hoelzl@33639  283 abbreviation "sort \ sort_key (\x. x)"  hoelzl@33639  284 abbreviation "insort \ insort_key (\x. x)"  nipkow@24616  285 wenzelm@25221  286 end  wenzelm@25221  287 nipkow@24616  288 wenzelm@23388  289 subsubsection {* List comprehension *}  nipkow@23192  290 nipkow@24349  291 text{* Input syntax for Haskell-like list comprehension notation.  nipkow@24349  292 Typical example: @{text"[(x,y). x \ xs, y \ ys, x \ y]"},  nipkow@24349  293 the list of all pairs of distinct elements from @{text xs} and @{text ys}.  nipkow@24349  294 The syntax is as in Haskell, except that @{text"|"} becomes a dot  nipkow@24349  295 (like in Isabelle's set comprehension): @{text"[e. x \ xs, \]"} rather than  nipkow@24349  296 \verb![e| x <- xs, ...]!.  nipkow@24349  297 nipkow@24349  298 The qualifiers after the dot are  nipkow@24349  299 \begin{description}  nipkow@24349  300 \item[generators] @{text"p \ xs"},  nipkow@24476  301  where @{text p} is a pattern and @{text xs} an expression of list type, or  nipkow@24476  302 \item[guards] @{text"b"}, where @{text b} is a boolean expression.  nipkow@24476  303 %\item[local bindings] @ {text"let x = e"}.  nipkow@24349  304 \end{description}  nipkow@23240  305 nipkow@24476  306 Just like in Haskell, list comprehension is just a shorthand. To avoid  nipkow@24476  307 misunderstandings, the translation into desugared form is not reversed  nipkow@24476  308 upon output. Note that the translation of @{text"[e. x \ xs]"} is  nipkow@24476  309 optmized to @{term"map (%x. e) xs"}.  nipkow@23240  310 nipkow@24349  311 It is easy to write short list comprehensions which stand for complex  nipkow@24349  312 expressions. During proofs, they may become unreadable (and  nipkow@24349  313 mangled). In such cases it can be advisable to introduce separate  nipkow@24349  314 definitions for the list comprehensions in question. *}  nipkow@24349  315 nipkow@23209  316 (*  nipkow@23240  317 Proper theorem proving support would be nice. For example, if  nipkow@23192  318 @{text"set[f x y. x \ xs, y \ ys, P x y]"}  nipkow@23192  319 produced something like  nipkow@23209  320 @{term"{z. EX x: set xs. EX y:set ys. P x y \ z = f x y}"}.  nipkow@23209  321 *)  nipkow@23209  322 nipkow@23240  323 nonterminals lc_qual lc_quals  nipkow@23192  324 nipkow@23192  325 syntax  nipkow@23240  326 "_listcompr" :: "'a \ lc_qual \ lc_quals \ 'a list" ("[_ . __")  nipkow@24349  327 "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ <- _")  nipkow@23240  328 "_lc_test" :: "bool \ lc_qual" ("_")  nipkow@24476  329 (*"_lc_let" :: "letbinds => lc_qual" ("let _")*)  nipkow@23240  330 "_lc_end" :: "lc_quals" ("]")  nipkow@23240  331 "_lc_quals" :: "lc_qual \ lc_quals \ lc_quals" (", __")  nipkow@24349  332 "_lc_abs" :: "'a => 'b list => 'b list"  nipkow@23192  333 nipkow@24476  334 (* These are easier than ML code but cannot express the optimized  nipkow@24476  335  translation of [e. p<-xs]  nipkow@23192  336 translations  nipkow@24349  337 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"  nipkow@23240  338 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"  nipkow@24349  339  => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"  nipkow@23240  340 "[e. P]" => "if P then [e] else []"  nipkow@23240  341 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"  nipkow@23240  342  => "if P then (_listcompr e Q Qs) else []"  nipkow@24349  343 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"  nipkow@24349  344  => "_Let b (_listcompr e Q Qs)"  nipkow@24476  345 *)  nipkow@23240  346 nipkow@23279  347 syntax (xsymbols)  nipkow@24349  348 "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _")  nipkow@23279  349 syntax (HTML output)  nipkow@24349  350 "_lc_gen" :: "'a \ 'a list \ lc_qual" ("_ \ _")  nipkow@24349  351 nipkow@24349  352 parse_translation (advanced) {*  nipkow@24349  353 let  nipkow@24476  354  val NilC = Syntax.const @{const_name Nil};  nipkow@24476  355  val ConsC = Syntax.const @{const_name Cons};  nipkow@24476  356  val mapC = Syntax.const @{const_name map};  nipkow@24476  357  val concatC = Syntax.const @{const_name concat};  nipkow@24476  358  val IfC = Syntax.const @{const_name If};  nipkow@24476  359  fun singl x = ConsC $x$ NilC;  nipkow@24476  360 nipkow@24476  361  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)  nipkow@24349  362  let  wenzelm@29281  363  val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);  nipkow@24476  364  val e = if opti then singl e else e;  nipkow@24476  365  val case1 = Syntax.const "_case1" $p$ e;  nipkow@24349  366  val case2 = Syntax.const "_case1" $Syntax.const Term.dummy_patternN  nipkow@24476  367 $ NilC;  nipkow@24349  368  val cs = Syntax.const "_case2" $case1$ case2  haftmann@31784  369  val ft = DatatypeCase.case_tr false Datatype.info_of_constr  nipkow@24349  370  ctxt [x, cs]  nipkow@24349  371  in lambda x ft end;  nipkow@24349  372 nipkow@24476  373  fun abs_tr ctxt (p as Free(s,T)) e opti =  nipkow@24349  374  let val thy = ProofContext.theory_of ctxt;  nipkow@24349  375  val s' = Sign.intern_const thy s  nipkow@24476  376  in if Sign.declared_const thy s'  nipkow@24476  377  then (pat_tr ctxt p e opti, false)  nipkow@24476  378  else (lambda p e, true)  nipkow@24349  379  end  nipkow@24476  380  | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);  nipkow@24476  381 nipkow@24476  382  fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =  nipkow@24476  383  let val res = case qs of Const("_lc_end",_) => singl e  nipkow@24476  384  | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];  nipkow@24476  385  in IfC$ b $res$ NilC end  nipkow@24476  386  | lc_tr ctxt [e, Const("_lc_gen",_) $p$ es, Const("_lc_end",_)] =  nipkow@24476  387  (case abs_tr ctxt p e true of  nipkow@24476  388  (f,true) => mapC $f$ es  nipkow@24476  389  | (f, false) => concatC $(mapC$ f $es))  nipkow@24476  390  | lc_tr ctxt [e, Const("_lc_gen",_)$ p $es, Const("_lc_quals",_)$q$qs] =  nipkow@24476  391  let val e' = lc_tr ctxt [e,q,qs];  nipkow@24476  392  in concatC$ (mapC $(fst(abs_tr ctxt p e' false))$ es) end  nipkow@24476  393 nipkow@24476  394 in [("_listcompr", lc_tr)] end  nipkow@24349  395 *}  nipkow@23279  396 nipkow@23240  397 (*  nipkow@23240  398 term "[(x,y,z). b]"  nipkow@24476  399 term "[(x,y,z). x\xs]"  nipkow@24476  400 term "[e x y. x\xs, y\ys]"  nipkow@24476  401 term "[(x,y,z). xb]"  nipkow@24476  402 term "[(x,y,z). x\xs, x>b]"  nipkow@24476  403 term "[(x,y,z). xxs]"  nipkow@24349  404 term "[(x,y). Cons True x \ xs]"  nipkow@24349  405 term "[(x,y,z). Cons x [] \ xs]"  nipkow@23240  406 term "[(x,y,z). xb, x=d]"  nipkow@23240  407 term "[(x,y,z). xb, y\ys]"  nipkow@23240  408 term "[(x,y,z). xxs,y>b]"  nipkow@23240  409 term "[(x,y,z). xxs, y\ys]"  nipkow@23240  410 term "[(x,y,z). x\xs, x>b, yxs, x>b, y\ys]"  nipkow@23240  412 term "[(x,y,z). x\xs, y\ys,y>x]"  nipkow@23240  413 term "[(x,y,z). x\xs, y\ys,z\zs]"  nipkow@24349  414 term "[(x,y). x\xs, let xx = x+x, y\ys, y \ xx]"  nipkow@23192  415 *)  nipkow@23192  416 haftmann@21061  417 subsubsection {* @{const Nil} and @{const Cons} *}  haftmann@21061  418 haftmann@21061  419 lemma not_Cons_self [simp]:  haftmann@21061  420  "xs \ x # xs"  nipkow@13145  421 by (induct xs) auto  wenzelm@13114  422 wenzelm@13142  423 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]  wenzelm@13114  424 wenzelm@13142  425 lemma neq_Nil_conv: "(xs \ []) = (\y ys. xs = y # ys)"  nipkow@13145  426 by (induct xs) auto  wenzelm@13114  427 wenzelm@13142  428 lemma length_induct:  haftmann@21061  429  "(\xs. \ys. length ys < length xs \ P ys \ P xs) \ P xs"  nipkow@17589  430 by (rule measure_induct [of length]) iprover  wenzelm@13114  431 wenzelm@13114  432 haftmann@21061  433 subsubsection {* @{const length} *}  wenzelm@13114  434 wenzelm@13142  435 text {*  haftmann@21061  436  Needs to come before @{text "@"} because of theorem @{text  haftmann@21061  437  append_eq_append_conv}.  wenzelm@13142  438 *}  wenzelm@13114  439 wenzelm@13142  440 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"  nipkow@13145  441 by (induct xs) auto  wenzelm@13114  442 wenzelm@13142  443 lemma length_map [simp]: "length (map f xs) = length xs"  nipkow@13145  444 by (induct xs) auto  wenzelm@13114  445 wenzelm@13142  446 lemma length_rev [simp]: "length (rev xs) = length xs"  nipkow@13145  447 by (induct xs) auto  wenzelm@13114  448 wenzelm@13142  449 lemma length_tl [simp]: "length (tl xs) = length xs - 1"  nipkow@13145  450 by (cases xs) auto  wenzelm@13114  451 wenzelm@13142  452 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"  nipkow@13145  453 by (induct xs) auto  wenzelm@13114  454 wenzelm@13142  455 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \ [])"  nipkow@13145  456 by (induct xs) auto  wenzelm@13114  457 nipkow@23479  458 lemma length_pos_if_in_set: "x : set xs \ length xs > 0"  nipkow@23479  459 by auto  nipkow@23479  460 wenzelm@13114  461 lemma length_Suc_conv:  nipkow@13145  462 "(length xs = Suc n) = (\y ys. xs = y # ys \ length ys = n)"  nipkow@13145  463 by (induct xs) auto  wenzelm@13142  464 nipkow@14025  465 lemma Suc_length_conv:  nipkow@14025  466 "(Suc n = length xs) = (\y ys. xs = y # ys \ length ys = n)"  paulson@14208  467 apply (induct xs, simp, simp)  nipkow@14025  468 apply blast  nipkow@14025  469 done  nipkow@14025  470 wenzelm@25221  471 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"  wenzelm@25221  472  by (induct xs) auto  wenzelm@25221  473 haftmann@26442  474 lemma list_induct2 [consumes 1, case_names Nil Cons]:  haftmann@26442  475  "length xs = length ys \ P [] [] \  haftmann@26442  476  (\x xs y ys. length xs = length ys \ P xs ys \ P (x#xs) (y#ys))  haftmann@26442  477  \ P xs ys"  haftmann@26442  478 proof (induct xs arbitrary: ys)  haftmann@26442  479  case Nil then show ?case by simp  haftmann@26442  480 next  haftmann@26442  481  case (Cons x xs ys) then show ?case by (cases ys) simp_all  haftmann@26442  482 qed  haftmann@26442  483 haftmann@26442  484 lemma list_induct3 [consumes 2, case_names Nil Cons]:  haftmann@26442  485  "length xs = length ys \ length ys = length zs \ P [] [] [] \  haftmann@26442  486  (\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  487  \ P xs ys zs"  haftmann@26442  488 proof (induct xs arbitrary: ys zs)  haftmann@26442  489  case Nil then show ?case by simp  haftmann@26442  490 next  haftmann@26442  491  case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)  haftmann@26442  492  (cases zs, simp_all)  haftmann@26442  493 qed  wenzelm@13114  494 krauss@22493  495 lemma list_induct2':  krauss@22493  496  "\ P [] [];  krauss@22493  497  \x xs. P (x#xs) [];  krauss@22493  498  \y ys. P [] (y#ys);  krauss@22493  499  \x xs y ys. P xs ys \ P (x#xs) (y#ys) \  krauss@22493  500  \ P xs ys"  krauss@22493  501 by (induct xs arbitrary: ys) (case_tac x, auto)+  krauss@22493  502 nipkow@22143  503 lemma neq_if_length_neq: "length xs \ length ys \ (xs = ys) == False"  nipkow@24349  504 by (rule Eq_FalseI) auto  wenzelm@24037  505 wenzelm@24037  506 simproc_setup list_neq ("(xs::'a list) = ys") = {*  nipkow@22143  507 (*  nipkow@22143  508 Reduces xs=ys to False if xs and ys cannot be of the same length.  nipkow@22143  509 This is the case if the atomic sublists of one are a submultiset  nipkow@22143  510 of those of the other list and there are fewer Cons's in one than the other.  nipkow@22143  511 *)  wenzelm@24037  512 wenzelm@24037  513 let  nipkow@22143  514 huffman@29856  515 fun len (Const(@{const_name Nil},_)) acc = acc  huffman@29856  516  | len (Const(@{const_name Cons},_) $_$ xs) (ts,n) = len xs (ts,n+1)  huffman@29856  517  | len (Const(@{const_name append},_) $xs$ ys) acc = len xs (len ys acc)  huffman@29856  518  | len (Const(@{const_name rev},_) $xs) acc = len xs acc  huffman@29856  519  | len (Const(@{const_name map},_)$ _ $xs) acc = len xs acc  nipkow@22143  520  | len t (ts,n) = (t::ts,n);  nipkow@22143  521 wenzelm@24037  522 fun list_neq _ ss ct =  nipkow@22143  523  let  wenzelm@24037  524  val (Const(_,eqT)$ lhs $rhs) = Thm.term_of ct;  nipkow@22143  525  val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);  nipkow@22143  526  fun prove_neq() =  nipkow@22143  527  let  nipkow@22143  528  val Type(_,listT::_) = eqT;  haftmann@22994  529  val size = HOLogic.size_const listT;  nipkow@22143  530  val eq_len = HOLogic.mk_eq (size$ lhs, size $rhs);  nipkow@22143  531  val neq_len = HOLogic.mk_Trueprop (HOLogic.Not$ eq_len);  nipkow@22143  532  val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len  haftmann@22633  533  (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));  haftmann@22633  534  in SOME (thm RS @{thm neq_if_length_neq}) end  nipkow@22143  535  in  wenzelm@23214  536  if m < n andalso submultiset (op aconv) (ls,rs) orelse  wenzelm@23214  537  n < m andalso submultiset (op aconv) (rs,ls)  nipkow@22143  538  then prove_neq() else NONE  nipkow@22143  539  end;  wenzelm@24037  540 in list_neq end;  nipkow@22143  541 *}  nipkow@22143  542 nipkow@22143  543 nipkow@15392  544 subsubsection {* @{text "@"} -- append *}  wenzelm@13114  545 wenzelm@13142  546 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"  nipkow@13145  547 by (induct xs) auto  wenzelm@13114  548 wenzelm@13142  549 lemma append_Nil2 [simp]: "xs @ [] = xs"  nipkow@13145  550 by (induct xs) auto  nipkow@3507  551 wenzelm@13142  552 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \ ys = [])"  nipkow@13145  553 by (induct xs) auto  wenzelm@13114  554 wenzelm@13142  555 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \ ys = [])"  nipkow@13145  556 by (induct xs) auto  wenzelm@13114  557 wenzelm@13142  558 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"  nipkow@13145  559 by (induct xs) auto  wenzelm@13114  560 wenzelm@13142  561 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"  nipkow@13145  562 by (induct xs) auto  wenzelm@13114  563 wenzelm@25221  564 lemma append_eq_append_conv [simp, noatp]:  nipkow@24526  565  "length xs = length ys \ length us = length vs  berghofe@13883  566  ==> (xs@us = ys@vs) = (xs=ys \ us=vs)"  nipkow@24526  567 apply (induct xs arbitrary: ys)  paulson@14208  568  apply (case_tac ys, simp, force)  paulson@14208  569 apply (case_tac ys, force, simp)  nipkow@13145  570 done  wenzelm@13142  571 nipkow@24526  572 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =  nipkow@24526  573  (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"  nipkow@24526  574 apply (induct xs arbitrary: ys zs ts)  nipkow@14495  575  apply fastsimp  nipkow@14495  576 apply(case_tac zs)  nipkow@14495  577  apply simp  nipkow@14495  578 apply fastsimp  nipkow@14495  579 done  nipkow@14495  580 wenzelm@13142  581 lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"  nipkow@13145  582 by simp  wenzelm@13142  583 wenzelm@13142  584 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \ x = y)"  nipkow@13145  585 by simp  wenzelm@13114  586 wenzelm@13142  587 lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)"  nipkow@13145  588 by simp  wenzelm@13114  589 wenzelm@13142  590 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"  nipkow@13145  591 using append_same_eq [of _ _ "[]"] by auto  nipkow@3507  592 wenzelm@13142  593 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"  nipkow@13145  594 using append_same_eq [of "[]"] by auto  wenzelm@13114  595 paulson@24286  596 lemma hd_Cons_tl [simp,noatp]: "xs \ [] ==> hd xs # tl xs = xs"  nipkow@13145  597 by (induct xs) auto  wenzelm@13114  598 wenzelm@13142  599 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"  nipkow@13145  600 by (induct xs) auto  wenzelm@13114  601 wenzelm@13142  602 lemma hd_append2 [simp]: "xs \ [] ==> hd (xs @ ys) = hd xs"  nipkow@13145  603 by (simp add: hd_append split: list.split)  wenzelm@13114  604 wenzelm@13142  605 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"  nipkow@13145  606 by (simp split: list.split)  wenzelm@13114  607 wenzelm@13142  608 lemma tl_append2 [simp]: "xs \ [] ==> tl (xs @ ys) = tl xs @ ys"  nipkow@13145  609 by (simp add: tl_append split: list.split)  wenzelm@13114  610 wenzelm@13114  611 nipkow@14300  612 lemma Cons_eq_append_conv: "x#xs = ys@zs =  nipkow@14300  613  (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"  nipkow@14300  614 by(cases ys) auto  nipkow@14300  615 nipkow@15281  616 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =  nipkow@15281  617  (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"  nipkow@15281  618 by(cases ys) auto  nipkow@15281  619 nipkow@14300  620 wenzelm@13142  621 text {* Trivial rules for solving @{text "@"}-equations automatically. *}  wenzelm@13114  622 wenzelm@13114  623 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"  nipkow@13145  624 by simp  wenzelm@13114  625 wenzelm@13142  626 lemma Cons_eq_appendI:  nipkow@13145  627 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"  nipkow@13145  628 by (drule sym) simp  wenzelm@13114  629 wenzelm@13142  630 lemma append_eq_appendI:  nipkow@13145  631 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"  nipkow@13145  632 by (drule sym) simp  wenzelm@13114  633 wenzelm@13114  634 wenzelm@13142  635 text {*  nipkow@13145  636 Simplification procedure for all list equalities.  nipkow@13145  637 Currently only tries to rearrange @{text "@"} to see if  nipkow@13145  638 - both lists end in a singleton list,  nipkow@13145  639 - or both lists end in the same list.  wenzelm@13142  640 *}  wenzelm@13142  641 wenzelm@26480  642 ML {*  nipkow@3507  643 local  nipkow@3507  644 huffman@29856  645 fun last (cons as Const(@{const_name Cons},_) $_$ xs) =  huffman@29856  646  (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)  huffman@29856  647  | last (Const(@{const_name append},_) $_$ ys) = last ys  wenzelm@13462  648  | last t = t;  wenzelm@13114  649 huffman@29856  650 fun list1 (Const(@{const_name Cons},_) $_$ Const(@{const_name Nil},_)) = true  wenzelm@13462  651  | list1 _ = false;  wenzelm@13114  652 huffman@29856  653 fun butlast ((cons as Const(@{const_name Cons},_) $x)$ xs) =  huffman@29856  654  (case xs of Const(@{const_name Nil},_) => xs | _ => cons $butlast xs)  huffman@29856  655  | butlast ((app as Const(@{const_name append},_)$ xs) $ys) = app$ butlast ys  huffman@29856  656  | butlast xs = Const(@{const_name Nil},fastype_of xs);  wenzelm@13114  657 haftmann@22633  658 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},  haftmann@22633  659  @{thm append_Nil}, @{thm append_Cons}];  wenzelm@16973  660 wenzelm@20044  661 fun list_eq ss (F as (eq as Const(_,eqT)) $lhs$ rhs) =  wenzelm@13462  662  let  wenzelm@13462  663  val lastl = last lhs and lastr = last rhs;  wenzelm@13462  664  fun rearr conv =  wenzelm@13462  665  let  wenzelm@13462  666  val lhs1 = butlast lhs and rhs1 = butlast rhs;  wenzelm@13462  667  val Type(_,listT::_) = eqT  wenzelm@13462  668  val appT = [listT,listT] ---> listT  huffman@29856  669  val app = Const(@{const_name append},appT)  wenzelm@13462  670  val F2 = eq $(app$lhs1$lastl)$ (app$rhs1$lastr)  wenzelm@13480  671  val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));  wenzelm@20044  672  val thm = Goal.prove (Simplifier.the_context ss) [] [] eq  wenzelm@17877  673  (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));  skalberg@15531  674  in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;  wenzelm@13114  675 wenzelm@13462  676  in  haftmann@22633  677  if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}  haftmann@22633  678  else if lastl aconv lastr then rearr @{thm append_same_eq}  skalberg@15531  679  else NONE  wenzelm@13462  680  end;  wenzelm@13462  681 wenzelm@13114  682 in  wenzelm@13462  683 wenzelm@13462  684 val list_eq_simproc =  wenzelm@32010  685  Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);  wenzelm@13462  686 wenzelm@13114  687 end;  wenzelm@13114  688 wenzelm@13114  689 Addsimprocs [list_eq_simproc];  wenzelm@13114  690 *}  wenzelm@13114  691 wenzelm@13114  692 nipkow@15392  693 subsubsection {* @{text map} *}  wenzelm@13114  694 wenzelm@13142  695 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"  nipkow@13145  696 by (induct xs) simp_all  wenzelm@13114  697 wenzelm@13142  698 lemma map_ident [simp]: "map (\x. x) = (\xs. xs)"  nipkow@13145  699 by (rule ext, induct_tac xs) auto  wenzelm@13114  700 wenzelm@13142  701 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"  nipkow@13145  702 by (induct xs) auto  wenzelm@13114  703 hoelzl@33639  704 lemma map_map [simp]: "map f (map g xs) = map (f \ g) xs"  hoelzl@33639  705 by (induct xs) auto  hoelzl@33639  706 hoelzl@33639  707 lemma map_compose: "map (f \ g) xs = map f (map g xs)"  hoelzl@33639  708 by simp  wenzelm@13114  709 wenzelm@13142  710 lemma rev_map: "rev (map f xs) = map f (rev xs)"  nipkow@13145  711 by (induct xs) auto  wenzelm@13114  712 nipkow@13737  713 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"  nipkow@13737  714 by (induct xs) auto  nipkow@13737  715 krauss@19770  716 lemma map_cong [fundef_cong, recdef_cong]:  nipkow@13145  717 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"  nipkow@13145  718 -- {* a congruence rule for @{text map} *}  nipkow@13737  719 by simp  wenzelm@13114  720 wenzelm@13142  721 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"  nipkow@13145  722 by (cases xs) auto  wenzelm@13114  723 wenzelm@13142  724 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"  nipkow@13145  725 by (cases xs) auto  wenzelm@13114  726 paulson@18447  727 lemma map_eq_Cons_conv:  nipkow@14025  728  "(map f xs = y#ys) = (\z zs. xs = z#zs \ f z = y \ map f zs = ys)"  nipkow@13145  729 by (cases xs) auto  wenzelm@13114  730 paulson@18447  731 lemma Cons_eq_map_conv:  nipkow@14025  732  "(x#xs = map f ys) = (\z zs. ys = z#zs \ x = f z \ xs = map f zs)"  nipkow@14025  733 by (cases ys) auto  nipkow@14025  734 paulson@18447  735 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]  paulson@18447  736 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]  paulson@18447  737 declare map_eq_Cons_D [dest!] Cons_eq_map_D [dest!]  paulson@18447  738 nipkow@14111  739 lemma ex_map_conv:  nipkow@14111  740  "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"  paulson@18447  741 by(induct ys, auto simp add: Cons_eq_map_conv)  nipkow@14111  742 nipkow@15110  743 lemma map_eq_imp_length_eq:  haftmann@26734  744  assumes "map f xs = map f ys"  haftmann@26734  745  shows "length xs = length ys"  haftmann@26734  746 using assms proof (induct ys arbitrary: xs)  haftmann@26734  747  case Nil then show ?case by simp  haftmann@26734  748 next  haftmann@26734  749  case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto  haftmann@26734  750  from Cons xs have "map f zs = map f ys" by simp  haftmann@26734  751  moreover with Cons have "length zs = length ys" by blast  haftmann@26734  752  with xs show ?case by simp  haftmann@26734  753 qed  haftmann@26734  754   nipkow@15110  755 lemma map_inj_on:  nipkow@15110  756  "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]  nipkow@15110  757  ==> xs = ys"  nipkow@15110  758 apply(frule map_eq_imp_length_eq)  nipkow@15110  759 apply(rotate_tac -1)  nipkow@15110  760 apply(induct rule:list_induct2)  nipkow@15110  761  apply simp  nipkow@15110  762 apply(simp)  nipkow@15110  763 apply (blast intro:sym)  nipkow@15110  764 done  nipkow@15110  765 nipkow@15110  766 lemma inj_on_map_eq_map:  nipkow@15110  767  "inj_on f (set xs Un set ys) \ (map f xs = map f ys) = (xs = ys)"  nipkow@15110  768 by(blast dest:map_inj_on)  nipkow@15110  769 wenzelm@13114  770 lemma map_injective:  nipkow@24526  771  "map f xs = map f ys ==> inj f ==> xs = ys"  nipkow@24526  772 by (induct ys arbitrary: xs) (auto dest!:injD)  wenzelm@13114  773 nipkow@14339  774 lemma inj_map_eq_map[simp]: "inj f \ (map f xs = map f ys) = (xs = ys)"  nipkow@14339  775 by(blast dest:map_injective)  nipkow@14339  776 wenzelm@13114  777 lemma inj_mapI: "inj f ==> inj (map f)"  nipkow@17589  778 by (iprover dest: map_injective injD intro: inj_onI)  wenzelm@13114  779 wenzelm@13114  780 lemma inj_mapD: "inj (map f) ==> inj f"  paulson@14208  781 apply (unfold inj_on_def, clarify)  nipkow@13145  782 apply (erule_tac x = "[x]" in ballE)  paulson@14208  783  apply (erule_tac x = "[y]" in ballE, simp, blast)  nipkow@13145  784 apply blast  nipkow@13145  785 done  wenzelm@13114  786 nipkow@14339  787 lemma inj_map[iff]: "inj (map f) = inj f"  nipkow@13145  788 by (blast dest: inj_mapD intro: inj_mapI)  wenzelm@13114  789 nipkow@15303  790 lemma inj_on_mapI: "inj_on f (\(set  A)) \ inj_on (map f) A"  nipkow@15303  791 apply(rule inj_onI)  nipkow@15303  792 apply(erule map_inj_on)  nipkow@15303  793 apply(blast intro:inj_onI dest:inj_onD)  nipkow@15303  794 done  nipkow@15303  795 kleing@14343  796 lemma map_idI: "(\x. x \ set xs \ f x = x) \ map f xs = xs"  kleing@14343  797 by (induct xs, auto)  wenzelm@13114  798 nipkow@14402  799 lemma map_fun_upd [simp]: "y \ set xs \ map (f(y:=v)) xs = map f xs"  nipkow@14402  800 by (induct xs) auto  nipkow@14402  801 nipkow@15110  802 lemma map_fst_zip[simp]:  nipkow@15110  803  "length xs = length ys \ map fst (zip xs ys) = xs"  nipkow@15110  804 by (induct rule:list_induct2, simp_all)  nipkow@15110  805 nipkow@15110  806 lemma map_snd_zip[simp]:  nipkow@15110  807  "length xs = length ys \ map snd (zip xs ys) = ys"  nipkow@15110  808 by (induct rule:list_induct2, simp_all)  nipkow@15110  809 nipkow@15110  810 nipkow@15392  811 subsubsection {* @{text rev} *}  wenzelm@13114  812 wenzelm@13142  813 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"  nipkow@13145  814 by (induct xs) auto  wenzelm@13114  815 wenzelm@13142  816 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"  nipkow@13145  817 by (induct xs) auto  wenzelm@13114  818 kleing@15870  819 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"  kleing@15870  820 by auto  kleing@15870  821 wenzelm@13142  822 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"  nipkow@13145  823 by (induct xs) auto  wenzelm@13114  824 wenzelm@13142  825 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"  nipkow@13145  826 by (induct xs) auto  wenzelm@13114  827 kleing@15870  828 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"  kleing@15870  829 by (cases xs) auto  kleing@15870  830 kleing@15870  831 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"  kleing@15870  832 by (cases xs) auto  kleing@15870  833 haftmann@21061  834 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"  haftmann@21061  835 apply (induct xs arbitrary: ys, force)  paulson@14208  836 apply (case_tac ys, simp, force)  nipkow@13145  837 done  wenzelm@13114  838 nipkow@15439  839 lemma inj_on_rev[iff]: "inj_on rev A"  nipkow@15439  840 by(simp add:inj_on_def)  nipkow@15439  841 wenzelm@13366  842 lemma rev_induct [case_names Nil snoc]:  wenzelm@13366  843  "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"  berghofe@15489  844 apply(simplesubst rev_rev_ident[symmetric])  nipkow@13145  845 apply(rule_tac list = "rev xs" in list.induct, simp_all)  nipkow@13145  846 done  wenzelm@13114  847 wenzelm@13366  848 lemma rev_exhaust [case_names Nil snoc]:  wenzelm@13366  849  "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"  nipkow@13145  850 by (induct xs rule: rev_induct) auto  wenzelm@13114  851 wenzelm@13366  852 lemmas rev_cases = rev_exhaust  wenzelm@13366  853 nipkow@18423  854 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"  nipkow@18423  855 by(rule rev_cases[of xs]) auto  nipkow@18423  856 wenzelm@13114  857 nipkow@15392  858 subsubsection {* @{text set} *}  wenzelm@13114  859 wenzelm@13142  860 lemma finite_set [iff]: "finite (set xs)"  nipkow@13145  861 by (induct xs) auto  wenzelm@13114  862 wenzelm@13142  863 lemma set_append [simp]: "set (xs @ ys) = (set xs \ set ys)"  nipkow@13145  864 by (induct xs) auto  wenzelm@13114  865 nipkow@17830  866 lemma hd_in_set[simp]: "xs \ [] \ hd xs : set xs"  nipkow@17830  867 by(cases xs) auto  oheimb@14099  868 wenzelm@13142  869 lemma set_subset_Cons: "set xs \ set (x # xs)"  nipkow@13145  870 by auto  wenzelm@13114  871 oheimb@14099  872 lemma set_ConsD: "y \ set (x # xs) \ y=x \ y \ set xs"  oheimb@14099  873 by auto  oheimb@14099  874 wenzelm@13142  875 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"  nipkow@13145  876 by (induct xs) auto  wenzelm@13114  877 nipkow@15245  878 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"  nipkow@15245  879 by(induct xs) auto  nipkow@15245  880 wenzelm@13142  881 lemma set_rev [simp]: "set (rev xs) = set xs"  nipkow@13145  882 by (induct xs) auto  wenzelm@13114  883 wenzelm@13142  884 lemma set_map [simp]: "set (map f xs) = f(set xs)"  nipkow@13145  885 by (induct xs) auto  wenzelm@13114  886 wenzelm@13142  887 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \ P x}"  nipkow@13145  888 by (induct xs) auto  wenzelm@13114  889 nipkow@32417  890 lemma set_upt [simp]: "set[i.. \ys zs. xs = ys @ x # zs"  nipkow@18049  895 proof (induct xs)  nipkow@26073  896  case Nil thus ?case by simp  nipkow@26073  897 next  nipkow@26073  898  case Cons thus ?case by (auto intro: Cons_eq_appendI)  nipkow@26073  899 qed  nipkow@26073  900 haftmann@26734  901 lemma in_set_conv_decomp: "x \ set xs \ (\ys zs. xs = ys @ x # zs)"  haftmann@26734  902  by (auto elim: split_list)  nipkow@26073  903 nipkow@26073  904 lemma split_list_first: "x : set xs \ \ys zs. xs = ys @ x # zs \ x \ set ys"  nipkow@26073  905 proof (induct xs)  nipkow@26073  906  case Nil thus ?case by simp  nipkow@18049  907 next  nipkow@18049  908  case (Cons a xs)  nipkow@18049  909  show ?case  nipkow@18049  910  proof cases  wenzelm@25221  911  assume "x = a" thus ?case using Cons by fastsimp  nipkow@18049  912  next  nipkow@26073  913  assume "x \ a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)  nipkow@26073  914  qed  nipkow@26073  915 qed  nipkow@26073  916 nipkow@26073  917 lemma in_set_conv_decomp_first:  nipkow@26073  918  "(x : set xs) = (\ys zs. xs = ys @ x # zs \ x \ set ys)"  haftmann@26734  919  by (auto dest!: split_list_first)  nipkow@26073  920 nipkow@26073  921 lemma split_list_last: "x : set xs \ \ys zs. xs = ys @ x # zs \ x \ set zs"  nipkow@26073  922 proof (induct xs rule:rev_induct)  nipkow@26073  923  case Nil thus ?case by simp  nipkow@26073  924 next  nipkow@26073  925  case (snoc a xs)  nipkow@26073  926  show ?case  nipkow@26073  927  proof cases  nipkow@26073  928  assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)  nipkow@26073  929  next  nipkow@26073  930  assume "x \ a" thus ?case using snoc by fastsimp  nipkow@18049  931  qed  nipkow@18049  932 qed  nipkow@18049  933 nipkow@26073  934 lemma in_set_conv_decomp_last:  nipkow@26073  935  "(x : set xs) = (\ys zs. xs = ys @ x # zs \ x \ set zs)"  haftmann@26734  936  by (auto dest!: split_list_last)  nipkow@26073  937 nipkow@26073  938 lemma split_list_prop: "\x \ set xs. P x \ \ys x zs. xs = ys @ x # zs & P x"  nipkow@26073  939 proof (induct xs)  nipkow@26073  940  case Nil thus ?case by simp  nipkow@26073  941 next  nipkow@26073  942  case Cons thus ?case  nipkow@26073  943  by(simp add:Bex_def)(metis append_Cons append.simps(1))  nipkow@26073  944 qed  nipkow@26073  945 nipkow@26073  946 lemma split_list_propE:  haftmann@26734  947  assumes "\x \ set xs. P x"  haftmann@26734  948  obtains ys x zs where "xs = ys @ x # zs" and "P x"  haftmann@26734  949 using split_list_prop [OF assms] by blast  nipkow@26073  950 nipkow@26073  951 lemma split_list_first_prop:  nipkow@26073  952  "\x \ set xs. P x \  nipkow@26073  953  \ys x zs. xs = ys@x#zs \ P x \ (\y \ set ys. \ P y)"  haftmann@26734  954 proof (induct xs)  nipkow@26073  955  case Nil thus ?case by simp  nipkow@26073  956 next  nipkow@26073  957  case (Cons x xs)  nipkow@26073  958  show ?case  nipkow@26073  959  proof cases  nipkow@26073  960  assume "P x"  haftmann@26734  961  thus ?thesis by simp  haftmann@26734  962  (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)  nipkow@26073  963  next  nipkow@26073  964  assume "\ P x"  nipkow@26073  965  hence "\x\set xs. P x" using Cons(2) by simp  nipkow@26073  966  thus ?thesis using \ P x Cons(1) by (metis append_Cons set_ConsD)  nipkow@26073  967  qed  nipkow@26073  968 qed  nipkow@26073  969 nipkow@26073  970 lemma split_list_first_propE:  haftmann@26734  971  assumes "\x \ set xs. P x"  haftmann@26734  972  obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\y \ set ys. \ P y"  haftmann@26734  973 using split_list_first_prop [OF assms] by blast  nipkow@26073  974 nipkow@26073  975 lemma split_list_first_prop_iff:  nipkow@26073  976  "(\x \ set xs. P x) \  nipkow@26073  977  (\ys x zs. xs = ys@x#zs \ P x \ (\y \ set ys. \ P y))"  haftmann@26734  978 by (rule, erule split_list_first_prop) auto  nipkow@26073  979 nipkow@26073  980 lemma split_list_last_prop:  nipkow@26073  981  "\x \ set xs. P x \  nipkow@26073  982  \ys x zs. xs = ys@x#zs \ P x \ (\z \ set zs. \ P z)"  nipkow@26073  983 proof(induct xs rule:rev_induct)  nipkow@26073  984  case Nil thus ?case by simp  nipkow@26073  985 next  nipkow@26073  986  case (snoc x xs)  nipkow@26073  987  show ?case  nipkow@26073  988  proof cases  nipkow@26073  989  assume "P x" thus ?thesis by (metis emptyE set_empty)  nipkow@26073  990  next  nipkow@26073  991  assume "\ P x"  nipkow@26073  992  hence "\x\set xs. P x" using snoc(2) by simp  nipkow@26073  993  thus ?thesis using \ P x snoc(1) by fastsimp  nipkow@26073  994  qed  nipkow@26073  995 qed  nipkow@26073  996 nipkow@26073  997 lemma split_list_last_propE:  haftmann@26734  998  assumes "\x \ set xs. P x"  haftmann@26734  999  obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\z \ set zs. \ P z"  haftmann@26734  1000 using split_list_last_prop [OF assms] by blast  nipkow@26073  1001 nipkow@26073  1002 lemma split_list_last_prop_iff:  nipkow@26073  1003  "(\x \ set xs. P x) \  nipkow@26073  1004  (\ys x zs. xs = ys@x#zs \ P x \ (\z \ set zs. \ P z))"  haftmann@26734  1005 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)  nipkow@26073  1006 nipkow@26073  1007 lemma finite_list: "finite A ==> EX xs. set xs = A"  haftmann@26734  1008  by (erule finite_induct)  haftmann@26734  1009  (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))  paulson@13508  1010 kleing@14388  1011 lemma card_length: "card (set xs) \ length xs"  kleing@14388  1012 by (induct xs) (auto simp add: card_insert_if)  wenzelm@13114  1013 haftmann@26442  1014 lemma set_minus_filter_out:  haftmann@26442  1015  "set xs - {y} = set (filter (\x. \ (x = y)) xs)"  haftmann@26442  1016  by (induct xs) auto  paulson@15168  1017 nipkow@15392  1018 subsubsection {* @{text filter} *}  wenzelm@13114  1019 wenzelm@13142  1020 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"  nipkow@13145  1021 by (induct xs) auto  wenzelm@13114  1022 nipkow@15305  1023 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"  nipkow@15305  1024 by (induct xs) simp_all  nipkow@15305  1025 wenzelm@13142  1026 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\x. Q x \ P x) xs"  nipkow@13145  1027 by (induct xs) auto  wenzelm@13114  1028 nipkow@16998  1029 lemma length_filter_le [simp]: "length (filter P xs) \ length xs"  nipkow@16998  1030 by (induct xs) (auto simp add: le_SucI)  nipkow@16998  1031 nipkow@18423  1032 lemma sum_length_filter_compl:  nipkow@18423  1033  "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"  nipkow@18423  1034 by(induct xs) simp_all  nipkow@18423  1035 wenzelm@13142  1036 lemma filter_True [simp]: "\x \ set xs. P x ==> filter P xs = xs"  nipkow@13145  1037 by (induct xs) auto  wenzelm@13114  1038 wenzelm@13142  1039 lemma filter_False [simp]: "\x \ set xs. \ P x ==> filter P xs = []"  nipkow@13145  1040 by (induct xs) auto  wenzelm@13114  1041 nipkow@16998  1042 lemma filter_empty_conv: "(filter P xs = []) = (\x\set xs. \ P x)"  nipkow@24349  1043 by (induct xs) simp_all  nipkow@16998  1044 nipkow@16998  1045 lemma filter_id_conv: "(filter P xs = xs) = (\x\set xs. P x)"  nipkow@16998  1046 apply (induct xs)  nipkow@16998  1047  apply auto  nipkow@16998  1048 apply(cut_tac P=P and xs=xs in length_filter_le)  nipkow@16998  1049 apply simp  nipkow@16998  1050 done  wenzelm@13114  1051 nipkow@16965  1052 lemma filter_map:  nipkow@16965  1053  "filter P (map f xs) = map f (filter (P o f) xs)"  nipkow@16965  1054 by (induct xs) simp_all  nipkow@16965  1055 nipkow@16965  1056 lemma length_filter_map[simp]:  nipkow@16965  1057  "length (filter P (map f xs)) = length(filter (P o f) xs)"  nipkow@16965  1058 by (simp add:filter_map)  nipkow@16965  1059 wenzelm@13142  1060 lemma filter_is_subset [simp]: "set (filter P xs) \ set xs"  nipkow@13145  1061 by auto  wenzelm@13114  1062 nipkow@15246  1063 lemma length_filter_less:  nipkow@15246  1064  "\ x : set xs; ~ P x \ \ length(filter P xs) < length xs"  nipkow@15246  1065 proof (induct xs)  nipkow@15246  1066  case Nil thus ?case by simp  nipkow@15246  1067 next  nipkow@15246  1068  case (Cons x xs) thus ?case  nipkow@15246  1069  apply (auto split:split_if_asm)  nipkow@15246  1070  using length_filter_le[of P xs] apply arith  nipkow@15246  1071  done  nipkow@15246  1072 qed  wenzelm@13114  1073 nipkow@15281  1074 lemma length_filter_conv_card:  nipkow@15281  1075  "length(filter p xs) = card{i. i < length xs & p(xs!i)}"  nipkow@15281  1076 proof (induct xs)  nipkow@15281  1077  case Nil thus ?case by simp  nipkow@15281  1078 next  nipkow@15281  1079  case (Cons x xs)  nipkow@15281  1080  let ?S = "{i. i < length xs & p(xs!i)}"  nipkow@15281  1081  have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)  nipkow@15281  1082  show ?case (is "?l = card ?S'")  nipkow@15281  1083  proof (cases)  nipkow@15281  1084  assume "p x"  nipkow@15281  1085  hence eq: "?S' = insert 0 (Suc  ?S)"  nipkow@25162  1086  by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)  nipkow@15281  1087  have "length (filter p (x # xs)) = Suc(card ?S)"  wenzelm@23388  1088  using Cons p x by simp  nipkow@15281  1089  also have "\ = Suc(card(Suc  ?S))" using fin  nipkow@15281  1090  by (simp add: card_image inj_Suc)  nipkow@15281  1091  also have "\ = card ?S'" using eq fin  nipkow@15281  1092  by (simp add:card_insert_if) (simp add:image_def)  nipkow@15281  1093  finally show ?thesis .  nipkow@15281  1094  next  nipkow@15281  1095  assume "\ p x"  nipkow@15281  1096  hence eq: "?S' = Suc  ?S"  nipkow@25162  1097  by(auto simp add: image_def split:nat.split elim:lessE)  nipkow@15281  1098  have "length (filter p (x # xs)) = card ?S"  wenzelm@23388  1099  using Cons \ p x by simp  nipkow@15281  1100  also have "\ = card(Suc  ?S)" using fin  nipkow@15281  1101  by (simp add: card_image inj_Suc)  nipkow@15281  1102  also have "\ = card ?S'" using eq fin  nipkow@15281  1103  by (simp add:card_insert_if)  nipkow@15281  1104  finally show ?thesis .  nipkow@15281  1105  qed  nipkow@15281  1106 qed  nipkow@15281  1107 nipkow@17629  1108 lemma Cons_eq_filterD:  nipkow@17629  1109  "x#xs = filter P ys \  nipkow@17629  1110  \us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs"  wenzelm@19585  1111  (is "_ \ \us vs. ?P ys us vs")  nipkow@17629  1112 proof(induct ys)  nipkow@17629  1113  case Nil thus ?case by simp  nipkow@17629  1114 next  nipkow@17629  1115  case (Cons y ys)  nipkow@17629  1116  show ?case (is "\x. ?Q x")  nipkow@17629  1117  proof cases  nipkow@17629  1118  assume Py: "P y"  nipkow@17629  1119  show ?thesis  nipkow@17629  1120  proof cases  wenzelm@25221  1121  assume "x = y"  wenzelm@25221  1122  with Py Cons.prems have "?Q []" by simp  wenzelm@25221  1123  then show ?thesis ..  nipkow@17629  1124  next  wenzelm@25221  1125  assume "x \ y"  wenzelm@25221  1126  with Py Cons.prems show ?thesis by simp  nipkow@17629  1127  qed  nipkow@17629  1128  next  wenzelm@25221  1129  assume "\ P y"  wenzelm@25221  1130  with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp  wenzelm@25221  1131  then have "?Q (y#us)" by simp  wenzelm@25221  1132  then show ?thesis ..  nipkow@17629  1133  qed  nipkow@17629  1134 qed  nipkow@17629  1135 nipkow@17629  1136 lemma filter_eq_ConsD:  nipkow@17629  1137  "filter P ys = x#xs \  nipkow@17629  1138  \us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs"  nipkow@17629  1139 by(rule Cons_eq_filterD) simp  nipkow@17629  1140 nipkow@17629  1141 lemma filter_eq_Cons_iff:  nipkow@17629  1142  "(filter P ys = x#xs) =  nipkow@17629  1143  (\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)"  nipkow@17629  1144 by(auto dest:filter_eq_ConsD)  nipkow@17629  1145 nipkow@17629  1146 lemma Cons_eq_filter_iff:  nipkow@17629  1147  "(x#xs = filter P ys) =  nipkow@17629  1148  (\us vs. ys = us @ x # vs \ (\u\set us. \ P u) \ P x \ xs = filter P vs)"  nipkow@17629  1149 by(auto dest:Cons_eq_filterD)  nipkow@17629  1150 krauss@19770  1151 lemma filter_cong[fundef_cong, recdef_cong]:  nipkow@17501  1152  "xs = ys \ (\x. x \ set ys \ P x = Q x) \ filter P xs = filter Q ys"  nipkow@17501  1153 apply simp  nipkow@17501  1154 apply(erule thin_rl)  nipkow@17501  1155 by (induct ys) simp_all  nipkow@17501  1156 nipkow@15281  1157 haftmann@26442  1158 subsubsection {* List partitioning *}  haftmann@26442  1159 haftmann@26442  1160 primrec partition :: "('a \ bool) \'a list \ 'a list \ 'a list" where  haftmann@26442  1161  "partition P [] = ([], [])"  haftmann@26442  1162  | "partition P (x # xs) =  haftmann@26442  1163  (let (yes, no) = partition P xs  haftmann@26442  1164  in if P x then (x # yes, no) else (yes, x # no))"  haftmann@26442  1165 haftmann@26442  1166 lemma partition_filter1:  haftmann@26442  1167  "fst (partition P xs) = filter P xs"  haftmann@26442  1168 by (induct xs) (auto simp add: Let_def split_def)  haftmann@26442  1169 haftmann@26442  1170 lemma partition_filter2:  haftmann@26442  1171  "snd (partition P xs) = filter (Not o P) xs"  haftmann@26442  1172 by (induct xs) (auto simp add: Let_def split_def)  haftmann@26442  1173 haftmann@26442  1174 lemma partition_P:  haftmann@26442  1175  assumes "partition P xs = (yes, no)"  haftmann@26442  1176  shows "(\p \ set yes. P p) \ (\p \ set no. \ P p)"  haftmann@26442  1177 proof -  haftmann@26442  1178  from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"  haftmann@26442  1179  by simp_all  haftmann@26442  1180  then show ?thesis by (simp_all add: partition_filter1 partition_filter2)  haftmann@26442  1181 qed  haftmann@26442  1182 haftmann@26442  1183 lemma partition_set:  haftmann@26442  1184  assumes "partition P xs = (yes, no)"  haftmann@26442  1185  shows "set yes \ set no = set xs"  haftmann@26442  1186 proof -  haftmann@26442  1187  from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"  haftmann@26442  1188  by simp_all  haftmann@26442  1189  then show ?thesis by (auto simp add: partition_filter1 partition_filter2)  haftmann@26442  1190 qed  haftmann@26442  1191 hoelzl@33639  1192 lemma partition_filter_conv[simp]:  hoelzl@33639  1193  "partition f xs = (filter f xs,filter (Not o f) xs)"  hoelzl@33639  1194 unfolding partition_filter2[symmetric]  hoelzl@33639  1195 unfolding partition_filter1[symmetric] by simp  hoelzl@33639  1196 hoelzl@33639  1197 declare partition.simps[simp del]  haftmann@26442  1198 nipkow@15392  1199 subsubsection {* @{text concat} *}  wenzelm@13114  1200 wenzelm@13142  1201 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"  nipkow@13145  1202 by (induct xs) auto  wenzelm@13114  1203 paulson@18447  1204 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\xs \ set xss. xs = [])"  nipkow@13145  1205 by (induct xss) auto  wenzelm@13114  1206 paulson@18447  1207 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\xs \ set xss. xs = [])"  nipkow@13145  1208 by (induct xss) auto  wenzelm@13114  1209 nipkow@24308  1210 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"  nipkow@13145  1211 by (induct xs) auto  wenzelm@13114  1212 nipkow@24476  1213 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"  nipkow@24349  1214 by (induct xs) auto  nipkow@24349  1215 wenzelm@13142  1216 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"  nipkow@13145  1217 by (induct xs) auto  wenzelm@13114  1218 wenzelm@13142  1219 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"  nipkow@13145  1220 by (induct xs) auto  wenzelm@13114  1221 wenzelm@13142  1222 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"  nipkow@13145  1223 by (induct xs) auto  wenzelm@13114  1224 wenzelm@13114  1225 nipkow@15392  1226 subsubsection {* @{text nth} *}  wenzelm@13114  1227 haftmann@29827  1228 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"  nipkow@13145  1229 by auto  wenzelm@13114  1230 haftmann@29827  1231 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"  nipkow@13145  1232 by auto  wenzelm@13114  1233 wenzelm@13142  1234 declare nth.simps [simp del]  wenzelm@13114  1235 wenzelm@13114  1236 lemma nth_append:  nipkow@24526  1237  "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"  nipkow@24526  1238 apply (induct xs arbitrary: n, simp)  paulson@14208  1239 apply (case_tac n, auto)  nipkow@13145  1240 done  wenzelm@13114  1241 nipkow@14402  1242 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"  wenzelm@25221  1243 by (induct xs) auto  nipkow@14402  1244 nipkow@14402  1245 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"  wenzelm@25221  1246 by (induct xs) auto  nipkow@14402  1247 nipkow@24526  1248 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"  nipkow@24526  1249 apply (induct xs arbitrary: n, simp)  paulson@14208  1250 apply (case_tac n, auto)  nipkow@13145  1251 done  wenzelm@13114  1252 nipkow@18423  1253 lemma hd_conv_nth: "xs \ [] \ hd xs = xs!0"  nipkow@18423  1254 by(cases xs) simp_all  nipkow@18423  1255 nipkow@18049  1256 nipkow@18049  1257 lemma list_eq_iff_nth_eq:  nipkow@24526  1258  "(xs = ys) = (length xs = length ys \ (ALL i set xs) = (\i < length xs. xs!i = x)"  nipkow@17501  1276 by(auto simp:set_conv_nth)  nipkow@17501  1277 nipkow@13145  1278 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"  nipkow@13145  1279 by (auto simp add: set_conv_nth)  wenzelm@13114  1280 wenzelm@13142  1281 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"  nipkow@13145  1282 by (auto simp add: set_conv_nth)  wenzelm@13114  1283 wenzelm@13114  1284 lemma all_nth_imp_all_set:  nipkow@13145  1285 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"  nipkow@13145  1286 by (auto simp add: set_conv_nth)  wenzelm@13114  1287 wenzelm@13114  1288 lemma all_set_conv_all_nth:  nipkow@13145  1289 "(\x \ set xs. P x) = (\i. i < length xs --> P (xs ! i))"  nipkow@13145  1290 by (auto simp add: set_conv_nth)  wenzelm@13114  1291 kleing@25296  1292 lemma rev_nth:  kleing@25296  1293  "n < size xs \ rev xs ! n = xs ! (length xs - Suc n)"  kleing@25296  1294 proof (induct xs arbitrary: n)  kleing@25296  1295  case Nil thus ?case by simp  kleing@25296  1296 next  kleing@25296  1297  case (Cons x xs)  kleing@25296  1298  hence n: "n < Suc (length xs)" by simp  kleing@25296  1299  moreover  kleing@25296  1300  { assume "n < length xs"  kleing@25296  1301  with n obtain n' where "length xs - n = Suc n'"  kleing@25296  1302  by (cases "length xs - n", auto)  kleing@25296  1303  moreover  kleing@25296  1304  then have "length xs - Suc n = n'" by simp  kleing@25296  1305  ultimately  kleing@25296  1306  have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp  kleing@25296  1307  }  kleing@25296  1308  ultimately  kleing@25296  1309  show ?case by (clarsimp simp add: Cons nth_append)  kleing@25296  1310 qed  wenzelm@13114  1311 nipkow@31159  1312 lemma Skolem_list_nth:  nipkow@31159  1313  "(ALL i (xs[i:=x])!j = (if i = j then x else xs!j)"  nipkow@24526  1338 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)  wenzelm@13114  1339 wenzelm@13142  1340 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"  nipkow@13145  1341 by (simp add: nth_list_update)  wenzelm@13114  1342 nipkow@24526  1343 lemma nth_list_update_neq [simp]: "i \ j ==> xs[i:=x]!j = xs!j"  nipkow@24526  1344 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)  wenzelm@13114  1345 nipkow@24526  1346 lemma list_update_id[simp]: "xs[i := xs!i] = xs"  nipkow@24526  1347 by (induct xs arbitrary: i) (simp_all split:nat.splits)  nipkow@24526  1348 nipkow@24526  1349 lemma list_update_beyond[simp]: "length xs \ i \ xs[i:=x] = xs"  nipkow@24526  1350 apply (induct xs arbitrary: i)  nipkow@17501  1351  apply simp  nipkow@17501  1352 apply (case_tac i)  nipkow@17501  1353 apply simp_all  nipkow@17501  1354 done  nipkow@17501  1355 nipkow@31077  1356 lemma list_update_nonempty[simp]: "xs[k:=x] = [] \ xs=[]"  nipkow@31077  1357 by(metis length_0_conv length_list_update)  nipkow@31077  1358 wenzelm@13114  1359 lemma list_update_same_conv:  nipkow@24526  1360 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"  nipkow@24526  1361 by (induct xs arbitrary: i) (auto split: nat.split)  wenzelm@13114  1362 nipkow@14187  1363 lemma list_update_append1:  nipkow@24526  1364  "i < size xs \ (xs @ ys)[i:=x] = xs[i:=x] @ ys"  nipkow@24526  1365 apply (induct xs arbitrary: i, simp)  nipkow@14187  1366 apply(simp split:nat.split)  nipkow@14187  1367 done  nipkow@14187  1368 kleing@15868  1369 lemma list_update_append:  nipkow@24526  1370  "(xs @ ys) [n:= x] =  kleing@15868  1371  (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"  nipkow@24526  1372 by (induct xs arbitrary: n) (auto split:nat.splits)  kleing@15868  1373 nipkow@14402  1374 lemma list_update_length [simp]:  nipkow@14402  1375  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"  nipkow@14402  1376 by (induct xs, auto)  nipkow@14402  1377 nipkow@31264  1378 lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"  nipkow@31264  1379 by(induct xs arbitrary: k)(auto split:nat.splits)  nipkow@31264  1380 nipkow@31264  1381 lemma rev_update:  nipkow@31264  1382  "k < length xs \ rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"  nipkow@31264  1383 by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)  nipkow@31264  1384 wenzelm@13114  1385 lemma update_zip:  nipkow@31080  1386  "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"  nipkow@24526  1387 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)  nipkow@24526  1388 nipkow@24526  1389 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"  nipkow@24526  1390 by (induct xs arbitrary: i) (auto split: nat.split)  wenzelm@13114  1391 wenzelm@13114  1392 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"  nipkow@13145  1393 by (blast dest!: set_update_subset_insert [THEN subsetD])  wenzelm@13114  1394 nipkow@24526  1395 lemma set_update_memI: "n < length xs \ x \ set (xs[n := x])"  nipkow@24526  1396 by (induct xs arbitrary: n) (auto split:nat.splits)  kleing@15868  1397 nipkow@31077  1398 lemma list_update_overwrite[simp]:  haftmann@24796  1399  "xs [i := x, i := y] = xs [i := y]"  nipkow@31077  1400 apply (induct xs arbitrary: i) apply simp  nipkow@31077  1401 apply (case_tac i, simp_all)  haftmann@24796  1402 done  haftmann@24796  1403 haftmann@24796  1404 lemma list_update_swap:  haftmann@24796  1405  "i \ i' \ xs [i := x, i' := x'] = xs [i' := x', i := x]"  haftmann@24796  1406 apply (induct xs arbitrary: i i')  haftmann@24796  1407 apply simp  haftmann@24796  1408 apply (case_tac i, case_tac i')  haftmann@24796  1409 apply auto  haftmann@24796  1410 apply (case_tac i')  haftmann@24796  1411 apply auto  haftmann@24796  1412 done  haftmann@24796  1413 haftmann@29827  1414 lemma list_update_code [code]:  haftmann@29827  1415  "[][i := y] = []"  haftmann@29827  1416  "(x # xs)[0 := y] = y # xs"  haftmann@29827  1417  "(x # xs)[Suc i := y] = x # xs[i := y]"  haftmann@29827  1418  by simp_all  haftmann@29827  1419 wenzelm@13114  1420 nipkow@15392  1421 subsubsection {* @{text last} and @{text butlast} *}  wenzelm@13114  1422 wenzelm@13142  1423 lemma last_snoc [simp]: "last (xs @ [x]) = x"  nipkow@13145  1424 by (induct xs) auto  wenzelm@13114  1425 wenzelm@13142  1426 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"  nipkow@13145  1427 by (induct xs) auto  wenzelm@13114  1428 nipkow@14302  1429 lemma last_ConsL: "xs = [] \ last(x#xs) = x"  nipkow@14302  1430 by(simp add:last.simps)  nipkow@14302  1431 nipkow@14302  1432 lemma last_ConsR: "xs \ [] \ last(x#xs) = last xs"  nipkow@14302  1433 by(simp add:last.simps)  nipkow@14302  1434 nipkow@14302  1435 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"  nipkow@14302  1436 by (induct xs) (auto)  nipkow@14302  1437 nipkow@14302  1438 lemma last_appendL[simp]: "ys = [] \ last(xs @ ys) = last xs"  nipkow@14302  1439 by(simp add:last_append)  nipkow@14302  1440 nipkow@14302  1441 lemma last_appendR[simp]: "ys \ [] \ last(xs @ ys) = last ys"  nipkow@14302  1442 by(simp add:last_append)  nipkow@14302  1443 nipkow@17762  1444 lemma hd_rev: "xs \ [] \ hd(rev xs) = last xs"  nipkow@17762  1445 by(rule rev_exhaust[of xs]) simp_all  nipkow@17762  1446 nipkow@17762  1447 lemma last_rev: "xs \ [] \ last(rev xs) = hd xs"  nipkow@17762  1448 by(cases xs) simp_all  nipkow@17762  1449 nipkow@17765  1450 lemma last_in_set[simp]: "as \ [] \ last as \ set as"  nipkow@17765  1451 by (induct as) auto  nipkow@17762  1452 wenzelm@13142  1453 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"  nipkow@13145  1454 by (induct xs rule: rev_induct) auto  wenzelm@13114  1455 wenzelm@13114  1456 lemma butlast_append:  nipkow@24526  1457  "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"  nipkow@24526  1458 by (induct xs arbitrary: ys) auto  wenzelm@13114  1459 wenzelm@13142  1460 lemma append_butlast_last_id [simp]:  nipkow@13145  1461 "xs \ [] ==> butlast xs @ [last xs] = xs"  nipkow@13145  1462 by (induct xs) auto  wenzelm@13114  1463 wenzelm@13142  1464 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"  nipkow@13145  1465 by (induct xs) (auto split: split_if_asm)  wenzelm@13114  1466 wenzelm@13114  1467 lemma in_set_butlast_appendI:  nipkow@13145  1468 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"  nipkow@13145  1469 by (auto dest: in_set_butlastD simp add: butlast_append)  wenzelm@13114  1470 nipkow@24526  1471 lemma last_drop[simp]: "n < length xs \ last (drop n xs) = last xs"  nipkow@24526  1472 apply (induct xs arbitrary: n)  nipkow@17501  1473  apply simp  nipkow@17501  1474 apply (auto split:nat.split)  nipkow@17501  1475 done  nipkow@17501  1476 huffman@30128  1477 lemma last_conv_nth: "xs\[] \ last xs = xs!(length xs - 1)"  nipkow@17589  1478 by(induct xs)(auto simp:neq_Nil_conv)  nipkow@17589  1479 huffman@30128  1480 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"  huffman@26584  1481 by (induct xs, simp, case_tac xs, simp_all)  huffman@26584  1482 nipkow@31077  1483 lemma last_list_update:  nipkow@31077  1484  "xs \ [] \ last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"  nipkow@31077  1485 by (auto simp: last_conv_nth)  nipkow@31077  1486 nipkow@31077  1487 lemma butlast_list_update:  nipkow@31077  1488  "butlast(xs[k:=x]) =  nipkow@31077  1489  (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"  nipkow@31077  1490 apply(cases xs rule:rev_cases)  nipkow@31077  1491 apply simp  nipkow@31077  1492 apply(simp add:list_update_append split:nat.splits)  nipkow@31077  1493 done  nipkow@31077  1494 haftmann@24796  1495 nipkow@15392  1496 subsubsection {* @{text take} and @{text drop} *}  wenzelm@13114  1497 wenzelm@13142  1498 lemma take_0 [simp]: "take 0 xs = []"  nipkow@13145  1499 by (induct xs) auto  wenzelm@13114  1500 wenzelm@13142  1501 lemma drop_0 [simp]: "drop 0 xs = xs"  nipkow@13145  1502 by (induct xs) auto  wenzelm@13114  1503 wenzelm@13142  1504 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"  nipkow@13145  1505 by simp  wenzelm@13114  1506 wenzelm@13142  1507 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"  nipkow@13145  1508 by simp  wenzelm@13114  1509 wenzelm@13142  1510 declare take_Cons [simp del] and drop_Cons [simp del]  wenzelm@13114  1511 huffman@30128  1512 lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"  huffman@30128  1513  unfolding One_nat_def by simp  huffman@30128  1514 huffman@30128  1515 lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"  huffman@30128  1516  unfolding One_nat_def by simp  huffman@30128  1517 nipkow@15110  1518 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"  nipkow@15110  1519 by(clarsimp simp add:neq_Nil_conv)  nipkow@15110  1520 nipkow@14187  1521 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"  nipkow@14187  1522 by(cases xs, simp_all)  nipkow@14187  1523 huffman@26584  1524 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"  huffman@26584  1525 by (induct xs arbitrary: n) simp_all  huffman@26584  1526 nipkow@24526  1527 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"  nipkow@24526  1528 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)  nipkow@24526  1529 huffman@26584  1530 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"  huffman@26584  1531 by (cases n, simp, cases xs, auto)  huffman@26584  1532 huffman@26584  1533 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"  huffman@26584  1534 by (simp only: drop_tl)  huffman@26584  1535 nipkow@24526  1536 lemma nth_via_drop: "drop n xs = y#ys \ xs!n = y"  nipkow@24526  1537 apply (induct xs arbitrary: n, simp)  nipkow@14187  1538 apply(simp add:drop_Cons nth_Cons split:nat.splits)  nipkow@14187  1539 done  nipkow@14187  1540 nipkow@13913  1541 lemma take_Suc_conv_app_nth:  nipkow@24526  1542  "i < length xs \ take (Suc i) xs = take i xs @ [xs!i]"  nipkow@24526  1543 apply (induct xs arbitrary: i, simp)  paulson@14208  1544 apply (case_tac i, auto)  nipkow@13913  1545 done  nipkow@13913  1546 mehta@14591  1547 lemma drop_Suc_conv_tl:  nipkow@24526  1548  "i < length xs \ (xs!i) # (drop (Suc i) xs) = drop i xs"  nipkow@24526  1549 apply (induct xs arbitrary: i, simp)  mehta@14591  1550 apply (case_tac i, auto)  mehta@14591  1551 done  mehta@14591  1552 nipkow@24526  1553 lemma length_take [simp]: "length (take n xs) = min (length xs) n"  nipkow@24526  1554 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  nipkow@24526  1555 nipkow@24526  1556 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"  nipkow@24526  1557 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  nipkow@24526  1558 nipkow@24526  1559 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"  nipkow@24526  1560 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  nipkow@24526  1561 nipkow@24526  1562 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"  nipkow@24526  1563 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  wenzelm@13114  1564 wenzelm@13142  1565 lemma take_append [simp]:  nipkow@24526  1566  "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"  nipkow@24526  1567 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  wenzelm@13114  1568 wenzelm@13142  1569 lemma drop_append [simp]:  nipkow@24526  1570  "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"  nipkow@24526  1571 by (induct n arbitrary: xs) (auto, case_tac xs, auto)  nipkow@24526  1572 nipkow@24526  1573 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"  nipkow@24526  1574 apply (induct m arbitrary: xs n, auto)  paulson@14208  1575 apply (case_tac xs, auto)  nipkow@15236  1576 apply (case_tac n, auto)  nipkow@13145  1577 done  wenzelm@13114  1578 nipkow@24526  1579 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"  nipkow@24526  1580 apply (induct m arbitrary: xs, auto)  paulson@14208  1581 apply (case_tac xs, auto)  nipkow@13145  1582 done  wenzelm@13114  1583 nipkow@24526  1584 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"  nipkow@24526  1585 apply (induct m arbitrary: xs n, auto)  paulson@14208  1586 apply (case_tac xs, auto)  nipkow@13145  1587 done  wenzelm@13114  1588 nipkow@24526  1589 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"  nipkow@24526  1590 apply(induct xs arbitrary: m n)  nipkow@14802  1591  apply simp  nipkow@14802  1592 apply(simp add: take_Cons drop_Cons split:nat.split)  nipkow@14802  1593 done  nipkow@14802  1594 nipkow@24526  1595 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"  nipkow@24526  1596 apply (induct n arbitrary: xs, auto)  paulson@14208  1597 apply (case_tac xs, auto)  nipkow@13145  1598 done  wenzelm@13114  1599 nipkow@24526  1600 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \ xs = [])"  nipkow@24526  1601 apply(induct xs arbitrary: n)  nipkow@15110  1602  apply simp  nipkow@15110  1603 apply(simp add:take_Cons split:nat.split)  nipkow@15110  1604 done  nipkow@15110  1605 nipkow@24526  1606 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"  nipkow@24526  1607 apply(induct xs arbitrary: n)  nipkow@15110  1608 apply simp  nipkow@15110  1609 apply(simp add:drop_Cons split:nat.split)  nipkow@15110  1610 done  nipkow@15110  1611 nipkow@24526  1612 lemma take_map: "take n (map f xs) = map f (take n xs)"  nipkow@24526  1613 apply (induct n arbitrary: xs, auto)  paulson@14208  1614 apply (case_tac xs, auto)  nipkow@13145  1615 done  wenzelm@13114  1616 nipkow@24526  1617 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"  nipkow@24526  1618 apply (induct n arbitrary: xs, auto)  paulson@14208  1619 apply (case_tac xs, auto)  nipkow@13145  1620 done  wenzelm@13114  1621 nipkow@24526  1622 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"  nipkow@24526  1623 apply (induct xs arbitrary: i, auto)  paulson@14208  1624 apply (case_tac i, auto)  nipkow@13145  1625 done  wenzelm@13114  1626 nipkow@24526  1627 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"  nipkow@24526  1628 apply (induct xs arbitrary: i, auto)  paulson@14208  1629 apply (case_tac i, auto)  nipkow@13145  1630 done  wenzelm@13114  1631 nipkow@24526  1632 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"  nipkow@24526  1633 apply (induct xs arbitrary: i n, auto)  paulson@14208  1634 apply (case_tac n, blast)  paulson@14208  1635 apply (case_tac i, auto)  nipkow@13145  1636 done  wenzelm@13114  1637 wenzelm@13142  1638 lemma nth_drop [simp]:  nipkow@24526  1639  "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"  nipkow@24526  1640 apply (induct n arbitrary: xs i, auto)  paulson@14208  1641 apply (case_tac xs, auto)  nipkow@13145  1642 done  nipkow@3507  1643 huffman@26584  1644 lemma butlast_take:  huffman@30128  1645  "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"  huffman@26584  1646 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)  huffman@26584  1647 huffman@26584  1648 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"  huffman@30128  1649 by (simp add: butlast_conv_take drop_take add_ac)  huffman@26584  1650 huffman@26584  1651 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"  huffman@26584  1652 by (simp add: butlast_conv_take min_max.inf_absorb1)  huffman@26584  1653 huffman@26584  1654 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"  huffman@30128  1655 by (simp add: butlast_conv_take drop_take add_ac)  huffman@26584  1656 nipkow@18423  1657 lemma hd_drop_conv_nth: "\ xs \ []; n < length xs \ \ hd(drop n xs) = xs!n"  nipkow@18423  1658 by(simp add: hd_conv_nth)  nipkow@18423  1659 nipkow@24526  1660 lemma set_take_subset: "set(take n xs) \ set xs"  nipkow@24526  1661 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)  nipkow@24526  1662 nipkow@24526  1663 lemma set_drop_subset: "set(drop n xs) \ set xs"  nipkow@24526  1664 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)  nipkow@14025  1665 nipkow@14187  1666 lemma in_set_takeD: "x : set(take n xs) \ x : set xs"  nipkow@14187  1667 using set_take_subset by fast  nipkow@14187  1668 nipkow@14187  1669 lemma in_set_dropD: "x : set(drop n xs) \ x : set xs"  nipkow@14187  1670 using set_drop_subset by fast  nipkow@14187  1671 wenzelm@13114  1672 lemma append_eq_conv_conj:  nipkow@24526  1673  "(xs @ ys = zs) = (xs = take (length xs) zs \ ys = drop (length xs) zs)"  nipkow@24526  1674 apply (induct xs arbitrary: zs, simp, clarsimp)  paulson@14208  1675 apply (case_tac zs, auto)  nipkow@13145  1676 done  wenzelm@13142  1677 nipkow@24526  1678 lemma take_add:  nipkow@24526  1679  "i+j \ length(xs) \ take (i+j) xs = take i xs @ take j (drop i xs)"  nipkow@24526  1680 apply (induct xs arbitrary: i, auto)  nipkow@24526  1681 apply (case_tac i, simp_all)  paulson@14050  1682 done  paulson@14050  1683 nipkow@14300  1684 lemma append_eq_append_conv_if:  nipkow@24526  1685  "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =  nipkow@14300  1686  (if size xs\<^isub>1 \ size ys\<^isub>1  nipkow@14300  1687  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  1688  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  1689 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)  nipkow@14300  1690  apply simp  nipkow@14300  1691 apply(case_tac ys\<^isub>1)  nipkow@14300  1692 apply simp_all  nipkow@14300  1693 done  nipkow@14300  1694 nipkow@15110  1695 lemma take_hd_drop:  huffman@30079  1696  "n < length xs \ take n xs @ [hd (drop n xs)] = take (Suc n) xs"  nipkow@24526  1697 apply(induct xs arbitrary: n)  nipkow@15110  1698 apply simp  nipkow@15110  1699 apply(simp add:drop_Cons split:nat.split)  nipkow@15110  1700 done  nipkow@15110  1701 nipkow@17501  1702 lemma id_take_nth_drop:  nipkow@17501  1703  "i < length xs \ xs = take i xs @ xs!i # drop (Suc i) xs"  nipkow@17501  1704 proof -  nipkow@17501  1705  assume si: "i < length xs"  nipkow@17501  1706  hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto  nipkow@17501  1707  moreover  nipkow@17501  1708  from si have "take (Suc i) xs = take i xs @ [xs!i]"  nipkow@17501  1709  apply (rule_tac take_Suc_conv_app_nth) by arith  nipkow@17501  1710  ultimately show ?thesis by auto  nipkow@17501  1711 qed  nipkow@17501  1712   nipkow@17501  1713 lemma upd_conv_take_nth_drop:  nipkow@17501  1714  "i < length xs \ xs[i:=a] = take i xs @ a # drop (Suc i) xs"  nipkow@17501  1715 proof -  nipkow@17501  1716  assume i: "i < length xs"  nipkow@17501  1717  have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"  nipkow@17501  1718  by(rule arg_cong[OF id_take_nth_drop[OF i]])  nipkow@17501  1719  also have "\ = take i xs @ a # drop (Suc i) xs"  nipkow@17501  1720  using i by (simp add: list_update_append)  nipkow@17501  1721  finally show ?thesis .  nipkow@17501  1722 qed  nipkow@17501  1723 haftmann@24796  1724 lemma nth_drop':  haftmann@24796  1725  "i < length xs \ xs ! i # drop (Suc i) xs = drop i xs"  haftmann@24796  1726 apply (induct i arbitrary: xs)  haftmann@24796  1727 apply (simp add: neq_Nil_conv)  haftmann@24796  1728 apply (erule exE)+  haftmann@24796  1729 apply simp  haftmann@24796  1730 apply (case_tac xs)  haftmann@24796  1731 apply simp_all  haftmann@24796  1732 done  haftmann@24796  1733 wenzelm@13114  1734 nipkow@15392  1735 subsubsection {* @{text takeWhile} and @{text dropWhile} *}  wenzelm@13114  1736 hoelzl@33639  1737 lemma length_takeWhile_le: "length (takeWhile P xs) \ length xs"  hoelzl@33639  1738  by (induct xs) auto  hoelzl@33639  1739 wenzelm@13142  1740 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"  nipkow@13145  1741 by (induct xs) auto  wenzelm@13114  1742 wenzelm@13142  1743 lemma takeWhile_append1 [simp]:  nipkow@13145  1744 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"  nipkow@13145  1745 by (induct xs) auto  wenzelm@13114  1746 wenzelm@13142  1747 lemma takeWhile_append2 [simp]:  nipkow@13145  1748 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"  nipkow@13145  1749 by (induct xs) auto  wenzelm@13114  1750 wenzelm@13142  1751 lemma takeWhile_tail: "\ P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"  nipkow@13145  1752 by (induct xs) auto  wenzelm@13114  1753 hoelzl@33639  1754 lemma takeWhile_nth: "j < length (takeWhile P xs) \ takeWhile P xs ! j = xs ! j"  hoelzl@33639  1755 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto  hoelzl@33639  1756 hoelzl@33639  1757 lemma dropWhile_nth: "j < length (dropWhile P xs) \ dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"  hoelzl@33639  1758 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto  hoelzl@33639  1759 hoelzl@33639  1760 lemma length_dropWhile_le: "length (dropWhile P xs) \ length xs"  hoelzl@33639  1761 by (induct xs) auto  hoelzl@33639  1762 wenzelm@13142  1763 lemma dropWhile_append1 [simp]:  nipkow@13145  1764 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"  nipkow@13145  1765 by (induct xs) auto  wenzelm@13114  1766 wenzelm@13142  1767 lemma dropWhile_append2 [simp]:  nipkow@13145  1768 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"  nipkow@13145  1769 by (induct xs) auto  wenzelm@13114  1770 krauss@23971  1771 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \ P x"  nipkow@13145  1772 by (induct xs) (auto split: split_if_asm)  wenzelm@13114  1773 nipkow@13913  1774 lemma takeWhile_eq_all_conv[simp]:  nipkow@13913  1775  "(takeWhile P xs = xs) = (\x \ set xs. P x)"  nipkow@13913  1776 by(induct xs, auto)  nipkow@13913  1777 nipkow@13913  1778 lemma dropWhile_eq_Nil_conv[simp]:  nipkow@13913  1779  "(dropWhile P xs = []) = (\x \ set xs. P x)"  nipkow@13913  1780 by(induct xs, auto)  nipkow@13913  1781 nipkow@13913  1782 lemma dropWhile_eq_Cons_conv:  nipkow@13913  1783  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \ P y)"  nipkow@13913  1784 by(induct xs, auto)  nipkow@13913  1785 nipkow@31077  1786 lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"  nipkow@31077  1787 by (induct xs) (auto dest: set_takeWhileD)  nipkow@31077  1788 nipkow@31077  1789 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"  nipkow@31077  1790 by (induct xs) auto  nipkow@31077  1791 hoelzl@33639  1792 lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \ f) xs)"  hoelzl@33639  1793 by (induct xs) auto  hoelzl@33639  1794 hoelzl@33639  1795 lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \ f) xs)"  hoelzl@33639  1796 by (induct xs) auto  hoelzl@33639  1797 hoelzl@33639  1798 lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"  hoelzl@33639  1799 by (induct xs) auto  hoelzl@33639  1800 hoelzl@33639  1801 lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"  hoelzl@33639  1802 by (induct xs) auto  hoelzl@33639  1803 hoelzl@33639  1804 lemma hd_dropWhile:  hoelzl@33639  1805  "dropWhile P xs \ [] \ \ P (hd (dropWhile P xs))"  hoelzl@33639  1806 using assms by (induct xs) auto  hoelzl@33639  1807 hoelzl@33639  1808 lemma takeWhile_eq_filter:  hoelzl@33639  1809  assumes "\ x. x \ set (dropWhile P xs) \ \ P x"  hoelzl@33639  1810  shows "takeWhile P xs = filter P xs"  hoelzl@33639  1811 proof -  hoelzl@33639  1812  have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)"  hoelzl@33639  1813  by simp  hoelzl@33639  1814  have B: "filter P (dropWhile P xs) = []"  hoelzl@33639  1815  unfolding filter_empty_conv using assms by blast  hoelzl@33639  1816  have "filter P xs = takeWhile P xs"  hoelzl@33639  1817  unfolding A filter_append B  hoelzl@33639  1818  by (auto simp add: filter_id_conv dest: set_takeWhileD)  hoelzl@33639  1819  thus ?thesis ..  hoelzl@33639  1820 qed  hoelzl@33639  1821 hoelzl@33639  1822 lemma takeWhile_eq_take_P_nth:  hoelzl@33639  1823  "\ \ i. \ i < n ; i < length xs \ \ P (xs ! i) ; n < length xs \ \ P (xs ! n) \ \  hoelzl@33639  1824  takeWhile P xs = take n xs"  hoelzl@33639  1825 proof (induct xs arbitrary: n)  hoelzl@33639  1826  case (Cons x xs)  hoelzl@33639  1827  thus ?case  hoelzl@33639  1828  proof (cases n)  hoelzl@33639  1829  case (Suc n') note this[simp]  hoelzl@33639  1830  have "P x" using Cons.prems(1)[of 0] by simp  hoelzl@33639  1831  moreover have "takeWhile P xs = take n' xs"  hoelzl@33639  1832  proof (rule Cons.hyps)  hoelzl@33639  1833  case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp  hoelzl@33639  1834  next case goal2 thus ?case using Cons by auto  hoelzl@33639  1835  qed  hoelzl@33639  1836  ultimately show ?thesis by simp  hoelzl@33639  1837  qed simp  hoelzl@33639  1838 qed simp  hoelzl@33639  1839 hoelzl@33639  1840 lemma nth_length_takeWhile:  hoelzl@33639  1841  "length (takeWhile P xs) < length xs \ \ P (xs ! length (takeWhile P xs))"  hoelzl@33639  1842 by (induct xs) auto  hoelzl@33639  1843 hoelzl@33639  1844 lemma length_takeWhile_less_P_nth:  hoelzl@33639  1845  assumes all: "\ i. i < j \ P (xs ! i)" and "j \ length xs"  hoelzl@33639  1846  shows "j \ length (takeWhile P xs)"  hoelzl@33639  1847 proof (rule classical)  hoelzl@33639  1848  assume "\ ?thesis"  hoelzl@33639  1849  hence "length (takeWhile P xs) < length xs" using assms by simp  hoelzl@33639  1850  thus ?thesis using all \ ?thesis nth_length_takeWhile[of P xs] by auto  hoelzl@33639  1851 qed  nipkow@31077  1852 nipkow@17501  1853 text{* The following two lemmmas could be generalized to an arbitrary  nipkow@17501  1854 property. *}  nipkow@17501  1855 nipkow@17501  1856 lemma takeWhile_neq_rev: "\distinct xs; x \ set xs\ \  nipkow@17501  1857  takeWhile (\y. y \ x) (rev xs) = rev (tl (dropWhile (\y. y \ x) xs))"  nipkow@17501  1858 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])  nipkow@17501  1859 nipkow@17501  1860 lemma dropWhile_neq_rev: "\distinct xs; x \ set xs\ \  nipkow@17501  1861  dropWhile (\y. y \ x) (rev xs) = x # rev (takeWhile (\y. y \ x) xs)"  nipkow@17501  1862 apply(induct xs)  nipkow@17501  1863  apply simp  nipkow@17501  1864 apply auto  nipkow@17501  1865 apply(subst dropWhile_append2)  nipkow@17501  1866 apply auto  nipkow@17501  1867 done  nipkow@17501  1868 nipkow@18423  1869 lemma takeWhile_not_last:  nipkow@18423  1870  "\ xs \ []; distinct xs\ \ takeWhile (\y. y \ last xs) xs = butlast xs"  nipkow@18423  1871 apply(induct xs)  nipkow@18423  1872  apply simp  nipkow@18423  1873 apply(case_tac xs)  nipkow@18423  1874 apply(auto)  nipkow@18423  1875 done  nipkow@18423  1876 krauss@19770  1877 lemma takeWhile_cong [fundef_cong, recdef_cong]:  krauss@18336  1878  "[| l = k; !!x. x : set l ==> P x = Q x |]  krauss@18336  1879  ==> takeWhile P l = takeWhile Q k"  nipkow@24349  1880 by (induct k arbitrary: l) (simp_all)  krauss@18336  1881 krauss@19770  1882 lemma dropWhile_cong [fundef_cong, recdef_cong]:  krauss@18336  1883  "[| l = k; !!x. x : set l ==> P x = Q x |]  krauss@18336  1884  ==> dropWhile P l = dropWhile Q k"  nipkow@24349  1885 by (induct k arbitrary: l, simp_all)  krauss@18336  1886 wenzelm@13114  1887 nipkow@15392  1888 subsubsection {* @{text zip} *}  wenzelm@13114  1889 wenzelm@13142  1890 lemma zip_Nil [simp]: "zip [] ys = []"  nipkow@13145  1891 by (induct ys) auto  wenzelm@13114  1892 wenzelm@13142  1893 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"  nipkow@13145  1894 by simp  wenzelm@13114  1895 wenzelm@13142  1896 declare zip_Cons [simp del]  wenzelm@13114  1897 nipkow@15281  1898 lemma zip_Cons1:  nipkow@15281  1899  "zip (x#xs) ys = (case ys of [] \ [] | y#ys \ (x,y)#zip xs ys)"  nipkow@15281  1900 by(auto split:list.split)  nipkow@15281  1901 wenzelm@13142  1902 lemma length_zip [simp]:  krauss@22493  1903 "length (zip xs ys) = min (length xs) (length ys)"  krauss@22493  1904 by (induct xs ys rule:list_induct2') auto  wenzelm@13114  1905 wenzelm@13114  1906 lemma zip_append1:  krauss@22493  1907 "zip (xs @ ys) zs =  nipkow@13145  1908 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"  krauss@22493  1909 by (induct xs zs rule:list_induct2') auto  wenzelm@13114  1910 wenzelm@13114  1911 lemma zip_append2:  krauss@22493  1912 "zip xs (ys @ zs) =  nipkow@13145  1913 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"  krauss@22493  1914 by (induct xs ys rule:list_induct2') auto  wenzelm@13114  1915 wenzelm@13142  1916 lemma zip_append [simp]:  wenzelm@13142  1917  "[| length xs = length us; length ys = length vs |] ==>  nipkow@13145  1918 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"  nipkow@13145  1919 by (simp add: zip_append1)  wenzelm@13114  1920 wenzelm@13114  1921 lemma zip_rev:  nipkow@14247  1922 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"  nipkow@14247  1923 by (induct rule:list_induct2, simp_all)  wenzelm@13114  1924 hoelzl@33639  1925 lemma zip_map_map:  hoelzl@33639  1926  "zip (map f xs) (map g ys) = map (\ (x, y). (f x, g y)) (zip xs ys)"  hoelzl@33639  1927 proof (induct xs arbitrary: ys)  hoelzl@33639  1928  case (Cons x xs) note Cons_x_xs = Cons.hyps  hoelzl@33639  1929  show ?case  hoelzl@33639  1930  proof (cases ys)  hoelzl@33639  1931  case (Cons y ys')  hoelzl@33639  1932  show ?thesis unfolding Cons using Cons_x_xs by simp  hoelzl@33639  1933  qed simp  hoelzl@33639  1934 qed simp  hoelzl@33639  1935 hoelzl@33639  1936 lemma zip_map1:  hoelzl@33639  1937  "zip (map f xs) ys = map (\(x, y). (f x, y)) (zip xs ys)"  hoelzl@33639  1938 using zip_map_map[of f xs "\x. x" ys] by simp  hoelzl@33639  1939 hoelzl@33639  1940 lemma zip_map2:  hoelzl@33639  1941  "zip xs (map f ys) = map (\(x, y). (x, f y)) (zip xs ys)"  hoelzl@33639  1942 using zip_map_map[of "\x. x" xs f ys] by simp  hoelzl@33639  1943 nipkow@23096  1944 lemma map_zip_map:  hoelzl@33639  1945  "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"  hoelzl@33639  1946 unfolding zip_map1 by auto  nipkow@23096  1947 nipkow@23096  1948 lemma map_zip_map2:  hoelzl@33639  1949  "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"  hoelzl@33639  1950 unfolding zip_map2 by auto  nipkow@23096  1951 nipkow@31080  1952 text{* Courtesy of Andreas Lochbihler: *}  nipkow@31080  1953 lemma zip_same_conv_map: "zip xs xs = map (\x. (x, x)) xs"  nipkow@31080  1954 by(induct xs) auto  nipkow@31080  1955 wenzelm@13142  1956 lemma nth_zip [simp]:  nipkow@24526  1957 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"  nipkow@24526  1958 apply (induct ys arbitrary: i xs, simp)  nipkow@13145  1959 apply (case_tac xs)  nipkow@13145  1960  apply (simp_all add: nth.simps split: nat.split)  nipkow@13145  1961 done  wenzelm@13114  1962 wenzelm@13114  1963 lemma set_zip:  nipkow@13145  1964 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"  nipkow@31080  1965 by(simp add: set_conv_nth cong: rev_conj_cong)  wenzelm@13114  1966 hoelzl@33639  1967 lemma zip_same: "((a,b) \ set (zip xs xs)) = (a \ set xs \ a = b)"  hoelzl@33639  1968 by(induct xs) auto  hoelzl@33639  1969 wenzelm@13114  1970 lemma zip_update:  nipkow@31080  1971  "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"  nipkow@31080  1972 by(rule sym, simp add: update_zip)  wenzelm@13114  1973 wenzelm@13142  1974 lemma zip_replicate [simp]:  nipkow@24526  1975  "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"  nipkow@24526  1976 apply (induct i arbitrary: j, auto)  paulson@14208  1977 apply (case_tac j, auto)  nipkow@13145  1978 done  wenzelm@13114  1979 nipkow@19487  1980 lemma take_zip:  nipkow@24526  1981  "take n (zip xs ys) = zip (take n xs) (take n ys)"  nipkow@24526  1982 apply (induct n arbitrary: xs ys)  nipkow@19487  1983  apply simp  nipkow@19487  1984 apply (case_tac xs, simp)  nipkow@19487  1985 apply (case_tac ys, simp_all)  nipkow@19487  1986 done  nipkow@19487  1987 nipkow@19487  1988 lemma drop_zip:  nipkow@24526  1989  "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"  nipkow@24526  1990 apply (induct n arbitrary: xs ys)  nipkow@19487  1991  apply simp  nipkow@19487  1992 apply (case_tac xs, simp)  nipkow@19487  1993 apply (case_tac ys, simp_all)  nipkow@19487  1994 done  nipkow@19487  1995 hoelzl@33639  1996 lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \ fst) (zip xs ys)"  hoelzl@33639  1997 proof (induct xs arbitrary: ys)  hoelzl@33639  1998  case (Cons x xs) thus ?case by (cases ys) auto  hoelzl@33639  1999 qed simp  hoelzl@33639  2000 hoelzl@33639  2001 lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \ snd) (zip xs ys)"  hoelzl@33639  2002 proof (induct xs arbitrary: ys)  hoelzl@33639  2003  case (Cons x xs) thus ?case by (cases ys) auto  hoelzl@33639  2004 qed simp  hoelzl@33639  2005 krauss@22493  2006 lemma set_zip_leftD:  krauss@22493  2007  "(x,y)\ set (zip xs ys) \ x \ set xs"  krauss@22493  2008 by (induct xs ys rule:list_induct2') auto  krauss@22493  2009 krauss@22493  2010 lemma set_zip_rightD:  krauss@22493  2011  "(x,y)\ set (zip xs ys) \ y \ set ys"  krauss@22493  2012 by (induct xs ys rule:list_induct2') auto  wenzelm@13142  2013 nipkow@23983  2014 lemma in_set_zipE:  nipkow@23983  2015  "(x,y) : set(zip xs ys) \ (\ x : set xs; y : set ys \ \ R) \ R"  nipkow@23983  2016 by(blast dest: set_zip_leftD set_zip_rightD)  nipkow@23983  2017 haftmann@29829  2018 lemma zip_map_fst_snd:  haftmann@29829  2019  "zip (map fst zs) (map snd zs) = zs"  haftmann@29829  2020  by (induct zs) simp_all  haftmann@29829  2021 haftmann@29829  2022 lemma zip_eq_conv:  haftmann@29829  2023  "length xs = length ys \ zip xs ys = zs \ map fst zs = xs \ map snd zs = ys"  haftmann@29829  2024  by (auto simp add: zip_map_fst_snd)  haftmann@29829  2025 hoelzl@33639  2026 lemma distinct_zipI1:  hoelzl@33639  2027  "distinct xs \ distinct (zip xs ys)"  hoelzl@33639  2028 proof (induct xs arbitrary: ys)  hoelzl@33639  2029  case (Cons x xs)  hoelzl@33639  2030  show ?case  hoelzl@33639  2031  proof (cases ys)  hoelzl@33639  2032  case (Cons y ys')  hoelzl@33639  2033  have "(x, y) \ set (zip xs ys')"  hoelzl@33639  2034  using Cons.prems by (auto simp: set_zip)  hoelzl@33639  2035  thus ?thesis  hoelzl@33639  2036  unfolding Cons zip_Cons_Cons distinct.simps  hoelzl@33639  2037  using Cons.hyps Cons.prems by simp  hoelzl@33639  2038  qed simp  hoelzl@33639  2039 qed simp  hoelzl@33639  2040 hoelzl@33639  2041 lemma distinct_zipI2:  hoelzl@33639  2042  "distinct xs \ distinct (zip xs ys)"  hoelzl@33639  2043 proof (induct xs arbitrary: ys)  hoelzl@33639  2044  case (Cons x xs)  hoelzl@33639  2045  show ?case  hoelzl@33639  2046  proof (cases ys)  hoelzl@33639  2047  case (Cons y ys')  hoelzl@33639  2048  have "(x, y) \ set (zip xs ys')"  hoelzl@33639  2049  using Cons.prems by (auto simp: set_zip)  hoelzl@33639  2050  thus ?thesis  hoelzl@33639  2051  unfolding Cons zip_Cons_Cons distinct.simps  hoelzl@33639  2052  using Cons.hyps Cons.prems by simp  hoelzl@33639  2053  qed simp  hoelzl@33639  2054 qed simp  haftmann@29829  2055 nipkow@15392  2056 subsubsection {* @{text list_all2} *}  wenzelm@13114  2057 kleing@14316  2058 lemma list_all2_lengthD [intro?]:  kleing@14316  2059  "list_all2 P xs ys ==> length xs = length ys"  nipkow@24349  2060 by (simp add: list_all2_def)  haftmann@19607  2061 haftmann@19787  2062 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"  nipkow@24349  2063 by (simp add: list_all2_def)  haftmann@19607  2064 haftmann@19787  2065 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"  nipkow@24349  2066 by (simp add: list_all2_def)  haftmann@19607  2067 haftmann@19607  2068 lemma list_all2_Cons [iff, code]:  haftmann@19607  2069  "list_all2 P (x # xs) (y # ys) = (P x y \ list_all2 P xs ys)"  nipkow@24349  2070 by (auto simp add: list_all2_def)  wenzelm@13114  2071 wenzelm@13114  2072 lemma list_all2_Cons1:  nipkow@13145  2073 "list_all2 P (x # xs) ys = (\z zs. ys = z # zs \ P x z \ list_all2 P xs zs)"  nipkow@13145  2074 by (cases ys) auto  wenzelm@13114  2075 wenzelm@13114  2076 lemma list_all2_Cons2:  nipkow@13145  2077 "list_all2 P xs (y # ys) = (\z zs. xs = z # zs \ P z y \ list_all2 P zs ys)"  nipkow@13145  2078 by (cases xs) auto  wenzelm@13114  2079 wenzelm@13142  2080 lemma list_all2_rev [iff]:  nipkow@13145  2081 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"  nipkow@13145  2082 by (simp add: list_all2_def zip_rev cong: conj_cong)  wenzelm@13114  2083 kleing@13863  2084 lemma list_all2_rev1:  kleing@13863  2085 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"  kleing@13863  2086 by (subst list_all2_rev [symmetric]) simp  kleing@13863  2087 wenzelm@13114  2088 lemma list_all2_append1:  nipkow@13145  2089 "list_all2 P (xs @ ys) zs =  nipkow@13145  2090 (EX us vs. zs = us @ vs \ length us = length xs \ length vs = length ys \  nipkow@13145  2091 list_all2 P xs us \ list_all2 P ys vs)"  nipkow@13145  2092 apply (simp add: list_all2_def zip_append1)  nipkow@13145  2093 apply (rule iffI)  nipkow@13145  2094  apply (rule_tac x = "take (length xs) zs" in exI)  nipkow@13145  2095  apply (rule_tac x = "drop (length xs) zs" in exI)  paulson@14208  2096  apply (force split: nat_diff_split simp add: min_def, clarify)  nipkow@13145  2097 apply (simp add: ball_Un)  nipkow@13145  2098 done  wenzelm@13114  2099 wenzelm@13114  2100 lemma list_all2_append2:  nipkow@13145  2101 "list_all2 P xs (ys @ zs) =  nipkow@13145  2102 (EX us vs. xs = us @ vs \ length us = length ys \ length vs = length zs \  nipkow@13145  2103 list_all2 P us ys \ list_all2 P vs zs)"  nipkow@13145  2104 apply (simp add: list_all2_def zip_append2)  nipkow@13145  2105 apply (rule iffI)  nipkow@13145  2106  apply (rule_tac x = "take (length ys) xs" in exI)  nipkow@13145  2107  apply (rule_tac x = "drop (length ys) xs" in exI)  paulson@14208  2108  apply (force split: nat_diff_split simp add: min_def, clarify)  nipkow@13145  2109 apply (simp add: ball_Un)  nipkow@13145  2110 done  wenzelm@13114  2111 kleing@13863  2112 lemma list_all2_append:  nipkow@14247  2113  "length xs = length ys \  nipkow@14247  2114  list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \ list_all2 P us vs)"  nipkow@14247  2115 by (induct rule:list_induct2, simp_all)  kleing@13863  2116 kleing@13863  2117 lemma list_all2_appendI [intro?, trans]:  kleing@13863  2118  "\ list_all2 P a b; list_all2 P c d \ \ list_all2 P (a@c) (b@d)"  nipkow@24349  2119 by (simp add: list_all2_append list_all2_lengthD)  kleing@13863  2120 wenzelm@13114  2121 lemma list_all2_conv_all_nth:  nipkow@13145  2122 "list_all2 P xs ys =  nipkow@13145  2123 (length xs = length ys \ (\i < length xs. P (xs!i) (ys!i)))"  nipkow@13145  2124 by (force simp add: list_all2_def set_zip)  wenzelm@13114  2125 berghofe@13883  2126 lemma list_all2_trans:  berghofe@13883  2127  assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"  berghofe@13883  2128  shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"  berghofe@13883  2129  (is "!!bs cs. PROP ?Q as bs cs")  berghofe@13883  2130 proof (induct as)  berghofe@13883  2131  fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"  berghofe@13883  2132  show "!!cs. PROP ?Q (x # xs) bs cs"  berghofe@13883  2133  proof (induct bs)  berghofe@13883  2134  fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"  berghofe@13883  2135  show "PROP ?Q (x # xs) (y # ys) cs"  berghofe@13883  2136  by (induct cs) (auto intro: tr I1 I2)  berghofe@13883  2137  qed simp  berghofe@13883  2138 qed simp  berghofe@13883  2139 kleing@13863  2140 lemma list_all2_all_nthI [intro?]:  kleing@13863  2141  "length a = length b \ (\n. n < length a \ P (a!n) (b!n)) \ list_all2 P a b"  nipkow@24349  2142 by (simp add: list_all2_conv_all_nth)  kleing@13863  2143 paulson@14395  2144 lemma list_all2I:  paulson@14395  2145  "\x \ set (zip a b). split P x \ length a = length b \ list_all2 P a b"  nipkow@24349  2146 by (simp add: list_all2_def)  paulson@14395  2147 kleing@14328  2148 lemma list_all2_nthD:  kleing@13863  2149  "\ list_all2 P xs ys; p < size xs \ \ P (xs!p) (ys!p)"  nipkow@24349  2150 by (simp add: list_all2_conv_all_nth)  kleing@13863  2151 nipkow@14302  2152 lemma list_all2_nthD2:  nipkow@14302  2153  "\list_all2 P xs ys; p < size ys\ \ P (xs!p) (ys!p)"  nipkow@24349  2154 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)  nipkow@14302  2155 kleing@13863  2156 lemma list_all2_map1:  kleing@13863  2157  "list_all2 P (map f as) bs = list_all2 (\x y. P (f x) y) as bs"  nipkow@24349  2158 by (simp add: list_all2_conv_all_nth)  kleing@13863  2159 kleing@13863  2160 lemma list_all2_map2:  kleing@13863  2161  "list_all2 P as (map f bs) = list_all2 (\x y. P x (f y)) as bs"  nipkow@24349  2162 by (auto simp add: list_all2_conv_all_nth)  kleing@13863  2163 kleing@14316  2164 lemma list_all2_refl [intro?]:  kleing@13863  2165  "(\x. P x x) \ list_all2 P xs xs"  nipkow@24349  2166 by (simp add: list_all2_conv_all_nth)  kleing@13863  2167 kleing@13863  2168 lemma list_all2_update_cong:  kleing@13863  2169  "\ i \ list_all2 P (xs[i:=x]) (ys[i:=y])"  nipkow@24349  2170 by (simp add: list_all2_conv_all_nth nth_list_update)  kleing@13863  2171 kleing@13863  2172 lemma list_all2_update_cong2:  kleing@13863  2173  "\list_all2 P xs ys; P x y; i < length ys\ \ list_all2 P (xs[i:=x]) (ys[i:=y])"  nipkow@24349  2174 by (simp add: list_all2_lengthD list_all2_update_cong)  kleing@13863  2175 nipkow@14302  2176 lemma list_all2_takeI [simp,intro?]:  nipkow@24526  2177  "list_all2 P xs ys \ list_all2 P (take n xs) (take n ys)"  nipkow@24526  2178 apply (induct xs arbitrary: n ys)  nipkow@24526  2179  apply simp  nipkow@24526  2180 apply (clarsimp simp add: list_all2_Cons1)  nipkow@24526  2181 apply (case_tac n)  nipkow@24526  2182 apply auto  nipkow@24526  2183 done  nipkow@14302  2184 nipkow@14302  2185 lemma list_all2_dropI [simp,intro?]:  nipkow@24526  2186  "list_all2 P as bs \ list_all2 P (drop n as) (drop n bs)"  nipkow@24526  2187 apply (induct as arbitrary: n bs, simp)  nipkow@24526  2188 apply (clarsimp simp add: list_all2_Cons1)  nipkow@24526  2189 apply (case_tac n, simp, simp)  nipkow@24526  2190 done  kleing@13863  2191 kleing@14327  2192 lemma list_all2_mono [intro?]:  nipkow@24526  2193  "list_all2 P xs ys \ (\xs ys. P xs ys \ Q xs ys) \ list_all2 Q xs ys"  nipkow@24526  2194 apply (induct xs arbitrary: ys, simp)  nipkow@24526  2195 apply (case_tac ys, auto)  nipkow@24526  2196 done  kleing@13863  2197 haftmann@22551  2198 lemma list_all2_eq:  haftmann@22551  2199  "xs = ys \ list_all2 (op =) xs ys"  nipkow@24349  2200 by (induct xs ys rule: list_induct2') auto  haftmann@22551  2201 wenzelm@13142  2202 nipkow@15392  2203 subsubsection {* @{text foldl} and @{text foldr} *}  wenzelm@13142  2204 wenzelm@13142  2205 lemma foldl_append [simp]:  nipkow@24526  2206  "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"  nipkow@24526  2207 by (induct xs arbitrary: a) auto  wenzelm@13142  2208 nipkow@14402  2209 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"  nipkow@14402  2210 by (induct xs) auto  nipkow@14402  2211 nipkow@23096  2212 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"  nipkow@23096  2213 by(induct xs) simp_all  nipkow@23096  2214 nipkow@24449  2215 text{* For efficient code generation: avoid intermediate list. *}  haftmann@31998  2216 lemma foldl_map[code_unfold]:  nipkow@24449  2217  "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"  nipkow@23096  2218 by(induct xs arbitrary:a) simp_all  nipkow@23096  2219 haftmann@31930  2220 lemma foldl_apply_inv:  haftmann@31930  2221  assumes "\x. g (h x) = x"  haftmann@31930  2222  shows "foldl f (g s) xs = g (foldl (\s x. h (f (g s) x)) s xs)"  haftmann@31930  2223  by (rule sym, induct xs arbitrary: s) (simp_all add: assms)  haftmann@31930  2224 krauss@19770  2225 lemma foldl_cong [fundef_cong, recdef_cong]:  krauss@18336  2226  "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]  krauss@18336  2227  ==> foldl f a l = foldl g b k"  nipkow@24349  2228 by (induct k arbitrary: a b l) simp_all  krauss@18336  2229 krauss@19770  2230 lemma foldr_cong [fundef_cong, recdef_cong]:  krauss@18336  2231  "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]  krauss@18336  2232  ==> foldr f l a = foldr g k b"  nipkow@24349  2233 by (induct k arbitrary: a b l) simp_all  krauss@18336  2234 nipkow@24449  2235 lemma (in semigroup_add) foldl_assoc:  haftmann@25062  2236 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"  nipkow@24449  2237 by (induct zs arbitrary: y) (simp_all add:add_assoc)  nipkow@24449  2238 nipkow@24449  2239 lemma (in monoid_add) foldl_absorb0:  haftmann@25062  2240 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"  nipkow@24449  2241 by (induct zs) (simp_all add:foldl_assoc)  nipkow@24449  2242 nipkow@24449  2243 nipkow@23096  2244 text{* The First Duality Theorem'' in Bird \& Wadler: *}  nipkow@23096  2245 nipkow@23096  2246 lemma foldl_foldr1_lemma:  nipkow@23096  2247  "foldl op + a xs = a + foldr op + xs (0\'a::monoid_add)"  nipkow@23096  2248 by (induct xs arbitrary: a) (auto simp:add_assoc)  nipkow@23096  2249 nipkow@23096  2250 corollary foldl_foldr1:  nipkow@23096  2251  "foldl op + 0 xs = foldr op + xs (0\'a::monoid_add)"  nipkow@23096  2252 by (simp add:foldl_foldr1_lemma)  nipkow@23096  2253 nipkow@23096  2254 nipkow@23096  2255 text{* The Third Duality Theorem'' in Bird \& Wadler: *}  nipkow@23096  2256 nipkow@14402  2257 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"  nipkow@14402  2258 by (induct xs) auto  nipkow@14402  2259 nipkow@14402  2260 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"  nipkow@14402  2261 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])  nipkow@14402  2262 haftmann@25062  2263 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"  chaieb@24471  2264  by (induct xs, auto simp add: foldl_assoc add_commute)  chaieb@24471  2265 wenzelm@13142  2266 text {*  nipkow@13145  2267 Note: @{text "n \ foldl (op +) n ns"} looks simpler, but is more  nipkow@13145  2268 difficult to use because it requires an additional transitivity step.  wenzelm@13142  2269 *}  wenzelm@13142  2270 nipkow@24526  2271 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"  nipkow@24526  2272 by (induct ns arbitrary: n) auto  nipkow@24526  2273 nipkow@24526  2274 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"  nipkow@13145  2275 by (force intro: start_le_sum simp add: in_set_conv_decomp)  wenzelm@13142  2276 wenzelm@13142  2277 lemma sum_eq_0_conv [iff]:  nipkow@24526  2278  "(foldl (op +) (m::nat) ns = 0) = (m = 0 \ (\n \ set ns. n = 0))"  nipkow@24526  2279 by (induct ns arbitrary: m) auto  wenzelm@13114  2280 chaieb@24471  2281 lemma foldr_invariant:  chaieb@24471  2282  "\Q x ; \ x\ set xs. P x; \ x y. P x \ Q y \ Q (f x y) \ \ Q (foldr f xs x)"  chaieb@24471  2283  by (induct xs, simp_all)  chaieb@24471  2284 chaieb@24471  2285 lemma foldl_invariant:  chaieb@24471  2286  "\Q x ; \ x\ set xs. P x; \ x y. P x \ Q y \ Q (f y x) \ \ Q (foldl f x xs)"  chaieb@24471  2287  by (induct xs arbitrary: x, simp_all)  chaieb@24471  2288 haftmann@31455  2289 text {* @{const foldl} and @{const concat} *}  nipkow@24449  2290 nipkow@24449  2291 lemma foldl_conv_concat:  haftmann@29782  2292  "foldl (op @) xs xss = xs @ concat xss"  haftmann@29782  2293 proof (induct xss arbitrary: xs)  haftmann@29782  2294  case Nil show ?case by simp  haftmann@29782  2295 next  haftmann@29782  2296  interpret monoid_add "[]" "op @" proof qed simp_all  haftmann@29782  2297  case Cons then show ?case by (simp add: foldl_absorb0)  haftmann@29782  2298 qed  haftmann@29782  2299 haftmann@29782  2300 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"  haftmann@29782  2301  by (simp add: foldl_conv_concat)  haftmann@29782  2302 haftmann@31455  2303 text {* @{const Finite_Set.fold} and @{const foldl} *}  haftmann@31455  2304 haftmann@31455  2305 lemma (in fun_left_comm_idem) fold_set:  haftmann@31455  2306  "fold f y (set xs) = foldl (\y x. f x y) y xs"  haftmann@31455  2307  by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)  haftmann@31455  2308 haftmann@32681  2309 lemma (in ab_semigroup_idem_mult) fold1_set:  haftmann@32681  2310  assumes "xs \ []"  haftmann@32681  2311  shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"  haftmann@32681  2312 proof -  haftmann@32681  2313  interpret fun_left_comm_idem times by (fact fun_left_comm_idem)  haftmann@32681  2314  from assms obtain y ys where xs: "xs = y # ys"  haftmann@32681  2315  by (cases xs) auto  haftmann@32681  2316  show ?thesis  haftmann@32681  2317  proof (cases "set ys = {}")  haftmann@32681  2318  case True with xs show ?thesis by simp  haftmann@32681  2319  next  haftmann@32681  2320  case False  haftmann@32681  2321  then have "fold1 times (insert y (set ys)) = fold times y (set ys)"  haftmann@32681  2322  by (simp only: finite_set fold1_eq_fold_idem)  haftmann@32681  2323  with xs show ?thesis by (simp add: fold_set mult_commute)  haftmann@32681  2324  qed  haftmann@32681  2325 qed  haftmann@32681  2326 haftmann@32681  2327 lemma (in lattice) Inf_fin_set_fold [code_unfold]:  haftmann@32681  2328  "Inf_fin (set (x # xs)) = foldl inf x xs"  haftmann@32681  2329 proof -  haftmann@32681  2330  interpret ab_semigroup_idem_mult "inf :: 'a \ 'a \ 'a"  haftmann@32681  2331  by (fact ab_semigroup_idem_mult_inf)  haftmann@32681  2332  show ?thesis  haftmann@32681  2333  by (simp add: Inf_fin_def fold1_set del: set.simps)  haftmann@32681  2334 qed  haftmann@32681  2335 haftmann@32681  2336 lemma (in lattice) Sup_fin_set_fold [code_unfold]:  haftmann@32681  2337  "Sup_fin (set (x # xs)) = foldl sup x xs"  haftmann@32681  2338 proof -  haftmann@32681  2339  interpret ab_semigroup_idem_mult "sup :: 'a \ 'a \ 'a"  haftmann@32681  2340  by (fact ab_semigroup_idem_mult_sup)  haftmann@32681  2341  show ?thesis  haftmann@32681  2342  by (simp add: Sup_fin_def fold1_set del: set.simps)  haftmann@32681  2343 qed  haftmann@32681  2344 haftmann@32681  2345 lemma (in linorder) Min_fin_set_fold [code_unfold]:  haftmann@32681  2346  "Min (set (x # xs)) = foldl min x xs"  haftmann@32681  2347 proof -  haftmann@32681  2348  interpret ab_semigroup_idem_mult "min :: 'a \ 'a \ 'a"  haftmann@32681  2349  by (fact ab_semigroup_idem_mult_min)  haftmann@32681  2350  show ?thesis  haftmann@32681  2351  by (simp add: Min_def fold1_set del: set.simps)  haftmann@32681  2352 qed  haftmann@32681  2353 haftmann@32681  2354 lemma (in linorder) Max_fin_set_fold [code_unfold]:  haftmann@32681  2355  "Max (set (x # xs)) = foldl max x xs"  haftmann@32681  2356 proof -  haftmann@32681  2357  interpret ab_semigroup_idem_mult "max :: 'a \ 'a \ 'a"  haftmann@32681  2358  by (fact ab_semigroup_idem_mult_max)  haftmann@32681  2359  show ?thesis  haftmann@32681  2360  by (simp add: Max_def fold1_set del: set.simps)  haftmann@32681  2361 qed  haftmann@32681  2362 haftmann@32681  2363 lemma (in complete_lattice) Inf_set_fold [code_unfold]:  haftmann@32681  2364  "Inf (set xs) = foldl inf top xs"  haftmann@32681  2365  by (cases xs)  haftmann@32681  2366  (simp_all add: Inf_fin_Inf [symmetric] Inf_fin_set_fold  haftmann@32681  2367  inf_commute del: set.simps, simp add: top_def)  haftmann@32681  2368 haftmann@32681  2369 lemma (in complete_lattice) Sup_set_fold [code_unfold]:  haftmann@32681  2370  "Sup (set xs) = foldl sup bot xs"  haftmann@32681  2371  by (cases xs)  haftmann@32681  2372  (simp_all add: Sup_fin_Sup [symmetric] Sup_fin_set_fold  haftmann@32681  2373  sup_commute del: set.simps, simp add: bot_def)  haftmann@31455  2374 nipkow@24449  2375 nipkow@23096  2376 subsubsection {* List summation: @{const listsum} and @{text"\"}*}  nipkow@23096  2377 haftmann@26442  2378 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"  nipkow@24449  2379 by (induct xs) (simp_all add:add_assoc)  nipkow@24449  2380 haftmann@26442  2381 lemma listsum_rev [simp]:  haftmann@26442  2382  fixes xs :: "'a\comm_monoid_add list"  haftmann@26442  2383  shows "listsum (rev xs) = listsum xs"  nipkow@24449  2384 by (induct xs) (simp_all add:add_ac)  nipkow@24449  2385 nipkow@31022  2386 lemma listsum_map_remove1:  nipkow@31022  2387 fixes f :: "'a \ ('b::comm_monoid_add)"  nipkow@31022  2388 shows "x : set xs \ listsum(map f xs) = f x + listsum(map f (remove1 x xs))"  nipkow@31022  2389 by (induct xs)(auto simp add:add_ac)  nipkow@31022  2390 nipkow@31022  2391 lemma list_size_conv_listsum:  nipkow@31022  2392  "list_size f xs = listsum (map f xs) + size xs"  nipkow@31022  2393 by(induct xs) auto  nipkow@31022  2394 haftmann@26442  2395 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"  haftmann@26442  2396 by (induct xs) auto  haftmann@26442  2397 haftmann@26442  2398 lemma length_concat: "length (concat xss) = listsum (map length xss)"  haftmann@26442  2399 by (induct xss) simp_all  nipkow@23096  2400 hoelzl@33639  2401 lemma listsum_map_filter:  hoelzl@33639  2402  fixes f :: "'a \ 'b \ comm_monoid_add"  hoelzl@33639  2403  assumes "\ x. \ x \ set xs ; \ P x \ \ f x = 0"  hoelzl@33639  2404  shows "listsum (map f (filter P xs)) = listsum (map f xs)"  hoelzl@33639  2405 using assms by (induct xs) auto  hoelzl@33639  2406 nipkow@24449  2407 text{* For efficient code generation ---  nipkow@24449  2408  @{const listsum} is not tail recursive but @{const foldl} is. *}  haftmann@31998  2409 lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"  nipkow@23096  2410 by(simp add:listsum_foldr foldl_foldr1)  nipkow@23096  2411 nipkow@31077  2412 lemma distinct_listsum_conv_Setsum:  nipkow@31077  2413  "distinct xs \ listsum xs = Setsum(set xs)"  nipkow@31077  2414 by (induct xs) simp_all  nipkow@31077  2415 nipkow@24449  2416 nipkow@23096  2417 text{* Some syntactic sugar for summing a function over a list: *}  nipkow@23096  2418 nipkow@23096  2419 syntax  nipkow@23096  2420  "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3SUM _<-_. _)" [0, 51, 10] 10)  nipkow@23096  2421 syntax (xsymbols)  nipkow@23096  2422  "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10)  nipkow@23096  2423 syntax (HTML output)  nipkow@23096  2424  "_listsum" :: "pttrn => 'a list => 'b => 'b" ("(3\_\_. _)" [0, 51, 10] 10)  nipkow@23096  2425 nipkow@23096  2426 translations -- {* Beware of argument permutation! *}  nipkow@23096  2427  "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"  nipkow@23096  2428  "\x\xs. b" == "CONST listsum (map (%x. b) xs)"  nipkow@23096  2429 haftmann@26442  2430 lemma listsum_triv: "(\x\xs. r) = of_nat (length xs) * r"  haftmann@26442  2431  by (induct xs) (simp_all add: left_distrib)  haftmann@26442  2432 nipkow@23096  2433 lemma listsum_0 [simp]: "(\x\xs. 0) = 0"  haftmann@26442  2434  by (induct xs) (simp_all add: left_distrib)  nipkow@23096  2435 nipkow@23096  2436 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}  nipkow@23096  2437 lemma uminus_listsum_map:  haftmann@26442  2438  fixes f :: "'a \ 'b\ab_group_add"  haftmann@26442  2439  shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"  haftmann@26442  2440 by (induct xs) simp_all  nipkow@23096  2441 huffman@31258  2442 lemma listsum_addf:  huffman@31258  2443  fixes f g :: "'a \ 'b::comm_monoid_add"  huffman@31258  2444  shows "(\x\xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"  huffman@31258  2445 by (induct xs) (simp_all add: algebra_simps)  huffman@31258  2446 huffman@31258  2447 lemma listsum_subtractf:  huffman@31258  2448  fixes f g :: "'a \ 'b::ab_group_add"  huffman@31258  2449  shows "(\x\xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"  huffman@31258  2450 by (induct xs) simp_all  huffman@31258  2451 huffman@31258  2452 lemma listsum_const_mult:  huffman@31258  2453  fixes f :: "'a \ 'b::semiring_0"  huffman@31258  2454  shows "(\x\xs. c * f x) = c * (\x\xs. f x)"  huffman@31258  2455 by (induct xs, simp_all add: algebra_simps)  huffman@31258  2456 huffman@31258  2457 lemma listsum_mult_const:  huffman@31258  2458  fixes f :: "'a \ 'b::semiring_0"  huffman@31258  2459  shows "(\x\xs. f x * c) = (\x\xs. f x) * c"  huffman@31258  2460 by (induct xs, simp_all add: algebra_simps)  huffman@31258  2461 huffman@31258  2462 lemma listsum_abs:  huffman@31258  2463  fixes xs :: "'a::pordered_ab_group_add_abs list"  huffman@31258  2464  shows "\listsum xs\ \ listsum (map abs xs)"  huffman@31258  2465 by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])  huffman@31258  2466 huffman@31258  2467 lemma listsum_mono:  huffman@31258  2468  fixes f g :: "'a \ 'b::{comm_monoid_add, pordered_ab_semigroup_add}"  huffman@31258  2469  shows "(\x. x \ set xs \ f x \ g x) \ (\x\xs. f x) \ (\x\xs. g x)"  huffman@31258  2470 by (induct xs, simp, simp add: add_mono)  huffman@31258  2471 wenzelm@13114  2472 nipkow@24645  2473 subsubsection {* @{text upt} *}  wenzelm@13114  2474 nipkow@17090  2475 lemma upt_rec[code]: "[i.. [i.. j <= i)"  nipkow@15281  2485 by(induct j)simp_all  nipkow@15281  2486 nipkow@15281  2487 lemma upt_eq_Cons_conv:  nipkow@24526  2488  "([i.. [i..<(Suc j)] = [i.. [i.. [i.. [i.. hd[i.. last[i.. take m [i.. (map f [m.. k <= length ys ==>  berghofe@13883  2547  (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"  nipkow@24526  2548 apply (atomize, induct k arbitrary: xs ys)  paulson@14208  2549 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)  nipkow@13145  2550 txt {* Both lists must be non-empty *}  paulson@14208  2551 apply (case_tac xs, simp)  paulson@14208  2552 apply (case_tac ys, clarify)  nipkow@13145  2553  apply (simp (no_asm_use))  nipkow@13145  2554 apply clarify  nipkow@13145  2555 txt {* prenexing's needed, not miniscoping *}  nipkow@13145  2556 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)  nipkow@13145  2557 apply blast  nipkow@13145  2558 done  wenzelm@13114  2559 wenzelm@13114  2560 lemma nth_equalityI:  wenzelm@13114  2561  "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"  nipkow@13145  2562 apply (frule nth_take_lemma [OF le_refl eq_imp_le])  nipkow@13145  2563 apply (simp_all add: take_all)  nipkow@13145  2564 done  wenzelm@13142  2565 haftmann@24796  2566 lemma map_nth:  haftmann@24796  2567  "map (\i. xs ! i) [0.. (\x y. \P x y; Q y x\ \ x = y); list_all2 P xs ys; list_all2 Q ys xs \  kleing@13863  2573  \ xs = ys"  kleing@13863  2574  apply (simp add: list_all2_conv_all_nth)  paulson@14208  2575  apply (rule nth_equalityI, blast, simp)  kleing@13863  2576  done  kleing@13863  2577 wenzelm@13142  2578 lemma take_equalityI: "(\i. take i xs = take i ys) ==> xs = ys"  nipkow@13145  2579 -- {* The famous take-lemma. *}  nipkow@13145  2580 apply (drule_tac x = "max (length xs) (length ys)" in spec)  nipkow@13145  2581 apply (simp add: le_max_iff_disj take_all)  nipkow@13145  2582 done  wenzelm@13142  2583 wenzelm@13142  2584 nipkow@15302  2585 lemma take_Cons':  nipkow@15302  2586  "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"  nipkow@15302  2587 by (cases n) simp_all  nipkow@15302  2588 nipkow@15302  2589 lemma drop_Cons':  nipkow@15302  2590  "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"  nipkow@15302  2591 by (cases n) simp_all  nipkow@15302  2592 nipkow@15302  2593 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"  nipkow@15302  2594 by (cases n) simp_all  nipkow@15302  2595 paulson@18622  2596 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]  paulson@18622  2597 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]  paulson@18622  2598 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]  paulson@18622  2599 paulson@18622  2600 declare take_Cons_number_of [simp]  paulson@18622  2601  drop_Cons_number_of [simp]  paulson@18622  2602  nth_Cons_number_of [simp]  nipkow@15302  2603 nipkow@15302  2604 nipkow@32415  2605 subsubsection {* @{text upto}: interval-list on @{typ int} *}  nipkow@32415  2606 nipkow@32415  2607 (* FIXME make upto tail recursive? *)  nipkow@32415  2608 nipkow@32415  2609 function upto :: "int \ int \ int list" ("(1[_../_])") where  nipkow@32415  2610 "upto i j = (if i \ j then i # [i+1..j] else [])"  nipkow@32415  2611 by auto  nipkow@32415  2612 termination  nipkow@32415  2613 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto  nipkow@32415  2614 nipkow@32415  2615 declare upto.simps[code, simp del]  nipkow@32415  2616 nipkow@32415  2617 lemmas upto_rec_number_of[simp] =  nipkow@32415  2618  upto.simps[of "number_of m" "number_of n", standard]  nipkow@32415  2619 nipkow@32415  2620 lemma upto_empty[simp]: "j < i \ [i..j] = []"  nipkow@32415  2621 by(simp add: upto.simps)  nipkow@32415  2622 nipkow@32415  2623 lemma set_upto[simp]: "set[i..j] = {i..j}"  nipkow@32415  2624 apply(induct i j rule:upto.induct)  nipkow@32415  2625 apply(simp add: upto.simps simp_from_to)  nipkow@32415  2626 done  nipkow@32415  2627 nipkow@32415  2628 nipkow@15392  2629 subsubsection {* @{text "distinct"} and @{text remdups} *}  wenzelm@13142  2630 wenzelm@13142  2631 lemma distinct_append [simp]:  nipkow@13145  2632 "distinct (xs @ ys) = (distinct xs \ distinct ys \ set xs \ set ys = {})"  nipkow@13145  2633 by (induct xs) auto  wenzelm@13142  2634 nipkow@15305  2635 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"  nipkow@15305  2636 by(induct xs) auto  nipkow@15305  2637 wenzelm@13142  2638 lemma set_remdups [simp]: "set (remdups xs) = set xs"  nipkow@13145  2639 by (induct xs) (auto simp add: insert_absorb)  wenzelm@13142  2640 wenzelm@13142  2641 lemma distinct_remdups [iff]: "distinct (remdups xs)"  nipkow@13145  2642 by (induct xs) auto  wenzelm@13142  2643 nipkow@25287  2644 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"  nipkow@25287  2645 by (induct xs, auto)  nipkow@25287  2646 haftmann@26734  2647 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \ distinct xs"  haftmann@26734  2648 by (metis distinct_remdups distinct_remdups_id)  nipkow@25287  2649 nipkow@24566  2650 lemma finite_distinct_list: "finite A \ EX xs. set xs = A & distinct xs"  paulson@24632  2651 by (metis distinct_remdups finite_list set_remdups)  nipkow@24566  2652 paulson@15072  2653 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"  nipkow@24349  2654 by (induct x, auto)  paulson@15072  2655 paulson@15072  2656 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"  nipkow@24349  2657 by (induct x, auto)  paulson@15072  2658 nipkow@15245  2659 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"  nipkow@15245  2660 by (induct xs) auto  nipkow@15245  2661 nipkow@15245  2662 lemma length_remdups_eq[iff]:  nipkow@15245  2663  "(length (remdups xs) = length xs) = (remdups xs = xs)"  nipkow@15245  2664 apply(induct xs)  nipkow@15245  2665  apply auto  nipkow@15245  2666 apply(subgoal_tac "length (remdups xs) <= length xs")  nipkow@15245  2667  apply arith  nipkow@15245  2668 apply(rule length_remdups_leq)  nipkow@15245  2669 done  nipkow@15245  2670 nipkow@18490  2671 nipkow@18490  2672 lemma distinct_map:  nipkow@18490  2673  "distinct(map f xs) = (distinct xs & inj_on f (set xs))"  nipkow@18490  2674 by (induct xs) auto  nipkow@18490  2675 nipkow@18490  2676 wenzelm@13142  2677 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"  nipkow@13145  2678 by (induct xs) auto  wenzelm@13114  2679 nipkow@17501  2680 lemma distinct_upt[simp]: "distinct[i.. distinct (take i xs)"  nipkow@24526  2690 apply(induct xs arbitrary: i)  nipkow@17501  2691  apply simp  nipkow@17501  2692 apply (case_tac i)  nipkow@17501  2693  apply simp_all  nipkow@17501  2694 apply(blast dest:in_set_takeD)  nipkow@17501  2695 done  nipkow@17501  2696 nipkow@24526  2697 lemma distinct_drop[simp]: "distinct xs \ distinct (drop i xs)"  nipkow@24526  2698 apply(induct xs arbitrary: i)  nipkow@17501 <