finite lemmas
authornipkow
Thu Jun 04 19:44:06 2009 +0200 (2009-06-04)
changeset 31441428e4caf2299
parent 31440 ee1d5bec4ce3
child 31442 b861e58086ab
finite lemmas
src/HOL/Finite_Set.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Finite_Set.thy	Thu Jun 04 15:00:44 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu Jun 04 19:44:06 2009 +0200
     1.3 @@ -457,6 +457,18 @@
     1.4  by(blast intro: finite_subset[OF subset_Pow_Union])
     1.5  
     1.6  
     1.7 +lemma finite_subset_image:
     1.8 +  assumes "finite B"
     1.9 +  shows "B \<subseteq> f ` A \<Longrightarrow> \<exists>C\<subseteq>A. finite C \<and> B = f ` C"
    1.10 +using assms proof(induct)
    1.11 +  case empty thus ?case by simp
    1.12 +next
    1.13 +  case insert thus ?case
    1.14 +    by (clarsimp simp del: image_insert simp add: image_insert[symmetric])
    1.15 +       blast
    1.16 +qed
    1.17 +
    1.18 +
    1.19  subsection {* Class @{text finite}  *}
    1.20  
    1.21  setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
     2.1 --- a/src/HOL/Set.thy	Thu Jun 04 15:00:44 2009 +0200
     2.2 +++ b/src/HOL/Set.thy	Thu Jun 04 19:44:06 2009 +0200
     2.3 @@ -1344,13 +1344,16 @@
     2.4  by auto
     2.5  
     2.6  lemma image_image: "f ` (g ` A) = (\<lambda>x. f (g x)) ` A"
     2.7 -  by blast
     2.8 +by blast
     2.9  
    2.10  lemma insert_image [simp]: "x \<in> A ==> insert (f x) (f`A) = f`A"
    2.11 -  by blast
    2.12 +by blast
    2.13  
    2.14  lemma image_is_empty [iff]: "(f`A = {}) = (A = {})"
    2.15 -  by blast
    2.16 +by blast
    2.17 +
    2.18 +lemma empty_is_image[iff]: "({} = f ` A) = (A = {})"
    2.19 +by blast
    2.20  
    2.21  
    2.22  lemma image_Collect [noatp]: "f ` {x. P x} = {f x | x. P x}"