equal
deleted
inserted
replaced
107 lemma Limit_nat [iff]: "Limit(nat)" |
107 lemma Limit_nat [iff]: "Limit(nat)" |
108 apply (unfold Limit_def) |
108 apply (unfold Limit_def) |
109 apply (safe intro!: ltI Ord_nat) |
109 apply (safe intro!: ltI Ord_nat) |
110 apply (erule ltD) |
110 apply (erule ltD) |
111 done |
111 done |
|
112 |
|
113 lemma naturals_not_limit: "a \<in> nat ==> ~ Limit(a)" |
|
114 by (induct a rule: nat_induct, auto) |
112 |
115 |
113 lemma succ_natD [dest!]: "succ(i): nat ==> i: nat" |
116 lemma succ_natD [dest!]: "succ(i): nat ==> i: nat" |
114 by (rule Ord_trans [OF succI1], auto) |
117 by (rule Ord_trans [OF succI1], auto) |
115 |
118 |
116 lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat" |
119 lemma nat_succ_iff [iff]: "succ(n): nat <-> n: nat" |