src/HOL/List.thy
author nipkow
Wed Aug 26 19:54:01 2009 +0200 (2009-08-26)
changeset 32415 1dddf2f64266
parent 32078 1c14f77201d4
child 32417 e87d9c78910c
permissions -rw-r--r--
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
     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 Presburger Recdef ATP_Linkup
     9 uses ("Tools/list_code.ML")
    10 begin
    11 
    12 datatype 'a list =
    13     Nil    ("[]")
    14   | Cons 'a  "'a list"    (infixr "#" 65)
    15 
    16 subsection{*Basic list processing functions*}
    17 
    18 consts
    19   filter:: "('a => bool) => 'a list => 'a list"
    20   concat:: "'a list list => 'a list"
    21   foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
    22   foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
    23   hd:: "'a list => 'a"
    24   tl:: "'a list => 'a list"
    25   last:: "'a list => 'a"
    26   butlast :: "'a list => 'a list"
    27   set :: "'a list => 'a set"
    28   map :: "('a=>'b) => ('a list => 'b list)"
    29   listsum ::  "'a list => 'a::monoid_add"
    30   list_update :: "'a list => nat => 'a => 'a list"
    31   take:: "nat => 'a list => 'a list"
    32   drop:: "nat => 'a list => 'a list"
    33   takeWhile :: "('a => bool) => 'a list => 'a list"
    34   dropWhile :: "('a => bool) => 'a list => 'a list"
    35   rev :: "'a list => 'a list"
    36   zip :: "'a list => 'b list => ('a * 'b) list"
    37   upt :: "nat => nat => nat list" ("(1[_..</_'])")
    38   remdups :: "'a list => 'a list"
    39   remove1 :: "'a => 'a list => 'a list"
    40   removeAll :: "'a => 'a list => 'a list"
    41   "distinct":: "'a list => bool"
    42   replicate :: "nat => 'a => 'a list"
    43   splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    44 
    45 
    46 nonterminals lupdbinds lupdbind
    47 
    48 syntax
    49   -- {* list Enumeration *}
    50   "@list" :: "args => 'a list"    ("[(_)]")
    51 
    52   -- {* Special syntax for filter *}
    53   "@filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
    54 
    55   -- {* list update *}
    56   "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")
    57   "" :: "lupdbind => lupdbinds"    ("_")
    58   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")
    59   "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)
    60 
    61 translations
    62   "[x, xs]" == "x#[xs]"
    63   "[x]" == "x#[]"
    64   "[x<-xs . P]"== "filter (%x. P) xs"
    65 
    66   "_LUpdate xs (_lupdbinds b bs)"== "_LUpdate (_LUpdate xs b) bs"
    67   "xs[i:=x]" == "list_update xs i x"
    68 
    69 
    70 syntax (xsymbols)
    71   "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    72 syntax (HTML output)
    73   "@filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
    74 
    75 
    76 text {*
    77   Function @{text size} is overloaded for all datatypes. Users may
    78   refer to the list version as @{text length}. *}
    79 
    80 abbreviation
    81   length :: "'a list => nat" where
    82   "length == size"
    83 
    84 primrec
    85   "hd(x#xs) = x"
    86 
    87 primrec
    88   "tl([]) = []"
    89   "tl(x#xs) = xs"
    90 
    91 primrec
    92   "last(x#xs) = (if xs=[] then x else last xs)"
    93 
    94 primrec
    95   "butlast []= []"
    96   "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
    97 
    98 primrec
    99   "set [] = {}"
   100   "set (x#xs) = insert x (set xs)"
   101 
   102 primrec
   103   "map f [] = []"
   104   "map f (x#xs) = f(x)#map f xs"
   105 
   106 primrec
   107   append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
   108 where
   109   append_Nil:"[] @ ys = ys"
   110   | append_Cons: "(x#xs) @ ys = x # xs @ ys"
   111 
   112 primrec
   113   "rev([]) = []"
   114   "rev(x#xs) = rev(xs) @ [x]"
   115 
   116 primrec
   117   "filter P [] = []"
   118   "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
   119 
   120 primrec
   121   foldl_Nil:"foldl f a [] = a"
   122   foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
   123 
   124 primrec
   125   "foldr f [] a = a"
   126   "foldr f (x#xs) a = f x (foldr f xs a)"
   127 
   128 primrec
   129   "concat([]) = []"
   130   "concat(x#xs) = x @ concat(xs)"
   131 
   132 primrec
   133 "listsum [] = 0"
   134 "listsum (x # xs) = x + listsum xs"
   135 
   136 primrec
   137   drop_Nil:"drop n [] = []"
   138   drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
   139   -- {*Warning: simpset does not contain this definition, but separate
   140        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   141 
   142 primrec
   143   take_Nil:"take n [] = []"
   144   take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
   145   -- {*Warning: simpset does not contain this definition, but separate
   146        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   147 
   148 primrec nth :: "'a list => nat => 'a" (infixl "!" 100) where
   149   nth_Cons: "(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
   150   -- {*Warning: simpset does not contain this definition, but separate
   151        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
   152 
   153 primrec
   154   "[][i:=v] = []"
   155   "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
   156 
   157 primrec
   158   "takeWhile P [] = []"
   159   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
   160 
   161 primrec
   162   "dropWhile P [] = []"
   163   "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
   164 
   165 primrec
   166   "zip xs [] = []"
   167   zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
   168   -- {*Warning: simpset does not contain this definition, but separate
   169        theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
   170 
   171 primrec
   172   upt_0: "[i..<0] = []"
   173   upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"
   174 
   175 primrec
   176   "distinct [] = True"
   177   "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
   178 
   179 primrec
   180   "remdups [] = []"
   181   "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
   182 
   183 primrec
   184   "remove1 x [] = []"
   185   "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
   186 
   187 primrec
   188   "removeAll x [] = []"
   189   "removeAll x (y#xs) = (if x=y then removeAll x xs else y # removeAll x xs)"
   190 
   191 primrec
   192   replicate_0: "replicate 0 x = []"
   193   replicate_Suc: "replicate (Suc n) x = x # replicate n x"
   194 
   195 definition
   196   rotate1 :: "'a list \<Rightarrow> 'a list" where
   197   "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
   198 
   199 definition
   200   rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   201   "rotate n = rotate1 ^^ n"
   202 
   203 definition
   204   list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where
   205   [code del]: "list_all2 P xs ys =
   206     (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"
   207 
   208 definition
   209   sublist :: "'a list => nat set => 'a list" where
   210   "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"
   211 
   212 primrec
   213   "splice [] ys = ys"
   214   "splice (x#xs) ys = (if ys=[] then x#xs else x # hd ys # splice xs (tl ys))"
   215     -- {*Warning: simpset does not contain the second eqn but a derived one. *}
   216 
   217 text{*
   218 \begin{figure}[htbp]
   219 \fbox{
   220 \begin{tabular}{l}
   221 @{lemma "[a,b]@[c,d] = [a,b,c,d]" by simp}\\
   222 @{lemma "length [a,b,c] = 3" by simp}\\
   223 @{lemma "set [a,b,c] = {a,b,c}" by simp}\\
   224 @{lemma "map f [a,b,c] = [f a, f b, f c]" by simp}\\
   225 @{lemma "rev [a,b,c] = [c,b,a]" by simp}\\
   226 @{lemma "hd [a,b,c,d] = a" by simp}\\
   227 @{lemma "tl [a,b,c,d] = [b,c,d]" by simp}\\
   228 @{lemma "last [a,b,c,d] = d" by simp}\\
   229 @{lemma "butlast [a,b,c,d] = [a,b,c]" by simp}\\
   230 @{lemma[source] "filter (\<lambda>n::nat. n<2) [0,2,1] = [0,1]" by simp}\\
   231 @{lemma "concat [[a,b],[c,d,e],[],[f]] = [a,b,c,d,e,f]" by simp}\\
   232 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
   233 @{lemma "foldr f [a,b,c] x = f a (f b (f c x))" by simp}\\
   234 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
   235 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
   236 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
   237 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
   238 @{lemma "take 2 [a,b,c,d] = [a,b]" by simp}\\
   239 @{lemma "take 6 [a,b,c,d] = [a,b,c,d]" by simp}\\
   240 @{lemma "drop 2 [a,b,c,d] = [c,d]" by simp}\\
   241 @{lemma "drop 6 [a,b,c,d] = []" by simp}\\
   242 @{lemma "takeWhile (%n::nat. n<3) [1,2,3,0] = [1,2]" by simp}\\
   243 @{lemma "dropWhile (%n::nat. n<3) [1,2,3,0] = [3,0]" by simp}\\
   244 @{lemma "distinct [2,0,1::nat]" by simp}\\
   245 @{lemma "remdups [2,0,2,1::nat,2] = [0,1,2]" by simp}\\
   246 @{lemma "remove1 2 [2,0,2,1::nat,2] = [0,2,1,2]" by simp}\\
   247 @{lemma "removeAll 2 [2,0,2,1::nat,2] = [0,1]" by simp}\\
   248 @{lemma "nth [a,b,c,d] 2 = c" by simp}\\
   249 @{lemma "[a,b,c,d][2 := x] = [a,b,x,d]" by simp}\\
   250 @{lemma "sublist [a,b,c,d,e] {0,2,3} = [a,c,d]" by (simp add:sublist_def)}\\
   251 @{lemma "rotate1 [a,b,c,d] = [b,c,d,a]" by (simp add:rotate1_def)}\\
   252 @{lemma "rotate 3 [a,b,c,d] = [d,a,b,c]" by (simp add:rotate1_def rotate_def nat_number)}\\
   253 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number)}\\
   254 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number)}\\
   255 @{lemma "listsum [1,2,3::nat] = 6" by simp}
   256 \end{tabular}}
   257 \caption{Characteristic examples}
   258 \label{fig:Characteristic}
   259 \end{figure}
   260 Figure~\ref{fig:Characteristic} shows characteristic examples
   261 that should give an intuitive understanding of the above functions.
   262 *}
   263 
   264 text{* The following simple sort functions are intended for proofs,
   265 not for efficient implementations. *}
   266 
   267 context linorder
   268 begin
   269 
   270 fun sorted :: "'a list \<Rightarrow> bool" where
   271 "sorted [] \<longleftrightarrow> True" |
   272 "sorted [x] \<longleftrightarrow> True" |
   273 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
   274 
   275 primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
   276 "insort x [] = [x]" |
   277 "insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
   278 
   279 primrec sort :: "'a list \<Rightarrow> 'a list" where
   280 "sort [] = []" |
   281 "sort (x#xs) = insort x (sort xs)"
   282 
   283 end
   284 
   285 
   286 subsubsection {* List comprehension *}
   287 
   288 text{* Input syntax for Haskell-like list comprehension notation.
   289 Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},
   290 the list of all pairs of distinct elements from @{text xs} and @{text ys}.
   291 The syntax is as in Haskell, except that @{text"|"} becomes a dot
   292 (like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than
   293 \verb![e| x <- xs, ...]!.
   294 
   295 The qualifiers after the dot are
   296 \begin{description}
   297 \item[generators] @{text"p \<leftarrow> xs"},
   298  where @{text p} is a pattern and @{text xs} an expression of list type, or
   299 \item[guards] @{text"b"}, where @{text b} is a boolean expression.
   300 %\item[local bindings] @ {text"let x = e"}.
   301 \end{description}
   302 
   303 Just like in Haskell, list comprehension is just a shorthand. To avoid
   304 misunderstandings, the translation into desugared form is not reversed
   305 upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
   306 optmized to @{term"map (%x. e) xs"}.
   307 
   308 It is easy to write short list comprehensions which stand for complex
   309 expressions. During proofs, they may become unreadable (and
   310 mangled). In such cases it can be advisable to introduce separate
   311 definitions for the list comprehensions in question.  *}
   312 
   313 (*
   314 Proper theorem proving support would be nice. For example, if
   315 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}
   316 produced something like
   317 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.
   318 *)
   319 
   320 nonterminals lc_qual lc_quals
   321 
   322 syntax
   323 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
   324 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
   325 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
   326 (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
   327 "_lc_end" :: "lc_quals" ("]")
   328 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
   329 "_lc_abs" :: "'a => 'b list => 'b list"
   330 
   331 (* These are easier than ML code but cannot express the optimized
   332    translation of [e. p<-xs]
   333 translations
   334 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
   335 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
   336  => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
   337 "[e. P]" => "if P then [e] else []"
   338 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
   339  => "if P then (_listcompr e Q Qs) else []"
   340 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
   341  => "_Let b (_listcompr e Q Qs)"
   342 *)
   343 
   344 syntax (xsymbols)
   345 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
   346 syntax (HTML output)
   347 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
   348 
   349 parse_translation (advanced) {*
   350 let
   351   val NilC = Syntax.const @{const_name Nil};
   352   val ConsC = Syntax.const @{const_name Cons};
   353   val mapC = Syntax.const @{const_name map};
   354   val concatC = Syntax.const @{const_name concat};
   355   val IfC = Syntax.const @{const_name If};
   356   fun singl x = ConsC $ x $ NilC;
   357 
   358    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
   359     let
   360       val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);
   361       val e = if opti then singl e else e;
   362       val case1 = Syntax.const "_case1" $ p $ e;
   363       val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
   364                                         $ NilC;
   365       val cs = Syntax.const "_case2" $ case1 $ case2
   366       val ft = DatatypeCase.case_tr false Datatype.info_of_constr
   367                  ctxt [x, cs]
   368     in lambda x ft end;
   369 
   370   fun abs_tr ctxt (p as Free(s,T)) e opti =
   371         let val thy = ProofContext.theory_of ctxt;
   372             val s' = Sign.intern_const thy s
   373         in if Sign.declared_const thy s'
   374            then (pat_tr ctxt p e opti, false)
   375            else (lambda p e, true)
   376         end
   377     | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
   378 
   379   fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
   380         let val res = case qs of Const("_lc_end",_) => singl e
   381                       | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
   382         in IfC $ b $ res $ NilC end
   383     | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
   384         (case abs_tr ctxt p e true of
   385            (f,true) => mapC $ f $ es
   386          | (f, false) => concatC $ (mapC $ f $ es))
   387     | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
   388         let val e' = lc_tr ctxt [e,q,qs];
   389         in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
   390 
   391 in [("_listcompr", lc_tr)] end
   392 *}
   393 
   394 (*
   395 term "[(x,y,z). b]"
   396 term "[(x,y,z). x\<leftarrow>xs]"
   397 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
   398 term "[(x,y,z). x<a, x>b]"
   399 term "[(x,y,z). x\<leftarrow>xs, x>b]"
   400 term "[(x,y,z). x<a, x\<leftarrow>xs]"
   401 term "[(x,y). Cons True x \<leftarrow> xs]"
   402 term "[(x,y,z). Cons x [] \<leftarrow> xs]"
   403 term "[(x,y,z). x<a, x>b, x=d]"
   404 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
   405 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
   406 term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"
   407 term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"
   408 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"
   409 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"
   410 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"
   411 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
   412 *)
   413 
   414 subsubsection {* @{const Nil} and @{const Cons} *}
   415 
   416 lemma not_Cons_self [simp]:
   417   "xs \<noteq> x # xs"
   418 by (induct xs) auto
   419 
   420 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]
   421 
   422 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"
   423 by (induct xs) auto
   424 
   425 lemma length_induct:
   426   "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"
   427 by (rule measure_induct [of length]) iprover
   428 
   429 
   430 subsubsection {* @{const length} *}
   431 
   432 text {*
   433   Needs to come before @{text "@"} because of theorem @{text
   434   append_eq_append_conv}.
   435 *}
   436 
   437 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"
   438 by (induct xs) auto
   439 
   440 lemma length_map [simp]: "length (map f xs) = length xs"
   441 by (induct xs) auto
   442 
   443 lemma length_rev [simp]: "length (rev xs) = length xs"
   444 by (induct xs) auto
   445 
   446 lemma length_tl [simp]: "length (tl xs) = length xs - 1"
   447 by (cases xs) auto
   448 
   449 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"
   450 by (induct xs) auto
   451 
   452 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"
   453 by (induct xs) auto
   454 
   455 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"
   456 by auto
   457 
   458 lemma length_Suc_conv:
   459 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
   460 by (induct xs) auto
   461 
   462 lemma Suc_length_conv:
   463 "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"
   464 apply (induct xs, simp, simp)
   465 apply blast
   466 done
   467 
   468 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"
   469   by (induct xs) auto
   470 
   471 lemma list_induct2 [consumes 1, case_names Nil Cons]:
   472   "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>
   473    (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))
   474    \<Longrightarrow> P xs ys"
   475 proof (induct xs arbitrary: ys)
   476   case Nil then show ?case by simp
   477 next
   478   case (Cons x xs ys) then show ?case by (cases ys) simp_all
   479 qed
   480 
   481 lemma list_induct3 [consumes 2, case_names Nil Cons]:
   482   "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>
   483    (\<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))
   484    \<Longrightarrow> P xs ys zs"
   485 proof (induct xs arbitrary: ys zs)
   486   case Nil then show ?case by simp
   487 next
   488   case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)
   489     (cases zs, simp_all)
   490 qed
   491 
   492 lemma list_induct2': 
   493   "\<lbrakk> P [] [];
   494   \<And>x xs. P (x#xs) [];
   495   \<And>y ys. P [] (y#ys);
   496    \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>
   497  \<Longrightarrow> P xs ys"
   498 by (induct xs arbitrary: ys) (case_tac x, auto)+
   499 
   500 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"
   501 by (rule Eq_FalseI) auto
   502 
   503 simproc_setup list_neq ("(xs::'a list) = ys") = {*
   504 (*
   505 Reduces xs=ys to False if xs and ys cannot be of the same length.
   506 This is the case if the atomic sublists of one are a submultiset
   507 of those of the other list and there are fewer Cons's in one than the other.
   508 *)
   509 
   510 let
   511 
   512 fun len (Const(@{const_name Nil},_)) acc = acc
   513   | len (Const(@{const_name Cons},_) $ _ $ xs) (ts,n) = len xs (ts,n+1)
   514   | len (Const(@{const_name append},_) $ xs $ ys) acc = len xs (len ys acc)
   515   | len (Const(@{const_name rev},_) $ xs) acc = len xs acc
   516   | len (Const(@{const_name map},_) $ _ $ xs) acc = len xs acc
   517   | len t (ts,n) = (t::ts,n);
   518 
   519 fun list_neq _ ss ct =
   520   let
   521     val (Const(_,eqT) $ lhs $ rhs) = Thm.term_of ct;
   522     val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);
   523     fun prove_neq() =
   524       let
   525         val Type(_,listT::_) = eqT;
   526         val size = HOLogic.size_const listT;
   527         val eq_len = HOLogic.mk_eq (size $ lhs, size $ rhs);
   528         val neq_len = HOLogic.mk_Trueprop (HOLogic.Not $ eq_len);
   529         val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len
   530           (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));
   531       in SOME (thm RS @{thm neq_if_length_neq}) end
   532   in
   533     if m < n andalso submultiset (op aconv) (ls,rs) orelse
   534        n < m andalso submultiset (op aconv) (rs,ls)
   535     then prove_neq() else NONE
   536   end;
   537 in list_neq end;
   538 *}
   539 
   540 
   541 subsubsection {* @{text "@"} -- append *}
   542 
   543 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"
   544 by (induct xs) auto
   545 
   546 lemma append_Nil2 [simp]: "xs @ [] = xs"
   547 by (induct xs) auto
   548 
   549 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
   550 by (induct xs) auto
   551 
   552 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"
   553 by (induct xs) auto
   554 
   555 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"
   556 by (induct xs) auto
   557 
   558 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"
   559 by (induct xs) auto
   560 
   561 lemma append_eq_append_conv [simp, noatp]:
   562  "length xs = length ys \<or> length us = length vs
   563  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"
   564 apply (induct xs arbitrary: ys)
   565  apply (case_tac ys, simp, force)
   566 apply (case_tac ys, force, simp)
   567 done
   568 
   569 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =
   570   (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"
   571 apply (induct xs arbitrary: ys zs ts)
   572  apply fastsimp
   573 apply(case_tac zs)
   574  apply simp
   575 apply fastsimp
   576 done
   577 
   578 lemma same_append_eq [iff]: "(xs @ ys = xs @ zs) = (ys = zs)"
   579 by simp
   580 
   581 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"
   582 by simp
   583 
   584 lemma append_same_eq [iff]: "(ys @ xs = zs @ xs) = (ys = zs)"
   585 by simp
   586 
   587 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"
   588 using append_same_eq [of _ _ "[]"] by auto
   589 
   590 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"
   591 using append_same_eq [of "[]"] by auto
   592 
   593 lemma hd_Cons_tl [simp,noatp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"
   594 by (induct xs) auto
   595 
   596 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"
   597 by (induct xs) auto
   598 
   599 lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"
   600 by (simp add: hd_append split: list.split)
   601 
   602 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"
   603 by (simp split: list.split)
   604 
   605 lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"
   606 by (simp add: tl_append split: list.split)
   607 
   608 
   609 lemma Cons_eq_append_conv: "x#xs = ys@zs =
   610  (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"
   611 by(cases ys) auto
   612 
   613 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =
   614  (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"
   615 by(cases ys) auto
   616 
   617 
   618 text {* Trivial rules for solving @{text "@"}-equations automatically. *}
   619 
   620 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
   621 by simp
   622 
   623 lemma Cons_eq_appendI:
   624 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"
   625 by (drule sym) simp
   626 
   627 lemma append_eq_appendI:
   628 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"
   629 by (drule sym) simp
   630 
   631 
   632 text {*
   633 Simplification procedure for all list equalities.
   634 Currently only tries to rearrange @{text "@"} to see if
   635 - both lists end in a singleton list,
   636 - or both lists end in the same list.
   637 *}
   638 
   639 ML {*
   640 local
   641 
   642 fun last (cons as Const(@{const_name Cons},_) $ _ $ xs) =
   643   (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)
   644   | last (Const(@{const_name append},_) $ _ $ ys) = last ys
   645   | last t = t;
   646 
   647 fun list1 (Const(@{const_name Cons},_) $ _ $ Const(@{const_name Nil},_)) = true
   648   | list1 _ = false;
   649 
   650 fun butlast ((cons as Const(@{const_name Cons},_) $ x) $ xs) =
   651   (case xs of Const(@{const_name Nil},_) => xs | _ => cons $ butlast xs)
   652   | butlast ((app as Const(@{const_name append},_) $ xs) $ ys) = app $ butlast ys
   653   | butlast xs = Const(@{const_name Nil},fastype_of xs);
   654 
   655 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},
   656   @{thm append_Nil}, @{thm append_Cons}];
   657 
   658 fun list_eq ss (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
   659   let
   660     val lastl = last lhs and lastr = last rhs;
   661     fun rearr conv =
   662       let
   663         val lhs1 = butlast lhs and rhs1 = butlast rhs;
   664         val Type(_,listT::_) = eqT
   665         val appT = [listT,listT] ---> listT
   666         val app = Const(@{const_name append},appT)
   667         val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
   668         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
   669         val thm = Goal.prove (Simplifier.the_context ss) [] [] eq
   670           (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
   671       in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;
   672 
   673   in
   674     if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}
   675     else if lastl aconv lastr then rearr @{thm append_same_eq}
   676     else NONE
   677   end;
   678 
   679 in
   680 
   681 val list_eq_simproc =
   682   Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);
   683 
   684 end;
   685 
   686 Addsimprocs [list_eq_simproc];
   687 *}
   688 
   689 
   690 subsubsection {* @{text map} *}
   691 
   692 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"
   693 by (induct xs) simp_all
   694 
   695 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"
   696 by (rule ext, induct_tac xs) auto
   697 
   698 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"
   699 by (induct xs) auto
   700 
   701 lemma map_compose: "map (f o g) xs = map f (map g xs)"
   702 by (induct xs) (auto simp add: o_def)
   703 
   704 lemma rev_map: "rev (map f xs) = map f (rev xs)"
   705 by (induct xs) auto
   706 
   707 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"
   708 by (induct xs) auto
   709 
   710 lemma map_cong [fundef_cong, recdef_cong]:
   711 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"
   712 -- {* a congruence rule for @{text map} *}
   713 by simp
   714 
   715 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"
   716 by (cases xs) auto
   717 
   718 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"
   719 by (cases xs) auto
   720 
   721 lemma map_eq_Cons_conv:
   722  "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"
   723 by (cases xs) auto
   724 
   725 lemma Cons_eq_map_conv:
   726  "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"
   727 by (cases ys) auto
   728 
   729 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]
   730 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]
   731 declare map_eq_Cons_D [dest!]  Cons_eq_map_D [dest!]
   732 
   733 lemma ex_map_conv:
   734   "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"
   735 by(induct ys, auto simp add: Cons_eq_map_conv)
   736 
   737 lemma map_eq_imp_length_eq:
   738   assumes "map f xs = map f ys"
   739   shows "length xs = length ys"
   740 using assms proof (induct ys arbitrary: xs)
   741   case Nil then show ?case by simp
   742 next
   743   case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto
   744   from Cons xs have "map f zs = map f ys" by simp
   745   moreover with Cons have "length zs = length ys" by blast
   746   with xs show ?case by simp
   747 qed
   748   
   749 lemma map_inj_on:
   750  "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]
   751   ==> xs = ys"
   752 apply(frule map_eq_imp_length_eq)
   753 apply(rotate_tac -1)
   754 apply(induct rule:list_induct2)
   755  apply simp
   756 apply(simp)
   757 apply (blast intro:sym)
   758 done
   759 
   760 lemma inj_on_map_eq_map:
   761  "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
   762 by(blast dest:map_inj_on)
   763 
   764 lemma map_injective:
   765  "map f xs = map f ys ==> inj f ==> xs = ys"
   766 by (induct ys arbitrary: xs) (auto dest!:injD)
   767 
   768 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"
   769 by(blast dest:map_injective)
   770 
   771 lemma inj_mapI: "inj f ==> inj (map f)"
   772 by (iprover dest: map_injective injD intro: inj_onI)
   773 
   774 lemma inj_mapD: "inj (map f) ==> inj f"
   775 apply (unfold inj_on_def, clarify)
   776 apply (erule_tac x = "[x]" in ballE)
   777  apply (erule_tac x = "[y]" in ballE, simp, blast)
   778 apply blast
   779 done
   780 
   781 lemma inj_map[iff]: "inj (map f) = inj f"
   782 by (blast dest: inj_mapD intro: inj_mapI)
   783 
   784 lemma inj_on_mapI: "inj_on f (\<Union>(set ` A)) \<Longrightarrow> inj_on (map f) A"
   785 apply(rule inj_onI)
   786 apply(erule map_inj_on)
   787 apply(blast intro:inj_onI dest:inj_onD)
   788 done
   789 
   790 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"
   791 by (induct xs, auto)
   792 
   793 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"
   794 by (induct xs) auto
   795 
   796 lemma map_fst_zip[simp]:
   797   "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"
   798 by (induct rule:list_induct2, simp_all)
   799 
   800 lemma map_snd_zip[simp]:
   801   "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
   802 by (induct rule:list_induct2, simp_all)
   803 
   804 
   805 subsubsection {* @{text rev} *}
   806 
   807 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"
   808 by (induct xs) auto
   809 
   810 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"
   811 by (induct xs) auto
   812 
   813 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"
   814 by auto
   815 
   816 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"
   817 by (induct xs) auto
   818 
   819 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"
   820 by (induct xs) auto
   821 
   822 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"
   823 by (cases xs) auto
   824 
   825 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"
   826 by (cases xs) auto
   827 
   828 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"
   829 apply (induct xs arbitrary: ys, force)
   830 apply (case_tac ys, simp, force)
   831 done
   832 
   833 lemma inj_on_rev[iff]: "inj_on rev A"
   834 by(simp add:inj_on_def)
   835 
   836 lemma rev_induct [case_names Nil snoc]:
   837   "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"
   838 apply(simplesubst rev_rev_ident[symmetric])
   839 apply(rule_tac list = "rev xs" in list.induct, simp_all)
   840 done
   841 
   842 lemma rev_exhaust [case_names Nil snoc]:
   843   "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"
   844 by (induct xs rule: rev_induct) auto
   845 
   846 lemmas rev_cases = rev_exhaust
   847 
   848 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"
   849 by(rule rev_cases[of xs]) auto
   850 
   851 
   852 subsubsection {* @{text set} *}
   853 
   854 lemma finite_set [iff]: "finite (set xs)"
   855 by (induct xs) auto
   856 
   857 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"
   858 by (induct xs) auto
   859 
   860 lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"
   861 by(cases xs) auto
   862 
   863 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"
   864 by auto
   865 
   866 lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs" 
   867 by auto
   868 
   869 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"
   870 by (induct xs) auto
   871 
   872 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"
   873 by(induct xs) auto
   874 
   875 lemma set_rev [simp]: "set (rev xs) = set xs"
   876 by (induct xs) auto
   877 
   878 lemma set_map [simp]: "set (map f xs) = f`(set xs)"
   879 by (induct xs) auto
   880 
   881 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"
   882 by (induct xs) auto
   883 
   884 lemma set_upt [simp]: "set[i..<j] = {k. i \<le> k \<and> k < j}"
   885 apply (induct j, simp_all)
   886 apply (erule ssubst, auto)
   887 done
   888 
   889 
   890 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
   891 proof (induct xs)
   892   case Nil thus ?case by simp
   893 next
   894   case Cons thus ?case by (auto intro: Cons_eq_appendI)
   895 qed
   896 
   897 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
   898   by (auto elim: split_list)
   899 
   900 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
   901 proof (induct xs)
   902   case Nil thus ?case by simp
   903 next
   904   case (Cons a xs)
   905   show ?case
   906   proof cases
   907     assume "x = a" thus ?case using Cons by fastsimp
   908   next
   909     assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
   910   qed
   911 qed
   912 
   913 lemma in_set_conv_decomp_first:
   914   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
   915   by (auto dest!: split_list_first)
   916 
   917 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
   918 proof (induct xs rule:rev_induct)
   919   case Nil thus ?case by simp
   920 next
   921   case (snoc a xs)
   922   show ?case
   923   proof cases
   924     assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
   925   next
   926     assume "x \<noteq> a" thus ?case using snoc by fastsimp
   927   qed
   928 qed
   929 
   930 lemma in_set_conv_decomp_last:
   931   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
   932   by (auto dest!: split_list_last)
   933 
   934 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
   935 proof (induct xs)
   936   case Nil thus ?case by simp
   937 next
   938   case Cons thus ?case
   939     by(simp add:Bex_def)(metis append_Cons append.simps(1))
   940 qed
   941 
   942 lemma split_list_propE:
   943   assumes "\<exists>x \<in> set xs. P x"
   944   obtains ys x zs where "xs = ys @ x # zs" and "P x"
   945 using split_list_prop [OF assms] by blast
   946 
   947 lemma split_list_first_prop:
   948   "\<exists>x \<in> set xs. P x \<Longrightarrow>
   949    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
   950 proof (induct xs)
   951   case Nil thus ?case by simp
   952 next
   953   case (Cons x xs)
   954   show ?case
   955   proof cases
   956     assume "P x"
   957     thus ?thesis by simp
   958       (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
   959   next
   960     assume "\<not> P x"
   961     hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
   962     thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
   963   qed
   964 qed
   965 
   966 lemma split_list_first_propE:
   967   assumes "\<exists>x \<in> set xs. P x"
   968   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
   969 using split_list_first_prop [OF assms] by blast
   970 
   971 lemma split_list_first_prop_iff:
   972   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
   973    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
   974 by (rule, erule split_list_first_prop) auto
   975 
   976 lemma split_list_last_prop:
   977   "\<exists>x \<in> set xs. P x \<Longrightarrow>
   978    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
   979 proof(induct xs rule:rev_induct)
   980   case Nil thus ?case by simp
   981 next
   982   case (snoc x xs)
   983   show ?case
   984   proof cases
   985     assume "P x" thus ?thesis by (metis emptyE set_empty)
   986   next
   987     assume "\<not> P x"
   988     hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
   989     thus ?thesis using `\<not> P x` snoc(1) by fastsimp
   990   qed
   991 qed
   992 
   993 lemma split_list_last_propE:
   994   assumes "\<exists>x \<in> set xs. P x"
   995   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
   996 using split_list_last_prop [OF assms] by blast
   997 
   998 lemma split_list_last_prop_iff:
   999   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
  1000    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
  1001 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
  1002 
  1003 lemma finite_list: "finite A ==> EX xs. set xs = A"
  1004   by (erule finite_induct)
  1005     (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
  1006 
  1007 lemma card_length: "card (set xs) \<le> length xs"
  1008 by (induct xs) (auto simp add: card_insert_if)
  1009 
  1010 lemma set_minus_filter_out:
  1011   "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
  1012   by (induct xs) auto
  1013 
  1014 subsubsection {* @{text filter} *}
  1015 
  1016 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
  1017 by (induct xs) auto
  1018 
  1019 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
  1020 by (induct xs) simp_all
  1021 
  1022 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
  1023 by (induct xs) auto
  1024 
  1025 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
  1026 by (induct xs) (auto simp add: le_SucI)
  1027 
  1028 lemma sum_length_filter_compl:
  1029   "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
  1030 by(induct xs) simp_all
  1031 
  1032 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
  1033 by (induct xs) auto
  1034 
  1035 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
  1036 by (induct xs) auto
  1037 
  1038 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
  1039 by (induct xs) simp_all
  1040 
  1041 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
  1042 apply (induct xs)
  1043  apply auto
  1044 apply(cut_tac P=P and xs=xs in length_filter_le)
  1045 apply simp
  1046 done
  1047 
  1048 lemma filter_map:
  1049   "filter P (map f xs) = map f (filter (P o f) xs)"
  1050 by (induct xs) simp_all
  1051 
  1052 lemma length_filter_map[simp]:
  1053   "length (filter P (map f xs)) = length(filter (P o f) xs)"
  1054 by (simp add:filter_map)
  1055 
  1056 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
  1057 by auto
  1058 
  1059 lemma length_filter_less:
  1060   "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
  1061 proof (induct xs)
  1062   case Nil thus ?case by simp
  1063 next
  1064   case (Cons x xs) thus ?case
  1065     apply (auto split:split_if_asm)
  1066     using length_filter_le[of P xs] apply arith
  1067   done
  1068 qed
  1069 
  1070 lemma length_filter_conv_card:
  1071  "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
  1072 proof (induct xs)
  1073   case Nil thus ?case by simp
  1074 next
  1075   case (Cons x xs)
  1076   let ?S = "{i. i < length xs & p(xs!i)}"
  1077   have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
  1078   show ?case (is "?l = card ?S'")
  1079   proof (cases)
  1080     assume "p x"
  1081     hence eq: "?S' = insert 0 (Suc ` ?S)"
  1082       by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
  1083     have "length (filter p (x # xs)) = Suc(card ?S)"
  1084       using Cons `p x` by simp
  1085     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
  1086       by (simp add: card_image inj_Suc)
  1087     also have "\<dots> = card ?S'" using eq fin
  1088       by (simp add:card_insert_if) (simp add:image_def)
  1089     finally show ?thesis .
  1090   next
  1091     assume "\<not> p x"
  1092     hence eq: "?S' = Suc ` ?S"
  1093       by(auto simp add: image_def split:nat.split elim:lessE)
  1094     have "length (filter p (x # xs)) = card ?S"
  1095       using Cons `\<not> p x` by simp
  1096     also have "\<dots> = card(Suc ` ?S)" using fin
  1097       by (simp add: card_image inj_Suc)
  1098     also have "\<dots> = card ?S'" using eq fin
  1099       by (simp add:card_insert_if)
  1100     finally show ?thesis .
  1101   qed
  1102 qed
  1103 
  1104 lemma Cons_eq_filterD:
  1105  "x#xs = filter P ys \<Longrightarrow>
  1106   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  1107   (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
  1108 proof(induct ys)
  1109   case Nil thus ?case by simp
  1110 next
  1111   case (Cons y ys)
  1112   show ?case (is "\<exists>x. ?Q x")
  1113   proof cases
  1114     assume Py: "P y"
  1115     show ?thesis
  1116     proof cases
  1117       assume "x = y"
  1118       with Py Cons.prems have "?Q []" by simp
  1119       then show ?thesis ..
  1120     next
  1121       assume "x \<noteq> y"
  1122       with Py Cons.prems show ?thesis by simp
  1123     qed
  1124   next
  1125     assume "\<not> P y"
  1126     with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
  1127     then have "?Q (y#us)" by simp
  1128     then show ?thesis ..
  1129   qed
  1130 qed
  1131 
  1132 lemma filter_eq_ConsD:
  1133  "filter P ys = x#xs \<Longrightarrow>
  1134   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  1135 by(rule Cons_eq_filterD) simp
  1136 
  1137 lemma filter_eq_Cons_iff:
  1138  "(filter P ys = x#xs) =
  1139   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
  1140 by(auto dest:filter_eq_ConsD)
  1141 
  1142 lemma Cons_eq_filter_iff:
  1143  "(x#xs = filter P ys) =
  1144   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
  1145 by(auto dest:Cons_eq_filterD)
  1146 
  1147 lemma filter_cong[fundef_cong, recdef_cong]:
  1148  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
  1149 apply simp
  1150 apply(erule thin_rl)
  1151 by (induct ys) simp_all
  1152 
  1153 
  1154 subsubsection {* List partitioning *}
  1155 
  1156 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
  1157   "partition P [] = ([], [])"
  1158   | "partition P (x # xs) = 
  1159       (let (yes, no) = partition P xs
  1160       in if P x then (x # yes, no) else (yes, x # no))"
  1161 
  1162 lemma partition_filter1:
  1163     "fst (partition P xs) = filter P xs"
  1164 by (induct xs) (auto simp add: Let_def split_def)
  1165 
  1166 lemma partition_filter2:
  1167     "snd (partition P xs) = filter (Not o P) xs"
  1168 by (induct xs) (auto simp add: Let_def split_def)
  1169 
  1170 lemma partition_P:
  1171   assumes "partition P xs = (yes, no)"
  1172   shows "(\<forall>p \<in> set yes.  P p) \<and> (\<forall>p  \<in> set no. \<not> P p)"
  1173 proof -
  1174   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
  1175     by simp_all
  1176   then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
  1177 qed
  1178 
  1179 lemma partition_set:
  1180   assumes "partition P xs = (yes, no)"
  1181   shows "set yes \<union> set no = set xs"
  1182 proof -
  1183   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
  1184     by simp_all
  1185   then show ?thesis by (auto simp add: partition_filter1 partition_filter2) 
  1186 qed
  1187 
  1188 
  1189 subsubsection {* @{text concat} *}
  1190 
  1191 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
  1192 by (induct xs) auto
  1193 
  1194 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
  1195 by (induct xss) auto
  1196 
  1197 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
  1198 by (induct xss) auto
  1199 
  1200 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
  1201 by (induct xs) auto
  1202 
  1203 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
  1204 by (induct xs) auto
  1205 
  1206 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
  1207 by (induct xs) auto
  1208 
  1209 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
  1210 by (induct xs) auto
  1211 
  1212 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
  1213 by (induct xs) auto
  1214 
  1215 
  1216 subsubsection {* @{text nth} *}
  1217 
  1218 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
  1219 by auto
  1220 
  1221 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
  1222 by auto
  1223 
  1224 declare nth.simps [simp del]
  1225 
  1226 lemma nth_append:
  1227   "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
  1228 apply (induct xs arbitrary: n, simp)
  1229 apply (case_tac n, auto)
  1230 done
  1231 
  1232 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
  1233 by (induct xs) auto
  1234 
  1235 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
  1236 by (induct xs) auto
  1237 
  1238 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
  1239 apply (induct xs arbitrary: n, simp)
  1240 apply (case_tac n, auto)
  1241 done
  1242 
  1243 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
  1244 by(cases xs) simp_all
  1245 
  1246 
  1247 lemma list_eq_iff_nth_eq:
  1248  "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
  1249 apply(induct xs arbitrary: ys)
  1250  apply force
  1251 apply(case_tac ys)
  1252  apply simp
  1253 apply(simp add:nth_Cons split:nat.split)apply blast
  1254 done
  1255 
  1256 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
  1257 apply (induct xs, simp, simp)
  1258 apply safe
  1259 apply (metis nat_case_0 nth.simps zero_less_Suc)
  1260 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
  1261 apply (case_tac i, simp)
  1262 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
  1263 done
  1264 
  1265 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
  1266 by(auto simp:set_conv_nth)
  1267 
  1268 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
  1269 by (auto simp add: set_conv_nth)
  1270 
  1271 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
  1272 by (auto simp add: set_conv_nth)
  1273 
  1274 lemma all_nth_imp_all_set:
  1275 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
  1276 by (auto simp add: set_conv_nth)
  1277 
  1278 lemma all_set_conv_all_nth:
  1279 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
  1280 by (auto simp add: set_conv_nth)
  1281 
  1282 lemma rev_nth:
  1283   "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
  1284 proof (induct xs arbitrary: n)
  1285   case Nil thus ?case by simp
  1286 next
  1287   case (Cons x xs)
  1288   hence n: "n < Suc (length xs)" by simp
  1289   moreover
  1290   { assume "n < length xs"
  1291     with n obtain n' where "length xs - n = Suc n'"
  1292       by (cases "length xs - n", auto)
  1293     moreover
  1294     then have "length xs - Suc n = n'" by simp
  1295     ultimately
  1296     have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
  1297   }
  1298   ultimately
  1299   show ?case by (clarsimp simp add: Cons nth_append)
  1300 qed
  1301 
  1302 lemma Skolem_list_nth:
  1303   "(ALL i<k. EX x. P i x) = (EX xs. size xs = k & (ALL i<k. P i (xs!i)))"
  1304   (is "_ = (EX xs. ?P k xs)")
  1305 proof(induct k)
  1306   case 0 show ?case by simp
  1307 next
  1308   case (Suc k)
  1309   show ?case (is "?L = ?R" is "_ = (EX xs. ?P' xs)")
  1310   proof
  1311     assume "?R" thus "?L" using Suc by auto
  1312   next
  1313     assume "?L"
  1314     with Suc obtain x xs where "?P k xs & P k x" by (metis less_Suc_eq)
  1315     hence "?P'(xs@[x])" by(simp add:nth_append less_Suc_eq)
  1316     thus "?R" ..
  1317   qed
  1318 qed
  1319 
  1320 
  1321 subsubsection {* @{text list_update} *}
  1322 
  1323 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
  1324 by (induct xs arbitrary: i) (auto split: nat.split)
  1325 
  1326 lemma nth_list_update:
  1327 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
  1328 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
  1329 
  1330 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
  1331 by (simp add: nth_list_update)
  1332 
  1333 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
  1334 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
  1335 
  1336 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
  1337 by (induct xs arbitrary: i) (simp_all split:nat.splits)
  1338 
  1339 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
  1340 apply (induct xs arbitrary: i)
  1341  apply simp
  1342 apply (case_tac i)
  1343 apply simp_all
  1344 done
  1345 
  1346 lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
  1347 by(metis length_0_conv length_list_update)
  1348 
  1349 lemma list_update_same_conv:
  1350 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
  1351 by (induct xs arbitrary: i) (auto split: nat.split)
  1352 
  1353 lemma list_update_append1:
  1354  "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
  1355 apply (induct xs arbitrary: i, simp)
  1356 apply(simp split:nat.split)
  1357 done
  1358 
  1359 lemma list_update_append:
  1360   "(xs @ ys) [n:= x] = 
  1361   (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
  1362 by (induct xs arbitrary: n) (auto split:nat.splits)
  1363 
  1364 lemma list_update_length [simp]:
  1365  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
  1366 by (induct xs, auto)
  1367 
  1368 lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
  1369 by(induct xs arbitrary: k)(auto split:nat.splits)
  1370 
  1371 lemma rev_update:
  1372   "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
  1373 by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
  1374 
  1375 lemma update_zip:
  1376   "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
  1377 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
  1378 
  1379 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
  1380 by (induct xs arbitrary: i) (auto split: nat.split)
  1381 
  1382 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
  1383 by (blast dest!: set_update_subset_insert [THEN subsetD])
  1384 
  1385 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
  1386 by (induct xs arbitrary: n) (auto split:nat.splits)
  1387 
  1388 lemma list_update_overwrite[simp]:
  1389   "xs [i := x, i := y] = xs [i := y]"
  1390 apply (induct xs arbitrary: i) apply simp
  1391 apply (case_tac i, simp_all)
  1392 done
  1393 
  1394 lemma list_update_swap:
  1395   "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
  1396 apply (induct xs arbitrary: i i')
  1397 apply simp
  1398 apply (case_tac i, case_tac i')
  1399 apply auto
  1400 apply (case_tac i')
  1401 apply auto
  1402 done
  1403 
  1404 lemma list_update_code [code]:
  1405   "[][i := y] = []"
  1406   "(x # xs)[0 := y] = y # xs"
  1407   "(x # xs)[Suc i := y] = x # xs[i := y]"
  1408   by simp_all
  1409 
  1410 
  1411 subsubsection {* @{text last} and @{text butlast} *}
  1412 
  1413 lemma last_snoc [simp]: "last (xs @ [x]) = x"
  1414 by (induct xs) auto
  1415 
  1416 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
  1417 by (induct xs) auto
  1418 
  1419 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
  1420 by(simp add:last.simps)
  1421 
  1422 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
  1423 by(simp add:last.simps)
  1424 
  1425 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
  1426 by (induct xs) (auto)
  1427 
  1428 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
  1429 by(simp add:last_append)
  1430 
  1431 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
  1432 by(simp add:last_append)
  1433 
  1434 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
  1435 by(rule rev_exhaust[of xs]) simp_all
  1436 
  1437 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
  1438 by(cases xs) simp_all
  1439 
  1440 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
  1441 by (induct as) auto
  1442 
  1443 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
  1444 by (induct xs rule: rev_induct) auto
  1445 
  1446 lemma butlast_append:
  1447   "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
  1448 by (induct xs arbitrary: ys) auto
  1449 
  1450 lemma append_butlast_last_id [simp]:
  1451 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
  1452 by (induct xs) auto
  1453 
  1454 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
  1455 by (induct xs) (auto split: split_if_asm)
  1456 
  1457 lemma in_set_butlast_appendI:
  1458 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
  1459 by (auto dest: in_set_butlastD simp add: butlast_append)
  1460 
  1461 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
  1462 apply (induct xs arbitrary: n)
  1463  apply simp
  1464 apply (auto split:nat.split)
  1465 done
  1466 
  1467 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
  1468 by(induct xs)(auto simp:neq_Nil_conv)
  1469 
  1470 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
  1471 by (induct xs, simp, case_tac xs, simp_all)
  1472 
  1473 lemma last_list_update:
  1474   "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
  1475 by (auto simp: last_conv_nth)
  1476 
  1477 lemma butlast_list_update:
  1478   "butlast(xs[k:=x]) =
  1479  (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
  1480 apply(cases xs rule:rev_cases)
  1481 apply simp
  1482 apply(simp add:list_update_append split:nat.splits)
  1483 done
  1484 
  1485 
  1486 subsubsection {* @{text take} and @{text drop} *}
  1487 
  1488 lemma take_0 [simp]: "take 0 xs = []"
  1489 by (induct xs) auto
  1490 
  1491 lemma drop_0 [simp]: "drop 0 xs = xs"
  1492 by (induct xs) auto
  1493 
  1494 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
  1495 by simp
  1496 
  1497 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
  1498 by simp
  1499 
  1500 declare take_Cons [simp del] and drop_Cons [simp del]
  1501 
  1502 lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
  1503   unfolding One_nat_def by simp
  1504 
  1505 lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
  1506   unfolding One_nat_def by simp
  1507 
  1508 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
  1509 by(clarsimp simp add:neq_Nil_conv)
  1510 
  1511 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
  1512 by(cases xs, simp_all)
  1513 
  1514 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
  1515 by (induct xs arbitrary: n) simp_all
  1516 
  1517 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
  1518 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
  1519 
  1520 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
  1521 by (cases n, simp, cases xs, auto)
  1522 
  1523 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
  1524 by (simp only: drop_tl)
  1525 
  1526 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
  1527 apply (induct xs arbitrary: n, simp)
  1528 apply(simp add:drop_Cons nth_Cons split:nat.splits)
  1529 done
  1530 
  1531 lemma take_Suc_conv_app_nth:
  1532   "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
  1533 apply (induct xs arbitrary: i, simp)
  1534 apply (case_tac i, auto)
  1535 done
  1536 
  1537 lemma drop_Suc_conv_tl:
  1538   "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
  1539 apply (induct xs arbitrary: i, simp)
  1540 apply (case_tac i, auto)
  1541 done
  1542 
  1543 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
  1544 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1545 
  1546 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
  1547 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1548 
  1549 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
  1550 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1551 
  1552 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
  1553 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1554 
  1555 lemma take_append [simp]:
  1556   "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
  1557 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1558 
  1559 lemma drop_append [simp]:
  1560   "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
  1561 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1562 
  1563 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
  1564 apply (induct m arbitrary: xs n, auto)
  1565 apply (case_tac xs, auto)
  1566 apply (case_tac n, auto)
  1567 done
  1568 
  1569 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
  1570 apply (induct m arbitrary: xs, auto)
  1571 apply (case_tac xs, auto)
  1572 done
  1573 
  1574 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
  1575 apply (induct m arbitrary: xs n, auto)
  1576 apply (case_tac xs, auto)
  1577 done
  1578 
  1579 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
  1580 apply(induct xs arbitrary: m n)
  1581  apply simp
  1582 apply(simp add: take_Cons drop_Cons split:nat.split)
  1583 done
  1584 
  1585 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
  1586 apply (induct n arbitrary: xs, auto)
  1587 apply (case_tac xs, auto)
  1588 done
  1589 
  1590 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
  1591 apply(induct xs arbitrary: n)
  1592  apply simp
  1593 apply(simp add:take_Cons split:nat.split)
  1594 done
  1595 
  1596 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
  1597 apply(induct xs arbitrary: n)
  1598 apply simp
  1599 apply(simp add:drop_Cons split:nat.split)
  1600 done
  1601 
  1602 lemma take_map: "take n (map f xs) = map f (take n xs)"
  1603 apply (induct n arbitrary: xs, auto)
  1604 apply (case_tac xs, auto)
  1605 done
  1606 
  1607 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
  1608 apply (induct n arbitrary: xs, auto)
  1609 apply (case_tac xs, auto)
  1610 done
  1611 
  1612 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
  1613 apply (induct xs arbitrary: i, auto)
  1614 apply (case_tac i, auto)
  1615 done
  1616 
  1617 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
  1618 apply (induct xs arbitrary: i, auto)
  1619 apply (case_tac i, auto)
  1620 done
  1621 
  1622 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
  1623 apply (induct xs arbitrary: i n, auto)
  1624 apply (case_tac n, blast)
  1625 apply (case_tac i, auto)
  1626 done
  1627 
  1628 lemma nth_drop [simp]:
  1629   "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
  1630 apply (induct n arbitrary: xs i, auto)
  1631 apply (case_tac xs, auto)
  1632 done
  1633 
  1634 lemma butlast_take:
  1635   "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
  1636 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
  1637 
  1638 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
  1639 by (simp add: butlast_conv_take drop_take add_ac)
  1640 
  1641 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
  1642 by (simp add: butlast_conv_take min_max.inf_absorb1)
  1643 
  1644 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
  1645 by (simp add: butlast_conv_take drop_take add_ac)
  1646 
  1647 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
  1648 by(simp add: hd_conv_nth)
  1649 
  1650 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
  1651 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
  1652 
  1653 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
  1654 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
  1655 
  1656 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
  1657 using set_take_subset by fast
  1658 
  1659 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
  1660 using set_drop_subset by fast
  1661 
  1662 lemma append_eq_conv_conj:
  1663   "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
  1664 apply (induct xs arbitrary: zs, simp, clarsimp)
  1665 apply (case_tac zs, auto)
  1666 done
  1667 
  1668 lemma take_add: 
  1669   "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
  1670 apply (induct xs arbitrary: i, auto) 
  1671 apply (case_tac i, simp_all)
  1672 done
  1673 
  1674 lemma append_eq_append_conv_if:
  1675  "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
  1676   (if size xs\<^isub>1 \<le> size ys\<^isub>1
  1677    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
  1678    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)"
  1679 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
  1680  apply simp
  1681 apply(case_tac ys\<^isub>1)
  1682 apply simp_all
  1683 done
  1684 
  1685 lemma take_hd_drop:
  1686   "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
  1687 apply(induct xs arbitrary: n)
  1688 apply simp
  1689 apply(simp add:drop_Cons split:nat.split)
  1690 done
  1691 
  1692 lemma id_take_nth_drop:
  1693  "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs" 
  1694 proof -
  1695   assume si: "i < length xs"
  1696   hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
  1697   moreover
  1698   from si have "take (Suc i) xs = take i xs @ [xs!i]"
  1699     apply (rule_tac take_Suc_conv_app_nth) by arith
  1700   ultimately show ?thesis by auto
  1701 qed
  1702   
  1703 lemma upd_conv_take_nth_drop:
  1704  "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
  1705 proof -
  1706   assume i: "i < length xs"
  1707   have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
  1708     by(rule arg_cong[OF id_take_nth_drop[OF i]])
  1709   also have "\<dots> = take i xs @ a # drop (Suc i) xs"
  1710     using i by (simp add: list_update_append)
  1711   finally show ?thesis .
  1712 qed
  1713 
  1714 lemma nth_drop':
  1715   "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
  1716 apply (induct i arbitrary: xs)
  1717 apply (simp add: neq_Nil_conv)
  1718 apply (erule exE)+
  1719 apply simp
  1720 apply (case_tac xs)
  1721 apply simp_all
  1722 done
  1723 
  1724 
  1725 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
  1726 
  1727 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
  1728 by (induct xs) auto
  1729 
  1730 lemma takeWhile_append1 [simp]:
  1731 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
  1732 by (induct xs) auto
  1733 
  1734 lemma takeWhile_append2 [simp]:
  1735 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
  1736 by (induct xs) auto
  1737 
  1738 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
  1739 by (induct xs) auto
  1740 
  1741 lemma dropWhile_append1 [simp]:
  1742 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
  1743 by (induct xs) auto
  1744 
  1745 lemma dropWhile_append2 [simp]:
  1746 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
  1747 by (induct xs) auto
  1748 
  1749 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
  1750 by (induct xs) (auto split: split_if_asm)
  1751 
  1752 lemma takeWhile_eq_all_conv[simp]:
  1753  "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
  1754 by(induct xs, auto)
  1755 
  1756 lemma dropWhile_eq_Nil_conv[simp]:
  1757  "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
  1758 by(induct xs, auto)
  1759 
  1760 lemma dropWhile_eq_Cons_conv:
  1761  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
  1762 by(induct xs, auto)
  1763 
  1764 lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
  1765 by (induct xs) (auto dest: set_takeWhileD)
  1766 
  1767 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
  1768 by (induct xs) auto
  1769 
  1770 
  1771 text{* The following two lemmmas could be generalized to an arbitrary
  1772 property. *}
  1773 
  1774 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
  1775  takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
  1776 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
  1777 
  1778 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
  1779   dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
  1780 apply(induct xs)
  1781  apply simp
  1782 apply auto
  1783 apply(subst dropWhile_append2)
  1784 apply auto
  1785 done
  1786 
  1787 lemma takeWhile_not_last:
  1788  "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
  1789 apply(induct xs)
  1790  apply simp
  1791 apply(case_tac xs)
  1792 apply(auto)
  1793 done
  1794 
  1795 lemma takeWhile_cong [fundef_cong, recdef_cong]:
  1796   "[| l = k; !!x. x : set l ==> P x = Q x |] 
  1797   ==> takeWhile P l = takeWhile Q k"
  1798 by (induct k arbitrary: l) (simp_all)
  1799 
  1800 lemma dropWhile_cong [fundef_cong, recdef_cong]:
  1801   "[| l = k; !!x. x : set l ==> P x = Q x |] 
  1802   ==> dropWhile P l = dropWhile Q k"
  1803 by (induct k arbitrary: l, simp_all)
  1804 
  1805 
  1806 subsubsection {* @{text zip} *}
  1807 
  1808 lemma zip_Nil [simp]: "zip [] ys = []"
  1809 by (induct ys) auto
  1810 
  1811 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
  1812 by simp
  1813 
  1814 declare zip_Cons [simp del]
  1815 
  1816 lemma zip_Cons1:
  1817  "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
  1818 by(auto split:list.split)
  1819 
  1820 lemma length_zip [simp]:
  1821 "length (zip xs ys) = min (length xs) (length ys)"
  1822 by (induct xs ys rule:list_induct2') auto
  1823 
  1824 lemma zip_append1:
  1825 "zip (xs @ ys) zs =
  1826 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
  1827 by (induct xs zs rule:list_induct2') auto
  1828 
  1829 lemma zip_append2:
  1830 "zip xs (ys @ zs) =
  1831 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
  1832 by (induct xs ys rule:list_induct2') auto
  1833 
  1834 lemma zip_append [simp]:
  1835  "[| length xs = length us; length ys = length vs |] ==>
  1836 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
  1837 by (simp add: zip_append1)
  1838 
  1839 lemma zip_rev:
  1840 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
  1841 by (induct rule:list_induct2, simp_all)
  1842 
  1843 lemma map_zip_map:
  1844  "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
  1845 apply(induct xs arbitrary:ys) apply simp
  1846 apply(case_tac ys)
  1847 apply simp_all
  1848 done
  1849 
  1850 lemma map_zip_map2:
  1851  "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
  1852 apply(induct xs arbitrary:ys) apply simp
  1853 apply(case_tac ys)
  1854 apply simp_all
  1855 done
  1856 
  1857 text{* Courtesy of Andreas Lochbihler: *}
  1858 lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
  1859 by(induct xs) auto
  1860 
  1861 lemma nth_zip [simp]:
  1862 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
  1863 apply (induct ys arbitrary: i xs, simp)
  1864 apply (case_tac xs)
  1865  apply (simp_all add: nth.simps split: nat.split)
  1866 done
  1867 
  1868 lemma set_zip:
  1869 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
  1870 by(simp add: set_conv_nth cong: rev_conj_cong)
  1871 
  1872 lemma zip_update:
  1873   "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
  1874 by(rule sym, simp add: update_zip)
  1875 
  1876 lemma zip_replicate [simp]:
  1877   "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
  1878 apply (induct i arbitrary: j, auto)
  1879 apply (case_tac j, auto)
  1880 done
  1881 
  1882 lemma take_zip:
  1883   "take n (zip xs ys) = zip (take n xs) (take n ys)"
  1884 apply (induct n arbitrary: xs ys)
  1885  apply simp
  1886 apply (case_tac xs, simp)
  1887 apply (case_tac ys, simp_all)
  1888 done
  1889 
  1890 lemma drop_zip:
  1891   "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
  1892 apply (induct n arbitrary: xs ys)
  1893  apply simp
  1894 apply (case_tac xs, simp)
  1895 apply (case_tac ys, simp_all)
  1896 done
  1897 
  1898 lemma set_zip_leftD:
  1899   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
  1900 by (induct xs ys rule:list_induct2') auto
  1901 
  1902 lemma set_zip_rightD:
  1903   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
  1904 by (induct xs ys rule:list_induct2') auto
  1905 
  1906 lemma in_set_zipE:
  1907   "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
  1908 by(blast dest: set_zip_leftD set_zip_rightD)
  1909 
  1910 lemma zip_map_fst_snd:
  1911   "zip (map fst zs) (map snd zs) = zs"
  1912   by (induct zs) simp_all
  1913 
  1914 lemma zip_eq_conv:
  1915   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
  1916   by (auto simp add: zip_map_fst_snd)
  1917 
  1918 
  1919 subsubsection {* @{text list_all2} *}
  1920 
  1921 lemma list_all2_lengthD [intro?]: 
  1922   "list_all2 P xs ys ==> length xs = length ys"
  1923 by (simp add: list_all2_def)
  1924 
  1925 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
  1926 by (simp add: list_all2_def)
  1927 
  1928 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
  1929 by (simp add: list_all2_def)
  1930 
  1931 lemma list_all2_Cons [iff, code]:
  1932   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
  1933 by (auto simp add: list_all2_def)
  1934 
  1935 lemma list_all2_Cons1:
  1936 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
  1937 by (cases ys) auto
  1938 
  1939 lemma list_all2_Cons2:
  1940 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
  1941 by (cases xs) auto
  1942 
  1943 lemma list_all2_rev [iff]:
  1944 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
  1945 by (simp add: list_all2_def zip_rev cong: conj_cong)
  1946 
  1947 lemma list_all2_rev1:
  1948 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
  1949 by (subst list_all2_rev [symmetric]) simp
  1950 
  1951 lemma list_all2_append1:
  1952 "list_all2 P (xs @ ys) zs =
  1953 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
  1954 list_all2 P xs us \<and> list_all2 P ys vs)"
  1955 apply (simp add: list_all2_def zip_append1)
  1956 apply (rule iffI)
  1957  apply (rule_tac x = "take (length xs) zs" in exI)
  1958  apply (rule_tac x = "drop (length xs) zs" in exI)
  1959  apply (force split: nat_diff_split simp add: min_def, clarify)
  1960 apply (simp add: ball_Un)
  1961 done
  1962 
  1963 lemma list_all2_append2:
  1964 "list_all2 P xs (ys @ zs) =
  1965 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
  1966 list_all2 P us ys \<and> list_all2 P vs zs)"
  1967 apply (simp add: list_all2_def zip_append2)
  1968 apply (rule iffI)
  1969  apply (rule_tac x = "take (length ys) xs" in exI)
  1970  apply (rule_tac x = "drop (length ys) xs" in exI)
  1971  apply (force split: nat_diff_split simp add: min_def, clarify)
  1972 apply (simp add: ball_Un)
  1973 done
  1974 
  1975 lemma list_all2_append:
  1976   "length xs = length ys \<Longrightarrow>
  1977   list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
  1978 by (induct rule:list_induct2, simp_all)
  1979 
  1980 lemma list_all2_appendI [intro?, trans]:
  1981   "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
  1982 by (simp add: list_all2_append list_all2_lengthD)
  1983 
  1984 lemma list_all2_conv_all_nth:
  1985 "list_all2 P xs ys =
  1986 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
  1987 by (force simp add: list_all2_def set_zip)
  1988 
  1989 lemma list_all2_trans:
  1990   assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
  1991   shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
  1992         (is "!!bs cs. PROP ?Q as bs cs")
  1993 proof (induct as)
  1994   fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
  1995   show "!!cs. PROP ?Q (x # xs) bs cs"
  1996   proof (induct bs)
  1997     fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
  1998     show "PROP ?Q (x # xs) (y # ys) cs"
  1999       by (induct cs) (auto intro: tr I1 I2)
  2000   qed simp
  2001 qed simp
  2002 
  2003 lemma list_all2_all_nthI [intro?]:
  2004   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
  2005 by (simp add: list_all2_conv_all_nth)
  2006 
  2007 lemma list_all2I:
  2008   "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
  2009 by (simp add: list_all2_def)
  2010 
  2011 lemma list_all2_nthD:
  2012   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
  2013 by (simp add: list_all2_conv_all_nth)
  2014 
  2015 lemma list_all2_nthD2:
  2016   "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
  2017 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
  2018 
  2019 lemma list_all2_map1: 
  2020   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
  2021 by (simp add: list_all2_conv_all_nth)
  2022 
  2023 lemma list_all2_map2: 
  2024   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
  2025 by (auto simp add: list_all2_conv_all_nth)
  2026 
  2027 lemma list_all2_refl [intro?]:
  2028   "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
  2029 by (simp add: list_all2_conv_all_nth)
  2030 
  2031 lemma list_all2_update_cong:
  2032   "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  2033 by (simp add: list_all2_conv_all_nth nth_list_update)
  2034 
  2035 lemma list_all2_update_cong2:
  2036   "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  2037 by (simp add: list_all2_lengthD list_all2_update_cong)
  2038 
  2039 lemma list_all2_takeI [simp,intro?]:
  2040   "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
  2041 apply (induct xs arbitrary: n ys)
  2042  apply simp
  2043 apply (clarsimp simp add: list_all2_Cons1)
  2044 apply (case_tac n)
  2045 apply auto
  2046 done
  2047 
  2048 lemma list_all2_dropI [simp,intro?]:
  2049   "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
  2050 apply (induct as arbitrary: n bs, simp)
  2051 apply (clarsimp simp add: list_all2_Cons1)
  2052 apply (case_tac n, simp, simp)
  2053 done
  2054 
  2055 lemma list_all2_mono [intro?]:
  2056   "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
  2057 apply (induct xs arbitrary: ys, simp)
  2058 apply (case_tac ys, auto)
  2059 done
  2060 
  2061 lemma list_all2_eq:
  2062   "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
  2063 by (induct xs ys rule: list_induct2') auto
  2064 
  2065 
  2066 subsubsection {* @{text foldl} and @{text foldr} *}
  2067 
  2068 lemma foldl_append [simp]:
  2069   "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
  2070 by (induct xs arbitrary: a) auto
  2071 
  2072 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
  2073 by (induct xs) auto
  2074 
  2075 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
  2076 by(induct xs) simp_all
  2077 
  2078 text{* For efficient code generation: avoid intermediate list. *}
  2079 lemma foldl_map[code_unfold]:
  2080   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
  2081 by(induct xs arbitrary:a) simp_all
  2082 
  2083 lemma foldl_apply_inv:
  2084   assumes "\<And>x. g (h x) = x"
  2085   shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
  2086   by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
  2087 
  2088 lemma foldl_cong [fundef_cong, recdef_cong]:
  2089   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
  2090   ==> foldl f a l = foldl g b k"
  2091 by (induct k arbitrary: a b l) simp_all
  2092 
  2093 lemma foldr_cong [fundef_cong, recdef_cong]:
  2094   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
  2095   ==> foldr f l a = foldr g k b"
  2096 by (induct k arbitrary: a b l) simp_all
  2097 
  2098 lemma (in semigroup_add) foldl_assoc:
  2099 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
  2100 by (induct zs arbitrary: y) (simp_all add:add_assoc)
  2101 
  2102 lemma (in monoid_add) foldl_absorb0:
  2103 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
  2104 by (induct zs) (simp_all add:foldl_assoc)
  2105 
  2106 
  2107 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
  2108 
  2109 lemma foldl_foldr1_lemma:
  2110  "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
  2111 by (induct xs arbitrary: a) (auto simp:add_assoc)
  2112 
  2113 corollary foldl_foldr1:
  2114  "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
  2115 by (simp add:foldl_foldr1_lemma)
  2116 
  2117 
  2118 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
  2119 
  2120 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
  2121 by (induct xs) auto
  2122 
  2123 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
  2124 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
  2125 
  2126 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
  2127   by (induct xs, auto simp add: foldl_assoc add_commute)
  2128 
  2129 text {*
  2130 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
  2131 difficult to use because it requires an additional transitivity step.
  2132 *}
  2133 
  2134 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
  2135 by (induct ns arbitrary: n) auto
  2136 
  2137 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
  2138 by (force intro: start_le_sum simp add: in_set_conv_decomp)
  2139 
  2140 lemma sum_eq_0_conv [iff]:
  2141   "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
  2142 by (induct ns arbitrary: m) auto
  2143 
  2144 lemma foldr_invariant: 
  2145   "\<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)"
  2146   by (induct xs, simp_all)
  2147 
  2148 lemma foldl_invariant: 
  2149   "\<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)"
  2150   by (induct xs arbitrary: x, simp_all)
  2151 
  2152 text {* @{const foldl} and @{const concat} *}
  2153 
  2154 lemma foldl_conv_concat:
  2155   "foldl (op @) xs xss = xs @ concat xss"
  2156 proof (induct xss arbitrary: xs)
  2157   case Nil show ?case by simp
  2158 next
  2159   interpret monoid_add "[]" "op @" proof qed simp_all
  2160   case Cons then show ?case by (simp add: foldl_absorb0)
  2161 qed
  2162 
  2163 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
  2164   by (simp add: foldl_conv_concat)
  2165 
  2166 text {* @{const Finite_Set.fold} and @{const foldl} *}
  2167 
  2168 lemma (in fun_left_comm_idem) fold_set:
  2169   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
  2170   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
  2171 
  2172 
  2173 
  2174 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
  2175 
  2176 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
  2177 by (induct xs) (simp_all add:add_assoc)
  2178 
  2179 lemma listsum_rev [simp]:
  2180   fixes xs :: "'a\<Colon>comm_monoid_add list"
  2181   shows "listsum (rev xs) = listsum xs"
  2182 by (induct xs) (simp_all add:add_ac)
  2183 
  2184 lemma listsum_map_remove1:
  2185 fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
  2186 shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
  2187 by (induct xs)(auto simp add:add_ac)
  2188 
  2189 lemma list_size_conv_listsum:
  2190   "list_size f xs = listsum (map f xs) + size xs"
  2191 by(induct xs) auto
  2192 
  2193 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
  2194 by (induct xs) auto
  2195 
  2196 lemma length_concat: "length (concat xss) = listsum (map length xss)"
  2197 by (induct xss) simp_all
  2198 
  2199 text{* For efficient code generation ---
  2200        @{const listsum} is not tail recursive but @{const foldl} is. *}
  2201 lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
  2202 by(simp add:listsum_foldr foldl_foldr1)
  2203 
  2204 lemma distinct_listsum_conv_Setsum:
  2205   "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
  2206 by (induct xs) simp_all
  2207 
  2208 
  2209 text{* Some syntactic sugar for summing a function over a list: *}
  2210 
  2211 syntax
  2212   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
  2213 syntax (xsymbols)
  2214   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2215 syntax (HTML output)
  2216   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2217 
  2218 translations -- {* Beware of argument permutation! *}
  2219   "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
  2220   "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
  2221 
  2222 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
  2223   by (induct xs) (simp_all add: left_distrib)
  2224 
  2225 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
  2226   by (induct xs) (simp_all add: left_distrib)
  2227 
  2228 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
  2229 lemma uminus_listsum_map:
  2230   fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
  2231   shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
  2232 by (induct xs) simp_all
  2233 
  2234 lemma listsum_addf:
  2235   fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
  2236   shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
  2237 by (induct xs) (simp_all add: algebra_simps)
  2238 
  2239 lemma listsum_subtractf:
  2240   fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
  2241   shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
  2242 by (induct xs) simp_all
  2243 
  2244 lemma listsum_const_mult:
  2245   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
  2246   shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
  2247 by (induct xs, simp_all add: algebra_simps)
  2248 
  2249 lemma listsum_mult_const:
  2250   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
  2251   shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
  2252 by (induct xs, simp_all add: algebra_simps)
  2253 
  2254 lemma listsum_abs:
  2255   fixes xs :: "'a::pordered_ab_group_add_abs list"
  2256   shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
  2257 by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
  2258 
  2259 lemma listsum_mono:
  2260   fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, pordered_ab_semigroup_add}"
  2261   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)"
  2262 by (induct xs, simp, simp add: add_mono)
  2263 
  2264 
  2265 subsubsection {* @{text upt} *}
  2266 
  2267 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
  2268 -- {* simp does not terminate! *}
  2269 by (induct j) auto
  2270 
  2271 lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
  2272 
  2273 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
  2274 by (subst upt_rec) simp
  2275 
  2276 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
  2277 by(induct j)simp_all
  2278 
  2279 lemma upt_eq_Cons_conv:
  2280  "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
  2281 apply(induct j arbitrary: x xs)
  2282  apply simp
  2283 apply(clarsimp simp add: append_eq_Cons_conv)
  2284 apply arith
  2285 done
  2286 
  2287 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
  2288 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
  2289 by simp
  2290 
  2291 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
  2292   by (simp add: upt_rec)
  2293 
  2294 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
  2295 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
  2296 by (induct k) auto
  2297 
  2298 lemma length_upt [simp]: "length [i..<j] = j - i"
  2299 by (induct j) (auto simp add: Suc_diff_le)
  2300 
  2301 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
  2302 apply (induct j)
  2303 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
  2304 done
  2305 
  2306 
  2307 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
  2308 by(simp add:upt_conv_Cons)
  2309 
  2310 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
  2311 apply(cases j)
  2312  apply simp
  2313 by(simp add:upt_Suc_append)
  2314 
  2315 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
  2316 apply (induct m arbitrary: i, simp)
  2317 apply (subst upt_rec)
  2318 apply (rule sym)
  2319 apply (subst upt_rec)
  2320 apply (simp del: upt.simps)
  2321 done
  2322 
  2323 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
  2324 apply(induct j)
  2325 apply auto
  2326 done
  2327 
  2328 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
  2329 by (induct n) auto
  2330 
  2331 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
  2332 apply (induct n m  arbitrary: i rule: diff_induct)
  2333 prefer 3 apply (subst map_Suc_upt[symmetric])
  2334 apply (auto simp add: less_diff_conv nth_upt)
  2335 done
  2336 
  2337 lemma nth_take_lemma:
  2338   "k <= length xs ==> k <= length ys ==>
  2339      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
  2340 apply (atomize, induct k arbitrary: xs ys)
  2341 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
  2342 txt {* Both lists must be non-empty *}
  2343 apply (case_tac xs, simp)
  2344 apply (case_tac ys, clarify)
  2345  apply (simp (no_asm_use))
  2346 apply clarify
  2347 txt {* prenexing's needed, not miniscoping *}
  2348 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
  2349 apply blast
  2350 done
  2351 
  2352 lemma nth_equalityI:
  2353  "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
  2354 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
  2355 apply (simp_all add: take_all)
  2356 done
  2357 
  2358 lemma map_nth:
  2359   "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
  2360   by (rule nth_equalityI, auto)
  2361 
  2362 (* needs nth_equalityI *)
  2363 lemma list_all2_antisym:
  2364   "\<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> 
  2365   \<Longrightarrow> xs = ys"
  2366   apply (simp add: list_all2_conv_all_nth) 
  2367   apply (rule nth_equalityI, blast, simp)
  2368   done
  2369 
  2370 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
  2371 -- {* The famous take-lemma. *}
  2372 apply (drule_tac x = "max (length xs) (length ys)" in spec)
  2373 apply (simp add: le_max_iff_disj take_all)
  2374 done
  2375 
  2376 
  2377 lemma take_Cons':
  2378      "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
  2379 by (cases n) simp_all
  2380 
  2381 lemma drop_Cons':
  2382      "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
  2383 by (cases n) simp_all
  2384 
  2385 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
  2386 by (cases n) simp_all
  2387 
  2388 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
  2389 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
  2390 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
  2391 
  2392 declare take_Cons_number_of [simp] 
  2393         drop_Cons_number_of [simp] 
  2394         nth_Cons_number_of [simp] 
  2395 
  2396 
  2397 subsubsection {* @{text upto}: interval-list on @{typ int} *}
  2398 
  2399 (* FIXME make upto tail recursive? *)
  2400 
  2401 function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
  2402 "upto i j = (if i \<le> j then i # [i+1..j] else [])"
  2403 by auto
  2404 termination
  2405 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
  2406 
  2407 declare upto.simps[code, simp del]
  2408 
  2409 lemmas upto_rec_number_of[simp] =
  2410   upto.simps[of "number_of m" "number_of n", standard]
  2411 
  2412 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
  2413 by(simp add: upto.simps)
  2414 
  2415 lemma set_upto[simp]: "set[i..j] = {i..j}"
  2416 apply(induct i j rule:upto.induct)
  2417 apply(simp add: upto.simps simp_from_to)
  2418 done
  2419 
  2420 
  2421 subsubsection {* @{text "distinct"} and @{text remdups} *}
  2422 
  2423 lemma distinct_append [simp]:
  2424 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
  2425 by (induct xs) auto
  2426 
  2427 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
  2428 by(induct xs) auto
  2429 
  2430 lemma set_remdups [simp]: "set (remdups xs) = set xs"
  2431 by (induct xs) (auto simp add: insert_absorb)
  2432 
  2433 lemma distinct_remdups [iff]: "distinct (remdups xs)"
  2434 by (induct xs) auto
  2435 
  2436 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
  2437 by (induct xs, auto)
  2438 
  2439 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
  2440 by (metis distinct_remdups distinct_remdups_id)
  2441 
  2442 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
  2443 by (metis distinct_remdups finite_list set_remdups)
  2444 
  2445 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
  2446 by (induct x, auto) 
  2447 
  2448 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
  2449 by (induct x, auto)
  2450 
  2451 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
  2452 by (induct xs) auto
  2453 
  2454 lemma length_remdups_eq[iff]:
  2455   "(length (remdups xs) = length xs) = (remdups xs = xs)"
  2456 apply(induct xs)
  2457  apply auto
  2458 apply(subgoal_tac "length (remdups xs) <= length xs")
  2459  apply arith
  2460 apply(rule length_remdups_leq)
  2461 done
  2462 
  2463 
  2464 lemma distinct_map:
  2465   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
  2466 by (induct xs) auto
  2467 
  2468 
  2469 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
  2470 by (induct xs) auto
  2471 
  2472 lemma distinct_upt[simp]: "distinct[i..<j]"
  2473 by (induct j) auto
  2474 
  2475 lemma distinct_upto[simp]: "distinct[i..j]"
  2476 apply(induct i j rule:upto.induct)
  2477 apply(subst upto.simps)
  2478 apply(simp)
  2479 done
  2480 
  2481 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
  2482 apply(induct xs arbitrary: i)
  2483  apply simp
  2484 apply (case_tac i)
  2485  apply simp_all
  2486 apply(blast dest:in_set_takeD)
  2487 done
  2488 
  2489 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
  2490 apply(induct xs arbitrary: i)
  2491  apply simp
  2492 apply (case_tac i)
  2493  apply simp_all
  2494 done
  2495 
  2496 lemma distinct_list_update:
  2497 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
  2498 shows "distinct (xs[i:=a])"
  2499 proof (cases "i < length xs")
  2500   case True
  2501   with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
  2502     apply (drule_tac id_take_nth_drop) by simp
  2503   with d True show ?thesis
  2504     apply (simp add: upd_conv_take_nth_drop)
  2505     apply (drule subst [OF id_take_nth_drop]) apply assumption
  2506     apply simp apply (cases "a = xs!i") apply simp by blast
  2507 next
  2508   case False with d show ?thesis by auto
  2509 qed
  2510 
  2511 lemma distinct_concat:
  2512   assumes "distinct xs"
  2513   and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"
  2514   and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"
  2515   shows "distinct (concat xs)"
  2516   using assms by (induct xs) auto
  2517 
  2518 text {* It is best to avoid this indexed version of distinct, but
  2519 sometimes it is useful. *}
  2520 
  2521 lemma distinct_conv_nth:
  2522 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
  2523 apply (induct xs, simp, simp)
  2524 apply (rule iffI, clarsimp)
  2525  apply (case_tac i)
  2526 apply (case_tac j, simp)
  2527 apply (simp add: set_conv_nth)
  2528  apply (case_tac j)
  2529 apply (clarsimp simp add: set_conv_nth, simp) 
  2530 apply (rule conjI)
  2531 (*TOO SLOW
  2532 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2533 *)
  2534  apply (clarsimp simp add: set_conv_nth)
  2535  apply (erule_tac x = 0 in allE, simp)
  2536  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
  2537 (*TOO SLOW
  2538 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
  2539 *)
  2540 apply (erule_tac x = "Suc i" in allE, simp)
  2541 apply (erule_tac x = "Suc j" in allE, simp)
  2542 done
  2543 
  2544 lemma nth_eq_iff_index_eq:
  2545  "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
  2546 by(auto simp: distinct_conv_nth)
  2547 
  2548 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
  2549 by (induct xs) auto
  2550 
  2551 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
  2552 proof (induct xs)
  2553   case Nil thus ?case by simp
  2554 next
  2555   case (Cons x xs)
  2556   show ?case
  2557   proof (cases "x \<in> set xs")
  2558     case False with Cons show ?thesis by simp
  2559   next
  2560     case True with Cons.prems
  2561     have "card (set xs) = Suc (length xs)" 
  2562       by (simp add: card_insert_if split: split_if_asm)
  2563     moreover have "card (set xs) \<le> length xs" by (rule card_length)
  2564     ultimately have False by simp
  2565     thus ?thesis ..
  2566   qed
  2567 qed
  2568 
  2569 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
  2570 apply (induct n == "length ws" arbitrary:ws) apply simp
  2571 apply(case_tac ws) apply simp
  2572 apply (simp split:split_if_asm)
  2573 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
  2574 done
  2575 
  2576 lemma length_remdups_concat:
  2577  "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
  2578 by(simp add: set_concat distinct_card[symmetric])
  2579 
  2580 
  2581 subsubsection {* @{text remove1} *}
  2582 
  2583 lemma remove1_append:
  2584   "remove1 x (xs @ ys) =
  2585   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
  2586 by (induct xs) auto
  2587 
  2588 lemma in_set_remove1[simp]:
  2589   "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
  2590 apply (induct xs)
  2591 apply auto
  2592 done
  2593 
  2594 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
  2595 apply(induct xs)
  2596  apply simp
  2597 apply simp
  2598 apply blast
  2599 done
  2600 
  2601 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
  2602 apply(induct xs)
  2603  apply simp
  2604 apply simp
  2605 apply blast
  2606 done
  2607 
  2608 lemma length_remove1:
  2609   "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
  2610 apply (induct xs)
  2611  apply (auto dest!:length_pos_if_in_set)
  2612 done
  2613 
  2614 lemma remove1_filter_not[simp]:
  2615   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
  2616 by(induct xs) auto
  2617 
  2618 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
  2619 apply(insert set_remove1_subset)
  2620 apply fast
  2621 done
  2622 
  2623 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
  2624 by (induct xs) simp_all
  2625 
  2626 
  2627 subsubsection {* @{text removeAll} *}
  2628 
  2629 lemma removeAll_append[simp]:
  2630   "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
  2631 by (induct xs) auto
  2632 
  2633 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
  2634 by (induct xs) auto
  2635 
  2636 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
  2637 by (induct xs) auto
  2638 
  2639 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
  2640 lemma length_removeAll:
  2641   "length(removeAll x xs) = length xs - count x xs"
  2642 *)
  2643 
  2644 lemma removeAll_filter_not[simp]:
  2645   "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
  2646 by(induct xs) auto
  2647 
  2648 
  2649 lemma distinct_remove1_removeAll:
  2650   "distinct xs ==> remove1 x xs = removeAll x xs"
  2651 by (induct xs) simp_all
  2652 
  2653 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
  2654   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  2655 by (induct xs) (simp_all add:inj_on_def)
  2656 
  2657 lemma map_removeAll_inj: "inj f \<Longrightarrow>
  2658   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  2659 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
  2660 
  2661 
  2662 subsubsection {* @{text replicate} *}
  2663 
  2664 lemma length_replicate [simp]: "length (replicate n x) = n"
  2665 by (induct n) auto
  2666 
  2667 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
  2668 by (induct n) auto
  2669 
  2670 lemma map_replicate_const:
  2671   "map (\<lambda> x. k) lst = replicate (length lst) k"
  2672   by (induct lst) auto
  2673 
  2674 lemma replicate_app_Cons_same:
  2675 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
  2676 by (induct n) auto
  2677 
  2678 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
  2679 apply (induct n, simp)
  2680 apply (simp add: replicate_app_Cons_same)
  2681 done
  2682 
  2683 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
  2684 by (induct n) auto
  2685 
  2686 text{* Courtesy of Matthias Daum: *}
  2687 lemma append_replicate_commute:
  2688   "replicate n x @ replicate k x = replicate k x @ replicate n x"
  2689 apply (simp add: replicate_add [THEN sym])
  2690 apply (simp add: add_commute)
  2691 done
  2692 
  2693 text{* Courtesy of Andreas Lochbihler: *}
  2694 lemma filter_replicate:
  2695   "filter P (replicate n x) = (if P x then replicate n x else [])"
  2696 by(induct n) auto
  2697 
  2698 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
  2699 by (induct n) auto
  2700 
  2701 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
  2702 by (induct n) auto
  2703 
  2704 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
  2705 by (atomize (full), induct n) auto
  2706 
  2707 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
  2708 apply (induct n arbitrary: i, simp)
  2709 apply (simp add: nth_Cons split: nat.split)
  2710 done
  2711 
  2712 text{* Courtesy of Matthias Daum (2 lemmas): *}
  2713 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
  2714 apply (case_tac "k \<le> i")
  2715  apply  (simp add: min_def)
  2716 apply (drule not_leE)
  2717 apply (simp add: min_def)
  2718 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
  2719  apply  simp
  2720 apply (simp add: replicate_add [symmetric])
  2721 done
  2722 
  2723 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
  2724 apply (induct k arbitrary: i)
  2725  apply simp
  2726 apply clarsimp
  2727 apply (case_tac i)
  2728  apply simp
  2729 apply clarsimp
  2730 done
  2731 
  2732 
  2733 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
  2734 by (induct n) auto
  2735 
  2736 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
  2737 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
  2738 
  2739 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
  2740 by auto
  2741 
  2742 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
  2743 by (simp add: set_replicate_conv_if split: split_if_asm)
  2744 
  2745 lemma replicate_append_same:
  2746   "replicate i x @ [x] = x # replicate i x"
  2747   by (induct i) simp_all
  2748 
  2749 lemma map_replicate_trivial:
  2750   "map (\<lambda>i. x) [0..<i] = replicate i x"
  2751   by (induct i) (simp_all add: replicate_append_same)
  2752 
  2753 lemma concat_replicate_trivial[simp]:
  2754   "concat (replicate i []) = []"
  2755   by (induct i) (auto simp add: map_replicate_const)
  2756 
  2757 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
  2758 by (induct n) auto
  2759 
  2760 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
  2761 by (induct n) auto
  2762 
  2763 lemma replicate_eq_replicate[simp]:
  2764   "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
  2765 apply(induct m arbitrary: n)
  2766  apply simp
  2767 apply(induct_tac n)
  2768 apply auto
  2769 done
  2770 
  2771 
  2772 subsubsection{*@{text rotate1} and @{text rotate}*}
  2773 
  2774 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
  2775 by(simp add:rotate1_def)
  2776 
  2777 lemma rotate0[simp]: "rotate 0 = id"
  2778 by(simp add:rotate_def)
  2779 
  2780 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
  2781 by(simp add:rotate_def)
  2782 
  2783 lemma rotate_add:
  2784   "rotate (m+n) = rotate m o rotate n"
  2785 by(simp add:rotate_def funpow_add)
  2786 
  2787 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
  2788 by(simp add:rotate_add)
  2789 
  2790 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
  2791 by(simp add:rotate_def funpow_swap1)
  2792 
  2793 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
  2794 by(cases xs) simp_all
  2795 
  2796 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
  2797 apply(induct n)
  2798  apply simp
  2799 apply (simp add:rotate_def)
  2800 done
  2801 
  2802 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
  2803 by(simp add:rotate1_def split:list.split)
  2804 
  2805 lemma rotate_drop_take:
  2806   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
  2807 apply(induct n)
  2808  apply simp
  2809 apply(simp add:rotate_def)
  2810 apply(cases "xs = []")
  2811  apply (simp)
  2812 apply(case_tac "n mod length xs = 0")
  2813  apply(simp add:mod_Suc)
  2814  apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
  2815 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
  2816                 take_hd_drop linorder_not_le)
  2817 done
  2818 
  2819 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
  2820 by(simp add:rotate_drop_take)
  2821 
  2822 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
  2823 by(simp add:rotate_drop_take)
  2824 
  2825 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
  2826 by(simp add:rotate1_def split:list.split)
  2827 
  2828 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
  2829 by (induct n arbitrary: xs) (simp_all add:rotate_def)
  2830 
  2831 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
  2832 by(simp add:rotate1_def split:list.split) blast
  2833 
  2834 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
  2835 by (induct n) (simp_all add:rotate_def)
  2836 
  2837 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
  2838 by(simp add:rotate_drop_take take_map drop_map)
  2839 
  2840 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
  2841 by(simp add:rotate1_def split:list.split)
  2842 
  2843 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
  2844 by (induct n) (simp_all add:rotate_def)
  2845 
  2846 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
  2847 by(simp add:rotate1_def split:list.split)
  2848 
  2849 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
  2850 by (induct n) (simp_all add:rotate_def)
  2851 
  2852 lemma rotate_rev:
  2853   "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
  2854 apply(simp add:rotate_drop_take rev_drop rev_take)
  2855 apply(cases "length xs = 0")
  2856  apply simp
  2857 apply(cases "n mod length xs = 0")
  2858  apply simp
  2859 apply(simp add:rotate_drop_take rev_drop rev_take)
  2860 done
  2861 
  2862 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
  2863 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
  2864 apply(subgoal_tac "length xs \<noteq> 0")
  2865  prefer 2 apply simp
  2866 using mod_less_divisor[of "length xs" n] by arith
  2867 
  2868 
  2869 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
  2870 
  2871 lemma sublist_empty [simp]: "sublist xs {} = []"
  2872 by (auto simp add: sublist_def)
  2873 
  2874 lemma sublist_nil [simp]: "sublist [] A = []"
  2875 by (auto simp add: sublist_def)
  2876 
  2877 lemma length_sublist:
  2878   "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
  2879 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
  2880 
  2881 lemma sublist_shift_lemma_Suc:
  2882   "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
  2883    map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
  2884 apply(induct xs arbitrary: "is")
  2885  apply simp
  2886 apply (case_tac "is")
  2887  apply simp
  2888 apply simp
  2889 done
  2890 
  2891 lemma sublist_shift_lemma:
  2892      "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
  2893       map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
  2894 by (induct xs rule: rev_induct) (simp_all add: add_commute)
  2895 
  2896 lemma sublist_append:
  2897      "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
  2898 apply (unfold sublist_def)
  2899 apply (induct l' rule: rev_induct, simp)
  2900 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
  2901 apply (simp add: add_commute)
  2902 done
  2903 
  2904 lemma sublist_Cons:
  2905 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
  2906 apply (induct l rule: rev_induct)
  2907  apply (simp add: sublist_def)
  2908 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
  2909 done
  2910 
  2911 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
  2912 apply(induct xs arbitrary: I)
  2913 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  2914 done
  2915 
  2916 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
  2917 by(auto simp add:set_sublist)
  2918 
  2919 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
  2920 by(auto simp add:set_sublist)
  2921 
  2922 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
  2923 by(auto simp add:set_sublist)
  2924 
  2925 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
  2926 by (simp add: sublist_Cons)
  2927 
  2928 
  2929 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
  2930 apply(induct xs arbitrary: I)
  2931  apply simp
  2932 apply(auto simp add:sublist_Cons)
  2933 done
  2934 
  2935 
  2936 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
  2937 apply (induct l rule: rev_induct, simp)
  2938 apply (simp split: nat_diff_split add: sublist_append)
  2939 done
  2940 
  2941 lemma filter_in_sublist:
  2942  "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
  2943 proof (induct xs arbitrary: s)
  2944   case Nil thus ?case by simp
  2945 next
  2946   case (Cons a xs)
  2947   moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
  2948   ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
  2949 qed
  2950 
  2951 
  2952 subsubsection {* @{const splice} *}
  2953 
  2954 lemma splice_Nil2 [simp, code]:
  2955  "splice xs [] = xs"
  2956 by (cases xs) simp_all
  2957 
  2958 lemma splice_Cons_Cons [simp, code]:
  2959  "splice (x#xs) (y#ys) = x # y # splice xs ys"
  2960 by simp
  2961 
  2962 declare splice.simps(2) [simp del, code del]
  2963 
  2964 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  2965 apply(induct xs arbitrary: ys) apply simp
  2966 apply(case_tac ys)
  2967  apply auto
  2968 done
  2969 
  2970 
  2971 subsubsection {* (In)finiteness *}
  2972 
  2973 lemma finite_maxlen:
  2974   "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
  2975 proof (induct rule: finite.induct)
  2976   case emptyI show ?case by simp
  2977 next
  2978   case (insertI M xs)
  2979   then obtain n where "\<forall>s\<in>M. length s < n" by blast
  2980   hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
  2981   thus ?case ..
  2982 qed
  2983 
  2984 lemma finite_lists_length_eq:
  2985 assumes "finite A"
  2986 shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
  2987 proof(induct n)
  2988   case 0 show ?case by simp
  2989 next
  2990   case (Suc n)
  2991   have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
  2992     by (auto simp:length_Suc_conv)
  2993   then show ?case using `finite A`
  2994     by (auto intro: finite_imageI Suc) (* FIXME metis? *)
  2995 qed
  2996 
  2997 lemma finite_lists_length_le:
  2998   assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
  2999  (is "finite ?S")
  3000 proof-
  3001   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
  3002   thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
  3003 qed
  3004 
  3005 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
  3006 apply(rule notI)
  3007 apply(drule finite_maxlen)
  3008 apply (metis UNIV_I length_replicate less_not_refl)
  3009 done
  3010 
  3011 
  3012 subsection {*Sorting*}
  3013 
  3014 text{* Currently it is not shown that @{const sort} returns a
  3015 permutation of its input because the nicest proof is via multisets,
  3016 which are not yet available. Alternatively one could define a function
  3017 that counts the number of occurrences of an element in a list and use
  3018 that instead of multisets to state the correctness property. *}
  3019 
  3020 context linorder
  3021 begin
  3022 
  3023 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
  3024 apply(induct xs arbitrary: x) apply simp
  3025 by simp (blast intro: order_trans)
  3026 
  3027 lemma sorted_append:
  3028   "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
  3029 by (induct xs) (auto simp add:sorted_Cons)
  3030 
  3031 lemma sorted_nth_mono:
  3032   "sorted xs \<Longrightarrow> i <= j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i <= xs!j"
  3033 by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
  3034 
  3035 lemma set_insort: "set(insort x xs) = insert x (set xs)"
  3036 by (induct xs) auto
  3037 
  3038 lemma set_sort[simp]: "set(sort xs) = set xs"
  3039 by (induct xs) (simp_all add:set_insort)
  3040 
  3041 lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
  3042 by(induct xs)(auto simp:set_insort)
  3043 
  3044 lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
  3045 by(induct xs)(simp_all add:distinct_insort set_sort)
  3046 
  3047 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
  3048 apply (induct xs)
  3049  apply(auto simp:sorted_Cons set_insort)
  3050 done
  3051 
  3052 theorem sorted_sort[simp]: "sorted (sort xs)"
  3053 by (induct xs) (auto simp:sorted_insort)
  3054 
  3055 lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
  3056 by (cases xs) auto
  3057 
  3058 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
  3059 by (induct xs, auto simp add: sorted_Cons)
  3060 
  3061 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
  3062 by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
  3063 
  3064 lemma sorted_remdups[simp]:
  3065   "sorted l \<Longrightarrow> sorted (remdups l)"
  3066 by (induct l) (auto simp: sorted_Cons)
  3067 
  3068 lemma sorted_distinct_set_unique:
  3069 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
  3070 shows "xs = ys"
  3071 proof -
  3072   from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
  3073   from assms show ?thesis
  3074   proof(induct rule:list_induct2[OF 1])
  3075     case 1 show ?case by simp
  3076   next
  3077     case 2 thus ?case by (simp add:sorted_Cons)
  3078        (metis Diff_insert_absorb antisym insertE insert_iff)
  3079   qed
  3080 qed
  3081 
  3082 lemma finite_sorted_distinct_unique:
  3083 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
  3084 apply(drule finite_distinct_list)
  3085 apply clarify
  3086 apply(rule_tac a="sort xs" in ex1I)
  3087 apply (auto simp: sorted_distinct_set_unique)
  3088 done
  3089 
  3090 lemma sorted_take:
  3091   "sorted xs \<Longrightarrow> sorted (take n xs)"
  3092 proof (induct xs arbitrary: n rule: sorted.induct)
  3093   case 1 show ?case by simp
  3094 next
  3095   case 2 show ?case by (cases n) simp_all
  3096 next
  3097   case (3 x y xs)
  3098   then have "x \<le> y" by simp
  3099   show ?case proof (cases n)
  3100     case 0 then show ?thesis by simp
  3101   next
  3102     case (Suc m) 
  3103     with 3 have "sorted (take m (y # xs))" by simp
  3104     with Suc  `x \<le> y` show ?thesis by (cases m) simp_all
  3105   qed
  3106 qed
  3107 
  3108 lemma sorted_drop:
  3109   "sorted xs \<Longrightarrow> sorted (drop n xs)"
  3110 proof (induct xs arbitrary: n rule: sorted.induct)
  3111   case 1 show ?case by simp
  3112 next
  3113   case 2 show ?case by (cases n) simp_all
  3114 next
  3115   case 3 then show ?case by (cases n) simp_all
  3116 qed
  3117 
  3118 
  3119 end
  3120 
  3121 lemma sorted_upt[simp]: "sorted[i..<j]"
  3122 by (induct j) (simp_all add:sorted_append)
  3123 
  3124 lemma sorted_upto[simp]: "sorted[i..j]"
  3125 apply(induct i j rule:upto.induct)
  3126 apply(subst upto.simps)
  3127 apply(simp add:sorted_Cons)
  3128 done
  3129 
  3130 
  3131 subsubsection {* @{text sorted_list_of_set} *}
  3132 
  3133 text{* This function maps (finite) linearly ordered sets to sorted
  3134 lists. Warning: in most cases it is not a good idea to convert from
  3135 sets to lists but one should convert in the other direction (via
  3136 @{const set}). *}
  3137 
  3138 
  3139 context linorder
  3140 begin
  3141 
  3142 definition
  3143  sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
  3144  [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
  3145 
  3146 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
  3147   set(sorted_list_of_set A) = A &
  3148   sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
  3149 apply(simp add:sorted_list_of_set_def)
  3150 apply(rule the1I2)
  3151  apply(simp_all add: finite_sorted_distinct_unique)
  3152 done
  3153 
  3154 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
  3155 unfolding sorted_list_of_set_def
  3156 apply(subst the_equality[of _ "[]"])
  3157 apply simp_all
  3158 done
  3159 
  3160 end
  3161 
  3162 
  3163 subsubsection {* @{text lists}: the list-forming operator over sets *}
  3164 
  3165 inductive_set
  3166   lists :: "'a set => 'a list set"
  3167   for A :: "'a set"
  3168 where
  3169     Nil [intro!]: "[]: lists A"
  3170   | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
  3171 
  3172 inductive_cases listsE [elim!,noatp]: "x#l : lists A"
  3173 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
  3174 
  3175 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
  3176 by (rule predicate1I, erule listsp.induct, blast+)
  3177 
  3178 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
  3179 
  3180 lemma listsp_infI:
  3181   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
  3182 by induct blast+
  3183 
  3184 lemmas lists_IntI = listsp_infI [to_set]
  3185 
  3186 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
  3187 proof (rule mono_inf [where f=listsp, THEN order_antisym])
  3188   show "mono listsp" by (simp add: mono_def listsp_mono)
  3189   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
  3190 qed
  3191 
  3192 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
  3193 
  3194 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
  3195 
  3196 lemma append_in_listsp_conv [iff]:
  3197      "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
  3198 by (induct xs) auto
  3199 
  3200 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
  3201 
  3202 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
  3203 -- {* eliminate @{text listsp} in favour of @{text set} *}
  3204 by (induct xs) auto
  3205 
  3206 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
  3207 
  3208 lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
  3209 by (rule in_listsp_conv_set [THEN iffD1])
  3210 
  3211 lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
  3212 
  3213 lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
  3214 by (rule in_listsp_conv_set [THEN iffD2])
  3215 
  3216 lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
  3217 
  3218 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
  3219 by auto
  3220 
  3221 
  3222 
  3223 subsubsection{* Inductive definition for membership *}
  3224 
  3225 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
  3226 where
  3227     elem:  "ListMem x (x # xs)"
  3228   | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
  3229 
  3230 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
  3231 apply (rule iffI)
  3232  apply (induct set: ListMem)
  3233   apply auto
  3234 apply (induct xs)
  3235  apply (auto intro: ListMem.intros)
  3236 done
  3237 
  3238 
  3239 
  3240 subsubsection{*Lists as Cartesian products*}
  3241 
  3242 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
  3243 @{term A} and tail drawn from @{term Xs}.*}
  3244 
  3245 constdefs
  3246   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
  3247   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
  3248 declare set_Cons_def [code del]
  3249 
  3250 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
  3251 by (auto simp add: set_Cons_def)
  3252 
  3253 text{*Yields the set of lists, all of the same length as the argument and
  3254 with elements drawn from the corresponding element of the argument.*}
  3255 
  3256 consts  listset :: "'a set list \<Rightarrow> 'a list set"
  3257 primrec
  3258    "listset []    = {[]}"
  3259    "listset(A#As) = set_Cons A (listset As)"
  3260 
  3261 
  3262 subsection{*Relations on Lists*}
  3263 
  3264 subsubsection {* Length Lexicographic Ordering *}
  3265 
  3266 text{*These orderings preserve well-foundedness: shorter lists 
  3267   precede longer lists. These ordering are not used in dictionaries.*}
  3268 
  3269 consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
  3270         --{*The lexicographic ordering for lists of the specified length*}
  3271 primrec
  3272   "lexn r 0 = {}"
  3273   "lexn r (Suc n) =
  3274     (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
  3275     {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
  3276 
  3277 constdefs
  3278   lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
  3279     "lex r == \<Union>n. lexn r n"
  3280         --{*Holds only between lists of the same length*}
  3281 
  3282   lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
  3283     "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
  3284         --{*Compares lists by their length and then lexicographically*}
  3285 
  3286 declare lex_def [code del]
  3287 
  3288 
  3289 lemma wf_lexn: "wf r ==> wf (lexn r n)"
  3290 apply (induct n, simp, simp)
  3291 apply(rule wf_subset)
  3292  prefer 2 apply (rule Int_lower1)
  3293 apply(rule wf_prod_fun_image)
  3294  prefer 2 apply (rule inj_onI, auto)
  3295 done
  3296 
  3297 lemma lexn_length:
  3298   "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
  3299 by (induct n arbitrary: xs ys) auto
  3300 
  3301 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
  3302 apply (unfold lex_def)
  3303 apply (rule wf_UN)
  3304 apply (blast intro: wf_lexn, clarify)
  3305 apply (rename_tac m n)
  3306 apply (subgoal_tac "m \<noteq> n")
  3307  prefer 2 apply blast
  3308 apply (blast dest: lexn_length not_sym)
  3309 done
  3310 
  3311 lemma lexn_conv:
  3312   "lexn r n =
  3313     {(xs,ys). length xs = n \<and> length ys = n \<and>
  3314     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
  3315 apply (induct n, simp)
  3316 apply (simp add: image_Collect lex_prod_def, safe, blast)
  3317  apply (rule_tac x = "ab # xys" in exI, simp)
  3318 apply (case_tac xys, simp_all, blast)
  3319 done
  3320 
  3321 lemma lex_conv:
  3322   "lex r =
  3323     {(xs,ys). length xs = length ys \<and>
  3324     (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
  3325 by (force simp add: lex_def lexn_conv)
  3326 
  3327 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
  3328 by (unfold lenlex_def) blast
  3329 
  3330 lemma lenlex_conv:
  3331     "lenlex r = {(xs,ys). length xs < length ys |
  3332                  length xs = length ys \<and> (xs, ys) : lex r}"
  3333 by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
  3334 
  3335 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
  3336 by (simp add: lex_conv)
  3337 
  3338 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
  3339 by (simp add:lex_conv)
  3340 
  3341 lemma Cons_in_lex [simp]:
  3342     "((x # xs, y # ys) : lex r) =
  3343       ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
  3344 apply (simp add: lex_conv)
  3345 apply (rule iffI)
  3346  prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
  3347 apply (case_tac xys, simp, simp)
  3348 apply blast
  3349 done
  3350 
  3351 
  3352 subsubsection {* Lexicographic Ordering *}
  3353 
  3354 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
  3355     This ordering does \emph{not} preserve well-foundedness.
  3356      Author: N. Voelker, March 2005. *} 
  3357 
  3358 constdefs 
  3359   lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
  3360   "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
  3361             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
  3362 declare lexord_def [code del]
  3363 
  3364 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
  3365 by (unfold lexord_def, induct_tac y, auto) 
  3366 
  3367 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
  3368 by (unfold lexord_def, induct_tac x, auto)
  3369 
  3370 lemma lexord_cons_cons[simp]:
  3371      "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
  3372   apply (unfold lexord_def, safe, simp_all)
  3373   apply (case_tac u, simp, simp)
  3374   apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
  3375   apply (erule_tac x="b # u" in allE)
  3376   by force
  3377 
  3378 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
  3379 
  3380 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
  3381 by (induct_tac x, auto)  
  3382 
  3383 lemma lexord_append_left_rightI:
  3384      "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
  3385 by (induct_tac u, auto)
  3386 
  3387 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
  3388 by (induct x, auto)
  3389 
  3390 lemma lexord_append_leftD:
  3391      "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
  3392 by (erule rev_mp, induct_tac x, auto)
  3393 
  3394 lemma lexord_take_index_conv: 
  3395    "((x,y) : lexord r) = 
  3396     ((length x < length y \<and> take (length x) y = x) \<or> 
  3397      (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
  3398   apply (unfold lexord_def Let_def, clarsimp) 
  3399   apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
  3400   apply auto 
  3401   apply (rule_tac x="hd (drop (length x) y)" in exI)
  3402   apply (rule_tac x="tl (drop (length x) y)" in exI)
  3403   apply (erule subst, simp add: min_def) 
  3404   apply (rule_tac x ="length u" in exI, simp) 
  3405   apply (rule_tac x ="take i x" in exI) 
  3406   apply (rule_tac x ="x ! i" in exI) 
  3407   apply (rule_tac x ="y ! i" in exI, safe) 
  3408   apply (rule_tac x="drop (Suc i) x" in exI)
  3409   apply (drule sym, simp add: drop_Suc_conv_tl) 
  3410   apply (rule_tac x="drop (Suc i) y" in exI)
  3411   by (simp add: drop_Suc_conv_tl) 
  3412 
  3413 -- {* lexord is extension of partial ordering List.lex *} 
  3414 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
  3415   apply (rule_tac x = y in spec) 
  3416   apply (induct_tac x, clarsimp) 
  3417   by (clarify, case_tac x, simp, force)
  3418 
  3419 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
  3420   by (induct y, auto)
  3421 
  3422 lemma lexord_trans: 
  3423     "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
  3424    apply (erule rev_mp)+
  3425    apply (rule_tac x = x in spec) 
  3426   apply (rule_tac x = z in spec) 
  3427   apply ( induct_tac y, simp, clarify)
  3428   apply (case_tac xa, erule ssubst) 
  3429   apply (erule allE, erule allE) -- {* avoid simp recursion *} 
  3430   apply (case_tac x, simp, simp) 
  3431   apply (case_tac x, erule allE, erule allE, simp)
  3432   apply (erule_tac x = listb in allE) 
  3433   apply (erule_tac x = lista in allE, simp)
  3434   apply (unfold trans_def)
  3435   by blast
  3436 
  3437 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
  3438 by (rule transI, drule lexord_trans, blast) 
  3439 
  3440 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"
  3441   apply (rule_tac x = y in spec) 
  3442   apply (induct_tac x, rule allI) 
  3443   apply (case_tac x, simp, simp) 
  3444   apply (rule allI, case_tac x, simp, simp) 
  3445   by blast
  3446 
  3447 
  3448 subsection {* Lexicographic combination of measure functions *}
  3449 
  3450 text {* These are useful for termination proofs *}
  3451 
  3452 definition
  3453   "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
  3454 
  3455 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
  3456 unfolding measures_def
  3457 by blast
  3458 
  3459 lemma in_measures[simp]: 
  3460   "(x, y) \<in> measures [] = False"
  3461   "(x, y) \<in> measures (f # fs)
  3462          = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
  3463 unfolding measures_def
  3464 by auto
  3465 
  3466 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
  3467 by simp
  3468 
  3469 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
  3470 by auto
  3471 
  3472 
  3473 subsubsection{*Lifting a Relation on List Elements to the Lists*}
  3474 
  3475 inductive_set
  3476   listrel :: "('a * 'a)set => ('a list * 'a list)set"
  3477   for r :: "('a * 'a)set"
  3478 where
  3479     Nil:  "([],[]) \<in> listrel r"
  3480   | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
  3481 
  3482 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
  3483 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
  3484 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
  3485 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
  3486 
  3487 
  3488 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
  3489 apply clarify  
  3490 apply (erule listrel.induct)
  3491 apply (blast intro: listrel.intros)+
  3492 done
  3493 
  3494 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
  3495 apply clarify 
  3496 apply (erule listrel.induct, auto) 
  3497 done
  3498 
  3499 lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)" 
  3500 apply (simp add: refl_on_def listrel_subset Ball_def)
  3501 apply (rule allI) 
  3502 apply (induct_tac x) 
  3503 apply (auto intro: listrel.intros)
  3504 done
  3505 
  3506 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
  3507 apply (auto simp add: sym_def)
  3508 apply (erule listrel.induct) 
  3509 apply (blast intro: listrel.intros)+
  3510 done
  3511 
  3512 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
  3513 apply (simp add: trans_def)
  3514 apply (intro allI) 
  3515 apply (rule impI) 
  3516 apply (erule listrel.induct) 
  3517 apply (blast intro: listrel.intros)+
  3518 done
  3519 
  3520 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
  3521 by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) 
  3522 
  3523 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
  3524 by (blast intro: listrel.intros)
  3525 
  3526 lemma listrel_Cons:
  3527      "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
  3528 by (auto simp add: set_Cons_def intro: listrel.intros) 
  3529 
  3530 
  3531 subsection {* Size function *}
  3532 
  3533 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
  3534 by (rule is_measure_trivial)
  3535 
  3536 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
  3537 by (rule is_measure_trivial)
  3538 
  3539 lemma list_size_estimation[termination_simp]: 
  3540   "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
  3541 by (induct xs) auto
  3542 
  3543 lemma list_size_estimation'[termination_simp]: 
  3544   "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
  3545 by (induct xs) auto
  3546 
  3547 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
  3548 by (induct xs) auto
  3549 
  3550 lemma list_size_pointwise[termination_simp]: 
  3551   "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
  3552 by (induct xs) force+
  3553 
  3554 
  3555 subsection {* Code generator *}
  3556 
  3557 subsubsection {* Setup *}
  3558 
  3559 use "Tools/list_code.ML"
  3560 
  3561 code_type list
  3562   (SML "_ list")
  3563   (OCaml "_ list")
  3564   (Haskell "![_]")
  3565 
  3566 code_const Nil
  3567   (SML "[]")
  3568   (OCaml "[]")
  3569   (Haskell "[]")
  3570 
  3571 code_instance list :: eq
  3572   (Haskell -)
  3573 
  3574 code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
  3575   (Haskell infixl 4 "==")
  3576 
  3577 code_reserved SML
  3578   list
  3579 
  3580 code_reserved OCaml
  3581   list
  3582 
  3583 types_code
  3584   "list" ("_ list")
  3585 attach (term_of) {*
  3586 fun term_of_list f T = HOLogic.mk_list T o map f;
  3587 *}
  3588 attach (test) {*
  3589 fun gen_list' aG aT i j = frequency
  3590   [(i, fn () =>
  3591       let
  3592         val (x, t) = aG j;
  3593         val (xs, ts) = gen_list' aG aT (i-1) j
  3594       in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
  3595    (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
  3596 and gen_list aG aT i = gen_list' aG aT i i;
  3597 *}
  3598 
  3599 consts_code Cons ("(_ ::/ _)")
  3600 
  3601 setup {*
  3602 let
  3603   fun list_codegen thy defs dep thyname b t gr =
  3604     let
  3605       val ts = HOLogic.dest_list t;
  3606       val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
  3607         (fastype_of t) gr;
  3608       val (ps, gr'') = fold_map
  3609         (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
  3610     in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
  3611 in
  3612   fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell"]
  3613   #> Codegen.add_codegen "list_codegen" list_codegen
  3614 end
  3615 *}
  3616 
  3617 
  3618 subsubsection {* Generation of efficient code *}
  3619 
  3620 primrec
  3621   member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
  3622 where 
  3623   "x mem [] \<longleftrightarrow> False"
  3624   | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
  3625 
  3626 primrec
  3627   null:: "'a list \<Rightarrow> bool"
  3628 where
  3629   "null [] = True"
  3630   | "null (x#xs) = False"
  3631 
  3632 primrec
  3633   list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  3634 where
  3635   "list_inter [] bs = []"
  3636   | "list_inter (a#as) bs =
  3637      (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
  3638 
  3639 primrec
  3640   list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
  3641 where
  3642   "list_all P [] = True"
  3643   | "list_all P (x#xs) = (P x \<and> list_all P xs)"
  3644 
  3645 primrec
  3646   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
  3647 where
  3648   "list_ex P [] = False"
  3649   | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
  3650 
  3651 primrec
  3652   filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  3653 where
  3654   "filtermap f [] = []"
  3655   | "filtermap f (x#xs) =
  3656      (case f x of None \<Rightarrow> filtermap f xs
  3657       | Some y \<Rightarrow> y # filtermap f xs)"
  3658 
  3659 primrec
  3660   map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  3661 where
  3662   "map_filter f P [] = []"
  3663   | "map_filter f P (x#xs) =
  3664      (if P x then f x # map_filter f P xs else map_filter f P xs)"
  3665 
  3666 primrec
  3667   length_unique :: "'a list \<Rightarrow> nat"
  3668 where
  3669   "length_unique [] = 0"
  3670   | "length_unique (x#xs) =
  3671       (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
  3672 
  3673 text {*
  3674   Only use @{text mem} for generating executable code.  Otherwise use
  3675   @{prop "x : set xs"} instead --- it is much easier to reason about.
  3676   The same is true for @{const list_all} and @{const list_ex}: write
  3677   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
  3678   quantifiers are aleady known to the automatic provers. In fact, the
  3679   declarations in the code subsection make sure that @{text "\<in>"},
  3680   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
  3681   efficiently.
  3682 
  3683   Efficient emptyness check is implemented by @{const null}.
  3684 
  3685   The functions @{const filtermap} and @{const map_filter} are just
  3686   there to generate efficient code. Do not use
  3687   them for modelling and proving.
  3688 *}
  3689 
  3690 lemma rev_foldl_cons [code]:
  3691   "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
  3692 proof (induct xs)
  3693   case Nil then show ?case by simp
  3694 next
  3695   case Cons
  3696   {
  3697     fix x xs ys
  3698     have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
  3699       = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
  3700     by (induct xs arbitrary: ys) auto
  3701   }
  3702   note aux = this
  3703   show ?case by (induct xs) (auto simp add: Cons aux)
  3704 qed
  3705 
  3706 lemma mem_iff [code_post]:
  3707   "x mem xs \<longleftrightarrow> x \<in> set xs"
  3708 by (induct xs) auto
  3709 
  3710 lemmas in_set_code [code_unfold] = mem_iff [symmetric]
  3711 
  3712 lemma empty_null:
  3713   "xs = [] \<longleftrightarrow> null xs"
  3714 by (cases xs) simp_all
  3715 
  3716 lemma [code_unfold]:
  3717   "eq_class.eq xs [] \<longleftrightarrow> null xs"
  3718 by (simp add: eq empty_null)
  3719 
  3720 lemmas null_empty [code_post] =
  3721   empty_null [symmetric]
  3722 
  3723 lemma list_inter_conv:
  3724   "set (list_inter xs ys) = set xs \<inter> set ys"
  3725 by (induct xs) auto
  3726 
  3727 lemma list_all_iff [code_post]:
  3728   "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
  3729 by (induct xs) auto
  3730 
  3731 lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
  3732 
  3733 lemma list_all_append [simp]:
  3734   "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
  3735 by (induct xs) auto
  3736 
  3737 lemma list_all_rev [simp]:
  3738   "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
  3739 by (simp add: list_all_iff)
  3740 
  3741 lemma list_all_length:
  3742   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
  3743   unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
  3744 
  3745 lemma list_ex_iff [code_post]:
  3746   "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
  3747 by (induct xs) simp_all
  3748 
  3749 lemmas list_bex_code [code_unfold] =
  3750   list_ex_iff [symmetric]
  3751 
  3752 lemma list_ex_length:
  3753   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
  3754   unfolding list_ex_iff set_conv_nth by auto
  3755 
  3756 lemma filtermap_conv:
  3757    "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
  3758 by (induct xs) (simp_all split: option.split) 
  3759 
  3760 lemma map_filter_conv [simp]:
  3761   "map_filter f P xs = map f (filter P xs)"
  3762 by (induct xs) auto
  3763 
  3764 lemma length_remdups_length_unique [code_unfold]:
  3765   "length (remdups xs) = length_unique xs"
  3766   by (induct xs) simp_all
  3767 
  3768 hide (open) const length_unique
  3769 
  3770 
  3771 text {* Code for bounded quantification and summation over nats. *}
  3772 
  3773 lemma atMost_upto [code_unfold]:
  3774   "{..n} = set [0..<Suc n]"
  3775 by auto
  3776 
  3777 lemma atLeast_upt [code_unfold]:
  3778   "{..<n} = set [0..<n]"
  3779 by auto
  3780 
  3781 lemma greaterThanLessThan_upt [code_unfold]:
  3782   "{n<..<m} = set [Suc n..<m]"
  3783 by auto
  3784 
  3785 lemma atLeastLessThan_upt [code_unfold]:
  3786   "{n..<m} = set [n..<m]"
  3787 by auto
  3788 
  3789 lemma greaterThanAtMost_upt [code_unfold]:
  3790   "{n<..m} = set [Suc n..<Suc m]"
  3791 by auto
  3792 
  3793 lemma atLeastAtMost_upt [code_unfold]:
  3794   "{n..m} = set [n..<Suc m]"
  3795 by auto
  3796 
  3797 lemma all_nat_less_eq [code_unfold]:
  3798   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
  3799 by auto
  3800 
  3801 lemma ex_nat_less_eq [code_unfold]:
  3802   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
  3803 by auto
  3804 
  3805 lemma all_nat_less [code_unfold]:
  3806   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
  3807 by auto
  3808 
  3809 lemma ex_nat_less [code_unfold]:
  3810   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
  3811 by auto
  3812 
  3813 lemma setsum_set_distinct_conv_listsum:
  3814   "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
  3815 by (induct xs) simp_all
  3816 
  3817 lemma setsum_set_upt_conv_listsum [code_unfold]:
  3818   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
  3819 by (rule setsum_set_distinct_conv_listsum) simp
  3820 
  3821 
  3822 text {* Code for summation over ints. *}
  3823 
  3824 lemma greaterThanLessThan_upto [code_unfold]:
  3825   "{i<..<j::int} = set [i+1..j - 1]"
  3826 by auto
  3827 
  3828 lemma atLeastLessThan_upto [code_unfold]:
  3829   "{i..<j::int} = set [i..j - 1]"
  3830 by auto
  3831 
  3832 lemma greaterThanAtMost_upto [code_unfold]:
  3833   "{i<..j::int} = set [i+1..j]"
  3834 by auto
  3835 
  3836 lemmas atLeastAtMost_upto [code_unfold] = set_upto[symmetric]
  3837 
  3838 lemma setsum_set_upto_conv_listsum [code_unfold]:
  3839   "setsum f (set [i..j::int]) = listsum (map f [i..j])"
  3840 by (rule setsum_set_distinct_conv_listsum) simp
  3841 
  3842 end