--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon Jul 11 14:02:13 2011 +0200
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon Jul 11 23:42:22 2011 +0900
@@ -1,6 +1,9 @@
 header {* CPS transformation of Danvy and Filinski *}
 theory CPS3_DanvyFilinski imports Lt begin
 
+lemma TODO: "eqvt_at f a \<Longrightarrow> eqvt_at f (p \<bullet> a)"
+  sorry
+
 nominal_primrec
   CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
 and
@@ -100,12 +103,16 @@
   apply rule
   apply (case_tac "c = xa")
   apply simp_all[2]
+  apply (rotate_tac 1)
+  apply (drule TODO)
+  apply (drule_tac x="(atom ca \<rightleftharpoons> atom x)" in spec)
+  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 clarify
-  apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)
-  apply (simp add: eqvt_at_def)
-  apply clarify
-  apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)
+  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~))")
@@ -160,7 +167,7 @@
   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: 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)
@@ -181,12 +188,16 @@
   apply rule
   apply (case_tac "c = xa")
   apply simp_all[2]
+  apply (rotate_tac 1)
+  apply (drule TODO)
+  apply (drule_tac x="(atom ca \<rightleftharpoons> atom x)" in spec)
+  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 clarify
-  apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)
-  apply (simp add: eqvt_at_def)
-  apply clarify
-  apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)
+  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~))")