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