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