src/ZF/OrderType.ML
changeset 771 067767b0b35e
parent 760 f0200e91b272
child 782 200a16083201
equal deleted inserted replaced
770:216ec1299bf0 771:067767b0b35e
   215 		  [well_ord_is_wf RS ordermap_pred_unfold]) 1);
   215 		  [well_ord_is_wf RS ordermap_pred_unfold]) 1);
   216 by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold,
   216 by (asm_simp_tac (ZF_ss addsimps [ordertype_unfold,
   217 				  ordermap_pred_eq_ordermap]) 1);
   217 				  ordermap_pred_eq_ordermap]) 1);
   218 qed "ordertype_subset";
   218 qed "ordertype_subset";
   219 
   219 
       
   220 
       
   221 (*Kunen's Theorem 7.3 (i), page 16;  see also Ordinal/Ord_in_Ord
       
   222   The smaller ordinal is an initial segment of the larger *)
       
   223 goalw OrderType.thy [pred_def, lt_def]
       
   224     "!!i j. j<i ==> j = pred(i, j, Memrel(i))";
       
   225 by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
       
   226 by (fast_tac (eq_cs addEs [Ord_trans]) 1);
       
   227 val lt_eq_pred = result();
       
   228 
       
   229 goal OrderType.thy
       
   230     "!!i. [| j<i;  f: ord_iso(i,Memrel(i),j,Memrel(j))	\
       
   231 \         |] ==> R";
       
   232 by (forward_tac [lt_eq_pred] 1);
       
   233 be ltE 1;
       
   234 by (rtac (well_ord_Memrel RS not_well_ord_iso_pred RS notE) 1 THEN
       
   235     assume_tac 1 THEN assume_tac 1);
       
   236 be subst 1;
       
   237 by (asm_full_simp_tac (ZF_ss addsimps [ord_iso_def]) 1);
       
   238 (*Combining the two simplifications causes looping*)
       
   239 by (asm_simp_tac (ZF_ss addsimps [Memrel_iff]) 1);
       
   240 by (fast_tac (ZF_cs addSEs [bij_is_fun RS apply_type]  
       
   241                     addEs  [Ord_trans]) 1);
       
   242 val Ord_iso_implies_eq_lemma = result();
       
   243 
       
   244 (*Kunen's Theorem 7.3 (ii), page 16.  Isomorphic ordinals are equal*)
       
   245 goal OrderType.thy
       
   246     "!!i. [| Ord(i);  Ord(j);  f:  ord_iso(i,Memrel(i),j,Memrel(j))	\
       
   247 \         |] ==> i=j";
       
   248 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_lt 1);
       
   249 by (REPEAT (eresolve_tac [asm_rl, ord_iso_sym, Ord_iso_implies_eq_lemma] 1));
       
   250 val Ord_iso_implies_eq = result();