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