774 lemma alpha_gen_simpler:

   775   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"

   776   and fin_fv: "finite (f x)"

   777   and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"

   778   shows "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow>

   779      (f x - bs) \<sharp>* pi \<and>

   780      R (pi \<bullet> x) y \<and>

   781      pi \<bullet> bs = cs"

   782   apply rule

   783   unfolding alpha_gen

   784   apply clarify

   785   apply (erule conjE)+

   786   apply (simp)

   787   apply (subgoal_tac "f y - cs = pi \<bullet> (f x - bs)")

   788   apply (rule sym)

   789   apply simp

   790   apply (rule supp_perm_eq)

   791   apply (subst supp_finite_atom_set)

   792   apply (rule finite_Diff)

   793   apply (rule fin_fv)

   794   apply (assumption)

   795   apply (simp add: eqvts fv_eqvt)

   796   apply (subst fv_rsp)

   797   apply assumption

   798   apply (simp)

   799   done

   800 

   801 lemma alpha_lst_simpler:

   802   assumes fv_rsp: "\<And>x y. R y x \<Longrightarrow> f x = f y"

   803   and fin_fv: "finite (f x)"

   804   and fv_eqvt: "pi \<bullet> f x = f (pi \<bullet> x)"

   805   shows "alpha_lst (bs, x) R f pi (cs, y) \<longleftrightarrow>

   806      (f x - set bs) \<sharp>* pi \<and>

   807      R (pi \<bullet> x) y \<and>

   808      pi \<bullet> bs = cs"

   809   apply rule

   810   unfolding alpha_lst

   811   apply clarify

   812   apply (erule conjE)+

   813   apply (simp)

   814   apply (subgoal_tac "f y - set cs = pi \<bullet> (f x - set bs)")

   815   apply (rule sym)

   816   apply simp

   817   apply (rule supp_perm_eq)

   818   apply (subst supp_finite_atom_set)

   819   apply (rule finite_Diff)

   820   apply (rule fin_fv)

   821   apply (assumption)

   822   apply (simp add: eqvts fv_eqvt)

   823   apply (subst fv_rsp)

   824   apply assumption

   825   apply (simp)

   826   done

   827 

   828