src/HOL/List.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30242 aea5d7fa7ef5
child 30949 37f887b55e7f
permissions -rw-r--r--
added lemmas
     1 (*  Title:      HOL/List.thy
     2     Author:     Tobias Nipkow
     3 *)
     4 
     5 header {* The datatype of finite lists *}
     6 
     7 theory List
     8 imports Plain Relation_Power Presburger Recdef ATP_Linkup
     9 uses "Tools/string_syntax.ML"
    10 begin
    11 
    12 datatype 'a list =
    13     Nil    ("[]")
    14   | Cons 'a  "'a list"    (infixr "#" 65)
    15 
    16 subsection{*Basic list processing functions*}
    17 
    18 consts
    19   filter:: "('a => bool) => 'a list => 'a list"
    20   concat:: "'a list list => 'a list"
    21   foldl :: "('b => 'a => 'b) => 'b => 'a list => 'b"
    22   foldr :: "('a => 'b => 'b) => 'a list => 'b => 'b"
    23   hd:: "'a list => 'a"
    24   tl:: "'a list => 'a list"
    25   last:: "'a list => 'a"
    26   butlast :: "'a list => 'a list"
    27   set :: "'a list => 'a set"
    28   map :: "('a=>'b) => ('a list => 'b list)"
    29   listsum ::  "'a list => 'a::monoid_add"
    30   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 DatatypePackage.datatype_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 (the_context ()) "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] = {k. i \<le> k \<and> k < j}"
   885 apply (induct j, simp_all)
   886 apply (erule ssubst, auto)
   887 done
   888 
   889 
   890 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"
   891 proof (induct xs)
   892   case Nil thus ?case by simp
   893 next
   894   case Cons thus ?case by (auto intro: Cons_eq_appendI)
   895 qed
   896 
   897 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
   898   by (auto elim: split_list)
   899 
   900 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"
   901 proof (induct xs)
   902   case Nil thus ?case by simp
   903 next
   904   case (Cons a xs)
   905   show ?case
   906   proof cases
   907     assume "x = a" thus ?case using Cons by fastsimp
   908   next
   909     assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)
   910   qed
   911 qed
   912 
   913 lemma in_set_conv_decomp_first:
   914   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"
   915   by (auto dest!: split_list_first)
   916 
   917 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"
   918 proof (induct xs rule:rev_induct)
   919   case Nil thus ?case by simp
   920 next
   921   case (snoc a xs)
   922   show ?case
   923   proof cases
   924     assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)
   925   next
   926     assume "x \<noteq> a" thus ?case using snoc by fastsimp
   927   qed
   928 qed
   929 
   930 lemma in_set_conv_decomp_last:
   931   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"
   932   by (auto dest!: split_list_last)
   933 
   934 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"
   935 proof (induct xs)
   936   case Nil thus ?case by simp
   937 next
   938   case Cons thus ?case
   939     by(simp add:Bex_def)(metis append_Cons append.simps(1))
   940 qed
   941 
   942 lemma split_list_propE:
   943   assumes "\<exists>x \<in> set xs. P x"
   944   obtains ys x zs where "xs = ys @ x # zs" and "P x"
   945 using split_list_prop [OF assms] by blast
   946 
   947 lemma split_list_first_prop:
   948   "\<exists>x \<in> set xs. P x \<Longrightarrow>
   949    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"
   950 proof (induct xs)
   951   case Nil thus ?case by simp
   952 next
   953   case (Cons x xs)
   954   show ?case
   955   proof cases
   956     assume "P x"
   957     thus ?thesis by simp
   958       (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)
   959   next
   960     assume "\<not> P x"
   961     hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp
   962     thus ?thesis using `\<not> P x` Cons(1) by (metis append_Cons set_ConsD)
   963   qed
   964 qed
   965 
   966 lemma split_list_first_propE:
   967   assumes "\<exists>x \<in> set xs. P x"
   968   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"
   969 using split_list_first_prop [OF assms] by blast
   970 
   971 lemma split_list_first_prop_iff:
   972   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
   973    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"
   974 by (rule, erule split_list_first_prop) auto
   975 
   976 lemma split_list_last_prop:
   977   "\<exists>x \<in> set xs. P x \<Longrightarrow>
   978    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"
   979 proof(induct xs rule:rev_induct)
   980   case Nil thus ?case by simp
   981 next
   982   case (snoc x xs)
   983   show ?case
   984   proof cases
   985     assume "P x" thus ?thesis by (metis emptyE set_empty)
   986   next
   987     assume "\<not> P x"
   988     hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp
   989     thus ?thesis using `\<not> P x` snoc(1) by fastsimp
   990   qed
   991 qed
   992 
   993 lemma split_list_last_propE:
   994   assumes "\<exists>x \<in> set xs. P x"
   995   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"
   996 using split_list_last_prop [OF assms] by blast
   997 
   998 lemma split_list_last_prop_iff:
   999   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
  1000    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
  1001 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)
  1002 
  1003 lemma finite_list: "finite A ==> EX xs. set xs = A"
  1004   by (erule finite_induct)
  1005     (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))
  1006 
  1007 lemma card_length: "card (set xs) \<le> length xs"
  1008 by (induct xs) (auto simp add: card_insert_if)
  1009 
  1010 lemma set_minus_filter_out:
  1011   "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"
  1012   by (induct xs) auto
  1013 
  1014 subsubsection {* @{text filter} *}
  1015 
  1016 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"
  1017 by (induct xs) auto
  1018 
  1019 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"
  1020 by (induct xs) simp_all
  1021 
  1022 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"
  1023 by (induct xs) auto
  1024 
  1025 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"
  1026 by (induct xs) (auto simp add: le_SucI)
  1027 
  1028 lemma sum_length_filter_compl:
  1029   "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"
  1030 by(induct xs) simp_all
  1031 
  1032 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"
  1033 by (induct xs) auto
  1034 
  1035 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"
  1036 by (induct xs) auto
  1037 
  1038 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)" 
  1039 by (induct xs) simp_all
  1040 
  1041 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"
  1042 apply (induct xs)
  1043  apply auto
  1044 apply(cut_tac P=P and xs=xs in length_filter_le)
  1045 apply simp
  1046 done
  1047 
  1048 lemma filter_map:
  1049   "filter P (map f xs) = map f (filter (P o f) xs)"
  1050 by (induct xs) simp_all
  1051 
  1052 lemma length_filter_map[simp]:
  1053   "length (filter P (map f xs)) = length(filter (P o f) xs)"
  1054 by (simp add:filter_map)
  1055 
  1056 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"
  1057 by auto
  1058 
  1059 lemma length_filter_less:
  1060   "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"
  1061 proof (induct xs)
  1062   case Nil thus ?case by simp
  1063 next
  1064   case (Cons x xs) thus ?case
  1065     apply (auto split:split_if_asm)
  1066     using length_filter_le[of P xs] apply arith
  1067   done
  1068 qed
  1069 
  1070 lemma length_filter_conv_card:
  1071  "length(filter p xs) = card{i. i < length xs & p(xs!i)}"
  1072 proof (induct xs)
  1073   case Nil thus ?case by simp
  1074 next
  1075   case (Cons x xs)
  1076   let ?S = "{i. i < length xs & p(xs!i)}"
  1077   have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)
  1078   show ?case (is "?l = card ?S'")
  1079   proof (cases)
  1080     assume "p x"
  1081     hence eq: "?S' = insert 0 (Suc ` ?S)"
  1082       by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)
  1083     have "length (filter p (x # xs)) = Suc(card ?S)"
  1084       using Cons `p x` by simp
  1085     also have "\<dots> = Suc(card(Suc ` ?S))" using fin
  1086       by (simp add: card_image inj_Suc)
  1087     also have "\<dots> = card ?S'" using eq fin
  1088       by (simp add:card_insert_if) (simp add:image_def)
  1089     finally show ?thesis .
  1090   next
  1091     assume "\<not> p x"
  1092     hence eq: "?S' = Suc ` ?S"
  1093       by(auto simp add: image_def split:nat.split elim:lessE)
  1094     have "length (filter p (x # xs)) = card ?S"
  1095       using Cons `\<not> p x` by simp
  1096     also have "\<dots> = card(Suc ` ?S)" using fin
  1097       by (simp add: card_image inj_Suc)
  1098     also have "\<dots> = card ?S'" using eq fin
  1099       by (simp add:card_insert_if)
  1100     finally show ?thesis .
  1101   qed
  1102 qed
  1103 
  1104 lemma Cons_eq_filterD:
  1105  "x#xs = filter P ys \<Longrightarrow>
  1106   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  1107   (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
  1108 proof(induct ys)
  1109   case Nil thus ?case by simp
  1110 next
  1111   case (Cons y ys)
  1112   show ?case (is "\<exists>x. ?Q x")
  1113   proof cases
  1114     assume Py: "P y"
  1115     show ?thesis
  1116     proof cases
  1117       assume "x = y"
  1118       with Py Cons.prems have "?Q []" by simp
  1119       then show ?thesis ..
  1120     next
  1121       assume "x \<noteq> y"
  1122       with Py Cons.prems show ?thesis by simp
  1123     qed
  1124   next
  1125     assume "\<not> P y"
  1126     with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp
  1127     then have "?Q (y#us)" by simp
  1128     then show ?thesis ..
  1129   qed
  1130 qed
  1131 
  1132 lemma filter_eq_ConsD:
  1133  "filter P ys = x#xs \<Longrightarrow>
  1134   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
  1135 by(rule Cons_eq_filterD) simp
  1136 
  1137 lemma filter_eq_Cons_iff:
  1138  "(filter P ys = x#xs) =
  1139   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
  1140 by(auto dest:filter_eq_ConsD)
  1141 
  1142 lemma Cons_eq_filter_iff:
  1143  "(x#xs = filter P ys) =
  1144   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"
  1145 by(auto dest:Cons_eq_filterD)
  1146 
  1147 lemma filter_cong[fundef_cong, recdef_cong]:
  1148  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"
  1149 apply simp
  1150 apply(erule thin_rl)
  1151 by (induct ys) simp_all
  1152 
  1153 
  1154 subsubsection {* List partitioning *}
  1155 
  1156 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where
  1157   "partition P [] = ([], [])"
  1158   | "partition P (x # xs) = 
  1159       (let (yes, no) = partition P xs
  1160       in if P x then (x # yes, no) else (yes, x # no))"
  1161 
  1162 lemma partition_filter1:
  1163     "fst (partition P xs) = filter P xs"
  1164 by (induct xs) (auto simp add: Let_def split_def)
  1165 
  1166 lemma partition_filter2:
  1167     "snd (partition P xs) = filter (Not o P) xs"
  1168 by (induct xs) (auto simp add: Let_def split_def)
  1169 
  1170 lemma partition_P:
  1171   assumes "partition P xs = (yes, no)"
  1172   shows "(\<forall>p \<in> set yes.  P p) \<and> (\<forall>p  \<in> set no. \<not> P p)"
  1173 proof -
  1174   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
  1175     by simp_all
  1176   then show ?thesis by (simp_all add: partition_filter1 partition_filter2)
  1177 qed
  1178 
  1179 lemma partition_set:
  1180   assumes "partition P xs = (yes, no)"
  1181   shows "set yes \<union> set no = set xs"
  1182 proof -
  1183   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"
  1184     by simp_all
  1185   then show ?thesis by (auto simp add: partition_filter1 partition_filter2) 
  1186 qed
  1187 
  1188 
  1189 subsubsection {* @{text concat} *}
  1190 
  1191 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"
  1192 by (induct xs) auto
  1193 
  1194 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"
  1195 by (induct xss) auto
  1196 
  1197 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"
  1198 by (induct xss) auto
  1199 
  1200 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
  1201 by (induct xs) auto
  1202 
  1203 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
  1204 by (induct xs) auto
  1205 
  1206 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"
  1207 by (induct xs) auto
  1208 
  1209 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"
  1210 by (induct xs) auto
  1211 
  1212 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"
  1213 by (induct xs) auto
  1214 
  1215 
  1216 subsubsection {* @{text nth} *}
  1217 
  1218 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"
  1219 by auto
  1220 
  1221 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"
  1222 by auto
  1223 
  1224 declare nth.simps [simp del]
  1225 
  1226 lemma nth_append:
  1227   "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
  1228 apply (induct xs arbitrary: n, simp)
  1229 apply (case_tac n, auto)
  1230 done
  1231 
  1232 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"
  1233 by (induct xs) auto
  1234 
  1235 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"
  1236 by (induct xs) auto
  1237 
  1238 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"
  1239 apply (induct xs arbitrary: n, simp)
  1240 apply (case_tac n, auto)
  1241 done
  1242 
  1243 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"
  1244 by(cases xs) simp_all
  1245 
  1246 
  1247 lemma list_eq_iff_nth_eq:
  1248  "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"
  1249 apply(induct xs arbitrary: ys)
  1250  apply force
  1251 apply(case_tac ys)
  1252  apply simp
  1253 apply(simp add:nth_Cons split:nat.split)apply blast
  1254 done
  1255 
  1256 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"
  1257 apply (induct xs, simp, simp)
  1258 apply safe
  1259 apply (metis nat_case_0 nth.simps zero_less_Suc)
  1260 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)
  1261 apply (case_tac i, simp)
  1262 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)
  1263 done
  1264 
  1265 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"
  1266 by(auto simp:set_conv_nth)
  1267 
  1268 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"
  1269 by (auto simp add: set_conv_nth)
  1270 
  1271 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"
  1272 by (auto simp add: set_conv_nth)
  1273 
  1274 lemma all_nth_imp_all_set:
  1275 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"
  1276 by (auto simp add: set_conv_nth)
  1277 
  1278 lemma all_set_conv_all_nth:
  1279 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"
  1280 by (auto simp add: set_conv_nth)
  1281 
  1282 lemma rev_nth:
  1283   "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"
  1284 proof (induct xs arbitrary: n)
  1285   case Nil thus ?case by simp
  1286 next
  1287   case (Cons x xs)
  1288   hence n: "n < Suc (length xs)" by simp
  1289   moreover
  1290   { assume "n < length xs"
  1291     with n obtain n' where "length xs - n = Suc n'"
  1292       by (cases "length xs - n", auto)
  1293     moreover
  1294     then have "length xs - Suc n = n'" by simp
  1295     ultimately
  1296     have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp
  1297   }
  1298   ultimately
  1299   show ?case by (clarsimp simp add: Cons nth_append)
  1300 qed
  1301 
  1302 subsubsection {* @{text list_update} *}
  1303 
  1304 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"
  1305 by (induct xs arbitrary: i) (auto split: nat.split)
  1306 
  1307 lemma nth_list_update:
  1308 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"
  1309 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
  1310 
  1311 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"
  1312 by (simp add: nth_list_update)
  1313 
  1314 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"
  1315 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)
  1316 
  1317 lemma list_update_id[simp]: "xs[i := xs!i] = xs"
  1318 by (induct xs arbitrary: i) (simp_all split:nat.splits)
  1319 
  1320 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"
  1321 apply (induct xs arbitrary: i)
  1322  apply simp
  1323 apply (case_tac i)
  1324 apply simp_all
  1325 done
  1326 
  1327 lemma list_update_same_conv:
  1328 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"
  1329 by (induct xs arbitrary: i) (auto split: nat.split)
  1330 
  1331 lemma list_update_append1:
  1332  "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"
  1333 apply (induct xs arbitrary: i, simp)
  1334 apply(simp split:nat.split)
  1335 done
  1336 
  1337 lemma list_update_append:
  1338   "(xs @ ys) [n:= x] = 
  1339   (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"
  1340 by (induct xs arbitrary: n) (auto split:nat.splits)
  1341 
  1342 lemma list_update_length [simp]:
  1343  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"
  1344 by (induct xs, auto)
  1345 
  1346 lemma update_zip:
  1347   "length xs = length ys ==>
  1348   (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
  1349 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)
  1350 
  1351 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"
  1352 by (induct xs arbitrary: i) (auto split: nat.split)
  1353 
  1354 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
  1355 by (blast dest!: set_update_subset_insert [THEN subsetD])
  1356 
  1357 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"
  1358 by (induct xs arbitrary: n) (auto split:nat.splits)
  1359 
  1360 lemma list_update_overwrite:
  1361   "xs [i := x, i := y] = xs [i := y]"
  1362 apply (induct xs arbitrary: i)
  1363 apply simp
  1364 apply (case_tac i)
  1365 apply simp_all
  1366 done
  1367 
  1368 lemma list_update_swap:
  1369   "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"
  1370 apply (induct xs arbitrary: i i')
  1371 apply simp
  1372 apply (case_tac i, case_tac i')
  1373 apply auto
  1374 apply (case_tac i')
  1375 apply auto
  1376 done
  1377 
  1378 lemma list_update_code [code]:
  1379   "[][i := y] = []"
  1380   "(x # xs)[0 := y] = y # xs"
  1381   "(x # xs)[Suc i := y] = x # xs[i := y]"
  1382   by simp_all
  1383 
  1384 
  1385 subsubsection {* @{text last} and @{text butlast} *}
  1386 
  1387 lemma last_snoc [simp]: "last (xs @ [x]) = x"
  1388 by (induct xs) auto
  1389 
  1390 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"
  1391 by (induct xs) auto
  1392 
  1393 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"
  1394 by(simp add:last.simps)
  1395 
  1396 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
  1397 by(simp add:last.simps)
  1398 
  1399 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"
  1400 by (induct xs) (auto)
  1401 
  1402 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"
  1403 by(simp add:last_append)
  1404 
  1405 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"
  1406 by(simp add:last_append)
  1407 
  1408 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"
  1409 by(rule rev_exhaust[of xs]) simp_all
  1410 
  1411 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"
  1412 by(cases xs) simp_all
  1413 
  1414 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"
  1415 by (induct as) auto
  1416 
  1417 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"
  1418 by (induct xs rule: rev_induct) auto
  1419 
  1420 lemma butlast_append:
  1421   "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"
  1422 by (induct xs arbitrary: ys) auto
  1423 
  1424 lemma append_butlast_last_id [simp]:
  1425 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"
  1426 by (induct xs) auto
  1427 
  1428 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"
  1429 by (induct xs) (auto split: split_if_asm)
  1430 
  1431 lemma in_set_butlast_appendI:
  1432 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"
  1433 by (auto dest: in_set_butlastD simp add: butlast_append)
  1434 
  1435 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"
  1436 apply (induct xs arbitrary: n)
  1437  apply simp
  1438 apply (auto split:nat.split)
  1439 done
  1440 
  1441 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
  1442 by(induct xs)(auto simp:neq_Nil_conv)
  1443 
  1444 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"
  1445 by (induct xs, simp, case_tac xs, simp_all)
  1446 
  1447 
  1448 subsubsection {* @{text take} and @{text drop} *}
  1449 
  1450 lemma take_0 [simp]: "take 0 xs = []"
  1451 by (induct xs) auto
  1452 
  1453 lemma drop_0 [simp]: "drop 0 xs = xs"
  1454 by (induct xs) auto
  1455 
  1456 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"
  1457 by simp
  1458 
  1459 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"
  1460 by simp
  1461 
  1462 declare take_Cons [simp del] and drop_Cons [simp del]
  1463 
  1464 lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"
  1465   unfolding One_nat_def by simp
  1466 
  1467 lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"
  1468   unfolding One_nat_def by simp
  1469 
  1470 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"
  1471 by(clarsimp simp add:neq_Nil_conv)
  1472 
  1473 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"
  1474 by(cases xs, simp_all)
  1475 
  1476 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"
  1477 by (induct xs arbitrary: n) simp_all
  1478 
  1479 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"
  1480 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)
  1481 
  1482 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"
  1483 by (cases n, simp, cases xs, auto)
  1484 
  1485 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"
  1486 by (simp only: drop_tl)
  1487 
  1488 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"
  1489 apply (induct xs arbitrary: n, simp)
  1490 apply(simp add:drop_Cons nth_Cons split:nat.splits)
  1491 done
  1492 
  1493 lemma take_Suc_conv_app_nth:
  1494   "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"
  1495 apply (induct xs arbitrary: i, simp)
  1496 apply (case_tac i, auto)
  1497 done
  1498 
  1499 lemma drop_Suc_conv_tl:
  1500   "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"
  1501 apply (induct xs arbitrary: i, simp)
  1502 apply (case_tac i, auto)
  1503 done
  1504 
  1505 lemma length_take [simp]: "length (take n xs) = min (length xs) n"
  1506 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1507 
  1508 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"
  1509 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1510 
  1511 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
  1512 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1513 
  1514 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"
  1515 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1516 
  1517 lemma take_append [simp]:
  1518   "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
  1519 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1520 
  1521 lemma drop_append [simp]:
  1522   "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"
  1523 by (induct n arbitrary: xs) (auto, case_tac xs, auto)
  1524 
  1525 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"
  1526 apply (induct m arbitrary: xs n, auto)
  1527 apply (case_tac xs, auto)
  1528 apply (case_tac n, auto)
  1529 done
  1530 
  1531 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"
  1532 apply (induct m arbitrary: xs, auto)
  1533 apply (case_tac xs, auto)
  1534 done
  1535 
  1536 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"
  1537 apply (induct m arbitrary: xs n, auto)
  1538 apply (case_tac xs, auto)
  1539 done
  1540 
  1541 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"
  1542 apply(induct xs arbitrary: m n)
  1543  apply simp
  1544 apply(simp add: take_Cons drop_Cons split:nat.split)
  1545 done
  1546 
  1547 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"
  1548 apply (induct n arbitrary: xs, auto)
  1549 apply (case_tac xs, auto)
  1550 done
  1551 
  1552 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"
  1553 apply(induct xs arbitrary: n)
  1554  apply simp
  1555 apply(simp add:take_Cons split:nat.split)
  1556 done
  1557 
  1558 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"
  1559 apply(induct xs arbitrary: n)
  1560 apply simp
  1561 apply(simp add:drop_Cons split:nat.split)
  1562 done
  1563 
  1564 lemma take_map: "take n (map f xs) = map f (take n xs)"
  1565 apply (induct n arbitrary: xs, auto)
  1566 apply (case_tac xs, auto)
  1567 done
  1568 
  1569 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"
  1570 apply (induct n arbitrary: xs, auto)
  1571 apply (case_tac xs, auto)
  1572 done
  1573 
  1574 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"
  1575 apply (induct xs arbitrary: i, auto)
  1576 apply (case_tac i, auto)
  1577 done
  1578 
  1579 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"
  1580 apply (induct xs arbitrary: i, auto)
  1581 apply (case_tac i, auto)
  1582 done
  1583 
  1584 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"
  1585 apply (induct xs arbitrary: i n, auto)
  1586 apply (case_tac n, blast)
  1587 apply (case_tac i, auto)
  1588 done
  1589 
  1590 lemma nth_drop [simp]:
  1591   "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"
  1592 apply (induct n arbitrary: xs i, auto)
  1593 apply (case_tac xs, auto)
  1594 done
  1595 
  1596 lemma butlast_take:
  1597   "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"
  1598 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)
  1599 
  1600 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"
  1601 by (simp add: butlast_conv_take drop_take add_ac)
  1602 
  1603 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"
  1604 by (simp add: butlast_conv_take min_max.inf_absorb1)
  1605 
  1606 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"
  1607 by (simp add: butlast_conv_take drop_take add_ac)
  1608 
  1609 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"
  1610 by(simp add: hd_conv_nth)
  1611 
  1612 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"
  1613 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)
  1614 
  1615 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"
  1616 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)
  1617 
  1618 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"
  1619 using set_take_subset by fast
  1620 
  1621 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"
  1622 using set_drop_subset by fast
  1623 
  1624 lemma append_eq_conv_conj:
  1625   "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"
  1626 apply (induct xs arbitrary: zs, simp, clarsimp)
  1627 apply (case_tac zs, auto)
  1628 done
  1629 
  1630 lemma take_add: 
  1631   "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"
  1632 apply (induct xs arbitrary: i, auto) 
  1633 apply (case_tac i, simp_all)
  1634 done
  1635 
  1636 lemma append_eq_append_conv_if:
  1637  "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =
  1638   (if size xs\<^isub>1 \<le> size ys\<^isub>1
  1639    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
  1640    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)"
  1641 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)
  1642  apply simp
  1643 apply(case_tac ys\<^isub>1)
  1644 apply simp_all
  1645 done
  1646 
  1647 lemma take_hd_drop:
  1648   "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"
  1649 apply(induct xs arbitrary: n)
  1650 apply simp
  1651 apply(simp add:drop_Cons split:nat.split)
  1652 done
  1653 
  1654 lemma id_take_nth_drop:
  1655  "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs" 
  1656 proof -
  1657   assume si: "i < length xs"
  1658   hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto
  1659   moreover
  1660   from si have "take (Suc i) xs = take i xs @ [xs!i]"
  1661     apply (rule_tac take_Suc_conv_app_nth) by arith
  1662   ultimately show ?thesis by auto
  1663 qed
  1664   
  1665 lemma upd_conv_take_nth_drop:
  1666  "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"
  1667 proof -
  1668   assume i: "i < length xs"
  1669   have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"
  1670     by(rule arg_cong[OF id_take_nth_drop[OF i]])
  1671   also have "\<dots> = take i xs @ a # drop (Suc i) xs"
  1672     using i by (simp add: list_update_append)
  1673   finally show ?thesis .
  1674 qed
  1675 
  1676 lemma nth_drop':
  1677   "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"
  1678 apply (induct i arbitrary: xs)
  1679 apply (simp add: neq_Nil_conv)
  1680 apply (erule exE)+
  1681 apply simp
  1682 apply (case_tac xs)
  1683 apply simp_all
  1684 done
  1685 
  1686 
  1687 subsubsection {* @{text takeWhile} and @{text dropWhile} *}
  1688 
  1689 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"
  1690 by (induct xs) auto
  1691 
  1692 lemma takeWhile_append1 [simp]:
  1693 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"
  1694 by (induct xs) auto
  1695 
  1696 lemma takeWhile_append2 [simp]:
  1697 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
  1698 by (induct xs) auto
  1699 
  1700 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
  1701 by (induct xs) auto
  1702 
  1703 lemma dropWhile_append1 [simp]:
  1704 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
  1705 by (induct xs) auto
  1706 
  1707 lemma dropWhile_append2 [simp]:
  1708 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
  1709 by (induct xs) auto
  1710 
  1711 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"
  1712 by (induct xs) (auto split: split_if_asm)
  1713 
  1714 lemma takeWhile_eq_all_conv[simp]:
  1715  "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"
  1716 by(induct xs, auto)
  1717 
  1718 lemma dropWhile_eq_Nil_conv[simp]:
  1719  "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"
  1720 by(induct xs, auto)
  1721 
  1722 lemma dropWhile_eq_Cons_conv:
  1723  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"
  1724 by(induct xs, auto)
  1725 
  1726 text{* The following two lemmmas could be generalized to an arbitrary
  1727 property. *}
  1728 
  1729 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
  1730  takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"
  1731 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])
  1732 
  1733 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>
  1734   dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"
  1735 apply(induct xs)
  1736  apply simp
  1737 apply auto
  1738 apply(subst dropWhile_append2)
  1739 apply auto
  1740 done
  1741 
  1742 lemma takeWhile_not_last:
  1743  "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"
  1744 apply(induct xs)
  1745  apply simp
  1746 apply(case_tac xs)
  1747 apply(auto)
  1748 done
  1749 
  1750 lemma takeWhile_cong [fundef_cong, recdef_cong]:
  1751   "[| l = k; !!x. x : set l ==> P x = Q x |] 
  1752   ==> takeWhile P l = takeWhile Q k"
  1753 by (induct k arbitrary: l) (simp_all)
  1754 
  1755 lemma dropWhile_cong [fundef_cong, recdef_cong]:
  1756   "[| l = k; !!x. x : set l ==> P x = Q x |] 
  1757   ==> dropWhile P l = dropWhile Q k"
  1758 by (induct k arbitrary: l, simp_all)
  1759 
  1760 
  1761 subsubsection {* @{text zip} *}
  1762 
  1763 lemma zip_Nil [simp]: "zip [] ys = []"
  1764 by (induct ys) auto
  1765 
  1766 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"
  1767 by simp
  1768 
  1769 declare zip_Cons [simp del]
  1770 
  1771 lemma zip_Cons1:
  1772  "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"
  1773 by(auto split:list.split)
  1774 
  1775 lemma length_zip [simp]:
  1776 "length (zip xs ys) = min (length xs) (length ys)"
  1777 by (induct xs ys rule:list_induct2') auto
  1778 
  1779 lemma zip_append1:
  1780 "zip (xs @ ys) zs =
  1781 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
  1782 by (induct xs zs rule:list_induct2') auto
  1783 
  1784 lemma zip_append2:
  1785 "zip xs (ys @ zs) =
  1786 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
  1787 by (induct xs ys rule:list_induct2') auto
  1788 
  1789 lemma zip_append [simp]:
  1790  "[| length xs = length us; length ys = length vs |] ==>
  1791 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
  1792 by (simp add: zip_append1)
  1793 
  1794 lemma zip_rev:
  1795 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
  1796 by (induct rule:list_induct2, simp_all)
  1797 
  1798 lemma map_zip_map:
  1799  "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"
  1800 apply(induct xs arbitrary:ys) apply simp
  1801 apply(case_tac ys)
  1802 apply simp_all
  1803 done
  1804 
  1805 lemma map_zip_map2:
  1806  "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"
  1807 apply(induct xs arbitrary:ys) apply simp
  1808 apply(case_tac ys)
  1809 apply simp_all
  1810 done
  1811 
  1812 lemma nth_zip [simp]:
  1813 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"
  1814 apply (induct ys arbitrary: i xs, simp)
  1815 apply (case_tac xs)
  1816  apply (simp_all add: nth.simps split: nat.split)
  1817 done
  1818 
  1819 lemma set_zip:
  1820 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"
  1821 by (simp add: set_conv_nth cong: rev_conj_cong)
  1822 
  1823 lemma zip_update:
  1824 "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
  1825 by (rule sym, simp add: update_zip)
  1826 
  1827 lemma zip_replicate [simp]:
  1828   "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
  1829 apply (induct i arbitrary: j, auto)
  1830 apply (case_tac j, auto)
  1831 done
  1832 
  1833 lemma take_zip:
  1834   "take n (zip xs ys) = zip (take n xs) (take n ys)"
  1835 apply (induct n arbitrary: xs ys)
  1836  apply simp
  1837 apply (case_tac xs, simp)
  1838 apply (case_tac ys, simp_all)
  1839 done
  1840 
  1841 lemma drop_zip:
  1842   "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"
  1843 apply (induct n arbitrary: xs ys)
  1844  apply simp
  1845 apply (case_tac xs, simp)
  1846 apply (case_tac ys, simp_all)
  1847 done
  1848 
  1849 lemma set_zip_leftD:
  1850   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"
  1851 by (induct xs ys rule:list_induct2') auto
  1852 
  1853 lemma set_zip_rightD:
  1854   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"
  1855 by (induct xs ys rule:list_induct2') auto
  1856 
  1857 lemma in_set_zipE:
  1858   "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"
  1859 by(blast dest: set_zip_leftD set_zip_rightD)
  1860 
  1861 lemma zip_map_fst_snd:
  1862   "zip (map fst zs) (map snd zs) = zs"
  1863   by (induct zs) simp_all
  1864 
  1865 lemma zip_eq_conv:
  1866   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
  1867   by (auto simp add: zip_map_fst_snd)
  1868 
  1869 
  1870 subsubsection {* @{text list_all2} *}
  1871 
  1872 lemma list_all2_lengthD [intro?]: 
  1873   "list_all2 P xs ys ==> length xs = length ys"
  1874 by (simp add: list_all2_def)
  1875 
  1876 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"
  1877 by (simp add: list_all2_def)
  1878 
  1879 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"
  1880 by (simp add: list_all2_def)
  1881 
  1882 lemma list_all2_Cons [iff, code]:
  1883   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
  1884 by (auto simp add: list_all2_def)
  1885 
  1886 lemma list_all2_Cons1:
  1887 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
  1888 by (cases ys) auto
  1889 
  1890 lemma list_all2_Cons2:
  1891 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"
  1892 by (cases xs) auto
  1893 
  1894 lemma list_all2_rev [iff]:
  1895 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
  1896 by (simp add: list_all2_def zip_rev cong: conj_cong)
  1897 
  1898 lemma list_all2_rev1:
  1899 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"
  1900 by (subst list_all2_rev [symmetric]) simp
  1901 
  1902 lemma list_all2_append1:
  1903 "list_all2 P (xs @ ys) zs =
  1904 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>
  1905 list_all2 P xs us \<and> list_all2 P ys vs)"
  1906 apply (simp add: list_all2_def zip_append1)
  1907 apply (rule iffI)
  1908  apply (rule_tac x = "take (length xs) zs" in exI)
  1909  apply (rule_tac x = "drop (length xs) zs" in exI)
  1910  apply (force split: nat_diff_split simp add: min_def, clarify)
  1911 apply (simp add: ball_Un)
  1912 done
  1913 
  1914 lemma list_all2_append2:
  1915 "list_all2 P xs (ys @ zs) =
  1916 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>
  1917 list_all2 P us ys \<and> list_all2 P vs zs)"
  1918 apply (simp add: list_all2_def zip_append2)
  1919 apply (rule iffI)
  1920  apply (rule_tac x = "take (length ys) xs" in exI)
  1921  apply (rule_tac x = "drop (length ys) xs" in exI)
  1922  apply (force split: nat_diff_split simp add: min_def, clarify)
  1923 apply (simp add: ball_Un)
  1924 done
  1925 
  1926 lemma list_all2_append:
  1927   "length xs = length ys \<Longrightarrow>
  1928   list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"
  1929 by (induct rule:list_induct2, simp_all)
  1930 
  1931 lemma list_all2_appendI [intro?, trans]:
  1932   "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"
  1933 by (simp add: list_all2_append list_all2_lengthD)
  1934 
  1935 lemma list_all2_conv_all_nth:
  1936 "list_all2 P xs ys =
  1937 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"
  1938 by (force simp add: list_all2_def set_zip)
  1939 
  1940 lemma list_all2_trans:
  1941   assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"
  1942   shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"
  1943         (is "!!bs cs. PROP ?Q as bs cs")
  1944 proof (induct as)
  1945   fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"
  1946   show "!!cs. PROP ?Q (x # xs) bs cs"
  1947   proof (induct bs)
  1948     fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"
  1949     show "PROP ?Q (x # xs) (y # ys) cs"
  1950       by (induct cs) (auto intro: tr I1 I2)
  1951   qed simp
  1952 qed simp
  1953 
  1954 lemma list_all2_all_nthI [intro?]:
  1955   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"
  1956 by (simp add: list_all2_conv_all_nth)
  1957 
  1958 lemma list_all2I:
  1959   "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"
  1960 by (simp add: list_all2_def)
  1961 
  1962 lemma list_all2_nthD:
  1963   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
  1964 by (simp add: list_all2_conv_all_nth)
  1965 
  1966 lemma list_all2_nthD2:
  1967   "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"
  1968 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)
  1969 
  1970 lemma list_all2_map1: 
  1971   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"
  1972 by (simp add: list_all2_conv_all_nth)
  1973 
  1974 lemma list_all2_map2: 
  1975   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"
  1976 by (auto simp add: list_all2_conv_all_nth)
  1977 
  1978 lemma list_all2_refl [intro?]:
  1979   "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"
  1980 by (simp add: list_all2_conv_all_nth)
  1981 
  1982 lemma list_all2_update_cong:
  1983   "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  1984 by (simp add: list_all2_conv_all_nth nth_list_update)
  1985 
  1986 lemma list_all2_update_cong2:
  1987   "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"
  1988 by (simp add: list_all2_lengthD list_all2_update_cong)
  1989 
  1990 lemma list_all2_takeI [simp,intro?]:
  1991   "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"
  1992 apply (induct xs arbitrary: n ys)
  1993  apply simp
  1994 apply (clarsimp simp add: list_all2_Cons1)
  1995 apply (case_tac n)
  1996 apply auto
  1997 done
  1998 
  1999 lemma list_all2_dropI [simp,intro?]:
  2000   "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"
  2001 apply (induct as arbitrary: n bs, simp)
  2002 apply (clarsimp simp add: list_all2_Cons1)
  2003 apply (case_tac n, simp, simp)
  2004 done
  2005 
  2006 lemma list_all2_mono [intro?]:
  2007   "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"
  2008 apply (induct xs arbitrary: ys, simp)
  2009 apply (case_tac ys, auto)
  2010 done
  2011 
  2012 lemma list_all2_eq:
  2013   "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"
  2014 by (induct xs ys rule: list_induct2') auto
  2015 
  2016 
  2017 subsubsection {* @{text foldl} and @{text foldr} *}
  2018 
  2019 lemma foldl_append [simp]:
  2020   "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
  2021 by (induct xs arbitrary: a) auto
  2022 
  2023 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"
  2024 by (induct xs) auto
  2025 
  2026 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"
  2027 by(induct xs) simp_all
  2028 
  2029 text{* For efficient code generation: avoid intermediate list. *}
  2030 lemma foldl_map[code unfold]:
  2031   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"
  2032 by(induct xs arbitrary:a) simp_all
  2033 
  2034 lemma foldl_cong [fundef_cong, recdef_cong]:
  2035   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |] 
  2036   ==> foldl f a l = foldl g b k"
  2037 by (induct k arbitrary: a b l) simp_all
  2038 
  2039 lemma foldr_cong [fundef_cong, recdef_cong]:
  2040   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |] 
  2041   ==> foldr f l a = foldr g k b"
  2042 by (induct k arbitrary: a b l) simp_all
  2043 
  2044 lemma (in semigroup_add) foldl_assoc:
  2045 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"
  2046 by (induct zs arbitrary: y) (simp_all add:add_assoc)
  2047 
  2048 lemma (in monoid_add) foldl_absorb0:
  2049 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"
  2050 by (induct zs) (simp_all add:foldl_assoc)
  2051 
  2052 
  2053 text{* The ``First Duality Theorem'' in Bird \& Wadler: *}
  2054 
  2055 lemma foldl_foldr1_lemma:
  2056  "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"
  2057 by (induct xs arbitrary: a) (auto simp:add_assoc)
  2058 
  2059 corollary foldl_foldr1:
  2060  "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"
  2061 by (simp add:foldl_foldr1_lemma)
  2062 
  2063 
  2064 text{* The ``Third Duality Theorem'' in Bird \& Wadler: *}
  2065 
  2066 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"
  2067 by (induct xs) auto
  2068 
  2069 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"
  2070 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])
  2071 
  2072 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"
  2073   by (induct xs, auto simp add: foldl_assoc add_commute)
  2074 
  2075 text {*
  2076 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more
  2077 difficult to use because it requires an additional transitivity step.
  2078 *}
  2079 
  2080 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"
  2081 by (induct ns arbitrary: n) auto
  2082 
  2083 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"
  2084 by (force intro: start_le_sum simp add: in_set_conv_decomp)
  2085 
  2086 lemma sum_eq_0_conv [iff]:
  2087   "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"
  2088 by (induct ns arbitrary: m) auto
  2089 
  2090 lemma foldr_invariant: 
  2091   "\<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)"
  2092   by (induct xs, simp_all)
  2093 
  2094 lemma foldl_invariant: 
  2095   "\<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)"
  2096   by (induct xs arbitrary: x, simp_all)
  2097 
  2098 text{* @{const foldl} and @{text concat} *}
  2099 
  2100 lemma foldl_conv_concat:
  2101   "foldl (op @) xs xss = xs @ concat xss"
  2102 proof (induct xss arbitrary: xs)
  2103   case Nil show ?case by simp
  2104 next
  2105   interpret monoid_add "[]" "op @" proof qed simp_all
  2106   case Cons then show ?case by (simp add: foldl_absorb0)
  2107 qed
  2108 
  2109 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"
  2110   by (simp add: foldl_conv_concat)
  2111 
  2112 
  2113 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
  2114 
  2115 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"
  2116 by (induct xs) (simp_all add:add_assoc)
  2117 
  2118 lemma listsum_rev [simp]:
  2119   fixes xs :: "'a\<Colon>comm_monoid_add list"
  2120   shows "listsum (rev xs) = listsum xs"
  2121 by (induct xs) (simp_all add:add_ac)
  2122 
  2123 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"
  2124 by (induct xs) auto
  2125 
  2126 lemma length_concat: "length (concat xss) = listsum (map length xss)"
  2127 by (induct xss) simp_all
  2128 
  2129 text{* For efficient code generation ---
  2130        @{const listsum} is not tail recursive but @{const foldl} is. *}
  2131 lemma listsum[code unfold]: "listsum xs = foldl (op +) 0 xs"
  2132 by(simp add:listsum_foldr foldl_foldr1)
  2133 
  2134 
  2135 text{* Some syntactic sugar for summing a function over a list: *}
  2136 
  2137 syntax
  2138   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
  2139 syntax (xsymbols)
  2140   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2141 syntax (HTML output)
  2142   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2143 
  2144 translations -- {* Beware of argument permutation! *}
  2145   "SUM x<-xs. b" == "CONST listsum (map (%x. b) xs)"
  2146   "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (map (%x. b) xs)"
  2147 
  2148 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
  2149   by (induct xs) (simp_all add: left_distrib)
  2150 
  2151 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"
  2152   by (induct xs) (simp_all add: left_distrib)
  2153 
  2154 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
  2155 lemma uminus_listsum_map:
  2156   fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"
  2157   shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"
  2158 by (induct xs) simp_all
  2159 
  2160 
  2161 subsubsection {* @{text upt} *}
  2162 
  2163 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"
  2164 -- {* simp does not terminate! *}
  2165 by (induct j) auto
  2166 
  2167 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
  2168 by (subst upt_rec) simp
  2169 
  2170 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"
  2171 by(induct j)simp_all
  2172 
  2173 lemma upt_eq_Cons_conv:
  2174  "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"
  2175 apply(induct j arbitrary: x xs)
  2176  apply simp
  2177 apply(clarsimp simp add: append_eq_Cons_conv)
  2178 apply arith
  2179 done
  2180 
  2181 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"
  2182 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}
  2183 by simp
  2184 
  2185 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"
  2186   by (simp add: upt_rec)
  2187 
  2188 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
  2189 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}
  2190 by (induct k) auto
  2191 
  2192 lemma length_upt [simp]: "length [i..<j] = j - i"
  2193 by (induct j) (auto simp add: Suc_diff_le)
  2194 
  2195 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"
  2196 apply (induct j)
  2197 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)
  2198 done
  2199 
  2200 
  2201 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"
  2202 by(simp add:upt_conv_Cons)
  2203 
  2204 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"
  2205 apply(cases j)
  2206  apply simp
  2207 by(simp add:upt_Suc_append)
  2208 
  2209 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"
  2210 apply (induct m arbitrary: i, simp)
  2211 apply (subst upt_rec)
  2212 apply (rule sym)
  2213 apply (subst upt_rec)
  2214 apply (simp del: upt.simps)
  2215 done
  2216 
  2217 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"
  2218 apply(induct j)
  2219 apply auto
  2220 done
  2221 
  2222 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"
  2223 by (induct n) auto
  2224 
  2225 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"
  2226 apply (induct n m  arbitrary: i rule: diff_induct)
  2227 prefer 3 apply (subst map_Suc_upt[symmetric])
  2228 apply (auto simp add: less_diff_conv nth_upt)
  2229 done
  2230 
  2231 lemma nth_take_lemma:
  2232   "k <= length xs ==> k <= length ys ==>
  2233      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"
  2234 apply (atomize, induct k arbitrary: xs ys)
  2235 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)
  2236 txt {* Both lists must be non-empty *}
  2237 apply (case_tac xs, simp)
  2238 apply (case_tac ys, clarify)
  2239  apply (simp (no_asm_use))
  2240 apply clarify
  2241 txt {* prenexing's needed, not miniscoping *}
  2242 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)
  2243 apply blast
  2244 done
  2245 
  2246 lemma nth_equalityI:
  2247  "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
  2248 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
  2249 apply (simp_all add: take_all)
  2250 done
  2251 
  2252 lemma map_nth:
  2253   "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
  2254   by (rule nth_equalityI, auto)
  2255 
  2256 (* needs nth_equalityI *)
  2257 lemma list_all2_antisym:
  2258   "\<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> 
  2259   \<Longrightarrow> xs = ys"
  2260   apply (simp add: list_all2_conv_all_nth) 
  2261   apply (rule nth_equalityI, blast, simp)
  2262   done
  2263 
  2264 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
  2265 -- {* The famous take-lemma. *}
  2266 apply (drule_tac x = "max (length xs) (length ys)" in spec)
  2267 apply (simp add: le_max_iff_disj take_all)
  2268 done
  2269 
  2270 
  2271 lemma take_Cons':
  2272      "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
  2273 by (cases n) simp_all
  2274 
  2275 lemma drop_Cons':
  2276      "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
  2277 by (cases n) simp_all
  2278 
  2279 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
  2280 by (cases n) simp_all
  2281 
  2282 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
  2283 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
  2284 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
  2285 
  2286 declare take_Cons_number_of [simp] 
  2287         drop_Cons_number_of [simp] 
  2288         nth_Cons_number_of [simp] 
  2289 
  2290 
  2291 subsubsection {* @{text "distinct"} and @{text remdups} *}
  2292 
  2293 lemma distinct_append [simp]:
  2294 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
  2295 by (induct xs) auto
  2296 
  2297 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
  2298 by(induct xs) auto
  2299 
  2300 lemma set_remdups [simp]: "set (remdups xs) = set xs"
  2301 by (induct xs) (auto simp add: insert_absorb)
  2302 
  2303 lemma distinct_remdups [iff]: "distinct (remdups xs)"
  2304 by (induct xs) auto
  2305 
  2306 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
  2307 by (induct xs, auto)
  2308 
  2309 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
  2310 by (metis distinct_remdups distinct_remdups_id)
  2311 
  2312 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
  2313 by (metis distinct_remdups finite_list set_remdups)
  2314 
  2315 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
  2316 by (induct x, auto) 
  2317 
  2318 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
  2319 by (induct x, auto)
  2320 
  2321 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
  2322 by (induct xs) auto
  2323 
  2324 lemma length_remdups_eq[iff]:
  2325   "(length (remdups xs) = length xs) = (remdups xs = xs)"
  2326 apply(induct xs)
  2327  apply auto
  2328 apply(subgoal_tac "length (remdups xs) <= length xs")
  2329  apply arith
  2330 apply(rule length_remdups_leq)
  2331 done
  2332 
  2333 
  2334 lemma distinct_map:
  2335   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
  2336 by (induct xs) auto
  2337 
  2338 
  2339 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
  2340 by (induct xs) auto
  2341 
  2342 lemma distinct_upt[simp]: "distinct[i..<j]"
  2343 by (induct j) auto
  2344 
  2345 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
  2346 apply(induct xs arbitrary: i)
  2347  apply simp
  2348 apply (case_tac i)
  2349  apply simp_all
  2350 apply(blast dest:in_set_takeD)
  2351 done
  2352 
  2353 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
  2354 apply(induct xs arbitrary: i)
  2355  apply simp
  2356 apply (case_tac i)
  2357  apply simp_all
  2358 done
  2359 
  2360 lemma distinct_list_update:
  2361 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
  2362 shows "distinct (xs[i:=a])"
  2363 proof (cases "i < length xs")
  2364   case True
  2365   with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
  2366     apply (drule_tac id_take_nth_drop) by simp
  2367   with d True show ?thesis
  2368     apply (simp add: upd_conv_take_nth_drop)
  2369     apply (drule subst [OF id_take_nth_drop]) apply assumption
  2370     apply simp apply (cases "a = xs!i") apply simp by blast
  2371 next
  2372   case False with d show ?thesis by auto
  2373 qed
  2374 
  2375 
  2376 text {* It is best to avoid this indexed version of distinct, but
  2377 sometimes it is useful. *}
  2378 
  2379 lemma distinct_conv_nth:
  2380 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
  2381 apply (induct xs, simp, simp)
  2382 apply (rule iffI, clarsimp)
  2383  apply (case_tac i)
  2384 apply (case_tac j, simp)
  2385 apply (simp add: set_conv_nth)
  2386  apply (case_tac j)
  2387 apply (clarsimp simp add: set_conv_nth, simp) 
  2388 apply (rule conjI)
  2389 (*TOO SLOW
  2390 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2391 *)
  2392  apply (clarsimp simp add: set_conv_nth)
  2393  apply (erule_tac x = 0 in allE, simp)
  2394  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
  2395 (*TOO SLOW
  2396 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
  2397 *)
  2398 apply (erule_tac x = "Suc i" in allE, simp)
  2399 apply (erule_tac x = "Suc j" in allE, simp)
  2400 done
  2401 
  2402 lemma nth_eq_iff_index_eq:
  2403  "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
  2404 by(auto simp: distinct_conv_nth)
  2405 
  2406 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
  2407 by (induct xs) auto
  2408 
  2409 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
  2410 proof (induct xs)
  2411   case Nil thus ?case by simp
  2412 next
  2413   case (Cons x xs)
  2414   show ?case
  2415   proof (cases "x \<in> set xs")
  2416     case False with Cons show ?thesis by simp
  2417   next
  2418     case True with Cons.prems
  2419     have "card (set xs) = Suc (length xs)" 
  2420       by (simp add: card_insert_if split: split_if_asm)
  2421     moreover have "card (set xs) \<le> length xs" by (rule card_length)
  2422     ultimately have False by simp
  2423     thus ?thesis ..
  2424   qed
  2425 qed
  2426 
  2427 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"
  2428 apply (induct n == "length ws" arbitrary:ws) apply simp
  2429 apply(case_tac ws) apply simp
  2430 apply (simp split:split_if_asm)
  2431 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)
  2432 done
  2433 
  2434 lemma length_remdups_concat:
  2435  "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
  2436 by(simp add: set_concat distinct_card[symmetric])
  2437 
  2438 
  2439 subsubsection {* @{text remove1} *}
  2440 
  2441 lemma remove1_append:
  2442   "remove1 x (xs @ ys) =
  2443   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
  2444 by (induct xs) auto
  2445 
  2446 lemma in_set_remove1[simp]:
  2447   "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
  2448 apply (induct xs)
  2449 apply auto
  2450 done
  2451 
  2452 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
  2453 apply(induct xs)
  2454  apply simp
  2455 apply simp
  2456 apply blast
  2457 done
  2458 
  2459 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
  2460 apply(induct xs)
  2461  apply simp
  2462 apply simp
  2463 apply blast
  2464 done
  2465 
  2466 lemma length_remove1:
  2467   "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
  2468 apply (induct xs)
  2469  apply (auto dest!:length_pos_if_in_set)
  2470 done
  2471 
  2472 lemma remove1_filter_not[simp]:
  2473   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
  2474 by(induct xs) auto
  2475 
  2476 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
  2477 apply(insert set_remove1_subset)
  2478 apply fast
  2479 done
  2480 
  2481 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
  2482 by (induct xs) simp_all
  2483 
  2484 
  2485 subsubsection {* @{text removeAll} *}
  2486 
  2487 lemma removeAll_append[simp]:
  2488   "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
  2489 by (induct xs) auto
  2490 
  2491 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
  2492 by (induct xs) auto
  2493 
  2494 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
  2495 by (induct xs) auto
  2496 
  2497 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
  2498 lemma length_removeAll:
  2499   "length(removeAll x xs) = length xs - count x xs"
  2500 *)
  2501 
  2502 lemma removeAll_filter_not[simp]:
  2503   "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
  2504 by(induct xs) auto
  2505 
  2506 
  2507 lemma distinct_remove1_removeAll:
  2508   "distinct xs ==> remove1 x xs = removeAll x xs"
  2509 by (induct xs) simp_all
  2510 
  2511 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
  2512   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  2513 by (induct xs) (simp_all add:inj_on_def)
  2514 
  2515 lemma map_removeAll_inj: "inj f \<Longrightarrow>
  2516   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  2517 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
  2518 
  2519 
  2520 subsubsection {* @{text replicate} *}
  2521 
  2522 lemma length_replicate [simp]: "length (replicate n x) = n"
  2523 by (induct n) auto
  2524 
  2525 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
  2526 by (induct n) auto
  2527 
  2528 lemma replicate_app_Cons_same:
  2529 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
  2530 by (induct n) auto
  2531 
  2532 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
  2533 apply (induct n, simp)
  2534 apply (simp add: replicate_app_Cons_same)
  2535 done
  2536 
  2537 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
  2538 by (induct n) auto
  2539 
  2540 text{* Courtesy of Matthias Daum: *}
  2541 lemma append_replicate_commute:
  2542   "replicate n x @ replicate k x = replicate k x @ replicate n x"
  2543 apply (simp add: replicate_add [THEN sym])
  2544 apply (simp add: add_commute)
  2545 done
  2546 
  2547 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
  2548 by (induct n) auto
  2549 
  2550 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
  2551 by (induct n) auto
  2552 
  2553 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
  2554 by (atomize (full), induct n) auto
  2555 
  2556 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
  2557 apply (induct n arbitrary: i, simp)
  2558 apply (simp add: nth_Cons split: nat.split)
  2559 done
  2560 
  2561 text{* Courtesy of Matthias Daum (2 lemmas): *}
  2562 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
  2563 apply (case_tac "k \<le> i")
  2564  apply  (simp add: min_def)
  2565 apply (drule not_leE)
  2566 apply (simp add: min_def)
  2567 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
  2568  apply  simp
  2569 apply (simp add: replicate_add [symmetric])
  2570 done
  2571 
  2572 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
  2573 apply (induct k arbitrary: i)
  2574  apply simp
  2575 apply clarsimp
  2576 apply (case_tac i)
  2577  apply simp
  2578 apply clarsimp
  2579 done
  2580 
  2581 
  2582 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
  2583 by (induct n) auto
  2584 
  2585 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
  2586 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
  2587 
  2588 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
  2589 by auto
  2590 
  2591 lemma in_set_replicateD: "x : set (replicate n y) ==> x = y"
  2592 by (simp add: set_replicate_conv_if split: split_if_asm)
  2593 
  2594 lemma replicate_append_same:
  2595   "replicate i x @ [x] = x # replicate i x"
  2596   by (induct i) simp_all
  2597 
  2598 lemma map_replicate_trivial:
  2599   "map (\<lambda>i. x) [0..<i] = replicate i x"
  2600   by (induct i) (simp_all add: replicate_append_same)
  2601 
  2602 
  2603 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
  2604 by (induct n) auto
  2605 
  2606 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
  2607 by (induct n) auto
  2608 
  2609 lemma replicate_eq_replicate[simp]:
  2610   "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
  2611 apply(induct m arbitrary: n)
  2612  apply simp
  2613 apply(induct_tac n)
  2614 apply auto
  2615 done
  2616 
  2617 
  2618 subsubsection{*@{text rotate1} and @{text rotate}*}
  2619 
  2620 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
  2621 by(simp add:rotate1_def)
  2622 
  2623 lemma rotate0[simp]: "rotate 0 = id"
  2624 by(simp add:rotate_def)
  2625 
  2626 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
  2627 by(simp add:rotate_def)
  2628 
  2629 lemma rotate_add:
  2630   "rotate (m+n) = rotate m o rotate n"
  2631 by(simp add:rotate_def funpow_add)
  2632 
  2633 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
  2634 by(simp add:rotate_add)
  2635 
  2636 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
  2637 by(simp add:rotate_def funpow_swap1)
  2638 
  2639 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
  2640 by(cases xs) simp_all
  2641 
  2642 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
  2643 apply(induct n)
  2644  apply simp
  2645 apply (simp add:rotate_def)
  2646 done
  2647 
  2648 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
  2649 by(simp add:rotate1_def split:list.split)
  2650 
  2651 lemma rotate_drop_take:
  2652   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
  2653 apply(induct n)
  2654  apply simp
  2655 apply(simp add:rotate_def)
  2656 apply(cases "xs = []")
  2657  apply (simp)
  2658 apply(case_tac "n mod length xs = 0")
  2659  apply(simp add:mod_Suc)
  2660  apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
  2661 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
  2662                 take_hd_drop linorder_not_le)
  2663 done
  2664 
  2665 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
  2666 by(simp add:rotate_drop_take)
  2667 
  2668 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
  2669 by(simp add:rotate_drop_take)
  2670 
  2671 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
  2672 by(simp add:rotate1_def split:list.split)
  2673 
  2674 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
  2675 by (induct n arbitrary: xs) (simp_all add:rotate_def)
  2676 
  2677 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
  2678 by(simp add:rotate1_def split:list.split) blast
  2679 
  2680 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
  2681 by (induct n) (simp_all add:rotate_def)
  2682 
  2683 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
  2684 by(simp add:rotate_drop_take take_map drop_map)
  2685 
  2686 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
  2687 by(simp add:rotate1_def split:list.split)
  2688 
  2689 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
  2690 by (induct n) (simp_all add:rotate_def)
  2691 
  2692 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
  2693 by(simp add:rotate1_def split:list.split)
  2694 
  2695 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
  2696 by (induct n) (simp_all add:rotate_def)
  2697 
  2698 lemma rotate_rev:
  2699   "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
  2700 apply(simp add:rotate_drop_take rev_drop rev_take)
  2701 apply(cases "length xs = 0")
  2702  apply simp
  2703 apply(cases "n mod length xs = 0")
  2704  apply simp
  2705 apply(simp add:rotate_drop_take rev_drop rev_take)
  2706 done
  2707 
  2708 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
  2709 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
  2710 apply(subgoal_tac "length xs \<noteq> 0")
  2711  prefer 2 apply simp
  2712 using mod_less_divisor[of "length xs" n] by arith
  2713 
  2714 
  2715 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
  2716 
  2717 lemma sublist_empty [simp]: "sublist xs {} = []"
  2718 by (auto simp add: sublist_def)
  2719 
  2720 lemma sublist_nil [simp]: "sublist [] A = []"
  2721 by (auto simp add: sublist_def)
  2722 
  2723 lemma length_sublist:
  2724   "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
  2725 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
  2726 
  2727 lemma sublist_shift_lemma_Suc:
  2728   "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
  2729    map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
  2730 apply(induct xs arbitrary: "is")
  2731  apply simp
  2732 apply (case_tac "is")
  2733  apply simp
  2734 apply simp
  2735 done
  2736 
  2737 lemma sublist_shift_lemma:
  2738      "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
  2739       map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
  2740 by (induct xs rule: rev_induct) (simp_all add: add_commute)
  2741 
  2742 lemma sublist_append:
  2743      "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
  2744 apply (unfold sublist_def)
  2745 apply (induct l' rule: rev_induct, simp)
  2746 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
  2747 apply (simp add: add_commute)
  2748 done
  2749 
  2750 lemma sublist_Cons:
  2751 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
  2752 apply (induct l rule: rev_induct)
  2753  apply (simp add: sublist_def)
  2754 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
  2755 done
  2756 
  2757 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
  2758 apply(induct xs arbitrary: I)
  2759 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  2760 done
  2761 
  2762 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
  2763 by(auto simp add:set_sublist)
  2764 
  2765 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
  2766 by(auto simp add:set_sublist)
  2767 
  2768 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
  2769 by(auto simp add:set_sublist)
  2770 
  2771 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
  2772 by (simp add: sublist_Cons)
  2773 
  2774 
  2775 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
  2776 apply(induct xs arbitrary: I)
  2777  apply simp
  2778 apply(auto simp add:sublist_Cons)
  2779 done
  2780 
  2781 
  2782 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
  2783 apply (induct l rule: rev_induct, simp)
  2784 apply (simp split: nat_diff_split add: sublist_append)
  2785 done
  2786 
  2787 lemma filter_in_sublist:
  2788  "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
  2789 proof (induct xs arbitrary: s)
  2790   case Nil thus ?case by simp
  2791 next
  2792   case (Cons a xs)
  2793   moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
  2794   ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
  2795 qed
  2796 
  2797 
  2798 subsubsection {* @{const splice} *}
  2799 
  2800 lemma splice_Nil2 [simp, code]:
  2801  "splice xs [] = xs"
  2802 by (cases xs) simp_all
  2803 
  2804 lemma splice_Cons_Cons [simp, code]:
  2805  "splice (x#xs) (y#ys) = x # y # splice xs ys"
  2806 by simp
  2807 
  2808 declare splice.simps(2) [simp del, code del]
  2809 
  2810 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  2811 apply(induct xs arbitrary: ys) apply simp
  2812 apply(case_tac ys)
  2813  apply auto
  2814 done
  2815 
  2816 
  2817 subsubsection {* Infiniteness *}
  2818 
  2819 lemma finite_maxlen:
  2820   "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
  2821 proof (induct rule: finite.induct)
  2822   case emptyI show ?case by simp
  2823 next
  2824   case (insertI M xs)
  2825   then obtain n where "\<forall>s\<in>M. length s < n" by blast
  2826   hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
  2827   thus ?case ..
  2828 qed
  2829 
  2830 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
  2831 apply(rule notI)
  2832 apply(drule finite_maxlen)
  2833 apply (metis UNIV_I length_replicate less_not_refl)
  2834 done
  2835 
  2836 
  2837 subsection {*Sorting*}
  2838 
  2839 text{* Currently it is not shown that @{const sort} returns a
  2840 permutation of its input because the nicest proof is via multisets,
  2841 which are not yet available. Alternatively one could define a function
  2842 that counts the number of occurrences of an element in a list and use
  2843 that instead of multisets to state the correctness property. *}
  2844 
  2845 context linorder
  2846 begin
  2847 
  2848 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
  2849 apply(induct xs arbitrary: x) apply simp
  2850 by simp (blast intro: order_trans)
  2851 
  2852 lemma sorted_append:
  2853   "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
  2854 by (induct xs) (auto simp add:sorted_Cons)
  2855 
  2856 lemma set_insort: "set(insort x xs) = insert x (set xs)"
  2857 by (induct xs) auto
  2858 
  2859 lemma set_sort[simp]: "set(sort xs) = set xs"
  2860 by (induct xs) (simp_all add:set_insort)
  2861 
  2862 lemma distinct_insort: "distinct (insort x xs) = (x \<notin> set xs \<and> distinct xs)"
  2863 by(induct xs)(auto simp:set_insort)
  2864 
  2865 lemma distinct_sort[simp]: "distinct (sort xs) = distinct xs"
  2866 by(induct xs)(simp_all add:distinct_insort set_sort)
  2867 
  2868 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
  2869 apply (induct xs)
  2870  apply(auto simp:sorted_Cons set_insort)
  2871 done
  2872 
  2873 theorem sorted_sort[simp]: "sorted (sort xs)"
  2874 by (induct xs) (auto simp:sorted_insort)
  2875 
  2876 lemma insort_is_Cons: "\<forall>x\<in>set xs. a \<le> x \<Longrightarrow> insort a xs = a # xs"
  2877 by (cases xs) auto
  2878 
  2879 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
  2880 by (induct xs, auto simp add: sorted_Cons)
  2881 
  2882 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"
  2883 by (induct xs, auto simp add: sorted_Cons insort_is_Cons)
  2884 
  2885 lemma sorted_remdups[simp]:
  2886   "sorted l \<Longrightarrow> sorted (remdups l)"
  2887 by (induct l) (auto simp: sorted_Cons)
  2888 
  2889 lemma sorted_distinct_set_unique:
  2890 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
  2891 shows "xs = ys"
  2892 proof -
  2893   from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
  2894   from assms show ?thesis
  2895   proof(induct rule:list_induct2[OF 1])
  2896     case 1 show ?case by simp
  2897   next
  2898     case 2 thus ?case by (simp add:sorted_Cons)
  2899        (metis Diff_insert_absorb antisym insertE insert_iff)
  2900   qed
  2901 qed
  2902 
  2903 lemma finite_sorted_distinct_unique:
  2904 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
  2905 apply(drule finite_distinct_list)
  2906 apply clarify
  2907 apply(rule_tac a="sort xs" in ex1I)
  2908 apply (auto simp: sorted_distinct_set_unique)
  2909 done
  2910 
  2911 lemma sorted_take:
  2912   "sorted xs \<Longrightarrow> sorted (take n xs)"
  2913 proof (induct xs arbitrary: n rule: sorted.induct)
  2914   case 1 show ?case by simp
  2915 next
  2916   case 2 show ?case by (cases n) simp_all
  2917 next
  2918   case (3 x y xs)
  2919   then have "x \<le> y" by simp
  2920   show ?case proof (cases n)
  2921     case 0 then show ?thesis by simp
  2922   next
  2923     case (Suc m) 
  2924     with 3 have "sorted (take m (y # xs))" by simp
  2925     with Suc  `x \<le> y` show ?thesis by (cases m) simp_all
  2926   qed
  2927 qed
  2928 
  2929 lemma sorted_drop:
  2930   "sorted xs \<Longrightarrow> sorted (drop n xs)"
  2931 proof (induct xs arbitrary: n rule: sorted.induct)
  2932   case 1 show ?case by simp
  2933 next
  2934   case 2 show ?case by (cases n) simp_all
  2935 next
  2936   case 3 then show ?case by (cases n) simp_all
  2937 qed
  2938 
  2939 
  2940 end
  2941 
  2942 lemma sorted_upt[simp]: "sorted[i..<j]"
  2943 by (induct j) (simp_all add:sorted_append)
  2944 
  2945 
  2946 subsubsection {* @{text sorted_list_of_set} *}
  2947 
  2948 text{* This function maps (finite) linearly ordered sets to sorted
  2949 lists. Warning: in most cases it is not a good idea to convert from
  2950 sets to lists but one should convert in the other direction (via
  2951 @{const set}). *}
  2952 
  2953 
  2954 context linorder
  2955 begin
  2956 
  2957 definition
  2958  sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
  2959  [code del]: "sorted_list_of_set A == THE xs. set xs = A & sorted xs & distinct xs"
  2960 
  2961 lemma sorted_list_of_set[simp]: "finite A \<Longrightarrow>
  2962   set(sorted_list_of_set A) = A &
  2963   sorted(sorted_list_of_set A) & distinct(sorted_list_of_set A)"
  2964 apply(simp add:sorted_list_of_set_def)
  2965 apply(rule the1I2)
  2966  apply(simp_all add: finite_sorted_distinct_unique)
  2967 done
  2968 
  2969 lemma sorted_list_of_empty[simp]: "sorted_list_of_set {} = []"
  2970 unfolding sorted_list_of_set_def
  2971 apply(subst the_equality[of _ "[]"])
  2972 apply simp_all
  2973 done
  2974 
  2975 end
  2976 
  2977 
  2978 subsubsection {* @{text upto}: the generic interval-list *}
  2979 
  2980 class finite_intvl_succ = linorder +
  2981 fixes successor :: "'a \<Rightarrow> 'a"
  2982 assumes finite_intvl: "finite{a..b}"
  2983 and successor_incr: "a < successor a"
  2984 and ord_discrete: "\<not>(\<exists>x. a < x & x < successor a)"
  2985 
  2986 context finite_intvl_succ
  2987 begin
  2988 
  2989 definition
  2990  upto :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list" ("(1[_../_])") where
  2991 "upto i j == sorted_list_of_set {i..j}"
  2992 
  2993 lemma upto[simp]: "set[a..b] = {a..b} & sorted[a..b] & distinct[a..b]"
  2994 by(simp add:upto_def finite_intvl)
  2995 
  2996 lemma insert_intvl: "i \<le> j \<Longrightarrow> insert i {successor i..j} = {i..j}"
  2997 apply(insert successor_incr[of i])
  2998 apply(auto simp: atLeastAtMost_def atLeast_def atMost_def)
  2999 apply(metis ord_discrete less_le not_le)
  3000 done
  3001 
  3002 lemma sorted_list_of_set_rec: "i \<le> j \<Longrightarrow>
  3003   sorted_list_of_set {i..j} = i # sorted_list_of_set {successor i..j}"
  3004 apply(simp add:sorted_list_of_set_def upto_def)
  3005 apply (rule the1_equality[OF finite_sorted_distinct_unique])
  3006  apply (simp add:finite_intvl)
  3007 apply(rule the1I2[OF finite_sorted_distinct_unique])
  3008  apply (simp add:finite_intvl)
  3009 apply (simp add: sorted_Cons insert_intvl Ball_def)
  3010 apply (metis successor_incr leD less_imp_le order_trans)
  3011 done
  3012 
  3013 lemma sorted_list_of_set_rec2: "i \<le> j \<Longrightarrow>
  3014   sorted_list_of_set {i..successor j} =
  3015   sorted_list_of_set {i..j} @ [successor j]"
  3016 apply(simp add:sorted_list_of_set_def upto_def)
  3017 apply (rule the1_equality[OF finite_sorted_distinct_unique])
  3018  apply (simp add:finite_intvl)
  3019 apply(rule the1I2[OF finite_sorted_distinct_unique])
  3020  apply (simp add:finite_intvl)
  3021 apply (simp add: sorted_append Ball_def expand_set_eq)
  3022 apply(rule conjI)
  3023 apply (metis eq_iff leD linear not_leE ord_discrete order_trans successor_incr)
  3024 apply (metis leD linear order_trans successor_incr)
  3025 done
  3026 
  3027 lemma upto_rec[code]: "[i..j] = (if i \<le> j then i # [successor i..j] else [])"
  3028 by(simp add: upto_def sorted_list_of_set_rec)
  3029 
  3030 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
  3031 by(simp add: upto_rec)
  3032 
  3033 lemma upto_rec2: "i \<le> j \<Longrightarrow> [i..successor j] = [i..j] @ [successor j]"
  3034 by(simp add: upto_def sorted_list_of_set_rec2)
  3035 
  3036 end
  3037 
  3038 text{* The integers are an instance of the above class: *}
  3039 
  3040 instantiation int:: finite_intvl_succ
  3041 begin
  3042 
  3043 definition
  3044 successor_int_def: "successor = (%i\<Colon>int. i+1)"
  3045 
  3046 instance
  3047 by intro_classes (simp_all add: successor_int_def)
  3048 
  3049 end
  3050 
  3051 text{* Now @{term"[i..j::int]"} is defined for integers. *}
  3052 
  3053 hide (open) const successor
  3054 
  3055 lemma upto_rec2_int: "(i::int) \<le> j \<Longrightarrow> [i..j+1] = [i..j] @ [j+1]"
  3056 by(rule upto_rec2[where 'a = int, simplified successor_int_def])
  3057 
  3058 
  3059 subsubsection {* @{text lists}: the list-forming operator over sets *}
  3060 
  3061 inductive_set
  3062   lists :: "'a set => 'a list set"
  3063   for A :: "'a set"
  3064 where
  3065     Nil [intro!]: "[]: lists A"
  3066   | Cons [intro!,noatp]: "[| a: A; l: lists A|] ==> a#l : lists A"
  3067 
  3068 inductive_cases listsE [elim!,noatp]: "x#l : lists A"
  3069 inductive_cases listspE [elim!,noatp]: "listsp A (x # l)"
  3070 
  3071 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
  3072 by (rule predicate1I, erule listsp.induct, blast+)
  3073 
  3074 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
  3075 
  3076 lemma listsp_infI:
  3077   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
  3078 by induct blast+
  3079 
  3080 lemmas lists_IntI = listsp_infI [to_set]
  3081 
  3082 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
  3083 proof (rule mono_inf [where f=listsp, THEN order_antisym])
  3084   show "mono listsp" by (simp add: mono_def listsp_mono)
  3085   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
  3086 qed
  3087 
  3088 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]
  3089 
  3090 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
  3091 
  3092 lemma append_in_listsp_conv [iff]:
  3093      "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
  3094 by (induct xs) auto
  3095 
  3096 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
  3097 
  3098 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
  3099 -- {* eliminate @{text listsp} in favour of @{text set} *}
  3100 by (induct xs) auto
  3101 
  3102 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
  3103 
  3104 lemma in_listspD [dest!,noatp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
  3105 by (rule in_listsp_conv_set [THEN iffD1])
  3106 
  3107 lemmas in_listsD [dest!,noatp] = in_listspD [to_set]
  3108 
  3109 lemma in_listspI [intro!,noatp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
  3110 by (rule in_listsp_conv_set [THEN iffD2])
  3111 
  3112 lemmas in_listsI [intro!,noatp] = in_listspI [to_set]
  3113 
  3114 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
  3115 by auto
  3116 
  3117 
  3118 
  3119 subsubsection{* Inductive definition for membership *}
  3120 
  3121 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
  3122 where
  3123     elem:  "ListMem x (x # xs)"
  3124   | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
  3125 
  3126 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
  3127 apply (rule iffI)
  3128  apply (induct set: ListMem)
  3129   apply auto
  3130 apply (induct xs)
  3131  apply (auto intro: ListMem.intros)
  3132 done
  3133 
  3134 
  3135 
  3136 subsubsection{*Lists as Cartesian products*}
  3137 
  3138 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
  3139 @{term A} and tail drawn from @{term Xs}.*}
  3140 
  3141 constdefs
  3142   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set"
  3143   "set_Cons A XS == {z. \<exists>x xs. z = x#xs & x \<in> A & xs \<in> XS}"
  3144 declare set_Cons_def [code del]
  3145 
  3146 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
  3147 by (auto simp add: set_Cons_def)
  3148 
  3149 text{*Yields the set of lists, all of the same length as the argument and
  3150 with elements drawn from the corresponding element of the argument.*}
  3151 
  3152 consts  listset :: "'a set list \<Rightarrow> 'a list set"
  3153 primrec
  3154    "listset []    = {[]}"
  3155    "listset(A#As) = set_Cons A (listset As)"
  3156 
  3157 
  3158 subsection{*Relations on Lists*}
  3159 
  3160 subsubsection {* Length Lexicographic Ordering *}
  3161 
  3162 text{*These orderings preserve well-foundedness: shorter lists 
  3163   precede longer lists. These ordering are not used in dictionaries.*}
  3164 
  3165 consts lexn :: "('a * 'a)set => nat => ('a list * 'a list)set"
  3166         --{*The lexicographic ordering for lists of the specified length*}
  3167 primrec
  3168   "lexn r 0 = {}"
  3169   "lexn r (Suc n) =
  3170     (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
  3171     {(xs,ys). length xs = Suc n \<and> length ys = Suc n}"
  3172 
  3173 constdefs
  3174   lex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
  3175     "lex r == \<Union>n. lexn r n"
  3176         --{*Holds only between lists of the same length*}
  3177 
  3178   lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set"
  3179     "lenlex r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
  3180         --{*Compares lists by their length and then lexicographically*}
  3181 
  3182 declare lex_def [code del]
  3183 
  3184 
  3185 lemma wf_lexn: "wf r ==> wf (lexn r n)"
  3186 apply (induct n, simp, simp)
  3187 apply(rule wf_subset)
  3188  prefer 2 apply (rule Int_lower1)
  3189 apply(rule wf_prod_fun_image)
  3190  prefer 2 apply (rule inj_onI, auto)
  3191 done
  3192 
  3193 lemma lexn_length:
  3194   "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
  3195 by (induct n arbitrary: xs ys) auto
  3196 
  3197 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
  3198 apply (unfold lex_def)
  3199 apply (rule wf_UN)
  3200 apply (blast intro: wf_lexn, clarify)
  3201 apply (rename_tac m n)
  3202 apply (subgoal_tac "m \<noteq> n")
  3203  prefer 2 apply blast
  3204 apply (blast dest: lexn_length not_sym)
  3205 done
  3206 
  3207 lemma lexn_conv:
  3208   "lexn r n =
  3209     {(xs,ys). length xs = n \<and> length ys = n \<and>
  3210     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
  3211 apply (induct n, simp)
  3212 apply (simp add: image_Collect lex_prod_def, safe, blast)
  3213  apply (rule_tac x = "ab # xys" in exI, simp)
  3214 apply (case_tac xys, simp_all, blast)
  3215 done
  3216 
  3217 lemma lex_conv:
  3218   "lex r =
  3219     {(xs,ys). length xs = length ys \<and>
  3220     (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
  3221 by (force simp add: lex_def lexn_conv)
  3222 
  3223 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
  3224 by (unfold lenlex_def) blast
  3225 
  3226 lemma lenlex_conv:
  3227     "lenlex r = {(xs,ys). length xs < length ys |
  3228                  length xs = length ys \<and> (xs, ys) : lex r}"
  3229 by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
  3230 
  3231 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
  3232 by (simp add: lex_conv)
  3233 
  3234 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
  3235 by (simp add:lex_conv)
  3236 
  3237 lemma Cons_in_lex [simp]:
  3238     "((x # xs, y # ys) : lex r) =
  3239       ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
  3240 apply (simp add: lex_conv)
  3241 apply (rule iffI)
  3242  prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
  3243 apply (case_tac xys, simp, simp)
  3244 apply blast
  3245 done
  3246 
  3247 
  3248 subsubsection {* Lexicographic Ordering *}
  3249 
  3250 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
  3251     This ordering does \emph{not} preserve well-foundedness.
  3252      Author: N. Voelker, March 2005. *} 
  3253 
  3254 constdefs 
  3255   lexord :: "('a * 'a)set \<Rightarrow> ('a list * 'a list) set" 
  3256   "lexord  r == {(x,y). \<exists> a v. y = x @ a # v \<or> 
  3257             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
  3258 declare lexord_def [code del]
  3259 
  3260 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
  3261 by (unfold lexord_def, induct_tac y, auto) 
  3262 
  3263 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
  3264 by (unfold lexord_def, induct_tac x, auto)
  3265 
  3266 lemma lexord_cons_cons[simp]:
  3267      "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
  3268   apply (unfold lexord_def, safe, simp_all)
  3269   apply (case_tac u, simp, simp)
  3270   apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
  3271   apply (erule_tac x="b # u" in allE)
  3272   by force
  3273 
  3274 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
  3275 
  3276 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
  3277 by (induct_tac x, auto)  
  3278 
  3279 lemma lexord_append_left_rightI:
  3280      "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
  3281 by (induct_tac u, auto)
  3282 
  3283 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
  3284 by (induct x, auto)
  3285 
  3286 lemma lexord_append_leftD:
  3287      "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
  3288 by (erule rev_mp, induct_tac x, auto)
  3289 
  3290 lemma lexord_take_index_conv: 
  3291    "((x,y) : lexord r) = 
  3292     ((length x < length y \<and> take (length x) y = x) \<or> 
  3293      (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
  3294   apply (unfold lexord_def Let_def, clarsimp) 
  3295   apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
  3296   apply auto 
  3297   apply (rule_tac x="hd (drop (length x) y)" in exI)
  3298   apply (rule_tac x="tl (drop (length x) y)" in exI)
  3299   apply (erule subst, simp add: min_def) 
  3300   apply (rule_tac x ="length u" in exI, simp) 
  3301   apply (rule_tac x ="take i x" in exI) 
  3302   apply (rule_tac x ="x ! i" in exI) 
  3303   apply (rule_tac x ="y ! i" in exI, safe) 
  3304   apply (rule_tac x="drop (Suc i) x" in exI)
  3305   apply (drule sym, simp add: drop_Suc_conv_tl) 
  3306   apply (rule_tac x="drop (Suc i) y" in exI)
  3307   by (simp add: drop_Suc_conv_tl) 
  3308 
  3309 -- {* lexord is extension of partial ordering List.lex *} 
  3310 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
  3311   apply (rule_tac x = y in spec) 
  3312   apply (induct_tac x, clarsimp) 
  3313   by (clarify, case_tac x, simp, force)
  3314 
  3315 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"
  3316   by (induct y, auto)
  3317 
  3318 lemma lexord_trans: 
  3319     "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
  3320    apply (erule rev_mp)+
  3321    apply (rule_tac x = x in spec) 
  3322   apply (rule_tac x = z in spec) 
  3323   apply ( induct_tac y, simp, clarify)
  3324   apply (case_tac xa, erule ssubst) 
  3325   apply (erule allE, erule allE) -- {* avoid simp recursion *} 
  3326   apply (case_tac x, simp, simp) 
  3327   apply (case_tac x, erule allE, erule allE, simp)
  3328   apply (erule_tac x = listb in allE) 
  3329   apply (erule_tac x = lista in allE, simp)
  3330   apply (unfold trans_def)
  3331   by blast
  3332 
  3333 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
  3334 by (rule transI, drule lexord_trans, blast) 
  3335 
  3336 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"
  3337   apply (rule_tac x = y in spec) 
  3338   apply (induct_tac x, rule allI) 
  3339   apply (case_tac x, simp, simp) 
  3340   apply (rule allI, case_tac x, simp, simp) 
  3341   by blast
  3342 
  3343 
  3344 subsection {* Lexicographic combination of measure functions *}
  3345 
  3346 text {* These are useful for termination proofs *}
  3347 
  3348 definition
  3349   "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
  3350 
  3351 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"
  3352 unfolding measures_def
  3353 by blast
  3354 
  3355 lemma in_measures[simp]: 
  3356   "(x, y) \<in> measures [] = False"
  3357   "(x, y) \<in> measures (f # fs)
  3358          = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
  3359 unfolding measures_def
  3360 by auto
  3361 
  3362 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
  3363 by simp
  3364 
  3365 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
  3366 by auto
  3367 
  3368 
  3369 subsubsection{*Lifting a Relation on List Elements to the Lists*}
  3370 
  3371 inductive_set
  3372   listrel :: "('a * 'a)set => ('a list * 'a list)set"
  3373   for r :: "('a * 'a)set"
  3374 where
  3375     Nil:  "([],[]) \<in> listrel r"
  3376   | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
  3377 
  3378 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
  3379 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
  3380 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
  3381 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
  3382 
  3383 
  3384 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
  3385 apply clarify  
  3386 apply (erule listrel.induct)
  3387 apply (blast intro: listrel.intros)+
  3388 done
  3389 
  3390 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
  3391 apply clarify 
  3392 apply (erule listrel.induct, auto) 
  3393 done
  3394 
  3395 lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)" 
  3396 apply (simp add: refl_on_def listrel_subset Ball_def)
  3397 apply (rule allI) 
  3398 apply (induct_tac x) 
  3399 apply (auto intro: listrel.intros)
  3400 done
  3401 
  3402 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
  3403 apply (auto simp add: sym_def)
  3404 apply (erule listrel.induct) 
  3405 apply (blast intro: listrel.intros)+
  3406 done
  3407 
  3408 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
  3409 apply (simp add: trans_def)
  3410 apply (intro allI) 
  3411 apply (rule impI) 
  3412 apply (erule listrel.induct) 
  3413 apply (blast intro: listrel.intros)+
  3414 done
  3415 
  3416 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
  3417 by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) 
  3418 
  3419 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
  3420 by (blast intro: listrel.intros)
  3421 
  3422 lemma listrel_Cons:
  3423      "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})";
  3424 by (auto simp add: set_Cons_def intro: listrel.intros) 
  3425 
  3426 
  3427 subsection{*Miscellany*}
  3428 
  3429 subsubsection {* Characters and strings *}
  3430 
  3431 datatype nibble =
  3432     Nibble0 | Nibble1 | Nibble2 | Nibble3 | Nibble4 | Nibble5 | Nibble6 | Nibble7
  3433   | Nibble8 | Nibble9 | NibbleA | NibbleB | NibbleC | NibbleD | NibbleE | NibbleF
  3434 
  3435 lemma UNIV_nibble:
  3436   "UNIV = {Nibble0, Nibble1, Nibble2, Nibble3, Nibble4, Nibble5, Nibble6, Nibble7,
  3437     Nibble8, Nibble9, NibbleA, NibbleB, NibbleC, NibbleD, NibbleE, NibbleF}" (is "_ = ?A")
  3438 proof (rule UNIV_eq_I)
  3439   fix x show "x \<in> ?A" by (cases x) simp_all
  3440 qed
  3441 
  3442 instance nibble :: finite
  3443   by default (simp add: UNIV_nibble)
  3444 
  3445 datatype char = Char nibble nibble
  3446   -- "Note: canonical order of character encoding coincides with standard term ordering"
  3447 
  3448 lemma UNIV_char:
  3449   "UNIV = image (split Char) (UNIV \<times> UNIV)"
  3450 proof (rule UNIV_eq_I)
  3451   fix x show "x \<in> image (split Char) (UNIV \<times> UNIV)" by (cases x) auto
  3452 qed
  3453 
  3454 instance char :: finite
  3455   by default (simp add: UNIV_char)
  3456 
  3457 lemma size_char [code, simp]:
  3458   "size (c::char) = 0" by (cases c) simp
  3459 
  3460 lemma char_size [code, simp]:
  3461   "char_size (c::char) = 0" by (cases c) simp
  3462 
  3463 primrec nibble_pair_of_char :: "char \<Rightarrow> nibble \<times> nibble" where
  3464   "nibble_pair_of_char (Char n m) = (n, m)"
  3465 
  3466 declare nibble_pair_of_char.simps [code del]
  3467 
  3468 setup {*
  3469 let
  3470   val nibbles = map (Thm.cterm_of @{theory} o HOLogic.mk_nibble) (0 upto 15);
  3471   val thms = map_product
  3472    (fn n => fn m => Drule.instantiate' [] [SOME n, SOME m] @{thm nibble_pair_of_char.simps})
  3473       nibbles nibbles;
  3474 in
  3475   PureThy.note_thmss Thm.lemmaK [((Binding.name "nibble_pair_of_char_simps", []), [(thms, [])])]
  3476   #-> (fn [(_, thms)] => fold_rev Code.add_eqn thms)
  3477 end
  3478 *}
  3479 
  3480 lemma char_case_nibble_pair [code, code inline]:
  3481   "char_case f = split f o nibble_pair_of_char"
  3482   by (simp add: expand_fun_eq split: char.split)
  3483 
  3484 lemma char_rec_nibble_pair [code, code inline]:
  3485   "char_rec f = split f o nibble_pair_of_char"
  3486   unfolding char_case_nibble_pair [symmetric]
  3487   by (simp add: expand_fun_eq split: char.split)
  3488 
  3489 types string = "char list"
  3490 
  3491 syntax
  3492   "_Char" :: "xstr => char"    ("CHR _")
  3493   "_String" :: "xstr => string"    ("_")
  3494 
  3495 setup StringSyntax.setup
  3496 
  3497 
  3498 subsection {* Size function *}
  3499 
  3500 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
  3501 by (rule is_measure_trivial)
  3502 
  3503 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
  3504 by (rule is_measure_trivial)
  3505 
  3506 lemma list_size_estimation[termination_simp]: 
  3507   "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
  3508 by (induct xs) auto
  3509 
  3510 lemma list_size_estimation'[termination_simp]: 
  3511   "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
  3512 by (induct xs) auto
  3513 
  3514 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
  3515 by (induct xs) auto
  3516 
  3517 lemma list_size_pointwise[termination_simp]: 
  3518   "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
  3519 by (induct xs) force+
  3520 
  3521 subsection {* Code generator *}
  3522 
  3523 subsubsection {* Setup *}
  3524 
  3525 types_code
  3526   "list" ("_ list")
  3527 attach (term_of) {*
  3528 fun term_of_list f T = HOLogic.mk_list T o map f;
  3529 *}
  3530 attach (test) {*
  3531 fun gen_list' aG aT i j = frequency
  3532   [(i, fn () =>
  3533       let
  3534         val (x, t) = aG j;
  3535         val (xs, ts) = gen_list' aG aT (i-1) j
  3536       in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
  3537    (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
  3538 and gen_list aG aT i = gen_list' aG aT i i;
  3539 *}
  3540   "char" ("string")
  3541 attach (term_of) {*
  3542 val term_of_char = HOLogic.mk_char o ord;
  3543 *}
  3544 attach (test) {*
  3545 fun gen_char i =
  3546   let val j = random_range (ord "a") (Int.min (ord "a" + i, ord "z"))
  3547   in (chr j, fn () => HOLogic.mk_char j) end;
  3548 *}
  3549 
  3550 consts_code "Cons" ("(_ ::/ _)")
  3551 
  3552 code_type list
  3553   (SML "_ list")
  3554   (OCaml "_ list")
  3555   (Haskell "![_]")
  3556 
  3557 code_reserved SML
  3558   list
  3559 
  3560 code_reserved OCaml
  3561   list
  3562 
  3563 code_const Nil
  3564   (SML "[]")
  3565   (OCaml "[]")
  3566   (Haskell "[]")
  3567 
  3568 ML {*
  3569 local
  3570 
  3571 open Basic_Code_Thingol;
  3572 
  3573 fun implode_list naming t = case pairself
  3574   (Code_Thingol.lookup_const naming) (@{const_name Nil}, @{const_name Cons})
  3575    of (SOME nil', SOME cons') => let
  3576           fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
  3577                 if c = cons'
  3578                 then SOME (t1, t2)
  3579                 else NONE
  3580             | dest_cons _ = NONE;
  3581           val (ts, t') = Code_Thingol.unfoldr dest_cons t;
  3582         in case t'
  3583          of IConst (c, _) => if c = nil' then SOME ts else NONE
  3584           | _ => NONE
  3585         end
  3586     | _ => NONE
  3587 
  3588 fun decode_char naming (IConst (c1, _), IConst (c2, _)) = (case map_filter
  3589   (Code_Thingol.lookup_const naming)[@{const_name Nibble0}, @{const_name Nibble1},
  3590    @{const_name Nibble2}, @{const_name Nibble3},
  3591    @{const_name Nibble4}, @{const_name Nibble5},
  3592    @{const_name Nibble6}, @{const_name Nibble7},
  3593    @{const_name Nibble8}, @{const_name Nibble9},
  3594    @{const_name NibbleA}, @{const_name NibbleB},
  3595    @{const_name NibbleC}, @{const_name NibbleD},
  3596    @{const_name NibbleE}, @{const_name NibbleF}]
  3597    of nibbles' as [_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] => let
  3598           fun idx c = find_index (curry (op =) c) nibbles';
  3599           fun decode ~1 _ = NONE
  3600             | decode _ ~1 = NONE
  3601             | decode n m = SOME (chr (n * 16 + m));
  3602         in decode (idx c1) (idx c2) end
  3603     | _ => NONE)
  3604  | decode_char _ _ = NONE
  3605    
  3606 fun implode_string naming mk_char mk_string ts = case
  3607   Code_Thingol.lookup_const naming @{const_name Char}
  3608    of SOME char' => let
  3609         fun implode_char (IConst (c, _) `$ t1 `$ t2) =
  3610               if c = char' then decode_char naming (t1, t2) else NONE
  3611           | implode_char _ = NONE;
  3612         val ts' = map implode_char ts;
  3613       in if forall is_some ts'
  3614         then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
  3615         else NONE
  3616       end
  3617     | _ => NONE;
  3618 
  3619 fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
  3620   Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
  3621     pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
  3622     Code_Printer.str target_cons,
  3623     pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
  3624   ];
  3625 
  3626 fun pretty_list literals =
  3627   let
  3628     val mk_list = Code_Printer.literal_list literals;
  3629     fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
  3630       case Option.map (cons t1) (implode_list naming t2)
  3631        of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
  3632         | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
  3633   in (2, pretty) end;
  3634 
  3635 fun pretty_list_string literals =
  3636   let
  3637     val mk_list = Code_Printer.literal_list literals;
  3638     val mk_char = Code_Printer.literal_char literals;
  3639     val mk_string = Code_Printer.literal_string literals;
  3640     fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
  3641       case Option.map (cons t1) (implode_list naming t2)
  3642        of SOME ts => (case implode_string naming mk_char mk_string ts
  3643            of SOME p => p
  3644             | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
  3645         | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
  3646   in (2, pretty) end;
  3647 
  3648 fun pretty_char literals =
  3649   let
  3650     val mk_char = Code_Printer.literal_char literals;
  3651     fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
  3652       case decode_char naming (t1, t2)
  3653        of SOME c => (Code_Printer.str o mk_char) c
  3654         | NONE => Code_Printer.nerror thm "Illegal character expression";
  3655   in (2, pretty) end;
  3656 
  3657 fun pretty_message literals =
  3658   let
  3659     val mk_char = Code_Printer.literal_char literals;
  3660     val mk_string = Code_Printer.literal_string literals;
  3661     fun pretty _ naming thm _ _ [(t, _)] =
  3662       case implode_list naming t
  3663        of SOME ts => (case implode_string naming mk_char mk_string ts
  3664            of SOME p => p
  3665             | NONE => Code_Printer.nerror thm "Illegal message expression")
  3666         | NONE => Code_Printer.nerror thm "Illegal message expression";
  3667   in (1, pretty) end;
  3668 
  3669 in
  3670 
  3671 fun add_literal_list target thy =
  3672   let
  3673     val pr = pretty_list (Code_Target.the_literals thy target);
  3674   in
  3675     thy
  3676     |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
  3677   end;
  3678 
  3679 fun add_literal_list_string target thy =
  3680   let
  3681     val pr = pretty_list_string (Code_Target.the_literals thy target);
  3682   in
  3683     thy
  3684     |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
  3685   end;
  3686 
  3687 fun add_literal_char target thy =
  3688   let
  3689     val pr = pretty_char (Code_Target.the_literals thy target);
  3690   in
  3691     thy
  3692     |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
  3693   end;
  3694 
  3695 fun add_literal_message str target thy =
  3696   let
  3697     val pr = pretty_message (Code_Target.the_literals thy target);
  3698   in
  3699     thy
  3700     |> Code_Target.add_syntax_const target str (SOME pr)
  3701   end;
  3702 
  3703 end;
  3704 *}
  3705 
  3706 setup {*
  3707   fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
  3708 *}
  3709 
  3710 code_instance list :: eq
  3711   (Haskell -)
  3712 
  3713 code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
  3714   (Haskell infixl 4 "==")
  3715 
  3716 setup {*
  3717 let
  3718 
  3719 fun list_codegen thy defs dep thyname b t gr =
  3720   let
  3721     val ts = HOLogic.dest_list t;
  3722     val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
  3723       (fastype_of t) gr;
  3724     val (ps, gr'') = fold_map
  3725       (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
  3726   in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
  3727 
  3728 fun char_codegen thy defs dep thyname b t gr =
  3729   let
  3730     val i = HOLogic.dest_char t;
  3731     val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
  3732       (fastype_of t) gr;
  3733   in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
  3734   end handle TERM _ => NONE;
  3735 
  3736 in
  3737   Codegen.add_codegen "list_codegen" list_codegen
  3738   #> Codegen.add_codegen "char_codegen" char_codegen
  3739 end;
  3740 *}
  3741 
  3742 
  3743 subsubsection {* Generation of efficient code *}
  3744 
  3745 primrec
  3746   member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
  3747 where 
  3748   "x mem [] \<longleftrightarrow> False"
  3749   | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
  3750 
  3751 primrec
  3752   null:: "'a list \<Rightarrow> bool"
  3753 where
  3754   "null [] = True"
  3755   | "null (x#xs) = False"
  3756 
  3757 primrec
  3758   list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  3759 where
  3760   "list_inter [] bs = []"
  3761   | "list_inter (a#as) bs =
  3762      (if a \<in> set bs then a # list_inter as bs else list_inter as bs)"
  3763 
  3764 primrec
  3765   list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
  3766 where
  3767   "list_all P [] = True"
  3768   | "list_all P (x#xs) = (P x \<and> list_all P xs)"
  3769 
  3770 primrec
  3771   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
  3772 where
  3773   "list_ex P [] = False"
  3774   | "list_ex P (x#xs) = (P x \<or> list_ex P xs)"
  3775 
  3776 primrec
  3777   filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  3778 where
  3779   "filtermap f [] = []"
  3780   | "filtermap f (x#xs) =
  3781      (case f x of None \<Rightarrow> filtermap f xs
  3782       | Some y \<Rightarrow> y # filtermap f xs)"
  3783 
  3784 primrec
  3785   map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  3786 where
  3787   "map_filter f P [] = []"
  3788   | "map_filter f P (x#xs) =
  3789      (if P x then f x # map_filter f P xs else map_filter f P xs)"
  3790 
  3791 primrec
  3792   length_unique :: "'a list \<Rightarrow> nat"
  3793 where
  3794   "length_unique [] = 0"
  3795   | "length_unique (x#xs) =
  3796       (if x \<in> set xs then length_unique xs else Suc (length_unique xs))"
  3797 
  3798 text {*
  3799   Only use @{text mem} for generating executable code.  Otherwise use
  3800   @{prop "x : set xs"} instead --- it is much easier to reason about.
  3801   The same is true for @{const list_all} and @{const list_ex}: write
  3802   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} instead because the HOL
  3803   quantifiers are aleady known to the automatic provers. In fact, the
  3804   declarations in the code subsection make sure that @{text "\<in>"},
  3805   @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"} are implemented
  3806   efficiently.
  3807 
  3808   Efficient emptyness check is implemented by @{const null}.
  3809 
  3810   The functions @{const filtermap} and @{const map_filter} are just
  3811   there to generate efficient code. Do not use
  3812   them for modelling and proving.
  3813 *}
  3814 
  3815 lemma rev_foldl_cons [code]:
  3816   "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"
  3817 proof (induct xs)
  3818   case Nil then show ?case by simp
  3819 next
  3820   case Cons
  3821   {
  3822     fix x xs ys
  3823     have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]
  3824       = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"
  3825     by (induct xs arbitrary: ys) auto
  3826   }
  3827   note aux = this
  3828   show ?case by (induct xs) (auto simp add: Cons aux)
  3829 qed
  3830 
  3831 lemma mem_iff [code post]:
  3832   "x mem xs \<longleftrightarrow> x \<in> set xs"
  3833 by (induct xs) auto
  3834 
  3835 lemmas in_set_code [code unfold] = mem_iff [symmetric]
  3836 
  3837 lemma empty_null [code inline]:
  3838   "xs = [] \<longleftrightarrow> null xs"
  3839 by (cases xs) simp_all
  3840 
  3841 lemmas null_empty [code post] =
  3842   empty_null [symmetric]
  3843 
  3844 lemma list_inter_conv:
  3845   "set (list_inter xs ys) = set xs \<inter> set ys"
  3846 by (induct xs) auto
  3847 
  3848 lemma list_all_iff [code post]:
  3849   "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
  3850 by (induct xs) auto
  3851 
  3852 lemmas list_ball_code [code unfold] = list_all_iff [symmetric]
  3853 
  3854 lemma list_all_append [simp]:
  3855   "list_all P (xs @ ys) \<longleftrightarrow> (list_all P xs \<and> list_all P ys)"
  3856 by (induct xs) auto
  3857 
  3858 lemma list_all_rev [simp]:
  3859   "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
  3860 by (simp add: list_all_iff)
  3861 
  3862 lemma list_all_length:
  3863   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
  3864   unfolding list_all_iff by (auto intro: all_nth_imp_all_set)
  3865 
  3866 lemma list_ex_iff [code post]:
  3867   "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
  3868 by (induct xs) simp_all
  3869 
  3870 lemmas list_bex_code [code unfold] =
  3871   list_ex_iff [symmetric]
  3872 
  3873 lemma list_ex_length:
  3874   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
  3875   unfolding list_ex_iff set_conv_nth by auto
  3876 
  3877 lemma filtermap_conv:
  3878    "filtermap f xs = map (\<lambda>x. the (f x)) (filter (\<lambda>x. f x \<noteq> None) xs)"
  3879 by (induct xs) (simp_all split: option.split) 
  3880 
  3881 lemma map_filter_conv [simp]:
  3882   "map_filter f P xs = map f (filter P xs)"
  3883 by (induct xs) auto
  3884 
  3885 lemma length_remdups_length_unique [code inline]:
  3886   "length (remdups xs) = length_unique xs"
  3887   by (induct xs) simp_all
  3888 
  3889 hide (open) const length_unique
  3890 
  3891 
  3892 text {* Code for bounded quantification and summation over nats. *}
  3893 
  3894 lemma atMost_upto [code unfold]:
  3895   "{..n} = set [0..<Suc n]"
  3896 by auto
  3897 
  3898 lemma atLeast_upt [code unfold]:
  3899   "{..<n} = set [0..<n]"
  3900 by auto
  3901 
  3902 lemma greaterThanLessThan_upt [code unfold]:
  3903   "{n<..<m} = set [Suc n..<m]"
  3904 by auto
  3905 
  3906 lemma atLeastLessThan_upt [code unfold]:
  3907   "{n..<m} = set [n..<m]"
  3908 by auto
  3909 
  3910 lemma greaterThanAtMost_upt [code unfold]:
  3911   "{n<..m} = set [Suc n..<Suc m]"
  3912 by auto
  3913 
  3914 lemma atLeastAtMost_upt [code unfold]:
  3915   "{n..m} = set [n..<Suc m]"
  3916 by auto
  3917 
  3918 lemma all_nat_less_eq [code unfold]:
  3919   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
  3920 by auto
  3921 
  3922 lemma ex_nat_less_eq [code unfold]:
  3923   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
  3924 by auto
  3925 
  3926 lemma all_nat_less [code unfold]:
  3927   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
  3928 by auto
  3929 
  3930 lemma ex_nat_less [code unfold]:
  3931   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
  3932 by auto
  3933 
  3934 lemma setsum_set_distinct_conv_listsum:
  3935   "distinct xs \<Longrightarrow> setsum f (set xs) = listsum (map f xs)"
  3936 by (induct xs) simp_all
  3937 
  3938 lemma setsum_set_upt_conv_listsum [code unfold]:
  3939   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
  3940 by (rule setsum_set_distinct_conv_listsum) simp
  3941 
  3942 
  3943 text {* Code for summation over ints. *}
  3944 
  3945 lemma greaterThanLessThan_upto [code unfold]:
  3946   "{i<..<j::int} = set [i+1..j - 1]"
  3947 by auto
  3948 
  3949 lemma atLeastLessThan_upto [code unfold]:
  3950   "{i..<j::int} = set [i..j - 1]"
  3951 by auto
  3952 
  3953 lemma greaterThanAtMost_upto [code unfold]:
  3954   "{i<..j::int} = set [i+1..j]"
  3955 by auto
  3956 
  3957 lemma atLeastAtMost_upto [code unfold]:
  3958   "{i..j::int} = set [i..j]"
  3959 by auto
  3960 
  3961 lemma setsum_set_upto_conv_listsum [code unfold]:
  3962   "setsum f (set [i..j::int]) = listsum (map f [i..j])"
  3963 by (rule setsum_set_distinct_conv_listsum) simp
  3964 
  3965 end