# HG changeset patch # User paulson # Date 949932842 -3600 # Node ID a81d18b0a9b1e9c5f4156a6a7b1b32509b7b3a0a # Parent 700067a98634c1f5fbdced67f848c0a139e0df55 tidied some proofs diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/Arith.ML --- a/src/ZF/Arith.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/Arith.ML Mon Feb 07 15:14:02 2000 +0100 @@ -78,8 +78,7 @@ "[| m:nat; n:nat |] ==> m #- n le m"; by (rtac (prems MRS diff_induct) 1); by (etac leE 3); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps prems @ [le_iff, nat_into_Ord]))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps prems @ [le_iff]))); qed "diff_le_self"; (*** Simplification over add, mult, diff ***) @@ -284,7 +283,7 @@ [Ord_transrec_type, apply_type, div_termination RS ltD, if_type, nat_into_Ord, not_lt_iff_le RS iffD1]; -val div_ss = simpset() addsimps [nat_into_Ord, div_termination RS ltD, +val div_ss = simpset() addsimps [div_termination RS ltD, not_lt_iff_le RS iffD2]; (*Type checking depends upon termination!*) @@ -336,7 +335,7 @@ by (Asm_simp_tac 2); (*case n le x*) by (asm_full_simp_tac - (simpset() addsimps [not_lt_iff_le, nat_into_Ord, add_assoc, + (simpset() addsimps [not_lt_iff_le, add_assoc, div_termination RS ltD, add_diff_inverse]) 1); qed "mod_div_equality"; @@ -352,8 +351,7 @@ succ_neq_self]) 2); by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2); (* case n le succ(x) *) -by (asm_full_simp_tac - (simpset() addsimps [not_lt_iff_le, nat_into_Ord]) 1); +by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1); by (etac leE 1); (*equality case*) by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2); @@ -367,8 +365,7 @@ by (asm_simp_tac (simpset() addsimps [mod_less]) 2); (*case n le x*) by (asm_full_simp_tac - (simpset() addsimps [not_lt_iff_le, nat_into_Ord, - mod_geq, div_termination RS ltD]) 1); + (simpset() addsimps [not_lt_iff_le, mod_geq, div_termination RS ltD]) 1); qed "mod_less_divisor"; @@ -411,7 +408,7 @@ by (ftac lt_nat_in_nat 1); by (assume_tac 1); by (etac succ_lt_induct 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nat_into_Ord, leI]))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI]))); qed "add_lt_mono1"; (*strict, in both arguments*) @@ -496,7 +493,7 @@ by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff, mult_lt_mono2]) 2); by (asm_full_simp_tac - (simpset() addsimps [not_lt_iff_le, nat_into_Ord, + (simpset() addsimps [not_lt_iff_le, zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq, diff_mult_distrib2 RS sym, div_termination RS ltD]) 1); @@ -509,7 +506,7 @@ by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff, mult_lt_mono2]) 2); by (asm_full_simp_tac - (simpset() addsimps [not_lt_iff_le, nat_into_Ord, + (simpset() addsimps [not_lt_iff_le, zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq, diff_mult_distrib2 RS sym, div_termination RS ltD]) 1); @@ -530,7 +527,7 @@ by (induct_tac "m" 1); by (Asm_simp_tac 1); by Safe_tac; -by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt,nat_into_Ord]) 1); +by (asm_full_simp_tac (simpset() addsimps [not_le_iff_lt]) 1); qed "add_le_elim1"; Goal "[| m EX k: nat. n = succ(m#+k)"; diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/CardinalArith.ML --- a/src/ZF/CardinalArith.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/CardinalArith.ML Mon Feb 07 15:14:02 2000 +0100 @@ -121,7 +121,7 @@ Goal "[| m: nat; n: nat |] ==> m |+| n = m#+n"; by (induct_tac "m" 1); by (asm_simp_tac (simpset() addsimps [nat_into_Card RS cadd_0]) 1); -by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cadd_succ_lemma, +by (asm_simp_tac (simpset() addsimps [cadd_succ_lemma, nat_into_Card RS Card_cardinal_eq]) 1); qed "nat_cadd_eq_add"; @@ -285,8 +285,7 @@ Goal "[| m: nat; n: nat |] ==> m |*| n = m#*n"; by (induct_tac "m" 1); by (Asm_simp_tac 1); -by (asm_simp_tac (simpset() addsimps [nat_into_Ord, cmult_succ_lemma, - nat_cadd_eq_add]) 1); +by (asm_simp_tac (simpset() addsimps [cmult_succ_lemma, nat_cadd_eq_add]) 1); qed "nat_cmult_eq_mult"; Goal "Card(n) ==> 2 |*| n = n |+| n"; diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/Epsilon.ML --- a/src/ZF/Epsilon.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/Epsilon.ML Mon Feb 07 15:14:02 2000 +0100 @@ -107,9 +107,8 @@ by (REPEAT (assume_tac 1)); qed "mem_eclose_sing_trans"; -Goalw [Transset_def] - "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; -by (blast_tac (claset() addSIs [MemrelI] addSEs [MemrelE]) 1); +Goalw [Transset_def] "[| Transset(i); j:i |] ==> Memrel(i)-``{j} = j"; +by (Blast_tac 1); qed "under_Memrel"; (* j : eclose(A) ==> Memrel(eclose(A)) -`` j = j *) @@ -318,7 +317,7 @@ Goal "transrec2(succ(i),a,b) = b(i, transrec2(i,a,b))"; by (rtac (transrec2_def RS def_transrec RS trans) 1); -by (simp_tac (simpset() addsimps [succ_not_0, THE_eq, if_P]) 1); +by (simp_tac (simpset() addsimps [THE_eq, if_P]) 1); by (Blast_tac 1); qed "transrec2_succ"; diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/Finite.ML --- a/src/ZF/Finite.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/Finite.ML Mon Feb 07 15:14:02 2000 +0100 @@ -103,7 +103,7 @@ (*Functions from a finite ordinal*) Goal "n: nat ==> n->A <= Fin(nat*A)"; by (induct_tac "n" 1); -by (simp_tac (simpset() addsimps [Pi_empty1, subset_iff, cons_iff]) 1); +by (simp_tac (simpset() addsimps [subset_iff]) 1); by (asm_simp_tac (simpset() addsimps [succ_def, mem_not_refl RS cons_fun_eq]) 1); by (fast_tac (claset() addSIs [Fin.consI]) 1); @@ -125,14 +125,14 @@ Goal "h: A -||>B ==> h: domain(h) -> B"; by (etac FiniteFun.induct 1); -by (simp_tac (simpset() addsimps [empty_fun, domain_0]) 1); -by (asm_simp_tac (simpset() addsimps [fun_extend3, domain_cons]) 1); +by (Simp_tac 1); +by (asm_simp_tac (simpset() addsimps [fun_extend3]) 1); qed "FiniteFun_is_fun"; Goal "h: A -||>B ==> domain(h) : Fin(A)"; by (etac FiniteFun.induct 1); -by (simp_tac (simpset() addsimps [domain_0]) 1); -by (asm_simp_tac (simpset() addsimps [domain_cons]) 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); qed "FiniteFun_domain_Fin"; bind_thm ("FiniteFun_apply_type", FiniteFun_is_fun RS apply_type); diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/Integ/Int.ML --- a/src/ZF/Integ/Int.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/Integ/Int.ML Mon Feb 07 15:14:02 2000 +0100 @@ -193,7 +193,7 @@ by (rtac bexI 1); by (rtac (add_diff_inverse2 RS sym) 1); by Auto_tac; -by (asm_full_simp_tac (simpset() addsimps [nat_into_Ord, not_lt_iff_le]) 1); +by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le]) 1); qed "not_zneg_int_of"; Goal "[| z: int; ~ znegative(z) |] ==> $# (zmagnitude(z)) = z"; diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/Order.ML --- a/src/ZF/Order.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/Order.ML Mon Feb 07 15:14:02 2000 +0100 @@ -9,8 +9,6 @@ by Ken Kunen. Chapter 1, section 6. *) -open Order; - (** Basic properties of the definitions **) (*needed?*) @@ -567,8 +565,7 @@ \ range(ord_iso_map(A,r,B,s)) = B | \ \ (EX y:B. range(ord_iso_map(A,r,B,s))= pred(B,y,s))"; by (resolve_tac [converse_ord_iso_map RS subst] 1); -by (asm_simp_tac - (simpset() addsimps [range_converse, domain_ord_iso_map_cases]) 1); +by (asm_simp_tac (simpset() addsimps [domain_ord_iso_map_cases]) 1); qed "range_ord_iso_map_cases"; (*Kunen's Theorem 6.3: Fundamental Theorem for Well-Ordered Sets*) diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/OrderArith.ML --- a/src/ZF/OrderArith.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/OrderArith.ML Mon Feb 07 15:14:02 2000 +0100 @@ -6,9 +6,6 @@ Towards ordinal arithmetic *) -open OrderArith; - - (**** Addition of relations -- disjoint sum ****) (** Rewrite rules. Can be used to obtain introduction rules **) @@ -67,8 +64,7 @@ Goalw [linear_def] "[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"; -by (REPEAT_FIRST (ares_tac [ballI] ORELSE' etac sumE)); -by (ALLGOALS Asm_simp_tac); +by (Force_tac 1); qed "linear_radd"; @@ -110,7 +106,7 @@ by (res_inst_tac [("d", "case(%x. Inl(converse(f)`x), %y. Inr(converse(g)`y))")] lam_bijective 1); -by (safe_tac (claset() addSEs [sumE])); +by Safe_tac; by (ALLGOALS (asm_simp_tac bij_inverse_ss)); qed "sum_bij"; @@ -134,11 +130,7 @@ \ (lam z:A+B. case(%x. x, %y. y, z)) : bij(A+B, A Un B)"; by (res_inst_tac [("d", "%z. if z:A then Inl(z) else Inr(z)")] lam_bijective 1); -by (blast_tac (claset() addSIs [if_type]) 2); -by (DEPTH_SOLVE_1 (eresolve_tac [case_type, UnI1, UnI2] 1)); -by Safe_tac; -by (ALLGOALS Asm_simp_tac); -by (blast_tac (claset() addEs [equalityE]) 1); +by Auto_tac; qed "sum_disjoint_bij"; (** Associativity **) @@ -147,15 +139,14 @@ \ : bij((A+B)+C, A+(B+C))"; by (res_inst_tac [("d", "case(%x. Inl(Inl(x)), case(%x. Inl(Inr(x)), Inr))")] lam_bijective 1); -by (ALLGOALS (asm_simp_tac (simpset() setloop etac sumE))); +by Auto_tac; qed "sum_assoc_bij"; Goal "(lam z:(A+B)+C. case(case(Inl, %y. Inr(Inl(y))), %y. Inr(Inr(y)), z)) \ \ : ord_iso((A+B)+C, radd(A+B, radd(A,r,B,s), C, t), \ \ A+(B+C), radd(A, r, B+C, radd(B,s,C,t)))"; by (resolve_tac [sum_assoc_bij RS ord_isoI] 1); -by (REPEAT_FIRST (etac sumE)); -by (ALLGOALS Asm_simp_tac); +by Auto_tac; qed "sum_assoc_ord_iso"; @@ -255,8 +246,7 @@ Goal "(lam z:A. ) : bij(A, {x}*A)"; by (res_inst_tac [("d", "snd")] lam_bijective 1); -by Safe_tac; -by (ALLGOALS Asm_simp_tac); +by Auto_tac; qed "singleton_prod_bij"; (*Used??*) @@ -277,7 +267,7 @@ by (rtac singleton_prod_bij 1); by (rtac sum_disjoint_bij 1); by (Blast_tac 1); -by (asm_simp_tac (simpset() addcongs [case_cong] addsimps [id_conv]) 1); +by (asm_simp_tac (simpset() addcongs [case_cong]) 1); by (resolve_tac [comp_lam RS trans RS sym] 1); by (fast_tac (claset() addSEs [case_type]) 1); by (asm_simp_tac (simpset() addsimps [case_case]) 1); @@ -303,40 +293,35 @@ \ : bij((A+B)*C, (A*C)+(B*C))"; by (res_inst_tac [("d", "case(%., %.)")] lam_bijective 1); -by (safe_tac (claset() addSEs [sumE])); -by (ALLGOALS Asm_simp_tac); +by Auto_tac; qed "sum_prod_distrib_bij"; Goal "(lam :(A+B)*C. case(%y. Inl(), %y. Inr(), x)) \ \ : ord_iso((A+B)*C, rmult(A+B, radd(A,r,B,s), C, t), \ \ (A*C)+(B*C), radd(A*C, rmult(A,r,C,t), B*C, rmult(B,s,C,t)))"; by (resolve_tac [sum_prod_distrib_bij RS ord_isoI] 1); -by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE])); -by (ALLGOALS Asm_simp_tac); +by Auto_tac; qed "sum_prod_distrib_ord_iso"; (** Associativity **) Goal "(lam <, z>:(A*B)*C. >) : bij((A*B)*C, A*(B*C))"; by (res_inst_tac [("d", "%>. <, z>")] lam_bijective 1); -by (ALLGOALS (asm_simp_tac (simpset() setloop etac SigmaE))); +by Auto_tac; qed "prod_assoc_bij"; Goal "(lam <, z>:(A*B)*C. >) \ \ : ord_iso((A*B)*C, rmult(A*B, rmult(A,r,B,s), C, t), \ \ A*(B*C), rmult(A, r, B*C, rmult(B,s,C,t)))"; by (resolve_tac [prod_assoc_bij RS ord_isoI] 1); -by (REPEAT_FIRST (eresolve_tac [SigmaE, ssubst])); -by (Asm_simp_tac 1); -by (Blast_tac 1); +by Auto_tac; qed "prod_assoc_ord_iso"; (**** Inverse image of a relation ****) (** Rewrite rule **) -Goalw [rvimage_def] - " : rvimage(A,f,r) <-> : r & a:A & b:A"; +Goalw [rvimage_def] " : rvimage(A,f,r) <-> : r & a:A & b:A"; by (Blast_tac 1); qed "rvimage_iff"; @@ -348,8 +333,7 @@ bind_thm ("field_rvimage", (rvimage_type RS field_rel_subset)); -Goalw [rvimage_def] - "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"; +Goalw [rvimage_def] "rvimage(A,f, converse(r)) = converse(rvimage(A,f,r))"; by (Blast_tac 1); qed "rvimage_converse"; @@ -398,7 +382,7 @@ by (eres_inst_tac [("a","f`y")] wf_on_induct 1); by (blast_tac (claset() addSIs [apply_funtype]) 1); by (blast_tac (claset() addSIs [apply_funtype] - addSDs [rvimage_iff RS iffD1]) 1); + addSDs [rvimage_iff RS iffD1]) 1); qed "wf_on_rvimage"; (*Note that we need only wf[A](...) and linear(A,...) to get the result!*) diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/Resid/Substitution.ML --- a/src/ZF/Resid/Substitution.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/Resid/Substitution.ML Mon Feb 07 15:14:02 2000 +0100 @@ -34,7 +34,7 @@ qed "gt_pred"; -Addsimps [nat_into_Ord, not_lt_iff_le, if_P, if_not_P]; +Addsimps [not_lt_iff_le, if_P, if_not_P]; (* ------------------------------------------------------------------------- *) diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/Sum.ML --- a/src/ZF/Sum.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/Sum.ML Mon Feb 07 15:14:02 2000 +0100 @@ -131,11 +131,11 @@ (*** Eliminator -- case ***) Goalw sum_defs "case(c, d, Inl(a)) = c(a)"; -by (simp_tac (simpset() addsimps [cond_0]) 1); +by (Simp_tac 1); qed "case_Inl"; Goalw sum_defs "case(c, d, Inr(b)) = d(b)"; -by (simp_tac (simpset() addsimps [cond_1]) 1); +by (Simp_tac 1); qed "case_Inr"; Addsimps [case_Inl, case_Inr]; diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/ex/Limit.ML --- a/src/ZF/ex/Limit.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/ex/Limit.ML Mon Feb 07 15:14:02 2000 +0100 @@ -1784,7 +1784,6 @@ (* Must control rewriting by instantiating a variable. *) by (asm_full_simp_tac(simpset() addsimps [read_instantiate [("i1","n")] (nat_into_Ord RS not_le_iff_lt RS iff_sym), - nat_into_Ord, add_le_self]) 1); qed "eps_e_gr_add"; diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/ex/Primrec.ML --- a/src/ZF/ex/Primrec.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/ex/Primrec.ML Mon Feb 07 15:14:02 2000 +0100 @@ -52,7 +52,7 @@ by (asm_simp_tac (simpset() addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1); qed "ack_succ_succ"; -Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type, nat_into_Ord]; +Addsimps [ack_0, ack_succ_0, ack_succ_succ, ack_type]; Delsimps [ACK_0, ACK_succ]; @@ -165,7 +165,7 @@ (*** MAIN RESULT ***) -Addsimps [list_add_type, nat_into_Ord]; +Addsimps [list_add_type]; Goalw [SC_def] "l: list(nat) ==> SC ` l < ack(1, list_add(l))"; by (exhaust_tac "l" 1); diff -r 700067a98634 -r a81d18b0a9b1 src/ZF/func.ML --- a/src/ZF/func.ML Sat Feb 05 17:31:53 2000 +0100 +++ b/src/ZF/func.ML Mon Feb 07 15:14:02 2000 +0100 @@ -353,7 +353,7 @@ (** The Union of 2 disjoint functions is a function **) -val Un_rls = [Un_subset_iff, domain_Un_eq, SUM_Un_distrib1, prod_Un_distrib2, +val Un_rls = [Un_subset_iff, SUM_Un_distrib1, prod_Un_distrib2, Un_upper1 RSN (2, subset_trans), Un_upper2 RSN (2, subset_trans)];