src/ZF/AC/AC_Equiv.ML
changeset 1037 03063caa960a
parent 991 547931cbbf08
child 1057 5097aa914449
equal deleted inserted replaced
1036:0d28f4bc8a44 1037:03063caa960a
    95 by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] 
    95 by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] 
    96     (rvimage_id RS subst) 1);
    96     (rvimage_id RS subst) 1);
    97 by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1);
    97 by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1);
    98 val ordertype_Int = result();
    98 val ordertype_Int = result();
    99 
    99 
   100 (* used only in WO6WO1.ML *)
       
   101 (* corrected according to LCP'a advise *)
       
   102 goal Cardinal.thy 
       
   103       "!!i j k. [| k < i++j; Ord(i); Ord(j) |] ==>  \
       
   104 \                  k<i | (EX! l. l<j & k = i++l)";
       
   105 by (dresolve_tac [lt_oadd_disj] 1 THEN (REPEAT (atac 1)));
       
   106 by (fast_tac (ZF_cs addIs [ex1I, ltI] addSEs [oadd_inject RS sym, lt_Ord]
       
   107 		addEs [Ord_in_Ord]) 1);
       
   108 val lt_oadd_disj1 = result();
       
   109 
       
   110 (* used only in AC16_lemmas.ML *)
   100 (* used only in AC16_lemmas.ML *)
   111 goalw CardinalArith.thy [InfCard_def]
   101 goalw CardinalArith.thy [InfCard_def]
   112 	"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";
   102 	"!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)";
   113 by (asm_simp_tac (ZF_ss addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1);
   103 by (asm_simp_tac (ZF_ss addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1);
   114 val Inf_Card_is_InfCard = result();
   104 val Inf_Card_is_InfCard = result();