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