Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use eqvt_at_perm
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 12 Jul 2011 03:12:32 +0900
changeset 2965 d8a6b424f80a
parent 2964 0d95e19e4f93
child 2966 fa37c2a33812
use eqvt_at_perm
Nominal/Ex/CPS/CPS3_DanvyFilinski.thy file | annotate | diff | comparison | revisions
Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy file | annotate | diff | comparison | revisions 
--- 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~))")
--- 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
nominal2