author bulwahn Fri, 02 Mar 2012 09:35:32 +0100 changeset 46756 faf62905cd53 parent 46754 e33519ec9e91 child 46757 ad878aff9c15
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
 src/HOL/Int.thy file | annotate | diff | comparison | revisions src/HOL/Library/Multiset.thy file | annotate | diff | comparison | revisions src/HOL/Old_Number_Theory/Gauss.thy file | annotate | diff | comparison | revisions
```--- 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