326 apply (erule exE) |
326 apply (erule exE) |
327 apply (rule_tac x="-pi" in exI) |
327 apply (rule_tac x="-pi" in exI) |
328 by auto |
328 by auto |
329 |
329 |
330 ML {* |
330 ML {* |
331 fun symp_tac induct inj eqvt = |
331 fun symp_tac induct inj eqvt ctxt = |
332 (((rtac impI THEN' etac induct) ORELSE' rtac induct) THEN_ALL_NEW |
332 ind_tac induct THEN_ALL_NEW |
333 asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW |
333 simp_tac ((mk_minimal_ss ctxt) addsimps inj) THEN_ALL_NEW split_conjs |
334 (REPEAT o etac conjE THEN' etac @{thm exi_neg} THEN' REPEAT o etac conjE THEN' |
334 THEN_ALL_NEW |
335 (TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI))) THEN_ALL_NEW |
335 REPEAT o etac @{thm exi_neg} |
336 (asm_full_simp_tac HOL_ss) THEN_ALL_NEW |
336 THEN_ALL_NEW |
337 (etac @{thm alpha_gen_compose_sym} THEN' |
337 split_conjs THEN_ALL_NEW |
338 (asm_full_simp_tac (HOL_ss addsimps (@{thm atom_eqvt} :: eqvt))))) |
338 asm_full_simp_tac (HOL_ss addsimps @{thms supp_minus_perm minus_add[symmetric]}) THEN_ALL_NEW |
|
339 (rtac @{thm alpha_gen_compose_sym} THEN' RANGE [ |
|
340 (asm_full_simp_tac (HOL_ss addsimps @{thms plus_perm_eq})), |
|
341 (asm_full_simp_tac (HOL_ss addsimps (eqvt @ all_eqvts ctxt))) |
|
342 ]) |
339 *} |
343 *} |
340 |
344 |
341 ML {* |
345 ML {* |
342 fun imp_elim_tac case_rules = |
346 fun imp_elim_tac case_rules = |
343 Subgoal.FOCUS (fn {concl, context, ...} => |
347 Subgoal.FOCUS (fn {concl, context, ...} => |
400 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
404 fun build_equivps alphas term_induct alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
401 let |
405 let |
402 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
406 val ([x, y, z], ctxt') = Variable.variant_fixes ["x","y","z"] ctxt; |
403 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
407 val (reflg, (symg, transg)) = build_alpha_refl_gl alphas (x, y, z) |
404 fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1; |
408 fun reflp_tac' _ = reflp_tac term_induct alpha_inj ctxt 1; |
405 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt 1; |
409 fun symp_tac' _ = symp_tac alpha_induct alpha_inj eqvt ctxt 1; |
406 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
410 fun transp_tac' _ = transp_tac ctxt alpha_induct alpha_inj term_inj distinct cases eqvt 1; |
407 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
411 val reflt = Goal.prove ctxt' [] [] reflg reflp_tac'; |
408 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
412 val symt = Goal.prove ctxt' [] [] symg symp_tac'; |
409 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
413 val transt = Goal.prove ctxt' [] [] transg transp_tac'; |
410 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |
414 val [refltg, symtg, transtg] = Variable.export ctxt' ctxt [reflt, symt, transt] |