--- a/Nominal/Ex/SingleLet.thy	Mon Oct 04 12:39:57 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Tue Oct 05 07:30:37 2010 +0100
@@ -21,12 +21,10 @@
 where
   "bn (As x y t) = [atom x]"
 
-
-
 thm single_let.distinct
 thm single_let.induct
 thm single_let.inducts
-thm single_let.exhaust
+thm single_let.exhaust[no_vars]
 thm single_let.fv_defs
 thm single_let.bn_defs
 thm single_let.perm_simps
@@ -38,6 +36,131 @@
 thm single_let.supp
 thm single_let.fresh
 
+primrec
+  permute_bn_raw
+where
+  "permute_bn_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t"
+
+quotient_definition
+  "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"
+is
+  "permute_bn_raw"
+
+lemma [quot_respect]:
+  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
+  apply (rule TrueI)+
+  apply simp_all
+  apply (rule_tac [!] alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
+  apply simp_all
+  done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+
+lemma uu:
+  shows "alpha_bn as (permute_bn p as)"
+apply(induct as rule: single_let.inducts(2))
+apply(auto)[7]
+apply(simp add: permute_bn)
+apply(simp add: single_let.eq_iff)
+done
+
+lemma tt:
+  shows "(p \<bullet> bn as) = bn (permute_bn p as)"
+apply(induct as rule: single_let.inducts(2))
+apply(auto)[7]
+apply(simp add: permute_bn single_let.bn_defs)
+apply(simp add: atom_eqvt)
+done
+
+lemma Abs_fresh_star':
+  fixes x::"'a::fs"
+  shows  "set bs = as \<Longrightarrow> as \<sharp>* Abs_lst bs x"
+  unfolding fresh_star_def
+  by(simp_all add: Abs_fresh_iff)
+
+lemma strong_exhaust:
+  fixes c::"'a::fs"
+  assumes "\<And>name. y = Var name \<Longrightarrow> P" 
+  and "\<And>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P" 
+  and "\<And>name trm. \<lbrakk>{atom name} \<sharp>* c; y = Lam name trm\<rbrakk> \<Longrightarrow> P"
+  and "\<And>assg trm. \<lbrakk>set (bn assg) \<sharp>* c; y = Let assg trm\<rbrakk> \<Longrightarrow> P"
+  and "\<And>name1 name2 trm1 trm2 trm3. \<lbrakk>{atom name1} \<sharp>* c; y = Foo name1 name2 trm1 trm2 trm3\<rbrakk> \<Longrightarrow> P"
+  and "\<And>name1 name2 trm. \<lbrakk>{atom name1, atom name2} \<sharp>* c; y = Bar name1 name2 trm\<rbrakk> \<Longrightarrow> P" 
+  and "\<And>name trm1 trm2. \<lbrakk>{atom name} \<sharp>* c; y = Baz name trm1 trm2\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+  apply(rule_tac y="y" in single_let.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 ([[atom name]]lst.trm) \<sharp>* q")
+  apply(erule exE)
+  apply(erule conjE)
+  apply(perm_simp)
+  apply(rule assms(3))
+  apply(assumption)
+  apply(drule supp_perm_eq[symmetric])
+  apply(simp add: single_let.eq_iff)
+  apply(perm_simp)
+  apply(rule refl)
+  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')
+  apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assg))) \<sharp>* (c::'a::fs) \<and> supp ([bn assg]lst.trm) \<sharp>* q")
+  apply(erule exE)
+  apply(erule conjE)
+  apply(perm_simp add: tt)
+  apply(rule_tac assms(4))
+  apply(assumption)
+  apply(drule supp_perm_eq[symmetric])
+  apply(simp add: single_let.eq_iff)
+  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)
+  apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1}) \<sharp>* (c::'a::fs) \<and> 
+    supp ([{atom name1}]set.(((name2, trm1), trm2), trm3)) \<sharp>* q")
+  apply(erule exE)
+  apply(erule conjE)
+  apply(perm_simp add: tt)
+  apply(rule_tac assms(5))
+  apply(assumption)
+  apply(drule supp_perm_eq[symmetric])
+  apply(simp add: single_let.eq_iff)
+  apply(perm_simp)
+  apply(rule refl)
+  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)
+  apply(subgoal_tac "\<exists>q. (q \<bullet> {atom name1, atom name2}) \<sharp>* (c::'a::fs) \<and> 
+    supp ([[atom name2, atom name1]]lst.((trm, name1), name2)) \<sharp>* q")
+  apply(erule exE)
+  apply(erule conjE)
+  apply(perm_simp add: tt)
+  apply(rule_tac assms(6))
+  apply(assumption)
+  apply(drule supp_perm_eq[symmetric])
+  apply(simp add: single_let.eq_iff)
+  apply(perm_simp)
+  apply(rule refl)
+  apply(rule at_set_avoiding2)
+  apply(simp add: finite_supp)
+  apply(simp add: finite_supp)
+  apply(simp add: finite_supp)
+  oops
+  (*apply(simp add: Abs_fresh_star)*)
+sorry
+  
+done
 
 end