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