# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1256913124 -3600
# Node ID 55b156ac4a4046df7754388d5219d26918a0b32e
# Parent  42dac1cfcd14d06d04638fafcec6b38cdd24c9ed# Parent  47de63a883c2d6a5b4b94b8653f540e48e166371
merged

diff -r 47de63a883c2 -r 55b156ac4a40 FSet.thy
--- a/FSet.thy	Fri Oct 30 15:22:59 2009 +0100
+++ b/FSet.thy	Fri Oct 30 15:32:04 2009 +0100
@@ -169,9 +169,9 @@
 
 (* FIXME: does not work yet for all types*)
 quotient_def (for "'a fset")
-  fmap::"('a \<Rightarrow> 'a) \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
+  fmap::"('a \<Rightarrow> 'b) \<Rightarrow> 'a fset \<Rightarrow> 'b fset"
 where
-  "fmap \<equiv> (map::('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list)"
+  "fmap \<equiv> (map::('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list)"
 
 term map
 term fmap
diff -r 47de63a883c2 -r 55b156ac4a40 LamEx.thy
--- a/LamEx.thy	Fri Oct 30 15:22:59 2009 +0100
+++ b/LamEx.thy	Fri Oct 30 15:32:04 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,6 +96,18 @@
   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>[b].s"
   shows "Lam a t = Lam b s"