--- a/Nominal/Ex/SingleLet.thy	Thu Jul 29 10:16:33 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Fri Jul 30 00:40:32 2010 +0100
@@ -4,7 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 16]]
+declare [[STEPS = 17]]
 
 nominal_datatype trm  =
   Var "name"
@@ -21,6 +21,7 @@
 where
   "bn (As x y t) = {atom x}"
 
+thm size_eqvt
 thm alpha_bn_imps
 thm distinct
 thm eq_iff
@@ -28,6 +29,7 @@
 thm fv_defs
 thm perm_simps
 thm perm_laws
+thm funs_rsp
 
 
 typ trm
@@ -40,61 +42,31 @@
 term alpha_bn
 
 
-lemma a2:
-  shows "alpha_trm_raw x1 y1 \<Longrightarrow> fv_trm_raw x1 = fv_trm_raw y1"
-  and   "alpha_assg_raw x2 y2 \<Longrightarrow> fv_assg_raw x2 = fv_assg_raw y2 \<and> bn_raw x2 = bn_raw y2"
-  and   "alpha_bn_raw x3 y3 \<Longrightarrow>  fv_bn_raw x3 = fv_bn_raw y3"
-apply(induct rule: alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-apply(simp_all only: fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps bn_raw.simps 
-  alphas prod_fv.simps prod_alpha_def ex_simps Un_assoc set.simps append.simps Un_insert_left Un_empty_right Un_empty_left simp_thms)
-done
+lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto
+
+ML {* 
+  val pre_ss = @{thms fun_rel_def}
+  val post_ss = @{thms alphas prod_alpha_def prod_rel.simps 
+    prod_fv.simps fresh_star_zero permute_zero funs_rsp prod.cases alpha_bn_imps}
+
+  val tac = 
+    asm_full_simp_tac (HOL_ss addsimps pre_ss)
+    THEN' REPEAT o (resolve_tac @{thms allI impI})
+    THEN' resolve_tac @{thms alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros} 
+    THEN_ALL_NEW (TRY o (rtac @{thm exi_zero}) THEN' asm_full_simp_tac (HOL_ss addsimps post_ss))
+*}
 
 lemma [quot_respect]: 
   "(op= ===> alpha_trm_raw) Var_raw Var_raw"
   "(alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) App_raw App_raw"
   "(op= ===> alpha_trm_raw ===> alpha_trm_raw) Lam_raw Lam_raw"
   "(alpha_assg_raw ===> alpha_trm_raw ===> alpha_trm_raw) Let_raw Let_raw"
-  "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) 
+  "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw)
      Foo_raw Foo_raw"
   "(op= ===> op= ===> alpha_trm_raw ===> alpha_trm_raw) Bar_raw Bar_raw"
   "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
   "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
-apply(simp only: fun_rel_def)
-apply(simp only: eq_iff)
-apply(simp only: simp_thms)
-apply(simp only: fun_rel_def)
-apply(simp only: eq_iff)
-apply(tactic {* asm_full_simp_tac HOL_ss 1*})
-apply(simp only: fun_rel_def)
-apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2)
-apply(rule allI | rule impI)+
-apply(rule_tac x="0" in exI)
-apply(simp only: eq_iff alphas fresh_star_def fresh_zero_perm a2 permute_zero a2)
-apply(simp add: a2)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 alpha_bn_imps)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(simp only: fun_rel_def)
-apply(rule allI | rule impI)+
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(simp add: alphas fresh_star_def fresh_zero_perm a2 prod_alpha_def)
-apply(assumption)
+apply(tactic {* ALLGOALS tac *})
 done
 
 lemma [quot_respect]:
@@ -103,7 +75,7 @@
   "(alpha_assg_raw ===> op =) bn_raw bn_raw"
   "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw"
   "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
-apply(simp_all add: a2 a1)
+apply(simp_all add: alpha_bn_imps funs_rsp)
 sorry
 
 ML {*