677 (conj sym_eqs, conj trans_eqs) |
677 (conj sym_eqs, conj trans_eqs) |
678 end |
678 end |
679 *} |
679 *} |
680 |
680 |
681 ML {* |
681 ML {* |
682 fun build_alpha_refl_gl fv_alphas_lst = |
682 fun build_alpha_refl_gl fv_alphas_lst alphas = |
683 let |
683 let |
684 val (fvs_alphas, ls) = split_list fv_alphas_lst; |
684 val (fvs_alphas, _) = split_list fv_alphas_lst; |
685 val (_, alpha_ts) = split_list fvs_alphas; |
685 val (_, alpha_ts) = split_list fvs_alphas; |
686 val tys = map (domain_type o fastype_of) alpha_ts; |
686 val tys = map (domain_type o fastype_of) alpha_ts; |
687 val names = Datatype_Prop.make_tnames tys; |
687 val names = Datatype_Prop.make_tnames tys; |
688 val args = map Free (names ~~ tys); |
688 val args = map Free (names ~~ tys); |
|
689 fun find_alphas ty x = |
|
690 domain_type (fastype_of x) = ty; |
689 fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg; |
691 fun mk_alpha_refl arg (_, alpha) = alpha $ arg $ arg; |
690 fun refl_eq_arg ((alpha, arg), l) = |
692 fun refl_eq_arg (ty, arg) = |
691 foldr1 HOLogic.mk_conj |
693 let |
692 ((alpha $ arg $ arg) :: |
694 val rel_alphas = filter (find_alphas ty) alphas; |
693 (map (mk_alpha_refl arg) l)) |
695 in |
694 val eqs = map refl_eq_arg ((alpha_ts ~~ args) ~~ ls) |
696 map (fn x => x $ arg $ arg) rel_alphas |
|
697 end; |
|
698 (* Flattening loses the induction structure *) |
|
699 val eqs = map (foldr1 HOLogic.mk_conj) (map refl_eq_arg (tys ~~ args)) |
695 in |
700 in |
696 (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) |
701 (names, HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj eqs)) |
697 end |
702 end |
698 *} |
703 *} |
699 |
704 |
706 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
711 @{thms alpha_gen fresh_star_def fresh_zero_perm permute_zero ball_triv |
707 add_0_left supp_zero_perm Int_empty_left split_conv}) |
712 add_0_left supp_zero_perm Int_empty_left split_conv}) |
708 *} |
713 *} |
709 |
714 |
710 ML {* |
715 ML {* |
711 fun build_alpha_refl fv_alphas_lst induct eq_iff ctxt = |
716 fun build_alpha_refl fv_alphas_lst alphas induct eq_iff ctxt = |
712 let |
717 let |
713 val (names, gl) = build_alpha_refl_gl fv_alphas_lst; |
718 val (names, gl) = build_alpha_refl_gl fv_alphas_lst alphas; |
714 val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1); |
719 val refl_conj = Goal.prove ctxt names [] gl (fn _ => reflp_tac induct eq_iff ctxt 1); |
715 in |
720 in |
716 HOLogic.conj_elims refl_conj |
721 HOLogic.conj_elims refl_conj |
717 end |
722 end |
718 *} |
723 *} |
823 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
828 (TRY o rtac allI THEN' imp_elim_tac cases ctxt) THEN_ALL_NEW |
824 asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW |
829 asm_full_simp_tac ((mk_minimal_ss ctxt) addsimps alpha_inj) THEN_ALL_NEW |
825 split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs |
830 split_conjs THEN_ALL_NEW REPEAT o (eetac @{thm exi_sum} ctxt) THEN_ALL_NEW split_conjs |
826 THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
831 THEN_ALL_NEW (asm_full_simp_tac (HOL_ss addsimps (term_inj @ distinct))) |
827 THEN_ALL_NEW split_conjs THEN_ALL_NEW |
832 THEN_ALL_NEW split_conjs THEN_ALL_NEW |
828 TRY o (etac @{thm alpha_gen_compose_trans} THEN' RANGE[atac]) THEN_ALL_NEW |
833 TRY o (etac @{thm alpha_gen_compose_trans2} ORELSE' etac @{thm alpha_gen_compose_trans}) THEN_ALL_NEW |
829 (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) |
834 (asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ eqvt @ term_inj @ distinct))) |
830 *} |
835 *} |
831 |
836 |
832 lemma transp_aux: |
837 lemma transpI: |
833 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
838 "(\<And>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z)) \<Longrightarrow> transp R" |
834 unfolding transp_def |
839 unfolding transp_def |
835 by blast |
840 by blast |
836 |
841 |
837 ML {* |
842 ML {* |
838 fun equivp_tac reflps symps transps = |
843 fun equivp_tac reflps symps transps = |
|
844 let val _ = tracing (PolyML.makestring (reflps, symps, transps)) in |
839 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
845 simp_tac (HOL_ss addsimps @{thms equivp_reflp_symp_transp reflp_def symp_def}) |
840 THEN' rtac conjI THEN' rtac allI THEN' |
846 THEN' rtac conjI THEN' rtac allI THEN' |
841 resolve_tac reflps THEN' |
847 resolve_tac reflps THEN' |
842 rtac conjI THEN' rtac allI THEN' rtac allI THEN' |
848 rtac conjI THEN' rtac allI THEN' rtac allI THEN' |
843 resolve_tac symps THEN' |
849 resolve_tac symps THEN' |
844 rtac @{thm transp_aux} THEN' resolve_tac transps |
850 rtac @{thm transpI} THEN' resolve_tac transps |
|
851 end |
845 *} |
852 *} |
846 |
853 |
847 ML {* |
854 ML {* |
848 fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
855 fun build_equivps alphas reflps alpha_induct term_inj alpha_inj distinct cases eqvt ctxt = |
849 let |
856 let |