12 term list * term list * thm list * thm list * thm * local_theory |
12 term list * term list * thm list * thm list * thm * local_theory |
13 |
13 |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> |
14 val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> |
15 term list -> term list -> bn_info -> thm list * thm list |
15 term list -> term list -> bn_info -> thm list * thm list |
16 |
16 |
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 -> |
|
18 thm list -> (thm list * thm list) |
18 |
19 |
19 val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
20 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 |
21 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 |
22 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 |
23 val raw_prove_equivp: term list -> thm list -> thm list -> thm list -> Proof.context -> thm list |
23 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
24 val raw_prove_bn_imp: term list -> term list -> thm list -> thm -> Proof.context -> thm list |
|
25 val raw_fv_bn_rsp_aux: term list -> term list -> term list -> term list -> |
|
26 term list -> thm -> thm list -> Proof.context -> thm list |
24 end |
27 end |
25 |
28 |
26 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
29 structure Nominal_Dt_Alpha: NOMINAL_DT_ALPHA = |
27 struct |
30 struct |
28 |
31 |
331 val goals = map mk_alpha_eq_iff_goal thms_imp; |
334 val goals = map mk_alpha_eq_iff_goal thms_imp; |
332 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
335 val tac = alpha_eq_iff_tac (distinct_thms @ inject_thms) alpha_intros alpha_elims 1; |
333 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
336 val thms = map (fn goal => Goal.prove ctxt' [] [] goal (K tac)) goals; |
334 in |
337 in |
335 Variable.export ctxt' ctxt thms |
338 Variable.export ctxt' ctxt thms |
336 |> map mk_simp_rule |
339 |> `(map mk_simp_rule) |
337 end |
340 end |
338 |
341 |
339 |
342 |
340 |
343 |
341 (** reflexivity proof for the alphas **) |
344 (** reflexivity proof for the alphas **) |
635 |> map Datatype_Aux.split_conj_thm |
638 |> map Datatype_Aux.split_conj_thm |
636 |> flat |
639 |> flat |
637 |> filter_out (is_true o concl_of) |
640 |> filter_out (is_true o concl_of) |
638 end |
641 end |
639 |
642 |
|
643 |
|
644 (* helper lemmas for respectfulness for fv_raw / bn_raw *) |
|
645 |
|
646 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
|
647 let |
|
648 val arg_tys = |
|
649 alpha_trms |
|
650 |> map fastype_of |
|
651 |> map domain_type |
|
652 |
|
653 val fv_bn_tys1 = |
|
654 (bns @ fvs) |
|
655 |> map fastype_of |
|
656 |> map domain_type |
|
657 |
|
658 val (arg_names1, (arg_names2, ctxt')) = |
|
659 ctxt |
|
660 |> Variable.variant_fixes (replicate (length arg_tys) "x") |
|
661 ||> Variable.variant_fixes (replicate (length arg_tys) "y") |
|
662 |
|
663 val args1 = map Free (arg_names1 ~~ arg_tys) |
|
664 val args2 = map Free (arg_names2 ~~ arg_tys) |
|
665 |
|
666 val fv_bn_args1a = map (lookup (arg_tys ~~ args1)) fv_bn_tys1 |
|
667 val fv_bn_args1b = map (lookup (arg_tys ~~ args2)) fv_bn_tys1 |
|
668 val fv_bn_eqs1 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) |
|
669 (bns @ fvs) (fv_bn_args1a ~~ fv_bn_args1b) |
|
670 |
|
671 val arg_bn_tys = |
|
672 alpha_bn_trms |
|
673 |> map fastype_of |
|
674 |> map domain_type |
|
675 |
|
676 val fv_bn_tys2 = |
|
677 fv_bns |
|
678 |> map fastype_of |
|
679 |> map domain_type |
|
680 |
|
681 val (arg_bn_names1, (arg_bn_names2, ctxt'')) = |
|
682 ctxt' |
|
683 |> Variable.variant_fixes (replicate (length arg_bn_tys) "x") |
|
684 ||> Variable.variant_fixes (replicate (length arg_bn_tys) "y") |
|
685 |
|
686 val args_bn1 = map Free (arg_bn_names1 ~~ fv_bn_tys2) |
|
687 val args_bn2 = map Free (arg_bn_names2 ~~ fv_bn_tys2) |
|
688 val fv_bn_eqs2 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) |
|
689 fv_bns (args_bn1 ~~ args_bn2) |
|
690 |
|
691 val goal_rhs = |
|
692 group (fv_bn_tys1 ~~ fv_bn_eqs1) |
|
693 |> map snd |
|
694 |> map (foldr1 HOLogic.mk_conj) |
|
695 |
|
696 val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) |
|
697 (alpha_trms @ alpha_bn_trms) ((args1 ~~ args2) @ (args_bn1 ~~ args_bn2)) |
|
698 |
|
699 val goal = |
|
700 map2 (curry HOLogic.mk_imp) goal_lhs (goal_rhs @ fv_bn_eqs2) |
|
701 |> foldr1 HOLogic.mk_conj |
|
702 |> HOLogic.mk_Trueprop |
|
703 |
|
704 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
|
705 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
|
706 in |
|
707 Goal.prove ctxt'' [] [] goal (fn {context, ...} => |
|
708 HEADGOAL (DETERM o (rtac alpha_induct) THEN_ALL_NEW (asm_full_simp_tac ss))) |
|
709 |> singleton (ProofContext.export ctxt'' ctxt) |
|
710 |> Datatype_Aux.split_conj_thm |
|
711 |> map (fn th => zero_var_indexes (th RS mp)) |
|
712 |> map Datatype_Aux.split_conj_thm |
|
713 |> flat |
|
714 end |
|
715 |
640 end (* structure *) |
716 end (* structure *) |
641 |
717 |