author nipkow Sat, 14 Feb 2009 08:45:16 +0100 changeset 29903 2c0046b26f80 parent 29902 445320b620ef child 29908 b82ab2aebbbf child 29916 f24137b42d9b
more finiteness changes
 src/HOL/Finite_Set.thy file | annotate | diff | comparison | revisions src/HOL/Nominal/Nominal.thy file | annotate | diff | comparison | revisions
```--- 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)"

+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)
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" ```