# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1271002208 -7200
# Node ID 81b171e2d6d57f9af983e3be96872731c105f97f
# Parent  ed46cf122016485268a9abc5f0599367eaec4377
added eqvt rules that are more standard

diff -r ed46cf122016 -r 81b171e2d6d5 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sun Apr 11 18:08:57 2010 +0200
+++ b/Nominal/Abs.thy	Sun Apr 11 18:10:08 2010 +0200
@@ -1,10 +1,10 @@
 theory Abs
-imports "Nominal2_Atoms" 
-        "Nominal2_Eqvt" 
-        "Nominal2_Supp" 
-        "Nominal2_FSet"
-        "../Quotient" 
-        "../Quotient_Product" 
+imports "../Nominal-General/Nominal2_Atoms" 
+        "../Nominal-General/Nominal2_Eqvt" 
+        "../Nominal-General/Nominal2_Supp" 
+        "../Nominal-General/Nominal2_FSet"
+        "Quotient" 
+        "Quotient_Product" 
 begin
 
 fun
@@ -761,6 +761,20 @@
   unfolding alphas fresh_star_def
   by (simp_all add: fresh_plus_perm)
 
+
+(* PROBLEM: this should be the real eqvt lemma for the alphas *)
+lemma alpha_gen_real_eqvt:
+  shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
+  unfolding alphas
+  unfolding permute_eqvt[symmetric]
+  unfolding set_eqvt[symmetric]
+  unfolding permute_fun_app_eq[symmetric]
+  unfolding Diff_eqvt[symmetric]
+  by (auto simp add: permute_bool_def fresh_star_permute_iff)
+
+
 lemma alpha_gen_eqvt:
   assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"
   and     b: "p \<bullet> (f x) = f (p \<bullet> x)"