# HG changeset patch
# User paulson
# Date 1011267952 -3600
# Node ID 459b5de466b220a62ec2de4adab3150d4d0cba12
# Parent  6842f90972da14050fd2cb43393a3543ff4bdcd0
new definitions from Sidi Ehmety

diff -r 6842f90972da -r 459b5de466b2 src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Thu Jan 17 12:45:36 2002 +0100
+++ b/src/ZF/Arith.ML	Thu Jan 17 12:45:52 2002 +0100
@@ -501,3 +501,24 @@
 qed "mult_left_commute";
 
 bind_thms ("mult_ac", [mult_assoc,mult_commute,mult_left_commute]);
+
+
+Goal "[| m:nat; n:nat |] \
+\     ==> (m < succ(n)) <-> (m = 0 | (EX j:nat. m = succ(j) & j < n))";
+by (induct_tac "m" 1);
+by Auto_tac;
+qed "lt_succ_eq_0_disj";
+
+Goal "[| m:nat; n:nat |] ==> (m < succ(n)) <-> (m < n | m =n)";
+by (induct_tac "n" 1);
+by (auto_tac (claset() addIs [leI], simpset()));
+by (dtac not_lt_imp_le 1);
+by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [le_iff]));
+qed "lt_succ_iff";
+
+Goal "[| j:nat; k:nat |] ==> ALL i:nat. (i < j #- k) <-> (i #+ k < j)";
+by (eres_inst_tac [("m", "k")] diff_induct  1);
+by Auto_tac;
+qed_spec_mp "less_diff_conv";
+
diff -r 6842f90972da -r 459b5de466b2 src/ZF/List.ML
--- a/src/ZF/List.ML	Thu Jan 17 12:45:36 2002 +0100
+++ b/src/ZF/List.ML	Thu Jan 17 12:45:52 2002 +0100
@@ -16,9 +16,8 @@
 bind_thm ("Nil_Cons_iff", list.mk_free "~ Nil=Cons(a,l)");
 
 Goal "list(A) = {0} + (A * list(A))";
-let open list;  val rew = rewrite_rule con_defs in  
-by (blast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
-end;
+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 **)
@@ -334,3 +333,943 @@
 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 (res_inst_tac [("x", "succ(i)")] 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];
+
diff -r 6842f90972da -r 459b5de466b2 src/ZF/List.thy
--- a/src/ZF/List.thy	Thu Jan 17 12:45:36 2002 +0100
+++ b/src/ZF/List.thy	Thu Jan 17 12:45:52 2002 +0100
@@ -13,7 +13,7 @@
 List = Datatype + ArithSimp +
 
 consts
-  list       :: i=>i
+  list       :: "i=>i"
   
 datatype
   "list(A)" = Nil | Cons ("a:A", "l: list(A)")
@@ -21,7 +21,7 @@
 
 syntax
  "[]"        :: i                                       ("[]")
- "@List"     :: is => i                                 ("[(_)]")
+ "@List"     :: "is => i"                                 ("[(_)]")
 
 translations
   "[x, xs]"     == "Cons(x, [xs])"
@@ -30,9 +30,9 @@
 
 
 consts
-  length :: i=>i
-  hd      :: i=>i
-  tl      :: i=>i
+  length :: "i=>i"
+  hd      :: "i=>i"
+  tl      :: "i=>i"
 
 primrec
   "length([]) = 0"
@@ -47,9 +47,9 @@
 
 
 consts
-  map        :: [i=>i, i] => i
-  set_of_list :: i=>i
-  "@"        :: [i,i]=>i                        (infixr 60)
+  map        :: "[i=>i, i] => i"
+  set_of_list :: "i=>i"
+  "@"        :: "[i,i]=>i"                        (infixr 60)
   
 primrec
   "map(f,[]) = []"
@@ -65,9 +65,9 @@
   
 
 consts
-  rev :: i=>i
-  flat       :: i=>i
-  list_add   :: i=>i
+  rev :: "i=>i"
+  flat       :: "i=>i"
+  list_add   :: "i=>i"
 
 primrec
   "rev([]) = []"
@@ -82,10 +82,66 @@
   "list_add(Cons(a,l)) = a #+ list_add(l)"
        
 consts
-  drop       :: [i,i]=>i
+  drop       :: "[i,i]=>i"
 
 primrec
   drop_0    "drop(0,l) = l"
   drop_SUCC "drop(succ(i), l) = tl (drop(i,l))"
 
+
+(*** Thanks to Sidi Ehmety for the following ***)
+
+constdefs
+(* Function `take' returns the first n elements of a list *)
+  take     :: "[i,i]=>i"
+  "take(n, as) == list_rec(lam n:nat. [],
+		%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
+  
+(* 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,
+		%a l r. lam n:nat. nat_case(a, %m. r`m, n), as)`n"
+
+  list_update :: "[i, i, i]=>i"
+  "list_update(xs, i, v) == list_rec(lam n:nat. Nil,
+      %u us vs. lam n:nat. nat_case(Cons(v, us), %m. Cons(u, vs`m), n), xs)`i"
+
+consts
+  filter :: "[i=>o, i] => i"
+  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"
+  "filter(P, Cons(x, xs)) =
+     (if P(x) then Cons(x, filter(P, xs)) else filter(P, xs))"
+
+primrec
+  "upt(i, 0) = Nil"
+  "upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)"
+
+constdefs
+  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)"
+
 end
diff -r 6842f90972da -r 459b5de466b2 src/ZF/Nat.thy
--- a/src/ZF/Nat.thy	Thu Jan 17 12:45:36 2002 +0100
+++ b/src/ZF/Nat.thy	Thu Jan 17 12:45:52 2002 +0100
@@ -7,20 +7,36 @@
 *)
 
 Nat = OrdQuant + Bool + mono +
-consts
-    nat         ::      i
-    nat_case    ::      [i, i=>i, i]=>i
-    nat_rec     ::      [i, i, [i,i]=>i]=>i
 
-defs
+constdefs
+  nat :: i
+    "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
 
-    nat_def     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
+  nat_case :: "[i, i=>i, i]=>i"
+    "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
 
-    nat_case_def
-        "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
-
-    nat_rec_def
-        "nat_rec(k,a,b) ==   
+  nat_rec :: "[i, i, [i,i]=>i]=>i"
+    "nat_rec(k,a,b) ==   
           wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
 
+  (*Internalized relations on the naturals*)
+  
+  Le :: i
+    "Le == {<x,y>:nat*nat. x le y}"
+
+  Lt :: i
+    "Lt == {<x, y>:nat*nat. x < y}"
+  
+  Ge :: i
+    "Ge == {<x,y>:nat*nat. y le x}"
+
+  Gt :: i
+    "Gt == {<x,y>:nat*nat. y < x}"
+
+  less_than :: i=>i
+    "less_than(n) == {i:nat.  i<n}"
+
+  greater_than :: i=>i
+    "greater_than(n) == {i:nat. n < i}"
+
 end