src/HOL/List.thy
 author haftmann Mon Jul 12 10:48:37 2010 +0200 (2010-07-12) changeset 37767 a2b7a20d6ea3 parent 37605 625bc011768a child 37880 3b9ca8d2c5fb permissions -rw-r--r--
dropped superfluous [code del]s
     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 Quotient Presburger Code_Numeral Sledgehammer Recdef

     9 uses ("Tools/list_code.ML")

    10 begin

    11

    12 datatype 'a list =

    13     Nil    ("[]")

    14   | Cons 'a  "'a list"    (infixr "#" 65)

    15

    16 syntax

    17   -- {* list Enumeration *}

    18   "_list" :: "args => 'a list"    ("[(_)]")

    19

    20 translations

    21   "[x, xs]" == "x#[xs]"

    22   "[x]" == "x#[]"

    23

    24

    25 subsection {* Basic list processing functions *}

    26

    27 primrec

    28   hd :: "'a list \<Rightarrow> 'a" where

    29   "hd (x # xs) = x"

    30

    31 primrec

    32   tl :: "'a list \<Rightarrow> 'a list" where

    33     "tl [] = []"

    34   | "tl (x # xs) = xs"

    35

    36 primrec

    37   last :: "'a list \<Rightarrow> 'a" where

    38   "last (x # xs) = (if xs = [] then x else last xs)"

    39

    40 primrec

    41   butlast :: "'a list \<Rightarrow> 'a list" where

    42     "butlast []= []"

    43   | "butlast (x # xs) = (if xs = [] then [] else x # butlast xs)"

    44

    45 primrec

    46   set :: "'a list \<Rightarrow> 'a set" where

    47     "set [] = {}"

    48   | "set (x # xs) = insert x (set xs)"

    49

    50 primrec

    51   map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list" where

    52     "map f [] = []"

    53   | "map f (x # xs) = f x # map f xs"

    54

    55 primrec

    56   append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65) where

    57     append_Nil:"[] @ ys = ys"

    58   | append_Cons: "(x#xs) @ ys = x # xs @ ys"

    59

    60 primrec

    61   rev :: "'a list \<Rightarrow> 'a list" where

    62     "rev [] = []"

    63   | "rev (x # xs) = rev xs @ [x]"

    64

    65 primrec

    66   filter:: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where

    67     "filter P [] = []"

    68   | "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"

    69

    70 syntax

    71   -- {* Special syntax for filter *}

    72   "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")

    73

    74 translations

    75   "[x<-xs . P]"== "CONST filter (%x. P) xs"

    76

    77 syntax (xsymbols)

    78   "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")

    79 syntax (HTML output)

    80   "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")

    81

    82 primrec

    83   foldl :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b" where

    84     foldl_Nil: "foldl f a [] = a"

    85   | foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"

    86

    87 primrec

    88   foldr :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where

    89     "foldr f [] a = a"

    90   | "foldr f (x # xs) a = f x (foldr f xs a)"

    91

    92 primrec

    93   concat:: "'a list list \<Rightarrow> 'a list" where

    94     "concat [] = []"

    95   | "concat (x # xs) = x @ concat xs"

    96

    97 primrec (in monoid_add)

    98   listsum :: "'a list \<Rightarrow> 'a" where

    99     "listsum [] = 0"

   100   | "listsum (x # xs) = x + listsum xs"

   101

   102 primrec

   103   drop:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   104     drop_Nil: "drop n [] = []"

   105   | drop_Cons: "drop n (x # xs) = (case n of 0 \<Rightarrow> x # xs | Suc m \<Rightarrow> drop m xs)"

   106   -- {*Warning: simpset does not contain this definition, but separate

   107        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}

   108

   109 primrec

   110   take:: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   111     take_Nil:"take n [] = []"

   112   | take_Cons: "take n (x # xs) = (case n of 0 \<Rightarrow> [] | Suc m \<Rightarrow> x # take m xs)"

   113   -- {*Warning: simpset does not contain this definition, but separate

   114        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}

   115

   116 primrec

   117   nth :: "'a list => nat => 'a" (infixl "!" 100) where

   118   nth_Cons: "(x # xs) ! n = (case n of 0 \<Rightarrow> x | Suc k \<Rightarrow> xs ! k)"

   119   -- {*Warning: simpset does not contain this definition, but separate

   120        theorems for @{text "n = 0"} and @{text "n = Suc k"} *}

   121

   122 primrec

   123   list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list" where

   124     "list_update [] i v = []"

   125   | "list_update (x # xs) i v = (case i of 0 \<Rightarrow> v # xs | Suc j \<Rightarrow> x # list_update xs j v)"

   126

   127 nonterminals lupdbinds lupdbind

   128

   129 syntax

   130   "_lupdbind":: "['a, 'a] => lupdbind"    ("(2_ :=/ _)")

   131   "" :: "lupdbind => lupdbinds"    ("_")

   132   "_lupdbinds" :: "[lupdbind, lupdbinds] => lupdbinds"    ("_,/ _")

   133   "_LUpdate" :: "['a, lupdbinds] => 'a"    ("_/[(_)]" [900,0] 900)

   134

   135 translations

   136   "_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"

   137   "xs[i:=x]" == "CONST list_update xs i x"

   138

   139 primrec

   140   takeWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   141     "takeWhile P [] = []"

   142   | "takeWhile P (x # xs) = (if P x then x # takeWhile P xs else [])"

   143

   144 primrec

   145   dropWhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   146     "dropWhile P [] = []"

   147   | "dropWhile P (x # xs) = (if P x then dropWhile P xs else x # xs)"

   148

   149 primrec

   150   zip :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a \<times> 'b) list" where

   151     "zip xs [] = []"

   152   | zip_Cons: "zip xs (y # ys) = (case xs of [] => [] | z # zs => (z, y) # zip zs ys)"

   153   -- {*Warning: simpset does not contain this definition, but separate

   154        theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}

   155

   156 primrec

   157   upt :: "nat \<Rightarrow> nat \<Rightarrow> nat list" ("(1[_..</_'])") where

   158     upt_0: "[i..<0] = []"

   159   | upt_Suc: "[i..<(Suc j)] = (if i <= j then [i..<j] @ [j] else [])"

   160

   161 primrec

   162   distinct :: "'a list \<Rightarrow> bool" where

   163     "distinct [] \<longleftrightarrow> True"

   164   | "distinct (x # xs) \<longleftrightarrow> x \<notin> set xs \<and> distinct xs"

   165

   166 primrec

   167   remdups :: "'a list \<Rightarrow> 'a list" where

   168     "remdups [] = []"

   169   | "remdups (x # xs) = (if x \<in> set xs then remdups xs else x # remdups xs)"

   170

   171 definition

   172   insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   173   "insert x xs = (if x \<in> set xs then xs else x # xs)"

   174

   175 hide_const (open) insert

   176 hide_fact (open) insert_def

   177

   178 primrec

   179   remove1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   180     "remove1 x [] = []"

   181   | "remove1 x (y # xs) = (if x = y then xs else y # remove1 x xs)"

   182

   183 primrec

   184   removeAll :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   185     "removeAll x [] = []"

   186   | "removeAll x (y # xs) = (if x = y then removeAll x xs else y # removeAll x xs)"

   187

   188 primrec

   189   replicate :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list" where

   190     replicate_0: "replicate 0 x = []"

   191   | replicate_Suc: "replicate (Suc n) x = x # replicate n x"

   192

   193 text {*

   194   Function @{text size} is overloaded for all datatypes. Users may

   195   refer to the list version as @{text length}. *}

   196

   197 abbreviation

   198   length :: "'a list \<Rightarrow> nat" where

   199   "length \<equiv> size"

   200

   201 definition

   202   rotate1 :: "'a list \<Rightarrow> 'a list" where

   203   "rotate1 xs = (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"

   204

   205 definition

   206   rotate :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   207   "rotate n = rotate1 ^^ n"

   208

   209 definition

   210   list_all2 :: "('a => 'b => bool) => 'a list => 'b list => bool" where

   211   "list_all2 P xs ys =

   212     (length xs = length ys \<and> (\<forall>(x, y) \<in> set (zip xs ys). P x y))"

   213

   214 definition

   215   sublist :: "'a list => nat set => 'a list" where

   216   "sublist xs A = map fst (filter (\<lambda>p. snd p \<in> A) (zip xs [0..<size xs]))"

   217

   218 primrec

   219   splice :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   220     "splice [] ys = ys"

   221   | "splice (x # xs) ys = (if ys = [] then x # xs else x # hd ys # splice xs (tl ys))"

   222     -- {*Warning: simpset does not contain the second eqn but a derived one. *}

   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 nat_number')}\\

   262 @{lemma "replicate 4 a = [a,a,a,a]" by (simp add:nat_number')}\\

   263 @{lemma "[2..<5] = [2,3,4]" by (simp add:nat_number')}\\

   264 @{lemma "listsum [1,2,3::nat] = 6" by simp}

   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 fun sorted :: "'a list \<Rightarrow> bool" where

   280 "sorted [] \<longleftrightarrow> True" |

   281 "sorted [x] \<longleftrightarrow> True" |

   282 "sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"

   283

   284 primrec insort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where

   285 "insort_key f x [] = [x]" |

   286 "insort_key f x (y#ys) = (if f x \<le> f y then (x#y#ys) else y#(insort_key f x ys))"

   287

   288 definition sort_key :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list" where

   289 "sort_key f xs = foldr (insort_key f) xs []"

   290

   291 abbreviation "sort \<equiv> sort_key (\<lambda>x. x)"

   292 abbreviation "insort \<equiv> insort_key (\<lambda>x. x)"

   293

   294 definition insort_insert :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where

   295   "insort_insert x xs = (if x \<in> set xs then xs else insort x xs)"

   296

   297 end

   298

   299

   300 subsubsection {* List comprehension *}

   301

   302 text{* Input syntax for Haskell-like list comprehension notation.

   303 Typical example: @{text"[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x \<noteq> y]"},

   304 the list of all pairs of distinct elements from @{text xs} and @{text ys}.

   305 The syntax is as in Haskell, except that @{text"|"} becomes a dot

   306 (like in Isabelle's set comprehension): @{text"[e. x \<leftarrow> xs, \<dots>]"} rather than

   307 \verb![e| x <- xs, ...]!.

   308

   309 The qualifiers after the dot are

   310 \begin{description}

   311 \item[generators] @{text"p \<leftarrow> xs"},

   312  where @{text p} is a pattern and @{text xs} an expression of list type, or

   313 \item[guards] @{text"b"}, where @{text b} is a boolean expression.

   314 %\item[local bindings] @ {text"let x = e"}.

   315 \end{description}

   316

   317 Just like in Haskell, list comprehension is just a shorthand. To avoid

   318 misunderstandings, the translation into desugared form is not reversed

   319 upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is

   320 optmized to @{term"map (%x. e) xs"}.

   321

   322 It is easy to write short list comprehensions which stand for complex

   323 expressions. During proofs, they may become unreadable (and

   324 mangled). In such cases it can be advisable to introduce separate

   325 definitions for the list comprehensions in question.  *}

   326

   327 (*

   328 Proper theorem proving support would be nice. For example, if

   329 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"}

   330 produced something like

   331 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}.

   332 *)

   333

   334 nonterminals lc_qual lc_quals

   335

   336 syntax

   337 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")

   338 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")

   339 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")

   340 (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)

   341 "_lc_end" :: "lc_quals" ("]")

   342 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")

   343 "_lc_abs" :: "'a => 'b list => 'b list"

   344

   345 (* These are easier than ML code but cannot express the optimized

   346    translation of [e. p<-xs]

   347 translations

   348 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"

   349 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"

   350  => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"

   351 "[e. P]" => "if P then [e] else []"

   352 "_listcompr e (_lc_test P) (_lc_quals Q Qs)"

   353  => "if P then (_listcompr e Q Qs) else []"

   354 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"

   355  => "_Let b (_listcompr e Q Qs)"

   356 *)

   357

   358 syntax (xsymbols)

   359 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")

   360 syntax (HTML output)

   361 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")

   362

   363 parse_translation (advanced) {*

   364 let

   365   val NilC = Syntax.const @{const_syntax Nil};

   366   val ConsC = Syntax.const @{const_syntax Cons};

   367   val mapC = Syntax.const @{const_syntax map};

   368   val concatC = Syntax.const @{const_syntax concat};

   369   val IfC = Syntax.const @{const_syntax If};

   370

   371   fun singl x = ConsC $x$ NilC;

   372

   373   fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)

   374     let

   375       val x = Free (Name.variant (fold Term.add_free_names [p, e] []) "x", dummyT);

   376       val e = if opti then singl e else e;

   377       val case1 = Syntax.const @{syntax_const "_case1"} $p$ e;

   378       val case2 =

   379         Syntax.const @{syntax_const "_case1"} $  380 Syntax.const @{const_syntax dummy_pattern}$ NilC;

   381       val cs = Syntax.const @{syntax_const "_case2"} $case1$ case2;

   382       val ft = Datatype_Case.case_tr false Datatype.info_of_constr ctxt [x, cs];

   383     in lambda x ft end;

   384

   385   fun abs_tr ctxt (p as Free (s, T)) e opti =

   386         let

   387           val thy = ProofContext.theory_of ctxt;

   388           val s' = Sign.intern_const thy s;

   389         in

   390           if Sign.declared_const thy s'

   391           then (pat_tr ctxt p e opti, false)

   392           else (lambda p e, true)

   393         end

   394     | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);

   395

   396   fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $b, qs] =   397 let   398 val res =   399 (case qs of   400 Const (@{syntax_const "_lc_end"}, _) => singl e   401 | Const (@{syntax_const "_lc_quals"}, _)$ q $qs => lc_tr ctxt [e, q, qs]);   402 in IfC$ b $res$ NilC end

   403     | lc_tr ctxt

   404           [e, Const (@{syntax_const "_lc_gen"}, _) $p$ es,

   405             Const(@{syntax_const "_lc_end"}, _)] =

   406         (case abs_tr ctxt p e true of

   407           (f, true) => mapC $f$ es

   408         | (f, false) => concatC $(mapC$ f $es))   409 | lc_tr ctxt   410 [e, Const (@{syntax_const "_lc_gen"}, _)$ p $es,   411 Const (@{syntax_const "_lc_quals"}, _)$ q $qs] =   412 let val e' = lc_tr ctxt [e, q, qs];   413 in concatC$ (mapC $(fst (abs_tr ctxt p e' false))$ es) end;

   414

   415 in [(@{syntax_const "_listcompr"}, lc_tr)] end

   416 *}

   417

   418 term "[(x,y,z). b]"

   419 term "[(x,y,z). x\<leftarrow>xs]"

   420 term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"

   421 term "[(x,y,z). x<a, x>b]"

   422 term "[(x,y,z). x\<leftarrow>xs, x>b]"

   423 term "[(x,y,z). x<a, x\<leftarrow>xs]"

   424 term "[(x,y). Cons True x \<leftarrow> xs]"

   425 term "[(x,y,z). Cons x [] \<leftarrow> xs]"

   426 term "[(x,y,z). x<a, x>b, x=d]"

   427 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"

   428 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"

   429 term "[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]"

   430 term "[(x,y,z). x\<leftarrow>xs, x>b, y<a]"

   431 term "[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]"

   432 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]"

   433 term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]"

   434 (*

   435 term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"

   436 *)

   437

   438

   439 subsubsection {* @{const Nil} and @{const Cons} *}

   440

   441 lemma not_Cons_self [simp]:

   442   "xs \<noteq> x # xs"

   443 by (induct xs) auto

   444

   445 lemmas not_Cons_self2 [simp] = not_Cons_self [symmetric]

   446

   447 lemma neq_Nil_conv: "(xs \<noteq> []) = (\<exists>y ys. xs = y # ys)"

   448 by (induct xs) auto

   449

   450 lemma length_induct:

   451   "(\<And>xs. \<forall>ys. length ys < length xs \<longrightarrow> P ys \<Longrightarrow> P xs) \<Longrightarrow> P xs"

   452 by (rule measure_induct [of length]) iprover

   453

   454 lemma list_nonempty_induct [consumes 1, case_names single cons]:

   455   assumes "xs \<noteq> []"

   456   assumes single: "\<And>x. P [x]"

   457   assumes cons: "\<And>x xs. xs \<noteq> [] \<Longrightarrow> P xs \<Longrightarrow> P (x # xs)"

   458   shows "P xs"

   459 using xs \<noteq> [] proof (induct xs)

   460   case Nil then show ?case by simp

   461 next

   462   case (Cons x xs) show ?case proof (cases xs)

   463     case Nil with single show ?thesis by simp

   464   next

   465     case Cons then have "xs \<noteq> []" by simp

   466     moreover with Cons.hyps have "P xs" .

   467     ultimately show ?thesis by (rule cons)

   468   qed

   469 qed

   470

   471

   472 subsubsection {* @{const length} *}

   473

   474 text {*

   475   Needs to come before @{text "@"} because of theorem @{text

   476   append_eq_append_conv}.

   477 *}

   478

   479 lemma length_append [simp]: "length (xs @ ys) = length xs + length ys"

   480 by (induct xs) auto

   481

   482 lemma length_map [simp]: "length (map f xs) = length xs"

   483 by (induct xs) auto

   484

   485 lemma length_rev [simp]: "length (rev xs) = length xs"

   486 by (induct xs) auto

   487

   488 lemma length_tl [simp]: "length (tl xs) = length xs - 1"

   489 by (cases xs) auto

   490

   491 lemma length_0_conv [iff]: "(length xs = 0) = (xs = [])"

   492 by (induct xs) auto

   493

   494 lemma length_greater_0_conv [iff]: "(0 < length xs) = (xs \<noteq> [])"

   495 by (induct xs) auto

   496

   497 lemma length_pos_if_in_set: "x : set xs \<Longrightarrow> length xs > 0"

   498 by auto

   499

   500 lemma length_Suc_conv:

   501 "(length xs = Suc n) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"

   502 by (induct xs) auto

   503

   504 lemma Suc_length_conv:

   505 "(Suc n = length xs) = (\<exists>y ys. xs = y # ys \<and> length ys = n)"

   506 apply (induct xs, simp, simp)

   507 apply blast

   508 done

   509

   510 lemma impossible_Cons: "length xs <= length ys ==> xs = x # ys = False"

   511   by (induct xs) auto

   512

   513 lemma list_induct2 [consumes 1, case_names Nil Cons]:

   514   "length xs = length ys \<Longrightarrow> P [] [] \<Longrightarrow>

   515    (\<And>x xs y ys. length xs = length ys \<Longrightarrow> P xs ys \<Longrightarrow> P (x#xs) (y#ys))

   516    \<Longrightarrow> P xs ys"

   517 proof (induct xs arbitrary: ys)

   518   case Nil then show ?case by simp

   519 next

   520   case (Cons x xs ys) then show ?case by (cases ys) simp_all

   521 qed

   522

   523 lemma list_induct3 [consumes 2, case_names Nil Cons]:

   524   "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> P [] [] [] \<Longrightarrow>

   525    (\<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))

   526    \<Longrightarrow> P xs ys zs"

   527 proof (induct xs arbitrary: ys zs)

   528   case Nil then show ?case by simp

   529 next

   530   case (Cons x xs ys zs) then show ?case by (cases ys, simp_all)

   531     (cases zs, simp_all)

   532 qed

   533

   534 lemma list_induct4 [consumes 3, case_names Nil Cons]:

   535   "length xs = length ys \<Longrightarrow> length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow>

   536    P [] [] [] [] \<Longrightarrow> (\<And>x xs y ys z zs w ws. length xs = length ys \<Longrightarrow>

   537    length ys = length zs \<Longrightarrow> length zs = length ws \<Longrightarrow> P xs ys zs ws \<Longrightarrow>

   538    P (x#xs) (y#ys) (z#zs) (w#ws)) \<Longrightarrow> P xs ys zs ws"

   539 proof (induct xs arbitrary: ys zs ws)

   540   case Nil then show ?case by simp

   541 next

   542   case (Cons x xs ys zs ws) then show ?case by ((cases ys, simp_all), (cases zs,simp_all)) (cases ws, simp_all)

   543 qed

   544

   545 lemma list_induct2':

   546   "\<lbrakk> P [] [];

   547   \<And>x xs. P (x#xs) [];

   548   \<And>y ys. P [] (y#ys);

   549    \<And>x xs y ys. P xs ys  \<Longrightarrow> P (x#xs) (y#ys) \<rbrakk>

   550  \<Longrightarrow> P xs ys"

   551 by (induct xs arbitrary: ys) (case_tac x, auto)+

   552

   553 lemma neq_if_length_neq: "length xs \<noteq> length ys \<Longrightarrow> (xs = ys) == False"

   554 by (rule Eq_FalseI) auto

   555

   556 simproc_setup list_neq ("(xs::'a list) = ys") = {*

   557 (*

   558 Reduces xs=ys to False if xs and ys cannot be of the same length.

   559 This is the case if the atomic sublists of one are a submultiset

   560 of those of the other list and there are fewer Cons's in one than the other.

   561 *)

   562

   563 let

   564

   565 fun len (Const(@{const_name Nil},_)) acc = acc

   566   | len (Const(@{const_name Cons},_) $_$ xs) (ts,n) = len xs (ts,n+1)

   567   | len (Const(@{const_name append},_) $xs$ ys) acc = len xs (len ys acc)

   568   | len (Const(@{const_name rev},_) $xs) acc = len xs acc   569 | len (Const(@{const_name map},_)$ _ $xs) acc = len xs acc   570 | len t (ts,n) = (t::ts,n);   571   572 fun list_neq _ ss ct =   573 let   574 val (Const(_,eqT)$ lhs $rhs) = Thm.term_of ct;   575 val (ls,m) = len lhs ([],0) and (rs,n) = len rhs ([],0);   576 fun prove_neq() =   577 let   578 val Type(_,listT::_) = eqT;   579 val size = HOLogic.size_const listT;   580 val eq_len = HOLogic.mk_eq (size$ lhs, size $rhs);   581 val neq_len = HOLogic.mk_Trueprop (HOLogic.Not$ eq_len);

   582         val thm = Goal.prove (Simplifier.the_context ss) [] [] neq_len

   583           (K (simp_tac (Simplifier.inherit_context ss @{simpset}) 1));

   584       in SOME (thm RS @{thm neq_if_length_neq}) end

   585   in

   586     if m < n andalso submultiset (op aconv) (ls,rs) orelse

   587        n < m andalso submultiset (op aconv) (rs,ls)

   588     then prove_neq() else NONE

   589   end;

   590 in list_neq end;

   591 *}

   592

   593

   594 subsubsection {* @{text "@"} -- append *}

   595

   596 lemma append_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"

   597 by (induct xs) auto

   598

   599 lemma append_Nil2 [simp]: "xs @ [] = xs"

   600 by (induct xs) auto

   601

   602 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"

   603 by (induct xs) auto

   604

   605 lemma Nil_is_append_conv [iff]: "([] = xs @ ys) = (xs = [] \<and> ys = [])"

   606 by (induct xs) auto

   607

   608 lemma append_self_conv [iff]: "(xs @ ys = xs) = (ys = [])"

   609 by (induct xs) auto

   610

   611 lemma self_append_conv [iff]: "(xs = xs @ ys) = (ys = [])"

   612 by (induct xs) auto

   613

   614 lemma append_eq_append_conv [simp, no_atp]:

   615  "length xs = length ys \<or> length us = length vs

   616  ==> (xs@us = ys@vs) = (xs=ys \<and> us=vs)"

   617 apply (induct xs arbitrary: ys)

   618  apply (case_tac ys, simp, force)

   619 apply (case_tac ys, force, simp)

   620 done

   621

   622 lemma append_eq_append_conv2: "(xs @ ys = zs @ ts) =

   623   (EX us. xs = zs @ us & us @ ys = ts | xs @ us = zs & ys = us@ ts)"

   624 apply (induct xs arbitrary: ys zs ts)

   625  apply fastsimp

   626 apply(case_tac zs)

   627  apply simp

   628 apply fastsimp

   629 done

   630

   631 lemma same_append_eq [iff, induct_simp]: "(xs @ ys = xs @ zs) = (ys = zs)"

   632 by simp

   633

   634 lemma append1_eq_conv [iff]: "(xs @ [x] = ys @ [y]) = (xs = ys \<and> x = y)"

   635 by simp

   636

   637 lemma append_same_eq [iff, induct_simp]: "(ys @ xs = zs @ xs) = (ys = zs)"

   638 by simp

   639

   640 lemma append_self_conv2 [iff]: "(xs @ ys = ys) = (xs = [])"

   641 using append_same_eq [of _ _ "[]"] by auto

   642

   643 lemma self_append_conv2 [iff]: "(ys = xs @ ys) = (xs = [])"

   644 using append_same_eq [of "[]"] by auto

   645

   646 lemma hd_Cons_tl [simp,no_atp]: "xs \<noteq> [] ==> hd xs # tl xs = xs"

   647 by (induct xs) auto

   648

   649 lemma hd_append: "hd (xs @ ys) = (if xs = [] then hd ys else hd xs)"

   650 by (induct xs) auto

   651

   652 lemma hd_append2 [simp]: "xs \<noteq> [] ==> hd (xs @ ys) = hd xs"

   653 by (simp add: hd_append split: list.split)

   654

   655 lemma tl_append: "tl (xs @ ys) = (case xs of [] => tl ys | z#zs => zs @ ys)"

   656 by (simp split: list.split)

   657

   658 lemma tl_append2 [simp]: "xs \<noteq> [] ==> tl (xs @ ys) = tl xs @ ys"

   659 by (simp add: tl_append split: list.split)

   660

   661

   662 lemma Cons_eq_append_conv: "x#xs = ys@zs =

   663  (ys = [] & x#xs = zs | (EX ys'. x#ys' = ys & xs = ys'@zs))"

   664 by(cases ys) auto

   665

   666 lemma append_eq_Cons_conv: "(ys@zs = x#xs) =

   667  (ys = [] & zs = x#xs | (EX ys'. ys = x#ys' & ys'@zs = xs))"

   668 by(cases ys) auto

   669

   670

   671 text {* Trivial rules for solving @{text "@"}-equations automatically. *}

   672

   673 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"

   674 by simp

   675

   676 lemma Cons_eq_appendI:

   677 "[| x # xs1 = ys; xs = xs1 @ zs |] ==> x # xs = ys @ zs"

   678 by (drule sym) simp

   679

   680 lemma append_eq_appendI:

   681 "[| xs @ xs1 = zs; ys = xs1 @ us |] ==> xs @ ys = zs @ us"

   682 by (drule sym) simp

   683

   684

   685 text {*

   686 Simplification procedure for all list equalities.

   687 Currently only tries to rearrange @{text "@"} to see if

   688 - both lists end in a singleton list,

   689 - or both lists end in the same list.

   690 *}

   691

   692 ML {*

   693 local

   694

   695 fun last (cons as Const(@{const_name Cons},_) $_$ xs) =

   696   (case xs of Const(@{const_name Nil},_) => cons | _ => last xs)

   697   | last (Const(@{const_name append},_) $_$ ys) = last ys

   698   | last t = t;

   699

   700 fun list1 (Const(@{const_name Cons},_) $_$ Const(@{const_name Nil},_)) = true

   701   | list1 _ = false;

   702

   703 fun butlast ((cons as Const(@{const_name Cons},_) $x)$ xs) =

   704   (case xs of Const(@{const_name Nil},_) => xs | _ => cons $butlast xs)   705 | butlast ((app as Const(@{const_name append},_)$ xs) $ys) = app$ butlast ys

   706   | butlast xs = Const(@{const_name Nil},fastype_of xs);

   707

   708 val rearr_ss = HOL_basic_ss addsimps [@{thm append_assoc},

   709   @{thm append_Nil}, @{thm append_Cons}];

   710

   711 fun list_eq ss (F as (eq as Const(_,eqT)) $lhs$ rhs) =

   712   let

   713     val lastl = last lhs and lastr = last rhs;

   714     fun rearr conv =

   715       let

   716         val lhs1 = butlast lhs and rhs1 = butlast rhs;

   717         val Type(_,listT::_) = eqT

   718         val appT = [listT,listT] ---> listT

   719         val app = Const(@{const_name append},appT)

   720         val F2 = eq $(app$lhs1$lastl)$ (app$rhs1$lastr)

   721         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));

   722         val thm = Goal.prove (Simplifier.the_context ss) [] [] eq

   723           (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));

   724       in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;

   725

   726   in

   727     if list1 lastl andalso list1 lastr then rearr @{thm append1_eq_conv}

   728     else if lastl aconv lastr then rearr @{thm append_same_eq}

   729     else NONE

   730   end;

   731

   732 in

   733

   734 val list_eq_simproc =

   735   Simplifier.simproc @{theory} "list_eq" ["(xs::'a list) = ys"] (K list_eq);

   736

   737 end;

   738

   739 Addsimprocs [list_eq_simproc];

   740 *}

   741

   742

   743 subsubsection {* @{text map} *}

   744

   745 lemma map_ext: "(!!x. x : set xs --> f x = g x) ==> map f xs = map g xs"

   746 by (induct xs) simp_all

   747

   748 lemma map_ident [simp]: "map (\<lambda>x. x) = (\<lambda>xs. xs)"

   749 by (rule ext, induct_tac xs) auto

   750

   751 lemma map_append [simp]: "map f (xs @ ys) = map f xs @ map f ys"

   752 by (induct xs) auto

   753

   754 lemma map_map [simp]: "map f (map g xs) = map (f \<circ> g) xs"

   755 by (induct xs) auto

   756

   757 lemma map_comp_map[simp]: "((map f) o (map g)) = map(f o g)"

   758 apply(rule ext)

   759 apply(simp)

   760 done

   761

   762 lemma rev_map: "rev (map f xs) = map f (rev xs)"

   763 by (induct xs) auto

   764

   765 lemma map_eq_conv[simp]: "(map f xs = map g xs) = (!x : set xs. f x = g x)"

   766 by (induct xs) auto

   767

   768 lemma map_cong [fundef_cong, recdef_cong]:

   769 "xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> map f xs = map g ys"

   770 -- {* a congruence rule for @{text map} *}

   771 by simp

   772

   773 lemma map_is_Nil_conv [iff]: "(map f xs = []) = (xs = [])"

   774 by (cases xs) auto

   775

   776 lemma Nil_is_map_conv [iff]: "([] = map f xs) = (xs = [])"

   777 by (cases xs) auto

   778

   779 lemma map_eq_Cons_conv:

   780  "(map f xs = y#ys) = (\<exists>z zs. xs = z#zs \<and> f z = y \<and> map f zs = ys)"

   781 by (cases xs) auto

   782

   783 lemma Cons_eq_map_conv:

   784  "(x#xs = map f ys) = (\<exists>z zs. ys = z#zs \<and> x = f z \<and> xs = map f zs)"

   785 by (cases ys) auto

   786

   787 lemmas map_eq_Cons_D = map_eq_Cons_conv [THEN iffD1]

   788 lemmas Cons_eq_map_D = Cons_eq_map_conv [THEN iffD1]

   789 declare map_eq_Cons_D [dest!]  Cons_eq_map_D [dest!]

   790

   791 lemma ex_map_conv:

   792   "(EX xs. ys = map f xs) = (ALL y : set ys. EX x. y = f x)"

   793 by(induct ys, auto simp add: Cons_eq_map_conv)

   794

   795 lemma map_eq_imp_length_eq:

   796   assumes "map f xs = map g ys"

   797   shows "length xs = length ys"

   798 using assms proof (induct ys arbitrary: xs)

   799   case Nil then show ?case by simp

   800 next

   801   case (Cons y ys) then obtain z zs where xs: "xs = z # zs" by auto

   802   from Cons xs have "map f zs = map g ys" by simp

   803   moreover with Cons have "length zs = length ys" by blast

   804   with xs show ?case by simp

   805 qed

   806

   807 lemma map_inj_on:

   808  "[| map f xs = map f ys; inj_on f (set xs Un set ys) |]

   809   ==> xs = ys"

   810 apply(frule map_eq_imp_length_eq)

   811 apply(rotate_tac -1)

   812 apply(induct rule:list_induct2)

   813  apply simp

   814 apply(simp)

   815 apply (blast intro:sym)

   816 done

   817

   818 lemma inj_on_map_eq_map:

   819  "inj_on f (set xs Un set ys) \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"

   820 by(blast dest:map_inj_on)

   821

   822 lemma map_injective:

   823  "map f xs = map f ys ==> inj f ==> xs = ys"

   824 by (induct ys arbitrary: xs) (auto dest!:injD)

   825

   826 lemma inj_map_eq_map[simp]: "inj f \<Longrightarrow> (map f xs = map f ys) = (xs = ys)"

   827 by(blast dest:map_injective)

   828

   829 lemma inj_mapI: "inj f ==> inj (map f)"

   830 by (iprover dest: map_injective injD intro: inj_onI)

   831

   832 lemma inj_mapD: "inj (map f) ==> inj f"

   833 apply (unfold inj_on_def, clarify)

   834 apply (erule_tac x = "[x]" in ballE)

   835  apply (erule_tac x = "[y]" in ballE, simp, blast)

   836 apply blast

   837 done

   838

   839 lemma inj_map[iff]: "inj (map f) = inj f"

   840 by (blast dest: inj_mapD intro: inj_mapI)

   841

   842 lemma inj_on_mapI: "inj_on f (\<Union>(set  A)) \<Longrightarrow> inj_on (map f) A"

   843 apply(rule inj_onI)

   844 apply(erule map_inj_on)

   845 apply(blast intro:inj_onI dest:inj_onD)

   846 done

   847

   848 lemma map_idI: "(\<And>x. x \<in> set xs \<Longrightarrow> f x = x) \<Longrightarrow> map f xs = xs"

   849 by (induct xs, auto)

   850

   851 lemma map_fun_upd [simp]: "y \<notin> set xs \<Longrightarrow> map (f(y:=v)) xs = map f xs"

   852 by (induct xs) auto

   853

   854 lemma map_fst_zip[simp]:

   855   "length xs = length ys \<Longrightarrow> map fst (zip xs ys) = xs"

   856 by (induct rule:list_induct2, simp_all)

   857

   858 lemma map_snd_zip[simp]:

   859   "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"

   860 by (induct rule:list_induct2, simp_all)

   861

   862

   863 subsubsection {* @{text rev} *}

   864

   865 lemma rev_append [simp]: "rev (xs @ ys) = rev ys @ rev xs"

   866 by (induct xs) auto

   867

   868 lemma rev_rev_ident [simp]: "rev (rev xs) = xs"

   869 by (induct xs) auto

   870

   871 lemma rev_swap: "(rev xs = ys) = (xs = rev ys)"

   872 by auto

   873

   874 lemma rev_is_Nil_conv [iff]: "(rev xs = []) = (xs = [])"

   875 by (induct xs) auto

   876

   877 lemma Nil_is_rev_conv [iff]: "([] = rev xs) = (xs = [])"

   878 by (induct xs) auto

   879

   880 lemma rev_singleton_conv [simp]: "(rev xs = [x]) = (xs = [x])"

   881 by (cases xs) auto

   882

   883 lemma singleton_rev_conv [simp]: "([x] = rev xs) = (xs = [x])"

   884 by (cases xs) auto

   885

   886 lemma rev_is_rev_conv [iff]: "(rev xs = rev ys) = (xs = ys)"

   887 apply (induct xs arbitrary: ys, force)

   888 apply (case_tac ys, simp, force)

   889 done

   890

   891 lemma inj_on_rev[iff]: "inj_on rev A"

   892 by(simp add:inj_on_def)

   893

   894 lemma rev_induct [case_names Nil snoc]:

   895   "[| P []; !!x xs. P xs ==> P (xs @ [x]) |] ==> P xs"

   896 apply(simplesubst rev_rev_ident[symmetric])

   897 apply(rule_tac list = "rev xs" in list.induct, simp_all)

   898 done

   899

   900 lemma rev_exhaust [case_names Nil snoc]:

   901   "(xs = [] ==> P) ==>(!!ys y. xs = ys @ [y] ==> P) ==> P"

   902 by (induct xs rule: rev_induct) auto

   903

   904 lemmas rev_cases = rev_exhaust

   905

   906 lemma rev_eq_Cons_iff[iff]: "(rev xs = y#ys) = (xs = rev ys @ [y])"

   907 by(rule rev_cases[of xs]) auto

   908

   909

   910 subsubsection {* @{text set} *}

   911

   912 lemma finite_set [iff]: "finite (set xs)"

   913 by (induct xs) auto

   914

   915 lemma set_append [simp]: "set (xs @ ys) = (set xs \<union> set ys)"

   916 by (induct xs) auto

   917

   918 lemma hd_in_set[simp]: "xs \<noteq> [] \<Longrightarrow> hd xs : set xs"

   919 by(cases xs) auto

   920

   921 lemma set_subset_Cons: "set xs \<subseteq> set (x # xs)"

   922 by auto

   923

   924 lemma set_ConsD: "y \<in> set (x # xs) \<Longrightarrow> y=x \<or> y \<in> set xs"

   925 by auto

   926

   927 lemma set_empty [iff]: "(set xs = {}) = (xs = [])"

   928 by (induct xs) auto

   929

   930 lemma set_empty2[iff]: "({} = set xs) = (xs = [])"

   931 by(induct xs) auto

   932

   933 lemma set_rev [simp]: "set (rev xs) = set xs"

   934 by (induct xs) auto

   935

   936 lemma set_map [simp]: "set (map f xs) = f(set xs)"

   937 by (induct xs) auto

   938

   939 lemma set_filter [simp]: "set (filter P xs) = {x. x : set xs \<and> P x}"

   940 by (induct xs) auto

   941

   942 lemma set_upt [simp]: "set[i..<j] = {i..<j}"

   943 by (induct j) (simp_all add: atLeastLessThanSuc)

   944

   945

   946 lemma split_list: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs"

   947 proof (induct xs)

   948   case Nil thus ?case by simp

   949 next

   950   case Cons thus ?case by (auto intro: Cons_eq_appendI)

   951 qed

   952

   953 lemma in_set_conv_decomp: "x \<in> set xs \<longleftrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"

   954   by (auto elim: split_list)

   955

   956 lemma split_list_first: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys"

   957 proof (induct xs)

   958   case Nil thus ?case by simp

   959 next

   960   case (Cons a xs)

   961   show ?case

   962   proof cases

   963     assume "x = a" thus ?case using Cons by fastsimp

   964   next

   965     assume "x \<noteq> a" thus ?case using Cons by(fastsimp intro!: Cons_eq_appendI)

   966   qed

   967 qed

   968

   969 lemma in_set_conv_decomp_first:

   970   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set ys)"

   971   by (auto dest!: split_list_first)

   972

   973 lemma split_list_last: "x : set xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs"

   974 proof (induct xs rule:rev_induct)

   975   case Nil thus ?case by simp

   976 next

   977   case (snoc a xs)

   978   show ?case

   979   proof cases

   980     assume "x = a" thus ?case using snoc by simp (metis ex_in_conv set_empty2)

   981   next

   982     assume "x \<noteq> a" thus ?case using snoc by fastsimp

   983   qed

   984 qed

   985

   986 lemma in_set_conv_decomp_last:

   987   "(x : set xs) = (\<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> set zs)"

   988   by (auto dest!: split_list_last)

   989

   990 lemma split_list_prop: "\<exists>x \<in> set xs. P x \<Longrightarrow> \<exists>ys x zs. xs = ys @ x # zs & P x"

   991 proof (induct xs)

   992   case Nil thus ?case by simp

   993 next

   994   case Cons thus ?case

   995     by(simp add:Bex_def)(metis append_Cons append.simps(1))

   996 qed

   997

   998 lemma split_list_propE:

   999   assumes "\<exists>x \<in> set xs. P x"

  1000   obtains ys x zs where "xs = ys @ x # zs" and "P x"

  1001 using split_list_prop [OF assms] by blast

  1002

  1003 lemma split_list_first_prop:

  1004   "\<exists>x \<in> set xs. P x \<Longrightarrow>

  1005    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y)"

  1006 proof (induct xs)

  1007   case Nil thus ?case by simp

  1008 next

  1009   case (Cons x xs)

  1010   show ?case

  1011   proof cases

  1012     assume "P x"

  1013     thus ?thesis by simp

  1014       (metis Un_upper1 contra_subsetD in_set_conv_decomp_first self_append_conv2 set_append)

  1015   next

  1016     assume "\<not> P x"

  1017     hence "\<exists>x\<in>set xs. P x" using Cons(2) by simp

  1018     thus ?thesis using \<not> P x Cons(1) by (metis append_Cons set_ConsD)

  1019   qed

  1020 qed

  1021

  1022 lemma split_list_first_propE:

  1023   assumes "\<exists>x \<in> set xs. P x"

  1024   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>y \<in> set ys. \<not> P y"

  1025 using split_list_first_prop [OF assms] by blast

  1026

  1027 lemma split_list_first_prop_iff:

  1028   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>

  1029    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>y \<in> set ys. \<not> P y))"

  1030 by (rule, erule split_list_first_prop) auto

  1031

  1032 lemma split_list_last_prop:

  1033   "\<exists>x \<in> set xs. P x \<Longrightarrow>

  1034    \<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z)"

  1035 proof(induct xs rule:rev_induct)

  1036   case Nil thus ?case by simp

  1037 next

  1038   case (snoc x xs)

  1039   show ?case

  1040   proof cases

  1041     assume "P x" thus ?thesis by (metis emptyE set_empty)

  1042   next

  1043     assume "\<not> P x"

  1044     hence "\<exists>x\<in>set xs. P x" using snoc(2) by simp

  1045     thus ?thesis using \<not> P x snoc(1) by fastsimp

  1046   qed

  1047 qed

  1048

  1049 lemma split_list_last_propE:

  1050   assumes "\<exists>x \<in> set xs. P x"

  1051   obtains ys x zs where "xs = ys @ x # zs" and "P x" and "\<forall>z \<in> set zs. \<not> P z"

  1052 using split_list_last_prop [OF assms] by blast

  1053

  1054 lemma split_list_last_prop_iff:

  1055   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>

  1056    (\<exists>ys x zs. xs = ys@x#zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"

  1057 by (metis split_list_last_prop [where P=P] in_set_conv_decomp)

  1058

  1059 lemma finite_list: "finite A ==> EX xs. set xs = A"

  1060   by (erule finite_induct)

  1061     (auto simp add: set.simps(2) [symmetric] simp del: set.simps(2))

  1062

  1063 lemma card_length: "card (set xs) \<le> length xs"

  1064 by (induct xs) (auto simp add: card_insert_if)

  1065

  1066 lemma set_minus_filter_out:

  1067   "set xs - {y} = set (filter (\<lambda>x. \<not> (x = y)) xs)"

  1068   by (induct xs) auto

  1069

  1070

  1071 subsubsection {* @{text filter} *}

  1072

  1073 lemma filter_append [simp]: "filter P (xs @ ys) = filter P xs @ filter P ys"

  1074 by (induct xs) auto

  1075

  1076 lemma rev_filter: "rev (filter P xs) = filter P (rev xs)"

  1077 by (induct xs) simp_all

  1078

  1079 lemma filter_filter [simp]: "filter P (filter Q xs) = filter (\<lambda>x. Q x \<and> P x) xs"

  1080 by (induct xs) auto

  1081

  1082 lemma length_filter_le [simp]: "length (filter P xs) \<le> length xs"

  1083 by (induct xs) (auto simp add: le_SucI)

  1084

  1085 lemma sum_length_filter_compl:

  1086   "length(filter P xs) + length(filter (%x. ~P x) xs) = length xs"

  1087 by(induct xs) simp_all

  1088

  1089 lemma filter_True [simp]: "\<forall>x \<in> set xs. P x ==> filter P xs = xs"

  1090 by (induct xs) auto

  1091

  1092 lemma filter_False [simp]: "\<forall>x \<in> set xs. \<not> P x ==> filter P xs = []"

  1093 by (induct xs) auto

  1094

  1095 lemma filter_empty_conv: "(filter P xs = []) = (\<forall>x\<in>set xs. \<not> P x)"

  1096 by (induct xs) simp_all

  1097

  1098 lemma filter_id_conv: "(filter P xs = xs) = (\<forall>x\<in>set xs. P x)"

  1099 apply (induct xs)

  1100  apply auto

  1101 apply(cut_tac P=P and xs=xs in length_filter_le)

  1102 apply simp

  1103 done

  1104

  1105 lemma filter_map:

  1106   "filter P (map f xs) = map f (filter (P o f) xs)"

  1107 by (induct xs) simp_all

  1108

  1109 lemma length_filter_map[simp]:

  1110   "length (filter P (map f xs)) = length(filter (P o f) xs)"

  1111 by (simp add:filter_map)

  1112

  1113 lemma filter_is_subset [simp]: "set (filter P xs) \<le> set xs"

  1114 by auto

  1115

  1116 lemma length_filter_less:

  1117   "\<lbrakk> x : set xs; ~ P x \<rbrakk> \<Longrightarrow> length(filter P xs) < length xs"

  1118 proof (induct xs)

  1119   case Nil thus ?case by simp

  1120 next

  1121   case (Cons x xs) thus ?case

  1122     apply (auto split:split_if_asm)

  1123     using length_filter_le[of P xs] apply arith

  1124   done

  1125 qed

  1126

  1127 lemma length_filter_conv_card:

  1128  "length(filter p xs) = card{i. i < length xs & p(xs!i)}"

  1129 proof (induct xs)

  1130   case Nil thus ?case by simp

  1131 next

  1132   case (Cons x xs)

  1133   let ?S = "{i. i < length xs & p(xs!i)}"

  1134   have fin: "finite ?S" by(fast intro: bounded_nat_set_is_finite)

  1135   show ?case (is "?l = card ?S'")

  1136   proof (cases)

  1137     assume "p x"

  1138     hence eq: "?S' = insert 0 (Suc  ?S)"

  1139       by(auto simp: image_def split:nat.split dest:gr0_implies_Suc)

  1140     have "length (filter p (x # xs)) = Suc(card ?S)"

  1141       using Cons p x by simp

  1142     also have "\<dots> = Suc(card(Suc  ?S))" using fin

  1143       by (simp add: card_image inj_Suc)

  1144     also have "\<dots> = card ?S'" using eq fin

  1145       by (simp add:card_insert_if) (simp add:image_def)

  1146     finally show ?thesis .

  1147   next

  1148     assume "\<not> p x"

  1149     hence eq: "?S' = Suc  ?S"

  1150       by(auto simp add: image_def split:nat.split elim:lessE)

  1151     have "length (filter p (x # xs)) = card ?S"

  1152       using Cons \<not> p x by simp

  1153     also have "\<dots> = card(Suc  ?S)" using fin

  1154       by (simp add: card_image inj_Suc)

  1155     also have "\<dots> = card ?S'" using eq fin

  1156       by (simp add:card_insert_if)

  1157     finally show ?thesis .

  1158   qed

  1159 qed

  1160

  1161 lemma Cons_eq_filterD:

  1162  "x#xs = filter P ys \<Longrightarrow>

  1163   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"

  1164   (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")

  1165 proof(induct ys)

  1166   case Nil thus ?case by simp

  1167 next

  1168   case (Cons y ys)

  1169   show ?case (is "\<exists>x. ?Q x")

  1170   proof cases

  1171     assume Py: "P y"

  1172     show ?thesis

  1173     proof cases

  1174       assume "x = y"

  1175       with Py Cons.prems have "?Q []" by simp

  1176       then show ?thesis ..

  1177     next

  1178       assume "x \<noteq> y"

  1179       with Py Cons.prems show ?thesis by simp

  1180     qed

  1181   next

  1182     assume "\<not> P y"

  1183     with Cons obtain us vs where "?P (y#ys) (y#us) vs" by fastsimp

  1184     then have "?Q (y#us)" by simp

  1185     then show ?thesis ..

  1186   qed

  1187 qed

  1188

  1189 lemma filter_eq_ConsD:

  1190  "filter P ys = x#xs \<Longrightarrow>

  1191   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"

  1192 by(rule Cons_eq_filterD) simp

  1193

  1194 lemma filter_eq_Cons_iff:

  1195  "(filter P ys = x#xs) =

  1196   (\<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs)"

  1197 by(auto dest:filter_eq_ConsD)

  1198

  1199 lemma Cons_eq_filter_iff:

  1200  "(x#xs = filter P ys) =

  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 by(auto dest:Cons_eq_filterD)

  1203

  1204 lemma filter_cong[fundef_cong, recdef_cong]:

  1205  "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> P x = Q x) \<Longrightarrow> filter P xs = filter Q ys"

  1206 apply simp

  1207 apply(erule thin_rl)

  1208 by (induct ys) simp_all

  1209

  1210

  1211 subsubsection {* List partitioning *}

  1212

  1213 primrec partition :: "('a \<Rightarrow> bool) \<Rightarrow>'a list \<Rightarrow> 'a list \<times> 'a list" where

  1214   "partition P [] = ([], [])"

  1215   | "partition P (x # xs) =

  1216       (let (yes, no) = partition P xs

  1217       in if P x then (x # yes, no) else (yes, x # no))"

  1218

  1219 lemma partition_filter1:

  1220     "fst (partition P xs) = filter P xs"

  1221 by (induct xs) (auto simp add: Let_def split_def)

  1222

  1223 lemma partition_filter2:

  1224     "snd (partition P xs) = filter (Not o P) xs"

  1225 by (induct xs) (auto simp add: Let_def split_def)

  1226

  1227 lemma partition_P:

  1228   assumes "partition P xs = (yes, no)"

  1229   shows "(\<forall>p \<in> set yes.  P p) \<and> (\<forall>p  \<in> set no. \<not> P p)"

  1230 proof -

  1231   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"

  1232     by simp_all

  1233   then show ?thesis by (simp_all add: partition_filter1 partition_filter2)

  1234 qed

  1235

  1236 lemma partition_set:

  1237   assumes "partition P xs = (yes, no)"

  1238   shows "set yes \<union> set no = set xs"

  1239 proof -

  1240   from assms have "yes = fst (partition P xs)" and "no = snd (partition P xs)"

  1241     by simp_all

  1242   then show ?thesis by (auto simp add: partition_filter1 partition_filter2)

  1243 qed

  1244

  1245 lemma partition_filter_conv[simp]:

  1246   "partition f xs = (filter f xs,filter (Not o f) xs)"

  1247 unfolding partition_filter2[symmetric]

  1248 unfolding partition_filter1[symmetric] by simp

  1249

  1250 declare partition.simps[simp del]

  1251

  1252

  1253 subsubsection {* @{text concat} *}

  1254

  1255 lemma concat_append [simp]: "concat (xs @ ys) = concat xs @ concat ys"

  1256 by (induct xs) auto

  1257

  1258 lemma concat_eq_Nil_conv [simp]: "(concat xss = []) = (\<forall>xs \<in> set xss. xs = [])"

  1259 by (induct xss) auto

  1260

  1261 lemma Nil_eq_concat_conv [simp]: "([] = concat xss) = (\<forall>xs \<in> set xss. xs = [])"

  1262 by (induct xss) auto

  1263

  1264 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"

  1265 by (induct xs) auto

  1266

  1267 lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"

  1268 by (induct xs) auto

  1269

  1270 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"

  1271 by (induct xs) auto

  1272

  1273 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)"

  1274 by (induct xs) auto

  1275

  1276 lemma rev_concat: "rev (concat xs) = concat (map rev (rev xs))"

  1277 by (induct xs) auto

  1278

  1279

  1280 subsubsection {* @{text nth} *}

  1281

  1282 lemma nth_Cons_0 [simp, code]: "(x # xs)!0 = x"

  1283 by auto

  1284

  1285 lemma nth_Cons_Suc [simp, code]: "(x # xs)!(Suc n) = xs!n"

  1286 by auto

  1287

  1288 declare nth.simps [simp del]

  1289

  1290 lemma nth_append:

  1291   "(xs @ ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"

  1292 apply (induct xs arbitrary: n, simp)

  1293 apply (case_tac n, auto)

  1294 done

  1295

  1296 lemma nth_append_length [simp]: "(xs @ x # ys) ! length xs = x"

  1297 by (induct xs) auto

  1298

  1299 lemma nth_append_length_plus[simp]: "(xs @ ys) ! (length xs + n) = ys ! n"

  1300 by (induct xs) auto

  1301

  1302 lemma nth_map [simp]: "n < length xs ==> (map f xs)!n = f(xs!n)"

  1303 apply (induct xs arbitrary: n, simp)

  1304 apply (case_tac n, auto)

  1305 done

  1306

  1307 lemma hd_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd xs = xs!0"

  1308 by(cases xs) simp_all

  1309

  1310

  1311 lemma list_eq_iff_nth_eq:

  1312  "(xs = ys) = (length xs = length ys \<and> (ALL i<length xs. xs!i = ys!i))"

  1313 apply(induct xs arbitrary: ys)

  1314  apply force

  1315 apply(case_tac ys)

  1316  apply simp

  1317 apply(simp add:nth_Cons split:nat.split)apply blast

  1318 done

  1319

  1320 lemma set_conv_nth: "set xs = {xs!i | i. i < length xs}"

  1321 apply (induct xs, simp, simp)

  1322 apply safe

  1323 apply (metis nat_case_0 nth.simps zero_less_Suc)

  1324 apply (metis less_Suc_eq_0_disj nth_Cons_Suc)

  1325 apply (case_tac i, simp)

  1326 apply (metis diff_Suc_Suc nat_case_Suc nth.simps zero_less_diff)

  1327 done

  1328

  1329 lemma in_set_conv_nth: "(x \<in> set xs) = (\<exists>i < length xs. xs!i = x)"

  1330 by(auto simp:set_conv_nth)

  1331

  1332 lemma list_ball_nth: "[| n < length xs; !x : set xs. P x|] ==> P(xs!n)"

  1333 by (auto simp add: set_conv_nth)

  1334

  1335 lemma nth_mem [simp]: "n < length xs ==> xs!n : set xs"

  1336 by (auto simp add: set_conv_nth)

  1337

  1338 lemma all_nth_imp_all_set:

  1339 "[| !i < length xs. P(xs!i); x : set xs|] ==> P x"

  1340 by (auto simp add: set_conv_nth)

  1341

  1342 lemma all_set_conv_all_nth:

  1343 "(\<forall>x \<in> set xs. P x) = (\<forall>i. i < length xs --> P (xs ! i))"

  1344 by (auto simp add: set_conv_nth)

  1345

  1346 lemma rev_nth:

  1347   "n < size xs \<Longrightarrow> rev xs ! n = xs ! (length xs - Suc n)"

  1348 proof (induct xs arbitrary: n)

  1349   case Nil thus ?case by simp

  1350 next

  1351   case (Cons x xs)

  1352   hence n: "n < Suc (length xs)" by simp

  1353   moreover

  1354   { assume "n < length xs"

  1355     with n obtain n' where "length xs - n = Suc n'"

  1356       by (cases "length xs - n", auto)

  1357     moreover

  1358     then have "length xs - Suc n = n'" by simp

  1359     ultimately

  1360     have "xs ! (length xs - Suc n) = (x # xs) ! (length xs - n)" by simp

  1361   }

  1362   ultimately

  1363   show ?case by (clarsimp simp add: Cons nth_append)

  1364 qed

  1365

  1366 lemma Skolem_list_nth:

  1367   "(ALL i<k. EX x. P i x) = (EX xs. size xs = k & (ALL i<k. P i (xs!i)))"

  1368   (is "_ = (EX xs. ?P k xs)")

  1369 proof(induct k)

  1370   case 0 show ?case by simp

  1371 next

  1372   case (Suc k)

  1373   show ?case (is "?L = ?R" is "_ = (EX xs. ?P' xs)")

  1374   proof

  1375     assume "?R" thus "?L" using Suc by auto

  1376   next

  1377     assume "?L"

  1378     with Suc obtain x xs where "?P k xs & P k x" by (metis less_Suc_eq)

  1379     hence "?P'(xs@[x])" by(simp add:nth_append less_Suc_eq)

  1380     thus "?R" ..

  1381   qed

  1382 qed

  1383

  1384

  1385 subsubsection {* @{text list_update} *}

  1386

  1387 lemma length_list_update [simp]: "length(xs[i:=x]) = length xs"

  1388 by (induct xs arbitrary: i) (auto split: nat.split)

  1389

  1390 lemma nth_list_update:

  1391 "i < length xs==> (xs[i:=x])!j = (if i = j then x else xs!j)"

  1392 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)

  1393

  1394 lemma nth_list_update_eq [simp]: "i < length xs ==> (xs[i:=x])!i = x"

  1395 by (simp add: nth_list_update)

  1396

  1397 lemma nth_list_update_neq [simp]: "i \<noteq> j ==> xs[i:=x]!j = xs!j"

  1398 by (induct xs arbitrary: i j) (auto simp add: nth_Cons split: nat.split)

  1399

  1400 lemma list_update_id[simp]: "xs[i := xs!i] = xs"

  1401 by (induct xs arbitrary: i) (simp_all split:nat.splits)

  1402

  1403 lemma list_update_beyond[simp]: "length xs \<le> i \<Longrightarrow> xs[i:=x] = xs"

  1404 apply (induct xs arbitrary: i)

  1405  apply simp

  1406 apply (case_tac i)

  1407 apply simp_all

  1408 done

  1409

  1410 lemma list_update_nonempty[simp]: "xs[k:=x] = [] \<longleftrightarrow> xs=[]"

  1411 by(metis length_0_conv length_list_update)

  1412

  1413 lemma list_update_same_conv:

  1414 "i < length xs ==> (xs[i := x] = xs) = (xs!i = x)"

  1415 by (induct xs arbitrary: i) (auto split: nat.split)

  1416

  1417 lemma list_update_append1:

  1418  "i < size xs \<Longrightarrow> (xs @ ys)[i:=x] = xs[i:=x] @ ys"

  1419 apply (induct xs arbitrary: i, simp)

  1420 apply(simp split:nat.split)

  1421 done

  1422

  1423 lemma list_update_append:

  1424   "(xs @ ys) [n:= x] =

  1425   (if n < length xs then xs[n:= x] @ ys else xs @ (ys [n-length xs:= x]))"

  1426 by (induct xs arbitrary: n) (auto split:nat.splits)

  1427

  1428 lemma list_update_length [simp]:

  1429  "(xs @ x # ys)[length xs := y] = (xs @ y # ys)"

  1430 by (induct xs, auto)

  1431

  1432 lemma map_update: "map f (xs[k:= y]) = (map f xs)[k := f y]"

  1433 by(induct xs arbitrary: k)(auto split:nat.splits)

  1434

  1435 lemma rev_update:

  1436   "k < length xs \<Longrightarrow> rev (xs[k:= y]) = (rev xs)[length xs - k - 1 := y]"

  1437 by (induct xs arbitrary: k) (auto simp: list_update_append split:nat.splits)

  1438

  1439 lemma update_zip:

  1440   "(zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"

  1441 by (induct ys arbitrary: i xy xs) (auto, case_tac xs, auto split: nat.split)

  1442

  1443 lemma set_update_subset_insert: "set(xs[i:=x]) <= insert x (set xs)"

  1444 by (induct xs arbitrary: i) (auto split: nat.split)

  1445

  1446 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"

  1447 by (blast dest!: set_update_subset_insert [THEN subsetD])

  1448

  1449 lemma set_update_memI: "n < length xs \<Longrightarrow> x \<in> set (xs[n := x])"

  1450 by (induct xs arbitrary: n) (auto split:nat.splits)

  1451

  1452 lemma list_update_overwrite[simp]:

  1453   "xs [i := x, i := y] = xs [i := y]"

  1454 apply (induct xs arbitrary: i) apply simp

  1455 apply (case_tac i, simp_all)

  1456 done

  1457

  1458 lemma list_update_swap:

  1459   "i \<noteq> i' \<Longrightarrow> xs [i := x, i' := x'] = xs [i' := x', i := x]"

  1460 apply (induct xs arbitrary: i i')

  1461 apply simp

  1462 apply (case_tac i, case_tac i')

  1463 apply auto

  1464 apply (case_tac i')

  1465 apply auto

  1466 done

  1467

  1468 lemma list_update_code [code]:

  1469   "[][i := y] = []"

  1470   "(x # xs)[0 := y] = y # xs"

  1471   "(x # xs)[Suc i := y] = x # xs[i := y]"

  1472   by simp_all

  1473

  1474

  1475 subsubsection {* @{text last} and @{text butlast} *}

  1476

  1477 lemma last_snoc [simp]: "last (xs @ [x]) = x"

  1478 by (induct xs) auto

  1479

  1480 lemma butlast_snoc [simp]: "butlast (xs @ [x]) = xs"

  1481 by (induct xs) auto

  1482

  1483 lemma last_ConsL: "xs = [] \<Longrightarrow> last(x#xs) = x"

  1484 by(simp add:last.simps)

  1485

  1486 lemma last_ConsR: "xs \<noteq> [] \<Longrightarrow> last(x#xs) = last xs"

  1487 by(simp add:last.simps)

  1488

  1489 lemma last_append: "last(xs @ ys) = (if ys = [] then last xs else last ys)"

  1490 by (induct xs) (auto)

  1491

  1492 lemma last_appendL[simp]: "ys = [] \<Longrightarrow> last(xs @ ys) = last xs"

  1493 by(simp add:last_append)

  1494

  1495 lemma last_appendR[simp]: "ys \<noteq> [] \<Longrightarrow> last(xs @ ys) = last ys"

  1496 by(simp add:last_append)

  1497

  1498 lemma hd_rev: "xs \<noteq> [] \<Longrightarrow> hd(rev xs) = last xs"

  1499 by(rule rev_exhaust[of xs]) simp_all

  1500

  1501 lemma last_rev: "xs \<noteq> [] \<Longrightarrow> last(rev xs) = hd xs"

  1502 by(cases xs) simp_all

  1503

  1504 lemma last_in_set[simp]: "as \<noteq> [] \<Longrightarrow> last as \<in> set as"

  1505 by (induct as) auto

  1506

  1507 lemma length_butlast [simp]: "length (butlast xs) = length xs - 1"

  1508 by (induct xs rule: rev_induct) auto

  1509

  1510 lemma butlast_append:

  1511   "butlast (xs @ ys) = (if ys = [] then butlast xs else xs @ butlast ys)"

  1512 by (induct xs arbitrary: ys) auto

  1513

  1514 lemma append_butlast_last_id [simp]:

  1515 "xs \<noteq> [] ==> butlast xs @ [last xs] = xs"

  1516 by (induct xs) auto

  1517

  1518 lemma in_set_butlastD: "x : set (butlast xs) ==> x : set xs"

  1519 by (induct xs) (auto split: split_if_asm)

  1520

  1521 lemma in_set_butlast_appendI:

  1522 "x : set (butlast xs) | x : set (butlast ys) ==> x : set (butlast (xs @ ys))"

  1523 by (auto dest: in_set_butlastD simp add: butlast_append)

  1524

  1525 lemma last_drop[simp]: "n < length xs \<Longrightarrow> last (drop n xs) = last xs"

  1526 apply (induct xs arbitrary: n)

  1527  apply simp

  1528 apply (auto split:nat.split)

  1529 done

  1530

  1531 lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"

  1532 by(induct xs)(auto simp:neq_Nil_conv)

  1533

  1534 lemma butlast_conv_take: "butlast xs = take (length xs - 1) xs"

  1535 by (induct xs, simp, case_tac xs, simp_all)

  1536

  1537 lemma last_list_update:

  1538   "xs \<noteq> [] \<Longrightarrow> last(xs[k:=x]) = (if k = size xs - 1 then x else last xs)"

  1539 by (auto simp: last_conv_nth)

  1540

  1541 lemma butlast_list_update:

  1542   "butlast(xs[k:=x]) =

  1543  (if k = size xs - 1 then butlast xs else (butlast xs)[k:=x])"

  1544 apply(cases xs rule:rev_cases)

  1545 apply simp

  1546 apply(simp add:list_update_append split:nat.splits)

  1547 done

  1548

  1549 lemma last_map:

  1550   "xs \<noteq> [] \<Longrightarrow> last (map f xs) = f (last xs)"

  1551   by (cases xs rule: rev_cases) simp_all

  1552

  1553 lemma map_butlast:

  1554   "map f (butlast xs) = butlast (map f xs)"

  1555   by (induct xs) simp_all

  1556

  1557

  1558 subsubsection {* @{text take} and @{text drop} *}

  1559

  1560 lemma take_0 [simp]: "take 0 xs = []"

  1561 by (induct xs) auto

  1562

  1563 lemma drop_0 [simp]: "drop 0 xs = xs"

  1564 by (induct xs) auto

  1565

  1566 lemma take_Suc_Cons [simp]: "take (Suc n) (x # xs) = x # take n xs"

  1567 by simp

  1568

  1569 lemma drop_Suc_Cons [simp]: "drop (Suc n) (x # xs) = drop n xs"

  1570 by simp

  1571

  1572 declare take_Cons [simp del] and drop_Cons [simp del]

  1573

  1574 lemma take_1_Cons [simp]: "take 1 (x # xs) = [x]"

  1575   unfolding One_nat_def by simp

  1576

  1577 lemma drop_1_Cons [simp]: "drop 1 (x # xs) = xs"

  1578   unfolding One_nat_def by simp

  1579

  1580 lemma take_Suc: "xs ~= [] ==> take (Suc n) xs = hd xs # take n (tl xs)"

  1581 by(clarsimp simp add:neq_Nil_conv)

  1582

  1583 lemma drop_Suc: "drop (Suc n) xs = drop n (tl xs)"

  1584 by(cases xs, simp_all)

  1585

  1586 lemma take_tl: "take n (tl xs) = tl (take (Suc n) xs)"

  1587 by (induct xs arbitrary: n) simp_all

  1588

  1589 lemma drop_tl: "drop n (tl xs) = tl(drop n xs)"

  1590 by(induct xs arbitrary: n, simp_all add:drop_Cons drop_Suc split:nat.split)

  1591

  1592 lemma tl_take: "tl (take n xs) = take (n - 1) (tl xs)"

  1593 by (cases n, simp, cases xs, auto)

  1594

  1595 lemma tl_drop: "tl (drop n xs) = drop n (tl xs)"

  1596 by (simp only: drop_tl)

  1597

  1598 lemma nth_via_drop: "drop n xs = y#ys \<Longrightarrow> xs!n = y"

  1599 apply (induct xs arbitrary: n, simp)

  1600 apply(simp add:drop_Cons nth_Cons split:nat.splits)

  1601 done

  1602

  1603 lemma take_Suc_conv_app_nth:

  1604   "i < length xs \<Longrightarrow> take (Suc i) xs = take i xs @ [xs!i]"

  1605 apply (induct xs arbitrary: i, simp)

  1606 apply (case_tac i, auto)

  1607 done

  1608

  1609 lemma drop_Suc_conv_tl:

  1610   "i < length xs \<Longrightarrow> (xs!i) # (drop (Suc i) xs) = drop i xs"

  1611 apply (induct xs arbitrary: i, simp)

  1612 apply (case_tac i, auto)

  1613 done

  1614

  1615 lemma length_take [simp]: "length (take n xs) = min (length xs) n"

  1616 by (induct n arbitrary: xs) (auto, case_tac xs, auto)

  1617

  1618 lemma length_drop [simp]: "length (drop n xs) = (length xs - n)"

  1619 by (induct n arbitrary: xs) (auto, case_tac xs, auto)

  1620

  1621 lemma take_all [simp]: "length xs <= n ==> take n xs = xs"

  1622 by (induct n arbitrary: xs) (auto, case_tac xs, auto)

  1623

  1624 lemma drop_all [simp]: "length xs <= n ==> drop n xs = []"

  1625 by (induct n arbitrary: xs) (auto, case_tac xs, auto)

  1626

  1627 lemma take_append [simp]:

  1628   "take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"

  1629 by (induct n arbitrary: xs) (auto, case_tac xs, auto)

  1630

  1631 lemma drop_append [simp]:

  1632   "drop n (xs @ ys) = drop n xs @ drop (n - length xs) ys"

  1633 by (induct n arbitrary: xs) (auto, case_tac xs, auto)

  1634

  1635 lemma take_take [simp]: "take n (take m xs) = take (min n m) xs"

  1636 apply (induct m arbitrary: xs n, auto)

  1637 apply (case_tac xs, auto)

  1638 apply (case_tac n, auto)

  1639 done

  1640

  1641 lemma drop_drop [simp]: "drop n (drop m xs) = drop (n + m) xs"

  1642 apply (induct m arbitrary: xs, auto)

  1643 apply (case_tac xs, auto)

  1644 done

  1645

  1646 lemma take_drop: "take n (drop m xs) = drop m (take (n + m) xs)"

  1647 apply (induct m arbitrary: xs n, auto)

  1648 apply (case_tac xs, auto)

  1649 done

  1650

  1651 lemma drop_take: "drop n (take m xs) = take (m-n) (drop n xs)"

  1652 apply(induct xs arbitrary: m n)

  1653  apply simp

  1654 apply(simp add: take_Cons drop_Cons split:nat.split)

  1655 done

  1656

  1657 lemma append_take_drop_id [simp]: "take n xs @ drop n xs = xs"

  1658 apply (induct n arbitrary: xs, auto)

  1659 apply (case_tac xs, auto)

  1660 done

  1661

  1662 lemma take_eq_Nil[simp]: "(take n xs = []) = (n = 0 \<or> xs = [])"

  1663 apply(induct xs arbitrary: n)

  1664  apply simp

  1665 apply(simp add:take_Cons split:nat.split)

  1666 done

  1667

  1668 lemma drop_eq_Nil[simp]: "(drop n xs = []) = (length xs <= n)"

  1669 apply(induct xs arbitrary: n)

  1670 apply simp

  1671 apply(simp add:drop_Cons split:nat.split)

  1672 done

  1673

  1674 lemma take_map: "take n (map f xs) = map f (take n xs)"

  1675 apply (induct n arbitrary: xs, auto)

  1676 apply (case_tac xs, auto)

  1677 done

  1678

  1679 lemma drop_map: "drop n (map f xs) = map f (drop n xs)"

  1680 apply (induct n arbitrary: xs, auto)

  1681 apply (case_tac xs, auto)

  1682 done

  1683

  1684 lemma rev_take: "rev (take i xs) = drop (length xs - i) (rev xs)"

  1685 apply (induct xs arbitrary: i, auto)

  1686 apply (case_tac i, auto)

  1687 done

  1688

  1689 lemma rev_drop: "rev (drop i xs) = take (length xs - i) (rev xs)"

  1690 apply (induct xs arbitrary: i, auto)

  1691 apply (case_tac i, auto)

  1692 done

  1693

  1694 lemma nth_take [simp]: "i < n ==> (take n xs)!i = xs!i"

  1695 apply (induct xs arbitrary: i n, auto)

  1696 apply (case_tac n, blast)

  1697 apply (case_tac i, auto)

  1698 done

  1699

  1700 lemma nth_drop [simp]:

  1701   "n + i <= length xs ==> (drop n xs)!i = xs!(n + i)"

  1702 apply (induct n arbitrary: xs i, auto)

  1703 apply (case_tac xs, auto)

  1704 done

  1705

  1706 lemma butlast_take:

  1707   "n <= length xs ==> butlast (take n xs) = take (n - 1) xs"

  1708 by (simp add: butlast_conv_take min_max.inf_absorb1 min_max.inf_absorb2)

  1709

  1710 lemma butlast_drop: "butlast (drop n xs) = drop n (butlast xs)"

  1711 by (simp add: butlast_conv_take drop_take add_ac)

  1712

  1713 lemma take_butlast: "n < length xs ==> take n (butlast xs) = take n xs"

  1714 by (simp add: butlast_conv_take min_max.inf_absorb1)

  1715

  1716 lemma drop_butlast: "drop n (butlast xs) = butlast (drop n xs)"

  1717 by (simp add: butlast_conv_take drop_take add_ac)

  1718

  1719 lemma hd_drop_conv_nth: "\<lbrakk> xs \<noteq> []; n < length xs \<rbrakk> \<Longrightarrow> hd(drop n xs) = xs!n"

  1720 by(simp add: hd_conv_nth)

  1721

  1722 lemma set_take_subset_set_take:

  1723   "m <= n \<Longrightarrow> set(take m xs) <= set(take n xs)"

  1724 by(induct xs arbitrary: m n)(auto simp:take_Cons split:nat.split)

  1725

  1726 lemma set_take_subset: "set(take n xs) \<subseteq> set xs"

  1727 by(induct xs arbitrary: n)(auto simp:take_Cons split:nat.split)

  1728

  1729 lemma set_drop_subset: "set(drop n xs) \<subseteq> set xs"

  1730 by(induct xs arbitrary: n)(auto simp:drop_Cons split:nat.split)

  1731

  1732 lemma set_drop_subset_set_drop:

  1733   "m >= n \<Longrightarrow> set(drop m xs) <= set(drop n xs)"

  1734 apply(induct xs arbitrary: m n)

  1735 apply(auto simp:drop_Cons split:nat.split)

  1736 apply (metis set_drop_subset subset_iff)

  1737 done

  1738

  1739 lemma in_set_takeD: "x : set(take n xs) \<Longrightarrow> x : set xs"

  1740 using set_take_subset by fast

  1741

  1742 lemma in_set_dropD: "x : set(drop n xs) \<Longrightarrow> x : set xs"

  1743 using set_drop_subset by fast

  1744

  1745 lemma append_eq_conv_conj:

  1746   "(xs @ ys = zs) = (xs = take (length xs) zs \<and> ys = drop (length xs) zs)"

  1747 apply (induct xs arbitrary: zs, simp, clarsimp)

  1748 apply (case_tac zs, auto)

  1749 done

  1750

  1751 lemma take_add:

  1752   "i+j \<le> length(xs) \<Longrightarrow> take (i+j) xs = take i xs @ take j (drop i xs)"

  1753 apply (induct xs arbitrary: i, auto)

  1754 apply (case_tac i, simp_all)

  1755 done

  1756

  1757 lemma append_eq_append_conv_if:

  1758  "(xs\<^isub>1 @ xs\<^isub>2 = ys\<^isub>1 @ ys\<^isub>2) =

  1759   (if size xs\<^isub>1 \<le> size ys\<^isub>1

  1760    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

  1761    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)"

  1762 apply(induct xs\<^isub>1 arbitrary: ys\<^isub>1)

  1763  apply simp

  1764 apply(case_tac ys\<^isub>1)

  1765 apply simp_all

  1766 done

  1767

  1768 lemma take_hd_drop:

  1769   "n < length xs \<Longrightarrow> take n xs @ [hd (drop n xs)] = take (Suc n) xs"

  1770 apply(induct xs arbitrary: n)

  1771 apply simp

  1772 apply(simp add:drop_Cons split:nat.split)

  1773 done

  1774

  1775 lemma id_take_nth_drop:

  1776  "i < length xs \<Longrightarrow> xs = take i xs @ xs!i # drop (Suc i) xs"

  1777 proof -

  1778   assume si: "i < length xs"

  1779   hence "xs = take (Suc i) xs @ drop (Suc i) xs" by auto

  1780   moreover

  1781   from si have "take (Suc i) xs = take i xs @ [xs!i]"

  1782     apply (rule_tac take_Suc_conv_app_nth) by arith

  1783   ultimately show ?thesis by auto

  1784 qed

  1785

  1786 lemma upd_conv_take_nth_drop:

  1787  "i < length xs \<Longrightarrow> xs[i:=a] = take i xs @ a # drop (Suc i) xs"

  1788 proof -

  1789   assume i: "i < length xs"

  1790   have "xs[i:=a] = (take i xs @ xs!i # drop (Suc i) xs)[i:=a]"

  1791     by(rule arg_cong[OF id_take_nth_drop[OF i]])

  1792   also have "\<dots> = take i xs @ a # drop (Suc i) xs"

  1793     using i by (simp add: list_update_append)

  1794   finally show ?thesis .

  1795 qed

  1796

  1797 lemma nth_drop':

  1798   "i < length xs \<Longrightarrow> xs ! i # drop (Suc i) xs = drop i xs"

  1799 apply (induct i arbitrary: xs)

  1800 apply (simp add: neq_Nil_conv)

  1801 apply (erule exE)+

  1802 apply simp

  1803 apply (case_tac xs)

  1804 apply simp_all

  1805 done

  1806

  1807

  1808 subsubsection {* @{text takeWhile} and @{text dropWhile} *}

  1809

  1810 lemma length_takeWhile_le: "length (takeWhile P xs) \<le> length xs"

  1811   by (induct xs) auto

  1812

  1813 lemma takeWhile_dropWhile_id [simp]: "takeWhile P xs @ dropWhile P xs = xs"

  1814 by (induct xs) auto

  1815

  1816 lemma takeWhile_append1 [simp]:

  1817 "[| x:set xs; ~P(x)|] ==> takeWhile P (xs @ ys) = takeWhile P xs"

  1818 by (induct xs) auto

  1819

  1820 lemma takeWhile_append2 [simp]:

  1821 "(!!x. x : set xs ==> P x) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"

  1822 by (induct xs) auto

  1823

  1824 lemma takeWhile_tail: "\<not> P x ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"

  1825 by (induct xs) auto

  1826

  1827 lemma takeWhile_nth: "j < length (takeWhile P xs) \<Longrightarrow> takeWhile P xs ! j = xs ! j"

  1828 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto

  1829

  1830 lemma dropWhile_nth: "j < length (dropWhile P xs) \<Longrightarrow> dropWhile P xs ! j = xs ! (j + length (takeWhile P xs))"

  1831 apply (subst (3) takeWhile_dropWhile_id[symmetric]) unfolding nth_append by auto

  1832

  1833 lemma length_dropWhile_le: "length (dropWhile P xs) \<le> length xs"

  1834 by (induct xs) auto

  1835

  1836 lemma dropWhile_append1 [simp]:

  1837 "[| x : set xs; ~P(x)|] ==> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"

  1838 by (induct xs) auto

  1839

  1840 lemma dropWhile_append2 [simp]:

  1841 "(!!x. x:set xs ==> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"

  1842 by (induct xs) auto

  1843

  1844 lemma set_takeWhileD: "x : set (takeWhile P xs) ==> x : set xs \<and> P x"

  1845 by (induct xs) (auto split: split_if_asm)

  1846

  1847 lemma takeWhile_eq_all_conv[simp]:

  1848  "(takeWhile P xs = xs) = (\<forall>x \<in> set xs. P x)"

  1849 by(induct xs, auto)

  1850

  1851 lemma dropWhile_eq_Nil_conv[simp]:

  1852  "(dropWhile P xs = []) = (\<forall>x \<in> set xs. P x)"

  1853 by(induct xs, auto)

  1854

  1855 lemma dropWhile_eq_Cons_conv:

  1856  "(dropWhile P xs = y#ys) = (xs = takeWhile P xs @ y # ys & \<not> P y)"

  1857 by(induct xs, auto)

  1858

  1859 lemma distinct_takeWhile[simp]: "distinct xs ==> distinct (takeWhile P xs)"

  1860 by (induct xs) (auto dest: set_takeWhileD)

  1861

  1862 lemma distinct_dropWhile[simp]: "distinct xs ==> distinct (dropWhile P xs)"

  1863 by (induct xs) auto

  1864

  1865 lemma takeWhile_map: "takeWhile P (map f xs) = map f (takeWhile (P \<circ> f) xs)"

  1866 by (induct xs) auto

  1867

  1868 lemma dropWhile_map: "dropWhile P (map f xs) = map f (dropWhile (P \<circ> f) xs)"

  1869 by (induct xs) auto

  1870

  1871 lemma takeWhile_eq_take: "takeWhile P xs = take (length (takeWhile P xs)) xs"

  1872 by (induct xs) auto

  1873

  1874 lemma dropWhile_eq_drop: "dropWhile P xs = drop (length (takeWhile P xs)) xs"

  1875 by (induct xs) auto

  1876

  1877 lemma hd_dropWhile:

  1878   "dropWhile P xs \<noteq> [] \<Longrightarrow> \<not> P (hd (dropWhile P xs))"

  1879 using assms by (induct xs) auto

  1880

  1881 lemma takeWhile_eq_filter:

  1882   assumes "\<And> x. x \<in> set (dropWhile P xs) \<Longrightarrow> \<not> P x"

  1883   shows "takeWhile P xs = filter P xs"

  1884 proof -

  1885   have A: "filter P xs = filter P (takeWhile P xs @ dropWhile P xs)"

  1886     by simp

  1887   have B: "filter P (dropWhile P xs) = []"

  1888     unfolding filter_empty_conv using assms by blast

  1889   have "filter P xs = takeWhile P xs"

  1890     unfolding A filter_append B

  1891     by (auto simp add: filter_id_conv dest: set_takeWhileD)

  1892   thus ?thesis ..

  1893 qed

  1894

  1895 lemma takeWhile_eq_take_P_nth:

  1896   "\<lbrakk> \<And> i. \<lbrakk> i < n ; i < length xs \<rbrakk> \<Longrightarrow> P (xs ! i) ; n < length xs \<Longrightarrow> \<not> P (xs ! n) \<rbrakk> \<Longrightarrow>

  1897   takeWhile P xs = take n xs"

  1898 proof (induct xs arbitrary: n)

  1899   case (Cons x xs)

  1900   thus ?case

  1901   proof (cases n)

  1902     case (Suc n') note this[simp]

  1903     have "P x" using Cons.prems(1)[of 0] by simp

  1904     moreover have "takeWhile P xs = take n' xs"

  1905     proof (rule Cons.hyps)

  1906       case goal1 thus "P (xs ! i)" using Cons.prems(1)[of "Suc i"] by simp

  1907     next case goal2 thus ?case using Cons by auto

  1908     qed

  1909     ultimately show ?thesis by simp

  1910    qed simp

  1911 qed simp

  1912

  1913 lemma nth_length_takeWhile:

  1914   "length (takeWhile P xs) < length xs \<Longrightarrow> \<not> P (xs ! length (takeWhile P xs))"

  1915 by (induct xs) auto

  1916

  1917 lemma length_takeWhile_less_P_nth:

  1918   assumes all: "\<And> i. i < j \<Longrightarrow> P (xs ! i)" and "j \<le> length xs"

  1919   shows "j \<le> length (takeWhile P xs)"

  1920 proof (rule classical)

  1921   assume "\<not> ?thesis"

  1922   hence "length (takeWhile P xs) < length xs" using assms by simp

  1923   thus ?thesis using all \<not> ?thesis nth_length_takeWhile[of P xs] by auto

  1924 qed

  1925

  1926 text{* The following two lemmmas could be generalized to an arbitrary

  1927 property. *}

  1928

  1929 lemma takeWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>

  1930  takeWhile (\<lambda>y. y \<noteq> x) (rev xs) = rev (tl (dropWhile (\<lambda>y. y \<noteq> x) xs))"

  1931 by(induct xs) (auto simp: takeWhile_tail[where l="[]"])

  1932

  1933 lemma dropWhile_neq_rev: "\<lbrakk>distinct xs; x \<in> set xs\<rbrakk> \<Longrightarrow>

  1934   dropWhile (\<lambda>y. y \<noteq> x) (rev xs) = x # rev (takeWhile (\<lambda>y. y \<noteq> x) xs)"

  1935 apply(induct xs)

  1936  apply simp

  1937 apply auto

  1938 apply(subst dropWhile_append2)

  1939 apply auto

  1940 done

  1941

  1942 lemma takeWhile_not_last:

  1943  "\<lbrakk> xs \<noteq> []; distinct xs\<rbrakk> \<Longrightarrow> takeWhile (\<lambda>y. y \<noteq> last xs) xs = butlast xs"

  1944 apply(induct xs)

  1945  apply simp

  1946 apply(case_tac xs)

  1947 apply(auto)

  1948 done

  1949

  1950 lemma takeWhile_cong [fundef_cong, recdef_cong]:

  1951   "[| l = k; !!x. x : set l ==> P x = Q x |]

  1952   ==> takeWhile P l = takeWhile Q k"

  1953 by (induct k arbitrary: l) (simp_all)

  1954

  1955 lemma dropWhile_cong [fundef_cong, recdef_cong]:

  1956   "[| l = k; !!x. x : set l ==> P x = Q x |]

  1957   ==> dropWhile P l = dropWhile Q k"

  1958 by (induct k arbitrary: l, simp_all)

  1959

  1960

  1961 subsubsection {* @{text zip} *}

  1962

  1963 lemma zip_Nil [simp]: "zip [] ys = []"

  1964 by (induct ys) auto

  1965

  1966 lemma zip_Cons_Cons [simp]: "zip (x # xs) (y # ys) = (x, y) # zip xs ys"

  1967 by simp

  1968

  1969 declare zip_Cons [simp del]

  1970

  1971 lemma [code]:

  1972   "zip [] ys = []"

  1973   "zip xs [] = []"

  1974   "zip (x # xs) (y # ys) = (x, y) # zip xs ys"

  1975   by (fact zip_Nil zip.simps(1) zip_Cons_Cons)+

  1976

  1977 lemma zip_Cons1:

  1978  "zip (x#xs) ys = (case ys of [] \<Rightarrow> [] | y#ys \<Rightarrow> (x,y)#zip xs ys)"

  1979 by(auto split:list.split)

  1980

  1981 lemma length_zip [simp]:

  1982 "length (zip xs ys) = min (length xs) (length ys)"

  1983 by (induct xs ys rule:list_induct2') auto

  1984

  1985 lemma zip_obtain_same_length:

  1986   assumes "\<And>zs ws n. length zs = length ws \<Longrightarrow> n = min (length xs) (length ys)

  1987     \<Longrightarrow> zs = take n xs \<Longrightarrow> ws = take n ys \<Longrightarrow> P (zip zs ws)"

  1988   shows "P (zip xs ys)"

  1989 proof -

  1990   let ?n = "min (length xs) (length ys)"

  1991   have "P (zip (take ?n xs) (take ?n ys))"

  1992     by (rule assms) simp_all

  1993   moreover have "zip xs ys = zip (take ?n xs) (take ?n ys)"

  1994   proof (induct xs arbitrary: ys)

  1995     case Nil then show ?case by simp

  1996   next

  1997     case (Cons x xs) then show ?case by (cases ys) simp_all

  1998   qed

  1999   ultimately show ?thesis by simp

  2000 qed

  2001

  2002 lemma zip_append1:

  2003 "zip (xs @ ys) zs =

  2004 zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"

  2005 by (induct xs zs rule:list_induct2') auto

  2006

  2007 lemma zip_append2:

  2008 "zip xs (ys @ zs) =

  2009 zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"

  2010 by (induct xs ys rule:list_induct2') auto

  2011

  2012 lemma zip_append [simp]:

  2013  "[| length xs = length us; length ys = length vs |] ==>

  2014 zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"

  2015 by (simp add: zip_append1)

  2016

  2017 lemma zip_rev:

  2018 "length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"

  2019 by (induct rule:list_induct2, simp_all)

  2020

  2021 lemma zip_map_map:

  2022   "zip (map f xs) (map g ys) = map (\<lambda> (x, y). (f x, g y)) (zip xs ys)"

  2023 proof (induct xs arbitrary: ys)

  2024   case (Cons x xs) note Cons_x_xs = Cons.hyps

  2025   show ?case

  2026   proof (cases ys)

  2027     case (Cons y ys')

  2028     show ?thesis unfolding Cons using Cons_x_xs by simp

  2029   qed simp

  2030 qed simp

  2031

  2032 lemma zip_map1:

  2033   "zip (map f xs) ys = map (\<lambda>(x, y). (f x, y)) (zip xs ys)"

  2034 using zip_map_map[of f xs "\<lambda>x. x" ys] by simp

  2035

  2036 lemma zip_map2:

  2037   "zip xs (map f ys) = map (\<lambda>(x, y). (x, f y)) (zip xs ys)"

  2038 using zip_map_map[of "\<lambda>x. x" xs f ys] by simp

  2039

  2040 lemma map_zip_map:

  2041   "map f (zip (map g xs) ys) = map (%(x,y). f(g x, y)) (zip xs ys)"

  2042 unfolding zip_map1 by auto

  2043

  2044 lemma map_zip_map2:

  2045   "map f (zip xs (map g ys)) = map (%(x,y). f(x, g y)) (zip xs ys)"

  2046 unfolding zip_map2 by auto

  2047

  2048 text{* Courtesy of Andreas Lochbihler: *}

  2049 lemma zip_same_conv_map: "zip xs xs = map (\<lambda>x. (x, x)) xs"

  2050 by(induct xs) auto

  2051

  2052 lemma nth_zip [simp]:

  2053 "[| i < length xs; i < length ys|] ==> (zip xs ys)!i = (xs!i, ys!i)"

  2054 apply (induct ys arbitrary: i xs, simp)

  2055 apply (case_tac xs)

  2056  apply (simp_all add: nth.simps split: nat.split)

  2057 done

  2058

  2059 lemma set_zip:

  2060 "set (zip xs ys) = {(xs!i, ys!i) | i. i < min (length xs) (length ys)}"

  2061 by(simp add: set_conv_nth cong: rev_conj_cong)

  2062

  2063 lemma zip_same: "((a,b) \<in> set (zip xs xs)) = (a \<in> set xs \<and> a = b)"

  2064 by(induct xs) auto

  2065

  2066 lemma zip_update:

  2067   "zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"

  2068 by(rule sym, simp add: update_zip)

  2069

  2070 lemma zip_replicate [simp]:

  2071   "zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"

  2072 apply (induct i arbitrary: j, auto)

  2073 apply (case_tac j, auto)

  2074 done

  2075

  2076 lemma take_zip:

  2077   "take n (zip xs ys) = zip (take n xs) (take n ys)"

  2078 apply (induct n arbitrary: xs ys)

  2079  apply simp

  2080 apply (case_tac xs, simp)

  2081 apply (case_tac ys, simp_all)

  2082 done

  2083

  2084 lemma drop_zip:

  2085   "drop n (zip xs ys) = zip (drop n xs) (drop n ys)"

  2086 apply (induct n arbitrary: xs ys)

  2087  apply simp

  2088 apply (case_tac xs, simp)

  2089 apply (case_tac ys, simp_all)

  2090 done

  2091

  2092 lemma zip_takeWhile_fst: "zip (takeWhile P xs) ys = takeWhile (P \<circ> fst) (zip xs ys)"

  2093 proof (induct xs arbitrary: ys)

  2094   case (Cons x xs) thus ?case by (cases ys) auto

  2095 qed simp

  2096

  2097 lemma zip_takeWhile_snd: "zip xs (takeWhile P ys) = takeWhile (P \<circ> snd) (zip xs ys)"

  2098 proof (induct xs arbitrary: ys)

  2099   case (Cons x xs) thus ?case by (cases ys) auto

  2100 qed simp

  2101

  2102 lemma set_zip_leftD:

  2103   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs"

  2104 by (induct xs ys rule:list_induct2') auto

  2105

  2106 lemma set_zip_rightD:

  2107   "(x,y)\<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys"

  2108 by (induct xs ys rule:list_induct2') auto

  2109

  2110 lemma in_set_zipE:

  2111   "(x,y) : set(zip xs ys) \<Longrightarrow> (\<lbrakk> x : set xs; y : set ys \<rbrakk> \<Longrightarrow> R) \<Longrightarrow> R"

  2112 by(blast dest: set_zip_leftD set_zip_rightD)

  2113

  2114 lemma zip_map_fst_snd:

  2115   "zip (map fst zs) (map snd zs) = zs"

  2116   by (induct zs) simp_all

  2117

  2118 lemma zip_eq_conv:

  2119   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"

  2120   by (auto simp add: zip_map_fst_snd)

  2121

  2122 lemma distinct_zipI1:

  2123   "distinct xs \<Longrightarrow> distinct (zip xs ys)"

  2124 proof (induct xs arbitrary: ys)

  2125   case (Cons x xs)

  2126   show ?case

  2127   proof (cases ys)

  2128     case (Cons y ys')

  2129     have "(x, y) \<notin> set (zip xs ys')"

  2130       using Cons.prems by (auto simp: set_zip)

  2131     thus ?thesis

  2132       unfolding Cons zip_Cons_Cons distinct.simps

  2133       using Cons.hyps Cons.prems by simp

  2134   qed simp

  2135 qed simp

  2136

  2137 lemma distinct_zipI2:

  2138   "distinct xs \<Longrightarrow> distinct (zip xs ys)"

  2139 proof (induct xs arbitrary: ys)

  2140   case (Cons x xs)

  2141   show ?case

  2142   proof (cases ys)

  2143     case (Cons y ys')

  2144      have "(x, y) \<notin> set (zip xs ys')"

  2145       using Cons.prems by (auto simp: set_zip)

  2146     thus ?thesis

  2147       unfolding Cons zip_Cons_Cons distinct.simps

  2148       using Cons.hyps Cons.prems by simp

  2149   qed simp

  2150 qed simp

  2151

  2152

  2153 subsubsection {* @{text list_all2} *}

  2154

  2155 lemma list_all2_lengthD [intro?]:

  2156   "list_all2 P xs ys ==> length xs = length ys"

  2157 by (simp add: list_all2_def)

  2158

  2159 lemma list_all2_Nil [iff, code]: "list_all2 P [] ys = (ys = [])"

  2160 by (simp add: list_all2_def)

  2161

  2162 lemma list_all2_Nil2 [iff, code]: "list_all2 P xs [] = (xs = [])"

  2163 by (simp add: list_all2_def)

  2164

  2165 lemma list_all2_Cons [iff, code]:

  2166   "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"

  2167 by (auto simp add: list_all2_def)

  2168

  2169 lemma list_all2_Cons1:

  2170 "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"

  2171 by (cases ys) auto

  2172

  2173 lemma list_all2_Cons2:

  2174 "list_all2 P xs (y # ys) = (\<exists>z zs. xs = z # zs \<and> P z y \<and> list_all2 P zs ys)"

  2175 by (cases xs) auto

  2176

  2177 lemma list_all2_rev [iff]:

  2178 "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"

  2179 by (simp add: list_all2_def zip_rev cong: conj_cong)

  2180

  2181 lemma list_all2_rev1:

  2182 "list_all2 P (rev xs) ys = list_all2 P xs (rev ys)"

  2183 by (subst list_all2_rev [symmetric]) simp

  2184

  2185 lemma list_all2_append1:

  2186 "list_all2 P (xs @ ys) zs =

  2187 (EX us vs. zs = us @ vs \<and> length us = length xs \<and> length vs = length ys \<and>

  2188 list_all2 P xs us \<and> list_all2 P ys vs)"

  2189 apply (simp add: list_all2_def zip_append1)

  2190 apply (rule iffI)

  2191  apply (rule_tac x = "take (length xs) zs" in exI)

  2192  apply (rule_tac x = "drop (length xs) zs" in exI)

  2193  apply (force split: nat_diff_split simp add: min_def, clarify)

  2194 apply (simp add: ball_Un)

  2195 done

  2196

  2197 lemma list_all2_append2:

  2198 "list_all2 P xs (ys @ zs) =

  2199 (EX us vs. xs = us @ vs \<and> length us = length ys \<and> length vs = length zs \<and>

  2200 list_all2 P us ys \<and> list_all2 P vs zs)"

  2201 apply (simp add: list_all2_def zip_append2)

  2202 apply (rule iffI)

  2203  apply (rule_tac x = "take (length ys) xs" in exI)

  2204  apply (rule_tac x = "drop (length ys) xs" in exI)

  2205  apply (force split: nat_diff_split simp add: min_def, clarify)

  2206 apply (simp add: ball_Un)

  2207 done

  2208

  2209 lemma list_all2_append:

  2210   "length xs = length ys \<Longrightarrow>

  2211   list_all2 P (xs@us) (ys@vs) = (list_all2 P xs ys \<and> list_all2 P us vs)"

  2212 by (induct rule:list_induct2, simp_all)

  2213

  2214 lemma list_all2_appendI [intro?, trans]:

  2215   "\<lbrakk> list_all2 P a b; list_all2 P c d \<rbrakk> \<Longrightarrow> list_all2 P (a@c) (b@d)"

  2216 by (simp add: list_all2_append list_all2_lengthD)

  2217

  2218 lemma list_all2_conv_all_nth:

  2219 "list_all2 P xs ys =

  2220 (length xs = length ys \<and> (\<forall>i < length xs. P (xs!i) (ys!i)))"

  2221 by (force simp add: list_all2_def set_zip)

  2222

  2223 lemma list_all2_trans:

  2224   assumes tr: "!!a b c. P1 a b ==> P2 b c ==> P3 a c"

  2225   shows "!!bs cs. list_all2 P1 as bs ==> list_all2 P2 bs cs ==> list_all2 P3 as cs"

  2226         (is "!!bs cs. PROP ?Q as bs cs")

  2227 proof (induct as)

  2228   fix x xs bs assume I1: "!!bs cs. PROP ?Q xs bs cs"

  2229   show "!!cs. PROP ?Q (x # xs) bs cs"

  2230   proof (induct bs)

  2231     fix y ys cs assume I2: "!!cs. PROP ?Q (x # xs) ys cs"

  2232     show "PROP ?Q (x # xs) (y # ys) cs"

  2233       by (induct cs) (auto intro: tr I1 I2)

  2234   qed simp

  2235 qed simp

  2236

  2237 lemma list_all2_all_nthI [intro?]:

  2238   "length a = length b \<Longrightarrow> (\<And>n. n < length a \<Longrightarrow> P (a!n) (b!n)) \<Longrightarrow> list_all2 P a b"

  2239 by (simp add: list_all2_conv_all_nth)

  2240

  2241 lemma list_all2I:

  2242   "\<forall>x \<in> set (zip a b). split P x \<Longrightarrow> length a = length b \<Longrightarrow> list_all2 P a b"

  2243 by (simp add: list_all2_def)

  2244

  2245 lemma list_all2_nthD:

  2246   "\<lbrakk> list_all2 P xs ys; p < size xs \<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"

  2247 by (simp add: list_all2_conv_all_nth)

  2248

  2249 lemma list_all2_nthD2:

  2250   "\<lbrakk>list_all2 P xs ys; p < size ys\<rbrakk> \<Longrightarrow> P (xs!p) (ys!p)"

  2251 by (frule list_all2_lengthD) (auto intro: list_all2_nthD)

  2252

  2253 lemma list_all2_map1:

  2254   "list_all2 P (map f as) bs = list_all2 (\<lambda>x y. P (f x) y) as bs"

  2255 by (simp add: list_all2_conv_all_nth)

  2256

  2257 lemma list_all2_map2:

  2258   "list_all2 P as (map f bs) = list_all2 (\<lambda>x y. P x (f y)) as bs"

  2259 by (auto simp add: list_all2_conv_all_nth)

  2260

  2261 lemma list_all2_refl [intro?]:

  2262   "(\<And>x. P x x) \<Longrightarrow> list_all2 P xs xs"

  2263 by (simp add: list_all2_conv_all_nth)

  2264

  2265 lemma list_all2_update_cong:

  2266   "\<lbrakk> i<size xs; list_all2 P xs ys; P x y \<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"

  2267 by (simp add: list_all2_conv_all_nth nth_list_update)

  2268

  2269 lemma list_all2_update_cong2:

  2270   "\<lbrakk>list_all2 P xs ys; P x y; i < length ys\<rbrakk> \<Longrightarrow> list_all2 P (xs[i:=x]) (ys[i:=y])"

  2271 by (simp add: list_all2_lengthD list_all2_update_cong)

  2272

  2273 lemma list_all2_takeI [simp,intro?]:

  2274   "list_all2 P xs ys \<Longrightarrow> list_all2 P (take n xs) (take n ys)"

  2275 apply (induct xs arbitrary: n ys)

  2276  apply simp

  2277 apply (clarsimp simp add: list_all2_Cons1)

  2278 apply (case_tac n)

  2279 apply auto

  2280 done

  2281

  2282 lemma list_all2_dropI [simp,intro?]:

  2283   "list_all2 P as bs \<Longrightarrow> list_all2 P (drop n as) (drop n bs)"

  2284 apply (induct as arbitrary: n bs, simp)

  2285 apply (clarsimp simp add: list_all2_Cons1)

  2286 apply (case_tac n, simp, simp)

  2287 done

  2288

  2289 lemma list_all2_mono [intro?]:

  2290   "list_all2 P xs ys \<Longrightarrow> (\<And>xs ys. P xs ys \<Longrightarrow> Q xs ys) \<Longrightarrow> list_all2 Q xs ys"

  2291 apply (induct xs arbitrary: ys, simp)

  2292 apply (case_tac ys, auto)

  2293 done

  2294

  2295 lemma list_all2_eq:

  2296   "xs = ys \<longleftrightarrow> list_all2 (op =) xs ys"

  2297 by (induct xs ys rule: list_induct2') auto

  2298

  2299

  2300 subsubsection {* @{text foldl} and @{text foldr} *}

  2301

  2302 lemma foldl_append [simp]:

  2303   "foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"

  2304 by (induct xs arbitrary: a) auto

  2305

  2306 lemma foldr_append[simp]: "foldr f (xs @ ys) a = foldr f xs (foldr f ys a)"

  2307 by (induct xs) auto

  2308

  2309 lemma foldr_map: "foldr g (map f xs) a = foldr (g o f) xs a"

  2310 by(induct xs) simp_all

  2311

  2312 text{* For efficient code generation: avoid intermediate list. *}

  2313 lemma foldl_map[code_unfold]:

  2314   "foldl g a (map f xs) = foldl (%a x. g a (f x)) a xs"

  2315 by(induct xs arbitrary:a) simp_all

  2316

  2317 lemma foldl_apply:

  2318   assumes "\<And>x. x \<in> set xs \<Longrightarrow> f x \<circ> h = h \<circ> g x"

  2319   shows "foldl (\<lambda>s x. f x s) (h s) xs = h (foldl (\<lambda>s x. g x s) s xs)"

  2320   by (rule sym, insert assms, induct xs arbitrary: s) (simp_all add: expand_fun_eq)

  2321

  2322 lemma foldl_cong [fundef_cong, recdef_cong]:

  2323   "[| a = b; l = k; !!a x. x : set l ==> f a x = g a x |]

  2324   ==> foldl f a l = foldl g b k"

  2325 by (induct k arbitrary: a b l) simp_all

  2326

  2327 lemma foldr_cong [fundef_cong, recdef_cong]:

  2328   "[| a = b; l = k; !!a x. x : set l ==> f x a = g x a |]

  2329   ==> foldr f l a = foldr g k b"

  2330 by (induct k arbitrary: a b l) simp_all

  2331

  2332 lemma foldl_fun_comm:

  2333   assumes "\<And>x y s. f (f s x) y = f (f s y) x"

  2334   shows "f (foldl f s xs) x = foldl f (f s x) xs"

  2335   by (induct xs arbitrary: s)

  2336     (simp_all add: assms)

  2337

  2338 lemma (in semigroup_add) foldl_assoc:

  2339 shows "foldl op+ (x+y) zs = x + (foldl op+ y zs)"

  2340 by (induct zs arbitrary: y) (simp_all add:add_assoc)

  2341

  2342 lemma (in monoid_add) foldl_absorb0:

  2343 shows "x + (foldl op+ 0 zs) = foldl op+ x zs"

  2344 by (induct zs) (simp_all add:foldl_assoc)

  2345

  2346 lemma foldl_rev:

  2347   assumes "\<And>x y s. f (f s x) y = f (f s y) x"

  2348   shows "foldl f s (rev xs) = foldl f s xs"

  2349 proof (induct xs arbitrary: s)

  2350   case Nil then show ?case by simp

  2351 next

  2352   case (Cons x xs) with assms show ?case by (simp add: foldl_fun_comm)

  2353 qed

  2354

  2355 lemma rev_foldl_cons [code]:

  2356   "rev xs = foldl (\<lambda>xs x. x # xs) [] xs"

  2357 proof (induct xs)

  2358   case Nil then show ?case by simp

  2359 next

  2360   case Cons

  2361   {

  2362     fix x xs ys

  2363     have "foldl (\<lambda>xs x. x # xs) ys xs @ [x]

  2364       = foldl (\<lambda>xs x. x # xs) (ys @ [x]) xs"

  2365     by (induct xs arbitrary: ys) auto

  2366   }

  2367   note aux = this

  2368   show ?case by (induct xs) (auto simp add: Cons aux)

  2369 qed

  2370

  2371

  2372 text{* The First Duality Theorem'' in Bird \& Wadler: *}

  2373

  2374 lemma foldl_foldr1_lemma:

  2375  "foldl op + a xs = a + foldr op + xs (0\<Colon>'a::monoid_add)"

  2376 by (induct xs arbitrary: a) (auto simp:add_assoc)

  2377

  2378 corollary foldl_foldr1:

  2379  "foldl op + 0 xs = foldr op + xs (0\<Colon>'a::monoid_add)"

  2380 by (simp add:foldl_foldr1_lemma)

  2381

  2382

  2383 text{* The Third Duality Theorem'' in Bird \& Wadler: *}

  2384

  2385 lemma foldr_foldl: "foldr f xs a = foldl (%x y. f y x) a (rev xs)"

  2386 by (induct xs) auto

  2387

  2388 lemma foldl_foldr: "foldl f a xs = foldr (%x y. f y x) (rev xs) a"

  2389 by (simp add: foldr_foldl [of "%x y. f y x" "rev xs"])

  2390

  2391 lemma (in ab_semigroup_add) foldr_conv_foldl: "foldr op + xs a = foldl op + a xs"

  2392   by (induct xs, auto simp add: foldl_assoc add_commute)

  2393

  2394 text {*

  2395 Note: @{text "n \<le> foldl (op +) n ns"} looks simpler, but is more

  2396 difficult to use because it requires an additional transitivity step.

  2397 *}

  2398

  2399 lemma start_le_sum: "(m::nat) <= n ==> m <= foldl (op +) n ns"

  2400 by (induct ns arbitrary: n) auto

  2401

  2402 lemma elem_le_sum: "(n::nat) : set ns ==> n <= foldl (op +) 0 ns"

  2403 by (force intro: start_le_sum simp add: in_set_conv_decomp)

  2404

  2405 lemma sum_eq_0_conv [iff]:

  2406   "(foldl (op +) (m::nat) ns = 0) = (m = 0 \<and> (\<forall>n \<in> set ns. n = 0))"

  2407 by (induct ns arbitrary: m) auto

  2408

  2409 lemma foldr_invariant:

  2410   "\<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)"

  2411   by (induct xs, simp_all)

  2412

  2413 lemma foldl_invariant:

  2414   "\<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)"

  2415   by (induct xs arbitrary: x, simp_all)

  2416

  2417 lemma foldl_weak_invariant:

  2418   assumes "P s"

  2419     and "\<And>s x. x \<in> set xs \<Longrightarrow> P s \<Longrightarrow> P (f s x)"

  2420   shows "P (foldl f s xs)"

  2421   using assms by (induct xs arbitrary: s) simp_all

  2422

  2423 text {* @{const foldl} and @{const concat} *}

  2424

  2425 lemma foldl_conv_concat:

  2426   "foldl (op @) xs xss = xs @ concat xss"

  2427 proof (induct xss arbitrary: xs)

  2428   case Nil show ?case by simp

  2429 next

  2430   interpret monoid_add "op @" "[]" proof qed simp_all

  2431   case Cons then show ?case by (simp add: foldl_absorb0)

  2432 qed

  2433

  2434 lemma concat_conv_foldl: "concat xss = foldl (op @) [] xss"

  2435   by (simp add: foldl_conv_concat)

  2436

  2437 text {* @{const Finite_Set.fold} and @{const foldl} *}

  2438

  2439 lemma (in fun_left_comm) fold_set_remdups:

  2440   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y (remdups xs)"

  2441   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm insert_absorb)

  2442

  2443 lemma (in fun_left_comm_idem) fold_set:

  2444   "fold f y (set xs) = foldl (\<lambda>y x. f x y) y xs"

  2445   by (rule sym, induct xs arbitrary: y) (simp_all add: fold_fun_comm)

  2446

  2447 lemma (in ab_semigroup_idem_mult) fold1_set:

  2448   assumes "xs \<noteq> []"

  2449   shows "fold1 times (set xs) = foldl times (hd xs) (tl xs)"

  2450 proof -

  2451   interpret fun_left_comm_idem times by (fact fun_left_comm_idem)

  2452   from assms obtain y ys where xs: "xs = y # ys"

  2453     by (cases xs) auto

  2454   show ?thesis

  2455   proof (cases "set ys = {}")

  2456     case True with xs show ?thesis by simp

  2457   next

  2458     case False

  2459     then have "fold1 times (insert y (set ys)) = fold times y (set ys)"

  2460       by (simp only: finite_set fold1_eq_fold_idem)

  2461     with xs show ?thesis by (simp add: fold_set mult_commute)

  2462   qed

  2463 qed

  2464

  2465 lemma (in lattice) Inf_fin_set_fold [code_unfold]:

  2466   "Inf_fin (set (x # xs)) = foldl inf x xs"

  2467 proof -

  2468   interpret ab_semigroup_idem_mult "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

  2469     by (fact ab_semigroup_idem_mult_inf)

  2470   show ?thesis

  2471     by (simp add: Inf_fin_def fold1_set del: set.simps)

  2472 qed

  2473

  2474 lemma (in lattice) Sup_fin_set_fold [code_unfold]:

  2475   "Sup_fin (set (x # xs)) = foldl sup x xs"

  2476 proof -

  2477   interpret ab_semigroup_idem_mult "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

  2478     by (fact ab_semigroup_idem_mult_sup)

  2479   show ?thesis

  2480     by (simp add: Sup_fin_def fold1_set del: set.simps)

  2481 qed

  2482

  2483 lemma (in linorder) Min_fin_set_fold [code_unfold]:

  2484   "Min (set (x # xs)) = foldl min x xs"

  2485 proof -

  2486   interpret ab_semigroup_idem_mult "min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

  2487     by (fact ab_semigroup_idem_mult_min)

  2488   show ?thesis

  2489     by (simp add: Min_def fold1_set del: set.simps)

  2490 qed

  2491

  2492 lemma (in linorder) Max_fin_set_fold [code_unfold]:

  2493   "Max (set (x # xs)) = foldl max x xs"

  2494 proof -

  2495   interpret ab_semigroup_idem_mult "max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

  2496     by (fact ab_semigroup_idem_mult_max)

  2497   show ?thesis

  2498     by (simp add: Max_def fold1_set del: set.simps)

  2499 qed

  2500

  2501 lemma (in complete_lattice) Inf_set_fold [code_unfold]:

  2502   "Inf (set xs) = foldl inf top xs"

  2503 proof -

  2504   interpret fun_left_comm_idem "inf :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

  2505     by (fact fun_left_comm_idem_inf)

  2506   show ?thesis by (simp add: Inf_fold_inf fold_set inf_commute)

  2507 qed

  2508

  2509 lemma (in complete_lattice) Sup_set_fold [code_unfold]:

  2510   "Sup (set xs) = foldl sup bot xs"

  2511 proof -

  2512   interpret fun_left_comm_idem "sup :: 'a \<Rightarrow> 'a \<Rightarrow> 'a"

  2513     by (fact fun_left_comm_idem_sup)

  2514   show ?thesis by (simp add: Sup_fold_sup fold_set sup_commute)

  2515 qed

  2516

  2517 lemma (in complete_lattice) INFI_set_fold:

  2518   "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"

  2519   unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map

  2520     by (simp add: inf_commute)

  2521

  2522 lemma (in complete_lattice) SUPR_set_fold:

  2523   "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"

  2524   unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map

  2525     by (simp add: sup_commute)

  2526

  2527

  2528 subsubsection {* @{text upt} *}

  2529

  2530 lemma upt_rec[code]: "[i..<j] = (if i<j then i#[Suc i..<j] else [])"

  2531 -- {* simp does not terminate! *}

  2532 by (induct j) auto

  2533

  2534 lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]

  2535

  2536 lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"

  2537 by (subst upt_rec) simp

  2538

  2539 lemma upt_eq_Nil_conv[simp]: "([i..<j] = []) = (j = 0 \<or> j <= i)"

  2540 by(induct j)simp_all

  2541

  2542 lemma upt_eq_Cons_conv:

  2543  "([i..<j] = x#xs) = (i < j & i = x & [i+1..<j] = xs)"

  2544 apply(induct j arbitrary: x xs)

  2545  apply simp

  2546 apply(clarsimp simp add: append_eq_Cons_conv)

  2547 apply arith

  2548 done

  2549

  2550 lemma upt_Suc_append: "i <= j ==> [i..<(Suc j)] = [i..<j]@[j]"

  2551 -- {* Only needed if @{text upt_Suc} is deleted from the simpset. *}

  2552 by simp

  2553

  2554 lemma upt_conv_Cons: "i < j ==> [i..<j] = i # [Suc i..<j]"

  2555   by (simp add: upt_rec)

  2556

  2557 lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"

  2558 -- {* LOOPS as a simprule, since @{text "j <= j"}. *}

  2559 by (induct k) auto

  2560

  2561 lemma length_upt [simp]: "length [i..<j] = j - i"

  2562 by (induct j) (auto simp add: Suc_diff_le)

  2563

  2564 lemma nth_upt [simp]: "i + k < j ==> [i..<j] ! k = i + k"

  2565 apply (induct j)

  2566 apply (auto simp add: less_Suc_eq nth_append split: nat_diff_split)

  2567 done

  2568

  2569

  2570 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i"

  2571 by(simp add:upt_conv_Cons)

  2572

  2573 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1"

  2574 apply(cases j)

  2575  apply simp

  2576 by(simp add:upt_Suc_append)

  2577

  2578 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]"

  2579 apply (induct m arbitrary: i, simp)

  2580 apply (subst upt_rec)

  2581 apply (rule sym)

  2582 apply (subst upt_rec)

  2583 apply (simp del: upt.simps)

  2584 done

  2585

  2586 lemma drop_upt[simp]: "drop m [i..<j] = [i+m..<j]"

  2587 apply(induct j)

  2588 apply auto

  2589 done

  2590

  2591 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]"

  2592 by (induct n) auto

  2593

  2594 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)"

  2595 apply (induct n m  arbitrary: i rule: diff_induct)

  2596 prefer 3 apply (subst map_Suc_upt[symmetric])

  2597 apply (auto simp add: less_diff_conv nth_upt)

  2598 done

  2599

  2600 lemma nth_take_lemma:

  2601   "k <= length xs ==> k <= length ys ==>

  2602      (!!i. i < k --> xs!i = ys!i) ==> take k xs = take k ys"

  2603 apply (atomize, induct k arbitrary: xs ys)

  2604 apply (simp_all add: less_Suc_eq_0_disj all_conj_distrib, clarify)

  2605 txt {* Both lists must be non-empty *}

  2606 apply (case_tac xs, simp)

  2607 apply (case_tac ys, clarify)

  2608  apply (simp (no_asm_use))

  2609 apply clarify

  2610 txt {* prenexing's needed, not miniscoping *}

  2611 apply (simp (no_asm_use) add: all_simps [symmetric] del: all_simps)

  2612 apply blast

  2613 done

  2614

  2615 lemma nth_equalityI:

  2616  "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"

  2617 apply (frule nth_take_lemma [OF le_refl eq_imp_le])

  2618 apply (simp_all add: take_all)

  2619 done

  2620

  2621 lemma map_nth:

  2622   "map (\<lambda>i. xs ! i) [0..<length xs] = xs"

  2623   by (rule nth_equalityI, auto)

  2624

  2625 (* needs nth_equalityI *)

  2626 lemma list_all2_antisym:

  2627   "\<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>

  2628   \<Longrightarrow> xs = ys"

  2629   apply (simp add: list_all2_conv_all_nth)

  2630   apply (rule nth_equalityI, blast, simp)

  2631   done

  2632

  2633 lemma take_equalityI: "(\<forall>i. take i xs = take i ys) ==> xs = ys"

  2634 -- {* The famous take-lemma. *}

  2635 apply (drule_tac x = "max (length xs) (length ys)" in spec)

  2636 apply (simp add: le_max_iff_disj take_all)

  2637 done

  2638

  2639

  2640 lemma take_Cons':

  2641      "take n (x # xs) = (if n = 0 then [] else x # take (n - 1) xs)"

  2642 by (cases n) simp_all

  2643

  2644 lemma drop_Cons':

  2645      "drop n (x # xs) = (if n = 0 then x # xs else drop (n - 1) xs)"

  2646 by (cases n) simp_all

  2647

  2648 lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"

  2649 by (cases n) simp_all

  2650

  2651 lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]

  2652 lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]

  2653 lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]

  2654

  2655 declare take_Cons_number_of [simp]

  2656         drop_Cons_number_of [simp]

  2657         nth_Cons_number_of [simp]

  2658

  2659

  2660 subsubsection {* @{text upto}: interval-list on @{typ int} *}

  2661

  2662 (* FIXME make upto tail recursive? *)

  2663

  2664 function upto :: "int \<Rightarrow> int \<Rightarrow> int list" ("(1[_../_])") where

  2665 "upto i j = (if i \<le> j then i # [i+1..j] else [])"

  2666 by auto

  2667 termination

  2668 by(relation "measure(%(i::int,j). nat(j - i + 1))") auto

  2669

  2670 declare upto.simps[code, simp del]

  2671

  2672 lemmas upto_rec_number_of[simp] =

  2673   upto.simps[of "number_of m" "number_of n", standard]

  2674

  2675 lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"

  2676 by(simp add: upto.simps)

  2677

  2678 lemma set_upto[simp]: "set[i..j] = {i..j}"

  2679 apply(induct i j rule:upto.induct)

  2680 apply(simp add: upto.simps simp_from_to)

  2681 done

  2682

  2683

  2684 subsubsection {* @{text "distinct"} and @{text remdups} *}

  2685

  2686 lemma distinct_append [simp]:

  2687 "distinct (xs @ ys) = (distinct xs \<and> distinct ys \<and> set xs \<inter> set ys = {})"

  2688 by (induct xs) auto

  2689

  2690 lemma distinct_rev[simp]: "distinct(rev xs) = distinct xs"

  2691 by(induct xs) auto

  2692

  2693 lemma set_remdups [simp]: "set (remdups xs) = set xs"

  2694 by (induct xs) (auto simp add: insert_absorb)

  2695

  2696 lemma distinct_remdups [iff]: "distinct (remdups xs)"

  2697 by (induct xs) auto

  2698

  2699 lemma distinct_remdups_id: "distinct xs ==> remdups xs = xs"

  2700 by (induct xs, auto)

  2701

  2702 lemma remdups_id_iff_distinct [simp]: "remdups xs = xs \<longleftrightarrow> distinct xs"

  2703 by (metis distinct_remdups distinct_remdups_id)

  2704

  2705 lemma finite_distinct_list: "finite A \<Longrightarrow> EX xs. set xs = A & distinct xs"

  2706 by (metis distinct_remdups finite_list set_remdups)

  2707

  2708 lemma remdups_eq_nil_iff [simp]: "(remdups x = []) = (x = [])"

  2709 by (induct x, auto)

  2710

  2711 lemma remdups_eq_nil_right_iff [simp]: "([] = remdups x) = (x = [])"

  2712 by (induct x, auto)

  2713

  2714 lemma length_remdups_leq[iff]: "length(remdups xs) <= length xs"

  2715 by (induct xs) auto

  2716

  2717 lemma length_remdups_eq[iff]:

  2718   "(length (remdups xs) = length xs) = (remdups xs = xs)"

  2719 apply(induct xs)

  2720  apply auto

  2721 apply(subgoal_tac "length (remdups xs) <= length xs")

  2722  apply arith

  2723 apply(rule length_remdups_leq)

  2724 done

  2725

  2726 lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"

  2727 apply(induct xs)

  2728 apply auto

  2729 done

  2730

  2731 lemma distinct_map:

  2732   "distinct(map f xs) = (distinct xs & inj_on f (set xs))"

  2733 by (induct xs) auto

  2734

  2735

  2736 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"

  2737 by (induct xs) auto

  2738

  2739 lemma distinct_upt[simp]: "distinct[i..<j]"

  2740 by (induct j) auto

  2741

  2742 lemma distinct_upto[simp]: "distinct[i..j]"

  2743 apply(induct i j rule:upto.induct)

  2744 apply(subst upto.simps)

  2745 apply(simp)

  2746 done

  2747

  2748 lemma distinct_take[simp]: "distinct xs \<Longrightarrow> distinct (take i xs)"

  2749 apply(induct xs arbitrary: i)

  2750  apply simp

  2751 apply (case_tac i)

  2752  apply simp_all

  2753 apply(blast dest:in_set_takeD)

  2754 done

  2755

  2756 lemma distinct_drop[simp]: "distinct xs \<Longrightarrow> distinct (drop i xs)"

  2757 apply(induct xs arbitrary: i)

  2758  apply simp

  2759 apply (case_tac i)

  2760  apply simp_all

  2761 done

  2762

  2763 lemma distinct_list_update:

  2764 assumes d: "distinct xs" and a: "a \<notin> set xs - {xs!i}"

  2765 shows "distinct (xs[i:=a])"

  2766 proof (cases "i < length xs")

  2767   case True

  2768   with a have "a \<notin> set (take i xs @ xs ! i # drop (Suc i) xs) - {xs!i}"

  2769     apply (drule_tac id_take_nth_drop) by simp

  2770   with d True show ?thesis

  2771     apply (simp add: upd_conv_take_nth_drop)

  2772     apply (drule subst [OF id_take_nth_drop]) apply assumption

  2773     apply simp apply (cases "a = xs!i") apply simp by blast

  2774 next

  2775   case False with d show ?thesis by auto

  2776 qed

  2777

  2778 lemma distinct_concat:

  2779   assumes "distinct xs"

  2780   and "\<And> ys. ys \<in> set xs \<Longrightarrow> distinct ys"

  2781   and "\<And> ys zs. \<lbrakk> ys \<in> set xs ; zs \<in> set xs ; ys \<noteq> zs \<rbrakk> \<Longrightarrow> set ys \<inter> set zs = {}"

  2782   shows "distinct (concat xs)"

  2783   using assms by (induct xs) auto

  2784

  2785 text {* It is best to avoid this indexed version of distinct, but

  2786 sometimes it is useful. *}

  2787

  2788 lemma distinct_conv_nth:

  2789 "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j --> xs!i \<noteq> xs!j)"

  2790 apply (induct xs, simp, simp)

  2791 apply (rule iffI, clarsimp)

  2792  apply (case_tac i)

  2793 apply (case_tac j, simp)

  2794 apply (simp add: set_conv_nth)

  2795  apply (case_tac j)

  2796 apply (clarsimp simp add: set_conv_nth, simp)

  2797 apply (rule conjI)

  2798 (*TOO SLOW

  2799 apply (metis Zero_neq_Suc gr0_conv_Suc in_set_conv_nth lessI less_trans_Suc nth_Cons' nth_Cons_Suc)

  2800 *)

  2801  apply (clarsimp simp add: set_conv_nth)

  2802  apply (erule_tac x = 0 in allE, simp)

  2803  apply (erule_tac x = "Suc i" in allE, simp, clarsimp)

  2804 (*TOO SLOW

  2805 apply (metis Suc_Suc_eq lessI less_trans_Suc nth_Cons_Suc)

  2806 *)

  2807 apply (erule_tac x = "Suc i" in allE, simp)

  2808 apply (erule_tac x = "Suc j" in allE, simp)

  2809 done

  2810

  2811 lemma nth_eq_iff_index_eq:

  2812  "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"

  2813 by(auto simp: distinct_conv_nth)

  2814

  2815 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"

  2816 by (induct xs) auto

  2817

  2818 lemma card_distinct: "card (set xs) = size xs ==> distinct xs"

  2819 proof (induct xs)

  2820   case Nil thus ?case by simp

  2821 next

  2822   case (Cons x xs)

  2823   show ?case

  2824   proof (cases "x \<in> set xs")

  2825     case False with Cons show ?thesis by simp

  2826   next

  2827     case True with Cons.prems

  2828     have "card (set xs) = Suc (length xs)"

  2829       by (simp add: card_insert_if split: split_if_asm)

  2830     moreover have "card (set xs) \<le> length xs" by (rule card_length)

  2831     ultimately have False by simp

  2832     thus ?thesis ..

  2833   qed

  2834 qed

  2835

  2836 lemma not_distinct_decomp: "~ distinct ws ==> EX xs ys zs y. ws = xs@[y]@ys@[y]@zs"

  2837 apply (induct n == "length ws" arbitrary:ws) apply simp

  2838 apply(case_tac ws) apply simp

  2839 apply (simp split:split_if_asm)

  2840 apply (metis Cons_eq_appendI eq_Nil_appendI split_list)

  2841 done

  2842

  2843 lemma length_remdups_concat:

  2844  "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"

  2845 by(simp add: set_concat distinct_card[symmetric])

  2846

  2847 lemma length_remdups_card_conv: "length(remdups xs) = card(set xs)"

  2848 proof -

  2849   have xs: "concat[xs] = xs" by simp

  2850   from length_remdups_concat[of "[xs]"] show ?thesis unfolding xs by simp

  2851 qed

  2852

  2853 lemma remdups_remdups:

  2854   "remdups (remdups xs) = remdups xs"

  2855   by (induct xs) simp_all

  2856

  2857 lemma distinct_butlast:

  2858   assumes "xs \<noteq> []" and "distinct xs"

  2859   shows "distinct (butlast xs)"

  2860 proof -

  2861   from xs \<noteq> [] obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto

  2862   with distinct xs show ?thesis by simp

  2863 qed

  2864

  2865

  2866 subsubsection {* List summation: @{const listsum} and @{text"\<Sum>"}*}

  2867

  2868 lemma listsum_append [simp]: "listsum (xs @ ys) = listsum xs + listsum ys"

  2869 by (induct xs) (simp_all add:add_assoc)

  2870

  2871 lemma listsum_rev [simp]:

  2872   fixes xs :: "'a\<Colon>comm_monoid_add list"

  2873   shows "listsum (rev xs) = listsum xs"

  2874 by (induct xs) (simp_all add:add_ac)

  2875

  2876 lemma listsum_map_remove1:

  2877 fixes f :: "'a \<Rightarrow> ('b::comm_monoid_add)"

  2878 shows "x : set xs \<Longrightarrow> listsum(map f xs) = f x + listsum(map f (remove1 x xs))"

  2879 by (induct xs)(auto simp add:add_ac)

  2880

  2881 lemma list_size_conv_listsum:

  2882   "list_size f xs = listsum (map f xs) + size xs"

  2883 by(induct xs) auto

  2884

  2885 lemma listsum_foldr: "listsum xs = foldr (op +) xs 0"

  2886 by (induct xs) auto

  2887

  2888 lemma length_concat: "length (concat xss) = listsum (map length xss)"

  2889 by (induct xss) simp_all

  2890

  2891 lemma listsum_map_filter:

  2892   fixes f :: "'a \<Rightarrow> 'b \<Colon> comm_monoid_add"

  2893   assumes "\<And> x. \<lbrakk> x \<in> set xs ; \<not> P x \<rbrakk> \<Longrightarrow> f x = 0"

  2894   shows "listsum (map f (filter P xs)) = listsum (map f xs)"

  2895 using assms by (induct xs) auto

  2896

  2897 text{* For efficient code generation ---

  2898        @{const listsum} is not tail recursive but @{const foldl} is. *}

  2899 lemma listsum[code_unfold]: "listsum xs = foldl (op +) 0 xs"

  2900 by(simp add:listsum_foldr foldl_foldr1)

  2901

  2902 lemma distinct_listsum_conv_Setsum:

  2903   "distinct xs \<Longrightarrow> listsum xs = Setsum(set xs)"

  2904 by (induct xs) simp_all

  2905

  2906 lemma listsum_eq_0_nat_iff_nat[simp]:

  2907   "listsum ns = (0::nat) \<longleftrightarrow> (\<forall> n \<in> set ns. n = 0)"

  2908 by(simp add: listsum)

  2909

  2910 lemma elem_le_listsum_nat: "k<size ns \<Longrightarrow> ns!k <= listsum(ns::nat list)"

  2911 apply(induct ns arbitrary: k)

  2912  apply simp

  2913 apply(fastsimp simp add:nth_Cons split: nat.split)

  2914 done

  2915

  2916 lemma listsum_update_nat: "k<size ns \<Longrightarrow>

  2917   listsum (ns[k := (n::nat)]) = listsum ns + n - ns!k"

  2918 apply(induct ns arbitrary:k)

  2919  apply (auto split:nat.split)

  2920 apply(drule elem_le_listsum_nat)

  2921 apply arith

  2922 done

  2923

  2924 text{* Some syntactic sugar for summing a function over a list: *}

  2925

  2926 syntax

  2927   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)

  2928 syntax (xsymbols)

  2929   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)

  2930 syntax (HTML output)

  2931   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)

  2932

  2933 translations -- {* Beware of argument permutation! *}

  2934   "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"

  2935   "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"

  2936

  2937 lemma listsum_triv: "(\<Sum>x\<leftarrow>xs. r) = of_nat (length xs) * r"

  2938   by (induct xs) (simp_all add: left_distrib)

  2939

  2940 lemma listsum_0 [simp]: "(\<Sum>x\<leftarrow>xs. 0) = 0"

  2941   by (induct xs) (simp_all add: left_distrib)

  2942

  2943 text{* For non-Abelian groups @{text xs} needs to be reversed on one side: *}

  2944 lemma uminus_listsum_map:

  2945   fixes f :: "'a \<Rightarrow> 'b\<Colon>ab_group_add"

  2946   shows "- listsum (map f xs) = (listsum (map (uminus o f) xs))"

  2947 by (induct xs) simp_all

  2948

  2949 lemma listsum_addf:

  2950   fixes f g :: "'a \<Rightarrow> 'b::comm_monoid_add"

  2951   shows "(\<Sum>x\<leftarrow>xs. f x + g x) = listsum (map f xs) + listsum (map g xs)"

  2952 by (induct xs) (simp_all add: algebra_simps)

  2953

  2954 lemma listsum_subtractf:

  2955   fixes f g :: "'a \<Rightarrow> 'b::ab_group_add"

  2956   shows "(\<Sum>x\<leftarrow>xs. f x - g x) = listsum (map f xs) - listsum (map g xs)"

  2957 by (induct xs) simp_all

  2958

  2959 lemma listsum_const_mult:

  2960   fixes f :: "'a \<Rightarrow> 'b::semiring_0"

  2961   shows "(\<Sum>x\<leftarrow>xs. c * f x) = c * (\<Sum>x\<leftarrow>xs. f x)"

  2962 by (induct xs, simp_all add: algebra_simps)

  2963

  2964 lemma listsum_mult_const:

  2965   fixes f :: "'a \<Rightarrow> 'b::semiring_0"

  2966   shows "(\<Sum>x\<leftarrow>xs. f x * c) = (\<Sum>x\<leftarrow>xs. f x) * c"

  2967 by (induct xs, simp_all add: algebra_simps)

  2968

  2969 lemma listsum_abs:

  2970   fixes xs :: "'a::ordered_ab_group_add_abs list"

  2971   shows "\<bar>listsum xs\<bar> \<le> listsum (map abs xs)"

  2972 by (induct xs, simp, simp add: order_trans [OF abs_triangle_ineq])

  2973

  2974 lemma listsum_mono:

  2975   fixes f g :: "'a \<Rightarrow> 'b::{comm_monoid_add, ordered_ab_semigroup_add}"

  2976   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)"

  2977 by (induct xs, simp, simp add: add_mono)

  2978

  2979 lemma listsum_distinct_conv_setsum_set:

  2980   "distinct xs \<Longrightarrow> listsum (map f xs) = setsum f (set xs)"

  2981   by (induct xs) simp_all

  2982

  2983 lemma interv_listsum_conv_setsum_set_nat:

  2984   "listsum (map f [m..<n]) = setsum f (set [m..<n])"

  2985   by (simp add: listsum_distinct_conv_setsum_set)

  2986

  2987 lemma interv_listsum_conv_setsum_set_int:

  2988   "listsum (map f [k..l]) = setsum f (set [k..l])"

  2989   by (simp add: listsum_distinct_conv_setsum_set)

  2990

  2991 text {* General equivalence between @{const listsum} and @{const setsum} *}

  2992 lemma listsum_setsum_nth:

  2993   "listsum xs = (\<Sum> i = 0 ..< length xs. xs ! i)"

  2994   using interv_listsum_conv_setsum_set_nat [of "op ! xs" 0 "length xs"] by (simp add: map_nth)

  2995

  2996

  2997 subsubsection {* @{const insert} *}

  2998

  2999 lemma in_set_insert [simp]:

  3000   "x \<in> set xs \<Longrightarrow> List.insert x xs = xs"

  3001   by (simp add: List.insert_def)

  3002

  3003 lemma not_in_set_insert [simp]:

  3004   "x \<notin> set xs \<Longrightarrow> List.insert x xs = x # xs"

  3005   by (simp add: List.insert_def)

  3006

  3007 lemma insert_Nil [simp]:

  3008   "List.insert x [] = [x]"

  3009   by simp

  3010

  3011 lemma set_insert [simp]:

  3012   "set (List.insert x xs) = insert x (set xs)"

  3013   by (auto simp add: List.insert_def)

  3014

  3015 lemma distinct_insert [simp]:

  3016   "distinct xs \<Longrightarrow> distinct (List.insert x xs)"

  3017   by (simp add: List.insert_def)

  3018

  3019 lemma insert_remdups:

  3020   "List.insert x (remdups xs) = remdups (List.insert x xs)"

  3021   by (simp add: List.insert_def)

  3022

  3023 lemma distinct_induct [consumes 1, case_names Nil insert]:

  3024   assumes "distinct xs"

  3025   assumes "P []"

  3026   assumes insert: "\<And>x xs. distinct xs \<Longrightarrow> x \<notin> set xs

  3027     \<Longrightarrow> P xs \<Longrightarrow> P (List.insert x xs)"

  3028   shows "P xs"

  3029 using distinct xs proof (induct xs)

  3030   case Nil from P [] show ?case .

  3031 next

  3032   case (Cons x xs)

  3033   then have "distinct xs" and "x \<notin> set xs" and "P xs" by simp_all

  3034   with insert have "P (List.insert x xs)" .

  3035   with x \<notin> set xs show ?case by simp

  3036 qed

  3037

  3038

  3039 subsubsection {* @{text remove1} *}

  3040

  3041 lemma remove1_append:

  3042   "remove1 x (xs @ ys) =

  3043   (if x \<in> set xs then remove1 x xs @ ys else xs @ remove1 x ys)"

  3044 by (induct xs) auto

  3045

  3046 lemma remove1_commute: "remove1 x (remove1 y zs) = remove1 y (remove1 x zs)"

  3047 by (induct zs) auto

  3048

  3049 lemma in_set_remove1[simp]:

  3050   "a \<noteq> b \<Longrightarrow> a : set(remove1 b xs) = (a : set xs)"

  3051 apply (induct xs)

  3052 apply auto

  3053 done

  3054

  3055 lemma set_remove1_subset: "set(remove1 x xs) <= set xs"

  3056 apply(induct xs)

  3057  apply simp

  3058 apply simp

  3059 apply blast

  3060 done

  3061

  3062 lemma set_remove1_eq [simp]: "distinct xs ==> set(remove1 x xs) = set xs - {x}"

  3063 apply(induct xs)

  3064  apply simp

  3065 apply simp

  3066 apply blast

  3067 done

  3068

  3069 lemma length_remove1:

  3070   "length(remove1 x xs) = (if x : set xs then length xs - 1 else length xs)"

  3071 apply (induct xs)

  3072  apply (auto dest!:length_pos_if_in_set)

  3073 done

  3074

  3075 lemma remove1_filter_not[simp]:

  3076   "\<not> P x \<Longrightarrow> remove1 x (filter P xs) = filter P xs"

  3077 by(induct xs) auto

  3078

  3079 lemma notin_set_remove1[simp]: "x ~: set xs ==> x ~: set(remove1 y xs)"

  3080 apply(insert set_remove1_subset)

  3081 apply fast

  3082 done

  3083

  3084 lemma distinct_remove1[simp]: "distinct xs ==> distinct(remove1 x xs)"

  3085 by (induct xs) simp_all

  3086

  3087 lemma remove1_remdups:

  3088   "distinct xs \<Longrightarrow> remove1 x (remdups xs) = remdups (remove1 x xs)"

  3089   by (induct xs) simp_all

  3090

  3091 lemma remove1_idem:

  3092   assumes "x \<notin> set xs"

  3093   shows "remove1 x xs = xs"

  3094   using assms by (induct xs) simp_all

  3095

  3096

  3097 subsubsection {* @{text removeAll} *}

  3098

  3099 lemma removeAll_filter_not_eq:

  3100   "removeAll x = filter (\<lambda>y. x \<noteq> y)"

  3101 proof

  3102   fix xs

  3103   show "removeAll x xs = filter (\<lambda>y. x \<noteq> y) xs"

  3104     by (induct xs) auto

  3105 qed

  3106

  3107 lemma removeAll_append[simp]:

  3108   "removeAll x (xs @ ys) = removeAll x xs @ removeAll x ys"

  3109 by (induct xs) auto

  3110

  3111 lemma set_removeAll[simp]: "set(removeAll x xs) = set xs - {x}"

  3112 by (induct xs) auto

  3113

  3114 lemma removeAll_id[simp]: "x \<notin> set xs \<Longrightarrow> removeAll x xs = xs"

  3115 by (induct xs) auto

  3116

  3117 (* Needs count:: 'a \<Rightarrow> a' list \<Rightarrow> nat

  3118 lemma length_removeAll:

  3119   "length(removeAll x xs) = length xs - count x xs"

  3120 *)

  3121

  3122 lemma removeAll_filter_not[simp]:

  3123   "\<not> P x \<Longrightarrow> removeAll x (filter P xs) = filter P xs"

  3124 by(induct xs) auto

  3125

  3126 lemma distinct_removeAll:

  3127   "distinct xs \<Longrightarrow> distinct (removeAll x xs)"

  3128   by (simp add: removeAll_filter_not_eq)

  3129

  3130 lemma distinct_remove1_removeAll:

  3131   "distinct xs ==> remove1 x xs = removeAll x xs"

  3132 by (induct xs) simp_all

  3133

  3134 lemma map_removeAll_inj_on: "inj_on f (insert x (set xs)) \<Longrightarrow>

  3135   map f (removeAll x xs) = removeAll (f x) (map f xs)"

  3136 by (induct xs) (simp_all add:inj_on_def)

  3137

  3138 lemma map_removeAll_inj: "inj f \<Longrightarrow>

  3139   map f (removeAll x xs) = removeAll (f x) (map f xs)"

  3140 by(metis map_removeAll_inj_on subset_inj_on subset_UNIV)

  3141

  3142

  3143 subsubsection {* @{text replicate} *}

  3144

  3145 lemma length_replicate [simp]: "length (replicate n x) = n"

  3146 by (induct n) auto

  3147

  3148 lemma Ex_list_of_length: "\<exists>xs. length xs = n"

  3149 by (rule exI[of _ "replicate n undefined"]) simp

  3150

  3151 lemma map_replicate [simp]: "map f (replicate n x) = replicate n (f x)"

  3152 by (induct n) auto

  3153

  3154 lemma map_replicate_const:

  3155   "map (\<lambda> x. k) lst = replicate (length lst) k"

  3156   by (induct lst) auto

  3157

  3158 lemma replicate_app_Cons_same:

  3159 "(replicate n x) @ (x # xs) = x # replicate n x @ xs"

  3160 by (induct n) auto

  3161

  3162 lemma rev_replicate [simp]: "rev (replicate n x) = replicate n x"

  3163 apply (induct n, simp)

  3164 apply (simp add: replicate_app_Cons_same)

  3165 done

  3166

  3167 lemma replicate_add: "replicate (n + m) x = replicate n x @ replicate m x"

  3168 by (induct n) auto

  3169

  3170 text{* Courtesy of Matthias Daum: *}

  3171 lemma append_replicate_commute:

  3172   "replicate n x @ replicate k x = replicate k x @ replicate n x"

  3173 apply (simp add: replicate_add [THEN sym])

  3174 apply (simp add: add_commute)

  3175 done

  3176

  3177 text{* Courtesy of Andreas Lochbihler: *}

  3178 lemma filter_replicate:

  3179   "filter P (replicate n x) = (if P x then replicate n x else [])"

  3180 by(induct n) auto

  3181

  3182 lemma hd_replicate [simp]: "n \<noteq> 0 ==> hd (replicate n x) = x"

  3183 by (induct n) auto

  3184

  3185 lemma tl_replicate [simp]: "n \<noteq> 0 ==> tl (replicate n x) = replicate (n - 1) x"

  3186 by (induct n) auto

  3187

  3188 lemma last_replicate [simp]: "n \<noteq> 0 ==> last (replicate n x) = x"

  3189 by (atomize (full), induct n) auto

  3190

  3191 lemma nth_replicate[simp]: "i < n ==> (replicate n x)!i = x"

  3192 apply (induct n arbitrary: i, simp)

  3193 apply (simp add: nth_Cons split: nat.split)

  3194 done

  3195

  3196 text{* Courtesy of Matthias Daum (2 lemmas): *}

  3197 lemma take_replicate[simp]: "take i (replicate k x) = replicate (min i k) x"

  3198 apply (case_tac "k \<le> i")

  3199  apply  (simp add: min_def)

  3200 apply (drule not_leE)

  3201 apply (simp add: min_def)

  3202 apply (subgoal_tac "replicate k x = replicate i x @ replicate (k - i) x")

  3203  apply  simp

  3204 apply (simp add: replicate_add [symmetric])

  3205 done

  3206

  3207 lemma drop_replicate[simp]: "drop i (replicate k x) = replicate (k-i) x"

  3208 apply (induct k arbitrary: i)

  3209  apply simp

  3210 apply clarsimp

  3211 apply (case_tac i)

  3212  apply simp

  3213 apply clarsimp

  3214 done

  3215

  3216

  3217 lemma set_replicate_Suc: "set (replicate (Suc n) x) = {x}"

  3218 by (induct n) auto

  3219

  3220 lemma set_replicate [simp]: "n \<noteq> 0 ==> set (replicate n x) = {x}"

  3221 by (fast dest!: not0_implies_Suc intro!: set_replicate_Suc)

  3222

  3223 lemma set_replicate_conv_if: "set (replicate n x) = (if n = 0 then {} else {x})"

  3224 by auto

  3225

  3226 lemma in_set_replicate[simp]: "(x : set (replicate n y)) = (x = y & n \<noteq> 0)"

  3227 by (simp add: set_replicate_conv_if)

  3228

  3229 lemma Ball_set_replicate[simp]:

  3230   "(ALL x : set(replicate n a). P x) = (P a | n=0)"

  3231 by(simp add: set_replicate_conv_if)

  3232

  3233 lemma Bex_set_replicate[simp]:

  3234   "(EX x : set(replicate n a). P x) = (P a & n\<noteq>0)"

  3235 by(simp add: set_replicate_conv_if)

  3236

  3237 lemma replicate_append_same:

  3238   "replicate i x @ [x] = x # replicate i x"

  3239   by (induct i) simp_all

  3240

  3241 lemma map_replicate_trivial:

  3242   "map (\<lambda>i. x) [0..<i] = replicate i x"

  3243   by (induct i) (simp_all add: replicate_append_same)

  3244

  3245 lemma concat_replicate_trivial[simp]:

  3246   "concat (replicate i []) = []"

  3247   by (induct i) (auto simp add: map_replicate_const)

  3248

  3249 lemma replicate_empty[simp]: "(replicate n x = []) \<longleftrightarrow> n=0"

  3250 by (induct n) auto

  3251

  3252 lemma empty_replicate[simp]: "([] = replicate n x) \<longleftrightarrow> n=0"

  3253 by (induct n) auto

  3254

  3255 lemma replicate_eq_replicate[simp]:

  3256   "(replicate m x = replicate n y) \<longleftrightarrow> (m=n & (m\<noteq>0 \<longrightarrow> x=y))"

  3257 apply(induct m arbitrary: n)

  3258  apply simp

  3259 apply(induct_tac n)

  3260 apply auto

  3261 done

  3262

  3263

  3264 subsubsection{*@{text rotate1} and @{text rotate}*}

  3265

  3266 lemma rotate_simps[simp]: "rotate1 [] = [] \<and> rotate1 (x#xs) = xs @ [x]"

  3267 by(simp add:rotate1_def)

  3268

  3269 lemma rotate0[simp]: "rotate 0 = id"

  3270 by(simp add:rotate_def)

  3271

  3272 lemma rotate_Suc[simp]: "rotate (Suc n) xs = rotate1(rotate n xs)"

  3273 by(simp add:rotate_def)

  3274

  3275 lemma rotate_add:

  3276   "rotate (m+n) = rotate m o rotate n"

  3277 by(simp add:rotate_def funpow_add)

  3278

  3279 lemma rotate_rotate: "rotate m (rotate n xs) = rotate (m+n) xs"

  3280 by(simp add:rotate_add)

  3281

  3282 lemma rotate1_rotate_swap: "rotate1 (rotate n xs) = rotate n (rotate1 xs)"

  3283 by(simp add:rotate_def funpow_swap1)

  3284

  3285 lemma rotate1_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate1 xs = xs"

  3286 by(cases xs) simp_all

  3287

  3288 lemma rotate_length01[simp]: "length xs <= 1 \<Longrightarrow> rotate n xs = xs"

  3289 apply(induct n)

  3290  apply simp

  3291 apply (simp add:rotate_def)

  3292 done

  3293

  3294 lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]"

  3295 by(simp add:rotate1_def split:list.split)

  3296

  3297 lemma rotate_drop_take:

  3298   "rotate n xs = drop (n mod length xs) xs @ take (n mod length xs) xs"

  3299 apply(induct n)

  3300  apply simp

  3301 apply(simp add:rotate_def)

  3302 apply(cases "xs = []")

  3303  apply (simp)

  3304 apply(case_tac "n mod length xs = 0")

  3305  apply(simp add:mod_Suc)

  3306  apply(simp add: rotate1_hd_tl drop_Suc take_Suc)

  3307 apply(simp add:mod_Suc rotate1_hd_tl drop_Suc[symmetric] drop_tl[symmetric]

  3308                 take_hd_drop linorder_not_le)

  3309 done

  3310

  3311 lemma rotate_conv_mod: "rotate n xs = rotate (n mod length xs) xs"

  3312 by(simp add:rotate_drop_take)

  3313

  3314 lemma rotate_id[simp]: "n mod length xs = 0 \<Longrightarrow> rotate n xs = xs"

  3315 by(simp add:rotate_drop_take)

  3316

  3317 lemma length_rotate1[simp]: "length(rotate1 xs) = length xs"

  3318 by(simp add:rotate1_def split:list.split)

  3319

  3320 lemma length_rotate[simp]: "length(rotate n xs) = length xs"

  3321 by (induct n arbitrary: xs) (simp_all add:rotate_def)

  3322

  3323 lemma distinct1_rotate[simp]: "distinct(rotate1 xs) = distinct xs"

  3324 by(simp add:rotate1_def split:list.split) blast

  3325

  3326 lemma distinct_rotate[simp]: "distinct(rotate n xs) = distinct xs"

  3327 by (induct n) (simp_all add:rotate_def)

  3328

  3329 lemma rotate_map: "rotate n (map f xs) = map f (rotate n xs)"

  3330 by(simp add:rotate_drop_take take_map drop_map)

  3331

  3332 lemma set_rotate1[simp]: "set(rotate1 xs) = set xs"

  3333 by(simp add:rotate1_def split:list.split)

  3334

  3335 lemma set_rotate[simp]: "set(rotate n xs) = set xs"

  3336 by (induct n) (simp_all add:rotate_def)

  3337

  3338 lemma rotate1_is_Nil_conv[simp]: "(rotate1 xs = []) = (xs = [])"

  3339 by(simp add:rotate1_def split:list.split)

  3340

  3341 lemma rotate_is_Nil_conv[simp]: "(rotate n xs = []) = (xs = [])"

  3342 by (induct n) (simp_all add:rotate_def)

  3343

  3344 lemma rotate_rev:

  3345   "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"

  3346 apply(simp add:rotate_drop_take rev_drop rev_take)

  3347 apply(cases "length xs = 0")

  3348  apply simp

  3349 apply(cases "n mod length xs = 0")

  3350  apply simp

  3351 apply(simp add:rotate_drop_take rev_drop rev_take)

  3352 done

  3353

  3354 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"

  3355 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)

  3356 apply(subgoal_tac "length xs \<noteq> 0")

  3357  prefer 2 apply simp

  3358 using mod_less_divisor[of "length xs" n] by arith

  3359

  3360

  3361 subsubsection {* @{text sublist} --- a generalization of @{text nth} to sets *}

  3362

  3363 lemma sublist_empty [simp]: "sublist xs {} = []"

  3364 by (auto simp add: sublist_def)

  3365

  3366 lemma sublist_nil [simp]: "sublist [] A = []"

  3367 by (auto simp add: sublist_def)

  3368

  3369 lemma length_sublist:

  3370   "length(sublist xs I) = card{i. i < length xs \<and> i : I}"

  3371 by(simp add: sublist_def length_filter_conv_card cong:conj_cong)

  3372

  3373 lemma sublist_shift_lemma_Suc:

  3374   "map fst (filter (%p. P(Suc(snd p))) (zip xs is)) =

  3375    map fst (filter (%p. P(snd p)) (zip xs (map Suc is)))"

  3376 apply(induct xs arbitrary: "is")

  3377  apply simp

  3378 apply (case_tac "is")

  3379  apply simp

  3380 apply simp

  3381 done

  3382

  3383 lemma sublist_shift_lemma:

  3384      "map fst [p<-zip xs [i..<i + length xs] . snd p : A] =

  3385       map fst [p<-zip xs [0..<length xs] . snd p + i : A]"

  3386 by (induct xs rule: rev_induct) (simp_all add: add_commute)

  3387

  3388 lemma sublist_append:

  3389      "sublist (l @ l') A = sublist l A @ sublist l' {j. j + length l : A}"

  3390 apply (unfold sublist_def)

  3391 apply (induct l' rule: rev_induct, simp)

  3392 apply (simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)

  3393 apply (simp add: add_commute)

  3394 done

  3395

  3396 lemma sublist_Cons:

  3397 "sublist (x # l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"

  3398 apply (induct l rule: rev_induct)

  3399  apply (simp add: sublist_def)

  3400 apply (simp del: append_Cons add: append_Cons[symmetric] sublist_append)

  3401 done

  3402

  3403 lemma set_sublist: "set(sublist xs I) = {xs!i|i. i<size xs \<and> i \<in> I}"

  3404 apply(induct xs arbitrary: I)

  3405 apply(auto simp: sublist_Cons nth_Cons split:nat.split dest!: gr0_implies_Suc)

  3406 done

  3407

  3408 lemma set_sublist_subset: "set(sublist xs I) \<subseteq> set xs"

  3409 by(auto simp add:set_sublist)

  3410

  3411 lemma notin_set_sublistI[simp]: "x \<notin> set xs \<Longrightarrow> x \<notin> set(sublist xs I)"

  3412 by(auto simp add:set_sublist)

  3413

  3414 lemma in_set_sublistD: "x \<in> set(sublist xs I) \<Longrightarrow> x \<in> set xs"

  3415 by(auto simp add:set_sublist)

  3416

  3417 lemma sublist_singleton [simp]: "sublist [x] A = (if 0 : A then [x] else [])"

  3418 by (simp add: sublist_Cons)

  3419

  3420

  3421 lemma distinct_sublistI[simp]: "distinct xs \<Longrightarrow> distinct(sublist xs I)"

  3422 apply(induct xs arbitrary: I)

  3423  apply simp

  3424 apply(auto simp add:sublist_Cons)

  3425 done

  3426

  3427

  3428 lemma sublist_upt_eq_take [simp]: "sublist l {..<n} = take n l"

  3429 apply (induct l rule: rev_induct, simp)

  3430 apply (simp split: nat_diff_split add: sublist_append)

  3431 done

  3432

  3433 lemma filter_in_sublist:

  3434  "distinct xs \<Longrightarrow> filter (%x. x \<in> set(sublist xs s)) xs = sublist xs s"

  3435 proof (induct xs arbitrary: s)

  3436   case Nil thus ?case by simp

  3437 next

  3438   case (Cons a xs)

  3439   moreover hence "!x. x: set xs \<longrightarrow> x \<noteq> a" by auto

  3440   ultimately show ?case by(simp add: sublist_Cons cong:filter_cong)

  3441 qed

  3442

  3443

  3444 subsubsection {* @{const splice} *}

  3445

  3446 lemma splice_Nil2 [simp, code]:

  3447  "splice xs [] = xs"

  3448 by (cases xs) simp_all

  3449

  3450 lemma splice_Cons_Cons [simp, code]:

  3451  "splice (x#xs) (y#ys) = x # y # splice xs ys"

  3452 by simp

  3453

  3454 declare splice.simps(2) [simp del, code del]

  3455

  3456 lemma length_splice[simp]: "length(splice xs ys) = length xs + length ys"

  3457 apply(induct xs arbitrary: ys) apply simp

  3458 apply(case_tac ys)

  3459  apply auto

  3460 done

  3461

  3462

  3463 subsubsection {* Transpose *}

  3464

  3465 function transpose where

  3466 "transpose []             = []" |

  3467 "transpose ([]     # xss) = transpose xss" |

  3468 "transpose ((x#xs) # xss) =

  3469   (x # [h. (h#t) \<leftarrow> xss]) # transpose (xs # [t. (h#t) \<leftarrow> xss])"

  3470 by pat_completeness auto

  3471

  3472 lemma transpose_aux_filter_head:

  3473   "concat (map (list_case [] (\<lambda>h t. [h])) xss) =

  3474   map (\<lambda>xs. hd xs) [ys\<leftarrow>xss . ys \<noteq> []]"

  3475   by (induct xss) (auto split: list.split)

  3476

  3477 lemma transpose_aux_filter_tail:

  3478   "concat (map (list_case [] (\<lambda>h t. [t])) xss) =

  3479   map (\<lambda>xs. tl xs) [ys\<leftarrow>xss . ys \<noteq> []]"

  3480   by (induct xss) (auto split: list.split)

  3481

  3482 lemma transpose_aux_max:

  3483   "max (Suc (length xs)) (foldr (\<lambda>xs. max (length xs)) xss 0) =

  3484   Suc (max (length xs) (foldr (\<lambda>x. max (length x - Suc 0)) [ys\<leftarrow>xss . ys\<noteq>[]] 0))"

  3485   (is "max _ ?foldB = Suc (max _ ?foldA)")

  3486 proof (cases "[ys\<leftarrow>xss . ys\<noteq>[]] = []")

  3487   case True

  3488   hence "foldr (\<lambda>xs. max (length xs)) xss 0 = 0"

  3489   proof (induct xss)

  3490     case (Cons x xs)

  3491     moreover hence "x = []" by (cases x) auto

  3492     ultimately show ?case by auto

  3493   qed simp

  3494   thus ?thesis using True by simp

  3495 next

  3496   case False

  3497

  3498   have foldA: "?foldA = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0 - 1"

  3499     by (induct xss) auto

  3500   have foldB: "?foldB = foldr (\<lambda>x. max (length x)) [ys\<leftarrow>xss . ys \<noteq> []] 0"

  3501     by (induct xss) auto

  3502

  3503   have "0 < ?foldB"

  3504   proof -

  3505     from False

  3506     obtain z zs where zs: "[ys\<leftarrow>xss . ys \<noteq> []] = z#zs" by (auto simp: neq_Nil_conv)

  3507     hence "z \<in> set ([ys\<leftarrow>xss . ys \<noteq> []])" by auto

  3508     hence "z \<noteq> []" by auto

  3509     thus ?thesis

  3510       unfolding foldB zs

  3511       by (auto simp: max_def intro: less_le_trans)

  3512   qed

  3513   thus ?thesis

  3514     unfolding foldA foldB max_Suc_Suc[symmetric]

  3515     by simp

  3516 qed

  3517

  3518 termination transpose

  3519   by (relation "measure (\<lambda>xs. foldr (\<lambda>xs. max (length xs)) xs 0 + length xs)")

  3520      (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max less_Suc_eq_le)

  3521

  3522 lemma transpose_empty: "(transpose xs = []) \<longleftrightarrow> (\<forall>x \<in> set xs. x = [])"

  3523   by (induct rule: transpose.induct) simp_all

  3524

  3525 lemma length_transpose:

  3526   fixes xs :: "'a list list"

  3527   shows "length (transpose xs) = foldr (\<lambda>xs. max (length xs)) xs 0"

  3528   by (induct rule: transpose.induct)

  3529     (auto simp: transpose_aux_filter_tail foldr_map comp_def transpose_aux_max

  3530                 max_Suc_Suc[symmetric] simp del: max_Suc_Suc)

  3531

  3532 lemma nth_transpose:

  3533   fixes xs :: "'a list list"

  3534   assumes "i < length (transpose xs)"

  3535   shows "transpose xs ! i = map (\<lambda>xs. xs ! i) [ys \<leftarrow> xs. i < length ys]"

  3536 using assms proof (induct arbitrary: i rule: transpose.induct)

  3537   case (3 x xs xss)

  3538   def XS == "(x # xs) # xss"

  3539   hence [simp]: "XS \<noteq> []" by auto

  3540   thus ?case

  3541   proof (cases i)

  3542     case 0

  3543     thus ?thesis by (simp add: transpose_aux_filter_head hd_conv_nth)

  3544   next

  3545     case (Suc j)

  3546     have *: "\<And>xss. xs # map tl xss = map tl ((x#xs)#xss)" by simp

  3547     have **: "\<And>xss. (x#xs) # filter (\<lambda>ys. ys \<noteq> []) xss = filter (\<lambda>ys. ys \<noteq> []) ((x#xs)#xss)" by simp

  3548     { fix x have "Suc j < length x \<longleftrightarrow> x \<noteq> [] \<and> j < length x - Suc 0"

  3549       by (cases x) simp_all

  3550     } note *** = this

  3551

  3552     have j_less: "j < length (transpose (xs # concat (map (list_case [] (\<lambda>h t. [t])) xss)))"

  3553       using "3.prems" by (simp add: transpose_aux_filter_tail length_transpose Suc)

  3554

  3555     show ?thesis

  3556       unfolding transpose.simps i = Suc j nth_Cons_Suc "3.hyps"[OF j_less]

  3557       apply (auto simp: transpose_aux_filter_tail filter_map comp_def length_transpose * ** *** XS_def[symmetric])

  3558       apply (rule_tac y=x in list.exhaust)

  3559       by auto

  3560   qed

  3561 qed simp_all

  3562

  3563 lemma transpose_map_map:

  3564   "transpose (map (map f) xs) = map (map f) (transpose xs)"

  3565 proof (rule nth_equalityI, safe)

  3566   have [simp]: "length (transpose (map (map f) xs)) = length (transpose xs)"

  3567     by (simp add: length_transpose foldr_map comp_def)

  3568   show "length (transpose (map (map f) xs)) = length (map (map f) (transpose xs))" by simp

  3569

  3570   fix i assume "i < length (transpose (map (map f) xs))"

  3571   thus "transpose (map (map f) xs) ! i = map (map f) (transpose xs) ! i"

  3572     by (simp add: nth_transpose filter_map comp_def)

  3573 qed

  3574

  3575

  3576 subsubsection {* (In)finiteness *}

  3577

  3578 lemma finite_maxlen:

  3579   "finite (M::'a list set) ==> EX n. ALL s:M. size s < n"

  3580 proof (induct rule: finite.induct)

  3581   case emptyI show ?case by simp

  3582 next

  3583   case (insertI M xs)

  3584   then obtain n where "\<forall>s\<in>M. length s < n" by blast

  3585   hence "ALL s:insert xs M. size s < max n (size xs) + 1" by auto

  3586   thus ?case ..

  3587 qed

  3588

  3589 lemma finite_lists_length_eq:

  3590 assumes "finite A"

  3591 shows "finite {xs. set xs \<subseteq> A \<and> length xs = n}" (is "finite (?S n)")

  3592 proof(induct n)

  3593   case 0 show ?case by simp

  3594 next

  3595   case (Suc n)

  3596   have "?S (Suc n) = (\<Union>x\<in>A. (\<lambda>xs. x#xs)  ?S n)"

  3597     by (auto simp:length_Suc_conv)

  3598   then show ?case using finite A

  3599     by (auto intro: finite_imageI Suc) (* FIXME metis? *)

  3600 qed

  3601

  3602 lemma finite_lists_length_le:

  3603   assumes "finite A" shows "finite {xs. set xs \<subseteq> A \<and> length xs \<le> n}"

  3604  (is "finite ?S")

  3605 proof-

  3606   have "?S = (\<Union>n\<in>{0..n}. {xs. set xs \<subseteq> A \<and> length xs = n})" by auto

  3607   thus ?thesis by (auto intro: finite_lists_length_eq[OF finite A])

  3608 qed

  3609

  3610 lemma infinite_UNIV_listI: "~ finite(UNIV::'a list set)"

  3611 apply(rule notI)

  3612 apply(drule finite_maxlen)

  3613 apply (metis UNIV_I length_replicate less_not_refl)

  3614 done

  3615

  3616

  3617 subsection {* Sorting *}

  3618

  3619 text{* Currently it is not shown that @{const sort} returns a

  3620 permutation of its input because the nicest proof is via multisets,

  3621 which are not yet available. Alternatively one could define a function

  3622 that counts the number of occurrences of an element in a list and use

  3623 that instead of multisets to state the correctness property. *}

  3624

  3625 context linorder

  3626 begin

  3627

  3628 lemma length_insert[simp] : "length (insort_key f x xs) = Suc (length xs)"

  3629 by (induct xs, auto)

  3630

  3631 lemma insort_left_comm:

  3632   "insort x (insort y xs) = insort y (insort x xs)"

  3633   by (induct xs) auto

  3634

  3635 lemma fun_left_comm_insort:

  3636   "fun_left_comm insort"

  3637 proof

  3638 qed (fact insort_left_comm)

  3639

  3640 lemma sort_key_simps [simp]:

  3641   "sort_key f [] = []"

  3642   "sort_key f (x#xs) = insort_key f x (sort_key f xs)"

  3643   by (simp_all add: sort_key_def)

  3644

  3645 lemma sort_foldl_insort:

  3646   "sort xs = foldl (\<lambda>ys x. insort x ys) [] xs"

  3647   by (simp add: sort_key_def foldr_foldl foldl_rev insort_left_comm)

  3648

  3649 lemma length_sort[simp]: "length (sort_key f xs) = length xs"

  3650 by (induct xs, auto)

  3651

  3652 lemma sorted_Cons: "sorted (x#xs) = (sorted xs & (ALL y:set xs. x <= y))"

  3653 apply(induct xs arbitrary: x) apply simp

  3654 by simp (blast intro: order_trans)

  3655

  3656 lemma sorted_append:

  3657   "sorted (xs@ys) = (sorted xs & sorted ys & (\<forall>x \<in> set xs. \<forall>y \<in> set ys. x\<le>y))"

  3658 by (induct xs) (auto simp add:sorted_Cons)

  3659

  3660 lemma sorted_nth_mono:

  3661   "sorted xs \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!i \<le> xs!j"

  3662 by (induct xs arbitrary: i j) (auto simp:nth_Cons' sorted_Cons)

  3663

  3664 lemma sorted_rev_nth_mono:

  3665   "sorted (rev xs) \<Longrightarrow> i \<le> j \<Longrightarrow> j < length xs \<Longrightarrow> xs!j \<le> xs!i"

  3666 using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]

  3667       rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]

  3668 by auto

  3669

  3670 lemma sorted_nth_monoI:

  3671   "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"

  3672 proof (induct xs)

  3673   case (Cons x xs)

  3674   have "sorted xs"

  3675   proof (rule Cons.hyps)

  3676     fix i j assume "i \<le> j" and "j < length xs"

  3677     with Cons.prems[of "Suc i" "Suc j"]

  3678     show "xs ! i \<le> xs ! j" by auto

  3679   qed

  3680   moreover

  3681   {

  3682     fix y assume "y \<in> set xs"

  3683     then obtain j where "j < length xs" and "xs ! j = y"

  3684       unfolding in_set_conv_nth by blast

  3685     with Cons.prems[of 0 "Suc j"]

  3686     have "x \<le> y"

  3687       by auto

  3688   }

  3689   ultimately

  3690   show ?case

  3691     unfolding sorted_Cons by auto

  3692 qed simp

  3693

  3694 lemma sorted_equals_nth_mono:

  3695   "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"

  3696 by (auto intro: sorted_nth_monoI sorted_nth_mono)

  3697

  3698 lemma set_insort: "set(insort_key f x xs) = insert x (set xs)"

  3699 by (induct xs) auto

  3700

  3701 lemma set_sort[simp]: "set(sort_key f xs) = set xs"

  3702 by (induct xs) (simp_all add:set_insort)

  3703

  3704 lemma distinct_insort: "distinct (insort_key f x xs) = (x \<notin> set xs \<and> distinct xs)"

  3705 by(induct xs)(auto simp:set_insort)

  3706

  3707 lemma distinct_sort[simp]: "distinct (sort_key f xs) = distinct xs"

  3708 by(induct xs)(simp_all add:distinct_insort set_sort)

  3709

  3710 lemma sorted_insort_key: "sorted (map f (insort_key f x xs)) = sorted (map f xs)"

  3711 by(induct xs)(auto simp:sorted_Cons set_insort)

  3712

  3713 lemma sorted_insort: "sorted (insort x xs) = sorted xs"

  3714 using sorted_insort_key[where f="\<lambda>x. x"] by simp

  3715

  3716 theorem sorted_sort_key[simp]: "sorted (map f (sort_key f xs))"

  3717 by(induct xs)(auto simp:sorted_insort_key)

  3718

  3719 theorem sorted_sort[simp]: "sorted (sort xs)"

  3720 by(induct xs)(auto simp:sorted_insort)

  3721

  3722 lemma sorted_butlast:

  3723   assumes "xs \<noteq> []" and "sorted xs"

  3724   shows "sorted (butlast xs)"

  3725 proof -

  3726   from xs \<noteq> [] obtain ys y where "xs = ys @ [y]" by (cases xs rule: rev_cases) auto

  3727   with sorted xs show ?thesis by (simp add: sorted_append)

  3728 qed

  3729

  3730 lemma insort_not_Nil [simp]:

  3731   "insort_key f a xs \<noteq> []"

  3732   by (induct xs) simp_all

  3733

  3734 lemma insort_is_Cons: "\<forall>x\<in>set xs. f a \<le> f x \<Longrightarrow> insort_key f a xs = a # xs"

  3735 by (cases xs) auto

  3736

  3737 lemma sorted_remove1: "sorted xs \<Longrightarrow> sorted (remove1 a xs)"

  3738 by(induct xs)(auto simp add: sorted_Cons)

  3739

  3740 lemma insort_key_remove1: "\<lbrakk> a \<in> set xs; sorted (map f xs) ; inj_on f (set xs) \<rbrakk>

  3741   \<Longrightarrow> insort_key f a (remove1 a xs) = xs"

  3742 proof (induct xs)

  3743   case (Cons x xs)

  3744   thus ?case

  3745   proof (cases "x = a")

  3746     case False

  3747     hence "f x \<noteq> f a" using Cons.prems by auto

  3748     hence "f x < f a" using Cons.prems by (auto simp: sorted_Cons)

  3749     thus ?thesis using Cons by (auto simp: sorted_Cons insort_is_Cons)

  3750   qed (auto simp: sorted_Cons insort_is_Cons)

  3751 qed simp

  3752

  3753 lemma insort_remove1: "\<lbrakk> a \<in> set xs; sorted xs \<rbrakk> \<Longrightarrow> insort a (remove1 a xs) = xs"

  3754 using insort_key_remove1[where f="\<lambda>x. x"] by simp

  3755

  3756 lemma sorted_remdups[simp]:

  3757   "sorted l \<Longrightarrow> sorted (remdups l)"

  3758 by (induct l) (auto simp: sorted_Cons)

  3759

  3760 lemma sorted_distinct_set_unique:

  3761 assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" "set xs = set ys"

  3762 shows "xs = ys"

  3763 proof -

  3764   from assms have 1: "length xs = length ys" by (auto dest!: distinct_card)

  3765   from assms show ?thesis

  3766   proof(induct rule:list_induct2[OF 1])

  3767     case 1 show ?case by simp

  3768   next

  3769     case 2 thus ?case by (simp add:sorted_Cons)

  3770        (metis Diff_insert_absorb antisym insertE insert_iff)

  3771   qed

  3772 qed

  3773

  3774 lemma map_sorted_distinct_set_unique:

  3775   assumes "inj_on f (set xs \<union> set ys)"

  3776   assumes "sorted (map f xs)" "distinct (map f xs)"

  3777     "sorted (map f ys)" "distinct (map f ys)"

  3778   assumes "set xs = set ys"

  3779   shows "xs = ys"

  3780 proof -

  3781   from assms have "map f xs = map f ys"

  3782     by (simp add: sorted_distinct_set_unique)

  3783   moreover with inj_on f (set xs \<union> set ys) show "xs = ys"

  3784     by (blast intro: map_inj_on)

  3785 qed

  3786

  3787 lemma finite_sorted_distinct_unique:

  3788 shows "finite A \<Longrightarrow> EX! xs. set xs = A & sorted xs & distinct xs"

  3789 apply(drule finite_distinct_list)

  3790 apply clarify

  3791 apply(rule_tac a="sort xs" in ex1I)

  3792 apply (auto simp: sorted_distinct_set_unique)

  3793 done

  3794

  3795 lemma sorted_take:

  3796   "sorted xs \<Longrightarrow> sorted (take n xs)"

  3797 proof (induct xs arbitrary: n rule: sorted.induct)

  3798   case 1 show ?case by simp

  3799 next

  3800   case 2 show ?case by (cases n) simp_all

  3801 next

  3802   case (3 x y xs)

  3803   then have "x \<le> y" by simp

  3804   show ?case proof (cases n)

  3805     case 0 then show ?thesis by simp

  3806   next

  3807     case (Suc m)

  3808     with 3 have "sorted (take m (y # xs))" by simp

  3809     with Suc  x \<le> y show ?thesis by (cases m) simp_all

  3810   qed

  3811 qed

  3812

  3813 lemma sorted_drop:

  3814   "sorted xs \<Longrightarrow> sorted (drop n xs)"

  3815 proof (induct xs arbitrary: n rule: sorted.induct)

  3816   case 1 show ?case by simp

  3817 next

  3818   case 2 show ?case by (cases n) simp_all

  3819 next

  3820   case 3 then show ?case by (cases n) simp_all

  3821 qed

  3822

  3823 lemma sorted_dropWhile: "sorted xs \<Longrightarrow> sorted (dropWhile P xs)"

  3824   unfolding dropWhile_eq_drop by (rule sorted_drop)

  3825

  3826 lemma sorted_takeWhile: "sorted xs \<Longrightarrow> sorted (takeWhile P xs)"

  3827   apply (subst takeWhile_eq_take) by (rule sorted_take)

  3828

  3829 lemma sorted_filter:

  3830   "sorted (map f xs) \<Longrightarrow> sorted (map f (filter P xs))"

  3831   by (induct xs) (simp_all add: sorted_Cons)

  3832

  3833 lemma foldr_max_sorted:

  3834   assumes "sorted (rev xs)"

  3835   shows "foldr max xs y = (if xs = [] then y else max (xs ! 0) y)"

  3836 using assms proof (induct xs)

  3837   case (Cons x xs)

  3838   moreover hence "sorted (rev xs)" using sorted_append by auto

  3839   ultimately show ?case

  3840     by (cases xs, auto simp add: sorted_append max_def)

  3841 qed simp

  3842

  3843 lemma filter_equals_takeWhile_sorted_rev:

  3844   assumes sorted: "sorted (rev (map f xs))"

  3845   shows "[x \<leftarrow> xs. t < f x] = takeWhile (\<lambda> x. t < f x) xs"

  3846     (is "filter ?P xs = ?tW")

  3847 proof (rule takeWhile_eq_filter[symmetric])

  3848   let "?dW" = "dropWhile ?P xs"

  3849   fix x assume "x \<in> set ?dW"

  3850   then obtain i where i: "i < length ?dW" and nth_i: "x = ?dW ! i"

  3851     unfolding in_set_conv_nth by auto

  3852   hence "length ?tW + i < length (?tW @ ?dW)"

  3853     unfolding length_append by simp

  3854   hence i': "length (map f ?tW) + i < length (map f xs)" by simp

  3855   have "(map f ?tW @ map f ?dW) ! (length (map f ?tW) + i) \<le>

  3856         (map f ?tW @ map f ?dW) ! (length (map f ?tW) + 0)"

  3857     using sorted_rev_nth_mono[OF sorted _ i', of "length ?tW"]

  3858     unfolding map_append[symmetric] by simp

  3859   hence "f x \<le> f (?dW ! 0)"

  3860     unfolding nth_append_length_plus nth_i

  3861     using i preorder_class.le_less_trans[OF le0 i] by simp

  3862   also have "... \<le> t"

  3863     using hd_dropWhile[of "?P" xs] le0[THEN preorder_class.le_less_trans, OF i]

  3864     using hd_conv_nth[of "?dW"] by simp

  3865   finally show "\<not> t < f x" by simp

  3866 qed

  3867

  3868 lemma set_insort_insert:

  3869   "set (insort_insert x xs) = insert x (set xs)"

  3870   by (auto simp add: insort_insert_def set_insort)

  3871

  3872 lemma distinct_insort_insert:

  3873   assumes "distinct xs"

  3874   shows "distinct (insort_insert x xs)"

  3875   using assms by (induct xs) (auto simp add: insort_insert_def set_insort)

  3876

  3877 lemma sorted_insort_insert:

  3878   assumes "sorted xs"

  3879   shows "sorted (insort_insert x xs)"

  3880   using assms by (simp add: insort_insert_def sorted_insort)

  3881

  3882 lemma filter_insort_key_triv:

  3883   "\<not> P x \<Longrightarrow> filter P (insort_key f x xs) = filter P xs"

  3884   by (induct xs) simp_all

  3885

  3886 lemma filter_insort_key:

  3887   "sorted (map f xs) \<Longrightarrow> P x \<Longrightarrow> filter P (insort_key f x xs) = insort_key f x (filter P xs)"

  3888   using assms by (induct xs)

  3889     (auto simp add: sorted_Cons, subst insort_is_Cons, auto)

  3890

  3891 lemma filter_sort_key:

  3892   "filter P (sort_key f xs) = sort_key f (filter P xs)"

  3893   by (induct xs) (simp_all add: filter_insort_key_triv filter_insort_key)

  3894

  3895 lemma sorted_same [simp]:

  3896   "sorted [x\<leftarrow>xs. x = f xs]"

  3897 proof (induct xs arbitrary: f)

  3898   case Nil then show ?case by simp

  3899 next

  3900   case (Cons x xs)

  3901   then have "sorted [y\<leftarrow>xs . y = (\<lambda>xs. x) xs]" .

  3902   moreover from Cons have "sorted [y\<leftarrow>xs . y = (f \<circ> Cons x) xs]" .

  3903   ultimately show ?case by (simp_all add: sorted_Cons)

  3904 qed

  3905

  3906 lemma remove1_insort [simp]:

  3907   "remove1 x (insort x xs) = xs"

  3908   by (induct xs) simp_all

  3909

  3910 end

  3911

  3912 lemma sorted_upt[simp]: "sorted[i..<j]"

  3913 by (induct j) (simp_all add:sorted_append)

  3914

  3915 lemma sorted_upto[simp]: "sorted[i..j]"

  3916 apply(induct i j rule:upto.induct)

  3917 apply(subst upto.simps)

  3918 apply(simp add:sorted_Cons)

  3919 done

  3920

  3921

  3922 subsubsection {* @{const transpose} on sorted lists *}

  3923

  3924 lemma sorted_transpose[simp]:

  3925   shows "sorted (rev (map length (transpose xs)))"

  3926   by (auto simp: sorted_equals_nth_mono rev_nth nth_transpose

  3927     length_filter_conv_card intro: card_mono)

  3928

  3929 lemma transpose_max_length:

  3930   "foldr (\<lambda>xs. max (length xs)) (transpose xs) 0 = length [x \<leftarrow> xs. x \<noteq> []]"

  3931   (is "?L = ?R")

  3932 proof (cases "transpose xs = []")

  3933   case False

  3934   have "?L = foldr max (map length (transpose xs)) 0"

  3935     by (simp add: foldr_map comp_def)

  3936   also have "... = length (transpose xs ! 0)"

  3937     using False sorted_transpose by (simp add: foldr_max_sorted)

  3938   finally show ?thesis

  3939     using False by (simp add: nth_transpose)

  3940 next

  3941   case True

  3942   hence "[x \<leftarrow> xs. x \<noteq> []] = []"

  3943     by (auto intro!: filter_False simp: transpose_empty)

  3944   thus ?thesis by (simp add: transpose_empty True)

  3945 qed

  3946

  3947 lemma length_transpose_sorted:

  3948   fixes xs :: "'a list list"

  3949   assumes sorted: "sorted (rev (map length xs))"

  3950   shows "length (transpose xs) = (if xs = [] then 0 else length (xs ! 0))"

  3951 proof (cases "xs = []")

  3952   case False

  3953   thus ?thesis

  3954     using foldr_max_sorted[OF sorted] False

  3955     unfolding length_transpose foldr_map comp_def

  3956     by simp

  3957 qed simp

  3958

  3959 lemma nth_nth_transpose_sorted[simp]:

  3960   fixes xs :: "'a list list"

  3961   assumes sorted: "sorted (rev (map length xs))"

  3962   and i: "i < length (transpose xs)"

  3963   and j: "j < length [ys \<leftarrow> xs. i < length ys]"

  3964   shows "transpose xs ! i ! j = xs ! j  ! i"

  3965   using j filter_equals_takeWhile_sorted_rev[OF sorted, of i]

  3966     nth_transpose[OF i] nth_map[OF j]

  3967   by (simp add: takeWhile_nth)

  3968

  3969 lemma transpose_column_length:

  3970   fixes xs :: "'a list list"

  3971   assumes sorted: "sorted (rev (map length xs))" and "i < length xs"

  3972   shows "length (filter (\<lambda>ys. i < length ys) (transpose xs)) = length (xs ! i)"

  3973 proof -

  3974   have "xs \<noteq> []" using i < length xs by auto

  3975   note filter_equals_takeWhile_sorted_rev[OF sorted, simp]

  3976   { fix j assume "j \<le> i"

  3977     note sorted_rev_nth_mono[OF sorted, of j i, simplified, OF this i < length xs]

  3978   } note sortedE = this[consumes 1]

  3979

  3980   have "{j. j < length (transpose xs) \<and> i < length (transpose xs ! j)}

  3981     = {..< length (xs ! i)}"

  3982   proof safe

  3983     fix j

  3984     assume "j < length (transpose xs)" and "i < length (transpose xs ! j)"

  3985     with this(2) nth_transpose[OF this(1)]

  3986     have "i < length (takeWhile (\<lambda>ys. j < length ys) xs)" by simp

  3987     from nth_mem[OF this] takeWhile_nth[OF this]

  3988     show "j < length (xs ! i)" by (auto dest: set_takeWhileD)

  3989   next

  3990     fix j assume "j < length (xs ! i)"

  3991     thus "j < length (transpose xs)"

  3992       using foldr_max_sorted[OF sorted] xs \<noteq> [] sortedE[OF le0]

  3993       by (auto simp: length_transpose comp_def foldr_map)

  3994

  3995     have "Suc i \<le> length (takeWhile (\<lambda>ys. j < length ys) xs)"

  3996       using i < length xs j < length (xs ! i) less_Suc_eq_le

  3997       by (auto intro!: length_takeWhile_less_P_nth dest!: sortedE)

  3998     with nth_transpose[OF j < length (transpose xs)]

  3999     show "i < length (transpose xs ! j)" by simp

  4000   qed

  4001   thus ?thesis by (simp add: length_filter_conv_card)

  4002 qed

  4003

  4004 lemma transpose_column:

  4005   fixes xs :: "'a list list"

  4006   assumes sorted: "sorted (rev (map length xs))" and "i < length xs"

  4007   shows "map (\<lambda>ys. ys ! i) (filter (\<lambda>ys. i < length ys) (transpose xs))

  4008     = xs ! i" (is "?R = _")

  4009 proof (rule nth_equalityI, safe)

  4010   show length: "length ?R = length (xs ! i)"

  4011     using transpose_column_length[OF assms] by simp

  4012

  4013   fix j assume j: "j < length ?R"

  4014   note * = less_le_trans[OF this, unfolded length_map, OF length_filter_le]

  4015   from j have j_less: "j < length (xs ! i)" using length by simp

  4016   have i_less_tW: "Suc i \<le> length (takeWhile (\<lambda>ys. Suc j \<le> length ys) xs)"

  4017   proof (rule length_takeWhile_less_P_nth)

  4018     show "Suc i \<le> length xs" using i < length xs by simp

  4019     fix k assume "k < Suc i"

  4020     hence "k \<le> i" by auto

  4021     with sorted_rev_nth_mono[OF sorted this] i < length xs

  4022     have "length (xs ! i) \<le> length (xs ! k)" by simp

  4023     thus "Suc j \<le> length (xs ! k)" using j_less by simp

  4024   qed

  4025   have i_less_filter: "i < length [ys\<leftarrow>xs . j < length ys]"

  4026     unfolding filter_equals_takeWhile_sorted_rev[OF sorted, of j]

  4027     using i_less_tW by (simp_all add: Suc_le_eq)

  4028   from j show "?R ! j = xs ! i ! j"

  4029     unfolding filter_equals_takeWhile_sorted_rev[OF sorted_transpose, of i]

  4030     by (simp add: takeWhile_nth nth_nth_transpose_sorted[OF sorted * i_less_filter])

  4031 qed

  4032

  4033 lemma transpose_transpose:

  4034   fixes xs :: "'a list list"

  4035   assumes sorted: "sorted (rev (map length xs))"

  4036   shows "transpose (transpose xs) = takeWhile (\<lambda>x. x \<noteq> []) xs" (is "?L = ?R")

  4037 proof -

  4038   have len: "length ?L = length ?R"

  4039     unfolding length_transpose transpose_max_length

  4040     using filter_equals_takeWhile_sorted_rev[OF sorted, of 0]

  4041     by simp

  4042

  4043   { fix i assume "i < length ?R"

  4044     with less_le_trans[OF _ length_takeWhile_le[of _ xs]]

  4045     have "i < length xs" by simp

  4046   } note * = this

  4047   show ?thesis

  4048     by (rule nth_equalityI)

  4049        (simp_all add: len nth_transpose transpose_column[OF sorted] * takeWhile_nth)

  4050 qed

  4051

  4052 theorem transpose_rectangle:

  4053   assumes "xs = [] \<Longrightarrow> n = 0"

  4054   assumes rect: "\<And> i. i < length xs \<Longrightarrow> length (xs ! i) = n"

  4055   shows "transpose xs = map (\<lambda> i. map (\<lambda> j. xs ! j ! i) [0..<length xs]) [0..<n]"

  4056     (is "?trans = ?map")

  4057 proof (rule nth_equalityI)

  4058   have "sorted (rev (map length xs))"

  4059     by (auto simp: rev_nth rect intro!: sorted_nth_monoI)

  4060   from foldr_max_sorted[OF this] assms

  4061   show len: "length ?trans = length ?map"

  4062     by (simp_all add: length_transpose foldr_map comp_def)

  4063   moreover

  4064   { fix i assume "i < n" hence "[ys\<leftarrow>xs . i < length ys] = xs"

  4065       using rect by (auto simp: in_set_conv_nth intro!: filter_True) }

  4066   ultimately show "\<forall>i < length ?trans. ?trans ! i = ?map ! i"

  4067     by (auto simp: nth_transpose intro: nth_equalityI)

  4068 qed

  4069

  4070

  4071 subsubsection {* @{text sorted_list_of_set} *}

  4072

  4073 text{* This function maps (finite) linearly ordered sets to sorted

  4074 lists. Warning: in most cases it is not a good idea to convert from

  4075 sets to lists but one should convert in the other direction (via

  4076 @{const set}). *}

  4077

  4078 context linorder

  4079 begin

  4080

  4081 definition sorted_list_of_set :: "'a set \<Rightarrow> 'a list" where

  4082   "sorted_list_of_set = Finite_Set.fold insort []"

  4083

  4084 lemma sorted_list_of_set_empty [simp]:

  4085   "sorted_list_of_set {} = []"

  4086   by (simp add: sorted_list_of_set_def)

  4087

  4088 lemma sorted_list_of_set_insert [simp]:

  4089   assumes "finite A"

  4090   shows "sorted_list_of_set (insert x A) = insort x (sorted_list_of_set (A - {x}))"

  4091 proof -

  4092   interpret fun_left_comm insort by (fact fun_left_comm_insort)

  4093   with assms show ?thesis by (simp add: sorted_list_of_set_def fold_insert_remove)

  4094 qed

  4095

  4096 lemma sorted_list_of_set [simp]:

  4097   "finite A \<Longrightarrow> set (sorted_list_of_set A) = A \<and> sorted (sorted_list_of_set A)

  4098     \<and> distinct (sorted_list_of_set A)"

  4099   by (induct A rule: finite_induct) (simp_all add: set_insort sorted_insort distinct_insort)

  4100

  4101 lemma sorted_list_of_set_sort_remdups:

  4102   "sorted_list_of_set (set xs) = sort (remdups xs)"

  4103 proof -

  4104   interpret fun_left_comm insort by (fact fun_left_comm_insort)

  4105   show ?thesis by (simp add: sort_foldl_insort sorted_list_of_set_def fold_set_remdups)

  4106 qed

  4107

  4108 lemma sorted_list_of_set_remove:

  4109   assumes "finite A"

  4110   shows "sorted_list_of_set (A - {x}) = remove1 x (sorted_list_of_set A)"

  4111 proof (cases "x \<in> A")

  4112   case False with assms have "x \<notin> set (sorted_list_of_set A)" by simp

  4113   with False show ?thesis by (simp add: remove1_idem)

  4114 next

  4115   case True then obtain B where A: "A = insert x B" by (rule Set.set_insert)

  4116   with assms show ?thesis by simp

  4117 qed

  4118

  4119 end

  4120

  4121 lemma sorted_list_of_set_range [simp]:

  4122   "sorted_list_of_set {m..<n} = [m..<n]"

  4123   by (rule sorted_distinct_set_unique) simp_all

  4124

  4125

  4126

  4127 subsubsection {* @{text lists}: the list-forming operator over sets *}

  4128

  4129 inductive_set

  4130   lists :: "'a set => 'a list set"

  4131   for A :: "'a set"

  4132 where

  4133     Nil [intro!]: "[]: lists A"

  4134   | Cons [intro!,no_atp]: "[| a: A; l: lists A|] ==> a#l : lists A"

  4135

  4136 inductive_cases listsE [elim!,no_atp]: "x#l : lists A"

  4137 inductive_cases listspE [elim!,no_atp]: "listsp A (x # l)"

  4138

  4139 lemma listsp_mono [mono]: "A \<le> B ==> listsp A \<le> listsp B"

  4140 by (rule predicate1I, erule listsp.induct, (blast dest: predicate1D)+)

  4141

  4142 lemmas lists_mono = listsp_mono [to_set pred_subset_eq]

  4143

  4144 lemma listsp_infI:

  4145   assumes l: "listsp A l" shows "listsp B l ==> listsp (inf A B) l" using l

  4146 by induct blast+

  4147

  4148 lemmas lists_IntI = listsp_infI [to_set]

  4149

  4150 lemma listsp_inf_eq [simp]: "listsp (inf A B) = inf (listsp A) (listsp B)"

  4151 proof (rule mono_inf [where f=listsp, THEN order_antisym])

  4152   show "mono listsp" by (simp add: mono_def listsp_mono)

  4153   show "inf (listsp A) (listsp B) \<le> listsp (inf A B)" by (blast intro!: listsp_infI predicate1I)

  4154 qed

  4155

  4156 lemmas listsp_conj_eq [simp] = listsp_inf_eq [simplified inf_fun_eq inf_bool_eq]

  4157

  4158 lemmas lists_Int_eq [simp] = listsp_inf_eq [to_set pred_equals_eq]

  4159

  4160 lemma append_in_listsp_conv [iff]:

  4161      "(listsp A (xs @ ys)) = (listsp A xs \<and> listsp A ys)"

  4162 by (induct xs) auto

  4163

  4164 lemmas append_in_lists_conv [iff] = append_in_listsp_conv [to_set]

  4165

  4166 lemma in_listsp_conv_set: "(listsp A xs) = (\<forall>x \<in> set xs. A x)"

  4167 -- {* eliminate @{text listsp} in favour of @{text set} *}

  4168 by (induct xs) auto

  4169

  4170 lemmas in_lists_conv_set = in_listsp_conv_set [to_set]

  4171

  4172 lemma in_listspD [dest!,no_atp]: "listsp A xs ==> \<forall>x\<in>set xs. A x"

  4173 by (rule in_listsp_conv_set [THEN iffD1])

  4174

  4175 lemmas in_listsD [dest!,no_atp] = in_listspD [to_set]

  4176

  4177 lemma in_listspI [intro!,no_atp]: "\<forall>x\<in>set xs. A x ==> listsp A xs"

  4178 by (rule in_listsp_conv_set [THEN iffD2])

  4179

  4180 lemmas in_listsI [intro!,no_atp] = in_listspI [to_set]

  4181

  4182 lemma lists_UNIV [simp]: "lists UNIV = UNIV"

  4183 by auto

  4184

  4185

  4186 subsubsection {* Inductive definition for membership *}

  4187

  4188 inductive ListMem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"

  4189 where

  4190     elem:  "ListMem x (x # xs)"

  4191   | insert:  "ListMem x xs \<Longrightarrow> ListMem x (y # xs)"

  4192

  4193 lemma ListMem_iff: "(ListMem x xs) = (x \<in> set xs)"

  4194 apply (rule iffI)

  4195  apply (induct set: ListMem)

  4196   apply auto

  4197 apply (induct xs)

  4198  apply (auto intro: ListMem.intros)

  4199 done

  4200

  4201

  4202 subsubsection {* Lists as Cartesian products *}

  4203

  4204 text{*@{text"set_Cons A Xs"}: the set of lists with head drawn from

  4205 @{term A} and tail drawn from @{term Xs}.*}

  4206

  4207 definition

  4208   set_Cons :: "'a set \<Rightarrow> 'a list set \<Rightarrow> 'a list set" where

  4209   "set_Cons A XS = {z. \<exists>x xs. z = x # xs \<and> x \<in> A \<and> xs \<in> XS}"

  4210

  4211 lemma set_Cons_sing_Nil [simp]: "set_Cons A {[]} = (%x. [x])A"

  4212 by (auto simp add: set_Cons_def)

  4213

  4214 text{*Yields the set of lists, all of the same length as the argument and

  4215 with elements drawn from the corresponding element of the argument.*}

  4216

  4217 primrec

  4218   listset :: "'a set list \<Rightarrow> 'a list set" where

  4219      "listset [] = {[]}"

  4220   |  "listset (A # As) = set_Cons A (listset As)"

  4221

  4222

  4223 subsection {* Relations on Lists *}

  4224

  4225 subsubsection {* Length Lexicographic Ordering *}

  4226

  4227 text{*These orderings preserve well-foundedness: shorter lists

  4228   precede longer lists. These ordering are not used in dictionaries.*}

  4229

  4230 primrec -- {*The lexicographic ordering for lists of the specified length*}

  4231   lexn :: "('a \<times> 'a) set \<Rightarrow> nat \<Rightarrow> ('a list \<times> 'a list) set" where

  4232     "lexn r 0 = {}"

  4233   | "lexn r (Suc n) = (prod_fun (%(x, xs). x#xs) (%(x, xs). x#xs)  (r <*lex*> lexn r n)) Int

  4234       {(xs, ys). length xs = Suc n \<and> length ys = Suc n}"

  4235

  4236 definition

  4237   lex :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where

  4238   "lex r = (\<Union>n. lexn r n)" -- {*Holds only between lists of the same length*}

  4239

  4240 definition

  4241   lenlex :: "('a \<times> 'a) set => ('a list \<times> 'a list) set" where

  4242   "lenlex r = inv_image (less_than <*lex*> lex r) (\<lambda>xs. (length xs, xs))"

  4243         -- {*Compares lists by their length and then lexicographically*}

  4244

  4245 lemma wf_lexn: "wf r ==> wf (lexn r n)"

  4246 apply (induct n, simp, simp)

  4247 apply(rule wf_subset)

  4248  prefer 2 apply (rule Int_lower1)

  4249 apply(rule wf_prod_fun_image)

  4250  prefer 2 apply (rule inj_onI, auto)

  4251 done

  4252

  4253 lemma lexn_length:

  4254   "(xs, ys) : lexn r n ==> length xs = n \<and> length ys = n"

  4255 by (induct n arbitrary: xs ys) auto

  4256

  4257 lemma wf_lex [intro!]: "wf r ==> wf (lex r)"

  4258 apply (unfold lex_def)

  4259 apply (rule wf_UN)

  4260 apply (blast intro: wf_lexn, clarify)

  4261 apply (rename_tac m n)

  4262 apply (subgoal_tac "m \<noteq> n")

  4263  prefer 2 apply blast

  4264 apply (blast dest: lexn_length not_sym)

  4265 done

  4266

  4267 lemma lexn_conv:

  4268   "lexn r n =

  4269     {(xs,ys). length xs = n \<and> length ys = n \<and>

  4270     (\<exists>xys x y xs' ys'. xs= xys @ x#xs' \<and> ys= xys @ y # ys' \<and> (x, y):r)}"

  4271 apply (induct n, simp)

  4272 apply (simp add: image_Collect lex_prod_def, safe, blast)

  4273  apply (rule_tac x = "ab # xys" in exI, simp)

  4274 apply (case_tac xys, simp_all, blast)

  4275 done

  4276

  4277 lemma lex_conv:

  4278   "lex r =

  4279     {(xs,ys). length xs = length ys \<and>

  4280     (\<exists>xys x y xs' ys'. xs = xys @ x # xs' \<and> ys = xys @ y # ys' \<and> (x, y):r)}"

  4281 by (force simp add: lex_def lexn_conv)

  4282

  4283 lemma wf_lenlex [intro!]: "wf r ==> wf (lenlex r)"

  4284 by (unfold lenlex_def) blast

  4285

  4286 lemma lenlex_conv:

  4287     "lenlex r = {(xs,ys). length xs < length ys |

  4288                  length xs = length ys \<and> (xs, ys) : lex r}"

  4289 by (simp add: lenlex_def Id_on_def lex_prod_def inv_image_def)

  4290

  4291 lemma Nil_notin_lex [iff]: "([], ys) \<notin> lex r"

  4292 by (simp add: lex_conv)

  4293

  4294 lemma Nil2_notin_lex [iff]: "(xs, []) \<notin> lex r"

  4295 by (simp add:lex_conv)

  4296

  4297 lemma Cons_in_lex [simp]:

  4298     "((x # xs, y # ys) : lex r) =

  4299       ((x, y) : r \<and> length xs = length ys | x = y \<and> (xs, ys) : lex r)"

  4300 apply (simp add: lex_conv)

  4301 apply (rule iffI)

  4302  prefer 2 apply (blast intro: Cons_eq_appendI, clarify)

  4303 apply (case_tac xys, simp, simp)

  4304 apply blast

  4305 done

  4306

  4307

  4308 subsubsection {* Lexicographic Ordering *}

  4309

  4310 text {* Classical lexicographic ordering on lists, ie. "a" < "ab" < "b".

  4311     This ordering does \emph{not} preserve well-foundedness.

  4312      Author: N. Voelker, March 2005. *}

  4313

  4314 definition

  4315   lexord :: "('a \<times> 'a) set \<Rightarrow> ('a list \<times> 'a list) set" where

  4316   "lexord r = {(x,y ). \<exists> a v. y = x @ a # v \<or>

  4317             (\<exists> u a b v w. (a,b) \<in> r \<and> x = u @ (a # v) \<and> y = u @ (b # w))}"

  4318

  4319 lemma lexord_Nil_left[simp]:  "([],y) \<in> lexord r = (\<exists> a x. y = a # x)"

  4320 by (unfold lexord_def, induct_tac y, auto)

  4321

  4322 lemma lexord_Nil_right[simp]: "(x,[]) \<notin> lexord r"

  4323 by (unfold lexord_def, induct_tac x, auto)

  4324

  4325 lemma lexord_cons_cons[simp]:

  4326      "((a # x, b # y) \<in> lexord r) = ((a,b)\<in> r | (a = b & (x,y)\<in> lexord r))"

  4327   apply (unfold lexord_def, safe, simp_all)

  4328   apply (case_tac u, simp, simp)

  4329   apply (case_tac u, simp, clarsimp, blast, blast, clarsimp)

  4330   apply (erule_tac x="b # u" in allE)

  4331   by force

  4332

  4333 lemmas lexord_simps = lexord_Nil_left lexord_Nil_right lexord_cons_cons

  4334

  4335 lemma lexord_append_rightI: "\<exists> b z. y = b # z \<Longrightarrow> (x, x @ y) \<in> lexord r"

  4336 by (induct_tac x, auto)

  4337

  4338 lemma lexord_append_left_rightI:

  4339      "(a,b) \<in> r \<Longrightarrow> (u @ a # x, u @ b # y) \<in> lexord r"

  4340 by (induct_tac u, auto)

  4341

  4342 lemma lexord_append_leftI: " (u,v) \<in> lexord r \<Longrightarrow> (x @ u, x @ v) \<in> lexord r"

  4343 by (induct x, auto)

  4344

  4345 lemma lexord_append_leftD:

  4346      "\<lbrakk> (x @ u, x @ v) \<in> lexord r; (! a. (a,a) \<notin> r) \<rbrakk> \<Longrightarrow> (u,v) \<in> lexord r"

  4347 by (erule rev_mp, induct_tac x, auto)

  4348

  4349 lemma lexord_take_index_conv:

  4350    "((x,y) : lexord r) =

  4351     ((length x < length y \<and> take (length x) y = x) \<or>

  4352      (\<exists>i. i < min(length x)(length y) & take i x = take i y & (x!i,y!i) \<in> r))"

  4353   apply (unfold lexord_def Let_def, clarsimp)

  4354   apply (rule_tac f = "(% a b. a \<or> b)" in arg_cong2)

  4355   apply auto

  4356   apply (rule_tac x="hd (drop (length x) y)" in exI)

  4357   apply (rule_tac x="tl (drop (length x) y)" in exI)

  4358   apply (erule subst, simp add: min_def)

  4359   apply (rule_tac x ="length u" in exI, simp)

  4360   apply (rule_tac x ="take i x" in exI)

  4361   apply (rule_tac x ="x ! i" in exI)

  4362   apply (rule_tac x ="y ! i" in exI, safe)

  4363   apply (rule_tac x="drop (Suc i) x" in exI)

  4364   apply (drule sym, simp add: drop_Suc_conv_tl)

  4365   apply (rule_tac x="drop (Suc i) y" in exI)

  4366   by (simp add: drop_Suc_conv_tl)

  4367

  4368 -- {* lexord is extension of partial ordering List.lex *}

  4369 lemma lexord_lex: " (x,y) \<in> lex r = ((x,y) \<in> lexord r \<and> length x = length y)"

  4370   apply (rule_tac x = y in spec)

  4371   apply (induct_tac x, clarsimp)

  4372   by (clarify, case_tac x, simp, force)

  4373

  4374 lemma lexord_irreflexive: "(! x. (x,x) \<notin> r) \<Longrightarrow> (y,y) \<notin> lexord r"

  4375   by (induct y, auto)

  4376

  4377 lemma lexord_trans:

  4378     "\<lbrakk> (x, y) \<in> lexord r; (y, z) \<in> lexord r; trans r \<rbrakk> \<Longrightarrow> (x, z) \<in> lexord r"

  4379    apply (erule rev_mp)+

  4380    apply (rule_tac x = x in spec)

  4381   apply (rule_tac x = z in spec)

  4382   apply ( induct_tac y, simp, clarify)

  4383   apply (case_tac xa, erule ssubst)

  4384   apply (erule allE, erule allE) -- {* avoid simp recursion *}

  4385   apply (case_tac x, simp, simp)

  4386   apply (case_tac x, erule allE, erule allE, simp)

  4387   apply (erule_tac x = listb in allE)

  4388   apply (erule_tac x = lista in allE, simp)

  4389   apply (unfold trans_def)

  4390   by blast

  4391

  4392 lemma lexord_transI:  "trans r \<Longrightarrow> trans (lexord r)"

  4393 by (rule transI, drule lexord_trans, blast)

  4394

  4395 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"

  4396   apply (rule_tac x = y in spec)

  4397   apply (induct_tac x, rule allI)

  4398   apply (case_tac x, simp, simp)

  4399   apply (rule allI, case_tac x, simp, simp)

  4400   by blast

  4401

  4402

  4403 subsection {* Lexicographic combination of measure functions *}

  4404

  4405 text {* These are useful for termination proofs *}

  4406

  4407 definition

  4408   "measures fs = inv_image (lex less_than) (%a. map (%f. f a) fs)"

  4409

  4410 lemma wf_measures[recdef_wf, simp]: "wf (measures fs)"

  4411 unfolding measures_def

  4412 by blast

  4413

  4414 lemma in_measures[simp]:

  4415   "(x, y) \<in> measures [] = False"

  4416   "(x, y) \<in> measures (f # fs)

  4417          = (f x < f y \<or> (f x = f y \<and> (x, y) \<in> measures fs))"

  4418 unfolding measures_def

  4419 by auto

  4420

  4421 lemma measures_less: "f x < f y ==> (x, y) \<in> measures (f#fs)"

  4422 by simp

  4423

  4424 lemma measures_lesseq: "f x <= f y ==> (x, y) \<in> measures fs ==> (x, y) \<in> measures (f#fs)"

  4425 by auto

  4426

  4427

  4428 subsubsection {* Lifting a Relation on List Elements to the Lists *}

  4429

  4430 inductive_set

  4431   listrel :: "('a * 'a)set => ('a list * 'a list)set"

  4432   for r :: "('a * 'a)set"

  4433 where

  4434     Nil:  "([],[]) \<in> listrel r"

  4435   | Cons: "[| (x,y) \<in> r; (xs,ys) \<in> listrel r |] ==> (x#xs, y#ys) \<in> listrel r"

  4436

  4437 inductive_cases listrel_Nil1 [elim!]: "([],xs) \<in> listrel r"

  4438 inductive_cases listrel_Nil2 [elim!]: "(xs,[]) \<in> listrel r"

  4439 inductive_cases listrel_Cons1 [elim!]: "(y#ys,xs) \<in> listrel r"

  4440 inductive_cases listrel_Cons2 [elim!]: "(xs,y#ys) \<in> listrel r"

  4441

  4442

  4443 lemma listrel_mono: "r \<subseteq> s \<Longrightarrow> listrel r \<subseteq> listrel s"

  4444 apply clarify

  4445 apply (erule listrel.induct)

  4446 apply (blast intro: listrel.intros)+

  4447 done

  4448

  4449 lemma listrel_subset: "r \<subseteq> A \<times> A \<Longrightarrow> listrel r \<subseteq> lists A \<times> lists A"

  4450 apply clarify

  4451 apply (erule listrel.induct, auto)

  4452 done

  4453

  4454 lemma listrel_refl_on: "refl_on A r \<Longrightarrow> refl_on (lists A) (listrel r)"

  4455 apply (simp add: refl_on_def listrel_subset Ball_def)

  4456 apply (rule allI)

  4457 apply (induct_tac x)

  4458 apply (auto intro: listrel.intros)

  4459 done

  4460

  4461 lemma listrel_sym: "sym r \<Longrightarrow> sym (listrel r)"

  4462 apply (auto simp add: sym_def)

  4463 apply (erule listrel.induct)

  4464 apply (blast intro: listrel.intros)+

  4465 done

  4466

  4467 lemma listrel_trans: "trans r \<Longrightarrow> trans (listrel r)"

  4468 apply (simp add: trans_def)

  4469 apply (intro allI)

  4470 apply (rule impI)

  4471 apply (erule listrel.induct)

  4472 apply (blast intro: listrel.intros)+

  4473 done

  4474

  4475 theorem equiv_listrel: "equiv A r \<Longrightarrow> equiv (lists A) (listrel r)"

  4476 by (simp add: equiv_def listrel_refl_on listrel_sym listrel_trans)

  4477

  4478 lemma listrel_Nil [simp]: "listrel r  {[]} = {[]}"

  4479 by (blast intro: listrel.intros)

  4480

  4481 lemma listrel_Cons:

  4482      "listrel r  {x#xs} = set_Cons (r{x}) (listrel r  {xs})"

  4483 by (auto simp add: set_Cons_def intro: listrel.intros)

  4484

  4485

  4486 subsection {* Size function *}

  4487

  4488 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (list_size f)"

  4489 by (rule is_measure_trivial)

  4490

  4491 lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (option_size f)"

  4492 by (rule is_measure_trivial)

  4493

  4494 lemma list_size_estimation[termination_simp]:

  4495   "x \<in> set xs \<Longrightarrow> y < f x \<Longrightarrow> y < list_size f xs"

  4496 by (induct xs) auto

  4497

  4498 lemma list_size_estimation'[termination_simp]:

  4499   "x \<in> set xs \<Longrightarrow> y \<le> f x \<Longrightarrow> y \<le> list_size f xs"

  4500 by (induct xs) auto

  4501

  4502 lemma list_size_map[simp]: "list_size f (map g xs) = list_size (f o g) xs"

  4503 by (induct xs) auto

  4504

  4505 lemma list_size_pointwise[termination_simp]:

  4506   "(\<And>x. x \<in> set xs \<Longrightarrow> f x < g x) \<Longrightarrow> list_size f xs \<le> list_size g xs"

  4507 by (induct xs) force+

  4508

  4509

  4510 subsection {* Transfer *}

  4511

  4512 definition

  4513   embed_list :: "nat list \<Rightarrow> int list"

  4514 where

  4515   "embed_list l = map int l"

  4516

  4517 definition

  4518   nat_list :: "int list \<Rightarrow> bool"

  4519 where

  4520   "nat_list l = nat_set (set l)"

  4521

  4522 definition

  4523   return_list :: "int list \<Rightarrow> nat list"

  4524 where

  4525   "return_list l = map nat l"

  4526

  4527 lemma transfer_nat_int_list_return_embed: "nat_list l \<longrightarrow>

  4528     embed_list (return_list l) = l"

  4529   unfolding embed_list_def return_list_def nat_list_def nat_set_def

  4530   apply (induct l)

  4531   apply auto

  4532 done

  4533

  4534 lemma transfer_nat_int_list_functions:

  4535   "l @ m = return_list (embed_list l @ embed_list m)"

  4536   "[] = return_list []"

  4537   unfolding return_list_def embed_list_def

  4538   apply auto

  4539   apply (induct l, auto)

  4540   apply (induct m, auto)

  4541 done

  4542

  4543 (*

  4544 lemma transfer_nat_int_fold1: "fold f l x =

  4545     fold (%x. f (nat x)) (embed_list l) x";

  4546 *)

  4547

  4548

  4549 subsection {* Code generation *}

  4550

  4551 subsubsection {* Counterparts for set-related operations *}

  4552

  4553 definition member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool" where

  4554   [code_post]: "member xs x \<longleftrightarrow> x \<in> set xs"

  4555

  4556 text {*

  4557   Only use @{text member} for generating executable code.  Otherwise use

  4558   @{prop "x \<in> set xs"} instead --- it is much easier to reason about.

  4559 *}

  4560

  4561 lemma member_set:

  4562   "member = set"

  4563   by (simp add: expand_fun_eq member_def mem_def)

  4564

  4565 lemma member_rec [code]:

  4566   "member (x # xs) y \<longleftrightarrow> x = y \<or> member xs y"

  4567   "member [] y \<longleftrightarrow> False"

  4568   by (auto simp add: member_def)

  4569

  4570 lemma in_set_member [code_unfold]:

  4571   "x \<in> set xs \<longleftrightarrow> member xs x"

  4572   by (simp add: member_def)

  4573

  4574 declare INFI_def [code_unfold]

  4575 declare SUPR_def [code_unfold]

  4576

  4577 declare set_map [symmetric, code_unfold]

  4578

  4579 definition list_all :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where

  4580   list_all_iff [code_post]: "list_all P xs \<longleftrightarrow> (\<forall>x \<in> set xs. P x)"

  4581

  4582 definition list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where

  4583   list_ex_iff [code_post]: "list_ex P xs \<longleftrightarrow> (\<exists>x \<in> set xs. P x)"

  4584

  4585 text {*

  4586   Usually you should prefer @{text "\<forall>x\<in>set xs"} and @{text "\<exists>x\<in>set xs"}

  4587   over @{const list_all} and @{const list_ex} in specifications.

  4588 *}

  4589

  4590 lemma list_all_simps [simp, code]:

  4591   "list_all P (x # xs) \<longleftrightarrow> P x \<and> list_all P xs"

  4592   "list_all P [] \<longleftrightarrow> True"

  4593   by (simp_all add: list_all_iff)

  4594

  4595 lemma list_ex_simps [simp, code]:

  4596   "list_ex P (x # xs) \<longleftrightarrow> P x \<or> list_ex P xs"

  4597   "list_ex P [] \<longleftrightarrow> False"

  4598   by (simp_all add: list_ex_iff)

  4599

  4600 lemma Ball_set_list_all [code_unfold]:

  4601   "Ball (set xs) P \<longleftrightarrow> list_all P xs"

  4602   by (simp add: list_all_iff)

  4603

  4604 lemma Bex_set_list_ex [code_unfold]:

  4605   "Bex (set xs) P \<longleftrightarrow> list_ex P xs"

  4606   by (simp add: list_ex_iff)

  4607

  4608 lemma list_all_append [simp]:

  4609   "list_all P (xs @ ys) \<longleftrightarrow> list_all P xs \<and> list_all P ys"

  4610   by (auto simp add: list_all_iff)

  4611

  4612 lemma list_ex_append [simp]:

  4613   "list_ex P (xs @ ys) \<longleftrightarrow> list_ex P xs \<or> list_ex P ys"

  4614   by (auto simp add: list_ex_iff)

  4615

  4616 lemma list_all_rev [simp]:

  4617   "list_all P (rev xs) \<longleftrightarrow> list_all P xs"

  4618   by (simp add: list_all_iff)

  4619

  4620 lemma list_ex_rev [simp]:

  4621   "list_ex P (rev xs) \<longleftrightarrow> list_ex P xs"

  4622   by (simp add: list_ex_iff)

  4623

  4624 lemma list_all_length:

  4625   "list_all P xs \<longleftrightarrow> (\<forall>n < length xs. P (xs ! n))"

  4626   by (auto simp add: list_all_iff set_conv_nth)

  4627

  4628 lemma list_ex_length:

  4629   "list_ex P xs \<longleftrightarrow> (\<exists>n < length xs. P (xs ! n))"

  4630   by (auto simp add: list_ex_iff set_conv_nth)

  4631

  4632 lemma list_all_cong [fundef_cong]:

  4633   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_all f xs = list_all g ys"

  4634   by (simp add: list_all_iff)

  4635

  4636 lemma list_any_cong [fundef_cong]:

  4637   "xs = ys \<Longrightarrow> (\<And>x. x \<in> set ys \<Longrightarrow> f x = g x) \<Longrightarrow> list_ex f xs = list_ex g ys"

  4638   by (simp add: list_ex_iff)

  4639

  4640 text {* Bounded quantification and summation over nats. *}

  4641

  4642 lemma atMost_upto [code_unfold]:

  4643   "{..n} = set [0..<Suc n]"

  4644   by auto

  4645

  4646 lemma atLeast_upt [code_unfold]:

  4647   "{..<n} = set [0..<n]"

  4648   by auto

  4649

  4650 lemma greaterThanLessThan_upt [code_unfold]:

  4651   "{n<..<m} = set [Suc n..<m]"

  4652   by auto

  4653

  4654 lemmas atLeastLessThan_upt [code_unfold] = set_upt [symmetric]

  4655

  4656 lemma greaterThanAtMost_upt [code_unfold]:

  4657   "{n<..m} = set [Suc n..<Suc m]"

  4658   by auto

  4659

  4660 lemma atLeastAtMost_upt [code_unfold]:

  4661   "{n..m} = set [n..<Suc m]"

  4662   by auto

  4663

  4664 lemma all_nat_less_eq [code_unfold]:

  4665   "(\<forall>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..<n}. P m)"

  4666   by auto

  4667

  4668 lemma ex_nat_less_eq [code_unfold]:

  4669   "(\<exists>m<n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..<n}. P m)"

  4670   by auto

  4671

  4672 lemma all_nat_less [code_unfold]:

  4673   "(\<forall>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<forall>m \<in> {0..n}. P m)"

  4674   by auto

  4675

  4676 lemma ex_nat_less [code_unfold]:

  4677   "(\<exists>m\<le>n\<Colon>nat. P m) \<longleftrightarrow> (\<exists>m \<in> {0..n}. P m)"

  4678   by auto

  4679

  4680 lemma setsum_set_upt_conv_listsum_nat [code_unfold]:

  4681   "setsum f (set [m..<n]) = listsum (map f [m..<n])"

  4682   by (simp add: interv_listsum_conv_setsum_set_nat)

  4683

  4684 text {* Summation over ints. *}

  4685

  4686 lemma greaterThanLessThan_upto [code_unfold]:

  4687   "{i<..<j::int} = set [i+1..j - 1]"

  4688 by auto

  4689

  4690 lemma atLeastLessThan_upto [code_unfold]:

  4691   "{i..<j::int} = set [i..j - 1]"

  4692 by auto

  4693

  4694 lemma greaterThanAtMost_upto [code_unfold]:

  4695   "{i<..j::int} = set [i+1..j]"

  4696 by auto

  4697

  4698 lemmas atLeastAtMost_upto [code_unfold] = set_upto [symmetric]

  4699

  4700 lemma setsum_set_upto_conv_listsum_int [code_unfold]:

  4701   "setsum f (set [i..j::int]) = listsum (map f [i..j])"

  4702   by (simp add: interv_listsum_conv_setsum_set_int)

  4703

  4704

  4705 subsubsection {* Optimizing by rewriting *}

  4706

  4707 definition null :: "'a list \<Rightarrow> bool" where

  4708   [code_post]: "null xs \<longleftrightarrow> xs = []"

  4709

  4710 text {*

  4711   Efficient emptyness check is implemented by @{const null}.

  4712 *}

  4713

  4714 lemma null_rec [code]:

  4715   "null (x # xs) \<longleftrightarrow> False"

  4716   "null [] \<longleftrightarrow> True"

  4717   by (simp_all add: null_def)

  4718

  4719 lemma eq_Nil_null [code_unfold]:

  4720   "xs = [] \<longleftrightarrow> null xs"

  4721   by (simp add: null_def)

  4722

  4723 lemma equal_Nil_null [code_unfold]:

  4724   "eq_class.eq xs [] \<longleftrightarrow> null xs"

  4725   by (simp add: eq eq_Nil_null)

  4726

  4727 definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where

  4728   [code_post]: "maps f xs = concat (map f xs)"

  4729

  4730 definition map_filter :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list" where

  4731   [code_post]: "map_filter f xs = map (the \<circ> f) (filter (\<lambda>x. f x \<noteq> None) xs)"

  4732

  4733 text {*

  4734   Operations @{const maps} and @{const map_filter} avoid

  4735   intermediate lists on execution -- do not use for proving.

  4736 *}

  4737

  4738 lemma maps_simps [code]:

  4739   "maps f (x # xs) = f x @ maps f xs"

  4740   "maps f [] = []"

  4741   by (simp_all add: maps_def)

  4742

  4743 lemma map_filter_simps [code]:

  4744   "map_filter f (x # xs) = (case f x of None \<Rightarrow> map_filter f xs | Some y \<Rightarrow> y # map_filter f xs)"

  4745   "map_filter f [] = []"

  4746   by (simp_all add: map_filter_def split: option.split)

  4747

  4748 lemma concat_map_maps [code_unfold]:

  4749   "concat (map f xs) = maps f xs"

  4750   by (simp add: maps_def)

  4751

  4752 lemma map_filter_map_filter [code_unfold]:

  4753   "map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"

  4754   by (simp add: map_filter_def)

  4755

  4756 text {* Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}

  4757 and similiarly for @{text"\<exists>"}. *}

  4758

  4759 definition all_interval_nat :: "(nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where

  4760   "all_interval_nat P i j \<longleftrightarrow> (\<forall>n \<in> {i..<j}. P n)"

  4761

  4762 lemma [code]:

  4763   "all_interval_nat P i j \<longleftrightarrow> i \<ge> j \<or> P i \<and> all_interval_nat P (Suc i) j"

  4764 proof -

  4765   have *: "\<And>n. P i \<Longrightarrow> \<forall>n\<in>{Suc i..<j}. P n \<Longrightarrow> i \<le> n \<Longrightarrow> n < j \<Longrightarrow> P n"

  4766   proof -

  4767     fix n

  4768     assume "P i" "\<forall>n\<in>{Suc i..<j}. P n" "i \<le> n" "n < j"

  4769     then show "P n" by (cases "n = i") simp_all

  4770   qed

  4771   show ?thesis by (auto simp add: all_interval_nat_def intro: *)

  4772 qed

  4773

  4774 lemma list_all_iff_all_interval_nat [code_unfold]:

  4775   "list_all P [i..<j] \<longleftrightarrow> all_interval_nat P i j"

  4776   by (simp add: list_all_iff all_interval_nat_def)

  4777

  4778 lemma list_ex_iff_not_all_inverval_nat [code_unfold]:

  4779   "list_ex P [i..<j] \<longleftrightarrow> \<not> (all_interval_nat (Not \<circ> P) i j)"

  4780   by (simp add: list_ex_iff all_interval_nat_def)

  4781

  4782 definition all_interval_int :: "(int \<Rightarrow> bool) \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool" where

  4783   "all_interval_int P i j \<longleftrightarrow> (\<forall>k \<in> {i..j}. P k)"

  4784

  4785 lemma [code]:

  4786   "all_interval_int P i j \<longleftrightarrow> i > j \<or> P i \<and> all_interval_int P (i + 1) j"

  4787 proof -

  4788   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"

  4789   proof -

  4790     fix k

  4791     assume "P i" "\<forall>k\<in>{i+1..j}. P k" "i \<le> k" "k \<le> j"

  4792     then show "P k" by (cases "k = i") simp_all

  4793   qed

  4794   show ?thesis by (auto simp add: all_interval_int_def intro: *)

  4795 qed

  4796

  4797 lemma list_all_iff_all_interval_int [code_unfold]:

  4798   "list_all P [i..j] \<longleftrightarrow> all_interval_int P i j"

  4799   by (simp add: list_all_iff all_interval_int_def)

  4800

  4801 lemma list_ex_iff_not_all_inverval_int [code_unfold]:

  4802   "list_ex P [i..j] \<longleftrightarrow> \<not> (all_interval_int (Not \<circ> P) i j)"

  4803   by (simp add: list_ex_iff all_interval_int_def)

  4804

  4805 hide_const (open) member null maps map_filter all_interval_nat all_interval_int

  4806

  4807

  4808 subsubsection {* Pretty lists *}

  4809

  4810 use "Tools/list_code.ML"

  4811

  4812 code_type list

  4813   (SML "_ list")

  4814   (OCaml "_ list")

  4815   (Haskell "![(_)]")

  4816   (Scala "List[(_)]")

  4817

  4818 code_const Nil

  4819   (SML "[]")

  4820   (OCaml "[]")

  4821   (Haskell "[]")

  4822   (Scala "Nil")

  4823

  4824 code_instance list :: eq

  4825   (Haskell -)

  4826

  4827 code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"

  4828   (Haskell infixl 4 "==")

  4829

  4830 code_reserved SML

  4831   list

  4832

  4833 code_reserved OCaml

  4834   list

  4835

  4836 types_code

  4837   "list" ("_ list")

  4838 attach (term_of) {*

  4839 fun term_of_list f T = HOLogic.mk_list T o map f;

  4840 *}

  4841 attach (test) {*

  4842 fun gen_list' aG aT i j = frequency

  4843   [(i, fn () =>

  4844       let

  4845         val (x, t) = aG j;

  4846         val (xs, ts) = gen_list' aG aT (i-1) j

  4847       in (x :: xs, fn () => HOLogic.cons_const aT $t ()$ ts ()) end),

  4848    (1, fn () => ([], fn () => HOLogic.nil_const aT))] ()

  4849 and gen_list aG aT i = gen_list' aG aT i i;

  4850 *}

  4851

  4852 consts_code Cons ("(_ ::/ _)")

  4853

  4854 setup {*

  4855 let

  4856   fun list_codegen thy defs dep thyname b t gr =

  4857     let

  4858       val ts = HOLogic.dest_list t;

  4859       val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false

  4860         (fastype_of t) gr;

  4861       val (ps, gr'') = fold_map

  4862         (Codegen.invoke_codegen thy defs dep thyname false) ts gr'

  4863     in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;

  4864 in

  4865   fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]

  4866   #> Codegen.add_codegen "list_codegen" list_codegen

  4867 end

  4868 *}

  4869

  4870

  4871 subsubsection {* Use convenient predefined operations *}

  4872

  4873 code_const "op @"

  4874   (SML infixr 7 "@")

  4875   (OCaml infixr 6 "@")

  4876   (Haskell infixr 5 "++")

  4877   (Scala infixl 7 "++")

  4878

  4879 code_const map

  4880   (Haskell "map")

  4881

  4882 code_const filter

  4883   (Haskell "filter")

  4884

  4885 code_const concat

  4886   (Haskell "concat")

  4887

  4888 code_const List.maps

  4889   (Haskell "concatMap")

  4890

  4891 code_const rev

  4892   (Haskell "reverse")

  4893

  4894 code_const zip

  4895   (Haskell "zip")

  4896

  4897 code_const List.null

  4898   (Haskell "null")

  4899

  4900 code_const takeWhile

  4901   (Haskell "takeWhile")

  4902

  4903 code_const dropWhile

  4904   (Haskell "dropWhile")

  4905

  4906 code_const hd

  4907   (Haskell "head")

  4908

  4909 code_const last

  4910   (Haskell "last")

  4911

  4912 code_const list_all

  4913   (Haskell "all")

  4914

  4915 code_const list_ex

  4916   (Haskell "any")

  4917

  4918 end
`