diff -r 2b98012307f7 -r 693df83172f0 Nominal/Term1.thy
--- a/Nominal/Term1.thy	Thu Mar 04 18:57:23 2010 +0100
+++ b/Nominal/Term1.thy	Fri Mar 05 09:41:22 2010 +0100
@@ -138,9 +138,9 @@
   apply(simp_all add: supp_atom)
   done
 
-instance trm1 :: fs
+instance trm1 and bp :: fs
 apply default
-apply (rule rtrm1_bp_fs(1))
+apply (rule rtrm1_bp_fs)+
 done
 
 lemma fv_eq_bv: "fv_bp bp = bv1 bp"
@@ -173,7 +173,7 @@
 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
 apply(simp only: supp_at_base[simplified supp_def])
 apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp add: Collect_imp_eq Collect_neg_eq)
+apply(simp add: Collect_imp_eq Collect_neg_eq Un_commute)
 apply(subgoal_tac "supp (Lm1 name rtrm1) = supp (Abs {atom name} rtrm1)")
 apply(simp add: supp_Abs fv_trm1)
 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt permute_trm1)
@@ -181,21 +181,29 @@
 apply(simp add: Abs_eq_iff)
 apply(simp add: alpha_gen.simps)
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
-apply(subgoal_tac "supp (Lt1 bp rtrm11 rtrm12) = supp(rtrm11) \<union> supp (Abs (bv1 bp) rtrm12)")
-apply(simp add: supp_Abs fv_trm1 fv_eq_bv)
-apply(simp (no_asm) add: supp_def permute_trm1)
-apply(simp add: alpha1_INJ alpha_bp_eq)
-apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen)
-apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
-apply(simp add: Collect_imp_eq Collect_neg_eq fresh_star_def helper2)
+defer
 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
 apply(simp (no_asm) add: supp_def eqvts)
 apply(fold supp_def)
 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])
-done
+(*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)
+apply(blast) (* Un_commute in a good place *)
+apply(simp (no_asm) only: supp_def permute_trm1)
+apply(simp only: alpha1_INJ)
+apply(simp only: Un_commute)
+apply(simp add: Collect_imp_eq)
+apply(simp add: Collect_neg_eq[symmetric])
+apply(simp only: Abs_eq_iff)
+apply(simp add: alpha_bp_eq)
+apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
+apply(simp add: alpha_gen fv_eq_bv supp_Pair)
+apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv)
+apply(simp add: Collect_imp_eq Collect_neg_eq Collect_disj_eq fresh_star_def helper2)
+sorry
 
 lemma trm1_supp:
   "supp (Vr1 x) = {atom x}"