--- a/src/ZF/Cardinal.ML Tue Sep 05 10:16:03 2000 +0200
+++ b/src/ZF/Cardinal.ML Tue Sep 05 12:29:06 2000 +0200
@@ -771,7 +771,7 @@
by (etac nat_induct 1);
by (blast_tac (claset() addIs [wf_onI]) 1);
by (rtac wf_onI 1);
-by (asm_full_simp_tac (simpset() addsimps [wf_on_def, wf_def, Memrel_iff]) 1);
+by (asm_full_simp_tac (simpset() addsimps [wf_on_def, wf_def]) 1);
by (excluded_middle_tac "x:Z" 1);
by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2);
by (blast_tac (claset() addEs [mem_irrefl, mem_asym]) 2);
--- a/src/ZF/CardinalArith.ML Tue Sep 05 10:16:03 2000 +0200
+++ b/src/ZF/CardinalArith.ML Tue Sep 05 12:29:06 2000 +0200
@@ -397,7 +397,7 @@
"[| <<x,y>, <z,z>> : csquare_rel(K); x<K; y<K; z<K |] ==> x le z & y le z";
by (etac rev_mp 1);
by (REPEAT (etac ltE 1));
-by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff,
+by (asm_simp_tac (simpset() addsimps [rvimage_iff,
Un_absorb, Un_least_mem_iff, ltD]) 1);
by (safe_tac (claset() addSEs [mem_irrefl]
addSIs [Un_upper1_le, Un_upper2_le]));
@@ -417,7 +417,7 @@
by (subgoals_tac ["x<K", "y<K"] 1);
by (REPEAT (eresolve_tac [asm_rl, lt_trans] 2));
by (REPEAT (etac ltE 1));
-by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff,
+by (asm_simp_tac (simpset() addsimps [rvimage_iff,
Un_absorb, Un_least_mem_iff, ltD]) 1);
qed "csquare_ltI";
@@ -428,7 +428,7 @@
by (subgoals_tac ["x<K", "y<K"] 1);
by (REPEAT (eresolve_tac [asm_rl, lt_trans1] 2));
by (REPEAT (etac ltE 1));
-by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff,
+by (asm_simp_tac (simpset() addsimps [rvimage_iff,
Un_absorb, Un_least_mem_iff, ltD]) 1);
by (REPEAT_FIRST (etac succE));
by (ALLGOALS
--- a/src/ZF/Nat.ML Tue Sep 05 10:16:03 2000 +0200
+++ b/src/ZF/Nat.ML Tue Sep 05 12:29:06 2000 +0200
@@ -220,7 +220,7 @@
Goal "m: nat ==> nat_rec(succ(m),a,b) = b(m, nat_rec(m,a,b))";
by (rtac lemma 1);
-by (asm_simp_tac (simpset() addsimps [Memrel_iff, vimage_singleton_iff]) 1);
+by (asm_simp_tac (simpset() addsimps [vimage_singleton_iff]) 1);
qed "nat_rec_succ";
(** The union of two natural numbers is a natural number -- their maximum **)
--- a/src/ZF/OrderArith.ML Tue Sep 05 10:16:03 2000 +0200
+++ b/src/ZF/OrderArith.ML Tue Sep 05 12:29:06 2000 +0200
@@ -59,8 +59,8 @@
(** Linearity **)
-Addsimps [radd_Inl_iff, radd_Inr_iff,
- radd_Inl_Inr_iff, radd_Inr_Inl_iff];
+AddIffs [radd_Inl_iff, radd_Inr_iff,
+ radd_Inl_Inr_iff, radd_Inr_Inl_iff];
Goalw [linear_def]
"[| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))";
@@ -161,7 +161,7 @@
by (Blast_tac 1);
qed "rmult_iff";
-Addsimps [rmult_iff];
+AddIffs [rmult_iff];
val major::prems = Goal
"[| <<a',b'>, <a,b>> : rmult(A,r,B,s); \
@@ -225,8 +225,8 @@
(** An ord_iso congruence law **)
-Goal "[| f: bij(A,C); g: bij(B,D) |] ==> \
-\ (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
+Goal "[| f: bij(A,C); g: bij(B,D) |] \
+\ ==> (lam <x,y>:A*B. <f`x, g`y>) : bij(A*B, C*D)";
by (res_inst_tac [("d", "%<x,y>. <converse(f)`x, converse(g)`y>")]
lam_bijective 1);
by Safe_tac;
@@ -234,13 +234,12 @@
qed "prod_bij";
Goalw [ord_iso_def]
- "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] ==> \
-\ (lam <x,y>:A*B. <f`x, g`y>) \
-\ : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))";
+ "[| f: ord_iso(A,r,A',r'); g: ord_iso(B,s,B',s') |] \
+\ ==> (lam <x,y>:A*B. <f`x, g`y>) \
+\ : ord_iso(A*B, rmult(A,r,B,s), A'*B', rmult(A',r',B',s'))";
by (safe_tac (claset() addSIs [prod_bij]));
by (ALLGOALS
(asm_full_simp_tac (simpset() addsimps [bij_is_fun RS apply_type])));
-by (Blast_tac 1);
by (blast_tac (claset() addIs [bij_is_inj RS inj_apply_equality]) 1);
qed "prod_ord_iso_cong";
--- a/src/ZF/OrderType.ML Tue Sep 05 10:16:03 2000 +0200
+++ b/src/ZF/OrderType.ML Tue Sep 05 12:29:06 2000 +0200
@@ -16,7 +16,7 @@
by (rtac well_ordI 1);
by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
by (resolve_tac [prem RS ltE] 1);
-by (asm_simp_tac (simpset() addsimps [linear_def, Memrel_iff,
+by (asm_simp_tac (simpset() addsimps [linear_def,
[ltI, prem] MRS lt_trans2 RS ltD]) 1);
by (REPEAT (resolve_tac [ballI, Ord_linear] 1));
by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));
@@ -29,7 +29,7 @@
The smaller ordinal is an initial segment of the larger *)
Goalw [pred_def, lt_def]
"j<i ==> pred(i, j, Memrel(i)) = j";
-by (asm_simp_tac (simpset() addsimps [Memrel_iff]) 1);
+by (Asm_simp_tac 1);
by (blast_tac (claset() addIs [Ord_trans]) 1);
qed "lt_pred_Memrel";
@@ -43,15 +43,15 @@
by (etac ltE 1);
by (rtac (well_ord_Memrel RS well_ord_iso_predE) 1 THEN
assume_tac 3 THEN assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [ord_iso_def]) 1);
+by (rewtac ord_iso_def);
(*Combining the two simplifications causes looping*)
-by (asm_simp_tac (simpset() addsimps [Memrel_iff]) 1);
-by (fast_tac (claset() addSEs [bij_is_fun RS apply_type] addEs [Ord_trans]) 1);
+by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs [bij_is_fun RS apply_type, Ord_trans]) 1);
qed "Ord_iso_implies_eq_lemma";
(*Kunen's Theorem 7.3 (ii), page 16. Isomorphic ordinals are equal*)
-Goal "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) \
-\ |] ==> i=j";
+Goal "[| Ord(i); Ord(j); f: ord_iso(i,Memrel(i),j,Memrel(j)) |] \
+\ ==> i=j";
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
qed "Ord_iso_implies_eq";
@@ -194,7 +194,7 @@
by (rtac ord_iso_trans 1);
by (eresolve_tac [le_well_ord_Memrel RS ordertype_ord_iso] 2);
by (resolve_tac [id_bij RS ord_isoI] 1);
-by (asm_simp_tac (simpset() addsimps [id_conv, Memrel_iff]) 1);
+by (Asm_simp_tac 1);
by (fast_tac (claset() addEs [ltE, Ord_in_Ord, Ord_trans]) 1);
qed "le_ordertype_Memrel";
@@ -287,7 +287,7 @@
Goalw [Ord_alt_def, Ord_def, Transset_def, well_ord_def,
tot_ord_def, part_ord_def, trans_on_def]
"Ord_alt(i) ==> Ord(i)";
-by (asm_full_simp_tac (simpset() addsimps [Memrel_iff, pred_Memrel]) 1);
+by (asm_full_simp_tac (simpset() addsimps [pred_Memrel]) 1);
by (blast_tac (claset() addSEs [equalityE]) 1);
qed "Ord_alt_is_Ord";
@@ -307,7 +307,7 @@
Goal "well_ord(A,r) ==> ordertype(A+0, radd(A,r,0,s)) = ordertype(A,r)";
by (resolve_tac [bij_sum_0 RS ord_isoI RS ordertype_eq] 1);
by (assume_tac 2);
-by (fast_tac (claset() addss (simpset() addsimps [radd_Inl_iff, Memrel_iff])) 1);
+by (Force_tac 1);
qed "ordertype_sum_0_eq";
Goal "(lam z:0+A. case(%x. x, %y. y, z)) : bij(0+A, A)";
@@ -319,7 +319,7 @@
Goal "well_ord(A,r) ==> ordertype(0+A, radd(0,s,A,r)) = ordertype(A,r)";
by (resolve_tac [bij_0_sum RS ord_isoI RS ordertype_eq] 1);
by (assume_tac 2);
-by (fast_tac (claset() addss (simpset() addsimps [radd_Inr_iff, Memrel_iff])) 1);
+by (Force_tac 1);
qed "ordertype_0_sum_eq";
(** Initial segments of radd. Statements by Grabczewski **)
@@ -330,10 +330,7 @@
\ (lam x:pred(A,a,r). Inl(x)) \
\ : bij(pred(A,a,r), pred(A+B, Inl(a), radd(A,r,B,s)))";
by (res_inst_tac [("d", "case(%x. x, %y. y)")] lam_bijective 1);
-by Safe_tac;
-by (ALLGOALS
- (asm_full_simp_tac
- (simpset() addsimps [radd_Inl_iff, radd_Inr_Inl_iff])));
+by Auto_tac;
qed "pred_Inl_bij";
Goal "[| a:A; well_ord(A,r) |] ==> \
@@ -341,7 +338,7 @@
\ ordertype(pred(A,a,r), r)";
by (resolve_tac [pred_Inl_bij RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
by (REPEAT_FIRST (ares_tac [pred_subset, well_ord_subset]));
-by (asm_full_simp_tac (simpset() addsimps [radd_Inl_iff, pred_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [pred_def]) 1);
qed "ordertype_pred_Inl_eq";
Goalw [pred_def, id_def]
@@ -407,7 +404,7 @@
Goal "A<=B ==> id(A) : ord_iso(A, Memrel(A), A, Memrel(B))";
by (resolve_tac [id_bij RS ord_isoI] 1);
-by (asm_simp_tac (simpset() addsimps [id_conv, Memrel_iff]) 1);
+by (Asm_simp_tac 1);
by (Blast_tac 1);
qed "id_ord_iso_Memrel";
@@ -580,7 +577,7 @@
by (resolve_tac [bij_sum_Diff RS ord_isoI RS ord_iso_sym RS ordertype_eq] 1);
by (etac well_ord_Memrel 3);
by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [Memrel_iff]) 1);
+by (Asm_simp_tac 1);
by (forw_inst_tac [("j", "y")] Ord_in_Ord 1 THEN assume_tac 1);
by (forw_inst_tac [("j", "x")] Ord_in_Ord 1 THEN assume_tac 1);
by (asm_simp_tac (simpset() addsimps [Ord_mem_iff_lt, lt_Ord, not_lt_iff_le]) 1);
@@ -638,13 +635,12 @@
(*** A useful unfolding law ***)
Goalw [pred_def]
- "[| a:A; b:B |] ==> \
-\ pred(A*B, <a,b>, rmult(A,r,B,s)) = \
-\ pred(A,a,r)*B Un ({a} * pred(B,b,s))";
+ "[| a:A; b:B |] ==> pred(A*B, <a,b>, rmult(A,r,B,s)) = \
+\ pred(A,a,r)*B Un ({a} * pred(B,b,s))";
by (rtac equalityI 1);
by Safe_tac;
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [rmult_iff])));
-by (ALLGOALS (Blast_tac));
+by (ALLGOALS Asm_full_simp_tac);
+by (ALLGOALS Blast_tac);
qed "pred_Pair_eq";
Goal "[| a:A; b:B; well_ord(A,r); well_ord(B,s) |] ==> \
@@ -672,7 +668,7 @@
by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, ltE, ssubst]));
by (REPEAT_FIRST (ares_tac [well_ord_rmult, well_ord_radd, well_ord_Memrel,
Ord_ordertype]));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Memrel_iff])));
+by (ALLGOALS Asm_simp_tac);
by Safe_tac;
by (ALLGOALS (blast_tac (claset() addIs [Ord_trans])));
qed "ordertype_pred_Pair_lemma";
@@ -734,7 +730,7 @@
by (res_inst_tac [("c", "snd"), ("d", "%z.<0,z>")] lam_bijective 1);
by (REPEAT_FIRST (eresolve_tac [snd_type, SigmaE, succE, emptyE,
well_ord_Memrel, ordertype_Memrel]));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [rmult_iff, Memrel_iff])));
+by (ALLGOALS Asm_simp_tac);
qed "omult_1";
Goalw [omult_def] "Ord(i) ==> 1**i = i";
@@ -742,7 +738,7 @@
by (res_inst_tac [("c", "fst"), ("d", "%z.<z,0>")] lam_bijective 1);
by (REPEAT_FIRST (eresolve_tac [fst_type, SigmaE, succE, emptyE,
well_ord_Memrel, ordertype_Memrel]));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [rmult_iff, Memrel_iff])));
+by (ALLGOALS Asm_simp_tac);
qed "omult_1_left";
Addsimps [omult_1, omult_1_left];
--- a/src/ZF/Ordinal.ML Tue Sep 05 10:16:03 2000 +0200
+++ b/src/ZF/Ordinal.ML Tue Sep 05 12:29:06 2000 +0200
@@ -302,9 +302,11 @@
Goalw [Memrel_def] "<a,b> : Memrel(A) <-> a:b & a:A & b:A";
by (Blast_tac 1);
qed "Memrel_iff";
+Addsimps [Memrel_iff];
+ (*MemrelI/E give better speed than AddIffs here*)
Goal "[| a: b; a: A; b: A |] ==> <a,b> : Memrel(A)";
-by (REPEAT (ares_tac [conjI, Memrel_iff RS iffD2] 1));
+by Auto_tac;
qed "MemrelI";
val [major,minor] = Goal