--- a/src/ZF/List.ML Tue Jul 09 18:54:27 2002 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1273 +0,0 @@
-(* 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 ***)
-
-Addsimps list.intrs;
-
-(*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);
-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];
-
-(*TOO SLOW as a default simprule!*)
-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";
-
-(*TOO SLOW as a default simprule!*)
-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";
-
-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 (simpset() addsimps [append_left_is_Nil_iff]) 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,le_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];
-
--- a/src/ZF/List.thy Tue Jul 09 18:54:27 2002 +0200
+++ b/src/ZF/List.thy Tue Jul 09 23:03:21 2002 +0200
@@ -3,18 +3,15 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-Lists in Zermelo-Fraenkel Set Theory
-
-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.
*)
-List = Datatype + ArithSimp +
+header{*Lists in Zermelo-Fraenkel Set Theory*}
+
+theory List = Datatype + ArithSimp:
consts
list :: "i=>i"
-
+
datatype
"list(A)" = Nil | Cons ("a:A", "l: list(A)")
@@ -37,7 +34,7 @@
primrec
"length([]) = 0"
"length(Cons(a,l)) = succ(length(l))"
-
+
primrec
"hd(Cons(a,l)) = a"
@@ -47,22 +44,25 @@
consts
- map :: "[i=>i, i] => i"
+ map :: "[i=>i, i] => i"
set_of_list :: "i=>i"
- "@" :: "[i,i]=>i" (infixr 60)
-
+ 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
- "[] @ ys = ys"
- "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
-
+ app_Nil: "[] @ ys = ys"
+ app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
+
consts
rev :: "i=>i"
@@ -76,17 +76,17 @@
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))"
+ drop_0: "drop(0,l) = l"
+ drop_SUCC: "drop(succ(i), l) = tl (drop(i,l))"
(*** Thanks to Sidi Ehmety for the following ***)
@@ -96,7 +96,7 @@
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"
-
+
(* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *)
nth :: "[i, i]=>i"
"nth(n, as) == list_rec(lam n:nat. 0,
@@ -108,21 +108,7 @@
consts
filter :: "[i=>o, i] => i"
- zip :: "[i, i]=>i"
- ziprel :: "[i,i]=>i"
upt :: "[i, i] =>i"
-
-inductive domains "ziprel(A, B)" <= "list(A)*list(B)*list(A*B)"
-intrs
- ziprel_Nil1 "ys:list(B) ==><Nil, ys, Nil>:ziprel(A, B)"
- ziprel_Nil2 "xs:list(A) ==><xs, Nil, Nil>:ziprel(A, B)"
- ziprel_Cons "[| <xs, ys, zs>:ziprel(A, B); x:A; y:B |]==>
- <Cons(x, xs), Cons(y, ys), Cons(<x, y>, zs)>:ziprel(A,B)"
- type_intrs "list.intrs"
-
-defs
- zip_def "zip(xs, ys) ==
- THE zs. <xs, ys, zs>:ziprel(set_of_list(xs),set_of_list(ys))"
primrec
"filter(P, Nil) = Nil"
@@ -134,14 +120,1246 @@
"upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)"
constdefs
- sublist :: "[i, i] => i"
- "sublist(xs, A)==
- map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
-
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)"
+
+(*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)"
+apply (erule list.induct, 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 \<in> list(A)|] ==> x \<in> 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)"
+apply (induct_tac "xs")
+apply simp_all
+done
+
+lemma length_app [simp]:
+ "[| xs: list(A); ys: list(A) |]
+ ==> length(xs@ys) = length(xs) #+ length(ys)"
+apply (induct_tac "xs")
+apply simp_all
+done
+
+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) ==>
+ \<forall>x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
+apply (erule list.induct)
+apply simp_all
+done
+
+lemma drop_length [rule_format]:
+ "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
+apply (erule list.induct)
+apply simp_all
+apply safe
+apply (erule drop_length_Cons)
+apply (rule natE)
+apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption)
+apply 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"
+apply (erule list.induct)
+apply simp_all
+done
+
+lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
+apply (induct_tac "xs")
+apply simp_all
+done
+
+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")
+apply 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 rule **)
+
+
+lemma list_append_induct:
+ "[| 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
+
+
+(*** 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) ==> \<forall>ys \<in> 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) ==>
+ \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> 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)
+apply 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"
+apply (simp (no_asm_simp))
+done
+
+lemma append_self_iff2 [simp]:
+ "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
+apply (simp (no_asm_simp))
+done
+
+(* 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) ==> \<forall>ys \<in> 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 = xa in list.cases, simp_all)
+done
+
+
+lemma append_right_is_self_iff [simp]:
+ "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
+apply (simp (no_asm_simp) add: append_left_is_Nil_iff)
+done
+
+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) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
+apply (erule list.induct, force)
+apply clarify
+apply (erule_tac a = "ys" in list.cases, auto)
+done
+
+lemma rev_list_elim [rule_format]:
+ "xs:list(A) ==>
+ (xs=Nil --> P) --> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] -->P)-->P"
+apply (erule list_append_induct, auto)
+done
+
+
+(** more theorems about drop **)
+
+lemma length_drop [rule_format,simp]:
+ "n:nat ==> \<forall>xs \<in> 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 ==> \<forall>xs \<in> 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 ==>
+ \<forall>xs \<in> 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 ==> \<forall>xs \<in> list(A). \<forall>n \<in> 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 ==> \<forall>xs \<in> 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) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
+apply (erule list.induct, simp)
+apply clarify
+apply (erule natE, auto)
+done
+
+lemma take_append [rule_format,simp]:
+ "xs:list(A) ==>
+ \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
+ take(n, xs) @ take(n #- length(xs), ys)"
+apply (erule list.induct, simp)
+apply clarify
+apply (erule natE, auto)
+done
+
+lemma take_take [rule_format]:
+ "m : nat ==>
+ \<forall>xs \<in> list(A). \<forall>n \<in> 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 (rotate_tac 1)
+apply (erule natE)
+apply (auto intro: take_0 take_type)
+done
+
+(** nth **)
+
+lemma nth_0 [simp]: "nth(0, Cons(a, l))= a"
+by (unfold nth_def, auto)
+
+lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)"
+apply (unfold nth_def)
+apply (simp (no_asm_simp))
+done
+
+lemma nth_type [rule_format,simp,TC]:
+ "xs:list(A) ==> \<forall>n \<in> nat. n < length(xs) --> nth(n, xs):A"
+apply (erule list.induct, simp)
+apply clarify
+apply (erule natE, auto)
+done
+
+lemma nth_append [rule_format]:
+ "xs:list(A) ==>
+ \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
+ else nth(n #- length(xs),ys))"
+apply (induct_tac "xs", simp)
+apply 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 ==>
+ \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k le length(xs) --> k le length(ys) -->
+ (\<forall>i \<in> 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="xa" in list.cases, simp)
+apply (erule_tac a="xb" 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);
+ \<forall>i \<in> 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); (\<forall>i \<in> 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 ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). n #+ i le length(xs)
+ --> nth(i, drop(n, xs)) = nth(n #+ i, xs)"
+apply (induct_tac "n", simp_all)
+apply clarify
+apply (erule list.cases)
+apply (auto elim!: ConsE)
+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,[]) =
+ (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
+
+ "zip_aux(B,Cons(x,l)) =
+ (\<lambda>ys \<in> 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 \<in> list(A) ==> xs \<in> 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 \<in> list(A)|]
+ ==> \<forall>ys \<in> 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=x 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) ==> \<forall>ys \<in> 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) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
+ min(length(xs), length(ys))"
+apply (unfold min_def)
+apply (induct_tac "xs", simp_all)
+apply clarify
+apply (erule_tac a = "x" in list.cases, auto)
+done
+
+lemma zip_append1 [rule_format]:
+ "[| ys:list(A); zs:list(B) |] ==>
+ \<forall>xs \<in> list(A). zip(xs @ ys, zs) =
+ zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
+apply (induct_tac "zs", force)
+apply clarify
+apply (erule_tac a = "xs" in list.cases, simp_all)
+done
+
+lemma zip_append2 [rule_format]:
+ "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
+ zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
+apply (induct_tac "xs", force)
+apply 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) ==> \<forall>xs \<in> list(A).
+ length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
+apply (induct_tac "ys", force)
+apply 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) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
+ i < length(xs) --> i < length(ys) -->
+ nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
+apply (induct_tac "ys", force)
+apply 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 |] ==> \<forall>n \<in> 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) ==> \<forall>i \<in> 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) |] ==> \<forall>i \<in> nat. \<forall>j \<in> 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) ==> \<forall>i \<in> nat. \<forall>j \<in> 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) ==> \<forall>i \<in> 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) ==> \<forall>i \<in> 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) ==> \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> 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 = "xc" in list.cases)
+apply (auto elim: natE)
+done
+
+lemma set_update_subset_cons [rule_format]:
+ "xs:list(A) ==> \<forall>i \<in> 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)
+apply 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: length_app 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")
+apply (simp (no_asm_simp))
+apply (simp add: nth_append le_iff split add: nat_diff_split, safe)
+apply (auto dest!: not_lt_imp_le simp add: nth_append diff_self_eq_0
+ less_diff_conv add_commute)
+apply (drule_tac j = "x" in lt_trans2, auto)
+done
+
+lemma take_upt [rule_format,simp]:
+ "[| m:nat; n:nat |] ==>
+ \<forall>i \<in> 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) ==>
+ \<forall>n \<in> 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 |] ==>
+ \<forall>i \<in> 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)
+apply simp
+apply simp
+apply (subst map_succ_upt [symmetric], simp_all)
+apply clarify
+apply (subgoal_tac "xa < length (upt (0, x))")
+ prefer 2
+ apply (simp add: less_diff_conv)
+ apply (rule_tac j = "succ (xa #+ y) " in lt_trans2)
+ apply simp
+ apply simp
+apply (subgoal_tac "xa < 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)
+apply (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 (no_asm) add: sublist_Cons)
+
+
+lemma sublist_upt_eq_take [simp]:
+ "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)"
+apply (unfold less_than_def)
+apply (erule_tac l = "xs" in list_append_induct, simp)
+apply (simp split add: nat_diff_split add: sublist_append, auto)
+apply (subgoal_tac "n #- length (y) = 0")
+apply (simp (no_asm_simp))
+apply (auto dest!: not_lt_imp_le simp add: diff_is_0_iff)
+done
+
+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 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";
+
+structure list =
+struct
+val induct = thm "list.induct"
+val elim = thm "list.cases"
+val intrs = thms "list.intros"
+end;
+*}
+
end