26 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
26 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
27 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
27 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
28 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
28 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
29 val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> |
29 val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> |
30 Proof.context -> thm list * thm list |
30 Proof.context -> thm list * thm list |
|
31 |
31 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
32 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
32 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
33 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
33 term list -> thm -> thm list -> Proof.context -> thm list |
34 term list -> thm -> thm list -> Proof.context -> thm list |
34 val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list |
35 val raw_size_rsp_aux: term list -> thm -> thm list -> Proof.context -> thm list |
35 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
36 val raw_constrs_rsp: term list -> term list -> thm list -> thm list -> Proof.context -> thm list |
36 val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list |
37 val raw_alpha_bn_rsp: term list -> thm list -> thm list -> thm list |
37 |
38 val raw_perm_bn_rsp: term list -> term list -> thm -> thm list -> thm list -> |
|
39 Proof.context -> thm list |
|
40 |
38 val mk_funs_rsp: thm -> thm |
41 val mk_funs_rsp: thm -> thm |
39 val mk_alpha_permute_rsp: thm -> thm |
42 val mk_alpha_permute_rsp: thm -> thm |
40 end |
43 end |
41 |
44 |
42 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
45 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
580 |
583 |
581 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = |
584 fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt = |
582 let |
585 let |
583 val alpha_names = map (fst o dest_Const) alpha_trms |
586 val alpha_names = map (fst o dest_Const) alpha_trms |
584 val props = map prep_trans_goal alpha_trms |
587 val props = map prep_trans_goal alpha_trms |
585 val norm = @{lemma "A ==> (!x. B x --> C x) ==> (!!x. [|A; B x|] ==> C x)" by simp} |
|
586 in |
588 in |
587 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct |
589 alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct |
588 (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt |
590 (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt |
589 end |
591 end |
590 |
592 |
750 in |
752 in |
751 map2 mk_thm alpha_bn_equivp alpha_bn_imps' |
753 map2 mk_thm alpha_bn_equivp alpha_bn_imps' |
752 end |
754 end |
753 |
755 |
754 |
756 |
|
757 (* rsp for permute_bn functions *) |
|
758 |
|
759 val perm_bn_rsp = @{lemma "(!x y p. R x y --> R (f p x) (f p y)) ==> (op= ===> R ===> R) f f" |
|
760 by (simp add: fun_rel_def)} |
|
761 |
|
762 fun raw_prove_perm_bn_tac pred_names alpha_intros simps ctxt = |
|
763 SUBPROOF (fn {prems, context, ...} => |
|
764 let |
|
765 val prems' = flat (map Datatype_Aux.split_conj_thm prems) |
|
766 val prems'' = map (transform_prem1 context pred_names) prems' |
|
767 in |
|
768 HEADGOAL |
|
769 (simp_tac (HOL_basic_ss addsimps (simps @ prems')) |
|
770 THEN' TRY o REPEAT_ALL_NEW |
|
771 (FIRST' [ rtac @{thm TrueI}, |
|
772 rtac @{thm conjI}, |
|
773 rtac @{thm refl}, |
|
774 resolve_tac prems', |
|
775 resolve_tac prems'', |
|
776 resolve_tac alpha_intros ])) |
|
777 end) ctxt |
|
778 |
|
779 fun raw_perm_bn_rsp alpha_trms perm_bns alpha_induct alpha_intros simps ctxt = |
|
780 let |
|
781 val arg_ty = domain_type o fastype_of |
|
782 val perm_bn_ty = range_type o range_type o fastype_of |
|
783 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
|
784 |
|
785 val ([p], ctxt') = Variable.variant_fixes ["p"] ctxt |
|
786 val p = Free (p, @{typ perm}) |
|
787 |
|
788 fun mk_prop t = |
|
789 let |
|
790 val alpha_trm = lookup ty_assoc (perm_bn_ty t) |
|
791 in |
|
792 (alpha_trm, fn (x, y) => alpha_trm $ (t $ p $ x) $ (t $ p $ y)) |
|
793 end |
|
794 |
|
795 val goals = map mk_prop perm_bns |
|
796 val alpha_names = map (fst o dest_Const) alpha_trms |
|
797 |
|
798 in |
|
799 alpha_prove alpha_trms goals alpha_induct |
|
800 (raw_prove_perm_bn_tac alpha_names alpha_intros simps) ctxt |
|
801 |> ProofContext.export ctxt' ctxt |
|
802 |> map atomize |
|
803 |> map single |
|
804 |> map (curry (op OF) perm_bn_rsp) |
|
805 end |
|
806 |
|
807 |
|
808 |
755 (* transformation of the natural rsp-lemmas into standard form *) |
809 (* transformation of the natural rsp-lemmas into standard form *) |
756 |
810 |
757 val fun_rsp = @{lemma |
811 val fun_rsp = @{lemma |
758 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)} |
812 "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by (simp add: fun_rel_def)} |
759 |
813 |