89 |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind})) |
89 |> snd o (Quotient_Def.quotient_lift_const ("fv_kind", @{term fv_rkind})) |
90 |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty})) |
90 |> snd o (Quotient_Def.quotient_lift_const ("fv_ty", @{term fv_rty})) |
91 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} |
91 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} |
92 print_theorems |
92 print_theorems |
93 |
93 |
94 local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}] |
94 local_setup {* snd o prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}] |
95 (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *} |
95 (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *} |
96 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}] |
96 local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}] |
97 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
97 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
98 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}] |
98 local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}] |
99 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
99 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
100 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}] |
100 local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}] |
101 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
101 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
102 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} |
102 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} |
103 @{thms rfv_rsp} @{thms alpha_equivps} 1 *} |
103 @{thms rfv_rsp} @{thms alpha_equivps} 1 *} |
104 local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *} |
104 local_setup {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *} |
105 local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *} |
105 local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *} |
106 local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *} |
106 local_setup {* snd o prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *} |
107 local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *} |
107 local_setup {* snd o prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *} |
108 local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *} |
108 local_setup {* snd o prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *} |
109 local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *} |
109 local_setup {* snd o prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *} |
110 local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *} |
110 local_setup {* snd o prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *} |
111 local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *} |
111 local_setup {* snd o prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *} |
112 |
112 |
113 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
113 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
114 |
114 |
115 thm rkind_rty_rtrm.inducts |
115 thm rkind_rty_rtrm.inducts |
116 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] |
116 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] |