# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1310407952 -32400
# Node ID d8a6b424f80aec01f475d04ab485071d4369db7f
# Parent  0d95e19e4f935066be2a4e9fd93f37a2526c216a
use eqvt_at_perm

diff -r 0d95e19e4f93 -r d8a6b424f80a Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Mon Jul 11 23:42:52 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Jul 12 03:12:32 2011 +0900
@@ -1,9 +1,6 @@
 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
@@ -104,8 +101,7 @@
   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 (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~))")
@@ -189,8 +185,7 @@
   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 (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~))")
diff -r 0d95e19e4f93 -r d8a6b424f80a Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Mon Jul 11 23:42:52 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Tue Jul 12 03:12:32 2011 +0900
@@ -70,12 +70,11 @@
   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 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 (subgoal_tac "p \<bullet> CPS1_CPS2_sumC (Inr (M, a~)) = CPS1_CPS2_sumC (p \<bullet> (Inr (M, a~)))")
-  apply (simp add: perm_supp_eq fresh_star_def lt.fresh)
   oops
 
 end