equal
deleted
inserted
replaced
25 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
25 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
26 val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list |
26 val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list |
27 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
27 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
28 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
28 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
29 term list -> thm -> thm list -> Proof.context -> thm list |
29 term list -> thm -> thm list -> Proof.context -> thm list |
|
30 val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list |
30 end |
31 end |
31 |
32 |
32 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
33 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
33 struct |
34 struct |
34 |
35 |
619 in |
620 in |
620 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
621 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
621 (K (asm_full_simp_tac ss)) ctxt |
622 (K (asm_full_simp_tac ss)) ctxt |
622 end |
623 end |
623 |
624 |
|
625 (* helper lemmas for respectfulness for size *) |
|
626 |
|
627 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt = |
|
628 let |
|
629 val arg_tys = map (domain_type o fastype_of) all_alpha_trms |
|
630 |
|
631 fun mk_prop ty (x, y) = HOLogic.mk_eq |
|
632 (HOLogic.size_const ty $ x, HOLogic.size_const ty $ y) |
|
633 |
|
634 val props = map2 (fn trm => fn ty => (trm, mk_prop ty)) all_alpha_trms arg_tys |
|
635 |
|
636 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_alpha_def prod_rel.simps |
|
637 permute_prod_def prod.cases prod.recs}) |
|
638 |
|
639 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss |
|
640 in |
|
641 alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt |
|
642 end |
|
643 |
624 end (* structure *) |
644 end (* structure *) |
625 |
645 |