diff -r 354a930ef18f -r f884760ac6e2 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed Jun 15 09:25:36 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Wed Jun 15 09:50:53 2011 +0900
@@ -605,6 +605,37 @@
 oops (* can this be defined ? *)
   (* Yes, if "sub" is a constant. *)
 
+text {* TODO: nominal_primrec throws RSN if an argument is not in FS, but function works *}
+function q where
+  "q (Lam [x]. M) N = Lam [x]. (Lam [x]. (App M (q (Var x) N)))"
+| "q (Var x) N = Var x"
+| "q (App l r) N = App l r"
+oops
+
+text {* TODO: eqvt_at for the other side *}
+nominal_primrec q where
+  "atom c \<sharp> (x, M) \<Longrightarrow> q (Lam [x]. M) (N :: lam) = Lam [x]. (Lam [c]. (App M (q (Var c) N)))"
+| "q (Var x) N = Var x"
+| "q (App l r) N = App l r"
+unfolding eqvt_def q_graph_def
+apply (rule, perm_simp, rule)
+apply (rule TrueI)
+apply (case_tac x)
+apply (rule_tac y="a" in lam.exhaust)
+apply simp_all
+apply blast
+apply blast
+apply (rule_tac x="(name, lam)" and ?'a="name" in obtain_fresh)
+apply blast
+apply clarify
+apply (rule_tac x="(x, xa, M, Ma, c, ca, Na)" and ?'a="name" in obtain_fresh)
+apply (subgoal_tac "eqvt_at q_sumC (Var ca, Na)") --"Could come from nominal_function?"
+apply (subgoal_tac "Lam [c]. App M (q_sumC (Var c, Na)) = Lam [a]. App M (q_sumC (Var a, Na))")
+apply (subgoal_tac "Lam [ca]. App Ma (q_sumC (Var ca, Na)) = Lam [a]. App Ma (q_sumC (Var a, Na))")
+apply (simp only:)
+apply (erule Abs_lst1_fcb)
+oops
+
 text {* Working Examples *}
 
 nominal_primrec