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