# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267005810 -3600
# Node ID 76de3440887c71df866d6b4311d44c34a39f9ff3
# Parent  ab1aa1b48547af100a6cee843d82a8814e48c53d
Generate fv_rsp automatically.

diff -r ab1aa1b48547 -r 76de3440887c Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 10:59:31 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 11:03:30 2010 +0100
@@ -93,13 +93,8 @@
  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}
 print_theorems
 
-lemma alpha_rfv:
-  shows "(t \<approx>ki s \<longrightarrow> fv_rkind t = fv_rkind s) \<and>
-     (t1 \<approx>ty s1 \<longrightarrow> fv_rty t1 = fv_rty s1) \<and>
-     (t2 \<approx>tr s2 \<longrightarrow> fv_rtrm t2 = fv_rtrm s2)"
-  apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
-  apply(simp_all add: alpha_gen)
-  done
+local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]
+  (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}
 
 lemma perm_rsp[quot_respect]:
   "(op = ===> alpha_rkind ===> alpha_rkind) permute permute"
@@ -128,7 +123,7 @@
   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2)) apply simp_all
   apply (rule_tac x="0" in exI)
-  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
+  apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen)
   done
 
 lemma tpi_rsp[quot_respect]: 
@@ -136,26 +131,16 @@
   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5)) apply simp_all
   apply (rule_tac x="0" in exI)
-  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
+  apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen)
   done
 lemma lam_rsp[quot_respect]: 
   "(alpha_rty ===> op = ===> alpha_rtrm ===> alpha_rtrm) Lam Lam"
   apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros)
   apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9)) apply simp_all
   apply (rule_tac x="0" in exI)
-  apply (simp add: fresh_star_def fresh_zero_perm alpha_rfv alpha_gen)
+  apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen)
   done
 
-lemma fv_rty_rsp[quot_respect]: 
-  "(alpha_rty ===> op =) fv_rty fv_rty"
-  by (simp add: alpha_rfv)
-lemma fv_rkind_rsp[quot_respect]:
-  "(alpha_rkind ===> op =) fv_rkind fv_rkind"
-  by (simp add: alpha_rfv)
-lemma fv_rtrm_rsp[quot_respect]:
-  "(alpha_rtrm ===> op =) fv_rtrm fv_rtrm"
-  by (simp add: alpha_rfv)
-
 thm rkind_rty_rtrm.induct
 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]