--- 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();