src/HOL/List.thy
author nipkow
Wed May 08 13:01:40 2002 +0200 (2002-05-08)
changeset 13124 6e1decd8a7a9
parent 13122 c63612ffb186
child 13142 1ebd8ed5a1a0
permissions -rw-r--r--
new thm distinct_conv_nth
     1 (*  Title:      HOL/List.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1994 TU Muenchen
     5 *)
     6 
     7 header {* The datatype of finite lists *}
     8 
     9 theory List = PreList:
    10 
    11 datatype 'a list = Nil ("[]") | Cons 'a "'a list" (infixr "#" 65)
    12 
    13 consts
    14   "@"         :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"            (infixr 65)
    15   filter      :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    16   concat      :: "'a list list \<Rightarrow> 'a list"
    17   foldl       :: "('b \<Rightarrow> 'a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a list \<Rightarrow> 'b"
    18   foldr       :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b"
    19   hd          :: "'a list \<Rightarrow> 'a"
    20   tl          :: "'a list \<Rightarrow> 'a list"
    21   last        :: "'a list \<Rightarrow> 'a"
    22   butlast     :: "'a list \<Rightarrow> 'a list"
    23   set         :: "'a list \<Rightarrow> 'a set"
    24   list_all    :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
    25   list_all2   :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"
    26   map         :: "('a\<Rightarrow>'b) \<Rightarrow> ('a list \<Rightarrow> 'b list)"
    27   mem         :: "'a \<Rightarrow> 'a list \<Rightarrow> bool"                    (infixl 55)
    28   nth         :: "'a list \<Rightarrow> nat \<Rightarrow> 'a"			  (infixl "!" 100)
    29   list_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a list"
    30   take        :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
    31   drop        :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list"
    32   takeWhile   :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    33   dropWhile   :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list"
    34   rev         :: "'a list \<Rightarrow> 'a list"
    35   zip	      :: "'a list \<Rightarrow> 'b list \<Rightarrow> ('a * 'b) list"
    36   upt         :: "nat \<Rightarrow> nat \<Rightarrow> nat list"                   ("(1[_../_'(])")
    37   remdups     :: "'a list \<Rightarrow> 'a list"
    38   null        :: "'a list \<Rightarrow> bool"
    39   "distinct"  :: "'a list \<Rightarrow> bool"
    40   replicate   :: "nat \<Rightarrow> 'a \<Rightarrow> 'a list"
    41 
    42 nonterminals
    43   lupdbinds  lupdbind
    44 
    45 syntax
    46   (* list Enumeration *)
    47   "@list"     :: "args \<Rightarrow> 'a list"                          ("[(_)]")
    48 
    49   (* Special syntax for filter *)
    50   "@filter"   :: "[pttrn, 'a list, bool] \<Rightarrow> 'a list"        ("(1[_:_./ _])")
    51 
    52   (* list update *)
    53   "_lupdbind"      :: "['a, 'a] \<Rightarrow> lupdbind"            ("(2_ :=/ _)")
    54   ""               :: "lupdbind \<Rightarrow> lupdbinds"           ("_")
    55   "_lupdbinds"     :: "[lupdbind, lupdbinds] \<Rightarrow> lupdbinds" ("_,/ _")
    56   "_LUpdate"       :: "['a, lupdbinds] \<Rightarrow> 'a"           ("_/[(_)]" [900,0] 900)
    57 
    58   upto        :: "nat \<Rightarrow> nat \<Rightarrow> nat list"                   ("(1[_../_])")
    59 
    60 translations
    61   "[x, xs]"     == "x#[xs]"
    62   "[x]"         == "x#[]"
    63   "[x:xs . P]"  == "filter (%x. P) xs"
    64 
    65   "_LUpdate xs (_lupdbinds b bs)"  == "_LUpdate (_LUpdate xs b) bs"
    66   "xs[i:=x]"                       == "list_update xs i x"
    67 
    68   "[i..j]" == "[i..(Suc j)(]"
    69 
    70 
    71 syntax (xsymbols)
    72   "@filter"   :: "[pttrn, 'a list, bool] \<Rightarrow> 'a list"        ("(1[_\<in>_ ./ _])")
    73 
    74 
    75 consts
    76   lists        :: "'a set \<Rightarrow> 'a list set"
    77 
    78 inductive "lists A"
    79 intros
    80 Nil:  "[]: lists A"
    81 Cons: "\<lbrakk> a: A;  l: lists A \<rbrakk> \<Longrightarrow> a#l : lists A"
    82 
    83 
    84 (*Function "size" is overloaded for all datatypes.  Users may refer to the
    85   list version as "length".*)
    86 syntax   length :: "'a list \<Rightarrow> nat"
    87 translations  "length"  =>  "size:: _ list \<Rightarrow> nat"
    88 
    89 (* translating size::list -> length *)
    90 typed_print_translation
    91 {*
    92 let
    93 fun size_tr' _ (Type ("fun", (Type ("list", _) :: _))) [t] =
    94       Syntax.const "length" $ t
    95   | size_tr' _ _ _ = raise Match;
    96 in [("size", size_tr')] end
    97 *}
    98 
    99 primrec
   100   "hd(x#xs) = x"
   101 primrec
   102   "tl([])   = []"
   103   "tl(x#xs) = xs"
   104 primrec
   105   "null([])   = True"
   106   "null(x#xs) = False"
   107 primrec
   108   "last(x#xs) = (if xs=[] then x else last xs)"
   109 primrec
   110   "butlast []    = []"
   111   "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
   112 primrec
   113   "x mem []     = False"
   114   "x mem (y#ys) = (if y=x then True else x mem ys)"
   115 primrec
   116   "set [] = {}"
   117   "set (x#xs) = insert x (set xs)"
   118 primrec
   119   list_all_Nil:  "list_all P [] = True"
   120   list_all_Cons: "list_all P (x#xs) = (P(x) & list_all P xs)"
   121 primrec
   122   "map f []     = []"
   123   "map f (x#xs) = f(x)#map f xs"
   124 primrec
   125   append_Nil:  "[]    @ys = ys"
   126   append_Cons: "(x#xs)@ys = x#(xs@ys)"
   127 primrec
   128   "rev([])   = []"
   129   "rev(x#xs) = rev(xs) @ [x]"
   130 primrec
   131   "filter P []     = []"
   132   "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
   133 primrec
   134   foldl_Nil:  "foldl f a [] = a"
   135   foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
   136 primrec
   137   "foldr f [] a     = a"
   138   "foldr f (x#xs) a = f x (foldr f xs a)"
   139 primrec
   140   "concat([])   = []"
   141   "concat(x#xs) = x @ concat(xs)"
   142 primrec
   143   drop_Nil:  "drop n [] = []"
   144   drop_Cons: "drop n (x#xs) = (case n of 0 \<Rightarrow> x#xs | Suc(m) \<Rightarrow> drop m xs)"
   145   (* Warning: simpset does not contain this definition but separate theorems 
   146      for n=0 / n=Suc k*)
   147 primrec
   148   take_Nil:  "take n [] = []"
   149   take_Cons: "take n (x#xs) = (case n of 0 \<Rightarrow> [] | Suc(m) \<Rightarrow> x # take m xs)"
   150   (* Warning: simpset does not contain this definition but separate theorems 
   151      for n=0 / n=Suc k*)
   152 primrec 
   153   nth_Cons:  "(x#xs)!n = (case n of 0 \<Rightarrow> x | (Suc k) \<Rightarrow> xs!k)"
   154   (* Warning: simpset does not contain this definition but separate theorems 
   155      for n=0 / n=Suc k*)
   156 primrec
   157  "    [][i:=v] = []"
   158  "(x#xs)[i:=v] = (case i of 0     \<Rightarrow> v # xs 
   159 			  | Suc j \<Rightarrow> x # xs[j:=v])"
   160 primrec
   161   "takeWhile P []     = []"
   162   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
   163 primrec
   164   "dropWhile P []     = []"
   165   "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
   166 primrec
   167   "zip xs []     = []"
   168 zip_Cons:
   169   "zip xs (y#ys) = (case xs of [] \<Rightarrow> [] | z#zs \<Rightarrow> (z,y)#zip zs ys)"
   170   (* Warning: simpset does not contain this definition but separate theorems 
   171      for xs=[] / xs=z#zs *)
   172 primrec
   173   upt_0:   "[i..0(] = []"
   174   upt_Suc: "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
   175 primrec
   176   "distinct []     = True"
   177   "distinct (x#xs) = (x ~: set xs & distinct xs)"
   178 primrec
   179   "remdups [] = []"
   180   "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
   181 primrec
   182   replicate_0:   "replicate  0      x = []"
   183   replicate_Suc: "replicate (Suc n) x = x # replicate n x"
   184 defs
   185  list_all2_def:
   186  "list_all2 P xs ys == length xs = length ys & (!(x,y):set(zip xs ys). P x y)"
   187 
   188 
   189 (** Lexicographic orderings on lists **)
   190 
   191 consts
   192  lexn :: "('a * 'a)set \<Rightarrow> nat \<Rightarrow> ('a list * 'a list)set"
   193 primrec
   194 "lexn r 0       = {}"
   195 "lexn r (Suc n) = (prod_fun (%(x,xs). x#xs) (%(x,xs). x#xs) ` (r <*lex*> lexn r n)) Int
   196                   {(xs,ys). length xs = Suc n & length ys = Suc n}"
   197 
   198 constdefs
   199   lex :: "('a * 'a)set \<Rightarrow> ('a list * 'a list)set"
   200     "lex r == UN n. lexn r n"
   201 
   202   lexico :: "('a * 'a)set \<Rightarrow> ('a list * 'a list)set"
   203     "lexico r == inv_image (less_than <*lex*> lex r) (%xs. (length xs, xs))"
   204 
   205   sublist :: "['a list, nat set] \<Rightarrow> 'a list"
   206     "sublist xs A == map fst (filter (%p. snd p : A) (zip xs [0..size xs(]))"
   207 
   208 
   209 lemma not_Cons_self[simp]: "\<And>x. xs ~= x#xs"
   210 by(induct_tac "xs", auto)
   211 
   212 lemmas not_Cons_self2[simp] = not_Cons_self[THEN not_sym]
   213 
   214 lemma neq_Nil_conv: "(xs ~= []) = (? y ys. xs = y#ys)"
   215 by(induct_tac "xs", auto)
   216 
   217 (* Induction over the length of a list: *)
   218 (* "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)" *)
   219 lemmas length_induct = measure_induct[of length]
   220 
   221 
   222 (** "lists": the list-forming operator over sets **)
   223 
   224 lemma lists_mono: "A<=B ==> lists A <= lists B"
   225 apply(unfold lists.defs)
   226 apply(blast intro!:lfp_mono)
   227 done
   228 
   229 inductive_cases listsE[elim!]: "x#l : lists A"
   230 declare lists.intros[intro!]
   231 
   232 lemma lists_IntI[rule_format]:
   233  "l: lists A ==> l: lists B --> l: lists (A Int B)"
   234 apply(erule lists.induct)
   235 apply blast+
   236 done
   237 
   238 lemma lists_Int_eq[simp]: "lists (A Int B) = lists A Int lists B"
   239 apply(rule mono_Int[THEN equalityI])
   240 apply(simp add:mono_def lists_mono)
   241 apply(blast intro!: lists_IntI)
   242 done
   243 
   244 lemma append_in_lists_conv[iff]:
   245  "(xs@ys : lists A) = (xs : lists A & ys : lists A)"
   246 by(induct_tac "xs", auto)
   247 
   248 (** length **)
   249 (* needs to come before "@" because of thm append_eq_append_conv *)
   250 
   251 section "length"
   252 
   253 lemma length_append[simp]: "length(xs@ys) = length(xs)+length(ys)"
   254 by(induct_tac "xs", auto)
   255 
   256 lemma length_map[simp]: "length (map f xs) = length xs"
   257 by(induct_tac "xs", auto)
   258 
   259 lemma length_rev[simp]: "length(rev xs) = length(xs)"
   260 by(induct_tac "xs", auto)
   261 
   262 lemma length_tl[simp]: "length(tl xs) = (length xs) - 1"
   263 by(case_tac "xs", auto)
   264 
   265 lemma length_0_conv[iff]: "(length xs = 0) = (xs = [])"
   266 by(induct_tac "xs", auto)
   267 
   268 lemma length_greater_0_conv[iff]: "(0 < length xs) = (xs ~= [])"
   269 by(induct_tac xs, auto)
   270 
   271 lemma length_Suc_conv:
   272  "(length xs = Suc n) = (? y ys. xs = y#ys & length ys = n)"
   273 by(induct_tac "xs", auto)
   274 
   275 (** @ - append **)
   276 
   277 section "@ - append"
   278 
   279 lemma append_assoc[simp]: "(xs@ys)@zs = xs@(ys@zs)"
   280 by(induct_tac "xs", auto)
   281 
   282 lemma append_Nil2[simp]: "xs @ [] = xs"
   283 by(induct_tac "xs", auto)
   284 
   285 lemma append_is_Nil_conv[iff]: "(xs@ys = []) = (xs=[] & ys=[])"
   286 by(induct_tac "xs", auto)
   287 
   288 lemma Nil_is_append_conv[iff]: "([] = xs@ys) = (xs=[] & ys=[])"
   289 by(induct_tac "xs", auto)
   290 
   291 lemma append_self_conv[iff]: "(xs @ ys = xs) = (ys=[])"
   292 by(induct_tac "xs", auto)
   293 
   294 lemma self_append_conv[iff]: "(xs = xs @ ys) = (ys=[])"
   295 by(induct_tac "xs", auto)
   296 
   297 lemma append_eq_append_conv[rule_format,simp]:
   298  "!ys. length xs = length ys | length us = length vs
   299        --> (xs@us = ys@vs) = (xs=ys & us=vs)"
   300 apply(induct_tac "xs")
   301  apply(rule allI)
   302  apply(case_tac "ys")
   303   apply simp
   304  apply force
   305 apply(rule allI)
   306 apply(case_tac "ys")
   307  apply force
   308 apply simp
   309 done
   310 
   311 lemma same_append_eq[iff]: "(xs @ ys = xs @ zs) = (ys=zs)"
   312 by simp
   313 
   314 lemma append1_eq_conv[iff]: "(xs @ [x] = ys @ [y]) = (xs = ys & x = y)" 
   315 by simp
   316 
   317 lemma append_same_eq[iff]: "(ys @ xs = zs @ xs) = (ys=zs)"
   318 by simp
   319 
   320 lemma append_self_conv2[iff]: "(xs @ ys = ys) = (xs=[])"
   321 by(insert append_same_eq[of _ _ "[]"], auto)
   322 
   323 lemma self_append_conv2[iff]: "(ys = xs @ ys) = (xs=[])"
   324 by(auto simp add: append_same_eq[of "[]", simplified])
   325 
   326 lemma hd_Cons_tl[rule_format,simp]: "xs ~= [] --> hd xs # tl xs = xs"
   327 by(induct_tac "xs", auto)
   328 
   329 lemma hd_append: "hd(xs@ys) = (if xs=[] then hd ys else hd xs)"
   330 by(induct_tac "xs", auto)
   331 
   332 lemma hd_append2[simp]: "xs ~= [] ==> hd(xs @ ys) = hd xs"
   333 by(simp add: hd_append split: list.split)
   334 
   335 lemma tl_append: "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)"
   336 by(simp split: list.split)
   337 
   338 lemma tl_append2[simp]: "xs ~= [] ==> tl(xs @ ys) = (tl xs) @ ys"
   339 by(simp add: tl_append split: list.split)
   340 
   341 (* trivial rules for solving @-equations automatically *)
   342 
   343 lemma eq_Nil_appendI: "xs = ys ==> xs = [] @ ys"
   344 by simp
   345 
   346 lemma Cons_eq_appendI: "[| x#xs1 = ys; xs = xs1 @ zs |] ==> x#xs = ys@zs"
   347 by(drule sym, simp)
   348 
   349 lemma append_eq_appendI: "[| xs@xs1 = zs; ys = xs1 @ us |] ==> xs@ys = zs@us"
   350 by(drule sym, simp)
   351 
   352 
   353 (***
   354 Simplification procedure for all list equalities.
   355 Currently only tries to rearrange @ to see if
   356 - both lists end in a singleton list,
   357 - or both lists end in the same list.
   358 ***)
   359 ML_setup{*
   360 local
   361 
   362 val append_assoc = thm "append_assoc";
   363 val append_Nil = thm "append_Nil";
   364 val append_Cons = thm "append_Cons";
   365 val append1_eq_conv = thm "append1_eq_conv";
   366 val append_same_eq = thm "append_same_eq";
   367 
   368 val list_eq_pattern =
   369   Thm.read_cterm (Theory.sign_of (the_context ())) ("(xs::'a list) = ys",HOLogic.boolT)
   370 
   371 fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
   372       (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
   373   | last (Const("List.op @",_) $ _ $ ys) = last ys
   374   | last t = t
   375 
   376 fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
   377   | list1 _ = false
   378 
   379 fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
   380       (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
   381   | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
   382   | butlast xs = Const("List.list.Nil",fastype_of xs)
   383 
   384 val rearr_tac =
   385   simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons])
   386 
   387 fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
   388   let
   389     val lastl = last lhs and lastr = last rhs
   390     fun rearr conv =
   391       let val lhs1 = butlast lhs and rhs1 = butlast rhs
   392           val Type(_,listT::_) = eqT
   393           val appT = [listT,listT] ---> listT
   394           val app = Const("List.op @",appT)
   395           val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
   396           val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
   397           val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
   398             handle ERROR =>
   399             error("The error(s) above occurred while trying to prove " ^
   400                   string_of_cterm ct)
   401       in Some((conv RS (thm RS trans)) RS eq_reflection) end
   402 
   403   in if list1 lastl andalso list1 lastr
   404      then rearr append1_eq_conv
   405      else
   406      if lastl aconv lastr
   407      then rearr append_same_eq
   408      else None
   409   end
   410 in
   411 val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq
   412 end;
   413 
   414 Addsimprocs [list_eq_simproc];
   415 *}
   416 
   417 
   418 (** map **)
   419 
   420 section "map"
   421 
   422 lemma map_ext: "(\<And>x. x : set xs \<longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g xs"
   423 by (induct xs, simp_all)
   424 
   425 lemma map_ident[simp]: "map (%x. x) = (%xs. xs)"
   426 by(rule ext, induct_tac "xs", auto)
   427 
   428 lemma map_append[simp]: "map f (xs@ys) = map f xs @ map f ys"
   429 by(induct_tac "xs", auto)
   430 
   431 lemma map_compose(*[simp]*): "map (f o g) xs = map f (map g xs)"
   432 by(unfold o_def, induct_tac "xs", auto)
   433 
   434 lemma rev_map: "rev(map f xs) = map f (rev xs)"
   435 by(induct_tac xs, auto)
   436 
   437 (* a congruence rule for map: *)
   438 lemma map_cong:
   439  "xs=ys ==> (!!x. x : set ys \<Longrightarrow> f x = g x) \<Longrightarrow> map f xs = map g ys"
   440 by (clarify, induct ys, auto)
   441 
   442 lemma map_is_Nil_conv[iff]: "(map f xs = []) = (xs = [])"
   443 by(case_tac xs, auto)
   444 
   445 lemma Nil_is_map_conv[iff]: "([] = map f xs) = (xs = [])"
   446 by(case_tac xs, auto)
   447 
   448 lemma map_eq_Cons:
   449  "(map f xs = y#ys) = (? x xs'. xs = x#xs' & f x = y & map f xs' = ys)"
   450 by(case_tac xs, auto)
   451 
   452 lemma map_injective:
   453  "\<And>xs. map f xs = map f ys \<Longrightarrow> (!x y. f x = f y --> x=y) \<Longrightarrow> xs=ys"
   454 by(induct "ys", simp, fastsimp simp add:map_eq_Cons)
   455 
   456 lemma inj_mapI: "inj f ==> inj (map f)"
   457 by(blast dest:map_injective injD intro:injI)
   458 
   459 lemma inj_mapD: "inj (map f) ==> inj f"
   460 apply(unfold inj_on_def)
   461 apply clarify
   462 apply(erule_tac x = "[x]" in ballE)
   463  apply(erule_tac x = "[y]" in ballE)
   464   apply simp
   465  apply blast
   466 apply blast
   467 done
   468 
   469 lemma inj_map: "inj (map f) = inj f"
   470 by(blast dest:inj_mapD intro:inj_mapI)
   471 
   472 (** rev **)
   473 
   474 section "rev"
   475 
   476 lemma rev_append[simp]: "rev(xs@ys) = rev(ys) @ rev(xs)"
   477 by(induct_tac xs, auto)
   478 
   479 lemma rev_rev_ident[simp]: "rev(rev xs) = xs"
   480 by(induct_tac xs, auto)
   481 
   482 lemma rev_is_Nil_conv[iff]: "(rev xs = []) = (xs = [])"
   483 by(induct_tac xs, auto)
   484 
   485 lemma Nil_is_rev_conv[iff]: "([] = rev xs) = (xs = [])"
   486 by(induct_tac xs, auto)
   487 
   488 lemma rev_is_rev_conv[iff]: "!!ys. (rev xs = rev ys) = (xs = ys)"
   489 apply(induct "xs" )
   490  apply force
   491 apply(case_tac ys)
   492  apply simp
   493 apply force
   494 done
   495 
   496 lemma rev_induct: "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs"
   497 apply(subst rev_rev_ident[symmetric])
   498 apply(rule_tac list = "rev xs" in list.induct, simp_all)
   499 done
   500 
   501 (* Instead of (rev_induct_tac xs) use (induct_tac xs rule: rev_induct) *)
   502 
   503 lemma rev_exhaust: "(xs = [] \<Longrightarrow> P) \<Longrightarrow>  (!!ys y. xs = ys@[y] \<Longrightarrow> P) \<Longrightarrow> P"
   504 by(induct xs rule: rev_induct, auto)
   505 
   506 
   507 (** set **)
   508 
   509 section "set"
   510 
   511 lemma finite_set[iff]: "finite (set xs)"
   512 by(induct_tac xs, auto)
   513 
   514 lemma set_append[simp]: "set (xs@ys) = (set xs Un set ys)"
   515 by(induct_tac xs, auto)
   516 
   517 lemma set_subset_Cons: "set xs \<subseteq> set (x#xs)"
   518 by auto
   519 
   520 lemma set_empty[iff]: "(set xs = {}) = (xs = [])"
   521 by(induct_tac xs, auto)
   522 
   523 lemma set_rev[simp]: "set(rev xs) = set(xs)"
   524 by(induct_tac xs, auto)
   525 
   526 lemma set_map[simp]: "set(map f xs) = f`(set xs)"
   527 by(induct_tac xs, auto)
   528 
   529 lemma set_filter[simp]: "set(filter P xs) = {x. x : set xs & P x}"
   530 by(induct_tac xs, auto)
   531 
   532 lemma set_upt[simp]: "set[i..j(] = {k. i <= k & k < j}"
   533 apply(induct_tac j)
   534  apply simp_all
   535 apply(erule ssubst)
   536 apply auto
   537 apply arith
   538 done
   539 
   540 lemma in_set_conv_decomp: "(x : set xs) = (? ys zs. xs = ys@x#zs)"
   541 apply(induct_tac "xs")
   542  apply simp
   543 apply simp
   544 apply(rule iffI)
   545  apply(blast intro: eq_Nil_appendI Cons_eq_appendI)
   546 apply(erule exE)+
   547 apply(case_tac "ys")
   548 apply auto
   549 done
   550 
   551 
   552 (* eliminate `lists' in favour of `set' *)
   553 
   554 lemma in_lists_conv_set: "(xs : lists A) = (!x : set xs. x : A)"
   555 by(induct_tac xs, auto)
   556 
   557 lemmas in_listsD[dest!] = in_lists_conv_set[THEN iffD1]
   558 lemmas in_listsI[intro!] = in_lists_conv_set[THEN iffD2]
   559 
   560 
   561 (** mem **)
   562  
   563 section "mem"
   564 
   565 lemma set_mem_eq: "(x mem xs) = (x : set xs)"
   566 by(induct_tac xs, auto)
   567 
   568 
   569 (** list_all **)
   570 
   571 section "list_all"
   572 
   573 lemma list_all_conv: "list_all P xs = (!x:set xs. P x)"
   574 by(induct_tac xs, auto)
   575 
   576 lemma list_all_append[simp]:
   577  "list_all P (xs@ys) = (list_all P xs & list_all P ys)"
   578 by(induct_tac xs, auto)
   579 
   580 
   581 (** filter **)
   582 
   583 section "filter"
   584 
   585 lemma filter_append[simp]: "filter P (xs@ys) = filter P xs @ filter P ys"
   586 by(induct_tac xs, auto)
   587 
   588 lemma filter_filter[simp]: "filter P (filter Q xs) = filter (%x. Q x & P x) xs"
   589 by(induct_tac xs, auto)
   590 
   591 lemma filter_True[simp]: "!x : set xs. P x \<Longrightarrow> filter P xs = xs"
   592 by(induct xs, auto)
   593 
   594 lemma filter_False[simp]: "!x : set xs. ~P x \<Longrightarrow> filter P xs = []"
   595 by(induct xs, auto)
   596 
   597 lemma length_filter[simp]: "length (filter P xs) <= length xs"
   598 by(induct xs, auto simp add: le_SucI)
   599 
   600 lemma filter_is_subset[simp]: "set (filter P xs) <= set xs"
   601 by auto
   602 
   603 
   604 section "concat"
   605 
   606 lemma concat_append[simp]: "concat(xs@ys) = concat(xs)@concat(ys)"
   607 by(induct xs, auto)
   608 
   609 lemma concat_eq_Nil_conv[iff]: "(concat xss = []) = (!xs:set xss. xs=[])"
   610 by(induct xss, auto)
   611 
   612 lemma Nil_eq_concat_conv[iff]: "([] = concat xss) = (!xs:set xss. xs=[])"
   613 by(induct xss, auto)
   614 
   615 lemma set_concat[simp]: "set(concat xs) = Union(set ` set xs)"
   616 by(induct xs, auto)
   617 
   618 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)" 
   619 by(induct xs, auto)
   620 
   621 lemma filter_concat: "filter p (concat xs) = concat (map (filter p) xs)" 
   622 by(induct xs, auto)
   623 
   624 lemma rev_concat: "rev(concat xs) = concat (map rev (rev xs))"
   625 by(induct xs, auto)
   626 
   627 (** nth **)
   628 
   629 section "nth"
   630 
   631 lemma nth_Cons_0[simp]: "(x#xs)!0 = x"
   632 by auto
   633 
   634 lemma nth_Cons_Suc[simp]: "(x#xs)!(Suc n) = xs!n"
   635 by auto
   636 
   637 declare nth.simps[simp del]
   638 
   639 lemma nth_append:
   640  "!!n. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))"
   641 apply(induct "xs")
   642  apply simp
   643 apply(case_tac "n" )
   644  apply auto
   645 done
   646 
   647 lemma nth_map[simp]: "!!n. n < length xs \<Longrightarrow> (map f xs)!n = f(xs!n)"
   648 apply(induct "xs" )
   649  apply simp
   650 apply(case_tac "n")
   651  apply auto
   652 done
   653 
   654 lemma set_conv_nth: "set xs = {xs!i |i. i < length xs}"
   655 apply(induct_tac "xs")
   656  apply simp
   657 apply simp
   658 apply safe
   659   apply(rule_tac x = 0 in exI)
   660   apply simp
   661  apply(rule_tac x = "Suc i" in exI)
   662  apply simp
   663 apply(case_tac "i")
   664  apply simp
   665 apply(rename_tac "j")
   666 apply(rule_tac x = "j" in exI)
   667 apply simp
   668 done
   669 
   670 lemma list_ball_nth: "\<lbrakk> n < length xs; !x : set xs. P x \<rbrakk> \<Longrightarrow> P(xs!n)"
   671 by(simp add:set_conv_nth, blast)
   672 
   673 lemma nth_mem[simp]: "n < length xs ==> xs!n : set xs"
   674 by(simp add:set_conv_nth, blast)
   675 
   676 lemma all_nth_imp_all_set:
   677  "\<lbrakk> !i < length xs. P(xs!i); x : set xs \<rbrakk> \<Longrightarrow> P x"
   678 by(simp add:set_conv_nth, blast)
   679 
   680 lemma all_set_conv_all_nth:
   681  "(!x : set xs. P x) = (!i. i<length xs --> P (xs ! i))"
   682 by(simp add:set_conv_nth, blast)
   683 
   684 
   685 (** list update **)
   686 
   687 section "list update"
   688 
   689 lemma length_list_update[simp]: "!!i. length(xs[i:=x]) = length xs"
   690 by(induct xs, simp, simp split:nat.split)
   691 
   692 lemma nth_list_update:
   693  "!!i j. i < length xs  \<Longrightarrow> (xs[i:=x])!j = (if i=j then x else xs!j)"
   694 by(induct xs, simp, auto simp add:nth_Cons split:nat.split)
   695 
   696 lemma nth_list_update_eq[simp]: "i < length xs  ==> (xs[i:=x])!i = x"
   697 by(simp add:nth_list_update)
   698 
   699 lemma nth_list_update_neq[simp]: "!!i j. i ~= j \<Longrightarrow> xs[i:=x]!j = xs!j"
   700 by(induct xs, simp, auto simp add:nth_Cons split:nat.split)
   701 
   702 lemma list_update_overwrite[simp]:
   703  "!!i. i < size xs ==> xs[i:=x, i:=y] = xs[i:=y]"
   704 by(induct xs, simp, simp split:nat.split)
   705 
   706 lemma list_update_same_conv:
   707  "!!i. i < length xs \<Longrightarrow> (xs[i := x] = xs) = (xs!i = x)"
   708 by(induct xs, simp, simp split:nat.split, blast)
   709 
   710 lemma update_zip:
   711 "!!i xy xs. length xs = length ys \<Longrightarrow>
   712     (zip xs ys)[i:=xy] = zip (xs[i:=fst xy]) (ys[i:=snd xy])"
   713 by(induct ys, auto, case_tac xs, auto split:nat.split)
   714 
   715 lemma set_update_subset_insert: "!!i. set(xs[i:=x]) <= insert x (set xs)"
   716 by(induct xs, simp, simp split:nat.split, fast)
   717 
   718 lemma set_update_subsetI: "[| set xs <= A; x:A |] ==> set(xs[i := x]) <= A"
   719 by(fast dest!:set_update_subset_insert[THEN subsetD])
   720 
   721 
   722 (** last & butlast **)
   723 
   724 section "last / butlast"
   725 
   726 lemma last_snoc[simp]: "last(xs@[x]) = x"
   727 by(induct xs, auto)
   728 
   729 lemma butlast_snoc[simp]:"butlast(xs@[x]) = xs"
   730 by(induct xs, auto)
   731 
   732 lemma length_butlast[simp]: "length(butlast xs) = length xs - 1"
   733 by(induct xs rule:rev_induct, auto)
   734 
   735 lemma butlast_append:
   736  "!!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)"
   737 by(induct xs, auto)
   738 
   739 lemma append_butlast_last_id[simp]:
   740  "xs ~= [] --> butlast xs @ [last xs] = xs"
   741 by(induct xs, auto)
   742 
   743 lemma in_set_butlastD: "x:set(butlast xs) ==> x:set xs"
   744 by(induct xs, auto split:split_if_asm)
   745 
   746 lemma in_set_butlast_appendI:
   747  "x:set(butlast xs) | x:set(butlast ys) ==> x:set(butlast(xs@ys))"
   748 by(auto dest:in_set_butlastD simp add:butlast_append)
   749 
   750 (** take  & drop **)
   751 section "take & drop"
   752 
   753 lemma take_0[simp]: "take 0 xs = []"
   754 by(induct xs, auto)
   755 
   756 lemma drop_0[simp]: "drop 0 xs = xs"
   757 by(induct xs, auto)
   758 
   759 lemma take_Suc_Cons[simp]: "take (Suc n) (x#xs) = x # take n xs"
   760 by simp
   761 
   762 lemma drop_Suc_Cons[simp]: "drop (Suc n) (x#xs) = drop n xs"
   763 by simp
   764 
   765 declare take_Cons[simp del] drop_Cons[simp del]
   766 
   767 lemma length_take[simp]: "!!xs. length(take n xs) = min (length xs) n"
   768 by(induct n, auto, case_tac xs, auto)
   769 
   770 lemma length_drop[simp]: "!!xs. length(drop n xs) = (length xs - n)"
   771 by(induct n, auto, case_tac xs, auto)
   772 
   773 lemma take_all[simp]: "!!xs. length xs <= n ==> take n xs = xs"
   774 by(induct n, auto, case_tac xs, auto)
   775 
   776 lemma drop_all[simp]: "!!xs. length xs <= n ==> drop n xs = []"
   777 by(induct n, auto, case_tac xs, auto)
   778 
   779 lemma take_append[simp]:
   780  "!!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)"
   781 by(induct n, auto, case_tac xs, auto)
   782 
   783 lemma drop_append[simp]:
   784  "!!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys" 
   785 by(induct n, auto, case_tac xs, auto)
   786 
   787 lemma take_take[simp]: "!!xs n. take n (take m xs) = take (min n m) xs"
   788 apply(induct m)
   789  apply auto
   790 apply(case_tac xs)
   791  apply auto
   792 apply(case_tac na)
   793  apply auto
   794 done
   795 
   796 lemma drop_drop[simp]: "!!xs. drop n (drop m xs) = drop (n + m) xs" 
   797 apply(induct m)
   798  apply auto
   799 apply(case_tac xs)
   800  apply auto
   801 done
   802 
   803 lemma take_drop: "!!xs n. take n (drop m xs) = drop m (take (n + m) xs)"
   804 apply(induct m)
   805  apply auto
   806 apply(case_tac xs)
   807  apply auto
   808 done
   809 
   810 lemma append_take_drop_id[simp]: "!!xs. take n xs @ drop n xs = xs"
   811 apply(induct n)
   812  apply auto
   813 apply(case_tac xs)
   814  apply auto
   815 done
   816 
   817 lemma take_map: "!!xs. take n (map f xs) = map f (take n xs)"
   818 apply(induct n)
   819  apply auto
   820 apply(case_tac xs)
   821  apply auto
   822 done
   823 
   824 lemma drop_map: "!!xs. drop n (map f xs) = map f (drop n xs)" 
   825 apply(induct n)
   826  apply auto
   827 apply(case_tac xs)
   828  apply auto
   829 done
   830 
   831 lemma rev_take: "!!i. rev (take i xs) = drop (length xs - i) (rev xs)"
   832 apply(induct xs)
   833  apply auto
   834 apply(case_tac i)
   835  apply auto
   836 done
   837 
   838 lemma rev_drop: "!!i. rev (drop i xs) = take (length xs - i) (rev xs)"
   839 apply(induct xs)
   840  apply auto
   841 apply(case_tac i)
   842  apply auto
   843 done
   844 
   845 lemma nth_take[simp]: "!!n i. i < n ==> (take n xs)!i = xs!i"
   846 apply(induct xs)
   847  apply auto
   848 apply(case_tac n)
   849  apply(blast )
   850 apply(case_tac i)
   851  apply auto
   852 done
   853 
   854 lemma nth_drop[simp]: "!!xs i. n + i <= length xs ==> (drop n xs)!i = xs!(n+i)"
   855 apply(induct n)
   856  apply auto
   857 apply(case_tac xs)
   858  apply auto
   859 done
   860 
   861 lemma append_eq_conv_conj:
   862  "!!zs. (xs@ys = zs) = (xs = take (length xs) zs & ys = drop (length xs) zs)"
   863 apply(induct xs)
   864  apply simp
   865 apply clarsimp
   866 apply(case_tac zs)
   867 apply auto
   868 done
   869 
   870 (** takeWhile & dropWhile **)
   871 
   872 section "takeWhile & dropWhile"
   873 
   874 lemma takeWhile_dropWhile_id[simp]: "takeWhile P xs @ dropWhile P xs = xs"
   875 by(induct xs, auto)
   876 
   877 lemma  takeWhile_append1[simp]:
   878  "\<lbrakk> x:set xs; ~P(x) \<rbrakk> \<Longrightarrow> takeWhile P (xs @ ys) = takeWhile P xs"
   879 by(induct xs, auto)
   880 
   881 lemma takeWhile_append2[simp]:
   882  "(!!x. x : set xs \<Longrightarrow> P(x)) ==> takeWhile P (xs @ ys) = xs @ takeWhile P ys"
   883 by(induct xs, auto)
   884 
   885 lemma takeWhile_tail: "~P(x) ==> takeWhile P (xs @ (x#l)) = takeWhile P xs"
   886 by(induct xs, auto)
   887 
   888 lemma dropWhile_append1[simp]:
   889  "\<lbrakk> x : set xs; ~P(x) \<rbrakk> \<Longrightarrow> dropWhile P (xs @ ys) = (dropWhile P xs)@ys"
   890 by(induct xs, auto)
   891 
   892 lemma dropWhile_append2[simp]:
   893  "(!!x. x:set xs \<Longrightarrow> P(x)) ==> dropWhile P (xs @ ys) = dropWhile P ys"
   894 by(induct xs, auto)
   895 
   896 lemma set_take_whileD: "x:set(takeWhile P xs) ==> x:set xs & P x"
   897 by(induct xs, auto split:split_if_asm)
   898 
   899 
   900 (** zip **)
   901 section "zip"
   902 
   903 lemma zip_Nil[simp]: "zip [] ys = []"
   904 by(induct ys, auto)
   905 
   906 lemma zip_Cons_Cons[simp]: "zip (x#xs) (y#ys) = (x,y)#zip xs ys"
   907 by simp
   908 
   909 declare zip_Cons[simp del]
   910 
   911 lemma length_zip[simp]:
   912  "!!xs. length (zip xs ys) = min (length xs) (length ys)"
   913 apply(induct ys)
   914  apply simp
   915 apply(case_tac xs)
   916  apply auto
   917 done
   918 
   919 lemma zip_append1:
   920  "!!xs. zip (xs@ys) zs =
   921         zip xs (take (length xs) zs) @ zip ys (drop (length xs) zs)"
   922 apply(induct zs)
   923  apply simp
   924 apply(case_tac xs)
   925  apply simp_all
   926 done
   927 
   928 lemma zip_append2:
   929  "!!ys. zip xs (ys@zs) =
   930         zip (take (length ys) xs) ys @ zip (drop (length ys) xs) zs"
   931 apply(induct xs)
   932  apply simp
   933 apply(case_tac ys)
   934  apply simp_all
   935 done
   936 
   937 lemma zip_append[simp]:
   938  "[| length xs = length us; length ys = length vs |] ==> \
   939 \ zip (xs@ys) (us@vs) = zip xs us @ zip ys vs"
   940 by(simp add: zip_append1)
   941 
   942 lemma zip_rev:
   943  "!!xs. length xs = length ys ==> zip (rev xs) (rev ys) = rev (zip xs ys)"
   944 apply(induct ys)
   945  apply simp
   946 apply(case_tac xs)
   947  apply simp_all
   948 done
   949 
   950 lemma nth_zip[simp]:
   951 "!!i xs. \<lbrakk> i < length xs; i < length ys \<rbrakk> \<Longrightarrow> (zip xs ys)!i = (xs!i, ys!i)"
   952 apply(induct ys)
   953  apply simp
   954 apply(case_tac xs)
   955  apply (simp_all add: nth.simps split:nat.split)
   956 done
   957 
   958 lemma set_zip:
   959  "set(zip xs ys) = {(xs!i,ys!i) |i. i < min (length xs) (length ys)}"
   960 by(simp add: set_conv_nth cong: rev_conj_cong)
   961 
   962 lemma zip_update:
   963  "length xs = length ys ==> zip (xs[i:=x]) (ys[i:=y]) = (zip xs ys)[i:=(x,y)]"
   964 by(rule sym, simp add: update_zip)
   965 
   966 lemma zip_replicate[simp]:
   967  "!!j. zip (replicate i x) (replicate j y) = replicate (min i j) (x,y)"
   968 apply(induct i)
   969  apply auto
   970 apply(case_tac j)
   971  apply auto
   972 done
   973 
   974 (** list_all2 **)
   975 section "list_all2"
   976 
   977 lemma list_all2_lengthD: "list_all2 P xs ys ==> length xs = length ys"
   978 by(simp add:list_all2_def)
   979 
   980 lemma list_all2_Nil[iff]: "list_all2 P [] ys = (ys=[])"
   981 by(simp add:list_all2_def)
   982 
   983 lemma list_all2_Nil2[iff]: "list_all2 P xs [] = (xs=[])"
   984 by(simp add:list_all2_def)
   985 
   986 lemma list_all2_Cons[iff]:
   987  "list_all2 P (x#xs) (y#ys) = (P x y & list_all2 P xs ys)"
   988 by(auto simp add:list_all2_def)
   989 
   990 lemma list_all2_Cons1:
   991  "list_all2 P (x#xs) ys = (? z zs. ys = z#zs & P x z & list_all2 P xs zs)"
   992 by(case_tac ys, auto)
   993 
   994 lemma list_all2_Cons2:
   995  "list_all2 P xs (y#ys) = (? z zs. xs = z#zs & P z y & list_all2 P zs ys)"
   996 by(case_tac xs, auto)
   997 
   998 lemma list_all2_rev[iff]:
   999  "list_all2 P (rev xs) (rev ys) = list_all2 P xs ys"
  1000 by(simp add:list_all2_def zip_rev cong:conj_cong)
  1001 
  1002 lemma list_all2_append1:
  1003  "list_all2 P (xs@ys) zs =
  1004   (EX us vs. zs = us@vs & length us = length xs & length vs = length ys &
  1005              list_all2 P xs us & list_all2 P ys vs)"
  1006 apply(simp add:list_all2_def zip_append1)
  1007 apply(rule iffI)
  1008  apply(rule_tac x = "take (length xs) zs" in exI)
  1009  apply(rule_tac x = "drop (length xs) zs" in exI)
  1010  apply(force split: nat_diff_split simp add:min_def)
  1011 apply clarify
  1012 apply(simp add: ball_Un)
  1013 done
  1014 
  1015 lemma list_all2_append2:
  1016  "list_all2 P xs (ys@zs) =
  1017   (EX us vs. xs = us@vs & length us = length ys & length vs = length zs &
  1018              list_all2 P us ys & list_all2 P vs zs)"
  1019 apply(simp add:list_all2_def zip_append2)
  1020 apply(rule iffI)
  1021  apply(rule_tac x = "take (length ys) xs" in exI)
  1022  apply(rule_tac x = "drop (length ys) xs" in exI)
  1023  apply(force split: nat_diff_split simp add:min_def)
  1024 apply clarify
  1025 apply(simp add: ball_Un)
  1026 done
  1027 
  1028 lemma list_all2_conv_all_nth:
  1029   "list_all2 P xs ys =
  1030    (length xs = length ys & (!i<length xs. P (xs!i) (ys!i)))"
  1031 by(force simp add:list_all2_def set_zip)
  1032 
  1033 lemma list_all2_trans[rule_format]:
  1034  "ALL a b c. P1 a b --> P2 b c --> P3 a c ==>
  1035   ALL bs cs. list_all2 P1 as bs --> list_all2 P2 bs cs --> list_all2 P3 as cs"
  1036 apply(induct_tac as)
  1037  apply simp
  1038 apply(rule allI)
  1039 apply(induct_tac bs)
  1040  apply simp
  1041 apply(rule allI)
  1042 apply(induct_tac cs)
  1043  apply auto
  1044 done
  1045 
  1046 
  1047 section "foldl"
  1048 
  1049 lemma foldl_append[simp]:
  1050  "!!a. foldl f a (xs @ ys) = foldl f (foldl f a xs) ys"
  1051 by(induct xs, auto)
  1052 
  1053 (* Note: `n <= foldl op+ n ns' looks simpler, but is more difficult to use
  1054    because it requires an additional transitivity step
  1055 *)
  1056 lemma start_le_sum: "!!n::nat. m <= n ==> m <= foldl op+ n ns"
  1057 by(induct ns, auto)
  1058 
  1059 lemma elem_le_sum: "!!n::nat. n : set ns ==> n <= foldl op+ 0 ns"
  1060 by(force intro: start_le_sum simp add:in_set_conv_decomp)
  1061 
  1062 lemma sum_eq_0_conv[iff]:
  1063  "!!m::nat. (foldl op+ m ns = 0) = (m=0 & (!n : set ns. n=0))"
  1064 by(induct ns, auto)
  1065 
  1066 (** upto **)
  1067 
  1068 (* Does not terminate! *)
  1069 lemma upt_rec: "[i..j(] = (if i<j then i#[Suc i..j(] else [])"
  1070 by(induct j, auto)
  1071 
  1072 lemma upt_conv_Nil[simp]: "j<=i ==> [i..j(] = []"
  1073 by(subst upt_rec, simp)
  1074 
  1075 (*Only needed if upt_Suc is deleted from the simpset*)
  1076 lemma upt_Suc_append: "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]"
  1077 by simp
  1078 
  1079 lemma upt_conv_Cons: "i<j ==> [i..j(] = i#[Suc i..j(]"
  1080 apply(rule trans)
  1081 apply(subst upt_rec)
  1082  prefer 2 apply(rule refl)
  1083 apply simp
  1084 done
  1085 
  1086 (*LOOPS as a simprule, since j<=j*)
  1087 lemma upt_add_eq_append: "i<=j ==> [i..j+k(] = [i..j(]@[j..j+k(]"
  1088 by(induct_tac "k", auto)
  1089 
  1090 lemma length_upt[simp]: "length [i..j(] = j-i"
  1091 by(induct_tac j, simp, simp add: Suc_diff_le)
  1092 
  1093 lemma nth_upt[simp]: "i+k < j ==> [i..j(] ! k = i+k"
  1094 apply(induct j)
  1095 apply(auto simp add: less_Suc_eq nth_append split:nat_diff_split)
  1096 done
  1097 
  1098 lemma take_upt[simp]: "!!i. i+m <= n ==> take m [i..n(] = [i..i+m(]"
  1099 apply(induct m)
  1100  apply simp
  1101 apply(subst upt_rec)
  1102 apply(rule sym)
  1103 apply(subst upt_rec)
  1104 apply(simp del: upt.simps)
  1105 done
  1106 
  1107 lemma map_Suc_upt: "map Suc [m..n(] = [Suc m..n]"
  1108 by(induct n, auto)
  1109 
  1110 lemma nth_map_upt: "!!i. i < n-m ==> (map f [m..n(]) ! i = f(m+i)"
  1111 thm diff_induct
  1112 apply(induct n m rule: diff_induct)
  1113 prefer 3 apply(subst map_Suc_upt[symmetric])
  1114 apply(auto simp add: less_diff_conv nth_upt)
  1115 done
  1116 
  1117 lemma nth_take_lemma[rule_format]:
  1118  "ALL xs ys. k <= length xs --> k <= length ys
  1119              --> (ALL i. i < k --> xs!i = ys!i)
  1120              --> take k xs = take k ys"
  1121 apply(induct_tac k)
  1122 apply(simp_all add: less_Suc_eq_0_disj all_conj_distrib)
  1123 apply clarify
  1124 (*Both lists must be non-empty*)
  1125 apply(case_tac xs)
  1126  apply simp
  1127 apply(case_tac ys)
  1128  apply clarify
  1129  apply(simp (no_asm_use))
  1130 apply clarify
  1131 (*prenexing's needed, not miniscoping*)
  1132 apply(simp (no_asm_use) add: all_simps[symmetric] del: all_simps)
  1133 apply blast
  1134 (*prenexing's needed, not miniscoping*)
  1135 done
  1136 
  1137 lemma nth_equalityI:
  1138  "[| length xs = length ys; ALL i < length xs. xs!i = ys!i |] ==> xs = ys"
  1139 apply(frule nth_take_lemma[OF le_refl eq_imp_le])
  1140 apply(simp_all add: take_all)
  1141 done
  1142 
  1143 (*The famous take-lemma*)
  1144 lemma take_equalityI: "(ALL i. take i xs = take i ys) ==> xs = ys"
  1145 apply(drule_tac x = "max (length xs) (length ys)" in spec)
  1146 apply(simp add: le_max_iff_disj take_all)
  1147 done
  1148 
  1149 
  1150 (** distinct & remdups **)
  1151 section "distinct & remdups"
  1152 
  1153 lemma distinct_append[simp]:
  1154  "distinct(xs@ys) = (distinct xs & distinct ys & set xs Int set ys = {})"
  1155 by(induct xs, auto)
  1156 
  1157 lemma set_remdups[simp]: "set(remdups xs) = set xs"
  1158 by(induct xs, simp, simp add:insert_absorb)
  1159 
  1160 lemma distinct_remdups[iff]: "distinct(remdups xs)"
  1161 by(induct xs, auto)
  1162 
  1163 lemma distinct_filter[simp]: "distinct xs ==> distinct (filter P xs)"
  1164 by(induct xs, auto)
  1165 
  1166 (* It is best to avoid this indexed version of distinct,
  1167    but sometimes it is useful *)
  1168 lemma distinct_conv_nth:
  1169  "distinct xs = (\<forall>i j. i < size xs \<and> j < size xs \<and> i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
  1170 apply(induct_tac xs)
  1171  apply simp
  1172 apply simp
  1173 apply(rule iffI)
  1174  apply(clarsimp)
  1175  apply(case_tac i)
  1176   apply(case_tac j)
  1177    apply simp
  1178   apply(simp add:set_conv_nth)
  1179  apply(case_tac j)
  1180   apply(clarsimp simp add:set_conv_nth)
  1181  apply simp
  1182 apply(rule conjI)
  1183  apply(clarsimp simp add:set_conv_nth)
  1184  apply(erule_tac x = 0 in allE)
  1185  apply(erule_tac x = "Suc i" in allE)
  1186  apply simp
  1187 apply clarsimp
  1188 apply(erule_tac x = "Suc i" in allE)
  1189 apply(erule_tac x = "Suc j" in allE)
  1190 apply simp
  1191 done
  1192 
  1193 (** replicate **)
  1194 section "replicate"
  1195 
  1196 lemma length_replicate[simp]: "length(replicate n x) = n"
  1197 by(induct n, auto)
  1198 
  1199 lemma map_replicate[simp]: "map f (replicate n x) = replicate n (f x)"
  1200 by(induct n, auto)
  1201 
  1202 lemma replicate_app_Cons_same:
  1203  "(replicate n x) @ (x#xs) = x # replicate n x @ xs"
  1204 by(induct n, auto)
  1205 
  1206 lemma rev_replicate[simp]: "rev(replicate n x) = replicate n x"
  1207 apply(induct n)
  1208  apply simp
  1209 apply(simp add: replicate_app_Cons_same)
  1210 done
  1211 
  1212 lemma replicate_add: "replicate (n+m) x = replicate n x @ replicate m x"
  1213 by(induct n, auto)
  1214 
  1215 lemma hd_replicate[simp]: "n ~= 0 ==> hd(replicate n x) = x"
  1216 by(induct n, auto)
  1217 
  1218 lemma tl_replicate[simp]: "n ~= 0 ==> tl(replicate n x) = replicate (n - 1) x"
  1219 by(induct n, auto)
  1220 
  1221 lemma last_replicate[rule_format,simp]:
  1222  "n ~= 0 --> last(replicate n x) = x"
  1223 by(induct_tac n, auto)
  1224 
  1225 lemma nth_replicate[simp]: "!!i. i<n ==> (replicate n x)!i = x"
  1226 apply(induct n)
  1227  apply simp
  1228 apply(simp add: nth_Cons split:nat.split)
  1229 done
  1230 
  1231 lemma set_replicate_Suc: "set(replicate (Suc n) x) = {x}"
  1232 by(induct n, auto)
  1233 
  1234 lemma set_replicate[simp]: "n ~= 0 ==> set(replicate n x) = {x}"
  1235 by(fast dest!: not0_implies_Suc intro!: set_replicate_Suc)
  1236 
  1237 lemma set_replicate_conv_if: "set(replicate n x) = (if n=0 then {} else {x})"
  1238 by auto
  1239 
  1240 lemma in_set_replicateD: "x : set(replicate n y) ==> x=y"
  1241 by(simp add: set_replicate_conv_if split:split_if_asm)
  1242 
  1243 
  1244 (*** Lexcicographic orderings on lists ***)
  1245 section"Lexcicographic orderings on lists"
  1246 
  1247 lemma wf_lexn: "wf r ==> wf(lexn r n)"
  1248 apply(induct_tac n)
  1249  apply simp
  1250 apply simp
  1251 apply(rule wf_subset)
  1252  prefer 2 apply(rule Int_lower1)
  1253 apply(rule wf_prod_fun_image)
  1254  prefer 2 apply(rule injI)
  1255 apply auto
  1256 done
  1257 
  1258 lemma lexn_length:
  1259  "!!xs ys. (xs,ys) : lexn r n ==> length xs = n & length ys = n"
  1260 by(induct n, auto)
  1261 
  1262 lemma wf_lex[intro!]: "wf r ==> wf(lex r)"
  1263 apply(unfold lex_def)
  1264 apply(rule wf_UN)
  1265 apply(blast intro: wf_lexn)
  1266 apply clarify
  1267 apply(rename_tac m n)
  1268 apply(subgoal_tac "m ~= n")
  1269  prefer 2 apply blast
  1270 apply(blast dest: lexn_length not_sym)
  1271 done
  1272 
  1273 
  1274 lemma lexn_conv:
  1275  "lexn r n =
  1276   {(xs,ys). length xs = n & length ys = n &
  1277             (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}"
  1278 apply(induct_tac n)
  1279  apply simp
  1280  apply blast
  1281 apply(simp add: image_Collect lex_prod_def)
  1282 apply auto
  1283   apply blast
  1284  apply(rename_tac a xys x xs' y ys')
  1285  apply(rule_tac x = "a#xys" in exI)
  1286  apply simp
  1287 apply(case_tac xys)
  1288  apply simp_all
  1289 apply blast
  1290 done
  1291 
  1292 lemma lex_conv:
  1293  "lex r =
  1294   {(xs,ys). length xs = length ys &
  1295             (? xys x y xs' ys'. xs= xys @ x#xs' & ys= xys @ y#ys' & (x,y):r)}"
  1296 by(force simp add: lex_def lexn_conv)
  1297 
  1298 lemma wf_lexico[intro!]: "wf r ==> wf(lexico r)"
  1299 by(unfold lexico_def, blast)
  1300 
  1301 lemma lexico_conv:
  1302 "lexico r = {(xs,ys). length xs < length ys |
  1303                       length xs = length ys & (xs,ys) : lex r}"
  1304 by(simp add: lexico_def diag_def lex_prod_def measure_def inv_image_def)
  1305 
  1306 lemma Nil_notin_lex[iff]: "([],ys) ~: lex r"
  1307 by(simp add:lex_conv)
  1308 
  1309 lemma Nil2_notin_lex[iff]: "(xs,[]) ~: lex r"
  1310 by(simp add:lex_conv)
  1311 
  1312 lemma Cons_in_lex[iff]:
  1313  "((x#xs,y#ys) : lex r) =
  1314   ((x,y) : r & length xs = length ys | x=y & (xs,ys) : lex r)"
  1315 apply(simp add:lex_conv)
  1316 apply(rule iffI)
  1317  prefer 2 apply(blast intro: Cons_eq_appendI)
  1318 apply clarify
  1319 apply(case_tac xys)
  1320  apply simp
  1321 apply simp
  1322 apply blast
  1323 done
  1324 
  1325 
  1326 (*** sublist (a generalization of nth to sets) ***)
  1327 
  1328 lemma sublist_empty[simp]: "sublist xs {} = []"
  1329 by(auto simp add:sublist_def)
  1330 
  1331 lemma sublist_nil[simp]: "sublist [] A = []"
  1332 by(auto simp add:sublist_def)
  1333 
  1334 lemma sublist_shift_lemma:
  1335  "map fst [p:zip xs [i..i + length xs(] . snd p : A] =
  1336   map fst [p:zip xs [0..length xs(] . snd p + i : A]"
  1337 apply(induct_tac xs rule: rev_induct)
  1338  apply simp
  1339 apply(simp add:add_commute)
  1340 done
  1341 
  1342 lemma sublist_append:
  1343  "sublist (l@l') A = sublist l A @ sublist l' {j. j + length l : A}"
  1344 apply(unfold sublist_def)
  1345 apply(induct_tac l' rule: rev_induct)
  1346  apply simp
  1347 apply(simp add: upt_add_eq_append[of 0] zip_append sublist_shift_lemma)
  1348 apply(simp add:add_commute)
  1349 done
  1350 
  1351 lemma sublist_Cons:
  1352  "sublist (x#l) A = (if 0:A then [x] else []) @ sublist l {j. Suc j : A}"
  1353 apply(induct_tac l rule: rev_induct)
  1354  apply(simp add:sublist_def)
  1355 apply(simp del: append_Cons add: append_Cons[symmetric] sublist_append)
  1356 done
  1357 
  1358 lemma sublist_singleton[simp]: "sublist [x] A = (if 0 : A then [x] else [])"
  1359 by(simp add:sublist_Cons)
  1360 
  1361 lemma sublist_upt_eq_take[simp]: "sublist l {..n(} = take n l"
  1362 apply(induct_tac l rule: rev_induct)
  1363  apply simp
  1364 apply(simp split:nat_diff_split add:sublist_append)
  1365 done
  1366 
  1367 
  1368 lemma take_Cons': "take n (x#xs) = (if n=0 then [] else x # take (n - 1) xs)"
  1369 by(case_tac n, simp_all)
  1370 
  1371 lemma drop_Cons': "drop n (x#xs) = (if n=0 then x#xs else drop (n - 1) xs)"
  1372 by(case_tac n, simp_all)
  1373 
  1374 lemma nth_Cons': "(x#xs)!n = (if n=0 then x else xs!(n - 1))"
  1375 by(case_tac n, simp_all)
  1376 
  1377 lemmas [simp] = take_Cons'[of "number_of v",standard]
  1378                 drop_Cons'[of "number_of v",standard]
  1379                 nth_Cons'[of "number_of v",standard]
  1380 
  1381 end