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