# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264745392 -3600
# Node ID c25ff084868f1522e6117f89f3c9d8d948e69349
# Parent  af02b193a19a8d191c8df9240ce17104e03d7c39
now also final step is proved - the supp of lambdas is now completely characterised

diff -r af02b193a19a -r c25ff084868f Quot/Nominal/LamEx.thy
--- a/Quot/Nominal/LamEx.thy	Fri Jan 29 00:22:00 2010 +0100
+++ b/Quot/Nominal/LamEx.thy	Fri Jan 29 07:09:52 2010 +0100
@@ -428,6 +428,11 @@
 apply(lifting rfv_var rfv_app rfv_lam)
 done
 
+lemma fv_eqvt:
+  shows "(p \<bullet> fv t) = fv (p \<bullet> t)"
+apply(lifting rfv_eqvt)
+done
+
 lemma a1: 
   "a = b \<Longrightarrow> Var a = Var b"
   by  (lifting a1)
@@ -547,7 +552,7 @@
 apply(simp add: Collect_imp_eq Collect_neg_eq)
 done
 
-(* needs thinking *)
+(* supp for lam *)
 lemma lam_supp1:
   shows "(supp (atom x, t)) supports (Lam x t) "
 apply(simp add: supports_def)
@@ -574,11 +579,24 @@
 apply(simp add: lam_fsupp1)
 done
 
+lemma supp_fv:
+  shows "supp t = fv t"
+apply(induct t rule: lam_induct)
+apply(simp add: var_supp)
+apply(simp add: app_supp)
+apply(subgoal_tac "supp (Lam name lam) = supp (Abs {atom name} lam)")
+apply(simp add: supp_Abs)
+apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
+apply(simp add: Lam_pseudo_inject)
+apply(simp add: abs_eq)
+apply(simp add: supp_eqvt[symmetric] fv_eqvt[symmetric])
+done
+
 lemma lam_supp2:
   shows "supp (Lam x t) = supp (Abs {atom x} t)"
 apply(simp add: supp_def permute_set_eq atom_eqvt)
 apply(simp add: Lam_pseudo_inject)
-apply(simp add: abs_eq)
+apply(simp add: abs_eq supp_fv)
 sorry
 
 lemma lam_supp: