equal
deleted
inserted
replaced
44 val mk_alpha_permute_rsp: thm -> thm |
44 val mk_alpha_permute_rsp: thm -> thm |
45 end |
45 end |
46 |
46 |
47 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
47 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
48 struct |
48 struct |
|
49 |
|
50 open Nominal_Permeq |
49 |
51 |
50 fun lookup xs x = the (AList.lookup (op=) xs x) |
52 fun lookup xs x = the (AList.lookup (op=) xs x) |
51 fun group xs = AList.group (op=) xs |
53 fun group xs = AList.group (op=) xs |
52 |
54 |
53 (** definition of the inductive rules for alpha and alpha_bn **) |
55 (** definition of the inductive rules for alpha and alpha_bn **) |
503 in |
505 in |
504 EVERY' |
506 EVERY' |
505 [ etac exi_neg, |
507 [ etac exi_neg, |
506 resolve_tac @{thms alpha_sym_eqvt}, |
508 resolve_tac @{thms alpha_sym_eqvt}, |
507 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
509 asm_full_simp_tac (HOL_ss addsimps prod_simps), |
508 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
510 eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl}, |
509 trans_prem_tac pred_names ctxt ] |
511 trans_prem_tac pred_names ctxt ] |
510 end |
512 end |
511 |
513 |
512 fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = |
514 fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt = |
513 let |
515 let |
558 etac @{thm exE}, |
560 etac @{thm exE}, |
559 perm_inst_tac ctxt, |
561 perm_inst_tac ctxt, |
560 resolve_tac @{thms alpha_trans_eqvt}, |
562 resolve_tac @{thms alpha_trans_eqvt}, |
561 atac, |
563 atac, |
562 aatac pred_names ctxt, |
564 aatac pred_names ctxt, |
563 Nominal_Permeq.eqvt_tac ctxt [] [] THEN' rtac @{thm refl}, |
565 eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl}, |
564 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
566 asm_full_simp_tac (HOL_ss addsimps prod_simps) ]) |
565 end |
567 end |
566 |
568 |
567 fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt = |
569 fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt = |
568 let |
570 let |