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