src/ZF/Ordinal.ML
changeset 2717 b29c45ef3d86
parent 2493 bdeb5024353a
child 2925 b0ae2e13db93
equal deleted inserted replaced
2716:9e11a914156a 2717:b29c45ef3d86
    85 qed "Transset_Inter_family";
    85 qed "Transset_Inter_family";
    86 
    86 
    87 (*** Natural Deduction rules for Ord ***)
    87 (*** Natural Deduction rules for Ord ***)
    88 
    88 
    89 val prems = goalw Ordinal.thy [Ord_def]
    89 val prems = goalw Ordinal.thy [Ord_def]
    90     "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i) ";
    90     "[| Transset(i);  !!x. x:i ==> Transset(x) |]  ==>  Ord(i)";
    91 by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
    91 by (REPEAT (ares_tac (prems@[ballI,conjI]) 1));
    92 qed "OrdI";
    92 qed "OrdI";
    93 
    93 
    94 val [major] = goalw Ordinal.thy [Ord_def]
    94 val [major] = goalw Ordinal.thy [Ord_def]
    95     "Ord(i) ==> Transset(i)";
    95     "Ord(i) ==> Transset(i)";
   621 by (REPEAT (eresolve_tac [asm_rl, leprem RS ltE] 1
   621 by (REPEAT (eresolve_tac [asm_rl, leprem RS ltE] 1
   622      ORELSE dtac Ord_succD 1));
   622      ORELSE dtac Ord_succD 1));
   623 qed "le_implies_UN_le_UN";
   623 qed "le_implies_UN_le_UN";
   624 
   624 
   625 goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
   625 goal Ordinal.thy "!!i. Ord(i) ==> (UN y:i. succ(y)) = i";
   626 by (fast_tac (!claset addEs [Ord_trans]) 1);
   626 by (best_tac (!claset addEs [Ord_trans]) 1);
   627 qed "Ord_equality";
   627 qed "Ord_equality";
   628 
   628 
   629 (*Holds for all transitive sets, not just ordinals*)
   629 (*Holds for all transitive sets, not just ordinals*)
   630 goal Ordinal.thy "!!i. Ord(i) ==> Union(i) <= i";
   630 goal Ordinal.thy "!!i. Ord(i) ==> Union(i) <= i";
   631 by (fast_tac (!claset addSEs [Ord_trans]) 1);
   631 by (fast_tac (!claset addSEs [Ord_trans]) 1);