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