# HG changeset patch # User paulson # Date 962182594 -7200 # Node ID 422968aeed49d019c88bda696a3d7089b53ed60b # Parent 2dbb80d4fdb77f0014002098c32c3d732ad6a62d fixed some weak elim rules diff -r 2dbb80d4fdb7 -r 422968aeed49 src/ZF/Cardinal.ML --- a/src/ZF/Cardinal.ML Wed Jun 28 10:56:01 2000 +0200 +++ b/src/ZF/Cardinal.ML Wed Jun 28 10:56:34 2000 +0200 @@ -449,8 +449,8 @@ by (rtac CollectI 1); (*Proving it's in the function space A->B*) by (rtac (if_type RS lam_type) 1); -by (blast_tac (claset() addEs [apply_funtype RS consE]) 1); -by (blast_tac (claset() addSEs [mem_irrefl] addEs [apply_funtype RS consE]) 1); +by (blast_tac (claset() addDs [apply_funtype]) 1); +by (blast_tac (claset() addSEs [mem_irrefl] addDs [apply_funtype]) 1); (*Proving it's injective*) by (Asm_simp_tac 1); by (Blast_tac 1); @@ -481,7 +481,7 @@ by (rtac iffI 1); by (asm_simp_tac (simpset() addsimps [eqpoll_refl]) 2); by (blast_tac (claset() addIs [nat_lepoll_imp_le, le_anti_sym] - addSEs [eqpollE]) 1); + addSEs [eqpollE]) 1); qed "nat_eqpoll_iff"; (*The object of all this work: every natural number is a (finite) cardinal*) diff -r 2dbb80d4fdb7 -r 422968aeed49 src/ZF/Finite.ML --- a/src/ZF/Finite.ML Wed Jun 28 10:56:01 2000 +0200 +++ b/src/ZF/Finite.ML Wed Jun 28 10:56:34 2000 +0200 @@ -177,8 +177,7 @@ \ <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))"; by Auto_tac; by (blast_tac (claset() addIs [impOfSubs FiniteFun_mono]) 1); -by (blast_tac (claset() addDs [FiniteFun_is_fun] - addEs [Pair_mem_PiE]) 1); +by (blast_tac (claset() addDs [Pair_mem_PiD, FiniteFun_is_fun]) 1); by (res_inst_tac [("A1", "domain(f)")] (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1); by (fast_tac (claset() addDs diff -r 2dbb80d4fdb7 -r 422968aeed49 src/ZF/OrderArith.ML --- a/src/ZF/OrderArith.ML Wed Jun 28 10:56:01 2000 +0200 +++ b/src/ZF/OrderArith.ML Wed Jun 28 10:56:34 2000 +0200 @@ -254,7 +254,7 @@ \ (lam z:A. ) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))"; by (resolve_tac [singleton_prod_bij RS ord_isoI] 1); by (Asm_simp_tac 1); -by (blast_tac (claset() addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1); +by (blast_tac (claset() addDs [well_ord_is_wf RS wf_on_not_refl]) 1); qed "singleton_prod_ord_iso"; (*Here we build a complicated function term, then simplify it using @@ -281,10 +281,8 @@ by (resolve_tac [prod_sum_singleton_bij RS ord_isoI] 1); by (asm_simp_tac (simpset() addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1); -by (Asm_simp_tac 1); -by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, predE])); -by (ALLGOALS Asm_simp_tac); -by (ALLGOALS (blast_tac (claset() addEs [well_ord_is_wf RS wf_on_asym]))); +by (auto_tac (claset() addSEs [well_ord_is_wf RS wf_on_asym, predE], + simpset())); qed "prod_sum_singleton_ord_iso"; (** Distributive law **) diff -r 2dbb80d4fdb7 -r 422968aeed49 src/ZF/OrderType.ML --- a/src/ZF/OrderType.ML Wed Jun 28 10:56:01 2000 +0200 +++ b/src/ZF/OrderType.ML Wed Jun 28 10:56:34 2000 +0200 @@ -510,14 +510,14 @@ \ i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))"; by (blast_tac (claset() addIs prems @ [ltI, Ord_UN, Ord_oadd, lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD] - addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1); + addSEs [ltE] addSDs [ltI RS lt_oadd_disj]) 1); qed "oadd_UN"; Goal "[| Ord(i); Limit(j) |] ==> i++j = (UN k:j. i++k)"; by (forward_tac [Limit_has_0 RS ltD] 1); by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord, - oadd_UN RS sym, Union_eq_UN RS sym, - Limit_Union_eq]) 1); + oadd_UN RS sym, Union_eq_UN RS sym, + Limit_Union_eq]) 1); qed "oadd_Limit"; (** Order/monotonicity properties of ordinal addition **) diff -r 2dbb80d4fdb7 -r 422968aeed49 src/ZF/Perm.ML --- a/src/ZF/Perm.ML Wed Jun 28 10:56:01 2000 +0200 +++ b/src/ZF/Perm.ML Wed Jun 28 10:56:34 2000 +0200 @@ -57,8 +57,7 @@ (*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*) Goalw [inj_def] "[| :f; :f; f: inj(A,B) |] ==> a=c"; -by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1)); -by (Blast_tac 1); +by (blast_tac (claset() addDs [Pair_mem_PiD]) 1); qed "inj_equality"; Goalw [inj_def] "[| f:inj(A,B); a:A; b:A; f`a=f`b |] ==> a=b"; diff -r 2dbb80d4fdb7 -r 422968aeed49 src/ZF/Univ.ML --- a/src/ZF/Univ.ML Wed Jun 28 10:56:01 2000 +0200 +++ b/src/ZF/Univ.ML Wed Jun 28 10:56:34 2000 +0200 @@ -193,9 +193,10 @@ qed "Limit_VfromI"; val prems = Goal - "[| a: Vfrom(A,i); Limit(i); \ + "[| a: Vfrom(A,i); ~R ==> Limit(i); \ \ !!x. [| x R \ \ |] ==> R"; +by (rtac classical 1); by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1); by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1)); qed "Limit_VfromE"; @@ -209,8 +210,8 @@ by (etac (limiti RS Limit_has_succ) 1); qed "singleton_in_VLimit"; -val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD) -and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD); +bind_thm ("Vfrom_UnI1", Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)); +bind_thm ("Vfrom_UnI2", Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD)); (*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*) val [aprem,bprem,limiti] = goal Univ.thy @@ -403,7 +404,7 @@ Goal "[| a: Vfrom(A,i); Limit(i); Transset(A) |] ==> Pow(a) : Vfrom(A,i)"; by (blast_tac (claset() addEs [Limit_VfromE] - addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1); + addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1); qed "Pow_in_VLimit"; diff -r 2dbb80d4fdb7 -r 422968aeed49 src/ZF/WF.ML --- a/src/ZF/WF.ML Wed Jun 28 10:56:01 2000 +0200 +++ b/src/ZF/WF.ML Wed Jun 28 10:56:34 2000 +0200 @@ -17,8 +17,6 @@ a mess. *) -open WF; - (*** Well-founded relations ***) @@ -159,15 +157,9 @@ by (Blast_tac 1); qed_spec_mp "wf_on_not_sym"; -(* [| wf[A](r); : r; a:A; b:A; ~P ==> : r |] ==> P *) -bind_thm ("wf_on_asym", wf_on_not_sym RS swap); - -val prems = -Goal "[| wf[A](r); :r; ~P ==> :r; a:A; b:A |] ==> P"; -by (rtac ccontr 1); -by (rtac (wf_on_not_sym RS notE) 1); -by (DEPTH_SOLVE (ares_tac prems 1)); -qed "wf_on_asym"; +(* [| wf[A](r); ~Z ==> : r; + ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z *) +bind_thm ("wf_on_asym", permute_prems 1 2 (cla_make_elim wf_on_not_sym)); (*Needed to prove well_ordI. Could also reason that wf[A](r) means wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *) diff -r 2dbb80d4fdb7 -r 422968aeed49 src/ZF/func.ML --- a/src/ZF/func.ML Wed Jun 28 10:56:01 2000 +0200 +++ b/src/ZF/func.ML Wed Jun 28 10:56:34 2000 +0200 @@ -142,14 +142,9 @@ by (assume_tac 1); qed "range_type"; -val prems = Goal - "[| : f; f: Pi(A,B); \ -\ [| a:A; b:B(a); f`a = b |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac prems 1); -by (resolve_tac prems 1); -by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1)); -qed "Pair_mem_PiE"; +Goal "[| : f; f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b"; +by (blast_tac (claset() addIs [domain_type, range_type, apply_equality]) 1); +qed "Pair_mem_PiD"; (*** Lambda Abstraction ***)