# Theory List

Up to index of Isabelle/ZF

theory List
imports Datatype ArithSimp
begin

    (*  Title:      ZF/List
        ID:         $Id: List.thy,v 1.31 2005/06/17 14:15:09 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge

    *)

    header{*Lists in Zermelo-Fraenkel Set Theory*}

    theory List imports Datatype ArithSimp begin

    consts
      list       :: "i=>i"

    datatype
      "list(A)" = Nil | Cons ("a:A", "l: list(A)")

    syntax
     "[]"        :: i                                       ("[]")
     "@List"     :: "is => i"                                 ("[(_)]")

    translations
      "[x, xs]"     == "Cons(x, [xs])"
      "[x]"         == "Cons(x, [])"
      "[]"          == "Nil"

    consts
      length :: "i=>i"
      hd     :: "i=>i"
      tl     :: "i=>i"

    primrec
      "length([]) = 0"
      "length(Cons(a,l)) = succ(length(l))"

    primrec
      "hd([]) = 0"
      "hd(Cons(a,l)) = a"

    primrec
      "tl([]) = []"
      "tl(Cons(a,l)) = l"

    consts
      map         :: "[i=>i, i] => i"
      set_of_list :: "i=>i"
      app         :: "[i,i]=>i"                        (infixr "@" 60)

    (*map is a binding operator -- it applies to meta-level functions, not
    object-level functions.  This simplifies the final form of term_rec_conv,
    although complicating its derivation.*)
    primrec
      "map(f,[]) = []"
      "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"

    primrec
      "set_of_list([]) = 0"
      "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"

    primrec
      app_Nil:  "[] @ ys = ys"
      app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"

    consts
      rev :: "i=>i"
      flat       :: "i=>i"
      list_add   :: "i=>i"

    primrec
      "rev([]) = []"
      "rev(Cons(a,l)) = rev(l) @ [a]"

    primrec
      "flat([]) = []"
      "flat(Cons(l,ls)) = l @ flat(ls)"

    primrec
      "list_add([]) = 0"
      "list_add(Cons(a,l)) = a #+ list_add(l)"

    consts
      drop       :: "[i,i]=>i"

    primrec
      drop_0:    "drop(0,l) = l"
      drop_succ: "drop(succ(i), l) = tl (drop(i,l))"

    (*** Thanks to Sidi Ehmety for the following ***)

    constdefs
    (* Function `take' returns the first n elements of a list *)
      take     :: "[i,i]=>i"
      "take(n, as) == list_rec(lam n:nat. [],
                    %a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"

      nth :: "[i, i]=>i"
      --{*returns the (n+1)th element of a list, or 0 if the
       list is too short.*}
      "nth(n, as) == list_rec(lam n:nat. 0,
                              %a l r. lam n:nat. nat_case(a, %m. r`m, n), as) ` n"

      list_update :: "[i, i, i]=>i"
      "list_update(xs, i, v) == list_rec(lam n:nat. Nil,
          %u us vs. lam n:nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"

    consts
      filter :: "[i=>o, i] => i"
      upt :: "[i, i] =>i"

    primrec
      "filter(P, Nil) = Nil"
      "filter(P, Cons(x, xs)) =
         (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"

    primrec
      "upt(i, 0) = Nil"
      "upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)"

    constdefs
      min :: "[i,i] =>i"
        "min(x, y) == (if x le y then x else y)"

      max :: "[i, i] =>i"
        "max(x, y) == (if x le y then y else x)"

    (*** Aspects of the datatype definition ***)

    declare list.intros [simp,TC]

    (*An elimination rule, for type-checking*)
    inductive_cases ConsE: "Cons(a,l) : list(A)"

    lemma Cons_type_iff [simp]: "Cons(a,l) ∈ list(A) <-> a ∈ A & l ∈ list(A)"
    by (blast elim: ConsE)

    (*Proving freeness results*)
    lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
    by auto

    lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
    by auto

    lemma list_unfold: "list(A) = {0} + (A * list(A))"
    by (blast intro!: list.intros [unfolded list.con_defs]
              elim: list.cases [unfolded list.con_defs])

    (**  Lemmas to justify using "list" in other recursive type definitions **)

    lemma list_mono: "A<=B ==> list(A) <= list(B)"
    apply (unfold list.defs )
    apply (rule lfp_mono)
    apply (simp_all add: list.bnd_mono)
    apply (assumption | rule univ_mono basic_monos)+
    done

    (*There is a similar proof by list induction.*)
    lemma list_univ: "list(univ(A)) <= univ(A)"
    apply (unfold list.defs list.con_defs)
    apply (rule lfp_lowerbound)
    apply (rule_tac [2] A_subset_univ [THEN univ_mono])
    apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
    done

    (*These two theorems justify datatypes involving list(nat), list(A), ...*)
    lemmas list_subset_univ = subset_trans [OF list_mono list_univ]

    lemma list_into_univ: "[| l: list(A);  A <= univ(B) |] ==> l: univ(B)"
    by (blast intro: list_subset_univ [THEN subsetD])

    lemma list_case_type:
        "[| l: list(A);
            c: C(Nil);
            !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))
         |] ==> list_case(c,h,l) : C(l)"
    by (erule list.induct, auto)

    lemma list_0_triv: "list(0) = {Nil}"
    apply (rule equalityI, auto)
    apply (induct_tac x, auto)
    done

    (*** List functions ***)

    lemma tl_type: "l: list(A) ==> tl(l) : list(A)"
    apply (induct_tac "l")
    apply (simp_all (no_asm_simp) add: list.intros)
    done

    (** drop **)

    lemma drop_Nil [simp]: "i:nat ==> drop(i, Nil) = Nil"
    apply (induct_tac "i")
    apply (simp_all (no_asm_simp))
    done

    lemma drop_succ_Cons [simp]: "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"
    apply (rule sym)
    apply (induct_tac "i")
    apply (simp (no_asm))
    apply (simp (no_asm_simp))
    done

    lemma drop_type [simp,TC]: "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"
    apply (induct_tac "i")
    apply (simp_all (no_asm_simp) add: tl_type)
    done

    declare drop_succ [simp del]

    (** Type checking -- proved by induction, as usual **)

    lemma list_rec_type [TC]:
        "[| l: list(A);
            c: C(Nil);
            !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))
         |] ==> list_rec(c,h,l) : C(l)"
    by (induct_tac "l", auto)

    (** map **)

    lemma map_type [TC]:
        "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"
    apply (simp add: map_list_def)
    apply (typecheck add: list.intros list_rec_type, blast)
    done

    lemma map_type2 [TC]: "l: list(A) ==> map(h,l) : list({h(u). u:A})"
    apply (erule map_type)
    apply (erule RepFunI)
    done

    (** length **)

    lemma length_type [TC]: "l: list(A) ==> length(l) : nat"
    by (simp add: length_list_def)

    lemma lt_length_in_nat:
       "[|x < length(xs); xs ∈ list(A)|] ==> x ∈ nat"
    by (frule lt_nat_in_nat, typecheck)

    (** app **)

    lemma app_type [TC]: "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)"
    by (simp add: app_list_def)

    (** rev **)

    lemma rev_type [TC]: "xs: list(A) ==> rev(xs) : list(A)"
    by (simp add: rev_list_def)

    (** flat **)

    lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) : list(A)"
    by (simp add: flat_list_def)

    (** set_of_list **)

    lemma set_of_list_type [TC]: "l: list(A) ==> set_of_list(l) : Pow(A)"
    apply (unfold set_of_list_list_def)
    apply (erule list_rec_type, auto)
    done

    lemma set_of_list_append:
         "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)"
    apply (erule list.induct)
    apply (simp_all (no_asm_simp) add: Un_cons)
    done

    (** list_add **)

    lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) : nat"
    by (simp add: list_add_list_def)

    (*** theorems about map ***)

    lemma map_ident [simp]: "l: list(A) ==> map(%u. u, l) = l"
    apply (induct_tac "l")
    apply (simp_all (no_asm_simp))
    done

    lemma map_compose: "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"
    apply (induct_tac "l")
    apply (simp_all (no_asm_simp))
    done

    lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"
    apply (induct_tac "xs")
    apply (simp_all (no_asm_simp))
    done

    lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"
    apply (induct_tac "ls")
    apply (simp_all (no_asm_simp) add: map_app_distrib)
    done

    lemma list_rec_map:
         "l: list(A) ==>
          list_rec(c, d, map(h,l)) =
          list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"
    apply (induct_tac "l")
    apply (simp_all (no_asm_simp))
    done

    (** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)

    (* c : list(Collect(B,P)) ==> c : list(B) *)
    lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard]

    lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
    apply (induct_tac "l")
    apply (simp_all (no_asm_simp))
    done

    (*** theorems about length ***)

    lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
    by (induct_tac "xs", simp_all)

    lemma length_app [simp]:
         "[| xs: list(A); ys: list(A) |]
          ==> length(xs@ys) = length(xs) #+ length(ys)"
    by (induct_tac "xs", simp_all)

    lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
    apply (induct_tac "xs")
    apply (simp_all (no_asm_simp) add: length_app)
    done

    lemma length_flat:
         "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"
    apply (induct_tac "ls")
    apply (simp_all (no_asm_simp) add: length_app)
    done

    (** Length and drop **)

    (*Lemma for the inductive step of drop_length*)
    lemma drop_length_Cons [rule_format]:
         "xs: list(A) ==>
               ∀x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
    by (erule list.induct, simp_all)

    lemma drop_length [rule_format]:
         "l: list(A) ==> ∀i ∈ length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
    apply (erule list.induct, simp_all, safe)
    apply (erule drop_length_Cons)
    apply (rule natE)
    apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption, simp_all)
    apply (blast intro: succ_in_naturalD length_type)
    done

    (*** theorems about app ***)

    lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
    by (erule list.induct, simp_all)

    lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
    by (induct_tac "xs", simp_all)

    lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"
    apply (induct_tac "ls")
    apply (simp_all (no_asm_simp) add: app_assoc)
    done

    (*** theorems about rev ***)

    lemma rev_map_distrib: "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"
    apply (induct_tac "l")
    apply (simp_all (no_asm_simp) add: map_app_distrib)
    done

    (*Simplifier needs the premises as assumptions because rewriting will not
      instantiate the variable ?A in the rules' typing conditions; note that
      rev_type does not instantiate ?A.  Only the premises do.
    *)
    lemma rev_app_distrib:
         "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"
    apply (erule list.induct)
    apply (simp_all add: app_assoc)
    done

    lemma rev_rev_ident [simp]: "l: list(A) ==> rev(rev(l))=l"
    apply (induct_tac "l")
    apply (simp_all (no_asm_simp) add: rev_app_distrib)
    done

    lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"
    apply (induct_tac "ls")
    apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib)
    done

    (*** theorems about list_add ***)

    lemma list_add_app:
         "[| xs: list(nat);  ys: list(nat) |]
          ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
    apply (induct_tac "xs", simp_all)
    done

    lemma list_add_rev: "l: list(nat) ==> list_add(rev(l)) = list_add(l)"
    apply (induct_tac "l")
    apply (simp_all (no_asm_simp) add: list_add_app)
    done

    lemma list_add_flat:
         "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"
    apply (induct_tac "ls")
    apply (simp_all (no_asm_simp) add: list_add_app)
    done

    (** New induction rules **)

    lemma list_append_induct [case_names Nil snoc, consumes 1]:
        "[| l: list(A);
            P(Nil);
            !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x])
         |] ==> P(l)"
    apply (subgoal_tac "P(rev(rev(l)))", simp)
    apply (erule rev_type [THEN list.induct], simp_all)
    done

    lemma list_complete_induct_lemma [rule_format]:
     assumes ih:
        "!!l. [| l ∈ list(A);
                 ∀l' ∈ list(A). length(l') < length(l) --> P(l')|]
              ==> P(l)"
      shows "n ∈ nat ==> ∀l ∈ list(A). length(l) < n --> P(l)"
    apply (induct_tac n, simp)
    apply (blast intro: ih elim!: leE)
    done

    theorem list_complete_induct:
          "[| l ∈ list(A);
              !!l. [| l ∈ list(A);
                      ∀l' ∈ list(A). length(l') < length(l) --> P(l')|]
                   ==> P(l)
           |] ==> P(l)"
    apply (rule list_complete_induct_lemma [of A])
       prefer 4 apply (rule le_refl, simp)
      apply blast
     apply simp
    apply assumption
    done

    (*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)

    (** min FIXME: replace by Int! **)
    (* Min theorems are also true for i, j ordinals *)
    lemma min_sym: "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)"
    apply (unfold min_def)
    apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
    done

    lemma min_type [simp,TC]: "[| i:nat; j:nat |] ==> min(i,j):nat"
    by (unfold min_def, auto)

    lemma min_0 [simp]: "i:nat ==> min(0,i) = 0"
    apply (unfold min_def)
    apply (auto dest: not_lt_imp_le)
    done

    lemma min_02 [simp]: "i:nat ==> min(i, 0) = 0"
    apply (unfold min_def)
    apply (auto dest: not_lt_imp_le)
    done

    lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k"
    apply (unfold min_def)
    apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
    done

    lemma min_succ_succ [simp]:
         "[| i:nat; j:nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))"
    apply (unfold min_def, auto)
    done

    (*** more theorems about lists ***)

    (** filter **)

    lemma filter_append [simp]:
         "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)"
    by (induct_tac "xs", auto)

    lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)"
    by (induct_tac "xs", auto)

    lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) le length(xs)"
    apply (induct_tac "xs", auto)
    apply (rule_tac j = "length (l) " in le_trans)
    apply (auto simp add: le_iff)
    done

    lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)"
    by (induct_tac "xs", auto)

    lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil"
    by (induct_tac "xs", auto)

    lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs"
    by (induct_tac "xs", auto)

    (** length **)

    lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil"
    by (erule list.induct, auto)

    lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil"
    by (erule list.induct, auto)

    lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
    by (erule list.induct, auto)

    lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil"
    by (erule list.induct, auto)

    lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)"
    by (erule list.induct, auto)

    (** more theorems about append **)

    lemma append_is_Nil_iff [simp]:
         "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)"
    by (erule list.induct, auto)

    lemma append_is_Nil_iff2 [simp]:
         "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)"
    by (erule list.induct, auto)

    lemma append_left_is_self_iff [simp]:
         "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)"
    by (erule list.induct, auto)

    lemma append_left_is_self_iff2 [simp]:
         "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)"
    by (erule list.induct, auto)

    (*TOO SLOW as a default simprule!*)
    lemma append_left_is_Nil_iff [rule_format]:
         "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
       length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))"
    apply (erule list.induct)
    apply (auto simp add: length_app)
    done

    (*TOO SLOW as a default simprule!*)
    lemma append_left_is_Nil_iff2 [rule_format]:
         "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
       length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))"
    apply (erule list.induct)
    apply (auto simp add: length_app)
    done

    lemma append_eq_append_iff [rule_format,simp]:
         "xs:list(A) ==> ∀ys ∈ list(A).
          length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)"
    apply (erule list.induct)
    apply (simp (no_asm_simp))
    apply clarify
    apply (erule_tac a = ys in list.cases, auto)
    done

    lemma append_eq_append [rule_format]:
      "xs:list(A) ==>
       ∀ys ∈ list(A). ∀us ∈ list(A). ∀vs ∈ list(A).
       length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)"
    apply (induct_tac "xs")
    apply (force simp add: length_app, clarify)
    apply (erule_tac a = ys in list.cases, simp)
    apply (subgoal_tac "Cons (a, l) @ us =vs")
     apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all, blast)
    done

    lemma append_eq_append_iff2 [simp]:
     "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
      ==>  xs@us = ys@vs <-> (xs=ys & us=vs)"
    apply (rule iffI)
    apply (rule append_eq_append, auto)
    done

    lemma append_self_iff [simp]:
         "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
    by simp

    lemma append_self_iff2 [simp]:
         "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
    by simp

    (* Can also be proved from append_eq_append_iff2,
    but the proof requires two more hypotheses: x:A and y:A *)
    lemma append1_eq_iff [rule_format,simp]:
         "xs:list(A) ==> ∀ys ∈ list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
    apply (erule list.induct)
     apply clarify
     apply (erule list.cases)
     apply simp_all
    txt{*Inductive step*}
    apply clarify
    apply (erule_tac a=ys in list.cases, simp_all)
    done

    lemma append_right_is_self_iff [simp]:
         "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
    by (simp (no_asm_simp) add: append_left_is_Nil_iff)

    lemma append_right_is_self_iff2 [simp]:
         "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
    apply (rule iffI)
    apply (drule sym, auto)
    done

    lemma hd_append [rule_format,simp]:
         "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)"
    by (induct_tac "xs", auto)

    lemma tl_append [rule_format,simp]:
         "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys"
    by (induct_tac "xs", auto)

    (** rev **)
    lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)"
    by (erule list.induct, auto)

    lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)"
    by (erule list.induct, auto)

    lemma rev_is_rev_iff [rule_format,simp]:
         "xs:list(A) ==> ∀ys ∈ list(A). rev(xs)=rev(ys) <-> xs=ys"
    apply (erule list.induct, force, clarify)
    apply (erule_tac a = ys in list.cases, auto)
    done

    lemma rev_list_elim [rule_format]:
         "xs:list(A) ==>
          (xs=Nil --> P) --> (∀ys ∈ list(A). ∀y ∈ A. xs =ys@[y] -->P)-->P"
    by (erule list_append_induct, auto)

    (** more theorems about drop **)

    lemma length_drop [rule_format,simp]:
         "n:nat ==> ∀xs ∈ list(A). length(drop(n, xs)) = length(xs) #- n"
    apply (erule nat_induct)
    apply (auto elim: list.cases)
    done

    lemma drop_all [rule_format,simp]:
         "n:nat ==> ∀xs ∈ list(A). length(xs) le n --> drop(n, xs)=Nil"
    apply (erule nat_induct)
    apply (auto elim: list.cases)
    done

    lemma drop_append [rule_format]:
         "n:nat ==>
          ∀xs ∈ list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
    apply (induct_tac "n")
    apply (auto elim: list.cases)
    done

    lemma drop_drop:
        "m:nat ==> ∀xs ∈ list(A). ∀n ∈ nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
    apply (induct_tac "m")
    apply (auto elim: list.cases)
    done

    (** take **)

    lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) =  Nil"
    apply (unfold take_def)
    apply (erule list.induct, auto)
    done

    lemma take_succ_Cons [simp]:
        "n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))"
    by (simp add: take_def)

    (* Needed for proving take_all *)
    lemma take_Nil [simp]: "n:nat ==> take(n, Nil) = Nil"
    by (unfold take_def, auto)

    lemma take_all [rule_format,simp]:
         "n:nat ==> ∀xs ∈ list(A). length(xs) le n  --> take(n, xs) = xs"
    apply (erule nat_induct)
    apply (auto elim: list.cases)
    done

    lemma take_type [rule_format,simp,TC]:
         "xs:list(A) ==> ∀n ∈ nat. take(n, xs):list(A)"
    apply (erule list.induct, simp, clarify)
    apply (erule natE, auto)
    done

    lemma take_append [rule_format,simp]:
     "xs:list(A) ==>
      ∀ys ∈ list(A). ∀n ∈ nat. take(n, xs @ ys) =
                                take(n, xs) @ take(n #- length(xs), ys)"
    apply (erule list.induct, simp, clarify)
    apply (erule natE, auto)
    done

    lemma take_take [rule_format]:
       "m : nat ==>
        ∀xs ∈ list(A). ∀n ∈ nat. take(n, take(m,xs))= take(min(n, m), xs)"
    apply (induct_tac "m", auto)
    apply (erule_tac a = xs in list.cases)
    apply (auto simp add: take_Nil)
    apply (erule_tac n=n in natE)
    apply (auto intro: take_0 take_type)
    done

    (** nth **)

    lemma nth_0 [simp]: "nth(0, Cons(a, l)) = a"
    by (simp add: nth_def)

    lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a,l)) = nth(n,l)"
    by (simp add: nth_def)

    lemma nth_empty [simp]: "nth(n, Nil) = 0"
    by (simp add: nth_def)

    lemma nth_type [rule_format,simp,TC]:
         "xs:list(A) ==> ∀n. n < length(xs) --> nth(n,xs) : A"
    apply (erule list.induct, simp, clarify)
    apply (subgoal_tac "n ∈ nat")
     apply (erule natE, auto dest!: le_in_nat)
    done

    lemma nth_eq_0 [rule_format]:
         "xs:list(A) ==> ∀n ∈ nat. length(xs) le n --> nth(n,xs) = 0"
    apply (erule list.induct, simp, clarify)
    apply (erule natE, auto)
    done

    lemma nth_append [rule_format]:
      "xs:list(A) ==>
       ∀n ∈ nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
                                    else nth(n #- length(xs), ys))"
    apply (induct_tac "xs", simp, clarify)
    apply (erule natE, auto)
    done

    lemma set_of_list_conv_nth:
        "xs:list(A)
         ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x = nth(i,xs)}"
    apply (induct_tac "xs", simp_all)
    apply (rule equalityI, auto)
    apply (rule_tac x = 0 in bexI, auto)
    apply (erule natE, auto)
    done

    (* Other theorems about lists *)

    lemma nth_take_lemma [rule_format]:
     "k:nat ==>
      ∀xs ∈ list(A). (∀ys ∈ list(A). k le length(xs) --> k le length(ys) -->
          (∀i ∈ nat. i<k --> nth(i,xs) = nth(i,ys))--> take(k,xs) = take(k,ys))"
    apply (induct_tac "k")
    apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
    apply clarify
    (*Both lists are non-empty*)
    apply (erule_tac a=xs in list.cases, simp)
    apply (erule_tac a=ys in list.cases, clarify)
    apply (simp (no_asm_use) )
    apply clarify
    apply (simp (no_asm_simp))
    apply (rule conjI, force)
    apply (rename_tac y ys z zs)
    apply (drule_tac x = zs and x1 = ys in bspec [THEN bspec], auto)
    done

    lemma nth_equalityI [rule_format]:
         "[| xs:list(A); ys:list(A); length(xs) = length(ys);
             ∀i ∈ nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |]
          ==> xs = ys"
    apply (subgoal_tac "length (xs) le length (ys) ")
    apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma)
    apply (simp_all add: take_all)
    done

    (*The famous take-lemma*)

    lemma take_equalityI [rule_format]:
        "[| xs:list(A); ys:list(A); (∀i ∈ nat. take(i, xs) = take(i,ys)) |]
         ==> xs = ys"
    apply (case_tac "length (xs) le length (ys) ")
    apply (drule_tac x = "length (ys) " in bspec)
    apply (drule_tac [3] not_lt_imp_le)
    apply (subgoal_tac [5] "length (ys) le length (xs) ")
    apply (rule_tac [6] j = "succ (length (ys))" in le_trans)
    apply (rule_tac [6] leI)
    apply (drule_tac [5] x = "length (xs) " in bspec)
    apply (simp_all add: take_all)
    done

    lemma nth_drop [rule_format]:
      "n:nat ==> ∀i ∈ nat. ∀xs ∈ list(A). nth(i, drop(n, xs)) = nth(n #+ i, xs)"
    apply (induct_tac "n", simp_all, clarify)
    apply (erule list.cases, auto)
    done

    lemma take_succ [rule_format]:
      "xs∈list(A)
       ==> ∀i. i < length(xs) --> take(succ(i), xs) = take(i,xs) @ [nth(i, xs)]"
    apply (induct_tac "xs", auto)
    apply (subgoal_tac "i∈nat")
    apply (erule natE)
    apply (auto simp add: le_in_nat)
    done

    lemma take_add [rule_format]:
         "[|xs∈list(A); j∈nat|]
          ==> ∀i∈nat. take(i #+ j, xs) = take(i,xs) @ take(j, drop(i,xs))"
    apply (induct_tac "xs", simp_all, clarify)
    apply (erule_tac n = i in natE, simp_all)
    done

    lemma length_take:
         "l∈list(A) ==> ∀n∈nat. length(take(n,l)) = min(n, length(l))"
    apply (induct_tac "l", safe, simp_all)
    apply (erule natE, simp_all)
    done

    subsection{*The function zip*}

    text{*Crafty definition to eliminate a type argument*}

    consts
      zip_aux        :: "[i,i]=>i"

    primrec (*explicit lambda is required because both arguments of "un" vary*)
      "zip_aux(B,[]) =
         (λys ∈ list(B). list_case([], %y l. [], ys))"

      "zip_aux(B,Cons(x,l)) =
         (λys ∈ list(B).
            list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"

    constdefs
      zip :: "[i, i]=>i"
       "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys"

    (* zip equations *)

    lemma list_on_set_of_list: "xs ∈ list(A) ==> xs ∈ list(set_of_list(xs))"
    apply (induct_tac xs, simp_all)
    apply (blast intro: list_mono [THEN subsetD])
    done

    lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil"
    apply (simp add: zip_def list_on_set_of_list [of _ A])
    apply (erule list.cases, simp_all)
    done

    lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil"
    apply (simp add: zip_def list_on_set_of_list [of _ A])
    apply (erule list.cases, simp_all)
    done

    lemma zip_aux_unique [rule_format]:
         "[|B<=C;  xs ∈ list(A)|]
          ==> ∀ys ∈ list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
    apply (induct_tac xs)
     apply simp_all
     apply (blast intro: list_mono [THEN subsetD], clarify)
    apply (erule_tac a=ys in list.cases, auto)
    apply (blast intro: list_mono [THEN subsetD])
    done

    lemma zip_Cons_Cons [simp]:
         "[| xs:list(A); ys:list(B); x:A; y:B |] ==>
          zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))"
    apply (simp add: zip_def, auto)
    apply (rule zip_aux_unique, auto)
    apply (simp add: list_on_set_of_list [of _ B])
    apply (blast intro: list_on_set_of_list list_mono [THEN subsetD])
    done

    lemma zip_type [rule_format,simp,TC]:
         "xs:list(A) ==> ∀ys ∈ list(B). zip(xs, ys):list(A*B)"
    apply (induct_tac "xs")
    apply (simp (no_asm))
    apply clarify
    apply (erule_tac a = ys in list.cases, auto)
    done

    (* zip length *)
    lemma length_zip [rule_format,simp]:
         "xs:list(A) ==> ∀ys ∈ list(B). length(zip(xs,ys)) =
                                         min(length(xs), length(ys))"
    apply (unfold min_def)
    apply (induct_tac "xs", simp_all, clarify)
    apply (erule_tac a = ys in list.cases, auto)
    done

    lemma zip_append1 [rule_format]:
     "[| ys:list(A); zs:list(B) |] ==>
      ∀xs ∈ list(A). zip(xs @ ys, zs) =
                     zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
    apply (induct_tac "zs", force, clarify)
    apply (erule_tac a = xs in list.cases, simp_all)
    done

    lemma zip_append2 [rule_format]:
     "[| xs:list(A); zs:list(B) |] ==> ∀ys ∈ list(B). zip(xs, ys@zs) =
           zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
    apply (induct_tac "xs", force, clarify)
    apply (erule_tac a = ys in list.cases, auto)
    done

    lemma zip_append [simp]:
     "[| length(xs) = length(us); length(ys) = length(vs);
         xs:list(A); us:list(B); ys:list(A); vs:list(B) |]
      ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)"
    by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)

    lemma zip_rev [rule_format,simp]:
     "ys:list(B) ==> ∀xs ∈ list(A).
        length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
    apply (induct_tac "ys", force, clarify)
    apply (erule_tac a = xs in list.cases)
    apply (auto simp add: length_rev)
    done

    lemma nth_zip [rule_format,simp]:
       "ys:list(B) ==> ∀i ∈ nat. ∀xs ∈ list(A).
                        i < length(xs) --> i < length(ys) -->
                        nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
    apply (induct_tac "ys", force, clarify)
    apply (erule_tac a = xs in list.cases, simp)
    apply (auto elim: natE)
    done

    lemma set_of_list_zip [rule_format]:
         "[| xs:list(A); ys:list(B); i:nat |]
          ==> set_of_list(zip(xs, ys)) =
              {<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys))
              & x = nth(i, xs) & y = nth(i, ys)}"
    by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)

    (** list_update **)

    lemma list_update_Nil [simp]: "i:nat ==>list_update(Nil, i, v) = Nil"
    by (unfold list_update_def, auto)

    lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)"
    by (unfold list_update_def, auto)

    lemma list_update_Cons_succ [simp]:
      "n:nat ==>
        list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))"
    apply (unfold list_update_def, auto)
    done

    lemma list_update_type [rule_format,simp,TC]:
         "[| xs:list(A); v:A |] ==> ∀n ∈ nat. list_update(xs, n, v):list(A)"
    apply (induct_tac "xs")
    apply (simp (no_asm))
    apply clarify
    apply (erule natE, auto)
    done

    lemma length_list_update [rule_format,simp]:
         "xs:list(A) ==> ∀i ∈ nat. length(list_update(xs, i, v))=length(xs)"
    apply (induct_tac "xs")
    apply (simp (no_asm))
    apply clarify
    apply (erule natE, auto)
    done

    lemma nth_list_update [rule_format]:
         "[| xs:list(A) |] ==> ∀i ∈ nat. ∀j ∈ nat. i < length(xs)  -->
             nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"
    apply (induct_tac "xs")
     apply simp_all
    apply clarify
    apply (rename_tac i j)
    apply (erule_tac n=i in natE)
    apply (erule_tac [2] n=j in natE)
    apply (erule_tac n=j in natE, simp_all, force)
    done

    lemma nth_list_update_eq [simp]:
         "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x"
    by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)

    lemma nth_list_update_neq [rule_format,simp]:
      "xs:list(A) ==>
         ∀i ∈ nat. ∀j ∈ nat. i ~= j --> nth(j, list_update(xs,i,x)) = nth(j,xs)"
    apply (induct_tac "xs")
     apply (simp (no_asm))
    apply clarify
    apply (erule natE)
    apply (erule_tac [2] natE, simp_all)
    apply (erule natE, simp_all)
    done

    lemma list_update_overwrite [rule_format,simp]:
         "xs:list(A) ==> ∀i ∈ nat. i < length(xs)
       --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
    apply (induct_tac "xs")
     apply (simp (no_asm))
    apply clarify
    apply (erule natE, auto)
    done

    lemma list_update_same_conv [rule_format]:
         "xs:list(A) ==>
          ∀i ∈ nat. i < length(xs) -->
                     (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
    apply (induct_tac "xs")
     apply (simp (no_asm))
    apply clarify
    apply (erule natE, auto)
    done

    lemma update_zip [rule_format]:
         "ys:list(B) ==>
          ∀i ∈ nat. ∀xy ∈ A*B. ∀xs ∈ list(A).
            length(xs) = length(ys) -->
            list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
                                                  list_update(ys, i, snd(xy)))"
    apply (induct_tac "ys")
     apply auto
    apply (erule_tac a = xs in list.cases)
    apply (auto elim: natE)
    done

    lemma set_update_subset_cons [rule_format]:
      "xs:list(A) ==>
       ∀i ∈ nat. set_of_list(list_update(xs, i, x)) <= cons(x, set_of_list(xs))"
    apply (induct_tac "xs")
     apply simp
    apply (rule ballI)
    apply (erule natE, simp_all, auto)
    done

    lemma set_of_list_update_subsetI:
         "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|]
       ==> set_of_list(list_update(xs, i,x)) <= A"
    apply (rule subset_trans)
    apply (rule set_update_subset_cons, auto)
    done

    (** upt **)

    lemma upt_rec:
         "j:nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)"
    apply (induct_tac "j", auto)
    apply (drule not_lt_imp_le)
    apply (auto simp: lt_Ord intro: le_anti_sym)
    done

    lemma upt_conv_Nil [simp]: "[| j le i; j:nat |] ==> upt(i,j) = Nil"
    apply (subst upt_rec, auto)
    apply (auto simp add: le_iff)
    apply (drule lt_asym [THEN notE], auto)
    done

    (*Only needed if upt_Suc is deleted from the simpset*)
    lemma upt_succ_append:
         "[| i le j; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]"
    by simp

    lemma upt_conv_Cons:
         "[| i<j; j:nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))"
    apply (rule trans)
    apply (rule upt_rec, auto)
    done

    lemma upt_type [simp,TC]: "j:nat ==> upt(i,j):list(nat)"
    by (induct_tac "j", auto)

    (*LOOPS as a simprule, since j<=j*)
    lemma upt_add_eq_append:
         "[| i le j; j:nat; k:nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"
    apply (induct_tac "k")
    apply (auto simp add: app_assoc app_type)
    apply (rule_tac j = j in le_trans, auto)
    done

    lemma length_upt [simp]: "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i"
    apply (induct_tac "j")
    apply (rule_tac [2] sym)
    apply (auto dest!: not_lt_imp_le simp add: diff_succ diff_is_0_iff)
    done

    lemma nth_upt [rule_format,simp]:
         "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k"
    apply (induct_tac "j", simp)
    apply (simp add: nth_append le_iff)
    apply (auto dest!: not_lt_imp_le
                simp add: nth_append less_diff_conv add_commute)
    done

    lemma take_upt [rule_format,simp]:
         "[| m:nat; n:nat |] ==>
             ∀i ∈ nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
    apply (induct_tac "m")
    apply (simp (no_asm_simp) add: take_0)
    apply clarify
    apply (subst upt_rec, simp)
    apply (rule sym)
    apply (subst upt_rec, simp)
    apply (simp_all del: upt.simps)
    apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
    apply auto
    done

    lemma map_succ_upt:
         "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
    apply (induct_tac "n")
    apply (auto simp add: map_app_distrib)
    done

    lemma nth_map [rule_format,simp]:
         "xs:list(A) ==>
          ∀n ∈ nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))"
    apply (induct_tac "xs", simp)
    apply (rule ballI)
    apply (induct_tac "n", auto)
    done

    lemma nth_map_upt [rule_format]:
         "[| m:nat; n:nat |] ==>
          ∀i ∈ nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
    apply (rule_tac n = m and m = n in diff_induct, typecheck, simp, simp)
    apply (subst map_succ_upt [symmetric], simp_all, clarify)
    apply (subgoal_tac "i < length (upt (0, x))")
     prefer 2
     apply (simp add: less_diff_conv)
     apply (rule_tac j = "succ (i #+ y) " in lt_trans2)
      apply simp
     apply simp
    apply (subgoal_tac "i < length (upt (y, x))")
     apply (simp_all add: add_commute less_diff_conv)
    done

    (** sublist (a generalization of nth to sets) **)

    constdefs
      sublist :: "[i, i] => i"
        "sublist(xs, A)==
         map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"

    lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil"
    by (unfold sublist_def, auto)

    lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil"
    by (unfold sublist_def, auto)

    lemma sublist_shift_lemma:
     "[| xs:list(B); i:nat |] ==>
      map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
      map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))"
    apply (erule list_append_induct)
    apply (simp (no_asm_simp))
    apply (auto simp add: add_commute length_app filter_append map_app_distrib)
    done

    lemma sublist_type [simp,TC]:
         "xs:list(B) ==> sublist(xs, A):list(B)"
    apply (unfold sublist_def)
    apply (induct_tac "xs")
    apply (auto simp add: filter_append map_app_distrib)
    done

    lemma upt_add_eq_append2:
         "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)"
    by (simp add: upt_add_eq_append [of 0] nat_0_le)

    lemma sublist_append:
     "[| xs:list(B); ys:list(B)  |] ==>
      sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})"
    apply (unfold sublist_def)
    apply (erule_tac l = ys in list_append_induct, simp)
    apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
    apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
    apply (simp_all add: add_commute)
    done

    lemma sublist_Cons:
         "[| xs:list(B); x:B |] ==>
          sublist(Cons(x, xs), A) =
          (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})"
    apply (erule_tac l = xs in list_append_induct)
    apply (simp (no_asm_simp) add: sublist_def)
    apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp)
    done

    lemma sublist_singleton [simp]:
         "sublist([x], A) = (if 0 : A then [x] else [])"
    by (simp add: sublist_Cons)

    lemma sublist_upt_eq_take [rule_format, simp]:
        "xs:list(A) ==> ALL n:nat. sublist(xs,n) = take(n,xs)"
    apply (erule list.induct, simp)
    apply (clarify );
    apply (erule natE)
    apply (simp_all add: nat_eq_Collect_lt Ord_mem_iff_lt sublist_Cons)
    done

    lemma sublist_Int_eq:
         "xs : list(B) ==> sublist(xs, A ∩ nat) = sublist(xs, A)"
    apply (erule list.induct)
    apply (simp_all add: sublist_Cons)
    done

    text{*Repetition of a List Element*}

    consts   repeat :: "[i,i]=>i"
    primrec
      "repeat(a,0) = []"

      "repeat(a,succ(n)) = Cons(a,repeat(a,n))"

    lemma length_repeat: "n ∈ nat ==> length(repeat(a,n)) = n"
    by (induct_tac n, auto)

    lemma repeat_succ_app: "n ∈ nat ==> repeat(a,succ(n)) = repeat(a,n) @ [a]"
    apply (induct_tac n)
    apply (simp_all del: app_Cons add: app_Cons [symmetric])
    done

    lemma repeat_type [TC]: "[|a ∈ A; n ∈ nat|] ==> repeat(a,n) ∈ list(A)"
    by (induct_tac n, auto)

    ML
    {*
    val ConsE = thm "ConsE";
    val Cons_iff = thm "Cons_iff";
    val Nil_Cons_iff = thm "Nil_Cons_iff";
    val list_unfold = thm "list_unfold";
    val list_mono = thm "list_mono";
    val list_univ = thm "list_univ";
    val list_subset_univ = thm "list_subset_univ";
    val list_into_univ = thm "list_into_univ";
    val list_case_type = thm "list_case_type";
    val tl_type = thm "tl_type";
    val drop_Nil = thm "drop_Nil";
    val drop_succ_Cons = thm "drop_succ_Cons";
    val drop_type = thm "drop_type";
    val list_rec_type = thm "list_rec_type";
    val map_type = thm "map_type";
    val map_type2 = thm "map_type2";
    val length_type = thm "length_type";
    val lt_length_in_nat = thm "lt_length_in_nat";
    val app_type = thm "app_type";
    val rev_type = thm "rev_type";
    val flat_type = thm "flat_type";
    val set_of_list_type = thm "set_of_list_type";
    val set_of_list_append = thm "set_of_list_append";
    val list_add_type = thm "list_add_type";
    val map_ident = thm "map_ident";
    val map_compose = thm "map_compose";
    val map_app_distrib = thm "map_app_distrib";
    val map_flat = thm "map_flat";
    val list_rec_map = thm "list_rec_map";
    val list_CollectD = thm "list_CollectD";
    val map_list_Collect = thm "map_list_Collect";
    val length_map = thm "length_map";
    val length_app = thm "length_app";
    val length_rev = thm "length_rev";
    val length_flat = thm "length_flat";
    val drop_length_Cons = thm "drop_length_Cons";
    val drop_length = thm "drop_length";
    val app_right_Nil = thm "app_right_Nil";
    val app_assoc = thm "app_assoc";
    val flat_app_distrib = thm "flat_app_distrib";
    val rev_map_distrib = thm "rev_map_distrib";
    val rev_app_distrib = thm "rev_app_distrib";
    val rev_rev_ident = thm "rev_rev_ident";
    val rev_flat = thm "rev_flat";
    val list_add_app = thm "list_add_app";
    val list_add_rev = thm "list_add_rev";
    val list_add_flat = thm "list_add_flat";
    val list_append_induct = thm "list_append_induct";
    val min_sym = thm "min_sym";
    val min_type = thm "min_type";
    val min_0 = thm "min_0";
    val min_02 = thm "min_02";
    val lt_min_iff = thm "lt_min_iff";
    val min_succ_succ = thm "min_succ_succ";
    val filter_append = thm "filter_append";
    val filter_type = thm "filter_type";
    val length_filter = thm "length_filter";
    val filter_is_subset = thm "filter_is_subset";
    val filter_False = thm "filter_False";
    val filter_True = thm "filter_True";
    val length_is_0_iff = thm "length_is_0_iff";
    val length_is_0_iff2 = thm "length_is_0_iff2";
    val length_tl = thm "length_tl";
    val length_greater_0_iff = thm "length_greater_0_iff";
    val length_succ_iff = thm "length_succ_iff";
    val append_is_Nil_iff = thm "append_is_Nil_iff";
    val append_is_Nil_iff2 = thm "append_is_Nil_iff2";
    val append_left_is_self_iff = thm "append_left_is_self_iff";
    val append_left_is_self_iff2 = thm "append_left_is_self_iff2";
    val append_left_is_Nil_iff = thm "append_left_is_Nil_iff";
    val append_left_is_Nil_iff2 = thm "append_left_is_Nil_iff2";
    val append_eq_append_iff = thm "append_eq_append_iff";
    val append_eq_append = thm "append_eq_append";
    val append_eq_append_iff2 = thm "append_eq_append_iff2";
    val append_self_iff = thm "append_self_iff";
    val append_self_iff2 = thm "append_self_iff2";
    val append1_eq_iff = thm "append1_eq_iff";
    val append_right_is_self_iff = thm "append_right_is_self_iff";
    val append_right_is_self_iff2 = thm "append_right_is_self_iff2";
    val hd_append = thm "hd_append";
    val tl_append = thm "tl_append";
    val rev_is_Nil_iff = thm "rev_is_Nil_iff";
    val Nil_is_rev_iff = thm "Nil_is_rev_iff";
    val rev_is_rev_iff = thm "rev_is_rev_iff";
    val rev_list_elim = thm "rev_list_elim";
    val length_drop = thm "length_drop";
    val drop_all = thm "drop_all";
    val drop_append = thm "drop_append";
    val drop_drop = thm "drop_drop";
    val take_0 = thm "take_0";
    val take_succ_Cons = thm "take_succ_Cons";
    val take_Nil = thm "take_Nil";
    val take_all = thm "take_all";
    val take_type = thm "take_type";
    val take_append = thm "take_append";
    val take_take = thm "take_take";
    val take_add = thm "take_add";
    val take_succ = thm "take_succ";
    val nth_0 = thm "nth_0";
    val nth_Cons = thm "nth_Cons";
    val nth_type = thm "nth_type";
    val nth_append = thm "nth_append";
    val set_of_list_conv_nth = thm "set_of_list_conv_nth";
    val nth_take_lemma = thm "nth_take_lemma";
    val nth_equalityI = thm "nth_equalityI";
    val take_equalityI = thm "take_equalityI";
    val nth_drop = thm "nth_drop";
    val list_on_set_of_list = thm "list_on_set_of_list";
    val zip_Nil = thm "zip_Nil";
    val zip_Nil2 = thm "zip_Nil2";
    val zip_Cons_Cons = thm "zip_Cons_Cons";
    val zip_type = thm "zip_type";
    val length_zip = thm "length_zip";
    val zip_append1 = thm "zip_append1";
    val zip_append2 = thm "zip_append2";
    val zip_append = thm "zip_append";
    val zip_rev = thm "zip_rev";
    val nth_zip = thm "nth_zip";
    val set_of_list_zip = thm "set_of_list_zip";
    val list_update_Nil = thm "list_update_Nil";
    val list_update_Cons_0 = thm "list_update_Cons_0";
    val list_update_Cons_succ = thm "list_update_Cons_succ";
    val list_update_type = thm "list_update_type";
    val length_list_update = thm "length_list_update";
    val nth_list_update = thm "nth_list_update";
    val nth_list_update_eq = thm "nth_list_update_eq";
    val nth_list_update_neq = thm "nth_list_update_neq";
    val list_update_overwrite = thm "list_update_overwrite";
    val list_update_same_conv = thm "list_update_same_conv";
    val update_zip = thm "update_zip";
    val set_update_subset_cons = thm "set_update_subset_cons";
    val set_of_list_update_subsetI = thm "set_of_list_update_subsetI";
    val upt_rec = thm "upt_rec";
    val upt_conv_Nil = thm "upt_conv_Nil";
    val upt_succ_append = thm "upt_succ_append";
    val upt_conv_Cons = thm "upt_conv_Cons";
    val upt_type = thm "upt_type";
    val upt_add_eq_append = thm "upt_add_eq_append";
    val length_upt = thm "length_upt";
    val nth_upt = thm "nth_upt";
    val take_upt = thm "take_upt";
    val map_succ_upt = thm "map_succ_upt";
    val nth_map = thm "nth_map";
    val nth_map_upt = thm "nth_map_upt";
    val sublist_0 = thm "sublist_0";
    val sublist_Nil = thm "sublist_Nil";
    val sublist_shift_lemma = thm "sublist_shift_lemma";
    val sublist_type = thm "sublist_type";
    val upt_add_eq_append2 = thm "upt_add_eq_append2";
    val sublist_append = thm "sublist_append";
    val sublist_Cons = thm "sublist_Cons";
    val sublist_singleton = thm "sublist_singleton";
    val sublist_upt_eq_take = thm "sublist_upt_eq_take";
    val sublist_Int_eq = thm "sublist_Int_eq";

    structure list =
    struct
    val induct = thm "list.induct"
    val elim   = thm "list.cases"
    val intrs  = thms "list.intros"
    end;
    *}

    end

lemmas ConsE:

      [| Cons(a, l) ∈ list(A); [| a ∈ A; l ∈ list(A) |] ==> Q |] ==> Q

lemma Cons_type_iff:

      Cons(a, l) ∈ list(A) <-> a ∈ A ∧ l ∈ list(A)

lemma Cons_iff:

      Cons(a, l) = Cons(a', l') <-> a = a' ∧ l = l'

lemma Nil_Cons_iff:

      [] ≠ Cons(a, l)

lemma list_unfold:

      list(A) = {0} + A × list(A)

lemma list_mono:

      A ⊆ B ==> list(A) ⊆ list(B)

lemma list_univ:

      list(univ(A)) ⊆ univ(A)

lemmas list_subset_univ:

      A2 ⊆ univ(A1) ==> list(A2) ⊆ univ(A1)

lemmas list_subset_univ:

      A2 ⊆ univ(A1) ==> list(A2) ⊆ univ(A1)

lemma list_into_univ:

      [| l ∈ list(A); A ⊆ univ(B) |] ==> l ∈ univ(B)

lemma list_case_type:

      [| l ∈ list(A); c ∈ C([]);
         !!x y. [| x ∈ A; y ∈ list(A) |] ==> h(x, y) ∈ C(Cons(x, y)) |]
      ==> list_case(c, h, l) ∈ C(l)

lemma list_0_triv:

      list(0) = {[]}

lemma tl_type:

      l ∈ list(A) ==> tl(l) ∈ list(A)

lemma drop_Nil:

      i ∈ nat ==> drop(i, []) = []

lemma drop_succ_Cons:

      i ∈ nat ==> drop(succ(i), Cons(a, l)) = drop(i, l)

lemma drop_type:

      [| i ∈ nat; l ∈ list(A) |] ==> drop(i, l) ∈ list(A)

lemma list_rec_type:

      [| l ∈ list(A); c ∈ C([]);
         !!x y r. [| x ∈ A; y ∈ list(A); r ∈ C(y) |] ==> h(x, y, r) ∈ C(Cons(x, y)) |]
      ==> list_rec(c, h, l) ∈ C(l)

lemma map_type:

      [| l ∈ list(A); !!x. x ∈ A ==> h(x) ∈ B |] ==> map(h, l) ∈ list(B)

lemma map_type2:

      l ∈ list(A) ==> map(h, l) ∈ list({h(u) . u ∈ A})

lemma length_type:

      l ∈ list(A) ==> length(l) ∈ nat

lemma lt_length_in_nat:

      [| x < length(xs); xs ∈ list(A) |] ==> x ∈ nat

lemma app_type:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> xs @ ys ∈ list(A)

lemma rev_type:

      xs ∈ list(A) ==> rev(xs) ∈ list(A)

lemma flat_type:

      ls ∈ list(list(A)) ==> flat(ls) ∈ list(A)

lemma set_of_list_type:

      l ∈ list(A) ==> set_of_list(l) ∈ Pow(A)

lemma set_of_list_append:

      xs ∈ list(A) ==> set_of_list(xs @ ys) = set_of_list(xs) ∪ set_of_list(ys)

lemma list_add_type:

      xs ∈ list(nat) ==> list_add(xs) ∈ nat

lemma map_ident:

      l ∈ list(A) ==> map(%u. u, l) = l

lemma map_compose:

      l ∈ list(A) ==> map(h, map(j, l)) = map(%u. h(j(u)), l)

lemma map_app_distrib:

      xs ∈ list(A) ==> map(h, xs @ ys) = map(h, xs) @ map(h, ys)

lemma map_flat:

      ls ∈ list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h), ls))

lemma list_rec_map:

      l ∈ list(A)
      ==> list_rec(c, d, map(h, l)) = list_rec(c, %x xs r. d(h(x), map(h, xs), r), l)

lemmas list_CollectD:

      c ∈ list(Collect(B, P)) ==> c ∈ list(B)

lemmas list_CollectD:

      c ∈ list(Collect(B, P)) ==> c ∈ list(B)

lemma map_list_Collect:

      l ∈ list({x ∈ A . h(x) = j(x)}) ==> map(h, l) = map(j, l)

lemma length_map:

      xs ∈ list(A) ==> length(map(h, xs)) = length(xs)

lemma length_app:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> length(xs @ ys) = length(xs) #+ length(ys)

lemma length_rev:

      xs ∈ list(A) ==> length(rev(xs)) = length(xs)

lemma length_flat:

      ls ∈ list(list(A)) ==> length(flat(ls)) = list_add(map(length, ls))

lemma drop_length_Cons:

      xs ∈ list(A) ==> ∃z zs. drop(length(xs), Cons(x, xs)) = Cons(z, zs)

lemma drop_length:

      [| l ∈ list(A); i ∈ length(l) |] ==> ∃z zs. drop(i, l) = Cons(z, zs)

lemma app_right_Nil:

      xs ∈ list(A) ==> xs @ [] = xs

lemma app_assoc:

      xs ∈ list(A) ==> (xs @ ys) @ zs = xs @ ys @ zs

lemma flat_app_distrib:

      ls ∈ list(list(A)) ==> flat(ls @ ms) = flat(ls) @ flat(ms)

lemma rev_map_distrib:

      l ∈ list(A) ==> rev(map(h, l)) = map(h, rev(l))

lemma rev_app_distrib:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> rev(xs @ ys) = rev(ys) @ rev(xs)

lemma rev_rev_ident:

      l ∈ list(A) ==> rev(rev(l)) = l

lemma rev_flat:

      ls ∈ list(list(A)) ==> rev(flat(ls)) = flat(map(rev, rev(ls)))

lemma list_add_app:

      [| xs ∈ list(nat); ys ∈ list(nat) |]
      ==> list_add(xs @ ys) = list_add(ys) #+ list_add(xs)

lemma list_add_rev:

      l ∈ list(nat) ==> list_add(rev(l)) = list_add(l)

lemma list_add_flat:

      ls ∈ list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add, ls))

lemma list_append_induct:

      [| l ∈ list(A); P([]); !!x y. [| x ∈ A; y ∈ list(A); P(y) |] ==> P(y @ [x]) |]
      ==> P(l)

lemma list_complete_induct_lemma:

      [| !!l. [| l ∈ list(A); ∀l'∈list(A). length(l') < length(l) --> P(l') |]
              ==> P(l);
         n ∈ nat |]
      ==> ∀l∈list(A). length(l) < n --> P(l)

theorem list_complete_induct:

      [| l ∈ list(A);
         !!l. [| l ∈ list(A); ∀l'∈list(A). length(l') < length(l) --> P(l') |]
              ==> P(l) |]
      ==> P(l)

lemma min_sym:

      [| i ∈ nat; j ∈ nat |] ==> min(i, j) = min(j, i)

lemma min_type:

      [| i ∈ nat; j ∈ nat |] ==> min(i, j) ∈ nat

lemma min_0:

      i ∈ nat ==> min(0, i) = 0

lemma min_02:

      i ∈ nat ==> min(i, 0) = 0

lemma lt_min_iff:

      [| i ∈ nat; j ∈ nat; k ∈ nat |] ==> i < min(j, k) <-> i < j ∧ i < k

lemma min_succ_succ:

      [| i ∈ nat; j ∈ nat |] ==> min(succ(i), succ(j)) = succ(min(i, j))

lemma filter_append:

      xs ∈ list(A) ==> filter(P, xs @ ys) = filter(P, xs) @ filter(P, ys)

lemma filter_type:

      xs ∈ list(A) ==> filter(P, xs) ∈ list(A)

lemma length_filter:

      xs ∈ list(A) ==> length(filter(P, xs)) ≤ length(xs)

lemma filter_is_subset:

      xs ∈ list(A) ==> set_of_list(filter(P, xs)) ⊆ set_of_list(xs)

lemma filter_False:

      xs ∈ list(A) ==> filter(%p. False, xs) = []

lemma filter_True:

      xs ∈ list(A) ==> filter(%p. True, xs) = xs

lemma length_is_0_iff:

      xs ∈ list(A) ==> length(xs) = 0 <-> xs = []

lemma length_is_0_iff2:

      xs ∈ list(A) ==> 0 = length(xs) <-> xs = []

lemma length_tl:

      xs ∈ list(A) ==> length(tl(xs)) = length(xs) #- 1

lemma length_greater_0_iff:

      xs ∈ list(A) ==> 0 < length(xs) <-> xs ≠ []

lemma length_succ_iff:

      xs ∈ list(A)
      ==> length(xs) = succ(n) <-> (∃y ys. xs = Cons(y, ys) ∧ length(ys) = n)

lemma append_is_Nil_iff:

      xs ∈ list(A) ==> xs @ ys = [] <-> xs = [] ∧ ys = []

lemma append_is_Nil_iff2:

      xs ∈ list(A) ==> [] = xs @ ys <-> xs = [] ∧ ys = []

lemma append_left_is_self_iff:

      xs ∈ list(A) ==> xs @ ys = xs <-> ys = []

lemma append_left_is_self_iff2:

      xs ∈ list(A) ==> xs = xs @ ys <-> ys = []

lemma append_left_is_Nil_iff:

      [| xs ∈ list(A); ys ∈ list(A); zs ∈ list(A); length(ys) = length(zs) |]
      ==> xs @ ys = zs <-> xs = [] ∧ ys = zs

lemma append_left_is_Nil_iff2:

      [| xs ∈ list(A); ys ∈ list(A); zs ∈ list(A); length(ys) = length(zs) |]
      ==> zs = ys @ xs <-> xs = [] ∧ ys = zs

lemma append_eq_append_iff:

      [| xs ∈ list(A); ys ∈ list(A); length(xs) = length(ys) |]
      ==> xs @ us = ys @ vs <-> xs = ys ∧ us = vs

lemma append_eq_append:

      [| xs ∈ list(A); ys ∈ list(A); us ∈ list(A); vs ∈ list(A);
         length(us) = length(vs); xs @ us = ys @ vs |]
      ==> xs = ys ∧ us = vs

lemma append_eq_append_iff2:

      [| xs ∈ list(A); ys ∈ list(A); us ∈ list(A); vs ∈ list(A);
         length(us) = length(vs) |]
      ==> xs @ us = ys @ vs <-> xs = ys ∧ us = vs

lemma append_self_iff:

      [| xs ∈ list(A); ys ∈ list(A); zs ∈ list(A) |] ==> xs @ ys = xs @ zs <-> ys = zs

lemma append_self_iff2:

      [| xs ∈ list(A); ys ∈ list(A); zs ∈ list(A) |] ==> ys @ xs = zs @ xs <-> ys = zs

lemma append1_eq_iff:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> xs @ [x] = ys @ [y] <-> xs = ys ∧ x = y

lemma append_right_is_self_iff:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> xs @ ys = ys <-> xs = []

lemma append_right_is_self_iff2:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> ys = xs @ ys <-> xs = []

lemma hd_append:

      [| xs ∈ list(A); xs ≠ [] |] ==> hd(xs @ ys) = hd(xs)

lemma tl_append:

      [| xs ∈ list(A); xs ≠ [] |] ==> tl(xs @ ys) = tl(xs) @ ys

lemma rev_is_Nil_iff:

      xs ∈ list(A) ==> rev(xs) = [] <-> xs = []

lemma Nil_is_rev_iff:

      xs ∈ list(A) ==> [] = rev(xs) <-> xs = []

lemma rev_is_rev_iff:

      [| xs ∈ list(A); ys ∈ list(A) |] ==> rev(xs) = rev(ys) <-> xs = ys

lemma rev_list_elim:

      [| xs ∈ list(A); xs = [] ==> P;
         !!ys y. [| ys ∈ list(A); y ∈ A; xs = ys @ [y] |] ==> P |]
      ==> P

lemma length_drop:

      [| n ∈ nat; xs ∈ list(A) |] ==> length(drop(n, xs)) = length(xs) #- n

lemma drop_all:

      [| n ∈ nat; xs ∈ list(A); length(xs) ≤ n |] ==> drop(n, xs) = []

lemma drop_append:

      [| n ∈ nat; xs ∈ list(A) |]
      ==> drop(n, xs @ ys) = drop(n, xs) @ drop(n #- length(xs), ys)

lemma drop_drop:

      m ∈ nat ==> ∀xs∈list(A). ∀n∈nat. drop(n, drop(m, xs)) = drop(n #+ m, xs)

lemma take_0:

      xs ∈ list(A) ==> take(0, xs) = []

lemma take_succ_Cons:

      n ∈ nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))

lemma take_Nil:

      n ∈ nat ==> take(n, []) = []

lemma take_all:

      [| n ∈ nat; xs ∈ list(A); length(xs) ≤ n |] ==> take(n, xs) = xs

lemma take_type:

      [| xs ∈ list(A); n ∈ nat |] ==> take(n, xs) ∈ list(A)

lemma take_append:

      [| xs ∈ list(A); ys ∈ list(A); n ∈ nat |]
      ==> take(n, xs @ ys) = take(n, xs) @ take(n #- length(xs), ys)

lemma take_take:

      [| m ∈ nat; xs ∈ list(A); n ∈ nat |]
      ==> take(n, take(m, xs)) = take(min(n, m), xs)

lemma nth_0:

      nth(0, Cons(a, l)) = a

lemma nth_Cons:

      n ∈ nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)

lemma nth_empty:

      nth(n, []) = 0

lemma nth_type:

      [| xs ∈ list(A); n < length(xs) |] ==> nth(n, xs) ∈ A

lemma nth_eq_0:

      [| xs ∈ list(A); n ∈ nat; length(xs) ≤ n |] ==> nth(n, xs) = 0

lemma nth_append:

      [| xs ∈ list(A); n ∈ nat |]
      ==> nth(n, xs @ ys) =
          (if n < length(xs) then nth(n, xs) else nth(n #- length(xs), ys))

lemma set_of_list_conv_nth:

      xs ∈ list(A)
      ==> set_of_list(xs) = {x ∈ A . ∃i∈nat. i < length(xs) ∧ x = nth(i, xs)}

lemma nth_take_lemma:

      [| k ∈ nat; xs ∈ list(A); ys ∈ list(A); k ≤ length(xs); k ≤ length(ys);
         !!i. [| i ∈ nat; i < k |] ==> nth(i, xs) = nth(i, ys) |]
      ==> take(k, xs) = take(k, ys)

lemma nth_equalityI:

      [| xs ∈ list(A); ys ∈ list(A); length(xs) = length(ys);
         !!i. [| i ∈ nat; i < length(xs) |] ==> nth(i, xs) = nth(i, ys) |]
      ==> xs = ys

lemma take_equalityI:

      [| xs ∈ list(A); ys ∈ list(A); !!i. i ∈ nat ==> take(i, xs) = take(i, ys) |]
      ==> xs = ys

lemma nth_drop:

      [| n ∈ nat; i ∈ nat; xs ∈ list(A) |] ==> nth(i, drop(n, xs)) = nth(n #+ i, xs)

lemma take_succ:

      [| xs ∈ list(A); i < length(xs) |]
      ==> take(succ(i), xs) = take(i, xs) @ [nth(i, xs)]

lemma take_add:

      [| xs ∈ list(A); j ∈ nat; i ∈ nat |]
      ==> take(i #+ j, xs) = take(i, xs) @ take(j, drop(i, xs))

lemma length_take:

      l ∈ list(A) ==> ∀n∈nat. length(take(n, l)) = min(n, length(l))

### The function zip

lemma list_on_set_of_list:

      xs ∈ list(A) ==> xs ∈ list(set_of_list(xs))

lemma zip_Nil:

      ys ∈ list(A) ==> zip([], ys) = []

lemma zip_Nil2:

      xs ∈ list(A) ==> zip(xs, []) = []

lemma zip_aux_unique:

      [| B ⊆ C; xs ∈ list(A); ys ∈ list(B) |]
      ==> zip_aux(C, xs) ` ys = zip_aux(B, xs) ` ys

lemma zip_Cons_Cons:

      [| xs ∈ list(A); ys ∈ list(B); x ∈ A; y ∈ B |]
      ==> zip(Cons(x, xs), Cons(y, ys)) = Cons(⟨x, y⟩, zip(xs, ys))

lemma zip_type:

      [| xs ∈ list(A); ys ∈ list(B) |] ==> zip(xs, ys) ∈ list(A × B)

lemma length_zip:

      [| xs ∈ list(A); ys ∈ list(B) |]
      ==> length(zip(xs, ys)) = min(length(xs), length(ys))

lemma zip_append1:

      [| ys ∈ list(A); zs ∈ list(B); xs ∈ list(A) |]
      ==> zip(xs @ ys, zs) =
          zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs), zs))

lemma zip_append2:

      [| xs ∈ list(A); zs ∈ list(B); ys ∈ list(B) |]
      ==> zip(xs, ys @ zs) =
          zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)

lemma zip_append:

      [| length(xs) = length(us); length(ys) = length(vs); xs ∈ list(A); us ∈ list(B);
         ys ∈ list(A); vs ∈ list(B) |]
      ==> zip(xs @ ys, us @ vs) = zip(xs, us) @ zip(ys, vs)

lemma zip_rev:

      [| ys ∈ list(B); xs ∈ list(A); length(xs) = length(ys) |]
      ==> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))

lemma nth_zip:

      [| ys ∈ list(B); i ∈ nat; xs ∈ list(A); i < length(xs); i < length(ys) |]
      ==> nth(i, zip(xs, ys)) = ⟨nth(i, xs), nth(i, ys)⟩

lemma set_of_list_zip:

      [| xs ∈ list(A); ys ∈ list(B); i ∈ nat |]
      ==> set_of_list(zip(xs, ys)) =
          {⟨x,y⟩ ∈ A × B .
           ∃i∈nat. i < min(length(xs), length(ys)) ∧ x = nth(i, xs) ∧ y = nth(i, ys)}

lemma list_update_Nil:

      i ∈ nat ==> list_update([], i, v) = []

lemma list_update_Cons_0:

      list_update(Cons(x, xs), 0, v) = Cons(v, xs)

lemma list_update_Cons_succ:

      n ∈ nat
      ==> list_update(Cons(x, xs), succ(n), v) = Cons(x, list_update(xs, n, v))

lemma list_update_type:

      [| xs ∈ list(A); v ∈ A; n ∈ nat |] ==> list_update(xs, n, v) ∈ list(A)

lemma length_list_update:

      [| xs ∈ list(A); i ∈ nat |] ==> length(list_update(xs, i, v)) = length(xs)

lemma nth_list_update:

      [| xs ∈ list(A); i ∈ nat; j ∈ nat; i < length(xs) |]
      ==> nth(j, list_update(xs, i, x)) = (if i = j then x else nth(j, xs))

lemma nth_list_update_eq:

      [| i < length(xs); xs ∈ list(A) |] ==> nth(i, list_update(xs, i, x)) = x

lemma nth_list_update_neq:

      [| xs ∈ list(A); i ∈ nat; j ∈ nat; i ≠ j |]
      ==> nth(j, list_update(xs, i, x)) = nth(j, xs)

lemma list_update_overwrite:

      [| xs ∈ list(A); i ∈ nat; i < length(xs) |]
      ==> list_update(list_update(xs, i, x), i, y) = list_update(xs, i, y)

lemma list_update_same_conv:

      [| xs ∈ list(A); i ∈ nat; i < length(xs) |]
      ==> list_update(xs, i, x) = xs <-> nth(i, xs) = x

lemma update_zip:

      [| ys ∈ list(B); i ∈ nat; xy ∈ A × B; xs ∈ list(A); length(xs) = length(ys) |]
      ==> list_update(zip(xs, ys), i, xy) =
          zip(list_update(xs, i, fst(xy)), list_update(ys, i, snd(xy)))

lemma set_update_subset_cons:

      [| xs ∈ list(A); i ∈ nat |]
      ==> set_of_list(list_update(xs, i, x)) ⊆ cons(x, set_of_list(xs))

lemma set_of_list_update_subsetI:

      [| set_of_list(xs) ⊆ A; xs ∈ list(A); x ∈ A; i ∈ nat |]
      ==> set_of_list(list_update(xs, i, x)) ⊆ A

lemma upt_rec:

      j ∈ nat ==> upt(i, j) = (if i < j then Cons(i, upt(succ(i), j)) else [])

lemma upt_conv_Nil:

      [| j ≤ i; j ∈ nat |] ==> upt(i, j) = []

lemma upt_succ_append:

      [| i ≤ j; j ∈ nat |] ==> upt(i, succ(j)) = upt(i, j) @ [j]

lemma upt_conv_Cons:

      [| i < j; j ∈ nat |] ==> upt(i, j) = Cons(i, upt(succ(i), j))

lemma upt_type:

      j ∈ nat ==> upt(i, j) ∈ list(nat)

lemma upt_add_eq_append:

      [| i ≤ j; j ∈ nat; k ∈ nat |] ==> upt(i, j #+ k) = upt(i, j) @ upt(j, j #+ k)

lemma length_upt:

      [| i ∈ nat; j ∈ nat |] ==> length(upt(i, j)) = j #- i

lemma nth_upt:

      [| i ∈ nat; j ∈ nat; k ∈ nat; i #+ k < j |] ==> nth(k, upt(i, j)) = i #+ k

lemma take_upt:

      [| m ∈ nat; n ∈ nat; i ∈ nat; i #+ m ≤ n |]
      ==> take(m, upt(i, n)) = upt(i, i #+ m)

lemma map_succ_upt:

      [| m ∈ nat; n ∈ nat |] ==> map(succ, upt(m, n)) = upt(succ(m), succ(n))

lemma nth_map:

      [| xs ∈ list(A); n ∈ nat; n < length(xs) |]
      ==> nth(n, map(f, xs)) = f(nth(n, xs))

lemma nth_map_upt:

      [| m ∈ nat; n ∈ nat; i ∈ nat; i < n #- m |]
      ==> nth(i, map(f, upt(m, n))) = f(m #+ i)

lemma sublist_0:

      xs ∈ list(A) ==> sublist(xs, 0) = []

lemma sublist_Nil:

      sublist([], A) = []

lemma sublist_shift_lemma:

      [| xs ∈ list(B); i ∈ nat |]
      ==> map(fst, filter(%p. snd(p) ∈ A, zip(xs, upt(i, i #+ length(xs))))) =
          map(fst,
              filter(%p. snd(p) ∈ nat ∧ snd(p) #+ i ∈ A, zip(xs, upt(0, length(xs)))))

lemma sublist_type:

      xs ∈ list(B) ==> sublist(xs, A) ∈ list(B)

lemma upt_add_eq_append2:

      [| i ∈ nat; j ∈ nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)

lemma sublist_append:

      [| xs ∈ list(B); ys ∈ list(B) |]
      ==> sublist(xs @ ys, A) =
          sublist(xs, A) @ sublist(ys, {j ∈ nat . j #+ length(xs) ∈ A})

lemma sublist_Cons:

      [| xs ∈ list(B); x ∈ B |]
      ==> sublist(Cons(x, xs), A) =
          (if 0 ∈ A then [x] else []) @ sublist(xs, {j ∈ nat . succ(j) ∈ A})

lemma sublist_singleton:

      sublist([x], A) = (if 0 ∈ A then [x] else [])

lemma sublist_upt_eq_take:

      [| xs ∈ list(A); n ∈ nat |] ==> sublist(xs, n) = take(n, xs)

lemma sublist_Int_eq:

      xs ∈ list(B) ==> sublist(xs, A ∩ nat) = sublist(xs, A)

lemma length_repeat:

      n ∈ nat ==> length(repeat(a, n)) = n

lemma repeat_succ_app:

      n ∈ nat ==> repeat(a, succ(n)) = repeat(a, n) @ [a]

lemma repeat_type:

      [| a ∈ A; n ∈ nat |] ==> repeat(a, n) ∈ list(A)