src/ZF/ord.ML
changeset 186 320f6bdb593a
parent 37 cebe01deba80
equal deleted inserted replaced
185:b63888ea0b28 186:320f6bdb593a
   154 val Ord_succ = result();
   154 val Ord_succ = result();
   155 
   155 
   156 goal Ord.thy "Ord(succ(i)) <-> Ord(i)";
   156 goal Ord.thy "Ord(succ(i)) <-> Ord(i)";
   157 by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
   157 by (fast_tac (ZF_cs addIs [Ord_succ] addDs [Ord_succD]) 1);
   158 val Ord_succ_iff = result();
   158 val Ord_succ_iff = result();
       
   159 
       
   160 goalw Ord.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Un j)";
       
   161 by (fast_tac (ZF_cs addSIs [Transset_Un]) 1);
       
   162 val Ord_Un = result();
       
   163 
       
   164 goalw Ord.thy [Ord_def] "!!i j. [| Ord(i); Ord(j) |] ==> Ord(i Int j)";
       
   165 by (fast_tac (ZF_cs addSIs [Transset_Int]) 1);
       
   166 val Ord_Int = result();
   159 
   167 
   160 val nonempty::prems = goal Ord.thy
   168 val nonempty::prems = goal Ord.thy
   161     "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
   169     "[| j:A;  !!i. i:A ==> Ord(i) |] ==> Ord(Inter(A))";
   162 by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
   170 by (rtac (nonempty RS Transset_Inter_family RS OrdI) 1);
   163 by (rtac Ord_is_Transset 1);
   171 by (rtac Ord_is_Transset 1);
   441 by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1));
   449 by (REPEAT (ares_tac [iffI,succ_leI,succ_leE] 1));
   442 val succ_le_iff = result();
   450 val succ_le_iff = result();
   443 
   451 
   444 (** Union and Intersection **)
   452 (** Union and Intersection **)
   445 
   453 
       
   454 goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> i le i Un j";
       
   455 by (rtac (Un_upper1 RS subset_imp_le) 1);
       
   456 by (REPEAT (ares_tac [Ord_Un] 1));
       
   457 val Un_upper1_le = result();
       
   458 
       
   459 goal Ord.thy "!!i j. [| Ord(i); Ord(j) |] ==> j le i Un j";
       
   460 by (rtac (Un_upper2 RS subset_imp_le) 1);
       
   461 by (REPEAT (ares_tac [Ord_Un] 1));
       
   462 val Un_upper2_le = result();
       
   463 
   446 (*Replacing k by succ(k') yields the similar rule for le!*)
   464 (*Replacing k by succ(k') yields the similar rule for le!*)
   447 goal Ord.thy "!!i j k. [| i<k;  j<k |] ==> i Un j < k";
   465 goal Ord.thy "!!i j k. [| i<k;  j<k |] ==> i Un j < k";
   448 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
   466 by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1);
   449 by (rtac (Un_commute RS ssubst) 4);
   467 by (rtac (Un_commute RS ssubst) 4);
   450 by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4);
   468 by (asm_full_simp_tac (ZF_ss addsimps [le_subset_iff, subset_Un_iff]) 4);