# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268816274 -3600
# Node ID 4fa5365cd871224c96fc4611b5d3978bdcd3ab29
# Parent  7fe643ad19e47e5dbf58a36692a3db7d24c35f6d
Fix in alpha; support of the recursive Let works :)

diff -r 7fe643ad19e4 -r 4fa5365cd871 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 17 09:42:56 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 09:57:54 2010 +0100
@@ -364,13 +364,16 @@
           val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no
                                        | ((SOME (_, false), _, j), _) => j = arg_no
                                        | _ => false) bind_pis;
+          val rel_has_rec_binds = filter 
+            (fn ((SOME (_, true), _, j), _) => j = arg_no | _ => false) bind_pis;
         in
-          case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of
-            ([], [], []) =>
+          case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds, rel_has_rec_binds) of
+            ([], [], [], []) =>
               if is_rec_type dt then (nth alpha_frees (body_index dt) $ arg $ arg2)
               else (HOLogic.mk_eq (arg, arg2))
-          | (_, [], []) => @{term True}
-          | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), []) =>
+          | (_, [], [], []) => @{term True}
+          | ([], [], [], _) => @{term True}
+          | ([], ((((SOME (bn, is_rec)), _, _), pi) :: _), [], []) =>
             if not (bns_same rel_in_comp_binds) then error "incompatible bindings for an argument" else
             if is_rec then
               let
@@ -409,7 +412,7 @@
               in
                 alpha_bn_const $ arg $ arg2
               end
-          | ([], [], relevant) =>
+          | ([], [], relevant, []) =>
             let
               val (rbinds, rpis) = split_list relevant
               val lhs_binds = fv_binds args rbinds
diff -r 7fe643ad19e4 -r 4fa5365cd871 Nominal/Test.thy
--- a/Nominal/Test.thy	Wed Mar 17 09:42:56 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 09:57:54 2010 +0100
@@ -131,7 +131,7 @@
 thm lam'_bp'_distinct
 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
 
-lemma supp_fv:
+lemma supp_fv':
   shows "supp t = fv_lam' t" 
   and "supp bp = fv_bp' bp"
 apply(induct t and bp rule: lam'_bp'_inducts)
@@ -174,9 +174,21 @@
 apply(simp only: eqvts split_def fst_conv snd_conv)
 apply(simp only: eqvts[symmetric] supp_Pair)
 apply(simp only: eqvts Pair_eq)
-oops
+apply(simp add: supp_Abs supp_Pair)
+apply blast
+apply(simp only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base supp_atom)
+apply simp
+done
 
-thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+thm lam'_bp'_fv[simplified supp_fv'[symmetric]]
 
 
 text {* example 2 *}