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