# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1320791491 0
# Node ID 014edadaeb59f56bc7c472be51ed8fd1e3231ff8
# Parent  9b0324e1293b563288cdd1b0352a8db294d17837
Add equivariance for alpha_lam_raw and abs_lam.

diff -r 9b0324e1293b -r 014edadaeb59 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Mon Nov 07 13:58:18 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Tue Nov 08 22:31:31 2011 +0000
@@ -12,6 +12,22 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
 
+lemma alpha_lam_raw_eqvt[eqvt]: "p \<bullet> (alpha_lam_raw x y) = alpha_lam_raw (p \<bullet> x) (p \<bullet> y)"
+  unfolding alpha_lam_raw_def
+  by perm_simp rule
+
+lemma abs_lam_eqvt[eqvt]: "(p \<bullet> abs_lam t) = abs_lam (p \<bullet> t)"
+proof -
+  have "alpha_lam_raw (rep_lam (abs_lam t)) t"
+    using rep_abs_rsp_left Quotient_lam equivp_reflp lam_equivp by metis
+  then have "alpha_lam_raw (p \<bullet> rep_lam (abs_lam t)) (p \<bullet> t)"
+    unfolding alpha_lam_raw_eqvt[symmetric] permute_pure .
+  then have "abs_lam (p \<bullet> rep_lam (abs_lam t)) = abs_lam (p \<bullet> t)"
+    using Quotient_rel Quotient_lam by metis
+  thus ?thesis using permute_lam_def id_apply map_fun_apply by metis
+qed
+
+
 section {* Simple examples from Norrish 2004 *}
 
 nominal_primrec