# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1339419777 -3600
# Node ID 425b4c406d8028e0f3091f9284e27f3b7141757c
# Parent  3641530002d665b9d60834f9c2d2477e149a06e0
added CPS files to test (not all proofs have been completed)

diff -r 3641530002d6 -r 425b4c406d80 IsaMakefile
--- a/IsaMakefile	Sat Jun 09 19:48:19 2012 +0100
+++ b/IsaMakefile	Mon Jun 11 14:02:57 2012 +0100
@@ -30,6 +30,7 @@
 $(LOG)/HOL-Nominal2-tests.gz: Nominal/ROOT.ML Nominal/*.thy
 	@$(USEDIR) HOL Nominal
 	@$(USEDIR) HOL Tutorial
+	@$(USEDIR) HOL Nominal/Ex/CPS
 
 ## ESOP Paper
 
diff -r 3641530002d6 -r 425b4c406d80 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -14,7 +14,7 @@
 apply (rule, perm_simp, rule, rule)
 apply (simp_all add: fresh_Pair_elim)
 apply (rule_tac y="x" in lt.exhaust)
-apply (auto)
+apply (auto)[3]
 apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
 apply (simp_all add: fresh_at_base)[3]
 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
@@ -28,11 +28,16 @@
 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
 apply (case_tac "k = ka")
 apply simp
-apply(simp (no_asm) add: Abs1_eq_iff del:eqvts)
-apply (simp del: eqvts add: lt.fresh fresh_at_base)
+thm Abs1_eq_iff
+apply(subst Abs1_eq_iff)
+apply(auto)[2]
+apply(rule disjI2)
+apply(rule conjI)
+apply(simp)
+apply(rule conjI)
 apply (simp only: lt.perm_simps(1) lt.perm_simps(2) flip_def[symmetric] lt.eq_iff)
 apply (subst  flip_at_base_simps(2))
-apply simp
+apply(simp)
 apply (intro conjI refl)
 apply (rule flip_fresh_fresh[symmetric])
 apply (simp_all add: lt.fresh)
@@ -125,18 +130,15 @@
 apply (rename_tac M N u K)
 apply (subgoal_tac "Lam n (M+ $ n~ $ K) =  Lam u (M+ $ u~ $ K)")
 apply (simp only:)
-apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1]
+apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1]
 apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))")
 apply (simp only:)
-apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base)
-apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka")
-apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka")
-apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka")
+apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)
+apply(simp_all add: flip_def[symmetric])
 apply (case_tac "m = ma")
 apply simp_all
-apply rule
-apply (auto simp add: flip_fresh_fresh[symmetric])
-apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
+apply (case_tac "m = na")
+apply(simp_all add: flip_fresh_fresh)
 done
 
 termination (eqvt)
@@ -227,7 +229,7 @@
     have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+"
       using * d e by simp
     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)"
-      by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base)
+      by (rule evbeta')(simp_all add: * d e)
     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")
       assume f: "isValue lt2"
       have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp
diff -r 3641530002d6 -r 425b4c406d80 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -22,11 +22,13 @@
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
   apply (auto simp add: fresh_star_def)
   apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff)
+  apply (simp_all add: Abs_fresh_iff)[2]
   apply (erule fresh_eqvt_at)
   apply (simp add: finite_supp)
   apply (simp add: fresh_Pair)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: swap_fresh_fresh)
+  apply(simp)
   done
 
 termination (eqvt) by lexicographic_order
@@ -49,7 +51,8 @@
   apply (erule fresh_eqvt_at)
   apply (simp add: finite_supp)
   apply (simp add: fresh_Pair)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  apply (simp add: eqvt_at_def)
+  apply (simp add: swap_fresh_fresh)
   done
 
 termination (eqvt) by lexicographic_order
diff -r 3641530002d6 -r 425b4c406d80 Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -42,208 +42,7 @@
   apply (rule contra_subsetD[OF supp_fun_app])
   back
   apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
---"-"
-  apply (rule arg_cong)
-  back
-  apply simp
-  apply (thin_tac "eqvt ka")
-  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "c = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "ca = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only: )
-  apply (erule Abs_lst1_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply (drule sym)
-  apply (simp only:)
-  apply (simp add: Abs_fresh_iff lt.fresh)
-  apply clarify
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (drule sym)
-  apply (drule sym)
-  apply (drule sym)
-  apply (simp only:)
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))")
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
-  apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
-  apply (simp add: fresh_Pair_elim)
-  apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
-  back
-  back
-  back
-  apply assumption
-  apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
-  apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
-  apply simp_all[3]
-  apply rule
-  apply (case_tac "c = xa")
-  apply simp_all[2]
-  apply (rotate_tac 1)
-  apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm)
-  apply (simp add: swap_fresh_fresh)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
-  apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec)
-  apply simp
-  apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh)
-  apply (case_tac "c = xa")
-  apply simp
-  apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
-  apply (simp add: atom_eqvt eqvt_at_def)
-  apply (simp add: flip_fresh_fresh)
-  apply (subst fresh_permute_iff)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
-  apply simp
-  apply clarify
-  apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp supp_Inr)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh)
-  apply rule
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (simp add: fresh_def supp_at_base)
-  apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
---"-"
-  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "c = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "ca = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only: )
-  apply (erule Abs_lst1_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply (drule sym)
-  apply (simp only:)
-  apply (simp add: Abs_fresh_iff lt.fresh)
-  apply clarify
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp) (* TODO put sum of fs into fs typeclass *)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (drule sym)
-  apply (drule sym)
-  apply (drule sym)
-  apply (simp only:)
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))")
-  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
-  apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
-  apply (simp add: fresh_Pair_elim)
-  apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
-  back
-  back
-  back
-  apply assumption
-  apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
-  apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
-  apply simp_all[3]
-  apply rule
-  apply (case_tac "c = xa")
-  apply simp_all[2]
-  apply (rotate_tac 1)
-  apply (drule_tac q="(atom ca \<rightleftharpoons> atom x)" in eqvt_at_perm)
-  apply (simp add: swap_fresh_fresh)
-  apply (simp add: eqvt_at_def swap_fresh_fresh)
-  apply (thin_tac "eqvt_at CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (drule_tac x="(atom ca \<rightleftharpoons> atom c)" in spec)
-  apply simp
-  apply (metis (no_types) atom_eq_iff fresh_permute_iff permute_swap_cancel swap_atom_simps(3) swap_fresh_fresh)
-  apply (case_tac "c = xa")
-  apply simp
-  apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
-  apply (simp add: atom_eqvt eqvt_at_def)
-  apply (simp add: flip_fresh_fresh)
-  apply (subst fresh_permute_iff)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
-  apply simp
-  apply clarify
-  apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (simp add: eqvt_at_def)
-  apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: finite_supp supp_Inr)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh)
-  apply rule
-  apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
-  apply (simp add: fresh_def supp_at_base)
-  apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
-  done
-
-termination (eqvt)
-  by lexicographic_order
-
-definition psi:: "lt => lt"
-  where [simp]: "psi V == V*(\<lambda>x. x)"
-
-section {* Simple consequence of CPS *}
-
-lemma [simp]: "eqvt (\<lambda>x\<Colon>lt. x)"
-  by (simp add: eqvt_def eqvt_bound eqvt_lambda)
-
-lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"
-  apply (cases V rule: lt.exhaust)
-  apply simp_all
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply simp
-  done
-
-lemma value_eq2 : "isValue V \<Longrightarrow> V^K = K $ (psi V)"
-  apply (cases V rule: lt.exhaust)
-  apply simp_all
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply simp
-  done
-
-lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Lam n (k (Var n))))"
-  by (cases M rule: lt.exhaust) auto
-
+oops
 
 
 end
diff -r 3641530002d6 -r 425b4c406d80 Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -1,5 +1,7 @@
 header {* CPS transformation of Danvy and Filinski *}
-theory CPS3_DanvyFilinski imports Lt begin
+theory CPS3_DanvyFilinski_FCB2 
+imports Lt 
+begin
 
 nominal_primrec
   CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
@@ -15,66 +17,12 @@
 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
   apply (simp only: eqvt_def CPS1_CPS2_graph_def)
   apply (rule, perm_simp, rule)
-  apply auto
+  apply (auto simp only:)
   apply (case_tac x)
   apply (case_tac a)
   apply (case_tac "eqvt b")
   apply (rule_tac y="aa" in lt.strong_exhaust)
-  apply auto[4]
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
-  apply (simp add: fresh_at_base Abs1_eq_iff)
-  apply (case_tac b)
-  apply (rule_tac y="a" in lt.strong_exhaust)
-  apply auto[3]
-  apply blast
-  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) 
-  apply (simp add: fresh_at_base Abs1_eq_iff)
-  apply blast
---"-"
-  apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
-  apply (simp only:)
-  apply (simp add: Abs1_eq_iff)
-  apply (case_tac "c=ca")
-  apply simp_all[2]
-  apply rule
-  apply (perm_simp)
-  apply (simp add: eqvt_def)
-  apply (simp add: fresh_def)
-  apply (rule contra_subsetD[OF supp_fun_app])
-  back
-  apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
---"-"
-  apply (rule arg_cong)
-  back
-  apply (thin_tac "eqvt ka")
-  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "c = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
-  prefer 2
-  apply (simp add: Abs1_eq_iff')
-  apply (case_tac "ca = a")
-  apply simp_all[2]
-  apply rule
-  apply (simp add: eqvt_at_def)
-  apply (simp add: swap_fresh_fresh fresh_Pair_elim)
-  apply (erule fresh_eqvt_at)
-  apply (simp add: supp_Inr finite_supp)
-  apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (simp only:)
-  apply (simp (no_asm))
-  apply (erule_tac c="a" in Abs_lst1_fcb2')
-  apply (simp add: Abs_fresh_iff lt.fresh)
-  apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base)
+  apply auto
   oops
 
 end
diff -r 3641530002d6 -r 425b4c406d80 Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -17,7 +17,7 @@
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
   unfolding eqvt_def subst_graph_def
-  apply (rule, perm_simp, rule)
+  apply (simp)
   apply(rule TrueI)
   apply(auto simp add: lt.distinct lt.eq_iff)
   apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
@@ -25,9 +25,12 @@
   apply(simp_all add: fresh_star_def fresh_Pair_elim)
   apply blast
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
-  apply(simp_all add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)+
+  apply(simp add: eqvt_at_def)
+  apply(simp add: perm_supp_eq fresh_star_Pair)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: perm_supp_eq fresh_star_Pair)
 done
 
 termination (eqvt) by lexicographic_order