# HG changeset patch
# User huffman
# Date 1234465462 28800
# Node ID 3dee8ff45d3d0e0b6c1d16b5f58bbb5c40bad8a6
# Parent  4425849f5db715cb6e260c0f5a7ddbf7e06c9a76
move countability proof from Rational to Countable; add instance rat :: countable

diff -r 4425849f5db7 -r 3dee8ff45d3d src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Thu Feb 12 18:14:43 2009 +0100
+++ b/src/HOL/Library/Countable.thy	Thu Feb 12 11:04:22 2009 -0800
@@ -5,7 +5,12 @@
 header {* Encoding (almost) everything into natural numbers *}
 
 theory Countable
-imports Plain "~~/src/HOL/List" "~~/src/HOL/Hilbert_Choice"
+imports
+  Plain
+  "~~/src/HOL/List"
+  "~~/src/HOL/Hilbert_Choice"
+  "~~/src/HOL/Nat_Int_Bij"
+  "~~/src/HOL/Rational"
 begin
 
 subsection {* The class of countable types *}
@@ -193,4 +198,55 @@
   qed
 qed
 
+
+subsection {* The Rationals are Countably Infinite *}
+
+definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
+"nat_to_rat_surj n = (let (a,b) = nat_to_nat2 n
+                      in Fract (nat_to_int_bij a) (nat_to_int_bij b))"
+
+lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
+unfolding surj_def
+proof
+  fix r::rat
+  show "\<exists>n. r = nat_to_rat_surj n"
+  proof(cases r)
+    fix i j assume [simp]: "r = Fract i j" and "j \<noteq> 0"
+    have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
+               in nat_to_rat_surj(nat2_to_nat (m,n)))"
+      using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]
+      by(simp add:Let_def nat_to_rat_surj_def nat_to_nat2_def)
+    thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
+  qed
+qed
+
+lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
+by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
+
+context field_char_0
+begin
+
+lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
+  "\<rat> = range (of_rat o nat_to_rat_surj)"
+using surj_nat_to_rat_surj
+by (auto simp: Rats_def image_def surj_def)
+   (blast intro: arg_cong[where f = of_rat])
+
+lemma surj_of_rat_nat_to_rat_surj:
+  "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
+by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
+
 end
+
+instance rat :: countable
+proof
+  show "\<exists>to_nat::rat \<Rightarrow> nat. inj to_nat"
+  proof
+    have "surj nat_to_rat_surj"
+      by (rule surj_nat_to_rat_surj)
+    then show "inj (inv nat_to_rat_surj)"
+      by (rule surj_imp_inj_inv)
+  qed
+qed
+
+end
diff -r 4425849f5db7 -r 3dee8ff45d3d src/HOL/Rational.thy
--- a/src/HOL/Rational.thy	Thu Feb 12 18:14:43 2009 +0100
+++ b/src/HOL/Rational.thy	Thu Feb 12 11:04:22 2009 -0800
@@ -5,7 +5,7 @@
 header {* Rational numbers *}
 
 theory Rational
-imports Nat_Int_Bij GCD
+imports GCD
 uses ("Tools/rat_arith.ML")
 begin
 
@@ -790,46 +790,6 @@
   by (rule Rats_cases) auto
 
 
-subsection {* The Rationals are Countably Infinite *}
-
-definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
-"nat_to_rat_surj n = (let (a,b) = nat_to_nat2 n
-                      in Fract (nat_to_int_bij a) (nat_to_int_bij b))"
-
-lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
-unfolding surj_def
-proof
-  fix r::rat
-  show "\<exists>n. r = nat_to_rat_surj n"
-  proof(cases r)
-    fix i j assume [simp]: "r = Fract i j" and "j \<noteq> 0"
-    have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
-               in nat_to_rat_surj(nat2_to_nat (m,n)))"
-      using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]
-      by(simp add:Let_def nat_to_rat_surj_def nat_to_nat2_def)
-    thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
-  qed
-qed
-
-lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
-by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
-
-context field_char_0
-begin
-
-lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
-  "\<rat> = range (of_rat o nat_to_rat_surj)"
-using surj_nat_to_rat_surj
-by (auto simp: Rats_def image_def surj_def)
-   (blast intro: arg_cong[where f = of_rat])
-
-lemma surj_of_rat_nat_to_rat_surj:
-  "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
-by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
-
-end
-
-
 subsection {* Implementation of rational numbers as pairs of integers *}
 
 lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b"
@@ -1016,4 +976,4 @@
   | rat_of_int i = (i, 1);
 *}
 
-end
\ No newline at end of file
+end