src/HOL/Library/Nat_Infinity.thy
changeset 29337 450805a4a91f
parent 29023 ef3adebc6d98
child 29652 f4c6e546b7fe
child 29667 53103fc8ffa3
--- 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 *}