equal
deleted
inserted
replaced
27 thm list * thm list |
27 thm list * thm list |
28 val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list |
28 val raw_prove_bn_imp: Proof.context -> alpha_result -> thm list |
29 val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> |
29 val raw_fv_bn_rsp_aux: Proof.context -> alpha_result -> term list -> term list -> term list -> |
30 thm list -> thm list |
30 thm list -> thm list |
31 val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list |
31 val raw_size_rsp_aux: Proof.context -> alpha_result -> thm list -> thm list |
32 val raw_constrs_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list |
32 val raw_constrs_rsp: Proof.context -> alpha_result -> term list list -> thm list -> thm list list |
33 val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list |
33 val raw_alpha_bn_rsp: alpha_result -> thm list -> thm list -> thm list |
34 val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list |
34 val raw_perm_bn_rsp: Proof.context -> alpha_result -> term list -> thm list -> thm list |
35 |
35 |
36 val mk_funs_rsp: thm -> thm |
36 val mk_funs_rsp: thm -> thm |
37 val mk_alpha_permute_rsp: thm -> thm |
37 val mk_alpha_permute_rsp: thm -> thm |
747 |> foldr1 fun_rel_app |
747 |> foldr1 fun_rel_app |
748 |> (fn t => t $ trm $ trm) |
748 |> (fn t => t $ trm $ trm) |
749 |> Syntax.check_term ctxt |
749 |> Syntax.check_term ctxt |
750 |> HOLogic.mk_Trueprop |
750 |> HOLogic.mk_Trueprop |
751 in |
751 in |
|
752 map (fn constrs => |
752 Goal.prove_multi ctxt [] [] (map prep_goal constrs) |
753 Goal.prove_multi ctxt [] [] (map prep_goal constrs) |
753 (K (HEADGOAL |
754 (K (HEADGOAL |
754 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) |
755 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps)))) constrs |
755 end |
756 end |
756 |
757 |
757 |
758 |
758 (* rsp lemmas for alpha_bn relations *) |
759 (* rsp lemmas for alpha_bn relations *) |
759 |
760 |