--- a/src/ZF/Nat.thy Mon May 26 18:36:15 2003 +0200
+++ b/src/ZF/Nat.thy Tue May 27 11:39:03 2003 +0200
@@ -38,12 +38,13 @@
Gt :: i
"Gt == {<x,y>:nat*nat. y < x}"
- less_than :: "i=>i"
- "less_than(n) == {i:nat. i<n}"
-
greater_than :: "i=>i"
"greater_than(n) == {i:nat. n < i}"
+text{*No need for a less-than operator: a natural number is its list of
+predecessors!*}
+
+
lemma nat_bnd_mono: "bnd_mono(Inf, %X. {0} Un {succ(i). i:X})"
apply (rule bnd_monoI)
apply (cut_tac infinity, blast, blast)
@@ -281,6 +282,14 @@
lemma nat_nonempty [simp]: "nat ~= 0"
by blast
+text{*A natural number is the set of its predecessors*}
+lemma nat_eq_Collect_lt: "i \<in> nat ==> {j\<in>nat. j<i} = i"
+apply (rule equalityI)
+apply (blast dest: ltD)
+apply (auto simp add: Ord_mem_iff_lt)
+apply (blast intro: lt_trans)
+done
+
ML
{*
@@ -288,7 +297,6 @@
val Lt_def = thm "Lt_def";
val Ge_def = thm "Ge_def";
val Gt_def = thm "Gt_def";
-val less_than_def = thm "less_than_def";
val greater_than_def = thm "greater_than_def";
val nat_bnd_mono = thm "nat_bnd_mono";