1 header {* CPS transformation of Danvy and Filinski *}

     2 theory CPS3_DanvyFilinski_FCB2 

     3 imports Lt 

     4 begin

     5 

     6 nominal_primrec

     7   CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)

     8 and

     9   CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)

    10 where

    11   "eqvt k \<Longrightarrow> (x~)*k = k (x~)"

    12 | "eqvt k \<Longrightarrow> (M $$ N)*k = M*(%m. (N*(%n.((m $$ n) $$ (Lam c (k (c~)))))))"

    13 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))"

    14 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"

    15 | "(x~)^l = l $$ (x~)"

    16 | "(M $$ N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"

    17 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"

    18   apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def)

    19   apply (auto simp only:)

    20   apply (case_tac x)

    21   apply (case_tac a)

    22   apply (case_tac "eqvt b")

    23   apply (rule_tac y="aa" in lt.strong_exhaust)

    24   apply auto

    25   oops

    26 

    27 end

    28 

    29 

    30