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