# Theory SList

Up to index of Isabelle/HOL/Induct

theory SList
imports NatArith Sexp Hilbert_Choice
begin

    (* *********************************************************************** *)
    (*                                                                         *)
    (* Title:      SList.thy (Extended List Theory)                            *)
    (* Based on:   $Id: SList.thy,v 1.14 2005/06/17 14:13:07 haftmann Exp $      *)
    (* Author:     Lawrence C Paulson, Cambridge University Computer Laboratory*)
    (* Author:     B. Wolff, University of Bremen                              *)
    (* Purpose:    Enriched theory of lists                                    *)
    (*             mutual indirect recursive data-types                        *)
    (*                                                                         *)
    (* *********************************************************************** *)

    (* Definition of type 'a list (strict lists) by a least fixed point

    We use          list(A) == lfp(%Z. {NUMB(0)} <+> A <*> Z)
    and not         list    == lfp(%Z. {NUMB(0)} <+> range(Leaf) <*> Z)

    so that list can serve as a "functor" for defining other recursive types.

    This enables the conservative construction of mutual recursive data-types
    such as

    datatype 'a m = Node 'a * ('a m) list

    Tidied by lcp.  Still needs removal of nat_rec.
    *)

    theory SList imports NatArith Sexp Hilbert_Choice begin

    (*Hilbert_Choice is needed for the function "inv"*)

    (* *********************************************************************** *)
    (*                                                                         *)
    (* Building up data type                                                   *)
    (*                                                                         *)
    (* *********************************************************************** *)

    (* Defining the Concrete Constructors *)
    constdefs
      NIL  :: "'a item"
       "NIL == In0(Numb(0))"

      CONS :: "['a item, 'a item] => 'a item"
       "CONS M N == In1(Scons M N)"

    consts
      list      :: "'a item set => 'a item set"
    inductive "list(A)"
      intros
        NIL_I:  "NIL: list A"
        CONS_I: "[| a: A;  M: list A |] ==> CONS a M : list A"

    typedef (List)
      'a list = "list(range Leaf) :: 'a item set"
      by (blast intro: list.NIL_I)

    constdefs
      List_case :: "['b, ['a item, 'a item]=>'b, 'a item] => 'b"
       "List_case c d == Case(%x. c)(Split(d))"

      List_rec  :: "['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b"
       "List_rec M c d == wfrec (trancl pred_sexp)
                                (%g. List_case c (%x y. d x y (g y))) M"

    (* *********************************************************************** *)
    (*                                                                         *)
    (* Abstracting data type                                                   *)
    (*                                                                         *)
    (* *********************************************************************** *)

    (*Declaring the abstract list constructors*)

    constdefs
      Nil       :: "'a list"
       "Nil  == Abs_List(NIL)"

      "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65)
       "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"

      (* list Recursion -- the trancl is Essential; see list.ML *)
      list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
       "list_rec l c d ==
          List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"

      list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
       "list_case a f xs == list_rec xs a (%x xs r. f x xs)"

    (* list Enumeration *)
    consts
      "[]"      :: "'a list"                            ("[]")
    syntax
      "@list"   :: "args => 'a list"                    ("[(_)]")

    translations
      "[x, xs]" == "x#[xs]"
      "[x]"     == "x#[]"
      "[]"      == "Nil"

      "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys. b, xs)"

    (* *********************************************************************** *)
    (*                                                                         *)
    (* Generalized Map Functionals                                             *)
    (*                                                                         *)
    (* *********************************************************************** *)

    (* Generalized Map Functionals *)

    constdefs
      Rep_map   :: "('b => 'a item) => ('b list => 'a item)"
       "Rep_map f xs == list_rec xs  NIL(%x l r. CONS(f x) r)"

      Abs_map   :: "('a item => 'b) => 'a item => 'b list"
       "Abs_map g M  == List_rec M Nil (%N L r. g(N)#r)"

    (**** Function definitions ****)

    constdefs

      null      :: "'a list => bool"
      "null xs  == list_rec xs True (%x xs r. False)"

      hd        :: "'a list => 'a"
      "hd xs    == list_rec xs (@x. True) (%x xs r. x)"

      tl        :: "'a list => 'a list"
      "tl xs    == list_rec xs (@xs. True) (%x xs r. xs)"

      (* a total version of tl: *)
      ttl       :: "'a list => 'a list"
      "ttl xs   == list_rec xs [] (%x xs r. xs)"

      member :: "['a, 'a list] => bool"    (infixl "mem" 55)
      "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"

      list_all  :: "('a => bool) => ('a list => bool)"
      "list_all P xs == list_rec xs True(%x l r. P(x) & r)"

      map       :: "('a=>'b) => ('a list => 'b list)"
      "map f xs == list_rec xs [] (%x l r. f(x)#r)"

    constdefs
      append    :: "['a list, 'a list] => 'a list"   (infixr "@" 65)
      "xs@ys == list_rec xs ys (%x l r. x#r)"

      filter    :: "['a => bool, 'a list] => 'a list"
      "filter P xs == list_rec xs []  (%x xs r. if P(x)then x#r else r)"

      foldl     :: "[['b,'a] => 'b, 'b, 'a list] => 'b"
      "foldl f a xs == list_rec xs (%a. a)(%x xs r.%a. r(f a x))(a)"

      foldr     :: "[['a,'b] => 'b, 'b, 'a list] => 'b"
      "foldr f a xs     == list_rec xs a (%x xs r. (f x r))"

      length    :: "'a list => nat"
      "length xs== list_rec xs 0 (%x xs r. Suc r)"

      drop      :: "['a list,nat] => 'a list"
      "drop t n == (nat_rec(%x. x)(%m r xs. r(ttl xs)))(n)(t)"

      copy      :: "['a, nat] => 'a list"      (* make list of n copies of x *)
      "copy t   == nat_rec [] (%m xs. t # xs)"

      flat      :: "'a list list => 'a list"
      "flat     == foldr (op @) []"

      nth       :: "[nat, 'a list] => 'a"
      "nth      == nat_rec hd (%m r xs. r(tl xs))"

      rev       :: "'a list => 'a list"
      "rev xs   == list_rec xs [] (%x xs xsa. xsa @ [x])"

    (* miscellaneous definitions *)
      zipWith   :: "['a * 'b => 'c, 'a list * 'b list] => 'c list"
      "zipWith f S == (list_rec (fst S)  (%T.[])
                                (%x xs r. %T. if null T then []
                                              else f(x,hd T) # r(tl T)))(snd(S))"

      zip       :: "'a list * 'b list => ('a*'b) list"
      "zip      == zipWith  (%s. s)"

      unzip     :: "('a*'b) list => ('a list * 'b list)"
      "unzip    == foldr(% (a,b)(c,d).(a#c,b#d))([],[])"

    consts take      :: "['a list,nat] => 'a list"
    primrec
      take_0:  "take xs 0 = []"
      take_Suc: "take xs (Suc n) = list_case [] (%x l. x # take l n) xs"

    consts enum      :: "[nat,nat] => nat list"
    primrec
      enum_0:   "enum i 0 = []"
      enum_Suc: "enum i (Suc j) = (if i <= j then enum i j @ [j] else [])"

    syntax
      (* Special syntax for list_all and filter *)
      "@Alls"       :: "[idt, 'a list, bool] => bool"        ("(2Alls _:_./ _)" 10)
      "@filter"     :: "[idt, 'a list, bool] => 'a list"     ("(1[_:_ ./ _])")

    translations
      "[x:xs. P]"   == "filter(%x. P) xs"
      "Alls x:xs. P"== "list_all(%x. P)xs"

    lemma ListI: "x : list (range Leaf) ==> x : List"
    by (simp add: List_def)

    lemma ListD: "x : List ==> x : list (range Leaf)"
    by (simp add: List_def)

    lemma list_unfold: "list(A) = usum {Numb(0)} (uprod A (list(A)))"
      by (fast intro!: list.intros [unfolded NIL_def CONS_def]
               elim: list.cases [unfolded NIL_def CONS_def])

    (*This justifies 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 (assumption | rule basic_monos)+
    done

    (*Type checking -- list creates well-founded sets*)
    lemma list_sexp: "list(sexp) <= sexp"
    apply (unfold NIL_def CONS_def list.defs)
    apply (rule lfp_lowerbound)
    apply (fast intro: sexp.intros sexp_In0I sexp_In1I)
    done

    (* A <= sexp ==> list(A) <= sexp *)
    lemmas list_subset_sexp = subset_trans [OF list_mono list_sexp]

    (*Induction for the type 'a list *)
    lemma list_induct:
        "[| P(Nil);
            !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)"
    apply (unfold Nil_def Cons_def)
    apply (rule Rep_List_inverse [THEN subst])
                             (*types force good instantiation*)
    apply (rule Rep_List [unfolded List_def, THEN list.induct], simp)
    apply (erule Abs_List_inverse [unfolded List_def, THEN subst], blast)
    done

    (*** Isomorphisms ***)

    lemma inj_on_Abs_list: "inj_on Abs_List (list(range Leaf))"
    apply (rule inj_on_inverseI)
    apply (erule Abs_List_inverse [unfolded List_def])
    done

    (** Distinctness of constructors **)

    lemma CONS_not_NIL [iff]: "CONS M N ~= NIL"
    by (simp add: NIL_def CONS_def)

    lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
    lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard]
    lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]

    lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
    apply (unfold Nil_def Cons_def)
    apply (rule CONS_not_NIL [THEN inj_on_Abs_list [THEN inj_on_contraD]])
    apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
    done

    lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard]
    lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard]
    lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]

    (** Injectiveness of CONS and Cons **)

    lemma CONS_CONS_eq [iff]: "(CONS K M)=(CONS L N) = (K=L & M=N)"
    by (simp add: CONS_def)

    (*For reasoning about abstract list constructors*)
    declare Rep_List [THEN ListD, intro] ListI [intro]
    declare list.intros [intro,simp]
    declare Leaf_inject [dest!]

    lemma Cons_Cons_eq [iff]: "(x#xs=y#ys) = (x=y & xs=ys)"
    apply (simp add: Cons_def)
    apply (subst Abs_List_inject)
    apply (auto simp add: Rep_List_inject)
    done

    lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]

    lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
    apply (erule setup_induction)
    apply (erule list.induct, blast+)
    done

    lemma sexp_CONS_D: "CONS M N: sexp ==> M: sexp & N: sexp"
    apply (simp add: CONS_def In1_def)
    apply (fast dest!: Scons_D)
    done

    (*Reasoning about constructors and their freeness*)

    lemma not_CONS_self: "N: list(A) ==> !M. N ~= CONS M N"
    by (erule list.induct, simp_all)

    lemma not_Cons_self2: "∀x. l ~= x#l"
    by (induct_tac "l" rule: list_induct, simp_all)

    lemma neq_Nil_conv2: "(xs ~= []) = (∃y ys. xs = y#ys)"
    by (induct_tac "xs" rule: list_induct, auto)

    (** Conversion rules for List_case: case analysis operator **)

    lemma List_case_NIL [simp]: "List_case c h NIL = c"
    by (simp add: List_case_def NIL_def)

    lemma List_case_CONS [simp]: "List_case c h (CONS M N) = h M N"
    by (simp add: List_case_def CONS_def)

    (*** List_rec -- by wf recursion on pred_sexp ***)

    (* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
       hold if pred_sexp^+ were changed to pred_sexp. *)

    lemma List_rec_unfold_lemma:
         "(%M. List_rec M c d) ==
          wfrec (trancl pred_sexp) (%g. List_case c (%x y. d x y (g y)))"
    by (simp add: List_rec_def)

    lemmas List_rec_unfold =
        def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl],
                   standard]

    (** pred_sexp lemmas **)

    lemma pred_sexp_CONS_I1:
        "[| M: sexp;  N: sexp |] ==> (M, CONS M N) : pred_sexp^+"
    by (simp add: CONS_def In1_def)

    lemma pred_sexp_CONS_I2:
        "[| M: sexp;  N: sexp |] ==> (N, CONS M N) : pred_sexp^+"
    by (simp add: CONS_def In1_def)

    lemma pred_sexp_CONS_D:
        "(CONS M1 M2, N) : pred_sexp^+ ==>
         (M1,N) : pred_sexp^+ & (M2,N) : pred_sexp^+"
    apply (frule pred_sexp_subset_Sigma [THEN trancl_subset_Sigma, THEN subsetD])
    apply (blast dest!: sexp_CONS_D intro: pred_sexp_CONS_I1 pred_sexp_CONS_I2
                        trans_trancl [THEN transD])
    done

    (** Conversion rules for List_rec **)

    lemma List_rec_NIL [simp]: "List_rec NIL c h = c"
    apply (rule List_rec_unfold [THEN trans])
    apply (simp add: List_case_NIL)
    done

    lemma List_rec_CONS [simp]:
         "[| M: sexp;  N: sexp |]
          ==> List_rec (CONS M N) c h = h M N (List_rec N c h)"
    apply (rule List_rec_unfold [THEN trans])
    apply (simp add: pred_sexp_CONS_I2)
    done

    (*** list_rec -- by List_rec ***)

    lemmas Rep_List_in_sexp =
        subsetD [OF range_Leaf_subset_sexp [THEN list_subset_sexp]
                    Rep_List [THEN ListD]]

    lemma list_rec_Nil [simp]: "list_rec Nil c h = c"
    by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Nil_def)

    lemma list_rec_Cons [simp]: "list_rec (a#l) c h = h a l (list_rec l c h)"
    by (simp add: list_rec_def ListI [THEN Abs_List_inverse] Cons_def
                  Rep_List_inverse Rep_List [THEN ListD] inj_Leaf Rep_List_in_sexp)

    (*Type checking.  Useful?*)
    lemma List_rec_type:
         "[| M: list(A);
             A<=sexp;
             c: C(NIL);
             !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y)
          |] ==> List_rec M c h : C(M :: 'a item)"
    apply (erule list.induct, simp)
    apply (insert list_subset_sexp)
    apply (subst List_rec_CONS, blast+)
    done

    (** Generalized map functionals **)

    lemma Rep_map_Nil [simp]: "Rep_map f Nil = NIL"
    by (simp add: Rep_map_def)

    lemma Rep_map_Cons [simp]:
        "Rep_map f(x#xs) = CONS(f x)(Rep_map f xs)"
    by (simp add: Rep_map_def)

    lemma Rep_map_type: "(!!x. f(x): A) ==> Rep_map f xs: list(A)"
    apply (simp add: Rep_map_def)
    apply (rule list_induct, auto)
    done

    lemma Abs_map_NIL [simp]: "Abs_map g NIL = Nil"
    by (simp add: Abs_map_def)

    lemma Abs_map_CONS [simp]:
        "[| M: sexp;  N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N"
    by (simp add: Abs_map_def)

    (*Eases the use of primitive recursion.  NOTE USE OF == *)
    lemma def_list_rec_NilCons:
        "[| !!xs. f(xs) == list_rec xs c h  |]
         ==> f [] = c & f(x#xs) = h x xs (f xs)"
    by simp

    lemma Abs_map_inverse:
         "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |]
          ==> Rep_map f (Abs_map g M) = M"
    apply (erule list.induct, simp_all)
    apply (insert list_subset_sexp)
    apply (subst Abs_map_CONS, blast)
    apply blast
    apply simp
    done

    (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)

    (** list_case **)

    (* setting up rewrite sets *)

    text{*Better to have a single theorem with a conjunctive conclusion.*}
    declare def_list_rec_NilCons [OF list_case_def, simp]

    (** list_case **)

    lemma expand_list_case:
     "P(list_case a f xs) = ((xs=[] --> P a ) & (!y ys. xs=y#ys --> P(f y ys)))"
    by (induct_tac "xs" rule: list_induct, simp_all)

    (**** Function definitions ****)

    declare def_list_rec_NilCons [OF null_def, simp]
    declare def_list_rec_NilCons [OF hd_def, simp]
    declare def_list_rec_NilCons [OF tl_def, simp]
    declare def_list_rec_NilCons [OF ttl_def, simp]
    declare def_list_rec_NilCons [OF append_def, simp]
    declare def_list_rec_NilCons [OF member_def, simp]
    declare def_list_rec_NilCons [OF map_def, simp]
    declare def_list_rec_NilCons [OF filter_def, simp]
    declare def_list_rec_NilCons [OF list_all_def, simp]

    (** nth **)

    lemma def_nat_rec_0_eta:
        "[| !!n. f == nat_rec c h |] ==> f(0) = c"
    by simp

    lemma def_nat_rec_Suc_eta:
        "[| !!n. f == nat_rec c h |] ==> f(Suc(n)) = h n (f n)"
    by simp

    declare def_nat_rec_0_eta [OF nth_def, simp]
    declare def_nat_rec_Suc_eta [OF nth_def, simp]

    (** length **)

    lemma length_Nil [simp]: "length([]) = 0"
    by (simp add: length_def)

    lemma length_Cons [simp]: "length(a#xs) = Suc(length(xs))"
    by (simp add: length_def)

    (** @ - append **)

    lemma append_assoc [simp]: "(xs@ys)@zs = xs@(ys@zs)"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma append_Nil2 [simp]: "xs @ [] = xs"
    by (induct_tac "xs" rule: list_induct, simp_all)

    (** mem **)

    lemma mem_append [simp]: "x mem (xs@ys) = (x mem xs | x mem ys)"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma mem_filter [simp]: "x mem [x:xs. P x ] = (x mem xs & P(x))"
    by (induct_tac "xs" rule: list_induct, simp_all)

    (** list_all **)

    lemma list_all_True [simp]: "(Alls x:xs. True) = True"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma list_all_conj [simp]:
         "list_all p (xs@ys) = ((list_all p xs) & (list_all p ys))"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma list_all_mem_conv: "(Alls x:xs. P(x)) = (!x. x mem xs --> P(x))"
    apply (induct_tac "xs" rule: list_induct, simp_all)
    apply blast
    done

    lemma nat_case_dist : "(! n. P n) = (P 0 & (! n. P (Suc n)))"
    apply auto
    apply (induct_tac "n", auto)
    done

    lemma alls_P_eq_P_nth: "(Alls u:A. P u) = (!n. n < length A --> P(nth n A))"
    apply (induct_tac "A" rule: list_induct, simp_all)
    apply (rule trans)
    apply (rule_tac [2] nat_case_dist [symmetric], simp_all)
    done

    lemma list_all_imp:
         "[| !x. P x --> Q x;  (Alls x:xs. P(x)) |] ==> (Alls x:xs. Q(x))"
    by (simp add: list_all_mem_conv)

    (** The functional "map" and the generalized functionals **)

    lemma Abs_Rep_map:
         "(!!x. f(x): sexp) ==>
            Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs"
    apply (induct_tac "xs" rule: list_induct)
    apply (simp_all add: Rep_map_type list_sexp [THEN subsetD])
    done

    (** Additional mapping lemmas **)

    lemma map_ident [simp]: "map(%x. x)(xs) = xs"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma map_append [simp]: "map f (xs@ys) = map f xs  @ map f ys"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma map_compose: "map(f o g)(xs) = map f (map g xs)"
    apply (simp add: o_def)
    apply (induct_tac "xs" rule: list_induct, simp_all)
    done

    lemma mem_map_aux1 [rule_format]:
         "x mem (map f q) --> (∃y. y mem q & x = f y)"
    by (induct_tac "q" rule: list_induct, simp_all, blast)

    lemma mem_map_aux2 [rule_format]:
         "(∃y. y mem q & x = f y) --> x mem (map f q)"
    by (induct_tac "q" rule: list_induct, auto)

    lemma mem_map: "x mem (map f q) = (∃y. y mem q & x = f y)"
    apply (rule iffI)
    apply (erule mem_map_aux1)
    apply (erule mem_map_aux2)
    done

    lemma hd_append [rule_format]: "A ~= [] --> hd(A @ B) = hd(A)"
    by (induct_tac "A" rule: list_induct, auto)

    lemma tl_append [rule_format]: "A ~= [] --> tl(A @ B) = tl(A) @ B"
    by (induct_tac "A" rule: list_induct, auto)

    (** take **)

    lemma take_Suc1 [simp]: "take [] (Suc x) = []"
    by simp

    lemma take_Suc2 [simp]: "take(a#xs)(Suc x) = a#take xs x"
    by simp

    (** drop **)

    lemma drop_0 [simp]: "drop xs 0 = xs"
    by (simp add: drop_def)

    lemma drop_Suc1 [simp]: "drop [] (Suc x) = []"
    apply (simp add: drop_def)
    apply (induct_tac "x", auto)
    done

    lemma drop_Suc2 [simp]: "drop(a#xs)(Suc x) = drop xs x"
    by (simp add: drop_def)

    (** copy **)

    lemma copy_0 [simp]: "copy x 0 = []"
    by (simp add: copy_def)

    lemma copy_Suc [simp]: "copy x (Suc y) = x # copy x y"
    by (simp add: copy_def)

    (** fold **)

    lemma foldl_Nil [simp]: "foldl f a [] = a"
    by (simp add: foldl_def)

    lemma foldl_Cons [simp]: "foldl f a(x#xs) = foldl f (f a x) xs"
    by (simp add: foldl_def)

    lemma foldr_Nil [simp]: "foldr f a [] = a"
    by (simp add: foldr_def)

    lemma foldr_Cons [simp]: "foldr f z(x#xs)  = f x (foldr f z xs)"
    by (simp add: foldr_def)

    (** flat **)

    lemma flat_Nil [simp]: "flat [] = []"
    by (simp add: flat_def)

    lemma flat_Cons [simp]: "flat (x # xs) = x @ flat xs"
    by (simp add: flat_def)

    (** rev **)

    lemma rev_Nil [simp]: "rev [] = []"
    by (simp add: rev_def)

    lemma rev_Cons [simp]: "rev (x # xs) = rev xs @ [x]"
    by (simp add: rev_def)

    (** zip **)

    lemma zipWith_Cons_Cons [simp]:
         "zipWith f (a#as,b#bs)   = f(a,b) # zipWith f (as,bs)"
    by (simp add: zipWith_def)

    lemma zipWith_Nil_Nil [simp]: "zipWith f ([],[])      = []"
    by (simp add: zipWith_def)

    lemma zipWith_Cons_Nil [simp]: "zipWith f (x,[])  = []"
    apply (simp add: zipWith_def)
    apply (induct_tac "x" rule: list_induct, simp_all)
    done

    lemma zipWith_Nil_Cons [simp]: "zipWith f ([],x) = []"
    by (simp add: zipWith_def)

    lemma unzip_Nil [simp]: "unzip [] = ([],[])"
    by (simp add: unzip_def)

    (** SOME LIST THEOREMS **)

    (* SQUIGGOL LEMMAS *)

    lemma map_compose_ext: "map(f o g) = ((map f) o (map g))"
    apply (simp add: o_def)
    apply (rule ext)
    apply (simp add: map_compose [symmetric] o_def)
    done

    lemma map_flat: "map f (flat S) = flat(map (map f) S)"
    by (induct_tac "S" rule: list_induct, simp_all)

    lemma list_all_map_eq: "(Alls u:xs. f(u) = g(u)) --> map f xs = map g xs"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma filter_map_d: "filter p (map f xs) = map f (filter(p o f)(xs))"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma filter_compose: "filter p (filter q xs) = filter(%x. p x & q x) xs"
    by (induct_tac "xs" rule: list_induct, simp_all)

    (* "filter(p, filter(q,xs)) = filter(q, filter(p,xs))",
       "filter(p, filter(p,xs)) = filter(p,xs)" BIRD's thms.*)

    lemma filter_append [rule_format, simp]:
         "∀B. filter p (A @ B) = (filter p A @ filter p B)"
    by (induct_tac "A" rule: list_induct, simp_all)

    (* inits(xs) == map(fst,splits(xs)),

       splits([]) = []
       splits(a # xs) = <[],xs> @ map(%x. <a # fst(x),snd(x)>, splits(xs))
       (x @ y = z) = <x,y> mem splits(z)
       x mem xs & y mem ys = <x,y> mem diag(xs,ys) *)

    lemma length_append: "length(xs@ys) = length(xs)+length(ys)"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma length_map: "length(map f xs) = length(xs)"
    by (induct_tac "xs" rule: list_induct, simp_all)

    lemma take_Nil [simp]: "take [] n = []"
    by (induct_tac "n", simp_all)

    lemma take_take_eq [simp]: "∀n. take (take xs n) n = take xs n"
    apply (induct_tac "xs" rule: list_induct, simp_all)
    apply (rule allI)
    apply (induct_tac "n", auto)
    done

    lemma take_take_Suc_eq1 [rule_format]:
         "∀n. take (take xs(Suc(n+m))) n = take xs n"
    apply (induct_tac "xs" rule: list_induct, simp_all)
    apply (rule allI)
    apply (induct_tac "n", auto)
    done

    declare take_Suc [simp del]

    lemma take_take_1: "take (take xs (n+m)) n = take xs n"
    apply (induct_tac "m")
    apply (simp_all add: take_take_Suc_eq1)
    done

    lemma take_take_Suc_eq2 [rule_format]:
         "∀n. take (take xs n)(Suc(n+m)) = take xs n"
    apply (induct_tac "xs" rule: list_induct, simp_all)
    apply (rule allI)
    apply (induct_tac "n", auto)
    done

    lemma take_take_2: "take(take xs n)(n+m) = take xs n"
    apply (induct_tac "m")
    apply (simp_all add: take_take_Suc_eq2)
    done

    (* length(take(xs,n)) = min(n, length(xs)) *)
    (* length(drop(xs,n)) = length(xs) - n *)

    lemma drop_Nil [simp]: "drop  [] n  = []"
    by (induct_tac "n", auto)

    lemma drop_drop [rule_format]: "∀xs. drop (drop xs m) n = drop xs(m+n)"
    apply (induct_tac "m", auto)
    apply (induct_tac "xs" rule: list_induct, auto)
    done

    lemma take_drop [rule_format]: "∀xs. (take xs n) @ (drop xs n) = xs"
    apply (induct_tac "n", auto)
    apply (induct_tac "xs" rule: list_induct, auto)
    done

    lemma copy_copy: "copy x n @ copy x m = copy x (n+m)"
    by (induct_tac "n", auto)

    lemma length_copy: "length(copy x n)  = n"
    by (induct_tac "n", auto)

    lemma length_take [rule_format, simp]:
         "∀xs. length(take xs n) = min (length xs) n"
    apply (induct_tac "n")
     apply auto
    apply (induct_tac "xs" rule: list_induct)
     apply auto
    done

    lemma length_take_drop: "length(take A k) + length(drop A k) = length(A)"
    by (simp only: length_append [symmetric] take_drop)

    lemma take_append [rule_format]: "∀A. length(A) = n --> take(A@B) n = A"
    apply (induct_tac "n")
    apply (rule allI)
    apply (rule_tac [2] allI)
    apply (induct_tac "A" rule: list_induct)
    apply (induct_tac [3] "A" rule: list_induct, simp_all)
    done

    lemma take_append2 [rule_format]:
         "∀A. length(A) = n --> take(A@B) (n+k) = A @ take B k"
    apply (induct_tac "n")
    apply (rule allI)
    apply (rule_tac [2] allI)
    apply (induct_tac "A" rule: list_induct)
    apply (induct_tac [3] "A" rule: list_induct, simp_all)
    done

    lemma take_map [rule_format]: "∀n. take (map f A) n = map f (take A n)"
    apply (induct_tac "A" rule: list_induct, simp_all)
    apply (rule allI)
    apply (induct_tac "n", simp_all)
    done

    lemma drop_append [rule_format]: "∀A. length(A) = n --> drop(A@B)n = B"
    apply (induct_tac "n")
    apply (rule allI)
    apply (rule_tac [2] allI)
    apply (induct_tac "A" rule: list_induct)
    apply (induct_tac [3] "A" rule: list_induct, simp_all)
    done

    lemma drop_append2 [rule_format]:
         "∀A. length(A) = n --> drop(A@B)(n+k) = drop B k"
    apply (induct_tac "n")
    apply (rule allI)
    apply (rule_tac [2] allI)
    apply (induct_tac "A" rule: list_induct)
    apply (induct_tac [3] "A" rule: list_induct, simp_all)
    done

    lemma drop_all [rule_format]: "∀A. length(A) = n --> drop A n = []"
    apply (induct_tac "n")
    apply (rule allI)
    apply (rule_tac [2] allI)
    apply (induct_tac "A" rule: list_induct)
    apply (induct_tac [3] "A" rule: list_induct, auto)
    done

    lemma drop_map [rule_format]: "∀n. drop (map f A) n = map f (drop A n)"
    apply (induct_tac "A" rule: list_induct, simp_all)
    apply (rule allI)
    apply (induct_tac "n", simp_all)
    done

    lemma take_all [rule_format]: "∀A. length(A) = n --> take A n = A"
    apply (induct_tac "n")
    apply (rule allI)
    apply (rule_tac [2] allI)
    apply (induct_tac "A" rule: list_induct)
    apply (induct_tac [3] "A" rule: list_induct, auto)
    done

    lemma foldl_single: "foldl f a [b] = f a b"
    by simp_all

    lemma foldl_append [rule_format, simp]:
         "∀a. foldl f a (A @ B) = foldl f (foldl f a A) B"
    by (induct_tac "A" rule: list_induct, simp_all)

    lemma foldl_map [rule_format]:
         "∀e. foldl f e (map g S) = foldl (%x y. f x (g y)) e S"
    by (induct_tac "S" rule: list_induct, simp_all)

    lemma foldl_neutr_distr [rule_format]:
      assumes r_neutr: "∀a. f a e = a"
          and r_neutl: "∀a. f e a = a"
          and assoc:   "∀a b c. f a (f b c) = f(f a b) c"
      shows "∀y. f y (foldl f e A) = foldl f y A"
    apply (induct_tac "A" rule: list_induct)
    apply (simp_all add: r_neutr r_neutl, clarify)
    apply (erule all_dupE)
    apply (rule trans)
    prefer 2 apply assumption
    apply (simp (no_asm_use) add: assoc [THEN spec, THEN spec, THEN spec, THEN sym])
    apply simp
    done

    lemma foldl_append_sym:
    "[| !a. f a e = a; !a. f e a = a;
        !a b c. f a (f b c) = f(f a b) c |]
      ==> foldl f e (A @ B) = f(foldl f e A)(foldl f e B)"
    apply (rule trans)
    apply (rule foldl_append)
    apply (rule sym)
    apply (rule foldl_neutr_distr, auto)
    done

    lemma foldr_append [rule_format, simp]:
         "∀a. foldr f a (A @ B) = foldr f (foldr f a B) A"
    apply (induct_tac "A" rule: list_induct, simp_all)
    done

    lemma foldr_map [rule_format]: "∀e. foldr f e (map g S) = foldr (f o g) e S"
    apply (simp add: o_def)
    apply (induct_tac "S" rule: list_induct, simp_all)
    done

    lemma foldr_Un_eq_UN: "foldr op Un {} S = (UN X: {t. t mem S}.X)"
    by (induct_tac "S" rule: list_induct, auto)

    lemma foldr_neutr_distr:
         "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |]
          ==> foldr f y S = f (foldr f e S) y"
    by (induct_tac "S" rule: list_induct, auto)

    lemma foldr_append2:
        "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |]
         ==> foldr f e (A @ B) = f (foldr f e A) (foldr f e B)"
    apply auto
    apply (rule foldr_neutr_distr, auto)
    done

    lemma foldr_flat:
        "[| !a. f e a = a; !a b c. f a (f b c) = f(f a b) c |] ==>
          foldr f e (flat S) = (foldr f e)(map (foldr f e) S)"
    apply (induct_tac "S" rule: list_induct)
    apply (simp_all del: foldr_append add: foldr_append2)
    done

    lemma list_all_map: "(Alls x:map f xs .P(x)) = (Alls x:xs.(P o f)(x))"
    by (induct_tac "xs" rule: list_induct, auto)

    lemma list_all_and:
         "(Alls x:xs. P(x)&Q(x)) = ((Alls x:xs. P(x))&(Alls x:xs. Q(x)))"
    by (induct_tac "xs" rule: list_induct, auto)

    lemma nth_map [rule_format]:
         "∀i. i < length(A)  --> nth i (map f A) = f(nth i A)"
    apply (induct_tac "A" rule: list_induct, simp_all)
    apply (rule allI)
    apply (induct_tac "i", auto)
    done

    lemma nth_app_cancel_right [rule_format]:
         "∀i. i < length(A)  --> nth i(A@B) = nth i A"
    apply (induct_tac "A" rule: list_induct, simp_all)
    apply (rule allI)
    apply (induct_tac "i", simp_all)
    done

    lemma nth_app_cancel_left [rule_format]:
         "∀n. n = length(A) --> nth(n+i)(A@B) = nth i B"
    by (induct_tac "A" rule: list_induct, simp_all)

    (** flat **)

    lemma flat_append [simp]: "flat(xs@ys) = flat(xs) @ flat(ys)"
    by (induct_tac "xs" rule: list_induct, auto)

    lemma filter_flat: "filter p (flat S) = flat(map (filter p) S)"
    by (induct_tac "S" rule: list_induct, auto)

    (** rev **)

    lemma rev_append [simp]: "rev(xs@ys) = rev(ys) @ rev(xs)"
    by (induct_tac "xs" rule: list_induct, auto)

    lemma rev_rev_ident [simp]: "rev(rev l) = l"
    by (induct_tac "l" rule: list_induct, auto)

    lemma rev_flat: "rev(flat ls) = flat (map rev (rev ls))"
    by (induct_tac "ls" rule: list_induct, auto)

    lemma rev_map_distrib: "rev(map f l) = map f (rev l)"
    by (induct_tac "l" rule: list_induct, auto)

    lemma foldl_rev: "foldl f b (rev l) = foldr (%x y. f y x) b l"
    by (induct_tac "l" rule: list_induct, auto)

    lemma foldr_rev: "foldr f b (rev l) = foldl (%x y. f y x) b l"
    apply (rule sym)
    apply (rule trans)
    apply (rule_tac [2] foldl_rev, simp)
    done

    end

lemma ListI:

      x ∈ list (range Leaf) ==> x ∈ List

lemma ListD:

      x ∈ List ==> x ∈ list (range Leaf)

lemma list_unfold:

      list A = usum {Numb 0} (uprod A (list A))

lemma list_mono:

      A ⊆ B ==> list A ⊆ list B

lemma list_sexp:

      list sexp ⊆ sexp

lemmas list_subset_sexp:

      A2 ⊆ sexp ==> list A2 ⊆ sexp

lemmas list_subset_sexp:

      A2 ⊆ sexp ==> list A2 ⊆ sexp

lemma list_induct:

      [| P []; !!x xs. P xs ==> P (x # xs) |] ==> P l

lemma inj_on_Abs_list:

      inj_on Abs_List (list (range Leaf))

lemma CONS_not_NIL:

      CONS M N ≠ NIL

lemmas NIL_not_CONS:

      NIL ≠ CONS M1 N1

lemmas NIL_not_CONS:

      NIL ≠ CONS M1 N1

lemmas CONS_neq_NIL:

      CONS M N = NIL ==> R

lemmas CONS_neq_NIL:

      CONS M N = NIL ==> R

lemmas NIL_neq_CONS:

      NIL = CONS M N ==> R

lemmas NIL_neq_CONS:

      NIL = CONS M N ==> R

lemma Cons_not_Nil:

      x # xs ≠ []

lemmas Nil_not_Cons:

      [] ≠ x # xs

lemmas Nil_not_Cons:

      [] ≠ x # xs

lemmas Cons_neq_Nil:

      x # xs = [] ==> R

lemmas Cons_neq_Nil:

      x # xs = [] ==> R

lemmas Nil_neq_Cons:

      [] = x # xs ==> R

lemmas Nil_neq_Cons:

      [] = x # xs ==> R

lemma CONS_CONS_eq:

      (CONS K M = CONS L N) = (K = L ∧ M = N)

lemma Cons_Cons_eq:

      (x # xs = y # ys) = (x = y ∧ xs = ys)

lemmas Cons_inject2:

      [| x # xs = y # ys; [| x = y; xs = ys |] ==> R |] ==> R

lemmas Cons_inject2:

      [| x # xs = y # ys; [| x = y; xs = ys |] ==> R |] ==> R

lemma CONS_D:

      CONS M N ∈ list A ==> M ∈ A ∧ N ∈ list A

lemma sexp_CONS_D:

      CONS M N ∈ sexp ==> M ∈ sexp ∧ N ∈ sexp

lemma not_CONS_self:

      N ∈ list A ==> ∀M. N ≠ CONS M N

lemma not_Cons_self2:

      ∀x. l ≠ x # l

lemma neq_Nil_conv2:

      (xs ≠ []) = (∃y ys. xs = y # ys)

lemma List_case_NIL:

      List_case c h NIL = c

lemma List_case_CONS:

      List_case c h (CONS M N) = h M N

lemma List_rec_unfold_lemma:

      %M. List_rec M c d == wfrec (pred_sexp+) (%g. List_case c (%x y. d x y (g y)))

lemmas List_rec_unfold:

      List_rec a c d =
      List_case c (%x y. d x y (cut (%M. List_rec M c d) (pred_sexp+) a y)) a

lemmas List_rec_unfold:

      List_rec a c d =
      List_case c (%x y. d x y (cut (%M. List_rec M c d) (pred_sexp+) a y)) a

lemma pred_sexp_CONS_I1:

      [| M ∈ sexp; N ∈ sexp |] ==> (M, CONS M N) ∈ pred_sexp+

lemma pred_sexp_CONS_I2:

      [| M ∈ sexp; N ∈ sexp |] ==> (N, CONS M N) ∈ pred_sexp+

lemma pred_sexp_CONS_D:

      (CONS M1.0 M2.0, N) ∈ pred_sexp+
      ==> (M1.0, N) ∈ pred_sexp+ ∧ (M2.0, N) ∈ pred_sexp+

lemma List_rec_NIL:

      List_rec NIL c h = c

lemma List_rec_CONS:

      [| M ∈ sexp; N ∈ sexp |] ==> List_rec (CONS M N) c h = h M N (List_rec N c h)

lemmas Rep_List_in_sexp:

      Rep_List x2 ∈ sexp

lemmas Rep_List_in_sexp:

      Rep_List x2 ∈ sexp

lemma list_rec_Nil:

      list_rec [] c h = c

lemma list_rec_Cons:

      list_rec (a # l) c h = h a l (list_rec l c h)

lemma List_rec_type:

      [| M ∈ list A; A ⊆ sexp; c ∈ C NIL;
         !!x y r. [| x ∈ A; y ∈ list A; r ∈ C y |] ==> h x y r ∈ C (CONS x y) |]
      ==> List_rec M c h ∈ C M

lemma Rep_map_Nil:

      Rep_map f [] = NIL

lemma Rep_map_Cons:

      Rep_map f (x # xs) = CONS (f x) (Rep_map f xs)

lemma Rep_map_type:

      (!!x. f x ∈ A) ==> Rep_map f xs ∈ list A

lemma Abs_map_NIL:

      Abs_map g NIL = []

lemma Abs_map_CONS:

      [| M ∈ sexp; N ∈ sexp |] ==> Abs_map g (CONS M N) = g M # Abs_map g N

lemma def_list_rec_NilCons:

      (!!xs. f xs == list_rec xs c h) ==> f [] = c ∧ f (x # xs) = h x xs (f xs)

lemma Abs_map_inverse:

      [| M ∈ list A; A ⊆ sexp; !!z. z ∈ A ==> f (g z) = z |]
      ==> Rep_map f (Abs_map g M) = M

lemma expand_list_case:

      P (list_case a f xs) = ((xs = [] --> P a) ∧ (∀y ys. xs = y # ys --> P (f y ys)))

lemma def_nat_rec_0_eta:

      (!!n. f == nat_rec c h) ==> f 0 = c

lemma def_nat_rec_Suc_eta:

      (!!n. f == nat_rec c h) ==> f (Suc n) = h n (f n)

lemma length_Nil:

      length [] = 0

lemma length_Cons:

      length (a # xs) = Suc (length xs)

lemma append_assoc:

      (xs @ ys) @ zs = xs @ ys @ zs

lemma append_Nil2:

      xs @ [] = xs

lemma mem_append:

      x mem xs @ ys = (x mem xs ∨ x mem ys)

lemma mem_filter:

      x mem filter P xs = (x mem xs ∧ P x)

lemma list_all_True:

      (Alls x:xs. True) = True

lemma list_all_conj:

      list_all p (xs @ ys) = (list_all p xs ∧ list_all p ys)

lemma list_all_mem_conv:

      list_all P xs = (∀x. x mem xs --> P x)

lemma nat_case_dist:

      (∀n. P n) = (P 0 ∧ (∀n. P (Suc n)))

lemma alls_P_eq_P_nth:

      list_all P A = (∀n<length A. P (nth n A))

lemma list_all_imp:

      [| ∀x. P x --> Q x; list_all P xs |] ==> list_all Q xs

lemma Abs_Rep_map:

      (!!x. f x ∈ sexp) ==> Abs_map g (Rep_map f xs) = map (%t. g (f t)) xs

lemma map_ident:

      map (%x. x) xs = xs

lemma map_append:

      map f (xs @ ys) = map f xs @ map f ys

lemma map_compose:

      map (f o g) xs = map f (map g xs)

lemma mem_map_aux1:

      x mem map f q ==> ∃y. y mem q ∧ x = f y

lemma mem_map_aux2:

      ∃y. y mem q ∧ x = f y ==> x mem map f q

lemma mem_map:

      x mem map f q = (∃y. y mem q ∧ x = f y)

lemma hd_append:

      A ≠ [] ==> hd (A @ B) = hd A

lemma tl_append:

      A ≠ [] ==> tl (A @ B) = tl A @ B

lemma take_Suc1:

      take [] (Suc x) = []

lemma take_Suc2:

      take (a # xs) (Suc x) = a # take xs x

lemma drop_0:

      drop xs 0 = xs

lemma drop_Suc1:

      drop [] (Suc x) = []

lemma drop_Suc2:

      drop (a # xs) (Suc x) = drop xs x

lemma copy_0:

      copy x 0 = []

lemma copy_Suc:

      copy x (Suc y) = x # copy x y

lemma foldl_Nil:

      foldl f a [] = a

lemma foldl_Cons:

      foldl f a (x # xs) = foldl f (f a x) xs

lemma foldr_Nil:

      foldr f a [] = a

lemma foldr_Cons:

      foldr f z (x # xs) = f x (foldr f z xs)

lemma flat_Nil:

      flat [] = []

lemma flat_Cons:

      flat (x # xs) = x @ flat xs

lemma rev_Nil:

      rev [] = []

lemma rev_Cons:

      rev (x # xs) = rev xs @ [x]

lemma zipWith_Cons_Cons:

      zipWith f (a # as, b # bs) = f (a, b) # zipWith f (as, bs)

lemma zipWith_Nil_Nil:

      zipWith f ([], []) = []

lemma zipWith_Cons_Nil:

      zipWith f (x, []) = []

lemma zipWith_Nil_Cons:

      zipWith f ([], x) = []

lemma unzip_Nil:

      unzip [] = ([], [])

lemma map_compose_ext:

      map (f o g) = map f o map g

lemma map_flat:

      map f (flat S) = flat (map (map f) S)

lemma list_all_map_eq:

      (Alls u:xs. f u = g u) --> map f xs = map g xs

lemma filter_map_d:

      filter p (map f xs) = map f (filter (p o f) xs)

lemma filter_compose:

      filter p (filter q xs) = [x:xs . p x ∧ q x]

lemma filter_append:

      filter p (A @ B) = filter p A @ filter p B

lemma length_append:

      length (xs @ ys) = length xs + length ys

lemma length_map:

      length (map f xs) = length xs

lemma take_Nil:

      take [] n = []

lemma take_take_eq:

      ∀n. take (take xs n) n = take xs n

lemma take_take_Suc_eq1:

      take (take xs (Suc (n + m))) n = take xs n

lemma take_take_1:

      take (take xs (n + m)) n = take xs n

lemma take_take_Suc_eq2:

      take (take xs n) (Suc (n + m)) = take xs n

lemma take_take_2:

      take (take xs n) (n + m) = take xs n

lemma drop_Nil:

      drop [] n = []

lemma drop_drop:

      drop (drop xs m) n = drop xs (m + n)

lemma take_drop:

      take xs n @ drop xs n = xs

lemma copy_copy:

      copy x n @ copy x m = copy x (n + m)

lemma length_copy:

      length (copy x n) = n

lemma length_take:

      length (take xs n) = min (length xs) n

lemma length_take_drop:

      length (take A k) + length (drop A k) = length A

lemma take_append:

      length A = n ==> take (A @ B) n = A

lemma take_append2:

      length A = n ==> take (A @ B) (n + k) = A @ take B k

lemma take_map:

      take (map f A) n = map f (take A n)

lemma drop_append:

      length A = n ==> drop (A @ B) n = B

lemma drop_append2:

      length A = n ==> drop (A @ B) (n + k) = drop B k

lemma drop_all:

      length A = n ==> drop A n = []

lemma drop_map:

      drop (map f A) n = map f (drop A n)

lemma take_all:

      length A = n ==> take A n = A

lemma foldl_single:

      foldl f a [b] = f a b

lemma foldl_append:

      foldl f a (A @ B) = foldl f (foldl f a A) B

lemma foldl_map:

      foldl f e (map g S) = foldl (%x y. f x (g y)) e S

lemma foldl_neutr_distr:

      [| ∀a. f a e = a; ∀a. f e a = a; ∀a b c. f a (f b c) = f (f a b) c |]
      ==> ∀y. f y (foldl f e A) = foldl f y A

lemma foldl_append_sym:

      [| ∀a. f a e = a; ∀a. f e a = a; ∀a b c. f a (f b c) = f (f a b) c |]
      ==> foldl f e (A @ B) = f (foldl f e A) (foldl f e B)

lemma foldr_append:

      foldr f a (A @ B) = foldr f (foldr f a B) A

lemma foldr_map:

      foldr f e (map g S) = foldr (f o g) e S

lemma foldr_Un_eq_UN:

      foldr op ∪ {} S = (UN X:{t. t mem S}. X)

lemma foldr_neutr_distr:

      [| ∀a. f e a = a; ∀a b c. f a (f b c) = f (f a b) c |]
      ==> foldr f y S = f (foldr f e S) y

lemma foldr_append2:

      [| ∀a. f e a = a; ∀a b c. f a (f b c) = f (f a b) c |]
      ==> foldr f e (A @ B) = f (foldr f e A) (foldr f e B)

lemma foldr_flat:

      [| ∀a. f e a = a; ∀a b c. f a (f b c) = f (f a b) c |]
      ==> foldr f e (flat S) = foldr f e (map (foldr f e) S)

lemma list_all_map:

      list_all P (map f xs) = list_all (P o f) xs

lemma list_all_and:

      (Alls x:xs. P x ∧ Q x) = (list_all P xs ∧ list_all Q xs)

lemma nth_map:

      i < length A ==> nth i (map f A) = f (nth i A)

lemma nth_app_cancel_right:

      i < length A ==> nth i (A @ B) = nth i A

lemma nth_app_cancel_left:

      n = length A ==> nth (n + i) (A @ B) = nth i B

lemma flat_append:

      flat (xs @ ys) = flat xs @ flat ys

lemma filter_flat:

      filter p (flat S) = flat (map (filter p) S)

lemma rev_append:

      rev (xs @ ys) = rev ys @ rev xs

lemma rev_rev_ident:

      rev (rev l) = l

lemma rev_flat:

      rev (flat ls) = flat (map rev (rev ls))

lemma rev_map_distrib:

      rev (map f l) = map f (rev l)

lemma foldl_rev:

      foldl f b (rev l) = foldr (%x y. f y x) b l

lemma foldr_rev:

      foldr f b (rev l) = foldl (%x y. f y x) b l