--- a/Nominal/Ex/SingleLet.thy	Fri Jul 16 05:09:45 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Sat Jul 17 10:25:29 2010 +0100
@@ -114,7 +114,7 @@
 instance trm :: pt sorry
 instance assg :: pt sorry
 
-lemma
+lemma b1:
   "p \<bullet> Var name = Var (p \<bullet> name)"
   "p \<bullet> App trm1 trm2 = App (p \<bullet> trm1) (p \<bullet> trm2)"
   "p \<bullet> Lam name trm = Lam (p \<bullet> name) (p \<bullet> trm)"
@@ -133,43 +133,39 @@
 *}
 *)
 
+thm eq_iff[no_vars]
+
+ML {*
+  val q1 = lift_thm [@{typ trm}, @{typ assg}] @{context} @{thm "eq_iff"(1)}
+*}
+
 local_setup {* Local_Theory.note ((@{binding d1}, []), thms_d) #> snd *}
 local_setup {* Local_Theory.note ((@{binding i1}, []), thms_i) #> snd *}
 local_setup {* Local_Theory.note ((@{binding f1}, []), thms_f) #> snd *}
+local_setup {* Local_Theory.note ((@{binding q1}, []), [q1]) #> snd *}
+
 
 thm perm_defs
 thm perm_simps
 
-instance trm :: pt sorry
-instance assg :: pt sorry
-
 lemma supp_fv:
   "supp t = fv_trm t"
   "supp b = fv_bn b"
 apply(induct t and b rule: i1)
 apply(simp_all add: f1)
 apply(simp_all add: supp_def)
-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 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)
-apply(simp add: alpha1_INJ)
-apply(simp add: Abs_eq_iff)
-apply(simp add: alpha_gen.simps)
-apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
-apply(simp add: supp_fv_let fv_trm1 fv_eq_bv supp_Pair)
-apply blast
-apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp add: supp_def permute_trm1 alpha1_INJ fv_trm1)
-apply(simp only: supp_at_base[simplified supp_def])
-apply(simp (no_asm) only: supp_def permute_set_eq atom_eqvt permute_trm1 alpha1_INJ[simplified alpha_bp_eq])
-apply(simp add: Collect_imp_eq Collect_neg_eq[symmetric])
-apply(fold supp_def)
-apply simp
-done
+apply(simp_all add: b1)
+sorry
+
+consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
+consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"
+
+lemma y:
+  "perm_bn_trm p (Var x) = (Var x)"
+  "perm_bn_trm p (App t1 t2) = (App t1 t2)"
+  "perm_bn_trm p ("
+
+
 
 ML {*
   map (lift_thm [@{typ trm}, @{typ assg}] @{context}) @{thms eq_iff}