equal
deleted
inserted
replaced
177 |
177 |
178 quotient_def |
178 quotient_def |
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 |
|
183 ML {* val defs = |
|
184 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
|
185 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
|
186 *} |
|
187 ML {* val consts = lookup_quot_consts defs *} |
|
188 |
182 |
189 thm akind_aty_atrm.induct |
183 thm akind_aty_atrm.induct |
190 |
184 |
191 lemma left_ball_regular: |
185 lemma left_ball_regular: |
192 assumes a: "EQUIV R" |
186 assumes a: "EQUIV R" |
277 (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) |
271 (simp_tac (((Simplifier.context ctxt empty_ss) addsimps subs) addsimprocs [simproc])) |
278 ]) |
272 ]) |
279 end |
273 end |
280 *} |
274 *} |
281 |
275 |
|
276 ML {* val defs = |
|
277 @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def |
|
278 FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def} |
|
279 *} |
282 |
280 |
283 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
281 lemma "\<lbrakk>P1 TYP TYP; \<And>A A' K K' x. \<lbrakk>(A::TY) = A'; P2 A A'; (K::KIND) = K'; P1 K K'\<rbrakk> \<Longrightarrow> P1 (KPI A x K) (KPI A' x K'); |
284 \<And>A A' K x x' K'. |
282 \<And>A A' K x x' K'. |
285 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
283 \<lbrakk>(A ::TY) = A'; P2 A A'; (K :: KIND) = ([(x, x')] \<bullet> K'); P1 K ([(x, x')] \<bullet> K'); x \<notin> FV_ty A'; x \<notin> FV_kind K' - {x'}\<rbrakk> |
286 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
284 \<Longrightarrow> P1 (KPI A x K) (KPI A' x' K'); |
299 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
297 \<Longrightarrow> ((x1 :: KIND) = x2 \<longrightarrow> P1 x1 x2) \<and> |
300 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
298 ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)" |
301 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
299 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *}) |
302 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
300 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) |
303 prefer 2 |
301 prefer 2 |
304 apply(tactic {* r_mk_comb_tac' @{context} rty quot rel_refl trans2 rsp_thms 1*}) |
302 thm QUOTIENT_TY |
305 apply (tactic {* clean_tac @{context} quot defs reps_same absrep 1 *}) |
303 apply (tactic {* clean_tac @{context} @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} defs [] 1 *}) |
|
304 |
|
305 |
|
306 print_quotients |
|
307 apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 [] 1*}) |
|
308 |
|
309 |
|
310 ML {* val consts = lookup_quot_consts defs *} |
306 |
311 |
307 ML {* |
312 ML {* |
308 val rty_qty_rel = |
313 val rty_qty_rel = |
309 [(@{typ kind}, (@{typ KIND}, @{term akind})), |
314 [(@{typ kind}, (@{typ KIND}, @{term akind})), |
310 (@{typ ty}, (@{typ TY}, @{term aty})), |
315 (@{typ ty}, (@{typ TY}, @{term aty})), |