# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267193455 -3600
# Node ID 8814494fe4da14606ae256e1958d12082a07e28d
# Parent  6eacf60ce41d6759f9be097b73bb7bfdb0c8308a
Change in signature of prove_const_rsp for general lifting.

diff -r 6eacf60ce41d -r 8814494fe4da Nominal/LFex.thy
--- a/Nominal/LFex.thy	Fri Feb 26 13:57:43 2010 +0100
+++ b/Nominal/LFex.thy	Fri Feb 26 15:10:55 2010 +0100
@@ -91,24 +91,24 @@
  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}
 print_theorems
 
-local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]
+local_setup {* snd o 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) *}
-local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]
+local_setup {* snd o 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"}]
+local_setup {* snd o 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"}]
+local_setup {* snd o 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 *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}
 
 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]
 
diff -r 6eacf60ce41d -r 8814494fe4da Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Fri Feb 26 13:57:43 2010 +0100
+++ b/Nominal/Rsp.thy	Fri Feb 26 15:10:55 2010 +0100
@@ -69,7 +69,7 @@
    ctxt
 |> snd o Local_Theory.note 
   ((Binding.empty, [Attrib.internal (fn _ => Quotient_Info.rsp_rules_add)]), rsp_thms)
-|> snd o Local_Theory.note ((bind, []), user_thms)
+|> Local_Theory.note ((bind, []), user_thms)
 end
 *}
 
@@ -99,7 +99,7 @@
 *}
 
 (* Testing code
-local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]
+local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term rbv2}]
   (fn _ => fv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms fv_rtrm2_fv_rassign.simps} 1) *}*)
 
 (*ML {*
diff -r 6eacf60ce41d -r 8814494fe4da Nominal/Term1.thy
--- a/Nominal/Term1.thy	Fri Feb 26 13:57:43 2010 +0100
+++ b/Nominal/Term1.thy	Fri Feb 26 15:10:55 2010 +0100
@@ -93,18 +93,17 @@
 *}
 print_theorems
 
-thm alpha_rtrm1_alpha_bp.induct
-local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
+local_setup {* snd o 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}]
+local_setup {* snd o 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 {* snd o 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 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}]
+local_setup {* snd o 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 {* snd o 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 {* snd o 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]
diff -r 6eacf60ce41d -r 8814494fe4da Nominal/Term2.thy
--- a/Nominal/Term2.thy	Fri Feb 26 13:57:43 2010 +0100
+++ b/Nominal/Term2.thy	Fri Feb 26 15:10:55 2010 +0100
@@ -60,19 +60,19 @@
 *}
 print_theorems
 
-local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]
+local_setup {* snd o 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}]
+local_setup {* snd o 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}]
+local_setup {* snd o 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 {* snd o 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 {* snd o 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}]
+local_setup {* snd o 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"}]
+local_setup {* snd o 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) *}
 
 end