# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1290410185 -32400
# Node ID b1d38940040a668757bc2f9397c14a36e2950473
# Parent  50da1be9a7e5c4bf286a87e1eaa9f15c0c4edb7b
single rename in let2

diff -r 50da1be9a7e5 -r b1d38940040a Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Mon Nov 22 16:14:47 2010 +0900
+++ b/Nominal/Ex/Foo2.thy	Mon Nov 22 16:16:25 2010 +0900
@@ -34,7 +34,7 @@
 thm foo.fv_defs
 thm foo.bn_defs
 thm foo.perm_simps
-thm foo.eq_iff
+thm foo.eq_iff(5)
 thm foo.fv_bn_eqvt
 thm foo.size_eqvt
 thm foo.supports
@@ -75,6 +75,18 @@
 apply(simp add: uu1)
 done
 
+lemma Let2_rename:
+  assumes "(supp ([[atom x, atom y]]lst. t1)) \<sharp>* p" and "(supp ([[atom y]]lst. t2)) \<sharp>* p"
+  shows "Let2 x y t1 t2 = Let2 (p \<bullet> x) (p \<bullet> y) (p \<bullet> t1) (p \<bullet> t2)"
+  using assms
+  apply -
+  apply(drule supp_perm_eq[symmetric])
+  apply(drule supp_perm_eq[symmetric])
+  apply(simp only: foo.eq_iff)
+  apply(simp only: eqvts)
+  apply simp
+  done
+
 lemma strong_exhaust1:
   fixes c::"'a::fs"
   assumes "\<And>name. y = Var name \<Longrightarrow> P"