179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
179 perm_trm :: "'x prm \<Rightarrow> TRM \<Rightarrow> TRM" |
180 where |
180 where |
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
181 "perm_trm \<equiv> (perm::'x prm \<Rightarrow> trm \<Rightarrow> trm)" |
182 |
182 |
183 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
183 (* TODO/FIXME: Think whether these RSP theorems are true. *) |
184 lemma kpi_rsp[quot_rsp]: |
184 lemma kpi_rsp[quotient_rsp]: |
185 "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry |
185 "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry |
186 lemma tconst_rsp[quot_rsp]: |
186 lemma tconst_rsp[quotient_rsp]: |
187 "(op = ===> aty) TConst TConst" sorry |
187 "(op = ===> aty) TConst TConst" sorry |
188 lemma tapp_rsp[quot_rsp]: |
188 lemma tapp_rsp[quotient_rsp]: |
189 "(aty ===> atrm ===> aty) TApp TApp" sorry |
189 "(aty ===> atrm ===> aty) TApp TApp" sorry |
190 lemma tpi_rsp[quot_rsp]: |
190 lemma tpi_rsp[quotient_rsp]: |
191 "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry |
191 "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry |
192 lemma var_rsp[quot_rsp]: |
192 lemma var_rsp[quotient_rsp]: |
193 "(op = ===> atrm) Var Var" sorry |
193 "(op = ===> atrm) Var Var" sorry |
194 lemma app_rsp[quot_rsp]: |
194 lemma app_rsp[quotient_rsp]: |
195 "(atrm ===> atrm ===> atrm) App App" sorry |
195 "(atrm ===> atrm ===> atrm) App App" sorry |
196 lemma const_rsp[quot_rsp]: |
196 lemma const_rsp[quotient_rsp]: |
197 "(op = ===> atrm) Const Const" sorry |
197 "(op = ===> atrm) Const Const" sorry |
198 lemma lam_rsp[quot_rsp]: |
198 lemma lam_rsp[quotient_rsp]: |
199 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry |
199 "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry |
200 |
200 |
201 lemma perm_kind_rsp[quot_rsp]: |
201 lemma perm_kind_rsp[quotient_rsp]: |
202 "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry |
202 "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry |
203 lemma perm_ty_rsp[quot_rsp]: |
203 lemma perm_ty_rsp[quotient_rsp]: |
204 "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry |
204 "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry |
205 lemma perm_trm_rsp[quot_rsp]: |
205 lemma perm_trm_rsp[quotient_rsp]: |
206 "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry |
206 "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry |
207 |
207 |
208 lemma fv_ty_rsp[quot_rsp]: |
208 lemma fv_ty_rsp[quotient_rsp]: |
209 "(aty ===> op =) fv_ty fv_ty" sorry |
209 "(aty ===> op =) fv_ty fv_ty" sorry |
210 lemma fv_kind_rsp[quot_rsp]: |
210 lemma fv_kind_rsp[quotient_rsp]: |
211 "(akind ===> op =) fv_kind fv_kind" sorry |
211 "(akind ===> op =) fv_kind fv_kind" sorry |
212 lemma fv_trm_rsp[quot_rsp]: |
212 lemma fv_trm_rsp[quotient_rsp]: |
213 "(atrm ===> op =) fv_trm fv_trm" sorry |
213 "(atrm ===> op =) fv_trm fv_trm" sorry |
214 |
214 |
215 |
215 |
216 thm akind_aty_atrm.induct |
216 thm akind_aty_atrm.induct |
217 thm kind_ty_trm.induct |
217 thm kind_ty_trm.induct |
259 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
259 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 |
260 apply - |
260 apply - |
261 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
261 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
262 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
262 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
263 prefer 2 |
263 prefer 2 |
264 apply(tactic {* clean_tac @{context} quot 1 *}) |
264 apply(tactic {* clean_tac @{context} 1 *}) |
265 (* |
265 (* |
266 Profiling: |
266 Profiling: |
267 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
267 ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} |
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
268 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} |
269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
269 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} |
270 ML_prf {* PolyML.profiling 1 *} |
270 ML_prf {* PolyML.profiling 1 *} |
271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
271 ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} |
272 *) |
272 *) |
273 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
273 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
274 done |
274 done |
275 |
275 |
276 (* Does not work: |
276 (* Does not work: |
277 lemma |
277 lemma |
278 assumes a0: "P1 TYP" |
278 assumes a0: "P1 TYP" |
297 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
297 \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2); |
298 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
298 \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk> |
299 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
299 \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm" |
300 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
300 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *}) |
301 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
301 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
302 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *}) |
302 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) |
303 apply(tactic {* clean_tac @{context} quot 1 *}) |
303 apply(tactic {* clean_tac @{context} 1 *}) |
304 done |
304 done |
305 |
305 |
306 print_quotients |
306 print_quotients |
307 |
307 |
308 end |
308 end |