author huffman Sat, 14 Feb 2009 01:24:01 -0800 changeset 29908 b82ab2aebbbf parent 29907 6b9eea61057c (current diff) parent 29903 2c0046b26f80 (diff) child 29909 9433df099848
merged
--- a/src/HOL/Finite_Set.thy	Sat Feb 14 01:23:38 2009 -0800
+++ b/src/HOL/Finite_Set.thy	Sat Feb 14 01:24:01 2009 -0800
@@ -144,8 +144,7 @@
subsubsection{* Finiteness and set theoretic constructions *}

lemma finite_UnI: "finite F ==> finite G ==> finite (F Un G)"
-  -- {* The union of two finite sets is finite. *}
-  by (induct set: finite) simp_all
+by (induct set: finite) simp_all

lemma finite_subset: "A \<subseteq> B ==> finite B ==> finite A"
-- {* Every subset of a finite set is finite. *}
@@ -174,15 +173,21 @@
qed
qed

-lemma finite_Collect_subset[simp]: "finite A \<Longrightarrow> finite{x \<in> A. P x}"
-using finite_subset[of "{x \<in> A. P x}" "A"] by blast
-
lemma finite_Un [iff]: "finite (F Un G) = (finite F & finite G)"
-  by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
+by (blast intro: finite_subset [of _ "X Un Y", standard] finite_UnI)
+
+lemma finite_disjI[simp]:
+  "finite{x. P x | Q x} = (finite{x. P x} & finite{x. Q x})"

lemma finite_Int [simp, intro]: "finite F | finite G ==> finite (F Int G)"
-- {* The converse obviously fails. *}
-  by (blast intro: finite_subset)
+by (blast intro: finite_subset)
+
+lemma finite_conjI [simp, intro]:
+  "finite{x. P x} | finite{x. Q x} ==> finite{x. P x & Q x}"
+  -- {* The converse obviously fails. *}

lemma finite_insert [simp]: "finite (insert a A) = finite A"
apply (subst insert_is_Un)
@@ -227,8 +232,24 @@
then show ?thesis by simp
qed

-lemma finite_Diff [simp]: "finite B ==> finite (B - Ba)"
-  by (rule Diff_subset [THEN finite_subset])
+lemma finite_Diff [simp]: "finite A ==> finite (A - B)"
+by (rule Diff_subset [THEN finite_subset])
+
+lemma finite_Diff2 [simp]:
+  assumes "finite B" shows "finite (A - B) = finite A"
+proof -
+  have "finite A \<longleftrightarrow> finite((A-B) Un (A Int B))" by(simp add: Un_Diff_Int)
+  also have "\<dots> \<longleftrightarrow> finite(A-B)" using `finite B` by(simp)
+  finally show ?thesis ..
+qed
+
+lemma finite_compl[simp]:
+  "finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
+
+lemma finite_not[simp]:
+  "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"

lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
apply (subst Diff_insert)
@@ -237,9 +258,6 @@
apply (subst insert_Diff, simp_all)
done

-lemma finite_Diff_singleton [simp]: "finite (A - {a}) = finite A"
-  by simp
-

text {* Image and Inverse Image over Finite Sets *}

--- a/src/HOL/Library/Infinite_Set.thy	Sat Feb 14 01:23:38 2009 -0800
+++ b/src/HOL/Library/Infinite_Set.thy	Sat Feb 14 01:24:01 2009 -0800
@@ -461,10 +461,11 @@
by simp

lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
-  apply (induct n arbitrary: S)
-   apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
-  apply (fastsimp iff: finite_Diff_singleton)
-  done
+apply (induct n arbitrary: S)
+ apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
+apply simp
+apply (metis Collect_def Collect_mem_eq DiffE infinite_remove)
+done

declare enumerate_0 [simp del] enumerate_Suc [simp del]

--- a/src/HOL/Library/Multiset.thy	Sat Feb 14 01:23:38 2009 -0800
+++ b/src/HOL/Library/Multiset.thy	Sat Feb 14 01:24:01 2009 -0800
@@ -88,10 +88,8 @@

lemma union_preserves_multiset:
"M \<in> multiset ==> N \<in> multiset ==> (\<lambda>a. M a + N a) \<in> multiset"
-apply (drule (1) finite_UnI)
-apply (simp del: finite_Un add: Un_def)
-done
+

lemma diff_preserves_multiset:
"M \<in> multiset ==> (\<lambda>a. M a - N a) \<in> multiset"
--- a/src/HOL/Nominal/Nominal.thy	Sat Feb 14 01:23:38 2009 -0800
+++ b/src/HOL/Nominal/Nominal.thy	Sat Feb 14 01:24:01 2009 -0800
@@ -558,12 +558,7 @@
fixes x :: "'x"
assumes at: "at TYPE('x)"
shows "supp x = {x}"
-proof (simp add: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at], auto)
-  assume f: "finite {b::'x. b \<noteq> x}"
-  have a1: "{b::'x. b \<noteq> x} = UNIV-{x}" by force
-  have a2: "infinite (UNIV::'x set)" by (rule at4[OF at])
-  from f a1 a2 show False by force
-qed
+by(auto simp: supp_def Collect_conj_eq Collect_imp_eq at_calc[OF at] at4[OF at])

lemma at_fresh:
fixes a :: "'x"
@@ -1791,8 +1786,8 @@
by (simp add: finite_infinite[OF f3,OF at4[OF at], simplified])
hence "infinite ({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})"
by (force dest: Diff_infinite_finite)
-  hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
-    by (auto iff del: finite_Diff_insert Diff_eq_empty_iff)
+  hence "({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b}) \<noteq> {}"
+    by (metis Collect_def finite_set set_empty2)
hence "\<exists>c. c\<in>({c. [(a,c)]\<bullet>x = x \<and> [(b,c)]\<bullet>x = x}-{a,b})" by (force)
then obtain c
where eq1: "[(a,c)]\<bullet>x = x"
--- a/src/HOL/Set.thy	Sat Feb 14 01:23:38 2009 -0800
+++ b/src/HOL/Set.thy	Sat Feb 14 01:24:01 2009 -0800
@@ -787,6 +787,9 @@

lemma set_diff_eq: "A - B = {x. x : A & ~ x : B}" by blast

+lemma Compl_eq_Diff_UNIV: "-A = (UNIV - A)"
+by blast
+

subsubsection {* Augmenting a set -- insert *}