bugfix concerning claset(), added limited support for ALLGOALS + fast_tac etc.
(* Title: ZF/List.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
Datatype definition of Lists
*)
(*** Aspects of the datatype definition ***)
(*An elimination rule, for type-checking*)
bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)");
(*Proving freeness results*)
bind_thm ("Cons_iff", list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'");
bind_thm ("Nil_Cons_iff", list.mk_free "~ Nil=Cons(a,l)");
Goal "list(A) = {0} + (A * list(A))";
by (blast_tac (claset() addSIs (map (rewrite_rule list.con_defs) list.intrs)
addEs [rewrite_rule list.con_defs list.elim]) 1);
qed "list_unfold";
(** Lemmas to justify using "list" in other recursive type definitions **)
Goalw list.defs "A<=B ==> list(A) <= list(B)";
by (rtac lfp_mono 1);
by (REPEAT (rtac list.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
qed "list_mono";
(*There is a similar proof by list induction.*)
Goalw (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
by (blast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
Pair_in_univ]) 1);
qed "list_univ";
(*These two theorems justify datatypes involving list(nat), list(A), ...*)
bind_thm ("list_subset_univ", [list_mono, list_univ] MRS subset_trans);
Goal "[| l: list(A); A <= univ(B) |] ==> l: univ(B)";
by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
qed "list_into_univ";
val major::prems = Goal
"[| 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 (rtac (major RS list.induct) 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "list_case_type";
(*** List functions ***)
Goal "l: list(A) ==> tl(l) : list(A)";
by (exhaust_tac "l" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs)));
qed "tl_type";
(** drop **)
Goal "i:nat ==> drop(i, Nil) = Nil";
by (induct_tac "i" 1);
by (ALLGOALS Asm_simp_tac);
qed "drop_Nil";
Goal "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
by (rtac sym 1);
by (induct_tac "i" 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "drop_succ_Cons";
Addsimps [drop_Nil, drop_succ_Cons];
Goal "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
by (induct_tac "i" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
qed "drop_type";
Delsimps [drop_SUCC];
(** Type checking -- proved by induction, as usual **)
val prems = Goal
"[| 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 (cut_facts_tac prems 1);
by (induct_tac "l" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "list_rec_type";
(** map **)
val prems = Goalw [thm "map_list_def"]
"[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
qed "map_type";
Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})";
by (etac map_type 1);
by (etac RepFunI 1);
qed "map_type2";
(** length **)
Goalw [thm "length_list_def"]
"l: list(A) ==> length(l) : nat";
by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
qed "length_type";
(** app **)
Goalw [thm "op @_list_def"]
"[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)";
by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
qed "app_type";
(** rev **)
Goalw [thm "rev_list_def"]
"xs: list(A) ==> rev(xs) : list(A)";
by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
qed "rev_type";
(** flat **)
Goalw [thm "flat_list_def"]
"ls: list(list(A)) ==> flat(ls) : list(A)";
by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
qed "flat_type";
(** set_of_list **)
Goalw [thm "set_of_list_list_def"]
"l: list(A) ==> set_of_list(l) : Pow(A)";
by (etac list_rec_type 1);
by (ALLGOALS (Blast_tac));
qed "set_of_list_type";
Goal "xs: list(A) ==> \
\ set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)";
by (etac list.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
qed "set_of_list_append";
(** list_add **)
Goalw [thm "list_add_list_def"]
"xs: list(nat) ==> list_add(xs) : nat";
by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
qed "list_add_type";
bind_thms ("list_typechecks",
list.intrs @
[list_rec_type, map_type, map_type2, app_type, length_type,
rev_type, flat_type, list_add_type]);
AddTCs list_typechecks;
(*** theorems about map ***)
Goal "l: list(A) ==> map(%u. u, l) = l";
by (induct_tac "l" 1);
by (ALLGOALS Asm_simp_tac);
qed "map_ident";
Addsimps [map_ident];
Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
by (induct_tac "l" 1);
by (ALLGOALS Asm_simp_tac);
qed "map_compose";
Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "map_app_distrib";
Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
by (induct_tac "ls" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
qed "map_flat";
Goal "l: list(A) ==> \
\ list_rec(c, d, map(h,l)) = \
\ list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)";
by (induct_tac "l" 1);
by (ALLGOALS Asm_simp_tac);
qed "list_rec_map";
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
(* c : list(Collect(B,P)) ==> c : list(B) *)
bind_thm ("list_CollectD", Collect_subset RS list_mono RS subsetD);
Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
by (induct_tac "l" 1);
by (ALLGOALS Asm_simp_tac);
qed "map_list_Collect";
(*** theorems about length ***)
Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "length_map";
Goal "[| xs: list(A); ys: list(A) |] \
\ ==> length(xs@ys) = length(xs) #+ length(ys)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "length_app";
Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
by (induct_tac "xs" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
qed "length_rev";
Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
by (induct_tac "ls" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
qed "length_flat";
(** Length and drop **)
(*Lemma for the inductive step of drop_length*)
Goal "xs: list(A) ==> \
\ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
qed_spec_mp "drop_length_Cons";
Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
by Safe_tac;
by (etac drop_length_Cons 1);
by (rtac natE 1);
by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
by (assume_tac 1);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (blast_tac (claset() addIs [succ_in_naturalD, length_type])));
qed_spec_mp "drop_length";
(*** theorems about app ***)
Goal "xs: list(A) ==> xs@Nil=xs";
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "app_right_Nil";
Addsimps [app_right_Nil];
Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "app_assoc";
Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
by (induct_tac "ls" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
qed "flat_app_distrib";
(*** theorems about rev ***)
Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
by (induct_tac "l" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
qed "rev_map_distrib";
(*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.
*)
Goal "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
by (etac list.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
qed "rev_app_distrib";
Goal "l: list(A) ==> rev(rev(l))=l";
by (induct_tac "l" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
qed "rev_rev_ident";
Addsimps [rev_rev_ident];
Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
by (induct_tac "ls" 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps
[map_app_distrib, flat_app_distrib, rev_app_distrib])));
qed "rev_flat";
(*** theorems about list_add ***)
Goal "[| xs: list(nat); ys: list(nat) |] ==> \
\ list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
by (induct_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "list_add_app";
Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
by (induct_tac "l" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
qed "list_add_rev";
Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
by (induct_tac "ls" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
qed "list_add_flat";
(** New induction rule **)
val major::prems = Goal
"[| l: list(A); \
\ P(Nil); \
\ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \
\ |] ==> P(l)";
by (rtac (major RS rev_rev_ident RS subst) 1);
by (rtac (major RS rev_type RS list.induct) 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
qed "list_append_induct";
(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
(** min **)
(* Min theorems are also true for i, j ordinals *)
Goalw [min_def] "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)";
by (auto_tac (claset() addSDs [not_lt_imp_le]
addDs [lt_not_sym]
addIs [le_anti_sym], simpset()));
qed "min_sym";
Goalw [min_def] "[| i:nat; j:nat |] ==> min(i,j):nat";
by Auto_tac;
qed "min_type";
AddTCs [min_type];
Addsimps [min_type];
Goalw [min_def] "i:nat ==> min(0,i) = 0";
by (auto_tac (claset() addDs [not_lt_imp_le], simpset()));
qed "min_0";
Addsimps [min_0];
Goalw [min_def] "i:nat ==> min(i, 0) = 0";
by (auto_tac (claset() addDs [not_lt_imp_le], simpset()));
qed "min_02";
Addsimps [min_02];
Goalw [min_def] "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k";
by (auto_tac (claset() addSDs [not_lt_imp_le]
addIs [lt_trans2, lt_trans], simpset()));
qed "lt_min_iff";
Goalw [min_def]
"[| i:nat; j:nat |] ==> min(succ(i), succ(j))= succ(min(i, j))";
by Auto_tac;
qed "min_succ_succ";
Addsimps [min_succ_succ];
(*** more theorems about lists ***)
Goal "xs:list(A) ==> (xs~=Nil)<->(EX y:A. EX ys:list(A). xs=Cons(y,ys))";
by (induct_tac "xs" 1);
by Auto_tac;
qed "neq_Nil_iff";
(** filter **)
Goal "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "filter_append";
Addsimps [filter_append];
Goal "xs:list(A) ==> filter(P, xs):list(A)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "filter_type";
Goal "xs:list(A) ==> length(filter(P, xs)) le length(xs)";
by (induct_tac "xs" 1);
by Auto_tac;
by (res_inst_tac [("j", "length(l)")] le_trans 1);
by (auto_tac (claset(), simpset() addsimps [le_iff]));
qed "length_filter";
Goal "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)";
by (induct_tac "xs" 1);
by Auto_tac;
qed "filter_is_subset";
Goal "xs:list(A) ==> filter(%p. False, xs) = Nil";
by (induct_tac "xs" 1);
by Auto_tac;
qed "filter_False";
Goal "xs:list(A) ==> filter(%p. True, xs) = xs";
by (induct_tac "xs" 1);
by Auto_tac;
qed "filter_True";
Addsimps [filter_False, filter_True];
(** length **)
Goal "xs:list(A) ==> length(xs)=0 <-> xs=Nil";
by (etac list.induct 1);
by Auto_tac;
qed "length_is_0_iff";
Addsimps [length_is_0_iff];
Goal "xs:list(A) ==> 0 = length(xs) <-> xs=Nil";
by (etac list.induct 1);
by Auto_tac;
qed "length_is_0_iff2";
Addsimps [length_is_0_iff2];
Goal "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1";
by (etac list.induct 1);
by Auto_tac;
qed "length_tl";
Addsimps [length_tl];
Goal "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil";
by (etac list.induct 1);
by Auto_tac;
qed "length_greater_0_iff";
Goal "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)";
by (etac list.induct 1);
by Auto_tac;
qed "length_succ_iff";
(** more theorems about append **)
Goal "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)";
by (etac list.induct 1);
by Auto_tac;
qed "append_is_Nil_iff";
Addsimps [append_is_Nil_iff];
Goal "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)";
by (etac list.induct 1);
by Auto_tac;
qed "append_is_Nil_iff2";
Addsimps [append_is_Nil_iff2];
Goal "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)";
by (etac list.induct 1);
by Auto_tac;
qed "append_left_is_self_iff";
Addsimps [append_left_is_self_iff];
Goal "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)";
by (etac list.induct 1);
by Auto_tac;
qed "append_left_is_self_iff2";
Addsimps [append_left_is_self_iff2];
Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
\ length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))";
by (etac list.induct 1);
by (auto_tac (claset(), simpset() addsimps [length_app]));
qed_spec_mp "append_left_is_Nil_iff";
Addsimps [append_left_is_Nil_iff];
Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
\ length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))";
by (etac list.induct 1);
by (auto_tac (claset(), simpset() addsimps [length_app]));
qed_spec_mp "append_left_is_Nil_iff2";
Addsimps [append_left_is_Nil_iff2];
Goal "xs:list(A) ==> ALL ys:list(A). \
\ length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)";
by (etac list.induct 1);
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (eres_inst_tac [("a", "ys")] list.elim 1);
by (ALLGOALS(Asm_full_simp_tac));
qed_spec_mp "append_eq_append_iff";
Goal "xs:list(A) ==> \
\ ALL ys:list(A). ALL us:list(A). ALL vs:list(A). \
\ length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)";
by (induct_tac "xs" 1);
by (ALLGOALS(Clarify_tac));
by (asm_full_simp_tac (simpset() addsimps [length_app]) 1);
by (eres_inst_tac [("a", "ys")] list.elim 1);
by (Asm_full_simp_tac 1);
by (subgoal_tac "Cons(a, l) @ us =vs" 1);
by (dtac (rotate_prems 4 (append_left_is_Nil_iff RS iffD1)) 1);
by Auto_tac;
qed_spec_mp "append_eq_append";
Goal "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |] \
\ ==> xs@us = ys@vs <-> (xs=ys & us=vs)";
by (rtac iffI 1);
by (rtac append_eq_append 1);
by Auto_tac;
qed "append_eq_append_iff2";
Addsimps [append_eq_append_iff, append_eq_append_iff2];
Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs";
by (Asm_simp_tac 1);
qed "append_self_iff";
Addsimps [append_self_iff];
Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs";
by (Asm_simp_tac 1);
qed "append_self_iff2";
Addsimps [append_self_iff2];
(* Can also be proved from append_eq_append_iff2,
but the proof requires two more hypotheses: x:A and y:A *)
Goal "xs:list(A) ==> ALL ys:list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)";
by (etac list.induct 1);
by (ALLGOALS(Clarify_tac));
by (ALLGOALS(eres_inst_tac [("a", "ys")] list.elim));
by Auto_tac;
qed_spec_mp "append1_eq_iff";
Addsimps [append1_eq_iff];
Goal "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)";
by (Asm_simp_tac 1);
qed "append_right_is_self_iff";
Addsimps [append_right_is_self_iff];
Goal "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)";
by (rtac iffI 1);
by (dtac sym 1);
by (ALLGOALS(Asm_full_simp_tac));
qed "append_right_is_self_iff2";
Addsimps [append_right_is_self_iff2];
Goal "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)";
by (induct_tac "xs" 1);
by Auto_tac;
qed_spec_mp "hd_append";
Addsimps [hd_append];
Goal "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys";
by (induct_tac "xs" 1);
by Auto_tac;
qed_spec_mp "tl_append";
Addsimps [tl_append];
(** rev **)
Goal "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)";
by (etac list.induct 1);
by Auto_tac;
qed "rev_is_Nil_iff";
Addsimps [rev_is_Nil_iff];
Goal "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)";
by (etac list.induct 1);
by Auto_tac;
qed "Nil_is_rev_iff";
Addsimps [Nil_is_rev_iff];
Goal "xs:list(A) ==> ALL ys:list(A). rev(xs)=rev(ys) <-> xs=ys";
by (etac list.induct 1);
by (Force_tac 1);
by (Clarify_tac 1);
by (eres_inst_tac [("a", "ys")] list.elim 1);
by Auto_tac;
qed_spec_mp "rev_is_rev_iff";
Addsimps [rev_is_rev_iff];
Goal "xs:list(A) ==> \
\ (xs=Nil --> P) --> (ALL ys:list(A). ALL y:A. xs =ys@[y] -->P)-->P";
by (etac list_append_induct 1);
by Auto_tac;
qed_spec_mp "rev_list_elim_aux";
bind_thm("rev_list_elim", impI RS ballI RS ballI RSN(3, rev_list_elim_aux));
(** more theorems about drop **)
Goal "n:nat ==> ALL xs:list(A). length(drop(n, xs)) = length(xs) #- n";
by (etac nat_induct 1);
by (auto_tac (claset() addEs [list.elim], simpset()));
qed_spec_mp "length_drop";
Addsimps [length_drop];
Goal "n:nat ==> ALL xs:list(A). length(xs) le n --> drop(n, xs)=Nil";
by (etac nat_induct 1);
by (auto_tac (claset() addEs [list.elim], simpset()));
qed_spec_mp "drop_all";
Addsimps [drop_all];
Goal "n:nat ==> ALL xs:list(A). drop(n, xs@ys) = \
\ drop(n,xs) @ drop(n #- length(xs), ys)";
by (induct_tac "n" 1);
by (auto_tac (claset() addEs [list.elim], simpset()));
qed_spec_mp "drop_append";
Goal "m:nat ==> \
\ ALL xs:list(A). ALL n:nat. drop(n, drop(m, xs))=drop(n #+ m, xs)";
by (induct_tac "m" 1);
by (auto_tac (claset() addEs [list.elim], simpset()));
qed "drop_drop";
(** take **)
Goalw [take_def]
"xs:list(A) ==> take(0, xs) = Nil";
by (etac list.induct 1);
by Auto_tac;
qed "take_0";
Addsimps [take_0];
Goalw [take_def]
"n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))";
by (Asm_simp_tac 1);
qed "take_succ_Cons";
Addsimps [take_succ_Cons];
(* Needed for proving take_all *)
Goalw [take_def]
"n:nat ==> take(n, Nil) = Nil";
by Auto_tac;
qed "take_Nil";
Addsimps [take_Nil];
Goal "n:nat ==> ALL xs:list(A). length(xs) le n --> take(n, xs) = xs";
by (etac nat_induct 1);
by (auto_tac (claset() addEs [list.elim], simpset()));
qed_spec_mp "take_all";
Addsimps [take_all];
Goal "xs:list(A) ==> ALL n:nat. take(n, xs):list(A)";
by (etac list.induct 1);
by (Clarify_tac 2);
by (etac natE 2);
by Auto_tac;
qed_spec_mp "take_type";
Goal "xs:list(A) ==> \
\ ALL ys:list(A). ALL n:nat. take(n, xs @ ys) = \
\ take(n, xs) @ take(n #- length(xs), ys)";
by (etac list.induct 1);
by (Clarify_tac 2);
by (etac natE 2);
by Auto_tac;
qed_spec_mp "take_append";
Addsimps [take_append];
Goal
"m:nat ==> \
\ ALL xs:list(A). ALL n:nat. take(n, take(m,xs))= take(min(n, m), xs)";
by (induct_tac "m" 1);
by Auto_tac;
by (eres_inst_tac [("a", "xs")] list.elim 1);
by (auto_tac (claset(), simpset() addsimps [take_Nil]));
by (rotate_tac 1 1);
by (etac natE 1);
by (auto_tac (claset() addIs [take_0, take_type], simpset()));
qed_spec_mp "take_take";
(** nth **)
Goalw [nth_def] "nth(0, Cons(a, l))= a";
by Auto_tac;
qed "nth_0";
Addsimps [nth_0];
Goalw [nth_def]
"n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)";
by (Asm_simp_tac 1);
qed "nth_Cons";
Addsimps [nth_Cons];
Goal "xs:list(A) ==> ALL n:nat. n < length(xs) --> nth(n, xs):A";
by (etac list.induct 1);
by (ALLGOALS(Clarify_tac));
by (etac natE 2);
by (ALLGOALS(Asm_full_simp_tac));
qed_spec_mp "nth_type";
AddTCs [nth_type];
Addsimps [nth_type];
Goal
"xs:list(A) ==> ALL n:nat. \
\ nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) \
\ else nth(n #- length(xs),ys))";
by (induct_tac "xs" 1);
by (Clarify_tac 2);
by (etac natE 2);
by (ALLGOALS(Asm_full_simp_tac));
qed_spec_mp "nth_append";
Goal "xs:list(A) \
\ ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}";
by (induct_tac "xs" 1);
by (ALLGOALS(Asm_simp_tac));
by (rtac equalityI 1);
by Auto_tac;
by (res_inst_tac [("x", "0")] bexI 1);
by Auto_tac;
by (etac natE 1);
by Auto_tac;
qed "set_of_list_conv_nth";
(* Other theorems about lists *)
Goalw [Ball_def]
"k:nat ==> \
\ ALL xs:list(A). (ALL ys:list(A). k le length(xs) --> k le length(ys) --> \
\ (ALL i:nat. i<k --> nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))";
by (induct_tac "k" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps
[lt_succ_eq_0_disj, all_conj_distrib])));
by (Clarify_tac 1);
(*Both lists must be non-empty*)
by (case_tac "xa=Nil" 1);
by (case_tac "xb=Nil" 2);
by (Clarify_tac 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
by (Clarify_tac 1);
(*prenexing's needed, not miniscoping*)
by (Asm_simp_tac 1);
by (rtac conjI 1);
by (Force_tac 1);
by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [iff_sym])
delsimps (all_simps))));
by (dres_inst_tac [("x", "ys"), ("x1", "ysa")] (spec RS spec) 1);
by (Clarify_tac 1);
by Auto_tac;
qed_spec_mp "nth_take_lemma";
Goal "[| xs:list(A); ys:list(A); length(xs) = length(ys); \
\ ALL i:nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |] \
\ ==> xs = ys";
by (subgoal_tac "length(xs) le length(ys)" 1);
by (forw_inst_tac [("ys", "ys")] (rotate_prems 1 nth_take_lemma) 1);
by (ALLGOALS(Asm_simp_tac));
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [take_all])));
qed_spec_mp "nth_equalityI";
(*The famous take-lemma*)
Goal "[| xs:list(A); ys:list(A); (ALL i:nat. take(i, xs) = take(i,ys)) |] ==> xs = ys";
by (case_tac "length(xs) le length(ys)" 1);
by (dres_inst_tac [("x", "length(ys)")] bspec 1);
by (dtac not_lt_imp_le 3);
by (subgoal_tac "length(ys) le length(xs)" 5);
by (res_inst_tac [("j", "succ(length(ys))")] le_trans 6);
by (rtac leI 6);
by (dres_inst_tac [("x", "length(xs)")] bspec 5);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [take_all])));
qed_spec_mp "take_equalityI";
Goal "n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \
\ --> nth(i, drop(n, xs)) = nth(n #+ i, xs)";
by (induct_tac "n" 1);
by (ALLGOALS(Asm_full_simp_tac));
by (Clarify_tac 1);
by (case_tac "xb=Nil" 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
by (Clarify_tac 1);
by (auto_tac (claset() addSEs [ConsE], simpset()));
qed_spec_mp "nth_drop";
(** zip **)
Goal "l:list(A) ==> l:list(set_of_list(l))";
by (induct_tac "l" 1);
by Auto_tac;
by (res_inst_tac [("A1", "set_of_list(l)")] (list_mono RS subsetD) 1);
by Auto_tac;
qed "list_on_set_of_list";
Goal "A<=C ==> ziprel(A, B) <= ziprel(C,B)";
by (Clarify_tac 1);
by (forward_tac [ziprel.dom_subset RS subsetD] 1);
by (Clarify_tac 1);
by (etac ziprel.induct 1);
by (auto_tac (claset() addIs [list_mono RS subsetD]
addSIs ziprel.intrs, simpset()));
qed "ziprel_mono1";
Goal "B<=C ==> ziprel(A, B) <= ziprel(A,C)";
by (Clarify_tac 1);
by (forward_tac [ziprel.dom_subset RS subsetD] 1);
by (Clarify_tac 1);
by (etac ziprel.induct 1);
by (auto_tac (claset() addIs [list_mono RS subsetD]
addSIs ziprel.intrs, simpset()));
qed "ziprel_mono2";
Goal "[| A<=C; B<=D |] ==> ziprel(A, B) <= ziprel(C,D)";
by (rtac subset_trans 1);
by (rtac ziprel_mono1 2);
by (rtac ziprel_mono2 1);
by Auto_tac;
qed "ziprel_mono";
(* ziprel is a function *)
Goal "<xs, ys, zs>:ziprel(A,B) \
\ ==> ALL ks. <xs, ys, ks>:ziprel(A, B) --> ks=zs";
by (etac ziprel.induct 1);
by (ALLGOALS(Clarify_tac));
by (rotate_tac 1 3);
by (ALLGOALS(etac ziprel.elim));
by Safe_tac;
(* These hypotheses make Auto_tac loop! *)
by (thin_tac "ALL k. ?P(k)" 3);
by (thin_tac "ALL k. ?P(k)" 4);
by Auto_tac;
qed "ziprel_is_fun";
Goal "ys:list(B) ==> ALL xs:list(A). EX zs. <xs, ys, zs>:ziprel(A,B)";
by (induct_tac "ys" 1);
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
by (eres_inst_tac [("a", "xs")] list.elim 1);
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
qed_spec_mp "ziprel_exist";
Goalw [zip_def]
"[|xs:list(A); ys:list(B) |] ==> <xs, ys, zip(xs,ys)>:ziprel(A,B)";
by (rtac theI2 1);
by (asm_full_simp_tac (simpset() addsimps [set_of_list_append]) 2);
by (REPEAT(dtac set_of_list_type 2));
by (rtac (ziprel_mono RS subsetD) 2);
by (Blast_tac 3);
by (dtac list_on_set_of_list 1);
by (dtac list_on_set_of_list 1);
by (subgoal_tac "xs:list(set_of_list(xs@ys)) & \
\ ys:list(set_of_list(xs@ys))" 1);
by (auto_tac (claset() addIs [list_mono RS subsetD],
simpset() addsimps [set_of_list_append]));
by (rtac (ziprel_is_fun RS spec RS mp) 2);
by (rtac ziprel_exist 1);
by Auto_tac;
qed "zip_in_ziprel";
Goal
"<xs, ys, zs>:ziprel(A,B) ==> zip(xs, ys)=zs";
by (rtac (ziprel_is_fun RS spec RS mp) 1);
by (Blast_tac 1);
by (blast_tac (claset() addDs [ziprel.dom_subset RS subsetD]
addIs [zip_in_ziprel]) 1);
qed "zip_eq";
(* zip equations *)
Goal "ys:list(A) ==> zip(Nil, ys)=Nil";
by (res_inst_tac [("A", "A")] zip_eq 1);
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
qed "zip_Nil";
Addsimps [zip_Nil];
Goal "xs:list(A) ==> zip(xs, Nil)=Nil";
by (res_inst_tac [("A", "A")] zip_eq 1);
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
qed "zip_Nil2";
Addsimps [zip_Nil2];
Goal "[| xs:list(A); ys:list(B); x:A; y:B |] ==> \
\ zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))";
by (res_inst_tac [("A", "A")] zip_eq 1);
by (forw_inst_tac [("ys", "ys")] zip_in_ziprel 1);
by (auto_tac (claset() addIs ziprel.intrs, simpset()));
qed "zip_Cons_Cons";
Addsimps [zip_Cons_Cons];
Goal "xs:list(A) ==> ALL ys:list(B). zip(xs, ys):list(A*B)";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (eres_inst_tac [("a", "ys")] list.elim 1);
by Auto_tac;
qed_spec_mp "zip_type";
AddTCs [zip_type];
Addsimps [zip_type];
(* zip length *)
Goalw [min_def] "xs:list(A) ==> ALL ys:list(B). length(zip(xs,ys)) = \
\ min(length(xs), length(ys))";
by (induct_tac "xs" 1);
by (Clarify_tac 2);
by (eres_inst_tac [("a", "ys")] list.elim 2);
by Auto_tac;
qed_spec_mp "length_zip";
Addsimps [length_zip];
AddTCs [take_type];
Addsimps [take_type];
Goal "[| ys:list(A); zs:list(B) |] ==> ALL xs:list(A). zip(xs @ ys, zs) = \
\ zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))";
by (induct_tac "zs" 1);
by (Clarify_tac 2);
by (eres_inst_tac [("a", "xs")] list.elim 2);
by Auto_tac;
qed_spec_mp "zip_append1";
Goal
"[| xs:list(A); zs:list(B) |] ==> ALL ys:list(B). zip(xs, ys@zs) = \
\ zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)";
by (induct_tac "xs" 1);
by (Clarify_tac 2);
by (eres_inst_tac [("a", "ys")] list.elim 2);
by Auto_tac;
qed_spec_mp "zip_append2";
Goal
"[| 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 (asm_simp_tac (simpset() addsimps
[zip_append1, drop_append, diff_self_eq_0]) 1);
qed_spec_mp "zip_append";
Addsimps [zip_append];
Goal "ys:list(B) ==> ALL xs:list(A). \
\ length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))";
by (induct_tac "ys" 1);
by (Clarify_tac 2);
by (eres_inst_tac [("a", "xs")] list.elim 2);
by (auto_tac (claset(), simpset() addsimps [length_rev]));
qed_spec_mp "zip_rev";
Addsimps [zip_rev];
Goal
"ys:list(B) ==> ALL i:nat. ALL xs:list(A). \
\ i < length(xs) --> i < length(ys) --> \
\ nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>";
by (induct_tac "ys" 1);
by (Clarify_tac 2);
by (eres_inst_tac [("a", "xs")] list.elim 2);
by (auto_tac (claset() addEs [natE], simpset()));
qed_spec_mp "nth_zip";
Addsimps [nth_zip];
Goal "[| 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_tac (claset() addSIs [Collect_cong],
simpset() addsimps [lt_min_iff, set_of_list_conv_nth]) 1);
qed_spec_mp "set_of_list_zip";
(** list_update **)
Goalw [list_update_def] "i:nat ==>list_update(Nil, i, v) = Nil";
by Auto_tac;
qed "list_update_Nil";
Addsimps [list_update_Nil];
Goalw [list_update_def]
"list_update(Cons(x, xs), 0, v)= Cons(v, xs)";
by Auto_tac;
qed "list_update_Cons_0";
Addsimps [list_update_Cons_0];
Goalw [list_update_def]
"n:nat ==>\
\ list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))";
by Auto_tac;
qed "list_update_Cons_succ";
Addsimps [list_update_Cons_succ];
Goal "[| xs:list(A); v:A |] ==> ALL n:nat. list_update(xs, n, v):list(A)";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (etac natE 1);
by Auto_tac;
qed_spec_mp "list_update_type";
Addsimps [list_update_type];
AddTCs [list_update_type];
Goal "xs:list(A) ==> ALL i:nat. length(list_update(xs, i, v))=length(xs)";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (etac natE 1);
by Auto_tac;
qed_spec_mp "length_list_update";
Addsimps [length_list_update];
Goal "[| xs:list(A) |] ==> ALL i:nat. ALL j:nat. i < length(xs) --> \
\ nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (etac natE 1);
by (ALLGOALS(Asm_full_simp_tac));
by (ALLGOALS(Clarify_tac));
by (etac natE 1);
by (ALLGOALS(Asm_full_simp_tac));
by Safe_tac;
by (etac natE 2);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nth_Cons])));
qed_spec_mp "nth_list_update";
Goal "[| i < length(xs); xs:list(A); i:nat |] \
\ ==> nth(i, list_update(xs, i,x)) = x";
by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
qed "nth_list_update_eq";
Addsimps [nth_list_update_eq];
Goal "xs:list(A) ==> ALL i:nat. ALL j:nat. i ~= j \
\ --> nth(j, list_update(xs, i,x)) = nth(j, xs)";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (etac natE 1);
by (etac natE 2);
by (ALLGOALS(Asm_full_simp_tac));
by (etac natE 1);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nth_Cons])));
qed_spec_mp "nth_list_update_neq";
Addsimps [nth_list_update_neq];
Goal "xs:list(A) ==> ALL i:nat. i < length(xs)\
\ --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (etac natE 1);
by Auto_tac;
qed_spec_mp "list_update_overwrite";
Addsimps [list_update_overwrite];
Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \
\ (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)";
by (induct_tac "xs" 1);
by (Simp_tac 1);
by (Clarify_tac 1);
by (etac natE 1);
by Auto_tac;
qed_spec_mp "list_update_same_conv";
Goal "ys:list(B) ==> ALL i:nat. ALL xy:A*B. ALL 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)))";
by (induct_tac "ys" 1);
by Auto_tac;
by (eres_inst_tac [("a", "xc")] list.elim 1);
by (auto_tac (claset() addEs [natE], simpset()));
qed_spec_mp "update_zip";
Goal "xs:list(A) ==> ALL i:nat. set_of_list(list_update(xs, i, x)) \
\ <= cons(x, set_of_list(xs))";
by (induct_tac "xs" 1);
by (asm_full_simp_tac (simpset() addsimps []) 1);
by (rtac ballI 1);
by (etac natE 1);
by (ALLGOALS(Asm_full_simp_tac));
by Auto_tac;
qed_spec_mp "set_update_subset_cons";
Goal "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|] \
\ ==> set_of_list(list_update(xs, i,x)) <= A";
by (rtac subset_trans 1);
by (rtac set_update_subset_cons 1);
by Auto_tac;
qed "set_of_list_update_subsetI";
(** upt **)
Goal "[| i:nat; j:nat |] \
\ ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)";
by (induct_tac "j" 1);
by Auto_tac;
by (dtac not_lt_imp_le 1);
by (auto_tac (claset() addIs [le_anti_sym], simpset()));
qed "upt_rec";
Goal "[| j le i; i:nat; j:nat |] ==> upt(i,j) = Nil";
by (stac upt_rec 1);
by Auto_tac;
by (auto_tac (claset(), simpset() addsimps [le_iff]));
by (dtac (lt_asym RS notE) 1);
by Auto_tac;
qed "upt_conv_Nil";
Addsimps [upt_conv_Nil];
(*Only needed if upt_Suc is deleted from the simpset*)
Goal "[| i le j; i:nat; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]";
by (Asm_simp_tac 1);
qed "upt_succ_append";
Goal "[| i<j; i:nat; j:nat |] ==> upt(i,j) = Cons(i,upt(succ(i),j))";
by (rtac trans 1);
by (stac upt_rec 1);
by (rtac refl 4);
by Auto_tac;
qed "upt_conv_Cons";
Goal "[| i:nat; j:nat |] ==> upt(i,j):list(nat)";
by (induct_tac "j" 1);
by Auto_tac;
qed "upt_type";
AddTCs [upt_type];
Addsimps [upt_type];
(*LOOPS as a simprule, since j<=j*)
Goal "[| i le j; i:nat; j:nat; k:nat |] ==> \
\ upt(i, j #+k) = upt(i,j)@upt(j,j#+k)";
by (induct_tac "k" 1);
by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type]));
by (res_inst_tac [("j", "j")] le_trans 1);
by Auto_tac;
qed "upt_add_eq_append";
Goal "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i";
by (induct_tac "j" 1);
by (rtac sym 2);
by (auto_tac (claset() addSDs [not_lt_imp_le],
simpset() addsimps [length_app, diff_succ, diff_is_0_iff]));
qed "length_upt";
Addsimps [length_upt];
Goal "[| i:nat; j:nat; k:nat |] ==> \
\ i #+ k < j --> nth(k, upt(i,j)) = i #+ k";
by (induct_tac "j" 1);
by (Asm_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [nth_append,lt_succ_iff]
addsplits [nat_diff_split]) 1);
by Safe_tac;
by (auto_tac (claset() addSDs [not_lt_imp_le],
simpset() addsimps [nth_append, diff_self_eq_0,
less_diff_conv, add_commute]));
by (dres_inst_tac [("j", "x")] lt_trans2 1);
by Auto_tac;
qed_spec_mp "nth_upt";
Addsimps [nth_upt];
Goal "[| m:nat; n:nat |] ==> \
\ ALL i:nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)";
by (induct_tac "m" 1);
by (asm_simp_tac (simpset() addsimps [take_0]) 1);
by (Clarify_tac 1);
by (stac upt_rec 1);
by (rtac sym 3);
by (stac upt_rec 3);
by (ALLGOALS(asm_full_simp_tac (simpset() delsimps (thms"upt.simps"))));
by (res_inst_tac [("j", "succ(i #+ x)")] lt_trans2 1);
by Auto_tac;
qed_spec_mp "take_upt";
Addsimps [take_upt];
Goal "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))";
by (induct_tac "n" 1);
by (auto_tac (claset(), simpset() addsimps [map_app_distrib]));
qed "map_succ_upt";
Goal "xs:list(A) ==> \
\ ALL n:nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))";
by (induct_tac "xs" 1);
by (Asm_full_simp_tac 1);
by (rtac ballI 1);
by (induct_tac "n" 1);
by Auto_tac;
qed_spec_mp "nth_map";
Addsimps [nth_map];
Goal "[| m:nat; n:nat |] ==> \
\ ALL i:nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)";
by (res_inst_tac [("n", "m"), ("m", "n")] diff_induct 1);
by (stac (map_succ_upt RS sym) 5);
by (ALLGOALS(Asm_full_simp_tac));
by (ALLGOALS(Clarify_tac));
by (subgoal_tac "xa < length(upt(0, x))" 1);
by (Asm_simp_tac 2);
by (subgoal_tac "xa < length(upt(y, x))" 2);
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [map_compose,
nth_map, add_commute, less_diff_conv])));
by (res_inst_tac [("j", "succ(xa #+ y)")] lt_trans2 1);
by Auto_tac;
qed_spec_mp "nth_map_upt";
(** sublist (a generalization of nth to sets) **)
Goalw [sublist_def] "xs:list(A) ==>sublist(xs, 0) =Nil";
by Auto_tac;
qed "sublist_0";
Goalw [sublist_def] "sublist(Nil, A) = Nil";
by Auto_tac;
qed "sublist_Nil";
AddTCs [filter_type];
Addsimps [filter_type];
Goal "[| 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)))))";
by (etac list_append_induct 1);
by (Asm_simp_tac 1);
by (auto_tac (claset(), simpset() addsimps
[add_commute, length_app, filter_append, map_app_distrib]));
qed "sublist_shift_lemma";
Goalw [sublist_def]
"xs:list(B) ==> sublist(xs, A):list(B)";
by (induct_tac "xs" 1);
by (auto_tac (claset(), simpset() addsimps [filter_append, map_app_distrib]));
by (auto_tac (claset() addIs [map_type,filter_type,zip_type], simpset()));
qed "sublist_type";
AddTCs [sublist_type];
Addsimps [sublist_type];
Goal "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)";
by (asm_simp_tac (simpset() addsimps
[inst "i" "0" upt_add_eq_append, nat_0_le]) 1);
qed "upt_add_eq_append2";
Goalw [sublist_def]
"[| xs:list(B); ys:list(B) |] ==> \
\ sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})";
by (eres_inst_tac [("l", "ys")] list_append_induct 1);
by (Asm_simp_tac 1);
by (asm_simp_tac (simpset() addsimps [upt_add_eq_append2,
zip_append, length_app, app_assoc RS sym]) 1);
by (auto_tac (claset(), simpset() addsimps [sublist_shift_lemma,
length_type, map_app_distrib, app_assoc]));
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [add_commute])));
qed "sublist_append";
Addsimps [sublist_0, sublist_Nil];
Goal "[| xs:list(B); x:B |] ==> \
\ sublist(Cons(x, xs), A) = (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})";
by (eres_inst_tac [("l", "xs")] list_append_induct 1);
by (asm_simp_tac (simpset() addsimps [sublist_def]) 1);
by (asm_simp_tac (simpset() delsimps (thms "op @.simps")
addsimps [(hd (tl (thms "op @.simps"))) RS sym, sublist_append]) 1);
by Auto_tac;
qed "sublist_Cons";
Goal "sublist([x], A) = (if 0 : A then [x] else [])";
by (simp_tac (simpset() addsimps [sublist_Cons]) 1);
qed "sublist_singleton";
Addsimps [sublist_singleton];
Goalw [less_than_def]
"[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)";
by (eres_inst_tac [("l", "xs")] list_append_induct 1);
by (asm_simp_tac (simpset() addsplits [nat_diff_split]
addsimps [sublist_append]) 2);
by Auto_tac;
by (subgoal_tac "n #- length(y) = 0" 1);
by (Asm_simp_tac 1);
by (auto_tac (claset() addSDs [not_lt_imp_le],
simpset() addsimps [diff_is_0_iff]));
qed "sublist_upt_eq_take";
Addsimps [sublist_upt_eq_take];