# HG changeset patch
# User Andreas Lochbihler
# Date 1429004072 -7200
# Node ID f17bb06599f6da516f2373c8bf402f911070cf28
# Parent  86fa63ce8156240ae6971ffaa3a0100ea5d975ec
add lemmas

diff -r 86fa63ce8156 -r f17bb06599f6 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Apr 14 11:32:01 2015 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Tue Apr 14 11:34:32 2015 +0200
@@ -247,6 +247,13 @@
   shows "countable ((X ^^ i) `` Y)"
   using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
 
+lemma countable_funpow:
+  fixes f :: "'a set \<Rightarrow> 'a set"
+  assumes "\<And>A. countable A \<Longrightarrow> countable (f A)"
+  and "countable A"
+  shows "countable ((f ^^ n) A)"
+by(induction n)(simp_all add: assms)
+
 lemma countable_rtrancl:
   "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
   unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
@@ -276,6 +283,9 @@
   "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
   unfolding Collect_finite_subset_eq_lists by auto
 
+lemma countable_set_option [simp]: "countable (set_option x)"
+by(cases x) auto
+
 subsection {* Misc lemmas *}
 
 lemma countable_all: