# HG changeset patch
# User urbanc
# Date 1140989117 -3600
# Node ID 5a98cdf9907979847c4dbcc776c4897015e55e0b
# Parent  af69e41eab5d5a6bb66bca60c867bb442579fa03
replaced the lemma at_two by at_different;
this lemma now proves

  EX b. a != b

diff -r af69e41eab5d -r 5a98cdf99079 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Sun Feb 26 22:24:05 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Sun Feb 26 22:25:17 2006 +0100
@@ -666,15 +666,12 @@
   apply simp
   done
 
-lemma at_two:
+lemma at_different:
   assumes at: "at TYPE('x)"
-  shows "\<exists>(a::'x) (b::'x). a\<noteq>b"
+  shows "\<exists>(b::'x). a\<noteq>b"
 proof -
-  have inf1: "infinite (UNIV::'x set)" by (rule at4[OF at])
-  hence "UNIV \<noteq> ({}::'x set)" by blast
-  hence "\<exists>(a::'x). a\<in>UNIV" by blast
-  then obtain a::"'x" where mem1: "a\<in>UNIV" by blast
-  from inf1 have inf2: "infinite (UNIV-{a})" by (rule infinite_remove)
+  have "infinite (UNIV::'x set)" by (rule at4[OF at])
+  hence inf2: "infinite (UNIV-{a})" by (rule infinite_remove)
   have "(UNIV-{a}) \<noteq> ({}::'x set)" 
   proof (rule_tac ccontr, drule_tac notnotD)
     assume "UNIV-{a} = ({}::'x set)"
@@ -683,8 +680,8 @@
   qed
   hence "\<exists>(b::'x). b\<in>(UNIV-{a})" by blast
   then obtain b::"'x" where mem2: "b\<in>(UNIV-{a})" by blast
-  from mem1 mem2 have "a\<noteq>b" by blast
-  then show "\<exists>(a::'x) (b::'x). a\<noteq>b" by blast
+  from mem2 have "a\<noteq>b" by blast
+  then show "\<exists>(b::'x). a\<noteq>b" by blast
 qed
 
 --"the at-props imply the pt-props"