equal
deleted
inserted
replaced
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 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
32 val raw_alpha_bn_rsp: thm list -> thm list -> thm list |
32 val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list |
33 |
33 |
34 val mk_funs_rsp: thm -> thm |
34 val mk_funs_rsp: thm -> thm |
35 val mk_alpha_permute_rsp: thm -> thm |
35 val mk_alpha_permute_rsp: thm -> thm |
36 end |
36 end |
37 |
37 |
701 |
701 |
702 val rsp_equivp = |
702 val rsp_equivp = |
703 @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q" |
703 @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q" |
704 by (simp only: fun_rel_def equivp_def, metis)} |
704 by (simp only: fun_rel_def equivp_def, metis)} |
705 |
705 |
706 fun raw_alpha_bn_rsp alpha_bn_equivp alpha_bn_imps = |
706 |
707 let |
707 (* we have to reorder the alpha_bn_imps theorems in order |
|
708 to be in order with alpha_bn_trms *) |
|
709 fun raw_alpha_bn_rsp alpha_bn_trms alpha_bn_equivp alpha_bn_imps = |
|
710 let |
|
711 fun mk_map thm = |
|
712 thm |> `prop_of |
|
713 |>> List.last o snd o strip_comb |
|
714 |>> HOLogic.dest_Trueprop |
|
715 |>> head_of |
|
716 |>> fst o dest_Const |
|
717 |
|
718 val alpha_bn_imps' = |
|
719 map (lookup (map mk_map alpha_bn_imps) o fst o dest_Const) alpha_bn_trms |
|
720 |
708 fun mk_thm thm1 thm2 = |
721 fun mk_thm thm1 thm2 = |
709 (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) |
722 (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) |
710 in |
723 in |
711 map2 mk_thm alpha_bn_equivp alpha_bn_imps |
724 map2 mk_thm alpha_bn_equivp alpha_bn_imps' |
712 end |
725 end |
713 |
726 |
714 |
727 |
715 (* transformation of the natural rsp-lemmas into standard form *) |
728 (* transformation of the natural rsp-lemmas into standard form *) |
716 |
729 |