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