--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Thu Jun 16 13:32:36 2011 +0100
@@ -0,0 +1,83 @@
+header {* CPS transformation of Danvy and Nielsen *}
+theory DanvyNielsen
+imports Lt
+begin
+
+nominal_datatype cpsctxt =
+  Hole
+| CFun cpsctxt lt
+| CArg lt cpsctxt
+| CAbs x::name c::cpsctxt bind x in c
+
+nominal_primrec
+  fill   :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt"         ("_<_>" [200, 200] 100)
+where
+  fill_hole : "Hole<M> = M"
+| fill_fun  : "(CFun C N)<M> = (C<M>) $ N"
+| fill_arg  : "(CArg N C)<M> = N $ (C<M>)"
+| fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Abs x (C<M>)"
+  unfolding eqvt_def fill_graph_def
+  apply perm_simp
+  apply auto
+  apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
+  apply (auto simp add: fresh_star_def)
+  apply (erule Abs_lst1_fcb)
+  apply (simp_all add: Abs_fresh_iff)
+  apply (erule fresh_eqvt_at)
+  apply (simp add: finite_supp)
+  apply (simp add: fresh_Pair)
+  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  done
+
+termination
+  by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
+
+lemma [eqvt]: "p \<bullet> fill c t = fill (p \<bullet> c) (p \<bullet> t)"
+  by (nominal_induct c avoiding: t rule: cpsctxt.strong_induct) simp_all
+
+nominal_primrec
+  ccomp :: "cpsctxt => cpsctxt => cpsctxt"
+where
+  "ccomp Hole C  = C"
+| "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')"
+| "ccomp (CArg N C) C' = CArg N (ccomp C C')"
+| "ccomp (CFun C N) C'  = CFun (ccomp C C') N"
+  unfolding eqvt_def ccomp_graph_def
+  apply perm_simp
+  apply auto
+  apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
+  apply (auto simp add: fresh_star_def)
+  apply blast+
+  apply (erule Abs_lst1_fcb)
+  apply (simp_all add: Abs_fresh_iff)
+  apply (erule fresh_eqvt_at)
+  apply (simp add: finite_supp)
+  apply (simp add: fresh_Pair)
+  apply (simp add: eqvt_at_def swap_fresh_fresh)
+  done
+
+termination
+  by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
+
+lemma [eqvt]: "p \<bullet> ccomp c c' = ccomp (p \<bullet> c) (p \<bullet> c')"
+  by (nominal_induct c avoiding: c' rule: cpsctxt.strong_induct) simp_all
+
+nominal_primrec
+    CPSv :: "lt => lt"
+and CPS :: "lt => cpsctxt" where
+  "CPSv (Var x) = x~"
+| "CPS (Var x) = CFun Hole (x~)"
+| "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))"
+| "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))"
+| "CPSv (M $ N) = Abs x (Var x)"
+| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole"
+| "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =
+     ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))"
+| "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =
+     ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))"
+| "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) =
+     ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))"
+  apply auto
+  oops --"The goals seem reasonable"
+
+end