1.1 --- a/src/HOL/SetInterval.thy	Thu Oct 04 21:11:06 2007 +0200
     1.2 +++ b/src/HOL/SetInterval.thy	Fri Oct 05 08:38:09 2007 +0200
     1.3 @@ -414,12 +414,34 @@
     1.4  by (simp add: atLeastAtMost_def)
     1.5  
     1.6  lemma bounded_nat_set_is_finite:
     1.7 -    "(ALL i:N. i < (n::nat)) ==> finite N"
     1.8 +  "(ALL i:N. i < (n::nat)) ==> finite N"
     1.9    -- {* A bounded set of natural numbers is finite. *}
    1.10    apply (rule finite_subset)
    1.11     apply (rule_tac [2] finite_lessThan, auto)
    1.12    done
    1.13  
    1.14 +text{* Any subset of an interval of natural numbers the size of the
    1.15 +subset is exactly that interval. *}
    1.16 +
    1.17 +lemma subset_card_intvl_is_intvl:
    1.18 +  "A <= {k..<k+card A} \<Longrightarrow> A = {k..<k+card A}" (is "PROP ?P")
    1.19 +proof cases
    1.20 +  assume "finite A"
    1.21 +  thus "PROP ?P"
    1.22 +  proof(induct A rule:finite_linorder_induct)
    1.23 +    case empty thus ?case by auto
    1.24 +  next
    1.25 +    case (insert A b)
    1.26 +    moreover hence "b ~: A" by auto
    1.27 +    moreover have "A <= {k..<k+card A}" and "b = k+card A"
    1.28 +      using `b ~: A` insert by fastsimp+
    1.29 +    ultimately show ?case by auto
    1.30 +  qed
    1.31 +next
    1.32 +  assume "~finite A" thus "PROP ?P" by simp
    1.33 +qed
    1.34 +
    1.35 +
    1.36  subsubsection {* Cardinality *}
    1.37  
    1.38  lemma card_lessThan [simp]: "card {..<u} = u"
    1.39 @@ -495,6 +517,7 @@
    1.40  lemma finite_greaterThanLessThan_int [iff]: "finite {l<..<u::int}"
    1.41    by (subst atLeastPlusOneLessThan_greaterThanLessThan_int [THEN sym], simp)
    1.42  
    1.43 +
    1.44  subsubsection {* Cardinality *}
    1.45  
    1.46  lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"