src/HOL/SetInterval.thy
 changeset 24853 aab5798e5a33 parent 24748 ee0a0eb6b738 child 25062 af5ef0d4d655
```     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.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  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"
```