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