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