enat is countable
authorhoelzl
Tue Nov 12 19:28:55 2013 +0100 (2013-11-12)
changeset 54415eaf25431d4c4
parent 54414 72949fae4f81
child 54416 7fb88ed6ff3c
enat is countable
src/HOL/Library/Extended_Nat.thy
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Nov 12 19:28:54 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Nov 12 19:28:55 2013 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Extended natural numbers (i.e. with infinity) *}
     1.5  
     1.6  theory Extended_Nat
     1.7 -imports Main
     1.8 +imports Main Countable
     1.9  begin
    1.10  
    1.11  class infinity =
    1.12 @@ -26,7 +26,9 @@
    1.13  *}
    1.14  
    1.15  typedef enat = "UNIV :: nat option set" ..
    1.16 - 
    1.17 +
    1.18 +text {* TODO: introduce enat as coinductive datatype, enat is just of_nat *}
    1.19 +
    1.20  definition enat :: "nat \<Rightarrow> enat" where
    1.21    "enat n = Abs_enat (Some n)"
    1.22   
    1.23 @@ -35,6 +37,12 @@
    1.24    definition "\<infinity> = Abs_enat None"
    1.25    instance proof qed
    1.26  end
    1.27 +
    1.28 +instance enat :: countable
    1.29 +proof
    1.30 +  show "\<exists>to_nat::enat \<Rightarrow> nat. inj to_nat"
    1.31 +    by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
    1.32 +qed
    1.33   
    1.34  rep_datatype enat "\<infinity> :: enat"
    1.35  proof -
    1.36 @@ -555,7 +563,6 @@
    1.37  
    1.38  text {* TODO: add simprocs for combining and cancelling numerals *}
    1.39  
    1.40 -
    1.41  subsection {* Well-ordering *}
    1.42  
    1.43  lemma less_enatE:
    1.44 @@ -596,6 +603,8 @@
    1.45  
    1.46  subsection {* Complete Lattice *}
    1.47  
    1.48 +text {* TODO: enat as order topology? *}
    1.49 +
    1.50  instantiation enat :: complete_lattice
    1.51  begin
    1.52