1.1 --- a/src/HOL/Finite_Set.thy Sat Feb 14 01:23:38 2009 -0800
1.2 +++ b/src/HOL/Finite_Set.thy Sat Feb 14 01:24:01 2009 -0800
1.3 @@ -144,8 +144,7 @@
1.4 subsubsection{* Finiteness and set theoretic constructions *}
1.5
1.6 lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
1.7 - -- {* The union of two finite sets is finite. *}
1.8 - by (induct set: finite) simp_all
1.9 +by (induct set: finite) simp_all
1.10
1.11 lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
1.12 -- {* Every subset of a finite set is finite. *}
1.13 @@ -174,15 +173,21 @@
1.14 qed
1.15 qed
1.16
1.17 -lemma finite_Collect_subset[simp]: "finite A \<Longrightarrow> finite{x \<in> A. P x}"
1.18 -using finite_subset[of "{x \<in> A. P x}" "A"] by blast
1.19 -
1.20 lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
1.21 - by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
1.22 +by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
1.23 +
1.24 +lemma finite_disjI[simp]:
1.25 + "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"
1.26 +by(simp add:Collect_disj_eq)
1.27
1.28 lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
1.29 -- {* The converse obviously fails. *}
1.30 - by (blast intro: finite_subset)
1.31 +by (blast intro: finite_subset)
1.32 +
1.33 +lemma finite_conjI [simp, intro]:
1.34 + "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
1.35 + -- {* The converse obviously fails. *}
1.36 +by(simp add:Collect_conj_eq)
1.37
1.38 lemma finite_insert [simp]: "finite (insert a A) = finite A"
1.39 apply (subst insert_is_Un)
1.40 @@ -227,8 +232,24 @@
1.41 then show ?thesis by simp
1.42 qed
1.43
1.44 -lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
1.45 - by (rule Diff_subset [THEN finite_subset])
1.46 +lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
1.47 +by (rule Diff_subset [THEN finite_subset])
1.48 +
1.49 +lemma finite_Diff2 [simp]:
1.50 + assumes "finite B" shows "finite (A - B) = finite A"
1.51 +proof -
1.52 + have "finite A \<longleftrightarrow> finite((A-B) Un (A Int B))" by(simp add: Un_Diff_Int)
1.53 + also have "\<dots> \<longleftrightarrow> finite(A-B)" using `finite B` by(simp)
1.54 + finally show ?thesis ..
1.55 +qed
1.56 +
1.57 +lemma finite_compl[simp]:
1.58 + "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
1.59 +by(simp add:Compl_eq_Diff_UNIV)
1.60 +
1.61 +lemma finite_not[simp]:
1.62 + "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
1.63 +by(simp add:Collect_neg_eq)
1.64
1.65 lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
1.66 apply (subst Diff_insert)
1.67 @@ -237,9 +258,6 @@
1.68 apply (subst insert_Diff, simp_all)
1.69 done
1.70
1.71 -lemma finite_Diff_singleton [simp]: "finite (A - {a}) = finite A"
1.72 - by simp
1.73 -
1.74
1.75 text {* Image and Inverse Image over Finite Sets *}
1.76
2.1 --- a/src/HOL/Library/Infinite_Set.thy Sat Feb 14 01:23:38 2009 -0800
2.2 +++ b/src/HOL/Library/Infinite_Set.thy Sat Feb 14 01:24:01 2009 -0800
2.3 @@ -461,10 +461,11 @@
2.4 by simp
2.5
2.6 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
2.7 - apply (induct n arbitrary: S)
2.8 - apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
2.9 - apply (fastsimp iff: finite_Diff_singleton)
2.10 - done
2.11 +apply (induct n arbitrary: S)
2.12 + apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
2.13 +apply simp
2.14 +apply (metis Collect_def Collect_mem_eq DiffE infinite_remove)
2.15 +done
2.16
2.17 declare enumerate_0 [simp del] enumerate_Suc [simp del]
2.18
3.1 --- a/src/HOL/Library/Multiset.thy Sat Feb 14 01:23:38 2009 -0800
3.2 +++ b/src/HOL/Library/Multiset.thy Sat Feb 14 01:24:01 2009 -0800
3.3 @@ -88,10 +88,8 @@
3.4
3.5 lemma union_preserves_multiset:
3.6 "M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
3.7 -apply (simp add: multiset_def)
3.8 -apply (drule (1) finite_UnI)
3.9 -apply (simp del: finite_Un add: Un_def)
3.10 -done
3.11 +by (simp add: multiset_def)
3.12 +
3.13
3.14 lemma diff_preserves_multiset:
3.15 "M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
4.1 --- a/src/HOL/Nominal/Nominal.thy Sat Feb 14 01:23:38 2009 -0800
4.2 +++ b/src/HOL/Nominal/Nominal.thy Sat Feb 14 01:24:01 2009 -0800
4.3 @@ -558,12 +558,7 @@
4.4 fixes x :: "'x"
4.5 assumes at: "at TYPE('x)"
4.6 shows "supp x = {x}"
4.7 -proof (simp add: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at], auto)
4.8 - assume f: "finite {b::'x. b \<noteq> x}"
4.9 - have a1: "{b::'x. b \<noteq> x} = UNIV-{x}" by force
4.10 - have a2: "infinite (UNIV::'x set)" by (rule at4[OF at])
4.11 - from f a1 a2 show False by force
4.12 -qed
4.13 +by(auto simp: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at] at4[OF at])
4.14
4.15 lemma at_fresh:
4.16 fixes a :: "'x"
4.17 @@ -1791,8 +1786,8 @@
4.18 by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
4.19 hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})"
4.20 by (force dest: Diff_infinite_finite)
4.21 - hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
4.22 - by (auto iff del: finite_Diff_insert Diff_eq_empty_iff)
4.23 + hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
4.24 + by (metis Collect_def finite_set set_empty2)
4.25 hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
4.26 then obtain c
4.27 where eq1: "[(a,c)]\<bullet>x = x"
5.1 --- a/src/HOL/Set.thy Sat Feb 14 01:23:38 2009 -0800
5.2 +++ b/src/HOL/Set.thy Sat Feb 14 01:24:01 2009 -0800
5.3 @@ -787,6 +787,9 @@
5.4
5.5 lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast
5.6
5.7 +lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"
5.8 +by blast
5.9 +
5.10
5.11 subsubsection {* Augmenting a set -- insert *}
5.12