# HG changeset patch # User paulson # Date 1026248601 -7200 # Node ID be7105a066d35052938cd45c030f3fb1ef128677 # Parent 900f220c800daa593a56b5ec499b6597a9808200 converted List to new-style diff -r 900f220c800d -r be7105a066d3 src/ZF/IsaMakefile --- a/src/ZF/IsaMakefile Tue Jul 09 18:54:27 2002 +0200 +++ b/src/ZF/IsaMakefile Tue Jul 09 23:03:21 2002 +0200 @@ -36,7 +36,7 @@ InfDatatype.thy Integ/Bin.ML Integ/Bin.thy Integ/EquivClass.ML \ Integ/EquivClass.thy Integ/Int.ML Integ/Int.thy Integ/IntArith.thy \ Integ/IntDiv.ML Integ/IntDiv.thy Integ/int_arith.ML \ - Integ/twos_compl.ML Let.ML Let.thy List.ML List.thy Main.ML Main.thy \ + Integ/twos_compl.ML Let.ML Let.thy List.thy Main.ML Main.thy \ Main_ZFC.ML Main_ZFC.thy Nat.thy Order.thy OrderArith.thy \ OrderType.thy Ordinal.thy OrdQuant.thy Perm.thy \ QPair.thy QUniv.thy ROOT.ML \ diff -r 900f220c800d -r be7105a066d3 src/ZF/List.ML --- a/src/ZF/List.ML Tue Jul 09 18:54:27 2002 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1273 +0,0 @@ -(* Title: ZF/List.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Datatype definition of Lists -*) - -(*** Aspects of the datatype definition ***) - -Addsimps list.intrs; - -(*An elimination rule, for type-checking*) -bind_thm ("ConsE", list.mk_cases "Cons(a,l) : list(A)"); - -(*Proving freeness results*) -bind_thm ("Cons_iff", list.mk_free "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'"); -bind_thm ("Nil_Cons_iff", list.mk_free "~ Nil=Cons(a,l)"); - -Goal "list(A) = {0} + (A * list(A))"; -by (blast_tac (claset() addSIs (map (rewrite_rule list.con_defs) list.intrs) - addEs [rewrite_rule list.con_defs list.elim]) 1); -qed "list_unfold"; - -(** Lemmas to justify using "list" in other recursive type definitions **) - -Goalw list.defs "A<=B ==> list(A) <= list(B)"; -by (rtac lfp_mono 1); -by (REPEAT (rtac list.bnd_mono 1)); -by (REPEAT (ares_tac (univ_mono::basic_monos) 1)); -qed "list_mono"; - -(*There is a similar proof by list induction.*) -Goalw (list.defs@list.con_defs) "list(univ(A)) <= univ(A)"; -by (rtac lfp_lowerbound 1); -by (rtac (A_subset_univ RS univ_mono) 2); -by (blast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ, - Pair_in_univ]) 1); -qed "list_univ"; - -(*These two theorems justify datatypes involving list(nat), list(A), ...*) -bind_thm ("list_subset_univ", [list_mono, list_univ] MRS subset_trans); - -Goal "[| l: list(A); A <= univ(B) |] ==> l: univ(B)"; -by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1)); -qed "list_into_univ"; - -val major::prems = Goal - "[| l: list(A); \ -\ c: C(Nil); \ -\ !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) \ -\ |] ==> list_case(c,h,l) : C(l)"; -by (rtac (major RS list.induct) 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); -qed "list_case_type"; - - -(*** List functions ***) - -Goal "l: list(A) ==> tl(l) : list(A)"; -by (exhaust_tac "l" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps list.intrs))); -qed "tl_type"; - -(** drop **) - -Goal "i:nat ==> drop(i, Nil) = Nil"; -by (induct_tac "i" 1); -by (ALLGOALS Asm_simp_tac); -qed "drop_Nil"; - -Goal "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)"; -by (rtac sym 1); -by (induct_tac "i" 1); -by (Simp_tac 1); -by (Asm_simp_tac 1); -qed "drop_succ_Cons"; - -Addsimps [drop_Nil, drop_succ_Cons]; - -Goal "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)"; -by (induct_tac "i" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [tl_type]))); -qed "drop_type"; - -Delsimps [drop_SUCC]; - - -(** Type checking -- proved by induction, as usual **) - -val prems = Goal - "[| l: list(A); \ -\ c: C(Nil); \ -\ !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) \ -\ |] ==> list_rec(c,h,l) : C(l)"; -by (cut_facts_tac prems 1); -by (induct_tac "l" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); -qed "list_rec_type"; - -(** map **) - -val prems = Goalw [thm "map_list_def"] - "[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)"; -by (REPEAT (ares_tac (prems @ list.intrs @ [list_rec_type]) 1)); -qed "map_type"; - -Goal "l: list(A) ==> map(h,l) : list({h(u). u:A})"; -by (etac map_type 1); -by (etac RepFunI 1); -qed "map_type2"; - -(** length **) - -Goalw [thm "length_list_def"] - "l: list(A) ==> length(l) : nat"; -by (REPEAT (ares_tac [list_rec_type, nat_0I, nat_succI] 1)); -qed "length_type"; - -(** app **) - -Goalw [thm "op @_list_def"] - "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)"; -by (REPEAT (ares_tac [list_rec_type, list.Cons_I] 1)); -qed "app_type"; - -(** rev **) - -Goalw [thm "rev_list_def"] - "xs: list(A) ==> rev(xs) : list(A)"; -by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1)); -qed "rev_type"; - - -(** flat **) - -Goalw [thm "flat_list_def"] - "ls: list(list(A)) ==> flat(ls) : list(A)"; -by (REPEAT (ares_tac (list.intrs @ [list_rec_type, app_type]) 1)); -qed "flat_type"; - - -(** set_of_list **) - -Goalw [thm "set_of_list_list_def"] - "l: list(A) ==> set_of_list(l) : Pow(A)"; -by (etac list_rec_type 1); -by (ALLGOALS (Blast_tac)); -qed "set_of_list_type"; - -Goal "xs: list(A) ==> \ -\ set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)"; -by (etac list.induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_cons]))); -qed "set_of_list_append"; - - -(** list_add **) - -Goalw [thm "list_add_list_def"] - "xs: list(nat) ==> list_add(xs) : nat"; -by (REPEAT (ares_tac [list_rec_type, nat_0I, add_type] 1)); -qed "list_add_type"; - -bind_thms ("list_typechecks", - list.intrs @ - [list_rec_type, map_type, map_type2, app_type, length_type, - rev_type, flat_type, list_add_type]); - -AddTCs list_typechecks; - - -(*** theorems about map ***) - -Goal "l: list(A) ==> map(%u. u, l) = l"; -by (induct_tac "l" 1); -by (ALLGOALS Asm_simp_tac); -qed "map_ident"; -Addsimps [map_ident]; - -Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)"; -by (induct_tac "l" 1); -by (ALLGOALS Asm_simp_tac); -qed "map_compose"; - -Goal "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)"; -by (induct_tac "xs" 1); -by (ALLGOALS Asm_simp_tac); -qed "map_app_distrib"; - -Goal "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))"; -by (induct_tac "ls" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); -qed "map_flat"; - -Goal "l: list(A) ==> \ -\ list_rec(c, d, map(h,l)) = \ -\ list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)"; -by (induct_tac "l" 1); -by (ALLGOALS Asm_simp_tac); -qed "list_rec_map"; - -(** theorems about list(Collect(A,P)) -- used in ex/term.ML **) - -(* c : list(Collect(B,P)) ==> c : list(B) *) -bind_thm ("list_CollectD", Collect_subset RS list_mono RS subsetD); - -Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)"; -by (induct_tac "l" 1); -by (ALLGOALS Asm_simp_tac); -qed "map_list_Collect"; - -(*** theorems about length ***) - -Goal "xs: list(A) ==> length(map(h,xs)) = length(xs)"; -by (induct_tac "xs" 1); -by (ALLGOALS Asm_simp_tac); -qed "length_map"; - -Goal "[| xs: list(A); ys: list(A) |] \ -\ ==> length(xs@ys) = length(xs) #+ length(ys)"; -by (induct_tac "xs" 1); -by (ALLGOALS Asm_simp_tac); -qed "length_app"; - -Goal "xs: list(A) ==> length(rev(xs)) = length(xs)"; -by (induct_tac "xs" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app]))); -qed "length_rev"; - -Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))"; -by (induct_tac "ls" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app]))); -qed "length_flat"; - -(** Length and drop **) - -(*Lemma for the inductive step of drop_length*) -Goal "xs: list(A) ==> \ -\ ALL x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)"; -by (etac list.induct 1); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp "drop_length_Cons"; - -Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))"; -by (etac list.induct 1); -by (ALLGOALS Asm_simp_tac); -by Safe_tac; -by (etac drop_length_Cons 1); -by (rtac natE 1); -by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1); -by (assume_tac 1); -by (ALLGOALS Asm_simp_tac); -by (ALLGOALS (blast_tac (claset() addIs [succ_in_naturalD, length_type]))); -qed_spec_mp "drop_length"; - - -(*** theorems about app ***) - -Goal "xs: list(A) ==> xs@Nil=xs"; -by (etac list.induct 1); -by (ALLGOALS Asm_simp_tac); -qed "app_right_Nil"; -Addsimps [app_right_Nil]; - -Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)"; -by (induct_tac "xs" 1); -by (ALLGOALS Asm_simp_tac); -qed "app_assoc"; - -Goal "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)"; -by (induct_tac "ls" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc]))); -qed "flat_app_distrib"; - -(*** theorems about rev ***) - -Goal "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))"; -by (induct_tac "l" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [map_app_distrib]))); -qed "rev_map_distrib"; - -(*Simplifier needs the premises as assumptions because rewriting will not - instantiate the variable ?A in the rules' typing conditions; note that - rev_type does not instantiate ?A. Only the premises do. -*) -Goal "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)"; -by (etac list.induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc]))); -qed "rev_app_distrib"; - -Goal "l: list(A) ==> rev(rev(l))=l"; -by (induct_tac "l" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib]))); -qed "rev_rev_ident"; -Addsimps [rev_rev_ident]; - -Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))"; -by (induct_tac "ls" 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps - [map_app_distrib, flat_app_distrib, rev_app_distrib]))); -qed "rev_flat"; - - -(*** theorems about list_add ***) - -Goal "[| xs: list(nat); ys: list(nat) |] ==> \ -\ list_add(xs@ys) = list_add(ys) #+ list_add(xs)"; -by (induct_tac "xs" 1); -by (ALLGOALS Asm_simp_tac); -qed "list_add_app"; - -Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)"; -by (induct_tac "l" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app]))); -qed "list_add_rev"; - -Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))"; -by (induct_tac "ls" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app]))); -by (REPEAT (ares_tac [refl, list_add_type, map_type, add_commute] 1)); -qed "list_add_flat"; - -(** New induction rule **) - -val major::prems = Goal - "[| l: list(A); \ -\ P(Nil); \ -\ !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) \ -\ |] ==> P(l)"; -by (rtac (major RS rev_rev_ident RS subst) 1); -by (rtac (major RS rev_type RS list.induct) 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps prems))); -qed "list_append_induct"; - - -(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***) - -(** min **) -(* Min theorems are also true for i, j ordinals *) -Goalw [min_def] "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)"; -by (auto_tac (claset() addSDs [not_lt_imp_le] - addDs [lt_not_sym] - addIs [le_anti_sym], simpset())); -qed "min_sym"; - -Goalw [min_def] "[| i:nat; j:nat |] ==> min(i,j):nat"; -by Auto_tac; -qed "min_type"; -AddTCs [min_type]; -Addsimps [min_type]; - -Goalw [min_def] "i:nat ==> min(0,i) = 0"; -by (auto_tac (claset() addDs [not_lt_imp_le], simpset())); -qed "min_0"; -Addsimps [min_0]; - -Goalw [min_def] "i:nat ==> min(i, 0) = 0"; -by (auto_tac (claset() addDs [not_lt_imp_le], simpset())); -qed "min_02"; -Addsimps [min_02]; - -Goalw [min_def] "[| i:nat; j:nat; k:nat |] ==> i i min(succ(i), succ(j))= succ(min(i, j))"; -by Auto_tac; -qed "min_succ_succ"; -Addsimps [min_succ_succ]; - -(*** more theorems about lists ***) - -Goal "xs:list(A) ==> (xs~=Nil)<->(EX y:A. EX ys:list(A). xs=Cons(y,ys))"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "neq_Nil_iff"; - -(** filter **) - -Goal "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "filter_append"; -Addsimps [filter_append]; - -Goal "xs:list(A) ==> filter(P, xs):list(A)"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "filter_type"; - -Goal "xs:list(A) ==> length(filter(P, xs)) le length(xs)"; -by (induct_tac "xs" 1); -by Auto_tac; -by (res_inst_tac [("j", "length(l)")] le_trans 1); -by (auto_tac (claset(), simpset() addsimps [le_iff])); -qed "length_filter"; - -Goal "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "filter_is_subset"; - -Goal "xs:list(A) ==> filter(%p. False, xs) = Nil"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "filter_False"; - -Goal "xs:list(A) ==> filter(%p. True, xs) = xs"; -by (induct_tac "xs" 1); -by Auto_tac; -qed "filter_True"; -Addsimps [filter_False, filter_True]; - -(** length **) - -Goal "xs:list(A) ==> length(xs)=0 <-> xs=Nil"; -by (etac list.induct 1); -by Auto_tac; -qed "length_is_0_iff"; -Addsimps [length_is_0_iff]; - -Goal "xs:list(A) ==> 0 = length(xs) <-> xs=Nil"; -by (etac list.induct 1); -by Auto_tac; -qed "length_is_0_iff2"; -Addsimps [length_is_0_iff2]; - -Goal "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1"; -by (etac list.induct 1); -by Auto_tac; -qed "length_tl"; -Addsimps [length_tl]; - -Goal "xs:list(A) ==> 0 xs ~= Nil"; -by (etac list.induct 1); -by Auto_tac; -qed "length_greater_0_iff"; - -Goal "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)"; -by (etac list.induct 1); -by Auto_tac; -qed "length_succ_iff"; - -(** more theorems about append **) - -Goal "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)"; -by (etac list.induct 1); -by Auto_tac; -qed "append_is_Nil_iff"; -Addsimps [append_is_Nil_iff]; - -Goal "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)"; -by (etac list.induct 1); -by Auto_tac; -qed "append_is_Nil_iff2"; -Addsimps [append_is_Nil_iff2]; - -Goal "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)"; -by (etac list.induct 1); -by Auto_tac; -qed "append_left_is_self_iff"; -Addsimps [append_left_is_self_iff]; - -Goal "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)"; -by (etac list.induct 1); -by Auto_tac; -qed "append_left_is_self_iff2"; -Addsimps [append_left_is_self_iff2]; - -(*TOO SLOW as a default simprule!*) -Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \ -\ length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))"; -by (etac list.induct 1); -by (auto_tac (claset(), simpset() addsimps [length_app])); -qed_spec_mp "append_left_is_Nil_iff"; - -(*TOO SLOW as a default simprule!*) -Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \ -\ length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))"; -by (etac list.induct 1); -by (auto_tac (claset(), simpset() addsimps [length_app])); -qed_spec_mp "append_left_is_Nil_iff2"; - -Goal "xs:list(A) ==> ALL ys:list(A). \ -\ length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)"; -by (etac list.induct 1); -by (Asm_simp_tac 1); -by (Clarify_tac 1); -by (eres_inst_tac [("a", "ys")] list.elim 1); -by (ALLGOALS(Asm_full_simp_tac)); -qed_spec_mp "append_eq_append_iff"; - - -Goal "xs:list(A) ==> \ -\ ALL ys:list(A). ALL us:list(A). ALL vs:list(A). \ -\ length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)"; -by (induct_tac "xs" 1); -by (ALLGOALS(Clarify_tac)); -by (asm_full_simp_tac (simpset() addsimps [length_app]) 1); -by (eres_inst_tac [("a", "ys")] list.elim 1); -by (Asm_full_simp_tac 1); -by (subgoal_tac "Cons(a, l) @ us =vs" 1); -by (dtac (rotate_prems 4 (append_left_is_Nil_iff RS iffD1)) 1); -by Auto_tac; -qed_spec_mp "append_eq_append"; - -Goal "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |] \ -\ ==> xs@us = ys@vs <-> (xs=ys & us=vs)"; -by (rtac iffI 1); -by (rtac append_eq_append 1); -by Auto_tac; -qed "append_eq_append_iff2"; -Addsimps [append_eq_append_iff, append_eq_append_iff2]; - -Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs"; -by (Asm_simp_tac 1); -qed "append_self_iff"; -Addsimps [append_self_iff]; - -Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs"; -by (Asm_simp_tac 1); -qed "append_self_iff2"; -Addsimps [append_self_iff2]; - -(* Can also be proved from append_eq_append_iff2, -but the proof requires two more hypotheses: x:A and y:A *) -Goal "xs:list(A) ==> ALL ys:list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)"; -by (etac list.induct 1); -by (ALLGOALS(Clarify_tac)); -by (ALLGOALS(eres_inst_tac [("a", "ys")] list.elim)); -by Auto_tac; -qed_spec_mp "append1_eq_iff"; -Addsimps [append1_eq_iff]; - -Goal "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)"; -by (asm_simp_tac (simpset() addsimps [append_left_is_Nil_iff]) 1); -qed "append_right_is_self_iff"; -Addsimps [append_right_is_self_iff]; - -Goal "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)"; -by (rtac iffI 1); -by (dtac sym 1); -by (ALLGOALS(Asm_full_simp_tac)); -qed "append_right_is_self_iff2"; -Addsimps [append_right_is_self_iff2]; - -Goal "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)"; -by (induct_tac "xs" 1); -by Auto_tac; -qed_spec_mp "hd_append"; -Addsimps [hd_append]; - -Goal "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys"; -by (induct_tac "xs" 1); -by Auto_tac; -qed_spec_mp "tl_append"; -Addsimps [tl_append]; - -(** rev **) -Goal "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)"; -by (etac list.induct 1); -by Auto_tac; -qed "rev_is_Nil_iff"; -Addsimps [rev_is_Nil_iff]; - -Goal "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)"; -by (etac list.induct 1); -by Auto_tac; -qed "Nil_is_rev_iff"; -Addsimps [Nil_is_rev_iff]; - -Goal "xs:list(A) ==> ALL ys:list(A). rev(xs)=rev(ys) <-> xs=ys"; -by (etac list.induct 1); -by (Force_tac 1); -by (Clarify_tac 1); -by (eres_inst_tac [("a", "ys")] list.elim 1); -by Auto_tac; -qed_spec_mp "rev_is_rev_iff"; -Addsimps [rev_is_rev_iff]; - -Goal "xs:list(A) ==> \ -\ (xs=Nil --> P) --> (ALL ys:list(A). ALL y:A. xs =ys@[y] -->P)-->P"; -by (etac list_append_induct 1); -by Auto_tac; -qed_spec_mp "rev_list_elim_aux"; - -bind_thm("rev_list_elim", impI RS ballI RS ballI RSN(3, rev_list_elim_aux)); - -(** more theorems about drop **) - -Goal "n:nat ==> ALL xs:list(A). length(drop(n, xs)) = length(xs) #- n"; -by (etac nat_induct 1); -by (auto_tac (claset() addEs [list.elim], simpset())); -qed_spec_mp "length_drop"; -Addsimps [length_drop]; - -Goal "n:nat ==> ALL xs:list(A). length(xs) le n --> drop(n, xs)=Nil"; -by (etac nat_induct 1); -by (auto_tac (claset() addEs [list.elim], simpset())); -qed_spec_mp "drop_all"; -Addsimps [drop_all]; - -Goal "n:nat ==> ALL xs:list(A). drop(n, xs@ys) = \ -\ drop(n,xs) @ drop(n #- length(xs), ys)"; -by (induct_tac "n" 1); -by (auto_tac (claset() addEs [list.elim], simpset())); -qed_spec_mp "drop_append"; - -Goal "m:nat ==> \ -\ ALL xs:list(A). ALL n:nat. drop(n, drop(m, xs))=drop(n #+ m, xs)"; -by (induct_tac "m" 1); -by (auto_tac (claset() addEs [list.elim], simpset())); -qed "drop_drop"; - -(** take **) - -Goalw [take_def] - "xs:list(A) ==> take(0, xs) = Nil"; -by (etac list.induct 1); -by Auto_tac; -qed "take_0"; -Addsimps [take_0]; - -Goalw [take_def] -"n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))"; -by (Asm_simp_tac 1); -qed "take_succ_Cons"; -Addsimps [take_succ_Cons]; - -(* Needed for proving take_all *) -Goalw [take_def] - "n:nat ==> take(n, Nil) = Nil"; -by Auto_tac; -qed "take_Nil"; -Addsimps [take_Nil]; - -Goal "n:nat ==> ALL xs:list(A). length(xs) le n --> take(n, xs) = xs"; -by (etac nat_induct 1); -by (auto_tac (claset() addEs [list.elim], simpset())); -qed_spec_mp "take_all"; -Addsimps [take_all]; - -Goal "xs:list(A) ==> ALL n:nat. take(n, xs):list(A)"; -by (etac list.induct 1); -by (Clarify_tac 2); -by (etac natE 2); -by Auto_tac; -qed_spec_mp "take_type"; - -Goal "xs:list(A) ==> \ -\ ALL ys:list(A). ALL n:nat. take(n, xs @ ys) = \ -\ take(n, xs) @ take(n #- length(xs), ys)"; -by (etac list.induct 1); -by (Clarify_tac 2); -by (etac natE 2); -by Auto_tac; -qed_spec_mp "take_append"; -Addsimps [take_append]; - -Goal -"m:nat ==> \ -\ ALL xs:list(A). ALL n:nat. take(n, take(m,xs))= take(min(n, m), xs)"; -by (induct_tac "m" 1); -by Auto_tac; -by (eres_inst_tac [("a", "xs")] list.elim 1); -by (auto_tac (claset(), simpset() addsimps [take_Nil])); -by (rotate_tac 1 1); -by (etac natE 1); -by (auto_tac (claset() addIs [take_0, take_type], simpset())); -qed_spec_mp "take_take"; - -(** nth **) - -Goalw [nth_def] "nth(0, Cons(a, l))= a"; -by Auto_tac; -qed "nth_0"; -Addsimps [nth_0]; - -Goalw [nth_def] - "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)"; -by (Asm_simp_tac 1); -qed "nth_Cons"; -Addsimps [nth_Cons]; - -Goal "xs:list(A) ==> ALL n:nat. n < length(xs) --> nth(n, xs):A"; -by (etac list.induct 1); -by (ALLGOALS(Clarify_tac)); -by (etac natE 2); -by (ALLGOALS(Asm_full_simp_tac)); -qed_spec_mp "nth_type"; - -AddTCs [nth_type]; -Addsimps [nth_type]; - -Goal -"xs:list(A) ==> ALL n:nat. \ -\ nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) \ -\ else nth(n #- length(xs),ys))"; -by (induct_tac "xs" 1); -by (Clarify_tac 2); -by (etac natE 2); -by (ALLGOALS(Asm_full_simp_tac)); -qed_spec_mp "nth_append"; - -Goal "xs:list(A) \ -\ ==> set_of_list(xs) = {x:A. EX i:nat. i \ -\ ALL xs:list(A). (ALL ys:list(A). k le length(xs) --> k le length(ys) --> \ -\ (ALL i:nat. i nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))"; -by (induct_tac "k" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps - [lt_succ_eq_0_disj, all_conj_distrib]))); -by (Clarify_tac 1); -(*Both lists must be non-empty*) -by (case_tac "xa=Nil" 1); -by (case_tac "xb=Nil" 2); -by (Clarify_tac 1); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff]))); -by (Clarify_tac 1); -(*prenexing's needed, not miniscoping*) -by (Asm_simp_tac 1); -by (rtac conjI 1); -by (Force_tac 1); -by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [iff_sym]) - delsimps (all_simps)))); -by (dres_inst_tac [("x", "ys"), ("x1", "ysa")] (spec RS spec) 1); -by (Clarify_tac 1); -by Auto_tac; -qed_spec_mp "nth_take_lemma"; - -Goal "[| xs:list(A); ys:list(A); length(xs) = length(ys); \ -\ ALL i:nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |] \ -\ ==> xs = ys"; -by (subgoal_tac "length(xs) le length(ys)" 1); -by (forw_inst_tac [("ys", "ys")] (rotate_prems 1 nth_take_lemma) 1); -by (ALLGOALS(Asm_simp_tac)); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [take_all]))); -qed_spec_mp "nth_equalityI"; - -(*The famous take-lemma*) - -Goal "[| xs:list(A); ys:list(A); (ALL i:nat. take(i, xs) = take(i,ys)) |] ==> xs = ys"; -by (case_tac "length(xs) le length(ys)" 1); -by (dres_inst_tac [("x", "length(ys)")] bspec 1); -by (dtac not_lt_imp_le 3); -by (subgoal_tac "length(ys) le length(xs)" 5); -by (res_inst_tac [("j", "succ(length(ys))")] le_trans 6); -by (rtac leI 6); -by (dres_inst_tac [("x", "length(xs)")] bspec 5); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [take_all]))); -qed_spec_mp "take_equalityI"; - -Goal "n:nat ==> ALL i:nat. ALL xs:list(A). n #+ i le length(xs) \ -\ --> nth(i, drop(n, xs)) = nth(n #+ i, xs)"; -by (induct_tac "n" 1); -by (ALLGOALS(Asm_full_simp_tac)); -by (Clarify_tac 1); -by (case_tac "xb=Nil" 1); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff]))); -by (Clarify_tac 1); -by (auto_tac (claset() addSEs [ConsE], simpset())); -qed_spec_mp "nth_drop"; - -(** zip **) - -Goal "l:list(A) ==> l:list(set_of_list(l))"; -by (induct_tac "l" 1); -by Auto_tac; -by (res_inst_tac [("A1", "set_of_list(l)")] (list_mono RS subsetD) 1); -by Auto_tac; -qed "list_on_set_of_list"; - -Goal "A<=C ==> ziprel(A, B) <= ziprel(C,B)"; -by (Clarify_tac 1); -by (forward_tac [ziprel.dom_subset RS subsetD] 1); -by (Clarify_tac 1); -by (etac ziprel.induct 1); -by (auto_tac (claset() addIs [list_mono RS subsetD] - addSIs ziprel.intrs, simpset())); -qed "ziprel_mono1"; - -Goal "B<=C ==> ziprel(A, B) <= ziprel(A,C)"; -by (Clarify_tac 1); -by (forward_tac [ziprel.dom_subset RS subsetD] 1); -by (Clarify_tac 1); -by (etac ziprel.induct 1); -by (auto_tac (claset() addIs [list_mono RS subsetD] - addSIs ziprel.intrs, simpset())); -qed "ziprel_mono2"; - -Goal "[| A<=C; B<=D |] ==> ziprel(A, B) <= ziprel(C,D)"; -by (rtac subset_trans 1); -by (rtac ziprel_mono1 2); -by (rtac ziprel_mono2 1); -by Auto_tac; -qed "ziprel_mono"; - -(* ziprel is a function *) - -Goal ":ziprel(A,B) \ -\ ==> ALL ks. :ziprel(A, B) --> ks=zs"; -by (etac ziprel.induct 1); -by (ALLGOALS(Clarify_tac)); -by (rotate_tac 1 3); -by (ALLGOALS(etac ziprel.elim)); -by Safe_tac; -(* These hypotheses make Auto_tac loop! *) -by (thin_tac "ALL k. ?P(k)" 3); -by (thin_tac "ALL k. ?P(k)" 4); -by Auto_tac; -qed "ziprel_is_fun"; - -Goal "ys:list(B) ==> ALL xs:list(A). EX zs. :ziprel(A,B)"; -by (induct_tac "ys" 1); -by (auto_tac (claset() addIs ziprel.intrs, simpset())); -by (eres_inst_tac [("a", "xs")] list.elim 1); -by (auto_tac (claset() addIs ziprel.intrs, simpset())); -qed_spec_mp "ziprel_exist"; - -Goalw [zip_def] - "[|xs:list(A); ys:list(B) |] ==> :ziprel(A,B)"; -by (rtac theI2 1); -by (asm_full_simp_tac (simpset() addsimps [set_of_list_append]) 2); -by (REPEAT(dtac set_of_list_type 2)); -by (rtac (ziprel_mono RS subsetD) 2); -by (Blast_tac 3); -by (dtac list_on_set_of_list 1); -by (dtac list_on_set_of_list 1); -by (subgoal_tac "xs:list(set_of_list(xs@ys)) & \ -\ ys:list(set_of_list(xs@ys))" 1); -by (auto_tac (claset() addIs [list_mono RS subsetD], - simpset() addsimps [set_of_list_append])); -by (rtac (ziprel_is_fun RS spec RS mp) 2); -by (rtac ziprel_exist 1); -by Auto_tac; -qed "zip_in_ziprel"; - -Goal -":ziprel(A,B) ==> zip(xs, ys)=zs"; -by (rtac (ziprel_is_fun RS spec RS mp) 1); -by (Blast_tac 1); -by (blast_tac (claset() addDs [ziprel.dom_subset RS subsetD] - addIs [zip_in_ziprel]) 1); -qed "zip_eq"; - -(* zip equations *) - -Goal "ys:list(A) ==> zip(Nil, ys)=Nil"; -by (res_inst_tac [("A", "A")] zip_eq 1); -by (auto_tac (claset() addIs ziprel.intrs, simpset())); -qed "zip_Nil"; -Addsimps [zip_Nil]; - -Goal "xs:list(A) ==> zip(xs, Nil)=Nil"; -by (res_inst_tac [("A", "A")] zip_eq 1); -by (auto_tac (claset() addIs ziprel.intrs, simpset())); -qed "zip_Nil2"; -Addsimps [zip_Nil2]; - -Goal "[| xs:list(A); ys:list(B); x:A; y:B |] ==> \ -\ zip(Cons(x,xs), Cons(y, ys)) = Cons(, zip(xs, ys))"; -by (res_inst_tac [("A", "A")] zip_eq 1); -by (forw_inst_tac [("ys", "ys")] zip_in_ziprel 1); -by (auto_tac (claset() addIs ziprel.intrs, simpset())); -qed "zip_Cons_Cons"; -Addsimps [zip_Cons_Cons]; - -Goal "xs:list(A) ==> ALL ys:list(B). zip(xs, ys):list(A*B)"; -by (induct_tac "xs" 1); -by (Simp_tac 1); -by (Clarify_tac 1); -by (eres_inst_tac [("a", "ys")] list.elim 1); -by Auto_tac; -qed_spec_mp "zip_type"; - -AddTCs [zip_type]; -Addsimps [zip_type]; - -(* zip length *) -Goalw [min_def] "xs:list(A) ==> ALL ys:list(B). length(zip(xs,ys)) = \ -\ min(length(xs), length(ys))"; -by (induct_tac "xs" 1); -by (Clarify_tac 2); -by (eres_inst_tac [("a", "ys")] list.elim 2); -by Auto_tac; -qed_spec_mp "length_zip"; -Addsimps [length_zip]; - -AddTCs [take_type]; -Addsimps [take_type]; - -Goal "[| ys:list(A); zs:list(B) |] ==> ALL xs:list(A). zip(xs @ ys, zs) = \ -\ zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))"; -by (induct_tac "zs" 1); -by (Clarify_tac 2); -by (eres_inst_tac [("a", "xs")] list.elim 2); -by Auto_tac; -qed_spec_mp "zip_append1"; - -Goal - "[| xs:list(A); zs:list(B) |] ==> ALL ys:list(B). zip(xs, ys@zs) = \ -\ zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)"; -by (induct_tac "xs" 1); -by (Clarify_tac 2); -by (eres_inst_tac [("a", "ys")] list.elim 2); -by Auto_tac; -qed_spec_mp "zip_append2"; - -Goal - "[| length(xs) = length(us); length(ys) = length(vs); \ -\ xs:list(A); us:list(B); ys:list(A); vs:list(B) |] ==> \ -\ zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)"; -by (asm_simp_tac (simpset() addsimps - [zip_append1, drop_append, diff_self_eq_0]) 1); -qed_spec_mp "zip_append"; -Addsimps [zip_append]; - -Goal "ys:list(B) ==> ALL xs:list(A). \ -\ length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))"; -by (induct_tac "ys" 1); -by (Clarify_tac 2); -by (eres_inst_tac [("a", "xs")] list.elim 2); -by (auto_tac (claset(), simpset() addsimps [length_rev])); -qed_spec_mp "zip_rev"; -Addsimps [zip_rev]; - -Goal -"ys:list(B) ==> ALL i:nat. ALL xs:list(A). \ -\ i < length(xs) --> i < length(ys) --> \ -\ nth(i,zip(xs, ys)) = "; -by (induct_tac "ys" 1); -by (Clarify_tac 2); -by (eres_inst_tac [("a", "xs")] list.elim 2); -by (auto_tac (claset() addEs [natE], simpset())); -qed_spec_mp "nth_zip"; -Addsimps [nth_zip]; - -Goal "[| xs:list(A); ys:list(B); i:nat |] \ -\ ==> set_of_list(zip(xs, ys)) = \ -\ {:A*B. EX i:nat. i < min(length(xs), length(ys)) \ -\ & x=nth(i, xs) & y=nth(i, ys)}"; -by (force_tac (claset() addSIs [Collect_cong], - simpset() addsimps [lt_min_iff, set_of_list_conv_nth]) 1); -qed_spec_mp "set_of_list_zip"; - -(** list_update **) - -Goalw [list_update_def] "i:nat ==>list_update(Nil, i, v) = Nil"; -by Auto_tac; -qed "list_update_Nil"; -Addsimps [list_update_Nil]; - -Goalw [list_update_def] -"list_update(Cons(x, xs), 0, v)= Cons(v, xs)"; -by Auto_tac; -qed "list_update_Cons_0"; -Addsimps [list_update_Cons_0]; - -Goalw [list_update_def] -"n:nat ==>\ -\ list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))"; -by Auto_tac; -qed "list_update_Cons_succ"; -Addsimps [list_update_Cons_succ]; - -Goal "[| xs:list(A); v:A |] ==> ALL n:nat. list_update(xs, n, v):list(A)"; -by (induct_tac "xs" 1); -by (Simp_tac 1); -by (Clarify_tac 1); -by (etac natE 1); -by Auto_tac; -qed_spec_mp "list_update_type"; -Addsimps [list_update_type]; -AddTCs [list_update_type]; - -Goal "xs:list(A) ==> ALL i:nat. length(list_update(xs, i, v))=length(xs)"; -by (induct_tac "xs" 1); -by (Simp_tac 1); -by (Clarify_tac 1); -by (etac natE 1); -by Auto_tac; -qed_spec_mp "length_list_update"; -Addsimps [length_list_update]; - -Goal "[| xs:list(A) |] ==> ALL i:nat. ALL j:nat. i < length(xs) --> \ -\ nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (etac natE 1); -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS(Clarify_tac)); -by (etac natE 1); -by (ALLGOALS(Asm_full_simp_tac)); -by Safe_tac; -by (etac natE 2); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nth_Cons]))); -qed_spec_mp "nth_list_update"; - -Goal "[| i < length(xs); xs:list(A); i:nat |] \ -\ ==> nth(i, list_update(xs, i,x)) = x"; -by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1); -qed "nth_list_update_eq"; -Addsimps [nth_list_update_eq]; - -Goal "xs:list(A) ==> ALL i:nat. ALL j:nat. i ~= j \ -\ --> nth(j, list_update(xs, i,x)) = nth(j, xs)"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (etac natE 1); -by (etac natE 2); -by (ALLGOALS(Asm_full_simp_tac)); -by (etac natE 1); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [nth_Cons]))); -qed_spec_mp "nth_list_update_neq"; -Addsimps [nth_list_update_neq]; - -Goal "xs:list(A) ==> ALL i:nat. i < length(xs)\ -\ --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (etac natE 1); -by Auto_tac; -qed_spec_mp "list_update_overwrite"; -Addsimps [list_update_overwrite]; - -Goal "xs:list(A) ==> ALL i:nat. i < length(xs) --> \ -\ (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)"; -by (induct_tac "xs" 1); - by (Simp_tac 1); -by (Clarify_tac 1); -by (etac natE 1); -by Auto_tac; -qed_spec_mp "list_update_same_conv"; - -Goal "ys:list(B) ==> ALL i:nat. ALL xy:A*B. ALL xs:list(A). \ -\ length(xs) = length(ys) --> \ -\ list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)), \ -\ list_update(ys, i, snd(xy)))"; -by (induct_tac "ys" 1); - by Auto_tac; -by (eres_inst_tac [("a", "xc")] list.elim 1); -by (auto_tac (claset() addEs [natE], simpset())); -qed_spec_mp "update_zip"; - -Goal "xs:list(A) ==> ALL i:nat. set_of_list(list_update(xs, i, x)) \ -\ <= cons(x, set_of_list(xs))"; -by (induct_tac "xs" 1); - by (asm_full_simp_tac (simpset() addsimps []) 1); -by (rtac ballI 1); -by (etac natE 1); -by (ALLGOALS(Asm_full_simp_tac)); -by Auto_tac; -qed_spec_mp "set_update_subset_cons"; - -Goal "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|] \ -\ ==> set_of_list(list_update(xs, i,x)) <= A"; -by (rtac subset_trans 1); -by (rtac set_update_subset_cons 1); -by Auto_tac; -qed "set_of_list_update_subsetI"; - -(** upt **) - -Goal "[| i:nat; j:nat |] \ -\ ==> upt(i,j) = (if i upt(i,j) = Nil"; -by (stac upt_rec 1); -by Auto_tac; -by (auto_tac (claset(), simpset() addsimps [le_iff])); -by (dtac (lt_asym RS notE) 1); -by Auto_tac; -qed "upt_conv_Nil"; -Addsimps [upt_conv_Nil]; - -(*Only needed if upt_Suc is deleted from the simpset*) -Goal "[| i le j; i:nat; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]"; -by (Asm_simp_tac 1); -qed "upt_succ_append"; - -Goal "[| i upt(i,j) = Cons(i,upt(succ(i),j))"; -by (rtac trans 1); -by (stac upt_rec 1); -by (rtac refl 4); -by Auto_tac; -qed "upt_conv_Cons"; - -Goal "[| i:nat; j:nat |] ==> upt(i,j):list(nat)"; -by (induct_tac "j" 1); -by Auto_tac; -qed "upt_type"; - -AddTCs [upt_type]; -Addsimps [upt_type]; - -(*LOOPS as a simprule, since j<=j*) -Goal "[| i le j; i:nat; j:nat; k:nat |] ==> \ -\ upt(i, j #+k) = upt(i,j)@upt(j,j#+k)"; -by (induct_tac "k" 1); -by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type])); -by (res_inst_tac [("j", "j")] le_trans 1); -by Auto_tac; -qed "upt_add_eq_append"; - -Goal "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i"; -by (induct_tac "j" 1); -by (rtac sym 2); -by (auto_tac (claset() addSDs [not_lt_imp_le], - simpset() addsimps [length_app, diff_succ, diff_is_0_iff])); -qed "length_upt"; -Addsimps [length_upt]; - -Goal "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k"; -by (induct_tac "j" 1); -by (Asm_simp_tac 1); -by (asm_full_simp_tac (simpset() addsimps [nth_append,le_iff] - addsplits [nat_diff_split]) 1); -by Safe_tac; -by (auto_tac (claset() addSDs [not_lt_imp_le], - simpset() addsimps [nth_append, diff_self_eq_0, - less_diff_conv, add_commute])); -by (dres_inst_tac [("j", "x")] lt_trans2 1); -by Auto_tac; -qed_spec_mp "nth_upt"; -Addsimps [nth_upt]; - -Goal "[| m:nat; n:nat |] ==> \ -\ ALL i:nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)"; -by (induct_tac "m" 1); -by (asm_simp_tac (simpset() addsimps [take_0]) 1); -by (Clarify_tac 1); -by (stac upt_rec 1); -by (rtac sym 3); -by (stac upt_rec 3); -by (ALLGOALS(asm_full_simp_tac (simpset() delsimps (thms"upt.simps")))); -by (res_inst_tac [("j", "succ(i #+ x)")] lt_trans2 1); -by Auto_tac; -qed_spec_mp "take_upt"; -Addsimps [take_upt]; - -Goal "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))"; -by (induct_tac "n" 1); -by (auto_tac (claset(), simpset() addsimps [map_app_distrib])); -qed "map_succ_upt"; - -Goal "xs:list(A) ==> \ -\ ALL n:nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))"; -by (induct_tac "xs" 1); -by (Asm_full_simp_tac 1); -by (rtac ballI 1); -by (induct_tac "n" 1); -by Auto_tac; -qed_spec_mp "nth_map"; -Addsimps [nth_map]; - -Goal "[| m:nat; n:nat |] ==> \ -\ ALL i:nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)"; -by (res_inst_tac [("n", "m"), ("m", "n")] diff_induct 1); -by (stac (map_succ_upt RS sym) 5); -by (ALLGOALS(Asm_full_simp_tac)); -by (ALLGOALS(Clarify_tac)); -by (subgoal_tac "xa < length(upt(0, x))" 1); -by (Asm_simp_tac 2); -by (subgoal_tac "xa < length(upt(y, x))" 2); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [map_compose, - nth_map, add_commute, less_diff_conv]))); -by (res_inst_tac [("j", "succ(xa #+ y)")] lt_trans2 1); -by Auto_tac; -qed_spec_mp "nth_map_upt"; - -(** sublist (a generalization of nth to sets) **) - -Goalw [sublist_def] "xs:list(A) ==>sublist(xs, 0) =Nil"; -by Auto_tac; -qed "sublist_0"; - -Goalw [sublist_def] "sublist(Nil, A) = Nil"; -by Auto_tac; -qed "sublist_Nil"; - -AddTCs [filter_type]; -Addsimps [filter_type]; - -Goal "[| xs:list(B); i:nat |] ==>\ -\ map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) = \ -\ map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))"; -by (etac list_append_induct 1); -by (Asm_simp_tac 1); -by (auto_tac (claset(), simpset() addsimps - [add_commute, length_app, filter_append, map_app_distrib])); -qed "sublist_shift_lemma"; - -Goalw [sublist_def] - "xs:list(B) ==> sublist(xs, A):list(B)"; -by (induct_tac "xs" 1); -by (auto_tac (claset(), simpset() addsimps [filter_append, map_app_distrib])); -by (auto_tac (claset() addIs [map_type,filter_type,zip_type], simpset())); -qed "sublist_type"; - -AddTCs [sublist_type]; -Addsimps [sublist_type]; - -Goal "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)"; -by (asm_simp_tac (simpset() addsimps - [inst "i" "0" upt_add_eq_append, nat_0_le]) 1); -qed "upt_add_eq_append2"; - -Goalw [sublist_def] - "[| xs:list(B); ys:list(B) |] ==> \ -\ sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})"; -by (eres_inst_tac [("l", "ys")] list_append_induct 1); -by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addsimps [upt_add_eq_append2, - zip_append, length_app, app_assoc RS sym]) 1); -by (auto_tac (claset(), simpset() addsimps [sublist_shift_lemma, - length_type, map_app_distrib, app_assoc])); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [add_commute]))); -qed "sublist_append"; - -Addsimps [sublist_0, sublist_Nil]; - -Goal "[| xs:list(B); x:B |] ==> \ -\ sublist(Cons(x, xs), A) = (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})"; -by (eres_inst_tac [("l", "xs")] list_append_induct 1); -by (asm_simp_tac (simpset() addsimps [sublist_def]) 1); -by (asm_simp_tac (simpset() delsimps (thms "op @.simps") - addsimps [(hd (tl (thms "op @.simps"))) RS sym, sublist_append]) 1); -by Auto_tac; -qed "sublist_Cons"; - -Goal "sublist([x], A) = (if 0 : A then [x] else [])"; -by (simp_tac (simpset() addsimps [sublist_Cons]) 1); -qed "sublist_singleton"; -Addsimps [sublist_singleton]; - -Goalw [less_than_def] - "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)"; -by (eres_inst_tac [("l", "xs")] list_append_induct 1); - by (asm_simp_tac (simpset() addsplits [nat_diff_split] - addsimps [sublist_append]) 2); -by Auto_tac; -by (subgoal_tac "n #- length(y) = 0" 1); -by (Asm_simp_tac 1); -by (auto_tac (claset() addSDs [not_lt_imp_le], - simpset() addsimps [diff_is_0_iff])); -qed "sublist_upt_eq_take"; -Addsimps [sublist_upt_eq_take]; - diff -r 900f220c800d -r be7105a066d3 src/ZF/List.thy --- a/src/ZF/List.thy Tue Jul 09 18:54:27 2002 +0200 +++ b/src/ZF/List.thy Tue Jul 09 23:03:21 2002 +0200 @@ -3,18 +3,15 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1994 University of Cambridge -Lists in Zermelo-Fraenkel Set Theory - -map is a binding operator -- it applies to meta-level functions, not -object-level functions. This simplifies the final form of term_rec_conv, -although complicating its derivation. *) -List = Datatype + ArithSimp + +header{*Lists in Zermelo-Fraenkel Set Theory*} + +theory List = Datatype + ArithSimp: consts list :: "i=>i" - + datatype "list(A)" = Nil | Cons ("a:A", "l: list(A)") @@ -37,7 +34,7 @@ primrec "length([]) = 0" "length(Cons(a,l)) = succ(length(l))" - + primrec "hd(Cons(a,l)) = a" @@ -47,22 +44,25 @@ consts - map :: "[i=>i, i] => i" + map :: "[i=>i, i] => i" set_of_list :: "i=>i" - "@" :: "[i,i]=>i" (infixr 60) - + app :: "[i,i]=>i" (infixr "@" 60) + +(*map is a binding operator -- it applies to meta-level functions, not +object-level functions. This simplifies the final form of term_rec_conv, +although complicating its derivation.*) primrec "map(f,[]) = []" "map(f,Cons(a,l)) = Cons(f(a), map(f,l))" - + primrec "set_of_list([]) = 0" "set_of_list(Cons(a,l)) = cons(a, set_of_list(l))" - + primrec - "[] @ ys = ys" - "(Cons(a,l)) @ ys = Cons(a, l @ ys)" - + app_Nil: "[] @ ys = ys" + app_Cons: "(Cons(a,l)) @ ys = Cons(a, l @ ys)" + consts rev :: "i=>i" @@ -76,17 +76,17 @@ primrec "flat([]) = []" "flat(Cons(l,ls)) = l @ flat(ls)" - + primrec "list_add([]) = 0" "list_add(Cons(a,l)) = a #+ list_add(l)" - + consts drop :: "[i,i]=>i" primrec - drop_0 "drop(0,l) = l" - drop_SUCC "drop(succ(i), l) = tl (drop(i,l))" + drop_0: "drop(0,l) = l" + drop_SUCC: "drop(succ(i), l) = tl (drop(i,l))" (*** Thanks to Sidi Ehmety for the following ***) @@ -96,7 +96,7 @@ take :: "[i,i]=>i" "take(n, as) == list_rec(lam n:nat. [], %a l r. lam n:nat. nat_case([], %m. Cons(a, r`m), n), as)`n" - + (* Function `nth' returns the (n+1)th element in a list (not defined at Nil) *) nth :: "[i, i]=>i" "nth(n, as) == list_rec(lam n:nat. 0, @@ -108,21 +108,7 @@ consts filter :: "[i=>o, i] => i" - zip :: "[i, i]=>i" - ziprel :: "[i,i]=>i" upt :: "[i, i] =>i" - -inductive domains "ziprel(A, B)" <= "list(A)*list(B)*list(A*B)" -intrs - ziprel_Nil1 "ys:list(B) ==>:ziprel(A, B)" - ziprel_Nil2 "xs:list(A) ==>:ziprel(A, B)" - ziprel_Cons "[| :ziprel(A, B); x:A; y:B |]==> - , zs)>:ziprel(A,B)" - type_intrs "list.intrs" - -defs - zip_def "zip(xs, ys) == - THE zs. :ziprel(set_of_list(xs),set_of_list(ys))" primrec "filter(P, Nil) = Nil" @@ -134,14 +120,1246 @@ "upt(i, succ(j)) = (if i le j then upt(i, j)@[j] else Nil)" constdefs - sublist :: "[i, i] => i" - "sublist(xs, A)== - map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))" - min :: "[i,i] =>i" "min(x, y) == (if x le y then x else y)" - + max :: "[i, i] =>i" "max(x, y) == (if x le y then y else x)" +(*** Aspects of the datatype definition ***) + +declare list.intros [simp,TC] + +(*An elimination rule, for type-checking*) +inductive_cases ConsE: "Cons(a,l) : list(A)" + +(*Proving freeness results*) +lemma Cons_iff: "Cons(a,l)=Cons(a',l') <-> a=a' & l=l'" +by auto + +lemma Nil_Cons_iff: "~ Nil=Cons(a,l)" +by auto + +lemma list_unfold: "list(A) = {0} + (A * list(A))" +by (blast intro!: list.intros [unfolded list.con_defs] + elim: list.cases [unfolded list.con_defs]) + + +(** Lemmas to justify using "list" in other recursive type definitions **) + +lemma list_mono: "A<=B ==> list(A) <= list(B)" +apply (unfold list.defs ) +apply (rule lfp_mono) +apply (simp_all add: list.bnd_mono) +apply (assumption | rule univ_mono basic_monos)+ +done + +(*There is a similar proof by list induction.*) +lemma list_univ: "list(univ(A)) <= univ(A)" +apply (unfold list.defs list.con_defs) +apply (rule lfp_lowerbound) +apply (rule_tac [2] A_subset_univ [THEN univ_mono]) +apply (blast intro!: zero_in_univ Inl_in_univ Inr_in_univ Pair_in_univ) +done + +(*These two theorems justify datatypes involving list(nat), list(A), ...*) +lemmas list_subset_univ = subset_trans [OF list_mono list_univ] + +lemma list_into_univ: "[| l: list(A); A <= univ(B) |] ==> l: univ(B)" +by (blast intro: list_subset_univ [THEN subsetD]) + +lemma list_case_type: + "[| l: list(A); + c: C(Nil); + !!x y. [| x: A; y: list(A) |] ==> h(x,y): C(Cons(x,y)) + |] ==> list_case(c,h,l) : C(l)" +apply (erule list.induct, auto) +done + + +(*** List functions ***) + +lemma tl_type: "l: list(A) ==> tl(l) : list(A)" +apply (induct_tac "l") +apply (simp_all (no_asm_simp) add: list.intros) +done + +(** drop **) + +lemma drop_Nil [simp]: "i:nat ==> drop(i, Nil) = Nil" +apply (induct_tac "i") +apply (simp_all (no_asm_simp)) +done + +lemma drop_succ_Cons [simp]: "i:nat ==> drop(succ(i), Cons(a,l)) = drop(i,l)" +apply (rule sym) +apply (induct_tac "i") +apply (simp (no_asm)) +apply (simp (no_asm_simp)) +done + +lemma drop_type [simp,TC]: "[| i:nat; l: list(A) |] ==> drop(i,l) : list(A)" +apply (induct_tac "i") +apply (simp_all (no_asm_simp) add: tl_type) +done + +declare drop_SUCC [simp del] + + +(** Type checking -- proved by induction, as usual **) + +lemma list_rec_type [TC]: + "[| l: list(A); + c: C(Nil); + !!x y r. [| x:A; y: list(A); r: C(y) |] ==> h(x,y,r): C(Cons(x,y)) + |] ==> list_rec(c,h,l) : C(l)" +by (induct_tac "l", auto) + +(** map **) + +lemma map_type [TC]: + "[| l: list(A); !!x. x: A ==> h(x): B |] ==> map(h,l) : list(B)" +apply (simp add: map_list_def) +apply (typecheck add: list.intros list_rec_type, blast) +done + +lemma map_type2 [TC]: "l: list(A) ==> map(h,l) : list({h(u). u:A})" +apply (erule map_type) +apply (erule RepFunI) +done + +(** length **) + +lemma length_type [TC]: "l: list(A) ==> length(l) : nat" +by (simp add: length_list_def) + +lemma lt_length_in_nat: + "[|x < length(xs); xs \ list(A)|] ==> x \ nat" +by (frule lt_nat_in_nat, typecheck) + +(** app **) + +lemma app_type [TC]: "[| xs: list(A); ys: list(A) |] ==> xs@ys : list(A)" +by (simp add: app_list_def) + +(** rev **) + +lemma rev_type [TC]: "xs: list(A) ==> rev(xs) : list(A)" +by (simp add: rev_list_def) + + +(** flat **) + +lemma flat_type [TC]: "ls: list(list(A)) ==> flat(ls) : list(A)" +by (simp add: flat_list_def) + + +(** set_of_list **) + +lemma set_of_list_type [TC]: "l: list(A) ==> set_of_list(l) : Pow(A)" +apply (unfold set_of_list_list_def) +apply (erule list_rec_type, auto) +done + +lemma set_of_list_append: + "xs: list(A) ==> set_of_list (xs@ys) = set_of_list(xs) Un set_of_list(ys)" +apply (erule list.induct) +apply (simp_all (no_asm_simp) add: Un_cons) +done + + +(** list_add **) + +lemma list_add_type [TC]: "xs: list(nat) ==> list_add(xs) : nat" +by (simp add: list_add_list_def) + + +(*** theorems about map ***) + +lemma map_ident [simp]: "l: list(A) ==> map(%u. u, l) = l" +apply (induct_tac "l") +apply (simp_all (no_asm_simp)) +done + +lemma map_compose: "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)" +apply (induct_tac "l") +apply (simp_all (no_asm_simp)) +done + +lemma map_app_distrib: "xs: list(A) ==> map(h, xs@ys) = map(h,xs) @ map(h,ys)" +apply (induct_tac "xs") +apply (simp_all (no_asm_simp)) +done + +lemma map_flat: "ls: list(list(A)) ==> map(h, flat(ls)) = flat(map(map(h),ls))" +apply (induct_tac "ls") +apply (simp_all (no_asm_simp) add: map_app_distrib) +done + +lemma list_rec_map: + "l: list(A) ==> + list_rec(c, d, map(h,l)) = + list_rec(c, %x xs r. d(h(x), map(h,xs), r), l)" +apply (induct_tac "l") +apply (simp_all (no_asm_simp)) +done + +(** theorems about list(Collect(A,P)) -- used in Induct/Term.thy **) + +(* c : list(Collect(B,P)) ==> c : list(B) *) +lemmas list_CollectD = Collect_subset [THEN list_mono, THEN subsetD, standard] + +lemma map_list_Collect: "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)" +apply (induct_tac "l") +apply (simp_all (no_asm_simp)) +done + +(*** theorems about length ***) + +lemma length_map [simp]: "xs: list(A) ==> length(map(h,xs)) = length(xs)" +apply (induct_tac "xs") +apply simp_all +done + +lemma length_app [simp]: + "[| xs: list(A); ys: list(A) |] + ==> length(xs@ys) = length(xs) #+ length(ys)" +apply (induct_tac "xs") +apply simp_all +done + +lemma length_rev [simp]: "xs: list(A) ==> length(rev(xs)) = length(xs)" +apply (induct_tac "xs") +apply (simp_all (no_asm_simp) add: length_app) +done + +lemma length_flat: + "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))" +apply (induct_tac "ls") +apply (simp_all (no_asm_simp) add: length_app) +done + +(** Length and drop **) + +(*Lemma for the inductive step of drop_length*) +lemma drop_length_Cons [rule_format]: + "xs: list(A) ==> + \x. EX z zs. drop(length(xs), Cons(x,xs)) = Cons(z,zs)" +apply (erule list.induct) +apply simp_all +done + +lemma drop_length [rule_format]: + "l: list(A) ==> \i \ length(l). (EX z zs. drop(i,l) = Cons(z,zs))" +apply (erule list.induct) +apply simp_all +apply safe +apply (erule drop_length_Cons) +apply (rule natE) +apply (erule Ord_trans [OF asm_rl length_type Ord_nat], assumption) +apply simp_all +apply (blast intro: succ_in_naturalD length_type) +done + + +(*** theorems about app ***) + +lemma app_right_Nil [simp]: "xs: list(A) ==> xs@Nil=xs" +apply (erule list.induct) +apply simp_all +done + +lemma app_assoc: "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)" +apply (induct_tac "xs") +apply simp_all +done + +lemma flat_app_distrib: "ls: list(list(A)) ==> flat(ls@ms) = flat(ls)@flat(ms)" +apply (induct_tac "ls") +apply (simp_all (no_asm_simp) add: app_assoc) +done + +(*** theorems about rev ***) + +lemma rev_map_distrib: "l: list(A) ==> rev(map(h,l)) = map(h,rev(l))" +apply (induct_tac "l") +apply (simp_all (no_asm_simp) add: map_app_distrib) +done + +(*Simplifier needs the premises as assumptions because rewriting will not + instantiate the variable ?A in the rules' typing conditions; note that + rev_type does not instantiate ?A. Only the premises do. +*) +lemma rev_app_distrib: + "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)" +apply (erule list.induct) +apply (simp_all add: app_assoc) +done + +lemma rev_rev_ident [simp]: "l: list(A) ==> rev(rev(l))=l" +apply (induct_tac "l") +apply (simp_all (no_asm_simp) add: rev_app_distrib) +done + +lemma rev_flat: "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))" +apply (induct_tac "ls") +apply (simp_all add: map_app_distrib flat_app_distrib rev_app_distrib) +done + + +(*** theorems about list_add ***) + +lemma list_add_app: + "[| xs: list(nat); ys: list(nat) |] + ==> list_add(xs@ys) = list_add(ys) #+ list_add(xs)" +apply (induct_tac "xs") +apply simp_all +done + +lemma list_add_rev: "l: list(nat) ==> list_add(rev(l)) = list_add(l)" +apply (induct_tac "l") +apply (simp_all (no_asm_simp) add: list_add_app) +done + +lemma list_add_flat: + "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))" +apply (induct_tac "ls") +apply (simp_all (no_asm_simp) add: list_add_app) +done + +(** New induction rule **) + + +lemma list_append_induct: + "[| l: list(A); + P(Nil); + !!x y. [| x: A; y: list(A); P(y) |] ==> P(y @ [x]) + |] ==> P(l)" +apply (subgoal_tac "P(rev(rev(l)))", simp) +apply (erule rev_type [THEN list.induct], simp_all) +done + + +(*** Thanks to Sidi Ehmety for these results about min, take, etc. ***) + +(** min FIXME: replace by Int! **) +(* Min theorems are also true for i, j ordinals *) +lemma min_sym: "[| i:nat; j:nat |] ==> min(i,j)=min(j,i)" +apply (unfold min_def) +apply (auto dest!: not_lt_imp_le dest: lt_not_sym intro: le_anti_sym) +done + +lemma min_type [simp,TC]: "[| i:nat; j:nat |] ==> min(i,j):nat" +by (unfold min_def, auto) + +lemma min_0 [simp]: "i:nat ==> min(0,i) = 0" +apply (unfold min_def) +apply (auto dest: not_lt_imp_le) +done + +lemma min_02 [simp]: "i:nat ==> min(i, 0) = 0" +apply (unfold min_def) +apply (auto dest: not_lt_imp_le) +done + +lemma lt_min_iff: "[| i:nat; j:nat; k:nat |] ==> i i min(succ(i), succ(j))= succ(min(i, j))" +apply (unfold min_def, auto) +done + +(*** more theorems about lists ***) + +(** filter **) + +lemma filter_append [simp]: + "xs:list(A) ==> filter(P, xs@ys) = filter(P, xs) @ filter(P, ys)" +by (induct_tac "xs", auto) + +lemma filter_type [simp,TC]: "xs:list(A) ==> filter(P, xs):list(A)" +by (induct_tac "xs", auto) + +lemma length_filter: "xs:list(A) ==> length(filter(P, xs)) le length(xs)" +apply (induct_tac "xs", auto) +apply (rule_tac j = "length (l) " in le_trans) +apply (auto simp add: le_iff) +done + +lemma filter_is_subset: "xs:list(A) ==> set_of_list(filter(P,xs)) <= set_of_list(xs)" +by (induct_tac "xs", auto) + +lemma filter_False [simp]: "xs:list(A) ==> filter(%p. False, xs) = Nil" +by (induct_tac "xs", auto) + +lemma filter_True [simp]: "xs:list(A) ==> filter(%p. True, xs) = xs" +by (induct_tac "xs", auto) + +(** length **) + +lemma length_is_0_iff [simp]: "xs:list(A) ==> length(xs)=0 <-> xs=Nil" +by (erule list.induct, auto) + +lemma length_is_0_iff2 [simp]: "xs:list(A) ==> 0 = length(xs) <-> xs=Nil" +by (erule list.induct, auto) + +lemma length_tl [simp]: "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1" +by (erule list.induct, auto) + +lemma length_greater_0_iff: "xs:list(A) ==> 0 xs ~= Nil" +by (erule list.induct, auto) + +lemma length_succ_iff: "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)" +by (erule list.induct, auto) + +(** more theorems about append **) + +lemma append_is_Nil_iff [simp]: + "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)" +by (erule list.induct, auto) + +lemma append_is_Nil_iff2 [simp]: + "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)" +by (erule list.induct, auto) + +lemma append_left_is_self_iff [simp]: + "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)" +by (erule list.induct, auto) + +lemma append_left_is_self_iff2 [simp]: + "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)" +by (erule list.induct, auto) + +(*TOO SLOW as a default simprule!*) +lemma append_left_is_Nil_iff [rule_format]: + "[| xs:list(A); ys:list(A); zs:list(A) |] ==> + length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))" +apply (erule list.induct) +apply (auto simp add: length_app) +done + +(*TOO SLOW as a default simprule!*) +lemma append_left_is_Nil_iff2 [rule_format]: + "[| xs:list(A); ys:list(A); zs:list(A) |] ==> + length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))" +apply (erule list.induct) +apply (auto simp add: length_app) +done + +lemma append_eq_append_iff [rule_format,simp]: + "xs:list(A) ==> \ys \ list(A). + length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)" +apply (erule list.induct) +apply (simp (no_asm_simp)) +apply clarify +apply (erule_tac a = "ys" in list.cases, auto) +done + +lemma append_eq_append [rule_format]: + "xs:list(A) ==> + \ys \ list(A). \us \ list(A). \vs \ list(A). + length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)" +apply (induct_tac "xs") +apply (force simp add: length_app, clarify) +apply (erule_tac a = "ys" in list.cases, simp) +apply (subgoal_tac "Cons (a, l) @ us =vs") + apply (drule rev_iffD1 [OF _ append_left_is_Nil_iff], simp_all) +apply blast +done + +lemma append_eq_append_iff2 [simp]: + "[| xs:list(A); ys:list(A); us:list(A); vs:list(A); length(us)=length(vs) |] + ==> xs@us = ys@vs <-> (xs=ys & us=vs)" +apply (rule iffI) +apply (rule append_eq_append, auto) +done + +lemma append_self_iff [simp]: + "[| xs:list(A); ys:list(A); zs:list(A) |] ==> xs@ys=xs@zs <-> ys=zs" +apply (simp (no_asm_simp)) +done + +lemma append_self_iff2 [simp]: + "[| xs:list(A); ys:list(A); zs:list(A) |] ==> ys@xs=zs@xs <-> ys=zs" +apply (simp (no_asm_simp)) +done + +(* Can also be proved from append_eq_append_iff2, +but the proof requires two more hypotheses: x:A and y:A *) +lemma append1_eq_iff [rule_format,simp]: + "xs:list(A) ==> \ys \ list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)" +apply (erule list.induct) + apply clarify + apply (erule list.cases) + apply simp_all +txt{*Inductive step*} +apply clarify +apply (erule_tac a = xa in list.cases, simp_all) +done + + +lemma append_right_is_self_iff [simp]: + "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)" +apply (simp (no_asm_simp) add: append_left_is_Nil_iff) +done + +lemma append_right_is_self_iff2 [simp]: + "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)" +apply (rule iffI) +apply (drule sym, auto) +done + +lemma hd_append [rule_format,simp]: + "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)" +by (induct_tac "xs", auto) + +lemma tl_append [rule_format,simp]: + "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys" +by (induct_tac "xs", auto) + +(** rev **) +lemma rev_is_Nil_iff [simp]: "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)" +by (erule list.induct, auto) + +lemma Nil_is_rev_iff [simp]: "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)" +by (erule list.induct, auto) + +lemma rev_is_rev_iff [rule_format,simp]: + "xs:list(A) ==> \ys \ list(A). rev(xs)=rev(ys) <-> xs=ys" +apply (erule list.induct, force) +apply clarify +apply (erule_tac a = "ys" in list.cases, auto) +done + +lemma rev_list_elim [rule_format]: + "xs:list(A) ==> + (xs=Nil --> P) --> (\ys \ list(A). \y \ A. xs =ys@[y] -->P)-->P" +apply (erule list_append_induct, auto) +done + + +(** more theorems about drop **) + +lemma length_drop [rule_format,simp]: + "n:nat ==> \xs \ list(A). length(drop(n, xs)) = length(xs) #- n" +apply (erule nat_induct) +apply (auto elim: list.cases) +done + +lemma drop_all [rule_format,simp]: + "n:nat ==> \xs \ list(A). length(xs) le n --> drop(n, xs)=Nil" +apply (erule nat_induct) +apply (auto elim: list.cases) +done + +lemma drop_append [rule_format]: + "n:nat ==> + \xs \ list(A). drop(n, xs@ys) = drop(n,xs) @ drop(n #- length(xs), ys)" +apply (induct_tac "n") +apply (auto elim: list.cases) +done + +lemma drop_drop: + "m:nat ==> \xs \ list(A). \n \ nat. drop(n, drop(m, xs))=drop(n #+ m, xs)" +apply (induct_tac "m") +apply (auto elim: list.cases) +done + +(** take **) + +lemma take_0 [simp]: "xs:list(A) ==> take(0, xs) = Nil" +apply (unfold take_def) +apply (erule list.induct, auto) +done + +lemma take_succ_Cons [simp]: + "n:nat ==> take(succ(n), Cons(a, xs)) = Cons(a, take(n, xs))" +by (simp add: take_def) + +(* Needed for proving take_all *) +lemma take_Nil [simp]: "n:nat ==> take(n, Nil) = Nil" +by (unfold take_def, auto) + +lemma take_all [rule_format,simp]: + "n:nat ==> \xs \ list(A). length(xs) le n --> take(n, xs) = xs" +apply (erule nat_induct) +apply (auto elim: list.cases) +done + +lemma take_type [rule_format,simp,TC]: + "xs:list(A) ==> \n \ nat. take(n, xs):list(A)" +apply (erule list.induct, simp) +apply clarify +apply (erule natE, auto) +done + +lemma take_append [rule_format,simp]: + "xs:list(A) ==> + \ys \ list(A). \n \ nat. take(n, xs @ ys) = + take(n, xs) @ take(n #- length(xs), ys)" +apply (erule list.induct, simp) +apply clarify +apply (erule natE, auto) +done + +lemma take_take [rule_format]: + "m : nat ==> + \xs \ list(A). \n \ nat. take(n, take(m,xs))= take(min(n, m), xs)" +apply (induct_tac "m", auto) +apply (erule_tac a = "xs" in list.cases) +apply (auto simp add: take_Nil) +apply (rotate_tac 1) +apply (erule natE) +apply (auto intro: take_0 take_type) +done + +(** nth **) + +lemma nth_0 [simp]: "nth(0, Cons(a, l))= a" +by (unfold nth_def, auto) + +lemma nth_Cons [simp]: "n:nat ==> nth(succ(n), Cons(a, l)) = nth(n, l)" +apply (unfold nth_def) +apply (simp (no_asm_simp)) +done + +lemma nth_type [rule_format,simp,TC]: + "xs:list(A) ==> \n \ nat. n < length(xs) --> nth(n, xs):A" +apply (erule list.induct, simp) +apply clarify +apply (erule natE, auto) +done + +lemma nth_append [rule_format]: + "xs:list(A) ==> + \n \ nat. nth(n, xs @ ys) = (if n < length(xs) then nth(n,xs) + else nth(n #- length(xs),ys))" +apply (induct_tac "xs", simp) +apply clarify +apply (erule natE, auto) +done + +lemma set_of_list_conv_nth: + "xs:list(A) + ==> set_of_list(xs) = {x:A. EX i:nat. i + \xs \ list(A). (\ys \ list(A). k le length(xs) --> k le length(ys) --> + (\i \ nat. i nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))" +apply (induct_tac "k") +apply (simp_all (no_asm_simp) add: lt_succ_eq_0_disj all_conj_distrib) +apply clarify +(*Both lists are non-empty*) +apply (erule_tac a="xa" in list.cases, simp) +apply (erule_tac a="xb" in list.cases, clarify) +apply (simp (no_asm_use) ) +apply clarify +apply (simp (no_asm_simp)) +apply (rule conjI, force) +apply (rename_tac y ys z zs) +apply (drule_tac x = "zs" and x1 = "ys" in bspec [THEN bspec], auto) +done + +lemma nth_equalityI [rule_format]: + "[| xs:list(A); ys:list(A); length(xs) = length(ys); + \i \ nat. i < length(xs) --> nth(i,xs) = nth(i,ys) |] + ==> xs = ys" +apply (subgoal_tac "length (xs) le length (ys) ") +apply (cut_tac k="length(xs)" and xs=xs and ys=ys in nth_take_lemma) +apply (simp_all add: take_all) +done + +(*The famous take-lemma*) + +lemma take_equalityI [rule_format]: + "[| xs:list(A); ys:list(A); (\i \ nat. take(i, xs) = take(i,ys)) |] + ==> xs = ys" +apply (case_tac "length (xs) le length (ys) ") +apply (drule_tac x = "length (ys) " in bspec) +apply (drule_tac [3] not_lt_imp_le) +apply (subgoal_tac [5] "length (ys) le length (xs) ") +apply (rule_tac [6] j = "succ (length (ys))" in le_trans) +apply (rule_tac [6] leI) +apply (drule_tac [5] x = "length (xs) " in bspec) +apply (simp_all add: take_all) +done + +lemma nth_drop [rule_format]: + "n:nat ==> \i \ nat. \xs \ list(A). n #+ i le length(xs) + --> nth(i, drop(n, xs)) = nth(n #+ i, xs)" +apply (induct_tac "n", simp_all) +apply clarify +apply (erule list.cases) +apply (auto elim!: ConsE) +done + +subsection{*The function zip*} + +text{*Crafty definition to eliminate a type argument*} + +consts + zip_aux :: "[i,i]=>i" + +primrec (*explicit lambda is required because both arguments of "un" vary*) + "zip_aux(B,[]) = + (\ys \ list(B). list_case([], %y l. [], ys))" + + "zip_aux(B,Cons(x,l)) = + (\ys \ list(B). + list_case(Nil, %y zs. Cons(, zip_aux(B,l)`zs), ys))" + +constdefs + zip :: "[i, i]=>i" + "zip(xs, ys) == zip_aux(set_of_list(ys),xs)`ys" + + +(* zip equations *) + +lemma list_on_set_of_list: "xs \ list(A) ==> xs \ list(set_of_list(xs))" +apply (induct_tac xs, simp_all) +apply (blast intro: list_mono [THEN subsetD]) +done + +lemma zip_Nil [simp]: "ys:list(A) ==> zip(Nil, ys)=Nil" +apply (simp add: zip_def list_on_set_of_list [of _ A]) +apply (erule list.cases, simp_all) +done + +lemma zip_Nil2 [simp]: "xs:list(A) ==> zip(xs, Nil)=Nil" +apply (simp add: zip_def list_on_set_of_list [of _ A]) +apply (erule list.cases, simp_all) +done + +lemma zip_aux_unique [rule_format]: + "[|B<=C; xs \ list(A)|] + ==> \ys \ list(B). zip_aux(C,xs) ` ys = zip_aux(B,xs) ` ys" +apply (induct_tac xs) + apply simp_all + apply (blast intro: list_mono [THEN subsetD], clarify) +apply (erule_tac a=x in list.cases , auto) +apply (blast intro: list_mono [THEN subsetD]) +done + +lemma zip_Cons_Cons [simp]: + "[| xs:list(A); ys:list(B); x:A; y:B |] ==> + zip(Cons(x,xs), Cons(y, ys)) = Cons(, zip(xs, ys))" +apply (simp add: zip_def, auto) +apply (rule zip_aux_unique, auto) +apply (simp add: list_on_set_of_list [of _ B]) +apply (blast intro: list_on_set_of_list list_mono [THEN subsetD]) +done + +lemma zip_type [rule_format,simp,TC]: + "xs:list(A) ==> \ys \ list(B). zip(xs, ys):list(A*B)" +apply (induct_tac "xs") +apply (simp (no_asm)) +apply clarify +apply (erule_tac a = "ys" in list.cases, auto) +done + +(* zip length *) +lemma length_zip [rule_format,simp]: + "xs:list(A) ==> \ys \ list(B). length(zip(xs,ys)) = + min(length(xs), length(ys))" +apply (unfold min_def) +apply (induct_tac "xs", simp_all) +apply clarify +apply (erule_tac a = "x" in list.cases, auto) +done + +lemma zip_append1 [rule_format]: + "[| ys:list(A); zs:list(B) |] ==> + \xs \ list(A). zip(xs @ ys, zs) = + zip(xs, take(length(xs), zs)) @ zip(ys, drop(length(xs),zs))" +apply (induct_tac "zs", force) +apply clarify +apply (erule_tac a = "xs" in list.cases, simp_all) +done + +lemma zip_append2 [rule_format]: + "[| xs:list(A); zs:list(B) |] ==> \ys \ list(B). zip(xs, ys@zs) = + zip(take(length(ys), xs), ys) @ zip(drop(length(ys), xs), zs)" +apply (induct_tac "xs", force) +apply clarify +apply (erule_tac a = "ys" in list.cases, auto) +done + +lemma zip_append [simp]: + "[| length(xs) = length(us); length(ys) = length(vs); + xs:list(A); us:list(B); ys:list(A); vs:list(B) |] + ==> zip(xs@ys,us@vs) = zip(xs, us) @ zip(ys, vs)" +by (simp (no_asm_simp) add: zip_append1 drop_append diff_self_eq_0) + + +lemma zip_rev [rule_format,simp]: + "ys:list(B) ==> \xs \ list(A). + length(xs) = length(ys) --> zip(rev(xs), rev(ys)) = rev(zip(xs, ys))" +apply (induct_tac "ys", force) +apply clarify +apply (erule_tac a = "xs" in list.cases) +apply (auto simp add: length_rev) +done + +lemma nth_zip [rule_format,simp]: + "ys:list(B) ==> \i \ nat. \xs \ list(A). + i < length(xs) --> i < length(ys) --> + nth(i,zip(xs, ys)) = " +apply (induct_tac "ys", force) +apply clarify +apply (erule_tac a = "xs" in list.cases, simp) +apply (auto elim: natE) +done + +lemma set_of_list_zip [rule_format]: + "[| xs:list(A); ys:list(B); i:nat |] + ==> set_of_list(zip(xs, ys)) = + {:A*B. EX i:nat. i < min(length(xs), length(ys)) + & x=nth(i, xs) & y=nth(i, ys)}" +by (force intro!: Collect_cong simp add: lt_min_iff set_of_list_conv_nth) + +(** list_update **) + +lemma list_update_Nil [simp]: "i:nat ==>list_update(Nil, i, v) = Nil" +by (unfold list_update_def, auto) + +lemma list_update_Cons_0 [simp]: "list_update(Cons(x, xs), 0, v)= Cons(v, xs)" +by (unfold list_update_def, auto) + +lemma list_update_Cons_succ [simp]: + "n:nat ==> + list_update(Cons(x, xs), succ(n), v)= Cons(x, list_update(xs, n, v))" +apply (unfold list_update_def, auto) +done + +lemma list_update_type [rule_format,simp,TC]: + "[| xs:list(A); v:A |] ==> \n \ nat. list_update(xs, n, v):list(A)" +apply (induct_tac "xs") +apply (simp (no_asm)) +apply clarify +apply (erule natE, auto) +done + +lemma length_list_update [rule_format,simp]: + "xs:list(A) ==> \i \ nat. length(list_update(xs, i, v))=length(xs)" +apply (induct_tac "xs") +apply (simp (no_asm)) +apply clarify +apply (erule natE, auto) +done + +lemma nth_list_update [rule_format]: + "[| xs:list(A) |] ==> \i \ nat. \j \ nat. i < length(xs) --> + nth(j, list_update(xs, i, x)) = (if i=j then x else nth(j, xs))" +apply (induct_tac "xs") + apply simp_all +apply clarify +apply (rename_tac i j) +apply (erule_tac n=i in natE) +apply (erule_tac [2] n=j in natE) +apply (erule_tac n=j in natE, simp_all, force) +done + +lemma nth_list_update_eq [simp]: + "[| i < length(xs); xs:list(A) |] ==> nth(i, list_update(xs, i,x)) = x" +by (simp (no_asm_simp) add: lt_length_in_nat nth_list_update) + + +lemma nth_list_update_neq [rule_format,simp]: + "xs:list(A) ==> \i \ nat. \j \ nat. i ~= j + --> nth(j, list_update(xs, i,x)) = nth(j, xs)" +apply (induct_tac "xs") + apply (simp (no_asm)) +apply clarify +apply (erule natE) +apply (erule_tac [2] natE, simp_all) +apply (erule natE, simp_all) +done + +lemma list_update_overwrite [rule_format,simp]: + "xs:list(A) ==> \i \ nat. i < length(xs) + --> list_update(list_update(xs, i, x), i, y) = list_update(xs, i,y)" +apply (induct_tac "xs") + apply (simp (no_asm)) +apply clarify +apply (erule natE, auto) +done + +lemma list_update_same_conv [rule_format]: + "xs:list(A) ==> \i \ nat. i < length(xs) --> + (list_update(xs, i, x) = xs) <-> (nth(i, xs) = x)" +apply (induct_tac "xs") + apply (simp (no_asm)) +apply clarify +apply (erule natE, auto) +done + +lemma update_zip [rule_format]: + "ys:list(B) ==> \i \ nat. \xy \ A*B. \xs \ list(A). + length(xs) = length(ys) --> + list_update(zip(xs, ys), i, xy) = zip(list_update(xs, i, fst(xy)), + list_update(ys, i, snd(xy)))" +apply (induct_tac "ys") + apply auto +apply (erule_tac a = "xc" in list.cases) +apply (auto elim: natE) +done + +lemma set_update_subset_cons [rule_format]: + "xs:list(A) ==> \i \ nat. set_of_list(list_update(xs, i, x)) + <= cons(x, set_of_list(xs))" +apply (induct_tac "xs") + apply simp +apply (rule ballI) +apply (erule natE, simp_all) +apply auto +done + +lemma set_of_list_update_subsetI: + "[| set_of_list(xs) <= A; xs:list(A); x:A; i:nat|] + ==> set_of_list(list_update(xs, i,x)) <= A" +apply (rule subset_trans) +apply (rule set_update_subset_cons, auto) +done + +(** upt **) + +lemma upt_rec: + "j:nat ==> upt(i,j) = (if i upt(i,j) = Nil" +apply (subst upt_rec, auto) +apply (auto simp add: le_iff) +apply (drule lt_asym [THEN notE], auto) +done + +(*Only needed if upt_Suc is deleted from the simpset*) +lemma upt_succ_append: + "[| i le j; j:nat |] ==> upt(i,succ(j)) = upt(i, j)@[j]" +by simp + +lemma upt_conv_Cons: + "[| i upt(i,j) = Cons(i,upt(succ(i),j))" +apply (rule trans) +apply (rule upt_rec, auto) +done + +lemma upt_type [simp,TC]: "j:nat ==> upt(i,j):list(nat)" +by (induct_tac "j", auto) + +(*LOOPS as a simprule, since j<=j*) +lemma upt_add_eq_append: + "[| i le j; j:nat; k:nat |] ==> upt(i, j #+k) = upt(i,j)@upt(j,j#+k)" +apply (induct_tac "k") +apply (auto simp add: app_assoc app_type) +apply (rule_tac j = "j" in le_trans, auto) +done + +lemma length_upt [simp]: "[| i:nat; j:nat |] ==>length(upt(i,j)) = j #- i" +apply (induct_tac "j") +apply (rule_tac [2] sym) +apply (auto dest!: not_lt_imp_le simp add: length_app diff_succ diff_is_0_iff) +done + +lemma nth_upt [rule_format,simp]: + "[| i:nat; j:nat; k:nat |] ==> i #+ k < j --> nth(k, upt(i,j)) = i #+ k" +apply (induct_tac "j") +apply (simp (no_asm_simp)) +apply (simp add: nth_append le_iff split add: nat_diff_split, safe) +apply (auto dest!: not_lt_imp_le simp add: nth_append diff_self_eq_0 + less_diff_conv add_commute) +apply (drule_tac j = "x" in lt_trans2, auto) +done + +lemma take_upt [rule_format,simp]: + "[| m:nat; n:nat |] ==> + \i \ nat. i #+ m le n --> take(m, upt(i,n)) = upt(i,i#+m)" +apply (induct_tac "m") +apply (simp (no_asm_simp) add: take_0) +apply clarify +apply (subst upt_rec, simp) +apply (rule sym) +apply (subst upt_rec, simp) +apply (simp_all del: upt.simps) +apply (rule_tac j = "succ (i #+ x) " in lt_trans2) +apply auto +done + +lemma map_succ_upt: + "[| m:nat; n:nat |] ==> map(succ, upt(m,n))= upt(succ(m), succ(n))" +apply (induct_tac "n") +apply (auto simp add: map_app_distrib) +done + +lemma nth_map [rule_format,simp]: + "xs:list(A) ==> + \n \ nat. n < length(xs) --> nth(n, map(f, xs)) = f(nth(n, xs))" +apply (induct_tac "xs", simp) +apply (rule ballI) +apply (induct_tac "n", auto) +done + +lemma nth_map_upt [rule_format]: + "[| m:nat; n:nat |] ==> + \i \ nat. i < n #- m --> nth(i, map(f, upt(m,n))) = f(m #+ i)" +apply (rule_tac n = "m" and m = "n" in diff_induct, typecheck) +apply simp +apply simp +apply (subst map_succ_upt [symmetric], simp_all) +apply clarify +apply (subgoal_tac "xa < length (upt (0, x))") + prefer 2 + apply (simp add: less_diff_conv) + apply (rule_tac j = "succ (xa #+ y) " in lt_trans2) + apply simp + apply simp +apply (subgoal_tac "xa < length (upt (y, x))") + apply (simp_all add: add_commute less_diff_conv) +done + +(** sublist (a generalization of nth to sets) **) + +constdefs + sublist :: "[i, i] => i" + "sublist(xs, A)== + map(fst, (filter(%p. snd(p): A, zip(xs, upt(0,length(xs))))))" + +lemma sublist_0 [simp]: "xs:list(A) ==>sublist(xs, 0) =Nil" +by (unfold sublist_def, auto) + +lemma sublist_Nil [simp]: "sublist(Nil, A) = Nil" +by (unfold sublist_def, auto) + +lemma sublist_shift_lemma: + "[| xs:list(B); i:nat |] ==> + map(fst, filter(%p. snd(p):A, zip(xs, upt(i,i #+ length(xs))))) = + map(fst, filter(%p. snd(p):nat & snd(p) #+ i:A, zip(xs,upt(0,length(xs)))))" +apply (erule list_append_induct) +apply (simp (no_asm_simp)) +apply (auto simp add: add_commute length_app filter_append map_app_distrib) +done + +lemma sublist_type [simp,TC]: + "xs:list(B) ==> sublist(xs, A):list(B)" +apply (unfold sublist_def) +apply (induct_tac "xs") +apply (auto simp add: filter_append map_app_distrib) +done + +lemma upt_add_eq_append2: + "[| i:nat; j:nat |] ==> upt(0, i #+ j) = upt(0, i) @ upt(i, i #+ j)" +by (simp add: upt_add_eq_append [of 0] nat_0_le) + +lemma sublist_append: + "[| xs:list(B); ys:list(B) |] ==> + sublist(xs@ys, A) = sublist(xs, A) @ sublist(ys, {j:nat. j #+ length(xs): A})" +apply (unfold sublist_def) +apply (erule_tac l = "ys" in list_append_induct) +apply (simp) +apply (simp (no_asm_simp) add: upt_add_eq_append2 app_assoc [symmetric]) +apply (auto simp add: sublist_shift_lemma length_type map_app_distrib app_assoc) +apply (simp_all add: add_commute) +done + + +lemma sublist_Cons: + "[| xs:list(B); x:B |] ==> + sublist(Cons(x, xs), A) = + (if 0:A then [x] else []) @ sublist(xs, {j:nat. succ(j) : A})" +apply (erule_tac l = "xs" in list_append_induct) +apply (simp (no_asm_simp) add: sublist_def) +apply (simp del: app_Cons add: app_Cons [symmetric] sublist_append, simp) +done + +lemma sublist_singleton [simp]: + "sublist([x], A) = (if 0 : A then [x] else [])" +by (simp (no_asm) add: sublist_Cons) + + +lemma sublist_upt_eq_take [simp]: + "[| xs:list(A); n:nat |] ==> sublist(xs, less_than(n)) = take(n,xs)" +apply (unfold less_than_def) +apply (erule_tac l = "xs" in list_append_induct, simp) +apply (simp split add: nat_diff_split add: sublist_append, auto) +apply (subgoal_tac "n #- length (y) = 0") +apply (simp (no_asm_simp)) +apply (auto dest!: not_lt_imp_le simp add: diff_is_0_iff) +done + +ML +{* +val ConsE = thm "ConsE"; +val Cons_iff = thm "Cons_iff"; +val Nil_Cons_iff = thm "Nil_Cons_iff"; +val list_unfold = thm "list_unfold"; +val list_mono = thm "list_mono"; +val list_univ = thm "list_univ"; +val list_subset_univ = thm "list_subset_univ"; +val list_into_univ = thm "list_into_univ"; +val list_case_type = thm "list_case_type"; +val tl_type = thm "tl_type"; +val drop_Nil = thm "drop_Nil"; +val drop_succ_Cons = thm "drop_succ_Cons"; +val drop_type = thm "drop_type"; +val list_rec_type = thm "list_rec_type"; +val map_type = thm "map_type"; +val map_type2 = thm "map_type2"; +val length_type = thm "length_type"; +val lt_length_in_nat = thm "lt_length_in_nat"; +val app_type = thm "app_type"; +val rev_type = thm "rev_type"; +val flat_type = thm "flat_type"; +val set_of_list_type = thm "set_of_list_type"; +val set_of_list_append = thm "set_of_list_append"; +val list_add_type = thm "list_add_type"; +val map_ident = thm "map_ident"; +val map_compose = thm "map_compose"; +val map_app_distrib = thm "map_app_distrib"; +val map_flat = thm "map_flat"; +val list_rec_map = thm "list_rec_map"; +val list_CollectD = thm "list_CollectD"; +val map_list_Collect = thm "map_list_Collect"; +val length_map = thm "length_map"; +val length_app = thm "length_app"; +val length_rev = thm "length_rev"; +val length_flat = thm "length_flat"; +val drop_length_Cons = thm "drop_length_Cons"; +val drop_length = thm "drop_length"; +val app_right_Nil = thm "app_right_Nil"; +val app_assoc = thm "app_assoc"; +val flat_app_distrib = thm "flat_app_distrib"; +val rev_map_distrib = thm "rev_map_distrib"; +val rev_app_distrib = thm "rev_app_distrib"; +val rev_rev_ident = thm "rev_rev_ident"; +val rev_flat = thm "rev_flat"; +val list_add_app = thm "list_add_app"; +val list_add_rev = thm "list_add_rev"; +val list_add_flat = thm "list_add_flat"; +val list_append_induct = thm "list_append_induct"; +val min_sym = thm "min_sym"; +val min_type = thm "min_type"; +val min_0 = thm "min_0"; +val min_02 = thm "min_02"; +val lt_min_iff = thm "lt_min_iff"; +val min_succ_succ = thm "min_succ_succ"; +val filter_append = thm "filter_append"; +val filter_type = thm "filter_type"; +val length_filter = thm "length_filter"; +val filter_is_subset = thm "filter_is_subset"; +val filter_False = thm "filter_False"; +val filter_True = thm "filter_True"; +val length_is_0_iff = thm "length_is_0_iff"; +val length_is_0_iff2 = thm "length_is_0_iff2"; +val length_tl = thm "length_tl"; +val length_greater_0_iff = thm "length_greater_0_iff"; +val length_succ_iff = thm "length_succ_iff"; +val append_is_Nil_iff = thm "append_is_Nil_iff"; +val append_is_Nil_iff2 = thm "append_is_Nil_iff2"; +val append_left_is_self_iff = thm "append_left_is_self_iff"; +val append_left_is_self_iff2 = thm "append_left_is_self_iff2"; +val append_left_is_Nil_iff = thm "append_left_is_Nil_iff"; +val append_left_is_Nil_iff2 = thm "append_left_is_Nil_iff2"; +val append_eq_append_iff = thm "append_eq_append_iff"; +val append_eq_append = thm "append_eq_append"; +val append_eq_append_iff2 = thm "append_eq_append_iff2"; +val append_self_iff = thm "append_self_iff"; +val append_self_iff2 = thm "append_self_iff2"; +val append1_eq_iff = thm "append1_eq_iff"; +val append_right_is_self_iff = thm "append_right_is_self_iff"; +val append_right_is_self_iff2 = thm "append_right_is_self_iff2"; +val hd_append = thm "hd_append"; +val tl_append = thm "tl_append"; +val rev_is_Nil_iff = thm "rev_is_Nil_iff"; +val Nil_is_rev_iff = thm "Nil_is_rev_iff"; +val rev_is_rev_iff = thm "rev_is_rev_iff"; +val rev_list_elim = thm "rev_list_elim"; +val length_drop = thm "length_drop"; +val drop_all = thm "drop_all"; +val drop_append = thm "drop_append"; +val drop_drop = thm "drop_drop"; +val take_0 = thm "take_0"; +val take_succ_Cons = thm "take_succ_Cons"; +val take_Nil = thm "take_Nil"; +val take_all = thm "take_all"; +val take_type = thm "take_type"; +val take_append = thm "take_append"; +val take_take = thm "take_take"; +val nth_0 = thm "nth_0"; +val nth_Cons = thm "nth_Cons"; +val nth_type = thm "nth_type"; +val nth_append = thm "nth_append"; +val set_of_list_conv_nth = thm "set_of_list_conv_nth"; +val nth_take_lemma = thm "nth_take_lemma"; +val nth_equalityI = thm "nth_equalityI"; +val take_equalityI = thm "take_equalityI"; +val nth_drop = thm "nth_drop"; +val list_on_set_of_list = thm "list_on_set_of_list"; +val zip_Nil = thm "zip_Nil"; +val zip_Nil2 = thm "zip_Nil2"; +val zip_Cons_Cons = thm "zip_Cons_Cons"; +val zip_type = thm "zip_type"; +val length_zip = thm "length_zip"; +val zip_append1 = thm "zip_append1"; +val zip_append2 = thm "zip_append2"; +val zip_append = thm "zip_append"; +val zip_rev = thm "zip_rev"; +val nth_zip = thm "nth_zip"; +val set_of_list_zip = thm "set_of_list_zip"; +val list_update_Nil = thm "list_update_Nil"; +val list_update_Cons_0 = thm "list_update_Cons_0"; +val list_update_Cons_succ = thm "list_update_Cons_succ"; +val list_update_type = thm "list_update_type"; +val length_list_update = thm "length_list_update"; +val nth_list_update = thm "nth_list_update"; +val nth_list_update_eq = thm "nth_list_update_eq"; +val nth_list_update_neq = thm "nth_list_update_neq"; +val list_update_overwrite = thm "list_update_overwrite"; +val list_update_same_conv = thm "list_update_same_conv"; +val update_zip = thm "update_zip"; +val set_update_subset_cons = thm "set_update_subset_cons"; +val set_of_list_update_subsetI = thm "set_of_list_update_subsetI"; +val upt_rec = thm "upt_rec"; +val upt_conv_Nil = thm "upt_conv_Nil"; +val upt_succ_append = thm "upt_succ_append"; +val upt_conv_Cons = thm "upt_conv_Cons"; +val upt_type = thm "upt_type"; +val upt_add_eq_append = thm "upt_add_eq_append"; +val length_upt = thm "length_upt"; +val nth_upt = thm "nth_upt"; +val take_upt = thm "take_upt"; +val map_succ_upt = thm "map_succ_upt"; +val nth_map = thm "nth_map"; +val nth_map_upt = thm "nth_map_upt"; +val sublist_0 = thm "sublist_0"; +val sublist_Nil = thm "sublist_Nil"; +val sublist_shift_lemma = thm "sublist_shift_lemma"; +val sublist_type = thm "sublist_type"; +val upt_add_eq_append2 = thm "upt_add_eq_append2"; +val sublist_append = thm "sublist_append"; +val sublist_Cons = thm "sublist_Cons"; +val sublist_singleton = thm "sublist_singleton"; +val sublist_upt_eq_take = thm "sublist_upt_eq_take"; + +structure list = +struct +val induct = thm "list.induct" +val elim = thm "list.cases" +val intrs = thms "list.intros" +end; +*} + end