adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets

--- a/src/HOL/Int.thy	Thu Mar 01 21:35:49 2012 +0100
+++ b/src/HOL/Int.thy	Fri Mar 02 09:35:32 2012 +0100
@@ -2179,6 +2179,36 @@
 qed
 
 
+subsection {* Finiteness of intervals *}
+
+lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
+proof (cases "a <= b")
+  case True
+  from this show ?thesis
+  proof (induct b rule: int_ge_induct)
+    case base
+    have "{i. a <= i & i <= a} = {a}" by auto
+    from this show ?case by simp
+  next
+    case (step b)
+    from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
+    from this step show ?case by simp
+  qed
+next
+  case False from this show ?thesis
+    by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
+qed
+
+lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
+by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
+
+lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
+by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
+
+lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
+by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
+
+
 subsection {* Configuration of the code generator *}
 
 code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"

--- a/src/HOL/Library/Multiset.thy	Thu Mar 01 21:35:49 2012 +0100
+++ b/src/HOL/Library/Multiset.thy	Fri Mar 02 09:35:32 2012 +0100
@@ -476,6 +476,8 @@
 lemma finite_set_of [iff]: "finite (set_of M)"
   using count [of M] by (simp add: multiset_def set_of_def)
 
+lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
+  unfolding set_of_def[symmetric] by simp
 
 subsubsection {* Size *}
 

--- a/src/HOL/Old_Number_Theory/Gauss.thy	Thu Mar 01 21:35:49 2012 +0100
+++ b/src/HOL/Old_Number_Theory/Gauss.thy	Fri Mar 02 09:35:32 2012 +0100
@@ -67,10 +67,7 @@
 subsection {* Basic Properties of the Gauss Sets *}
 
 lemma finite_A: "finite (A)"
-  apply (auto simp add: A_def)
-  apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
-  apply (auto simp add: bdd_int_set_l_finite finite_subset)
-  done
+by (auto simp add: A_def)
 
 lemma finite_B: "finite (B)"
 by (auto simp add: B_def finite_A)