src/HOL/List.thy
author haftmann
Mon Jul 12 10:48:37 2010 +0200 (2010-07-12)
changeset 37767 a2b7a20d6ea3
parent 37605 625bc011768a
child 37880 3b9ca8d2c5fb
permissions -rw-r--r--
dropped superfluous [code del]s
     1 (*  Title:      HOL/List.thy
     2     Author:     Tobias Nipkow
     3 *)
     4 
     5 header {* The datatype of finite lists *}
     6 
     7 theory List
     8 imports Plain Quotient Presburger Code_Numeral Sledgehammer Recdef
     9 uses ("Tools/list_code.ML")
    10 begin
    11 
    12 datatype 'a list =
    13     Nil    ("[]")
    14   | Cons 'a  "'a list"    (infixr "#" 65)
    15 
    16 syntax
    17   -- {* list Enumeration *}
    18   "_list" :: "args => 'a list"    ("[(_)]")
    19 
    20 translations
    21   "[x, xs]" == "x#[xs]"
    22   "[x]" == "x#[]"
    23 
    24 
    25 subsection {* Basic list processing functions *}
    26 
    27 primrec
    28   hd :: "'a list \<Rightarrow> 'a" where
    29   "hd (x # xs) = x"
    30 
    31 primrec
    32   tl :: "'a list \<Rightarrow> 'a list" where
    33     "tl [] = []"
    34   | "tl (x # xs) = xs"
    35 
    36 primrec
    37   last :: "'a list \<Rightarrow> 'a" where
    38   "last (x # xs) = (if xs = [] then x else last xs)"
    39 
    40 primrec
    41   butlast :: "'a list \<Rightarrow> 'a list" where
    42     "butlast []= []"
    43   | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"
    44 
    45 primrec
    46   set :: "'a list \<Rightarrow> 'a set" where
    47     "set [] = {}"
    48   | "set (x # xs) = insert x (set xs)"
    49 
    50 primrec
    51   map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
    52     "map f [] = []"
    53   | "map f (x # xs) = f x # map f xs"
    54 
    55 primrec
    56   append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where
    57     append_Nil:"[] @ ys = ys"
    58   | append_Cons: "(x#xs) @ ys = x # xs @ ys"
    59 
    60 primrec
    61   rev :: "'a list \<Rightarrow> 'a list" where
    62     "rev [] = []"
    63   | "rev (x # xs) = rev xs @ [x]"
    64 
    65 primrec
    66   filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    67     "filter P [] = []"
    68   | "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
    69 
    70 syntax
    71   -- {* Special syntax for filter *}
    72   "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
    73 
    74 translations
    75   "[x<-xs . P]"== "CONST filter (%x. P) xs"
    76 
    77 syntax (xsymbols)
    78   "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    79 syntax (HTML output)
    80   "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    81 
    82 primrec
    83   foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where
    84     foldl_Nil: "foldl f a [] = a"
    85   | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
    86 
    87 primrec
    88   foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
    89     "foldr f [] a = a"
    90   | "foldr f (x # xs) a = f x (foldr f xs a)"
    91 
    92 primrec
    93   concat:: "'a list list \<Rightarrow> 'a list" where
    94     "concat [] = []"
    95   | "concat (x # xs) = x @ concat xs"
    96 
    97 primrec (in monoid_add)
    98   listsum :: "'a list \<Rightarrow> 'a" where
    99     "listsum [] = 0"
   100   | "listsum (x # xs) = x + listsum xs"
   101 
   102 primrec
   103   drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   104     drop_Nil: "drop n [] = []"
   105   | drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"
   106   -- {*Warning: simpset does not contain this definition, but separate
   107        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   108 
   109 primrec
   110   take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   111     take_Nil:"take n [] = []"
   112   | take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"
   113   -- {*Warning: simpset does not contain this definition, but separate
   114        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   115 
   116 primrec
   117   nth :: "'a list => nat => 'a" (infixl "!" 100) where
   118   nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"
   119   -- {*Warning: simpset does not contain this definition, but separate
   120        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   121 
   122 primrec
   123   list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   124     "list_update [] i v = []"
   125   | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"
   126 
   127 nonterminals lupdbinds lupdbind
   128 
   129 syntax
   130   "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
   131   "" :: "lupdbind => lupdbinds"    ("_")
   132   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
   133   "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)
   134 
   135 translations
   136   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
   137   "xs[i:=x]" == "CONST list_update xs i x"
   138 
   139 primrec
   140   takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   141     "takeWhile P [] = []"
   142   | "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"
   143 
   144 primrec
   145   dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   146     "dropWhile P [] = []"
   147   | "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"
   148 
   149 primrec
   150   zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where
   151     "zip xs [] = []"
   152   | zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"
   153   -- {*Warning: simpset does not contain this definition, but separate
   154        theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
   155 
   156 primrec 
   157   upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where
   158     upt_0: "[i..<0] = []"
   159   | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
   160 
   161 primrec
   162   distinct :: "'a list \<Rightarrow> bool" where
   163     "distinct [] \<longleftrightarrow> True"
   164   | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"
   165 
   166 primrec
   167   remdups :: "'a list \<Rightarrow> 'a list" where
   168     "remdups [] = []"
   169   | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"
   170 
   171 definition
   172   insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   173   "insert x xs = (if x \<in> set xs then xs else x # xs)"
   174 
   175 hide_const (open) insert
   176 hide_fact (open) insert_def
   177 
   178 primrec
   179   remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   180     "remove1 x [] = []"
   181   | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"
   182 
   183 primrec
   184   removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   185     "removeAll x [] = []"
   186   | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"
   187 
   188 primrec
   189   replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where
   190     replicate_0: "replicate 0 x = []"
   191   | replicate_Suc: "replicate (Suc n) x = x # replicate n x"
   192 
   193 text {*
   194   Function @{text size} is overloaded for all datatypes. Users may
   195   refer to the list version as @{text length}. *}
   196 
   197 abbreviation
   198   length :: "'a list \<Rightarrow> nat" where
   199   "length \<equiv> size"
   200 
   201 definition
   202   rotate1 :: "'a list \<Rightarrow> 'a list" where
   203   "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
   204 
   205 definition
   206   rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   207   "rotate n = rotate1 ^^ n"
   208 
   209 definition
   210   list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
   211   "list_all2 P xs ys =
   212     (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
   213 
   214 definition
   215   sublist :: "'a list => nat set => 'a list" where
   216   "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
   217 
   218 primrec
   219   splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   220     "splice [] ys = ys"
   221   | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))"
   222     -- {*Warning: simpset does not contain the second eqn but a derived one. *}
   223 
   224 text{*
   225 \begin{figure}[htbp]
   226 \fbox{
   227 \begin{tabular}{l}
   228 @{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
   229 @{lemma "length [a,b,c] = 3" by simp}\\
   230 @{lemma "set [a,b,c] = {a,b,c}" by simp}\\
   231 @{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
   232 @{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
   233 @{lemma "hd [a,b,c,d] = a" by simp}\\
   234 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
   235 @{lemma "last [a,b,c,d] = d" by simp}\\
   236 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
   237 @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
   238 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
   239 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
   240 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
   241 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
   242 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
   243 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
   244 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
   245 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
   246 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
   247 @{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
   248 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\
   249 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
   250 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
   251 @{lemma "distinct [2,0,1::nat]" by simp}\\
   252 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
   253 @{lemma "List.insert 2 [0::nat,1,2] = [0,1,2]" by (simp add: List.insert_def)}\\
   254 @{lemma "List.insert 3 [0::nat,1,2] = [3,0,1,2]" by (simp add: List.insert_def)}\\
   255 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
   256 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
   257 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
   258 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
   259 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
   260 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
   261 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number')}\\
   262 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\
   263 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\
   264 @{lemma "listsum [1,2,3::nat] = 6" by simp}
   265 \end{tabular}}
   266 \caption{Characteristic examples}
   267 \label{fig:Characteristic}
   268 \end{figure}
   269 Figure~\ref{fig:Characteristic} shows characteristic examples
   270 that should give an intuitive understanding of the above functions.
   271 *}
   272 
   273 text{* The following simple sort functions are intended for proofs,
   274 not for efficient implementations. *}
   275 
   276 context linorder
   277 begin
   278 
   279 fun sorted :: "'a list \<Rightarrow> bool" where
   280 "sorted [] \<longleftrightarrow> True" |
   281 "sorted [x] \<longleftrightarrow> True" |
   282 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
   283 
   284 primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   285 "insort_key f x [] = [x]" |
   286 "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"
   287 
   288 definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where
   289 "sort_key f xs = foldr (insort_key f) xs []"
   290 
   291 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"
   292 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"
   293 
   294 definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   295   "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"
   296 
   297 end
   298 
   299 
   300 subsubsection {* List comprehension *}
   301 
   302 text{* Input syntax for Haskell-like list comprehension notation.
   303 Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
   304 the list of all pairs of distinct elements from @{text xs} and @{text ys}.
   305 The syntax is as in Haskell, except that @{text"|"} becomes a dot
   306 (like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
   307 \verb![e| x <- xs, ...]!.
   308 
   309 The qualifiers after the dot are
   310 \begin{description}
   311 \item[generators] @{text"p \<leftarrow> xs"},
   312  where @{text p} is a pattern and @{text xs} an expression of list type, or
   313 \item[guards] @{text"b"}, where @{text b} is a boolean expression.
   314 %\item[local bindings] @ {text"let x = e"}.
   315 \end{description}
   316 
   317 Just like in Haskell, list comprehension is just a shorthand. To avoid
   318 misunderstandings, the translation into desugared form is not reversed
   319 upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
   320 optmized to @{term"map (%x. e) xs"}.
   321 
   322 It is easy to write short list comprehensions which stand for complex
   323 expressions. During proofs, they may become unreadable (and
   324 mangled). In such cases it can be advisable to introduce separate
   325 definitions for the list comprehensions in question.  *}
   326 
   327 (*
   328 Proper theorem proving support would be nice. For example, if
   329 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
   330 produced something like
   331 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
   332 *)
   333 
   334 nonterminals lc_qual lc_quals
   335 
   336 syntax
   337 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
   338 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
   339 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
   340 (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
   341 "_lc_end" :: "lc_quals" ("]")
   342 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
   343 "_lc_abs" :: "'a => 'b list => 'b list"
   344 
   345 (* These are easier than ML code but cannot express the optimized
   346    translation of [e. p<-xs]
   347 translations
   348 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
   349 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
   350  => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
   351 "[e. P]" => "if P then [e] else []"
   352 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
   353  => "if P then (_listcompr e Q Qs) else []"
   354 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
   355  => "_Let b (_listcompr e Q Qs)"
   356 *)
   357 
   358 syntax (xsymbols)
   359 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
   360 syntax (HTML output)
   361 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
   362 
   363 parse_translation (advanced) {*
   364 let
   365   val NilC = Syntax.const @{const_syntax Nil};
   366   val ConsC = Syntax.const @{const_syntax Cons};
   367   val mapC = Syntax.const @{const_syntax map};
   368   val concatC = Syntax.const @{const_syntax concat};
   369   val IfC = Syntax.const @{const_syntax If};
   370 
   371   fun singl x = ConsC $ x $ NilC;
   372 
   373   fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
   374     let
   375       val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
   376       val e = if opti then singl e else e;
   377       val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
   378       val case2 =
   379         Syntax.const @{syntax_const "_case1"} $
   380           Syntax.const @{const_syntax dummy_pattern} $ NilC;
   381       val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
   382       val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];
   383     in lambda x ft end;
   384 
   385   fun abs_tr ctxt (p as Free (s, T)) e opti =
   386         let
   387           val thy = ProofContext.theory_of ctxt;
   388           val s' = Sign.intern_const thy s;
   389         in
   390           if Sign.declared_const thy s'
   391           then (pat_tr ctxt p e opti, false)
   392           else (lambda p e, true)
   393         end
   394     | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
   395 
   396   fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
   397         let
   398           val res =
   399             (case qs of
   400               Const (@{syntax_const "_lc_end"}, _) => singl e
   401             | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
   402         in IfC $ b $ res $ NilC end
   403     | lc_tr ctxt
   404           [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   405             Const(@{syntax_const "_lc_end"}, _)] =
   406         (case abs_tr ctxt p e true of
   407           (f, true) => mapC $ f $ es
   408         | (f, false) => concatC $ (mapC $ f $ es))
   409     | lc_tr ctxt
   410           [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   411             Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
   412         let val e' = lc_tr ctxt [e, q, qs];
   413         in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
   414 
   415 in [(@{syntax_const "_listcompr"}, lc_tr)] end
   416 *}
   417 
   418 term "[(x,y,z). b]"
   419 term "[(x,y,z). x\<leftarrow>xs]"
   420 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
   421 term "[(x,y,z). x<a, x>b]"
   422 term "[(x,y,z). x\<leftarrow>xs, x>b]"
   423 term "[(x,y,z). x<a, x\<leftarrow>xs]"
   424 term "[(x,y). Cons True x \<leftarrow> xs]"
   425 term "[(x,y,z). Cons x [] \<leftarrow> xs]"
   426 term "[(x,y,z). x<a, x>b, x=d]"
   427 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
   428 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
   429 term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
   430 term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
   431 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
   432 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
   433 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
   434 (*
   435 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
   436 *)
   437 
   438 
   439 subsubsection {* @{const Nil} and @{const Cons} *}
   440 
   441 lemma not_Cons_self [simp]:
   442   "xs \<noteq> x # xs"
   443 by (induct xs) auto
   444 
   445 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
   446 
   447 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
   448 by (induct xs) auto
   449 
   450 lemma length_induct:
   451   "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
   452 by (rule measure_induct [of length]) iprover
   453 
   454 lemma list_nonempty_induct [consumes 1, case_names single cons]:
   455   assumes "xs \<noteq> []"
   456   assumes single: "\<And>x. P [x]"
   457   assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"
   458   shows "P xs"
   459 using `xs \<noteq> []` proof (induct xs)
   460   case Nil then show ?case by simp
   461 next
   462   case (Cons x xs) show ?case proof (cases xs)
   463     case Nil with single show ?thesis by simp
   464   next
   465     case Cons then have "xs \<noteq> []" by simp
   466     moreover with Cons.hyps have "P xs" .
   467     ultimately show ?thesis by (rule cons)
   468   qed
   469 qed
   470 
   471 
   472 subsubsection {* @{const length} *}
   473 
   474 text {*
   475   Needs to come before @{text "@"} because of theorem @{text
   476   append_eq_append_conv}.
   477 *}
   478 
   479 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"
   480 by (induct xs) auto
   481 
   482 lemma length_map [simp]: "length (map f xs) = length xs"
   483 by (induct xs) auto
   484 
   485 lemma length_rev [simp]: "length (rev xs) = length xs"
   486 by (induct xs) auto
   487 
   488 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
   489 by (cases xs) auto
   490 
   491 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
   492 by (induct xs) auto
   493 
   494 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"
   495 by (induct xs) auto
   496 
   497 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"
   498 by auto
   499 
   500 lemma length_Suc_conv:
   501 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
   502 by (induct xs) auto
   503 
   504 lemma Suc_length_conv:
   505 "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
   506 apply (induct xs, simp, simp)
   507 apply blast
   508 done
   509 
   510 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
   511   by (induct xs) auto
   512 
   513 lemma list_induct2 [consumes 1, case_names Nil Cons]:
   514   "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
   515    (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))
   516    \<Longrightarrow> P xs ys"
   517 proof (induct xs arbitrary: ys)
   518   case Nil then show ?case by simp
   519 next
   520   case (Cons x xs ys) then show ?case by (cases ys) simp_all
   521 qed
   522 
   523 lemma list_induct3 [consumes 2, case_names Nil Cons]:
   524   "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>
   525    (\<And>x xs y ys z zs. length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P xs ys zs \<Longrightarrow> P (x#xs) (y#ys) (z#zs))
   526    \<Longrightarrow> P xs ys zs"
   527 proof (induct xs arbitrary: ys zs)
   528   case Nil then show ?case by simp
   529 next
   530   case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)
   531     (cases zs, simp_all)
   532 qed
   533 
   534 lemma list_induct4 [consumes 3, case_names Nil Cons]:
   535   "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>
   536    P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>
   537    length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>
   538    P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"
   539 proof (induct xs arbitrary: ys zs ws)
   540   case Nil then show ?case by simp
   541 next
   542   case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)
   543 qed
   544 
   545 lemma list_induct2': 
   546   "\<lbrakk> P [] [];
   547   \<And>x xs. P (x#xs) [];
   548   \<And>y ys. P [] (y#ys);
   549    \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
   550  \<Longrightarrow> P xs ys"
   551 by (induct xs arbitrary: ys) (case_tac x, auto)+
   552 
   553 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
   554 by (rule Eq_FalseI) auto
   555 
   556 simproc_setup list_neq ("(xs::'a list) = ys") = {*
   557 (*
   558 Reduces xs=ys to False if xs and ys cannot be of the same length.
   559 This is the case if the atomic sublists of one are a submultiset
   560 of those of the other list and there are fewer Cons's in one than the other.
   561 *)
   562 
   563 let
   564 
   565 fun len (Const(@{const_name Nil},_)) acc = acc
   566   | len (Const(@{const_name Cons},_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
   567   | len (Const(@{const_name append},_) $ xs $ ys) acc = len xs (len ys acc)
   568   | len (Const(@{const_name rev},_) $ xs) acc = len xs acc
   569   | len (Const(@{const_name map},_) $ _ $ xs) acc = len xs acc
   570   | len t (ts,n) = (t::ts,n);
   571 
   572 fun list_neq _ ss ct =
   573   let
   574     val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
   575     val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
   576     fun prove_neq() =
   577       let
   578         val Type(_,listT::_) = eqT;
   579         val size = HOLogic.size_const listT;
   580         val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
   581         val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
   582         val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
   583           (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
   584       in SOME (thm RS @{thm neq_if_length_neq}) end
   585   in
   586     if m < n andalso submultiset (op aconv) (ls,rs) orelse
   587        n < m andalso submultiset (op aconv) (rs,ls)
   588     then prove_neq() else NONE
   589   end;
   590 in list_neq end;
   591 *}
   592 
   593 
   594 subsubsection {* @{text "@"} -- append *}
   595 
   596 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
   597 by (induct xs) auto
   598 
   599 lemma append_Nil2 [simp]: "xs @ [] = xs"
   600 by (induct xs) auto
   601 
   602 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
   603 by (induct xs) auto
   604 
   605 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"
   606 by (induct xs) auto
   607 
   608 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"
   609 by (induct xs) auto
   610 
   611 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
   612 by (induct xs) auto
   613 
   614 lemma append_eq_append_conv [simp, no_atp]:
   615  "length xs = length ys \<or> length us = length vs
   616  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
   617 apply (induct xs arbitrary: ys)
   618  apply (case_tac ys, simp, force)
   619 apply (case_tac ys, force, simp)
   620 done
   621 
   622 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
   623   (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
   624 apply (induct xs arbitrary: ys zs ts)
   625  apply fastsimp
   626 apply(case_tac zs)
   627  apply simp
   628 apply fastsimp
   629 done
   630 
   631 lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"
   632 by simp
   633 
   634 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
   635 by simp
   636 
   637 lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)"
   638 by simp
   639 
   640 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
   641 using append_same_eq [of _ _ "[]"] by auto
   642 
   643 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
   644 using append_same_eq [of "[]"] by auto
   645 
   646 lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
   647 by (induct xs) auto
   648 
   649 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
   650 by (induct xs) auto
   651 
   652 lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
   653 by (simp add: hd_append split: list.split)
   654 
   655 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"
   656 by (simp split: list.split)
   657 
   658 lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
   659 by (simp add: tl_append split: list.split)
   660 
   661 
   662 lemma Cons_eq_append_conv: "x#xs = ys@zs =
   663  (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
   664 by(cases ys) auto
   665 
   666 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =
   667  (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
   668 by(cases ys) auto
   669 
   670 
   671 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
   672 
   673 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
   674 by simp
   675 
   676 lemma Cons_eq_appendI:
   677 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
   678 by (drule sym) simp
   679 
   680 lemma append_eq_appendI:
   681 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
   682 by (drule sym) simp
   683 
   684 
   685 text {*
   686 Simplification procedure for all list equalities.
   687 Currently only tries to rearrange @{text "@"} to see if
   688 - both lists end in a singleton list,
   689 - or both lists end in the same list.
   690 *}
   691 
   692 ML {*
   693 local
   694 
   695 fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
   696   (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
   697   | last (Const(@{const_name append},_) $ _ $ ys) = last ys
   698   | last t = t;
   699 
   700 fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
   701   | list1 _ = false;
   702 
   703 fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
   704   (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
   705   | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
   706   | butlast xs = Const(@{const_name Nil},fastype_of xs);
   707 
   708 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
   709   @{thm append_Nil}, @{thm append_Cons}];
   710 
   711 fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
   712   let
   713     val lastl = last lhs and lastr = last rhs;
   714     fun rearr conv =
   715       let
   716         val lhs1 = butlast lhs and rhs1 = butlast rhs;
   717         val Type(_,listT::_) = eqT
   718         val appT = [listT,listT] ---> listT
   719         val app = Const(@{const_name append},appT)
   720         val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
   721         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
   722         val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
   723           (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
   724       in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
   725 
   726   in
   727     if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
   728     else if lastl aconv lastr then rearr @{thm append_same_eq}
   729     else NONE
   730   end;
   731 
   732 in
   733 
   734 val list_eq_simproc =
   735   Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
   736 
   737 end;
   738 
   739 Addsimprocs [list_eq_simproc];
   740 *}
   741 
   742 
   743 subsubsection {* @{text map} *}
   744 
   745 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
   746 by (induct xs) simp_all
   747 
   748 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
   749 by (rule ext, induct_tac xs) auto
   750 
   751 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
   752 by (induct xs) auto
   753 
   754 lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"
   755 by (induct xs) auto
   756 
   757 lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)"
   758 apply(rule ext)
   759 apply(simp)
   760 done
   761 
   762 lemma rev_map: "rev (map f xs) = map f (rev xs)"
   763 by (induct xs) auto
   764 
   765 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
   766 by (induct xs) auto
   767 
   768 lemma map_cong [fundef_cong, recdef_cong]:
   769 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
   770 -- {* a congruence rule for @{text map} *}
   771 by simp
   772 
   773 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
   774 by (cases xs) auto
   775 
   776 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
   777 by (cases xs) auto
   778 
   779 lemma map_eq_Cons_conv:
   780  "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
   781 by (cases xs) auto
   782 
   783 lemma Cons_eq_map_conv:
   784  "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
   785 by (cases ys) auto
   786 
   787 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
   788 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
   789 declare map_eq_Cons_D [dest!]  Cons_eq_map_D [dest!]
   790 
   791 lemma ex_map_conv:
   792   "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
   793 by(induct ys, auto simp add: Cons_eq_map_conv)
   794 
   795 lemma map_eq_imp_length_eq:
   796   assumes "map f xs = map g ys"
   797   shows "length xs = length ys"
   798 using assms proof (induct ys arbitrary: xs)
   799   case Nil then show ?case by simp
   800 next
   801   case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
   802   from Cons xs have "map f zs = map g ys" by simp
   803   moreover with Cons have "length zs = length ys" by blast
   804   with xs show ?case by simp
   805 qed
   806   
   807 lemma map_inj_on:
   808  "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
   809   ==> xs = ys"
   810 apply(frule map_eq_imp_length_eq)
   811 apply(rotate_tac -1)
   812 apply(induct rule:list_induct2)
   813  apply simp
   814 apply(simp)
   815 apply (blast intro:sym)
   816 done
   817 
   818 lemma inj_on_map_eq_map:
   819  "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
   820 by(blast dest:map_inj_on)
   821 
   822 lemma map_injective:
   823  "map f xs = map f ys ==> inj f ==> xs = ys"
   824 by (induct ys arbitrary: xs) (auto dest!:injD)
   825 
   826 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
   827 by(blast dest:map_injective)
   828 
   829 lemma inj_mapI: "inj f ==> inj (map f)"
   830 by (iprover dest: map_injective injD intro: inj_onI)
   831 
   832 lemma inj_mapD: "inj (map f) ==> inj f"
   833 apply (unfold inj_on_def, clarify)
   834 apply (erule_tac x = "[x]" in ballE)
   835  apply (erule_tac x = "[y]" in ballE, simp, blast)
   836 apply blast
   837 done
   838 
   839 lemma inj_map[iff]: "inj (map f) = inj f"
   840 by (blast dest: inj_mapD intro: inj_mapI)
   841 
   842 lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
   843 apply(rule inj_onI)
   844 apply(erule map_inj_on)
   845 apply(blast intro:inj_onI dest:inj_onD)
   846 done
   847 
   848 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
   849 by (induct xs, auto)
   850 
   851 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
   852 by (induct xs) auto
   853 
   854 lemma map_fst_zip[simp]:
   855   "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
   856 by (induct rule:list_induct2, simp_all)
   857 
   858 lemma map_snd_zip[simp]:
   859   "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
   860 by (induct rule:list_induct2, simp_all)
   861 
   862 
   863 subsubsection {* @{text rev} *}
   864 
   865 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
   866 by (induct xs) auto
   867 
   868 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
   869 by (induct xs) auto
   870 
   871 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
   872 by auto
   873 
   874 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
   875 by (induct xs) auto
   876 
   877 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
   878 by (induct xs) auto
   879 
   880 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
   881 by (cases xs) auto
   882 
   883 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
   884 by (cases xs) auto
   885 
   886 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
   887 apply (induct xs arbitrary: ys, force)
   888 apply (case_tac ys, simp, force)
   889 done
   890 
   891 lemma inj_on_rev[iff]: "inj_on rev A"
   892 by(simp add:inj_on_def)
   893 
   894 lemma rev_induct [case_names Nil snoc]:
   895   "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
   896 apply(simplesubst rev_rev_ident[symmetric])
   897 apply(rule_tac list = "rev xs" in list.induct, simp_all)
   898 done
   899 
   900 lemma rev_exhaust [case_names Nil snoc]:
   901   "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
   902 by (induct xs rule: rev_induct) auto
   903 
   904 lemmas rev_cases = rev_exhaust
   905 
   906 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
   907 by(rule rev_cases[of xs]) auto
   908 
   909 
   910 subsubsection {* @{text set} *}
   911 
   912 lemma finite_set [iff]: "finite (set xs)"
   913 by (induct xs) auto
   914 
   915 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
   916 by (induct xs) auto
   917 
   918 lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"
   919 by(cases xs) auto
   920 
   921 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
   922 by auto
   923 
   924 lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs" 
   925 by auto
   926 
   927 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
   928 by (induct xs) auto
   929 
   930 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
   931 by(induct xs) auto
   932 
   933 lemma set_rev [simp]: "set (rev xs) = set xs"
   934 by (induct xs) auto
   935 
   936 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
   937 by (induct xs) auto
   938 
   939 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
   940 by (induct xs) auto
   941 
   942 lemma set_upt [simp]: "set[i..<j] = {i..<j}"
   943 by (induct j) (simp_all add: atLeastLessThanSuc)
   944 
   945 
   946 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
   947 proof (induct xs)
   948   case Nil thus ?case by simp
   949 next
   950   case Cons thus ?case by (auto intro: Cons_eq_appendI)
   951 qed
   952 
   953 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
   954   by (auto elim: split_list)
   955 
   956 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
   957 proof (induct xs)
   958   case Nil thus ?case by simp
   959 next
   960   case (Cons a xs)
   961   show ?case
   962   proof cases
   963     assume "x = a" thus ?case using Cons by fastsimp
   964   next
   965     assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
   966   qed
   967 qed
   968 
   969 lemma in_set_conv_decomp_first:
   970   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
   971   by (auto dest!: split_list_first)
   972 
   973 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
   974 proof (induct xs rule:rev_induct)
   975   case Nil thus ?case by simp
   976 next
   977   case (snoc a xs)
   978   show ?case
   979   proof cases
   980     assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
   981   next
   982     assume "x \<noteq> a" thus ?case using snoc by fastsimp
   983   qed
   984 qed
   985 
   986 lemma in_set_conv_decomp_last:
   987   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
   988   by (auto dest!: split_list_last)
   989 
   990 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
   991 proof (induct xs)
   992   case Nil thus ?case by simp
   993 next
   994   case Cons thus ?case
   995     by(simp add:Bex_def)(metis append_Cons append.simps(1))
   996 qed
   997 
   998 lemma split_list_propE:
   999   assumes "\<exists>x \<in> set xs. P x"
  1000   obtains ys x zs where "xs = ys @ x # zs" and "P x"
  1001 using split_list_prop [OF assms] by blast
  1002 
  1003 lemma split_list_first_prop:
  1004   "\<exists>x \<in> set xs. P x \<Longrightarrow>
  1005    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
  1006 proof (induct xs)
  1007   case Nil thus ?case by simp
  1008 next
  1009   case (Cons x xs)
  1010   show ?case
  1011   proof cases
  1012     assume "P x"
  1013     thus ?thesis by simp
  1014       (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
  1015   next
  1016     assume "\<not> P x"
  1017     hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
  1018     thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
  1019   qed
  1020 qed
  1021 
  1022 lemma split_list_first_propE:
  1023   assumes "\<exists>x \<in> set xs. P x"
  1024   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
  1025 using split_list_first_prop [OF assms] by blast
  1026 
  1027 lemma split_list_first_prop_iff:
  1028   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
  1029    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
  1030 by (rule, erule split_list_first_prop) auto
  1031 
  1032 lemma split_list_last_prop:
  1033   "\<exists>x \<in> set xs. P x \<Longrightarrow>
  1034    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
  1035 proof(induct xs rule:rev_induct)
  1036   case Nil thus ?case by simp
  1037 next
  1038   case (snoc x xs)
  1039   show ?case
  1040   proof cases
  1041     assume "P x" thus ?thesis by (metis emptyE set_empty)
  1042   next
  1043     assume "\<not> P x"
  1044     hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
  1045     thus ?thesis using `\<not> P x` snoc(1) by fastsimp
  1046   qed
  1047 qed
  1048 
  1049 lemma split_list_last_propE:
  1050   assumes "\<exists>x \<in> set xs. P x"
  1051   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
  1052 using split_list_last_prop [OF assms] by blast
  1053 
  1054 lemma split_list_last_prop_iff:
  1055   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
  1056    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
  1057 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
  1058 
  1059 lemma finite_list: "finite A ==> EX xs. set xs = A"
  1060   by (erule finite_induct)
  1061     (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
  1062 
  1063 lemma card_length: "card (set xs) \<le> length xs"
  1064 by (induct xs) (auto simp add: card_insert_if)
  1065 
  1066 lemma set_minus_filter_out:
  1067   "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
  1068   by (induct xs) auto
  1069 
  1070 
  1071 subsubsection {* @{text filter} *}
  1072 
  1073 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
  1074 by (induct xs) auto
  1075 
  1076 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
  1077 by (induct xs) simp_all
  1078 
  1079 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
  1080 by (induct xs) auto
  1081 
  1082 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
  1083 by (induct xs) (auto simp add: le_SucI)
  1084 
  1085 lemma sum_length_filter_compl:
  1086   "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
  1087 by(induct xs) simp_all
  1088 
  1089 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
  1090 by (induct xs) auto
  1091 
  1092 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
  1093 by (induct xs) auto
  1094 
  1095 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
  1096 by (induct xs) simp_all
  1097 
  1098 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
  1099 apply (induct xs)
  1100  apply auto
  1101 apply(cut_tac P=P and xs=xs in length_filter_le)
  1102 apply simp
  1103 done
  1104 
  1105 lemma filter_map:
  1106   "filter P (map f xs) = map f (filter (P o f) xs)"
  1107 by (induct xs) simp_all
  1108 
  1109 lemma length_filter_map[simp]:
  1110   "length (filter P (map f xs)) = length(filter (P o f) xs)"
  1111 by (simp add:filter_map)
  1112 
  1113 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
  1114 by auto
  1115 
  1116 lemma length_filter_less:
  1117   "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
  1118 proof (induct xs)
  1119   case Nil thus ?case by simp
  1120 next
  1121   case (Cons x xs) thus ?case
  1122     apply (auto split:split_if_asm)
  1123     using length_filter_le[of P xs] apply arith
  1124   done
  1125 qed
  1126 
  1127 lemma length_filter_conv_card:
  1128  "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
  1129 proof (induct xs)
  1130   case Nil thus ?case by simp
  1131 next
  1132   case (Cons x xs)
  1133   let ?S = "{i. i < length xs & p(xs!i)}"
  1134   have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
  1135   show ?case (is "?l = card ?S'")
  1136   proof (cases)
  1137     assume "p x"
  1138     hence eq: "?S' = insert 0 (Suc ` ?S)"
  1139       by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
  1140     have "length (filter p (x # xs)) = Suc(card ?S)"
  1141       using Cons `p x` by simp
  1142     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
  1143       by (simp add: card_image inj_Suc)
  1144     also have "\<dots> = card ?S'" using eq fin
  1145       by (simp add:card_insert_if) (simp add:image_def)
  1146     finally show ?thesis .
  1147   next
  1148     assume "\<not> p x"
  1149     hence eq: "?S' = Suc ` ?S"
  1150       by(auto simp add: image_def split:nat.split elim:lessE)
  1151     have "length (filter p (x # xs)) = card ?S"
  1152       using Cons `\<not> p x` by simp
  1153     also have "\<dots> = card(Suc ` ?S)" using fin
  1154       by (simp add: card_image inj_Suc)
  1155     also have "\<dots> = card ?S'" using eq fin
  1156       by (simp add:card_insert_if)
  1157     finally show ?thesis .
  1158   qed
  1159 qed
  1160 
  1161 lemma Cons_eq_filterD:
  1162  "x#xs = filter P ys \<Longrightarrow>
  1163   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  1164   (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
  1165 proof(induct ys)
  1166   case Nil thus ?case by simp
  1167 next
  1168   case (Cons y ys)
  1169   show ?case (is "\<exists>x. ?Q x")
  1170   proof cases
  1171     assume Py: "P y"
  1172     show ?thesis
  1173     proof cases
  1174       assume "x = y"
  1175       with Py Cons.prems have "?Q []" by simp
  1176       then show ?thesis ..
  1177     next
  1178       assume "x \<noteq> y"
  1179       with Py Cons.prems show ?thesis by simp
  1180     qed
  1181   next
  1182     assume "\<not> P y"
  1183     with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
  1184     then have "?Q (y#us)" by simp
  1185     then show ?thesis ..
  1186   qed
  1187 qed
  1188 
  1189 lemma filter_eq_ConsD:
  1190  "filter P ys = x#xs \<Longrightarrow>
  1191   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  1192 by(rule Cons_eq_filterD) simp
  1193 
  1194 lemma filter_eq_Cons_iff:
  1195  "(filter P ys = x#xs) =
  1196   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
  1197 by(auto dest:filter_eq_ConsD)
  1198 
  1199 lemma Cons_eq_filter_iff:
  1200  "(x#xs = filter P ys) =
  1201   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
  1202 by(auto dest:Cons_eq_filterD)
  1203 
  1204 lemma filter_cong[fundef_cong, recdef_cong]:
  1205  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
  1206 apply simp
  1207 apply(erule thin_rl)
  1208 by (induct ys) simp_all
  1209 
  1210 
  1211 subsubsection {* List partitioning *}
  1212 
  1213 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
  1214   "partition P [] = ([], [])"
  1215   | "partition P (x # xs) = 
  1216       (let (yes, no) = partition P xs
  1217       in if P x then (x # yes, no) else (yes, x # no))"
  1218 
  1219 lemma partition_filter1:
  1220     "fst (partition P xs) = filter P xs"
  1221 by (induct xs) (auto simp add: Let_def split_def)
  1222 
  1223 lemma partition_filter2:
  1224     "snd (partition P xs) = filter (Not o P) xs"
  1225 by (induct xs) (auto simp add: Let_def split_def)
  1226 
  1227 lemma partition_P:
  1228   assumes "partition P xs = (yes, no)"
  1229   shows "(\<forall>p \<in> set yes.  P p) \<and> (\<forall>p  \<in> set no. \<not> P p)"
  1230 proof -
  1231   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
  1232     by simp_all
  1233   then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
  1234 qed
  1235 
  1236 lemma partition_set:
  1237   assumes "partition P xs = (yes, no)"
  1238   shows "set yes \<union> set no = set xs"
  1239 proof -
  1240   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
  1241     by simp_all
  1242   then show ?thesis by (auto simp add: partition_filter1 partition_filter2) 
  1243 qed
  1244 
  1245 lemma partition_filter_conv[simp]:
  1246   "partition f xs = (filter f xs,filter (Not o f) xs)"
  1247 unfolding partition_filter2[symmetric]
  1248 unfolding partition_filter1[symmetric] by simp
  1249 
  1250 declare partition.simps[simp del]
  1251 
  1252 
  1253 subsubsection {* @{text concat} *}
  1254 
  1255 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
  1256 by (induct xs) auto
  1257 
  1258 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
  1259 by (induct xss) auto
  1260 
  1261 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
  1262 by (induct xss) auto
  1263 
  1264 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
  1265 by (induct xs) auto
  1266 
  1267 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
  1268 by (induct xs) auto
  1269 
  1270 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
  1271 by (induct xs) auto
  1272 
  1273 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
  1274 by (induct xs) auto
  1275 
  1276 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
  1277 by (induct xs) auto
  1278 
  1279 
  1280 subsubsection {* @{text nth} *}
  1281 
  1282 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
  1283 by auto
  1284 
  1285 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
  1286 by auto
  1287 
  1288 declare nth.simps [simp del]
  1289 
  1290 lemma nth_append:
  1291   "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
  1292 apply (induct xs arbitrary: n, simp)
  1293 apply (case_tac n, auto)
  1294 done
  1295 
  1296 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
  1297 by (induct xs) auto
  1298 
  1299 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
  1300 by (induct xs) auto
  1301 
  1302 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
  1303 apply (induct xs arbitrary: n, simp)
  1304 apply (case_tac n, auto)
  1305 done
  1306 
  1307 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
  1308 by(cases xs) simp_all
  1309 
  1310 
  1311 lemma list_eq_iff_nth_eq:
  1312  "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
  1313 apply(induct xs arbitrary: ys)
  1314  apply force
  1315 apply(case_tac ys)
  1316  apply simp
  1317 apply(simp add:nth_Cons split:nat.split)apply blast
  1318 done
  1319 
  1320 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
  1321 apply (induct xs, simp, simp)
  1322 apply safe
  1323 apply (metis nat_case_0 nth.simps zero_less_Suc)
  1324 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
  1325 apply (case_tac i, simp)
  1326 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
  1327 done
  1328 
  1329 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
  1330 by(auto simp:set_conv_nth)
  1331 
  1332 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
  1333 by (auto simp add: set_conv_nth)
  1334 
  1335 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
  1336 by (auto simp add: set_conv_nth)
  1337 
  1338 lemma all_nth_imp_all_set:
  1339 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
  1340 by (auto simp add: set_conv_nth)
  1341 
  1342 lemma all_set_conv_all_nth:
  1343 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
  1344 by (auto simp add: set_conv_nth)
  1345 
  1346 lemma rev_nth:
  1347   "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
  1348 proof (induct xs arbitrary: n)
  1349   case Nil thus ?case by simp
  1350 next
  1351   case (Cons x xs)
  1352   hence n: "n < Suc (length xs)" by simp
  1353   moreover
  1354   { assume "n < length xs"
  1355     with n obtain n' where "length xs - n = Suc n'"
  1356       by (cases "length xs - n", auto)
  1357     moreover
  1358     then have "length xs - Suc n = n'" by simp
  1359     ultimately
  1360     have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
  1361   }
  1362   ultimately
  1363   show ?case by (clarsimp simp add: Cons nth_append)
  1364 qed
  1365 
  1366 lemma Skolem_list_nth:
  1367   "(ALL i<k. EX x. P i x) = (EX xs. size xs = k & (ALL i<k. P i (xs!i)))"
  1368   (is "_ = (EX xs. ?P k xs)")
  1369 proof(induct k)
  1370   case 0 show ?case by simp
  1371 next
  1372   case (Suc k)
  1373   show ?case (is "?L = ?R" is "_ = (EX xs. ?P' xs)")
  1374   proof
  1375     assume "?R" thus "?L" using Suc by auto
  1376   next
  1377     assume "?L"
  1378     with Suc obtain x xs where "?P k xs & P k x" by (metis less_Suc_eq)
  1379     hence "?P'(xs@[x])" by(simp add:nth_append less_Suc_eq)
  1380     thus "?R" ..
  1381   qed
  1382 qed
  1383 
  1384 
  1385 subsubsection {* @{text list_update} *}
  1386 
  1387 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
  1388 by (induct xs arbitrary: i) (auto split: nat.split)
  1389 
  1390 lemma nth_list_update:
  1391 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
  1392 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
  1393 
  1394 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
  1395 by (simp add: nth_list_update)
  1396 
  1397 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
  1398 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
  1399 
  1400 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
  1401 by (induct xs arbitrary: i) (simp_all split:nat.splits)
  1402 
  1403 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
  1404 apply (induct xs arbitrary: i)
  1405  apply simp
  1406 apply (case_tac i)
  1407 apply simp_all
  1408 done
  1409 
  1410 lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
  1411 by(metis length_0_conv length_list_update)
  1412 
  1413 lemma list_update_same_conv:
  1414 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
  1415 by (induct xs arbitrary: i) (auto split: nat.split)
  1416 
  1417 lemma list_update_append1:
  1418  "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
  1419 apply (induct xs arbitrary: i, simp)
  1420 apply(simp split:nat.split)
  1421 done
  1422 
  1423 lemma list_update_append:
  1424   "(xs @ ys) [n:= x] = 
  1425   (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
  1426 by (induct xs arbitrary: n) (auto split:nat.splits)
  1427 
  1428 lemma list_update_length [simp]:
  1429  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
  1430 by (induct xs, auto)
  1431 
  1432 lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
  1433 by(induct xs arbitrary: k)(auto split:nat.splits)
  1434 
  1435 lemma rev_update:
  1436   "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
  1437 by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
  1438 
  1439 lemma update_zip:
  1440   "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
  1441 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
  1442 
  1443 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
  1444 by (induct xs arbitrary: i) (auto split: nat.split)
  1445 
  1446 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
  1447 by (blast dest!: set_update_subset_insert [THEN subsetD])
  1448 
  1449 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
  1450 by (induct xs arbitrary: n) (auto split:nat.splits)
  1451 
  1452 lemma list_update_overwrite[simp]:
  1453   "xs [i := x, i := y] = xs [i := y]"
  1454 apply (induct xs arbitrary: i) apply simp
  1455 apply (case_tac i, simp_all)
  1456 done
  1457 
  1458 lemma list_update_swap:
  1459   "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
  1460 apply (induct xs arbitrary: i i')
  1461 apply simp
  1462 apply (case_tac i, case_tac i')
  1463 apply auto
  1464 apply (case_tac i')
  1465 apply auto
  1466 done
  1467 
  1468 lemma list_update_code [code]:
  1469   "[][i := y] = []"
  1470   "(x # xs)[0 := y] = y # xs"
  1471   "(x # xs)[Suc i := y] = x # xs[i := y]"
  1472   by simp_all
  1473 
  1474 
  1475 subsubsection {* @{text last} and @{text butlast} *}
  1476 
  1477 lemma last_snoc [simp]: "last (xs @ [x]) = x"
  1478 by (induct xs) auto
  1479 
  1480 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
  1481 by (induct xs) auto
  1482 
  1483 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
  1484 by(simp add:last.simps)
  1485 
  1486 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
  1487 by(simp add:last.simps)
  1488 
  1489 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
  1490 by (induct xs) (auto)
  1491 
  1492 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
  1493 by(simp add:last_append)
  1494 
  1495 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
  1496 by(simp add:last_append)
  1497 
  1498 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
  1499 by(rule rev_exhaust[of xs]) simp_all
  1500 
  1501 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
  1502 by(cases xs) simp_all
  1503 
  1504 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
  1505 by (induct as) auto
  1506 
  1507 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
  1508 by (induct xs rule: rev_induct) auto
  1509 
  1510 lemma butlast_append:
  1511   "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
  1512 by (induct xs arbitrary: ys) auto
  1513 
  1514 lemma append_butlast_last_id [simp]:
  1515 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
  1516 by (induct xs) auto
  1517 
  1518 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
  1519 by (induct xs) (auto split: split_if_asm)
  1520 
  1521 lemma in_set_butlast_appendI:
  1522 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
  1523 by (auto dest: in_set_butlastD simp add: butlast_append)
  1524 
  1525 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
  1526 apply (induct xs arbitrary: n)
  1527  apply simp
  1528 apply (auto split:nat.split)
  1529 done
  1530 
  1531 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
  1532 by(induct xs)(auto simp:neq_Nil_conv)
  1533 
  1534 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
  1535 by (induct xs, simp, case_tac xs, simp_all)
  1536 
  1537 lemma last_list_update:
  1538   "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
  1539 by (auto simp: last_conv_nth)
  1540 
  1541 lemma butlast_list_update:
  1542   "butlast(xs[k:=x]) =
  1543  (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
  1544 apply(cases xs rule:rev_cases)
  1545 apply simp
  1546 apply(simp add:list_update_append split:nat.splits)
  1547 done
  1548 
  1549 lemma last_map:
  1550   "xs \<noteq> [] \<Longrightarrow> last (map f xs) = f (last xs)"
  1551   by (cases xs rule: rev_cases) simp_all
  1552 
  1553 lemma map_butlast:
  1554   "map f (butlast xs) = butlast (map f xs)"
  1555   by (induct xs) simp_all
  1556 
  1557 
  1558 subsubsection {* @{text take} and @{text drop} *}
  1559 
  1560 lemma take_0 [simp]: "take 0 xs = []"
  1561 by (induct xs) auto
  1562 
  1563 lemma drop_0 [simp]: "drop 0 xs = xs"
  1564 by (induct xs) auto
  1565 
  1566 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
  1567 by simp
  1568 
  1569 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
  1570 by simp
  1571 
  1572 declare take_Cons [simp del] and drop_Cons [simp del]
  1573 
  1574 lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
  1575   unfolding One_nat_def by simp
  1576 
  1577 lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
  1578   unfolding One_nat_def by simp
  1579 
  1580 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
  1581 by(clarsimp simp add:neq_Nil_conv)
  1582 
  1583 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
  1584 by(cases xs, simp_all)
  1585 
  1586 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
  1587 by (induct xs arbitrary: n) simp_all
  1588 
  1589 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
  1590 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
  1591 
  1592 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
  1593 by (cases n, simp, cases xs, auto)
  1594 
  1595 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
  1596 by (simp only: drop_tl)
  1597 
  1598 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
  1599 apply (induct xs arbitrary: n, simp)
  1600 apply(simp add:drop_Cons nth_Cons split:nat.splits)
  1601 done
  1602 
  1603 lemma take_Suc_conv_app_nth:
  1604   "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
  1605 apply (induct xs arbitrary: i, simp)
  1606 apply (case_tac i, auto)
  1607 done
  1608 
  1609 lemma drop_Suc_conv_tl:
  1610   "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
  1611 apply (induct xs arbitrary: i, simp)
  1612 apply (case_tac i, auto)
  1613 done
  1614 
  1615 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
  1616 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1617 
  1618 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
  1619 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1620 
  1621 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
  1622 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1623 
  1624 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
  1625 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1626 
  1627 lemma take_append [simp]:
  1628   "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
  1629 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1630 
  1631 lemma drop_append [simp]:
  1632   "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
  1633 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1634 
  1635 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
  1636 apply (induct m arbitrary: xs n, auto)
  1637 apply (case_tac xs, auto)
  1638 apply (case_tac n, auto)
  1639 done
  1640 
  1641 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
  1642 apply (induct m arbitrary: xs, auto)
  1643 apply (case_tac xs, auto)
  1644 done
  1645 
  1646 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
  1647 apply (induct m arbitrary: xs n, auto)
  1648 apply (case_tac xs, auto)
  1649 done
  1650 
  1651 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
  1652 apply(induct xs arbitrary: m n)
  1653  apply simp
  1654 apply(simp add: take_Cons drop_Cons split:nat.split)
  1655 done
  1656 
  1657 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
  1658 apply (induct n arbitrary: xs, auto)
  1659 apply (case_tac xs, auto)
  1660 done
  1661 
  1662 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
  1663 apply(induct xs arbitrary: n)
  1664  apply simp
  1665 apply(simp add:take_Cons split:nat.split)
  1666 done
  1667 
  1668 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
  1669 apply(induct xs arbitrary: n)
  1670 apply simp
  1671 apply(simp add:drop_Cons split:nat.split)
  1672 done
  1673 
  1674 lemma take_map: "take n (map f xs) = map f (take n xs)"
  1675 apply (induct n arbitrary: xs, auto)
  1676 apply (case_tac xs, auto)
  1677 done
  1678 
  1679 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
  1680 apply (induct n arbitrary: xs, auto)
  1681 apply (case_tac xs, auto)
  1682 done
  1683 
  1684 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
  1685 apply (induct xs arbitrary: i, auto)
  1686 apply (case_tac i, auto)
  1687 done
  1688 
  1689 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
  1690 apply (induct xs arbitrary: i, auto)
  1691 apply (case_tac i, auto)
  1692 done
  1693 
  1694 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
  1695 apply (induct xs arbitrary: i n, auto)
  1696 apply (case_tac n, blast)
  1697 apply (case_tac i, auto)
  1698 done
  1699 
  1700 lemma nth_drop [simp]:
  1701   "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
  1702 apply (induct n arbitrary: xs i, auto)
  1703 apply (case_tac xs, auto)
  1704 done
  1705 
  1706 lemma butlast_take:
  1707   "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
  1708 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
  1709 
  1710 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
  1711 by (simp add: butlast_conv_take drop_take add_ac)
  1712 
  1713 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
  1714 by (simp add: butlast_conv_take min_max.inf_absorb1)
  1715 
  1716 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
  1717 by (simp add: butlast_conv_take drop_take add_ac)
  1718 
  1719 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
  1720 by(simp add: hd_conv_nth)
  1721 
  1722 lemma set_take_subset_set_take:
  1723   "m <= n \<Longrightarrow> set(take m xs) <= set(take n xs)"
  1724 by(induct xs arbitrary: m n)(auto simp:take_Cons split:nat.split)
  1725 
  1726 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
  1727 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
  1728 
  1729 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
  1730 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
  1731 
  1732 lemma set_drop_subset_set_drop:
  1733   "m >= n \<Longrightarrow> set(drop m xs) <= set(drop n xs)"
  1734 apply(induct xs arbitrary: m n)
  1735 apply(auto simp:drop_Cons split:nat.split)
  1736 apply (metis set_drop_subset subset_iff)
  1737 done
  1738 
  1739 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
  1740 using set_take_subset by fast
  1741 
  1742 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
  1743 using set_drop_subset by fast
  1744 
  1745 lemma append_eq_conv_conj:
  1746   "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
  1747 apply (induct xs arbitrary: zs, simp, clarsimp)
  1748 apply (case_tac zs, auto)
  1749 done
  1750 
  1751 lemma take_add: 
  1752   "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
  1753 apply (induct xs arbitrary: i, auto) 
  1754 apply (case_tac i, simp_all)
  1755 done
  1756 
  1757 lemma append_eq_append_conv_if:
  1758  "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
  1759   (if size xs\<^isub>1 \<le> size ys\<^isub>1
  1760    then xs\<^isub>1 = take (size xs\<^isub>1) ys\<^isub>1 \<and> xs\<^isub>2 = drop (size xs\<^isub>1) ys\<^isub>1 @ ys\<^isub>2
  1761    else take (size ys\<^isub>1) xs\<^isub>1 = ys\<^isub>1 \<and> drop (size ys\<^isub>1) xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>2)"
  1762 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
  1763  apply simp
  1764 apply(case_tac ys\<^isub>1)
  1765 apply simp_all
  1766 done
  1767 
  1768 lemma take_hd_drop:
  1769   "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
  1770 apply(induct xs arbitrary: n)
  1771 apply simp
  1772 apply(simp add:drop_Cons split:nat.split)
  1773 done
  1774 
  1775 lemma id_take_nth_drop:
  1776  "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs" 
  1777 proof -
  1778   assume si: "i < length xs"
  1779   hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
  1780   moreover
  1781   from si have "take (Suc i) xs = take i xs @ [xs!i]"
  1782     apply (rule_tac take_Suc_conv_app_nth) by arith
  1783   ultimately show ?thesis by auto
  1784 qed
  1785   
  1786 lemma upd_conv_take_nth_drop:
  1787  "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
  1788 proof -
  1789   assume i: "i < length xs"
  1790   have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
  1791     by(rule arg_cong[OF id_take_nth_drop[OF i]])
  1792   also have "\<dots> = take i xs @ a # drop (Suc i) xs"
  1793     using i by (simp add: list_update_append)
  1794   finally show ?thesis .
  1795 qed
  1796 
  1797 lemma nth_drop':
  1798   "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
  1799 apply (induct i arbitrary: xs)
  1800 apply (simp add: neq_Nil_conv)
  1801 apply (erule exE)+
  1802 apply simp
  1803 apply (case_tac xs)
  1804 apply simp_all
  1805 done
  1806 
  1807 
  1808 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
  1809 
  1810 lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"
  1811   by (induct xs) auto
  1812 
  1813 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
  1814 by (induct xs) auto
  1815 
  1816 lemma takeWhile_append1 [simp]:
  1817 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
  1818 by (induct xs) auto
  1819 
  1820 lemma takeWhile_append2 [simp]:
  1821 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
  1822 by (induct xs) auto
  1823 
  1824 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
  1825 by (induct xs) auto
  1826 
  1827 lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"
  1828 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
  1829 
  1830 lemma dropWhile_nth: "j < length (dropWhile P xs) \<Longrightarrow> dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"
  1831 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto
  1832 
  1833 lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"
  1834 by (induct xs) auto
  1835 
  1836 lemma dropWhile_append1 [simp]:
  1837 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
  1838 by (induct xs) auto
  1839 
  1840 lemma dropWhile_append2 [simp]:
  1841 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
  1842 by (induct xs) auto
  1843 
  1844 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
  1845 by (induct xs) (auto split: split_if_asm)
  1846 
  1847 lemma takeWhile_eq_all_conv[simp]:
  1848  "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
  1849 by(induct xs, auto)
  1850 
  1851 lemma dropWhile_eq_Nil_conv[simp]:
  1852  "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
  1853 by(induct xs, auto)
  1854 
  1855 lemma dropWhile_eq_Cons_conv:
  1856  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
  1857 by(induct xs, auto)
  1858 
  1859 lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
  1860 by (induct xs) (auto dest: set_takeWhileD)
  1861 
  1862 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
  1863 by (induct xs) auto
  1864 
  1865 lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"
  1866 by (induct xs) auto
  1867 
  1868 lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> f) xs)"
  1869 by (induct xs) auto
  1870 
  1871 lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"
  1872 by (induct xs) auto
  1873 
  1874 lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"
  1875 by (induct xs) auto
  1876 
  1877 lemma hd_dropWhile:
  1878   "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"
  1879 using assms by (induct xs) auto
  1880 
  1881 lemma takeWhile_eq_filter:
  1882   assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"
  1883   shows "takeWhile P xs = filter P xs"
  1884 proof -
  1885   have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)"
  1886     by simp
  1887   have B: "filter P (dropWhile P xs) = []"
  1888     unfolding filter_empty_conv using assms by blast
  1889   have "filter P xs = takeWhile P xs"
  1890     unfolding A filter_append B
  1891     by (auto simp add: filter_id_conv dest: set_takeWhileD)
  1892   thus ?thesis ..
  1893 qed
  1894 
  1895 lemma takeWhile_eq_take_P_nth:
  1896   "\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>
  1897   takeWhile P xs = take n xs"
  1898 proof (induct xs arbitrary: n)
  1899   case (Cons x xs)
  1900   thus ?case
  1901   proof (cases n)
  1902     case (Suc n') note this[simp]
  1903     have "P x" using Cons.prems(1)[of 0] by simp
  1904     moreover have "takeWhile P xs = take n' xs"
  1905     proof (rule Cons.hyps)
  1906       case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp
  1907     next case goal2 thus ?case using Cons by auto
  1908     qed
  1909     ultimately show ?thesis by simp
  1910    qed simp
  1911 qed simp
  1912 
  1913 lemma nth_length_takeWhile:
  1914   "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"
  1915 by (induct xs) auto
  1916 
  1917 lemma length_takeWhile_less_P_nth:
  1918   assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"
  1919   shows "j \<le> length (takeWhile P xs)"
  1920 proof (rule classical)
  1921   assume "\<not> ?thesis"
  1922   hence "length (takeWhile P xs) < length xs" using assms by simp
  1923   thus ?thesis using all `\<not> ?thesis` nth_length_takeWhile[of P xs] by auto
  1924 qed
  1925 
  1926 text{* The following two lemmmas could be generalized to an arbitrary
  1927 property. *}
  1928 
  1929 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
  1930  takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
  1931 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
  1932 
  1933 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
  1934   dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
  1935 apply(induct xs)
  1936  apply simp
  1937 apply auto
  1938 apply(subst dropWhile_append2)
  1939 apply auto
  1940 done
  1941 
  1942 lemma takeWhile_not_last:
  1943  "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
  1944 apply(induct xs)
  1945  apply simp
  1946 apply(case_tac xs)
  1947 apply(auto)
  1948 done
  1949 
  1950 lemma takeWhile_cong [fundef_cong, recdef_cong]:
  1951   "[| l = k; !!x. x : set l ==> P x = Q x |] 
  1952   ==> takeWhile P l = takeWhile Q k"
  1953 by (induct k arbitrary: l) (simp_all)
  1954 
  1955 lemma dropWhile_cong [fundef_cong, recdef_cong]:
  1956   "[| l = k; !!x. x : set l ==> P x = Q x |] 
  1957   ==> dropWhile P l = dropWhile Q k"
  1958 by (induct k arbitrary: l, simp_all)
  1959 
  1960 
  1961 subsubsection {* @{text zip} *}
  1962 
  1963 lemma zip_Nil [simp]: "zip [] ys = []"
  1964 by (induct ys) auto
  1965 
  1966 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
  1967 by simp
  1968 
  1969 declare zip_Cons [simp del]
  1970 
  1971 lemma [code]:
  1972   "zip [] ys = []"
  1973   "zip xs [] = []"
  1974   "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
  1975   by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+
  1976 
  1977 lemma zip_Cons1:
  1978  "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
  1979 by(auto split:list.split)
  1980 
  1981 lemma length_zip [simp]:
  1982 "length (zip xs ys) = min (length xs) (length ys)"
  1983 by (induct xs ys rule:list_induct2') auto
  1984 
  1985 lemma zip_obtain_same_length:
  1986   assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys)
  1987     \<Longrightarrow> zs = take n xs \<Longrightarrow> ws = take n ys \<Longrightarrow> P (zip zs ws)"
  1988   shows "P (zip xs ys)"
  1989 proof -
  1990   let ?n = "min (length xs) (length ys)"
  1991   have "P (zip (take ?n xs) (take ?n ys))"
  1992     by (rule assms) simp_all
  1993   moreover have "zip xs ys = zip (take ?n xs) (take ?n ys)"
  1994   proof (induct xs arbitrary: ys)
  1995     case Nil then show ?case by simp
  1996   next
  1997     case (Cons x xs) then show ?case by (cases ys) simp_all
  1998   qed
  1999   ultimately show ?thesis by simp
  2000 qed
  2001 
  2002 lemma zip_append1:
  2003 "zip (xs @ ys) zs =
  2004 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
  2005 by (induct xs zs rule:list_induct2') auto
  2006 
  2007 lemma zip_append2:
  2008 "zip xs (ys @ zs) =
  2009 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
  2010 by (induct xs ys rule:list_induct2') auto
  2011 
  2012 lemma zip_append [simp]:
  2013  "[| length xs = length us; length ys = length vs |] ==>
  2014 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
  2015 by (simp add: zip_append1)
  2016 
  2017 lemma zip_rev:
  2018 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
  2019 by (induct rule:list_induct2, simp_all)
  2020 
  2021 lemma zip_map_map:
  2022   "zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"
  2023 proof (induct xs arbitrary: ys)
  2024   case (Cons x xs) note Cons_x_xs = Cons.hyps
  2025   show ?case
  2026   proof (cases ys)
  2027     case (Cons y ys')
  2028     show ?thesis unfolding Cons using Cons_x_xs by simp
  2029   qed simp
  2030 qed simp
  2031 
  2032 lemma zip_map1:
  2033   "zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"
  2034 using zip_map_map[of f xs "\<lambda>x. x" ys] by simp
  2035 
  2036 lemma zip_map2:
  2037   "zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"
  2038 using zip_map_map[of "\<lambda>x. x" xs f ys] by simp
  2039 
  2040 lemma map_zip_map:
  2041   "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
  2042 unfolding zip_map1 by auto
  2043 
  2044 lemma map_zip_map2:
  2045   "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
  2046 unfolding zip_map2 by auto
  2047 
  2048 text{* Courtesy of Andreas Lochbihler: *}
  2049 lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
  2050 by(induct xs) auto
  2051 
  2052 lemma nth_zip [simp]:
  2053 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
  2054 apply (induct ys arbitrary: i xs, simp)
  2055 apply (case_tac xs)
  2056  apply (simp_all add: nth.simps split: nat.split)
  2057 done
  2058 
  2059 lemma set_zip:
  2060 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
  2061 by(simp add: set_conv_nth cong: rev_conj_cong)
  2062 
  2063 lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"
  2064 by(induct xs) auto
  2065 
  2066 lemma zip_update:
  2067   "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
  2068 by(rule sym, simp add: update_zip)
  2069 
  2070 lemma zip_replicate [simp]:
  2071   "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
  2072 apply (induct i arbitrary: j, auto)
  2073 apply (case_tac j, auto)
  2074 done
  2075 
  2076 lemma take_zip:
  2077   "take n (zip xs ys) = zip (take n xs) (take n ys)"
  2078 apply (induct n arbitrary: xs ys)
  2079  apply simp
  2080 apply (case_tac xs, simp)
  2081 apply (case_tac ys, simp_all)
  2082 done
  2083 
  2084 lemma drop_zip:
  2085   "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
  2086 apply (induct n arbitrary: xs ys)
  2087  apply simp
  2088 apply (case_tac xs, simp)
  2089 apply (case_tac ys, simp_all)
  2090 done
  2091 
  2092 lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"
  2093 proof (induct xs arbitrary: ys)
  2094   case (Cons x xs) thus ?case by (cases ys) auto
  2095 qed simp
  2096 
  2097 lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \<circ> snd) (zip xs ys)"
  2098 proof (induct xs arbitrary: ys)
  2099   case (Cons x xs) thus ?case by (cases ys) auto
  2100 qed simp
  2101 
  2102 lemma set_zip_leftD:
  2103   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
  2104 by (induct xs ys rule:list_induct2') auto
  2105 
  2106 lemma set_zip_rightD:
  2107   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
  2108 by (induct xs ys rule:list_induct2') auto
  2109 
  2110 lemma in_set_zipE:
  2111   "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
  2112 by(blast dest: set_zip_leftD set_zip_rightD)
  2113 
  2114 lemma zip_map_fst_snd:
  2115   "zip (map fst zs) (map snd zs) = zs"
  2116   by (induct zs) simp_all
  2117 
  2118 lemma zip_eq_conv:
  2119   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
  2120   by (auto simp add: zip_map_fst_snd)
  2121 
  2122 lemma distinct_zipI1:
  2123   "distinct xs \<Longrightarrow> distinct (zip xs ys)"
  2124 proof (induct xs arbitrary: ys)
  2125   case (Cons x xs)
  2126   show ?case
  2127   proof (cases ys)
  2128     case (Cons y ys')
  2129     have "(x, y) \<notin> set (zip xs ys')"
  2130       using Cons.prems by (auto simp: set_zip)
  2131     thus ?thesis
  2132       unfolding Cons zip_Cons_Cons distinct.simps
  2133       using Cons.hyps Cons.prems by simp
  2134   qed simp
  2135 qed simp
  2136 
  2137 lemma distinct_zipI2:
  2138   "distinct xs \<Longrightarrow> distinct (zip xs ys)"
  2139 proof (induct xs arbitrary: ys)
  2140   case (Cons x xs)
  2141   show ?case
  2142   proof (cases ys)
  2143     case (Cons y ys')
  2144      have "(x, y) \<notin> set (zip xs ys')"
  2145       using Cons.prems by (auto simp: set_zip)
  2146     thus ?thesis
  2147       unfolding Cons zip_Cons_Cons distinct.simps
  2148       using Cons.hyps Cons.prems by simp
  2149   qed simp
  2150 qed simp
  2151 
  2152 
  2153 subsubsection {* @{text list_all2} *}
  2154 
  2155 lemma list_all2_lengthD [intro?]: 
  2156   "list_all2 P xs ys ==> length xs = length ys"
  2157 by (simp add: list_all2_def)
  2158 
  2159 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
  2160 by (simp add: list_all2_def)
  2161 
  2162 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
  2163 by (simp add: list_all2_def)
  2164 
  2165 lemma list_all2_Cons [iff, code]:
  2166   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
  2167 by (auto simp add: list_all2_def)
  2168 
  2169 lemma list_all2_Cons1:
  2170 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
  2171 by (cases ys) auto
  2172 
  2173 lemma list_all2_Cons2:
  2174 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
  2175 by (cases xs) auto
  2176 
  2177 lemma list_all2_rev [iff]:
  2178 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
  2179 by (simp add: list_all2_def zip_rev cong: conj_cong)
  2180 
  2181 lemma list_all2_rev1:
  2182 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
  2183 by (subst list_all2_rev [symmetric]) simp
  2184 
  2185 lemma list_all2_append1:
  2186 "list_all2 P (xs @ ys) zs =
  2187 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
  2188 list_all2 P xs us \<and> list_all2 P ys vs)"
  2189 apply (simp add: list_all2_def zip_append1)
  2190 apply (rule iffI)
  2191  apply (rule_tac x = "take (length xs) zs" in exI)
  2192  apply (rule_tac x = "drop (length xs) zs" in exI)
  2193  apply (force split: nat_diff_split simp add: min_def, clarify)
  2194 apply (simp add: ball_Un)
  2195 done
  2196 
  2197 lemma list_all2_append2:
  2198 "list_all2 P xs (ys @ zs) =
  2199 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
  2200 list_all2 P us ys \<and> list_all2 P vs zs)"
  2201 apply (simp add: list_all2_def zip_append2)
  2202 apply (rule iffI)
  2203  apply (rule_tac x = "take (length ys) xs" in exI)
  2204  apply (rule_tac x = "drop (length ys) xs" in exI)
  2205  apply (force split: nat_diff_split simp add: min_def, clarify)
  2206 apply (simp add: ball_Un)
  2207 done
  2208 
  2209 lemma list_all2_append:
  2210   "length xs = length ys \<Longrightarrow>
  2211   list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
  2212 by (induct rule:list_induct2, simp_all)
  2213 
  2214 lemma list_all2_appendI [intro?, trans]:
  2215   "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
  2216 by (simp add: list_all2_append list_all2_lengthD)
  2217 
  2218 lemma list_all2_conv_all_nth:
  2219 "list_all2 P xs ys =
  2220 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
  2221 by (force simp add: list_all2_def set_zip)
  2222 
  2223 lemma list_all2_trans:
  2224   assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
  2225   shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
  2226         (is "!!bs cs. PROP ?Q as bs cs")
  2227 proof (induct as)
  2228   fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
  2229   show "!!cs. PROP ?Q (x # xs) bs cs"
  2230   proof (induct bs)
  2231     fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
  2232     show "PROP ?Q (x # xs) (y # ys) cs"
  2233       by (induct cs) (auto intro: tr I1 I2)
  2234   qed simp
  2235 qed simp
  2236 
  2237 lemma list_all2_all_nthI [intro?]:
  2238   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
  2239 by (simp add: list_all2_conv_all_nth)
  2240 
  2241 lemma list_all2I:
  2242   "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
  2243 by (simp add: list_all2_def)
  2244 
  2245 lemma list_all2_nthD:
  2246   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
  2247 by (simp add: list_all2_conv_all_nth)
  2248 
  2249 lemma list_all2_nthD2:
  2250   "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
  2251 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
  2252 
  2253 lemma list_all2_map1: 
  2254   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
  2255 by (simp add: list_all2_conv_all_nth)
  2256 
  2257 lemma list_all2_map2: 
  2258   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
  2259 by (auto simp add: list_all2_conv_all_nth)
  2260 
  2261 lemma list_all2_refl [intro?]:
  2262   "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
  2263 by (simp add: list_all2_conv_all_nth)
  2264 
  2265 lemma list_all2_update_cong:
  2266   "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  2267 by (simp add: list_all2_conv_all_nth nth_list_update)
  2268 
  2269 lemma list_all2_update_cong2:
  2270   "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  2271 by (simp add: list_all2_lengthD list_all2_update_cong)
  2272 
  2273 lemma list_all2_takeI [simp,intro?]:
  2274   "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
  2275 apply (induct xs arbitrary: n ys)
  2276  apply simp
  2277 apply (clarsimp simp add: list_all2_Cons1)
  2278 apply (case_tac n)
  2279 apply auto
  2280 done
  2281 
  2282 lemma list_all2_dropI [simp,intro?]:
  2283   "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
  2284 apply (induct as arbitrary: n bs, simp)
  2285 apply (clarsimp simp add: list_all2_Cons1)
  2286 apply (case_tac n, simp, simp)
  2287 done
  2288 
  2289 lemma list_all2_mono [intro?]:
  2290   "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
  2291 apply (induct xs arbitrary: ys, simp)
  2292 apply (case_tac ys, auto)
  2293 done
  2294 
  2295 lemma list_all2_eq:
  2296   "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
  2297 by (induct xs ys rule: list_induct2') auto
  2298 
  2299 
  2300 subsubsection {* @{text foldl} and @{text foldr} *}
  2301 
  2302 lemma foldl_append [simp]:
  2303   "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
  2304 by (induct xs arbitrary: a) auto
  2305 
  2306 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
  2307 by (induct xs) auto
  2308 
  2309 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
  2310 by(induct xs) simp_all
  2311 
  2312 text{* For efficient code generation: avoid intermediate list. *}
  2313 lemma foldl_map[code_unfold]:
  2314   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
  2315 by(induct xs arbitrary:a) simp_all
  2316 
  2317 lemma foldl_apply:
  2318   assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"
  2319   shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"
  2320   by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq)
  2321 
  2322 lemma foldl_cong [fundef_cong, recdef_cong]:
  2323   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
  2324   ==> foldl f a l = foldl g b k"
  2325 by (induct k arbitrary: a b l) simp_all
  2326 
  2327 lemma foldr_cong [fundef_cong, recdef_cong]:
  2328   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
  2329   ==> foldr f l a = foldr g k b"
  2330 by (induct k arbitrary: a b l) simp_all
  2331 
  2332 lemma foldl_fun_comm:
  2333   assumes "\<And>x y s. f (f s x) y = f (f s y) x"
  2334   shows "f (foldl f s xs) x = foldl f (f s x) xs"
  2335   by (induct xs arbitrary: s)
  2336     (simp_all add: assms)
  2337 
  2338 lemma (in semigroup_add) foldl_assoc:
  2339 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
  2340 by (induct zs arbitrary: y) (simp_all add:add_assoc)
  2341 
  2342 lemma (in monoid_add) foldl_absorb0:
  2343 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
  2344 by (induct zs) (simp_all add:foldl_assoc)
  2345 
  2346 lemma foldl_rev:
  2347   assumes "\<And>x y s. f (f s x) y = f (f s y) x"
  2348   shows "foldl f s (rev xs) = foldl f s xs"
  2349 proof (induct xs arbitrary: s)
  2350   case Nil then show ?case by simp
  2351 next
  2352   case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)
  2353 qed
  2354 
  2355 lemma rev_foldl_cons [code]:
  2356   "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
  2357 proof (induct xs)
  2358   case Nil then show ?case by simp
  2359 next
  2360   case Cons
  2361   {
  2362     fix x xs ys
  2363     have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
  2364       = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
  2365     by (induct xs arbitrary: ys) auto
  2366   }
  2367   note aux = this
  2368   show ?case by (induct xs) (auto simp add: Cons aux)
  2369 qed
  2370 
  2371 
  2372 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
  2373 
  2374 lemma foldl_foldr1_lemma:
  2375  "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
  2376 by (induct xs arbitrary: a) (auto simp:add_assoc)
  2377 
  2378 corollary foldl_foldr1:
  2379  "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
  2380 by (simp add:foldl_foldr1_lemma)
  2381 
  2382 
  2383 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
  2384 
  2385 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
  2386 by (induct xs) auto
  2387 
  2388 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
  2389 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
  2390 
  2391 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
  2392   by (induct xs, auto simp add: foldl_assoc add_commute)
  2393 
  2394 text {*
  2395 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
  2396 difficult to use because it requires an additional transitivity step.
  2397 *}
  2398 
  2399 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
  2400 by (induct ns arbitrary: n) auto
  2401 
  2402 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
  2403 by (force intro: start_le_sum simp add: in_set_conv_decomp)
  2404 
  2405 lemma sum_eq_0_conv [iff]:
  2406   "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
  2407 by (induct ns arbitrary: m) auto
  2408 
  2409 lemma foldr_invariant: 
  2410   "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f x y) \<rbrakk> \<Longrightarrow> Q (foldr f xs x)"
  2411   by (induct xs, simp_all)
  2412 
  2413 lemma foldl_invariant: 
  2414   "\<lbrakk>Q x ; \<forall> x\<in> set xs. P x; \<forall> x y. P x \<and> Q y \<longrightarrow> Q (f y x) \<rbrakk> \<Longrightarrow> Q (foldl f x xs)"
  2415   by (induct xs arbitrary: x, simp_all)
  2416 
  2417 lemma foldl_weak_invariant:
  2418   assumes "P s"
  2419     and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)"
  2420   shows "P (foldl f s xs)"
  2421   using assms by (induct xs arbitrary: s) simp_all
  2422 
  2423 text {* @{const foldl} and @{const concat} *}
  2424 
  2425 lemma foldl_conv_concat:
  2426   "foldl (op @) xs xss = xs @ concat xss"
  2427 proof (induct xss arbitrary: xs)
  2428   case Nil show ?case by simp
  2429 next
  2430   interpret monoid_add "op @" "[]" proof qed simp_all
  2431   case Cons then show ?case by (simp add: foldl_absorb0)
  2432 qed
  2433 
  2434 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
  2435   by (simp add: foldl_conv_concat)
  2436 
  2437 text {* @{const Finite_Set.fold} and @{const foldl} *}
  2438 
  2439 lemma (in fun_left_comm) fold_set_remdups:
  2440   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"
  2441   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)
  2442 
  2443 lemma (in fun_left_comm_idem) fold_set:
  2444   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
  2445   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
  2446 
  2447 lemma (in ab_semigroup_idem_mult) fold1_set:
  2448   assumes "xs \<noteq> []"
  2449   shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"
  2450 proof -
  2451   interpret fun_left_comm_idem times by (fact fun_left_comm_idem)
  2452   from assms obtain y ys where xs: "xs = y # ys"
  2453     by (cases xs) auto
  2454   show ?thesis
  2455   proof (cases "set ys = {}")
  2456     case True with xs show ?thesis by simp
  2457   next
  2458     case False
  2459     then have "fold1 times (insert y (set ys)) = fold times y (set ys)"
  2460       by (simp only: finite_set fold1_eq_fold_idem)
  2461     with xs show ?thesis by (simp add: fold_set mult_commute)
  2462   qed
  2463 qed
  2464 
  2465 lemma (in lattice) Inf_fin_set_fold [code_unfold]:
  2466   "Inf_fin (set (x # xs)) = foldl inf x xs"
  2467 proof -
  2468   interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2469     by (fact ab_semigroup_idem_mult_inf)
  2470   show ?thesis
  2471     by (simp add: Inf_fin_def fold1_set del: set.simps)
  2472 qed
  2473 
  2474 lemma (in lattice) Sup_fin_set_fold [code_unfold]:
  2475   "Sup_fin (set (x # xs)) = foldl sup x xs"
  2476 proof -
  2477   interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2478     by (fact ab_semigroup_idem_mult_sup)
  2479   show ?thesis
  2480     by (simp add: Sup_fin_def fold1_set del: set.simps)
  2481 qed
  2482 
  2483 lemma (in linorder) Min_fin_set_fold [code_unfold]:
  2484   "Min (set (x # xs)) = foldl min x xs"
  2485 proof -
  2486   interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2487     by (fact ab_semigroup_idem_mult_min)
  2488   show ?thesis
  2489     by (simp add: Min_def fold1_set del: set.simps)
  2490 qed
  2491 
  2492 lemma (in linorder) Max_fin_set_fold [code_unfold]:
  2493   "Max (set (x # xs)) = foldl max x xs"
  2494 proof -
  2495   interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2496     by (fact ab_semigroup_idem_mult_max)
  2497   show ?thesis
  2498     by (simp add: Max_def fold1_set del: set.simps)
  2499 qed
  2500 
  2501 lemma (in complete_lattice) Inf_set_fold [code_unfold]:
  2502   "Inf (set xs) = foldl inf top xs"
  2503 proof -
  2504   interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2505     by (fact fun_left_comm_idem_inf)
  2506   show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)
  2507 qed
  2508 
  2509 lemma (in complete_lattice) Sup_set_fold [code_unfold]:
  2510   "Sup (set xs) = foldl sup bot xs"
  2511 proof -
  2512   interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"
  2513     by (fact fun_left_comm_idem_sup)
  2514   show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)
  2515 qed
  2516 
  2517 lemma (in complete_lattice) INFI_set_fold:
  2518   "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
  2519   unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
  2520     by (simp add: inf_commute)
  2521 
  2522 lemma (in complete_lattice) SUPR_set_fold:
  2523   "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
  2524   unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
  2525     by (simp add: sup_commute)
  2526 
  2527 
  2528 subsubsection {* @{text upt} *}
  2529 
  2530 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
  2531 -- {* simp does not terminate! *}
  2532 by (induct j) auto
  2533 
  2534 lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
  2535 
  2536 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
  2537 by (subst upt_rec) simp
  2538 
  2539 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
  2540 by(induct j)simp_all
  2541 
  2542 lemma upt_eq_Cons_conv:
  2543  "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
  2544 apply(induct j arbitrary: x xs)
  2545  apply simp
  2546 apply(clarsimp simp add: append_eq_Cons_conv)
  2547 apply arith
  2548 done
  2549 
  2550 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
  2551 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
  2552 by simp
  2553 
  2554 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
  2555   by (simp add: upt_rec)
  2556 
  2557 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
  2558 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
  2559 by (induct k) auto
  2560 
  2561 lemma length_upt [simp]: "length [i..<j] = j - i"
  2562 by (induct j) (auto simp add: Suc_diff_le)
  2563 
  2564 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
  2565 apply (induct j)
  2566 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
  2567 done
  2568 
  2569 
  2570 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
  2571 by(simp add:upt_conv_Cons)
  2572 
  2573 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
  2574 apply(cases j)
  2575  apply simp
  2576 by(simp add:upt_Suc_append)
  2577 
  2578 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
  2579 apply (induct m arbitrary: i, simp)
  2580 apply (subst upt_rec)
  2581 apply (rule sym)
  2582 apply (subst upt_rec)
  2583 apply (simp del: upt.simps)
  2584 done
  2585 
  2586 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
  2587 apply(induct j)
  2588 apply auto
  2589 done
  2590 
  2591 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
  2592 by (induct n) auto
  2593 
  2594 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
  2595 apply (induct n m  arbitrary: i rule: diff_induct)
  2596 prefer 3 apply (subst map_Suc_upt[symmetric])
  2597 apply (auto simp add: less_diff_conv nth_upt)
  2598 done
  2599 
  2600 lemma nth_take_lemma:
  2601   "k <= length xs ==> k <= length ys ==>
  2602      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
  2603 apply (atomize, induct k arbitrary: xs ys)
  2604 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
  2605 txt {* Both lists must be non-empty *}
  2606 apply (case_tac xs, simp)
  2607 apply (case_tac ys, clarify)
  2608  apply (simp (no_asm_use))
  2609 apply clarify
  2610 txt {* prenexing's needed, not miniscoping *}
  2611 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
  2612 apply blast
  2613 done
  2614 
  2615 lemma nth_equalityI:
  2616  "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
  2617 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
  2618 apply (simp_all add: take_all)
  2619 done
  2620 
  2621 lemma map_nth:
  2622   "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
  2623   by (rule nth_equalityI, auto)
  2624 
  2625 (* needs nth_equalityI *)
  2626 lemma list_all2_antisym:
  2627   "\<lbrakk> (\<And>x y. \<lbrakk>P x y; Q y x\<rbrakk> \<Longrightarrow> x = y); list_all2 P xs ys; list_all2 Q ys xs \<rbrakk> 
  2628   \<Longrightarrow> xs = ys"
  2629   apply (simp add: list_all2_conv_all_nth) 
  2630   apply (rule nth_equalityI, blast, simp)
  2631   done
  2632 
  2633 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
  2634 -- {* The famous take-lemma. *}
  2635 apply (drule_tac x = "max (length xs) (length ys)" in spec)
  2636 apply (simp add: le_max_iff_disj take_all)
  2637 done
  2638 
  2639 
  2640 lemma take_Cons':
  2641      "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
  2642 by (cases n) simp_all
  2643 
  2644 lemma drop_Cons':
  2645      "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
  2646 by (cases n) simp_all
  2647 
  2648 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
  2649 by (cases n) simp_all
  2650 
  2651 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
  2652 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
  2653 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
  2654 
  2655 declare take_Cons_number_of [simp] 
  2656         drop_Cons_number_of [simp] 
  2657         nth_Cons_number_of [simp] 
  2658 
  2659 
  2660 subsubsection {* @{text upto}: interval-list on @{typ int} *}
  2661 
  2662 (* FIXME make upto tail recursive? *)
  2663 
  2664 function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
  2665 "upto i j = (if i \<le> j then i # [i+1..j] else [])"
  2666 by auto
  2667 termination
  2668 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
  2669 
  2670 declare upto.simps[code, simp del]
  2671 
  2672 lemmas upto_rec_number_of[simp] =
  2673   upto.simps[of "number_of m" "number_of n", standard]
  2674 
  2675 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
  2676 by(simp add: upto.simps)
  2677 
  2678 lemma set_upto[simp]: "set[i..j] = {i..j}"
  2679 apply(induct i j rule:upto.induct)
  2680 apply(simp add: upto.simps simp_from_to)
  2681 done
  2682 
  2683 
  2684 subsubsection {* @{text "distinct"} and @{text remdups} *}
  2685 
  2686 lemma distinct_append [simp]:
  2687 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
  2688 by (induct xs) auto
  2689 
  2690 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
  2691 by(induct xs) auto
  2692 
  2693 lemma set_remdups [simp]: "set (remdups xs) = set xs"
  2694 by (induct xs) (auto simp add: insert_absorb)
  2695 
  2696 lemma distinct_remdups [iff]: "distinct (remdups xs)"
  2697 by (induct xs) auto
  2698 
  2699 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
  2700 by (induct xs, auto)
  2701 
  2702 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
  2703 by (metis distinct_remdups distinct_remdups_id)
  2704 
  2705 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
  2706 by (metis distinct_remdups finite_list set_remdups)
  2707 
  2708 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
  2709 by (induct x, auto) 
  2710 
  2711 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
  2712 by (induct x, auto)
  2713 
  2714 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
  2715 by (induct xs) auto
  2716 
  2717 lemma length_remdups_eq[iff]:
  2718   "(length (remdups xs) = length xs) = (remdups xs = xs)"
  2719 apply(induct xs)
  2720  apply auto
  2721 apply(subgoal_tac "length (remdups xs) <= length xs")
  2722  apply arith
  2723 apply(rule length_remdups_leq)
  2724 done
  2725 
  2726 lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
  2727 apply(induct xs)
  2728 apply auto
  2729 done
  2730 
  2731 lemma distinct_map:
  2732   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
  2733 by (induct xs) auto
  2734 
  2735 
  2736 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
  2737 by (induct xs) auto
  2738 
  2739 lemma distinct_upt[simp]: "distinct[i..<j]"
  2740 by (induct j) auto
  2741 
  2742 lemma distinct_upto[simp]: "distinct[i..j]"
  2743 apply(induct i j rule:upto.induct)
  2744 apply(subst upto.simps)
  2745 apply(simp)
  2746 done
  2747 
  2748 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
  2749 apply(induct xs arbitrary: i)
  2750  apply simp
  2751 apply (case_tac i)
  2752  apply simp_all
  2753 apply(blast dest:in_set_takeD)
  2754 done
  2755 
  2756 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
  2757 apply(induct xs arbitrary: i)
  2758  apply simp
  2759 apply (case_tac i)
  2760  apply simp_all
  2761 done
  2762 
  2763 lemma distinct_list_update:
  2764 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
  2765 shows "distinct (xs[i:=a])"
  2766 proof (cases "i < length xs")
  2767   case True
  2768   with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
  2769     apply (drule_tac id_take_nth_drop) by simp
  2770   with d True show ?thesis
  2771     apply (simp add: upd_conv_take_nth_drop)
  2772     apply (drule subst [OF id_take_nth_drop]) apply assumption
  2773     apply simp apply (cases "a = xs!i") apply simp by blast
  2774 next
  2775   case False with d show ?thesis by auto
  2776 qed
  2777 
  2778 lemma distinct_concat:
  2779   assumes "distinct xs"
  2780   and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"
  2781   and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"
  2782   shows "distinct (concat xs)"
  2783   using assms by (induct xs) auto
  2784 
  2785 text {* It is best to avoid this indexed version of distinct, but
  2786 sometimes it is useful. *}
  2787 
  2788 lemma distinct_conv_nth:
  2789 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
  2790 apply (induct xs, simp, simp)
  2791 apply (rule iffI, clarsimp)
  2792  apply (case_tac i)
  2793 apply (case_tac j, simp)
  2794 apply (simp add: set_conv_nth)
  2795  apply (case_tac j)
  2796 apply (clarsimp simp add: set_conv_nth, simp) 
  2797 apply (rule conjI)
  2798 (*TOO SLOW
  2799 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2800 *)
  2801  apply (clarsimp simp add: set_conv_nth)
  2802  apply (erule_tac x = 0 in allE, simp)
  2803  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
  2804 (*TOO SLOW
  2805 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
  2806 *)
  2807 apply (erule_tac x = "Suc i" in allE, simp)
  2808 apply (erule_tac x = "Suc j" in allE, simp)
  2809 done
  2810 
  2811 lemma nth_eq_iff_index_eq:
  2812  "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
  2813 by(auto simp: distinct_conv_nth)
  2814 
  2815 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
  2816 by (induct xs) auto
  2817 
  2818 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
  2819 proof (induct xs)
  2820   case Nil thus ?case by simp
  2821 next
  2822   case (Cons x xs)
  2823   show ?case
  2824   proof (cases "x \<in> set xs")
  2825     case False with Cons show ?thesis by simp
  2826   next
  2827     case True with Cons.prems
  2828     have "card (set xs) = Suc (length xs)" 
  2829       by (simp add: card_insert_if split: split_if_asm)
  2830     moreover have "card (set xs) \<le> length xs" by (rule card_length)
  2831     ultimately have False by simp
  2832     thus ?thesis ..
  2833   qed
  2834 qed
  2835 
  2836 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
  2837 apply (induct n == "length ws" arbitrary:ws) apply simp
  2838 apply(case_tac ws) apply simp
  2839 apply (simp split:split_if_asm)
  2840 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
  2841 done
  2842 
  2843 lemma length_remdups_concat:
  2844  "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
  2845 by(simp add: set_concat distinct_card[symmetric])
  2846 
  2847 lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"
  2848 proof -
  2849   have xs: "concat[xs] = xs" by simp
  2850   from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp
  2851 qed
  2852 
  2853 lemma remdups_remdups:
  2854   "remdups (remdups xs) = remdups xs"
  2855   by (induct xs) simp_all
  2856 
  2857 lemma distinct_butlast:
  2858   assumes "xs \<noteq> []" and "distinct xs"
  2859   shows "distinct (butlast xs)"
  2860 proof -
  2861   from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
  2862   with `distinct xs` show ?thesis by simp
  2863 qed
  2864 
  2865 
  2866 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
  2867 
  2868 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
  2869 by (induct xs) (simp_all add:add_assoc)
  2870 
  2871 lemma listsum_rev [simp]:
  2872   fixes xs :: "'a\<Colon>comm_monoid_add list"
  2873   shows "listsum (rev xs) = listsum xs"
  2874 by (induct xs) (simp_all add:add_ac)
  2875 
  2876 lemma listsum_map_remove1:
  2877 fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
  2878 shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
  2879 by (induct xs)(auto simp add:add_ac)
  2880 
  2881 lemma list_size_conv_listsum:
  2882   "list_size f xs = listsum (map f xs) + size xs"
  2883 by(induct xs) auto
  2884 
  2885 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
  2886 by (induct xs) auto
  2887 
  2888 lemma length_concat: "length (concat xss) = listsum (map length xss)"
  2889 by (induct xss) simp_all
  2890 
  2891 lemma listsum_map_filter:
  2892   fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"
  2893   assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"
  2894   shows "listsum (map f (filter P xs)) = listsum (map f xs)"
  2895 using assms by (induct xs) auto
  2896 
  2897 text{* For efficient code generation ---
  2898        @{const listsum} is not tail recursive but @{const foldl} is. *}
  2899 lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
  2900 by(simp add:listsum_foldr foldl_foldr1)
  2901 
  2902 lemma distinct_listsum_conv_Setsum:
  2903   "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
  2904 by (induct xs) simp_all
  2905 
  2906 lemma listsum_eq_0_nat_iff_nat[simp]:
  2907   "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"
  2908 by(simp add: listsum)
  2909 
  2910 lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"
  2911 apply(induct ns arbitrary: k)
  2912  apply simp
  2913 apply(fastsimp simp add:nth_Cons split: nat.split)
  2914 done
  2915 
  2916 lemma listsum_update_nat: "k<size ns \<Longrightarrow>
  2917   listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"
  2918 apply(induct ns arbitrary:k)
  2919  apply (auto split:nat.split)
  2920 apply(drule elem_le_listsum_nat)
  2921 apply arith
  2922 done
  2923 
  2924 text{* Some syntactic sugar for summing a function over a list: *}
  2925 
  2926 syntax
  2927   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
  2928 syntax (xsymbols)
  2929   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2930 syntax (HTML output)
  2931   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2932 
  2933 translations -- {* Beware of argument permutation! *}
  2934   "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
  2935   "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
  2936 
  2937 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
  2938   by (induct xs) (simp_all add: left_distrib)
  2939 
  2940 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
  2941   by (induct xs) (simp_all add: left_distrib)
  2942 
  2943 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
  2944 lemma uminus_listsum_map:
  2945   fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
  2946   shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
  2947 by (induct xs) simp_all
  2948 
  2949 lemma listsum_addf:
  2950   fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
  2951   shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
  2952 by (induct xs) (simp_all add: algebra_simps)
  2953 
  2954 lemma listsum_subtractf:
  2955   fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
  2956   shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
  2957 by (induct xs) simp_all
  2958 
  2959 lemma listsum_const_mult:
  2960   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
  2961   shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
  2962 by (induct xs, simp_all add: algebra_simps)
  2963 
  2964 lemma listsum_mult_const:
  2965   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
  2966   shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
  2967 by (induct xs, simp_all add: algebra_simps)
  2968 
  2969 lemma listsum_abs:
  2970   fixes xs :: "'a::ordered_ab_group_add_abs list"
  2971   shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
  2972 by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
  2973 
  2974 lemma listsum_mono:
  2975   fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"
  2976   shows "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sum>x\<leftarrow>xs. f x) \<le> (\<Sum>x\<leftarrow>xs. g x)"
  2977 by (induct xs, simp, simp add: add_mono)
  2978 
  2979 lemma listsum_distinct_conv_setsum_set:
  2980   "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
  2981   by (induct xs) simp_all
  2982 
  2983 lemma interv_listsum_conv_setsum_set_nat:
  2984   "listsum (map f [m..<n]) = setsum f (set [m..<n])"
  2985   by (simp add: listsum_distinct_conv_setsum_set)
  2986 
  2987 lemma interv_listsum_conv_setsum_set_int:
  2988   "listsum (map f [k..l]) = setsum f (set [k..l])"
  2989   by (simp add: listsum_distinct_conv_setsum_set)
  2990 
  2991 text {* General equivalence between @{const listsum} and @{const setsum} *}
  2992 lemma listsum_setsum_nth:
  2993   "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
  2994   using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
  2995 
  2996 
  2997 subsubsection {* @{const insert} *}
  2998 
  2999 lemma in_set_insert [simp]:
  3000   "x \<in> set xs \<Longrightarrow> List.insert x xs = xs"
  3001   by (simp add: List.insert_def)
  3002 
  3003 lemma not_in_set_insert [simp]:
  3004   "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs"
  3005   by (simp add: List.insert_def)
  3006 
  3007 lemma insert_Nil [simp]:
  3008   "List.insert x [] = [x]"
  3009   by simp
  3010 
  3011 lemma set_insert [simp]:
  3012   "set (List.insert x xs) = insert x (set xs)"
  3013   by (auto simp add: List.insert_def)
  3014 
  3015 lemma distinct_insert [simp]:
  3016   "distinct xs \<Longrightarrow> distinct (List.insert x xs)"
  3017   by (simp add: List.insert_def)
  3018 
  3019 lemma insert_remdups:
  3020   "List.insert x (remdups xs) = remdups (List.insert x xs)"
  3021   by (simp add: List.insert_def)
  3022 
  3023 lemma distinct_induct [consumes 1, case_names Nil insert]:
  3024   assumes "distinct xs"
  3025   assumes "P []"
  3026   assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs
  3027     \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"
  3028   shows "P xs"
  3029 using `distinct xs` proof (induct xs)
  3030   case Nil from `P []` show ?case .
  3031 next
  3032   case (Cons x xs)
  3033   then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all
  3034   with insert have "P (List.insert x xs)" .
  3035   with `x \<notin> set xs` show ?case by simp
  3036 qed
  3037 
  3038 
  3039 subsubsection {* @{text remove1} *}
  3040 
  3041 lemma remove1_append:
  3042   "remove1 x (xs @ ys) =
  3043   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
  3044 by (induct xs) auto
  3045 
  3046 lemma remove1_commute: "remove1 x (remove1 y zs) = remove1 y (remove1 x zs)"
  3047 by (induct zs) auto
  3048 
  3049 lemma in_set_remove1[simp]:
  3050   "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
  3051 apply (induct xs)
  3052 apply auto
  3053 done
  3054 
  3055 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
  3056 apply(induct xs)
  3057  apply simp
  3058 apply simp
  3059 apply blast
  3060 done
  3061 
  3062 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
  3063 apply(induct xs)
  3064  apply simp
  3065 apply simp
  3066 apply blast
  3067 done
  3068 
  3069 lemma length_remove1:
  3070   "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
  3071 apply (induct xs)
  3072  apply (auto dest!:length_pos_if_in_set)
  3073 done
  3074 
  3075 lemma remove1_filter_not[simp]:
  3076   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
  3077 by(induct xs) auto
  3078 
  3079 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
  3080 apply(insert set_remove1_subset)
  3081 apply fast
  3082 done
  3083 
  3084 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
  3085 by (induct xs) simp_all
  3086 
  3087 lemma remove1_remdups:
  3088   "distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
  3089   by (induct xs) simp_all
  3090 
  3091 lemma remove1_idem:
  3092   assumes "x \<notin> set xs"
  3093   shows "remove1 x xs = xs"
  3094   using assms by (induct xs) simp_all
  3095 
  3096 
  3097 subsubsection {* @{text removeAll} *}
  3098 
  3099 lemma removeAll_filter_not_eq:
  3100   "removeAll x = filter (\<lambda>y. x \<noteq> y)"
  3101 proof
  3102   fix xs
  3103   show "removeAll x xs = filter (\<lambda>y. x \<noteq> y) xs"
  3104     by (induct xs) auto
  3105 qed
  3106 
  3107 lemma removeAll_append[simp]:
  3108   "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
  3109 by (induct xs) auto
  3110 
  3111 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
  3112 by (induct xs) auto
  3113 
  3114 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
  3115 by (induct xs) auto
  3116 
  3117 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
  3118 lemma length_removeAll:
  3119   "length(removeAll x xs) = length xs - count x xs"
  3120 *)
  3121 
  3122 lemma removeAll_filter_not[simp]:
  3123   "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
  3124 by(induct xs) auto
  3125 
  3126 lemma distinct_removeAll:
  3127   "distinct xs \<Longrightarrow> distinct (removeAll x xs)"
  3128   by (simp add: removeAll_filter_not_eq)
  3129 
  3130 lemma distinct_remove1_removeAll:
  3131   "distinct xs ==> remove1 x xs = removeAll x xs"
  3132 by (induct xs) simp_all
  3133 
  3134 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
  3135   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  3136 by (induct xs) (simp_all add:inj_on_def)
  3137 
  3138 lemma map_removeAll_inj: "inj f \<Longrightarrow>
  3139   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  3140 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
  3141 
  3142 
  3143 subsubsection {* @{text replicate} *}
  3144 
  3145 lemma length_replicate [simp]: "length (replicate n x) = n"
  3146 by (induct n) auto
  3147 
  3148 lemma Ex_list_of_length: "\<exists>xs. length xs = n"
  3149 by (rule exI[of _ "replicate n undefined"]) simp
  3150 
  3151 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
  3152 by (induct n) auto
  3153 
  3154 lemma map_replicate_const:
  3155   "map (\<lambda> x. k) lst = replicate (length lst) k"
  3156   by (induct lst) auto
  3157 
  3158 lemma replicate_app_Cons_same:
  3159 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
  3160 by (induct n) auto
  3161 
  3162 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
  3163 apply (induct n, simp)
  3164 apply (simp add: replicate_app_Cons_same)
  3165 done
  3166 
  3167 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
  3168 by (induct n) auto
  3169 
  3170 text{* Courtesy of Matthias Daum: *}
  3171 lemma append_replicate_commute:
  3172   "replicate n x @ replicate k x = replicate k x @ replicate n x"
  3173 apply (simp add: replicate_add [THEN sym])
  3174 apply (simp add: add_commute)
  3175 done
  3176 
  3177 text{* Courtesy of Andreas Lochbihler: *}
  3178 lemma filter_replicate:
  3179   "filter P (replicate n x) = (if P x then replicate n x else [])"
  3180 by(induct n) auto
  3181 
  3182 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
  3183 by (induct n) auto
  3184 
  3185 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
  3186 by (induct n) auto
  3187 
  3188 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
  3189 by (atomize (full), induct n) auto
  3190 
  3191 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
  3192 apply (induct n arbitrary: i, simp)
  3193 apply (simp add: nth_Cons split: nat.split)
  3194 done
  3195 
  3196 text{* Courtesy of Matthias Daum (2 lemmas): *}
  3197 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
  3198 apply (case_tac "k \<le> i")
  3199  apply  (simp add: min_def)
  3200 apply (drule not_leE)
  3201 apply (simp add: min_def)
  3202 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
  3203  apply  simp
  3204 apply (simp add: replicate_add [symmetric])
  3205 done
  3206 
  3207 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
  3208 apply (induct k arbitrary: i)
  3209  apply simp
  3210 apply clarsimp
  3211 apply (case_tac i)
  3212  apply simp
  3213 apply clarsimp
  3214 done
  3215 
  3216 
  3217 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
  3218 by (induct n) auto
  3219 
  3220 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
  3221 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
  3222 
  3223 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
  3224 by auto
  3225 
  3226 lemma in_set_replicate[simp]: "(x : set (replicate n y)) = (x = y & n \<noteq> 0)"
  3227 by (simp add: set_replicate_conv_if)
  3228 
  3229 lemma Ball_set_replicate[simp]:
  3230   "(ALL x : set(replicate n a). P x) = (P a | n=0)"
  3231 by(simp add: set_replicate_conv_if)
  3232 
  3233 lemma Bex_set_replicate[simp]:
  3234   "(EX x : set(replicate n a). P x) = (P a & n\<noteq>0)"
  3235 by(simp add: set_replicate_conv_if)
  3236 
  3237 lemma replicate_append_same:
  3238   "replicate i x @ [x] = x # replicate i x"
  3239   by (induct i) simp_all
  3240 
  3241 lemma map_replicate_trivial:
  3242   "map (\<lambda>i. x) [0..<i] = replicate i x"
  3243   by (induct i) (simp_all add: replicate_append_same)
  3244 
  3245 lemma concat_replicate_trivial[simp]:
  3246   "concat (replicate i []) = []"
  3247   by (induct i) (auto simp add: map_replicate_const)
  3248 
  3249 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
  3250 by (induct n) auto
  3251 
  3252 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
  3253 by (induct n) auto
  3254 
  3255 lemma replicate_eq_replicate[simp]:
  3256   "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
  3257 apply(induct m arbitrary: n)
  3258  apply simp
  3259 apply(induct_tac n)
  3260 apply auto
  3261 done
  3262 
  3263 
  3264 subsubsection{*@{text rotate1} and @{text rotate}*}
  3265 
  3266 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
  3267 by(simp add:rotate1_def)
  3268 
  3269 lemma rotate0[simp]: "rotate 0 = id"
  3270 by(simp add:rotate_def)
  3271 
  3272 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
  3273 by(simp add:rotate_def)
  3274 
  3275 lemma rotate_add:
  3276   "rotate (m+n) = rotate m o rotate n"
  3277 by(simp add:rotate_def funpow_add)
  3278 
  3279 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
  3280 by(simp add:rotate_add)
  3281 
  3282 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
  3283 by(simp add:rotate_def funpow_swap1)
  3284 
  3285 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
  3286 by(cases xs) simp_all
  3287 
  3288 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
  3289 apply(induct n)
  3290  apply simp
  3291 apply (simp add:rotate_def)
  3292 done
  3293 
  3294 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
  3295 by(simp add:rotate1_def split:list.split)
  3296 
  3297 lemma rotate_drop_take:
  3298   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
  3299 apply(induct n)
  3300  apply simp
  3301 apply(simp add:rotate_def)
  3302 apply(cases "xs = []")
  3303  apply (simp)
  3304 apply(case_tac "n mod length xs = 0")
  3305  apply(simp add:mod_Suc)
  3306  apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
  3307 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
  3308                 take_hd_drop linorder_not_le)
  3309 done
  3310 
  3311 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
  3312 by(simp add:rotate_drop_take)
  3313 
  3314 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
  3315 by(simp add:rotate_drop_take)
  3316 
  3317 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
  3318 by(simp add:rotate1_def split:list.split)
  3319 
  3320 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
  3321 by (induct n arbitrary: xs) (simp_all add:rotate_def)
  3322 
  3323 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
  3324 by(simp add:rotate1_def split:list.split) blast
  3325 
  3326 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
  3327 by (induct n) (simp_all add:rotate_def)
  3328 
  3329 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
  3330 by(simp add:rotate_drop_take take_map drop_map)
  3331 
  3332 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
  3333 by(simp add:rotate1_def split:list.split)
  3334 
  3335 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
  3336 by (induct n) (simp_all add:rotate_def)
  3337 
  3338 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
  3339 by(simp add:rotate1_def split:list.split)
  3340 
  3341 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
  3342 by (induct n) (simp_all add:rotate_def)
  3343 
  3344 lemma rotate_rev:
  3345   "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
  3346 apply(simp add:rotate_drop_take rev_drop rev_take)
  3347 apply(cases "length xs = 0")
  3348  apply simp
  3349 apply(cases "n mod length xs = 0")
  3350  apply simp
  3351 apply(simp add:rotate_drop_take rev_drop rev_take)
  3352 done
  3353 
  3354 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
  3355 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
  3356 apply(subgoal_tac "length xs \<noteq> 0")
  3357  prefer 2 apply simp
  3358 using mod_less_divisor[of "length xs" n] by arith
  3359 
  3360 
  3361 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
  3362 
  3363 lemma sublist_empty [simp]: "sublist xs {} = []"
  3364 by (auto simp add: sublist_def)
  3365 
  3366 lemma sublist_nil [simp]: "sublist [] A = []"
  3367 by (auto simp add: sublist_def)
  3368 
  3369 lemma length_sublist:
  3370   "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
  3371 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
  3372 
  3373 lemma sublist_shift_lemma_Suc:
  3374   "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
  3375    map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
  3376 apply(induct xs arbitrary: "is")
  3377  apply simp
  3378 apply (case_tac "is")
  3379  apply simp
  3380 apply simp
  3381 done
  3382 
  3383 lemma sublist_shift_lemma:
  3384      "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
  3385       map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
  3386 by (induct xs rule: rev_induct) (simp_all add: add_commute)
  3387 
  3388 lemma sublist_append:
  3389      "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
  3390 apply (unfold sublist_def)
  3391 apply (induct l' rule: rev_induct, simp)
  3392 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
  3393 apply (simp add: add_commute)
  3394 done
  3395 
  3396 lemma sublist_Cons:
  3397 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
  3398 apply (induct l rule: rev_induct)
  3399  apply (simp add: sublist_def)
  3400 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
  3401 done
  3402 
  3403 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
  3404 apply(induct xs arbitrary: I)
  3405 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  3406 done
  3407 
  3408 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
  3409 by(auto simp add:set_sublist)
  3410 
  3411 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
  3412 by(auto simp add:set_sublist)
  3413 
  3414 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
  3415 by(auto simp add:set_sublist)
  3416 
  3417 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
  3418 by (simp add: sublist_Cons)
  3419 
  3420 
  3421 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
  3422 apply(induct xs arbitrary: I)
  3423  apply simp
  3424 apply(auto simp add:sublist_Cons)
  3425 done
  3426 
  3427 
  3428 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
  3429 apply (induct l rule: rev_induct, simp)
  3430 apply (simp split: nat_diff_split add: sublist_append)
  3431 done
  3432 
  3433 lemma filter_in_sublist:
  3434  "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
  3435 proof (induct xs arbitrary: s)
  3436   case Nil thus ?case by simp
  3437 next
  3438   case (Cons a xs)
  3439   moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
  3440   ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
  3441 qed
  3442 
  3443 
  3444 subsubsection {* @{const splice} *}
  3445 
  3446 lemma splice_Nil2 [simp, code]:
  3447  "splice xs [] = xs"
  3448 by (cases xs) simp_all
  3449 
  3450 lemma splice_Cons_Cons [simp, code]:
  3451  "splice (x#xs) (y#ys) = x # y # splice xs ys"
  3452 by simp
  3453 
  3454 declare splice.simps(2) [simp del, code del]
  3455 
  3456 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  3457 apply(induct xs arbitrary: ys) apply simp
  3458 apply(case_tac ys)
  3459  apply auto
  3460 done
  3461 
  3462 
  3463 subsubsection {* Transpose *}
  3464 
  3465 function transpose where
  3466 "transpose []             = []" |
  3467 "transpose ([]     # xss) = transpose xss" |
  3468 "transpose ((x#xs) # xss) =
  3469   (x # [h. (h#t) \<leftarrow> xss]) # transpose (xs # [t. (h#t) \<leftarrow> xss])"
  3470 by pat_completeness auto
  3471 
  3472 lemma transpose_aux_filter_head:
  3473   "concat (map (list_case [] (\<lambda>h t. [h])) xss) =
  3474   map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
  3475   by (induct xss) (auto split: list.split)
  3476 
  3477 lemma transpose_aux_filter_tail:
  3478   "concat (map (list_case [] (\<lambda>h t. [t])) xss) =
  3479   map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
  3480   by (induct xss) (auto split: list.split)
  3481 
  3482 lemma transpose_aux_max:
  3483   "max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =
  3484   Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"
  3485   (is "max _ ?foldB = Suc (max _ ?foldA)")
  3486 proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")
  3487   case True
  3488   hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
  3489   proof (induct xss)
  3490     case (Cons x xs)
  3491     moreover hence "x = []" by (cases x) auto
  3492     ultimately show ?case by auto
  3493   qed simp
  3494   thus ?thesis using True by simp
  3495 next
  3496   case False
  3497 
  3498   have foldA: "?foldA = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"
  3499     by (induct xss) auto
  3500   have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"
  3501     by (induct xss) auto
  3502 
  3503   have "0 < ?foldB"
  3504   proof -
  3505     from False
  3506     obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)
  3507     hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto
  3508     hence "z \<noteq> []" by auto
  3509     thus ?thesis
  3510       unfolding foldB zs
  3511       by (auto simp: max_def intro: less_le_trans)
  3512   qed
  3513   thus ?thesis
  3514     unfolding foldA foldB max_Suc_Suc[symmetric]
  3515     by simp
  3516 qed
  3517 
  3518 termination transpose
  3519   by (relation "measure (\<lambda>xs. foldr (\<lambda>xs. max (length xs)) xs 0 + length xs)")
  3520      (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max less_Suc_eq_le)
  3521 
  3522 lemma transpose_empty: "(transpose xs = []) \<longleftrightarrow> (\<forall>x \<in> set xs. x = [])"
  3523   by (induct rule: transpose.induct) simp_all
  3524 
  3525 lemma length_transpose:
  3526   fixes xs :: "'a list list"
  3527   shows "length (transpose xs) = foldr (\<lambda>xs. max (length xs)) xs 0"
  3528   by (induct rule: transpose.induct)
  3529     (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max
  3530                 max_Suc_Suc[symmetric] simp del: max_Suc_Suc)
  3531 
  3532 lemma nth_transpose:
  3533   fixes xs :: "'a list list"
  3534   assumes "i < length (transpose xs)"
  3535   shows "transpose xs ! i = map (\<lambda>xs. xs ! i) [ys \<leftarrow> xs. i < length ys]"
  3536 using assms proof (induct arbitrary: i rule: transpose.induct)
  3537   case (3 x xs xss)
  3538   def XS == "(x # xs) # xss"
  3539   hence [simp]: "XS \<noteq> []" by auto
  3540   thus ?case
  3541   proof (cases i)
  3542     case 0
  3543     thus ?thesis by (simp add: transpose_aux_filter_head hd_conv_nth)
  3544   next
  3545     case (Suc j)
  3546     have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
  3547     have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
  3548     { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
  3549       by (cases x) simp_all
  3550     } note *** = this
  3551 
  3552     have j_less: "j < length (transpose (xs # concat (map (list_case [] (\<lambda>h t. [t])) xss)))"
  3553       using "3.prems" by (simp add: transpose_aux_filter_tail length_transpose Suc)
  3554 
  3555     show ?thesis
  3556       unfolding transpose.simps `i = Suc j` nth_Cons_Suc "3.hyps"[OF j_less]
  3557       apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
  3558       apply (rule_tac y=x in list.exhaust)
  3559       by auto
  3560   qed
  3561 qed simp_all
  3562 
  3563 lemma transpose_map_map:
  3564   "transpose (map (map f) xs) = map (map f) (transpose xs)"
  3565 proof (rule nth_equalityI, safe)
  3566   have [simp]: "length (transpose (map (map f) xs)) = length (transpose xs)"
  3567     by (simp add: length_transpose foldr_map comp_def)
  3568   show "length (transpose (map (map f) xs)) = length (map (map f) (transpose xs))" by simp
  3569 
  3570   fix i assume "i < length (transpose (map (map f) xs))"
  3571   thus "transpose (map (map f) xs) ! i = map (map f) (transpose xs) ! i"
  3572     by (simp add: nth_transpose filter_map comp_def)
  3573 qed
  3574 
  3575 
  3576 subsubsection {* (In)finiteness *}
  3577 
  3578 lemma finite_maxlen:
  3579   "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
  3580 proof (induct rule: finite.induct)
  3581   case emptyI show ?case by simp
  3582 next
  3583   case (insertI M xs)
  3584   then obtain n where "\<forall>s\<in>M. length s < n" by blast
  3585   hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
  3586   thus ?case ..
  3587 qed
  3588 
  3589 lemma finite_lists_length_eq:
  3590 assumes "finite A"
  3591 shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
  3592 proof(induct n)
  3593   case 0 show ?case by simp
  3594 next
  3595   case (Suc n)
  3596   have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
  3597     by (auto simp:length_Suc_conv)
  3598   then show ?case using `finite A`
  3599     by (auto intro: finite_imageI Suc) (* FIXME metis? *)
  3600 qed
  3601 
  3602 lemma finite_lists_length_le:
  3603   assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
  3604  (is "finite ?S")
  3605 proof-
  3606   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
  3607   thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
  3608 qed
  3609 
  3610 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
  3611 apply(rule notI)
  3612 apply(drule finite_maxlen)
  3613 apply (metis UNIV_I length_replicate less_not_refl)
  3614 done
  3615 
  3616 
  3617 subsection {* Sorting *}
  3618 
  3619 text{* Currently it is not shown that @{const sort} returns a
  3620 permutation of its input because the nicest proof is via multisets,
  3621 which are not yet available. Alternatively one could define a function
  3622 that counts the number of occurrences of an element in a list and use
  3623 that instead of multisets to state the correctness property. *}
  3624 
  3625 context linorder
  3626 begin
  3627 
  3628 lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"
  3629 by (induct xs, auto)
  3630 
  3631 lemma insort_left_comm:
  3632   "insort x (insort y xs) = insort y (insort x xs)"
  3633   by (induct xs) auto
  3634 
  3635 lemma fun_left_comm_insort:
  3636   "fun_left_comm insort"
  3637 proof
  3638 qed (fact insort_left_comm)
  3639 
  3640 lemma sort_key_simps [simp]:
  3641   "sort_key f [] = []"
  3642   "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
  3643   by (simp_all add: sort_key_def)
  3644 
  3645 lemma sort_foldl_insort:
  3646   "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
  3647   by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
  3648 
  3649 lemma length_sort[simp]: "length (sort_key f xs) = length xs"
  3650 by (induct xs, auto)
  3651 
  3652 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
  3653 apply(induct xs arbitrary: x) apply simp
  3654 by simp (blast intro: order_trans)
  3655 
  3656 lemma sorted_append:
  3657   "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
  3658 by (induct xs) (auto simp add:sorted_Cons)
  3659 
  3660 lemma sorted_nth_mono:
  3661   "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
  3662 by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
  3663 
  3664 lemma sorted_rev_nth_mono:
  3665   "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
  3666 using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
  3667       rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
  3668 by auto
  3669 
  3670 lemma sorted_nth_monoI:
  3671   "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
  3672 proof (induct xs)
  3673   case (Cons x xs)
  3674   have "sorted xs"
  3675   proof (rule Cons.hyps)
  3676     fix i j assume "i \<le> j" and "j < length xs"
  3677     with Cons.prems[of "Suc i" "Suc j"]
  3678     show "xs ! i \<le> xs ! j" by auto
  3679   qed
  3680   moreover
  3681   {
  3682     fix y assume "y \<in> set xs"
  3683     then obtain j where "j < length xs" and "xs ! j = y"
  3684       unfolding in_set_conv_nth by blast
  3685     with Cons.prems[of 0 "Suc j"]
  3686     have "x \<le> y"
  3687       by auto
  3688   }
  3689   ultimately
  3690   show ?case
  3691     unfolding sorted_Cons by auto
  3692 qed simp
  3693 
  3694 lemma sorted_equals_nth_mono:
  3695   "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
  3696 by (auto intro: sorted_nth_monoI sorted_nth_mono)
  3697 
  3698 lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"
  3699 by (induct xs) auto
  3700 
  3701 lemma set_sort[simp]: "set(sort_key f xs) = set xs"
  3702 by (induct xs) (simp_all add:set_insort)
  3703 
  3704 lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
  3705 by(induct xs)(auto simp:set_insort)
  3706 
  3707 lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
  3708 by(induct xs)(simp_all add:distinct_insort set_sort)
  3709 
  3710 lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
  3711 by(induct xs)(auto simp:sorted_Cons set_insort)
  3712 
  3713 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
  3714 using sorted_insort_key[where f="\<lambda>x. x"] by simp
  3715 
  3716 theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"
  3717 by(induct xs)(auto simp:sorted_insort_key)
  3718 
  3719 theorem sorted_sort[simp]: "sorted (sort xs)"
  3720 by(induct xs)(auto simp:sorted_insort)
  3721 
  3722 lemma sorted_butlast:
  3723   assumes "xs \<noteq> []" and "sorted xs"
  3724   shows "sorted (butlast xs)"
  3725 proof -
  3726   from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
  3727   with `sorted xs` show ?thesis by (simp add: sorted_append)
  3728 qed
  3729   
  3730 lemma insort_not_Nil [simp]:
  3731   "insort_key f a xs \<noteq> []"
  3732   by (induct xs) simp_all
  3733 
  3734 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
  3735 by (cases xs) auto
  3736 
  3737 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
  3738 by(induct xs)(auto simp add: sorted_Cons)
  3739 
  3740 lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk>
  3741   \<Longrightarrow> insort_key f a (remove1 a xs) = xs"
  3742 proof (induct xs)
  3743   case (Cons x xs)
  3744   thus ?case
  3745   proof (cases "x = a")
  3746     case False
  3747     hence "f x \<noteq> f a" using Cons.prems by auto
  3748     hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
  3749     thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
  3750   qed (auto simp: sorted_Cons insort_is_Cons)
  3751 qed simp
  3752 
  3753 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
  3754 using insort_key_remove1[where f="\<lambda>x. x"] by simp
  3755 
  3756 lemma sorted_remdups[simp]:
  3757   "sorted l \<Longrightarrow> sorted (remdups l)"
  3758 by (induct l) (auto simp: sorted_Cons)
  3759 
  3760 lemma sorted_distinct_set_unique:
  3761 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
  3762 shows "xs = ys"
  3763 proof -
  3764   from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
  3765   from assms show ?thesis
  3766   proof(induct rule:list_induct2[OF 1])
  3767     case 1 show ?case by simp
  3768   next
  3769     case 2 thus ?case by (simp add:sorted_Cons)
  3770        (metis Diff_insert_absorb antisym insertE insert_iff)
  3771   qed
  3772 qed
  3773 
  3774 lemma map_sorted_distinct_set_unique:
  3775   assumes "inj_on f (set xs \<union> set ys)"
  3776   assumes "sorted (map f xs)" "distinct (map f xs)"
  3777     "sorted (map f ys)" "distinct (map f ys)"
  3778   assumes "set xs = set ys"
  3779   shows "xs = ys"
  3780 proof -
  3781   from assms have "map f xs = map f ys"
  3782     by (simp add: sorted_distinct_set_unique)
  3783   moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
  3784     by (blast intro: map_inj_on)
  3785 qed
  3786 
  3787 lemma finite_sorted_distinct_unique:
  3788 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
  3789 apply(drule finite_distinct_list)
  3790 apply clarify
  3791 apply(rule_tac a="sort xs" in ex1I)
  3792 apply (auto simp: sorted_distinct_set_unique)
  3793 done
  3794 
  3795 lemma sorted_take:
  3796   "sorted xs \<Longrightarrow> sorted (take n xs)"
  3797 proof (induct xs arbitrary: n rule: sorted.induct)
  3798   case 1 show ?case by simp
  3799 next
  3800   case 2 show ?case by (cases n) simp_all
  3801 next
  3802   case (3 x y xs)
  3803   then have "x \<le> y" by simp
  3804   show ?case proof (cases n)
  3805     case 0 then show ?thesis by simp
  3806   next
  3807     case (Suc m) 
  3808     with 3 have "sorted (take m (y # xs))" by simp
  3809     with Suc  `x \<le> y` show ?thesis by (cases m) simp_all
  3810   qed
  3811 qed
  3812 
  3813 lemma sorted_drop:
  3814   "sorted xs \<Longrightarrow> sorted (drop n xs)"
  3815 proof (induct xs arbitrary: n rule: sorted.induct)
  3816   case 1 show ?case by simp
  3817 next
  3818   case 2 show ?case by (cases n) simp_all
  3819 next
  3820   case 3 then show ?case by (cases n) simp_all
  3821 qed
  3822 
  3823 lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
  3824   unfolding dropWhile_eq_drop by (rule sorted_drop)
  3825 
  3826 lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
  3827   apply (subst takeWhile_eq_take) by (rule sorted_take)
  3828 
  3829 lemma sorted_filter:
  3830   "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
  3831   by (induct xs) (simp_all add: sorted_Cons)
  3832 
  3833 lemma foldr_max_sorted:
  3834   assumes "sorted (rev xs)"
  3835   shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
  3836 using assms proof (induct xs)
  3837   case (Cons x xs)
  3838   moreover hence "sorted (rev xs)" using sorted_append by auto
  3839   ultimately show ?case
  3840     by (cases xs, auto simp add: sorted_append max_def)
  3841 qed simp
  3842 
  3843 lemma filter_equals_takeWhile_sorted_rev:
  3844   assumes sorted: "sorted (rev (map f xs))"
  3845   shows "[x \<leftarrow> xs. t < f x] = takeWhile (\<lambda> x. t < f x) xs"
  3846     (is "filter ?P xs = ?tW")
  3847 proof (rule takeWhile_eq_filter[symmetric])
  3848   let "?dW" = "dropWhile ?P xs"
  3849   fix x assume "x \<in> set ?dW"
  3850   then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i"
  3851     unfolding in_set_conv_nth by auto
  3852   hence "length ?tW + i < length (?tW @ ?dW)"
  3853     unfolding length_append by simp
  3854   hence i': "length (map f ?tW) + i < length (map f xs)" by simp
  3855   have "(map f ?tW @ map f ?dW) ! (length (map f ?tW) + i) \<le>
  3856         (map f ?tW @ map f ?dW) ! (length (map f ?tW) + 0)"
  3857     using sorted_rev_nth_mono[OF sorted _ i', of "length ?tW"]
  3858     unfolding map_append[symmetric] by simp
  3859   hence "f x \<le> f (?dW ! 0)"
  3860     unfolding nth_append_length_plus nth_i
  3861     using i preorder_class.le_less_trans[OF le0 i] by simp
  3862   also have "... \<le> t"
  3863     using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
  3864     using hd_conv_nth[of "?dW"] by simp
  3865   finally show "\<not> t < f x" by simp
  3866 qed
  3867 
  3868 lemma set_insort_insert:
  3869   "set (insort_insert x xs) = insert x (set xs)"
  3870   by (auto simp add: insort_insert_def set_insort)
  3871 
  3872 lemma distinct_insort_insert:
  3873   assumes "distinct xs"
  3874   shows "distinct (insort_insert x xs)"
  3875   using assms by (induct xs) (auto simp add: insort_insert_def set_insort)
  3876 
  3877 lemma sorted_insort_insert:
  3878   assumes "sorted xs"
  3879   shows "sorted (insort_insert x xs)"
  3880   using assms by (simp add: insort_insert_def sorted_insort)
  3881 
  3882 lemma filter_insort_key_triv:
  3883   "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
  3884   by (induct xs) simp_all
  3885 
  3886 lemma filter_insort_key:
  3887   "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
  3888   using assms by (induct xs)
  3889     (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
  3890 
  3891 lemma filter_sort_key:
  3892   "filter P (sort_key f xs) = sort_key f (filter P xs)"
  3893   by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)
  3894 
  3895 lemma sorted_same [simp]:
  3896   "sorted [x\<leftarrow>xs. x = f xs]"
  3897 proof (induct xs arbitrary: f)
  3898   case Nil then show ?case by simp
  3899 next
  3900   case (Cons x xs)
  3901   then have "sorted [y\<leftarrow>xs . y = (\<lambda>xs. x) xs]" .
  3902   moreover from Cons have "sorted [y\<leftarrow>xs . y = (f \<circ> Cons x) xs]" .
  3903   ultimately show ?case by (simp_all add: sorted_Cons)
  3904 qed
  3905 
  3906 lemma remove1_insort [simp]:
  3907   "remove1 x (insort x xs) = xs"
  3908   by (induct xs) simp_all
  3909 
  3910 end
  3911 
  3912 lemma sorted_upt[simp]: "sorted[i..<j]"
  3913 by (induct j) (simp_all add:sorted_append)
  3914 
  3915 lemma sorted_upto[simp]: "sorted[i..j]"
  3916 apply(induct i j rule:upto.induct)
  3917 apply(subst upto.simps)
  3918 apply(simp add:sorted_Cons)
  3919 done
  3920 
  3921 
  3922 subsubsection {* @{const transpose} on sorted lists *}
  3923 
  3924 lemma sorted_transpose[simp]:
  3925   shows "sorted (rev (map length (transpose xs)))"
  3926   by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose
  3927     length_filter_conv_card intro: card_mono)
  3928 
  3929 lemma transpose_max_length:
  3930   "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"
  3931   (is "?L = ?R")
  3932 proof (cases "transpose xs = []")
  3933   case False
  3934   have "?L = foldr max (map length (transpose xs)) 0"
  3935     by (simp add: foldr_map comp_def)
  3936   also have "... = length (transpose xs ! 0)"
  3937     using False sorted_transpose by (simp add: foldr_max_sorted)
  3938   finally show ?thesis
  3939     using False by (simp add: nth_transpose)
  3940 next
  3941   case True
  3942   hence "[x \<leftarrow> xs. x \<noteq> []] = []"
  3943     by (auto intro!: filter_False simp: transpose_empty)
  3944   thus ?thesis by (simp add: transpose_empty True)
  3945 qed
  3946 
  3947 lemma length_transpose_sorted:
  3948   fixes xs :: "'a list list"
  3949   assumes sorted: "sorted (rev (map length xs))"
  3950   shows "length (transpose xs) = (if xs = [] then 0 else length (xs ! 0))"
  3951 proof (cases "xs = []")
  3952   case False
  3953   thus ?thesis
  3954     using foldr_max_sorted[OF sorted] False
  3955     unfolding length_transpose foldr_map comp_def
  3956     by simp
  3957 qed simp
  3958 
  3959 lemma nth_nth_transpose_sorted[simp]:
  3960   fixes xs :: "'a list list"
  3961   assumes sorted: "sorted (rev (map length xs))"
  3962   and i: "i < length (transpose xs)"
  3963   and j: "j < length [ys \<leftarrow> xs. i < length ys]"
  3964   shows "transpose xs ! i ! j = xs ! j  ! i"
  3965   using j filter_equals_takeWhile_sorted_rev[OF sorted, of i]
  3966     nth_transpose[OF i] nth_map[OF j]
  3967   by (simp add: takeWhile_nth)
  3968 
  3969 lemma transpose_column_length:
  3970   fixes xs :: "'a list list"
  3971   assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
  3972   shows "length (filter (\<lambda>ys. i < length ys) (transpose xs)) = length (xs ! i)"
  3973 proof -
  3974   have "xs \<noteq> []" using `i < length xs` by auto
  3975   note filter_equals_takeWhile_sorted_rev[OF sorted, simp]
  3976   { fix j assume "j \<le> i"
  3977     note sorted_rev_nth_mono[OF sorted, of j i, simplified, OF this `i < length xs`]
  3978   } note sortedE = this[consumes 1]
  3979 
  3980   have "{j. j < length (transpose xs) \<and> i < length (transpose xs ! j)}
  3981     = {..< length (xs ! i)}"
  3982   proof safe
  3983     fix j
  3984     assume "j < length (transpose xs)" and "i < length (transpose xs ! j)"
  3985     with this(2) nth_transpose[OF this(1)]
  3986     have "i < length (takeWhile (\<lambda>ys. j < length ys) xs)" by simp
  3987     from nth_mem[OF this] takeWhile_nth[OF this]
  3988     show "j < length (xs ! i)" by (auto dest: set_takeWhileD)
  3989   next
  3990     fix j assume "j < length (xs ! i)"
  3991     thus "j < length (transpose xs)"
  3992       using foldr_max_sorted[OF sorted] `xs \<noteq> []` sortedE[OF le0]
  3993       by (auto simp: length_transpose comp_def foldr_map)
  3994 
  3995     have "Suc i \<le> length (takeWhile (\<lambda>ys. j < length ys) xs)"
  3996       using `i < length xs` `j < length (xs ! i)` less_Suc_eq_le
  3997       by (auto intro!: length_takeWhile_less_P_nth dest!: sortedE)
  3998     with nth_transpose[OF `j < length (transpose xs)`]
  3999     show "i < length (transpose xs ! j)" by simp
  4000   qed
  4001   thus ?thesis by (simp add: length_filter_conv_card)
  4002 qed
  4003 
  4004 lemma transpose_column:
  4005   fixes xs :: "'a list list"
  4006   assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
  4007   shows "map (\<lambda>ys. ys ! i) (filter (\<lambda>ys. i < length ys) (transpose xs))
  4008     = xs ! i" (is "?R = _")
  4009 proof (rule nth_equalityI, safe)
  4010   show length: "length ?R = length (xs ! i)"
  4011     using transpose_column_length[OF assms] by simp
  4012 
  4013   fix j assume j: "j < length ?R"
  4014   note * = less_le_trans[OF this, unfolded length_map, OF length_filter_le]
  4015   from j have j_less: "j < length (xs ! i)" using length by simp
  4016   have i_less_tW: "Suc i \<le> length (takeWhile (\<lambda>ys. Suc j \<le> length ys) xs)"
  4017   proof (rule length_takeWhile_less_P_nth)
  4018     show "Suc i \<le> length xs" using `i < length xs` by simp
  4019     fix k assume "k < Suc i"
  4020     hence "k \<le> i" by auto
  4021     with sorted_rev_nth_mono[OF sorted this] `i < length xs`
  4022     have "length (xs ! i) \<le> length (xs ! k)" by simp
  4023     thus "Suc j \<le> length (xs ! k)" using j_less by simp
  4024   qed
  4025   have i_less_filter: "i < length [ys\<leftarrow>xs . j < length ys]"
  4026     unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j]
  4027     using i_less_tW by (simp_all add: Suc_le_eq)
  4028   from j show "?R ! j = xs ! i ! j"
  4029     unfolding filter_equals_takeWhile_sorted_rev[OF sorted_transpose, of i]
  4030     by (simp add: takeWhile_nth nth_nth_transpose_sorted[OF sorted * i_less_filter])
  4031 qed
  4032 
  4033 lemma transpose_transpose:
  4034   fixes xs :: "'a list list"
  4035   assumes sorted: "sorted (rev (map length xs))"
  4036   shows "transpose (transpose xs) = takeWhile (\<lambda>x. x \<noteq> []) xs" (is "?L = ?R")
  4037 proof -
  4038   have len: "length ?L = length ?R"
  4039     unfolding length_transpose transpose_max_length
  4040     using filter_equals_takeWhile_sorted_rev[OF sorted, of 0]
  4041     by simp
  4042 
  4043   { fix i assume "i < length ?R"
  4044     with less_le_trans[OF _ length_takeWhile_le[of _ xs]]
  4045     have "i < length xs" by simp
  4046   } note * = this
  4047   show ?thesis
  4048     by (rule nth_equalityI)
  4049        (simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth)
  4050 qed
  4051 
  4052 theorem transpose_rectangle:
  4053   assumes "xs = [] \<Longrightarrow> n = 0"
  4054   assumes rect: "\<And> i. i < length xs \<Longrightarrow> length (xs ! i) = n"
  4055   shows "transpose xs = map (\<lambda> i. map (\<lambda> j. xs ! j ! i) [0..<length xs]) [0..<n]"
  4056     (is "?trans = ?map")
  4057 proof (rule nth_equalityI)
  4058   have "sorted (rev (map length xs))"
  4059     by (auto simp: rev_nth rect intro!: sorted_nth_monoI)
  4060   from foldr_max_sorted[OF this] assms
  4061   show len: "length ?trans = length ?map"
  4062     by (simp_all add: length_transpose foldr_map comp_def)
  4063   moreover
  4064   { fix i assume "i < n" hence "[ys\<leftarrow>xs . i < length ys] = xs"
  4065       using rect by (auto simp: in_set_conv_nth intro!: filter_True) }
  4066   ultimately show "\<forall>i < length ?trans. ?trans ! i = ?map ! i"
  4067     by (auto simp: nth_transpose intro: nth_equalityI)
  4068 qed
  4069 
  4070 
  4071 subsubsection {* @{text sorted_list_of_set} *}
  4072 
  4073 text{* This function maps (finite) linearly ordered sets to sorted
  4074 lists. Warning: in most cases it is not a good idea to convert from
  4075 sets to lists but one should convert in the other direction (via
  4076 @{const set}). *}
  4077 
  4078 context linorder
  4079 begin
  4080 
  4081 definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
  4082   "sorted_list_of_set = Finite_Set.fold insort []"
  4083 
  4084 lemma sorted_list_of_set_empty [simp]:
  4085   "sorted_list_of_set {} = []"
  4086   by (simp add: sorted_list_of_set_def)
  4087 
  4088 lemma sorted_list_of_set_insert [simp]:
  4089   assumes "finite A"
  4090   shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
  4091 proof -
  4092   interpret fun_left_comm insort by (fact fun_left_comm_insort)
  4093   with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
  4094 qed
  4095 
  4096 lemma sorted_list_of_set [simp]:
  4097   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
  4098     \<and> distinct (sorted_list_of_set A)"
  4099   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
  4100 
  4101 lemma sorted_list_of_set_sort_remdups:
  4102   "sorted_list_of_set (set xs) = sort (remdups xs)"
  4103 proof -
  4104   interpret fun_left_comm insort by (fact fun_left_comm_insort)
  4105   show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
  4106 qed
  4107 
  4108 lemma sorted_list_of_set_remove:
  4109   assumes "finite A"
  4110   shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
  4111 proof (cases "x \<in> A")
  4112   case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
  4113   with False show ?thesis by (simp add: remove1_idem)
  4114 next
  4115   case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
  4116   with assms show ?thesis by simp
  4117 qed
  4118 
  4119 end
  4120 
  4121 lemma sorted_list_of_set_range [simp]:
  4122   "sorted_list_of_set {m..<n} = [m..<n]"
  4123   by (rule sorted_distinct_set_unique) simp_all
  4124 
  4125 
  4126 
  4127 subsubsection {* @{text lists}: the list-forming operator over sets *}
  4128 
  4129 inductive_set
  4130   lists :: "'a set => 'a list set"
  4131   for A :: "'a set"
  4132 where
  4133     Nil [intro!]: "[]: lists A"
  4134   | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
  4135 
  4136 inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
  4137 inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
  4138 
  4139 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
  4140 by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
  4141 
  4142 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
  4143 
  4144 lemma listsp_infI:
  4145   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
  4146 by induct blast+
  4147 
  4148 lemmas lists_IntI = listsp_infI [to_set]
  4149 
  4150 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
  4151 proof (rule mono_inf [where f=listsp, THEN order_antisym])
  4152   show "mono listsp" by (simp add: mono_def listsp_mono)
  4153   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
  4154 qed
  4155 
  4156 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
  4157 
  4158 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
  4159 
  4160 lemma append_in_listsp_conv [iff]:
  4161      "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
  4162 by (induct xs) auto
  4163 
  4164 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
  4165 
  4166 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
  4167 -- {* eliminate @{text listsp} in favour of @{text set} *}
  4168 by (induct xs) auto
  4169 
  4170 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
  4171 
  4172 lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
  4173 by (rule in_listsp_conv_set [THEN iffD1])
  4174 
  4175 lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
  4176 
  4177 lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
  4178 by (rule in_listsp_conv_set [THEN iffD2])
  4179 
  4180 lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
  4181 
  4182 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
  4183 by auto
  4184 
  4185 
  4186 subsubsection {* Inductive definition for membership *}
  4187 
  4188 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
  4189 where
  4190     elem:  "ListMem x (x # xs)"
  4191   | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
  4192 
  4193 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
  4194 apply (rule iffI)
  4195  apply (induct set: ListMem)
  4196   apply auto
  4197 apply (induct xs)
  4198  apply (auto intro: ListMem.intros)
  4199 done
  4200 
  4201 
  4202 subsubsection {* Lists as Cartesian products *}
  4203 
  4204 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
  4205 @{term A} and tail drawn from @{term Xs}.*}
  4206 
  4207 definition
  4208   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
  4209   "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
  4210 
  4211 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
  4212 by (auto simp add: set_Cons_def)
  4213 
  4214 text{*Yields the set of lists, all of the same length as the argument and
  4215 with elements drawn from the corresponding element of the argument.*}
  4216 
  4217 primrec
  4218   listset :: "'a set list \<Rightarrow> 'a list set" where
  4219      "listset [] = {[]}"
  4220   |  "listset (A # As) = set_Cons A (listset As)"
  4221 
  4222 
  4223 subsection {* Relations on Lists *}
  4224 
  4225 subsubsection {* Length Lexicographic Ordering *}
  4226 
  4227 text{*These orderings preserve well-foundedness: shorter lists 
  4228   precede longer lists. These ordering are not used in dictionaries.*}
  4229         
  4230 primrec -- {*The lexicographic ordering for lists of the specified length*}
  4231   lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
  4232     "lexn r 0 = {}"
  4233   | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
  4234       {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
  4235 
  4236 definition
  4237   lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
  4238   "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
  4239 
  4240 definition
  4241   lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
  4242   "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
  4243         -- {*Compares lists by their length and then lexicographically*}
  4244 
  4245 lemma wf_lexn: "wf r ==> wf (lexn r n)"
  4246 apply (induct n, simp, simp)
  4247 apply(rule wf_subset)
  4248  prefer 2 apply (rule Int_lower1)
  4249 apply(rule wf_prod_fun_image)
  4250  prefer 2 apply (rule inj_onI, auto)
  4251 done
  4252 
  4253 lemma lexn_length:
  4254   "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
  4255 by (induct n arbitrary: xs ys) auto
  4256 
  4257 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
  4258 apply (unfold lex_def)
  4259 apply (rule wf_UN)
  4260 apply (blast intro: wf_lexn, clarify)
  4261 apply (rename_tac m n)
  4262 apply (subgoal_tac "m \<noteq> n")
  4263  prefer 2 apply blast
  4264 apply (blast dest: lexn_length not_sym)
  4265 done
  4266 
  4267 lemma lexn_conv:
  4268   "lexn r n =
  4269     {(xs,ys). length xs = n \<and> length ys = n \<and>
  4270     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
  4271 apply (induct n, simp)
  4272 apply (simp add: image_Collect lex_prod_def, safe, blast)
  4273  apply (rule_tac x = "ab # xys" in exI, simp)
  4274 apply (case_tac xys, simp_all, blast)
  4275 done
  4276 
  4277 lemma lex_conv:
  4278   "lex r =
  4279     {(xs,ys). length xs = length ys \<and>
  4280     (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
  4281 by (force simp add: lex_def lexn_conv)
  4282 
  4283 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
  4284 by (unfold lenlex_def) blast
  4285 
  4286 lemma lenlex_conv:
  4287     "lenlex r = {(xs,ys). length xs < length ys |
  4288                  length xs = length ys \<and> (xs, ys) : lex r}"
  4289 by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
  4290 
  4291 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
  4292 by (simp add: lex_conv)
  4293 
  4294 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
  4295 by (simp add:lex_conv)
  4296 
  4297 lemma Cons_in_lex [simp]:
  4298     "((x # xs, y # ys) : lex r) =
  4299       ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
  4300 apply (simp add: lex_conv)
  4301 apply (rule iffI)
  4302  prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
  4303 apply (case_tac xys, simp, simp)
  4304 apply blast
  4305 done
  4306 
  4307 
  4308 subsubsection {* Lexicographic Ordering *}
  4309 
  4310 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
  4311     This ordering does \emph{not} preserve well-foundedness.
  4312      Author: N. Voelker, March 2005. *} 
  4313 
  4314 definition
  4315   lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
  4316   "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
  4317             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
  4318 
  4319 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
  4320 by (unfold lexord_def, induct_tac y, auto) 
  4321 
  4322 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
  4323 by (unfold lexord_def, induct_tac x, auto)
  4324 
  4325 lemma lexord_cons_cons[simp]:
  4326      "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
  4327   apply (unfold lexord_def, safe, simp_all)
  4328   apply (case_tac u, simp, simp)
  4329   apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
  4330   apply (erule_tac x="b # u" in allE)
  4331   by force
  4332 
  4333 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
  4334 
  4335 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
  4336 by (induct_tac x, auto)  
  4337 
  4338 lemma lexord_append_left_rightI:
  4339      "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
  4340 by (induct_tac u, auto)
  4341 
  4342 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
  4343 by (induct x, auto)
  4344 
  4345 lemma lexord_append_leftD:
  4346      "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
  4347 by (erule rev_mp, induct_tac x, auto)
  4348 
  4349 lemma lexord_take_index_conv: 
  4350    "((x,y) : lexord r) = 
  4351     ((length x < length y \<and> take (length x) y = x) \<or> 
  4352      (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
  4353   apply (unfold lexord_def Let_def, clarsimp) 
  4354   apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
  4355   apply auto 
  4356   apply (rule_tac x="hd (drop (length x) y)" in exI)
  4357   apply (rule_tac x="tl (drop (length x) y)" in exI)
  4358   apply (erule subst, simp add: min_def) 
  4359   apply (rule_tac x ="length u" in exI, simp) 
  4360   apply (rule_tac x ="take i x" in exI) 
  4361   apply (rule_tac x ="x ! i" in exI) 
  4362   apply (rule_tac x ="y ! i" in exI, safe) 
  4363   apply (rule_tac x="drop (Suc i) x" in exI)
  4364   apply (drule sym, simp add: drop_Suc_conv_tl) 
  4365   apply (rule_tac x="drop (Suc i) y" in exI)
  4366   by (simp add: drop_Suc_conv_tl) 
  4367 
  4368 -- {* lexord is extension of partial ordering List.lex *} 
  4369 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
  4370   apply (rule_tac x = y in spec) 
  4371   apply (induct_tac x, clarsimp) 
  4372   by (clarify, case_tac x, simp, force)
  4373 
  4374 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
  4375   by (induct y, auto)
  4376 
  4377 lemma lexord_trans: 
  4378     "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
  4379    apply (erule rev_mp)+
  4380    apply (rule_tac x = x in spec) 
  4381   apply (rule_tac x = z in spec) 
  4382   apply ( induct_tac y, simp, clarify)
  4383   apply (case_tac xa, erule ssubst) 
  4384   apply (erule allE, erule allE) -- {* avoid simp recursion *} 
  4385   apply (case_tac x, simp, simp) 
  4386   apply (case_tac x, erule allE, erule allE, simp)
  4387   apply (erule_tac x = listb in allE) 
  4388   apply (erule_tac x = lista in allE, simp)
  4389   apply (unfold trans_def)
  4390   by blast
  4391 
  4392 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
  4393 by (rule transI, drule lexord_trans, blast) 
  4394 
  4395 lemma lexord_linear: "(! a b. (a,b)\<in> r | a = b | (b,a) \<in> r) \<Longrightarrow> (x,y) : lexord r | x = y | (y,x) : lexord r"
  4396   apply (rule_tac x = y in spec) 
  4397   apply (induct_tac x, rule allI) 
  4398   apply (case_tac x, simp, simp) 
  4399   apply (rule allI, case_tac x, simp, simp) 
  4400   by blast
  4401 
  4402 
  4403 subsection {* Lexicographic combination of measure functions *}
  4404 
  4405 text {* These are useful for termination proofs *}
  4406 
  4407 definition
  4408   "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
  4409 
  4410 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
  4411 unfolding measures_def
  4412 by blast
  4413 
  4414 lemma in_measures[simp]: 
  4415   "(x, y) \<in> measures [] = False"
  4416   "(x, y) \<in> measures (f # fs)
  4417          = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
  4418 unfolding measures_def
  4419 by auto
  4420 
  4421 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
  4422 by simp
  4423 
  4424 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
  4425 by auto
  4426 
  4427 
  4428 subsubsection {* Lifting a Relation on List Elements to the Lists *}
  4429 
  4430 inductive_set
  4431   listrel :: "('a * 'a)set => ('a list * 'a list)set"
  4432   for r :: "('a * 'a)set"
  4433 where
  4434     Nil:  "([],[]) \<in> listrel r"
  4435   | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
  4436 
  4437 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
  4438 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
  4439 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
  4440 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
  4441 
  4442 
  4443 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
  4444 apply clarify  
  4445 apply (erule listrel.induct)
  4446 apply (blast intro: listrel.intros)+
  4447 done
  4448 
  4449 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
  4450 apply clarify 
  4451 apply (erule listrel.induct, auto) 
  4452 done
  4453 
  4454 lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)" 
  4455 apply (simp add: refl_on_def listrel_subset Ball_def)
  4456 apply (rule allI) 
  4457 apply (induct_tac x) 
  4458 apply (auto intro: listrel.intros)
  4459 done
  4460 
  4461 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
  4462 apply (auto simp add: sym_def)
  4463 apply (erule listrel.induct) 
  4464 apply (blast intro: listrel.intros)+
  4465 done
  4466 
  4467 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
  4468 apply (simp add: trans_def)
  4469 apply (intro allI) 
  4470 apply (rule impI) 
  4471 apply (erule listrel.induct) 
  4472 apply (blast intro: listrel.intros)+
  4473 done
  4474 
  4475 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
  4476 by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) 
  4477 
  4478 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
  4479 by (blast intro: listrel.intros)
  4480 
  4481 lemma listrel_Cons:
  4482      "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
  4483 by (auto simp add: set_Cons_def intro: listrel.intros)
  4484 
  4485 
  4486 subsection {* Size function *}
  4487 
  4488 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
  4489 by (rule is_measure_trivial)
  4490 
  4491 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
  4492 by (rule is_measure_trivial)
  4493 
  4494 lemma list_size_estimation[termination_simp]: 
  4495   "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
  4496 by (induct xs) auto
  4497 
  4498 lemma list_size_estimation'[termination_simp]: 
  4499   "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
  4500 by (induct xs) auto
  4501 
  4502 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
  4503 by (induct xs) auto
  4504 
  4505 lemma list_size_pointwise[termination_simp]: 
  4506   "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
  4507 by (induct xs) force+
  4508 
  4509 
  4510 subsection {* Transfer *}
  4511 
  4512 definition
  4513   embed_list :: "nat list \<Rightarrow> int list"
  4514 where
  4515   "embed_list l = map int l"
  4516 
  4517 definition
  4518   nat_list :: "int list \<Rightarrow> bool"
  4519 where
  4520   "nat_list l = nat_set (set l)"
  4521 
  4522 definition
  4523   return_list :: "int list \<Rightarrow> nat list"
  4524 where
  4525   "return_list l = map nat l"
  4526 
  4527 lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
  4528     embed_list (return_list l) = l"
  4529   unfolding embed_list_def return_list_def nat_list_def nat_set_def
  4530   apply (induct l)
  4531   apply auto
  4532 done
  4533 
  4534 lemma transfer_nat_int_list_functions:
  4535   "l @ m = return_list (embed_list l @ embed_list m)"
  4536   "[] = return_list []"
  4537   unfolding return_list_def embed_list_def
  4538   apply auto
  4539   apply (induct l, auto)
  4540   apply (induct m, auto)
  4541 done
  4542 
  4543 (*
  4544 lemma transfer_nat_int_fold1: "fold f l x =
  4545     fold (%x. f (nat x)) (embed_list l) x";
  4546 *)
  4547 
  4548 
  4549 subsection {* Code generation *}
  4550 
  4551 subsubsection {* Counterparts for set-related operations *}
  4552 
  4553 definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
  4554   [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
  4555 
  4556 text {*
  4557   Only use @{text member} for generating executable code.  Otherwise use
  4558   @{prop "x \<in> set xs"} instead --- it is much easier to reason about.
  4559 *}
  4560 
  4561 lemma member_set:
  4562   "member = set"
  4563   by (simp add: expand_fun_eq member_def mem_def)
  4564 
  4565 lemma member_rec [code]:
  4566   "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
  4567   "member [] y \<longleftrightarrow> False"
  4568   by (auto simp add: member_def)
  4569 
  4570 lemma in_set_member [code_unfold]:
  4571   "x \<in> set xs \<longleftrightarrow> member xs x"
  4572   by (simp add: member_def)
  4573 
  4574 declare INFI_def [code_unfold]
  4575 declare SUPR_def [code_unfold]
  4576 
  4577 declare set_map [symmetric, code_unfold]
  4578 
  4579 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  4580   list_all_iff [code_post]: "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
  4581 
  4582 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  4583   list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
  4584 
  4585 text {*
  4586   Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
  4587   over @{const list_all} and @{const list_ex} in specifications.
  4588 *}
  4589 
  4590 lemma list_all_simps [simp, code]:
  4591   "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"
  4592   "list_all P [] \<longleftrightarrow> True"
  4593   by (simp_all add: list_all_iff)
  4594 
  4595 lemma list_ex_simps [simp, code]:
  4596   "list_ex P (x # xs) \<longleftrightarrow> P x \<or> list_ex P xs"
  4597   "list_ex P [] \<longleftrightarrow> False"
  4598   by (simp_all add: list_ex_iff)
  4599 
  4600 lemma Ball_set_list_all [code_unfold]:
  4601   "Ball (set xs) P \<longleftrightarrow> list_all P xs"
  4602   by (simp add: list_all_iff)
  4603 
  4604 lemma Bex_set_list_ex [code_unfold]:
  4605   "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
  4606   by (simp add: list_ex_iff)
  4607 
  4608 lemma list_all_append [simp]:
  4609   "list_all P (xs @ ys) \<longleftrightarrow> list_all P xs \<and> list_all P ys"
  4610   by (auto simp add: list_all_iff)
  4611 
  4612 lemma list_ex_append [simp]:
  4613   "list_ex P (xs @ ys) \<longleftrightarrow> list_ex P xs \<or> list_ex P ys"
  4614   by (auto simp add: list_ex_iff)
  4615 
  4616 lemma list_all_rev [simp]:
  4617   "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
  4618   by (simp add: list_all_iff)
  4619 
  4620 lemma list_ex_rev [simp]:
  4621   "list_ex P (rev xs) \<longleftrightarrow> list_ex P xs"
  4622   by (simp add: list_ex_iff)
  4623 
  4624 lemma list_all_length:
  4625   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
  4626   by (auto simp add: list_all_iff set_conv_nth)
  4627 
  4628 lemma list_ex_length:
  4629   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
  4630   by (auto simp add: list_ex_iff set_conv_nth)
  4631 
  4632 lemma list_all_cong [fundef_cong]:
  4633   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
  4634   by (simp add: list_all_iff)
  4635 
  4636 lemma list_any_cong [fundef_cong]:
  4637   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
  4638   by (simp add: list_ex_iff)
  4639 
  4640 text {* Bounded quantification and summation over nats. *}
  4641 
  4642 lemma atMost_upto [code_unfold]:
  4643   "{..n} = set [0..<Suc n]"
  4644   by auto
  4645 
  4646 lemma atLeast_upt [code_unfold]:
  4647   "{..<n} = set [0..<n]"
  4648   by auto
  4649 
  4650 lemma greaterThanLessThan_upt [code_unfold]:
  4651   "{n<..<m} = set [Suc n..<m]"
  4652   by auto
  4653 
  4654 lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
  4655 
  4656 lemma greaterThanAtMost_upt [code_unfold]:
  4657   "{n<..m} = set [Suc n..<Suc m]"
  4658   by auto
  4659 
  4660 lemma atLeastAtMost_upt [code_unfold]:
  4661   "{n..m} = set [n..<Suc m]"
  4662   by auto
  4663 
  4664 lemma all_nat_less_eq [code_unfold]:
  4665   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
  4666   by auto
  4667 
  4668 lemma ex_nat_less_eq [code_unfold]:
  4669   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
  4670   by auto
  4671 
  4672 lemma all_nat_less [code_unfold]:
  4673   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
  4674   by auto
  4675 
  4676 lemma ex_nat_less [code_unfold]:
  4677   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
  4678   by auto
  4679 
  4680 lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
  4681   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
  4682   by (simp add: interv_listsum_conv_setsum_set_nat)
  4683 
  4684 text {* Summation over ints. *}
  4685 
  4686 lemma greaterThanLessThan_upto [code_unfold]:
  4687   "{i<..<j::int} = set [i+1..j - 1]"
  4688 by auto
  4689 
  4690 lemma atLeastLessThan_upto [code_unfold]:
  4691   "{i..<j::int} = set [i..j - 1]"
  4692 by auto
  4693 
  4694 lemma greaterThanAtMost_upto [code_unfold]:
  4695   "{i<..j::int} = set [i+1..j]"
  4696 by auto
  4697 
  4698 lemmas atLeastAtMost_upto [code_unfold] = set_upto [symmetric]
  4699 
  4700 lemma setsum_set_upto_conv_listsum_int [code_unfold]:
  4701   "setsum f (set [i..j::int]) = listsum (map f [i..j])"
  4702   by (simp add: interv_listsum_conv_setsum_set_int)
  4703 
  4704 
  4705 subsubsection {* Optimizing by rewriting *}
  4706 
  4707 definition null :: "'a list \<Rightarrow> bool" where
  4708   [code_post]: "null xs \<longleftrightarrow> xs = []"
  4709 
  4710 text {*
  4711   Efficient emptyness check is implemented by @{const null}.
  4712 *}
  4713 
  4714 lemma null_rec [code]:
  4715   "null (x # xs) \<longleftrightarrow> False"
  4716   "null [] \<longleftrightarrow> True"
  4717   by (simp_all add: null_def)
  4718 
  4719 lemma eq_Nil_null [code_unfold]:
  4720   "xs = [] \<longleftrightarrow> null xs"
  4721   by (simp add: null_def)
  4722 
  4723 lemma equal_Nil_null [code_unfold]:
  4724   "eq_class.eq xs [] \<longleftrightarrow> null xs"
  4725   by (simp add: eq eq_Nil_null)
  4726 
  4727 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
  4728   [code_post]: "maps f xs = concat (map f xs)"
  4729 
  4730 definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
  4731   [code_post]: "map_filter f xs = map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) xs)"
  4732 
  4733 text {*
  4734   Operations @{const maps} and @{const map_filter} avoid
  4735   intermediate lists on execution -- do not use for proving.
  4736 *}
  4737 
  4738 lemma maps_simps [code]:
  4739   "maps f (x # xs) = f x @ maps f xs"
  4740   "maps f [] = []"
  4741   by (simp_all add: maps_def)
  4742 
  4743 lemma map_filter_simps [code]:
  4744   "map_filter f (x # xs) = (case f x of None \<Rightarrow> map_filter f xs | Some y \<Rightarrow> y # map_filter f xs)"
  4745   "map_filter f [] = []"
  4746   by (simp_all add: map_filter_def split: option.split)
  4747 
  4748 lemma concat_map_maps [code_unfold]:
  4749   "concat (map f xs) = maps f xs"
  4750   by (simp add: maps_def)
  4751 
  4752 lemma map_filter_map_filter [code_unfold]:
  4753   "map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
  4754   by (simp add: map_filter_def)
  4755 
  4756 text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
  4757 and similiarly for @{text"\<exists>"}. *}
  4758 
  4759 definition all_interval_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
  4760   "all_interval_nat P i j \<longleftrightarrow> (\<forall>n \<in> {i..<j}. P n)"
  4761 
  4762 lemma [code]:
  4763   "all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"
  4764 proof -
  4765   have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"
  4766   proof -
  4767     fix n
  4768     assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> n" "n < j"
  4769     then show "P n" by (cases "n = i") simp_all
  4770   qed
  4771   show ?thesis by (auto simp add: all_interval_nat_def intro: *)
  4772 qed
  4773 
  4774 lemma list_all_iff_all_interval_nat [code_unfold]:
  4775   "list_all P [i..<j] \<longleftrightarrow> all_interval_nat P i j"
  4776   by (simp add: list_all_iff all_interval_nat_def)
  4777 
  4778 lemma list_ex_iff_not_all_inverval_nat [code_unfold]:
  4779   "list_ex P [i..<j] \<longleftrightarrow> \<not> (all_interval_nat (Not \<circ> P) i j)"
  4780   by (simp add: list_ex_iff all_interval_nat_def)
  4781 
  4782 definition all_interval_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
  4783   "all_interval_int P i j \<longleftrightarrow> (\<forall>k \<in> {i..j}. P k)"
  4784 
  4785 lemma [code]:
  4786   "all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"
  4787 proof -
  4788   have *: "\<And>k. P i \<Longrightarrow> \<forall>k\<in>{i+1..j}. P k \<Longrightarrow> i \<le> k \<Longrightarrow> k \<le> j \<Longrightarrow> P k"
  4789   proof -
  4790     fix k
  4791     assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> j"
  4792     then show "P k" by (cases "k = i") simp_all
  4793   qed
  4794   show ?thesis by (auto simp add: all_interval_int_def intro: *)
  4795 qed
  4796 
  4797 lemma list_all_iff_all_interval_int [code_unfold]:
  4798   "list_all P [i..j] \<longleftrightarrow> all_interval_int P i j"
  4799   by (simp add: list_all_iff all_interval_int_def)
  4800 
  4801 lemma list_ex_iff_not_all_inverval_int [code_unfold]:
  4802   "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
  4803   by (simp add: list_ex_iff all_interval_int_def)
  4804 
  4805 hide_const (open) member null maps map_filter all_interval_nat all_interval_int
  4806 
  4807 
  4808 subsubsection {* Pretty lists *}
  4809 
  4810 use "Tools/list_code.ML"
  4811 
  4812 code_type list
  4813   (SML "_ list")
  4814   (OCaml "_ list")
  4815   (Haskell "![(_)]")
  4816   (Scala "List[(_)]")
  4817 
  4818 code_const Nil
  4819   (SML "[]")
  4820   (OCaml "[]")
  4821   (Haskell "[]")
  4822   (Scala "Nil")
  4823 
  4824 code_instance list :: eq
  4825   (Haskell -)
  4826 
  4827 code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
  4828   (Haskell infixl 4 "==")
  4829 
  4830 code_reserved SML
  4831   list
  4832 
  4833 code_reserved OCaml
  4834   list
  4835 
  4836 types_code
  4837   "list" ("_ list")
  4838 attach (term_of) {*
  4839 fun term_of_list f T = HOLogic.mk_list T o map f;
  4840 *}
  4841 attach (test) {*
  4842 fun gen_list' aG aT i j = frequency
  4843   [(i, fn () =>
  4844       let
  4845         val (x, t) = aG j;
  4846         val (xs, ts) = gen_list' aG aT (i-1) j
  4847       in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
  4848    (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
  4849 and gen_list aG aT i = gen_list' aG aT i i;
  4850 *}
  4851 
  4852 consts_code Cons ("(_ ::/ _)")
  4853 
  4854 setup {*
  4855 let
  4856   fun list_codegen thy defs dep thyname b t gr =
  4857     let
  4858       val ts = HOLogic.dest_list t;
  4859       val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
  4860         (fastype_of t) gr;
  4861       val (ps, gr'') = fold_map
  4862         (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
  4863     in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
  4864 in
  4865   fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
  4866   #> Codegen.add_codegen "list_codegen" list_codegen
  4867 end
  4868 *}
  4869 
  4870 
  4871 subsubsection {* Use convenient predefined operations *}
  4872 
  4873 code_const "op @"
  4874   (SML infixr 7 "@")
  4875   (OCaml infixr 6 "@")
  4876   (Haskell infixr 5 "++")
  4877   (Scala infixl 7 "++")
  4878 
  4879 code_const map
  4880   (Haskell "map")
  4881 
  4882 code_const filter
  4883   (Haskell "filter")
  4884 
  4885 code_const concat
  4886   (Haskell "concat")
  4887 
  4888 code_const List.maps
  4889   (Haskell "concatMap")
  4890 
  4891 code_const rev
  4892   (Haskell "reverse")
  4893 
  4894 code_const zip
  4895   (Haskell "zip")
  4896 
  4897 code_const List.null
  4898   (Haskell "null")
  4899 
  4900 code_const takeWhile
  4901   (Haskell "takeWhile")
  4902 
  4903 code_const dropWhile
  4904   (Haskell "dropWhile")
  4905 
  4906 code_const hd
  4907   (Haskell "head")
  4908 
  4909 code_const last
  4910   (Haskell "last")
  4911 
  4912 code_const list_all
  4913   (Haskell "all")
  4914 
  4915 code_const list_ex
  4916   (Haskell "any")
  4917 
  4918 end