(* CPS transformation of Danvy and Filinski *)
theory CPS3_DanvyFilinski_FCB2 
imports Lt 
begin

nominal_function
  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) $$ (Lam c (k (c~)))))))"
| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam 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> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
  apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def)
  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
  oops

end