converted List to new-style
authorpaulson
Tue Jul 09 23:03:21 2002 +0200 (2002-07-09)
changeset 13327be7105a066d3
parent 13326 900f220c800d
child 13328 703de709a64b
converted List to new-style
src/ZF/IsaMakefile
src/ZF/List.ML
src/ZF/List.thy
     1.1 --- a/src/ZF/IsaMakefile	Tue Jul 09 18:54:27 2002 +0200
     1.2 +++ b/src/ZF/IsaMakefile	Tue Jul 09 23:03:21 2002 +0200
     1.3 @@ -36,7 +36,7 @@
     1.4    InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML	\
     1.5    Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy	\
     1.6    Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML			\
     1.7 -  Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy	\
     1.8 +  Integ/twos_compl.ML Let.ML Let.thy List.thy Main.ML Main.thy	\
     1.9    Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy	\
    1.10    OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy	\
    1.11    QPair.thy QUniv.thy ROOT.ML	\
     2.1 --- a/src/ZF/List.ML	Tue Jul 09 18:54:27 2002 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,1273 +0,0 @@
     2.4 -(*  Title:      ZF/List.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 -    Copyright   1993  University of Cambridge
     2.8 -
     2.9 -Datatype definition of Lists
    2.10 -*)
    2.11 -
    2.12 -(*** Aspects of the datatype definition ***)
    2.13 -
    2.14 -Addsimps list.intrs;
    2.15 -
    2.16 -(*An elimination rule, for type-checking*)
    2.17 -bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)");
    2.18 -
    2.19 -(*Proving freeness results*)
    2.20 -bind_thm ("Cons_iff", list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'");
    2.21 -bind_thm ("Nil_Cons_iff", list.mk_free "~ Nil=Cons(a,l)");
    2.22 -
    2.23 -Goal "list(A) = {0} + (A * list(A))";
    2.24 -by (blast_tac (claset() addSIs (map (rewrite_rule list.con_defs) list.intrs) 
    2.25 -                        addEs [rewrite_rule list.con_defs list.elim]) 1);
    2.26 -qed "list_unfold";
    2.27 -
    2.28 -(**  Lemmas to justify using "list" in other recursive type definitions **)
    2.29 -
    2.30 -Goalw list.defs "A<=B ==> list(A) <= list(B)";
    2.31 -by (rtac lfp_mono 1);
    2.32 -by (REPEAT (rtac list.bnd_mono 1));
    2.33 -by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
    2.34 -qed "list_mono";
    2.35 -
    2.36 -(*There is a similar proof by list induction.*)
    2.37 -Goalw (list.defs@list.con_defs) "list(univ(A)) <= univ(A)";
    2.38 -by (rtac lfp_lowerbound 1);
    2.39 -by (rtac (A_subset_univ RS univ_mono) 2);
    2.40 -by (blast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
    2.41 -				Pair_in_univ]) 1);
    2.42 -qed "list_univ";
    2.43 -
    2.44 -(*These two theorems justify datatypes involving list(nat), list(A), ...*)
    2.45 -bind_thm ("list_subset_univ", [list_mono, list_univ] MRS subset_trans);
    2.46 -
    2.47 -Goal "[| l: list(A);  A <= univ(B) |] ==> l: univ(B)";
    2.48 -by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
    2.49 -qed "list_into_univ";
    2.50 -
    2.51 -val major::prems = Goal
    2.52 -    "[| l: list(A);    \
    2.53 -\       c: C(Nil);       \
    2.54 -\       !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))  \
    2.55 -\    |] ==> list_case(c,h,l) : C(l)";
    2.56 -by (rtac (major RS list.induct) 1);
    2.57 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
    2.58 -qed "list_case_type";
    2.59 -
    2.60 -
    2.61 -(*** List functions ***)
    2.62 -
    2.63 -Goal "l: list(A) ==> tl(l) : list(A)";
    2.64 -by (exhaust_tac "l" 1);
    2.65 -by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs)));
    2.66 -qed "tl_type";
    2.67 -
    2.68 -(** drop **)
    2.69 -
    2.70 -Goal "i:nat ==> drop(i, Nil) = Nil";
    2.71 -by (induct_tac "i" 1);
    2.72 -by (ALLGOALS Asm_simp_tac);
    2.73 -qed "drop_Nil";
    2.74 -
    2.75 -Goal "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)";
    2.76 -by (rtac sym 1);
    2.77 -by (induct_tac "i" 1);
    2.78 -by (Simp_tac 1);
    2.79 -by (Asm_simp_tac 1);
    2.80 -qed "drop_succ_Cons";
    2.81 -
    2.82 -Addsimps [drop_Nil, drop_succ_Cons];
    2.83 -
    2.84 -Goal "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)";
    2.85 -by (induct_tac "i" 1);
    2.86 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type])));
    2.87 -qed "drop_type";
    2.88 -
    2.89 -Delsimps [drop_SUCC];
    2.90 -
    2.91 -
    2.92 -(** Type checking -- proved by induction, as usual **)
    2.93 -
    2.94 -val prems = Goal
    2.95 -    "[| l: list(A);    \
    2.96 -\       c: C(Nil);       \
    2.97 -\       !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))  \
    2.98 -\    |] ==> list_rec(c,h,l) : C(l)";
    2.99 -by (cut_facts_tac prems 1);
   2.100 -by (induct_tac "l" 1);
   2.101 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   2.102 -qed "list_rec_type";
   2.103 -
   2.104 -(** map **)
   2.105 -
   2.106 -val prems = Goalw [thm "map_list_def"]
   2.107 -    "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)";
   2.108 -by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1));
   2.109 -qed "map_type";
   2.110 -
   2.111 -Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})";
   2.112 -by (etac map_type 1);
   2.113 -by (etac RepFunI 1);
   2.114 -qed "map_type2";
   2.115 -
   2.116 -(** length **)
   2.117 -
   2.118 -Goalw [thm "length_list_def"]
   2.119 -    "l: list(A) ==> length(l) : nat";
   2.120 -by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1));
   2.121 -qed "length_type";
   2.122 -
   2.123 -(** app **)
   2.124 -
   2.125 -Goalw [thm "op @_list_def"]
   2.126 -    "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)";
   2.127 -by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1));
   2.128 -qed "app_type";
   2.129 -
   2.130 -(** rev **)
   2.131 -
   2.132 -Goalw [thm "rev_list_def"]
   2.133 -    "xs: list(A) ==> rev(xs) : list(A)";
   2.134 -by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
   2.135 -qed "rev_type";
   2.136 -
   2.137 -
   2.138 -(** flat **)
   2.139 -
   2.140 -Goalw [thm "flat_list_def"]
   2.141 -    "ls: list(list(A)) ==> flat(ls) : list(A)";
   2.142 -by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1));
   2.143 -qed "flat_type";
   2.144 -
   2.145 -
   2.146 -(** set_of_list **)
   2.147 -
   2.148 -Goalw [thm "set_of_list_list_def"]
   2.149 -    "l: list(A) ==> set_of_list(l) : Pow(A)";
   2.150 -by (etac list_rec_type 1);
   2.151 -by (ALLGOALS (Blast_tac));
   2.152 -qed "set_of_list_type";
   2.153 -
   2.154 -Goal "xs: list(A) ==> \
   2.155 -\         set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)";
   2.156 -by (etac list.induct 1);
   2.157 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons])));
   2.158 -qed "set_of_list_append";
   2.159 -
   2.160 -
   2.161 -(** list_add **)
   2.162 -
   2.163 -Goalw [thm "list_add_list_def"] 
   2.164 -    "xs: list(nat) ==> list_add(xs) : nat";
   2.165 -by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1));
   2.166 -qed "list_add_type";
   2.167 -
   2.168 -bind_thms ("list_typechecks",
   2.169 -    list.intrs @
   2.170 -    [list_rec_type, map_type, map_type2, app_type, length_type, 
   2.171 -     rev_type, flat_type, list_add_type]);
   2.172 -
   2.173 -AddTCs list_typechecks;
   2.174 -
   2.175 -
   2.176 -(*** theorems about map ***)
   2.177 -
   2.178 -Goal "l: list(A) ==> map(%u. u, l) = l";
   2.179 -by (induct_tac "l" 1);
   2.180 -by (ALLGOALS Asm_simp_tac);
   2.181 -qed "map_ident";
   2.182 -Addsimps [map_ident];
   2.183 -
   2.184 -Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
   2.185 -by (induct_tac "l" 1);
   2.186 -by (ALLGOALS Asm_simp_tac);
   2.187 -qed "map_compose";
   2.188 -
   2.189 -Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)";
   2.190 -by (induct_tac "xs" 1);
   2.191 -by (ALLGOALS Asm_simp_tac);
   2.192 -qed "map_app_distrib";
   2.193 -
   2.194 -Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))";
   2.195 -by (induct_tac "ls" 1);
   2.196 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
   2.197 -qed "map_flat";
   2.198 -
   2.199 -Goal "l: list(A) ==> \
   2.200 -\    list_rec(c, d, map(h,l)) = \
   2.201 -\    list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)";
   2.202 -by (induct_tac "l" 1);
   2.203 -by (ALLGOALS Asm_simp_tac);
   2.204 -qed "list_rec_map";
   2.205 -
   2.206 -(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
   2.207 -
   2.208 -(* c : list(Collect(B,P)) ==> c : list(B) *)
   2.209 -bind_thm ("list_CollectD", Collect_subset RS list_mono RS subsetD);
   2.210 -
   2.211 -Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
   2.212 -by (induct_tac "l" 1);
   2.213 -by (ALLGOALS Asm_simp_tac);
   2.214 -qed "map_list_Collect";
   2.215 -
   2.216 -(*** theorems about length ***)
   2.217 -
   2.218 -Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)";
   2.219 -by (induct_tac "xs" 1);
   2.220 -by (ALLGOALS Asm_simp_tac);
   2.221 -qed "length_map";
   2.222 -
   2.223 -Goal "[| xs: list(A); ys: list(A) |] \
   2.224 -\     ==> length(xs@ys) = length(xs) #+ length(ys)";
   2.225 -by (induct_tac "xs" 1);
   2.226 -by (ALLGOALS Asm_simp_tac);
   2.227 -qed "length_app";
   2.228 -
   2.229 -Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
   2.230 -by (induct_tac "xs" 1);
   2.231 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
   2.232 -qed "length_rev";
   2.233 -
   2.234 -Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
   2.235 -by (induct_tac "ls" 1);
   2.236 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
   2.237 -qed "length_flat";
   2.238 -
   2.239 -(** Length and drop **)
   2.240 -
   2.241 -(*Lemma for the inductive step of drop_length*)
   2.242 -Goal "xs: list(A) ==> \
   2.243 -\          ALL x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)";
   2.244 -by (etac list.induct 1);
   2.245 -by (ALLGOALS Asm_simp_tac);
   2.246 -qed_spec_mp "drop_length_Cons";
   2.247 -
   2.248 -Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
   2.249 -by (etac list.induct 1);
   2.250 -by (ALLGOALS Asm_simp_tac);
   2.251 -by Safe_tac;
   2.252 -by (etac drop_length_Cons 1);
   2.253 -by (rtac natE 1);
   2.254 -by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
   2.255 -by (assume_tac 1);
   2.256 -by (ALLGOALS Asm_simp_tac);
   2.257 -by (ALLGOALS (blast_tac (claset() addIs [succ_in_naturalD, length_type])));
   2.258 -qed_spec_mp "drop_length";
   2.259 -
   2.260 -
   2.261 -(*** theorems about app ***)
   2.262 -
   2.263 -Goal "xs: list(A) ==> xs@Nil=xs";
   2.264 -by (etac list.induct 1);
   2.265 -by (ALLGOALS Asm_simp_tac);
   2.266 -qed "app_right_Nil";
   2.267 -Addsimps [app_right_Nil];
   2.268 -
   2.269 -Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
   2.270 -by (induct_tac "xs" 1);
   2.271 -by (ALLGOALS Asm_simp_tac);
   2.272 -qed "app_assoc";
   2.273 -
   2.274 -Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)";
   2.275 -by (induct_tac "ls" 1);
   2.276 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
   2.277 -qed "flat_app_distrib";
   2.278 -
   2.279 -(*** theorems about rev ***)
   2.280 -
   2.281 -Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))";
   2.282 -by (induct_tac "l" 1);
   2.283 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib])));
   2.284 -qed "rev_map_distrib";
   2.285 -
   2.286 -(*Simplifier needs the premises as assumptions because rewriting will not
   2.287 -  instantiate the variable ?A in the rules' typing conditions; note that
   2.288 -  rev_type does not instantiate ?A.  Only the premises do.
   2.289 -*)
   2.290 -Goal "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
   2.291 -by (etac list.induct 1);
   2.292 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
   2.293 -qed "rev_app_distrib";
   2.294 -
   2.295 -Goal "l: list(A) ==> rev(rev(l))=l";
   2.296 -by (induct_tac "l" 1);
   2.297 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
   2.298 -qed "rev_rev_ident";
   2.299 -Addsimps [rev_rev_ident];
   2.300 -
   2.301 -Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
   2.302 -by (induct_tac "ls" 1);
   2.303 -by (ALLGOALS
   2.304 -    (asm_simp_tac (simpset() addsimps 
   2.305 -		   [map_app_distrib, flat_app_distrib, rev_app_distrib])));
   2.306 -qed "rev_flat";
   2.307 -
   2.308 -
   2.309 -(*** theorems about list_add ***)
   2.310 -
   2.311 -Goal "[| xs: list(nat);  ys: list(nat) |] ==> \
   2.312 -\    list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
   2.313 -by (induct_tac "xs" 1);
   2.314 -by (ALLGOALS Asm_simp_tac);
   2.315 -qed "list_add_app";
   2.316 -
   2.317 -Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
   2.318 -by (induct_tac "l" 1);
   2.319 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
   2.320 -qed "list_add_rev";
   2.321 -
   2.322 -Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
   2.323 -by (induct_tac "ls" 1);
   2.324 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
   2.325 -by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1));
   2.326 -qed "list_add_flat";
   2.327 -
   2.328 -(** New induction rule **)
   2.329 -
   2.330 -val major::prems = Goal
   2.331 -    "[| l: list(A);  \
   2.332 -\       P(Nil);        \
   2.333 -\       !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x]) \
   2.334 -\    |] ==> P(l)";
   2.335 -by (rtac (major RS rev_rev_ident RS subst) 1);
   2.336 -by (rtac (major RS rev_type RS list.induct) 1);
   2.337 -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems)));
   2.338 -qed "list_append_induct";
   2.339 -
   2.340 -
   2.341 -(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
   2.342 -
   2.343 -(** min **)
   2.344 -(* Min theorems are also true for i, j ordinals *)
   2.345 -Goalw [min_def] "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)";
   2.346 -by (auto_tac (claset() addSDs [not_lt_imp_le] 
   2.347 -                       addDs [lt_not_sym] 
   2.348 -                       addIs [le_anti_sym], simpset()));
   2.349 -qed "min_sym";
   2.350 -
   2.351 -Goalw [min_def] "[| i:nat; j:nat |] ==> min(i,j):nat";
   2.352 -by Auto_tac;
   2.353 -qed "min_type";
   2.354 -AddTCs [min_type];
   2.355 -Addsimps [min_type];
   2.356 -
   2.357 -Goalw [min_def]  "i:nat ==> min(0,i) = 0";
   2.358 -by (auto_tac (claset() addDs [not_lt_imp_le], simpset()));
   2.359 -qed "min_0";
   2.360 -Addsimps [min_0];
   2.361 -
   2.362 -Goalw [min_def] "i:nat ==> min(i, 0) = 0";
   2.363 -by (auto_tac (claset() addDs [not_lt_imp_le], simpset()));
   2.364 -qed "min_02";
   2.365 -Addsimps [min_02];
   2.366 -
   2.367 -Goalw [min_def] "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k";
   2.368 -by (auto_tac (claset() addSDs [not_lt_imp_le]
   2.369 -                       addIs [lt_trans2, lt_trans], simpset()));
   2.370 -qed "lt_min_iff";
   2.371 -
   2.372 -Goalw [min_def]
   2.373 -     "[| i:nat; j:nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))";
   2.374 -by Auto_tac;
   2.375 -qed "min_succ_succ";
   2.376 -Addsimps [min_succ_succ];
   2.377 -
   2.378 -(*** more theorems about lists ***)
   2.379 -
   2.380 -Goal "xs:list(A) ==> (xs~=Nil)<->(EX y:A. EX ys:list(A). xs=Cons(y,ys))";
   2.381 -by (induct_tac "xs" 1);
   2.382 -by Auto_tac;
   2.383 -qed "neq_Nil_iff";
   2.384 -
   2.385 -(** filter **)
   2.386 -
   2.387 -Goal "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)";
   2.388 -by (induct_tac "xs" 1);
   2.389 -by Auto_tac;
   2.390 -qed "filter_append";
   2.391 -Addsimps [filter_append];
   2.392 -
   2.393 -Goal "xs:list(A) ==> filter(P, xs):list(A)";
   2.394 -by (induct_tac "xs" 1);
   2.395 -by Auto_tac;
   2.396 -qed "filter_type";
   2.397 -
   2.398 -Goal "xs:list(A) ==> length(filter(P, xs)) le length(xs)";
   2.399 -by (induct_tac "xs" 1);
   2.400 -by Auto_tac;
   2.401 -by (res_inst_tac [("j", "length(l)")] le_trans 1);
   2.402 -by (auto_tac (claset(), simpset() addsimps [le_iff]));
   2.403 -qed "length_filter";
   2.404 -
   2.405 -Goal "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)";
   2.406 -by (induct_tac "xs" 1);
   2.407 -by Auto_tac;
   2.408 -qed "filter_is_subset";
   2.409 -
   2.410 -Goal "xs:list(A) ==> filter(%p. False, xs) = Nil";
   2.411 -by (induct_tac "xs" 1);
   2.412 -by Auto_tac;
   2.413 -qed "filter_False";
   2.414 -
   2.415 -Goal "xs:list(A) ==> filter(%p. True, xs) = xs";
   2.416 -by (induct_tac "xs" 1);
   2.417 -by Auto_tac;
   2.418 -qed "filter_True";
   2.419 -Addsimps [filter_False, filter_True];
   2.420 -
   2.421 -(** length **)
   2.422 -
   2.423 -Goal "xs:list(A) ==> length(xs)=0 <-> xs=Nil";
   2.424 -by (etac list.induct 1);
   2.425 -by Auto_tac;
   2.426 -qed "length_is_0_iff";
   2.427 -Addsimps [length_is_0_iff];
   2.428 -
   2.429 -Goal "xs:list(A) ==> 0 = length(xs) <-> xs=Nil";
   2.430 -by (etac list.induct 1);
   2.431 -by Auto_tac;
   2.432 -qed "length_is_0_iff2";
   2.433 -Addsimps [length_is_0_iff2];
   2.434 -
   2.435 -Goal "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1";
   2.436 -by (etac list.induct 1);
   2.437 -by Auto_tac;
   2.438 -qed "length_tl";
   2.439 -Addsimps [length_tl];
   2.440 -
   2.441 -Goal "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil";
   2.442 -by (etac list.induct 1);
   2.443 -by Auto_tac;
   2.444 -qed "length_greater_0_iff";
   2.445 -
   2.446 -Goal "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)";
   2.447 -by (etac list.induct 1);
   2.448 -by Auto_tac;
   2.449 -qed "length_succ_iff";
   2.450 -
   2.451 -(** more theorems about append **)
   2.452 -
   2.453 -Goal "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)";
   2.454 -by (etac list.induct 1);
   2.455 -by Auto_tac;
   2.456 -qed "append_is_Nil_iff";
   2.457 -Addsimps [append_is_Nil_iff];
   2.458 -
   2.459 -Goal "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)";
   2.460 -by (etac list.induct 1);
   2.461 -by Auto_tac;
   2.462 -qed "append_is_Nil_iff2";
   2.463 -Addsimps [append_is_Nil_iff2];
   2.464 -
   2.465 -Goal "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)";
   2.466 -by (etac list.induct 1);
   2.467 -by Auto_tac;
   2.468 -qed "append_left_is_self_iff";
   2.469 -Addsimps [append_left_is_self_iff];
   2.470 -
   2.471 -Goal "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)";
   2.472 -by (etac list.induct 1);
   2.473 -by Auto_tac;
   2.474 -qed "append_left_is_self_iff2";
   2.475 -Addsimps [append_left_is_self_iff2];
   2.476 -
   2.477 -(*TOO SLOW as a default simprule!*)
   2.478 -Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
   2.479 -\  length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))";
   2.480 -by (etac list.induct 1);
   2.481 -by (auto_tac (claset(), simpset() addsimps [length_app]));
   2.482 -qed_spec_mp "append_left_is_Nil_iff";
   2.483 -
   2.484 -(*TOO SLOW as a default simprule!*)
   2.485 -Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
   2.486 -\  length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))";
   2.487 -by (etac list.induct 1);
   2.488 -by (auto_tac (claset(), simpset() addsimps [length_app]));
   2.489 -qed_spec_mp "append_left_is_Nil_iff2";
   2.490 -
   2.491 -Goal "xs:list(A) ==> ALL ys:list(A). \
   2.492 -\     length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)";
   2.493 -by (etac list.induct 1);
   2.494 -by (Asm_simp_tac 1);
   2.495 -by (Clarify_tac 1);
   2.496 -by (eres_inst_tac [("a", "ys")] list.elim 1);
   2.497 -by (ALLGOALS(Asm_full_simp_tac));
   2.498 -qed_spec_mp "append_eq_append_iff";
   2.499 -
   2.500 -
   2.501 -Goal "xs:list(A) ==>  \
   2.502 -\  ALL ys:list(A). ALL us:list(A). ALL vs:list(A). \
   2.503 -\  length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)";
   2.504 -by (induct_tac "xs" 1);
   2.505 -by (ALLGOALS(Clarify_tac));
   2.506 -by (asm_full_simp_tac (simpset() addsimps [length_app]) 1);
   2.507 -by (eres_inst_tac [("a", "ys")] list.elim 1);
   2.508 -by (Asm_full_simp_tac 1);
   2.509 -by (subgoal_tac "Cons(a, l) @ us =vs" 1);
   2.510 -by (dtac (rotate_prems 4 (append_left_is_Nil_iff RS iffD1)) 1);
   2.511 -by Auto_tac;
   2.512 -qed_spec_mp "append_eq_append";
   2.513 -
   2.514 -Goal "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |] \ 
   2.515 -\ ==>  xs@us = ys@vs <-> (xs=ys & us=vs)";
   2.516 -by (rtac iffI 1);
   2.517 -by (rtac append_eq_append 1);
   2.518 -by Auto_tac;
   2.519 -qed "append_eq_append_iff2";
   2.520 -Addsimps [append_eq_append_iff, append_eq_append_iff2];
   2.521 -
   2.522 -Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs";
   2.523 -by (Asm_simp_tac 1);
   2.524 -qed "append_self_iff";
   2.525 -Addsimps [append_self_iff];
   2.526 -
   2.527 -Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs";
   2.528 -by (Asm_simp_tac 1);
   2.529 -qed "append_self_iff2";
   2.530 -Addsimps [append_self_iff2];
   2.531 -
   2.532 -(* Can also be proved from append_eq_append_iff2,
   2.533 -but the proof requires two more hypotheses: x:A and y:A *)
   2.534 -Goal "xs:list(A) ==> ALL ys:list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)";
   2.535 -by (etac list.induct 1);
   2.536 -by (ALLGOALS(Clarify_tac));
   2.537 -by (ALLGOALS(eres_inst_tac [("a", "ys")] list.elim));
   2.538 -by Auto_tac;
   2.539 -qed_spec_mp "append1_eq_iff";
   2.540 -Addsimps [append1_eq_iff];
   2.541 -
   2.542 -Goal "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)";
   2.543 -by (asm_simp_tac (simpset() addsimps [append_left_is_Nil_iff]) 1);
   2.544 -qed "append_right_is_self_iff";
   2.545 -Addsimps [append_right_is_self_iff];
   2.546 -
   2.547 -Goal "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)";
   2.548 -by (rtac iffI 1);
   2.549 -by (dtac sym 1);
   2.550 -by (ALLGOALS(Asm_full_simp_tac));
   2.551 -qed "append_right_is_self_iff2";
   2.552 -Addsimps [append_right_is_self_iff2];
   2.553 -
   2.554 -Goal "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)";
   2.555 -by (induct_tac "xs" 1);
   2.556 -by Auto_tac;
   2.557 -qed_spec_mp "hd_append";
   2.558 -Addsimps [hd_append];
   2.559 -
   2.560 -Goal "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys";
   2.561 -by (induct_tac "xs" 1);
   2.562 -by Auto_tac;
   2.563 -qed_spec_mp "tl_append";
   2.564 -Addsimps [tl_append];
   2.565 -
   2.566 -(** rev **)
   2.567 -Goal "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)";
   2.568 -by (etac list.induct 1);
   2.569 -by Auto_tac;
   2.570 -qed "rev_is_Nil_iff";
   2.571 -Addsimps [rev_is_Nil_iff];
   2.572 -
   2.573 -Goal "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)";
   2.574 -by (etac list.induct 1);
   2.575 -by Auto_tac;
   2.576 -qed "Nil_is_rev_iff";
   2.577 -Addsimps [Nil_is_rev_iff];
   2.578 -
   2.579 -Goal "xs:list(A) ==> ALL ys:list(A). rev(xs)=rev(ys) <-> xs=ys";
   2.580 -by (etac list.induct 1);
   2.581 -by (Force_tac 1);
   2.582 -by (Clarify_tac 1);
   2.583 -by (eres_inst_tac [("a", "ys")] list.elim 1);
   2.584 -by Auto_tac;
   2.585 -qed_spec_mp "rev_is_rev_iff";
   2.586 -Addsimps [rev_is_rev_iff];
   2.587 -
   2.588 -Goal "xs:list(A) ==> \
   2.589 -\ (xs=Nil --> P) --> (ALL ys:list(A). ALL y:A. xs =ys@[y] -->P)-->P";
   2.590 -by (etac list_append_induct 1);
   2.591 -by Auto_tac;
   2.592 -qed_spec_mp "rev_list_elim_aux";
   2.593 -
   2.594 -bind_thm("rev_list_elim", impI RS ballI RS ballI RSN(3, rev_list_elim_aux));
   2.595 -
   2.596 -(** more theorems about drop **)
   2.597 -
   2.598 -Goal "n:nat ==> ALL xs:list(A). length(drop(n, xs)) = length(xs) #- n";
   2.599 -by (etac nat_induct 1);
   2.600 -by (auto_tac (claset() addEs [list.elim], simpset()));
   2.601 -qed_spec_mp "length_drop";
   2.602 -Addsimps [length_drop];
   2.603 -
   2.604 -Goal "n:nat ==> ALL xs:list(A). length(xs) le n --> drop(n, xs)=Nil";
   2.605 -by (etac nat_induct 1);
   2.606 -by (auto_tac (claset() addEs [list.elim], simpset()));
   2.607 -qed_spec_mp "drop_all";
   2.608 -Addsimps [drop_all];
   2.609 -
   2.610 -Goal "n:nat ==> ALL xs:list(A). drop(n, xs@ys) = \
   2.611 -\ drop(n,xs) @ drop(n #- length(xs), ys)"; 
   2.612 -by (induct_tac "n" 1);
   2.613 -by (auto_tac (claset() addEs [list.elim], simpset()));
   2.614 -qed_spec_mp "drop_append";
   2.615 -
   2.616 -Goal "m:nat ==> \
   2.617 -\ ALL xs:list(A). ALL n:nat. drop(n, drop(m, xs))=drop(n #+ m, xs)";
   2.618 -by (induct_tac "m" 1);
   2.619 -by (auto_tac (claset() addEs [list.elim], simpset()));
   2.620 -qed "drop_drop";
   2.621 -
   2.622 -(** take **)
   2.623 -
   2.624 -Goalw [take_def]
   2.625 - "xs:list(A) ==> take(0, xs) =  Nil";
   2.626 -by (etac list.induct 1);
   2.627 -by Auto_tac;
   2.628 -qed "take_0";
   2.629 -Addsimps [take_0];
   2.630 -
   2.631 -Goalw [take_def]
   2.632 -"n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))";
   2.633 -by (Asm_simp_tac 1);
   2.634 -qed "take_succ_Cons";
   2.635 -Addsimps [take_succ_Cons];
   2.636 -
   2.637 -(* Needed for proving take_all *)
   2.638 -Goalw [take_def]
   2.639 - "n:nat ==> take(n, Nil) = Nil";
   2.640 -by Auto_tac;
   2.641 -qed "take_Nil";
   2.642 -Addsimps [take_Nil];
   2.643 - 
   2.644 -Goal "n:nat ==> ALL xs:list(A). length(xs) le n  --> take(n, xs) = xs";
   2.645 -by (etac nat_induct 1);
   2.646 -by (auto_tac (claset() addEs [list.elim], simpset()));
   2.647 -qed_spec_mp  "take_all";
   2.648 -Addsimps [take_all];
   2.649 -
   2.650 -Goal "xs:list(A) ==> ALL n:nat. take(n, xs):list(A)";
   2.651 -by (etac list.induct 1);
   2.652 -by (Clarify_tac 2);
   2.653 -by (etac natE 2);
   2.654 -by Auto_tac;
   2.655 -qed_spec_mp "take_type";
   2.656 -
   2.657 -Goal "xs:list(A) ==> \
   2.658 -\ ALL ys:list(A). ALL n:nat. take(n, xs @ ys) = \
   2.659 -\                           take(n, xs) @ take(n #- length(xs), ys)";
   2.660 -by (etac list.induct 1);
   2.661 -by (Clarify_tac 2);
   2.662 -by (etac natE 2);
   2.663 -by Auto_tac;
   2.664 -qed_spec_mp "take_append";
   2.665 -Addsimps [take_append];
   2.666 -
   2.667 -Goal
   2.668 -"m:nat ==> \
   2.669 -\ ALL xs:list(A). ALL n:nat. take(n, take(m,xs))= take(min(n, m), xs)";
   2.670 -by (induct_tac "m" 1);
   2.671 -by Auto_tac;
   2.672 -by (eres_inst_tac [("a", "xs")] list.elim 1);
   2.673 -by (auto_tac (claset(), simpset() addsimps [take_Nil]));
   2.674 -by (rotate_tac 1 1);
   2.675 -by (etac natE 1);
   2.676 -by (auto_tac (claset() addIs [take_0, take_type], simpset()));
   2.677 -qed_spec_mp "take_take";
   2.678 -
   2.679 -(** nth **)
   2.680 -
   2.681 -Goalw [nth_def] "nth(0, Cons(a, l))= a";
   2.682 -by Auto_tac;
   2.683 -qed "nth_0";
   2.684 -Addsimps [nth_0];
   2.685 -
   2.686 -Goalw [nth_def]  
   2.687 -   "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)";
   2.688 -by (Asm_simp_tac 1);
   2.689 -qed "nth_Cons";
   2.690 -Addsimps [nth_Cons];
   2.691 -
   2.692 -Goal "xs:list(A) ==> ALL n:nat. n < length(xs) --> nth(n, xs):A";
   2.693 -by (etac list.induct 1);
   2.694 -by (ALLGOALS(Clarify_tac));
   2.695 -by (etac natE 2);
   2.696 -by (ALLGOALS(Asm_full_simp_tac));
   2.697 -qed_spec_mp "nth_type";
   2.698 -
   2.699 -AddTCs [nth_type];
   2.700 -Addsimps [nth_type];
   2.701 -
   2.702 -Goal 
   2.703 -"xs:list(A) ==> ALL n:nat. \
   2.704 -\ nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) \
   2.705 -\                      else nth(n #- length(xs),ys))";
   2.706 -by (induct_tac "xs" 1);
   2.707 -by (Clarify_tac 2);
   2.708 -by (etac natE 2);
   2.709 -by (ALLGOALS(Asm_full_simp_tac));
   2.710 -qed_spec_mp "nth_append";
   2.711 -
   2.712 -Goal "xs:list(A) \
   2.713 -\     ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}";
   2.714 -by (induct_tac "xs" 1);
   2.715 -by (ALLGOALS(Asm_simp_tac));
   2.716 -by (rtac equalityI 1);
   2.717 -by Auto_tac;
   2.718 -by (res_inst_tac [("x", "0")] bexI 1);
   2.719 -by Auto_tac;
   2.720 -by (etac natE 1);
   2.721 -by Auto_tac;
   2.722 -qed "set_of_list_conv_nth";
   2.723 -
   2.724 -(* Other theorems about lists *)
   2.725 -
   2.726 -Goalw [Ball_def]
   2.727 - "k:nat ==> \
   2.728 -\ ALL xs:list(A). (ALL ys:list(A). k le length(xs) --> k le length(ys) -->  \
   2.729 -\     (ALL i:nat. i<k --> nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))";
   2.730 -by (induct_tac "k" 1);
   2.731 -by (ALLGOALS (asm_simp_tac (simpset() addsimps 
   2.732 -             [lt_succ_eq_0_disj, all_conj_distrib])));
   2.733 -by (Clarify_tac 1);
   2.734 -(*Both lists must be non-empty*)
   2.735 -by (case_tac "xa=Nil" 1);
   2.736 -by (case_tac "xb=Nil" 2);
   2.737 -by (Clarify_tac 1);
   2.738 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
   2.739 -by (Clarify_tac 1);
   2.740 -(*prenexing's needed, not miniscoping*)
   2.741 -by (Asm_simp_tac 1);
   2.742 -by (rtac conjI 1);
   2.743 -by (Force_tac 1);
   2.744 -by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [iff_sym])  
   2.745 -                                       delsimps (all_simps))));
   2.746 -by (dres_inst_tac [("x", "ys"), ("x1", "ysa")] (spec RS spec) 1);
   2.747 -by (Clarify_tac 1);
   2.748 -by Auto_tac;
   2.749 -qed_spec_mp "nth_take_lemma";
   2.750 -
   2.751 -Goal "[| xs:list(A); ys:list(A); length(xs) = length(ys);  \
   2.752 -\        ALL i:nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |]  \
   2.753 -\     ==> xs = ys";
   2.754 -by (subgoal_tac "length(xs) le length(ys)" 1);
   2.755 -by (forw_inst_tac [("ys", "ys")] (rotate_prems 1 nth_take_lemma) 1);
   2.756 -by (ALLGOALS(Asm_simp_tac));
   2.757 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [take_all])));
   2.758 -qed_spec_mp "nth_equalityI";
   2.759 -
   2.760 -(*The famous take-lemma*)
   2.761 -
   2.762 -Goal "[| xs:list(A); ys:list(A); (ALL i:nat. take(i, xs) = take(i,ys)) |] ==> xs = ys";
   2.763 -by (case_tac "length(xs) le length(ys)" 1);
   2.764 -by (dres_inst_tac [("x", "length(ys)")] bspec 1);
   2.765 -by (dtac not_lt_imp_le 3);
   2.766 -by (subgoal_tac "length(ys) le length(xs)" 5);
   2.767 -by (res_inst_tac [("j", "succ(length(ys))")] le_trans 6);
   2.768 -by (rtac leI 6);
   2.769 -by (dres_inst_tac [("x", "length(xs)")] bspec 5);
   2.770 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [take_all])));
   2.771 -qed_spec_mp "take_equalityI";
   2.772 -
   2.773 -Goal "n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \
   2.774 -\               --> nth(i, drop(n, xs)) = nth(n #+ i, xs)";
   2.775 -by (induct_tac "n" 1);
   2.776 -by (ALLGOALS(Asm_full_simp_tac));
   2.777 -by (Clarify_tac 1);
   2.778 -by (case_tac "xb=Nil" 1);
   2.779 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
   2.780 -by (Clarify_tac 1);
   2.781 -by (auto_tac (claset() addSEs [ConsE], simpset()));
   2.782 -qed_spec_mp "nth_drop";
   2.783 -
   2.784 -(** zip **)
   2.785 -
   2.786 -Goal "l:list(A) ==> l:list(set_of_list(l))";
   2.787 -by (induct_tac "l" 1);
   2.788 -by Auto_tac;
   2.789 -by (res_inst_tac [("A1", "set_of_list(l)")] (list_mono RS subsetD) 1);
   2.790 -by Auto_tac;
   2.791 -qed "list_on_set_of_list";
   2.792 -
   2.793 -Goal "A<=C ==> ziprel(A, B) <= ziprel(C,B)";
   2.794 -by (Clarify_tac 1);
   2.795 -by (forward_tac [ziprel.dom_subset RS subsetD] 1);
   2.796 -by (Clarify_tac 1);
   2.797 -by (etac ziprel.induct 1);
   2.798 -by (auto_tac (claset() addIs [list_mono RS subsetD]
   2.799 -                       addSIs ziprel.intrs, simpset()));
   2.800 -qed "ziprel_mono1";
   2.801 -
   2.802 -Goal "B<=C ==> ziprel(A, B) <= ziprel(A,C)";
   2.803 -by (Clarify_tac 1);
   2.804 -by (forward_tac [ziprel.dom_subset RS subsetD] 1);
   2.805 -by (Clarify_tac 1);
   2.806 -by (etac ziprel.induct 1);
   2.807 -by (auto_tac (claset() addIs [list_mono RS subsetD]
   2.808 -                       addSIs ziprel.intrs, simpset()));
   2.809 -qed "ziprel_mono2";
   2.810 -
   2.811 -Goal "[| A<=C; B<=D |] ==> ziprel(A, B) <= ziprel(C,D)";
   2.812 -by (rtac subset_trans 1);
   2.813 -by (rtac ziprel_mono1 2);
   2.814 -by (rtac ziprel_mono2 1);
   2.815 -by Auto_tac;
   2.816 -qed "ziprel_mono";
   2.817 -
   2.818 -(* ziprel is a function *)
   2.819 -
   2.820 -Goal "<xs, ys, zs>:ziprel(A,B) \
   2.821 -\     ==> ALL ks. <xs, ys, ks>:ziprel(A, B) --> ks=zs";
   2.822 -by (etac ziprel.induct 1);
   2.823 -by (ALLGOALS(Clarify_tac));
   2.824 -by (rotate_tac 1 3);
   2.825 -by (ALLGOALS(etac ziprel.elim));
   2.826 -by Safe_tac;
   2.827 -(* These hypotheses make Auto_tac loop! *)
   2.828 -by (thin_tac "ALL k. ?P(k)" 3);
   2.829 -by (thin_tac "ALL k. ?P(k)" 4);
   2.830 -by Auto_tac;
   2.831 -qed "ziprel_is_fun";
   2.832 -
   2.833 -Goal "ys:list(B)  ==> ALL xs:list(A). EX zs. <xs, ys, zs>:ziprel(A,B)";
   2.834 -by (induct_tac "ys" 1);
   2.835 -by (auto_tac (claset() addIs ziprel.intrs, simpset()));
   2.836 -by (eres_inst_tac [("a", "xs")] list.elim 1);
   2.837 -by (auto_tac (claset() addIs ziprel.intrs, simpset()));
   2.838 -qed_spec_mp "ziprel_exist"; 
   2.839 -
   2.840 -Goalw [zip_def]
   2.841 - "[|xs:list(A); ys:list(B) |] ==> <xs, ys, zip(xs,ys)>:ziprel(A,B)";
   2.842 -by (rtac theI2 1);
   2.843 -by (asm_full_simp_tac (simpset() addsimps [set_of_list_append]) 2);
   2.844 -by (REPEAT(dtac set_of_list_type 2));
   2.845 -by (rtac (ziprel_mono RS subsetD) 2);
   2.846 -by (Blast_tac 3);
   2.847 -by (dtac list_on_set_of_list 1);
   2.848 -by (dtac list_on_set_of_list 1);
   2.849 -by (subgoal_tac "xs:list(set_of_list(xs@ys)) & \
   2.850 -\                ys:list(set_of_list(xs@ys))" 1);
   2.851 -by (auto_tac (claset() addIs [list_mono RS subsetD],
   2.852 -              simpset() addsimps [set_of_list_append]));
   2.853 -by (rtac (ziprel_is_fun RS spec RS mp) 2); 
   2.854 -by (rtac ziprel_exist 1);
   2.855 -by Auto_tac;
   2.856 -qed "zip_in_ziprel";
   2.857 -
   2.858 -Goal
   2.859 -"<xs, ys, zs>:ziprel(A,B) ==> zip(xs, ys)=zs";
   2.860 -by (rtac (ziprel_is_fun RS spec RS mp) 1);
   2.861 -by (Blast_tac 1);
   2.862 -by (blast_tac (claset() addDs [ziprel.dom_subset RS subsetD]
   2.863 -                        addIs [zip_in_ziprel]) 1);
   2.864 -qed "zip_eq";
   2.865 -
   2.866 -(* zip equations *)
   2.867 -
   2.868 -Goal "ys:list(A) ==> zip(Nil, ys)=Nil";
   2.869 -by (res_inst_tac [("A", "A")] zip_eq 1);
   2.870 -by (auto_tac (claset() addIs ziprel.intrs, simpset()));
   2.871 -qed "zip_Nil";
   2.872 -Addsimps [zip_Nil];
   2.873 -
   2.874 -Goal "xs:list(A) ==> zip(xs, Nil)=Nil";
   2.875 -by (res_inst_tac [("A", "A")] zip_eq 1);
   2.876 -by (auto_tac (claset() addIs ziprel.intrs, simpset()));
   2.877 -qed "zip_Nil2";
   2.878 -Addsimps [zip_Nil2];
   2.879 -
   2.880 -Goal "[| xs:list(A); ys:list(B); x:A; y:B |] ==> \
   2.881 -\ zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))";
   2.882 -by (res_inst_tac [("A", "A")] zip_eq 1);
   2.883 -by (forw_inst_tac [("ys", "ys")] zip_in_ziprel 1);
   2.884 -by (auto_tac (claset() addIs ziprel.intrs, simpset()));
   2.885 -qed "zip_Cons_Cons";
   2.886 -Addsimps [zip_Cons_Cons];
   2.887 -
   2.888 -Goal "xs:list(A) ==> ALL ys:list(B). zip(xs, ys):list(A*B)";
   2.889 -by (induct_tac "xs" 1);
   2.890 -by (Simp_tac 1);
   2.891 -by (Clarify_tac 1);
   2.892 -by (eres_inst_tac [("a", "ys")] list.elim 1);
   2.893 -by Auto_tac;
   2.894 -qed_spec_mp "zip_type";
   2.895 -
   2.896 -AddTCs [zip_type];
   2.897 -Addsimps [zip_type];    
   2.898 -
   2.899 -(* zip length *)
   2.900 -Goalw [min_def] "xs:list(A) ==> ALL ys:list(B). length(zip(xs,ys)) = \
   2.901 -\                               min(length(xs), length(ys))";
   2.902 -by (induct_tac "xs" 1);
   2.903 -by (Clarify_tac 2);
   2.904 -by (eres_inst_tac [("a", "ys")] list.elim 2);
   2.905 -by Auto_tac;
   2.906 -qed_spec_mp "length_zip";  
   2.907 -Addsimps [length_zip];
   2.908 -
   2.909 -AddTCs [take_type];
   2.910 -Addsimps [take_type];
   2.911 -
   2.912 -Goal "[| ys:list(A); zs:list(B) |] ==> ALL xs:list(A). zip(xs @ ys, zs) = \
   2.913 -\ zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))";
   2.914 -by (induct_tac "zs" 1);
   2.915 -by (Clarify_tac 2);
   2.916 -by (eres_inst_tac [("a", "xs")] list.elim 2);
   2.917 -by Auto_tac;
   2.918 -qed_spec_mp "zip_append1";
   2.919 -
   2.920 -Goal
   2.921 - "[| xs:list(A); zs:list(B) |] ==> ALL ys:list(B). zip(xs, ys@zs) = \
   2.922 -\      zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)";
   2.923 -by (induct_tac "xs" 1);
   2.924 -by (Clarify_tac 2);
   2.925 -by (eres_inst_tac [("a", "ys")] list.elim 2);
   2.926 -by Auto_tac;
   2.927 -qed_spec_mp "zip_append2";
   2.928 -
   2.929 -Goal
   2.930 - "[| length(xs) = length(us); length(ys) = length(vs); \
   2.931 -\  xs:list(A); us:list(B); ys:list(A); vs:list(B) |] ==> \
   2.932 -\ zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)";
   2.933 -by (asm_simp_tac (simpset() addsimps 
   2.934 -                  [zip_append1, drop_append, diff_self_eq_0]) 1);
   2.935 -qed_spec_mp "zip_append";
   2.936 -Addsimps [zip_append];
   2.937 -
   2.938 -Goal "ys:list(B) ==> ALL xs:list(A).  \
   2.939 -\ length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))";
   2.940 -by (induct_tac "ys" 1);
   2.941 -by (Clarify_tac 2);
   2.942 -by (eres_inst_tac [("a", "xs")] list.elim 2);
   2.943 -by (auto_tac (claset(), simpset() addsimps [length_rev]));
   2.944 -qed_spec_mp "zip_rev";
   2.945 -Addsimps [zip_rev];
   2.946 -
   2.947 -Goal
   2.948 -"ys:list(B) ==> ALL i:nat. ALL xs:list(A). \
   2.949 -\                   i < length(xs) --> i < length(ys) --> \
   2.950 -\                   nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>";
   2.951 -by (induct_tac "ys" 1);
   2.952 -by (Clarify_tac 2);
   2.953 -by (eres_inst_tac [("a", "xs")] list.elim 2);
   2.954 -by (auto_tac (claset() addEs [natE], simpset()));
   2.955 -qed_spec_mp "nth_zip";
   2.956 -Addsimps [nth_zip];
   2.957 -
   2.958 -Goal "[| xs:list(A); ys:list(B); i:nat |] \
   2.959 -\     ==> set_of_list(zip(xs, ys)) = \
   2.960 -\         {<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys))  \
   2.961 -\         & x=nth(i, xs) & y=nth(i, ys)}";
   2.962 -by (force_tac (claset() addSIs [Collect_cong], 
   2.963 -               simpset() addsimps [lt_min_iff, set_of_list_conv_nth]) 1);
   2.964 -qed_spec_mp "set_of_list_zip";
   2.965 -
   2.966 -(** list_update **)
   2.967 -
   2.968 -Goalw [list_update_def] "i:nat ==>list_update(Nil, i, v) = Nil";
   2.969 -by Auto_tac;
   2.970 -qed "list_update_Nil";
   2.971 -Addsimps [list_update_Nil];
   2.972 -
   2.973 -Goalw [list_update_def] 
   2.974 -"list_update(Cons(x, xs), 0, v)= Cons(v, xs)";
   2.975 -by Auto_tac;
   2.976 -qed "list_update_Cons_0";
   2.977 -Addsimps [list_update_Cons_0];
   2.978 -
   2.979 -Goalw [list_update_def] 
   2.980 -"n:nat ==>\
   2.981 -\ list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))";
   2.982 -by Auto_tac;
   2.983 -qed "list_update_Cons_succ";
   2.984 -Addsimps [list_update_Cons_succ];
   2.985 -
   2.986 -Goal "[| xs:list(A); v:A |] ==> ALL n:nat. list_update(xs, n, v):list(A)";
   2.987 -by (induct_tac "xs" 1);
   2.988 -by (Simp_tac 1);
   2.989 -by (Clarify_tac 1);
   2.990 -by (etac natE 1);
   2.991 -by Auto_tac;
   2.992 -qed_spec_mp "list_update_type";
   2.993 -Addsimps [list_update_type];
   2.994 -AddTCs [list_update_type];
   2.995 -
   2.996 -Goal "xs:list(A) ==> ALL i:nat. length(list_update(xs, i, v))=length(xs)";
   2.997 -by (induct_tac "xs" 1);
   2.998 -by (Simp_tac 1);
   2.999 -by (Clarify_tac 1);
  2.1000 -by (etac natE 1);
  2.1001 -by Auto_tac;
  2.1002 -qed_spec_mp "length_list_update";
  2.1003 -Addsimps [length_list_update];
  2.1004 -
  2.1005 -Goal "[| xs:list(A) |] ==> ALL i:nat. ALL j:nat. i < length(xs)  --> \
  2.1006 -\ nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))";
  2.1007 -by (induct_tac "xs" 1);
  2.1008 - by (Simp_tac 1);
  2.1009 -by (Clarify_tac 1);
  2.1010 -by (etac natE 1);
  2.1011 -by (ALLGOALS(Asm_full_simp_tac));
  2.1012 -by (ALLGOALS(Clarify_tac));
  2.1013 -by (etac natE 1);
  2.1014 -by (ALLGOALS(Asm_full_simp_tac));
  2.1015 -by Safe_tac;
  2.1016 -by (etac natE 2);
  2.1017 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nth_Cons])));
  2.1018 -qed_spec_mp "nth_list_update";
  2.1019 -
  2.1020 -Goal "[| i < length(xs); xs:list(A); i:nat |] \
  2.1021 -\  ==> nth(i, list_update(xs, i,x)) = x";
  2.1022 -by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
  2.1023 -qed "nth_list_update_eq";
  2.1024 -Addsimps [nth_list_update_eq];
  2.1025 -
  2.1026 -Goal "xs:list(A) ==> ALL i:nat. ALL j:nat. i ~= j \
  2.1027 -\ --> nth(j, list_update(xs, i,x)) = nth(j, xs)";
  2.1028 -by (induct_tac "xs" 1);
  2.1029 - by (Simp_tac 1);
  2.1030 -by (Clarify_tac 1);
  2.1031 -by (etac natE 1);
  2.1032 -by (etac natE 2);
  2.1033 -by (ALLGOALS(Asm_full_simp_tac));
  2.1034 -by (etac natE 1);
  2.1035 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nth_Cons])));
  2.1036 -qed_spec_mp "nth_list_update_neq";
  2.1037 -Addsimps [nth_list_update_neq];
  2.1038 -
  2.1039 -Goal "xs:list(A) ==> ALL i:nat. i < length(xs)\
  2.1040 -\  --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)";
  2.1041 -by (induct_tac "xs" 1);
  2.1042 - by (Simp_tac 1);
  2.1043 -by (Clarify_tac 1);
  2.1044 -by (etac natE 1);
  2.1045 -by Auto_tac;
  2.1046 -qed_spec_mp "list_update_overwrite";
  2.1047 -Addsimps [list_update_overwrite];
  2.1048 -
  2.1049 -Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \
  2.1050 -\ (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)";
  2.1051 -by (induct_tac "xs" 1);
  2.1052 - by (Simp_tac 1);
  2.1053 -by (Clarify_tac 1);
  2.1054 -by (etac natE 1);
  2.1055 -by Auto_tac;
  2.1056 -qed_spec_mp "list_update_same_conv";
  2.1057 -
  2.1058 -Goal "ys:list(B) ==> ALL i:nat. ALL xy:A*B. ALL xs:list(A). \
  2.1059 -\ length(xs) = length(ys) --> \
  2.1060 -\     list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)), \
  2.1061 -\                                         list_update(ys, i, snd(xy)))";
  2.1062 -by (induct_tac "ys" 1);
  2.1063 - by Auto_tac;
  2.1064 -by (eres_inst_tac [("a", "xc")] list.elim 1);
  2.1065 -by (auto_tac (claset() addEs [natE], simpset()));
  2.1066 -qed_spec_mp "update_zip";
  2.1067 -
  2.1068 -Goal "xs:list(A) ==> ALL i:nat. set_of_list(list_update(xs, i, x)) \
  2.1069 -\  <= cons(x, set_of_list(xs))";
  2.1070 -by (induct_tac "xs" 1);
  2.1071 - by (asm_full_simp_tac (simpset() addsimps []) 1);
  2.1072 -by (rtac ballI 1);
  2.1073 -by (etac natE 1);
  2.1074 -by (ALLGOALS(Asm_full_simp_tac));
  2.1075 -by Auto_tac;
  2.1076 -qed_spec_mp "set_update_subset_cons";
  2.1077 -
  2.1078 -Goal "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|]  \
  2.1079 -\  ==> set_of_list(list_update(xs, i,x)) <= A";
  2.1080 -by (rtac subset_trans 1);
  2.1081 -by (rtac set_update_subset_cons 1);
  2.1082 -by Auto_tac;
  2.1083 -qed "set_of_list_update_subsetI";
  2.1084 -
  2.1085 -(** upt **)
  2.1086 -
  2.1087 -Goal "[| i:nat; j:nat |] \
  2.1088 -\ ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)";
  2.1089 -by (induct_tac "j" 1);
  2.1090 -by Auto_tac;
  2.1091 -by (dtac not_lt_imp_le 1);
  2.1092 -by (auto_tac (claset() addIs [le_anti_sym], simpset()));
  2.1093 -qed "upt_rec";
  2.1094 -
  2.1095 -Goal "[| j le i; i:nat; j:nat |] ==> upt(i,j) = Nil";
  2.1096 -by (stac upt_rec 1);
  2.1097 -by Auto_tac;
  2.1098 -by (auto_tac (claset(), simpset() addsimps [le_iff]));
  2.1099 -by (dtac (lt_asym RS notE) 1);
  2.1100 -by Auto_tac;
  2.1101 -qed "upt_conv_Nil";
  2.1102 -Addsimps [upt_conv_Nil];
  2.1103 -
  2.1104 -(*Only needed if upt_Suc is deleted from the simpset*)
  2.1105 -Goal "[| i le j; i:nat; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]";
  2.1106 -by (Asm_simp_tac 1);
  2.1107 -qed "upt_succ_append";
  2.1108 -
  2.1109 -Goal "[| i<j; i:nat; j:nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))";
  2.1110 -by (rtac trans 1);
  2.1111 -by (stac upt_rec 1);
  2.1112 -by (rtac refl 4);
  2.1113 -by Auto_tac;
  2.1114 -qed "upt_conv_Cons";
  2.1115 -
  2.1116 -Goal "[| i:nat; j:nat |] ==> upt(i,j):list(nat)";
  2.1117 -by (induct_tac "j" 1);
  2.1118 -by Auto_tac;
  2.1119 -qed "upt_type";
  2.1120 -
  2.1121 -AddTCs [upt_type];
  2.1122 -Addsimps [upt_type];
  2.1123 -
  2.1124 -(*LOOPS as a simprule, since j<=j*)
  2.1125 -Goal "[| i le j; i:nat; j:nat; k:nat |] ==> \
  2.1126 -\ upt(i, j #+k) = upt(i,j)@upt(j,j#+k)";
  2.1127 -by (induct_tac "k" 1);
  2.1128 -by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type]));
  2.1129 -by (res_inst_tac [("j", "j")] le_trans 1);
  2.1130 -by Auto_tac;
  2.1131 -qed "upt_add_eq_append";
  2.1132 -
  2.1133 -Goal "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i";
  2.1134 -by (induct_tac "j" 1);
  2.1135 -by (rtac sym 2);
  2.1136 -by (auto_tac (claset() addSDs [not_lt_imp_le], 
  2.1137 -              simpset() addsimps [length_app, diff_succ, diff_is_0_iff]));
  2.1138 -qed "length_upt";
  2.1139 -Addsimps [length_upt];
  2.1140 -
  2.1141 -Goal "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k";
  2.1142 -by (induct_tac "j" 1);
  2.1143 -by (Asm_simp_tac 1);
  2.1144 -by (asm_full_simp_tac (simpset() addsimps [nth_append,le_iff] 
  2.1145 -                                 addsplits [nat_diff_split]) 1);
  2.1146 -by Safe_tac;
  2.1147 -by (auto_tac (claset() addSDs [not_lt_imp_le], 
  2.1148 -              simpset() addsimps [nth_append, diff_self_eq_0, 
  2.1149 -                                  less_diff_conv, add_commute])); 
  2.1150 -by (dres_inst_tac [("j", "x")] lt_trans2 1);
  2.1151 -by Auto_tac;
  2.1152 -qed_spec_mp "nth_upt";
  2.1153 -Addsimps [nth_upt];
  2.1154 -
  2.1155 -Goal "[| m:nat; n:nat |] ==> \
  2.1156 -\ ALL i:nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)";
  2.1157 -by (induct_tac "m" 1);
  2.1158 -by (asm_simp_tac (simpset() addsimps [take_0]) 1);
  2.1159 -by (Clarify_tac 1);
  2.1160 -by (stac upt_rec 1);
  2.1161 -by (rtac sym 3);
  2.1162 -by (stac upt_rec 3);
  2.1163 -by (ALLGOALS(asm_full_simp_tac (simpset() delsimps (thms"upt.simps"))));
  2.1164 -by (res_inst_tac [("j", "succ(i #+ x)")] lt_trans2 1);
  2.1165 -by Auto_tac;
  2.1166 -qed_spec_mp "take_upt";
  2.1167 -Addsimps [take_upt];
  2.1168 -
  2.1169 -Goal "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))";
  2.1170 -by (induct_tac "n" 1);
  2.1171 -by (auto_tac (claset(), simpset() addsimps [map_app_distrib]));
  2.1172 -qed "map_succ_upt";
  2.1173 -
  2.1174 -Goal "xs:list(A) ==> \
  2.1175 -\ ALL n:nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))";
  2.1176 -by (induct_tac "xs" 1);
  2.1177 -by (Asm_full_simp_tac 1);
  2.1178 -by (rtac ballI 1);
  2.1179 -by (induct_tac "n" 1);
  2.1180 -by Auto_tac;
  2.1181 -qed_spec_mp "nth_map";
  2.1182 -Addsimps [nth_map];
  2.1183 -
  2.1184 -Goal "[| m:nat; n:nat |] ==> \
  2.1185 -\ ALL i:nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)";
  2.1186 -by (res_inst_tac [("n", "m"), ("m", "n")] diff_induct 1);
  2.1187 -by (stac (map_succ_upt RS sym) 5);
  2.1188 -by (ALLGOALS(Asm_full_simp_tac));
  2.1189 -by (ALLGOALS(Clarify_tac));
  2.1190 -by (subgoal_tac "xa < length(upt(0, x))" 1);
  2.1191 -by (Asm_simp_tac 2);
  2.1192 -by (subgoal_tac "xa < length(upt(y, x))" 2);
  2.1193 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [map_compose, 
  2.1194 -          nth_map, add_commute, less_diff_conv])));
  2.1195 -by (res_inst_tac [("j", "succ(xa #+ y)")] lt_trans2 1);
  2.1196 -by Auto_tac;
  2.1197 -qed_spec_mp "nth_map_upt";
  2.1198 -
  2.1199 -(** sublist (a generalization of nth to sets) **)
  2.1200 -
  2.1201 -Goalw [sublist_def] "xs:list(A) ==>sublist(xs, 0) =Nil";
  2.1202 -by Auto_tac;
  2.1203 -qed "sublist_0";
  2.1204 -
  2.1205 -Goalw [sublist_def] "sublist(Nil, A) = Nil";
  2.1206 -by Auto_tac;
  2.1207 -qed "sublist_Nil";
  2.1208 -
  2.1209 -AddTCs [filter_type];
  2.1210 -Addsimps [filter_type];
  2.1211 -
  2.1212 -Goal "[| xs:list(B); i:nat |] ==>\
  2.1213 -\    map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) = \
  2.1214 -\    map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))";
  2.1215 -by (etac list_append_induct  1);
  2.1216 -by (Asm_simp_tac 1);
  2.1217 -by (auto_tac (claset(), simpset() addsimps 
  2.1218 -         [add_commute, length_app, filter_append, map_app_distrib]));
  2.1219 -qed "sublist_shift_lemma";
  2.1220 -
  2.1221 -Goalw [sublist_def]
  2.1222 - "xs:list(B) ==> sublist(xs, A):list(B)";
  2.1223 -by (induct_tac "xs" 1);
  2.1224 -by (auto_tac (claset(), simpset() addsimps [filter_append, map_app_distrib]));
  2.1225 -by (auto_tac (claset() addIs [map_type,filter_type,zip_type], simpset()));
  2.1226 -qed "sublist_type";
  2.1227 -
  2.1228 -AddTCs [sublist_type];
  2.1229 -Addsimps [sublist_type];
  2.1230 -
  2.1231 -Goal "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)";
  2.1232 -by (asm_simp_tac (simpset() addsimps 
  2.1233 -                [inst "i" "0" upt_add_eq_append, nat_0_le]) 1);
  2.1234 -qed "upt_add_eq_append2";
  2.1235 -
  2.1236 -Goalw [sublist_def]
  2.1237 -     "[| xs:list(B); ys:list(B)  |] ==> \
  2.1238 -\ sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})";
  2.1239 -by (eres_inst_tac [("l", "ys")] list_append_induct 1);
  2.1240 -by (Asm_simp_tac 1);
  2.1241 -by (asm_simp_tac (simpset() addsimps [upt_add_eq_append2, 
  2.1242 -                                      zip_append, length_app,  app_assoc RS sym]) 1);
  2.1243 -by (auto_tac (claset(), simpset() addsimps [sublist_shift_lemma, 
  2.1244 -                                           length_type, map_app_distrib, app_assoc]));
  2.1245 -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [add_commute])));
  2.1246 -qed "sublist_append";
  2.1247 -
  2.1248 -Addsimps [sublist_0, sublist_Nil];
  2.1249 -
  2.1250 -Goal "[| xs:list(B); x:B |] ==> \
  2.1251 -\ sublist(Cons(x, xs), A) = (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})";
  2.1252 -by (eres_inst_tac [("l", "xs")] list_append_induct 1);
  2.1253 -by (asm_simp_tac (simpset() addsimps [sublist_def]) 1);
  2.1254 -by (asm_simp_tac (simpset() delsimps (thms "op @.simps") 
  2.1255 -                 addsimps [(hd (tl (thms "op @.simps"))) RS sym, sublist_append]) 1);
  2.1256 -by Auto_tac;
  2.1257 -qed "sublist_Cons";
  2.1258 -
  2.1259 -Goal "sublist([x], A) = (if 0 : A then [x] else [])";
  2.1260 -by (simp_tac (simpset() addsimps [sublist_Cons]) 1);
  2.1261 -qed "sublist_singleton";
  2.1262 -Addsimps [sublist_singleton];
  2.1263 -
  2.1264 -Goalw [less_than_def]
  2.1265 -    "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)";
  2.1266 -by (eres_inst_tac [("l", "xs")] list_append_induct 1);
  2.1267 - by (asm_simp_tac (simpset() addsplits [nat_diff_split]
  2.1268 -                             addsimps [sublist_append]) 2);
  2.1269 -by Auto_tac;
  2.1270 -by (subgoal_tac "n #- length(y) = 0" 1);
  2.1271 -by (Asm_simp_tac 1);
  2.1272 -by (auto_tac (claset() addSDs [not_lt_imp_le], 
  2.1273 -          simpset() addsimps [diff_is_0_iff]));
  2.1274 -qed "sublist_upt_eq_take";
  2.1275 -Addsimps [sublist_upt_eq_take];
  2.1276 -
     3.1 --- a/src/ZF/List.thy	Tue Jul 09 18:54:27 2002 +0200
     3.2 +++ b/src/ZF/List.thy	Tue Jul 09 23:03:21 2002 +0200
     3.3 @@ -3,18 +3,15 @@
     3.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3.5      Copyright   1994  University of Cambridge
     3.6  
     3.7 -Lists in Zermelo-Fraenkel Set Theory 
     3.8 -
     3.9 -map is a binding operator -- it applies to meta-level functions, not 
    3.10 -object-level functions.  This simplifies the final form of term_rec_conv,
    3.11 -although complicating its derivation.
    3.12  *)
    3.13  
    3.14 -List = Datatype + ArithSimp +
    3.15 +header{*Lists in Zermelo-Fraenkel Set Theory*}
    3.16 +
    3.17 +theory List = Datatype + ArithSimp:
    3.18  
    3.19  consts
    3.20    list       :: "i=>i"
    3.21 -  
    3.22 +
    3.23  datatype
    3.24    "list(A)" = Nil | Cons ("a:A", "l: list(A)")
    3.25  
    3.26 @@ -37,7 +34,7 @@
    3.27  primrec
    3.28    "length([]) = 0"
    3.29    "length(Cons(a,l)) = succ(length(l))"
    3.30 -  
    3.31 +
    3.32  primrec
    3.33    "hd(Cons(a,l)) = a"
    3.34  
    3.35 @@ -47,22 +44,25 @@
    3.36  
    3.37  
    3.38  consts
    3.39 -  map        :: "[i=>i, i] => i"
    3.40 +  map         :: "[i=>i, i] => i"
    3.41    set_of_list :: "i=>i"
    3.42 -  "@"        :: "[i,i]=>i"                        (infixr 60)
    3.43 -  
    3.44 +  app         :: "[i,i]=>i"                        (infixr "@" 60)
    3.45 +
    3.46 +(*map is a binding operator -- it applies to meta-level functions, not
    3.47 +object-level functions.  This simplifies the final form of term_rec_conv,
    3.48 +although complicating its derivation.*)
    3.49  primrec
    3.50    "map(f,[]) = []"
    3.51    "map(f,Cons(a,l)) = Cons(f(a), map(f,l))"
    3.52 - 
    3.53 +
    3.54  primrec
    3.55    "set_of_list([]) = 0"
    3.56    "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))"
    3.57 -   
    3.58 +
    3.59  primrec
    3.60 -  "[] @ ys = ys"
    3.61 -  "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
    3.62 -  
    3.63 +  app_Nil:  "[] @ ys = ys"
    3.64 +  app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)"
    3.65 +
    3.66  
    3.67  consts
    3.68    rev :: "i=>i"
    3.69 @@ -76,17 +76,17 @@
    3.70  primrec
    3.71    "flat([]) = []"
    3.72    "flat(Cons(l,ls)) = l @ flat(ls)"
    3.73 -   
    3.74 +
    3.75  primrec
    3.76    "list_add([]) = 0"
    3.77    "list_add(Cons(a,l)) = a #+ list_add(l)"
    3.78 -       
    3.79 +
    3.80  consts
    3.81    drop       :: "[i,i]=>i"
    3.82  
    3.83  primrec
    3.84 -  drop_0    "drop(0,l) = l"
    3.85 -  drop_SUCC "drop(succ(i), l) = tl (drop(i,l))"
    3.86 +  drop_0:    "drop(0,l) = l"
    3.87 +  drop_SUCC: "drop(succ(i), l) = tl (drop(i,l))"
    3.88  
    3.89  
    3.90  (*** Thanks to Sidi Ehmety for the following ***)
    3.91 @@ -96,7 +96,7 @@
    3.92    take     :: "[i,i]=>i"
    3.93    "take(n, as) == list_rec(lam n:nat. [],
    3.94  		%a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n"
    3.95 -  
    3.96 +
    3.97  (* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *)
    3.98    nth :: "[i, i]=>i"
    3.99    "nth(n, as) == list_rec(lam n:nat. 0,
   3.100 @@ -108,21 +108,7 @@
   3.101  
   3.102  consts
   3.103    filter :: "[i=>o, i] => i"
   3.104 -  zip :: "[i, i]=>i"
   3.105 -  ziprel :: "[i,i]=>i"
   3.106    upt :: "[i, i] =>i"
   3.107 -  
   3.108 -inductive domains "ziprel(A, B)" <= "list(A)*list(B)*list(A*B)"
   3.109 -intrs   
   3.110 -  ziprel_Nil1  "ys:list(B) ==><Nil, ys, Nil>:ziprel(A, B)"
   3.111 -  ziprel_Nil2  "xs:list(A) ==><xs, Nil, Nil>:ziprel(A, B)"
   3.112 -  ziprel_Cons "[| <xs, ys, zs>:ziprel(A, B); x:A; y:B |]==>
   3.113 -	         <Cons(x, xs), Cons(y, ys), Cons(<x, y>, zs)>:ziprel(A,B)"
   3.114 -  type_intrs  "list.intrs"
   3.115 -  
   3.116 -defs
   3.117 -  zip_def "zip(xs, ys) ==
   3.118 -	      THE zs. <xs, ys, zs>:ziprel(set_of_list(xs),set_of_list(ys))"
   3.119  
   3.120  primrec
   3.121    "filter(P, Nil) = Nil"
   3.122 @@ -134,14 +120,1246 @@
   3.123    "upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)"
   3.124  
   3.125  constdefs
   3.126 -  sublist :: "[i, i] => i"
   3.127 -    "sublist(xs, A)== 
   3.128 -     map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
   3.129 -
   3.130    min :: "[i,i] =>i"
   3.131      "min(x, y) == (if x le y then x else y)"
   3.132 -  
   3.133 +
   3.134    max :: "[i, i] =>i"
   3.135      "max(x, y) == (if x le y then y else x)"
   3.136  
   3.137 +(*** Aspects of the datatype definition ***)
   3.138 +
   3.139 +declare list.intros [simp,TC]
   3.140 +
   3.141 +(*An elimination rule, for type-checking*)
   3.142 +inductive_cases ConsE: "Cons(a,l) : list(A)"
   3.143 +
   3.144 +(*Proving freeness results*)
   3.145 +lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"
   3.146 +by auto
   3.147 +
   3.148 +lemma Nil_Cons_iff: "~ Nil=Cons(a,l)"
   3.149 +by auto
   3.150 +
   3.151 +lemma list_unfold: "list(A) = {0} + (A * list(A))"
   3.152 +by (blast intro!: list.intros [unfolded list.con_defs]
   3.153 +          elim: list.cases [unfolded list.con_defs])
   3.154 +
   3.155 +
   3.156 +(**  Lemmas to justify using "list" in other recursive type definitions **)
   3.157 +
   3.158 +lemma list_mono: "A<=B ==> list(A) <= list(B)"
   3.159 +apply (unfold list.defs )
   3.160 +apply (rule lfp_mono)
   3.161 +apply (simp_all add: list.bnd_mono)
   3.162 +apply (assumption | rule univ_mono basic_monos)+
   3.163 +done
   3.164 +
   3.165 +(*There is a similar proof by list induction.*)
   3.166 +lemma list_univ: "list(univ(A)) <= univ(A)"
   3.167 +apply (unfold list.defs list.con_defs)
   3.168 +apply (rule lfp_lowerbound)
   3.169 +apply (rule_tac [2] A_subset_univ [THEN univ_mono])
   3.170 +apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ)
   3.171 +done
   3.172 +
   3.173 +(*These two theorems justify datatypes involving list(nat), list(A), ...*)
   3.174 +lemmas list_subset_univ = subset_trans [OF list_mono list_univ]
   3.175 +
   3.176 +lemma list_into_univ: "[| l: list(A);  A <= univ(B) |] ==> l: univ(B)"
   3.177 +by (blast intro: list_subset_univ [THEN subsetD])
   3.178 +
   3.179 +lemma list_case_type:
   3.180 +    "[| l: list(A);
   3.181 +        c: C(Nil);
   3.182 +        !!x y. [| x: A;  y: list(A) |] ==> h(x,y): C(Cons(x,y))
   3.183 +     |] ==> list_case(c,h,l) : C(l)"
   3.184 +apply (erule list.induct, auto)
   3.185 +done
   3.186 +
   3.187 +
   3.188 +(*** List functions ***)
   3.189 +
   3.190 +lemma tl_type: "l: list(A) ==> tl(l) : list(A)"
   3.191 +apply (induct_tac "l")
   3.192 +apply (simp_all (no_asm_simp) add: list.intros)
   3.193 +done
   3.194 +
   3.195 +(** drop **)
   3.196 +
   3.197 +lemma drop_Nil [simp]: "i:nat ==> drop(i, Nil) = Nil"
   3.198 +apply (induct_tac "i")
   3.199 +apply (simp_all (no_asm_simp))
   3.200 +done
   3.201 +
   3.202 +lemma drop_succ_Cons [simp]: "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"
   3.203 +apply (rule sym)
   3.204 +apply (induct_tac "i")
   3.205 +apply (simp (no_asm))
   3.206 +apply (simp (no_asm_simp))
   3.207 +done
   3.208 +
   3.209 +lemma drop_type [simp,TC]: "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"
   3.210 +apply (induct_tac "i")
   3.211 +apply (simp_all (no_asm_simp) add: tl_type)
   3.212 +done
   3.213 +
   3.214 +declare drop_SUCC [simp del]
   3.215 +
   3.216 +
   3.217 +(** Type checking -- proved by induction, as usual **)
   3.218 +
   3.219 +lemma list_rec_type [TC]:
   3.220 +    "[| l: list(A);
   3.221 +        c: C(Nil);
   3.222 +        !!x y r. [| x:A;  y: list(A);  r: C(y) |] ==> h(x,y,r): C(Cons(x,y))
   3.223 +     |] ==> list_rec(c,h,l) : C(l)"
   3.224 +by (induct_tac "l", auto)
   3.225 +
   3.226 +(** map **)
   3.227 +
   3.228 +lemma map_type [TC]:
   3.229 +    "[| l: list(A);  !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"
   3.230 +apply (simp add: map_list_def)
   3.231 +apply (typecheck add: list.intros list_rec_type, blast)
   3.232 +done
   3.233 +
   3.234 +lemma map_type2 [TC]: "l: list(A) ==> map(h,l) : list({h(u). u:A})"
   3.235 +apply (erule map_type)
   3.236 +apply (erule RepFunI)
   3.237 +done
   3.238 +
   3.239 +(** length **)
   3.240 +
   3.241 +lemma length_type [TC]: "l: list(A) ==> length(l) : nat"
   3.242 +by (simp add: length_list_def)
   3.243 +
   3.244 +lemma lt_length_in_nat:
   3.245 +   "[|x < length(xs); xs \<in> list(A)|] ==> x \<in> nat"
   3.246 +by (frule lt_nat_in_nat, typecheck) 
   3.247 +
   3.248 +(** app **)
   3.249 +
   3.250 +lemma app_type [TC]: "[| xs: list(A);  ys: list(A) |] ==> xs@ys : list(A)"
   3.251 +by (simp add: app_list_def)
   3.252 +
   3.253 +(** rev **)
   3.254 +
   3.255 +lemma rev_type [TC]: "xs: list(A) ==> rev(xs) : list(A)"
   3.256 +by (simp add: rev_list_def)
   3.257 +
   3.258 +
   3.259 +(** flat **)
   3.260 +
   3.261 +lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) : list(A)"
   3.262 +by (simp add: flat_list_def)
   3.263 +
   3.264 +
   3.265 +(** set_of_list **)
   3.266 +
   3.267 +lemma set_of_list_type [TC]: "l: list(A) ==> set_of_list(l) : Pow(A)"
   3.268 +apply (unfold set_of_list_list_def)
   3.269 +apply (erule list_rec_type, auto)
   3.270 +done
   3.271 +
   3.272 +lemma set_of_list_append:
   3.273 +     "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)"
   3.274 +apply (erule list.induct)
   3.275 +apply (simp_all (no_asm_simp) add: Un_cons)
   3.276 +done
   3.277 +
   3.278 +
   3.279 +(** list_add **)
   3.280 +
   3.281 +lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) : nat"
   3.282 +by (simp add: list_add_list_def)
   3.283 +
   3.284 +
   3.285 +(*** theorems about map ***)
   3.286 +
   3.287 +lemma map_ident [simp]: "l: list(A) ==> map(%u. u, l) = l"
   3.288 +apply (induct_tac "l")
   3.289 +apply (simp_all (no_asm_simp))
   3.290 +done
   3.291 +
   3.292 +lemma map_compose: "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"
   3.293 +apply (induct_tac "l")
   3.294 +apply (simp_all (no_asm_simp))
   3.295 +done
   3.296 +
   3.297 +lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"
   3.298 +apply (induct_tac "xs")
   3.299 +apply (simp_all (no_asm_simp))
   3.300 +done
   3.301 +
   3.302 +lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"
   3.303 +apply (induct_tac "ls")
   3.304 +apply (simp_all (no_asm_simp) add: map_app_distrib)
   3.305 +done
   3.306 +
   3.307 +lemma list_rec_map:
   3.308 +     "l: list(A) ==>
   3.309 +      list_rec(c, d, map(h,l)) =
   3.310 +      list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"
   3.311 +apply (induct_tac "l")
   3.312 +apply (simp_all (no_asm_simp))
   3.313 +done
   3.314 +
   3.315 +(** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **)
   3.316 +
   3.317 +(* c : list(Collect(B,P)) ==> c : list(B) *)
   3.318 +lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard]
   3.319 +
   3.320 +lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"
   3.321 +apply (induct_tac "l")
   3.322 +apply (simp_all (no_asm_simp))
   3.323 +done
   3.324 +
   3.325 +(*** theorems about length ***)
   3.326 +
   3.327 +lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)"
   3.328 +apply (induct_tac "xs")
   3.329 +apply simp_all
   3.330 +done
   3.331 +
   3.332 +lemma length_app [simp]:
   3.333 +     "[| xs: list(A); ys: list(A) |]
   3.334 +      ==> length(xs@ys) = length(xs) #+ length(ys)"
   3.335 +apply (induct_tac "xs")
   3.336 +apply simp_all
   3.337 +done
   3.338 +
   3.339 +lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)"
   3.340 +apply (induct_tac "xs")
   3.341 +apply (simp_all (no_asm_simp) add: length_app)
   3.342 +done
   3.343 +
   3.344 +lemma length_flat:
   3.345 +     "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"
   3.346 +apply (induct_tac "ls")
   3.347 +apply (simp_all (no_asm_simp) add: length_app)
   3.348 +done
   3.349 +
   3.350 +(** Length and drop **)
   3.351 +
   3.352 +(*Lemma for the inductive step of drop_length*)
   3.353 +lemma drop_length_Cons [rule_format]:
   3.354 +     "xs: list(A) ==>
   3.355 +           \<forall>x.  EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"
   3.356 +apply (erule list.induct)
   3.357 +apply simp_all
   3.358 +done
   3.359 +
   3.360 +lemma drop_length [rule_format]:
   3.361 +     "l: list(A) ==> \<forall>i \<in> length(l). (EX z zs. drop(i,l) = Cons(z,zs))"
   3.362 +apply (erule list.induct)
   3.363 +apply simp_all
   3.364 +apply safe
   3.365 +apply (erule drop_length_Cons)
   3.366 +apply (rule natE)
   3.367 +apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption)
   3.368 +apply simp_all
   3.369 +apply (blast intro: succ_in_naturalD length_type)
   3.370 +done
   3.371 +
   3.372 +
   3.373 +(*** theorems about app ***)
   3.374 +
   3.375 +lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs"
   3.376 +apply (erule list.induct)
   3.377 +apply simp_all
   3.378 +done
   3.379 +
   3.380 +lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"
   3.381 +apply (induct_tac "xs")
   3.382 +apply simp_all
   3.383 +done
   3.384 +
   3.385 +lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"
   3.386 +apply (induct_tac "ls")
   3.387 +apply (simp_all (no_asm_simp) add: app_assoc)
   3.388 +done
   3.389 +
   3.390 +(*** theorems about rev ***)
   3.391 +
   3.392 +lemma rev_map_distrib: "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"
   3.393 +apply (induct_tac "l")
   3.394 +apply (simp_all (no_asm_simp) add: map_app_distrib)
   3.395 +done
   3.396 +
   3.397 +(*Simplifier needs the premises as assumptions because rewriting will not
   3.398 +  instantiate the variable ?A in the rules' typing conditions; note that
   3.399 +  rev_type does not instantiate ?A.  Only the premises do.
   3.400 +*)
   3.401 +lemma rev_app_distrib:
   3.402 +     "[| xs: list(A);  ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"
   3.403 +apply (erule list.induct)
   3.404 +apply (simp_all add: app_assoc)
   3.405 +done
   3.406 +
   3.407 +lemma rev_rev_ident [simp]: "l: list(A) ==> rev(rev(l))=l"
   3.408 +apply (induct_tac "l")
   3.409 +apply (simp_all (no_asm_simp) add: rev_app_distrib)
   3.410 +done
   3.411 +
   3.412 +lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"
   3.413 +apply (induct_tac "ls")
   3.414 +apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib)
   3.415 +done
   3.416 +
   3.417 +
   3.418 +(*** theorems about list_add ***)
   3.419 +
   3.420 +lemma list_add_app:
   3.421 +     "[| xs: list(nat);  ys: list(nat) |]
   3.422 +      ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)"
   3.423 +apply (induct_tac "xs")
   3.424 +apply simp_all
   3.425 +done
   3.426 +
   3.427 +lemma list_add_rev: "l: list(nat) ==> list_add(rev(l)) = list_add(l)"
   3.428 +apply (induct_tac "l")
   3.429 +apply (simp_all (no_asm_simp) add: list_add_app)
   3.430 +done
   3.431 +
   3.432 +lemma list_add_flat:
   3.433 +     "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"
   3.434 +apply (induct_tac "ls")
   3.435 +apply (simp_all (no_asm_simp) add: list_add_app)
   3.436 +done
   3.437 +
   3.438 +(** New induction rule **)
   3.439 +
   3.440 +
   3.441 +lemma list_append_induct:
   3.442 +    "[| l: list(A);
   3.443 +        P(Nil);
   3.444 +        !!x y. [| x: A;  y: list(A);  P(y) |] ==> P(y @ [x])
   3.445 +     |] ==> P(l)"
   3.446 +apply (subgoal_tac "P(rev(rev(l)))", simp)
   3.447 +apply (erule rev_type [THEN list.induct], simp_all)
   3.448 +done
   3.449 +
   3.450 +
   3.451 +(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***)
   3.452 +
   3.453 +(** min FIXME: replace by Int! **)
   3.454 +(* Min theorems are also true for i, j ordinals *)
   3.455 +lemma min_sym: "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)"
   3.456 +apply (unfold min_def)
   3.457 +apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym)
   3.458 +done
   3.459 +
   3.460 +lemma min_type [simp,TC]: "[| i:nat; j:nat |] ==> min(i,j):nat"
   3.461 +by (unfold min_def, auto)
   3.462 +
   3.463 +lemma min_0 [simp]: "i:nat ==> min(0,i) = 0"
   3.464 +apply (unfold min_def)
   3.465 +apply (auto dest: not_lt_imp_le)
   3.466 +done
   3.467 +
   3.468 +lemma min_02 [simp]: "i:nat ==> min(i, 0) = 0"
   3.469 +apply (unfold min_def)
   3.470 +apply (auto dest: not_lt_imp_le)
   3.471 +done
   3.472 +
   3.473 +lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i<min(j,k) <-> i<j & i<k"
   3.474 +apply (unfold min_def)
   3.475 +apply (auto dest!: not_lt_imp_le intro: lt_trans2 lt_trans)
   3.476 +done
   3.477 +
   3.478 +lemma min_succ_succ [simp]:
   3.479 +     "[| i:nat; j:nat |] ==>  min(succ(i), succ(j))= succ(min(i, j))"
   3.480 +apply (unfold min_def, auto)
   3.481 +done
   3.482 +
   3.483 +(*** more theorems about lists ***)
   3.484 +
   3.485 +(** filter **)
   3.486 +
   3.487 +lemma filter_append [simp]:
   3.488 +     "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)"
   3.489 +by (induct_tac "xs", auto)
   3.490 +
   3.491 +lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)"
   3.492 +by (induct_tac "xs", auto)
   3.493 +
   3.494 +lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) le length(xs)"
   3.495 +apply (induct_tac "xs", auto)
   3.496 +apply (rule_tac j = "length (l) " in le_trans)
   3.497 +apply (auto simp add: le_iff)
   3.498 +done
   3.499 +
   3.500 +lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)"
   3.501 +by (induct_tac "xs", auto)
   3.502 +
   3.503 +lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil"
   3.504 +by (induct_tac "xs", auto)
   3.505 +
   3.506 +lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs"
   3.507 +by (induct_tac "xs", auto)
   3.508 +
   3.509 +(** length **)
   3.510 +
   3.511 +lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil"
   3.512 +by (erule list.induct, auto)
   3.513 +
   3.514 +lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil"
   3.515 +by (erule list.induct, auto)
   3.516 +
   3.517 +lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"
   3.518 +by (erule list.induct, auto)
   3.519 +
   3.520 +lemma length_greater_0_iff: "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil"
   3.521 +by (erule list.induct, auto)
   3.522 +
   3.523 +lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)"
   3.524 +by (erule list.induct, auto)
   3.525 +
   3.526 +(** more theorems about append **)
   3.527 +
   3.528 +lemma append_is_Nil_iff [simp]:
   3.529 +     "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)"
   3.530 +by (erule list.induct, auto)
   3.531 +
   3.532 +lemma append_is_Nil_iff2 [simp]:
   3.533 +     "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)"
   3.534 +by (erule list.induct, auto)
   3.535 +
   3.536 +lemma append_left_is_self_iff [simp]:
   3.537 +     "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)"
   3.538 +by (erule list.induct, auto)
   3.539 +
   3.540 +lemma append_left_is_self_iff2 [simp]:
   3.541 +     "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)"
   3.542 +by (erule list.induct, auto)
   3.543 +
   3.544 +(*TOO SLOW as a default simprule!*)
   3.545 +lemma append_left_is_Nil_iff [rule_format]:
   3.546 +     "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
   3.547 +   length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))"
   3.548 +apply (erule list.induct)
   3.549 +apply (auto simp add: length_app)
   3.550 +done
   3.551 +
   3.552 +(*TOO SLOW as a default simprule!*)
   3.553 +lemma append_left_is_Nil_iff2 [rule_format]:
   3.554 +     "[| xs:list(A); ys:list(A); zs:list(A) |] ==>
   3.555 +   length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))"
   3.556 +apply (erule list.induct)
   3.557 +apply (auto simp add: length_app)
   3.558 +done
   3.559 +
   3.560 +lemma append_eq_append_iff [rule_format,simp]:
   3.561 +     "xs:list(A) ==> \<forall>ys \<in> list(A).
   3.562 +      length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)"
   3.563 +apply (erule list.induct)
   3.564 +apply (simp (no_asm_simp))
   3.565 +apply clarify
   3.566 +apply (erule_tac a = "ys" in list.cases, auto)
   3.567 +done
   3.568 +
   3.569 +lemma append_eq_append [rule_format]:
   3.570 +  "xs:list(A) ==>
   3.571 +   \<forall>ys \<in> list(A). \<forall>us \<in> list(A). \<forall>vs \<in> list(A).
   3.572 +   length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)"
   3.573 +apply (induct_tac "xs")
   3.574 +apply (force simp add: length_app, clarify)
   3.575 +apply (erule_tac a = "ys" in list.cases, simp)
   3.576 +apply (subgoal_tac "Cons (a, l) @ us =vs")
   3.577 + apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all)
   3.578 +apply blast
   3.579 +done
   3.580 +
   3.581 +lemma append_eq_append_iff2 [simp]:
   3.582 + "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |]
   3.583 +  ==>  xs@us = ys@vs <-> (xs=ys & us=vs)"
   3.584 +apply (rule iffI)
   3.585 +apply (rule append_eq_append, auto)
   3.586 +done
   3.587 +
   3.588 +lemma append_self_iff [simp]:
   3.589 +     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"
   3.590 +apply (simp (no_asm_simp))
   3.591 +done
   3.592 +
   3.593 +lemma append_self_iff2 [simp]:
   3.594 +     "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"
   3.595 +apply (simp (no_asm_simp))
   3.596 +done
   3.597 +
   3.598 +(* Can also be proved from append_eq_append_iff2,
   3.599 +but the proof requires two more hypotheses: x:A and y:A *)
   3.600 +lemma append1_eq_iff [rule_format,simp]:
   3.601 +     "xs:list(A) ==> \<forall>ys \<in> list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"
   3.602 +apply (erule list.induct)  
   3.603 + apply clarify 
   3.604 + apply (erule list.cases)
   3.605 + apply simp_all
   3.606 +txt{*Inductive step*}  
   3.607 +apply clarify 
   3.608 +apply (erule_tac a = xa in list.cases, simp_all)  
   3.609 +done
   3.610 +
   3.611 +
   3.612 +lemma append_right_is_self_iff [simp]:
   3.613 +     "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"
   3.614 +apply (simp (no_asm_simp) add: append_left_is_Nil_iff)
   3.615 +done
   3.616 +
   3.617 +lemma append_right_is_self_iff2 [simp]:
   3.618 +     "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"
   3.619 +apply (rule iffI)
   3.620 +apply (drule sym, auto) 
   3.621 +done
   3.622 +
   3.623 +lemma hd_append [rule_format,simp]:
   3.624 +     "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)"
   3.625 +by (induct_tac "xs", auto)
   3.626 +
   3.627 +lemma tl_append [rule_format,simp]:
   3.628 +     "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys"
   3.629 +by (induct_tac "xs", auto)
   3.630 +
   3.631 +(** rev **)
   3.632 +lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)"
   3.633 +by (erule list.induct, auto)
   3.634 +
   3.635 +lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)"
   3.636 +by (erule list.induct, auto)
   3.637 +
   3.638 +lemma rev_is_rev_iff [rule_format,simp]:
   3.639 +     "xs:list(A) ==> \<forall>ys \<in> list(A). rev(xs)=rev(ys) <-> xs=ys"
   3.640 +apply (erule list.induct, force)
   3.641 +apply clarify
   3.642 +apply (erule_tac a = "ys" in list.cases, auto)
   3.643 +done
   3.644 +
   3.645 +lemma rev_list_elim [rule_format]:
   3.646 +     "xs:list(A) ==>
   3.647 +      (xs=Nil --> P) --> (\<forall>ys \<in> list(A). \<forall>y \<in> A. xs =ys@[y] -->P)-->P"
   3.648 +apply (erule list_append_induct, auto)
   3.649 +done
   3.650 +
   3.651 +
   3.652 +(** more theorems about drop **)
   3.653 +
   3.654 +lemma length_drop [rule_format,simp]:
   3.655 +     "n:nat ==> \<forall>xs \<in> list(A). length(drop(n, xs)) = length(xs) #- n"
   3.656 +apply (erule nat_induct)
   3.657 +apply (auto elim: list.cases)
   3.658 +done
   3.659 +
   3.660 +lemma drop_all [rule_format,simp]:
   3.661 +     "n:nat ==> \<forall>xs \<in> list(A). length(xs) le n --> drop(n, xs)=Nil"
   3.662 +apply (erule nat_induct)
   3.663 +apply (auto elim: list.cases)
   3.664 +done
   3.665 +
   3.666 +lemma drop_append [rule_format]:
   3.667 +     "n:nat ==> 
   3.668 +      \<forall>xs \<in> list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)"
   3.669 +apply (induct_tac "n")
   3.670 +apply (auto elim: list.cases)
   3.671 +done
   3.672 +
   3.673 +lemma drop_drop:
   3.674 +    "m:nat ==> \<forall>xs \<in> list(A). \<forall>n \<in> nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"
   3.675 +apply (induct_tac "m")
   3.676 +apply (auto elim: list.cases)
   3.677 +done
   3.678 +
   3.679 +(** take **)
   3.680 +
   3.681 +lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) =  Nil"
   3.682 +apply (unfold take_def)
   3.683 +apply (erule list.induct, auto)
   3.684 +done
   3.685 +
   3.686 +lemma take_succ_Cons [simp]:
   3.687 +    "n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))"
   3.688 +by (simp add: take_def)
   3.689 +
   3.690 +(* Needed for proving take_all *)
   3.691 +lemma take_Nil [simp]: "n:nat ==> take(n, Nil) = Nil"
   3.692 +by (unfold take_def, auto)
   3.693 +
   3.694 +lemma take_all [rule_format,simp]:
   3.695 +     "n:nat ==> \<forall>xs \<in> list(A). length(xs) le n  --> take(n, xs) = xs"
   3.696 +apply (erule nat_induct)
   3.697 +apply (auto elim: list.cases) 
   3.698 +done
   3.699 +
   3.700 +lemma take_type [rule_format,simp,TC]:
   3.701 +     "xs:list(A) ==> \<forall>n \<in> nat. take(n, xs):list(A)"
   3.702 +apply (erule list.induct, simp) 
   3.703 +apply clarify 
   3.704 +apply (erule natE, auto)
   3.705 +done
   3.706 +
   3.707 +lemma take_append [rule_format,simp]:
   3.708 + "xs:list(A) ==>
   3.709 +  \<forall>ys \<in> list(A). \<forall>n \<in> nat. take(n, xs @ ys) =
   3.710 +                            take(n, xs) @ take(n #- length(xs), ys)"
   3.711 +apply (erule list.induct, simp) 
   3.712 +apply clarify 
   3.713 +apply (erule natE, auto)
   3.714 +done
   3.715 +
   3.716 +lemma take_take [rule_format]:
   3.717 +   "m : nat ==>
   3.718 +    \<forall>xs \<in> list(A). \<forall>n \<in> nat. take(n, take(m,xs))= take(min(n, m), xs)"
   3.719 +apply (induct_tac "m", auto)
   3.720 +apply (erule_tac a = "xs" in list.cases)
   3.721 +apply (auto simp add: take_Nil)
   3.722 +apply (rotate_tac 1)
   3.723 +apply (erule natE)
   3.724 +apply (auto intro: take_0 take_type)
   3.725 +done
   3.726 +
   3.727 +(** nth **)
   3.728 +
   3.729 +lemma nth_0 [simp]: "nth(0, Cons(a, l))= a"
   3.730 +by (unfold nth_def, auto)
   3.731 +
   3.732 +lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)"
   3.733 +apply (unfold nth_def)
   3.734 +apply (simp (no_asm_simp))
   3.735 +done
   3.736 +
   3.737 +lemma nth_type [rule_format,simp,TC]:
   3.738 +     "xs:list(A) ==> \<forall>n \<in> nat. n < length(xs) --> nth(n, xs):A"
   3.739 +apply (erule list.induct, simp) 
   3.740 +apply clarify 
   3.741 +apply (erule natE, auto)
   3.742 +done
   3.743 +
   3.744 +lemma nth_append [rule_format]:
   3.745 +  "xs:list(A) ==> 
   3.746 +   \<forall>n \<in> nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs)
   3.747 +                                else nth(n #- length(xs),ys))"
   3.748 +apply (induct_tac "xs", simp) 
   3.749 +apply clarify 
   3.750 +apply (erule natE, auto)
   3.751 +done
   3.752 +
   3.753 +lemma set_of_list_conv_nth:
   3.754 +    "xs:list(A)
   3.755 +      ==> set_of_list(xs) = {x:A. EX i:nat. i<length(xs) & x=nth(i, xs)}"
   3.756 +apply (induct_tac "xs", simp_all)
   3.757 +apply (rule equalityI, auto)
   3.758 +apply (rule_tac x = "0" in bexI, auto)
   3.759 +apply (erule natE, auto)
   3.760 +done
   3.761 +
   3.762 +(* Other theorems about lists *)
   3.763 +
   3.764 +lemma nth_take_lemma [rule_format]:
   3.765 + "k:nat ==>
   3.766 +  \<forall>xs \<in> list(A). (\<forall>ys \<in> list(A). k le length(xs) --> k le length(ys) -->
   3.767 +      (\<forall>i \<in> nat. i<k --> nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))"
   3.768 +apply (induct_tac "k")
   3.769 +apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib)
   3.770 +apply clarify
   3.771 +(*Both lists are non-empty*)
   3.772 +apply (erule_tac a="xa" in list.cases, simp) 
   3.773 +apply (erule_tac a="xb" in list.cases, clarify) 
   3.774 +apply (simp (no_asm_use) )
   3.775 +apply clarify
   3.776 +apply (simp (no_asm_simp))
   3.777 +apply (rule conjI, force)
   3.778 +apply (rename_tac y ys z zs) 
   3.779 +apply (drule_tac x = "zs" and x1 = "ys" in bspec [THEN bspec], auto)   
   3.780 +done
   3.781 +
   3.782 +lemma nth_equalityI [rule_format]:
   3.783 +     "[| xs:list(A); ys:list(A); length(xs) = length(ys);
   3.784 +         \<forall>i \<in> nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |]
   3.785 +      ==> xs = ys"
   3.786 +apply (subgoal_tac "length (xs) le length (ys) ")
   3.787 +apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma) 
   3.788 +apply (simp_all add: take_all)
   3.789 +done
   3.790 +
   3.791 +(*The famous take-lemma*)
   3.792 +
   3.793 +lemma take_equalityI [rule_format]:
   3.794 +    "[| xs:list(A); ys:list(A); (\<forall>i \<in> nat. take(i, xs) = take(i,ys)) |] 
   3.795 +     ==> xs = ys"
   3.796 +apply (case_tac "length (xs) le length (ys) ")
   3.797 +apply (drule_tac x = "length (ys) " in bspec)
   3.798 +apply (drule_tac [3] not_lt_imp_le)
   3.799 +apply (subgoal_tac [5] "length (ys) le length (xs) ")
   3.800 +apply (rule_tac [6] j = "succ (length (ys))" in le_trans)
   3.801 +apply (rule_tac [6] leI)
   3.802 +apply (drule_tac [5] x = "length (xs) " in bspec)
   3.803 +apply (simp_all add: take_all)
   3.804 +done
   3.805 +
   3.806 +lemma nth_drop [rule_format]:
   3.807 +      "n:nat ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A). n #+ i le length(xs)
   3.808 +                      --> nth(i, drop(n, xs)) = nth(n #+ i, xs)"
   3.809 +apply (induct_tac "n", simp_all) 
   3.810 +apply clarify
   3.811 +apply (erule list.cases) 
   3.812 +apply (auto elim!: ConsE)
   3.813 +done
   3.814 +
   3.815 +subsection{*The function zip*}
   3.816 +
   3.817 +text{*Crafty definition to eliminate a type argument*}
   3.818 +
   3.819 +consts
   3.820 +  zip_aux        :: "[i,i]=>i"
   3.821 +
   3.822 +primrec (*explicit lambda is required because both arguments of "un" vary*)
   3.823 +  "zip_aux(B,[]) =
   3.824 +     (\<lambda>ys \<in> list(B). list_case([], %y l. [], ys))"
   3.825 +
   3.826 +  "zip_aux(B,Cons(x,l)) =
   3.827 +     (\<lambda>ys \<in> list(B).
   3.828 +        list_case(Nil, %y zs. Cons(<x,y>, zip_aux(B,l)`zs), ys))"
   3.829 +
   3.830 +constdefs
   3.831 +  zip :: "[i, i]=>i"
   3.832 +   "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys"
   3.833 +
   3.834 +
   3.835 +(* zip equations *)
   3.836 +
   3.837 +lemma list_on_set_of_list: "xs \<in> list(A) ==> xs \<in> list(set_of_list(xs))"
   3.838 +apply (induct_tac xs, simp_all) 
   3.839 +apply (blast intro: list_mono [THEN subsetD]) 
   3.840 +done
   3.841 +
   3.842 +lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil"
   3.843 +apply (simp add: zip_def list_on_set_of_list [of _ A])
   3.844 +apply (erule list.cases, simp_all) 
   3.845 +done
   3.846 +
   3.847 +lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil"
   3.848 +apply (simp add: zip_def list_on_set_of_list [of _ A])
   3.849 +apply (erule list.cases, simp_all) 
   3.850 +done
   3.851 +
   3.852 +lemma zip_aux_unique [rule_format]:
   3.853 +     "[|B<=C;  xs \<in> list(A)|] 
   3.854 +      ==> \<forall>ys \<in> list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys"
   3.855 +apply (induct_tac xs) 
   3.856 + apply simp_all 
   3.857 + apply (blast intro: list_mono [THEN subsetD], clarify) 
   3.858 +apply (erule_tac a=x in list.cases , auto) 
   3.859 +apply (blast intro: list_mono [THEN subsetD]) 
   3.860 +done
   3.861 +
   3.862 +lemma zip_Cons_Cons [simp]:
   3.863 +     "[| xs:list(A); ys:list(B); x:A; y:B |] ==>
   3.864 +      zip(Cons(x,xs), Cons(y, ys)) = Cons(<x,y>, zip(xs, ys))"
   3.865 +apply (simp add: zip_def, auto) 
   3.866 +apply (rule zip_aux_unique, auto) 
   3.867 +apply (simp add: list_on_set_of_list [of _ B])
   3.868 +apply (blast intro: list_on_set_of_list list_mono [THEN subsetD]) 
   3.869 +done
   3.870 +
   3.871 +lemma zip_type [rule_format,simp,TC]:
   3.872 +     "xs:list(A) ==> \<forall>ys \<in> list(B). zip(xs, ys):list(A*B)"
   3.873 +apply (induct_tac "xs")
   3.874 +apply (simp (no_asm))
   3.875 +apply clarify
   3.876 +apply (erule_tac a = "ys" in list.cases, auto)
   3.877 +done
   3.878 +
   3.879 +(* zip length *)
   3.880 +lemma length_zip [rule_format,simp]:
   3.881 +     "xs:list(A) ==> \<forall>ys \<in> list(B). length(zip(xs,ys)) =
   3.882 +                                     min(length(xs), length(ys))"
   3.883 +apply (unfold min_def)
   3.884 +apply (induct_tac "xs", simp_all) 
   3.885 +apply clarify 
   3.886 +apply (erule_tac a = "x" in list.cases, auto)
   3.887 +done
   3.888 +
   3.889 +lemma zip_append1 [rule_format]:
   3.890 + "[| ys:list(A); zs:list(B) |] ==>
   3.891 +  \<forall>xs \<in> list(A). zip(xs @ ys, zs) = 
   3.892 +                 zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"
   3.893 +apply (induct_tac "zs", force) 
   3.894 +apply clarify 
   3.895 +apply (erule_tac a = "xs" in list.cases, simp_all) 
   3.896 +done
   3.897 +
   3.898 +lemma zip_append2 [rule_format]:
   3.899 + "[| xs:list(A); zs:list(B) |] ==> \<forall>ys \<in> list(B). zip(xs, ys@zs) =
   3.900 +       zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"
   3.901 +apply (induct_tac "xs", force) 
   3.902 +apply clarify 
   3.903 +apply (erule_tac a = "ys" in list.cases, auto)
   3.904 +done
   3.905 +
   3.906 +lemma zip_append [simp]:
   3.907 + "[| length(xs) = length(us); length(ys) = length(vs);
   3.908 +     xs:list(A); us:list(B); ys:list(A); vs:list(B) |] 
   3.909 +  ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)"
   3.910 +by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0)
   3.911 +
   3.912 +
   3.913 +lemma zip_rev [rule_format,simp]:
   3.914 + "ys:list(B) ==> \<forall>xs \<in> list(A).
   3.915 +    length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"
   3.916 +apply (induct_tac "ys", force) 
   3.917 +apply clarify 
   3.918 +apply (erule_tac a = "xs" in list.cases)
   3.919 +apply (auto simp add: length_rev)
   3.920 +done
   3.921 +
   3.922 +lemma nth_zip [rule_format,simp]:
   3.923 +   "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xs \<in> list(A).
   3.924 +                    i < length(xs) --> i < length(ys) -->
   3.925 +                    nth(i,zip(xs, ys)) = <nth(i,xs),nth(i, ys)>"
   3.926 +apply (induct_tac "ys", force) 
   3.927 +apply clarify 
   3.928 +apply (erule_tac a = "xs" in list.cases, simp) 
   3.929 +apply (auto elim: natE)
   3.930 +done
   3.931 +
   3.932 +lemma set_of_list_zip [rule_format]:
   3.933 +     "[| xs:list(A); ys:list(B); i:nat |]
   3.934 +      ==> set_of_list(zip(xs, ys)) =
   3.935 +          {<x, y>:A*B. EX i:nat. i < min(length(xs), length(ys))
   3.936 +          & x=nth(i, xs) & y=nth(i, ys)}"
   3.937 +by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth)
   3.938 +
   3.939 +(** list_update **)
   3.940 +
   3.941 +lemma list_update_Nil [simp]: "i:nat ==>list_update(Nil, i, v) = Nil"
   3.942 +by (unfold list_update_def, auto)
   3.943 +
   3.944 +lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)"
   3.945 +by (unfold list_update_def, auto)
   3.946 +
   3.947 +lemma list_update_Cons_succ [simp]:
   3.948 +  "n:nat ==>
   3.949 +    list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))"
   3.950 +apply (unfold list_update_def, auto)
   3.951 +done
   3.952 +
   3.953 +lemma list_update_type [rule_format,simp,TC]:
   3.954 +     "[| xs:list(A); v:A |] ==> \<forall>n \<in> nat. list_update(xs, n, v):list(A)"
   3.955 +apply (induct_tac "xs")
   3.956 +apply (simp (no_asm))
   3.957 +apply clarify
   3.958 +apply (erule natE, auto)
   3.959 +done
   3.960 +
   3.961 +lemma length_list_update [rule_format,simp]:
   3.962 +     "xs:list(A) ==> \<forall>i \<in> nat. length(list_update(xs, i, v))=length(xs)"
   3.963 +apply (induct_tac "xs")
   3.964 +apply (simp (no_asm))
   3.965 +apply clarify
   3.966 +apply (erule natE, auto)
   3.967 +done
   3.968 +
   3.969 +lemma nth_list_update [rule_format]:
   3.970 +     "[| xs:list(A) |] ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i < length(xs)  -->
   3.971 +         nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"
   3.972 +apply (induct_tac "xs")
   3.973 + apply simp_all
   3.974 +apply clarify
   3.975 +apply (rename_tac i j) 
   3.976 +apply (erule_tac n=i in natE) 
   3.977 +apply (erule_tac [2] n=j in natE)
   3.978 +apply (erule_tac n=j in natE, simp_all, force) 
   3.979 +done
   3.980 +
   3.981 +lemma nth_list_update_eq [simp]:
   3.982 +     "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x"
   3.983 +by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update)
   3.984 +
   3.985 +
   3.986 +lemma nth_list_update_neq [rule_format,simp]:
   3.987 +     "xs:list(A) ==> \<forall>i \<in> nat. \<forall>j \<in> nat. i ~= j
   3.988 +  --> nth(j, list_update(xs, i,x)) = nth(j, xs)"
   3.989 +apply (induct_tac "xs")
   3.990 + apply (simp (no_asm))
   3.991 +apply clarify
   3.992 +apply (erule natE)
   3.993 +apply (erule_tac [2] natE, simp_all) 
   3.994 +apply (erule natE, simp_all)
   3.995 +done
   3.996 +
   3.997 +lemma list_update_overwrite [rule_format,simp]:
   3.998 +     "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs)
   3.999 +   --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"
  3.1000 +apply (induct_tac "xs")
  3.1001 + apply (simp (no_asm))
  3.1002 +apply clarify
  3.1003 +apply (erule natE, auto)
  3.1004 +done
  3.1005 +
  3.1006 +lemma list_update_same_conv [rule_format]:
  3.1007 +     "xs:list(A) ==> \<forall>i \<in> nat. i < length(xs) -->
  3.1008 +  (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"
  3.1009 +apply (induct_tac "xs")
  3.1010 + apply (simp (no_asm))
  3.1011 +apply clarify
  3.1012 +apply (erule natE, auto)
  3.1013 +done
  3.1014 +
  3.1015 +lemma update_zip [rule_format]:
  3.1016 +     "ys:list(B) ==> \<forall>i \<in> nat. \<forall>xy \<in> A*B. \<forall>xs \<in> list(A).
  3.1017 +  length(xs) = length(ys) -->
  3.1018 +      list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)),
  3.1019 +                                          list_update(ys, i, snd(xy)))"
  3.1020 +apply (induct_tac "ys")
  3.1021 + apply auto
  3.1022 +apply (erule_tac a = "xc" in list.cases)
  3.1023 +apply (auto elim: natE)
  3.1024 +done
  3.1025 +
  3.1026 +lemma set_update_subset_cons [rule_format]:
  3.1027 +     "xs:list(A) ==> \<forall>i \<in> nat. set_of_list(list_update(xs, i, x))
  3.1028 +   <= cons(x, set_of_list(xs))"
  3.1029 +apply (induct_tac "xs")
  3.1030 + apply simp
  3.1031 +apply (rule ballI)
  3.1032 +apply (erule natE, simp_all)
  3.1033 +apply auto
  3.1034 +done
  3.1035 +
  3.1036 +lemma set_of_list_update_subsetI:
  3.1037 +     "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|]
  3.1038 +   ==> set_of_list(list_update(xs, i,x)) <= A"
  3.1039 +apply (rule subset_trans)
  3.1040 +apply (rule set_update_subset_cons, auto)
  3.1041 +done
  3.1042 +
  3.1043 +(** upt **)
  3.1044 +
  3.1045 +lemma upt_rec:
  3.1046 +     "j:nat ==> upt(i,j) = (if i<j then Cons(i, upt(succ(i), j)) else Nil)"
  3.1047 +apply (induct_tac "j", auto)
  3.1048 +apply (drule not_lt_imp_le)
  3.1049 +apply (auto simp: lt_Ord intro: le_anti_sym)
  3.1050 +done
  3.1051 +
  3.1052 +lemma upt_conv_Nil [simp]: "[| j le i; j:nat |] ==> upt(i,j) = Nil"
  3.1053 +apply (subst upt_rec, auto)
  3.1054 +apply (auto simp add: le_iff)
  3.1055 +apply (drule lt_asym [THEN notE], auto)
  3.1056 +done
  3.1057 +
  3.1058 +(*Only needed if upt_Suc is deleted from the simpset*)
  3.1059 +lemma upt_succ_append:
  3.1060 +     "[| i le j; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]"
  3.1061 +by simp
  3.1062 +
  3.1063 +lemma upt_conv_Cons:
  3.1064 +     "[| i<j; j:nat |]  ==> upt(i,j) = Cons(i,upt(succ(i),j))"
  3.1065 +apply (rule trans)
  3.1066 +apply (rule upt_rec, auto)
  3.1067 +done
  3.1068 +
  3.1069 +lemma upt_type [simp,TC]: "j:nat ==> upt(i,j):list(nat)"
  3.1070 +by (induct_tac "j", auto)
  3.1071 +
  3.1072 +(*LOOPS as a simprule, since j<=j*)
  3.1073 +lemma upt_add_eq_append:
  3.1074 +     "[| i le j; j:nat; k:nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"
  3.1075 +apply (induct_tac "k")
  3.1076 +apply (auto simp add: app_assoc app_type)
  3.1077 +apply (rule_tac j = "j" in le_trans, auto)
  3.1078 +done
  3.1079 +
  3.1080 +lemma length_upt [simp]: "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i"
  3.1081 +apply (induct_tac "j")
  3.1082 +apply (rule_tac [2] sym)
  3.1083 +apply (auto dest!: not_lt_imp_le simp add: length_app diff_succ diff_is_0_iff)
  3.1084 +done
  3.1085 +
  3.1086 +lemma nth_upt [rule_format,simp]:
  3.1087 +     "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k"
  3.1088 +apply (induct_tac "j")
  3.1089 +apply (simp (no_asm_simp))
  3.1090 +apply (simp add: nth_append le_iff split add: nat_diff_split, safe)
  3.1091 +apply (auto dest!: not_lt_imp_le simp add: nth_append diff_self_eq_0 
  3.1092 +                   less_diff_conv add_commute)
  3.1093 +apply (drule_tac j = "x" in lt_trans2, auto)
  3.1094 +done
  3.1095 +
  3.1096 +lemma take_upt [rule_format,simp]:
  3.1097 +     "[| m:nat; n:nat |] ==>
  3.1098 +      \<forall>i \<in> nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"
  3.1099 +apply (induct_tac "m")
  3.1100 +apply (simp (no_asm_simp) add: take_0)
  3.1101 +apply clarify
  3.1102 +apply (subst upt_rec, simp) 
  3.1103 +apply (rule sym)
  3.1104 +apply (subst upt_rec, simp) 
  3.1105 +apply (simp_all del: upt.simps)
  3.1106 +apply (rule_tac j = "succ (i #+ x) " in lt_trans2)
  3.1107 +apply auto
  3.1108 +done
  3.1109 +
  3.1110 +lemma map_succ_upt:
  3.1111 +     "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"
  3.1112 +apply (induct_tac "n")
  3.1113 +apply (auto simp add: map_app_distrib)
  3.1114 +done
  3.1115 +
  3.1116 +lemma nth_map [rule_format,simp]:
  3.1117 +     "xs:list(A) ==>
  3.1118 +      \<forall>n \<in> nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))"
  3.1119 +apply (induct_tac "xs", simp)
  3.1120 +apply (rule ballI)
  3.1121 +apply (induct_tac "n", auto)
  3.1122 +done
  3.1123 +
  3.1124 +lemma nth_map_upt [rule_format]:
  3.1125 +     "[| m:nat; n:nat |] ==>
  3.1126 +      \<forall>i \<in> nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"
  3.1127 +apply (rule_tac n = "m" and m = "n" in diff_induct, typecheck)
  3.1128 +apply simp 
  3.1129 +apply simp 
  3.1130 +apply (subst map_succ_upt [symmetric], simp_all)
  3.1131 +apply clarify 
  3.1132 +apply (subgoal_tac "xa < length (upt (0, x))")
  3.1133 + prefer 2 
  3.1134 + apply (simp add: less_diff_conv) 
  3.1135 + apply (rule_tac j = "succ (xa #+ y) " in lt_trans2)
  3.1136 +  apply simp 
  3.1137 + apply simp 
  3.1138 +apply (subgoal_tac "xa < length (upt (y, x))")
  3.1139 + apply (simp_all add: add_commute less_diff_conv)
  3.1140 +done
  3.1141 +
  3.1142 +(** sublist (a generalization of nth to sets) **)
  3.1143 +
  3.1144 +constdefs
  3.1145 +  sublist :: "[i, i] => i"
  3.1146 +    "sublist(xs, A)==
  3.1147 +     map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))"
  3.1148 +
  3.1149 +lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil"
  3.1150 +by (unfold sublist_def, auto)
  3.1151 +
  3.1152 +lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil"
  3.1153 +by (unfold sublist_def, auto)
  3.1154 +
  3.1155 +lemma sublist_shift_lemma:
  3.1156 + "[| xs:list(B); i:nat |] ==>
  3.1157 +  map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) =
  3.1158 +  map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))"
  3.1159 +apply (erule list_append_induct)
  3.1160 +apply (simp (no_asm_simp))
  3.1161 +apply (auto simp add: add_commute length_app filter_append map_app_distrib)
  3.1162 +done
  3.1163 +
  3.1164 +lemma sublist_type [simp,TC]:
  3.1165 +     "xs:list(B) ==> sublist(xs, A):list(B)"
  3.1166 +apply (unfold sublist_def)
  3.1167 +apply (induct_tac "xs")
  3.1168 +apply (auto simp add: filter_append map_app_distrib)
  3.1169 +done
  3.1170 +
  3.1171 +lemma upt_add_eq_append2:
  3.1172 +     "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)"
  3.1173 +by (simp add: upt_add_eq_append [of 0] nat_0_le)
  3.1174 +
  3.1175 +lemma sublist_append:
  3.1176 + "[| xs:list(B); ys:list(B)  |] ==>
  3.1177 +  sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})"
  3.1178 +apply (unfold sublist_def)
  3.1179 +apply (erule_tac l = "ys" in list_append_induct)
  3.1180 +apply (simp)
  3.1181 +apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric])
  3.1182 +apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc)
  3.1183 +apply (simp_all add: add_commute)
  3.1184 +done
  3.1185 +
  3.1186 +
  3.1187 +lemma sublist_Cons:
  3.1188 +     "[| xs:list(B); x:B |] ==>
  3.1189 +      sublist(Cons(x, xs), A) = 
  3.1190 +      (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})"
  3.1191 +apply (erule_tac l = "xs" in list_append_induct)
  3.1192 +apply (simp (no_asm_simp) add: sublist_def)  
  3.1193 +apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp) 
  3.1194 +done
  3.1195 +
  3.1196 +lemma sublist_singleton [simp]:
  3.1197 +     "sublist([x], A) = (if 0 : A then [x] else [])"
  3.1198 +by (simp (no_asm) add: sublist_Cons)
  3.1199 +
  3.1200 +
  3.1201 +lemma sublist_upt_eq_take [simp]:
  3.1202 +    "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)"
  3.1203 +apply (unfold less_than_def)
  3.1204 +apply (erule_tac l = "xs" in list_append_induct, simp) 
  3.1205 +apply (simp split add: nat_diff_split add: sublist_append, auto)
  3.1206 +apply (subgoal_tac "n #- length (y) = 0")
  3.1207 +apply (simp (no_asm_simp))
  3.1208 +apply (auto dest!: not_lt_imp_le simp add: diff_is_0_iff)
  3.1209 +done
  3.1210 +
  3.1211 +ML
  3.1212 +{*
  3.1213 +val ConsE = thm "ConsE";
  3.1214 +val Cons_iff = thm "Cons_iff";
  3.1215 +val Nil_Cons_iff = thm "Nil_Cons_iff";
  3.1216 +val list_unfold = thm "list_unfold";
  3.1217 +val list_mono = thm "list_mono";
  3.1218 +val list_univ = thm "list_univ";
  3.1219 +val list_subset_univ = thm "list_subset_univ";
  3.1220 +val list_into_univ = thm "list_into_univ";
  3.1221 +val list_case_type = thm "list_case_type";
  3.1222 +val tl_type = thm "tl_type";
  3.1223 +val drop_Nil = thm "drop_Nil";
  3.1224 +val drop_succ_Cons = thm "drop_succ_Cons";
  3.1225 +val drop_type = thm "drop_type";
  3.1226 +val list_rec_type = thm "list_rec_type";
  3.1227 +val map_type = thm "map_type";
  3.1228 +val map_type2 = thm "map_type2";
  3.1229 +val length_type = thm "length_type";
  3.1230 +val lt_length_in_nat = thm "lt_length_in_nat";
  3.1231 +val app_type = thm "app_type";
  3.1232 +val rev_type = thm "rev_type";
  3.1233 +val flat_type = thm "flat_type";
  3.1234 +val set_of_list_type = thm "set_of_list_type";
  3.1235 +val set_of_list_append = thm "set_of_list_append";
  3.1236 +val list_add_type = thm "list_add_type";
  3.1237 +val map_ident = thm "map_ident";
  3.1238 +val map_compose = thm "map_compose";
  3.1239 +val map_app_distrib = thm "map_app_distrib";
  3.1240 +val map_flat = thm "map_flat";
  3.1241 +val list_rec_map = thm "list_rec_map";
  3.1242 +val list_CollectD = thm "list_CollectD";
  3.1243 +val map_list_Collect = thm "map_list_Collect";
  3.1244 +val length_map = thm "length_map";
  3.1245 +val length_app = thm "length_app";
  3.1246 +val length_rev = thm "length_rev";
  3.1247 +val length_flat = thm "length_flat";
  3.1248 +val drop_length_Cons = thm "drop_length_Cons";
  3.1249 +val drop_length = thm "drop_length";
  3.1250 +val app_right_Nil = thm "app_right_Nil";
  3.1251 +val app_assoc = thm "app_assoc";
  3.1252 +val flat_app_distrib = thm "flat_app_distrib";
  3.1253 +val rev_map_distrib = thm "rev_map_distrib";
  3.1254 +val rev_app_distrib = thm "rev_app_distrib";
  3.1255 +val rev_rev_ident = thm "rev_rev_ident";
  3.1256 +val rev_flat = thm "rev_flat";
  3.1257 +val list_add_app = thm "list_add_app";
  3.1258 +val list_add_rev = thm "list_add_rev";
  3.1259 +val list_add_flat = thm "list_add_flat";
  3.1260 +val list_append_induct = thm "list_append_induct";
  3.1261 +val min_sym = thm "min_sym";
  3.1262 +val min_type = thm "min_type";
  3.1263 +val min_0 = thm "min_0";
  3.1264 +val min_02 = thm "min_02";
  3.1265 +val lt_min_iff = thm "lt_min_iff";
  3.1266 +val min_succ_succ = thm "min_succ_succ";
  3.1267 +val filter_append = thm "filter_append";
  3.1268 +val filter_type = thm "filter_type";
  3.1269 +val length_filter = thm "length_filter";
  3.1270 +val filter_is_subset = thm "filter_is_subset";
  3.1271 +val filter_False = thm "filter_False";
  3.1272 +val filter_True = thm "filter_True";
  3.1273 +val length_is_0_iff = thm "length_is_0_iff";
  3.1274 +val length_is_0_iff2 = thm "length_is_0_iff2";
  3.1275 +val length_tl = thm "length_tl";
  3.1276 +val length_greater_0_iff = thm "length_greater_0_iff";
  3.1277 +val length_succ_iff = thm "length_succ_iff";
  3.1278 +val append_is_Nil_iff = thm "append_is_Nil_iff";
  3.1279 +val append_is_Nil_iff2 = thm "append_is_Nil_iff2";
  3.1280 +val append_left_is_self_iff = thm "append_left_is_self_iff";
  3.1281 +val append_left_is_self_iff2 = thm "append_left_is_self_iff2";
  3.1282 +val append_left_is_Nil_iff = thm "append_left_is_Nil_iff";
  3.1283 +val append_left_is_Nil_iff2 = thm "append_left_is_Nil_iff2";
  3.1284 +val append_eq_append_iff = thm "append_eq_append_iff";
  3.1285 +val append_eq_append = thm "append_eq_append";
  3.1286 +val append_eq_append_iff2 = thm "append_eq_append_iff2";
  3.1287 +val append_self_iff = thm "append_self_iff";
  3.1288 +val append_self_iff2 = thm "append_self_iff2";
  3.1289 +val append1_eq_iff = thm "append1_eq_iff";
  3.1290 +val append_right_is_self_iff = thm "append_right_is_self_iff";
  3.1291 +val append_right_is_self_iff2 = thm "append_right_is_self_iff2";
  3.1292 +val hd_append = thm "hd_append";
  3.1293 +val tl_append = thm "tl_append";
  3.1294 +val rev_is_Nil_iff = thm "rev_is_Nil_iff";
  3.1295 +val Nil_is_rev_iff = thm "Nil_is_rev_iff";
  3.1296 +val rev_is_rev_iff = thm "rev_is_rev_iff";
  3.1297 +val rev_list_elim = thm "rev_list_elim";
  3.1298 +val length_drop = thm "length_drop";
  3.1299 +val drop_all = thm "drop_all";
  3.1300 +val drop_append = thm "drop_append";
  3.1301 +val drop_drop = thm "drop_drop";
  3.1302 +val take_0 = thm "take_0";
  3.1303 +val take_succ_Cons = thm "take_succ_Cons";
  3.1304 +val take_Nil = thm "take_Nil";
  3.1305 +val take_all = thm "take_all";
  3.1306 +val take_type = thm "take_type";
  3.1307 +val take_append = thm "take_append";
  3.1308 +val take_take = thm "take_take";
  3.1309 +val nth_0 = thm "nth_0";
  3.1310 +val nth_Cons = thm "nth_Cons";
  3.1311 +val nth_type = thm "nth_type";
  3.1312 +val nth_append = thm "nth_append";
  3.1313 +val set_of_list_conv_nth = thm "set_of_list_conv_nth";
  3.1314 +val nth_take_lemma = thm "nth_take_lemma";
  3.1315 +val nth_equalityI = thm "nth_equalityI";
  3.1316 +val take_equalityI = thm "take_equalityI";
  3.1317 +val nth_drop = thm "nth_drop";
  3.1318 +val list_on_set_of_list = thm "list_on_set_of_list";
  3.1319 +val zip_Nil = thm "zip_Nil";
  3.1320 +val zip_Nil2 = thm "zip_Nil2";
  3.1321 +val zip_Cons_Cons = thm "zip_Cons_Cons";
  3.1322 +val zip_type = thm "zip_type";
  3.1323 +val length_zip = thm "length_zip";
  3.1324 +val zip_append1 = thm "zip_append1";
  3.1325 +val zip_append2 = thm "zip_append2";
  3.1326 +val zip_append = thm "zip_append";
  3.1327 +val zip_rev = thm "zip_rev";
  3.1328 +val nth_zip = thm "nth_zip";
  3.1329 +val set_of_list_zip = thm "set_of_list_zip";
  3.1330 +val list_update_Nil = thm "list_update_Nil";
  3.1331 +val list_update_Cons_0 = thm "list_update_Cons_0";
  3.1332 +val list_update_Cons_succ = thm "list_update_Cons_succ";
  3.1333 +val list_update_type = thm "list_update_type";
  3.1334 +val length_list_update = thm "length_list_update";
  3.1335 +val nth_list_update = thm "nth_list_update";
  3.1336 +val nth_list_update_eq = thm "nth_list_update_eq";
  3.1337 +val nth_list_update_neq = thm "nth_list_update_neq";
  3.1338 +val list_update_overwrite = thm "list_update_overwrite";
  3.1339 +val list_update_same_conv = thm "list_update_same_conv";
  3.1340 +val update_zip = thm "update_zip";
  3.1341 +val set_update_subset_cons = thm "set_update_subset_cons";
  3.1342 +val set_of_list_update_subsetI = thm "set_of_list_update_subsetI";
  3.1343 +val upt_rec = thm "upt_rec";
  3.1344 +val upt_conv_Nil = thm "upt_conv_Nil";
  3.1345 +val upt_succ_append = thm "upt_succ_append";
  3.1346 +val upt_conv_Cons = thm "upt_conv_Cons";
  3.1347 +val upt_type = thm "upt_type";
  3.1348 +val upt_add_eq_append = thm "upt_add_eq_append";
  3.1349 +val length_upt = thm "length_upt";
  3.1350 +val nth_upt = thm "nth_upt";
  3.1351 +val take_upt = thm "take_upt";
  3.1352 +val map_succ_upt = thm "map_succ_upt";
  3.1353 +val nth_map = thm "nth_map";
  3.1354 +val nth_map_upt = thm "nth_map_upt";
  3.1355 +val sublist_0 = thm "sublist_0";
  3.1356 +val sublist_Nil = thm "sublist_Nil";
  3.1357 +val sublist_shift_lemma = thm "sublist_shift_lemma";
  3.1358 +val sublist_type = thm "sublist_type";
  3.1359 +val upt_add_eq_append2 = thm "upt_add_eq_append2";
  3.1360 +val sublist_append = thm "sublist_append";
  3.1361 +val sublist_Cons = thm "sublist_Cons";
  3.1362 +val sublist_singleton = thm "sublist_singleton";
  3.1363 +val sublist_upt_eq_take = thm "sublist_upt_eq_take";
  3.1364 +
  3.1365 +structure list =
  3.1366 +struct
  3.1367 +val induct = thm "list.induct"
  3.1368 +val elim   = thm "list.cases"
  3.1369 +val intrs  = thms "list.intros"
  3.1370 +end;  
  3.1371 +*}
  3.1372 +
  3.1373  end