17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list |
17 val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> thm list -> thm list |
18 |
18 |
19 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
19 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
20 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
20 val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list |
21 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
21 val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list |
|
22 val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list |
22 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
23 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
23 end |
24 end |
24 |
25 |
25 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
26 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
26 struct |
27 struct |
540 |> singleton (ProofContext.export ctxt' ctxt) |
541 |> singleton (ProofContext.export ctxt' ctxt) |
541 |> Datatype_Aux.split_conj_thm |
542 |> Datatype_Aux.split_conj_thm |
542 |> map (fn th => zero_var_indexes (th RS norm)) |
543 |> map (fn th => zero_var_indexes (th RS norm)) |
543 end |
544 end |
544 |
545 |
|
546 (* proves the equivp predicate for all alphas *) |
|
547 |
|
548 val equivp_intro = |
|
549 @{lemma "[|!x. R x x; !x y. R x y --> R y x; !x y z. R x y --> R y z --> R x z|] ==> equivp R" |
|
550 by (rule equivpI, unfold reflp_def symp_def transp_def, blast+)} |
|
551 |
|
552 fun raw_prove_equivp alphas refl symm trans ctxt = |
|
553 let |
|
554 val atomize = Conv.fconv_rule Object_Logic.atomize o forall_intr_vars |
|
555 val refl' = map atomize refl |
|
556 val symm' = map atomize symm |
|
557 val trans' = map atomize trans |
|
558 fun prep_goal t = |
|
559 HOLogic.mk_Trueprop (Const (@{const_name "equivp"}, fastype_of t --> @{typ bool}) $ t) |
|
560 in |
|
561 Goal.prove_multi ctxt [] [] (map prep_goal alphas) |
|
562 (K (HEADGOAL (Goal.conjunction_tac THEN_ALL_NEW (rtac equivp_intro THEN' |
|
563 RANGE [resolve_tac refl', resolve_tac symm', resolve_tac trans'])))) |
|
564 end |
|
565 |
545 |
566 |
546 (* proves that alpha_raw implies alpha_bn *) |
567 (* proves that alpha_raw implies alpha_bn *) |
547 |
568 |
548 fun is_true @{term "Trueprop True"} = true |
569 fun is_true @{term "Trueprop True"} = true |
549 | is_true _ = false |
570 | is_true _ = false |
550 |
571 |
551 fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = |
572 fun raw_prove_bn_imp_tac pred_names alpha_intros ctxt = |
552 Subgoal.FOCUS (fn {prems, context, ...} => |
573 SUBPROOF (fn {prems, context, ...} => |
553 let |
574 let |
554 val prems' = flat (map Datatype_Aux.split_conj_thm prems) |
575 val prems' = flat (map Datatype_Aux.split_conj_thm prems) |
555 val prems'' = map (transform_prem1 context pred_names) prems' |
576 val prems'' = map (transform_prem1 context pred_names) prems' |
556 in |
577 in |
557 HEADGOAL (REPEAT o |
578 HEADGOAL |
558 FIRST' [ rtac @{thm TrueI}, |
579 (REPEAT_ALL_NEW |
559 rtac @{thm conjI}, |
580 (FIRST' [ rtac @{thm TrueI}, |
560 resolve_tac prems', |
581 rtac @{thm conjI}, |
561 resolve_tac prems'', |
582 resolve_tac prems', |
562 resolve_tac alpha_intros ]) |
583 resolve_tac prems'', |
|
584 resolve_tac alpha_intros ])) |
563 end) ctxt |
585 end) ctxt |
564 |
586 |
565 fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt = |
587 fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt = |
566 let |
588 let |
567 val alpha_names = map (fst o dest_Const) alpha_trms |
589 val alpha_names = map (fst o dest_Const) alpha_trms |
602 |> HOLogic.mk_Trueprop |
624 |> HOLogic.mk_Trueprop |
603 in |
625 in |
604 Goal.prove ctxt' [] [] goal |
626 Goal.prove ctxt' [] [] goal |
605 (fn {context, ...} => |
627 (fn {context, ...} => |
606 HEADGOAL (DETERM o (rtac alpha_induct) |
628 HEADGOAL (DETERM o (rtac alpha_induct) |
607 THEN_ALL_NEW raw_prove_bn_imp_tac alpha_names alpha_intros context)) |
629 THEN_ALL_NEW (raw_prove_bn_imp_tac alpha_names alpha_intros context))) |
608 |> singleton (ProofContext.export ctxt' ctxt) |
630 |> singleton (ProofContext.export ctxt' ctxt) |
609 |> Datatype_Aux.split_conj_thm |
631 |> Datatype_Aux.split_conj_thm |
610 |> map (fn th => zero_var_indexes (th RS mp)) |
632 |> map (fn th => zero_var_indexes (th RS mp)) |
611 |> map Datatype_Aux.split_conj_thm |
633 |> map Datatype_Aux.split_conj_thm |
612 |> flat |
634 |> flat |
613 |> filter_out (is_true o concl_of) |
635 |> filter_out (is_true o concl_of) |
614 end |
636 end |
615 |
637 |
616 |
|
617 end (* structure *) |
638 end (* structure *) |
618 |
639 |