src/HOL/SetInterval.thy
changeset 26105 ae06618225ec
parent 26072 f65a7fa2da6c
child 27656 d4f6e64ee7cc
     1.1 --- a/src/HOL/SetInterval.thy	Wed Feb 20 23:24:38 2008 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Thu Feb 21 17:33:58 2008 +0100
     1.3 @@ -469,6 +469,18 @@
     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 +apply(auto simp:atLeast0LessThan[symmetric] lessThan_def[symmetric] card_image bij_betw_def)
    1.12 +done
    1.13 +
    1.14 +lemma ex_bij_betw_finite_nat:
    1.15 +  "finite M \<Longrightarrow> \<exists>h. bij_betw h M {0..<card M}"
    1.16 +by (blast dest: ex_bij_betw_nat_finite bij_betw_inv)
    1.17 +
    1.18 +
    1.19  subsection {* Intervals of integers *}
    1.20  
    1.21  lemma atLeastLessThanPlusOne_atLeastAtMost_int: "{l..<u+1} = {l..(u::int)}"