--- a/src/HOL/Library/Nat_Infinity.thy Sat Jan 03 08:36:20 2009 +0100
+++ b/src/HOL/Library/Nat_Infinity.thy Sat Jan 03 08:36:46 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Library/Nat_Infinity.thy
- ID: $Id$
Author: David von Oheimb, TU Muenchen; Florian Haftmann, TU Muenchen
*)
@@ -9,6 +8,17 @@
imports Plain "~~/src/HOL/Presburger"
begin
+text {* FIXME: move to Nat.thy *}
+
+instantiation nat :: bot
+begin
+
+definition bot_nat :: nat where
+ "bot_nat = 0"
+
+instance proof
+qed (simp add: bot_nat_def)
+
subsection {* Type definition *}
text {*
@@ -16,6 +26,8 @@
infinity.
*}
+end
+
datatype inat = Fin nat | Infty
notation (xsymbols)
@@ -353,6 +365,20 @@
apply (erule (1) le_less_trans)
done
+instantiation inat :: "{bot, top}"
+begin
+
+definition bot_inat :: inat where
+ "bot_inat = 0"
+
+definition top_inat :: inat where
+ "top_inat = \<infinity>"
+
+instance proof
+qed (simp_all add: bot_inat_def top_inat_def)
+
+end
+
subsection {* Well-ordering *}