src/ZF/OrderType.ML

--- a/src/ZF/OrderType.ML	Thu Jun 23 16:44:57 1994 +0200
+++ b/src/ZF/OrderType.ML	Thu Jun 23 17:38:12 1994 +0200
@@ -9,8 +9,8 @@
 
 (*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
 goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
-br well_ordI 1;
-br (wf_Memrel RS wf_imp_wf_on) 1;
+by (rtac well_ordI 1);
+by (rtac (wf_Memrel RS wf_imp_wf_on) 1);
 by (asm_simp_tac (ZF_ss addsimps [linear_def, Memrel_iff]) 1);
 by (REPEAT (resolve_tac [ballI, Ord_linear] 1));;
 by (REPEAT (eresolve_tac [asm_rl, Ord_in_Ord] 1));;
@@ -18,28 +18,36 @@
 
 open OrderType;
 
+goalw OrderType.thy [ordermap_def,ordertype_def]
+    "ordermap(A,r) : A -> ordertype(A,r)";
+by (rtac lam_type 1);
+by (rtac (lamI RS imageI) 1);
+by (REPEAT (assume_tac 1));
+val ordermap_type = result();
+
 (** Unfolding of ordermap **)
 
+(*Useful for cardinality reasoning; see CardinalArith.ML*)
 goalw OrderType.thy [ordermap_def, pred_def]
     "!!r. [| wf[A](r);  x:A |] ==> \
+\         ordermap(A,r) ` x = ordermap(A,r) `` pred(A,x,r)";
+by (asm_simp_tac ZF_ss 1);
+by (etac (wfrec_on RS trans) 1);
+by (assume_tac 1);
+by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
+                                  vimage_singleton_iff]) 1);
+val ordermap_eq_image = result();
+
+goal OrderType.thy 
+    "!!r. [| wf[A](r);  x:A |] ==> \
 \         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
-by (asm_simp_tac ZF_ss 1);
-be (wfrec_on RS trans) 1;
-ba 1;
-by (asm_simp_tac (ZF_ss addsimps [subset_iff, image_lam,
-                                  vimage_singleton_iff]) 1);
+by (asm_simp_tac (ZF_ss addsimps [ordermap_eq_image, pred_subset, 
+				  ordermap_type RS image_fun]) 1);
 val ordermap_pred_unfold = result();
 
 (*pred-unfolded version.  NOT suitable for rewriting -- loops!*)
 val ordermap_unfold = rewrite_rule [pred_def] ordermap_pred_unfold;
 
-goalw OrderType.thy [ordermap_def,ordertype_def]
-    "ordermap(A,r) : A -> ordertype(A,r)";
-br lam_type 1;
-by (rtac (lamI RS imageI) 1);
-by (REPEAT (assume_tac 1));
-val ordermap_type = result();
-
 (** Showing that ordermap, ordertype yield ordinals **)
 
 fun ordermap_elim_tac i =
@@ -53,7 +61,7 @@
 by (wf_on_ind_tac "x" [] 1);
 by (asm_simp_tac (ZF_ss addsimps [ordermap_pred_unfold]) 1);
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
-bws [pred_def,Transset_def];
+by (rewrite_goals_tac [pred_def,Transset_def]);
 by (fast_tac ZF_cs 2);
 by (safe_tac ZF_cs);
 by (ordermap_elim_tac 1);
@@ -65,7 +73,7 @@
 by (rtac ([ordermap_type, subset_refl] MRS image_fun RS ssubst) 1);
 by (rtac (Ord_is_Transset RSN (2,OrdI)) 1);
 by (fast_tac (ZF_cs addIs [Ord_ordermap]) 2);
-bws [Transset_def,well_ord_def];
+by (rewrite_goals_tac [Transset_def,well_ord_def]);
 by (safe_tac ZF_cs);
 by (ordermap_elim_tac 1);
 by (fast_tac ZF_cs 1);
@@ -77,7 +85,7 @@
     "!!r. [| <w,x>: r;  wf[A](r);  w: A; x: A |] ==>	\
 \         ordermap(A,r)`w : ordermap(A,r)`x";
 by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
-ba 1;
+by (assume_tac 1);
 by (fast_tac ZF_cs 1);
 val less_imp_ordermap_in = result();
 
@@ -88,10 +96,10 @@
 by (safe_tac ZF_cs);
 by (linear_case_tac 1);
 by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
-bd less_imp_ordermap_in 1;
+by (dtac less_imp_ordermap_in 1);
 by (REPEAT_SOME assume_tac);
-be mem_anti_sym 1;
-ba 1;
+by (etac mem_asym 1);
+by (assume_tac 1);
 val ordermap_in_imp_less = result();
 
 val ordermap_surj = 
@@ -102,8 +110,8 @@
 goalw OrderType.thy [well_ord_def, tot_ord_def, bij_def, inj_def]
     "!!r. well_ord(A,r) ==> ordermap(A,r) : bij(A, ordertype(A,r))";
 by (safe_tac ZF_cs);
-br ordermap_type 1;
-br ordermap_surj 2;
+by (rtac ordermap_type 1);
+by (rtac ordermap_surj 2);
 by (linear_case_tac 1);
 (*The two cases yield similar contradictions*)
 by (ALLGOALS (dtac less_imp_ordermap_in));
@@ -115,10 +123,10 @@
  "!!r. well_ord(A,r) ==> \
 \      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
 by (safe_tac ZF_cs);
-br ordertype_bij 1;
-ba 1;
+by (rtac ordertype_bij 1);
+by (assume_tac 1);
 by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2);
-bw well_ord_def;
+by (rewtac well_ord_def);
 by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in,
 			    ordermap_type RS apply_type]) 1);
 val ordertype_ord_iso = result();