# HG changeset patch
# User urbanc
# Date 1140724591 -3600
# Node ID ff41946e5092fd520c5326ecc5a6cdeb61ea65fd
# Parent  06b6f5f8e4cb27e223bfc1ecb64b41929770ba4e
added lemmas

 at_two:  EX a b in an atom type such that a !=b
 at_ds10

and a "test"-lemma  at_prm_eq_compose (can probably be removed)

diff -r 06b6f5f8e4cb -r ff41946e5092 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Thu Feb 23 13:37:46 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Thu Feb 23 20:56:31 2006 +0100
@@ -619,16 +619,14 @@
 done
 
 lemma at_ds10:
-  fixes pi1 :: "'x prm"
-  and   pi2 :: "'x prm"
+  fixes pi :: "'x prm"
   and   a  :: "'x"
   and   b  :: "'x"
   assumes at: "at TYPE('x)"
-  and     a:  "b\<sharp>(rev pi1)"
-  shows "(pi2@([(pi1\<bullet>a,b)]@pi1)) \<triangleq> (pi2@(pi1@[(a,b)]))"
+  and     a:  "b\<sharp>(rev pi)"
+  shows "([(pi\<bullet>a,b)]@pi) \<triangleq> (pi@[(a,b)])"
 using a
 apply -
-apply(rule at_prm_eq_append[OF at])
 apply(rule at_prm_eq_trans)
 apply(rule at_ds2[OF at])
 apply(simp add: at_prm_fresh[OF at] at_rev_pi[OF at])
@@ -668,6 +666,27 @@
   apply simp
   done
 
+lemma at_two:
+  assumes at: "at TYPE('x)"
+  shows "\<exists>(a::'x) (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 "(UNIV-{a}) \<noteq> ({}::'x set)" 
+  proof (rule_tac ccontr, drule_tac notnotD)
+    assume "UNIV-{a} = ({}::'x set)"
+    with inf2 have "infinite ({}::'x set)" by simp
+    then show "False" by (auto intro: infinite_nonempty)
+  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
+qed
+
 --"the at-props imply the pt-props"
 lemma at_pt_inst:
   assumes at: "at TYPE('x)"
@@ -2669,6 +2688,33 @@
   by (simp add: perm_fun_def)
 
 
+section {* test *}
+lemma at_prm_eq_compose:
+  fixes pi1 :: "'x prm"
+  and   pi2 :: "'x prm"
+  and   pi3 :: "'x prm"
+  assumes at: "at TYPE('x)"
+  and     a: "pi1 \<triangleq> pi2"
+  shows "(pi3\<bullet>pi1) \<triangleq> (pi3\<bullet>pi2)"
+proof -
+  have pt: "pt TYPE('x) TYPE('x)" by (rule at_pt_inst[OF at])
+  have pt_prm: "pt TYPE('x prm) TYPE('x)" 
+    by (rule pt_list_inst[OF pt_prod_inst[OF pt, OF pt]])  
+  from a show ?thesis
+    apply -
+    apply(auto simp add: prm_eq_def)
+    apply(rule_tac pi="rev pi3" in pt_bij4[OF pt, OF at])
+    apply(rule trans)
+    apply(rule pt_perm_compose[OF pt, OF at])
+    apply(simp add: pt_rev_pi[OF pt_prm, OF at])
+    apply(rule sym)
+    apply(rule trans)
+    apply(rule pt_perm_compose[OF pt, OF at])
+    apply(simp add: pt_rev_pi[OF pt_prm, OF at])
+    done
+qed
+
+
 (***************************************)
 (* setup for the individial atom-kinds *)
 (* and nominal datatypes               *)