--- a/Quot/Nominal/Terms.thy	Tue Feb 23 16:12:30 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Tue Feb 23 18:27:32 2010 +0100
@@ -133,17 +133,18 @@
 *}
 print_theorems
 
-local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} @{term fv_rtrm1}
-  (fn _ => fv_rsp_tac @{thms alpha_rtrm1_alpha_bp.inducts} @{thms fv_rtrm1_fv_bp.simps} 1) *}
-local_setup {* prove_const_rsp @{binding rVr1_rsp} @{term rVr1}
-  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rAp1_rsp} @{term rAp1}
+thm alpha_rtrm1_alpha_bp.induct
+local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
+  (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *}
+local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}]
   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rLm1_rsp} @{term rLm1}
+local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}]
+  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}]
   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rLt1_rsp} @{term rLt1}
+local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]
   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}
+local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}
 
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
@@ -326,20 +327,19 @@
 *}
 print_theorems
 
-(*local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} @{term fv_rtrm2}
-  (fn _ => fv_rsp_tac @{thms alpha_rtrm2_alpha_rassign.inducts} @{thms fv_rtrm2_fv_rassign.simps} 1) *} *)
-lemma fv_rtrm2_rsp: "x \<approx>2 y \<Longrightarrow> fv_rtrm2 x = fv_rtrm2 y" sorry
-lemma bv2_rsp: "x \<approx>2b y \<Longrightarrow> rbv2 x = rbv2 y" sorry
-
-local_setup {* prove_const_rsp @{binding rVr2_rsp} @{term rVr2}
+local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]
+  (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *}
+local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]
+  (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *}
+local_setup {* prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}]
   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rAp2_rsp} @{term rAp2}
+local_setup {* prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}]
   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rLm2_rsp} @{term rLm2}
+local_setup {* prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}]
   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rLt2_rsp} @{term rLt2}
-  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp bv2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} @{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}
+local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]
+  (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *}
+local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}