src/HOL/Library/Countable.thy
 changeset 35700 951974ce903e parent 35374 af1c8c15340e child 37388 793618618f78
```--- a/src/HOL/Library/Countable.thy	Wed Mar 10 19:21:59 2010 +0100
+++ b/src/HOL/Library/Countable.thy	Wed Mar 10 14:57:13 2010 -0800
@@ -5,7 +5,7 @@
header {* Encoding (almost) everything into natural numbers *}

theory Countable
-imports Main Rat Nat_Int_Bij
+imports Main Rat Nat_Bijection
begin

subsection {* The class of countable types *}
@@ -48,7 +48,7 @@
subsection {* Countable types *}

instance nat :: countable
-  by (rule countable_classI [of "id"]) simp
+  by (rule countable_classI [of "id"]) simp

subclass (in finite) countable
proof
@@ -63,47 +63,9 @@

text {* Pairs *}

-primrec sum :: "nat \<Rightarrow> nat"
-where
-  "sum 0 = 0"
-| "sum (Suc n) = Suc n + sum n"
-
-lemma sum_arith: "sum n = n * Suc n div 2"
-  by (induct n) auto
-
-lemma sum_mono: "n \<ge> m \<Longrightarrow> sum n \<ge> sum m"
-  by (induct n m rule: diff_induct) auto
-
-definition
-  "pair_encode = (\<lambda>(m, n). sum (m + n) + m)"
-
-lemma inj_pair_cencode: "inj pair_encode"
-  unfolding pair_encode_def
-proof (rule injI, simp only: split_paired_all split_conv)
-  fix a b c d
-  assume eq: "sum (a + b) + a = sum (c + d) + c"
-  have "a + b = c + d \<or> a + b \<ge> Suc (c + d) \<or> c + d \<ge> Suc (a + b)" by arith
-  then
-  show "(a, b) = (c, d)"
-  proof (elim disjE)
-    assume sumeq: "a + b = c + d"
-    then have "a = c" using eq by auto
-    moreover from sumeq this have "b = d" by auto
-    ultimately show ?thesis by simp
-  next
-    assume "a + b \<ge> Suc (c + d)"
-    from sum_mono[OF this] eq
-    show ?thesis by auto
-  next
-    assume "c + d \<ge> Suc (a + b)"
-    from sum_mono[OF this] eq
-    show ?thesis by auto
-  qed
-qed
-
instance "*" :: (countable, countable) countable
-by (rule countable_classI [of "\<lambda>(x, y). pair_encode (to_nat x, to_nat y)"])
-  (auto dest: injD [OF inj_pair_cencode] injD [OF inj_to_nat])
+  by (rule countable_classI [of "\<lambda>(x, y). prod_encode (to_nat x, to_nat y)"])

text {* Sums *}
@@ -111,76 +73,28 @@
instance "+":: (countable, countable) countable
by (rule countable_classI [of "(\<lambda>x. case x of Inl a \<Rightarrow> to_nat (False, to_nat a)
| Inr b \<Rightarrow> to_nat (True, to_nat b))"])
-    (auto split:sum.splits)
+    (simp split: sum.split_asm)

text {* Integers *}

-lemma int_cases: "(i::int) = 0 \<or> i < 0 \<or> i > 0"
-by presburger
-
-lemma int_pos_neg_zero:
-  obtains (zero) "(z::int) = 0" "sgn z = 0" "abs z = 0"
-  | (pos) n where "z = of_nat n" "sgn z = 1" "abs z = of_nat n"
-  | (neg) n where "z = - (of_nat n)" "sgn z = -1" "abs z = of_nat n"
-apply atomize_elim
-apply (insert int_cases[of z])
-apply (auto simp:zsgn_def)
-apply (rule_tac x="nat (-z)" in exI, simp)
-apply (rule_tac x="nat z" in exI, simp)
-done
-
instance int :: countable
-proof (rule countable_classI [of "(\<lambda>i. to_nat (nat (sgn i + 1), nat (abs i)))"],
-    auto dest: injD [OF inj_to_nat])
-  fix x y
-  assume a: "nat (sgn x + 1) = nat (sgn y + 1)" "nat (abs x) = nat (abs y)"
-  show "x = y"
-  proof (cases rule: int_pos_neg_zero[of x])
-    case zero
-    with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
-  next
-    case (pos n)
-    with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
-  next
-    case (neg n)
-    with a show "x = y" by (cases rule: int_pos_neg_zero[of y]) auto
-  qed
-qed
+  by (rule countable_classI [of "int_encode"])

text {* Options *}

instance option :: (countable) countable
-by (rule countable_classI[of "\<lambda>x. case x of None \<Rightarrow> 0
-                                     | Some y \<Rightarrow> Suc (to_nat y)"])
- (auto split:option.splits)
+  by (rule countable_classI [of "option_case 0 (Suc \<circ> to_nat)"])
+    (simp split: option.split_asm)

text {* Lists *}

-lemma from_nat_to_nat_map [simp]: "map from_nat (map to_nat xs) = xs"
-
-primrec
-  list_encode :: "'a\<Colon>countable list \<Rightarrow> nat"
-where
-  "list_encode [] = 0"
-| "list_encode (x#xs) = Suc (to_nat (x, list_encode xs))"
-
instance list :: (countable) countable
-proof (rule countable_classI [of "list_encode"])
-  fix xs ys :: "'a list"
-  assume cenc: "list_encode xs = list_encode ys"
-  then show "xs = ys"
-  proof (induct xs arbitrary: ys)
-    case (Nil ys)
-    with cenc show ?case by (cases ys, auto)
-  next
-    case (Cons x xs' ys)
-    thus ?case by (cases ys) auto
-  qed
-qed
+  by (rule countable_classI [of "list_encode \<circ> map to_nat"])

text {* Functions *}
@@ -200,8 +114,8 @@
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))"
+"nat_to_rat_surj n = (let (a,b) = prod_decode n
+                      in Fract (int_decode a) (int_decode b))"

lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
unfolding surj_def
@@ -210,10 +124,9 @@
show "\<exists>n. r = nat_to_rat_surj n"
proof (cases r)
fix i j assume [simp]: "r = Fract i j" and "j > 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]