tidied
authorpaulson
Tue, 15 Sep 1998 10:40:40 +0200
changeset 5488 9df083aed63d
parent 5487 ff11f8b364ef
child 5489 15c97b95b3e3
tidied
src/ZF/CardinalArith.ML
src/ZF/Order.ML
src/ZF/OrderArith.ML
src/ZF/upair.ML
--- a/src/ZF/CardinalArith.ML	Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/CardinalArith.ML	Tue Sep 15 10:40:40 1998 +0200
@@ -21,8 +21,7 @@
 by (rtac exI 1);
 by (res_inst_tac [("c", "case(Inr, Inl)"), ("d", "case(Inr, Inl)")] 
     lam_bijective 1);
-by (safe_tac (claset() addSEs [sumE]));
-by (ALLGOALS (Asm_simp_tac));
+by Auto_tac;
 qed "sum_commute_eqpoll";
 
 Goalw [cadd_def] "i |+| j = j |+| i";
@@ -272,7 +271,7 @@
 by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"), 
                   ("d", "case(%y. <A,y>, %z. z)")] 
     lam_bijective 1);
-by (safe_tac (claset() addSEs [sumE]));
+by Safe_tac;
 by (ALLGOALS
     (asm_simp_tac (simpset() addsimps [succI2, if_type, mem_imp_not_eq])));
 qed "prod_succ_eqpoll";
@@ -390,14 +389,12 @@
 
 (** Establishing the well-ordering **)
 
-Goalw [inj_def]
- "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)";
-by (fast_tac (claset() addss (simpset())
-                       addIs [lam_type, Un_least_lt RS ltD, ltI]) 1);
+Goalw [inj_def] "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)";
+by (force_tac (claset() addIs [lam_type, Un_least_lt RS ltD, ltI],
+	       simpset()) 1);
 qed "csquare_lam_inj";
 
-Goalw [csquare_rel_def]
- "Ord(K) ==> well_ord(K*K, csquare_rel(K))";
+Goalw [csquare_rel_def] "Ord(K) ==> well_ord(K*K, csquare_rel(K))";
 by (rtac (csquare_lam_inj RS well_ord_rvimage) 1);
 by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
 qed "well_ord_csquare";
@@ -405,22 +402,21 @@
 (** Characterising initial segments of the well-ordering **)
 
 Goalw [csquare_rel_def]
- "[| x<K;  y<K;  z<K |] ==> \
-\      <<x,y>, <z,z>> : csquare_rel(K) --> x le z & y le z";
+ "[| <<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,
 				      Un_absorb, Un_least_mem_iff, ltD]) 1);
 by (safe_tac (claset() addSEs [mem_irrefl] 
                        addSIs [Un_upper1_le, Un_upper2_le]));
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2, Ord_succ])));
-qed_spec_mp "csquareD";
+qed "csquareD";
 
 Goalw [pred_def]
  "z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
-by (safe_tac (claset_of ZF.thy addSEs [SigmaE]));  (*avoids using succCI,...*)
-by (rtac (csquareD RS conjE) 1);
+by (safe_tac (claset() delrules [SigmaI,succCI]));  (*avoids using succCI,...*)
+by (etac (csquareD RS conjE) 1);
 by (rewtac lt_def);
-by (assume_tac 4);
 by (ALLGOALS Blast_tac);
 qed "pred_csquare_subset";
 
--- a/src/ZF/Order.ML	Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/Order.ML	Tue Sep 15 10:40:40 1998 +0200
@@ -504,7 +504,7 @@
 by (asm_simp_tac 
     (simpset() addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
 by (rewtac ord_iso_map_def);
-by (safe_tac (claset() addSEs [UN_E]));
+by Safe_tac;
 by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac);
 qed "ord_iso_map_mono_map";
 
--- a/src/ZF/OrderArith.ML	Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/OrderArith.ML	Tue Sep 15 10:40:40 1998 +0200
@@ -83,7 +83,7 @@
 by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
 by (best_tac (claset() addSEs [raddE, bspec RS mp]) 2);
 (*Returning to main part of proof*)
-by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
+by Safe_tac;
 by (Blast_tac 1);
 by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
 by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1);
--- a/src/ZF/upair.ML	Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/upair.ML	Tue Sep 15 10:40:40 1998 +0200
@@ -223,7 +223,7 @@
 (*If it's "undefined", it's zero!*)
 qed_goalw "the_0" thy [the_def]
     "!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
- (fn _ => [ (deepen_tac (claset() addSEs [ReplaceE]) 0 1) ]);
+ (fn _ => [ (blast_tac (claset() addSEs [ReplaceE]) 1) ]);
 
 
 (*** if -- a conditional expression for formulae ***)