# HG changeset patch
# User berghofe
# Date 1137000059 -3600
# Node ID 0a37df3bb99d61644b3be5c84be6ae869ca8cc3d
# Parent  32722023ff90f85e24069e823fc12537e93f2631
Added theorem at_finite_select.

diff -r 32722023ff90 -r 0a37df3bb99d src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed Jan 11 17:12:30 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Wed Jan 11 18:20:59 2006 +0100
@@ -615,6 +615,17 @@
   shows "\<exists>c::'x. c\<sharp>x"
   by (simp add: fresh_def, rule ex_in_inf[OF at, OF fs])
 
+lemma at_finite_select: "at (TYPE('a)) \<Longrightarrow> finite (S::'a set) \<Longrightarrow> \<exists>x. x \<notin> S"
+  apply (drule Diff_infinite_finite)
+  apply (simp add: at_def)
+  apply blast
+  apply (subgoal_tac "UNIV - S \<noteq> {}")
+  apply (simp only: ex_in_conv [symmetric])
+  apply blast
+  apply (rule notI)
+  apply simp
+  done
+
 --"the at-props imply the pt-props"
 lemma at_pt_inst:
   assumes at: "at TYPE('x)"