286 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
286 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv})) |
287 *} |
287 *} |
288 |
288 |
289 ML {* |
289 ML {* |
290 fun symp_tac induct inj eqvt = |
290 fun symp_tac induct inj eqvt = |
291 rtac induct THEN_ALL_NEW |
291 ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
292 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
292 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
293 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
293 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
294 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
294 (etac @{thm alpha_gen_compose_sym} THEN' eresolve_tac eqvt) |
295 *} |
295 *} |
296 |
296 |
297 ML {* |
297 ML {* |
298 fun transp_tac induct alpha_inj term_inj distinct cases eqvt = |
298 fun transp_tac induct alpha_inj term_inj distinct cases eqvt = |
299 rtac induct THEN_ALL_NEW |
299 ((rtac @{thm impI} THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
300 (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN' |
300 (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN' |
301 eresolve_tac cases) THEN_ALL_NEW |
301 eresolve_tac cases) THEN_ALL_NEW |
302 ( |
302 ( |
303 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
303 asm_full_simp_tac (HOL_ss addsimps alpha_inj @ term_inj @ distinct) THEN' |
304 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
304 TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW |
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 *} |
|
308 |
|
309 lemma transp_aux: |
|
310 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
|
311 unfolding transp_def |
|
312 by blast |
|
313 |
|
314 ML {* |
|
315 fun equivp_tac reflps symps transps = |
|
316 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
|
317 THEN' rtac @{thm conjI} THEN' rtac @{thm allI} THEN' |
|
318 resolve_tac reflps THEN' |
|
319 rtac @{thm conjI} THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' |
|
320 resolve_tac symps THEN' |
|
321 rtac @{thm transp_aux} THEN' resolve_tac transps |
307 *} |
322 *} |
308 |
323 |
309 ML {* |
324 ML {* |
310 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
325 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
311 let |
326 let |
316 fun transp_tac' _ = transp_tac alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
331 fun transp_tac' _ = transp_tac alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
317 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
332 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
318 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
333 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
319 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
334 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
320 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
335 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
|
336 val reflts = HOLogic.conj_elims refltg |
|
337 val symts = HOLogic.conj_elims symtg |
|
338 val transts = HOLogic.conj_elims transtg |
321 fun equivp alpha = |
339 fun equivp alpha = |
322 let |
340 let |
323 val goal = @{term Trueprop} $ (@{term equivp} $ alpha) |
341 val equivp = Const (@{const_name equivp}, fastype_of alpha --> @{typ bool}) |
324 val tac = |
342 val goal = @{term Trueprop} $ (equivp $ alpha) |
|
343 fun tac _ = equivp_tac reflts symts transts 1 |
|
344 in |
|
345 Goal.prove ctxt [] [] goal tac |
|
346 end |
325 in |
347 in |
326 (refltg, symtg, transtg) |
348 map equivp alphas |
327 end |
349 end |
328 *} |
350 *} |
329 |
351 |
330 end |
352 end |