equal
deleted
inserted
replaced
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 list -> thm list -> thm list 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: Proof.context -> thm -> thm |
37 val mk_alpha_permute_rsp: thm -> thm |
37 val mk_alpha_permute_rsp: Proof.context -> thm -> thm |
38 end |
38 end |
39 |
39 |
40 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
40 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
41 struct |
41 struct |
42 |
42 |
621 |
621 |
622 fun raw_prove_equivp ctxt alpha_result refl symm trans = |
622 fun raw_prove_equivp ctxt alpha_result refl symm trans = |
623 let |
623 let |
624 val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result |
624 val AlphaResult {alpha_trms, alpha_bn_trms, ...} = alpha_result |
625 |
625 |
626 val refl' = map (fold_rule [reflp_def'] o atomize) refl |
626 val refl' = map (fold_rule ctxt [reflp_def'] o atomize ctxt) refl |
627 val symm' = map (fold_rule [symp_def'] o atomize) symm |
627 val symm' = map (fold_rule ctxt [symp_def'] o atomize ctxt) symm |
628 val trans' = map (fold_rule [transp_def'] o atomize) trans |
628 val trans' = map (fold_rule ctxt [transp_def'] o atomize ctxt) trans |
629 |
629 |
630 fun prep_goal t = |
630 fun prep_goal t = |
631 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
631 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
632 in |
632 in |
633 Goal.prove_multi ctxt [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) |
633 Goal.prove_multi ctxt [] [] (map prep_goal (alpha_trms @ alpha_bn_trms)) |
832 val goals = map mk_prop perm_bns |
832 val goals = map mk_prop perm_bns |
833 in |
833 in |
834 alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct |
834 alpha_prove (alpha_trms @ alpha_bn_trms) goals alpha_raw_induct |
835 (raw_prove_perm_bn_tac alpha_result simps) ctxt |
835 (raw_prove_perm_bn_tac alpha_result simps) ctxt |
836 |> Proof_Context.export ctxt' ctxt |
836 |> Proof_Context.export ctxt' ctxt |
837 |> map atomize |
837 |> map (atomize ctxt) |
838 |> map single |
838 |> map single |
839 |> map (curry (op OF) perm_bn_rsp) |
839 |> map (curry (op OF) perm_bn_rsp) |
840 end |
840 end |
841 |
841 |
842 |
842 |
844 (* transformation of the natural rsp-lemmas into standard form *) |
844 (* transformation of the natural rsp-lemmas into standard form *) |
845 |
845 |
846 val fun_rsp = @{lemma |
846 val fun_rsp = @{lemma |
847 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)} |
847 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)} |
848 |
848 |
849 fun mk_funs_rsp thm = |
849 fun mk_funs_rsp ctxt thm = |
850 thm |
850 thm |
851 |> atomize |
851 |> atomize ctxt |
852 |> single |
852 |> single |
853 |> curry (op OF) fun_rsp |
853 |> curry (op OF) fun_rsp |
854 |
854 |
855 |
855 |
856 val permute_rsp = @{lemma |
856 val permute_rsp = @{lemma |
857 "(!x y p. R x y --> R (permute p x) (permute p y)) |
857 "(!x y p. R x y --> R (permute p x) (permute p y)) |
858 ==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)} |
858 ==> ((op =) ===> R ===> R) permute permute" by (simp add: fun_rel_def)} |
859 |
859 |
860 fun mk_alpha_permute_rsp thm = |
860 fun mk_alpha_permute_rsp ctxt thm = |
861 thm |
861 thm |
862 |> atomize |
862 |> atomize ctxt |
863 |> single |
863 |> single |
864 |> curry (op OF) permute_rsp |
864 |> curry (op OF) permute_rsp |
865 |
865 |
866 |
866 |
867 |
867 |