--- a/Nominal/Ex/Let.thy	Thu Jun 09 15:34:51 2011 +0900
+++ b/Nominal/Ex/Let.thy	Fri Jun 10 09:00:24 2011 +0900
@@ -100,72 +100,30 @@
 | "set (bn as) \<sharp>* (s, t) \<Longrightarrow> subst s t (Let as b) = Let (substa s t as) (subst s t b)"
 | "substa s t ANil = ANil"
 | "substa s t (ACons v t' as) = ACons v (subst v t t') as"
-oops
-
-(*apply (subgoal_tac "\<forall>l. \<exists>!r. subst_substa_graph l r")
-defer
-apply rule
-apply (simp only: Ex1_def)
-apply (case_tac l)
-apply (case_tac a)
-apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1))
-apply simp_all[3]
-apply rule
-apply rule
-apply (rule subst_substa_graph.intros)*)
+(*unfolding eqvt_def subst_substa_graph_def
+  apply (rule, perm_simp)*)
+  defer
+  apply (rule TrueI)
+  apply (case_tac x)
+  apply (case_tac a)
+  apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1))
+  apply (auto simp add: fresh_star_def)[3]
+  apply (drule_tac x="assn" in meta_spec)
+  apply (simp add: Abs1_eq_iff alpha_bn_refl)
+  apply (case_tac b)
+  apply (case_tac c rule: trm_assn.exhaust(2))
+  apply (auto)[2]
+  apply blast
+  apply blast
+  apply auto
+  apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
+  apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff])
+  prefer 3
+  apply (erule alpha_bn_inducts)
+  apply (simp add: alpha_bn_refl)
+  (* Needs an invariant *)
+  oops
 
-(*
-defer
-apply (case_tac x)
-apply (case_tac a)
-thm trm_assn.strong_exhaust(1)
-apply (rule_tac y="c" and c="(aa,b)" in trm_assn.strong_exhaust(1))
-apply (simp add: trm_assn.distinct trm_assn.eq_iff)
-apply auto[1]
-apply (simp add: trm_assn.distinct trm_assn.eq_iff)
-apply auto[1]
-apply (simp add: trm_assn.distinct trm_assn.eq_iff fresh_star_def)
-apply (simp add: trm_assn.distinct trm_assn.eq_iff)
-apply (drule_tac x="assn" in meta_spec)
-apply (rotate_tac 3)
-apply (drule_tac x="aa" in meta_spec)
-apply (rotate_tac -1)
-apply (drule_tac x="b" in meta_spec)
-apply (rotate_tac -1)
-apply (drule_tac x="trm" in meta_spec)
-apply (auto simp add: alpha_bn_refl)[1]
-apply (case_tac b)
-apply (rule_tac ya="c" in trm_assn.strong_exhaust(2))
-apply (simp add: trm_assn.distinct trm_assn.eq_iff)
-apply auto[1]
-apply blast
-apply (simp add: trm_assn.distinct trm_assn.eq_iff)
-apply auto[1]
-apply blast
-apply (simp_all only: sum.simps Pair_eq trm_assn.distinct trm_assn.eq_iff)
-apply simp_all
-apply (simp_all add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
-apply (simp_all add: meta_eq_to_obj_eq[OF substa_def, symmetric, unfolded fun_eq_iff])
-apply clarify
-prefer 2
-apply clarify
-apply (rule conjI)
-prefer 2
-apply (rename_tac a pp vv zzz a2 s t zz)
-apply (erule alpha_bn_inducts)
-apply (rule alpha_bn_refl)
-apply clarify
-apply (rename_tac t' a1 a2 n1 n2)
-thm subst_substa_graph.intros[no_vars]
-.
-alpha_bn (substa s t (ACons n1 t' a1))
-         (substa s t (ACons n2 t' a2))
-
-alpha_bn (Acons s (subst a t t') a1)
-         (Acons s (subst a t t') a2)
-
-ACons v (subst v t t') as"
-*)
 end