# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1270133734 -7200
# Node ID d803c0adfcf8cae8d0e3454940635ae90b1d6d31
# Parent  79569dd3479b3671bc06e6755b55f4c9339709c0
fv_perm_bn

diff -r 79569dd3479b -r d803c0adfcf8 Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Thu Apr 01 16:17:56 2010 +0200
+++ b/Nominal/ExLet.thy	Thu Apr 01 16:55:34 2010 +0200
@@ -6,7 +6,7 @@
 
 atom_decl name
 
-ML {* val _ = recursive := true *}
+ML {* val _ = recursive := false *}
 ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
@@ -85,6 +85,13 @@
   apply(simp_all add:permute_bn eqvts)
   done
 
+lemma fv_perm_bn:
+  "fv_bn l = fv_bn (permute_bn p l)"
+  apply(induct l rule: trm_lts.inducts(2))
+  apply(rule TrueI)
+  apply(simp_all add:permute_bn eqvts)
+  done
+
 lemma Lt_subst:
   "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
   apply (simp only: trm_lts.eq_iff)