# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1307013243 -3600
# Node ID ab6c24ae137fb6e1ab687d2bacc7961d0b4aae48
# Parent  13af2c8d732927ec95b180d5473dc48671895dac# Parent  377bea405940f3133cff345d99adca06d05c1c09
merged

diff -r 377bea405940 -r ab6c24ae137f Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Thu Jun 02 16:41:09 2011 +0900
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 02 12:14:03 2011 +0100
@@ -10,6 +10,36 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+lemma cheat: "P" sorry
+
+nominal_primrec
+  f
+where
+  "f f1 f2 f3 (Var x) = f1 x"
+| "f f1 f2 f3 (App t1 t2) = f2 t1 t2 (f f1 f2 f3 t1) (f f1 f2 f3 t2)"
+| "atom x \<sharp> (f1,f2,f3) \<Longrightarrow> f f1 f2 f3 (Lam [x].t) = f3 x t (f f1 f2 f3 t)"
+unfolding eqvt_def f_graph_def
+apply (rule, perm_simp, rule)
+apply(case_tac x)
+apply(simp)
+apply(rule_tac y="d" in lam.exhaust)
+apply(auto)[1]
+apply(auto simp add: lam.distinct lam.eq_iff)[3]
+apply(blast)
+apply(rule cheat) (* this can be solved *)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+apply(simp)
+sorry (*this could be defined *)
+
+termination sorry
+
+thm f.simps
+
+
+
 
 inductive 
   triv :: "lam \<Rightarrow> nat \<Rightarrow> bool"