# HG changeset patch
# User urbanc
# Date 1164635421 -3600
# Node ID 3c8e29a6e4f0aa606cc7dd961ca37cef3c2439a6
# Parent  e0ffb2d13f9fe7270998caf6bb00ed3466ccc4bc
added the function for free variables of a lambda-term, which is a
tad more difficult to define than capture-avoiding substitution

diff -r e0ffb2d13f9f -r 3c8e29a6e4f0 src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Mon Nov 27 14:33:18 2006 +0100
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Mon Nov 27 14:50:21 2006 +0100
@@ -10,6 +10,8 @@
                      | App "lam" "lam"
                      | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
+text {* depth of a lambda-term *}
+
 consts 
   depth :: "lam \<Rightarrow> nat"
 
@@ -23,6 +25,36 @@
   apply(fresh_guess add: perm_nat_def)+
   done
 
+text {* free variables of a lambda-term *}
+
+consts 
+  frees :: "lam \<Rightarrow> name set"
+
+nominal_primrec (invariant: "\<lambda>s::name set. finite s")
+  "frees (Var a) = {a}"
+  "frees (App t1 t2) = (frees t1) \<union> (frees t2)"
+  "frees (Lam [a].t) = (frees t) - {a}"
+apply(finite_guess add: perm_insert perm_set_def)
+apply(finite_guess add: perm_union)
+apply(finite_guess add: pt_set_diff_eqvt[OF pt_name_inst, OF at_name_inst] perm_insert)
+apply(simp add: perm_set_def)
+apply(simp add: fs_name1)
+apply(simp)+
+apply(simp add: fresh_def)
+apply(simp add: supp_of_fin_sets[OF pt_name_inst, OF at_name_inst, OF fs_at_inst[OF at_name_inst]])
+apply(simp add: supp_atm)
+apply(force)
+apply(fresh_guess add: perm_insert perm_set_def)
+apply(fresh_guess add: perm_union)
+apply(fresh_guess add: pt_set_diff_eqvt[OF pt_name_inst, OF at_name_inst] perm_insert)
+apply(simp add: perm_set_def)
+done
+
+lemma frees_equals_support:
+  shows "frees t = supp t"
+by (nominal_induct t rule: lam.induct)
+   (simp_all add: lam.supp supp_atm abs_supp)
+
 text {* capture-avoiding substitution *}
 
 lemma eq_eqvt: