# HG changeset patch
# User hoelzl
# Date 1454997860 -3600
# Node ID 4a35e3945cab1008f435e92e945bba51790fca0d
# Parent  acfc4ad7b76a87c510e1d68729cdc746f5f5fb46
add transfer rule for countable

diff -r acfc4ad7b76a -r 4a35e3945cab src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Feb 09 06:39:31 2016 +0100
+++ b/src/HOL/Library/Countable_Set.thy	Tue Feb 09 07:04:20 2016 +0100
@@ -312,6 +312,11 @@
   qed
 qed
 
+lemma transfer_countable[transfer_rule]:
+  "bi_unique R \<Longrightarrow> rel_fun (rel_set R) op = countable countable"
+  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
+     (auto dest: countable_image_inj_on)
+
 subsection \<open>Uncountable\<close>
 
 abbreviation uncountable where
@@ -323,10 +328,10 @@
 
 lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
   unfolding bij_betw_def by (metis countable_image)
-  
+
 lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
   by (metis countable_finite)
-  
+
 lemma uncountable_minus_countable:
   "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
   using countable_Un[of B "A - B"] assms by auto