--- a/Nominal/Ex/Foo2.thy	Thu Dec 16 02:25:35 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Thu Dec 16 08:42:48 2010 +0000
@@ -21,10 +21,12 @@
 binder
   bn::"assg \<Rightarrow> atom list"
 where
- "bn (As x y t a) = [atom x] @ bn a"
+  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
 
+
+
 thm foo.bn_defs
 thm foo.permute_bn
 thm foo.perm_bn_alpha
@@ -69,65 +71,26 @@
 *)
 
 
-text {* *}
 
 
 
-(*
-thm at_set_avoiding1[THEN exE]
-
-
-lemma Let1_rename:
-  fixes c::"'a::fs"
-  shows "\<exists>name' trm'. {atom name'} \<sharp>* c \<and>  Lam name trm = Lam name' trm'"
-apply(simp only: foo.eq_iff)
-apply(rule at_set_avoiding1[where c="(c, atom name, trm)" and xs="set [atom name]", THEN exE])
-apply(simp)
-apply(simp add: finite_supp)
-apply(perm_simp)
-apply(rule Abs_rename_list[THEN exE])
-apply(simp only: set_eqvt)
-apply
-sorry 
-*)
-
-thm foo.exhaust
-
-ML {*
-fun strip_prems_concl trm =
-  (Logic.strip_imp_prems trm, Logic.strip_imp_concl trm)
-*}
-
-ML {*
-  @{thms foo.exhaust}
-  |> map prop_of
-  |> map strip_prems_concl
-  |> map fst
-  |> map (map (Syntax.string_of_term @{context}))
-  |> map cat_lines
-  |> cat_lines
-  |> writeln 
-*}
-
 lemma test6:
   fixes c::"'a::fs"
-  assumes "\<exists>name. y = Var name \<Longrightarrow> P" 
-  and     "\<exists>trm1 trm2. y = App trm1 trm2 \<Longrightarrow> P"
+  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     "\<exists>a1 trm1 a2 trm2.  ((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c \<and> y = Let1 a1 trm1 a2 trm2 \<Longrightarrow> P"
+  and     "\<And>a1 trm1 a2 trm2.  \<lbrakk>((set (bn a1)) \<union> (set (bn a2))) \<sharp>* c; y = Let1 a1 trm1 a2 trm2\<rbrakk> \<Longrightarrow> P"
   and     "\<exists>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<Longrightarrow> P"
   shows "P"
-apply(rule_tac foo.exhaust(1))
+apply(rule_tac y="y" in foo.exhaust(1))
 apply(rule assms(1))
-apply(rule exI)+
 apply(assumption)
 apply(rule assms(2))
-apply(rule exI)+
 apply(assumption)
 (* lam case *)
 apply(subgoal_tac "\<exists>p. (p \<bullet> {atom name}) \<sharp>* (c, name, trm)")
 apply(erule exE)
-apply(insert Abs_rename_list)[1]
+apply(insert Abs_rename_lst)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="[atom name]" in meta_spec)
 apply(drule_tac x="trm" in meta_spec)
@@ -150,12 +113,18 @@
 apply(subgoal_tac "\<exists>p. (p \<bullet> ((set (bn assg1)) \<union> (set (bn assg2)))) \<sharp>* (c, bn assg1, bn assg2, trm1, trm2)")
 apply(erule exE)
 apply(rule assms(4))
+apply(perm_simp add: foo.permute_bn)
+apply(simp add: fresh_star_Pair)
+apply(erule conjE)+
+apply(assumption)
+apply(simp only:)
 apply(simp only: foo.eq_iff)
-apply(insert Abs_rename_list)[1]
+(* *)
+apply(insert Abs_rename_lst)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg1" in meta_spec)
 apply(drule_tac x="trm1" in meta_spec)
-apply(insert Abs_rename_list)[1]
+apply(insert Abs_rename_lst)[1]
 apply(drule_tac x="p" in meta_spec)
 apply(drule_tac x="bn assg2" in meta_spec)
 apply(drule_tac x="trm2" in meta_spec)
@@ -164,21 +133,18 @@
 apply(drule meta_mp)
 apply(simp only: union_eqvt fresh_star_Pair set.simps fresh_star_Un, simp)
 apply(erule exE)+
-apply(rule exI)+
 apply(perm_simp add: foo.permute_bn)
-apply(rule conjI)
-apply(simp add: fresh_star_Pair fresh_star_Un)
+apply(simp add: fresh_star_Pair)
 apply(erule conjE)+
+apply(rule assms(4))
+apply(assumption)
+apply(simp add: foo.eq_iff refl)
 apply(rule conjI)
-apply(assumption)
-apply(rotate_tac 4)
-apply(assumption)
-apply(rule conjI)
-apply(assumption)
+apply(rule refl)
 apply(rule conjI)
 apply(rule foo.perm_bn_alpha)
 apply(rule conjI)
-apply(assumption)
+apply(rule refl)
 apply(rule foo.perm_bn_alpha)
 apply(rule at_set_avoiding1)
 apply(simp)