diff -r 02b24877be3e -r e6e6a3da81aa Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Wed Dec 22 21:13:32 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy	Wed Dec 22 21:13:44 2010 +0000
@@ -22,7 +22,8 @@
 thm single_let.distinct
 thm single_let.induct
 thm single_let.inducts
-thm single_let.exhaust[no_vars]
+thm single_let.exhaust
+thm single_let.strong_exhaust
 thm single_let.fv_defs
 thm single_let.bn_defs
 thm single_let.perm_simps
@@ -34,107 +35,6 @@
 thm single_let.supp
 thm single_let.fresh
 
-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
-
 
 end