# HG changeset patch
# User urbanc
# Date 1143209708 -3600
# Node ID 35177b864f80976a0fd1e0ac47252eea79fff19b
# Parent  659b8165c7248e1ef46ed7700b983fc81764d02f
tuned some proofs

diff -r 659b8165c724 -r 35177b864f80 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Fri Mar 24 11:54:07 2006 +0100
+++ b/src/HOL/Nominal/Nominal.thy	Fri Mar 24 15:15:08 2006 +0100
@@ -495,6 +495,15 @@
   shows "(pi3@pi1) \<triangleq> (pi3@pi2)"
 using a by (simp add: prm_eq_def at_append[OF at] at_bij[OF at])
 
+lemma at_prm_eq_append':
+  fixes pi1 :: "'x prm"
+  and   pi2 :: "'x prm"
+  and   pi3 :: "'x prm"
+  assumes at: "at TYPE('x)"
+  and     a: "pi1 \<triangleq> pi2"
+  shows "(pi1@pi3) \<triangleq> (pi2@pi3)"
+using a by (simp add: prm_eq_def at_append[OF at])
+
 lemma at_prm_eq_trans:
   fixes pi1 :: "'x prm"
   and   pi2 :: "'x prm"
@@ -1355,7 +1364,7 @@
   from a1' a2' have a3: "a\<noteq>b" by force
   from a1' have "([(a,b)]\<bullet>a)\<in>([(a,b)]\<bullet>(supp x))" 
     by (simp only: pt_set_bij[OF at_pt_inst[OF at], OF at])
-  hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_append[OF at] at_calc[OF at])
+  hence "b\<in>([(a,b)]\<bullet>(supp x))" by (simp add: at_calc[OF at])
   hence "b\<in>(supp ([(a,b)]\<bullet>x))" by (simp add: pt_perm_supp[OF pt,OF at])
   with a2' neg show False by simp
 qed
@@ -1393,9 +1402,8 @@
   and     a1: "a\<sharp>x" and a2: "b\<sharp>x" 
   shows "[(a,b)]\<bullet>x=x"
 proof (cases "a=b")
-  assume c1: "a=b"
-  have "[(a,a)] \<triangleq> []" by (rule at_ds1[OF at])
-  hence "[(a,b)] \<triangleq> []" using c1 by simp
+  assume "a=b"
+  hence "[(a,b)] \<triangleq> []" by (simp add: at_ds1[OF at])
   hence "[(a,b)]\<bullet>x=([]::'x prm)\<bullet>x" by (rule pt3[OF pt])
   thus ?thesis by (simp only: pt1[OF pt])
 next