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