src/ZF/Nat.ML
changeset 829 ba28811c3496
parent 760 f0200e91b272
child 1461 6bcb44e4d6e5
equal deleted inserted replaced
828:03d7bfa70289 829:ba28811c3496
    33 
    33 
    34 goal Nat.thy "1 : nat";
    34 goal Nat.thy "1 : nat";
    35 by (rtac (nat_0I RS nat_succI) 1);
    35 by (rtac (nat_0I RS nat_succI) 1);
    36 qed "nat_1I";
    36 qed "nat_1I";
    37 
    37 
       
    38 goal Nat.thy "2 : nat";
       
    39 by (rtac (nat_1I RS nat_succI) 1);
       
    40 qed "nat_2I";
       
    41 
    38 goal Nat.thy "bool <= nat";
    42 goal Nat.thy "bool <= nat";
    39 by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
    43 by (REPEAT (ares_tac [subsetI,nat_0I,nat_1I] 1
    40 	    ORELSE eresolve_tac [boolE,ssubst] 1));
    44 	    ORELSE eresolve_tac [boolE,ssubst] 1));
    41 qed "bool_subset_nat";
    45 qed "bool_subset_nat";
    42 
    46 
    72 
    76 
    73 (* i: nat ==> 0 le i *)
    77 (* i: nat ==> 0 le i *)
    74 val nat_0_le = nat_into_Ord RS Ord_0_le;
    78 val nat_0_le = nat_into_Ord RS Ord_0_le;
    75 
    79 
    76 val nat_le_refl = nat_into_Ord RS le_refl;
    80 val nat_le_refl = nat_into_Ord RS le_refl;
    77 
       
    78 goal Nat.thy "!!n. n: nat ==> n=0 | 0:n";
       
    79 by (etac nat_induct 1);
       
    80 by (fast_tac ZF_cs 1);
       
    81 by (fast_tac (ZF_cs addIs [nat_0_le]) 1);
       
    82 qed "natE0";
       
    83 
    81 
    84 goal Nat.thy "Ord(nat)";
    82 goal Nat.thy "Ord(nat)";
    85 by (rtac OrdI 1);
    83 by (rtac OrdI 1);
    86 by (etac (nat_into_Ord RS Ord_is_Transset) 2);
    84 by (etac (nat_into_Ord RS Ord_is_Transset) 2);
    87 by (rewtac Transset_def);
    85 by (rewtac Transset_def);