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 val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list |
|
31 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
31 |
32 |
32 val resolve_fun_rel: thm -> thm |
33 val resolve_fun_rel: thm -> thm |
33 end |
34 end |
34 |
35 |
35 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
36 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
622 in |
623 in |
623 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
624 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
624 (K (asm_full_simp_tac ss)) ctxt |
625 (K (asm_full_simp_tac ss)) ctxt |
625 end |
626 end |
626 |
627 |
|
628 |
627 (* respectfulness for size *) |
629 (* respectfulness for size *) |
628 |
630 |
629 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt = |
631 fun raw_size_rsp_aux all_alpha_trms alpha_induct simps ctxt = |
630 let |
632 let |
631 val arg_tys = map (domain_type o fastype_of) all_alpha_trms |
633 val arg_tys = map (domain_type o fastype_of) all_alpha_trms |
639 permute_prod_def prod.cases prod.recs}) |
641 permute_prod_def prod.cases prod.recs}) |
640 |
642 |
641 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss |
643 val tac = (TRY o REPEAT o etac @{thm exE}) THEN' asm_full_simp_tac ss |
642 in |
644 in |
643 alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt |
645 alpha_prove all_alpha_trms props alpha_induct (K tac) ctxt |
|
646 end |
|
647 |
|
648 |
|
649 (* respectfulness for constructors *) |
|
650 |
|
651 fun raw_constr_rsp_tac alpha_intros simps = |
|
652 let |
|
653 val pre_ss = HOL_ss addsimps @{thms fun_rel_def} |
|
654 val post_ss = HOL_ss addsimps @{thms alphas prod_alpha_def prod_rel.simps |
|
655 prod_fv.simps fresh_star_zero permute_zero prod.cases} @ simps |
|
656 (* funs_rsp alpha_bn_simps *) |
|
657 in |
|
658 asm_full_simp_tac pre_ss |
|
659 THEN' REPEAT o (resolve_tac @{thms allI impI}) |
|
660 THEN' resolve_tac alpha_intros |
|
661 THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss) |
|
662 end |
|
663 |
|
664 |
|
665 fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt = |
|
666 let |
|
667 val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms |
|
668 |
|
669 fun lookup ty = |
|
670 case AList.lookup (op=) (alpha_arg_tys ~~ alpha_trms) ty of |
|
671 NONE => HOLogic.eq_const ty |
|
672 | SOME alpha => alpha |
|
673 |
|
674 fun fun_rel_app t1 t2 = |
|
675 Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2 |
|
676 |
|
677 fun prep_goal trm = |
|
678 trm |
|
679 |> strip_type o fastype_of |
|
680 |>> map lookup |
|
681 ||> lookup |
|
682 |> uncurry (fold_rev fun_rel_app) |
|
683 |> (fn t => t $ trm $ trm) |
|
684 |> Syntax.check_term ctxt |
|
685 |> HOLogic.mk_Trueprop |
|
686 in |
|
687 Goal.prove_multi ctxt [] [] (map prep_goal constrs) |
|
688 (K (HEADGOAL |
|
689 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) |
644 end |
690 end |
645 |
691 |
646 |
692 |
647 (* resolve with @{thm fun_relI} *) |
693 (* resolve with @{thm fun_relI} *) |
648 |
694 |