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