93 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} |
93 |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *} |
94 print_theorems |
94 print_theorems |
95 |
95 |
96 local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}] |
96 local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}] |
97 (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *} |
97 (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *} |
98 |
98 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}] |
99 lemma perm_rsp[quot_respect]: |
99 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
100 "(op = ===> alpha_rkind ===> alpha_rkind) permute permute" |
100 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}] |
101 "(op = ===> alpha_rty ===> alpha_rty) permute permute" |
101 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
102 "(op = ===> alpha_rtrm ===> alpha_rtrm) permute permute" |
102 local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}] |
103 by (simp_all add:alpha_eqvt) |
103 (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *} |
104 |
104 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj} |
105 lemma tconst_rsp[quot_respect]: |
105 @{thms rfv_rsp} @{thms alpha_equivps} 1 *} |
106 "(op = ===> alpha_rty) TConst TConst" |
106 local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *} |
107 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done |
107 local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *} |
108 lemma tapp_rsp[quot_respect]: |
108 local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *} |
109 "(alpha_rty ===> alpha_rtrm ===> alpha_rty) TApp TApp" |
109 local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *} |
110 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done |
110 local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *} |
111 lemma var_rsp[quot_respect]: |
111 local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *} |
112 "(op = ===> alpha_rtrm) Var Var" |
112 local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *} |
113 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done |
113 local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *} |
114 lemma app_rsp[quot_respect]: |
114 |
115 "(alpha_rtrm ===> alpha_rtrm ===> alpha_rtrm) App App" |
|
116 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done |
|
117 lemma const_rsp[quot_respect]: |
|
118 "(op = ===> alpha_rtrm) Const Const" |
|
119 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) done |
|
120 |
|
121 lemma kpi_rsp[quot_respect]: |
|
122 "(alpha_rty ===> op = ===> alpha_rkind ===> alpha_rkind) KPi KPi" |
|
123 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
124 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(2)) apply simp_all |
|
125 apply (rule_tac x="0" in exI) |
|
126 apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen) |
|
127 done |
|
128 |
|
129 lemma tpi_rsp[quot_respect]: |
|
130 "(alpha_rty ===> op = ===> alpha_rty ===> alpha_rty) TPi TPi" |
|
131 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
132 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(5)) apply simp_all |
|
133 apply (rule_tac x="0" in exI) |
|
134 apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen) |
|
135 done |
|
136 lemma lam_rsp[quot_respect]: |
|
137 "(alpha_rty ===> op = ===> alpha_rtrm ===> alpha_rtrm) Lam Lam" |
|
138 apply (auto intro: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
139 apply (rule alpha_rkind_alpha_rty_alpha_rtrm.intros(9)) apply simp_all |
|
140 apply (rule_tac x="0" in exI) |
|
141 apply (simp add: fresh_star_def fresh_zero_perm rfv_rsp alpha_gen) |
|
142 done |
|
143 |
|
144 thm rkind_rty_rtrm.induct |
|
145 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
115 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted] |
146 |
116 |
147 thm rkind_rty_rtrm.inducts |
117 thm rkind_rty_rtrm.inducts |
148 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] |
118 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted] |
149 |
119 |