add lemmas
authorAndreas Lochbihler
Tue Apr 14 11:34:32 2015 +0200 (2015-04-14)
changeset 60058f17bb06599f6
parent 60057 86fa63ce8156
child 60059 8a6d947cc756
add lemmas
src/HOL/Library/Countable_Set.thy
     1.1 --- a/src/HOL/Library/Countable_Set.thy	Tue Apr 14 11:32:01 2015 +0200
     1.2 +++ b/src/HOL/Library/Countable_Set.thy	Tue Apr 14 11:34:32 2015 +0200
     1.3 @@ -247,6 +247,13 @@
     1.4    shows "countable ((X ^^ i) `` Y)"
     1.5    using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
     1.6  
     1.7 +lemma countable_funpow:
     1.8 +  fixes f :: "'a set \<Rightarrow> 'a set"
     1.9 +  assumes "\<And>A. countable A \<Longrightarrow> countable (f A)"
    1.10 +  and "countable A"
    1.11 +  shows "countable ((f ^^ n) A)"
    1.12 +by(induction n)(simp_all add: assms)
    1.13 +
    1.14  lemma countable_rtrancl:
    1.15    "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)"
    1.16    unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
    1.17 @@ -276,6 +283,9 @@
    1.18    "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
    1.19    unfolding Collect_finite_subset_eq_lists by auto
    1.20  
    1.21 +lemma countable_set_option [simp]: "countable (set_option x)"
    1.22 +by(cases x) auto
    1.23 +
    1.24  subsection {* Misc lemmas *}
    1.25  
    1.26  lemma countable_all: