# HG changeset patch
# User nipkow
# Date 1234597516 -3600
# Node ID 2c0046b26f80811f19ecb239a560ed21be6c69e9
# Parent  445320b620ef5efa291cfee544e5a14eee827897
more finiteness changes

diff -r 445320b620ef -r 2c0046b26f80 src/HOL/Finite_Set.thy
--- 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")
diff -r 445320b620ef -r 2c0046b26f80 src/HOL/Nominal/Nominal.thy
--- 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"