--- a/src/HOL/Finite_Set.thy Fri Feb 13 23:55:24 2009 +0100
+++ b/src/HOL/Finite_Set.thy Sat Feb 14 08:45:16 2009 +0100
@@ -247,6 +247,10 @@
"finite(A::'a set) \<Longrightarrow> finite(-A) = finite(UNIV::'a set)"
by(simp add:Compl_eq_Diff_UNIV)
+lemma finite_not[simp]:
+ "finite{x::'a. P x} \<Longrightarrow> finite{x. ~P x} = finite(UNIV::'a set)"
+by(simp add:Collect_neg_eq)
+
lemma finite_Diff_insert [iff]: "finite (A - insert a B) = finite (A - B)"
apply (subst Diff_insert)
apply (case_tac "a : A - B")
--- a/src/HOL/Nominal/Nominal.thy Fri Feb 13 23:55:24 2009 +0100
+++ b/src/HOL/Nominal/Nominal.thy Sat Feb 14 08:45:16 2009 +0100
@@ -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"