adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
authorbulwahn
Fri Mar 02 09:35:32 2012 +0100 (2012-03-02)
changeset 46756faf62905cd53
parent 46754 e33519ec9e91
child 46757 ad878aff9c15
adding finiteness of intervals on integer sets; adding another finiteness theorem for multisets
src/HOL/Int.thy
src/HOL/Library/Multiset.thy
src/HOL/Old_Number_Theory/Gauss.thy
     1.1 --- a/src/HOL/Int.thy	Thu Mar 01 21:35:49 2012 +0100
     1.2 +++ b/src/HOL/Int.thy	Fri Mar 02 09:35:32 2012 +0100
     1.3 @@ -2179,6 +2179,36 @@
     1.4  qed
     1.5  
     1.6  
     1.7 +subsection {* Finiteness of intervals *}
     1.8 +
     1.9 +lemma finite_interval_int1 [iff]: "finite {i :: int. a <= i & i <= b}"
    1.10 +proof (cases "a <= b")
    1.11 +  case True
    1.12 +  from this show ?thesis
    1.13 +  proof (induct b rule: int_ge_induct)
    1.14 +    case base
    1.15 +    have "{i. a <= i & i <= a} = {a}" by auto
    1.16 +    from this show ?case by simp
    1.17 +  next
    1.18 +    case (step b)
    1.19 +    from this have "{i. a <= i & i <= b + 1} = {i. a <= i & i <= b} \<union> {b + 1}" by auto
    1.20 +    from this step show ?case by simp
    1.21 +  qed
    1.22 +next
    1.23 +  case False from this show ?thesis
    1.24 +    by (metis (lifting, no_types) Collect_empty_eq finite.emptyI order_trans)
    1.25 +qed
    1.26 +
    1.27 +lemma finite_interval_int2 [iff]: "finite {i :: int. a <= i & i < b}"
    1.28 +by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
    1.29 +
    1.30 +lemma finite_interval_int3 [iff]: "finite {i :: int. a < i & i <= b}"
    1.31 +by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
    1.32 +
    1.33 +lemma finite_interval_int4 [iff]: "finite {i :: int. a < i & i < b}"
    1.34 +by (rule rev_finite_subset[OF finite_interval_int1[of "a" "b"]]) auto
    1.35 +
    1.36 +
    1.37  subsection {* Configuration of the code generator *}
    1.38  
    1.39  code_datatype Pls Min Bit0 Bit1 "number_of \<Colon> int \<Rightarrow> int"
     2.1 --- a/src/HOL/Library/Multiset.thy	Thu Mar 01 21:35:49 2012 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Fri Mar 02 09:35:32 2012 +0100
     2.3 @@ -476,6 +476,8 @@
     2.4  lemma finite_set_of [iff]: "finite (set_of M)"
     2.5    using count [of M] by (simp add: multiset_def set_of_def)
     2.6  
     2.7 +lemma finite_Collect_mem [iff]: "finite {x. x :# M}"
     2.8 +  unfolding set_of_def[symmetric] by simp
     2.9  
    2.10  subsubsection {* Size *}
    2.11  
     3.1 --- a/src/HOL/Old_Number_Theory/Gauss.thy	Thu Mar 01 21:35:49 2012 +0100
     3.2 +++ b/src/HOL/Old_Number_Theory/Gauss.thy	Fri Mar 02 09:35:32 2012 +0100
     3.3 @@ -67,10 +67,7 @@
     3.4  subsection {* Basic Properties of the Gauss Sets *}
     3.5  
     3.6  lemma finite_A: "finite (A)"
     3.7 -  apply (auto simp add: A_def)
     3.8 -  apply (subgoal_tac "{x. 0 < x & x \<le> (p - 1) div 2} \<subseteq> {x. 0 \<le> x & x < 1 + (p - 1) div 2}")
     3.9 -  apply (auto simp add: bdd_int_set_l_finite finite_subset)
    3.10 -  done
    3.11 +by (auto simp add: A_def)
    3.12  
    3.13  lemma finite_B: "finite (B)"
    3.14  by (auto simp add: B_def finite_A)