# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1269857165 -7200
# Node ID b497ac81aead49c10557d6b50a176d36dbc427e9
# Parent  8c0eef2b84e7241065947685d935230f62ac3b28
Abs_gen and Abs_let simplifications.

diff -r 8c0eef2b84e7 -r b497ac81aead Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Mar 29 01:23:24 2010 +0200
+++ b/Nominal/Abs.thy	Mon Mar 29 12:06:05 2010 +0200
@@ -771,5 +771,60 @@
   by (auto simp add: fresh_star_permute_iff)
 
 
+lemma alpha_gen_simpler:
+  assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
+  and fin_fv: "finite (f x)"
+  and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
+  shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>
+     (f x - bs) \<sharp>* pi \<and>
+     R (pi \<bullet> x) y \<and>
+     pi \<bullet> bs = cs"
+  apply rule
+  unfolding alpha_gen
+  apply clarify
+  apply (erule conjE)+
+  apply (simp)
+  apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")
+  apply (rule sym)
+  apply simp
+  apply (rule supp_perm_eq)
+  apply (subst supp_finite_atom_set)
+  apply (rule finite_Diff)
+  apply (rule fin_fv)
+  apply (assumption)
+  apply (simp add: eqvts fv_eqvt)
+  apply (subst fv_rsp)
+  apply assumption
+  apply (simp)
+  done
+
+lemma alpha_lst_simpler:
+  assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"
+  and fin_fv: "finite (f x)"
+  and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"
+  shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>
+     (f x - set bs) \<sharp>* pi \<and>
+     R (pi \<bullet> x) y \<and>
+     pi \<bullet> bs = cs"
+  apply rule
+  unfolding alpha_lst
+  apply clarify
+  apply (erule conjE)+
+  apply (simp)
+  apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")
+  apply (rule sym)
+  apply simp
+  apply (rule supp_perm_eq)
+  apply (subst supp_finite_atom_set)
+  apply (rule finite_Diff)
+  apply (rule fin_fv)
+  apply (assumption)
+  apply (simp add: eqvts fv_eqvt)
+  apply (subst fv_rsp)
+  apply assumption
+  apply (simp)
+  done
+
+
 end