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