--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/GenPrefix.ML Thu Nov 15 16:46:38 2001 +0100
@@ -0,0 +1,617 @@
+(* Title: ZF/UNITY/GenPrefix.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Charpentier's Generalized Prefix Relation
+ <xs,ys>:gen_prefix(r)
+ if ys = xs' @ zs where length(xs) = length(xs')
+ and corresponding elements of xs, xs' are pairwise related by r
+
+Based on Lex/Prefix
+*)
+
+Goalw [refl_def]
+ "[| refl(A, r); x:A |] ==> <x,x>:r";
+by Auto_tac;
+qed "reflD";
+
+(*** preliminary lemmas ***)
+
+Goal "xs:list(A) ==> <[], xs>:gen_prefix(A, r)";
+by (dtac (rotate_prems 1 gen_prefix.append) 1);
+by (rtac gen_prefix.Nil 1);
+by Auto_tac;
+qed "Nil_gen_prefix";
+Addsimps [Nil_gen_prefix];
+
+
+Goal "<xs,ys>:gen_prefix(A, r) ==> length(xs) le length(ys)";
+by (etac gen_prefix.induct 1);
+by (subgoal_tac "ys:list(A)" 3);
+by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]
+ addIs [le_trans],
+ simpset() addsimps [length_app]));
+qed "gen_prefix_length_le";
+
+
+Goal "[| <xs', ys'>:gen_prefix(A, r) |] \
+\ ==> (ALL x xs. x:A --> xs'= Cons(x,xs) --> \
+\ (EX y ys. y:A & ys' = Cons(y,ys) &\
+\ <x,y>:r & <xs, ys>:gen_prefix(A, r)))";
+by (etac gen_prefix.induct 1);
+by (force_tac (claset() addIs [gen_prefix.append],
+ simpset()) 3);
+by (REPEAT(Asm_simp_tac 1));
+val lemma = result();
+
+(*As usual converting it to an elimination rule is tiresome*)
+val major::prems =
+Goal "[| <Cons(x,xs), zs>:gen_prefix(A, r); \
+\ !!y ys. [|zs = Cons(y, ys); y:A; x:A; <x,y>:r; \
+\ <xs,ys>:gen_prefix(A, r) |] ==> P \
+\ |] ==> P";
+by (cut_facts_tac [major] 1);
+by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
+by (Clarify_tac 1);
+by (etac ConsE 1);
+by (cut_facts_tac [major RS lemma] 1);
+by (Full_simp_tac 1);
+by (dtac mp 1);
+by (Asm_simp_tac 1);
+by (REPEAT (eresolve_tac [exE, conjE] 1));
+by (REPEAT (ares_tac prems 1));
+qed "Cons_gen_prefixE";
+AddSEs [Cons_gen_prefixE];
+
+Goal
+"(<Cons(x,xs),Cons(y,ys)>:gen_prefix(A, r)) \
+\ <-> (x:A & y:A & <x,y>:r & <xs,ys>:gen_prefix(A, r))";
+by (auto_tac (claset() addIs [gen_prefix.prepend], simpset()));
+qed"Cons_gen_prefix_Cons";
+AddIffs [Cons_gen_prefix_Cons];
+
+(** Monotonicity of gen_prefix **)
+
+Goal "r<=s ==> gen_prefix(A, r) <= gen_prefix(A, s)";
+by (Clarify_tac 1);
+by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
+by (Clarify_tac 1);
+by (etac rev_mp 1);
+by (etac gen_prefix.induct 1);
+by (auto_tac (claset() addIs
+ [gen_prefix.append], simpset()));
+qed "gen_prefix_mono2";
+
+Goal "A<=B ==>gen_prefix(A, r) <= gen_prefix(B, r)";
+by (Clarify_tac 1);
+by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
+by (Clarify_tac 1);
+by (etac rev_mp 1);
+by (eres_inst_tac [("P", "y:list(A)")] rev_mp 1);
+by (eres_inst_tac [("P", "xa:list(A)")] rev_mp 1);
+by (etac gen_prefix.induct 1);
+by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (REPEAT(etac ConsE 1));
+by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]
+ addIs [gen_prefix.append, list_mono RS subsetD],
+ simpset()));
+qed "gen_prefix_mono1";
+
+Goal "[| A <= B; r <= s |] ==> gen_prefix(A, r) <= gen_prefix(B, s)";
+by (rtac subset_trans 1);
+by (rtac gen_prefix_mono1 1);
+by (rtac gen_prefix_mono2 2);
+by Auto_tac;
+qed "gen_prefix_mono";
+
+(*** gen_prefix order ***)
+
+(* reflexivity *)
+Goalw [refl_def] "refl(A, r) ==> refl(list(A), gen_prefix(A, r))";
+by Auto_tac;
+by (induct_tac "x" 1);
+by Auto_tac;
+qed "refl_gen_prefix";
+Addsimps [refl_gen_prefix RS reflD];
+
+(* Transitivity *)
+(* A lemma for proving gen_prefix_trans_comp *)
+
+Goal "xs:list(A) ==> \
+\ ALL zs. <xs @ ys, zs>:gen_prefix(A, r) --> <xs, zs>: gen_prefix(A, r)";
+by (etac list.induct 1);
+by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset()));
+qed_spec_mp "append_gen_prefix";
+
+(* Lemma proving transitivity and more*)
+
+Goal "<x, y>: gen_prefix(A, r) ==> \
+\ (ALL z:list(A). <y,z>:gen_prefix(A, s)--><x, z>:gen_prefix(A, s O r))";
+by (etac gen_prefix.induct 1);
+by (auto_tac (claset() addEs [ConsE], simpset() addsimps [Nil_gen_prefix]));
+by (subgoal_tac "ys:list(A)" 1);
+by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2);
+by (dres_inst_tac [("xs", "ys"), ("r", "s")] append_gen_prefix 1);
+by Auto_tac;
+qed_spec_mp "gen_prefix_trans_comp";
+
+Goal "trans(r) ==> r O r <= r";
+by (auto_tac (claset() addDs [transD], simpset()));
+qed "trans_comp_subset";
+
+Goal "trans(r) ==> trans(gen_prefix(A,r))";
+by (simp_tac (simpset() addsimps [trans_def]) 1);
+by (Clarify_tac 1);
+by (rtac (impOfSubs (trans_comp_subset RS gen_prefix_mono2)) 1);
+ by (assume_tac 2);
+by (rtac gen_prefix_trans_comp 1);
+by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset()));
+qed_spec_mp "trans_gen_prefix";
+
+Goal
+ "trans(r) ==> trans[list(A)](gen_prefix(A, r))";
+by (dres_inst_tac [("A", "A")] trans_gen_prefix 1);
+by (rewrite_goal_tac [trans_def, trans_on_def] 1);
+by (Blast_tac 1);
+qed "trans_on_gen_prefix";
+
+Goalw [prefix_def]
+"[| <x,y>:prefix(A); <y, z>:gen_prefix(A, r); r<=A*A |] \
+\ ==> <x, z>:gen_prefix(A, r)";
+by (res_inst_tac [("P", "%r. <x,z>:gen_prefix(A, r)")]
+ (right_comp_id RS subst) 1);
+by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp,
+ gen_prefix.dom_subset RS subsetD]) 1));
+qed_spec_mp "prefix_gen_prefix_trans";
+
+
+Goalw [prefix_def]
+"[| <x,y>:gen_prefix(A,r); <y, z>:prefix(A); r<=A*A |] \
+\ ==> <x, z>:gen_prefix(A, r)";
+by (res_inst_tac [("P", "%r. <x,z>:gen_prefix(A, r)")] (left_comp_id RS subst) 1);
+by (REPEAT(blast_tac (claset() addDs [gen_prefix_trans_comp,
+ gen_prefix.dom_subset RS subsetD]) 1));
+qed_spec_mp "gen_prefix_prefix_trans";
+
+(** Antisymmetry **)
+
+Goal "n:nat ==> ALL b:nat. n #+ b le n --> b = 0";
+by (induct_tac "n" 1);
+by Auto_tac;
+qed_spec_mp "nat_le_lemma";
+
+Goal "antisym(r) ==> antisym(gen_prefix(A, r))";
+by (simp_tac (simpset() addsimps [antisym_def]) 1);
+by (rtac (impI RS allI RS allI) 1);
+by (etac gen_prefix.induct 1);
+by (full_simp_tac (simpset() addsimps [antisym_def]) 2);
+by (Blast_tac 2);
+by (Blast_tac 1);
+(*append case is hardest*)
+by (Clarify_tac 1);
+by (subgoal_tac "length(zs) = 0" 1);
+by (subgoal_tac "ys:list(A)" 1);
+by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 2);
+by (dres_inst_tac [("psi", "<ys @ zs, xs>:gen_prefix(A,r)")] asm_rl 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "length(ys @ zs) = length(ys) #+ length(zs) &ys:list(A)&xs:list(A)" 1);
+by (blast_tac (claset() addIs [length_app]
+ addDs [gen_prefix.dom_subset RS subsetD]) 2);
+by (REPEAT (dtac gen_prefix_length_le 1));
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("j", "length(xs)")] le_trans 1);
+by (Blast_tac 1);
+by (auto_tac (claset() addIs [nat_le_lemma], simpset()));
+qed_spec_mp "antisym_gen_prefix";
+
+(*** recursion equations ***)
+
+Goal "xs:list(A) ==> <xs, []>:gen_prefix(A,r) <-> (xs = [])";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "gen_prefix_Nil";
+Addsimps [gen_prefix_Nil];
+
+Goalw [refl_def]
+ "[| refl(A, r); xs:list(A) |] ==> \
+\ <xs@ys, xs@zs>: gen_prefix(A, r) <-> <ys,zs>:gen_prefix(A, r)";
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "same_gen_prefix_gen_prefix";
+Addsimps [same_gen_prefix_gen_prefix];
+
+Goal "[| xs:list(A); ys:list(A); y:A |] ==> \
+\ <xs, Cons(y,ys)> : gen_prefix(A,r) <-> \
+\ (xs=[] | (EX z zs. xs=Cons(z,zs) & z:A & <z,y>:r & <zs,ys>:gen_prefix(A,r)))";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed "gen_prefix_Cons";
+
+Goal "[| refl(A,r); <xs,ys>:gen_prefix(A, r); zs:list(A) |] \
+\ ==> <xs@zs, take(length(xs), ys) @ zs> : gen_prefix(A, r)";
+by (etac gen_prefix.induct 1);
+by (Asm_simp_tac 1);
+by (ALLGOALS(forward_tac [gen_prefix.dom_subset RS subsetD]));
+by Auto_tac;
+by (ftac gen_prefix_length_le 1);
+by (subgoal_tac "take(length(xs), ys):list(A)" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps
+ [diff_is_0_iff RS iffD2, take_type ])));
+qed "gen_prefix_take_append";
+
+Goal "[| refl(A, r); <xs,ys>:gen_prefix(A,r); \
+\ length(xs) = length(ys); zs:list(A) |] \
+\ ==> <xs@zs, ys @ zs> : gen_prefix(A, r)";
+by (dres_inst_tac [("zs", "zs")] gen_prefix_take_append 1);
+by (REPEAT(assume_tac 1));
+by (subgoal_tac "take(length(xs), ys)=ys" 1);
+by (auto_tac (claset() addSIs [take_all]
+ addDs [gen_prefix.dom_subset RS subsetD],
+ simpset()));
+qed "gen_prefix_append_both";
+
+(*NOT suitable for rewriting since [y] has the form y#ys*)
+Goal "xs:list(A) ==> xs @ Cons(y, ys) = (xs @ [y]) @ ys";
+by (auto_tac (claset(), simpset() addsimps [app_assoc]));
+qed "append_cons_conv";
+
+Goal "[| <xs,ys>:gen_prefix(A, r); refl(A, r) |] \
+\ ==> length(xs) < length(ys) --> \
+\ <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)";
+by (etac gen_prefix.induct 1);
+by (Blast_tac 1);
+by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
+by (Clarify_tac 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [length_type])));
+(* Append case is hardest *)
+by (forward_tac [gen_prefix_length_le RS (le_iff RS iffD1) ] 1);
+by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
+by (Clarify_tac 1);
+by (subgoal_tac "length(xs):nat&length(ys):nat &length(zs):nat" 1);
+by (blast_tac (claset() addIs [length_type]) 2);
+by (Clarify_tac 1);
+by (ALLGOALS (asm_full_simp_tac (simpset()
+ addsimps [nth_append, length_type, length_app])));
+by (Clarify_tac 1);
+by (rtac conjI 1);
+by (blast_tac (claset() addIs [gen_prefix.append]) 1);
+by (thin_tac "length(xs) < length(ys) -->?u" 1);
+by (case_tac "zs=[]" 1);
+by (auto_tac (claset(), simpset() addsimps [neq_Nil_iff]));
+by (res_inst_tac [("P1", "%x. <?u(x), ?v>:?w")] (nat_diff_split RS iffD2) 1);
+by Auto_tac;
+by (stac append_cons_conv 1);
+by (rtac gen_prefix.append 2);
+by (auto_tac (claset() addEs [ConsE],
+ simpset() addsimps [gen_prefix_append_both]));
+val lemma = result() RS mp;
+
+Goal "[| <xs,ys>: gen_prefix(A, r); length(xs) < length(ys); refl(A, r) |] \
+\ ==> <xs @ [nth(length(xs), ys)], ys>:gen_prefix(A, r)";
+by (blast_tac (claset() addIs [lemma]) 1);
+qed "append_one_gen_prefix";
+
+
+(** Proving the equivalence with Charpentier's definition **)
+
+Goal "xs:list(A) ==> \
+\ ALL ys:list(A). ALL i:nat. i < length(xs) \
+\ --> <xs, ys>: gen_prefix(A, r) --> <nth(i, xs), nth(i, ys)>:r";
+by (induct_tac "xs" 1);
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(Asm_full_simp_tac));
+by (etac natE 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (dres_inst_tac [("x", "ysa")] bspec 1);
+by (dres_inst_tac [("x", "x")] bspec 2);
+by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD], simpset()));
+qed_spec_mp "gen_prefix_imp_nth";
+
+Goal "xs:list(A) ==> \
+\ ALL ys:list(A). length(xs) le length(ys) \
+\ --> (ALL i:nat. i < length(xs)--> <nth(i, xs), nth(i,ys)>:r) \
+\ --> <xs, ys> : gen_prefix(A, r)";
+by (induct_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_succ_eq_0_disj])));
+by (Clarify_tac 1);
+by (case_tac "x=[]" 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
+by (Clarify_tac 1);
+by (dres_inst_tac [("x", "ys")] bspec 1);
+by (ALLGOALS(Clarify_tac));
+by Auto_tac;
+qed_spec_mp "nth_imp_gen_prefix";
+
+Goal "(<xs,ys>: gen_prefix(A,r)) <-> \
+\ (xs:list(A) & ys:list(A) & length(xs) le length(ys) & \
+\ (ALL i:nat. i < length(xs) --> <nth(i,xs), nth(i, ys)>: r))";
+by (rtac iffI 1);
+by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
+by (forward_tac [gen_prefix_length_le] 1);
+by (ALLGOALS(Clarify_tac));
+by (rtac nth_imp_gen_prefix 2);
+by (dtac (rotate_prems 4 gen_prefix_imp_nth) 1);
+by Auto_tac;
+qed "gen_prefix_iff_nth";
+
+(** prefix is a partial order: **)
+
+Goalw [prefix_def]
+ "refl(list(A), prefix(A))";
+by (rtac refl_gen_prefix 1);
+by (auto_tac (claset(), simpset() addsimps [refl_def]));
+qed "refl_prefix";
+Addsimps [refl_prefix RS reflD];
+
+Goalw [prefix_def] "trans(prefix(A))";
+by (rtac trans_gen_prefix 1);
+by (auto_tac (claset(), simpset() addsimps [trans_def]));
+qed "trans_prefix";
+
+bind_thm("prefix_trans", trans_prefix RS transD);
+
+Goalw [prefix_def] "trans[list(A)](prefix(A))";
+by (rtac trans_on_gen_prefix 1);
+by (auto_tac (claset(), simpset() addsimps [trans_def]));
+qed "trans_on_prefix";
+
+bind_thm("prefix_trans_on", trans_on_prefix RS trans_onD);
+
+(* Monotonicity of "set" operator WRT prefix *)
+
+Goalw [prefix_def]
+"<xs,ys>:prefix(A) ==> set_of_list(xs) <= set_of_list(ys)";
+by (etac gen_prefix.induct 1);
+by (subgoal_tac "xs:list(A)&ys:list(A)" 3);
+by (blast_tac (claset() addDs [gen_prefix.dom_subset RS subsetD]) 4);
+by (auto_tac (claset(), simpset() addsimps [set_of_list_append]));
+qed "set_of_list_prefix_mono";
+
+(** recursion equations **)
+
+Goalw [prefix_def] "xs:list(A) ==> <[],xs>:prefix(A)";
+by (asm_simp_tac (simpset() addsimps [Nil_gen_prefix]) 1);
+qed "Nil_prefix";
+Addsimps[Nil_prefix];
+
+
+Goalw [prefix_def] "<xs, []>:prefix(A) <-> (xs = [])";
+by Auto_tac;
+by (forward_tac [gen_prefix.dom_subset RS subsetD] 1);
+by (dres_inst_tac [("psi", "<xs, []>:gen_prefix(A, id(A))")] asm_rl 1);
+by (asm_full_simp_tac (simpset() addsimps [gen_prefix_Nil]) 1);
+qed "prefix_Nil";
+AddIffs [prefix_Nil];
+
+Goalw [prefix_def]
+"<Cons(x,xs), Cons(y,ys)>:prefix(A) <-> (x=y & <xs,ys>:prefix(A) & y:A)";
+by Auto_tac;
+qed"Cons_prefix_Cons";
+AddIffs [Cons_prefix_Cons];
+
+Goalw [prefix_def]
+"xs:list(A)==> <xs@ys,xs@zs>:prefix(A) <-> (<ys,zs>:prefix(A))";
+by (subgoal_tac "refl(A,id(A))" 1);
+by (Asm_simp_tac 1);
+by (auto_tac (claset(), simpset() addsimps[refl_def]));
+qed "same_prefix_prefix";
+Addsimps [same_prefix_prefix];
+
+Goal "xs:list(A) ==> <xs@ys,xs>:prefix(A) <-> (<ys,[]>:prefix(A))";
+by (res_inst_tac [("P", "%x. <?u, x>:?v <-> ?w(x)")] (app_right_Nil RS subst) 1);
+by (rtac same_prefix_prefix 2);
+by Auto_tac;
+qed "same_prefix_prefix_Nil";
+Addsimps [same_prefix_prefix_Nil];
+
+Goalw [prefix_def]
+"[| <xs,ys>:prefix(A); zs:list(A) |] ==> <xs,ys@zs>:prefix(A)";
+by (etac gen_prefix.append 1);
+by (assume_tac 1);
+qed "prefix_appendI";
+Addsimps [prefix_appendI];
+
+Goalw [prefix_def]
+"[| xs:list(A); ys:list(A); y:A |] ==> \
+\ <xs,Cons(y,ys)>:prefix(A) <-> \
+\ (xs=[] | (EX zs. xs=Cons(y,zs) & <zs,ys>:prefix(A)))";
+by (auto_tac (claset(), simpset() addsimps [gen_prefix_Cons]));
+qed "prefix_Cons";
+
+Goalw [prefix_def]
+ "[| <xs,ys>:prefix(A); length(xs) < length(ys) |] \
+\ ==> <xs @ [nth(length(xs),ys)], ys>:prefix(A)";
+by (subgoal_tac "refl(A, id(A))" 1);
+by (asm_simp_tac (simpset() addsimps [append_one_gen_prefix]) 1);
+by (auto_tac (claset(), simpset() addsimps [refl_def]));
+qed "append_one_prefix";
+
+Goalw [prefix_def]
+"<xs,ys>:prefix(A) ==> length(xs) le length(ys)";
+by (blast_tac (claset() addDs [gen_prefix_length_le]) 1);
+qed "prefix_length_le";
+
+Goalw [prefix_def]
+"<xs,ys>:prefix(A) ==> xs~=ys --> length(xs) < length(ys)";
+by (etac gen_prefix.induct 1);
+by (Clarify_tac 1);
+by (ALLGOALS(subgoal_tac "ys:list(A)&xs:list(A)"));
+by (auto_tac (claset() addDs [gen_prefix.dom_subset RS subsetD],
+ simpset() addsimps [length_app, length_type]));
+by (subgoal_tac "length(zs)=0" 1);
+by (dtac not_lt_imp_le 2);
+by (res_inst_tac [("j", "length(ys)")] lt_trans2 5);
+by Auto_tac;
+val lemma = result();
+
+Goalw [prefix_def]
+"prefix(A)<=list(A)*list(A)";
+by (blast_tac (claset() addSIs [gen_prefix.dom_subset]) 1);
+qed "prefix_type";
+
+Goalw [strict_prefix_def]
+"strict_prefix(A) <= list(A)*list(A)";
+by (blast_tac (claset() addSIs [prefix_type RS subsetD]) 1);
+qed "strict_prefix_type";
+
+Goalw [strict_prefix_def]
+ "<xs,ys>:strict_prefix(A) ==> length(xs) < length(ys)";
+by (resolve_tac [lemma RS mp] 1);
+by (auto_tac (claset() addDs [prefix_type RS subsetD], simpset()));
+qed "strict_prefix_length_lt";
+
+(*Equivalence to the definition used in Lex/Prefix.thy*)
+Goalw [prefix_def]
+"<xs,zs>:prefix(A) <-> (EX ys:list(A). zs = xs@ys) & xs:list(A)";
+by (auto_tac (claset(),
+ simpset() addsimps [gen_prefix_iff_nth,
+ nth_append, nth_type, app_type, length_app]));
+by (subgoal_tac "length(xs):nat&length(zs):nat & \
+\ drop(length(xs), zs):list(A)" 1);
+by (res_inst_tac [("x", "drop(length(xs), zs)")] bexI 1);
+by (ALLGOALS(Clarify_tac));
+by (asm_simp_tac (simpset() addsimps [length_type, drop_type]) 2);
+by (rtac nth_equalityI 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps
+ [nth_append, app_type, drop_type, length_app, length_drop])));
+by (rtac (nat_diff_split RS iffD2) 1);
+by (ALLGOALS(Asm_full_simp_tac));
+by (Clarify_tac 1);
+by (dres_inst_tac [("i", "length(zs)")] leI 1);
+by (force_tac (claset(), simpset() addsimps [le_subset_iff]) 1);
+by Safe_tac;
+by (Blast_tac 1);
+by (subgoal_tac "length(xs) #+ (x #- length(xs)) = x" 1);
+by (rtac (nth_drop RS ssubst) 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [leI])));
+by (rtac (nat_diff_split RS iffD2) 1);
+by Auto_tac;
+qed "prefix_iff";
+
+Goal
+"[|xs:list(A); ys:list(A); y:A |] ==> \
+\ <xs, ys@[y]>:prefix(A) <-> (xs = ys@[y] | <xs,ys>:prefix(A))";
+by (simp_tac (simpset() addsimps [prefix_iff]) 1);
+by (rtac iffI 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("xs", "ysa")] rev_list_elim 1);
+by (Asm_full_simp_tac 1);
+by (dres_inst_tac [("psi", "ya:list(A)")] asm_rl 1);
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [app_type, app_assoc RS sym] delsimps [app_assoc]) 1);
+by (auto_tac (claset(), simpset() addsimps [app_assoc, app_type]));
+qed "prefix_snoc";
+Addsimps [prefix_snoc];
+
+
+Goal "zs:list(A) ==> ALL xs:list(A). ALL ys:list(A). \
+\ (<xs, ys@zs>:prefix(A)) <-> \
+\ (<xs,ys>:prefix(A) | (EX us. xs = ys@us & <us,zs>:prefix(A)))";
+by (etac list_append_induct 1);
+by (Clarify_tac 2);
+by (rtac iffI 2);
+by (asm_full_simp_tac (simpset() delsimps [app_assoc]
+ addsimps [app_assoc RS sym]) 2);
+by (etac disjE 2 THEN etac disjE 3);
+by (rtac disjI2 2);
+by (res_inst_tac [("x", "y @ [x]")] exI 2);
+by (asm_full_simp_tac (simpset() delsimps [app_assoc]
+ addsimps [app_assoc RS sym]) 2);
+by (REPEAT(Force_tac 1));
+qed_spec_mp "prefix_append_iff";
+
+
+(*Although the prefix ordering is not linear, the prefixes of a list
+ are linearly ordered.*)
+Goal "[| zs:list(A); xs:list(A); ys:list(A) |] \
+\ ==> <xs, zs>:prefix(A) --> <ys,zs>:prefix(A) \
+\ --><xs,ys>:prefix(A) | <ys,xs>:prefix(A)";
+by (etac list_append_induct 1);
+by Auto_tac;
+qed_spec_mp "common_prefix_linear";
+
+
+(*** pfixLe, pfixGe: properties inherited from the translations ***)
+
+
+
+(** pfixLe **)
+
+Goalw [refl_def, Le_def] "refl(nat,Le)";
+by Auto_tac;
+qed "refl_Le";
+AddIffs [refl_Le];
+
+Goalw [antisym_def, Le_def] "antisym(Le)";
+by (auto_tac (claset() addIs [le_anti_sym], simpset()));
+qed "antisym_Le";
+AddIffs [antisym_Le];
+
+Goalw [trans_def, Le_def] "trans(Le)";
+by (auto_tac (claset() addIs [le_trans], simpset()));
+qed "trans_Le";
+AddIffs [trans_Le];
+
+Goal "x:list(nat) ==> x pfixLe x";
+by (blast_tac (claset() addIs [refl_gen_prefix RS reflD]) 1);
+qed "pfixLe_refl";
+Addsimps[pfixLe_refl];
+
+Goal "[| x pfixLe y; y pfixLe z |] ==> x pfixLe z";
+by (blast_tac (claset() addIs [trans_gen_prefix RS transD]) 1);
+qed "pfixLe_trans";
+
+Goal "[| x pfixLe y; y pfixLe x |] ==> x = y";
+by (blast_tac (claset() addIs [antisym_gen_prefix RS antisymE]) 1);
+qed "pfixLe_antisym";
+
+
+Goalw [prefix_def, Le_def]
+"<xs,ys>:prefix(nat)==> xs pfixLe ys";
+by (rtac (gen_prefix_mono RS subsetD) 1);
+by Auto_tac;
+qed "prefix_imp_pfixLe";
+
+Goalw [refl_def, Ge_def] "refl(nat, Ge)";
+by Auto_tac;
+qed "refl_Ge";
+AddIffs [refl_Ge];
+
+Goalw [antisym_def, Ge_def] "antisym(Ge)";
+by (auto_tac (claset() addIs [le_anti_sym], simpset()));
+qed "antisym_Ge";
+AddIffs [antisym_Ge];
+
+Goalw [trans_def, Ge_def] "trans(Ge)";
+by (auto_tac (claset() addIs [le_trans], simpset()));
+qed "trans_Ge";
+AddIffs [trans_Ge];
+
+Goal "x:list(nat) ==> x pfixGe x";
+by (blast_tac (claset() addIs [refl_gen_prefix RS reflD]) 1);
+qed "pfixGe_refl";
+Addsimps[pfixGe_refl];
+
+Goal "[| x pfixGe y; y pfixGe z |] ==> x pfixGe z";
+by (blast_tac (claset() addIs [trans_gen_prefix RS transD]) 1);
+qed "pfixGe_trans";
+
+Goal "[| x pfixGe y; y pfixGe x |] ==> x = y";
+by (blast_tac (claset() addIs [antisym_gen_prefix RS antisymE]) 1);
+qed "pfixGe_antisym";
+
+Goalw [prefix_def, Ge_def]
+ "<xs,ys>:prefix(nat) ==> xs pfixGe ys";
+by (rtac (gen_prefix_mono RS subsetD) 1);
+by Auto_tac;
+qed "prefix_imp_pfixGe";
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/ListPlus.ML Thu Nov 15 16:46:38 2001 +0100
@@ -0,0 +1,352 @@
+(* Title: ZF/UNITY/ListPlus.ML
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+More about lists
+
+*)
+
+(*** more theorems about lists ***)
+
+(** td and tl **)
+
+(** length **)
+
+Goal "xs:list(A) ==> length(xs)=0 <-> xs=Nil";
+by (etac list.induct 1);
+by Auto_tac;
+qed "length_is_0_iff";
+Addsimps [length_is_0_iff];
+
+Goal "xs:list(A) ==> 0 = length(xs) <-> xs=Nil";
+by (etac list.induct 1);
+by Auto_tac;
+qed "length_is_0_iff2";
+Addsimps [length_is_0_iff2];
+
+Goal "xs:list(A) ==> length(tl(xs)) = length(xs) #- 1";
+by (etac list.induct 1);
+by Auto_tac;
+qed "length_tl";
+Addsimps [length_tl];
+
+Goal "xs:list(A) ==> 0<length(xs) <-> xs ~= Nil";
+by (etac list.induct 1);
+by Auto_tac;
+qed "length_greater_0_iff";
+
+Goal "xs:list(A) ==> length(xs)=succ(n) <-> (EX y ys. xs=Cons(y, ys) & length(ys)=n)";
+by (etac list.induct 1);
+by Auto_tac;
+qed "length_succ_iff";
+
+(** more theorems about append **)
+Goal "xs:list(A) ==> (xs@ys = Nil) <-> (xs=Nil & ys = Nil)";
+by (etac list.induct 1);
+by Auto_tac;
+qed "append_is_Nil_iff";
+Addsimps [append_is_Nil_iff];
+
+Goal "xs:list(A) ==> (Nil = xs@ys) <-> (xs=Nil & ys = Nil)";
+by (etac list.induct 1);
+by Auto_tac;
+qed "append_is_Nil_iff2";
+Addsimps [append_is_Nil_iff2];
+
+Goal "xs:list(A) ==> (xs@ys = xs) <-> (ys = Nil)";
+by (etac list.induct 1);
+by Auto_tac;
+qed "append_left_is_self_iff";
+Addsimps [append_left_is_self_iff];
+
+Goal "xs:list(A) ==> (xs = xs@ys) <-> (ys = Nil)";
+by (etac list.induct 1);
+by Auto_tac;
+qed "append_left_is_self_iff2";
+Addsimps [append_left_is_self_iff2];
+
+Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
+\ length(ys)=length(zs) --> (xs@ys=zs <-> (xs=Nil & ys=zs))";
+by (etac list.induct 1);
+by (auto_tac (claset(), simpset() addsimps [length_app, length_type]));
+qed_spec_mp "append_left_is_Nil_iff";
+Addsimps [append_left_is_Nil_iff];
+
+Goal "[| xs:list(A); ys:list(A); zs:list(A) |] ==> \
+\ length(ys)=length(zs) --> (zs=ys@xs <-> (xs=Nil & ys=zs))";
+by (etac list.induct 1);
+by (auto_tac (claset(), simpset() addsimps [length_app, length_type]));
+qed_spec_mp "append_left_is_Nil_iff2";
+Addsimps [append_left_is_Nil_iff2];
+
+Goal "xs:list(A) ==> ALL ys:list(A). \
+\ length(xs)=length(ys) --> (xs@us = ys@vs) <-> (xs=ys & us=vs)";
+by (etac list.induct 1);
+by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("a", "ys")] list.elim 1);
+by (ALLGOALS(Asm_full_simp_tac));
+qed_spec_mp "append_eq_append_iff";
+
+
+Goal "xs:list(A) ==> \
+\ ALL ys:list(A). ALL us:list(A). ALL vs:list(A). \
+\ length(us) = length(vs) --> (xs@us = ys@vs) --> (xs=ys & us=vs)";
+by (induct_tac "xs" 1);
+by (ALLGOALS(Clarify_tac));
+by (asm_full_simp_tac (simpset() addsimps [length_type, 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 (ALLGOALS(asm_full_simp_tac (simpset() addsimps [length_type])));
+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
+ if we add two more hypotheses x:A and y:A *)
+Goal "xs:list(A) ==> ALL ys:list(A). xs@[x] = ys@[y] <-> (xs = ys & x=y)";
+by (etac list.induct 1);
+by (ALLGOALS(Clarify_tac));
+by (ALLGOALS(eres_inst_tac [("a", "ys")] list.elim));
+by Auto_tac;
+qed_spec_mp "append1_eq_iff";
+Addsimps [append1_eq_iff];
+
+Goal "[| xs:list(A); ys:list(A) |] ==> (xs@ys = ys) <-> (xs=Nil)";
+by (Asm_simp_tac 1);
+qed "append_right_is_self_iff";
+Addsimps [append_right_is_self_iff];
+
+Goal "[| xs:list(A); ys:list(A) |] ==> (ys = xs@ys) <-> (xs=Nil)";
+by (rtac iffI 1);
+by (dtac sym 1);
+by (ALLGOALS(Asm_full_simp_tac));
+qed "append_right_is_self_iff2";
+Addsimps [append_right_is_self_iff2];
+
+Goal "xs:list(A) ==> xs ~= Nil --> hd(xs @ ys) = hd(xs)";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed_spec_mp "hd_append";
+Addsimps [hd_append];
+
+Goal "xs:list(A) ==> xs~=Nil --> tl(xs @ ys) = tl(xs)@ys";
+by (induct_tac "xs" 1);
+by Auto_tac;
+qed_spec_mp "tl_append";
+Addsimps [tl_append];
+
+(** rev **)
+Goal "xs:list(A) ==> (rev(xs) = Nil <-> xs = Nil)";
+by (etac list.induct 1);
+by Auto_tac;
+qed "rev_is_Nil_iff";
+Addsimps [rev_is_Nil_iff];
+
+Goal "xs:list(A) ==> (Nil = rev(xs) <-> xs = Nil)";
+by (etac list.induct 1);
+by Auto_tac;
+qed "Nil_is_rev_iff";
+Addsimps [Nil_is_rev_iff];
+
+Goal "xs:list(A) ==> ALL ys:list(A). rev(xs)=rev(ys) <-> xs=ys";
+by (etac list.induct 1);
+by (Force_tac 1);
+by (Clarify_tac 1);
+by (eres_inst_tac [("a", "ys")] list.elim 1);
+by Auto_tac;
+qed_spec_mp "rev_is_rev_iff";
+Addsimps [rev_is_rev_iff];
+
+Goal "xs:list(A) ==> \
+\ (xs=Nil --> P) --> (ALL ys:list(A). ALL y:A. xs =ys@[y] -->P)-->P";
+by (etac list_append_induct 1);
+by Auto_tac;
+qed_spec_mp "rev_list_elim_aux";
+
+bind_thm("rev_list_elim", impI RS ballI RS ballI RSN(3, rev_list_elim_aux));
+
+(** more theorems about drop **)
+Goal "n:nat ==> ALL xs:list(A). length(drop(n, xs)) = length(xs) #- n";
+by (etac nat_induct 1);
+by (ALLGOALS(Clarify_tac));
+by (etac list.elim 2);
+by Auto_tac;
+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 (ALLGOALS(Clarify_tac));
+by (etac list.elim 2);
+by Auto_tac;
+qed_spec_mp "drop_all";
+Addsimps [drop_all];
+
+(** 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 (ALLGOALS(Clarify_tac));
+by (etac list.elim 2);
+by Auto_tac;
+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];
+
+(** nth **)
+
+Goalw [nth_def] "nth(0, Cons(a, l))= a";
+by Auto_tac;
+qed "nth_0";
+AddIffs [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";
+
+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";
+
+(* Other 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";
+
+Goalw [Ball_def]
+ "k:nat ==> \
+\ ALL xs:list(A). (ALL ys:list(A). k le length(xs) --> k le length(ys) --> \
+\ (ALL i:nat. i < k --> nth(i,xs)= nth(i,ys))--> take(k, xs) = take(k,ys))";
+by (induct_tac "k" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps
+ [lt_succ_eq_0_disj, all_conj_distrib])));
+by (Clarify_tac 1);
+(*Both lists must be non-empty*)
+by (case_tac "xa=Nil" 1);
+by (case_tac "xb=Nil" 2);
+by (Clarify_tac 1);
+by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [neq_Nil_iff])));
+by (Clarify_tac 1);
+(*prenexing's needed, not miniscoping*)
+by (Asm_simp_tac 1);
+by (rtac conjI 1);
+by (Force_tac 1);
+by (ALLGOALS (full_simp_tac (simpset() addsimps (all_simps RL [iff_sym])
+ delsimps (all_simps))));
+by (dres_inst_tac [("x", "ys"), ("x1", "ysa")] (spec RS spec) 1);
+by 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 [length_type,take_all])));
+qed_spec_mp "take_equalityI";
+
+(** More on lists **)
+
+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";
+
+
+
+