src/ZF/OrderType.ML

--- a/src/ZF/OrderType.ML	Tue Jul 12 14:26:04 1994 +0200
+++ b/src/ZF/OrderType.ML	Tue Jul 12 18:05:03 1994 +0200
@@ -7,15 +7,6 @@
 *)
 
 
-(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
-goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
-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));;
-val well_ord_Memrel = result();
-
 open OrderType;
 
 goalw OrderType.thy [ordermap_def,ordertype_def]
@@ -38,6 +29,7 @@
                                   vimage_singleton_iff]) 1);
 val ordermap_eq_image = result();
 
+(*Useful for rewriting PROVIDED pred is not unfolded until later!*)
 goal OrderType.thy 
     "!!r. [| wf[A](r);  x:A |] ==> \
 \         ordermap(A,r) ` x = {ordermap(A,r)`y . y : pred(A,x,r)}";
@@ -87,7 +79,7 @@
 by (eres_inst_tac [("x1", "x")] (ordermap_unfold RS ssubst) 1);
 by (assume_tac 1);
 by (fast_tac ZF_cs 1);
-val less_imp_ordermap_in = result();
+val ordermap_mono = result();
 
 (*linearity of r is crucial here*)
 goalw OrderType.thy [well_ord_def, tot_ord_def]
@@ -96,11 +88,11 @@
 by (safe_tac ZF_cs);
 by (linear_case_tac 1);
 by (fast_tac (ZF_cs addSEs [mem_not_refl RS notE]) 1);
-by (dtac less_imp_ordermap_in 1);
+by (dtac ordermap_mono 1);
 by (REPEAT_SOME assume_tac);
 by (etac mem_asym 1);
 by (assume_tac 1);
-val ordermap_in_imp_less = result();
+val converse_ordermap_mono = result();
 
 val ordermap_surj = 
     (ordermap_type RS surj_image) |>
@@ -114,20 +106,20 @@
 by (rtac ordermap_surj 2);
 by (linear_case_tac 1);
 (*The two cases yield similar contradictions*)
-by (ALLGOALS (dtac less_imp_ordermap_in));
+by (ALLGOALS (dtac ordermap_mono));
 by (REPEAT_SOME assume_tac);
 by (ALLGOALS (asm_full_simp_tac (ZF_ss addsimps [mem_not_refl])));
-val ordertype_bij = result();
+val ordermap_bij = result();
 
 goalw OrderType.thy [ord_iso_def]
  "!!r. well_ord(A,r) ==> \
 \      ordermap(A,r) : ord_iso(A,r, ordertype(A,r), Memrel(ordertype(A,r)))";
 by (safe_tac ZF_cs);
-by (rtac ordertype_bij 1);
+by (rtac ordermap_bij 1);
 by (assume_tac 1);
-by (fast_tac (ZF_cs addSEs [MemrelE, ordermap_in_imp_less]) 2);
+by (fast_tac (ZF_cs addSEs [MemrelE, converse_ordermap_mono]) 2);
 by (rewtac well_ord_def);
