1.1 --- a/src/HOL/Finite_Set.thy	Sun Oct 18 00:10:20 2009 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Sun Oct 18 12:07:56 2009 +0200
     1.3 @@ -155,6 +155,19 @@
     1.4    "finite A = (\<exists> (n::nat) f. A = f ` {i::nat. i<n})"
     1.5  by(blast intro: nat_seg_image_imp_finite dest: finite_imp_nat_seg_image_inj_on)
     1.6  
     1.7 +lemma finite_imp_inj_to_nat_seg:
     1.8 +assumes "finite A"
     1.9 +shows "EX f n::nat. f`A = {i. i<n} & inj_on f A"
    1.10 +proof -
    1.11 +  from finite_imp_nat_seg_image_inj_on[OF `finite A`]
    1.12 +  obtain f and n::nat where bij: "bij_betw f {i. i<n} A"
    1.13 +    by (auto simp:bij_betw_def)
    1.14 +  let ?f = "the_inv_onto {i. i<n} f"
    1.15 +  have "inj_on ?f A & ?f ` A = {i. i<n}"
    1.16 +    by (fold bij_betw_def) (rule bij_betw_the_inv_onto[OF bij])
    1.17 +  thus ?thesis by blast
    1.18 +qed
    1.19 +
    1.20  lemma finite_Collect_less_nat[iff]: "finite{n::nat. n<k}"
    1.21  by(fastsimp simp: finite_conv_nat_seg_image)
    1.22