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+
−