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