--- a/src/ZF/AC/AC16_WO4.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/AC/AC16_WO4.ML Wed Feb 03 15:50:37 1999 +0100
@@ -76,10 +76,7 @@
Goal "[| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \
\ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)";
by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1);
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps [inj_is_fun RS apply_type, left_inverse]
- setloop (split_tac [split_if] ORELSE' Step_tac))));
+by (auto_tac (claset(), simpset() addsimps [inj_is_fun RS apply_type]));
qed "succ_not_lepoll_lemma";
Goalw [lepoll_def, eqpoll_def, bij_def, surj_def]
--- a/src/ZF/AC/rel_is_fun.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/AC/rel_is_fun.ML Wed Feb 03 15:50:37 1999 +0100
@@ -20,8 +20,8 @@
by (etac domainE 1);
by (forward_tac [inj_is_fun RS apply_type] 1 THEN (atac 1));
by (rtac LeastI2 1);
-by (REPEAT (fast_tac (claset() addSEs [nat_into_Ord RS Ord_in_Ord]
- addss (simpset() addsimps [left_inverse])) 1));
+by (auto_tac (claset() addSEs [nat_into_Ord RS Ord_in_Ord],
+ simpset()));
qed "lepoll_m_imp_domain_lepoll_m";
goalw Cardinal.thy [function_def]
--- a/src/ZF/Cardinal.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/Cardinal.ML Wed Feb 03 15:50:37 1999 +0100
@@ -562,7 +562,7 @@
lam_injective 1);
by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, cons_iff]
setloop etac consE') 1);
-by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse]
+by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type]
setloop etac consE') 1);
qed "cons_lepoll_cong";
@@ -616,10 +616,9 @@
by (blast_tac (claset() addSIs [if_type, inj_is_fun RS apply_type]) 1);
by (asm_simp_tac
(simpset() addsimps [inj_converse_fun RS apply_funtype]) 1);
-by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI, left_inverse]
+by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI]
setloop etac UnE') 1);
-by (asm_simp_tac
- (simpset() addsimps [inj_converse_fun RS apply_funtype, right_inverse]) 1);
+by (asm_simp_tac (simpset() addsimps [inj_converse_fun RS apply_funtype]) 1);
by (Blast_tac 1);
qed "inj_disjoint_eqpoll";
--- a/src/ZF/CardinalArith.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/CardinalArith.ML Wed Feb 03 15:50:37 1999 +0100
@@ -85,8 +85,7 @@
[("d", "case(%w. Inl(converse(f)`w), %y. Inr(converse(fa)`y))")]
lam_injective 1);
by (typecheck_tac (tcset() addTCs [inj_is_fun]));
-by (etac sumE 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [left_inverse])));
+by Auto_tac;
qed "sum_lepoll_mono";
Goalw [cadd_def]
@@ -251,8 +250,7 @@
by (res_inst_tac [("d", "%<w,y>.<converse(f)`w, converse(fa)`y>")]
lam_injective 1);
by (typecheck_tac (tcset() addTCs [inj_is_fun]));
-by (etac SigmaE 1);
-by (asm_simp_tac (simpset() addsimps [left_inverse]) 1);
+by Auto_tac;
qed "prod_lepoll_mono";
Goalw [cmult_def]
@@ -329,9 +327,7 @@
by (asm_simp_tac
(simpset() addsimps [inj_is_fun RS apply_rangeI,
inj_converse_fun RS apply_rangeI,
- inj_converse_fun RS apply_funtype,
- left_inverse, right_inverse, nat_0I, nat_succI,
- nat_case_0, nat_case_succ]) 1);
+ inj_converse_fun RS apply_funtype]) 1);
qed "nat_cons_lepoll";
Goal "nat lepoll A ==> cons(u,A) eqpoll A";
--- a/src/ZF/Cardinal_AC.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/Cardinal_AC.ML Wed Feb 03 15:50:37 1999 +0100
@@ -124,9 +124,7 @@
by (ALLGOALS ball_tac);
by (blast_tac (claset() addIs [inj_is_fun RS apply_type]
addDs [apply_type]) 1);
-by (dtac apply_type 1);
-by (etac conjunct2 1);
-by (asm_simp_tac (simpset() addsimps [left_inverse]) 1);
+by Auto_tac;
qed "cardinal_UN_le";
@@ -155,20 +153,13 @@
set need not be a cardinal. Surprisingly complicated proof!
**)
-(*Saves checking Ord(j) below*)
-goal Ordinal.thy "!!i j. [| i <= j; j<k; Ord(i) |] ==> i<k";
-by (resolve_tac [subset_imp_le RS lt_trans1] 1);
-by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
-qed "lt_subset_trans";
-
(*Work backwards along the injection from W into K, given that W~=0.*)
Goal "[| f: inj(A,B); a:A |] ==> \
\ (UN x:A. C(x)) <= (UN y:B. C(if y: range(f) then converse(f)`y else a))";
by (rtac UN_least 1);
by (res_inst_tac [("x1", "f`x")] (UN_upper RSN (2,subset_trans)) 1);
by (eresolve_tac [inj_is_fun RS apply_type] 2 THEN assume_tac 2);
-by (asm_simp_tac
- (simpset() addsimps [inj_is_fun RS apply_rangeI, left_inverse]) 1);
+by (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_rangeI]) 1);
val inj_UN_subset = result();
(*Simpler to require |W|=K; we'd have a bijection; but the theorem would
--- a/src/ZF/Order.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/Order.ML Wed Feb 03 15:50:37 1999 +0100
@@ -240,6 +240,13 @@
by (Blast_tac 1);
qed "ord_iso_apply";
+(*Rewriting with bijections and converse (function inverse)*)
+val bij_inverse_ss =
+ simpset() setSolver
+ type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_inj,
+ inj_is_fun, comp_fun, comp_bij])
+ addsimps [right_inverse_bij];
+
Goalw [ord_iso_def]
"[| f: ord_iso(A,r,B,s); <x,y>: s; x:B; y:B |] ==> \
\ <converse(f) ` x, converse(f) ` y> : r";
@@ -247,16 +254,10 @@
by (etac (bspec RS bspec RS iffD2) 1);
by (REPEAT (eresolve_tac [asm_rl,
bij_converse_bij RS bij_is_fun RS apply_type] 1));
-by (asm_simp_tac (simpset() addsimps [right_inverse_bij]) 1);
+by (asm_simp_tac bij_inverse_ss 1);
qed "ord_iso_converse";
-(*Rewriting with bijections and converse (function inverse)*)
-val bij_inverse_ss =
- simpset() setSolver
- type_solver_tac (tcset() addTCs [ord_iso_is_bij, bij_is_fun, comp_fun, comp_bij])
- addsimps [right_inverse_bij, left_inverse_bij];
-
(** Symmetry and Transitivity Rules **)
(*Reflexivity of similarity*)
@@ -323,7 +324,7 @@
by (dres_inst_tac [("x1", "f`x"), ("x", "f`xa")] (bspec RS bspec) 1);
by (safe_tac (claset() addSEs [bij_is_fun RS apply_type]));
by (dres_inst_tac [("t", "op `(converse(f))")] subst_context 1);
-by (asm_full_simp_tac (simpset() addsimps [left_inverse_bij]) 1);
+by (asm_full_simp_tac bij_inverse_ss 1);
qed "linear_ord_iso";
Goalw [wf_on_def, wf_def, ord_iso_def]
--- a/src/ZF/Ordinal.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/Ordinal.ML Wed Feb 03 15:50:37 1999 +0100
@@ -532,6 +532,11 @@
by (blast_tac (claset() addSDs [succ_leE]) 1);
qed "succ_le_imp_le";
+Goal "[| i <= j; j<k; Ord(i) |] ==> i<k";
+by (resolve_tac [subset_imp_le RS lt_trans1] 1);
+by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
+qed "lt_subset_trans";
+
(** Union and Intersection **)
Goal "[| Ord(i); Ord(j) |] ==> i le i Un j";
--- a/src/ZF/Perm.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/Perm.ML Wed Feb 03 15:50:37 1999 +0100
@@ -178,7 +178,7 @@
Goal "[| f: inj(A,B); a: A |] ==> converse(f)`(f`a) = a";
by (blast_tac (claset() addIs [left_inverse_lemma, inj_converse_fun,
- inj_is_fun]) 1);
+ inj_is_fun]) 1);
qed "left_inverse";
val left_inverse_bij = bij_is_inj RS left_inverse;
@@ -195,12 +195,11 @@
by (REPEAT (ares_tac [inj_converse_fun,inj_is_fun] 1));
qed "right_inverse";
-(*Cannot add [left_inverse, right_inverse] to default simpset: there are too
- many ways of expressing sufficient conditions.*)
+Addsimps [left_inverse, right_inverse];
+
Goal "[| f: bij(A,B); b: B |] ==> f`(converse(f)`b) = b";
-by (fast_tac (claset() addss
- (simpset() addsimps [bij_def, right_inverse, surj_range])) 1);
+by (force_tac (claset(), simpset() addsimps [bij_def, surj_range]) 1);
qed "right_inverse_bij";
(** Converses of injections, surjections, bijections **)
@@ -213,8 +212,9 @@
qed "inj_converse_inj";
Goal "f: inj(A,B) ==> converse(f): surj(range(f), A)";
-by (blast_tac (claset() addIs [f_imp_surjective, inj_converse_fun, left_inverse,
- inj_is_fun, range_of_fun RS apply_type]) 1);
+by (blast_tac (claset() addIs [f_imp_surjective, inj_converse_fun,
+ left_inverse,
+ inj_is_fun, range_of_fun RS apply_type]) 1);
qed "inj_converse_surj";
Goalw [bij_def] "f: bij(A,B) ==> converse(f): bij(B,A)";
@@ -352,7 +352,7 @@
by (res_inst_tac [("d", "%y. converse(g) ` (converse(f) ` y)")]
f_imp_injective 1);
by (REPEAT (ares_tac [comp_fun, inj_is_fun] 1));
-by (asm_simp_tac (simpset() addsimps [left_inverse]
+by (asm_simp_tac (simpset()
setSolver
type_solver_tac (tcset() addTCs [inj_is_fun])) 1);
qed "comp_inj";
@@ -468,9 +468,8 @@
\ ==> (lam a: A Un C. if a:A then f`a else g`a) : inj(A Un C, B Un D)";
by (res_inst_tac [("d","%z. if z:B then converse(f)`z else converse(g)`z")]
lam_injective 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [inj_is_fun RS apply_type, left_inverse]
- setloop (split_tac [split_if] ORELSE' etac UnE))));
+by (auto_tac (claset(),
+ simpset() addsimps [inj_is_fun RS apply_type]));
by (blast_tac (claset() addIs [inj_is_fun RS apply_type]) 1);
qed "inj_disjoint_Un";
--- a/src/ZF/ex/Limit.ML Wed Feb 03 15:49:24 1999 +0100
+++ b/src/ZF/ex/Limit.ML Wed Feb 03 15:50:37 1999 +0100
@@ -1016,7 +1016,7 @@
bind_thm ("embRp_eq", embRp RS projpair_eq);
bind_thm ("embRp_rel", embRp RS projpair_rel);
-AddTCs [Rp_cont];
+AddTCs [emb_cont, Rp_cont];
val id_apply = prove_goalw Perm.thy [id_def]
"!!z. x:A ==> id(A)`x = x"
@@ -2154,6 +2154,8 @@
by (Fast_tac 1);
qed "commute_emb";
+AddTCs [commute_emb];
+
Goalw [commute_def] (* commute_eq *)
"[| commute(DD,ee,E,r); m le n; m:nat; n:nat |] ==> \
\ r(n) O eps(DD,ee,m,n) = r(m) ";
@@ -2414,8 +2416,7 @@
\ (lam na:nat. (f(na) O Rp(DD ` na, E, r(na))) O r(n))";
by (rtac fun_extension 1);
by (fast_tac (claset() addIs [lam_type]) 1);
-by (asm_simp_tac
- (simpset() setSolver type_solver_tac (tcset() addTCs [emb_cont, commute_emb])) 2);
+by (Asm_simp_tac 2);
by (fast_tac (claset() addIs [lam_type]) 1);
val lemma = result();