header {* CPS transformation of Danvy and Filinski *}

theory CPS3_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) $ (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 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 "Lam c (ka (c~)) = Lam 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 (thin_tac "eqvt ka")

  apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)

  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam 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 "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam 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 (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)

  oops

end