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