diff -r 526fad251a8e -r 0d059450a3fa Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Tue Feb 23 11:56:47 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 23 12:49:45 2010 +0100
@@ -145,33 +145,44 @@
 *}
 print_theorems
 
-lemma fv_rtrm1_rsp:
-  shows "t \<approx>1 s \<Longrightarrow> fv_rtrm1 t = fv_rtrm1 s"
-  apply(induct rule: alpha_rtrm1_alpha_bp.inducts(1))
-  apply(simp_all add: alpha_gen.simps alpha_bp_eq)
-  done
+prove fv_rtrm1_rsp': {*
+ (@{term Trueprop} $ (Quotient_Term.equiv_relation_chk @{context} (fastype_of @{term fv_rtrm1}, fastype_of @{term fv_trm1}) $ @{term fv_rtrm1} $ @{term fv_rtrm1})) *}
+by (tactic {*
+  (rtac @{thm fun_rel_id} THEN'
+  eresolve_tac @{thms alpha_rtrm1_alpha_bp.inducts} THEN_ALL_NEW
+  asm_full_simp_tac (HOL_ss addsimps @{thms alpha_gen fv_rtrm1_fv_bp.simps})) 1 *})
+
+
+lemmas fv_rtrm1_rsp = apply_rsp'[OF fv_rtrm1_rsp']
+
+(* We need this since 'prove' doesn't support attributes *)
+lemma [quot_respect]: "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"
+  by (rule fv_rtrm1_rsp')
+
+ML {*
+fun contr_rsp_tac inj rsp equivps =
+let
+  val reflps = map (fn x => @{thm equivp_reflp} OF [x]) equivps
+in
+  REPEAT o rtac @{thm fun_rel_id} THEN'
+  simp_tac (HOL_ss addsimps inj) THEN'
+  (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)) THEN_ALL_NEW
+  (asm_simp_tac HOL_ss THEN_ALL_NEW (
+   rtac @{thm exI[of _ "0 :: perm"]} THEN'
+   asm_full_simp_tac (HOL_ss addsimps (rsp @ reflps @
+     @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv}))
+  ))
+end
+*}
 
 lemma [quot_respect]:
  "(op = ===> alpha_rtrm1) rVr1 rVr1"
  "(alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rAp1 rAp1"
  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) rLm1 rLm1"
  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1 ===> alpha_rtrm1) rLt1 rLt1"
-apply (simp_all only: fun_rel_def alpha1_inj alpha_bp_eq)
-apply (clarify)
-apply (clarify)
-apply (clarify)
-apply (auto)
-apply (rule_tac [!] x="0" in exI)
-apply (simp_all add: alpha_gen fresh_star_def fresh_zero_perm fv_rtrm1_rsp)
+apply (tactic {* contr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1 *})+
 done
 
-lemma [quot_respect]:
-  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute"
-  by (simp add: alpha1_eqvt)
-
-lemma [quot_respect]:
-  "(alpha_rtrm1 ===> op =) fv_rtrm1 fv_rtrm1"
-  by (simp add: fv_rtrm1_rsp)
 
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
@@ -184,6 +195,10 @@
 is
   "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
 
+lemma [quot_respect]:
+  "(op = ===> alpha_rtrm1 ===> alpha_rtrm1) permute permute"
+  by (simp add: alpha1_eqvt)
+
 lemmas permute_trm1[simp] = permute_rtrm1_permute_bp.simps[quot_lifted]
 
 instance