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