diff -r 39ae45d3a11b -r 9c0df9901acf Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Sun Jun 19 13:10:15 2011 +0900
@@ -71,13 +71,51 @@
 | "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) =
+| "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<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
+  defer
+  apply (case_tac x)
+  apply (rule_tac y="a" in lt.exhaust)
+  apply auto
+  apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
+  apply (simp add: Abs1_eq_iff)
+  apply blast+
+  apply (rule_tac y="b" in lt.exhaust)
+  apply auto
+  apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)
+  apply (simp add: Abs1_eq_iff)
+  apply blast
+  apply (rule_tac ?'a="name" in obtain_fresh)
+  apply (rule_tac x="(lt1, lt2, a)" and ?'a="name" in obtain_fresh)
+  apply (simp add: fresh_Pair_elim)
+  apply (case_tac "isValue lt1", case_tac [!] "isValue lt2")[1]
+  apply (simp_all add: fresh_Pair)[4]
+--""
+  apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh)
+  apply (subgoal_tac "Abs b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
+  apply (subgoal_tac "Abs ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)")
+  apply (simp only:)
+  apply (erule Abs_lst1_fcb)
+  apply (simp add: Abs_fresh_iff)
+  apply (simp_all add: Abs_fresh_iff lt.fresh fresh_Pair_elim fresh_at_base swap_fresh_fresh)[2]
+  (* need an invariant to get eqvt_at (Proj) *)
+  defer defer
+  apply simp
+  apply (simp_all add: Abs1_eq_iff fresh_Pair_elim fresh_at_base)[2]
+  defer defer
+  defer
+  apply (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
+  apply (rule arg_cong) back
+  defer
+  apply (rule arg_cong) back
+  defer
+  apply (rule arg_cong) back
+  defer
   oops --"The goals seem reasonable"
 
 end