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