-by (fast_tac (ZF_cs addSIs [MemrelI, less_imp_ordermap_in,
+by (fast_tac (ZF_cs addSIs [MemrelI, ordermap_mono,
 			    ordermap_type RS apply_type]) 1);
 val ordertype_ord_iso = result();
 
@@ -138,3 +130,90 @@
     "ordertype(A,r) = {ordermap(A,r)`y . y : A}";
 by (rtac ([ordermap_type, subset_refl] MRS image_fun) 1);
 val ordertype_unfold = result();
+
+
+(** Ordertype of Memrel **)
+
+(*Requires Ordinal.thy as parent; otherwise could be in Order.ML*)
+goal OrderType.thy "!!i. Ord(i) ==> well_ord(i, Memrel(i))";
+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));;
+val well_ord_Memrel = result();
+
+goal OrderType.thy "!!i. [| Ord(i);  j:i |] ==> ordermap(i,Memrel(i)) ` j = j";
+by (eresolve_tac [Ord_induct] 1);
+ba 1;
+by (asm_simp_tac (ZF_ss addsimps
+	     [well_ord_Memrel RS well_ord_is_wf RS ordermap_pred_unfold]) 1);
+by (asm_simp_tac (ZF_ss addsimps [pred_def, Memrel_iff]) 1);
+by (dresolve_tac [OrdmemD] 1);
+by (assume_tac 1);
+by (fast_tac eq_cs 1);
+val ordermap_Memrel = result();
+
+goal OrderType.thy "!!i. Ord(i) ==> ordertype(i,Memrel(i)) = i";
+by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, ordermap_Memrel]) 1);
+val ordertype_Memrel = result();
+
+(** Ordertype of rvimage **)
+
+goal OrderType.thy
+    "!!f. [| f: bij(A,B);  well_ord(B,r);  x:A |] ==>	\
+\         ordermap(A,rvimage(A,f,r)) ` x = ordermap(B,r) ` (f`x)";
+by (metacut_tac well_ord_rvimage 1 THEN 
+    etac bij_is_inj 2 THEN assume_tac 2);
+by (res_inst_tac [("A","A"), ("a","x")] wf_on_induct 1 THEN
+    REPEAT (ares_tac [well_ord_is_wf] 1));
+by (asm_simp_tac
+    (bij_inverse_ss addsimps [ordermap_pred_unfold, well_ord_is_wf]) 1);
+by (asm_simp_tac (ZF_ss addsimps [pred_def, rvimage_iff]) 1);
+by (safe_tac eq_cs);
+by (fast_tac bij_apply_cs 1);
+by (res_inst_tac [("a", "converse(f)`xb")] RepFun_eqI 1);
+by (ALLGOALS (asm_simp_tac bij_inverse_ss));
+val bij_ordermap_vimage = result();
+
+goal OrderType.thy
+    "!!f. [| f: bij(A,B);  well_ord(B,r) |] ==>	\
+\    ordertype(A,rvimage(A,f,r)) = ordertype(B,r)";
+by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold, bij_ordermap_vimage]) 1);
+by (safe_tac eq_cs);
+by (fast_tac bij_apply_cs 1);
+by (res_inst_tac [("a", "converse(f)`xa")] RepFun_eqI 1);
+by (ALLGOALS (asm_simp_tac bij_inverse_ss));
+val bij_ordertype_vimage = result();
+
+
+goal OrderType.thy
+    "!!r. [| well_ord(A,r);  y:A;  z: pred(A,y,r) |] ==>	\
+\	  ordermap(pred(A,y,r), r) ` z = ordermap(A, r) ` z";
+by (forward_tac [[well_ord_is_wf, pred_subset] MRS wf_on_subset_A] 1);
+by (wf_on_ind_tac "z" [] 1);
+by (safe_tac (ZF_cs addSEs [predE]));
+by (asm_simp_tac
+    (ZF_ss addsimps [ordermap_pred_unfold, well_ord_is_wf, pred_iff]) 1);
+(*combining these two simplifications LOOPS! *)
+by (asm_simp_tac (ZF_ss addsimps [pred_pred_eq]) 1);
+by (asm_full_simp_tac (ZF_ss addsimps [pred_def]) 1);
+br (refl RSN (2,RepFun_cong)) 1;
+bd well_ord_is_trans_on 1;
+by (fast_tac (eq_cs addSEs [trans_onD]) 1);
+val ordermap_pred_eq_ordermap = result();
+
+
+goal OrderType.thy
+    "!!r. [| well_ord(A,r);  i: ordertype(A,r) |] ==>	\
+\	  EX B. B<=A & i = ordertype(B,r)";
+by (dresolve_tac [ordertype_unfold RS equalityD1 RS subsetD] 1);
+by (res_inst_tac [("x", "pred(A, converse(ordermap(A,r))`i, r)")]  exI  1);
+by (safe_tac (ZF_cs addSEs [predE]));
+by (asm_simp_tac (ZF_ss addsimps [ordermap_bij RS left_inverse_bij]) 1);
+by (asm_simp_tac (ZF_ss addsimps
+		  [well_ord_is_wf RS ordermap_pred_unfold]) 1);
+by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold,
+				  ordermap_pred_eq_ordermap]) 1);
+val ordertype_subset = result();
+