251 Variable.export ctxt' ctxt thms |
251 Variable.export ctxt' ctxt thms |
252 end |
252 end |
253 *} |
253 *} |
254 |
254 |
255 ML {* |
255 ML {* |
256 fun build_alpha_refl_gl alphas = |
256 fun build_alpha_refl_gl alphas (x, y, z) = |
257 let |
257 let |
258 fun build_alpha alpha = |
258 fun build_alpha alpha = |
259 let |
259 let |
260 val ty = domain_type (fastype_of alpha); |
260 val ty = domain_type (fastype_of alpha); |
261 val var = Free("x", ty); |
261 val var = Free(x, ty); |
262 val var2 = Free("y", ty); |
262 val var2 = Free(y, ty); |
263 val var3 = Free("z", ty); |
263 val var3 = Free(z, ty); |
264 val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); |
264 val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var); |
265 val transp = HOLogic.mk_imp (alpha $ var $ var2, |
265 val transp = HOLogic.mk_imp (alpha $ var $ var2, |
266 HOLogic.mk_all ("z", ty, |
266 HOLogic.mk_all (z, ty, |
267 HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) |
267 HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3))) |
268 in |
268 in |
269 ((alpha $ var $ var), (symp, transp)) |
269 ((alpha $ var $ var), (symp, transp)) |
270 end; |
270 end; |
271 val (refl_eqs, eqs) = split_list (map build_alpha alphas) |
271 val (refl_eqs, eqs) = split_list (map build_alpha alphas) |
305 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
305 (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac eqvt]) |
306 ) |
306 ) |
307 *} |
307 *} |
308 |
308 |
309 ML {* |
309 ML {* |
310 fun build_equivps alphas induct alpha_inj term_inj distinct cases eqvt ctxt = |
310 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
311 let |
311 let |
312 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas |
312 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
313 fun reflp_tac' _ = reflp_tac induct term_inj 1; |
313 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
314 fun symp_tac' _ = symp_tac induct alpha_inj eqvt 1; |
314 fun reflp_tac' _ = reflp_tac term_induct alpha_inj 1; |
315 fun transp_tac' _ = transp_tac induct alpha_inj term_inj distinct cases eqvt 1; |
315 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; |
316 val reflt = Goal.prove ctxt ["x"] [] reflg reflp_tac'; |
316 fun transp_tac' _ = transp_tac alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
317 val symt = Goal.prove ctxt ["x","y"] [] symg symp_tac'; |
317 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
318 val transt = Goal.prove ctxt ["x","y","z"] [] transg transp_tac'; |
318 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
|
319 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
|
320 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
|
321 fun equivp alpha = |
|
322 let |
|
323 val goal = @{term Trueprop} $ (@{term equivp} $ alpha) |
|
324 val tac = |
319 in |
325 in |
320 (reflt, symt, transt) |
326 (refltg, symtg, transtg) |
321 end |
327 end |
322 *} |
328 *} |
323 |
329 |
324 end |
330 end |