# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1306893547 -32400
# Node ID 6750964a69bf7aba65e19149346970e4efa88de0
# Parent  3e341af86bbd98ef03393b04673ea3493f3fea76
equivariance of db_trans

diff -r 3e341af86bbd -r 6750964a69bf Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 31 12:22:28 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 01 10:59:07 2011 +0900
@@ -436,6 +436,42 @@
   apply (simp_all add: lam.size)
   done
 
+lemma trans_eqvt[eqvt]:
+  "p \<bullet> trans t l n = trans (p \<bullet>t) (p \<bullet>l) (p \<bullet>n)"
+proof (nominal_induct t avoiding: l p arbitrary: n rule: lam.strong_induct)
+  fix name l n p
+  show "p \<bullet> trans (Var name) l n =
+       trans (p \<bullet> Var name) (p \<bullet> l) (p \<bullet> n)"
+    apply (induct l arbitrary: n)
+    apply simp
+    apply auto
+    apply (simp add: permute_pure)
+    done
+next
+  fix lam1 lam2 l n p
+  assume 
+    "\<And>b ba n. ba \<bullet> trans lam1 b n = trans (ba \<bullet> lam1) (ba \<bullet> b) (ba \<bullet> n)"
+  "  \<And>b ba n. ba \<bullet> trans lam2 b n = trans (ba \<bullet> lam2) (ba \<bullet> b) (ba \<bullet> n)"
+  then show "p \<bullet> trans (App lam1 lam2) l n =
+          trans (p \<bullet> App lam1 lam2) (p \<bullet> l) (p \<bullet> n)"
+    by (simp add: db_in_eqvt)
+next
+  fix name :: name and l :: "name list" and p :: perm
+  fix lam n
+  assume
+    "atom name \<sharp> l"
+    "atom name \<sharp> p"
+    "\<And>b ba n. ba \<bullet> trans lam b n = trans (ba \<bullet> lam) (ba \<bullet> b) (ba \<bullet> n)"
+  then show
+    "p \<bullet> trans (Lam [name]. lam) l n =
+          trans (p \<bullet> Lam [name]. lam) (p \<bullet> l) (p \<bullet> n)"
+  apply (simp add: fresh_at_list)
+  apply (subst trans.simps)
+  apply (simp add: fresh_at_list[symmetric])
+  apply (simp add: db_in_eqvt)
+  done
+qed
+
 lemma db_trans_test:
   assumes a: "y \<noteq> x"
   shows "trans (Lam [x]. Lam [y]. App (Var x) (Var y)) [] 0 = Some (DBLam (DBLam (DBApp (DBVar 1) (DBVar 0))))"