--- a/Nominal/Ex/SingleLet.thy	Sun Sep 05 07:00:19 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Fri Sep 10 09:17:40 2010 +0800
@@ -6,14 +6,14 @@
 
 declare [[STEPS = 100]]
 
-nominal_datatype single_let: trm  =
+nominal_datatype single_let: trm =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind x in t
 | Let a::"assg" t::"trm"  bind "bn a" in t
 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
-| Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 
+| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set) x in t2 
 and assg =
   As "name" x::"name" t::"trm" bind x in t
 binder
@@ -34,6 +34,7 @@
 thm single_let.size_eqvt
 thm single_let.supports
 thm single_let.fsupp
+thm single_let.supp
 
 lemma test2:
   assumes "fv_trm t = supp t" 
@@ -44,26 +45,25 @@
 apply(rule assms)
 done
 
-
 lemma supp_fv:
-  "fv_trm t = supp t" "fv_assg as = supp as" "fv_bn as = supp_rel alpha_bn as"
-apply(induct t and as rule: single_let.inducts)
+  "fv_trm x = supp x" 
+  "fv_assg xa = supp xa"
+  "fv_bn xa = supp_rel alpha_bn xa"
+apply(induct rule: single_let.inducts)
 -- " 0A "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])?
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
 -- " 0B"
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])?
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
 --" 1 "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *})
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -72,7 +72,7 @@
 apply(simp only:)
 -- " 2 "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(subst supp_abs(3)[symmetric])
 apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -82,7 +82,7 @@
 apply(simp only:)
 -- " 3 "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(1)[symmetric])
+apply(subst supp_abs(1)[symmetric])
 apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -91,7 +91,7 @@
 apply(simp only: supp_Pair Un_assoc conj_assoc)
 -- " Bar "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(subst supp_abs(3)[symmetric])
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -100,7 +100,8 @@
 apply(simp only: supp_Pair Un_assoc conj_assoc)
 -- " Baz "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(subst supp_abs(1)[symmetric])
+apply(subst supp_abs(1)[symmetric])
 apply(simp (no_asm) only: supp_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
@@ -110,7 +111,7 @@
 apply(simp only: supp_Pair Un_assoc conj_assoc)
 -- "last"
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
-apply(simp only: supp_abs(3)[symmetric])
+apply(tactic {* EqSubst.eqsubst_tac @{context} [1] @{thms supp_abs(3)[symmetric]} 1 *})
 apply(simp (no_asm) only: supp_def supp_rel_def)
 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)