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