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