--- 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<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
--- 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";
--- 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";
--- 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);
--- 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";
--- 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*)
--- 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. <x,z>) : 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(%<x,y>.<Inl(x),y>, %<x,y>.<Inr(x),y>)")] lam_bijective 1);
-by (safe_tac (claset() addSEs [sumE]));
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
qed "sum_prod_distrib_bij";
Goal "(lam <x,z>:(A+B)*C. case(%y. Inl(<y,z>), %y. Inr(<y,z>), 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 <<x,y>, z>:(A*B)*C. <x,<y,z>>) : bij((A*B)*C, A*(B*C))";
by (res_inst_tac [("d", "%<x, <y,z>>. <<x,y>, z>")] lam_bijective 1);
-by (ALLGOALS (asm_simp_tac (simpset() setloop etac SigmaE)));
+by Auto_tac;
qed "prod_assoc_bij";
Goal "(lam <<x,y>, z>:(A*B)*C. <x,<y,z>>) \
\ : 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]
- "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: r & a:A & b:A";
+Goalw [rvimage_def] "<a,b> : rvimage(A,f,r) <-> <f`a,f`b>: 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!*)
--- 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];
(* ------------------------------------------------------------------------- *)
--- 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];
--- 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";
--- 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);
--- 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)];