src/HOL/Hilbert_Choice.thy
 changeset 31380 f25536c0bb80 parent 29655 ac31940cfb69 child 31454 2c0959ab073f
```     1.1 --- a/src/HOL/Hilbert_Choice.thy	Tue Jun 02 15:53:34 2009 +0200
1.2 +++ b/src/HOL/Hilbert_Choice.thy	Tue Jun 02 16:23:43 2009 +0200
1.3 @@ -219,6 +219,25 @@
1.4  apply (blast intro: bij_is_inj [THEN inv_f_f, symmetric])
1.5  done
1.6
1.7 +lemma finite_fun_UNIVD1:
1.8 +  assumes fin: "finite (UNIV :: ('a \<Rightarrow> 'b) set)"
1.9 +  and card: "card (UNIV :: 'b set) \<noteq> Suc 0"
1.10 +  shows "finite (UNIV :: 'a set)"
1.11 +proof -
1.12 +  from fin have finb: "finite (UNIV :: 'b set)" by (rule finite_fun_UNIVD2)
1.13 +  with card have "card (UNIV :: 'b set) \<ge> Suc (Suc 0)"
1.14 +    by (cases "card (UNIV :: 'b set)") (auto simp add: card_eq_0_iff)
1.15 +  then obtain n where "card (UNIV :: 'b set) = Suc (Suc n)" "n = card (UNIV :: 'b set) - Suc (Suc 0)" by auto
1.16 +  then obtain b1 b2 where b1b2: "(b1 :: 'b) \<noteq> (b2 :: 'b)" by (auto simp add: card_Suc_eq)
1.17 +  from fin have "finite (range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1))" by (rule finite_imageI)
1.18 +  moreover have "UNIV = range (\<lambda>f :: 'a \<Rightarrow> 'b. inv f b1)"
1.19 +  proof (rule UNIV_eq_I)
1.20 +    fix x :: 'a
1.21 +    from b1b2 have "x = inv (\<lambda>y. if y = x then b1 else b2) b1" by (simp add: inv_def)
1.22 +    thus "x \<in> range (\<lambda>f\<Colon>'a \<Rightarrow> 'b. inv f b1)" by blast
1.23 +  qed
1.24 +  ultimately show "finite (UNIV :: 'a set)" by simp
1.25 +qed
1.26
1.27  subsection {*Inverse of a PI-function (restricted domain)*}
1.28
```