src/HOL/List.thy
author bulwahn
Tue Aug 30 20:10:48 2011 +0200 (2011-08-30)
changeset 44619 fd520fa2fb09
parent 44618 f3635643a376
child 44635 3d046864ebe6
permissions -rw-r--r--
adding list_size_append (thanks to Rene Thiemann)
     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 fastsimp
   663 apply(case_tac zs)
   664  apply simp
   665 apply fastsimp
   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 fastsimp
  1001   next
  1002     assume "x \<noteq> a" thus ?case using Cons by(fastsimp 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 fastsimp
  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 fastsimp
  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 inj_Suc)
  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 inj_Suc)
  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 fastsimp
  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 add:last.simps)
  1533 
  1534 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"
  1535 by(simp add:last.simps)
  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 INFI_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 SUPR_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", standard]
  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 nth_upt)
  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 apply (frule nth_take_lemma [OF le_refl eq_imp_le])
  2651 apply (simp_all add: take_all)
  2652 done
  2653 
  2654 lemma map_nth:
  2655   "map (\<lambda>i. xs ! i) [0..<length xs] = xs"
  2656   by (rule nth_equalityI, auto)
  2657 
  2658 (* needs nth_equalityI *)
  2659 lemma list_all2_antisym:
  2660   "\<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> 
  2661   \<Longrightarrow> xs = ys"
  2662   apply (simp add: list_all2_conv_all_nth) 
  2663   apply (rule nth_equalityI, blast, simp)
  2664   done
  2665 
  2666 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"
  2667 -- {* The famous take-lemma. *}
  2668 apply (drule_tac x = "max (length xs) (length ys)" in spec)
  2669 apply (simp add: le_max_iff_disj take_all)
  2670 done
  2671 
  2672 
  2673 lemma take_Cons':
  2674      "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"
  2675 by (cases n) simp_all
  2676 
  2677 lemma drop_Cons':
  2678      "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"
  2679 by (cases n) simp_all
  2680 
  2681 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
  2682 by (cases n) simp_all
  2683 
  2684 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
  2685 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
  2686 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
  2687 
  2688 declare take_Cons_number_of [simp] 
  2689         drop_Cons_number_of [simp] 
  2690         nth_Cons_number_of [simp] 
  2691 
  2692 
  2693 subsubsection {* @{text upto}: interval-list on @{typ int} *}
  2694 
  2695 (* FIXME make upto tail recursive? *)
  2696 
  2697 function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where
  2698 "upto i j = (if i \<le> j then i # [i+1..j] else [])"
  2699 by auto
  2700 termination
  2701 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto
  2702 
  2703 declare upto.simps[code, simp del]
  2704 
  2705 lemmas upto_rec_number_of[simp] =
  2706   upto.simps[of "number_of m" "number_of n", standard]
  2707 
  2708 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
  2709 by(simp add: upto.simps)
  2710 
  2711 lemma set_upto[simp]: "set[i..j] = {i..j}"
  2712 proof(induct i j rule:upto.induct)
  2713   case (1 i j)
  2714   from this show ?case
  2715     unfolding upto.simps[of i j] simp_from_to[of i j] by auto
  2716 qed
  2717 
  2718 
  2719 subsubsection {* @{text "distinct"} and @{text remdups} *}
  2720 
  2721 lemma distinct_tl:
  2722   "distinct xs \<Longrightarrow> distinct (tl xs)"
  2723   by (cases xs) simp_all
  2724 
  2725 lemma distinct_append [simp]:
  2726 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"
  2727 by (induct xs) auto
  2728 
  2729 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"
  2730 by(induct xs) auto
  2731 
  2732 lemma set_remdups [simp]: "set (remdups xs) = set xs"
  2733 by (induct xs) (auto simp add: insert_absorb)
  2734 
  2735 lemma distinct_remdups [iff]: "distinct (remdups xs)"
  2736 by (induct xs) auto
  2737 
  2738 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"
  2739 by (induct xs, auto)
  2740 
  2741 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"
  2742 by (metis distinct_remdups distinct_remdups_id)
  2743 
  2744 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"
  2745 by (metis distinct_remdups finite_list set_remdups)
  2746 
  2747 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"
  2748 by (induct x, auto) 
  2749 
  2750 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"
  2751 by (induct x, auto)
  2752 
  2753 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"
  2754 by (induct xs) auto
  2755 
  2756 lemma length_remdups_eq[iff]:
  2757   "(length (remdups xs) = length xs) = (remdups xs = xs)"
  2758 apply(induct xs)
  2759  apply auto
  2760 apply(subgoal_tac "length (remdups xs) <= length xs")
  2761  apply arith
  2762 apply(rule length_remdups_leq)
  2763 done
  2764 
  2765 lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
  2766 apply(induct xs)
  2767 apply auto
  2768 done
  2769 
  2770 lemma distinct_map:
  2771   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
  2772 by (induct xs) auto
  2773 
  2774 
  2775 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
  2776 by (induct xs) auto
  2777 
  2778 lemma distinct_upt[simp]: "distinct[i..<j]"
  2779 by (induct j) auto
  2780 
  2781 lemma distinct_upto[simp]: "distinct[i..j]"
  2782 apply(induct i j rule:upto.induct)
  2783 apply(subst upto.simps)
  2784 apply(simp)
  2785 done
  2786 
  2787 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"
  2788 apply(induct xs arbitrary: i)
  2789  apply simp
  2790 apply (case_tac i)
  2791  apply simp_all
  2792 apply(blast dest:in_set_takeD)
  2793 done
  2794 
  2795 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"
  2796 apply(induct xs arbitrary: i)
  2797  apply simp
  2798 apply (case_tac i)
  2799  apply simp_all
  2800 done
  2801 
  2802 lemma distinct_list_update:
  2803 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"
  2804 shows "distinct (xs[i:=a])"
  2805 proof (cases "i < length xs")
  2806   case True
  2807   with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"
  2808     apply (drule_tac id_take_nth_drop) by simp
  2809   with d True show ?thesis
  2810     apply (simp add: upd_conv_take_nth_drop)
  2811     apply (drule subst [OF id_take_nth_drop]) apply assumption
  2812     apply simp apply (cases "a = xs!i") apply simp by blast
  2813 next
  2814   case False with d show ?thesis by auto
  2815 qed
  2816 
  2817 lemma distinct_concat:
  2818   assumes "distinct xs"
  2819   and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"
  2820   and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"
  2821   shows "distinct (concat xs)"
  2822   using assms by (induct xs) auto
  2823 
  2824 text {* It is best to avoid this indexed version of distinct, but
  2825 sometimes it is useful. *}
  2826 
  2827 lemma distinct_conv_nth:
  2828 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"
  2829 apply (induct xs, simp, simp)
  2830 apply (rule iffI, clarsimp)
  2831  apply (case_tac i)
  2832 apply (case_tac j, simp)
  2833 apply (simp add: set_conv_nth)
  2834  apply (case_tac j)
  2835 apply (clarsimp simp add: set_conv_nth, simp) 
  2836 apply (rule conjI)
  2837 (*TOO SLOW
  2838 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)
  2839 *)
  2840  apply (clarsimp simp add: set_conv_nth)
  2841  apply (erule_tac x = 0 in allE, simp)
  2842  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)
  2843 (*TOO SLOW
  2844 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)
  2845 *)
  2846 apply (erule_tac x = "Suc i" in allE, simp)
  2847 apply (erule_tac x = "Suc j" in allE, simp)
  2848 done
  2849 
  2850 lemma nth_eq_iff_index_eq:
  2851  "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
  2852 by(auto simp: distinct_conv_nth)
  2853 
  2854 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
  2855 by (induct xs) auto
  2856 
  2857 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"
  2858 proof (induct xs)
  2859   case Nil thus ?case by simp
  2860 next
  2861   case (Cons x xs)
  2862   show ?case
  2863   proof (cases "x \<in> set xs")
  2864     case False with Cons show ?thesis by simp
  2865   next
  2866     case True with Cons.prems
  2867     have "card (set xs) = Suc (length xs)" 
  2868       by (simp add: card_insert_if split: split_if_asm)
  2869     moreover have "card (set xs) \<le> length xs" by (rule card_length)
  2870     ultimately have False by simp
  2871     thus ?thesis ..
  2872   qed
  2873 qed
  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: set_concat 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 
  2933 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}
  2934 
  2935 lemma (in monoid_add) listsum_foldl [code]:
  2936   "listsum = foldl (op +) 0"
  2937   by (simp add: listsum_def foldl_foldr1 fun_eq_iff)
  2938 
  2939 lemma (in monoid_add) listsum_simps [simp]:
  2940   "listsum [] = 0"
  2941   "listsum (x#xs) = x + listsum xs"
  2942   by (simp_all add: listsum_def)
  2943 
  2944 lemma (in monoid_add) listsum_append [simp]:
  2945   "listsum (xs @ ys) = listsum xs + listsum ys"
  2946   by (induct xs) (simp_all add: add.assoc)
  2947 
  2948 lemma (in comm_monoid_add) listsum_rev [simp]:
  2949   "listsum (rev xs) = listsum xs"
  2950   by (simp add: listsum_def [of "rev xs"]) (simp add: listsum_foldl foldr_foldl add.commute)
  2951 
  2952 lemma (in comm_monoid_add) listsum_map_remove1:
  2953   "x \<in> set xs \<Longrightarrow> listsum (map f xs) = f x + listsum (map f (remove1 x xs))"
  2954   by (induct xs) (auto simp add: ac_simps)
  2955 
  2956 lemma (in monoid_add) list_size_conv_listsum:
  2957   "list_size f xs = listsum (map f xs) + size xs"
  2958   by (induct xs) auto
  2959 
  2960 lemma (in monoid_add) length_concat:
  2961   "length (concat xss) = listsum (map length xss)"
  2962   by (induct xss) simp_all
  2963 
  2964 lemma (in monoid_add) listsum_map_filter:
  2965   assumes "\<And>x. x \<in> set xs \<Longrightarrow> \<not> P x \<Longrightarrow> f x = 0"
  2966   shows "listsum (map f (filter P xs)) = listsum (map f xs)"
  2967   using assms by (induct xs) auto
  2968 
  2969 lemma (in monoid_add) distinct_listsum_conv_Setsum:
  2970   "distinct xs \<Longrightarrow> listsum xs = Setsum (set xs)"
  2971   by (induct xs) simp_all
  2972 
  2973 lemma listsum_eq_0_nat_iff_nat [simp]:
  2974   "listsum ns = (0::nat) \<longleftrightarrow> (\<forall>n \<in> set ns. n = 0)"
  2975   by (simp add: listsum_foldl)
  2976 
  2977 lemma elem_le_listsum_nat:
  2978   "k < size ns \<Longrightarrow> ns ! k \<le> listsum (ns::nat list)"
  2979 apply(induct ns arbitrary: k)
  2980  apply simp
  2981 apply(fastsimp simp add:nth_Cons split: nat.split)
  2982 done
  2983 
  2984 lemma listsum_update_nat:
  2985   "k<size ns \<Longrightarrow> listsum (ns[k := (n::nat)]) = listsum ns + n - ns ! k"
  2986 apply(induct ns arbitrary:k)
  2987  apply (auto split:nat.split)
  2988 apply(drule elem_le_listsum_nat)
  2989 apply arith
  2990 done
  2991 
  2992 text{* Some syntactic sugar for summing a function over a list: *}
  2993 
  2994 syntax
  2995   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
  2996 syntax (xsymbols)
  2997   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  2998 syntax (HTML output)
  2999   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
  3000 
  3001 translations -- {* Beware of argument permutation! *}
  3002   "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
  3003   "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
  3004 
  3005 lemma (in monoid_add) listsum_triv:
  3006   "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"
  3007   by (induct xs) (simp_all add: left_distrib)
  3008 
  3009 lemma (in monoid_add) listsum_0 [simp]:
  3010   "(\<Sum>x\<leftarrow>xs. 0) = 0"
  3011   by (induct xs) (simp_all add: left_distrib)
  3012 
  3013 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}
  3014 lemma (in ab_group_add) uminus_listsum_map:
  3015   "- listsum (map f xs) = listsum (map (uminus \<circ> f) xs)"
  3016   by (induct xs) simp_all
  3017 
  3018 lemma (in comm_monoid_add) listsum_addf:
  3019   "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"
  3020   by (induct xs) (simp_all add: algebra_simps)
  3021 
  3022 lemma (in ab_group_add) listsum_subtractf:
  3023   "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"
  3024   by (induct xs) (simp_all add: algebra_simps)
  3025 
  3026 lemma (in semiring_0) listsum_const_mult:
  3027   "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"
  3028   by (induct xs) (simp_all add: algebra_simps)
  3029 
  3030 lemma (in semiring_0) listsum_mult_const:
  3031   "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"
  3032   by (induct xs) (simp_all add: algebra_simps)
  3033 
  3034 lemma (in ordered_ab_group_add_abs) listsum_abs:
  3035   "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"
  3036   by (induct xs) (simp_all add: order_trans [OF abs_triangle_ineq])
  3037 
  3038 lemma listsum_mono:
  3039   fixes f g :: "'a \<Rightarrow> 'b::{monoid_add, ordered_ab_semigroup_add}"
  3040   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)"
  3041   by (induct xs) (simp, simp add: add_mono)
  3042 
  3043 lemma (in monoid_add) listsum_distinct_conv_setsum_set:
  3044   "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"
  3045   by (induct xs) simp_all
  3046 
  3047 lemma (in monoid_add) interv_listsum_conv_setsum_set_nat:
  3048   "listsum (map f [m..<n]) = setsum f (set [m..<n])"
  3049   by (simp add: listsum_distinct_conv_setsum_set)
  3050 
  3051 lemma (in monoid_add) interv_listsum_conv_setsum_set_int:
  3052   "listsum (map f [k..l]) = setsum f (set [k..l])"
  3053   by (simp add: listsum_distinct_conv_setsum_set)
  3054 
  3055 text {* General equivalence between @{const listsum} and @{const setsum} *}
  3056 lemma (in monoid_add) listsum_setsum_nth:
  3057   "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"
  3058   using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)
  3059 
  3060 
  3061 subsubsection {* @{const insert} *}
  3062 
  3063 lemma in_set_insert [simp]:
  3064   "x \<in> set xs \<Longrightarrow> List.insert x xs = xs"
  3065   by (simp add: List.insert_def)
  3066 
  3067 lemma not_in_set_insert [simp]:
  3068   "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs"
  3069   by (simp add: List.insert_def)
  3070 
  3071 lemma insert_Nil [simp]:
  3072   "List.insert x [] = [x]"
  3073   by simp
  3074 
  3075 lemma set_insert [simp]:
  3076   "set (List.insert x xs) = insert x (set xs)"
  3077   by (auto simp add: List.insert_def)
  3078 
  3079 lemma distinct_insert [simp]:
  3080   "distinct xs \<Longrightarrow> distinct (List.insert x xs)"
  3081   by (simp add: List.insert_def)
  3082 
  3083 lemma insert_remdups:
  3084   "List.insert x (remdups xs) = remdups (List.insert x xs)"
  3085   by (simp add: List.insert_def)
  3086 
  3087 
  3088 subsubsection {* @{text remove1} *}
  3089 
  3090 lemma remove1_append:
  3091   "remove1 x (xs @ ys) =
  3092   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"
  3093 by (induct xs) auto
  3094 
  3095 lemma remove1_commute: "remove1 x (remove1 y zs) = remove1 y (remove1 x zs)"
  3096 by (induct zs) auto
  3097 
  3098 lemma in_set_remove1[simp]:
  3099   "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"
  3100 apply (induct xs)
  3101 apply auto
  3102 done
  3103 
  3104 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"
  3105 apply(induct xs)
  3106  apply simp
  3107 apply simp
  3108 apply blast
  3109 done
  3110 
  3111 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"
  3112 apply(induct xs)
  3113  apply simp
  3114 apply simp
  3115 apply blast
  3116 done
  3117 
  3118 lemma length_remove1:
  3119   "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"
  3120 apply (induct xs)
  3121  apply (auto dest!:length_pos_if_in_set)
  3122 done
  3123 
  3124 lemma remove1_filter_not[simp]:
  3125   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"
  3126 by(induct xs) auto
  3127 
  3128 lemma filter_remove1:
  3129   "filter Q (remove1 x xs) = remove1 x (filter Q xs)"
  3130 by (induct xs) auto
  3131 
  3132 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"
  3133 apply(insert set_remove1_subset)
  3134 apply fast
  3135 done
  3136 
  3137 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"
  3138 by (induct xs) simp_all
  3139 
  3140 lemma remove1_remdups:
  3141   "distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"
  3142   by (induct xs) simp_all
  3143 
  3144 lemma remove1_idem:
  3145   assumes "x \<notin> set xs"
  3146   shows "remove1 x xs = xs"
  3147   using assms by (induct xs) simp_all
  3148 
  3149 
  3150 subsubsection {* @{text removeAll} *}
  3151 
  3152 lemma removeAll_filter_not_eq:
  3153   "removeAll x = filter (\<lambda>y. x \<noteq> y)"
  3154 proof
  3155   fix xs
  3156   show "removeAll x xs = filter (\<lambda>y. x \<noteq> y) xs"
  3157     by (induct xs) auto
  3158 qed
  3159 
  3160 lemma removeAll_append[simp]:
  3161   "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"
  3162 by (induct xs) auto
  3163 
  3164 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"
  3165 by (induct xs) auto
  3166 
  3167 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"
  3168 by (induct xs) auto
  3169 
  3170 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat
  3171 lemma length_removeAll:
  3172   "length(removeAll x xs) = length xs - count x xs"
  3173 *)
  3174 
  3175 lemma removeAll_filter_not[simp]:
  3176   "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"
  3177 by(induct xs) auto
  3178 
  3179 lemma distinct_removeAll:
  3180   "distinct xs \<Longrightarrow> distinct (removeAll x xs)"
  3181   by (simp add: removeAll_filter_not_eq)
  3182 
  3183 lemma distinct_remove1_removeAll:
  3184   "distinct xs ==> remove1 x xs = removeAll x xs"
  3185 by (induct xs) simp_all
  3186 
  3187 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>
  3188   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  3189 by (induct xs) (simp_all add:inj_on_def)
  3190 
  3191 lemma map_removeAll_inj: "inj f \<Longrightarrow>
  3192   map f (removeAll x xs) = removeAll (f x) (map f xs)"
  3193 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)
  3194 
  3195 
  3196 subsubsection {* @{text replicate} *}
  3197 
  3198 lemma length_replicate [simp]: "length (replicate n x) = n"
  3199 by (induct n) auto
  3200 
  3201 lemma Ex_list_of_length: "\<exists>xs. length xs = n"
  3202 by (rule exI[of _ "replicate n undefined"]) simp
  3203 
  3204 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"
  3205 by (induct n) auto
  3206 
  3207 lemma map_replicate_const:
  3208   "map (\<lambda> x. k) lst = replicate (length lst) k"
  3209   by (induct lst) auto
  3210 
  3211 lemma replicate_app_Cons_same:
  3212 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"
  3213 by (induct n) auto
  3214 
  3215 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"
  3216 apply (induct n, simp)
  3217 apply (simp add: replicate_app_Cons_same)
  3218 done
  3219 
  3220 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"
  3221 by (induct n) auto
  3222 
  3223 text{* Courtesy of Matthias Daum: *}
  3224 lemma append_replicate_commute:
  3225   "replicate n x @ replicate k x = replicate k x @ replicate n x"
  3226 apply (simp add: replicate_add [THEN sym])
  3227 apply (simp add: add_commute)
  3228 done
  3229 
  3230 text{* Courtesy of Andreas Lochbihler: *}
  3231 lemma filter_replicate:
  3232   "filter P (replicate n x) = (if P x then replicate n x else [])"
  3233 by(induct n) auto
  3234 
  3235 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"
  3236 by (induct n) auto
  3237 
  3238 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"
  3239 by (induct n) auto
  3240 
  3241 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"
  3242 by (atomize (full), induct n) auto
  3243 
  3244 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"
  3245 apply (induct n arbitrary: i, simp)
  3246 apply (simp add: nth_Cons split: nat.split)
  3247 done
  3248 
  3249 text{* Courtesy of Matthias Daum (2 lemmas): *}
  3250 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"
  3251 apply (case_tac "k \<le> i")
  3252  apply  (simp add: min_def)
  3253 apply (drule not_leE)
  3254 apply (simp add: min_def)
  3255 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")
  3256  apply  simp
  3257 apply (simp add: replicate_add [symmetric])
  3258 done
  3259 
  3260 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"
  3261 apply (induct k arbitrary: i)
  3262  apply simp
  3263 apply clarsimp
  3264 apply (case_tac i)
  3265  apply simp
  3266 apply clarsimp
  3267 done
  3268 
  3269 
  3270 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"
  3271 by (induct n) auto
  3272 
  3273 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"
  3274 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
  3275 
  3276 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"
  3277 by auto
  3278 
  3279 lemma in_set_replicate[simp]: "(x : set (replicate n y)) = (x = y & n \<noteq> 0)"
  3280 by (simp add: set_replicate_conv_if)
  3281 
  3282 lemma Ball_set_replicate[simp]:
  3283   "(ALL x : set(replicate n a). P x) = (P a | n=0)"
  3284 by(simp add: set_replicate_conv_if)
  3285 
  3286 lemma Bex_set_replicate[simp]:
  3287   "(EX x : set(replicate n a). P x) = (P a & n\<noteq>0)"
  3288 by(simp add: set_replicate_conv_if)
  3289 
  3290 lemma replicate_append_same:
  3291   "replicate i x @ [x] = x # replicate i x"
  3292   by (induct i) simp_all
  3293 
  3294 lemma map_replicate_trivial:
  3295   "map (\<lambda>i. x) [0..<i] = replicate i x"
  3296   by (induct i) (simp_all add: replicate_append_same)
  3297 
  3298 lemma concat_replicate_trivial[simp]:
  3299   "concat (replicate i []) = []"
  3300   by (induct i) (auto simp add: map_replicate_const)
  3301 
  3302 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"
  3303 by (induct n) auto
  3304 
  3305 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"
  3306 by (induct n) auto
  3307 
  3308 lemma replicate_eq_replicate[simp]:
  3309   "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"
  3310 apply(induct m arbitrary: n)
  3311  apply simp
  3312 apply(induct_tac n)
  3313 apply auto
  3314 done
  3315 
  3316 lemma replicate_length_filter:
  3317   "replicate (length (filter (\<lambda>y. x = y) xs)) x = filter (\<lambda>y. x = y) xs"
  3318   by (induct xs) auto
  3319 
  3320 lemma comm_append_are_replicate:
  3321   fixes xs ys :: "'a list"
  3322   assumes "xs \<noteq> []" "ys \<noteq> []"
  3323   assumes "xs @ ys = ys @ xs"
  3324   shows "\<exists>m n zs. concat (replicate m zs) = xs \<and> concat (replicate n zs) = ys"
  3325   using assms
  3326 proof (induct "length (xs @ ys)" arbitrary: xs ys rule: less_induct)
  3327   case less
  3328 
  3329   def xs' \<equiv> "if (length xs \<le> length ys) then xs else ys"
  3330     and ys' \<equiv> "if (length xs \<le> length ys) then ys else xs"
  3331   then have
  3332     prems': "length xs' \<le> length ys'"
  3333             "xs' @ ys' = ys' @ xs'"
  3334       and "xs' \<noteq> []"
  3335       and len: "length (xs @ ys) = length (xs' @ ys')"
  3336     using less by (auto intro: less.hyps)
  3337 
  3338   from prems'
  3339   obtain ws where "ys' = xs' @ ws"
  3340     by (auto simp: append_eq_append_conv2)
  3341 
  3342   have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ys'"
  3343   proof (cases "ws = []")
  3344     case True
  3345     then have "concat (replicate 1 xs') = xs'"
  3346       and "concat (replicate 1 xs') = ys'"
  3347       using `ys' = xs' @ ws` by auto
  3348     then show ?thesis by blast
  3349   next
  3350     case False
  3351     from `ys' = xs' @ ws` and `xs' @ ys' = ys' @ xs'`
  3352     have "xs' @ ws = ws @ xs'" by simp
  3353     then have "\<exists>m n zs. concat (replicate m zs) = xs' \<and> concat (replicate n zs) = ws"
  3354       using False and `xs' \<noteq> []` and `ys' = xs' @ ws` and len
  3355       by (intro less.hyps) auto
  3356     then obtain m n zs where "concat (replicate m zs) = xs'"
  3357       and "concat (replicate n zs) = ws" by blast
  3358     moreover
  3359     then have "concat (replicate (m + n) zs) = ys'"
  3360       using `ys' = xs' @ ws`
  3361       by (simp add: replicate_add)
  3362     ultimately
  3363     show ?thesis by blast
  3364   qed
  3365   then show ?case
  3366     using xs'_def ys'_def by metis
  3367 qed
  3368 
  3369 lemma comm_append_is_replicate:
  3370   fixes xs ys :: "'a list"
  3371   assumes "xs \<noteq> []" "ys \<noteq> []"
  3372   assumes "xs @ ys = ys @ xs"
  3373   shows "\<exists>n zs. n > 1 \<and> concat (replicate n zs) = xs @ ys"
  3374 
  3375 proof -
  3376   obtain m n zs where "concat (replicate m zs) = xs"
  3377     and "concat (replicate n zs) = ys"
  3378     using assms by (metis comm_append_are_replicate)
  3379   then have "m + n > 1" and "concat (replicate (m+n) zs) = xs @ ys"
  3380     using `xs \<noteq> []` and `ys \<noteq> []`
  3381     by (auto simp: replicate_add)
  3382   then show ?thesis by blast
  3383 qed
  3384 
  3385 
  3386 subsubsection{*@{text rotate1} and @{text rotate}*}
  3387 
  3388 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"
  3389 by(simp add:rotate1_def)
  3390 
  3391 lemma rotate0[simp]: "rotate 0 = id"
  3392 by(simp add:rotate_def)
  3393 
  3394 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"
  3395 by(simp add:rotate_def)
  3396 
  3397 lemma rotate_add:
  3398   "rotate (m+n) = rotate m o rotate n"
  3399 by(simp add:rotate_def funpow_add)
  3400 
  3401 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"
  3402 by(simp add:rotate_add)
  3403 
  3404 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"
  3405 by(simp add:rotate_def funpow_swap1)
  3406 
  3407 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"
  3408 by(cases xs) simp_all
  3409 
  3410 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"
  3411 apply(induct n)
  3412  apply simp
  3413 apply (simp add:rotate_def)
  3414 done
  3415 
  3416 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"
  3417 by(simp add:rotate1_def split:list.split)
  3418 
  3419 lemma rotate_drop_take:
  3420   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"
  3421 apply(induct n)
  3422  apply simp
  3423 apply(simp add:rotate_def)
  3424 apply(cases "xs = []")
  3425  apply (simp)
  3426 apply(case_tac "n mod length xs = 0")
  3427  apply(simp add:mod_Suc)
  3428  apply(simp add: rotate1_hd_tl drop_Suc take_Suc)
  3429 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]
  3430                 take_hd_drop linorder_not_le)
  3431 done
  3432 
  3433 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"
  3434 by(simp add:rotate_drop_take)
  3435 
  3436 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"
  3437 by(simp add:rotate_drop_take)
  3438 
  3439 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"
  3440 by(simp add:rotate1_def split:list.split)
  3441 
  3442 lemma length_rotate[simp]: "length(rotate n xs) = length xs"
  3443 by (induct n arbitrary: xs) (simp_all add:rotate_def)
  3444 
  3445 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"
  3446 by(simp add:rotate1_def split:list.split) blast
  3447 
  3448 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"
  3449 by (induct n) (simp_all add:rotate_def)
  3450 
  3451 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"
  3452 by(simp add:rotate_drop_take take_map drop_map)
  3453 
  3454 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"
  3455 by (cases xs) (auto simp add:rotate1_def)
  3456 
  3457 lemma set_rotate[simp]: "set(rotate n xs) = set xs"
  3458 by (induct n) (simp_all add:rotate_def)
  3459 
  3460 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"
  3461 by(simp add:rotate1_def split:list.split)
  3462 
  3463 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"
  3464 by (induct n) (simp_all add:rotate_def)
  3465 
  3466 lemma rotate_rev:
  3467   "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
  3468 apply(simp add:rotate_drop_take rev_drop rev_take)
  3469 apply(cases "length xs = 0")
  3470  apply simp
  3471 apply(cases "n mod length xs = 0")
  3472  apply simp
  3473 apply(simp add:rotate_drop_take rev_drop rev_take)
  3474 done
  3475 
  3476 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
  3477 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
  3478 apply(subgoal_tac "length xs \<noteq> 0")
  3479  prefer 2 apply simp
  3480 using mod_less_divisor[of "length xs" n] by arith
  3481 
  3482 
  3483 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}
  3484 
  3485 lemma sublist_empty [simp]: "sublist xs {} = []"
  3486 by (auto simp add: sublist_def)
  3487 
  3488 lemma sublist_nil [simp]: "sublist [] A = []"
  3489 by (auto simp add: sublist_def)
  3490 
  3491 lemma length_sublist:
  3492   "length(sublist xs I) = card{i. i < length xs \<and> i : I}"
  3493 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)
  3494 
  3495 lemma sublist_shift_lemma_Suc:
  3496   "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =
  3497    map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"
  3498 apply(induct xs arbitrary: "is")
  3499  apply simp
  3500 apply (case_tac "is")
  3501  apply simp
  3502 apply simp
  3503 done
  3504 
  3505 lemma sublist_shift_lemma:
  3506      "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =
  3507       map fst [p<-zip xs [0..<length xs] . snd p + i : A]"
  3508 by (induct xs rule: rev_induct) (simp_all add: add_commute)
  3509 
  3510 lemma sublist_append:
  3511      "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"
  3512 apply (unfold sublist_def)
  3513 apply (induct l' rule: rev_induct, simp)
  3514 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
  3515 apply (simp add: add_commute)
  3516 done
  3517 
  3518 lemma sublist_Cons:
  3519 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
  3520 apply (induct l rule: rev_induct)
  3521  apply (simp add: sublist_def)
  3522 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)
  3523 done
  3524 
  3525 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"
  3526 apply(induct xs arbitrary: I)
  3527 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)
  3528 done
  3529 
  3530 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"
  3531 by(auto simp add:set_sublist)
  3532 
  3533 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"
  3534 by(auto simp add:set_sublist)
  3535 
  3536 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"
  3537 by(auto simp add:set_sublist)
  3538 
  3539 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"
  3540 by (simp add: sublist_Cons)
  3541 
  3542 
  3543 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"
  3544 apply(induct xs arbitrary: I)
  3545  apply simp
  3546 apply(auto simp add:sublist_Cons)
  3547 done
  3548 
  3549 
  3550 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"
  3551 apply (induct l rule: rev_induct, simp)
  3552 apply (simp split: nat_diff_split add: sublist_append)
  3553 done
  3554 
  3555 lemma filter_in_sublist:
  3556  "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"
  3557 proof (induct xs arbitrary: s)
  3558   case Nil thus ?case by simp
  3559 next
  3560   case (Cons a xs)
  3561   moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto
  3562   ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)
  3563 qed
  3564 
  3565 
  3566 subsubsection {* @{const splice} *}
  3567 
  3568 lemma splice_Nil2 [simp, code]: "splice xs [] = xs"
  3569 by (cases xs) simp_all
  3570 
  3571 declare splice.simps(1,3)[code]
  3572 declare splice.simps(2)[simp del]
  3573 
  3574 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"
  3575 by (induct xs ys rule: splice.induct) auto
  3576 
  3577 
  3578 subsubsection {* Transpose *}
  3579 
  3580 function transpose where
  3581 "transpose []             = []" |
  3582 "transpose ([]     # xss) = transpose xss" |
  3583 "transpose ((x#xs) # xss) =
  3584   (x # [h. (h#t) \<leftarrow> xss]) # transpose (xs # [t. (h#t) \<leftarrow> xss])"
  3585 by pat_completeness auto
  3586 
  3587 lemma transpose_aux_filter_head:
  3588   "concat (map (list_case [] (\<lambda>h t. [h])) xss) =
  3589   map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"
  3590   by (induct xss) (auto split: list.split)
  3591 
  3592 lemma transpose_aux_filter_tail:
  3593   "concat (map (list_case [] (\<lambda>h t. [t])) xss) =
  3594   map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"
  3595   by (induct xss) (auto split: list.split)
  3596 
  3597 lemma transpose_aux_max:
  3598   "max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =
  3599   Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"
  3600   (is "max _ ?foldB = Suc (max _ ?foldA)")
  3601 proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")
  3602   case True
  3603   hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"
  3604   proof (induct xss)
  3605     case (Cons x xs)
  3606     moreover hence "x = []" by (cases x) auto
  3607     ultimately show ?case by auto
  3608   qed simp
  3609   thus ?thesis using True by simp
  3610 next
  3611   case False
  3612 
  3613   have foldA: "?foldA = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"
  3614     by (induct xss) auto
  3615   have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"
  3616     by (induct xss) auto
  3617 
  3618   have "0 < ?foldB"
  3619   proof -
  3620     from False
  3621     obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)
  3622     hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto
  3623     hence "z \<noteq> []" by auto
  3624     thus ?thesis
  3625       unfolding foldB zs
  3626       by (auto simp: max_def intro: less_le_trans)
  3627   qed
  3628   thus ?thesis
  3629     unfolding foldA foldB max_Suc_Suc[symmetric]
  3630     by simp
  3631 qed
  3632 
  3633 termination transpose
  3634   by (relation "measure (\<lambda>xs. foldr (\<lambda>xs. max (length xs)) xs 0 + length xs)")
  3635      (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max less_Suc_eq_le)
  3636 
  3637 lemma transpose_empty: "(transpose xs = []) \<longleftrightarrow> (\<forall>x \<in> set xs. x = [])"
  3638   by (induct rule: transpose.induct) simp_all
  3639 
  3640 lemma length_transpose:
  3641   fixes xs :: "'a list list"
  3642   shows "length (transpose xs) = foldr (\<lambda>xs. max (length xs)) xs 0"
  3643   by (induct rule: transpose.induct)
  3644     (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max
  3645                 max_Suc_Suc[symmetric] simp del: max_Suc_Suc)
  3646 
  3647 lemma nth_transpose:
  3648   fixes xs :: "'a list list"
  3649   assumes "i < length (transpose xs)"
  3650   shows "transpose xs ! i = map (\<lambda>xs. xs ! i) [ys \<leftarrow> xs. i < length ys]"
  3651 using assms proof (induct arbitrary: i rule: transpose.induct)
  3652   case (3 x xs xss)
  3653   def XS == "(x # xs) # xss"
  3654   hence [simp]: "XS \<noteq> []" by auto
  3655   thus ?case
  3656   proof (cases i)
  3657     case 0
  3658     thus ?thesis by (simp add: transpose_aux_filter_head hd_conv_nth)
  3659   next
  3660     case (Suc j)
  3661     have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp
  3662     have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp
  3663     { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"
  3664       by (cases x) simp_all
  3665     } note *** = this
  3666 
  3667     have j_less: "j < length (transpose (xs # concat (map (list_case [] (\<lambda>h t. [t])) xss)))"
  3668       using "3.prems" by (simp add: transpose_aux_filter_tail length_transpose Suc)
  3669 
  3670     show ?thesis
  3671       unfolding transpose.simps `i = Suc j` nth_Cons_Suc "3.hyps"[OF j_less]
  3672       apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])
  3673       apply (rule_tac y=x in list.exhaust)
  3674       by auto
  3675   qed
  3676 qed simp_all
  3677 
  3678 lemma transpose_map_map:
  3679   "transpose (map (map f) xs) = map (map f) (transpose xs)"
  3680 proof (rule nth_equalityI, safe)
  3681   have [simp]: "length (transpose (map (map f) xs)) = length (transpose xs)"
  3682     by (simp add: length_transpose foldr_map comp_def)
  3683   show "length (transpose (map (map f) xs)) = length (map (map f) (transpose xs))" by simp
  3684 
  3685   fix i assume "i < length (transpose (map (map f) xs))"
  3686   thus "transpose (map (map f) xs) ! i = map (map f) (transpose xs) ! i"
  3687     by (simp add: nth_transpose filter_map comp_def)
  3688 qed
  3689 
  3690 
  3691 subsubsection {* (In)finiteness *}
  3692 
  3693 lemma finite_maxlen:
  3694   "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"
  3695 proof (induct rule: finite.induct)
  3696   case emptyI show ?case by simp
  3697 next
  3698   case (insertI M xs)
  3699   then obtain n where "\<forall>s\<in>M. length s < n" by blast
  3700   hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto
  3701   thus ?case ..
  3702 qed
  3703 
  3704 lemma finite_lists_length_eq:
  3705 assumes "finite A"
  3706 shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")
  3707 proof(induct n)
  3708   case 0 show ?case by simp
  3709 next
  3710   case (Suc n)
  3711   have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs) ` ?S n)"
  3712     by (auto simp:length_Suc_conv)
  3713   then show ?case using `finite A`
  3714     by (auto intro: Suc) (* FIXME metis? *)
  3715 qed
  3716 
  3717 lemma finite_lists_length_le:
  3718   assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"
  3719  (is "finite ?S")
  3720 proof-
  3721   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto
  3722   thus ?thesis by (auto intro: finite_lists_length_eq[OF `finite A`])
  3723 qed
  3724 
  3725 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"
  3726 apply(rule notI)
  3727 apply(drule finite_maxlen)
  3728 apply (metis UNIV_I length_replicate less_not_refl)
  3729 done
  3730 
  3731 
  3732 subsection {* Sorting *}
  3733 
  3734 text{* Currently it is not shown that @{const sort} returns a
  3735 permutation of its input because the nicest proof is via multisets,
  3736 which are not yet available. Alternatively one could define a function
  3737 that counts the number of occurrences of an element in a list and use
  3738 that instead of multisets to state the correctness property. *}
  3739 
  3740 context linorder
  3741 begin
  3742 
  3743 lemma length_insort [simp]:
  3744   "length (insort_key f x xs) = Suc (length xs)"
  3745   by (induct xs) simp_all
  3746 
  3747 lemma insort_key_left_comm:
  3748   assumes "f x \<noteq> f y"
  3749   shows "insort_key f y (insort_key f x xs) = insort_key f x (insort_key f y xs)"
  3750   by (induct xs) (auto simp add: assms dest: antisym)
  3751 
  3752 lemma insort_left_comm:
  3753   "insort x (insort y xs) = insort y (insort x xs)"
  3754   by (cases "x = y") (auto intro: insort_key_left_comm)
  3755 
  3756 lemma comp_fun_commute_insort:
  3757   "comp_fun_commute insort"
  3758 proof
  3759 qed (simp add: insort_left_comm fun_eq_iff)
  3760 
  3761 lemma sort_key_simps [simp]:
  3762   "sort_key f [] = []"
  3763   "sort_key f (x#xs) = insort_key f x (sort_key f xs)"
  3764   by (simp_all add: sort_key_def)
  3765 
  3766 lemma sort_foldl_insort:
  3767   "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"
  3768   by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)
  3769 
  3770 lemma length_sort[simp]: "length (sort_key f xs) = length xs"
  3771 by (induct xs, auto)
  3772 
  3773 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"
  3774 apply(induct xs arbitrary: x) apply simp
  3775 by simp (blast intro: order_trans)
  3776 
  3777 lemma sorted_tl:
  3778   "sorted xs \<Longrightarrow> sorted (tl xs)"
  3779   by (cases xs) (simp_all add: sorted_Cons)
  3780 
  3781 lemma sorted_append:
  3782   "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"
  3783 by (induct xs) (auto simp add:sorted_Cons)
  3784 
  3785 lemma sorted_nth_mono:
  3786   "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"
  3787 by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)
  3788 
  3789 lemma sorted_rev_nth_mono:
  3790   "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"
  3791 using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
  3792       rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
  3793 by auto
  3794 
  3795 lemma sorted_nth_monoI:
  3796   "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
  3797 proof (induct xs)
  3798   case (Cons x xs)
  3799   have "sorted xs"
  3800   proof (rule Cons.hyps)
  3801     fix i j assume "i \<le> j" and "j < length xs"
  3802     with Cons.prems[of "Suc i" "Suc j"]
  3803     show "xs ! i \<le> xs ! j" by auto
  3804   qed
  3805   moreover
  3806   {
  3807     fix y assume "y \<in> set xs"
  3808     then obtain j where "j < length xs" and "xs ! j = y"
  3809       unfolding in_set_conv_nth by blast
  3810     with Cons.prems[of 0 "Suc j"]
  3811     have "x \<le> y"
  3812       by auto
  3813   }
  3814   ultimately
  3815   show ?case
  3816     unfolding sorted_Cons by auto
  3817 qed simp
  3818 
  3819 lemma sorted_equals_nth_mono:
  3820   "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
  3821 by (auto intro: sorted_nth_monoI sorted_nth_mono)
  3822 
  3823 lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"
  3824 by (induct xs) auto
  3825 
  3826 lemma set_sort[simp]: "set(sort_key f xs) = set xs"
  3827 by (induct xs) (simp_all add:set_insort)
  3828 
  3829 lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"
  3830 by(induct xs)(auto simp:set_insort)
  3831 
  3832 lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"
  3833 by(induct xs)(simp_all add:distinct_insort set_sort)
  3834 
  3835 lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"
  3836   by (induct xs) (auto simp:sorted_Cons set_insort)
  3837 
  3838 lemma sorted_insort: "sorted (insort x xs) = sorted xs"
  3839   using sorted_insort_key [where f="\<lambda>x. x"] by simp
  3840 
  3841 theorem sorted_sort_key [simp]: "sorted (map f (sort_key f xs))"
  3842   by (induct xs) (auto simp:sorted_insort_key)
  3843 
  3844 theorem sorted_sort [simp]: "sorted (sort xs)"
  3845   using sorted_sort_key [where f="\<lambda>x. x"] by simp
  3846 
  3847 lemma sorted_butlast:
  3848   assumes "xs \<noteq> []" and "sorted xs"
  3849   shows "sorted (butlast xs)"
  3850 proof -
  3851   from `xs \<noteq> []` obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto
  3852   with `sorted xs` show ?thesis by (simp add: sorted_append)
  3853 qed
  3854   
  3855 lemma insort_not_Nil [simp]:
  3856   "insort_key f a xs \<noteq> []"
  3857   by (induct xs) simp_all
  3858 
  3859 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"
  3860 by (cases xs) auto
  3861 
  3862 lemma sorted_map_remove1:
  3863   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
  3864   by (induct xs) (auto simp add: sorted_Cons)
  3865 
  3866 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"
  3867   using sorted_map_remove1 [of "\<lambda>x. x"] by simp
  3868 
  3869 lemma insort_key_remove1:
  3870   assumes "a \<in> set xs" and "sorted (map f xs)" and "hd (filter (\<lambda>x. f a = f x) xs) = a"
  3871   shows "insort_key f a (remove1 a xs) = xs"
  3872 using assms proof (induct xs)
  3873   case (Cons x xs)
  3874   then show ?case
  3875   proof (cases "x = a")
  3876     case False
  3877     then have "f x \<noteq> f a" using Cons.prems by auto
  3878     then have "f x < f a" using Cons.prems by (auto simp: sorted_Cons)
  3879     with `f x \<noteq> f a` show ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)
  3880   qed (auto simp: sorted_Cons insort_is_Cons)
  3881 qed simp
  3882 
  3883 lemma insort_remove1:
  3884   assumes "a \<in> set xs" and "sorted xs"
  3885   shows "insort a (remove1 a xs) = xs"
  3886 proof (rule insort_key_remove1)
  3887   from `a \<in> set xs` show "a \<in> set xs" .
  3888   from `sorted xs` show "sorted (map (\<lambda>x. x) xs)" by simp
  3889   from `a \<in> set xs` have "a \<in> set (filter (op = a) xs)" by auto
  3890   then have "set (filter (op = a) xs) \<noteq> {}" by auto
  3891   then have "filter (op = a) xs \<noteq> []" by (auto simp only: set_empty)
  3892   then have "length (filter (op = a) xs) > 0" by simp
  3893   then obtain n where n: "Suc n = length (filter (op = a) xs)"
  3894     by (cases "length (filter (op = a) xs)") simp_all
  3895   moreover have "replicate (Suc n) a = a # replicate n a"
  3896     by simp
  3897   ultimately show "hd (filter (op = a) xs) = a" by (simp add: replicate_length_filter)
  3898 qed
  3899 
  3900 lemma sorted_remdups[simp]:
  3901   "sorted l \<Longrightarrow> sorted (remdups l)"
  3902 by (induct l) (auto simp: sorted_Cons)
  3903 
  3904 lemma sorted_distinct_set_unique:
  3905 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"
  3906 shows "xs = ys"
  3907 proof -
  3908   from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)
  3909   from assms show ?thesis
  3910   proof(induct rule:list_induct2[OF 1])
  3911     case 1 show ?case by simp
  3912   next
  3913     case 2 thus ?case by (simp add:sorted_Cons)
  3914        (metis Diff_insert_absorb antisym insertE insert_iff)
  3915   qed
  3916 qed
  3917 
  3918 lemma map_sorted_distinct_set_unique:
  3919   assumes "inj_on f (set xs \<union> set ys)"
  3920   assumes "sorted (map f xs)" "distinct (map f xs)"
  3921     "sorted (map f ys)" "distinct (map f ys)"
  3922   assumes "set xs = set ys"
  3923   shows "xs = ys"
  3924 proof -
  3925   from assms have "map f xs = map f ys"
  3926     by (simp add: sorted_distinct_set_unique)
  3927   moreover with `inj_on f (set xs \<union> set ys)` show "xs = ys"
  3928     by (blast intro: map_inj_on)
  3929 qed
  3930 
  3931 lemma finite_sorted_distinct_unique:
  3932 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"
  3933 apply(drule finite_distinct_list)
  3934 apply clarify
  3935 apply(rule_tac a="sort xs" in ex1I)
  3936 apply (auto simp: sorted_distinct_set_unique)
  3937 done
  3938 
  3939 lemma
  3940   assumes "sorted xs"
  3941   shows sorted_take: "sorted (take n xs)"
  3942   and sorted_drop: "sorted (drop n xs)"
  3943 proof -
  3944   from assms have "sorted (take n xs @ drop n xs)" by simp
  3945   then show "sorted (take n xs)" and "sorted (drop n xs)"
  3946     unfolding sorted_append by simp_all
  3947 qed
  3948 
  3949 lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"
  3950   by (auto dest: sorted_drop simp add: dropWhile_eq_drop)
  3951 
  3952 lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"
  3953   by (subst takeWhile_eq_take) (auto dest: sorted_take)
  3954 
  3955 lemma sorted_filter:
  3956   "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"
  3957   by (induct xs) (simp_all add: sorted_Cons)
  3958 
  3959 lemma foldr_max_sorted:
  3960   assumes "sorted (rev xs)"
  3961   shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"
  3962 using assms proof (induct xs)
  3963   case (Cons x xs)
  3964   moreover hence "sorted (rev xs)" using sorted_append by auto
  3965   ultimately show ?case
  3966     by (cases xs, auto simp add: sorted_append max_def)
  3967 qed simp
  3968 
  3969 lemma filter_equals_takeWhile_sorted_rev:
  3970   assumes sorted: "sorted (rev (map f xs))"
  3971   shows "[x \<leftarrow> xs. t < f x] = takeWhile (\<lambda> x. t < f x) xs"
  3972     (is "filter ?P xs = ?tW")
  3973 proof (rule takeWhile_eq_filter[symmetric])
  3974   let "?dW" = "dropWhile ?P xs"
  3975   fix x assume "x \<in> set ?dW"
  3976   then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i"
  3977     unfolding in_set_conv_nth by auto
  3978   hence "length ?tW + i < length (?tW @ ?dW)"
  3979     unfolding length_append by simp
  3980   hence i': "length (map f ?tW) + i < length (map f xs)" by simp
  3981   have "(map f ?tW @ map f ?dW) ! (length (map f ?tW) + i) \<le>
  3982         (map f ?tW @ map f ?dW) ! (length (map f ?tW) + 0)"
  3983     using sorted_rev_nth_mono[OF sorted _ i', of "length ?tW"]
  3984     unfolding map_append[symmetric] by simp
  3985   hence "f x \<le> f (?dW ! 0)"
  3986     unfolding nth_append_length_plus nth_i
  3987     using i preorder_class.le_less_trans[OF le0 i] by simp
  3988   also have "... \<le> t"
  3989     using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]
  3990     using hd_conv_nth[of "?dW"] by simp
  3991   finally show "\<not> t < f x" by simp
  3992 qed
  3993 
  3994 lemma insort_insert_key_triv:
  3995   "f x \<in> f ` set xs \<Longrightarrow> insort_insert_key f x xs = xs"
  3996   by (simp add: insort_insert_key_def)
  3997 
  3998 lemma insort_insert_triv:
  3999   "x \<in> set xs \<Longrightarrow> insort_insert x xs = xs"
  4000   using insort_insert_key_triv [of "\<lambda>x. x"] by simp
  4001 
  4002 lemma insort_insert_insort_key:
  4003   "f x \<notin> f ` set xs \<Longrightarrow> insort_insert_key f x xs = insort_key f x xs"
  4004   by (simp add: insort_insert_key_def)
  4005 
  4006 lemma insort_insert_insort:
  4007   "x \<notin> set xs \<Longrightarrow> insort_insert x xs = insort x xs"
  4008   using insort_insert_insort_key [of "\<lambda>x. x"] by simp
  4009 
  4010 lemma set_insort_insert:
  4011   "set (insort_insert x xs) = insert x (set xs)"
  4012   by (auto simp add: insort_insert_key_def set_insort)
  4013 
  4014 lemma distinct_insort_insert:
  4015   assumes "distinct xs"
  4016   shows "distinct (insort_insert_key f x xs)"
  4017   using assms by (induct xs) (auto simp add: insort_insert_key_def set_insort)
  4018 
  4019 lemma sorted_insort_insert_key:
  4020   assumes "sorted (map f xs)"
  4021   shows "sorted (map f (insort_insert_key f x xs))"
  4022   using assms by (simp add: insort_insert_key_def sorted_insort_key)
  4023 
  4024 lemma sorted_insort_insert:
  4025   assumes "sorted xs"
  4026   shows "sorted (insort_insert x xs)"
  4027   using assms sorted_insort_insert_key [of "\<lambda>x. x"] by simp
  4028 
  4029 lemma filter_insort_triv:
  4030   "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"
  4031   by (induct xs) simp_all
  4032 
  4033 lemma filter_insort:
  4034   "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"
  4035   using assms by (induct xs)
  4036     (auto simp add: sorted_Cons, subst insort_is_Cons, auto)
  4037 
  4038 lemma filter_sort:
  4039   "filter P (sort_key f xs) = sort_key f (filter P xs)"
  4040   by (induct xs) (simp_all add: filter_insort_triv filter_insort)
  4041 
  4042 lemma sorted_map_same:
  4043   "sorted (map f [x\<leftarrow>xs. f x = g xs])"
  4044 proof (induct xs arbitrary: g)
  4045   case Nil then show ?case by simp
  4046 next
  4047   case (Cons x xs)
  4048   then have "sorted (map f [y\<leftarrow>xs . f y = (\<lambda>xs. f x) xs])" .
  4049   moreover from Cons have "sorted (map f [y\<leftarrow>xs . f y = (g \<circ> Cons x) xs])" .
  4050   ultimately show ?case by (simp_all add: sorted_Cons)
  4051 qed
  4052 
  4053 lemma sorted_same:
  4054   "sorted [x\<leftarrow>xs. x = g xs]"
  4055   using sorted_map_same [of "\<lambda>x. x"] by simp
  4056 
  4057 lemma remove1_insort [simp]:
  4058   "remove1 x (insort x xs) = xs"
  4059   by (induct xs) simp_all
  4060 
  4061 end
  4062 
  4063 lemma sorted_upt[simp]: "sorted[i..<j]"
  4064 by (induct j) (simp_all add:sorted_append)
  4065 
  4066 lemma sorted_upto[simp]: "sorted[i..j]"
  4067 apply(induct i j rule:upto.induct)
  4068 apply(subst upto.simps)
  4069 apply(simp add:sorted_Cons)
  4070 done
  4071 
  4072 
  4073 subsubsection {* @{const transpose} on sorted lists *}
  4074 
  4075 lemma sorted_transpose[simp]:
  4076   shows "sorted (rev (map length (transpose xs)))"
  4077   by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose
  4078     length_filter_conv_card intro: card_mono)
  4079 
  4080 lemma transpose_max_length:
  4081   "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"
  4082   (is "?L = ?R")
  4083 proof (cases "transpose xs = []")
  4084   case False
  4085   have "?L = foldr max (map length (transpose xs)) 0"
  4086     by (simp add: foldr_map comp_def)
  4087   also have "... = length (transpose xs ! 0)"
  4088     using False sorted_transpose by (simp add: foldr_max_sorted)
  4089   finally show ?thesis
  4090     using False by (simp add: nth_transpose)
  4091 next
  4092   case True
  4093   hence "[x \<leftarrow> xs. x \<noteq> []] = []"
  4094     by (auto intro!: filter_False simp: transpose_empty)
  4095   thus ?thesis by (simp add: transpose_empty True)
  4096 qed
  4097 
  4098 lemma length_transpose_sorted:
  4099   fixes xs :: "'a list list"
  4100   assumes sorted: "sorted (rev (map length xs))"
  4101   shows "length (transpose xs) = (if xs = [] then 0 else length (xs ! 0))"
  4102 proof (cases "xs = []")
  4103   case False
  4104   thus ?thesis
  4105     using foldr_max_sorted[OF sorted] False
  4106     unfolding length_transpose foldr_map comp_def
  4107     by simp
  4108 qed simp
  4109 
  4110 lemma nth_nth_transpose_sorted[simp]:
  4111   fixes xs :: "'a list list"
  4112   assumes sorted: "sorted (rev (map length xs))"
  4113   and i: "i < length (transpose xs)"
  4114   and j: "j < length [ys \<leftarrow> xs. i < length ys]"
  4115   shows "transpose xs ! i ! j = xs ! j  ! i"
  4116   using j filter_equals_takeWhile_sorted_rev[OF sorted, of i]
  4117     nth_transpose[OF i] nth_map[OF j]
  4118   by (simp add: takeWhile_nth)
  4119 
  4120 lemma transpose_column_length:
  4121   fixes xs :: "'a list list"
  4122   assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
  4123   shows "length (filter (\<lambda>ys. i < length ys) (transpose xs)) = length (xs ! i)"
  4124 proof -
  4125   have "xs \<noteq> []" using `i < length xs` by auto
  4126   note filter_equals_takeWhile_sorted_rev[OF sorted, simp]
  4127   { fix j assume "j \<le> i"
  4128     note sorted_rev_nth_mono[OF sorted, of j i, simplified, OF this `i < length xs`]
  4129   } note sortedE = this[consumes 1]
  4130 
  4131   have "{j. j < length (transpose xs) \<and> i < length (transpose xs ! j)}
  4132     = {..< length (xs ! i)}"
  4133   proof safe
  4134     fix j
  4135     assume "j < length (transpose xs)" and "i < length (transpose xs ! j)"
  4136     with this(2) nth_transpose[OF this(1)]
  4137     have "i < length (takeWhile (\<lambda>ys. j < length ys) xs)" by simp
  4138     from nth_mem[OF this] takeWhile_nth[OF this]
  4139     show "j < length (xs ! i)" by (auto dest: set_takeWhileD)
  4140   next
  4141     fix j assume "j < length (xs ! i)"
  4142     thus "j < length (transpose xs)"
  4143       using foldr_max_sorted[OF sorted] `xs \<noteq> []` sortedE[OF le0]
  4144       by (auto simp: length_transpose comp_def foldr_map)
  4145 
  4146     have "Suc i \<le> length (takeWhile (\<lambda>ys. j < length ys) xs)"
  4147       using `i < length xs` `j < length (xs ! i)` less_Suc_eq_le
  4148       by (auto intro!: length_takeWhile_less_P_nth dest!: sortedE)
  4149     with nth_transpose[OF `j < length (transpose xs)`]
  4150     show "i < length (transpose xs ! j)" by simp
  4151   qed
  4152   thus ?thesis by (simp add: length_filter_conv_card)
  4153 qed
  4154 
  4155 lemma transpose_column:
  4156   fixes xs :: "'a list list"
  4157   assumes sorted: "sorted (rev (map length xs))" and "i < length xs"
  4158   shows "map (\<lambda>ys. ys ! i) (filter (\<lambda>ys. i < length ys) (transpose xs))
  4159     = xs ! i" (is "?R = _")
  4160 proof (rule nth_equalityI, safe)
  4161   show length: "length ?R = length (xs ! i)"
  4162     using transpose_column_length[OF assms] by simp
  4163 
  4164   fix j assume j: "j < length ?R"
  4165   note * = less_le_trans[OF this, unfolded length_map, OF length_filter_le]
  4166   from j have j_less: "j < length (xs ! i)" using length by simp
  4167   have i_less_tW: "Suc i \<le> length (takeWhile (\<lambda>ys. Suc j \<le> length ys) xs)"
  4168   proof (rule length_takeWhile_less_P_nth)
  4169     show "Suc i \<le> length xs" using `i < length xs` by simp
  4170     fix k assume "k < Suc i"
  4171     hence "k \<le> i" by auto
  4172     with sorted_rev_nth_mono[OF sorted this] `i < length xs`
  4173     have "length (xs ! i) \<le> length (xs ! k)" by simp
  4174     thus "Suc j \<le> length (xs ! k)" using j_less by simp
  4175   qed
  4176   have i_less_filter: "i < length [ys\<leftarrow>xs . j < length ys]"
  4177     unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j]
  4178     using i_less_tW by (simp_all add: Suc_le_eq)
  4179   from j show "?R ! j = xs ! i ! j"
  4180     unfolding filter_equals_takeWhile_sorted_rev[OF sorted_transpose, of i]
  4181     by (simp add: takeWhile_nth nth_nth_transpose_sorted[OF sorted * i_less_filter])
  4182 qed
  4183 
  4184 lemma transpose_transpose:
  4185   fixes xs :: "'a list list"
  4186   assumes sorted: "sorted (rev (map length xs))"
  4187   shows "transpose (transpose xs) = takeWhile (\<lambda>x. x \<noteq> []) xs" (is "?L = ?R")
  4188 proof -
  4189   have len: "length ?L = length ?R"
  4190     unfolding length_transpose transpose_max_length
  4191     using filter_equals_takeWhile_sorted_rev[OF sorted, of 0]
  4192     by simp
  4193 
  4194   { fix i assume "i < length ?R"
  4195     with less_le_trans[OF _ length_takeWhile_le[of _ xs]]
  4196     have "i < length xs" by simp
  4197   } note * = this
  4198   show ?thesis
  4199     by (rule nth_equalityI)
  4200        (simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth)
  4201 qed
  4202 
  4203 theorem transpose_rectangle:
  4204   assumes "xs = [] \<Longrightarrow> n = 0"
  4205   assumes rect: "\<And> i. i < length xs \<Longrightarrow> length (xs ! i) = n"
  4206   shows "transpose xs = map (\<lambda> i. map (\<lambda> j. xs ! j ! i) [0..<length xs]) [0..<n]"
  4207     (is "?trans = ?map")
  4208 proof (rule nth_equalityI)
  4209   have "sorted (rev (map length xs))"
  4210     by (auto simp: rev_nth rect intro!: sorted_nth_monoI)
  4211   from foldr_max_sorted[OF this] assms
  4212   show len: "length ?trans = length ?map"
  4213     by (simp_all add: length_transpose foldr_map comp_def)
  4214   moreover
  4215   { fix i assume "i < n" hence "[ys\<leftarrow>xs . i < length ys] = xs"
  4216       using rect by (auto simp: in_set_conv_nth intro!: filter_True) }
  4217   ultimately show "\<forall>i < length ?trans. ?trans ! i = ?map ! i"
  4218     by (auto simp: nth_transpose intro: nth_equalityI)
  4219 qed
  4220 
  4221 
  4222 subsubsection {* @{text sorted_list_of_set} *}
  4223 
  4224 text{* This function maps (finite) linearly ordered sets to sorted
  4225 lists. Warning: in most cases it is not a good idea to convert from
  4226 sets to lists but one should convert in the other direction (via
  4227 @{const set}). *}
  4228 
  4229 context linorder
  4230 begin
  4231 
  4232 definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where
  4233   "sorted_list_of_set = Finite_Set.fold insort []"
  4234 
  4235 lemma sorted_list_of_set_empty [simp]:
  4236   "sorted_list_of_set {} = []"
  4237   by (simp add: sorted_list_of_set_def)
  4238 
  4239 lemma sorted_list_of_set_insert [simp]:
  4240   assumes "finite A"
  4241   shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"
  4242 proof -
  4243   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
  4244   with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)
  4245 qed
  4246 
  4247 lemma sorted_list_of_set [simp]:
  4248   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A) 
  4249     \<and> distinct (sorted_list_of_set A)"
  4250   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)
  4251 
  4252 lemma sorted_list_of_set_sort_remdups:
  4253   "sorted_list_of_set (set xs) = sort (remdups xs)"
  4254 proof -
  4255   interpret comp_fun_commute insort by (fact comp_fun_commute_insort)
  4256   show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)
  4257 qed
  4258 
  4259 lemma sorted_list_of_set_remove:
  4260   assumes "finite A"
  4261   shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"
  4262 proof (cases "x \<in> A")
  4263   case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp
  4264   with False show ?thesis by (simp add: remove1_idem)
  4265 next
  4266   case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)
  4267   with assms show ?thesis by simp
  4268 qed
  4269 
  4270 end
  4271 
  4272 lemma sorted_list_of_set_range [simp]:
  4273   "sorted_list_of_set {m..<n} = [m..<n]"
  4274   by (rule sorted_distinct_set_unique) simp_all
  4275 
  4276 
  4277 subsubsection {* @{text lists}: the list-forming operator over sets *}
  4278 
  4279 inductive_set
  4280   lists :: "'a set => 'a list set"
  4281   for A :: "'a set"
  4282 where
  4283     Nil [intro!, simp]: "[]: lists A"
  4284   | Cons [intro!, simp, no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"
  4285 
  4286 inductive_cases listsE [elim!,no_atp]: "x#l : lists A"
  4287 inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"
  4288 
  4289 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"
  4290 by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)
  4291 
  4292 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]
  4293 
  4294 lemma listsp_infI:
  4295   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l
  4296 by induct blast+
  4297 
  4298 lemmas lists_IntI = listsp_infI [to_set]
  4299 
  4300 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"
  4301 proof (rule mono_inf [where f=listsp, THEN order_antisym])
  4302   show "mono listsp" by (simp add: mono_def listsp_mono)
  4303   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)
  4304 qed
  4305 
  4306 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_def inf_bool_def]
  4307 
  4308 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]
  4309 
  4310 lemma Cons_in_lists_iff[simp]: "x#xs : lists A \<longleftrightarrow> x:A \<and> xs : lists A"
  4311 by auto
  4312 
  4313 lemma append_in_listsp_conv [iff]:
  4314      "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"
  4315 by (induct xs) auto
  4316 
  4317 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]
  4318 
  4319 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"
  4320 -- {* eliminate @{text listsp} in favour of @{text set} *}
  4321 by (induct xs) auto
  4322 
  4323 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]
  4324 
  4325 lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"
  4326 by (rule in_listsp_conv_set [THEN iffD1])
  4327 
  4328 lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]
  4329 
  4330 lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"
  4331 by (rule in_listsp_conv_set [THEN iffD2])
  4332 
  4333 lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]
  4334 
  4335 lemma lists_eq_set: "lists A = {xs. set xs <= A}"
  4336 by auto
  4337 
  4338 lemma lists_empty [simp]: "lists {} = {[]}"
  4339 by auto
  4340 
  4341 lemma lists_UNIV [simp]: "lists UNIV = UNIV"
  4342 by auto
  4343 
  4344 
  4345 subsubsection {* Inductive definition for membership *}
  4346 
  4347 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"
  4348 where
  4349     elem:  "ListMem x (x # xs)"
  4350   | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"
  4351 
  4352 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"
  4353 apply (rule iffI)
  4354  apply (induct set: ListMem)
  4355   apply auto
  4356 apply (induct xs)
  4357  apply (auto intro: ListMem.intros)
  4358 done
  4359 
  4360 
  4361 subsubsection {* Lists as Cartesian products *}
  4362 
  4363 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from
  4364 @{term A} and tail drawn from @{term Xs}.*}
  4365 
  4366 definition
  4367   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where
  4368   "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"
  4369 
  4370 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])`A"
  4371 by (auto simp add: set_Cons_def)
  4372 
  4373 text{*Yields the set of lists, all of the same length as the argument and
  4374 with elements drawn from the corresponding element of the argument.*}
  4375 
  4376 primrec
  4377   listset :: "'a set list \<Rightarrow> 'a list set" where
  4378      "listset [] = {[]}"
  4379   |  "listset (A # As) = set_Cons A (listset As)"
  4380 
  4381 
  4382 subsection {* Relations on Lists *}
  4383 
  4384 subsubsection {* Length Lexicographic Ordering *}
  4385 
  4386 text{*These orderings preserve well-foundedness: shorter lists 
  4387   precede longer lists. These ordering are not used in dictionaries.*}
  4388         
  4389 primrec -- {*The lexicographic ordering for lists of the specified length*}
  4390   lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where
  4391     "lexn r 0 = {}"
  4392   | "lexn r (Suc n) = (map_pair (%(x, xs). x#xs) (%(x, xs). x#xs) ` (r <*lex*> lexn r n)) Int
  4393       {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"
  4394 
  4395 definition
  4396   lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
  4397   "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}
  4398 
  4399 definition
  4400   lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where
  4401   "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"
  4402         -- {*Compares lists by their length and then lexicographically*}
  4403 
  4404 lemma wf_lexn: "wf r ==> wf (lexn r n)"
  4405 apply (induct n, simp, simp)
  4406 apply(rule wf_subset)
  4407  prefer 2 apply (rule Int_lower1)
  4408 apply(rule wf_map_pair_image)
  4409  prefer 2 apply (rule inj_onI, auto)
  4410 done
  4411 
  4412 lemma lexn_length:
  4413   "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"
  4414 by (induct n arbitrary: xs ys) auto
  4415 
  4416 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"
  4417 apply (unfold lex_def)
  4418 apply (rule wf_UN)
  4419 apply (blast intro: wf_lexn, clarify)
  4420 apply (rename_tac m n)
  4421 apply (subgoal_tac "m \<noteq> n")
  4422  prefer 2 apply blast
  4423 apply (blast dest: lexn_length not_sym)
  4424 done
  4425 
  4426 lemma lexn_conv:
  4427   "lexn r n =
  4428     {(xs,ys). length xs = n \<and> length ys = n \<and>
  4429     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"
  4430 apply (induct n, simp)
  4431 apply (simp add: image_Collect lex_prod_def, safe, blast)
  4432  apply (rule_tac x = "ab # xys" in exI, simp)
  4433 apply (case_tac xys, simp_all, blast)
  4434 done
  4435 
  4436 lemma lex_conv:
  4437   "lex r =
  4438     {(xs,ys). length xs = length ys \<and>
  4439     (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"
  4440 by (force simp add: lex_def lexn_conv)
  4441 
  4442 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"
  4443 by (unfold lenlex_def) blast
  4444 
  4445 lemma lenlex_conv:
  4446     "lenlex r = {(xs,ys). length xs < length ys |
  4447                  length xs = length ys \<and> (xs, ys) : lex r}"
  4448 by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)
  4449 
  4450 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"
  4451 by (simp add: lex_conv)
  4452 
  4453 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"
  4454 by (simp add:lex_conv)
  4455 
  4456 lemma Cons_in_lex [simp]:
  4457     "((x # xs, y # ys) : lex r) =
  4458       ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"
  4459 apply (simp add: lex_conv)
  4460 apply (rule iffI)
  4461  prefer 2 apply (blast intro: Cons_eq_appendI, clarify)
  4462 apply (case_tac xys, simp, simp)
  4463 apply blast
  4464 done
  4465 
  4466 
  4467 subsubsection {* Lexicographic Ordering *}
  4468 
  4469 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".
  4470     This ordering does \emph{not} preserve well-foundedness.
  4471      Author: N. Voelker, March 2005. *} 
  4472 
  4473 definition
  4474   lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
  4475   "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>
  4476             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"
  4477 
  4478 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"
  4479 by (unfold lexord_def, induct_tac y, auto) 
  4480 
  4481 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"
  4482 by (unfold lexord_def, induct_tac x, auto)
  4483 
  4484 lemma lexord_cons_cons[simp]:
  4485      "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"
  4486   apply (unfold lexord_def, safe, simp_all)
  4487   apply (case_tac u, simp, simp)
  4488   apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)
  4489   apply (erule_tac x="b # u" in allE)
  4490   by force
  4491 
  4492 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons
  4493 
  4494 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"
  4495 by (induct_tac x, auto)  
  4496 
  4497 lemma lexord_append_left_rightI:
  4498      "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"
  4499 by (induct_tac u, auto)
  4500 
  4501 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"
  4502 by (induct x, auto)
  4503 
  4504 lemma lexord_append_leftD:
  4505      "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"
  4506 by (erule rev_mp, induct_tac x, auto)
  4507 
  4508 lemma lexord_take_index_conv: 
  4509    "((x,y) : lexord r) = 
  4510     ((length x < length y \<and> take (length x) y = x) \<or> 
  4511      (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"
  4512   apply (unfold lexord_def Let_def, clarsimp) 
  4513   apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)
  4514   apply auto 
  4515   apply (rule_tac x="hd (drop (length x) y)" in exI)
  4516   apply (rule_tac x="tl (drop (length x) y)" in exI)
  4517   apply (erule subst, simp add: min_def) 
  4518   apply (rule_tac x ="length u" in exI, simp) 
  4519   apply (rule_tac x ="take i x" in exI) 
  4520   apply (rule_tac x ="x ! i" in exI) 
  4521   apply (rule_tac x ="y ! i" in exI, safe) 
  4522   apply (rule_tac x="drop (Suc i) x" in exI)
  4523   apply (drule sym, simp add: drop_Suc_conv_tl) 
  4524   apply (rule_tac x="drop (Suc i) y" in exI)
  4525   by (simp add: drop_Suc_conv_tl) 
  4526 
  4527 -- {* lexord is extension of partial ordering List.lex *} 
  4528 lemma lexord_lex: "(x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"
  4529   apply (rule_tac x = y in spec) 
  4530   apply (induct_tac x, clarsimp) 
  4531   by (clarify, case_tac x, simp, force)
  4532 
  4533 lemma lexord_irreflexive: "ALL x. (x,x) \<notin> r \<Longrightarrow> (xs,xs) \<notin> lexord r"
  4534 by (induct xs) auto
  4535 
  4536 text{* By Ren\'e Thiemann: *}
  4537 lemma lexord_partial_trans: 
  4538   "(\<And>x y z. x \<in> set xs \<Longrightarrow> (x,y) \<in> r \<Longrightarrow> (y,z) \<in> r \<Longrightarrow> (x,z) \<in> r)
  4539    \<Longrightarrow>  (xs,ys) \<in> lexord r  \<Longrightarrow>  (ys,zs) \<in> lexord r \<Longrightarrow>  (xs,zs) \<in> lexord r"
  4540 proof (induct xs arbitrary: ys zs)
  4541   case Nil
  4542   from Nil(3) show ?case unfolding lexord_def by (cases zs, auto)
  4543 next
  4544   case (Cons x xs yys zzs)
  4545   from Cons(3) obtain y ys where yys: "yys = y # ys" unfolding lexord_def
  4546     by (cases yys, auto)
  4547   note Cons = Cons[unfolded yys]
  4548   from Cons(3) have one: "(x,y) \<in> r \<or> x = y \<and> (xs,ys) \<in> lexord r" by auto
  4549   from Cons(4) obtain z zs where zzs: "zzs = z # zs" unfolding lexord_def
  4550     by (cases zzs, auto)
  4551   note Cons = Cons[unfolded zzs]
  4552   from Cons(4) have two: "(y,z) \<in> r \<or> y = z \<and> (ys,zs) \<in> lexord r" by auto
  4553   {
  4554     assume "(xs,ys) \<in> lexord r" and "(ys,zs) \<in> lexord r"
  4555     from Cons(1)[OF _ this] Cons(2)
  4556     have "(xs,zs) \<in> lexord r" by auto
  4557   } note ind1 = this
  4558   {
  4559     assume "(x,y) \<in> r" and "(y,z) \<in> r"
  4560     from Cons(2)[OF _ this] have "(x,z) \<in> r" by auto
  4561   } note ind2 = this
  4562   from one two ind1 ind2
  4563   have "(x,z) \<in> r \<or> x = z \<and> (xs,zs) \<in> lexord r" by blast
  4564   thus ?case unfolding zzs by auto
  4565 qed
  4566 
  4567 lemma lexord_trans: 
  4568     "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"
  4569 by(auto simp: trans_def intro:lexord_partial_trans)
  4570 
  4571 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"
  4572 by (rule transI, drule lexord_trans, blast) 
  4573 
  4574 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"
  4575   apply (rule_tac x = y in spec) 
  4576   apply (induct_tac x, rule allI) 
  4577   apply (case_tac x, simp, simp) 
  4578   apply (rule allI, case_tac x, simp, simp) 
  4579   by blast
  4580 
  4581 
  4582 subsubsection {* Lexicographic combination of measure functions *}
  4583 
  4584 text {* These are useful for termination proofs *}
  4585 
  4586 definition
  4587   "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"
  4588 
  4589 lemma wf_measures[simp]: "wf (measures fs)"
  4590 unfolding measures_def
  4591 by blast
  4592 
  4593 lemma in_measures[simp]: 
  4594   "(x, y) \<in> measures [] = False"
  4595   "(x, y) \<in> measures (f # fs)
  4596          = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"  
  4597 unfolding measures_def
  4598 by auto
  4599 
  4600 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"
  4601 by simp
  4602 
  4603 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"
  4604 by auto
  4605 
  4606 
  4607 subsubsection {* Lifting Relations to Lists: one element *}
  4608 
  4609 definition listrel1 :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where
  4610 "listrel1 r = {(xs,ys).
  4611    \<exists>us z z' vs. xs = us @ z # vs \<and> (z,z') \<in> r \<and> ys = us @ z' # vs}"
  4612 
  4613 lemma listrel1I:
  4614   "\<lbrakk> (x, y) \<in> r;  xs = us @ x # vs;  ys = us @ y # vs \<rbrakk> \<Longrightarrow>
  4615   (xs, ys) \<in> listrel1 r"
  4616 unfolding listrel1_def by auto
  4617 
  4618 lemma listrel1E:
  4619   "\<lbrakk> (xs, ys) \<in> listrel1 r;
  4620      !!x y us vs. \<lbrakk> (x, y) \<in> r;  xs = us @ x # vs;  ys = us @ y # vs \<rbrakk> \<Longrightarrow> P
  4621    \<rbrakk> \<Longrightarrow> P"
  4622 unfolding listrel1_def by auto
  4623 
  4624 lemma not_Nil_listrel1 [iff]: "([], xs) \<notin> listrel1 r"
  4625 unfolding listrel1_def by blast
  4626 
  4627 lemma not_listrel1_Nil [iff]: "(xs, []) \<notin> listrel1 r"
  4628 unfolding listrel1_def by blast
  4629 
  4630 lemma Cons_listrel1_Cons [iff]:
  4631   "(x # xs, y # ys) \<in> listrel1 r \<longleftrightarrow>
  4632    (x,y) \<in> r \<and> xs = ys \<or> x = y \<and> (xs, ys) \<in> listrel1 r"
  4633 by (simp add: listrel1_def Cons_eq_append_conv) (blast)
  4634 
  4635 lemma listrel1I1: "(x,y) \<in> r \<Longrightarrow> (x # xs, y # xs) \<in> listrel1 r"
  4636 by (metis Cons_listrel1_Cons)
  4637 
  4638 lemma listrel1I2: "(xs, ys) \<in> listrel1 r \<Longrightarrow> (x # xs, x # ys) \<in> listrel1 r"
  4639 by (metis Cons_listrel1_Cons)
  4640 
  4641 lemma append_listrel1I:
  4642   "(xs, ys) \<in> listrel1 r \<and> us = vs \<or> xs = ys \<and> (us, vs) \<in> listrel1 r
  4643     \<Longrightarrow> (xs @ us, ys @ vs) \<in> listrel1 r"
  4644 unfolding listrel1_def
  4645 by auto (blast intro: append_eq_appendI)+
  4646 
  4647 lemma Cons_listrel1E1[elim!]:
  4648   assumes "(x # xs, ys) \<in> listrel1 r"
  4649     and "\<And>y. ys = y # xs \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> R"
  4650     and "\<And>zs. ys = x # zs \<Longrightarrow> (xs, zs) \<in> listrel1 r \<Longrightarrow> R"
  4651   shows R
  4652 using assms by (cases ys) blast+
  4653 
  4654 lemma Cons_listrel1E2[elim!]:
  4655   assumes "(xs, y # ys) \<in> listrel1 r"
  4656     and "\<And>x. xs = x # ys \<Longrightarrow> (x, y) \<in> r \<Longrightarrow> R"
  4657     and "\<And>zs. xs = y # zs \<Longrightarrow> (zs, ys) \<in> listrel1 r \<Longrightarrow> R"
  4658   shows R
  4659 using assms by (cases xs) blast+
  4660 
  4661 lemma snoc_listrel1_snoc_iff:
  4662   "(xs @ [x], ys @ [y]) \<in> listrel1 r
  4663     \<longleftrightarrow> (xs, ys) \<in> listrel1 r \<and> x = y \<or> xs = ys \<and> (x,y) \<in> r" (is "?L \<longleftrightarrow> ?R")
  4664 proof
  4665   assume ?L thus ?R
  4666     by (fastsimp simp: listrel1_def snoc_eq_iff_butlast butlast_append)
  4667 next
  4668   assume ?R then show ?L unfolding listrel1_def by force
  4669 qed
  4670 
  4671 lemma listrel1_eq_len: "(xs,ys) \<in> listrel1 r \<Longrightarrow> length xs = length ys"
  4672 unfolding listrel1_def by auto
  4673 
  4674 lemma listrel1_mono:
  4675   "r \<subseteq> s \<Longrightarrow> listrel1 r \<subseteq> listrel1 s"
  4676 unfolding listrel1_def by blast
  4677 
  4678 
  4679 lemma listrel1_converse: "listrel1 (r^-1) = (listrel1 r)^-1"
  4680 unfolding listrel1_def by blast
  4681 
  4682 lemma in_listrel1_converse:
  4683   "(x,y) : listrel1 (r^-1) \<longleftrightarrow> (x,y) : (listrel1 r)^-1"
  4684 unfolding listrel1_def by blast
  4685 
  4686 lemma listrel1_iff_update:
  4687   "(xs,ys) \<in> (listrel1 r)
  4688    \<longleftrightarrow> (\<exists>y n. (xs ! n, y) \<in> r \<and> n < length xs \<and> ys = xs[n:=y])" (is "?L \<longleftrightarrow> ?R")
  4689 proof
  4690   assume "?L"
  4691   then obtain x y u v where "xs = u @ x # v"  "ys = u @ y # v"  "(x,y) \<in> r"
  4692     unfolding listrel1_def by auto
  4693   then have "ys = xs[length u := y]" and "length u < length xs"
  4694     and "(xs ! length u, y) \<in> r" by auto
  4695   then show "?R" by auto
  4696 next
  4697   assume "?R"
  4698   then obtain x y n where "(xs!n, y) \<in> r" "n < size xs" "ys = xs[n:=y]" "x = xs!n"
  4699     by auto
  4700   then obtain u v where "xs = u @ x # v" and "ys = u @ y # v" and "(x, y) \<in> r"
  4701     by (auto intro: upd_conv_take_nth_drop id_take_nth_drop)
  4702   then show "?L" by (auto simp: listrel1_def)
  4703 qed
  4704 
  4705 
  4706 text{* Accessible part and wellfoundedness: *}
  4707 
  4708 lemma Cons_acc_listrel1I [intro!]:
  4709   "x \<in> acc r \<Longrightarrow> xs \<in> acc (listrel1 r) \<Longrightarrow> (x # xs) \<in> acc (listrel1 r)"
  4710 apply (induct arbitrary: xs set: acc)
  4711 apply (erule thin_rl)
  4712 apply (erule acc_induct)
  4713 apply (rule accI)
  4714 apply (blast)
  4715 done
  4716 
  4717 lemma lists_accD: "xs \<in> lists (acc r) \<Longrightarrow> xs \<in> acc (listrel1 r)"
  4718 apply (induct set: lists)
  4719  apply (rule accI)
  4720  apply simp
  4721 apply (rule accI)
  4722 apply (fast dest: acc_downward)
  4723 done
  4724 
  4725 lemma lists_accI: "xs \<in> acc (listrel1 r) \<Longrightarrow> xs \<in> lists (acc r)"
  4726 apply (induct set: acc)
  4727 apply clarify
  4728 apply (rule accI)
  4729 apply (fastsimp dest!: in_set_conv_decomp[THEN iffD1] simp: listrel1_def)
  4730 done
  4731 
  4732 lemma wf_listrel1_iff[simp]: "wf(listrel1 r) = wf r"
  4733 by(metis wf_acc_iff in_lists_conv_set lists_accI lists_accD Cons_in_lists_iff)
  4734 
  4735 
  4736 subsubsection {* Lifting Relations to Lists: all elements *}
  4737 
  4738 inductive_set
  4739   listrel :: "('a * 'a)set => ('a list * 'a list)set"
  4740   for r :: "('a * 'a)set"
  4741 where
  4742     Nil:  "([],[]) \<in> listrel r"
  4743   | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"
  4744 
  4745 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"
  4746 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"
  4747 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"
  4748 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"
  4749 
  4750 
  4751 lemma listrel_eq_len:  "(xs, ys) \<in> listrel r \<Longrightarrow> length xs = length ys"
  4752 by(induct rule: listrel.induct) auto
  4753 
  4754 lemma listrel_iff_zip: "(xs,ys) : listrel r \<longleftrightarrow>
  4755   length xs = length ys & (\<forall>(x,y) \<in> set(zip xs ys). (x,y) \<in> r)" (is "?L \<longleftrightarrow> ?R")
  4756 proof
  4757   assume ?L thus ?R by induct (auto intro: listrel_eq_len)
  4758 next
  4759   assume ?R thus ?L
  4760     apply (clarify)
  4761     by (induct rule: list_induct2) (auto intro: listrel.intros)
  4762 qed
  4763 
  4764 lemma listrel_iff_nth: "(xs,ys) : listrel r \<longleftrightarrow>
  4765   length xs = length ys & (\<forall>n < length xs. (xs!n, ys!n) \<in> r)" (is "?L \<longleftrightarrow> ?R")
  4766 by (auto simp add: all_set_conv_all_nth listrel_iff_zip)
  4767 
  4768 
  4769 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"
  4770 apply clarify  
  4771 apply (erule listrel.induct)
  4772 apply (blast intro: listrel.intros)+
  4773 done
  4774 
  4775 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"
  4776 apply clarify 
  4777 apply (erule listrel.induct, auto) 
  4778 done
  4779 
  4780 lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)" 
  4781 apply (simp add: refl_on_def listrel_subset Ball_def)
  4782 apply (rule allI) 
  4783 apply (induct_tac x) 
  4784 apply (auto intro: listrel.intros)
  4785 done
  4786 
  4787 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)" 
  4788 apply (auto simp add: sym_def)
  4789 apply (erule listrel.induct) 
  4790 apply (blast intro: listrel.intros)+
  4791 done
  4792 
  4793 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)" 
  4794 apply (simp add: trans_def)
  4795 apply (intro allI) 
  4796 apply (rule impI) 
  4797 apply (erule listrel.induct) 
  4798 apply (blast intro: listrel.intros)+
  4799 done
  4800 
  4801 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"
  4802 by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans) 
  4803 
  4804 lemma listrel_rtrancl_refl[iff]: "(xs,xs) : listrel(r^*)"
  4805 using listrel_refl_on[of UNIV, OF refl_rtrancl]
  4806 by(auto simp: refl_on_def)
  4807 
  4808 lemma listrel_rtrancl_trans:
  4809   "\<lbrakk> (xs,ys) : listrel(r^*);  (ys,zs) : listrel(r^*) \<rbrakk>
  4810   \<Longrightarrow> (xs,zs) : listrel(r^*)"
  4811 by (metis listrel_trans trans_def trans_rtrancl)
  4812 
  4813 
  4814 lemma listrel_Nil [simp]: "listrel r `` {[]} = {[]}"
  4815 by (blast intro: listrel.intros)
  4816 
  4817 lemma listrel_Cons:
  4818      "listrel r `` {x#xs} = set_Cons (r``{x}) (listrel r `` {xs})"
  4819 by (auto simp add: set_Cons_def intro: listrel.intros)
  4820 
  4821 text {* Relating @{term listrel1}, @{term listrel} and closures: *}
  4822 
  4823 lemma listrel1_rtrancl_subset_rtrancl_listrel1:
  4824   "listrel1 (r^*) \<subseteq> (listrel1 r)^*"
  4825 proof (rule subrelI)
  4826   fix xs ys assume 1: "(xs,ys) \<in> listrel1 (r^*)"
  4827   { fix x y us vs
  4828     have "(x,y) : r^* \<Longrightarrow> (us @ x # vs, us @ y # vs) : (listrel1 r)^*"
  4829     proof(induct rule: rtrancl.induct)
  4830       case rtrancl_refl show ?case by simp
  4831     next
  4832       case rtrancl_into_rtrancl thus ?case
  4833         by (metis listrel1I rtrancl.rtrancl_into_rtrancl)
  4834     qed }
  4835   thus "(xs,ys) \<in> (listrel1 r)^*" using 1 by(blast elim: listrel1E)
  4836 qed
  4837 
  4838 lemma rtrancl_listrel1_eq_len: "(x,y) \<in> (listrel1 r)^* \<Longrightarrow> length x = length y"
  4839 by (induct rule: rtrancl.induct) (auto intro: listrel1_eq_len)
  4840 
  4841 lemma rtrancl_listrel1_ConsI1:
  4842   "(xs,ys) : (listrel1 r)^* \<Longrightarrow> (x#xs,x#ys) : (listrel1 r)^*"
  4843 apply(induct rule: rtrancl.induct)
  4844  apply simp
  4845 by (metis listrel1I2 rtrancl.rtrancl_into_rtrancl)
  4846 
  4847 lemma rtrancl_listrel1_ConsI2:
  4848   "(x,y) \<in> r^* \<Longrightarrow> (xs, ys) \<in> (listrel1 r)^*
  4849   \<Longrightarrow> (x # xs, y # ys) \<in> (listrel1 r)^*"
  4850   by (blast intro: rtrancl_trans rtrancl_listrel1_ConsI1 
  4851     subsetD[OF listrel1_rtrancl_subset_rtrancl_listrel1 listrel1I1])
  4852 
  4853 lemma listrel1_subset_listrel:
  4854   "r \<subseteq> r' \<Longrightarrow> refl r' \<Longrightarrow> listrel1 r \<subseteq> listrel(r')"
  4855 by(auto elim!: listrel1E simp add: listrel_iff_zip set_zip refl_on_def)
  4856 
  4857 lemma listrel_reflcl_if_listrel1:
  4858   "(xs,ys) : listrel1 r \<Longrightarrow> (xs,ys) : listrel(r^*)"
  4859 by(erule listrel1E)(auto simp add: listrel_iff_zip set_zip)
  4860 
  4861 lemma listrel_rtrancl_eq_rtrancl_listrel1: "listrel (r^*) = (listrel1 r)^*"
  4862 proof
  4863   { fix x y assume "(x,y) \<in> listrel (r^*)"
  4864     then have "(x,y) \<in> (listrel1 r)^*"
  4865     by induct (auto intro: rtrancl_listrel1_ConsI2) }
  4866   then show "listrel (r^*) \<subseteq> (listrel1 r)^*"
  4867     by (rule subrelI)
  4868 next
  4869   show "listrel (r^*) \<supseteq> (listrel1 r)^*"
  4870   proof(rule subrelI)
  4871     fix xs ys assume "(xs,ys) \<in> (listrel1 r)^*"
  4872     then show "(xs,ys) \<in> listrel (r^*)"
  4873     proof induct
  4874       case base show ?case by(auto simp add: listrel_iff_zip set_zip)
  4875     next
  4876       case (step ys zs)
  4877       thus ?case  by (metis listrel_reflcl_if_listrel1 listrel_rtrancl_trans)
  4878     qed
  4879   qed
  4880 qed
  4881 
  4882 lemma rtrancl_listrel1_if_listrel:
  4883   "(xs,ys) : listrel r \<Longrightarrow> (xs,ys) : (listrel1 r)^*"
  4884 by(metis listrel_rtrancl_eq_rtrancl_listrel1 subsetD[OF listrel_mono] r_into_rtrancl subsetI)
  4885 
  4886 lemma listrel_subset_rtrancl_listrel1: "listrel r \<subseteq> (listrel1 r)^*"
  4887 by(fast intro:rtrancl_listrel1_if_listrel)
  4888 
  4889 
  4890 subsection {* Size function *}
  4891 
  4892 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"
  4893 by (rule is_measure_trivial)
  4894 
  4895 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"
  4896 by (rule is_measure_trivial)
  4897 
  4898 lemma list_size_estimation[termination_simp]: 
  4899   "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"
  4900 by (induct xs) auto
  4901 
  4902 lemma list_size_estimation'[termination_simp]: 
  4903   "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"
  4904 by (induct xs) auto
  4905 
  4906 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"
  4907 by (induct xs) auto
  4908 
  4909 lemma list_size_append[simp]: "list_size f (xs @ ys) = list_size f xs + list_size f ys"
  4910 by (induct xs, auto)
  4911 
  4912 lemma list_size_pointwise[termination_simp]: 
  4913   "(\<And>x. x \<in> set xs \<Longrightarrow> f x \<le> g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"
  4914 by (induct xs) force+
  4915 
  4916 
  4917 subsection {* Transfer *}
  4918 
  4919 definition
  4920   embed_list :: "nat list \<Rightarrow> int list"
  4921 where
  4922   "embed_list l = map int l"
  4923 
  4924 definition
  4925   nat_list :: "int list \<Rightarrow> bool"
  4926 where
  4927   "nat_list l = nat_set (set l)"
  4928 
  4929 definition
  4930   return_list :: "int list \<Rightarrow> nat list"
  4931 where
  4932   "return_list l = map nat l"
  4933 
  4934 lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>
  4935     embed_list (return_list l) = l"
  4936   unfolding embed_list_def return_list_def nat_list_def nat_set_def
  4937   apply (induct l)
  4938   apply auto
  4939 done
  4940 
  4941 lemma transfer_nat_int_list_functions:
  4942   "l @ m = return_list (embed_list l @ embed_list m)"
  4943   "[] = return_list []"
  4944   unfolding return_list_def embed_list_def
  4945   apply auto
  4946   apply (induct l, auto)
  4947   apply (induct m, auto)
  4948 done
  4949 
  4950 (*
  4951 lemma transfer_nat_int_fold1: "fold f l x =
  4952     fold (%x. f (nat x)) (embed_list l) x";
  4953 *)
  4954 
  4955 
  4956 subsection {* Code generation *}
  4957 
  4958 subsubsection {* Counterparts for set-related operations *}
  4959 
  4960 definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where
  4961   [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"
  4962 
  4963 text {*
  4964   Only use @{text member} for generating executable code.  Otherwise use
  4965   @{prop "x \<in> set xs"} instead --- it is much easier to reason about.
  4966 *}
  4967 
  4968 lemma member_set:
  4969   "member = set"
  4970   by (simp add: fun_eq_iff member_def mem_def)
  4971 
  4972 lemma member_rec [code]:
  4973   "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"
  4974   "member [] y \<longleftrightarrow> False"
  4975   by (auto simp add: member_def)
  4976 
  4977 lemma in_set_member [code_unfold]:
  4978   "x \<in> set xs \<longleftrightarrow> member xs x"
  4979   by (simp add: member_def)
  4980 
  4981 declare INFI_def [code_unfold]
  4982 declare SUPR_def [code_unfold]
  4983 
  4984 declare set_map [symmetric, code_unfold]
  4985 
  4986 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  4987   list_all_iff [code_post]: "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"
  4988 
  4989 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
  4990   list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"
  4991 
  4992 definition list_ex1
  4993 where
  4994   list_ex1_iff: "list_ex1 P xs \<longleftrightarrow> (\<exists>! x. x \<in> set xs \<and> P x)"
  4995 
  4996 text {*
  4997   Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}
  4998   over @{const list_all} and @{const list_ex} in specifications.
  4999 *}
  5000 
  5001 lemma list_all_simps [simp, code]:
  5002   "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"
  5003   "list_all P [] \<longleftrightarrow> True"
  5004   by (simp_all add: list_all_iff)
  5005 
  5006 lemma list_ex_simps [simp, code]:
  5007   "list_ex P (x # xs) \<longleftrightarrow> P x \<or> list_ex P xs"
  5008   "list_ex P [] \<longleftrightarrow> False"
  5009   by (simp_all add: list_ex_iff)
  5010 
  5011 lemma list_ex1_simps [simp, code]:
  5012   "list_ex1 P [] = False"
  5013   "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)"
  5014 unfolding list_ex1_iff list_all_iff by auto
  5015 
  5016 lemma Ball_set_list_all [code_unfold]:
  5017   "Ball (set xs) P \<longleftrightarrow> list_all P xs"
  5018   by (simp add: list_all_iff)
  5019 
  5020 lemma Bex_set_list_ex [code_unfold]:
  5021   "Bex (set xs) P \<longleftrightarrow> list_ex P xs"
  5022   by (simp add: list_ex_iff)
  5023 
  5024 lemma list_all_append [simp]:
  5025   "list_all P (xs @ ys) \<longleftrightarrow> list_all P xs \<and> list_all P ys"
  5026   by (auto simp add: list_all_iff)
  5027 
  5028 lemma list_ex_append [simp]:
  5029   "list_ex P (xs @ ys) \<longleftrightarrow> list_ex P xs \<or> list_ex P ys"
  5030   by (auto simp add: list_ex_iff)
  5031 
  5032 lemma list_all_rev [simp]:
  5033   "list_all P (rev xs) \<longleftrightarrow> list_all P xs"
  5034   by (simp add: list_all_iff)
  5035 
  5036 lemma list_ex_rev [simp]:
  5037   "list_ex P (rev xs) \<longleftrightarrow> list_ex P xs"
  5038   by (simp add: list_ex_iff)
  5039 
  5040 lemma list_all_length:
  5041   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"
  5042   by (auto simp add: list_all_iff set_conv_nth)
  5043 
  5044 lemma list_ex_length:
  5045   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"
  5046   by (auto simp add: list_ex_iff set_conv_nth)
  5047 
  5048 lemma list_all_cong [fundef_cong]:
  5049   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"
  5050   by (simp add: list_all_iff)
  5051 
  5052 lemma list_any_cong [fundef_cong]:
  5053   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"
  5054   by (simp add: list_ex_iff)
  5055 
  5056 text {* Bounded quantification and summation over nats. *}
  5057 
  5058 lemma atMost_upto [code_unfold]:
  5059   "{..n} = set [0..<Suc n]"
  5060   by auto
  5061 
  5062 lemma atLeast_upt [code_unfold]:
  5063   "{..<n} = set [0..<n]"
  5064   by auto
  5065 
  5066 lemma greaterThanLessThan_upt [code_unfold]:
  5067   "{n<..<m} = set [Suc n..<m]"
  5068   by auto
  5069 
  5070 lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]
  5071 
  5072 lemma greaterThanAtMost_upt [code_unfold]:
  5073   "{n<..m} = set [Suc n..<Suc m]"
  5074   by auto
  5075 
  5076 lemma atLeastAtMost_upt [code_unfold]:
  5077   "{n..m} = set [n..<Suc m]"
  5078   by auto
  5079 
  5080 lemma all_nat_less_eq [code_unfold]:
  5081   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"
  5082   by auto
  5083 
  5084 lemma ex_nat_less_eq [code_unfold]:
  5085   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"
  5086   by auto
  5087 
  5088 lemma all_nat_less [code_unfold]:
  5089   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"
  5090   by auto
  5091 
  5092 lemma ex_nat_less [code_unfold]:
  5093   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"
  5094   by auto
  5095 
  5096 lemma setsum_set_upt_conv_listsum_nat [code_unfold]:
  5097   "setsum f (set [m..<n]) = listsum (map f [m..<n])"
  5098   by (simp add: interv_listsum_conv_setsum_set_nat)
  5099 
  5100 text {* Summation over ints. *}
  5101 
  5102 lemma greaterThanLessThan_upto [code_unfold]:
  5103   "{i<..<j::int} = set [i+1..j - 1]"
  5104 by auto
  5105 
  5106 lemma atLeastLessThan_upto [code_unfold]:
  5107   "{i..<j::int} = set [i..j - 1]"
  5108 by auto
  5109 
  5110 lemma greaterThanAtMost_upto [code_unfold]:
  5111   "{i<..j::int} = set [i+1..j]"
  5112 by auto
  5113 
  5114 lemmas atLeastAtMost_upto [code_unfold] = set_upto [symmetric]
  5115 
  5116 lemma setsum_set_upto_conv_listsum_int [code_unfold]:
  5117   "setsum f (set [i..j::int]) = listsum (map f [i..j])"
  5118   by (simp add: interv_listsum_conv_setsum_set_int)
  5119 
  5120 
  5121 subsubsection {* Optimizing by rewriting *}
  5122 
  5123 definition null :: "'a list \<Rightarrow> bool" where
  5124   [code_post]: "null xs \<longleftrightarrow> xs = []"
  5125 
  5126 text {*
  5127   Efficient emptyness check is implemented by @{const null}.
  5128 *}
  5129 
  5130 lemma null_rec [code]:
  5131   "null (x # xs) \<longleftrightarrow> False"
  5132   "null [] \<longleftrightarrow> True"
  5133   by (simp_all add: null_def)
  5134 
  5135 lemma eq_Nil_null [code_unfold]:
  5136   "xs = [] \<longleftrightarrow> null xs"
  5137   by (simp add: null_def)
  5138 
  5139 lemma equal_Nil_null [code_unfold]:
  5140   "HOL.equal xs [] \<longleftrightarrow> null xs"
  5141   by (simp add: equal eq_Nil_null)
  5142 
  5143 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
  5144   [code_post]: "maps f xs = concat (map f xs)"
  5145 
  5146 definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
  5147   [code_post]: "map_filter f xs = map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) xs)"
  5148 
  5149 text {*
  5150   Operations @{const maps} and @{const map_filter} avoid
  5151   intermediate lists on execution -- do not use for proving.
  5152 *}
  5153 
  5154 lemma maps_simps [code]:
  5155   "maps f (x # xs) = f x @ maps f xs"
  5156   "maps f [] = []"
  5157   by (simp_all add: maps_def)
  5158 
  5159 lemma map_filter_simps [code]:
  5160   "map_filter f (x # xs) = (case f x of None \<Rightarrow> map_filter f xs | Some y \<Rightarrow> y # map_filter f xs)"
  5161   "map_filter f [] = []"
  5162   by (simp_all add: map_filter_def split: option.split)
  5163 
  5164 lemma concat_map_maps [code_unfold]:
  5165   "concat (map f xs) = maps f xs"
  5166   by (simp add: maps_def)
  5167 
  5168 lemma map_filter_map_filter [code_unfold]:
  5169   "map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
  5170   by (simp add: map_filter_def)
  5171 
  5172 text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
  5173 and similiarly for @{text"\<exists>"}. *}
  5174 
  5175 definition all_interval_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where
  5176   "all_interval_nat P i j \<longleftrightarrow> (\<forall>n \<in> {i..<j}. P n)"
  5177 
  5178 lemma [code]:
  5179   "all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"
  5180 proof -
  5181   have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"
  5182   proof -
  5183     fix n
  5184     assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> n" "n < j"
  5185     then show "P n" by (cases "n = i") simp_all
  5186   qed
  5187   show ?thesis by (auto simp add: all_interval_nat_def intro: *)
  5188 qed
  5189 
  5190 lemma list_all_iff_all_interval_nat [code_unfold]:
  5191   "list_all P [i..<j] \<longleftrightarrow> all_interval_nat P i j"
  5192   by (simp add: list_all_iff all_interval_nat_def)
  5193 
  5194 lemma list_ex_iff_not_all_inverval_nat [code_unfold]:
  5195   "list_ex P [i..<j] \<longleftrightarrow> \<not> (all_interval_nat (Not \<circ> P) i j)"
  5196   by (simp add: list_ex_iff all_interval_nat_def)
  5197 
  5198 definition all_interval_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where
  5199   "all_interval_int P i j \<longleftrightarrow> (\<forall>k \<in> {i..j}. P k)"
  5200 
  5201 lemma [code]:
  5202   "all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"
  5203 proof -
  5204   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"
  5205   proof -
  5206     fix k
  5207     assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> j"
  5208     then show "P k" by (cases "k = i") simp_all
  5209   qed
  5210   show ?thesis by (auto simp add: all_interval_int_def intro: *)
  5211 qed
  5212 
  5213 lemma list_all_iff_all_interval_int [code_unfold]:
  5214   "list_all P [i..j] \<longleftrightarrow> all_interval_int P i j"
  5215   by (simp add: list_all_iff all_interval_int_def)
  5216 
  5217 lemma list_ex_iff_not_all_inverval_int [code_unfold]:
  5218   "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"
  5219   by (simp add: list_ex_iff all_interval_int_def)
  5220 
  5221 hide_const (open) member null maps map_filter all_interval_nat all_interval_int
  5222 
  5223 
  5224 subsubsection {* Pretty lists *}
  5225 
  5226 use "Tools/list_code.ML"
  5227 
  5228 code_type list
  5229   (SML "_ list")
  5230   (OCaml "_ list")
  5231   (Haskell "![(_)]")
  5232   (Scala "List[(_)]")
  5233 
  5234 code_const Nil
  5235   (SML "[]")
  5236   (OCaml "[]")
  5237   (Haskell "[]")
  5238   (Scala "!Nil")
  5239 
  5240 code_instance list :: equal
  5241   (Haskell -)
  5242 
  5243 code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
  5244   (Haskell infix 4 "==")
  5245 
  5246 code_reserved SML
  5247   list
  5248 
  5249 code_reserved OCaml
  5250   list
  5251 
  5252 types_code
  5253   "list" ("_ list")
  5254 attach (term_of) {*
  5255 fun term_of_list f T = HOLogic.mk_list T o map f;
  5256 *}
  5257 attach (test) {*
  5258 fun gen_list' aG aT i j = frequency
  5259   [(i, fn () =>
  5260       let
  5261         val (x, t) = aG j;
  5262         val (xs, ts) = gen_list' aG aT (i-1) j
  5263       in (x :: xs, fn () => HOLogic.cons_const aT $ t () $ ts ()) end),
  5264    (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()
  5265 and gen_list aG aT i = gen_list' aG aT i i;
  5266 *}
  5267 
  5268 consts_code Cons ("(_ ::/ _)")
  5269 
  5270 setup {*
  5271 let
  5272   fun list_codegen thy mode defs dep thyname b t gr =
  5273     let
  5274       val ts = HOLogic.dest_list t;
  5275       val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
  5276         (fastype_of t) gr;
  5277       val (ps, gr'') = fold_map
  5278         (Codegen.invoke_codegen thy mode defs dep thyname false) ts gr'
  5279     in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
  5280 in
  5281   fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
  5282   #> Codegen.add_codegen "list_codegen" list_codegen
  5283 end
  5284 *}
  5285 
  5286 
  5287 subsubsection {* Use convenient predefined operations *}
  5288 
  5289 code_const "op @"
  5290   (SML infixr 7 "@")
  5291   (OCaml infixr 6 "@")
  5292   (Haskell infixr 5 "++")
  5293   (Scala infixl 7 "++")
  5294 
  5295 code_const map
  5296   (Haskell "map")
  5297 
  5298 code_const filter
  5299   (Haskell "filter")
  5300 
  5301 code_const concat
  5302   (Haskell "concat")
  5303 
  5304 code_const List.maps
  5305   (Haskell "concatMap")
  5306 
  5307 code_const rev
  5308   (Haskell "reverse")
  5309 
  5310 code_const zip
  5311   (Haskell "zip")
  5312 
  5313 code_const List.null
  5314   (Haskell "null")
  5315 
  5316 code_const takeWhile
  5317   (Haskell "takeWhile")
  5318 
  5319 code_const dropWhile
  5320   (Haskell "dropWhile")
  5321 
  5322 code_const hd
  5323   (Haskell "head")
  5324 
  5325 code_const last
  5326   (Haskell "last")
  5327 
  5328 code_const list_all
  5329   (Haskell "all")
  5330 
  5331 code_const list_ex
  5332   (Haskell "any")
  5333 
  5334 end