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