src/HOL/SetInterval.thy
changeset 31438 a1c4c1500abe
parent 31044 6896c2498ac0
child 31501 2a60c9b951e0
     1.1 --- a/src/HOL/SetInterval.thy	Wed Jun 03 12:24:09 2009 -0700
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Jun 04 13:26:32 2009 +0200
     1.3 @@ -468,7 +468,6 @@
     1.4  lemma card_greaterThanLessThan [simp]: "card {l<..<u} = u - Suc l"
     1.5    by (subst atLeastSucLessThan_greaterThanLessThan [THEN sym], simp)
     1.6  
     1.7 -
     1.8  lemma ex_bij_betw_nat_finite:
     1.9    "finite M \<Longrightarrow> \<exists>h. bij_betw h {0..<card M} M"
    1.10  apply(drule finite_imp_nat_seg_image_inj_on)
    1.11 @@ -479,6 +478,17 @@
    1.12    "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
    1.13  by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
    1.14  
    1.15 +lemma finite_same_card_bij:
    1.16 +  "finite A \<Longrightarrow> finite B \<Longrightarrow> card A = card B \<Longrightarrow> EX h. bij_betw h A B"
    1.17 +apply(drule ex_bij_betw_finite_nat)
    1.18 +apply(drule ex_bij_betw_nat_finite)
    1.19 +apply(auto intro!:bij_betw_trans)
    1.20 +done
    1.21 +
    1.22 +lemma ex_bij_betw_nat_finite_1:
    1.23 +  "finite M \<Longrightarrow> \<exists>h. bij_betw h {1 .. card M} M"
    1.24 +by (rule finite_same_card_bij) auto
    1.25 +
    1.26  
    1.27  subsection {* Intervals of integers *}
    1.28