# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267007314 -3600
# Node ID 14cf3d2b0e16c14fa0776ae099e229f2a25b0e44
# Parent  76de3440887c71df866d6b4311d44c34a39f9ff3
Respects of permute and constructors.

diff -r 76de3440887c -r 14cf3d2b0e16 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 11:03:30 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 11:28:34 2010 +0100
@@ -95,53 +95,23 @@
 
 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"
-  "(op = ===> alpha_rty ===> alpha_rty) permute permute"
-  "(op = ===> alpha_rtrm ===> alpha_rtrm) permute permute"
-  by (simp_all add:alpha_eqvt)
-
-lemma tconst_rsp[quot_respect]: 
-  "(op = ===> alpha_rty) TConst TConst"
-  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
-lemma tapp_rsp[quot_respect]: 
-  "(alpha_rty ===> alpha_rtrm ===> alpha_rty) TApp TApp" 
-  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
-lemma var_rsp[quot_respect]: 
-  "(op = ===> alpha_rtrm) Var Var"
-  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
-lemma app_rsp[quot_respect]: 
-  "(alpha_rtrm ===> alpha_rtrm ===> alpha_rtrm) App App"
-  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
-lemma const_rsp[quot_respect]: 
-  "(op = ===> alpha_rtrm) Const Const"
-  apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done
+local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
+local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
+local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]
+  (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
+ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
+  @{thms rfv_rsp} @{thms alpha_equivps} 1 *}
+local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}
+local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}
 
-lemma kpi_rsp[quot_respect]: 
-  "(alpha_rty ===> op = ===> alpha_rkind ===> alpha_rkind) KPi KPi"
-  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 rfv_rsp alpha_gen)
-  done
-
-lemma tpi_rsp[quot_respect]: 
-  "(alpha_rty ===> op = ===> alpha_rty ===> alpha_rty) TPi TPi"
-  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 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 rfv_rsp alpha_gen)
-  done
-
-thm rkind_rty_rtrm.induct
 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]
 
 thm rkind_rty_rtrm.inducts