src/ZF/List.thy
author wenzelm
Tue Jul 31 19:40:22 2007 +0200 (2007-07-31)
changeset 24091 109f19a13872
parent 16417 9bc16273c2d4
child 24893 b8ef7afe3a6b
permissions -rw-r--r--
added Tools/lin_arith.ML;
     1 (*  Title:      ZF/List
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1994  University of Cambridge
     5 
     6 *)
     7 
     8 header{*Lists in Zermelo-Fraenkel Set Theory*}
     9 
    10 theory List imports Datatype ArithSimp begin
    11 
    12 consts
    13   list       :: "i=>i"
    14 
    15 datatype
    16   "list(A)" = Nil | Cons ("a:A", "l: list(A)")
    17 
    18 
    19 syntax
    20  "[]"        :: i                                       ("[]")
    21  "@List"     :: "is => i"                                 ("[(_)]")
    22 
    23 translations
    24   "[x, xs]"     == "Cons(x, [xs])"
    25   "[x]"         == "Cons(x, [])"
    26   "[]"          == "Nil"
    27 
    28 
    29 consts
    30   length :: "i=>i"
    31   hd     :: "i=>i"
    32   tl     :: "i=>i"
    33 
    34 primrec
    35   "length([]) = 0"
    36   "length(Cons(a,l)) = succ(length(l))"
    37 
    38 primrec
    39   "hd([]) = 0"
    40   "hd(Cons(a,l)) = a"
    41 
    42 primrec
    43   "tl([]) = []"
    44   "tl(Cons(a,l)) = l"
    45 
    46 
    47 consts
    48   map         :: "[i=>i, i] => i"
    49   set_of_list :: "i=>i"
    50   app         :: "[i,i]=>i"                        (infixr "@" 60)
    51 
    52 (*map is a binding operator -- it applies to meta-level functions, not
    53 object-level functions.  This simplifies the final form of term_rec_conv,
    54 although complicating its derivation.*)
    55 primrec
    56   "map(f,[]) = []"
    57   "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
    58 
    59 primrec
    60   "set_of_list([]) = 0"
    61   "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
    62 
    63 primrec
    64   app_Nil:  "[] @ ys = ys"
    65   app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
    66 
    67 
    68 consts
    69   rev :: "i=>i"
    70   flat       :: "i=>i"
    71   list_add   :: "i=>i"
    72 
    73 primrec
    74   "rev([]) = []"
    75   "rev(Cons(a,l)) = rev(l) @ [a]"
    76 
    77 primrec
    78   "flat([]) = []"
    79   "flat(Cons(l,ls)) = l @ flat(ls)"
    80 
    81 primrec
    82   "list_add([]) = 0"
    83   "list_add(Cons(a,l)) = a #+ list_add(l)"
    84 
    85 consts
    86   drop       :: "[i,i]=>i"
    87 
    88 primrec
    89   drop_0:    "drop(0,l) = l"
    90   drop_succ: "drop(succ(i), l) = tl (drop(i,l))"
    91 
    92 
    93 (*** Thanks to Sidi Ehmety for the following ***)
    94 
    95 constdefs
    96 (* Function `take' returns the first n elements of a list *)
    97   take     :: "[i,i]=>i"
    98   "take(n, as) == list_rec(lam n:nat. [],
    99 		%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
   100 
   101   nth :: "[i, i]=>i"
   102   --{*returns the (n+1)th element of a list, or 0 if the
   103    list is too short.*}
   104   "nth(n, as) == list_rec(lam n:nat. 0,
   105  		          %a l r. lam n:nat. nat_case(a, %m. r`m, n), as) ` n"
   106 
   107   list_update :: "[i, i, i]=>i"
   108   "list_update(xs, i, v) == list_rec(lam n:nat. Nil,
   109       %u us vs. lam n:nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"
   110 
   111 consts
   112   filter :: "[i=>o, i] => i"
   113   upt :: "[i, i] =>i"
   114 
   115 primrec
   116   "filter(P, Nil) = Nil"
   117   "filter(P, Cons(x, xs)) =
   118      (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"
   119 
   120 primrec
   121   "upt(i, 0) = Nil"
   122   "upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)"
   123 
   124 constdefs
   125   min :: "[i,i] =>i"
   126     "min(x, y) == (if x le y then x else y)"
   127 
   128   max :: "[i, i] =>i"
   129     "max(x, y) == (if x le y then y else x)"
   130 
   131 (*** Aspects of the datatype definition ***)
   132 
   133 declare list.intros [simp,TC]
   134 
   135 (*An elimination rule, for type-checking*)
   136 inductive_cases ConsE: "Cons(a,l) : list(A)"
   137 
   138 lemma Cons_type_iff [simp]: "Cons(a,l) \<in> list(A) <-> a \<in> A & l \<in> list(A)"
   139 by (blast elim: ConsE) 
   140 
   141 (*Proving freeness results*)
   142 lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
   143 by auto
   144 
   145 lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
   146 by auto
   147 
   148 lemma list_unfold: "list(A) = {0} + (A * list(A))"
   149 by (blast intro!: list.intros [unfolded list.con_defs]
   150           elim: list.cases [unfolded list.con_defs])
   151 
   152 
   153 (**  Lemmas to justify using "list" in other recursive type definitions **)
   154 
   155 lemma list_mono: "A<=B ==> list(A) <= list(B)"
   156 apply (unfold list.defs )
   157 apply (rule lfp_mono)
   158 apply (simp_all add: list.bnd_mono)
   159 apply (assumption | rule univ_mono basic_monos)+
   160 done
   161 
   162 (*There is a similar proof by list induction.*)
   163 lemma list_univ: "list(univ(A)) <= univ(A)"
   164 apply (unfold list.defs list.con_defs)
   165 apply (rule lfp_lowerbound)
   166 apply (rule_tac [2] A_subset_univ [THEN univ_mono])
   167 apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
   168 done
   169 
   170 (*These two theorems justify datatypes involving list(nat), list(A), ...*)
   171 lemmas list_subset_univ = subset_trans [OF list_mono list_univ]
   172 
   173 lemma list_into_univ: "[| l: list(A);  A <= univ(B) |] ==> l: univ(B)"
   174 by (blast intro: list_subset_univ [THEN subsetD])
   175 
   176 lemma list_case_type:
   177     "[| l: list(A);
   178         c: C(Nil);
   179         !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))
   180      |] ==> list_case(c,h,l) : C(l)"
   181 by (erule list.induct, auto)
   182 
   183 lemma list_0_triv: "list(0) = {Nil}"
   184 apply (rule equalityI, auto) 
   185 apply (induct_tac x, auto) 
   186 done
   187 
   188 
   189 (*** List functions ***)
   190 
   191 lemma tl_type: "l: list(A) ==> tl(l) : list(A)"
   192 apply (induct_tac "l")
   193 apply (simp_all (no_asm_simp) add: list.intros)
   194 done
   195 
   196 (** drop **)
   197 
   198 lemma drop_Nil [simp]: "i:nat ==> drop(i, Nil) = Nil"
   199 apply (induct_tac "i")
   200 apply (simp_all (no_asm_simp))
   201 done
   202 
   203 lemma drop_succ_Cons [simp]: "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"
   204 apply (rule sym)
   205 apply (induct_tac "i")
   206 apply (simp (no_asm))
   207 apply (simp (no_asm_simp))
   208 done
   209 
   210 lemma drop_type [simp,TC]: "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"
   211 apply (induct_tac "i")
   212 apply (simp_all (no_asm_simp) add: tl_type)
   213 done
   214 
   215 declare drop_succ [simp del]
   216 
   217 
   218 (** Type checking -- proved by induction, as usual **)
   219 
   220 lemma list_rec_type [TC]:
   221     "[| l: list(A);
   222         c: C(Nil);
   223         !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))
   224      |] ==> list_rec(c,h,l) : C(l)"
   225 by (induct_tac "l", auto)
   226 
   227 (** map **)
   228 
   229 lemma map_type [TC]:
   230     "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"
   231 apply (simp add: map_list_def)
   232 apply (typecheck add: list.intros list_rec_type, blast)
   233 done
   234 
   235 lemma map_type2 [TC]: "l: list(A) ==> map(h,l) : list({h(u). u:A})"
   236 apply (erule map_type)
   237 apply (erule RepFunI)
   238 done
   239 
   240 (** length **)
   241 
   242 lemma length_type [TC]: "l: list(A) ==> length(l) : nat"
   243 by (simp add: length_list_def)
   244 
   245 lemma lt_length_in_nat:
   246    "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
   247 by (frule lt_nat_in_nat, typecheck) 
   248 
   249 (** app **)
   250 
   251 lemma app_type [TC]: "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)"
   252 by (simp add: app_list_def)
   253 
   254 (** rev **)
   255 
   256 lemma rev_type [TC]: "xs: list(A) ==> rev(xs) : list(A)"
   257 by (simp add: rev_list_def)
   258 
   259 
   260 (** flat **)
   261 
   262 lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) : list(A)"
   263 by (simp add: flat_list_def)
   264 
   265 
   266 (** set_of_list **)
   267 
   268 lemma set_of_list_type [TC]: "l: list(A) ==> set_of_list(l) : Pow(A)"
   269 apply (unfold set_of_list_list_def)
   270 apply (erule list_rec_type, auto)
   271 done
   272 
   273 lemma set_of_list_append:
   274      "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)"
   275 apply (erule list.induct)
   276 apply (simp_all (no_asm_simp) add: Un_cons)
   277 done
   278 
   279 
   280 (** list_add **)
   281 
   282 lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) : nat"
   283 by (simp add: list_add_list_def)
   284 
   285 
   286 (*** theorems about map ***)
   287 
   288 lemma map_ident [simp]: "l: list(A) ==> map(%u. u, l) = l"
   289 apply (induct_tac "l")
   290 apply (simp_all (no_asm_simp))
   291 done
   292 
   293 lemma map_compose: "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"
   294 apply (induct_tac "l")
   295 apply (simp_all (no_asm_simp))
   296 done
   297 
   298 lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"
   299 apply (induct_tac "xs")
   300 apply (simp_all (no_asm_simp))
   301 done
   302 
   303 lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"
   304 apply (induct_tac "ls")
   305 apply (simp_all (no_asm_simp) add: map_app_distrib)
   306 done
   307 
   308 lemma list_rec_map:
   309      "l: list(A) ==>
   310       list_rec(c, d, map(h,l)) =
   311       list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"
   312 apply (induct_tac "l")
   313 apply (simp_all (no_asm_simp))
   314 done
   315 
   316 (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)
   317 
   318 (* c : list(Collect(B,P)) ==> c : list(B) *)
   319 lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard]
   320 
   321 lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
   322 apply (induct_tac "l")
   323 apply (simp_all (no_asm_simp))
   324 done
   325 
   326 (*** theorems about length ***)
   327 
   328 lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
   329 by (induct_tac "xs", simp_all)
   330 
   331 lemma length_app [simp]:
   332      "[| xs: list(A); ys: list(A) |]
   333       ==> length(xs@ys) = length(xs) #+ length(ys)"
   334 by (induct_tac "xs", simp_all)
   335 
   336 lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
   337 apply (induct_tac "xs")
   338 apply (simp_all (no_asm_simp) add: length_app)
   339 done
   340 
   341 lemma length_flat:
   342      "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"
   343 apply (induct_tac "ls")
   344 apply (simp_all (no_asm_simp) add: length_app)
   345 done
   346 
   347 (** Length and drop **)
   348 
   349 (*Lemma for the inductive step of drop_length*)
   350 lemma drop_length_Cons [rule_format]:
   351      "xs: list(A) ==>
   352            \<forall>x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
   353 by (erule list.induct, simp_all)
   354 
   355 lemma drop_length [rule_format]:
   356      "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
   357 apply (erule list.induct, simp_all, safe)
   358 apply (erule drop_length_Cons)
   359 apply (rule natE)
   360 apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
   361 apply (blast intro: succ_in_naturalD length_type)
   362 done
   363 
   364 
   365 (*** theorems about app ***)
   366 
   367 lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
   368 by (erule list.induct, simp_all)
   369 
   370 lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
   371 by (induct_tac "xs", simp_all)
   372 
   373 lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"
   374 apply (induct_tac "ls")
   375 apply (simp_all (no_asm_simp) add: app_assoc)
   376 done
   377 
   378 (*** theorems about rev ***)
   379 
   380 lemma rev_map_distrib: "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"
   381 apply (induct_tac "l")
   382 apply (simp_all (no_asm_simp) add: map_app_distrib)
   383 done
   384 
   385 (*Simplifier needs the premises as assumptions because rewriting will not
   386   instantiate the variable ?A in the rules' typing conditions; note that
   387   rev_type does not instantiate ?A.  Only the premises do.
   388 *)
   389 lemma rev_app_distrib:
   390      "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"
   391 apply (erule list.induct)
   392 apply (simp_all add: app_assoc)
   393 done
   394 
   395 lemma rev_rev_ident [simp]: "l: list(A) ==> rev(rev(l))=l"
   396 apply (induct_tac "l")
   397 apply (simp_all (no_asm_simp) add: rev_app_distrib)
   398 done
   399 
   400 lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"
   401 apply (induct_tac "ls")
   402 apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib)
   403 done
   404 
   405 
   406 (*** theorems about list_add ***)
   407 
   408 lemma list_add_app:
   409      "[| xs: list(nat);  ys: list(nat) |]
   410       ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
   411 apply (induct_tac "xs", simp_all)
   412 done
   413 
   414 lemma list_add_rev: "l: list(nat) ==> list_add(rev(l)) = list_add(l)"
   415 apply (induct_tac "l")
   416 apply (simp_all (no_asm_simp) add: list_add_app)
   417 done
   418 
   419 lemma list_add_flat:
   420      "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"
   421 apply (induct_tac "ls")
   422 apply (simp_all (no_asm_simp) add: list_add_app)
   423 done
   424 
   425 (** New induction rules **)
   426 
   427 lemma list_append_induct [case_names Nil snoc, consumes 1]:
   428     "[| l: list(A);
   429         P(Nil);
   430         !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x])
   431      |] ==> P(l)"
   432 apply (subgoal_tac "P(rev(rev(l)))", simp)
   433 apply (erule rev_type [THEN list.induct], simp_all)
   434 done
   435 
   436 lemma list_complete_induct_lemma [rule_format]:
   437  assumes ih: 
   438     "\<And>l. [| l \<in> list(A); 
   439              \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|] 
   440           ==> P(l)"
   441   shows "n \<in> nat ==> \<forall>l \<in> list(A). length(l) < n --> P(l)"
   442 apply (induct_tac n, simp)
   443 apply (blast intro: ih elim!: leE) 
   444 done
   445 
   446 theorem list_complete_induct:
   447       "[| l \<in> list(A); 
   448           \<And>l. [| l \<in> list(A); 
   449                   \<forall>l' \<in> list(A). length(l') < length(l) --> P(l')|] 
   450                ==> P(l)
   451        |] ==> P(l)"
   452 apply (rule list_complete_induct_lemma [of A]) 
   453    prefer 4 apply (rule le_refl, simp) 
   454   apply blast 
   455  apply simp 
   456 apply assumption
   457 done
   458 
   459 
   460 (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
   461 
   462 (** min FIXME: replace by Int! **)
   463 (* Min theorems are also true for i, j ordinals *)
   464 lemma min_sym: "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)"
   465 apply (unfold min_def)
   466 apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
   467 done
   468 
   469 lemma min_type [simp,TC]: "[| i:nat; j:nat |] ==> min(i,j):nat"
   470 by (unfold min_def, auto)
   471 
   472 lemma min_0 [simp]: "i:nat ==> min(0,i) = 0"
   473 apply (unfold min_def)
   474 apply (auto dest: not_lt_imp_le)
   475 done
   476 
   477 lemma min_02 [simp]: "i:nat ==> min(i, 0) = 0"
   478 apply (unfold min_def)
   479 apply (auto dest: not_lt_imp_le)
   480 done
   481 
   482 lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k"
   483 apply (unfold min_def)
   484 apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
   485 done
   486 
   487 lemma min_succ_succ [simp]:
   488      "[| i:nat; j:nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))"
   489 apply (unfold min_def, auto)
   490 done
   491 
   492 (*** more theorems about lists ***)
   493 
   494 (** filter **)
   495 
   496 lemma filter_append [simp]:
   497      "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)"
   498 by (induct_tac "xs", auto)
   499 
   500 lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)"
   501 by (induct_tac "xs", auto)
   502 
   503 lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) le length(xs)"
   504 apply (induct_tac "xs", auto)
   505 apply (rule_tac j = "length (l) " in le_trans)
   506 apply (auto simp add: le_iff)
   507 done
   508 
   509 lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)"
   510 by (induct_tac "xs", auto)
   511 
   512 lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil"
   513 by (induct_tac "xs", auto)
   514 
   515 lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs"
   516 by (induct_tac "xs", auto)
   517 
   518 (** length **)
   519 
   520 lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil"
   521 by (erule list.induct, auto)
   522 
   523 lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil"
   524 by (erule list.induct, auto)
   525 
   526 lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
   527 by (erule list.induct, auto)
   528 
   529 lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil"
   530 by (erule list.induct, auto)
   531 
   532 lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)"
   533 by (erule list.induct, auto)
   534 
   535 (** more theorems about append **)
   536 
   537 lemma append_is_Nil_iff [simp]:
   538      "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)"
   539 by (erule list.induct, auto)
   540 
   541 lemma append_is_Nil_iff2 [simp]:
   542      "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)"
   543 by (erule list.induct, auto)
   544 
   545 lemma append_left_is_self_iff [simp]:
   546      "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)"
   547 by (erule list.induct, auto)
   548 
   549 lemma append_left_is_self_iff2 [simp]:
   550      "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)"
   551 by (erule list.induct, auto)
   552 
   553 (*TOO SLOW as a default simprule!*)
   554 lemma append_left_is_Nil_iff [rule_format]:
   555      "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
   556    length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))"
   557 apply (erule list.induct)
   558 apply (auto simp add: length_app)
   559 done
   560 
   561 (*TOO SLOW as a default simprule!*)
   562 lemma append_left_is_Nil_iff2 [rule_format]:
   563      "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
   564    length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))"
   565 apply (erule list.induct)
   566 apply (auto simp add: length_app)
   567 done
   568 
   569 lemma append_eq_append_iff [rule_format,simp]:
   570      "xs:list(A) ==> \<forall>ys \<in> list(A).
   571       length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)"
   572 apply (erule list.induct)
   573 apply (simp (no_asm_simp))
   574 apply clarify
   575 apply (erule_tac a = ys in list.cases, auto)
   576 done
   577 
   578 lemma append_eq_append [rule_format]:
   579   "xs:list(A) ==>
   580    \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A).
   581    length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)"
   582 apply (induct_tac "xs")
   583 apply (force simp add: length_app, clarify)
   584 apply (erule_tac a = ys in list.cases, simp)
   585 apply (subgoal_tac "Cons (a, l) @ us =vs")
   586  apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast)
   587 done
   588 
   589 lemma append_eq_append_iff2 [simp]:
   590  "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
   591   ==>  xs@us = ys@vs <-> (xs=ys & us=vs)"
   592 apply (rule iffI)
   593 apply (rule append_eq_append, auto)
   594 done
   595 
   596 lemma append_self_iff [simp]:
   597      "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
   598 by simp
   599 
   600 lemma append_self_iff2 [simp]:
   601      "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
   602 by simp
   603 
   604 (* Can also be proved from append_eq_append_iff2,
   605 but the proof requires two more hypotheses: x:A and y:A *)
   606 lemma append1_eq_iff [rule_format,simp]:
   607      "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
   608 apply (erule list.induct)  
   609  apply clarify 
   610  apply (erule list.cases)
   611  apply simp_all
   612 txt{*Inductive step*}  
   613 apply clarify 
   614 apply (erule_tac a=ys in list.cases, simp_all)  
   615 done
   616 
   617 
   618 lemma append_right_is_self_iff [simp]:
   619      "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
   620 by (simp (no_asm_simp) add: append_left_is_Nil_iff)
   621 
   622 lemma append_right_is_self_iff2 [simp]:
   623      "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
   624 apply (rule iffI)
   625 apply (drule sym, auto) 
   626 done
   627 
   628 lemma hd_append [rule_format,simp]:
   629      "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)"
   630 by (induct_tac "xs", auto)
   631 
   632 lemma tl_append [rule_format,simp]:
   633      "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys"
   634 by (induct_tac "xs", auto)
   635 
   636 (** rev **)
   637 lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)"
   638 by (erule list.induct, auto)
   639 
   640 lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)"
   641 by (erule list.induct, auto)
   642 
   643 lemma rev_is_rev_iff [rule_format,simp]:
   644      "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
   645 apply (erule list.induct, force, clarify)
   646 apply (erule_tac a = ys in list.cases, auto)
   647 done
   648 
   649 lemma rev_list_elim [rule_format]:
   650      "xs:list(A) ==>
   651       (xs=Nil --> P) --> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] -->P)-->P"
   652 by (erule list_append_induct, auto)
   653 
   654 
   655 (** more theorems about drop **)
   656 
   657 lemma length_drop [rule_format,simp]:
   658      "n:nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
   659 apply (erule nat_induct)
   660 apply (auto elim: list.cases)
   661 done
   662 
   663 lemma drop_all [rule_format,simp]:
   664      "n:nat ==> \<forall>xs \<in> list(A). length(xs) le n --> drop(n, xs)=Nil"
   665 apply (erule nat_induct)
   666 apply (auto elim: list.cases)
   667 done
   668 
   669 lemma drop_append [rule_format]:
   670      "n:nat ==> 
   671       \<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
   672 apply (induct_tac "n")
   673 apply (auto elim: list.cases)
   674 done
   675 
   676 lemma drop_drop:
   677     "m:nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
   678 apply (induct_tac "m")
   679 apply (auto elim: list.cases)
   680 done
   681 
   682 (** take **)
   683 
   684 lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) =  Nil"
   685 apply (unfold take_def)
   686 apply (erule list.induct, auto)
   687 done
   688 
   689 lemma take_succ_Cons [simp]:
   690     "n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))"
   691 by (simp add: take_def)
   692 
   693 (* Needed for proving take_all *)
   694 lemma take_Nil [simp]: "n:nat ==> take(n, Nil) = Nil"
   695 by (unfold take_def, auto)
   696 
   697 lemma take_all [rule_format,simp]:
   698      "n:nat ==> \<forall>xs \<in> list(A). length(xs) le n  --> take(n, xs) = xs"
   699 apply (erule nat_induct)
   700 apply (auto elim: list.cases) 
   701 done
   702 
   703 lemma take_type [rule_format,simp,TC]:
   704      "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
   705 apply (erule list.induct, simp, clarify) 
   706 apply (erule natE, auto)
   707 done
   708 
   709 lemma take_append [rule_format,simp]:
   710  "xs:list(A) ==>
   711   \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
   712                             take(n, xs) @ take(n #- length(xs), ys)"
   713 apply (erule list.induct, simp, clarify) 
   714 apply (erule natE, auto)
   715 done
   716 
   717 lemma take_take [rule_format]:
   718    "m : nat ==>
   719     \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
   720 apply (induct_tac "m", auto)
   721 apply (erule_tac a = xs in list.cases)
   722 apply (auto simp add: take_Nil)
   723 apply (erule_tac n=n in natE)
   724 apply (auto intro: take_0 take_type)
   725 done
   726 
   727 (** nth **)
   728 
   729 lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a"
   730 by (simp add: nth_def) 
   731 
   732 lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)"
   733 by (simp add: nth_def) 
   734 
   735 lemma nth_empty [simp]: "nth(n, Nil) = 0"
   736 by (simp add: nth_def) 
   737 
   738 lemma nth_type [rule_format,simp,TC]:
   739      "xs:list(A) ==> \<forall>n. n < length(xs) --> nth(n,xs) : A"
   740 apply (erule list.induct, simp, clarify)
   741 apply (subgoal_tac "n \<in> nat")  
   742  apply (erule natE, auto dest!: le_in_nat)
   743 done
   744 
   745 lemma nth_eq_0 [rule_format]:
   746      "xs:list(A) ==> \<forall>n \<in> nat. length(xs) le n --> nth(n,xs) = 0"
   747 apply (erule list.induct, simp, clarify) 
   748 apply (erule natE, auto)
   749 done
   750 
   751 lemma nth_append [rule_format]:
   752   "xs:list(A) ==> 
   753    \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
   754                                 else nth(n #- length(xs), ys))"
   755 apply (induct_tac "xs", simp, clarify) 
   756 apply (erule natE, auto)
   757 done
   758 
   759 lemma set_of_list_conv_nth:
   760     "xs:list(A)
   761      ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x = nth(i,xs)}"
   762 apply (induct_tac "xs", simp_all)
   763 apply (rule equalityI, auto)
   764 apply (rule_tac x = 0 in bexI, auto)
   765 apply (erule natE, auto)
   766 done
   767 
   768 (* Other theorems about lists *)
   769 
   770 lemma nth_take_lemma [rule_format]:
   771  "k:nat ==>
   772   \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k le length(xs) --> k le length(ys) -->
   773       (\<forall>i \<in> nat. i<k --> nth(i,xs) = nth(i,ys))--> take(k,xs) = take(k,ys))"
   774 apply (induct_tac "k")
   775 apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
   776 apply clarify
   777 (*Both lists are non-empty*)
   778 apply (erule_tac a=xs in list.cases, simp) 
   779 apply (erule_tac a=ys in list.cases, clarify) 
   780 apply (simp (no_asm_use) )
   781 apply clarify
   782 apply (simp (no_asm_simp))
   783 apply (rule conjI, force)
   784 apply (rename_tac y ys z zs) 
   785 apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto)   
   786 done
   787 
   788 lemma nth_equalityI [rule_format]:
   789      "[| xs:list(A); ys:list(A); length(xs) = length(ys);
   790          \<forall>i \<in> nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |]
   791       ==> xs = ys"
   792 apply (subgoal_tac "length (xs) le length (ys) ")
   793 apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma) 
   794 apply (simp_all add: take_all)
   795 done
   796 
   797 (*The famous take-lemma*)
   798 
   799 lemma take_equalityI [rule_format]:
   800     "[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |] 
   801      ==> xs = ys"
   802 apply (case_tac "length (xs) le length (ys) ")
   803 apply (drule_tac x = "length (ys) " in bspec)
   804 apply (drule_tac [3] not_lt_imp_le)
   805 apply (subgoal_tac [5] "length (ys) le length (xs) ")
   806 apply (rule_tac [6] j = "succ (length (ys))" in le_trans)
   807 apply (rule_tac [6] leI)
   808 apply (drule_tac [5] x = "length (xs) " in bspec)
   809 apply (simp_all add: take_all)
   810 done
   811 
   812 lemma nth_drop [rule_format]:
   813   "n:nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
   814 apply (induct_tac "n", simp_all, clarify)
   815 apply (erule list.cases, auto)  
   816 done
   817 
   818 lemma take_succ [rule_format]:
   819   "xs\<in>list(A) 
   820    ==> \<forall>i. i < length(xs) --> take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]"
   821 apply (induct_tac "xs", auto)
   822 apply (subgoal_tac "i\<in>nat") 
   823 apply (erule natE)
   824 apply (auto simp add: le_in_nat) 
   825 done
   826 
   827 lemma take_add [rule_format]:
   828      "[|xs\<in>list(A); j\<in>nat|] 
   829       ==> \<forall>i\<in>nat. take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))"
   830 apply (induct_tac "xs", simp_all, clarify)
   831 apply (erule_tac n = i in natE, simp_all)
   832 done
   833 
   834 lemma length_take:
   835      "l\<in>list(A) ==> \<forall>n\<in>nat. length(take(n,l)) = min(n, length(l))"
   836 apply (induct_tac "l", safe, simp_all)
   837 apply (erule natE, simp_all)
   838 done
   839 
   840 subsection{*The function zip*}
   841 
   842 text{*Crafty definition to eliminate a type argument*}
   843 
   844 consts
   845   zip_aux        :: "[i,i]=>i"
   846 
   847 primrec (*explicit lambda is required because both arguments of "un" vary*)
   848   "zip_aux(B,[]) =
   849      (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
   850 
   851   "zip_aux(B,Cons(x,l)) =
   852      (\<lambda>ys \<in> list(B).
   853         list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"
   854 
   855 constdefs
   856   zip :: "[i, i]=>i"
   857    "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys"
   858 
   859 
   860 (* zip equations *)
   861 
   862 lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))"
   863 apply (induct_tac xs, simp_all) 
   864 apply (blast intro: list_mono [THEN subsetD]) 
   865 done
   866 
   867 lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil"
   868 apply (simp add: zip_def list_on_set_of_list [of _ A])
   869 apply (erule list.cases, simp_all) 
   870 done
   871 
   872 lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil"
   873 apply (simp add: zip_def list_on_set_of_list [of _ A])
   874 apply (erule list.cases, simp_all) 
   875 done
   876 
   877 lemma zip_aux_unique [rule_format]:
   878      "[|B<=C;  xs \<in> list(A)|] 
   879       ==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
   880 apply (induct_tac xs) 
   881  apply simp_all 
   882  apply (blast intro: list_mono [THEN subsetD], clarify) 
   883 apply (erule_tac a=ys in list.cases, auto) 
   884 apply (blast intro: list_mono [THEN subsetD]) 
   885 done
   886 
   887 lemma zip_Cons_Cons [simp]:
   888      "[| xs:list(A); ys:list(B); x:A; y:B |] ==>
   889       zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))"
   890 apply (simp add: zip_def, auto) 
   891 apply (rule zip_aux_unique, auto) 
   892 apply (simp add: list_on_set_of_list [of _ B])
   893 apply (blast intro: list_on_set_of_list list_mono [THEN subsetD]) 
   894 done
   895 
   896 lemma zip_type [rule_format,simp,TC]:
   897      "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
   898 apply (induct_tac "xs")
   899 apply (simp (no_asm))
   900 apply clarify
   901 apply (erule_tac a = ys in list.cases, auto)
   902 done
   903 
   904 (* zip length *)
   905 lemma length_zip [rule_format,simp]:
   906      "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
   907                                      min(length(xs), length(ys))"
   908 apply (unfold min_def)
   909 apply (induct_tac "xs", simp_all, clarify) 
   910 apply (erule_tac a = ys in list.cases, auto)
   911 done
   912 
   913 lemma zip_append1 [rule_format]:
   914  "[| ys:list(A); zs:list(B) |] ==>
   915   \<forall>xs \<in> list(A). zip(xs @ ys, zs) = 
   916                  zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
   917 apply (induct_tac "zs", force, clarify) 
   918 apply (erule_tac a = xs in list.cases, simp_all) 
   919 done
   920 
   921 lemma zip_append2 [rule_format]:
   922  "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
   923        zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
   924 apply (induct_tac "xs", force, clarify) 
   925 apply (erule_tac a = ys in list.cases, auto)
   926 done
   927 
   928 lemma zip_append [simp]:
   929  "[| length(xs) = length(us); length(ys) = length(vs);
   930      xs:list(A); us:list(B); ys:list(A); vs:list(B) |] 
   931   ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)"
   932 by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)
   933 
   934 
   935 lemma zip_rev [rule_format,simp]:
   936  "ys:list(B) ==> \<forall>xs \<in> list(A).
   937     length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
   938 apply (induct_tac "ys", force, clarify) 
   939 apply (erule_tac a = xs in list.cases)
   940 apply (auto simp add: length_rev)
   941 done
   942 
   943 lemma nth_zip [rule_format,simp]:
   944    "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
   945                     i < length(xs) --> i < length(ys) -->
   946                     nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
   947 apply (induct_tac "ys", force, clarify) 
   948 apply (erule_tac a = xs in list.cases, simp) 
   949 apply (auto elim: natE)
   950 done
   951 
   952 lemma set_of_list_zip [rule_format]:
   953      "[| xs:list(A); ys:list(B); i:nat |]
   954       ==> set_of_list(zip(xs, ys)) =
   955           {<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys))
   956           & x = nth(i, xs) & y = nth(i, ys)}"
   957 by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
   958 
   959 (** list_update **)
   960 
   961 lemma list_update_Nil [simp]: "i:nat ==>list_update(Nil, i, v) = Nil"
   962 by (unfold list_update_def, auto)
   963 
   964 lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)"
   965 by (unfold list_update_def, auto)
   966 
   967 lemma list_update_Cons_succ [simp]:
   968   "n:nat ==>
   969     list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))"
   970 apply (unfold list_update_def, auto)
   971 done
   972 
   973 lemma list_update_type [rule_format,simp,TC]:
   974      "[| xs:list(A); v:A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
   975 apply (induct_tac "xs")
   976 apply (simp (no_asm))
   977 apply clarify
   978 apply (erule natE, auto)
   979 done
   980 
   981 lemma length_list_update [rule_format,simp]:
   982      "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
   983 apply (induct_tac "xs")
   984 apply (simp (no_asm))
   985 apply clarify
   986 apply (erule natE, auto)
   987 done
   988 
   989 lemma nth_list_update [rule_format]:
   990      "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs)  -->
   991          nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"
   992 apply (induct_tac "xs")
   993  apply simp_all
   994 apply clarify
   995 apply (rename_tac i j) 
   996 apply (erule_tac n=i in natE) 
   997 apply (erule_tac [2] n=j in natE)
   998 apply (erule_tac n=j in natE, simp_all, force) 
   999 done
  1000 
  1001 lemma nth_list_update_eq [simp]:
  1002      "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x"
  1003 by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)
  1004 
  1005 
  1006 lemma nth_list_update_neq [rule_format,simp]:
  1007   "xs:list(A) ==> 
  1008      \<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j --> nth(j, list_update(xs,i,x)) = nth(j,xs)"
  1009 apply (induct_tac "xs")
  1010  apply (simp (no_asm))
  1011 apply clarify
  1012 apply (erule natE)
  1013 apply (erule_tac [2] natE, simp_all) 
  1014 apply (erule natE, simp_all)
  1015 done
  1016 
  1017 lemma list_update_overwrite [rule_format,simp]:
  1018      "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
  1019    --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
  1020 apply (induct_tac "xs")
  1021  apply (simp (no_asm))
  1022 apply clarify
  1023 apply (erule natE, auto)
  1024 done
  1025 
  1026 lemma list_update_same_conv [rule_format]:
  1027      "xs:list(A) ==> 
  1028       \<forall>i \<in> nat. i < length(xs) --> 
  1029                  (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
  1030 apply (induct_tac "xs")
  1031  apply (simp (no_asm))
  1032 apply clarify
  1033 apply (erule natE, auto)
  1034 done
  1035 
  1036 lemma update_zip [rule_format]:
  1037      "ys:list(B) ==> 
  1038       \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
  1039         length(xs) = length(ys) -->
  1040         list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
  1041                                               list_update(ys, i, snd(xy)))"
  1042 apply (induct_tac "ys")
  1043  apply auto
  1044 apply (erule_tac a = xs in list.cases)
  1045 apply (auto elim: natE)
  1046 done
  1047 
  1048 lemma set_update_subset_cons [rule_format]:
  1049   "xs:list(A) ==> 
  1050    \<forall>i \<in> nat. set_of_list(list_update(xs, i, x)) <= cons(x, set_of_list(xs))"
  1051 apply (induct_tac "xs")
  1052  apply simp
  1053 apply (rule ballI)
  1054 apply (erule natE, simp_all, auto)
  1055 done
  1056 
  1057 lemma set_of_list_update_subsetI:
  1058      "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|]
  1059    ==> set_of_list(list_update(xs, i,x)) <= A"
  1060 apply (rule subset_trans)
  1061 apply (rule set_update_subset_cons, auto)
  1062 done
  1063 
  1064 (** upt **)
  1065 
  1066 lemma upt_rec:
  1067      "j:nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)"
  1068 apply (induct_tac "j", auto)
  1069 apply (drule not_lt_imp_le)
  1070 apply (auto simp: lt_Ord intro: le_anti_sym)
  1071 done
  1072 
  1073 lemma upt_conv_Nil [simp]: "[| j le i; j:nat |] ==> upt(i,j) = Nil"
  1074 apply (subst upt_rec, auto)
  1075 apply (auto simp add: le_iff)
  1076 apply (drule lt_asym [THEN notE], auto)
  1077 done
  1078 
  1079 (*Only needed if upt_Suc is deleted from the simpset*)
  1080 lemma upt_succ_append:
  1081      "[| i le j; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]"
  1082 by simp
  1083 
  1084 lemma upt_conv_Cons:
  1085      "[| i<j; j:nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))"
  1086 apply (rule trans)
  1087 apply (rule upt_rec, auto)
  1088 done
  1089 
  1090 lemma upt_type [simp,TC]: "j:nat ==> upt(i,j):list(nat)"
  1091 by (induct_tac "j", auto)
  1092 
  1093 (*LOOPS as a simprule, since j<=j*)
  1094 lemma upt_add_eq_append:
  1095      "[| i le j; j:nat; k:nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"
  1096 apply (induct_tac "k")
  1097 apply (auto simp add: app_assoc app_type)
  1098 apply (rule_tac j = j in le_trans, auto)
  1099 done
  1100 
  1101 lemma length_upt [simp]: "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i"
  1102 apply (induct_tac "j")
  1103 apply (rule_tac [2] sym)
  1104 apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
  1105 done
  1106 
  1107 lemma nth_upt [rule_format,simp]:
  1108      "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k"
  1109 apply (induct_tac "j", simp)
  1110 apply (simp add: nth_append le_iff)
  1111 apply (auto dest!: not_lt_imp_le 
  1112             simp add: nth_append less_diff_conv add_commute)
  1113 done
  1114 
  1115 lemma take_upt [rule_format,simp]:
  1116      "[| m:nat; n:nat |] ==>
  1117          \<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
  1118 apply (induct_tac "m")
  1119 apply (simp (no_asm_simp) add: take_0)
  1120 apply clarify
  1121 apply (subst upt_rec, simp) 
  1122 apply (rule sym)
  1123 apply (subst upt_rec, simp) 
  1124 apply (simp_all del: upt.simps)
  1125 apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
  1126 apply auto
  1127 done
  1128 
  1129 lemma map_succ_upt:
  1130      "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
  1131 apply (induct_tac "n")
  1132 apply (auto simp add: map_app_distrib)
  1133 done
  1134 
  1135 lemma nth_map [rule_format,simp]:
  1136      "xs:list(A) ==>
  1137       \<forall>n \<in> nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))"
  1138 apply (induct_tac "xs", simp)
  1139 apply (rule ballI)
  1140 apply (induct_tac "n", auto)
  1141 done
  1142 
  1143 lemma nth_map_upt [rule_format]:
  1144      "[| m:nat; n:nat |] ==>
  1145       \<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
  1146 apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp) 
  1147 apply (subst map_succ_upt [symmetric], simp_all, clarify) 
  1148 apply (subgoal_tac "i < length (upt (0, x))")
  1149  prefer 2 
  1150  apply (simp add: less_diff_conv) 
  1151  apply (rule_tac j = "succ (i #+ y) " in lt_trans2)
  1152   apply simp 
  1153  apply simp 
  1154 apply (subgoal_tac "i < length (upt (y, x))")
  1155  apply (simp_all add: add_commute less_diff_conv)
  1156 done
  1157 
  1158 (** sublist (a generalization of nth to sets) **)
  1159 
  1160 constdefs
  1161   sublist :: "[i, i] => i"
  1162     "sublist(xs, A)==
  1163      map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
  1164 
  1165 lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil"
  1166 by (unfold sublist_def, auto)
  1167 
  1168 lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil"
  1169 by (unfold sublist_def, auto)
  1170 
  1171 lemma sublist_shift_lemma:
  1172  "[| xs:list(B); i:nat |] ==>
  1173   map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
  1174   map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))"
  1175 apply (erule list_append_induct)
  1176 apply (simp (no_asm_simp))
  1177 apply (auto simp add: add_commute length_app filter_append map_app_distrib)
  1178 done
  1179 
  1180 lemma sublist_type [simp,TC]:
  1181      "xs:list(B) ==> sublist(xs, A):list(B)"
  1182 apply (unfold sublist_def)
  1183 apply (induct_tac "xs")
  1184 apply (auto simp add: filter_append map_app_distrib)
  1185 done
  1186 
  1187 lemma upt_add_eq_append2:
  1188      "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)"
  1189 by (simp add: upt_add_eq_append [of 0] nat_0_le)
  1190 
  1191 lemma sublist_append:
  1192  "[| xs:list(B); ys:list(B)  |] ==>
  1193   sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})"
  1194 apply (unfold sublist_def)
  1195 apply (erule_tac l = ys in list_append_induct, simp)
  1196 apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
  1197 apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
  1198 apply (simp_all add: add_commute)
  1199 done
  1200 
  1201 
  1202 lemma sublist_Cons:
  1203      "[| xs:list(B); x:B |] ==>
  1204       sublist(Cons(x, xs), A) = 
  1205       (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})"
  1206 apply (erule_tac l = xs in list_append_induct)
  1207 apply (simp (no_asm_simp) add: sublist_def)  
  1208 apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp) 
  1209 done
  1210 
  1211 lemma sublist_singleton [simp]:
  1212      "sublist([x], A) = (if 0 : A then [x] else [])"
  1213 by (simp add: sublist_Cons)
  1214 
  1215 lemma sublist_upt_eq_take [rule_format, simp]:
  1216     "xs:list(A) ==> ALL n:nat. sublist(xs,n) = take(n,xs)"
  1217 apply (erule list.induct, simp) 
  1218 apply (clarify ); 
  1219 apply (erule natE) 
  1220 apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
  1221 done
  1222 
  1223 lemma sublist_Int_eq:
  1224      "xs : list(B) ==> sublist(xs, A \<inter> nat) = sublist(xs, A)"
  1225 apply (erule list.induct)
  1226 apply (simp_all add: sublist_Cons) 
  1227 done
  1228 
  1229 text{*Repetition of a List Element*}
  1230 
  1231 consts   repeat :: "[i,i]=>i"
  1232 primrec
  1233   "repeat(a,0) = []"
  1234 
  1235   "repeat(a,succ(n)) = Cons(a,repeat(a,n))"
  1236 
  1237 lemma length_repeat: "n \<in> nat ==> length(repeat(a,n)) = n"
  1238 by (induct_tac n, auto)
  1239 
  1240 lemma repeat_succ_app: "n \<in> nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
  1241 apply (induct_tac n)
  1242 apply (simp_all del: app_Cons add: app_Cons [symmetric])
  1243 done
  1244 
  1245 lemma repeat_type [TC]: "[|a \<in> A; n \<in> nat|] ==> repeat(a,n) \<in> list(A)"
  1246 by (induct_tac n, auto)
  1247 
  1248 
  1249 ML
  1250 {*
  1251 val ConsE = thm "ConsE";
  1252 val Cons_iff = thm "Cons_iff";
  1253 val Nil_Cons_iff = thm "Nil_Cons_iff";
  1254 val list_unfold = thm "list_unfold";
  1255 val list_mono = thm "list_mono";
  1256 val list_univ = thm "list_univ";
  1257 val list_subset_univ = thm "list_subset_univ";
  1258 val list_into_univ = thm "list_into_univ";
  1259 val list_case_type = thm "list_case_type";
  1260 val tl_type = thm "tl_type";
  1261 val drop_Nil = thm "drop_Nil";
  1262 val drop_succ_Cons = thm "drop_succ_Cons";
  1263 val drop_type = thm "drop_type";
  1264 val list_rec_type = thm "list_rec_type";
  1265 val map_type = thm "map_type";
  1266 val map_type2 = thm "map_type2";
  1267 val length_type = thm "length_type";
  1268 val lt_length_in_nat = thm "lt_length_in_nat";
  1269 val app_type = thm "app_type";
  1270 val rev_type = thm "rev_type";
  1271 val flat_type = thm "flat_type";
  1272 val set_of_list_type = thm "set_of_list_type";
  1273 val set_of_list_append = thm "set_of_list_append";
  1274 val list_add_type = thm "list_add_type";
  1275 val map_ident = thm "map_ident";
  1276 val map_compose = thm "map_compose";
  1277 val map_app_distrib = thm "map_app_distrib";
  1278 val map_flat = thm "map_flat";
  1279 val list_rec_map = thm "list_rec_map";
  1280 val list_CollectD = thm "list_CollectD";
  1281 val map_list_Collect = thm "map_list_Collect";
  1282 val length_map = thm "length_map";
  1283 val length_app = thm "length_app";
  1284 val length_rev = thm "length_rev";
  1285 val length_flat = thm "length_flat";
  1286 val drop_length_Cons = thm "drop_length_Cons";
  1287 val drop_length = thm "drop_length";
  1288 val app_right_Nil = thm "app_right_Nil";
  1289 val app_assoc = thm "app_assoc";
  1290 val flat_app_distrib = thm "flat_app_distrib";
  1291 val rev_map_distrib = thm "rev_map_distrib";
  1292 val rev_app_distrib = thm "rev_app_distrib";
  1293 val rev_rev_ident = thm "rev_rev_ident";
  1294 val rev_flat = thm "rev_flat";
  1295 val list_add_app = thm "list_add_app";
  1296 val list_add_rev = thm "list_add_rev";
  1297 val list_add_flat = thm "list_add_flat";
  1298 val list_append_induct = thm "list_append_induct";
  1299 val min_sym = thm "min_sym";
  1300 val min_type = thm "min_type";
  1301 val min_0 = thm "min_0";
  1302 val min_02 = thm "min_02";
  1303 val lt_min_iff = thm "lt_min_iff";
  1304 val min_succ_succ = thm "min_succ_succ";
  1305 val filter_append = thm "filter_append";
  1306 val filter_type = thm "filter_type";
  1307 val length_filter = thm "length_filter";
  1308 val filter_is_subset = thm "filter_is_subset";
  1309 val filter_False = thm "filter_False";
  1310 val filter_True = thm "filter_True";
  1311 val length_is_0_iff = thm "length_is_0_iff";
  1312 val length_is_0_iff2 = thm "length_is_0_iff2";
  1313 val length_tl = thm "length_tl";
  1314 val length_greater_0_iff = thm "length_greater_0_iff";
  1315 val length_succ_iff = thm "length_succ_iff";
  1316 val append_is_Nil_iff = thm "append_is_Nil_iff";
  1317 val append_is_Nil_iff2 = thm "append_is_Nil_iff2";
  1318 val append_left_is_self_iff = thm "append_left_is_self_iff";
  1319 val append_left_is_self_iff2 = thm "append_left_is_self_iff2";
  1320 val append_left_is_Nil_iff = thm "append_left_is_Nil_iff";
  1321 val append_left_is_Nil_iff2 = thm "append_left_is_Nil_iff2";
  1322 val append_eq_append_iff = thm "append_eq_append_iff";
  1323 val append_eq_append = thm "append_eq_append";
  1324 val append_eq_append_iff2 = thm "append_eq_append_iff2";
  1325 val append_self_iff = thm "append_self_iff";
  1326 val append_self_iff2 = thm "append_self_iff2";
  1327 val append1_eq_iff = thm "append1_eq_iff";
  1328 val append_right_is_self_iff = thm "append_right_is_self_iff";
  1329 val append_right_is_self_iff2 = thm "append_right_is_self_iff2";
  1330 val hd_append = thm "hd_append";
  1331 val tl_append = thm "tl_append";
  1332 val rev_is_Nil_iff = thm "rev_is_Nil_iff";
  1333 val Nil_is_rev_iff = thm "Nil_is_rev_iff";
  1334 val rev_is_rev_iff = thm "rev_is_rev_iff";
  1335 val rev_list_elim = thm "rev_list_elim";
  1336 val length_drop = thm "length_drop";
  1337 val drop_all = thm "drop_all";
  1338 val drop_append = thm "drop_append";
  1339 val drop_drop = thm "drop_drop";
  1340 val take_0 = thm "take_0";
  1341 val take_succ_Cons = thm "take_succ_Cons";
  1342 val take_Nil = thm "take_Nil";
  1343 val take_all = thm "take_all";
  1344 val take_type = thm "take_type";
  1345 val take_append = thm "take_append";
  1346 val take_take = thm "take_take";
  1347 val take_add = thm "take_add";
  1348 val take_succ = thm "take_succ";
  1349 val nth_0 = thm "nth_0";
  1350 val nth_Cons = thm "nth_Cons";
  1351 val nth_type = thm "nth_type";
  1352 val nth_append = thm "nth_append";
  1353 val set_of_list_conv_nth = thm "set_of_list_conv_nth";
  1354 val nth_take_lemma = thm "nth_take_lemma";
  1355 val nth_equalityI = thm "nth_equalityI";
  1356 val take_equalityI = thm "take_equalityI";
  1357 val nth_drop = thm "nth_drop";
  1358 val list_on_set_of_list = thm "list_on_set_of_list";
  1359 val zip_Nil = thm "zip_Nil";
  1360 val zip_Nil2 = thm "zip_Nil2";
  1361 val zip_Cons_Cons = thm "zip_Cons_Cons";
  1362 val zip_type = thm "zip_type";
  1363 val length_zip = thm "length_zip";
  1364 val zip_append1 = thm "zip_append1";
  1365 val zip_append2 = thm "zip_append2";
  1366 val zip_append = thm "zip_append";
  1367 val zip_rev = thm "zip_rev";
  1368 val nth_zip = thm "nth_zip";
  1369 val set_of_list_zip = thm "set_of_list_zip";
  1370 val list_update_Nil = thm "list_update_Nil";
  1371 val list_update_Cons_0 = thm "list_update_Cons_0";
  1372 val list_update_Cons_succ = thm "list_update_Cons_succ";
  1373 val list_update_type = thm "list_update_type";
  1374 val length_list_update = thm "length_list_update";
  1375 val nth_list_update = thm "nth_list_update";
  1376 val nth_list_update_eq = thm "nth_list_update_eq";
  1377 val nth_list_update_neq = thm "nth_list_update_neq";
  1378 val list_update_overwrite = thm "list_update_overwrite";
  1379 val list_update_same_conv = thm "list_update_same_conv";
  1380 val update_zip = thm "update_zip";
  1381 val set_update_subset_cons = thm "set_update_subset_cons";
  1382 val set_of_list_update_subsetI = thm "set_of_list_update_subsetI";
  1383 val upt_rec = thm "upt_rec";
  1384 val upt_conv_Nil = thm "upt_conv_Nil";
  1385 val upt_succ_append = thm "upt_succ_append";
  1386 val upt_conv_Cons = thm "upt_conv_Cons";
  1387 val upt_type = thm "upt_type";
  1388 val upt_add_eq_append = thm "upt_add_eq_append";
  1389 val length_upt = thm "length_upt";
  1390 val nth_upt = thm "nth_upt";
  1391 val take_upt = thm "take_upt";
  1392 val map_succ_upt = thm "map_succ_upt";
  1393 val nth_map = thm "nth_map";
  1394 val nth_map_upt = thm "nth_map_upt";
  1395 val sublist_0 = thm "sublist_0";
  1396 val sublist_Nil = thm "sublist_Nil";
  1397 val sublist_shift_lemma = thm "sublist_shift_lemma";
  1398 val sublist_type = thm "sublist_type";
  1399 val upt_add_eq_append2 = thm "upt_add_eq_append2";
  1400 val sublist_append = thm "sublist_append";
  1401 val sublist_Cons = thm "sublist_Cons";
  1402 val sublist_singleton = thm "sublist_singleton";
  1403 val sublist_upt_eq_take = thm "sublist_upt_eq_take";
  1404 val sublist_Int_eq = thm "sublist_Int_eq";
  1405 
  1406 structure list =
  1407 struct
  1408 val induct = thm "list.induct"
  1409 val elim   = thm "list.cases"
  1410 val intrs  = thms "list.intros"
  1411 end;  
  1412 *}
  1413 
  1414 end