# HG changeset patch # User paulson # Date 918053437 -3600 # Node ID 707b6f9859d22487a4f0543e76f6bb0b3b044741 # Parent 8460ddd478d264d3f65ae301081f70229e95cfb0 tidied, with left_inverse & right_inverse as default simprules diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/AC/AC16_WO4.ML --- 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] diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/AC/rel_is_fun.ML --- 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] diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/Cardinal.ML --- 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"; diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/CardinalArith.ML --- 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", "%.")] 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"; diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/Cardinal_AC.ML --- 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 i \ \ (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 diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/Order.ML --- 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); : s; x:B; y:B |] ==> \ \ : 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] diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/Ordinal.ML --- 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 i i le i Un j"; diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/Perm.ML --- 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"; diff -r 8460ddd478d2 -r 707b6f9859d2 src/ZF/ex/Limit.ML --- 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();