--- a/Nominal/Term1.thy	Fri Mar 12 12:42:35 2010 +0100
+++ b/Nominal/Term1.thy	Fri Mar 12 17:42:31 2010 +0100
@@ -12,9 +12,9 @@
 | rLm1 "name" "rtrm1"        --"name is bound in trm1"
 | rLt1 "bp" "rtrm1" "rtrm1"   --"all variables in bp are bound in the 2nd trm1"
 and bp =
-  BUnit
-| BVr "name"
-| BPr "bp" "bp"
+(*  BUnit*)
+ BVr "name"
+(*| BPr "bp" "bp"*)
 
 print_theorems
 
@@ -23,9 +23,9 @@
 primrec 
   bv1
 where
-  "bv1 (BUnit) = {}"
-| "bv1 (BVr x) = {atom x}"
-| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"
+(*  "bv1 (BUnit) = {}"*)
+ "bv1 (BVr x) = {atom x}"
+(*| "bv1 (BPr bp1 bp2) = (bv1 bp1) \<union> (bv1 bp2)"*)
 
 setup {* snd o define_raw_perms (Datatype.the_info @{theory} "Term1.rtrm1") 2 *}
 thm permute_rtrm1_permute_bp.simps
@@ -33,13 +33,13 @@
 local_setup {*
   snd o define_fv_alpha (Datatype.the_info @{theory} "Term1.rtrm1")
   [[[], [], [(NONE, 0, 1)], [(SOME (@{term bv1}, true), 0, 2)]],
-  [[], [], []]] [(@{term bv1}, 1, [[], [0], [0, 1]])] *}
+  [[](*, [], []*)]] [(@{term bv1}, 1, [(*[],*) [0](*, [0, 1]*)])] *}
 
 notation
   alpha_rtrm1 ("_ \<approx>1 _" [100, 100] 100) and
   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
 thm alpha_rtrm1_alpha_bp_alpha_bv1.intros
-thm fv_rtrm1_fv_bp.simps[no_vars]
+(*thm fv_rtrm1_fv_bp.simps[no_vars]*)
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha1_inj}, []), (build_alpha_inj @{thms alpha_rtrm1_alpha_bp_alpha_bv1.intros} @{thms rtrm1.distinct rtrm1.inject bp.distinct bp.inject} @{thms alpha_rtrm1.cases alpha_bp.cases alpha_bv1.cases} ctxt)) ctxt)) *}
 thm alpha1_inj
@@ -134,9 +134,9 @@
   "(supp t \<union> supp s) supports (Ap1 t s)"
   "(supp (atom x) \<union> supp t) supports (Lm1 x t)"
   "(supp b \<union> supp t \<union> supp s) supports (Lt1 b t s)"
-  "{} supports BUnit"
+(*  "{} supports BUnit"*)
   "(supp (atom x)) supports (BVr x)"
-  "(supp a \<union> supp b) supports (BPr a b)"
+(*  "(supp a \<union> supp b) supports (BPr a b)"*)
 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *})
 done
 
@@ -215,10 +215,11 @@
 by (simp add: finite_Un)
 
 
+
 lemma supp_fv_let:
   assumes sa : "fv_bp bp = supp bp"
-  shows "\<lbrakk>fv_trm1 trm11 = supp trm11; fv_trm1 trm12 = supp trm12\<rbrakk>
-       \<Longrightarrow> supp (Lt1 bp trm11 trm12) = fv_trm1 (Lt1 bp trm11 trm12)"
+  shows "\<lbrakk>fv_trm1 ta = supp ta; fv_trm1 tb = supp tb\<rbrakk>
+       \<Longrightarrow> supp (Lt1 bp ta tb) = fv_trm1 (Lt1 bp ta tb)"
 apply(simp only: fv_trm1 fv_eq_bv sa[simplified fv_eq_bv])
 apply simp
 apply(fold supp_Abs)
@@ -235,8 +236,30 @@
 apply(simp only: Collect_disj_eq)
 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 apply(simp only: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric] bv1_eqvt fv_eq_bv sa[simplified fv_eq_bv,symmetric])
-apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric])
-apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric])
+apply(induct bp)
+apply(simp_all only: TrueI)
+apply(simp_all only: permute_trm1)
+apply(simp_all only: bv1.simps)
+apply(simp_all only: alpha1_INJ) (* Doesn't look true... *)
+apply(simp)
+sorry
+
+lemma
+"(\<not> (\<exists>p. (a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)} = supp tb - {atom name} \<and>
+ ({atom (p \<bullet> (a \<rightleftharpoons> b) \<bullet> name)} = {atom name}) \<and>
+ ((a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)}) \<sharp>* p \<and>
+ p \<bullet> (a \<rightleftharpoons> b) \<bullet> tb = tb)) =
+ (\<not> (\<exists>p. (a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)} = supp tb - {atom name} \<and>
+ ((a \<rightleftharpoons> b) \<bullet> supp tb - {atom ((a \<rightleftharpoons> b) \<bullet> name)}) \<sharp>* p \<and>
+ p \<bullet> (a \<rightleftharpoons> b) \<bullet> tb = tb))"
+apply simp
+apply rule
+prefer 2
+apply (meson)[2]
+apply clarify
+apply (erule_tac x="p" in allE)
+apply simp
+apply (simp add: atom_eqvt[symmetric])
 sorry
 
 lemma supp_fv: