--- a/Nominal/Ex/Lambda.thy	Thu Jun 16 11:03:01 2011 +0100
+++ b/Nominal/Ex/Lambda.thy	Thu Jun 16 12:12:25 2011 +0100
@@ -10,8 +10,9 @@
 | App "lam" "lam"
 | Lam x::"name" l::"lam"  bind x in l ("Lam [_]. _" [100, 100] 100)
 
+text {* free name function *}
 
-text {* free name function - returns an atom list *}
+text {* first returns an atom list *}
 
 nominal_primrec 
   frees_lst :: "lam \<Rightarrow> atom list"
@@ -38,7 +39,7 @@
 lemma shows "supp t = set (frees_lst t)"
   by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base)
 
-text {* free name function - returns an atom set *}
+text {* second returns an atom set - therefore needs an invariant *}
 
 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y")
   frees_set :: "lam \<Rightarrow> atom set"
@@ -173,8 +174,6 @@
 apply(simp_all add: swap_fresh_fresh)
 done
 
-declare lam.size[simp]
-
 termination
   by lexicographic_order
 
@@ -362,7 +361,7 @@
 termination
   by lexicographic_order
 
-text {* count bound-variable occurences *}
+text {* count the bound-variable occurences in a lambda-term *}
 
 nominal_primrec
   cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat"
@@ -521,15 +520,15 @@
 (* function that evaluates a lambda term *)
 nominal_primrec
    eval :: "lam \<Rightarrow> lam" and
-   app :: "lam \<Rightarrow> lam \<Rightarrow> lam"
+   apply_subst :: "lam \<Rightarrow> lam \<Rightarrow> lam"
 where
   "eval (Var x) = Var x"
 | "eval (Lam [x].t) = Lam [x].(eval t)"
-| "eval (App t1 t2) = sub (eval t1) (eval t2)"
-| "app (Var x) t2 = App (Var x) t2"
-| "app (App t0 t1) t2 = App (App t0 t1) t2"
-| "atom x \<sharp> t2 \<Longrightarrow> app (Lam [x].t1) t2 = eval (t1[x::= t2])"
-apply(simp add: eval_app_graph_def eqvt_def)
+| "eval (App t1 t2) = apply_subst (eval t1) (eval t2)"
+| "apply_subst (Var x) t2 = App (Var x) t2"
+| "apply_subst (App t0 t1) t2 = App (App t0 t1) t2"
+| "atom x \<sharp> t2 \<Longrightarrow> apply_subst (Lam [x].t1) t2 = eval (t1[x::= t2])"
+apply(simp add: eval_apply_subst_graph_def eqvt_def)
 apply(rule, perm_simp, rule)
 apply(rule TrueI)
 apply (case_tac x)
@@ -551,7 +550,6 @@
 apply (simp add: fresh_Inl)
 apply (simp add: eqvt_at_def)
 apply simp
-defer
 apply clarify
 apply(erule Abs_lst1_fcb)
 apply (erule fresh_eqvt_at)
@@ -567,15 +565,20 @@
 apply assumption+
 apply rule
 apply simp
-oops (* can this be defined ? *)
-  (* Yes, if "sub" is a constant. *)
+done
+
+
+(* a small test
+termination sorry
 
-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
+lemma 
+  assumes "x \<noteq> y"
+  shows "eval (App (Lam [x].App (Var x) (Var x)) (Var y)) = App (Var y) (Var y)"
+using assms
+apply(simp add: lam.supp fresh_def supp_at_base)
+done
+*)
+
 
 text {* TODO: eqvt_at for the other side *}
 nominal_primrec q where