475 (* lemma helpr: "atom x \<sharp> ta \<Longrightarrow> Lam [xa]. ta = Lam [x]. ((xa \<leftrightarrow> x) \<bullet> ta)"

   476   apply (case_tac "x = xa")

   477   apply simp

   478   apply (simp add: lam.eq_iff Abs1_eq_iff flip_def[symmetric])

   479   by (metis atom_eqvt flip_at_simps(2) fresh_permute_iff)

   480 

   481 lemma supp_lookup: "supp (lookup l n name) = {atom name} - supp l"

   482   apply (induct l arbitrary: n)

   483   apply (simp_all add: ln.supp supp_at_base supp_Nil supp_Cons pure_supp)

   484   done

   485 

   486 lemma trans_eqvt[eqvt]: "p \<bullet> (trans t l) = trans (p \<bullet> t) (p \<bullet> l)"

   487   apply (induct t l rule: trans.induct)

   488   apply simp_all

   489   apply (simp add: eqvts permute_pure)

   490   done

   491 

   492 lemma diff_un: "a - (b \<union> c) = a - b - c"

   493   by blast

   494 

   495 lemma supp_trans: "supp (trans t l) = supp t - supp l"

   496   apply (induct t arbitrary: l rule: lam.induct)

   497   apply (simp_all add: lam.supp supp_at_base supp_lookup ln.supp)

   498   apply blast

   499   apply (rule_tac x="(lam, l)" and ?'a="name" in obtain_fresh)

   500   apply (simp add: fresh_Pair)

   501   apply clarify

   502   apply (subgoal_tac "supp (Lambda.trans (Lam [a]. ((name \<leftrightarrow> a) \<bullet> lam)) l) =

   503     supp lam - {atom name} - supp l")

   504   using helpr

   505   apply simp

   506   apply (simp add: ln.supp)

   507   apply (subgoal_tac "supp ((name \<leftrightarrow> a) \<bullet> (Lambda.trans lam ((name \<leftrightarrow> a) \<bullet> (a # l)))) = supp lam - {atom name} - supp l")

   508   apply (simp add: trans_eqvt)

   509   apply (simp add: supp_eqvt[symmetric])

   510   apply (simp add: Diff_eqvt)

   511   apply (simp add: supp_eqvt supp_Cons  union_eqvt)

   512   apply (simp add: diff_un)

   513   apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*})

   514   apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1*})

   515   apply rule

   516   prefer 2

   517   apply rule

   518   apply (simp add: supp_at_base)

   519   apply (subgoal_tac "(name \<leftrightarrow> a) \<bullet> (supp lam - {atom name}) = supp lam - {atom name}")

   520   apply (simp add: eqvts)

   521   unfolding flip_def

   522   apply (rule swap_fresh_fresh)

   523 apply (metis fresh_at_base fresh_def fresh_minus_atom_set lam.fsupp supp_at_base)

   524 by (metis fresh_def fresh_finite_atom_set fresh_minus_atom_set lam.fsupp)

   525 

   526 lemma "atom x \<sharp> trans_sumC (t, x # xsa)"

   527   by (simp add: fresh_def meta_eq_to_obj_eq[OF trans_def, symmetric, unfolded fun_eq_iff] supp_trans supp_Cons supp_at_base)

   528 *)

   529