--- a/Nominal/LFex.thy	Fri Mar 05 14:55:21 2010 +0100
+++ b/Nominal/LFex.thy	Fri Mar 05 14:56:19 2010 +0100
@@ -50,11 +50,9 @@
    (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))"
 apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-apply (erule alpha_gen_compose_eqvt)
-apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
-apply (erule alpha_gen_compose_eqvt)
-apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
-apply (erule alpha_gen_compose_eqvt)
+apply (erule_tac [!] conjE)+
+apply (erule_tac [!] exi[of _ _ "p"])
+apply (erule_tac [!] alpha_gen_compose_eqvt)
 apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
 done
 
@@ -160,6 +158,14 @@
 apply(simp_all only: kind_ty_trm_fs)
 done
 
+lemma ex_out: 
+  "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
+  "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
+  "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+  "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+apply (blast)+
+done
+
 lemma supp_eqs:
   "supp TYP = {}"
   "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPI rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
@@ -170,13 +176,15 @@
   "supp (VAR x) = {atom x}"
   "supp (APP M N) = supp M \<union> supp N"
   "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
-  apply(simp_all (no_asm) add: supp_def)
+  apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt)
   apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen)
-  apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric])
-  apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute)
-  apply(simp_all add: supp_at_base[simplified supp_def])
+  apply(simp_all only:ex_out)
+  apply(simp_all only: supp_eqvt[symmetric] fv_eqvt[symmetric] eqvts[symmetric])
+  apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric])
+  apply(simp_all add: supp_at_base[simplified supp_def] Un_commute)
   done
 
+
 lemma supp_fv:
   "supp t1 = fv_kind t1"
   "supp t2 = fv_ty t2"

--- a/Nominal/Term1.thy	Fri Mar 05 14:55:21 2010 +0100
+++ b/Nominal/Term1.thy	Fri Mar 05 14:56:19 2010 +0100
@@ -138,14 +138,18 @@
   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_pre: "fv_bp bp = bv1 bp"
+apply(induct bp rule: trm1_bp_inducts(2))
+apply(simp_all)
 done
 
-lemma fv_eq_bv: "fv_bp bp = bv1 bp"
-apply(induct bp rule: trm1_bp_inducts(2))
-apply(simp_all)
+lemma fv_eq_bv: "fv_bp = bv1"
+apply(rule ext)
+apply(rule fv_eq_bv_pre)
 done
 
 lemma helper2: "{b. \<forall>pi. pi \<bullet> (a \<rightleftharpoons> b) \<bullet> bp \<noteq> bp} = {}"
@@ -165,6 +169,35 @@
 apply (rule alpha_bp_eq_eq)
 done
 
+lemma ex_out: 
+  "(\<exists>x. Z x \<and> Q) = (Q \<and> (\<exists>x. Z x))"
+  "(\<exists>x. Q \<and> Z x) = (Q \<and> (\<exists>x. Z x))"
+  "(\<exists>x. P x \<and> Q \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+  "(\<exists>x. Q \<and> P x \<and> Z x) = (Q \<and> (\<exists>x. P x \<and> Z x))"
+  "(\<exists>x. Q \<and> P x \<and> Z x \<and> W x) = (Q \<and> (\<exists>x. P x \<and> Z x \<and> W x))"
+apply (blast)+
+done
+
+lemma "(Abs bs (x, x') = Abs cs (y, y')) = (\<exists>p. (bs, x) \<approx>gen op = supp p (cs, y) \<and> (bs, x') \<approx>gen op = supp p (cs, y'))"
+thm Abs_eq_iff
+apply (simp add: Abs_eq_iff)
+apply (rule arg_cong[of _ _ "Ex"])
+apply (rule ext)
+apply (simp only: alpha_gen)
+apply (simp only: supp_Pair eqvts)
+apply rule
+apply (erule conjE)+
+oops
+
+lemma "(f (p \<bullet> bp), p \<bullet> bp) \<approx>gen op = f pi (f bp, bp) = False"
+apply (simp add: alpha_gen fresh_star_def)
+oops
+
+(* TODO: permute_ABS should be in eqvt? *)
+
+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 supp_fv:
   "supp t = fv_trm1 t"
   "supp b = fv_bp b"
@@ -173,7 +206,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 +214,31 @@
 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_set_eq atom_eqvt permute_trm1)
+apply(simp only: alpha1_INJ permute_ABS permute_prod.simps Abs_eq_iff)
+apply(simp only: ex_out)
+apply(simp only: Un_commute)
+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)
+apply(simp only: ex_out)
+apply(simp only: Collect_neg_conj finite_Un Diff_cancel)
+apply(simp)
+apply(simp add: Collect_imp_eq)
+apply(simp add: Collect_neg_eq[symmetric] fresh_star_def)
+apply(fold supp_def)
+sorry
 
 lemma trm1_supp:
   "supp (Vr1 x) = {atom x}"