379 in |
379 in |
380 Goal.prove ctxt' [] [] goal |
380 Goal.prove ctxt' [] [] goal |
381 (fn {context, ...} => HEADGOAL |
381 (fn {context, ...} => HEADGOAL |
382 (DETERM o (rtac alpha_induct_thm) THEN_ALL_NEW (rtac @{thm TrueI} ORELSE' cases_tac context))) |
382 (DETERM o (rtac alpha_induct_thm) THEN_ALL_NEW (rtac @{thm TrueI} ORELSE' cases_tac context))) |
383 |> singleton (ProofContext.export ctxt' ctxt) |
383 |> singleton (ProofContext.export ctxt' ctxt) |
384 |> Datatype_Aux.split_conj_thm |
384 |> Datatype_Aux.split_conj_thm |
|
385 |> map (fn th => th RS mp) |
385 |> map Datatype_Aux.split_conj_thm |
386 |> map Datatype_Aux.split_conj_thm |
386 |> flat |
387 |> flat |
387 |> map zero_var_indexes |
388 |> map zero_var_indexes |
388 |> map (fn th => th RS mp) |
389 |
389 |> filter_out (is_true o concl_of) |
390 |> filter_out (is_true o concl_of) |
390 end |
391 end |
391 |
392 |
392 |
393 |
393 (** reflexivity proof for the alphas **) |
394 (** reflexivity proof for the alphas **) |
585 resolve_tac prems', |
587 resolve_tac prems', |
586 resolve_tac prems'', |
588 resolve_tac prems'', |
587 resolve_tac alpha_intros ])) |
589 resolve_tac alpha_intros ])) |
588 end) ctxt |
590 end) ctxt |
589 |
591 |
590 fun raw_prove_bn_imp alpha_trms alpha_bns alpha_intros alpha_induct ctxt = |
592 fun raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct ctxt = |
591 let |
593 let |
|
594 val arg_ty = domain_type o fastype_of |
592 val alpha_names = map (fst o dest_Const) alpha_trms |
595 val alpha_names = map (fst o dest_Const) alpha_trms |
593 |
596 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
594 val arg_tys = |
597 val props = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => t $ x $ y)) alpha_bn_trms |
595 alpha_trms |
598 in |
596 |> map fastype_of |
599 alpha_prove (alpha_trms @ alpha_bn_trms) props alpha_induct |
597 |> map domain_type |
600 (raw_prove_bn_imp_tac alpha_names alpha_intros) ctxt |
598 val arg_bn_tys = |
|
599 alpha_bns |
|
600 |> map fastype_of |
|
601 |> map domain_type |
|
602 val (arg_names1, (arg_names2, ctxt')) = |
|
603 ctxt |
|
604 |> Variable.variant_fixes (replicate (length arg_tys) "x") |
|
605 ||> Variable.variant_fixes (replicate (length arg_tys) "y") |
|
606 val arg_bn_names1 = map (lookup (arg_tys ~~ arg_names1)) arg_bn_tys |
|
607 val arg_bn_names2 = map (lookup (arg_tys ~~ arg_names2)) arg_bn_tys |
|
608 val args1 = map Free (arg_names1 ~~ arg_tys) |
|
609 val args2 = map Free (arg_names2 ~~ arg_tys) |
|
610 val arg_bns1 = map Free (arg_bn_names1 ~~ arg_bn_tys) |
|
611 val arg_bns2 = map Free (arg_bn_names2 ~~ arg_bn_tys) |
|
612 |
|
613 val alpha_bn_trms = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_bns (arg_bns1 ~~ arg_bns2) |
|
614 val true_trms = map (K @{term True}) arg_tys |
|
615 |
|
616 val goal_rhs = |
|
617 group ((arg_bn_tys ~~ alpha_bn_trms) @ (arg_tys ~~ true_trms)) |
|
618 |> map snd |
|
619 |> map (foldr1 HOLogic.mk_conj) |
|
620 |
|
621 val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) alpha_trms (args1 ~~ args2) |
|
622 val goal_rest = map (fn t => HOLogic.mk_imp (t, @{term "True"})) alpha_bn_trms |
|
623 |
|
624 val goal = |
|
625 (map2 (curry HOLogic.mk_imp) goal_lhs goal_rhs) @ goal_rest |
|
626 |> foldr1 HOLogic.mk_conj |
|
627 |> HOLogic.mk_Trueprop |
|
628 in |
|
629 Goal.prove ctxt' [] [] goal |
|
630 (fn {context, ...} => |
|
631 HEADGOAL (DETERM o (rtac alpha_induct) |
|
632 THEN_ALL_NEW (raw_prove_bn_imp_tac alpha_names alpha_intros context))) |
|
633 |> singleton (ProofContext.export ctxt' ctxt) |
|
634 |> Datatype_Aux.split_conj_thm |
|
635 |> map (fn th => zero_var_indexes (th RS mp)) |
|
636 |> map Datatype_Aux.split_conj_thm |
|
637 |> flat |
|
638 |> filter_out (is_true o concl_of) |
|
639 end |
601 end |
640 |
602 |
641 |
603 |
642 (* helper lemmas for respectfulness for fv_raw / bn_raw *) |
604 (* helper lemmas for respectfulness for fv_raw / bn_raw *) |
643 |
605 |
644 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
606 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt = |
645 let |
607 let |
646 val arg_tys = |
608 val arg_ty = domain_type o fastype_of |
647 alpha_trms |
609 val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms |
648 |> map fastype_of |
610 |
649 |> map domain_type |
611 val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) fvs |
650 |
612 val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => HOLogic.mk_eq (t $ x, t $ y))) bns |
651 val fv_bn_tys1 = |
613 val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => HOLogic.mk_eq (t2 $ x, t2 $ y))) alpha_bn_trms fv_bns |
652 (bns @ fvs) |
|
653 |> map fastype_of |
|
654 |> map domain_type |
|
655 |
|
656 val (arg_names1, (arg_names2, ctxt')) = |
|
657 ctxt |
|
658 |> Variable.variant_fixes (replicate (length arg_tys) "x") |
|
659 ||> Variable.variant_fixes (replicate (length arg_tys) "y") |
|
660 |
614 |
661 val args1 = map Free (arg_names1 ~~ arg_tys) |
|
662 val args2 = map Free (arg_names2 ~~ arg_tys) |
|
663 |
|
664 val fv_bn_args1a = map (lookup (arg_tys ~~ args1)) fv_bn_tys1 |
|
665 val fv_bn_args1b = map (lookup (arg_tys ~~ args2)) fv_bn_tys1 |
|
666 val fv_bn_eqs1 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) |
|
667 (bns @ fvs) (fv_bn_args1a ~~ fv_bn_args1b) |
|
668 |
|
669 val arg_bn_tys = |
|
670 alpha_bn_trms |
|
671 |> map fastype_of |
|
672 |> map domain_type |
|
673 |
|
674 val fv_bn_tys2 = |
|
675 fv_bns |
|
676 |> map fastype_of |
|
677 |> map domain_type |
|
678 |
|
679 val (arg_bn_names1, (arg_bn_names2, ctxt'')) = |
|
680 ctxt' |
|
681 |> Variable.variant_fixes (replicate (length arg_bn_tys) "x") |
|
682 ||> Variable.variant_fixes (replicate (length arg_bn_tys) "y") |
|
683 |
|
684 val args_bn1 = map Free (arg_bn_names1 ~~ fv_bn_tys2) |
|
685 val args_bn2 = map Free (arg_bn_names2 ~~ fv_bn_tys2) |
|
686 val fv_bn_eqs2 = map2 (fn trm => fn (ar1, ar2) => HOLogic.mk_eq (trm $ ar1, trm $ ar2)) |
|
687 fv_bns (args_bn1 ~~ args_bn2) |
|
688 |
|
689 val goal_rhs = |
|
690 group (fv_bn_tys1 ~~ fv_bn_eqs1) |
|
691 |> map snd |
|
692 |> map (foldr1 HOLogic.mk_conj) |
|
693 |
|
694 val goal_lhs = map2 (fn t => fn (ar1, ar2) => t $ ar1 $ ar2) |
|
695 (alpha_trms @ alpha_bn_trms) ((args1 ~~ args2) @ (args_bn1 ~~ args_bn2)) |
|
696 |
|
697 val goal = |
|
698 map2 (curry HOLogic.mk_imp) goal_lhs (goal_rhs @ fv_bn_eqs2) |
|
699 |> foldr1 HOLogic.mk_conj |
|
700 |> HOLogic.mk_Trueprop |
|
701 |
|
702 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
615 val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} |
703 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
616 @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) |
704 in |
617 in |
705 Goal.prove ctxt'' [] [] goal (fn {context, ...} => |
618 alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct |
706 HEADGOAL (DETERM o (rtac alpha_induct) THEN_ALL_NEW (asm_full_simp_tac ss))) |
619 (K (asm_full_simp_tac ss)) ctxt |
707 |> singleton (ProofContext.export ctxt'' ctxt) |
|
708 |> Datatype_Aux.split_conj_thm |
|
709 |> map (fn th => zero_var_indexes (th RS mp)) |
|
710 |> map Datatype_Aux.split_conj_thm |
|
711 |> flat |
|
712 end |
620 end |
713 |
621 |
714 end (* structure *) |
622 end (* structure *) |
715 |
623 |