--- a/Nominal/Term1.thy	Fri Mar 05 17:09:48 2010 +0100
+++ b/Nominal/Term1.thy	Fri Mar 05 18:14:04 2010 +0100
@@ -198,6 +198,42 @@
 lemma Collect_neg_conj: "{x. \<not>(P x \<and> Q x)} = {x. \<not>(P x)} \<union> {x. \<not>(Q x)}"
 by (simp add: Collect_imp_eq Collect_neg_eq[symmetric])
 
+lemma "
+{a\<Colon>atom. infinite ({b\<Colon>atom. \<not> (\<exists>pi\<Colon>perm. P pi a b \<and> Q pi a b)})} =
+{a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. P p a b)}} \<union>
+{a\<Colon>atom. infinite {b\<Colon>atom. \<not> (\<exists>p\<Colon>perm. Q p a b)}}"
+oops
+
+lemma inf_or: "(infinite x \<or> infinite y) = infinite (x \<union> y)"
+by (simp add: finite_Un)
+
+
+lemma supp_fv_let:
+  assumes sa : "fv_bp bp = supp bp"
+  shows "\<lbrakk>fv_trm1 rtrm11 = supp rtrm11; fv_trm1 rtrm12 = supp rtrm12\<rbrakk>
+       \<Longrightarrow> supp (Lt1 bp rtrm11 rtrm12) = fv_trm1 (Lt1 bp rtrm11 rtrm12)"
+apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv])
+apply(fold supp_Abs)
+apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv,symmetric])
+apply(simp (no_asm) only: supp_def permute_set_eq permute_trm1 alpha1_INJ)
+apply(simp only: ex_out Collect_neg_conj permute_ABS Abs_eq_iff)
+apply(simp only: alpha_bp_eq fv_eq_bv)
+apply(simp only: alpha_gen fv_eq_bv supp_Pair)
+apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric])
+apply(simp only: Un_left_commute)
+apply simp
+apply(simp add: fresh_star_def) apply(fold fresh_star_def)
+apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric])
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
+apply(simp only: Un_assoc[symmetric])
+apply(simp only: Un_commute)
+apply(simp only: Un_left_commute)
+apply(simp only: Un_assoc[symmetric])
+apply(simp only: Un_commute)
+apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
+apply(simp only: Collect_disj_eq[symmetric] inf_or)
+sorry
+
 lemma supp_fv:
   "supp t = fv_trm1 t"
   "supp b = fv_bp b"
@@ -221,6 +257,7 @@
 apply(simp add: supp_at_base)
 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
+(*apply(rule supp_fv_let) apply(simp_all)*)
 apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (rtrm12)) \<union> supp(rtrm11)")
 (*apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp (Abs (bv1 bp) (bp, rtrm12)) \<union> supp(rtrm11)")*)
 apply(simp add: supp_Abs fv_trm1 supp_Pair Un_Diff Un_assoc fv_eq_bv)