--- a/LamEx.thy	Fri Oct 30 14:25:37 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 15:28:44 2009 +0100
@@ -4,6 +4,8 @@
 
 atom_decl name
 
+thm abs_fresh(1)
+
 nominal_datatype rlam =
   rVar "name"
 | rApp "rlam" "rlam"
@@ -16,6 +18,16 @@
 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
 | a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a\<sharp>[b].s\<rbrakk> \<Longrightarrow> rLam a t \<approx> rLam b s"
 
+function
+  rfv :: "rlam \<Rightarrow> name set"
+where
+  rfv_var: "rfv (rVar a) = {a}"
+| rfv_app: "rfv (rApp t1 t2) = (rfv t1) \<union> (rfv t2)"
+| rfv_lam: "rfv (rLam a t) = (rfv t) - {a}"
+sorry
+
+termination rfv sorry 
+
 quotient lam = rlam / alpha
 sorry
 
@@ -40,6 +52,13 @@
 thm App_def
 thm Lam_def
 
+quotient_def (for lam)
+  fv :: "lam \<Rightarrow> name set"
+where
+  "fv \<equiv> rfv"
+
+thm fv_def
+
 (* definition of overloaded permutation function *)
 (* for the lifted type lam                       *)
 overloading
@@ -77,8 +96,20 @@
   shows "(pi\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
   sorry
 
+lemma fv_var:
+  shows "fv (Var a) = {a}"
+sorry
+
+lemma fv_app:
+  shows "fv (App t1 t2) = (fv t1) \<union> (fv t2)"
+sorry
+
+lemma fv_lam:
+  shows "fv (Lam a t) = (fv t) - {a}"
+sorry 
+
 lemma real_alpha:
-  assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>s"
+  assumes "t = ([(a,b)]\<bullet>s)" "a\<sharp>[b].s"
   shows "Lam a t = Lam b s"
 sorry