src/HOL/List.thy
author nipkow
Fri Aug 28 18:52:41 2009 +0200 (2009-08-28)
changeset 32436 10cd49e0c067
parent 32422 46fc4d4ff4c0
child 32681 adeac3cbb659
permissions -rw-r--r--
Turned "x <= y ==> sup x y = y" (and relatives) into simp rules
     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] = {i..<j}"
   885 by (induct j) (simp_all add: atLeastLessThanSuc)
   886 
   887 
   888 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
   889 proof (induct xs)
   890   case Nil thus ?case by simp
   891 next
   892   case Cons thus ?case by (auto intro: Cons_eq_appendI)
   893 qed
   894 
   895 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
   896   by (auto elim: split_list)
   897 
   898 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
   899 proof (induct xs)
   900   case Nil thus ?case by simp
   901 next
   902   case (Cons a xs)
   903   show ?case
   904   proof cases
   905     assume "x = a" thus ?case using Cons by fastsimp
   906   next
   907     assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
   908   qed
   909 qed
   910 
   911 lemma in_set_conv_decomp_first:
   912   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
   913   by (auto dest!: split_list_first)
   914 
   915 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
   916 proof (induct xs rule:rev_induct)
   917   case Nil thus ?case by simp
   918 next
   919   case (snoc a xs)
   920   show ?case
   921   proof cases
   922     assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
   923   next
   924     assume "x \<noteq> a" thus ?case using snoc by fastsimp
   925   qed
   926 qed
   927 
   928 lemma in_set_conv_decomp_last:
   929   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
   930   by (auto dest!: split_list_last)
   931 
   932 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
   933 proof (induct xs)
   934   case Nil thus ?case by simp
   935 next
   936   case Cons thus ?case
   937     by(simp add:Bex_def)(metis append_Cons append.simps(1))
   938 qed
   939 
   940 lemma split_list_propE:
   941   assumes "\<exists>x \<in> set xs. P x"
   942   obtains ys x zs where "xs = ys @ x # zs" and "P x"
   943 using split_list_prop [OF assms] by blast
   944 
   945 lemma split_list_first_prop:
   946   "\<exists>x \<in> set xs. P x \<Longrightarrow>
   947    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
   948 proof (induct xs)
   949   case Nil thus ?case by simp
   950 next
   951   case (Cons x xs)
   952   show ?case
   953   proof cases
   954     assume "P x"
   955     thus ?thesis by simp
   956       (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
   957   next
   958     assume "\<not> P x"
   959     hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
   960     thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
   961   qed
   962 qed
   963 
   964 lemma split_list_first_propE:
   965   assumes "\<exists>x \<in> set xs. P x"
   966   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
   967 using split_list_first_prop [OF assms] by blast
   968 
   969 lemma split_list_first_prop_iff:
   970   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
   971    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
   972 by (rule, erule split_list_first_prop) auto
   973 
   974 lemma split_list_last_prop:
   975   "\<exists>x \<in> set xs. P x \<Longrightarrow>
   976    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
   977 proof(induct xs rule:rev_induct)
   978   case Nil thus ?case by simp
   979 next
   980   case (snoc x xs)
   981   show ?case
   982   proof cases
   983     assume "P x" thus ?thesis by (metis emptyE set_empty)
   984   next
   985     assume "\<not> P x"
   986     hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
   987     thus ?thesis using `\<not> P x` snoc(1) by fastsimp
   988   qed
   989 qed
   990 
   991 lemma split_list_last_propE:
   992   assumes "\<exists>x \<in> set xs. P x"
   993   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
   994 using split_list_last_prop [OF assms] by blast
   995 
   996 lemma split_list_last_prop_iff:
   997   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
   998    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
   999 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
  1000 
  1001 lemma finite_list: "finite A ==> EX xs. set xs = A"
  1002   by (erule finite_induct)
  1003     (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
  1004 
  1005 lemma card_length: "card (set xs) \<le> length xs"
  1006 by (induct xs) (auto simp add: card_insert_if)
  1007 
  1008 lemma set_minus_filter_out:
  1009   "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
  1010   by (induct xs) auto
  1011 
  1012 subsubsection {* @{text filter} *}
  1013 
  1014 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
  1015 by (induct xs) auto
  1016 
  1017 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
  1018 by (induct xs) simp_all
  1019 
  1020 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
  1021 by (induct xs) auto
  1022 
  1023 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
  1024 by (induct xs) (auto simp add: le_SucI)
  1025 
  1026 lemma sum_length_filter_compl:
  1027   "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
  1028 by(induct xs) simp_all
  1029 
  1030 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
  1031 by (induct xs) auto
  1032 
  1033 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
  1034 by (induct xs) auto
  1035 
  1036 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
  1037 by (induct xs) simp_all
  1038 
  1039 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
  1040 apply (induct xs)
  1041  apply auto
  1042 apply(cut_tac P=P and xs=xs in length_filter_le)
  1043 apply simp
  1044 done
  1045 
  1046 lemma filter_map:
  1047   "filter P (map f xs) = map f (filter (P o f) xs)"
  1048 by (induct xs) simp_all
  1049 
  1050 lemma length_filter_map[simp]:
  1051   "length (filter P (map f xs)) = length(filter (P o f) xs)"
  1052 by (simp add:filter_map)
  1053 
  1054 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
  1055 by auto
  1056 
  1057 lemma length_filter_less:
  1058   "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
  1059 proof (induct xs)
  1060   case Nil thus ?case by simp
  1061 next
  1062   case (Cons x xs) thus ?case
  1063     apply (auto split:split_if_asm)
  1064     using length_filter_le[of P xs] apply arith
  1065   done
  1066 qed
  1067 
  1068 lemma length_filter_conv_card:
  1069  "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
  1070 proof (induct xs)
  1071   case Nil thus ?case by simp
  1072 next
  1073   case (Cons x xs)
  1074   let ?S = "{i. i < length xs & p(xs!i)}"
  1075   have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
  1076   show ?case (is "?l = card ?S'")
  1077   proof (cases)
  1078     assume "p x"
  1079     hence eq: "?S' = insert 0 (Suc ` ?S)"
  1080       by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
  1081     have "length (filter p (x # xs)) = Suc(card ?S)"
  1082       using Cons `p x` by simp
  1083     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
  1084       by (simp add: card_image inj_Suc)
  1085     also have "\<dots> = card ?S'" using eq fin
  1086       by (simp add:card_insert_if) (simp add:image_def)
  1087     finally show ?thesis .
  1088   next
  1089     assume "\<not> p x"
  1090     hence eq: "?S' = Suc ` ?S"
  1091       by(auto simp add: image_def split:nat.split elim:lessE)
  1092     have "length (filter p (x # xs)) = card ?S"
  1093       using Cons `\<not> p x` by simp
  1094     also have "\<dots> = card(Suc ` ?S)" using fin
  1095       by (simp add: card_image inj_Suc)
  1096     also have "\<dots> = card ?S'" using eq fin
  1097       by (simp add:card_insert_if)
  1098     finally show ?thesis .
  1099   qed
  1100 qed
  1101 
  1102 lemma Cons_eq_filterD:
  1103  "x#xs = filter P ys \<Longrightarrow>
  1104   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  1105   (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
  1106 proof(induct ys)
  1107   case Nil thus ?case by simp
  1108 next
  1109   case (Cons y ys)
  1110   show ?case (is "\<exists>x. ?Q x")
  1111   proof cases
  1112     assume Py: "P y"
  1113     show ?thesis
  1114     proof cases
  1115       assume "x = y"
  1116       with Py Cons.prems have "?Q []" by simp
  1117       then show ?thesis ..
  1118     next
  1119       assume "x \<noteq> y"
  1120       with Py Cons.prems show ?thesis by simp
  1121     qed
  1122   next
  1123     assume "\<not> P y"
  1124     with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
  1125     then have "?Q (y#us)" by simp
  1126     then show ?thesis ..
  1127   qed
  1128 qed
  1129 
  1130 lemma filter_eq_ConsD:
  1131  "filter P ys = x#xs \<Longrightarrow>
  1132   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  1133 by(rule Cons_eq_filterD) simp
  1134 
  1135 lemma filter_eq_Cons_iff:
  1136  "(filter P ys = x#xs) =
  1137   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
  1138 by(auto dest:filter_eq_ConsD)
  1139 
  1140 lemma Cons_eq_filter_iff:
  1141  "(x#xs = filter P ys) =
  1142   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
  1143 by(auto dest:Cons_eq_filterD)
  1144 
  1145 lemma filter_cong[fundef_cong, recdef_cong]:
  1146  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
  1147 apply simp
  1148 apply(erule thin_rl)
  1149 by (induct ys) simp_all
  1150 
  1151 
  1152 subsubsection {* List partitioning *}
  1153 
  1154 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
  1155   "partition P [] = ([], [])"
  1156   | "partition P (x # xs) = 
  1157       (let (yes, no) = partition P xs
  1158       in if P x then (x # yes, no) else (yes, x # no))"
  1159 
  1160 lemma partition_filter1:
  1161     "fst (partition P xs) = filter P xs"
  1162 by (induct xs) (auto simp add: Let_def split_def)
  1163 
  1164 lemma partition_filter2:
  1165     "snd (partition P xs) = filter (Not o P) xs"
  1166 by (induct xs) (auto simp add: Let_def split_def)
  1167 
  1168 lemma partition_P:
  1169   assumes "partition P xs = (yes, no)"
  1170   shows "(\<forall>p \<in> set yes.  P p) \<and> (\<forall>p  \<in> set no. \<not> P p)"
  1171 proof -
  1172   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
  1173     by simp_all
  1174   then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
  1175 qed
  1176 
  1177 lemma partition_set:
  1178   assumes "partition P xs = (yes, no)"
  1179   shows "set yes \<union> set no = set xs"
  1180 proof -
  1181   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
  1182     by simp_all
  1183   then show ?thesis by (auto simp add: partition_filter1 partition_filter2) 
  1184 qed
  1185 
  1186 
  1187 subsubsection {* @{text concat} *}
  1188 
  1189 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
  1190 by (induct xs) auto
  1191 
  1192 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
  1193 by (induct xss) auto
  1194 
  1195 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
  1196 by (induct xss) auto
  1197 
  1198 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
  1199 by (induct xs) auto
  1200 
  1201 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
  1202 by (induct xs) auto
  1203 
  1204 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
  1205 by (induct xs) auto
  1206 
  1207 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
  1208 by (induct xs) auto
  1209 
  1210 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
  1211 by (induct xs) auto
  1212 
  1213 
  1214 subsubsection {* @{text nth} *}
  1215 
  1216 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
  1217 by auto
  1218 
  1219 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
  1220 by auto
  1221 
  1222 declare nth.simps [simp del]
  1223 
  1224 lemma nth_append:
  1225   "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
  1226 apply (induct xs arbitrary: n, simp)
  1227 apply (case_tac n, auto)
  1228 done
  1229 
  1230 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
  1231 by (induct xs) auto
  1232 
  1233 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
  1234 by (induct xs) auto
  1235 
  1236 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
  1237 apply (induct xs arbitrary: n, simp)
  1238 apply (case_tac n, auto)
  1239 done
  1240 
  1241 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
  1242 by(cases xs) simp_all
  1243 
  1244 
  1245 lemma list_eq_iff_nth_eq:
  1246  "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
  1247 apply(induct xs arbitrary: ys)
  1248  apply force
  1249 apply(case_tac ys)
  1250  apply simp
  1251 apply(simp add:nth_Cons split:nat.split)apply blast
  1252 done
  1253 
  1254 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
  1255 apply (induct xs, simp, simp)
  1256 apply safe
  1257 apply (metis nat_case_0 nth.simps zero_less_Suc)
  1258 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
  1259 apply (case_tac i, simp)
  1260 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
  1261 done
  1262 
  1263 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
  1264 by(auto simp:set_conv_nth)
  1265 
  1266 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
  1267 by (auto simp add: set_conv_nth)
  1268 
  1269 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
  1270 by (auto simp add: set_conv_nth)
  1271 
  1272 lemma all_nth_imp_all_set:
  1273 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
  1274 by (auto simp add: set_conv_nth)
  1275 
  1276 lemma all_set_conv_all_nth:
  1277 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
  1278 by (auto simp add: set_conv_nth)
  1279 
  1280 lemma rev_nth:
  1281   "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
  1282 proof (induct xs arbitrary: n)
  1283   case Nil thus ?case by simp
  1284 next
  1285   case (Cons x xs)
  1286   hence n: "n < Suc (length xs)" by simp
  1287   moreover
  1288   { assume "n < length xs"
  1289     with n obtain n' where "length xs - n = Suc n'"
  1290       by (cases "length xs - n", auto)
  1291     moreover
  1292     then have "length xs - Suc n = n'" by simp
  1293     ultimately
  1294     have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
  1295   }
  1296   ultimately
  1297   show ?case by (clarsimp simp add: Cons nth_append)
  1298 qed
  1299 
  1300 lemma Skolem_list_nth:
  1301   "(ALL i<k. EX x. P i x) = (EX xs. size xs = k & (ALL i<k. P i (xs!i)))"
  1302   (is "_ = (EX xs. ?P k xs)")
  1303 proof(induct k)
  1304   case 0 show ?case by simp
  1305 next
  1306   case (Suc k)
  1307   show ?case (is "?L = ?R" is "_ = (EX xs. ?P' xs)")
  1308   proof
  1309     assume "?R" thus "?L" using Suc by auto
  1310   next
  1311     assume "?L"
  1312     with Suc obtain x xs where "?P k xs & P k x" by (metis less_Suc_eq)
  1313     hence "?P'(xs@[x])" by(simp add:nth_append less_Suc_eq)
  1314     thus "?R" ..
  1315   qed
  1316 qed
  1317 
  1318 
  1319 subsubsection {* @{text list_update} *}
  1320 
  1321 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
  1322 by (induct xs arbitrary: i) (auto split: nat.split)
  1323 
  1324 lemma nth_list_update:
  1325 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
  1326 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
  1327 
  1328 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
  1329 by (simp add: nth_list_update)
  1330 
  1331 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
  1332 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
  1333 
  1334 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
  1335 by (induct xs arbitrary: i) (simp_all split:nat.splits)
  1336 
  1337 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
  1338 apply (induct xs arbitrary: i)
  1339  apply simp
  1340 apply (case_tac i)
  1341 apply simp_all
  1342 done
  1343 
  1344 lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"
  1345 by(metis length_0_conv length_list_update)
  1346 
  1347 lemma list_update_same_conv:
  1348 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
  1349 by (induct xs arbitrary: i) (auto split: nat.split)
  1350 
  1351 lemma list_update_append1:
  1352  "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
  1353 apply (induct xs arbitrary: i, simp)
  1354 apply(simp split:nat.split)
  1355 done
  1356 
  1357 lemma list_update_append:
  1358   "(xs @ ys) [n:= x] = 
  1359   (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
  1360 by (induct xs arbitrary: n) (auto split:nat.splits)
  1361 
  1362 lemma list_update_length [simp]:
  1363  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
  1364 by (induct xs, auto)
  1365 
  1366 lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"
  1367 by(induct xs arbitrary: k)(auto split:nat.splits)
  1368 
  1369 lemma rev_update:
  1370   "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"
  1371 by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)
  1372 
  1373 lemma update_zip:
  1374   "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
  1375 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
  1376 
  1377 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
  1378 by (induct xs arbitrary: i) (auto split: nat.split)
  1379 
  1380 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
  1381 by (blast dest!: set_update_subset_insert [THEN subsetD])
  1382 
  1383 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
  1384 by (induct xs arbitrary: n) (auto split:nat.splits)
  1385 
  1386 lemma list_update_overwrite[simp]:
  1387   "xs [i := x, i := y] = xs [i := y]"
  1388 apply (induct xs arbitrary: i) apply simp
  1389 apply (case_tac i, simp_all)
  1390 done
  1391 
  1392 lemma list_update_swap:
  1393   "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
  1394 apply (induct xs arbitrary: i i')
  1395 apply simp
  1396 apply (case_tac i, case_tac i')
  1397 apply auto
  1398 apply (case_tac i')
  1399 apply auto
  1400 done
  1401 
  1402 lemma list_update_code [code]:
  1403   "[][i := y] = []"
  1404   "(x # xs)[0 := y] = y # xs"
  1405   "(x # xs)[Suc i := y] = x # xs[i := y]"
  1406   by simp_all
  1407 
  1408 
  1409 subsubsection {* @{text last} and @{text butlast} *}
  1410 
  1411 lemma last_snoc [simp]: "last (xs @ [x]) = x"
  1412 by (induct xs) auto
  1413 
  1414 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
  1415 by (induct xs) auto
  1416 
  1417 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
  1418 by(simp add:last.simps)
  1419 
  1420 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
  1421 by(simp add:last.simps)
  1422 
  1423 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
  1424 by (induct xs) (auto)
  1425 
  1426 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
  1427 by(simp add:last_append)
  1428 
  1429 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
  1430 by(simp add:last_append)
  1431 
  1432 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
  1433 by(rule rev_exhaust[of xs]) simp_all
  1434 
  1435 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
  1436 by(cases xs) simp_all
  1437 
  1438 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
  1439 by (induct as) auto
  1440 
  1441 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
  1442 by (induct xs rule: rev_induct) auto
  1443 
  1444 lemma butlast_append:
  1445   "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
  1446 by (induct xs arbitrary: ys) auto
  1447 
  1448 lemma append_butlast_last_id [simp]:
  1449 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
  1450 by (induct xs) auto
  1451 
  1452 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
  1453 by (induct xs) (auto split: split_if_asm)
  1454 
  1455 lemma in_set_butlast_appendI:
  1456 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
  1457 by (auto dest: in_set_butlastD simp add: butlast_append)
  1458 
  1459 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
  1460 apply (induct xs arbitrary: n)
  1461  apply simp
  1462 apply (auto split:nat.split)
  1463 done
  1464 
  1465 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
  1466 by(induct xs)(auto simp:neq_Nil_conv)
  1467 
  1468 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
  1469 by (induct xs, simp, case_tac xs, simp_all)
  1470 
  1471 lemma last_list_update:
  1472   "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"
  1473 by (auto simp: last_conv_nth)
  1474 
  1475 lemma butlast_list_update:
  1476   "butlast(xs[k:=x]) =
  1477  (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"
  1478 apply(cases xs rule:rev_cases)
  1479 apply simp
  1480 apply(simp add:list_update_append split:nat.splits)
  1481 done
  1482 
  1483 
  1484 subsubsection {* @{text take} and @{text drop} *}
  1485 
  1486 lemma take_0 [simp]: "take 0 xs = []"
  1487 by (induct xs) auto
  1488 
  1489 lemma drop_0 [simp]: "drop 0 xs = xs"
  1490 by (induct xs) auto
  1491 
  1492 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
  1493 by simp
  1494 
  1495 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
  1496 by simp
  1497 
  1498 declare take_Cons [simp del] and drop_Cons [simp del]
  1499 
  1500 lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
  1501   unfolding One_nat_def by simp
  1502 
  1503 lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
  1504   unfolding One_nat_def by simp
  1505 
  1506 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
  1507 by(clarsimp simp add:neq_Nil_conv)
  1508 
  1509 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
  1510 by(cases xs, simp_all)
  1511 
  1512 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
  1513 by (induct xs arbitrary: n) simp_all
  1514 
  1515 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
  1516 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
  1517 
  1518 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
  1519 by (cases n, simp, cases xs, auto)
  1520 
  1521 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
  1522 by (simp only: drop_tl)
  1523 
  1524 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
  1525 apply (induct xs arbitrary: n, simp)
  1526 apply(simp add:drop_Cons nth_Cons split:nat.splits)
  1527 done
  1528 
  1529 lemma take_Suc_conv_app_nth:
  1530   "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
  1531 apply (induct xs arbitrary: i, simp)
  1532 apply (case_tac i, auto)
  1533 done
  1534 
  1535 lemma drop_Suc_conv_tl:
  1536   "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
  1537 apply (induct xs arbitrary: i, simp)
  1538 apply (case_tac i, auto)
  1539 done
  1540 
  1541 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
  1542 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1543 
  1544 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
  1545 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1546 
  1547 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
  1548 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1549 
  1550 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
  1551 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1552 
  1553 lemma take_append [simp]:
  1554   "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
  1555 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1556 
  1557 lemma drop_append [simp]:
  1558   "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
  1559 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1560 
  1561 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
  1562 apply (induct m arbitrary: xs n, auto)
  1563 apply (case_tac xs, auto)
  1564 apply (case_tac n, auto)
  1565 done
  1566 
  1567 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
  1568 apply (induct m arbitrary: xs, auto)
  1569 apply (case_tac xs, auto)
  1570 done
  1571 
  1572 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
  1573 apply (induct m arbitrary: xs n, auto)
  1574 apply (case_tac xs, auto)
  1575 done
  1576 
  1577 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
  1578 apply(induct xs arbitrary: m n)
  1579  apply simp
  1580 apply(simp add: take_Cons drop_Cons split:nat.split)
  1581 done
  1582 
  1583 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
  1584 apply (induct n arbitrary: xs, auto)
  1585 apply (case_tac xs, auto)
  1586 done
  1587 
  1588 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
  1589 apply(induct xs arbitrary: n)
  1590  apply simp
  1591 apply(simp add:take_Cons split:nat.split)
  1592 done
  1593 
  1594 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
  1595 apply(induct xs arbitrary: n)
  1596 apply simp
  1597 apply(simp add:drop_Cons split:nat.split)
  1598 done
  1599 
  1600 lemma take_map: "take n (map f xs) = map f (take n xs)"
  1601 apply (induct n arbitrary: xs, auto)
  1602 apply (case_tac xs, auto)
  1603 done
  1604 
  1605 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
  1606 apply (induct n arbitrary: xs, auto)
  1607 apply (case_tac xs, auto)
  1608 done
  1609 
  1610 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
  1611 apply (induct xs arbitrary: i, auto)
  1612 apply (case_tac i, auto)
  1613 done
  1614 
  1615 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
  1616 apply (induct xs arbitrary: i, auto)
  1617 apply (case_tac i, auto)
  1618 done
  1619 
  1620 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
  1621 apply (induct xs arbitrary: i n, auto)
  1622 apply (case_tac n, blast)
  1623 apply (case_tac i, auto)
  1624 done
  1625 
  1626 lemma nth_drop [simp]:
  1627   "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
  1628 apply (induct n arbitrary: xs i, auto)
  1629 apply (case_tac xs, auto)
  1630 done
  1631 
  1632 lemma butlast_take:
  1633   "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
  1634 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
  1635 
  1636 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
  1637 by (simp add: butlast_conv_take drop_take add_ac)
  1638 
  1639 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
  1640 by (simp add: butlast_conv_take min_max.inf_absorb1)
  1641 
  1642 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
  1643 by (simp add: butlast_conv_take drop_take add_ac)
  1644 
  1645 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
  1646 by(simp add: hd_conv_nth)
  1647 
  1648 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
  1649 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
  1650 
  1651 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
  1652 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
  1653 
  1654 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
  1655 using set_take_subset by fast
  1656 
  1657 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
  1658 using set_drop_subset by fast
  1659 
  1660 lemma append_eq_conv_conj:
  1661   "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
  1662 apply (induct xs arbitrary: zs, simp, clarsimp)
  1663 apply (case_tac zs, auto)
  1664 done
  1665 
  1666 lemma take_add: 
  1667   "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
  1668 apply (induct xs arbitrary: i, auto) 
  1669 apply (case_tac i, simp_all)
  1670 done
  1671 
  1672 lemma append_eq_append_conv_if:
  1673  "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
  1674   (if size xs\<^isub>1 \<le> size ys\<^isub>1
  1675    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
  1676    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)"
  1677 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
  1678  apply simp
  1679 apply(case_tac ys\<^isub>1)
  1680 apply simp_all
  1681 done
  1682 
  1683 lemma take_hd_drop:
  1684   "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
  1685 apply(induct xs arbitrary: n)
  1686 apply simp
  1687 apply(simp add:drop_Cons split:nat.split)
  1688 done
  1689 
  1690 lemma id_take_nth_drop:
  1691  "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs" 
  1692 proof -
  1693   assume si: "i < length xs"
  1694   hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
  1695   moreover
  1696   from si have "take (Suc i) xs = take i xs @ [xs!i]"
  1697     apply (rule_tac take_Suc_conv_app_nth) by arith
  1698   ultimately show ?thesis by auto
  1699 qed
  1700   
  1701 lemma upd_conv_take_nth_drop:
  1702  "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
  1703 proof -
  1704   assume i: "i < length xs"
  1705   have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
  1706     by(rule arg_cong[OF id_take_nth_drop[OF i]])
  1707   also have "\<dots> = take i xs @ a # drop (Suc i) xs"
  1708     using i by (simp add: list_update_append)
  1709   finally show ?thesis .
  1710 qed
  1711 
  1712 lemma nth_drop':
  1713   "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
  1714 apply (induct i arbitrary: xs)
  1715 apply (simp add: neq_Nil_conv)
  1716 apply (erule exE)+
  1717 apply simp
  1718 apply (case_tac xs)
  1719 apply simp_all
  1720 done
  1721 
  1722 
  1723 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
  1724 
  1725 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
  1726 by (induct xs) auto
  1727 
  1728 lemma takeWhile_append1 [simp]:
  1729 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
  1730 by (induct xs) auto
  1731 
  1732 lemma takeWhile_append2 [simp]:
  1733 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
  1734 by (induct xs) auto
  1735 
  1736 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
  1737 by (induct xs) auto
  1738 
  1739 lemma dropWhile_append1 [simp]:
  1740 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
  1741 by (induct xs) auto
  1742 
  1743 lemma dropWhile_append2 [simp]:
  1744 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
  1745 by (induct xs) auto
  1746 
  1747 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
  1748 by (induct xs) (auto split: split_if_asm)
  1749 
  1750 lemma takeWhile_eq_all_conv[simp]:
  1751  "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
  1752 by(induct xs, auto)
  1753 
  1754 lemma dropWhile_eq_Nil_conv[simp]:
  1755  "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
  1756 by(induct xs, auto)
  1757 
  1758 lemma dropWhile_eq_Cons_conv:
  1759  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
  1760 by(induct xs, auto)
  1761 
  1762 lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"
  1763 by (induct xs) (auto dest: set_takeWhileD)
  1764 
  1765 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"
  1766 by (induct xs) auto
  1767 
  1768 
  1769 text{* The following two lemmmas could be generalized to an arbitrary
  1770 property. *}
  1771 
  1772 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
  1773  takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
  1774 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
  1775 
  1776 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
  1777   dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
  1778 apply(induct xs)
  1779  apply simp
  1780 apply auto
  1781 apply(subst dropWhile_append2)
  1782 apply auto
  1783 done
  1784 
  1785 lemma takeWhile_not_last:
  1786  "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
  1787 apply(induct xs)
  1788  apply simp
  1789 apply(case_tac xs)
  1790 apply(auto)
  1791 done
  1792 
  1793 lemma takeWhile_cong [fundef_cong, recdef_cong]:
  1794   "[| l = k; !!x. x : set l ==> P x = Q x |] 
  1795   ==> takeWhile P l = takeWhile Q k"
  1796 by (induct k arbitrary: l) (simp_all)
  1797 
  1798 lemma dropWhile_cong [fundef_cong, recdef_cong]:
  1799   "[| l = k; !!x. x : set l ==> P x = Q x |] 
  1800   ==> dropWhile P l = dropWhile Q k"
  1801 by (induct k arbitrary: l, simp_all)
  1802 
  1803 
  1804 subsubsection {* @{text zip} *}
  1805 
  1806 lemma zip_Nil [simp]: "zip [] ys = []"
  1807 by (induct ys) auto
  1808 
  1809 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
  1810 by simp
  1811 
  1812 declare zip_Cons [simp del]
  1813 
  1814 lemma zip_Cons1:
  1815  "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
  1816 by(auto split:list.split)
  1817 
  1818 lemma length_zip [simp]:
  1819 "length (zip xs ys) = min (length xs) (length ys)"
  1820 by (induct xs ys rule:list_induct2') auto
  1821 
  1822 lemma zip_append1:
  1823 "zip (xs @ ys) zs =
  1824 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
  1825 by (induct xs zs rule:list_induct2') auto
  1826 
  1827 lemma zip_append2:
  1828 "zip xs (ys @ zs) =
  1829 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
  1830 by (induct xs ys rule:list_induct2') auto
  1831 
  1832 lemma zip_append [simp]:
  1833  "[| length xs = length us; length ys = length vs |] ==>
  1834 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
  1835 by (simp add: zip_append1)
  1836 
  1837 lemma zip_rev:
  1838 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
  1839 by (induct rule:list_induct2, simp_all)
  1840 
  1841 lemma map_zip_map:
  1842  "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
  1843 apply(induct xs arbitrary:ys) apply simp
  1844 apply(case_tac ys)
  1845 apply simp_all
  1846 done
  1847 
  1848 lemma map_zip_map2:
  1849  "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
  1850 apply(induct xs arbitrary:ys) apply simp
  1851 apply(case_tac ys)
  1852 apply simp_all
  1853 done
  1854 
  1855 text{* Courtesy of Andreas Lochbihler: *}
  1856 lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"
  1857 by(induct xs) auto
  1858 
  1859 lemma nth_zip [simp]:
  1860 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
  1861 apply (induct ys arbitrary: i xs, simp)
  1862 apply (case_tac xs)
  1863  apply (simp_all add: nth.simps split: nat.split)
  1864 done
  1865 
  1866 lemma set_zip:
  1867 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
  1868 by(simp add: set_conv_nth cong: rev_conj_cong)
  1869 
  1870 lemma zip_update:
  1871   "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
  1872 by(rule sym, simp add: update_zip)
  1873 
  1874 lemma zip_replicate [simp]:
  1875   "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
  1876 apply (induct i arbitrary: j, auto)
  1877 apply (case_tac j, auto)
  1878 done
  1879 
  1880 lemma take_zip:
  1881   "take n (zip xs ys) = zip (take n xs) (take n ys)"
  1882 apply (induct n arbitrary: xs ys)
  1883  apply simp
  1884 apply (case_tac xs, simp)
  1885 apply (case_tac ys, simp_all)
  1886 done
  1887 
  1888 lemma drop_zip:
  1889   "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
  1890 apply (induct n arbitrary: xs ys)
  1891  apply simp
  1892 apply (case_tac xs, simp)
  1893 apply (case_tac ys, simp_all)
  1894 done
  1895 
  1896 lemma set_zip_leftD:
  1897   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
  1898 by (induct xs ys rule:list_induct2') auto
  1899 
  1900 lemma set_zip_rightD:
  1901   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
  1902 by (induct xs ys rule:list_induct2') auto
  1903 
  1904 lemma in_set_zipE:
  1905   "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
  1906 by(blast dest: set_zip_leftD set_zip_rightD)
  1907 
  1908 lemma zip_map_fst_snd:
  1909   "zip (map fst zs) (map snd zs) = zs"
  1910   by (induct zs) simp_all
  1911 
  1912 lemma zip_eq_conv:
  1913   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
  1914   by (auto simp add: zip_map_fst_snd)
  1915 
  1916 
  1917 subsubsection {* @{text list_all2} *}
  1918 
  1919 lemma list_all2_lengthD [intro?]: 
  1920   "list_all2 P xs ys ==> length xs = length ys"
  1921 by (simp add: list_all2_def)
  1922 
  1923 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
  1924 by (simp add: list_all2_def)
  1925 
  1926 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
  1927 by (simp add: list_all2_def)
  1928 
  1929 lemma list_all2_Cons [iff, code]:
  1930   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
  1931 by (auto simp add: list_all2_def)
  1932 
  1933 lemma list_all2_Cons1:
  1934 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
  1935 by (cases ys) auto
  1936 
  1937 lemma list_all2_Cons2:
  1938 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
  1939 by (cases xs) auto
  1940 
  1941 lemma list_all2_rev [iff]:
  1942 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
  1943 by (simp add: list_all2_def zip_rev cong: conj_cong)
  1944 
  1945 lemma list_all2_rev1:
  1946 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
  1947 by (subst list_all2_rev [symmetric]) simp
  1948 
  1949 lemma list_all2_append1:
  1950 "list_all2 P (xs @ ys) zs =
  1951 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
  1952 list_all2 P xs us \<and> list_all2 P ys vs)"
  1953 apply (simp add: list_all2_def zip_append1)
  1954 apply (rule iffI)
  1955  apply (rule_tac x = "take (length xs) zs" in exI)
  1956  apply (rule_tac x = "drop (length xs) zs" in exI)
  1957  apply (force split: nat_diff_split simp add: min_def, clarify)
  1958 apply (simp add: ball_Un)
  1959 done
  1960 
  1961 lemma list_all2_append2:
  1962 "list_all2 P xs (ys @ zs) =
  1963 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
  1964 list_all2 P us ys \<and> list_all2 P vs zs)"
  1965 apply (simp add: list_all2_def zip_append2)
  1966 apply (rule iffI)
  1967  apply (rule_tac x = "take (length ys) xs" in exI)
  1968  apply (rule_tac x = "drop (length ys) xs" in exI)
  1969  apply (force split: nat_diff_split simp add: min_def, clarify)
  1970 apply (simp add: ball_Un)
  1971 done
  1972 
  1973 lemma list_all2_append:
  1974   "length xs = length ys \<Longrightarrow>
  1975   list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
  1976 by (induct rule:list_induct2, simp_all)
  1977 
  1978 lemma list_all2_appendI [intro?, trans]:
  1979   "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
  1980 by (simp add: list_all2_append list_all2_lengthD)
  1981 
  1982 lemma list_all2_conv_all_nth:
  1983 "list_all2 P xs ys =
  1984 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
  1985 by (force simp add: list_all2_def set_zip)
  1986 
  1987 lemma list_all2_trans:
  1988   assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
  1989   shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
  1990         (is "!!bs cs. PROP ?Q as bs cs")
  1991 proof (induct as)
  1992   fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
  1993   show "!!cs. PROP ?Q (x # xs) bs cs"
  1994   proof (induct bs)
  1995     fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
  1996     show "PROP ?Q (x # xs) (y # ys) cs"
  1997       by (induct cs) (auto intro: tr I1 I2)
  1998   qed simp
  1999 qed simp
  2000 
  2001 lemma list_all2_all_nthI [intro?]:
  2002   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
  2003 by (simp add: list_all2_conv_all_nth)
  2004 
  2005 lemma list_all2I:
  2006   "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
  2007 by (simp add: list_all2_def)
  2008 
  2009 lemma list_all2_nthD:
  2010   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
  2011 by (simp add: list_all2_conv_all_nth)
  2012 
  2013 lemma list_all2_nthD2:
  2014   "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
  2015 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
  2016 
  2017 lemma list_all2_map1: 
  2018   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
  2019 by (simp add: list_all2_conv_all_nth)
  2020 
  2021 lemma list_all2_map2: 
  2022   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
  2023 by (auto simp add: list_all2_conv_all_nth)
  2024 
  2025 lemma list_all2_refl [intro?]:
  2026   "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
  2027 by (simp add: list_all2_conv_all_nth)
  2028 
  2029 lemma list_all2_update_cong:
  2030   "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  2031 by (simp add: list_all2_conv_all_nth nth_list_update)
  2032 
  2033 lemma list_all2_update_cong2:
  2034   "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  2035 by (simp add: list_all2_lengthD list_all2_update_cong)
  2036 
  2037 lemma list_all2_takeI [simp,intro?]:
  2038   "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
  2039 apply (induct xs arbitrary: n ys)
  2040  apply simp
  2041 apply (clarsimp simp add: list_all2_Cons1)
  2042 apply (case_tac n)
  2043 apply auto
  2044 done
  2045 
  2046 lemma list_all2_dropI [simp,intro?]:
  2047   "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
  2048 apply (induct as arbitrary: n bs, simp)
  2049 apply (clarsimp simp add: list_all2_Cons1)
  2050 apply (case_tac n, simp, simp)
  2051 done
  2052 
  2053 lemma list_all2_mono [intro?]:
  2054   "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
  2055 apply (induct xs arbitrary: ys, simp)
  2056 apply (case_tac ys, auto)
  2057 done
  2058 
  2059 lemma list_all2_eq:
  2060   "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
  2061 by (induct xs ys rule: list_induct2') auto
  2062 
  2063 
  2064 subsubsection {* @{text foldl} and @{text foldr} *}
  2065 
  2066 lemma foldl_append [simp]:
  2067   "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
  2068 by (induct xs arbitrary: a) auto
  2069 
  2070 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
  2071 by (induct xs) auto
  2072 
  2073 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
  2074 by(induct xs) simp_all
  2075 
  2076 text{* For efficient code generation: avoid intermediate list. *}
  2077 lemma foldl_map[code_unfold]:
  2078   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
  2079 by(induct xs arbitrary:a) simp_all
  2080 
  2081 lemma foldl_apply_inv:
  2082   assumes "\<And>x. g (h x) = x"
  2083   shows "foldl f (g s) xs = g (foldl (\<lambda>s x. h (f (g s) x)) s xs)"
  2084   by (rule sym, induct xs arbitrary: s) (simp_all add: assms)
  2085 
  2086 lemma foldl_cong [fundef_cong, recdef_cong]:
  2087   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
  2088   ==> foldl f a l = foldl g b k"
  2089 by (induct k arbitrary: a b l) simp_all
  2090 
  2091 lemma foldr_cong [fundef_cong, recdef_cong]:
  2092   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
  2093   ==> foldr f l a = foldr g k b"
  2094 by (induct k arbitrary: a b l) simp_all
  2095 
  2096 lemma (in semigroup_add) foldl_assoc:
  2097 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
  2098 by (induct zs arbitrary: y) (simp_all add:add_assoc)
  2099 
  2100 lemma (in monoid_add) foldl_absorb0:
  2101 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
  2102 by (induct zs) (simp_all add:foldl_assoc)
  2103 
  2104 
  2105 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
  2106 
  2107 lemma foldl_foldr1_lemma:
  2108  "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
  2109 by (induct xs arbitrary: a) (auto simp:add_assoc)
  2110 
  2111 corollary foldl_foldr1:
  2112  "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
  2113 by (simp add:foldl_foldr1_lemma)
  2114 
  2115 
  2116 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
  2117 
  2118 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
  2119 by (induct xs) auto
  2120 
  2121 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
  2122 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
  2123 
  2124 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
  2125   by (induct xs, auto simp add: foldl_assoc add_commute)
  2126 
  2127 text {*
  2128 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
  2129 difficult to use because it requires an additional transitivity step.
  2130 *}
  2131 
  2132 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
  2133 by (induct ns arbitrary: n) auto
  2134 
  2135 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
  2136 by (force intro: start_le_sum simp add: in_set_conv_decomp)
  2137 
  2138 lemma sum_eq_0_conv [iff]:
  2139   "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
  2140 by (induct ns arbitrary: m) auto
  2141 
  2142 lemma foldr_invariant: 
  2143   "\<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)"
  2144   by (induct xs, simp_all)
  2145 
  2146 lemma foldl_invariant: 
  2147   "\<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)"
  2148   by (induct xs arbitrary: x, simp_all)
  2149 
  2150 text {* @{const foldl} and @{const concat} *}
  2151 
  2152 lemma foldl_conv_concat:
  2153   "foldl (op @) xs xss = xs @ concat xss"
  2154 proof (induct xss arbitrary: xs)
  2155   case Nil show ?case by simp
  2156 next
  2157   interpret monoid_add "[]" "op @" proof qed simp_all
  2158   case Cons then show ?case by (simp add: foldl_absorb0)
  2159 qed
  2160 
  2161 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
  2162   by (simp add: foldl_conv_concat)
  2163 
  2164 text {* @{const Finite_Set.fold} and @{const foldl} *}
  2165 
  2166 lemma (in fun_left_comm_idem) fold_set:
  2167   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"
  2168   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)
  2169 
  2170 
  2171 
  2172 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
  2173 
  2174 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
  2175 by (induct xs) (simp_all add:add_assoc)
  2176 
  2177 lemma listsum_rev [simp]:
  2178   fixes xs :: "'a\<Colon>comm_monoid_add list"
  2179   shows "listsum (rev xs) = listsum xs"
  2180 by (induct xs) (simp_all add:add_ac)
  2181 
  2182 lemma listsum_map_remove1:
  2183 fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"
  2184 shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"
  2185 by (induct xs)(auto simp add:add_ac)
  2186 
  2187 lemma list_size_conv_listsum:
  2188   "list_size f xs = listsum (map f xs) + size xs"
  2189 by(induct xs) auto
  2190 
  2191 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
  2192 by (induct xs) auto
  2193 
  2194 lemma length_concat: "length (concat xss) = listsum (map length xss)"
  2195 by (induct xss) simp_all
  2196 
  2197 text{* For efficient code generation ---
  2198        @{const listsum} is not tail recursive but @{const foldl} is. *}
  2199 lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"
  2200 by(simp add:listsum_foldr foldl_foldr1)
  2201 
  2202 lemma distinct_listsum_conv_Setsum:
  2203   "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"
  2204 by (induct xs) simp_all
  2205 
  2206 
  2207 text{* Some syntactic sugar for summing a function over a list: *}
  2208 
  2209 syntax
  2210   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
  2211 syntax (xsymbols)
  2212   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2213 syntax (HTML output)
  2214   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2215 
  2216 translations -- {* Beware of argument permutation! *}
  2217   "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
  2218   "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
  2219 
  2220 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
  2221   by (induct xs) (simp_all add: left_distrib)
  2222 
  2223 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
  2224   by (induct xs) (simp_all add: left_distrib)
  2225 
  2226 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
  2227 lemma uminus_listsum_map:
  2228   fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
  2229   shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
  2230 by (induct xs) simp_all
  2231 
  2232 lemma listsum_addf:
  2233   fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"
  2234   shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
  2235 by (induct xs) (simp_all add: algebra_simps)
  2236 
  2237 lemma listsum_subtractf:
  2238   fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"
  2239   shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
  2240 by (induct xs) simp_all
  2241 
  2242 lemma listsum_const_mult:
  2243   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
  2244   shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
  2245 by (induct xs, simp_all add: algebra_simps)
  2246 
  2247 lemma listsum_mult_const:
  2248   fixes f :: "'a \<Rightarrow> 'b::semiring_0"
  2249   shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
  2250 by (induct xs, simp_all add: algebra_simps)
  2251 
  2252 lemma listsum_abs:
  2253   fixes xs :: "'a::pordered_ab_group_add_abs list"
  2254   shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
  2255 by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])
  2256 
  2257 lemma listsum_mono:
  2258   fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, pordered_ab_semigroup_add}"
  2259   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)"
  2260 by (induct xs, simp, simp add: add_mono)
  2261 
  2262 
  2263 subsubsection {* @{text upt} *}
  2264 
  2265 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
  2266 -- {* simp does not terminate! *}
  2267 by (induct j) auto
  2268 
  2269 lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
  2270 
  2271 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
  2272 by (subst upt_rec) simp
  2273 
  2274 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
  2275 by(induct j)simp_all
  2276 
  2277 lemma upt_eq_Cons_conv:
  2278  "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
  2279 apply(induct j arbitrary: x xs)
  2280  apply simp
  2281 apply(clarsimp simp add: append_eq_Cons_conv)
  2282 apply arith
  2283 done
  2284 
  2285 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
  2286 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
  2287 by simp
  2288 
  2289 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
  2290   by (simp add: upt_rec)
  2291 
  2292 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
  2293 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
  2294 by (induct k) auto
  2295 
  2296 lemma length_upt [simp]: "length [i..<j] = j - i"
  2297 by (induct j) (auto simp add: Suc_diff_le)
  2298 
  2299 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
  2300 apply (induct j)
  2301 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
  2302 done
  2303 
  2304 
  2305 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
  2306 by(simp add:upt_conv_Cons)
  2307 
  2308 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
  2309 apply(cases j)
  2310  apply simp
  2311 by(simp add:upt_Suc_append)
  2312 
  2313 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
  2314 apply (induct m arbitrary: i, simp)
  2315 apply (subst upt_rec)
  2316 apply (rule sym)
  2317 apply (subst upt_rec)
  2318 apply (simp del: upt.simps)
  2319 done
  2320 
  2321 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
  2322 apply(induct j)
  2323 apply auto
  2324 done
  2325 
  2326 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
  2327 by (induct n) auto
  2328 
  2329 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
  2330 apply (induct n m  arbitrary: i rule: diff_induct)
  2331 prefer 3 apply (subst map_Suc_upt[symmetric])
  2332 apply (auto simp add: less_diff_conv nth_upt)
  2333 done
  2334 
  2335 lemma nth_take_lemma:
  2336   "k <= length xs ==> k <= length ys ==>
  2337      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
  2338 apply (atomize, induct k arbitrary: xs ys)
  2339 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
  2340 txt {* Both lists must be non-empty *}
  2341 apply (case_tac xs, simp)
  2342 apply (case_tac ys, clarify)
  2343  apply (simp (no_asm_use))
  2344 apply clarify
  2345 txt {* prenexing's needed, not miniscoping *}
  2346 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
  2347 apply blast
  2348 done
  2349 
  2350 lemma nth_equalityI:
  2351  "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
  2352 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
  2353 apply (simp_all add: take_all)
  2354 done
  2355 
  2356 lemma map_nth:
  2357   "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
  2358   by (rule nth_equalityI, auto)
  2359 
  2360 (* needs nth_equalityI *)
  2361 lemma list_all2_antisym:
  2362   "\<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> 
  2363   \<Longrightarrow> xs = ys"
  2364   apply (simp add: list_all2_conv_all_nth) 
  2365   apply (rule nth_equalityI, blast, simp)
  2366   done
  2367 
  2368 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
  2369 -- {* The famous take-lemma. *}
  2370 apply (drule_tac x = "max (length xs) (length ys)" in spec)
  2371 apply (simp add: le_max_iff_disj take_all)
  2372 done
  2373 
  2374 
  2375 lemma take_Cons':
  2376      "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
  2377 by (cases n) simp_all
  2378 
  2379 lemma drop_Cons':
  2380      "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
  2381 by (cases n) simp_all
  2382 
  2383 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
  2384 by (cases n) simp_all
  2385 
  2386 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
  2387 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
  2388 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
  2389 
  2390 declare take_Cons_number_of [simp] 
  2391         drop_Cons_number_of [simp] 
  2392         nth_Cons_number_of [simp] 
  2393 
  2394 
  2395 subsubsection {* @{text upto}: interval-list on @{typ int} *}
  2396 
  2397 (* FIXME make upto tail recursive? *)
  2398 
  2399 function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
  2400 "upto i j = (if i \<le> j then i # [i+1..j] else [])"
  2401 by auto
  2402 termination
  2403 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
  2404 
  2405 declare upto.simps[code, simp del]
  2406 
  2407 lemmas upto_rec_number_of[simp] =
  2408   upto.simps[of "number_of m" "number_of n", standard]
  2409 
  2410 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
  2411 by(simp add: upto.simps)
  2412 
  2413 lemma set_upto[simp]: "set[i..j] = {i..j}"
  2414 apply(induct i j rule:upto.induct)
  2415 apply(simp add: upto.simps simp_from_to)
  2416 done
  2417 
  2418 
  2419 subsubsection {* @{text "distinct"} and @{text remdups} *}
  2420 
  2421 lemma distinct_append [simp]:
  2422 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
  2423 by (induct xs) auto
  2424 
  2425 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
  2426 by(induct xs) auto
  2427 
  2428 lemma set_remdups [simp]: "set (remdups xs) = set xs"
  2429 by (induct xs) (auto simp add: insert_absorb)
  2430 
  2431 lemma distinct_remdups [iff]: "distinct (remdups xs)"
  2432 by (induct xs) auto
  2433 
  2434 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
  2435 by (induct xs, auto)
  2436 
  2437 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
  2438 by (metis distinct_remdups distinct_remdups_id)
  2439 
  2440 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
  2441 by (metis distinct_remdups finite_list set_remdups)
  2442 
  2443 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
  2444 by (induct x, auto) 
  2445 
  2446 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
  2447 by (induct x, auto)
  2448 
  2449 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
  2450 by (induct xs) auto
  2451 
  2452 lemma length_remdups_eq[iff]:
  2453   "(length (remdups xs) = length xs) = (remdups xs = xs)"
  2454 apply(induct xs)
  2455  apply auto
  2456 apply(subgoal_tac "length (remdups xs) <= length xs")
  2457  apply arith
  2458 apply(rule length_remdups_leq)
  2459 done
  2460 
  2461 
  2462 lemma distinct_map:
  2463   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
  2464 by (induct xs) auto
  2465 
  2466 
  2467 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
  2468 by (induct xs) auto
  2469 
  2470 lemma distinct_upt[simp]: "distinct[i..<j]"
  2471 by (induct j) auto
  2472 
  2473 lemma distinct_upto[simp]: "distinct[i..j]"
  2474 apply(induct i j rule:upto.induct)
  2475 apply(subst upto.simps)
  2476 apply(simp)
  2477 done
  2478 
  2479 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
  2480 apply(induct xs arbitrary: i)
  2481  apply simp
  2482 apply (case_tac i)
  2483  apply simp_all
  2484 apply(blast dest:in_set_takeD)
  2485 done
  2486 
  2487 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
  2488 apply(induct xs arbitrary: i)
  2489  apply simp
  2490 apply (case_tac i)
  2491  apply simp_all
  2492 done
  2493 
  2494 lemma distinct_list_update:
  2495 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
  2496 shows "distinct (xs[i:=a])"
  2497 proof (cases "i < length xs")
  2498   case True
  2499   with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
  2500     apply (drule_tac id_take_nth_drop) by simp
  2501   with d True show ?thesis
  2502     apply (simp add: upd_conv_take_nth_drop)
  2503     apply (drule subst [OF id_take_nth_drop]) apply assumption
  2504     apply simp apply (cases "a = xs!i") apply simp by blast
  2505 next
  2506   case False with d show ?thesis by auto
  2507 qed
  2508 
  2509 lemma distinct_concat:
  2510   assumes "distinct xs"
  2511   and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"
  2512   and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"
  2513   shows "distinct (concat xs)"
  2514   using assms by (induct xs) auto
  2515 
  2516 text {* It is best to avoid this indexed version of distinct, but
  2517 sometimes it is useful. *}
  2518 
  2519 lemma distinct_conv_nth:
  2520 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
  2521 apply (induct xs, simp, simp)
  2522 apply (rule iffI, clarsimp)
  2523  apply (case_tac i)
  2524 apply (case_tac j, simp)
  2525 apply (simp add: set_conv_nth)
  2526  apply (case_tac j)
  2527 apply (clarsimp simp add: set_conv_nth, simp) 
  2528 apply (rule conjI)
  2529 (*TOO SLOW
  2530 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2531 *)
  2532  apply (clarsimp simp add: set_conv_nth)
  2533  apply (erule_tac x = 0 in allE, simp)
  2534  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
  2535 (*TOO SLOW
  2536 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
  2537 *)
  2538 apply (erule_tac x = "Suc i" in allE, simp)
  2539 apply (erule_tac x = "Suc j" in allE, simp)
  2540 done
  2541 
  2542 lemma nth_eq_iff_index_eq:
  2543  "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
  2544 by(auto simp: distinct_conv_nth)
  2545 
  2546 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
  2547 by (induct xs) auto
  2548 
  2549 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
  2550 proof (induct xs)
  2551   case Nil thus ?case by simp
  2552 next
  2553   case (Cons x xs)
  2554   show ?case
  2555   proof (cases "x \<in> set xs")
  2556     case False with Cons show ?thesis by simp
  2557   next
  2558     case True with Cons.prems
  2559     have "card (set xs) = Suc (length xs)" 
  2560       by (simp add: card_insert_if split: split_if_asm)
  2561     moreover have "card (set xs) \<le> length xs" by (rule card_length)
  2562     ultimately have False by simp
  2563     thus ?thesis ..
  2564   qed
  2565 qed
  2566 
  2567 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
  2568 apply (induct n == "length ws" arbitrary:ws) apply simp
  2569 apply(case_tac ws) apply simp
  2570 apply (simp split:split_if_asm)
  2571 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
  2572 done
  2573 
  2574 lemma length_remdups_concat:
  2575  "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
  2576 by(simp add: set_concat distinct_card[symmetric])
  2577 
  2578 
  2579 subsubsection {* @{text remove1} *}
  2580 
  2581 lemma remove1_append:
  2582   "remove1 x (xs @ ys) =
  2583   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
  2584 by (induct xs) auto
  2585 
  2586 lemma in_set_remove1[simp]:
  2587   "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
  2588 apply (induct xs)
  2589 apply auto
  2590 done
  2591 
  2592 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
  2593 apply(induct xs)
  2594  apply simp
  2595 apply simp
  2596 apply blast
  2597 done
  2598 
  2599 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
  2600 apply(induct xs)
  2601  apply simp
  2602 apply simp
  2603 apply blast
  2604 done
  2605 
  2606 lemma length_remove1:
  2607   "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
  2608 apply (induct xs)
  2609  apply (auto dest!:length_pos_if_in_set)
  2610 done
  2611 
  2612 lemma remove1_filter_not[simp]:
  2613   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
  2614 by(induct xs) auto
  2615 
  2616 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
  2617 apply(insert set_remove1_subset)
  2618 apply fast
  2619 done
  2620 
  2621 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
  2622 by (induct xs) simp_all
  2623 
  2624 
  2625 subsubsection {* @{text removeAll} *}
  2626 
  2627 lemma removeAll_append[simp]:
  2628   "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
  2629 by (induct xs) auto
  2630 
  2631 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
  2632 by (induct xs) auto
  2633 
  2634 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
  2635 by (induct xs) auto
  2636 
  2637 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
  2638 lemma length_removeAll:
  2639   "length(removeAll x xs) = length xs - count x xs"
  2640 *)
  2641 
  2642 lemma removeAll_filter_not[simp]:
  2643   "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
  2644 by(induct xs) auto
  2645 
  2646 
  2647 lemma distinct_remove1_removeAll:
  2648   "distinct xs ==> remove1 x xs = removeAll x xs"
  2649 by (induct xs) simp_all
  2650 
  2651 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
  2652   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  2653 by (induct xs) (simp_all add:inj_on_def)
  2654 
  2655 lemma map_removeAll_inj: "inj f \<Longrightarrow>
  2656   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  2657 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
  2658 
  2659 
  2660 subsubsection {* @{text replicate} *}
  2661 
  2662 lemma length_replicate [simp]: "length (replicate n x) = n"
  2663 by (induct n) auto
  2664 
  2665 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
  2666 by (induct n) auto
  2667 
  2668 lemma map_replicate_const:
  2669   "map (\<lambda> x. k) lst = replicate (length lst) k"
  2670   by (induct lst) auto
  2671 
  2672 lemma replicate_app_Cons_same:
  2673 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
  2674 by (induct n) auto
  2675 
  2676 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
  2677 apply (induct n, simp)
  2678 apply (simp add: replicate_app_Cons_same)
  2679 done
  2680 
  2681 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
  2682 by (induct n) auto
  2683 
  2684 text{* Courtesy of Matthias Daum: *}
  2685 lemma append_replicate_commute:
  2686   "replicate n x @ replicate k x = replicate k x @ replicate n x"
  2687 apply (simp add: replicate_add [THEN sym])
  2688 apply (simp add: add_commute)
  2689 done
  2690 
  2691 text{* Courtesy of Andreas Lochbihler: *}
  2692 lemma filter_replicate:
  2693   "filter P (replicate n x) = (if P x then replicate n x else [])"
  2694 by(induct n) auto
  2695 
  2696 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
  2697 by (induct n) auto
  2698 
  2699 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
  2700 by (induct n) auto
  2701 
  2702 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
  2703 by (atomize (full), induct n) auto
  2704 
  2705 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
  2706 apply (induct n arbitrary: i, simp)
  2707 apply (simp add: nth_Cons split: nat.split)
  2708 done
  2709 
  2710 text{* Courtesy of Matthias Daum (2 lemmas): *}
  2711 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
  2712 apply (case_tac "k \<le> i")
  2713  apply  (simp add: min_def)
  2714 apply (drule not_leE)
  2715 apply (simp add: min_def)
  2716 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
  2717  apply  simp
  2718 apply (simp add: replicate_add [symmetric])
  2719 done
  2720 
  2721 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
  2722 apply (induct k arbitrary: i)
  2723  apply simp
  2724 apply clarsimp
  2725 apply (case_tac i)
  2726  apply simp
  2727 apply clarsimp
  2728 done
  2729 
  2730 
  2731 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
  2732 by (induct n) auto
  2733 
  2734 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
  2735 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
  2736 
  2737 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
  2738 by auto
  2739 
  2740 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
  2741 by (simp add: set_replicate_conv_if split: split_if_asm)
  2742 
  2743 lemma replicate_append_same:
  2744   "replicate i x @ [x] = x # replicate i x"
  2745   by (induct i) simp_all
  2746 
  2747 lemma map_replicate_trivial:
  2748   "map (\<lambda>i. x) [0..<i] = replicate i x"
  2749   by (induct i) (simp_all add: replicate_append_same)
  2750 
  2751 lemma concat_replicate_trivial[simp]:
  2752   "concat (replicate i []) = []"
  2753   by (induct i) (auto simp add: map_replicate_const)
  2754 
  2755 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
  2756 by (induct n) auto
  2757 
  2758 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
  2759 by (induct n) auto
  2760 
  2761 lemma replicate_eq_replicate[simp]:
  2762   "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
  2763 apply(induct m arbitrary: n)
  2764  apply simp
  2765 apply(induct_tac n)
  2766 apply auto
  2767 done
  2768 
  2769 
  2770 subsubsection{*@{text rotate1} and @{text rotate}*}
  2771 
  2772 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
  2773 by(simp add:rotate1_def)
  2774 
  2775 lemma rotate0[simp]: "rotate 0 = id"
  2776 by(simp add:rotate_def)
  2777 
  2778 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
  2779 by(simp add:rotate_def)
  2780 
  2781 lemma rotate_add:
  2782   "rotate (m+n) = rotate m o rotate n"
  2783 by(simp add:rotate_def funpow_add)
  2784 
  2785 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
  2786 by(simp add:rotate_add)
  2787 
  2788 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
  2789 by(simp add:rotate_def funpow_swap1)
  2790 
  2791 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
  2792 by(cases xs) simp_all
  2793 
  2794 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
  2795 apply(induct n)
  2796  apply simp
  2797 apply (simp add:rotate_def)
  2798 done
  2799 
  2800 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
  2801 by(simp add:rotate1_def split:list.split)
  2802 
  2803 lemma rotate_drop_take:
  2804   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
  2805 apply(induct n)
  2806  apply simp
  2807 apply(simp add:rotate_def)
  2808 apply(cases "xs = []")
  2809  apply (simp)
  2810 apply(case_tac "n mod length xs = 0")
  2811  apply(simp add:mod_Suc)
  2812  apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
  2813 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
  2814                 take_hd_drop linorder_not_le)
  2815 done
  2816 
  2817 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
  2818 by(simp add:rotate_drop_take)
  2819 
  2820 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
  2821 by(simp add:rotate_drop_take)
  2822 
  2823 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
  2824 by(simp add:rotate1_def split:list.split)
  2825 
  2826 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
  2827 by (induct n arbitrary: xs) (simp_all add:rotate_def)
  2828 
  2829 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
  2830 by(simp add:rotate1_def split:list.split) blast
  2831 
  2832 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
  2833 by (induct n) (simp_all add:rotate_def)
  2834 
  2835 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
  2836 by(simp add:rotate_drop_take take_map drop_map)
  2837 
  2838 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
  2839 by(simp add:rotate1_def split:list.split)
  2840 
  2841 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
  2842 by (induct n) (simp_all add:rotate_def)
  2843 
  2844 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
  2845 by(simp add:rotate1_def split:list.split)
  2846 
  2847 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
  2848 by (induct n) (simp_all add:rotate_def)
  2849 
  2850 lemma rotate_rev:
  2851   "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
  2852 apply(simp add:rotate_drop_take rev_drop rev_take)
  2853 apply(cases "length xs = 0")
  2854  apply simp
  2855 apply(cases "n mod length xs = 0")
  2856  apply simp
  2857 apply(simp add:rotate_drop_take rev_drop rev_take)
  2858 done
  2859 
  2860 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
  2861 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
  2862 apply(subgoal_tac "length xs \<noteq> 0")
  2863  prefer 2 apply simp
  2864 using mod_less_divisor[of "length xs" n] by arith
  2865 
  2866 
  2867 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
  2868 
  2869 lemma sublist_empty [simp]: "sublist xs {} = []"
  2870 by (auto simp add: sublist_def)
  2871 
  2872 lemma sublist_nil [simp]: "sublist [] A = []"
  2873 by (auto simp add: sublist_def)
  2874 
  2875 lemma length_sublist:
  2876   "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
  2877 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
  2878 
  2879 lemma sublist_shift_lemma_Suc:
  2880   "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
  2881    map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
  2882 apply(induct xs arbitrary: "is")
  2883  apply simp
  2884 apply (case_tac "is")
  2885  apply simp
  2886 apply simp
  2887 done
  2888 
  2889 lemma sublist_shift_lemma:
  2890      "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
  2891       map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
  2892 by (induct xs rule: rev_induct) (simp_all add: add_commute)
  2893 
  2894 lemma sublist_append:
  2895      "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
  2896 apply (unfold sublist_def)
  2897 apply (induct l' rule: rev_induct, simp)
  2898 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
  2899 apply (simp add: add_commute)
  2900 done
  2901 
  2902 lemma sublist_Cons:
  2903 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
  2904 apply (induct l rule: rev_induct)
  2905  apply (simp add: sublist_def)
  2906 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
  2907 done
  2908 
  2909 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
  2910 apply(induct xs arbitrary: I)
  2911 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  2912 done
  2913 
  2914 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
  2915 by(auto simp add:set_sublist)
  2916 
  2917 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
  2918 by(auto simp add:set_sublist)
  2919 
  2920 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
  2921 by(auto simp add:set_sublist)
  2922 
  2923 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
  2924 by (simp add: sublist_Cons)
  2925 
  2926 
  2927 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
  2928 apply(induct xs arbitrary: I)
  2929  apply simp
  2930 apply(auto simp add:sublist_Cons)
  2931 done
  2932 
  2933 
  2934 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
  2935 apply (induct l rule: rev_induct, simp)
  2936 apply (simp split: nat_diff_split add: sublist_append)
  2937 done
  2938 
  2939 lemma filter_in_sublist:
  2940  "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
  2941 proof (induct xs arbitrary: s)
  2942   case Nil thus ?case by simp
  2943 next
  2944   case (Cons a xs)
  2945   moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
  2946   ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
  2947 qed
  2948 
  2949 
  2950 subsubsection {* @{const splice} *}
  2951 
  2952 lemma splice_Nil2 [simp, code]:
  2953  "splice xs [] = xs"
  2954 by (cases xs) simp_all
  2955 
  2956 lemma splice_Cons_Cons [simp, code]:
  2957  "splice (x#xs) (y#ys) = x # y # splice xs ys"
  2958 by simp
  2959 
  2960 declare splice.simps(2) [simp del, code del]
  2961 
  2962 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  2963 apply(induct xs arbitrary: ys) apply simp
  2964 apply(case_tac ys)
  2965  apply auto
  2966 done
  2967 
  2968 
  2969 subsubsection {* (In)finiteness *}
  2970 
  2971 lemma finite_maxlen:
  2972   "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
  2973 proof (induct rule: finite.induct)
  2974   case emptyI show ?case by simp
  2975 next
  2976   case (insertI M xs)
  2977   then obtain n where "\<forall>s\<in>M. length s < n" by blast
  2978   hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
  2979   thus ?case ..
  2980 qed
  2981 
  2982 lemma finite_lists_length_eq:
  2983 assumes "finite A"
  2984 shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
  2985 proof(induct n)
  2986   case 0 show ?case by simp
  2987 next
  2988   case (Suc n)
  2989   have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
  2990     by (auto simp:length_Suc_conv)
  2991   then show ?case using `finite A`
  2992     by (auto intro: finite_imageI Suc) (* FIXME metis? *)
  2993 qed
  2994 
  2995 lemma finite_lists_length_le:
  2996   assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
  2997  (is "finite ?S")
  2998 proof-
  2999   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
  3000   thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
  3001 qed
  3002 
  3003 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
  3004 apply(rule notI)
  3005 apply(drule finite_maxlen)
  3006 apply (metis UNIV_I length_replicate less_not_refl)
  3007 done
  3008 
  3009 
  3010 subsection {*Sorting*}
  3011 
  3012 text{* Currently it is not shown that @{const sort} returns a
  3013 permutation of its input because the nicest proof is via multisets,
  3014 which are not yet available. Alternatively one could define a function
  3015 that counts the number of occurrences of an element in a list and use
  3016 that instead of multisets to state the correctness property. *}
  3017 
  3018 context linorder
  3019 begin
  3020 
  3021 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
  3022 apply(induct xs arbitrary: x) apply simp
  3023 by simp (blast intro: order_trans)
  3024 
  3025 lemma sorted_append:
  3026   "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
  3027 by (induct xs) (auto simp add:sorted_Cons)
  3028 
  3029 lemma sorted_nth_mono:
  3030   "sorted xs \<Longrightarrow> i <= j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i <= xs!j"
  3031 by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
  3032 
  3033 lemma set_insort: "set(insort x xs) = insert x (set xs)"
  3034 by (induct xs) auto
  3035 
  3036 lemma set_sort[simp]: "set(sort xs) = set xs"
  3037 by (induct xs) (simp_all add:set_insort)
  3038 
  3039 lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
  3040 by(induct xs)(auto simp:set_insort)
  3041 
  3042 lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
  3043 by(induct xs)(simp_all add:distinct_insort set_sort)
  3044 
  3045 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
  3046 apply (induct xs)
  3047  apply(auto simp:sorted_Cons set_insort)
  3048 done
  3049 
  3050 theorem sorted_sort[simp]: "sorted (sort xs)"
  3051 by (induct xs) (auto simp:sorted_insort)
  3052 
  3053 lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
  3054 by (cases xs) auto
  3055 
  3056 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
  3057 by (induct xs, auto simp add: sorted_Cons)
  3058 
  3059 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
  3060 by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
  3061 
  3062 lemma sorted_remdups[simp]:
  3063   "sorted l \<Longrightarrow> sorted (remdups l)"
  3064 by (induct l) (auto simp: sorted_Cons)
  3065 
  3066 lemma sorted_distinct_set_unique:
  3067 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
  3068 shows "xs = ys"
  3069 proof -
  3070   from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
  3071   from assms show ?thesis
  3072   proof(induct rule:list_induct2[OF 1])
  3073     case 1 show ?case by simp
  3074   next
  3075     case 2 thus ?case by (simp add:sorted_Cons)
  3076        (metis Diff_insert_absorb antisym insertE insert_iff)
  3077   qed
  3078 qed
  3079 
  3080 lemma finite_sorted_distinct_unique:
  3081 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
  3082 apply(drule finite_distinct_list)
  3083 apply clarify
  3084 apply(rule_tac a="sort xs" in ex1I)
  3085 apply (auto simp: sorted_distinct_set_unique)
  3086 done
  3087 
  3088 lemma sorted_take:
  3089   "sorted xs \<Longrightarrow> sorted (take n xs)"
  3090 proof (induct xs arbitrary: n rule: sorted.induct)
  3091   case 1 show ?case by simp
  3092 next
  3093   case 2 show ?case by (cases n) simp_all
  3094 next
  3095   case (3 x y xs)
  3096   then have "x \<le> y" by simp
  3097   show ?case proof (cases n)
  3098     case 0 then show ?thesis by simp
  3099   next
  3100     case (Suc m) 
  3101     with 3 have "sorted (take m (y # xs))" by simp
  3102     with Suc  `x \<le> y` show ?thesis by (cases m) simp_all
  3103   qed
  3104 qed
  3105 
  3106 lemma sorted_drop:
  3107   "sorted xs \<Longrightarrow> sorted (drop n xs)"
  3108 proof (induct xs arbitrary: n rule: sorted.induct)
  3109   case 1 show ?case by simp
  3110 next
  3111   case 2 show ?case by (cases n) simp_all
  3112 next
  3113   case 3 then show ?case by (cases n) simp_all
  3114 qed
  3115 
  3116 
  3117 end
  3118 
  3119 lemma sorted_upt[simp]: "sorted[i..<j]"
  3120 by (induct j) (simp_all add:sorted_append)
  3121 
  3122 lemma sorted_upto[simp]: "sorted[i..j]"
  3123 apply(induct i j rule:upto.induct)
  3124 apply(subst upto.simps)
  3125 apply(simp add:sorted_Cons)
  3126 done
  3127 
  3128 
  3129 subsubsection {* @{text sorted_list_of_set} *}
  3130 
  3131 text{* This function maps (finite) linearly ordered sets to sorted
  3132 lists. Warning: in most cases it is not a good idea to convert from
  3133 sets to lists but one should convert in the other direction (via
  3134 @{const set}). *}
  3135 
  3136 
  3137 context linorder
  3138 begin
  3139 
  3140 definition
  3141  sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
  3142  [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
  3143 
  3144 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
  3145   set(sorted_list_of_set A) = A &
  3146   sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
  3147 apply(simp add:sorted_list_of_set_def)
  3148 apply(rule the1I2)
  3149  apply(simp_all add: finite_sorted_distinct_unique)
  3150 done
  3151 
  3152 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
  3153 unfolding sorted_list_of_set_def
  3154 apply(subst the_equality[of _ "[]"])
  3155 apply simp_all
  3156 done
  3157 
  3158 end
  3159 
  3160 
  3161 subsubsection {* @{text lists}: the list-forming operator over sets *}
  3162 
  3163 inductive_set
  3164   lists :: "'a set => 'a list set"
  3165   for A :: "'a set"
  3166 where
  3167     Nil [intro!]: "[]: lists A"
  3168   | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
  3169 
  3170 inductive_cases listsE [elim!,noatp]: "x#l : lists A"
  3171 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
  3172 
  3173 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
  3174 by (rule predicate1I, erule listsp.induct, blast+)
  3175 
  3176 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
  3177 
  3178 lemma listsp_infI:
  3179   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
  3180 by induct blast+
  3181 
  3182 lemmas lists_IntI = listsp_infI [to_set]
  3183 
  3184 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
  3185 proof (rule mono_inf [where f=listsp, THEN order_antisym])
  3186   show "mono listsp" by (simp add: mono_def listsp_mono)
  3187   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
  3188 qed
  3189 
  3190 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
  3191 
  3192 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
  3193 
  3194 lemma append_in_listsp_conv [iff]:
  3195      "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
  3196 by (induct xs) auto
  3197 
  3198 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
  3199 
  3200 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
  3201 -- {* eliminate @{text listsp} in favour of @{text set} *}
  3202 by (induct xs) auto
  3203 
  3204 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
  3205 
  3206 lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
  3207 by (rule in_listsp_conv_set [THEN iffD1])
  3208 
  3209 lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
  3210 
  3211 lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
  3212 by (rule in_listsp_conv_set [THEN iffD2])
  3213 
  3214 lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
  3215 
  3216 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
  3217 by auto
  3218 
  3219 
  3220 
  3221 subsubsection{* Inductive definition for membership *}
  3222 
  3223 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
  3224 where
  3225     elem:  "ListMem x (x # xs)"
  3226   | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
  3227 
  3228 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
  3229 apply (rule iffI)
  3230  apply (induct set: ListMem)
  3231   apply auto
  3232 apply (induct xs)
  3233  apply (auto intro: ListMem.intros)
  3234 done
  3235 
  3236 
  3237 
  3238 subsubsection{*Lists as Cartesian products*}
  3239 
  3240 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
  3241 @{term A} and tail drawn from @{term Xs}.*}
  3242 
  3243 constdefs
  3244   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
  3245   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
  3246 declare set_Cons_def [code del]
  3247 
  3248 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
  3249 by (auto simp add: set_Cons_def)
  3250 
  3251 text{*Yields the set of lists, all of the same length as the argument and
  3252 with elements drawn from the corresponding element of the argument.*}
  3253 
  3254 consts  listset :: "'a set list \<Rightarrow> 'a list set"
  3255 primrec
  3256    "listset []    = {[]}"
  3257    "listset(A#As) = set_Cons A (listset As)"
  3258 
  3259 
  3260 subsection{*Relations on Lists*}
  3261 
  3262 subsubsection {* Length Lexicographic Ordering *}
  3263 
  3264 text{*These orderings preserve well-foundedness: shorter lists 
  3265   precede longer lists. These ordering are not used in dictionaries.*}
  3266 
  3267 consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
  3268         --{*The lexicographic ordering for lists of the specified length*}
  3269 primrec
  3270   "lexn r 0 = {}"
  3271   "lexn r (Suc n) =
  3272     (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
  3273     {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
  3274 
  3275 constdefs
  3276   lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
  3277     "lex r == \<Union>n. lexn r n"
  3278         --{*Holds only between lists of the same length*}
  3279 
  3280   lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
  3281     "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
  3282         --{*Compares lists by their length and then lexicographically*}
  3283 
  3284 declare lex_def [code del]
  3285 
  3286 
  3287 lemma wf_lexn: "wf r ==> wf (lexn r n)"
  3288 apply (induct n, simp, simp)
  3289 apply(rule wf_subset)
  3290  prefer 2 apply (rule Int_lower1)
  3291 apply(rule wf_prod_fun_image)
  3292  prefer 2 apply (rule inj_onI, auto)
  3293 done
  3294 
  3295 lemma lexn_length:
  3296   "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
  3297 by (induct n arbitrary: xs ys) auto
  3298 
  3299 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
  3300 apply (unfold lex_def)
  3301 apply (rule wf_UN)
  3302 apply (blast intro: wf_lexn, clarify)
  3303 apply (rename_tac m n)
  3304 apply (subgoal_tac "m \<noteq> n")
  3305  prefer 2 apply blast
  3306 apply (blast dest: lexn_length not_sym)
  3307 done
  3308 
  3309 lemma lexn_conv:
  3310   "lexn r n =
  3311     {(xs,ys). length xs = n \<and> length ys = n \<and>
  3312     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
  3313 apply (induct n, simp)
  3314 apply (simp add: image_Collect lex_prod_def, safe, blast)
  3315  apply (rule_tac x = "ab # xys" in exI, simp)
  3316 apply (case_tac xys, simp_all, blast)
  3317 done
  3318 
  3319 lemma lex_conv:
  3320   "lex r =
  3321     {(xs,ys). length xs = length ys \<and>
  3322     (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
  3323 by (force simp add: lex_def lexn_conv)
  3324 
  3325 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
  3326 by (unfold lenlex_def) blast
  3327 
  3328 lemma lenlex_conv:
  3329     "lenlex r = {(xs,ys). length xs < length ys |
  3330                  length xs = length ys \<and> (xs, ys) : lex r}"
  3331 by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
  3332 
  3333 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
  3334 by (simp add: lex_conv)
  3335 
  3336 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
  3337 by (simp add:lex_conv)
  3338 
  3339 lemma Cons_in_lex [simp]:
  3340     "((x # xs, y # ys) : lex r) =
  3341       ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
  3342 apply (simp add: lex_conv)
  3343 apply (rule iffI)
  3344  prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
  3345 apply (case_tac xys, simp, simp)
  3346 apply blast
  3347 done
  3348 
  3349 
  3350 subsubsection {* Lexicographic Ordering *}
  3351 
  3352 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
  3353     This ordering does \emph{not} preserve well-foundedness.
  3354      Author: N. Voelker, March 2005. *} 
  3355 
  3356 constdefs 
  3357   lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
  3358   "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
  3359             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
  3360 declare lexord_def [code del]
  3361 
  3362 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
  3363 by (unfold lexord_def, induct_tac y, auto) 
  3364 
  3365 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
  3366 by (unfold lexord_def, induct_tac x, auto)
  3367 
  3368 lemma lexord_cons_cons[simp]:
  3369      "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
  3370   apply (unfold lexord_def, safe, simp_all)
  3371   apply (case_tac u, simp, simp)
  3372   apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
  3373   apply (erule_tac x="b # u" in allE)
  3374   by force
  3375 
  3376 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
  3377 
  3378 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
  3379 by (induct_tac x, auto)  
  3380 
  3381 lemma lexord_append_left_rightI:
  3382      "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
  3383 by (induct_tac u, auto)
  3384 
  3385 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
  3386 by (induct x, auto)
  3387 
  3388 lemma lexord_append_leftD:
  3389      "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
  3390 by (erule rev_mp, induct_tac x, auto)
  3391 
  3392 lemma lexord_take_index_conv: 
  3393    "((x,y) : lexord r) = 
  3394     ((length x < length y \<and> take (length x) y = x) \<or> 
  3395      (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
  3396   apply (unfold lexord_def Let_def, clarsimp) 
  3397   apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
  3398   apply auto 
  3399   apply (rule_tac x="hd (drop (length x) y)" in exI)
  3400   apply (rule_tac x="tl (drop (length x) y)" in exI)
  3401   apply (erule subst, simp add: min_def) 
  3402   apply (rule_tac x ="length u" in exI, simp) 
  3403   apply (rule_tac x ="take i x" in exI) 
  3404   apply (rule_tac x ="x ! i" in exI) 
  3405   apply (rule_tac x ="y ! i" in exI, safe) 
  3406   apply (rule_tac x="drop (Suc i) x" in exI)
  3407   apply (drule sym, simp add: drop_Suc_conv_tl) 
  3408   apply (rule_tac x="drop (Suc i) y" in exI)
  3409   by (simp add: drop_Suc_conv_tl) 
  3410 
  3411 -- {* lexord is extension of partial ordering List.lex *} 
  3412 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
  3413   apply (rule_tac x = y in spec) 
  3414   apply (induct_tac x, clarsimp) 
  3415   by (clarify, case_tac x, simp, force)
  3416 
  3417 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
  3418   by (induct y, auto)
  3419 
  3420 lemma lexord_trans: 
  3421     "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
  3422    apply (erule rev_mp)+
  3423    apply (rule_tac x = x in spec) 
  3424   apply (rule_tac x = z in spec) 
  3425   apply ( induct_tac y, simp, clarify)
  3426   apply (case_tac xa, erule ssubst) 
  3427   apply (erule allE, erule allE) -- {* avoid simp recursion *} 
  3428   apply (case_tac x, simp, simp) 
  3429   apply (case_tac x, erule allE, erule allE, simp)
  3430   apply (erule_tac x = listb in allE) 
  3431   apply (erule_tac x = lista in allE, simp)
  3432   apply (unfold trans_def)
  3433   by blast
  3434 
  3435 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
  3436 by (rule transI, drule lexord_trans, blast) 
  3437 
  3438 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"
  3439   apply (rule_tac x = y in spec) 
  3440   apply (induct_tac x, rule allI) 
  3441   apply (case_tac x, simp, simp) 
  3442   apply (rule allI, case_tac x, simp, simp) 
  3443   by blast
  3444 
  3445 
  3446 subsection {* Lexicographic combination of measure functions *}
  3447 
  3448 text {* These are useful for termination proofs *}
  3449 
  3450 definition
  3451   "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
  3452 
  3453 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
  3454 unfolding measures_def
  3455 by blast
  3456 
  3457 lemma in_measures[simp]: 
  3458   "(x, y) \<in> measures [] = False"
  3459   "(x, y) \<in> measures (f # fs)
  3460          = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
  3461 unfolding measures_def
  3462 by auto
  3463 
  3464 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
  3465 by simp
  3466 
  3467 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
  3468 by auto
  3469 
  3470 
  3471 subsubsection{*Lifting a Relation on List Elements to the Lists*}
  3472 
  3473 inductive_set
  3474   listrel :: "('a * 'a)set => ('a list * 'a list)set"
  3475   for r :: "('a * 'a)set"
  3476 where
  3477     Nil:  "([],[]) \<in> listrel r"
  3478   | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
  3479 
  3480 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
  3481 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
  3482 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
  3483 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
  3484 
  3485 
  3486 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
  3487 apply clarify  
  3488 apply (erule listrel.induct)
  3489 apply (blast intro: listrel.intros)+
  3490 done
  3491 
  3492 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
  3493 apply clarify 
  3494 apply (erule listrel.induct, auto) 
  3495 done
  3496 
  3497 lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)" 
  3498 apply (simp add: refl_on_def listrel_subset Ball_def)
  3499 apply (rule allI) 
  3500 apply (induct_tac x) 
  3501 apply (auto intro: listrel.intros)
  3502 done
  3503 
  3504 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
  3505 apply (auto simp add: sym_def)
  3506 apply (erule listrel.induct) 
  3507 apply (blast intro: listrel.intros)+
  3508 done
  3509 
  3510 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
  3511 apply (simp add: trans_def)
  3512 apply (intro allI) 
  3513 apply (rule impI) 
  3514 apply (erule listrel.induct) 
  3515 apply (blast intro: listrel.intros)+
  3516 done
  3517 
  3518 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
  3519 by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) 
  3520 
  3521 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
  3522 by (blast intro: listrel.intros)
  3523 
  3524 lemma listrel_Cons:
  3525      "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
  3526 by (auto simp add: set_Cons_def intro: listrel.intros) 
  3527 
  3528 
  3529 subsection {* Size function *}
  3530 
  3531 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
  3532 by (rule is_measure_trivial)
  3533 
  3534 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
  3535 by (rule is_measure_trivial)
  3536 
  3537 lemma list_size_estimation[termination_simp]: 
  3538   "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
  3539 by (induct xs) auto
  3540 
  3541 lemma list_size_estimation'[termination_simp]: 
  3542   "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
  3543 by (induct xs) auto
  3544 
  3545 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
  3546 by (induct xs) auto
  3547 
  3548 lemma list_size_pointwise[termination_simp]: 
  3549   "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
  3550 by (induct xs) force+
  3551 
  3552 
  3553 subsection {* Code generator *}
  3554 
  3555 subsubsection {* Setup *}
  3556 
  3557 use "Tools/list_code.ML"
  3558 
  3559 code_type list
  3560   (SML "_ list")
  3561   (OCaml "_ list")
  3562   (Haskell "![_]")
  3563 
  3564 code_const Nil
  3565   (SML "[]")
  3566   (OCaml "[]")
  3567   (Haskell "[]")
  3568 
  3569 code_instance list :: eq
  3570   (Haskell -)
  3571 
  3572 code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
  3573   (Haskell infixl 4 "==")
  3574 
  3575 code_reserved SML
  3576   list
  3577 
  3578 code_reserved OCaml
  3579   list
  3580 
  3581 types_code
  3582   "list" ("_ list")
  3583 attach (term_of) {*
  3584 fun term_of_list f T = HOLogic.mk_list T o map f;
  3585 *}
  3586 attach (test) {*
  3587 fun gen_list' aG aT i j = frequency
  3588   [(i, fn () =>
  3589       let
  3590         val (x, t) = aG j;
  3591         val (xs, ts) = gen_list' aG aT (i-1) j
  3592       in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
  3593    (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
  3594 and gen_list aG aT i = gen_list' aG aT i i;
  3595 *}
  3596 
  3597 consts_code Cons ("(_ ::/ _)")
  3598 
  3599 setup {*
  3600 let
  3601   fun list_codegen thy defs dep thyname b t gr =
  3602     let
  3603       val ts = HOLogic.dest_list t;
  3604       val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
  3605         (fastype_of t) gr;
  3606       val (ps, gr'') = fold_map
  3607         (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
  3608     in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
  3609 in
  3610   fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell"]
  3611   #> Codegen.add_codegen "list_codegen" list_codegen
  3612 end
  3613 *}
  3614 
  3615 
  3616 subsubsection {* Generation of efficient code *}
  3617 
  3618 primrec
  3619   member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
  3620 where 
  3621   "x mem [] \<longleftrightarrow> False"
  3622   | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
  3623 
  3624 primrec
  3625   null:: "'a list \<Rightarrow> bool"
  3626 where
  3627   "null [] = True"
  3628   | "null (x#xs) = False"
  3629 
  3630 primrec
  3631   list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  3632 where
  3633   "list_inter [] bs = []"
  3634   | "list_inter (a#as) bs =
  3635      (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
  3636 
  3637 primrec
  3638   list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
  3639 where
  3640   "list_all P [] = True"
  3641   | "list_all P (x#xs) = (P x \<and> list_all P xs)"
  3642 
  3643 primrec
  3644   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
  3645 where
  3646   "list_ex P [] = False"
  3647   | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
  3648 
  3649 primrec
  3650   filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  3651 where
  3652   "filtermap f [] = []"
  3653   | "filtermap f (x#xs) =
  3654      (case f x of None \<Rightarrow> filtermap f xs
  3655       | Some y \<Rightarrow> y # filtermap f xs)"
  3656 
  3657 primrec
  3658   map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  3659 where
  3660   "map_filter f P [] = []"
  3661   | "map_filter f P (x#xs) =
  3662      (if P x then f x # map_filter f P xs else map_filter f P xs)"
  3663 
  3664 primrec
  3665   length_unique :: "'a list \<Rightarrow> nat"
  3666 where
  3667   "length_unique [] = 0"
  3668   | "length_unique (x#xs) =
  3669       (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
  3670 
  3671 text {*
  3672   Only use @{text mem} for generating executable code.  Otherwise use
  3673   @{prop "x : set xs"} instead --- it is much easier to reason about.
  3674   The same is true for @{const list_all} and @{const list_ex}: write
  3675   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
  3676   quantifiers are aleady known to the automatic provers. In fact, the
  3677   declarations in the code subsection make sure that @{text "\<in>"},
  3678   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
  3679   efficiently.
  3680 
  3681   Efficient emptyness check is implemented by @{const null}.
  3682 
  3683   The functions @{const filtermap} and @{const map_filter} are just
  3684   there to generate efficient code. Do not use
  3685   them for modelling and proving.
  3686 *}
  3687 
  3688 lemma rev_foldl_cons [code]:
  3689   "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
  3690 proof (induct xs)
  3691   case Nil then show ?case by simp
  3692 next
  3693   case Cons
  3694   {
  3695     fix x xs ys
  3696     have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
  3697       = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
  3698     by (induct xs arbitrary: ys) auto
  3699   }
  3700   note aux = this
  3701   show ?case by (induct xs) (auto simp add: Cons aux)
  3702 qed
  3703 
  3704 lemma mem_iff [code_post]:
  3705   "x mem xs \<longleftrightarrow> x \<in> set xs"
  3706 by (induct xs) auto
  3707 
  3708 lemmas in_set_code [code_unfold] = mem_iff [symmetric]
  3709 
  3710 lemma empty_null:
  3711   "xs = [] \<longleftrightarrow> null xs"
  3712 by (cases xs) simp_all
  3713 
  3714 lemma [code_unfold]:
  3715   "eq_class.eq xs [] \<longleftrightarrow> null xs"
  3716 by (simp add: eq empty_null)
  3717 
  3718 lemmas null_empty [code_post] =
  3719   empty_null [symmetric]
  3720 
  3721 lemma list_inter_conv:
  3722   "set (list_inter xs ys) = set xs \<inter> set ys"
  3723 by (induct xs) auto
  3724 
  3725 lemma list_all_iff [code_post]:
  3726   "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
  3727 by (induct xs) auto
  3728 
  3729 lemmas list_ball_code [code_unfold] = list_all_iff [symmetric]
  3730 
  3731 lemma list_all_append [simp]:
  3732   "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
  3733 by (induct xs) auto
  3734 
  3735 lemma list_all_rev [simp]:
  3736   "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
  3737 by (simp add: list_all_iff)
  3738 
  3739 lemma list_all_length:
  3740   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
  3741   unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
  3742 
  3743 lemma list_ex_iff [code_post]:
  3744   "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
  3745 by (induct xs) simp_all
  3746 
  3747 lemmas list_bex_code [code_unfold] =
  3748   list_ex_iff [symmetric]
  3749 
  3750 lemma list_ex_length:
  3751   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
  3752   unfolding list_ex_iff set_conv_nth by auto
  3753 
  3754 lemma filtermap_conv:
  3755    "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
  3756 by (induct xs) (simp_all split: option.split) 
  3757 
  3758 lemma map_filter_conv [simp]:
  3759   "map_filter f P xs = map f (filter P xs)"
  3760 by (induct xs) auto
  3761 
  3762 lemma length_remdups_length_unique [code_unfold]:
  3763   "length (remdups xs) = length_unique xs"
  3764   by (induct xs) simp_all
  3765 
  3766 hide (open) const length_unique
  3767 
  3768 
  3769 text {* Code for bounded quantification and summation over nats. *}
  3770 
  3771 lemma atMost_upto [code_unfold]:
  3772   "{..n} = set [0..<Suc n]"
  3773 by auto
  3774 
  3775 lemma atLeast_upt [code_unfold]:
  3776   "{..<n} = set [0..<n]"
  3777 by auto
  3778 
  3779 lemma greaterThanLessThan_upt [code_unfold]:
  3780   "{n<..<m} = set [Suc n..<m]"
  3781 by auto
  3782 
  3783 lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
  3784 
  3785 lemma greaterThanAtMost_upt [code_unfold]:
  3786   "{n<..m} = set [Suc n..<Suc m]"
  3787 by auto
  3788 
  3789 lemma atLeastAtMost_upt [code_unfold]:
  3790   "{n..m} = set [n..<Suc m]"
  3791 by auto
  3792 
  3793 lemma all_nat_less_eq [code_unfold]:
  3794   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
  3795 by auto
  3796 
  3797 lemma ex_nat_less_eq [code_unfold]:
  3798   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
  3799 by auto
  3800 
  3801 lemma all_nat_less [code_unfold]:
  3802   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
  3803 by auto
  3804 
  3805 lemma ex_nat_less [code_unfold]:
  3806   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
  3807 by auto
  3808 
  3809 lemma setsum_set_distinct_conv_listsum:
  3810   "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
  3811 by (induct xs) simp_all
  3812 
  3813 lemma setsum_set_upt_conv_listsum [code_unfold]:
  3814   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
  3815 by (rule setsum_set_distinct_conv_listsum) simp
  3816 
  3817 
  3818 text {* Code for summation over ints. *}
  3819 
  3820 lemma greaterThanLessThan_upto [code_unfold]:
  3821   "{i<..<j::int} = set [i+1..j - 1]"
  3822 by auto
  3823 
  3824 lemma atLeastLessThan_upto [code_unfold]:
  3825   "{i..<j::int} = set [i..j - 1]"
  3826 by auto
  3827 
  3828 lemma greaterThanAtMost_upto [code_unfold]:
  3829   "{i<..j::int} = set [i+1..j]"
  3830 by auto
  3831 
  3832 lemmas atLeastAtMost_upto [code_unfold] = set_upto[symmetric]
  3833 
  3834 lemma setsum_set_upto_conv_listsum [code_unfold]:
  3835   "setsum f (set [i..j::int]) = listsum (map f [i..j])"
  3836 by (rule setsum_set_distinct_conv_listsum) simp
  3837 
  3838 
  3839 text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
  3840 and similiarly for @{text"\<exists>"}. *}
  3841 
  3842 function all_from_to_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
  3843 "all_from_to_nat P i j =
  3844  (if i < j then if P i then all_from_to_nat P (i+1) j else False
  3845   else True)"
  3846 by auto
  3847 termination
  3848 by (relation "measure(%(P,i,j). j - i)") auto
  3849 
  3850 declare all_from_to_nat.simps[simp del]
  3851 
  3852 lemma all_from_to_nat_iff_ball:
  3853   "all_from_to_nat P i j = (ALL n : {i ..< j}. P n)"
  3854 proof(induct P i j rule:all_from_to_nat.induct)
  3855   case (1 P i j)
  3856   let ?yes = "i < j & P i"
  3857   show ?case
  3858   proof (cases)
  3859     assume ?yes
  3860     hence "all_from_to_nat P i j = (P i & all_from_to_nat P (i+1) j)"
  3861       by(simp add: all_from_to_nat.simps)
  3862     also have "... = (P i & (ALL n : {i+1 ..< j}. P n))" using `?yes` 1 by simp
  3863     also have "... = (ALL n : {i ..< j}. P n)" (is "?L = ?R")
  3864     proof
  3865       assume L: ?L
  3866       show ?R
  3867       proof clarify
  3868 	fix n assume n: "n : {i..<j}"
  3869 	show "P n"
  3870 	proof cases
  3871 	  assume "n = i" thus "P n" using L by simp
  3872 	next
  3873 	  assume "n ~= i"
  3874 	  hence "i+1 <= n" using n by auto
  3875 	  thus "P n" using L n by simp
  3876 	qed
  3877       qed
  3878     next
  3879       assume R: ?R thus ?L using `?yes` 1 by auto
  3880     qed
  3881     finally show ?thesis .
  3882   next
  3883     assume "~?yes" thus ?thesis by(auto simp add: all_from_to_nat.simps)
  3884   qed
  3885 qed
  3886 
  3887 
  3888 lemma list_all_iff_all_from_to_nat[code_unfold]:
  3889   "list_all P [i..<j] = all_from_to_nat P i j"
  3890 by(simp add: all_from_to_nat_iff_ball list_all_iff)
  3891 
  3892 lemma list_ex_iff_not_all_from_to_not_nat[code_unfold]:
  3893   "list_ex P [i..<j] = (~all_from_to_nat (%x. ~P x) i j)"
  3894 by(simp add: all_from_to_nat_iff_ball list_ex_iff)
  3895 
  3896 
  3897 function all_from_to_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
  3898 "all_from_to_int P i j =
  3899  (if i <= j then if P i then all_from_to_int P (i+1) j else False
  3900   else True)"
  3901 by auto
  3902 termination
  3903 by (relation "measure(%(P,i,j). nat(j - i + 1))") auto
  3904 
  3905 declare all_from_to_int.simps[simp del]
  3906 
  3907 lemma all_from_to_int_iff_ball:
  3908   "all_from_to_int P i j = (ALL n : {i .. j}. P n)"
  3909 proof(induct P i j rule:all_from_to_int.induct)
  3910   case (1 P i j)
  3911   let ?yes = "i <= j & P i"
  3912   show ?case
  3913   proof (cases)
  3914     assume ?yes
  3915     hence "all_from_to_int P i j = (P i & all_from_to_int P (i+1) j)"
  3916       by(simp add: all_from_to_int.simps)
  3917     also have "... = (P i & (ALL n : {i+1 .. j}. P n))" using `?yes` 1 by simp
  3918     also have "... = (ALL n : {i .. j}. P n)" (is "?L = ?R")
  3919     proof
  3920       assume L: ?L
  3921       show ?R
  3922       proof clarify
  3923 	fix n assume n: "n : {i..j}"
  3924 	show "P n"
  3925 	proof cases
  3926 	  assume "n = i" thus "P n" using L by simp
  3927 	next
  3928 	  assume "n ~= i"
  3929 	  hence "i+1 <= n" using n by auto
  3930 	  thus "P n" using L n by simp
  3931 	qed
  3932       qed
  3933     next
  3934       assume R: ?R thus ?L using `?yes` 1 by auto
  3935     qed
  3936     finally show ?thesis .
  3937   next
  3938     assume "~?yes" thus ?thesis by(auto simp add: all_from_to_int.simps)
  3939   qed
  3940 qed
  3941 
  3942 lemma list_all_iff_all_from_to_int[code_unfold]:
  3943   "list_all P [i..j] = all_from_to_int P i j"
  3944 by(simp add: all_from_to_int_iff_ball list_all_iff)
  3945 
  3946 lemma list_ex_iff_not_all_from_to_not_int[code_unfold]:
  3947   "list_ex P [i..j] = (~ all_from_to_int (%x. ~P x) i j)"
  3948 by(simp add: all_from_to_int_iff_ball list_ex_iff)
  3949 
  3950 
  3951 end