# HG changeset patch
# User urbanc
# Date 1217182096 -7200
# Node ID 224a18d1a3acd94632c45a735cf58cdd7bfbc8a8
# Parent  d1dbe31655be88ea739f732f7bfe600acc4ac015
simplified a proof

diff -r d1dbe31655be -r 224a18d1a3ac src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sat Jul 26 09:00:26 2008 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Sun Jul 27 20:08:16 2008 +0200
@@ -1743,29 +1743,17 @@
   shows "pi\<bullet>(c\<sharp>x) = (pi\<bullet>c)\<sharp>(pi\<bullet>x)"
 by (simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp] dj_perm_forget[OF dj] perm_bool)
 
--- "three helper lemmas for the perm_fresh_fresh-lemma"
-lemma comprehension_neg_UNIV: "{b. \<not> P b} = UNIV - {b. P b}"
-  by (auto)
-
-lemma infinite_or_neg_infinite:
-  assumes h:"infinite (UNIV::'a set)"
-  shows "infinite {b::'a. P b} \<or> infinite {b::'a. \<not> P b}"
-proof (subst comprehension_neg_UNIV, case_tac "finite {b. P b}")
-  assume j:"finite {b::'a. P b}"
-  have "infinite ((UNIV::'a set) - {b::'a. P b})"
-    using Diff_infinite_finite[OF j h] by auto
-  thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" ..
-next
-  assume j:"infinite {b::'a. P b}"
-  thus "infinite {b::'a. P b} \<or> infinite (UNIV - {b::'a. P b})" by simp
-qed
-
 --"the co-set of a finite set is infinte"
 lemma finite_infinite:
   assumes a: "finite {b::'x. P b}"
   and     b: "infinite (UNIV::'x set)"        
   shows "infinite {b. \<not>P b}"
-  using a and infinite_or_neg_infinite[OF b] by simp
+proof -
+  from a b have "infinite (UNIV - {b::'x. P b})" by (simp add: Diff_infinite_finite)
+  moreover 
+  have "{b::'x. \<not>P b} = UNIV - {b::'x. P b}" by auto
+  ultimately show "infinite {b::'x. \<not>P b}" by simp
+qed 
 
 lemma pt_fresh_fresh:
   fixes   x :: "'a"