# HG changeset patch
# User hoelzl
# Date 1384280935 -3600
# Node ID eaf25431d4c427b680671afd5628b42bbf4dbb52
# Parent  72949fae4f817e4ace0556c5717481ba8b70ee28
enat is countable

diff -r 72949fae4f81 -r eaf25431d4c4 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Tue Nov 12 19:28:54 2013 +0100
+++ b/src/HOL/Library/Extended_Nat.thy	Tue Nov 12 19:28:55 2013 +0100
@@ -6,7 +6,7 @@
 header {* Extended natural numbers (i.e. with infinity) *}
 
 theory Extended_Nat
-imports Main
+imports Main Countable
 begin
 
 class infinity =
@@ -26,7 +26,9 @@
 *}
 
 typedef enat = "UNIV :: nat option set" ..
- 
+
+text {* TODO: introduce enat as coinductive datatype, enat is just of_nat *}
+
 definition enat :: "nat \<Rightarrow> enat" where
   "enat n = Abs_enat (Some n)"
  
@@ -35,6 +37,12 @@
   definition "\<infinity> = Abs_enat None"
   instance proof qed
 end
+
+instance enat :: countable
+proof
+  show "\<exists>to_nat::enat \<Rightarrow> nat. inj to_nat"
+    by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
+qed
  
 rep_datatype enat "\<infinity> :: enat"
 proof -
@@ -555,7 +563,6 @@
 
 text {* TODO: add simprocs for combining and cancelling numerals *}
 
-
 subsection {* Well-ordering *}
 
 lemma less_enatE:
@@ -596,6 +603,8 @@
 
 subsection {* Complete Lattice *}
 
+text {* TODO: enat as order topology? *}
+
 instantiation enat :: complete_lattice
 begin