21 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
21 (Proof.context -> int -> tactic) -> Proof.context -> thm list |
22 |
22 |
23 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
23 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
24 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
24 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
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 -> term list -> thm list -> thm list -> thm list -> |
|
27 Proof.context -> thm list * thm list |
27 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
28 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 -> |
29 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
29 term list -> thm -> thm list -> Proof.context -> thm list |
30 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_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 |
32 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
|
33 val raw_alpha_bn_rsp: thm list -> thm list -> thm list |
32 |
34 |
33 val mk_funs_rsp: thm -> thm |
35 val mk_funs_rsp: thm -> thm |
34 val mk_alpha_permute_rsp: thm -> thm |
36 val mk_alpha_permute_rsp: thm -> thm |
35 end |
37 end |
36 |
38 |
561 |
563 |
562 val transp_def' = |
564 val transp_def' = |
563 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
565 @{lemma "transp R == !x y. R x y --> (!z. R y z --> R x z)" |
564 by (rule eq_reflection, auto simp add: transp_def)} |
566 by (rule eq_reflection, auto simp add: transp_def)} |
565 |
567 |
566 fun raw_prove_equivp alphas refl symm trans ctxt = |
568 fun raw_prove_equivp alphas alpha_bns refl symm trans ctxt = |
567 let |
569 let |
568 val refl' = map (fold_rule @{thms reflp_def} o atomize) refl |
570 val refl' = map (fold_rule @{thms reflp_def} o atomize) refl |
569 val symm' = map (fold_rule @{thms symp_def} o atomize) symm |
571 val symm' = map (fold_rule @{thms symp_def} o atomize) symm |
570 val trans' = map (fold_rule [transp_def'] o atomize) trans |
572 val trans' = map (fold_rule [transp_def'] o atomize) trans |
571 |
573 |
572 fun prep_goal t = |
574 fun prep_goal t = |
573 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
575 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
574 in |
576 in |
575 Goal.prove_multi ctxt [] [] (map prep_goal alphas) |
577 Goal.prove_multi ctxt [] [] (map prep_goal (alphas @ alpha_bns)) |
576 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' |
578 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac @{thm equivpI} THEN' |
577 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
579 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
|
580 |> chop (length alphas) |
578 end |
581 end |
579 |
582 |
580 |
583 |
581 (* proves that alpha_raw implies alpha_bn *) |
584 (* proves that alpha_raw implies alpha_bn *) |
582 |
585 |
689 (K (HEADGOAL |
692 (K (HEADGOAL |
690 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) |
693 (Goal.conjunction_tac THEN_ALL_NEW raw_constr_rsp_tac alpha_intros simps))) |
691 end |
694 end |
692 |
695 |
693 |
696 |
|
697 (* rsp lemmas for alpha_bn relations *) |
|
698 |
|
699 val rsp_equivp = |
|
700 @{lemma "[|equivp Q; !!x y. R x y ==> Q x y|] ==> (R ===> R ===> op =) Q Q" |
|
701 by (simp only: fun_rel_def equivp_def, metis)} |
|
702 |
|
703 fun raw_alpha_bn_rsp alpha_bn_equivp alpha_bn_imps = |
|
704 let |
|
705 fun mk_thm thm1 thm2 = |
|
706 (forall_intr_vars thm2) COMP (thm1 RS rsp_equivp) |
|
707 in |
|
708 map2 mk_thm alpha_bn_equivp alpha_bn_imps |
|
709 end |
|
710 |
|
711 |
694 (* transformation of the natural rsp-lemmas into standard form *) |
712 (* transformation of the natural rsp-lemmas into standard form *) |
695 |
713 |
696 val fun_rsp = @{lemma |
714 val fun_rsp = @{lemma |
697 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp} |
715 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp} |
698 |
716 |