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