diff -r dd7490fdd998 -r e44551d067e6 Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Tue Dec 21 10:28:08 2010 +0000
+++ b/Nominal/Ex/Let.thy	Wed Dec 22 09:13:25 2010 +0000
@@ -18,7 +18,6 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-thm at_set_avoiding2
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff 
 thm trm_assn.bn_defs
@@ -28,28 +27,8 @@
 thm trm_assn.distinct
 thm trm_assn.supp
 thm trm_assn.fresh
-thm trm_assn.exhaust[where y="t", no_vars]
-
-lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
-
-lemma uu:
-  shows "alpha_bn as (permute_bn p as)"
-apply(induct as rule: trm_assn.inducts(2))
-apply(auto)[4]
-apply(simp add: permute_bn)
-apply(simp add: trm_assn.eq_iff)
-apply(simp add: permute_bn)
-apply(simp add: trm_assn.eq_iff)
-done
-
-lemma tt:
-  shows "(p \<bullet> bn as) = bn (permute_bn p as)"
-apply(induct as rule: trm_assn.inducts(2))
-apply(auto)[4]
-apply(simp add: permute_bn trm_assn.bn_defs)
-apply(simp add: permute_bn trm_assn.bn_defs)
-apply(simp add: atom_eqvt)
-done
+thm trm_assn.exhaust
+thm trm_assn.strong_exhaust
 
 lemma strong_exhaust1:
   fixes c::"'a::fs"
@@ -58,41 +37,18 @@
   and     "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P" 
   and     "\<And>assn trm. \<lbrakk>set (bn assn) \<sharp>* c; y = Let assn trm\<rbrakk> \<Longrightarrow> P"
   shows "P"
-apply(rule_tac y="y" in trm_assn.exhaust(1))
+apply(rule_tac y="y" in trm_assn.strong_exhaust(1))
 apply(rule assms(1))
 apply(assumption)
 apply(rule assms(2))
 apply(assumption)
-apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name}) \<sharp>* c \<and> supp (Lam name trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
 apply(rule assms(3))
-apply(perm_simp)
+apply(assumption)
 apply(assumption)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: trm_assn.fresh fresh_star_def)
-apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q")
-apply(erule exE)
-apply(erule conjE)
-apply(simp add: set_eqvt)
-apply(subst (asm) tt)
-apply(rule_tac assms(4))
-apply(simp)
-apply(simp add: trm_assn.eq_iff)
-apply(drule supp_perm_eq[symmetric])
-apply(simp)
-apply(simp add: tt uu)
-apply(rule at_set_avoiding2)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: finite_supp)
-apply(simp add: Abs_fresh_star)
-done
+apply(rule assms(4))
+apply(assumption)
+apply(assumption)
+sorry
 
 
 lemma strong_exhaust2: