--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Thu Jun 16 22:00:52 2011 +0900
@@ -0,0 +1,240 @@
+header {* CPS transformation of Danvy and Filinski *}
+theory DanvyFilinski imports Lt begin
+
+nominal_primrec
+  CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)
+and
+  CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
+where
+  "eqvt k \<Longrightarrow> (x~)*k = k (x~)"
+| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))"
+| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))"
+| "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
+| "(x~)^l = l $ (x~)"
+| "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
+| "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))"
+  apply (simp only: eqvt_def CPS1_CPS2_graph_def)
+  apply (rule, perm_simp, rule)
+  apply auto
+  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 "Abs c (ka (c~)) = Abs 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 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 "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs 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 "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs 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 "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
+  apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs 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 (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 (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 "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs 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 "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs 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 "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
+  apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs 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 (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 (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
+  by lexicographic_order
+
+definition psi:: "lt => lt"
+  where "psi V == V*(\<lambda>x. x)"
+
+section {* Simple consequence of CPS *}
+
+lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"
+  apply (cases V rule: lt.exhaust)
+  apply (auto simp add: psi_def)
+  apply (subst CPS1.simps)
+  apply (simp add: eqvt_def eqvt_bound eqvt_lambda)
+  apply rule
+  apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
+  apply (subst CPS1.simps(3))
+  apply assumption+
+  apply (subst CPS1.simps(3))
+  apply (simp add: eqvt_def eqvt_bound eqvt_lambda)
+  apply assumption
+  apply rule
+  done
+
+end
+
+
+