684 add_rules simps case_thms size_thms rec_thms inject distinct |
684 add_rules simps case_thms size_thms rec_thms inject distinct |
685 weak_case_congs Simplifier.cong_add_global |> |
685 weak_case_congs Simplifier.cong_add_global |> |
686 put_datatypes (fold Symtab.update dt_infos dt_info) |> |
686 put_datatypes (fold Symtab.update dt_infos dt_info) |> |
687 add_cases_induct dt_infos induct |> |
687 add_cases_induct dt_infos induct |> |
688 Theory.parent_path |> |
688 Theory.parent_path |> |
689 (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> |
689 store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> |
690 DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos); |
690 DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos); |
691 in |
691 in |
692 ({distinct = distinct, |
692 ({distinct = distinct, |
693 inject = inject, |
693 inject = inject, |
694 exhaustion = exhaustion, |
694 exhaustion = exhaustion, |
706 fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info |
706 fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info |
707 case_names_induct case_names_exhausts thy = |
707 case_names_induct case_names_exhausts thy = |
708 let |
708 let |
709 val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names); |
709 val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names); |
710 |
710 |
711 val (thy2, inject, distinct, dist_rewrites, simproc_dists, induct) = thy |> |
711 val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |> |
712 DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts |
712 DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts |
713 types_syntax constr_syntax case_names_induct; |
713 types_syntax constr_syntax case_names_induct; |
714 |
714 |
715 val (thy3, casedist_thms) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr |
715 val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr |
716 sorts induct case_names_exhausts thy2; |
716 sorts induct case_names_exhausts thy2; |
717 val (thy4, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms |
717 val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms |
718 flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3; |
718 flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3; |
719 val (thy6, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms |
719 val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms |
720 flat_names new_type_names descr sorts reccomb_names rec_thms thy4; |
720 flat_names new_type_names descr sorts reccomb_names rec_thms thy4; |
721 val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names |
721 val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names |
722 descr sorts inject dist_rewrites casedist_thms case_thms thy6; |
722 descr sorts inject dist_rewrites casedist_thms case_thms thy6; |
723 val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names |
723 val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names |
724 descr sorts casedist_thms thy7; |
724 descr sorts casedist_thms thy7; |
725 val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names |
725 val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names |
726 descr sorts nchotomys case_thms thy8; |
726 descr sorts nchotomys case_thms thy8; |
727 val (thy10, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names |
727 val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names |
728 descr sorts thy9; |
728 descr sorts thy9; |
729 val (thy11, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names |
729 val (size_thms, thy11) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names |
730 descr sorts reccomb_names rec_thms thy10; |
730 descr sorts reccomb_names rec_thms thy10; |
731 |
731 |
732 val dt_infos = map (make_dt_info (List.concat descr) induct reccomb_names rec_thms) |
732 val dt_infos = map (make_dt_info (List.concat descr) induct reccomb_names rec_thms) |
733 ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~ |
733 ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~ |
734 casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); |
734 casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); |
741 add_rules simps case_thms size_thms rec_thms inject distinct |
741 add_rules simps case_thms size_thms rec_thms inject distinct |
742 weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> |
742 weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> |
743 put_datatypes (fold Symtab.update dt_infos dt_info) |> |
743 put_datatypes (fold Symtab.update dt_infos dt_info) |> |
744 add_cases_induct dt_infos induct |> |
744 add_cases_induct dt_infos induct |> |
745 Theory.parent_path |> |
745 Theory.parent_path |> |
746 (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> |
746 store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> |
747 DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos); |
747 DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos); |
748 in |
748 in |
749 ({distinct = distinct, |
749 ({distinct = distinct, |
750 inject = inject, |
750 inject = inject, |
751 exhaustion = casedist_thms, |
751 exhaustion = casedist_thms, |
808 val case_names_exhausts = mk_case_names_exhausts descr (map #1 dtnames); |
808 val case_names_exhausts = mk_case_names_exhausts descr (map #1 dtnames); |
809 |
809 |
810 |
810 |
811 val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names); |
811 val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names); |
812 |
812 |
813 val (thy2, casedist_thms) = thy1 |> |
813 val (casedist_thms, thy2) = thy1 |> |
814 DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction |
814 DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction |
815 case_names_exhausts; |
815 case_names_exhausts; |
816 val (thy3, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms |
816 val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms |
817 false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2; |
817 false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2; |
818 val (thy4, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms false |
818 val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false |
819 new_type_names [descr] sorts reccomb_names rec_thms thy3; |
819 new_type_names [descr] sorts reccomb_names rec_thms thy3; |
820 val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms |
820 val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms |
821 new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4; |
821 new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4; |
822 val (thy6, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names |
822 val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names |
823 [descr] sorts casedist_thms thy5; |
823 [descr] sorts casedist_thms thy5; |
824 val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names |
824 val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names |
825 [descr] sorts nchotomys case_thms thy6; |
825 [descr] sorts nchotomys case_thms thy6; |
826 val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names |
826 val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names |
827 [descr] sorts thy7; |
827 [descr] sorts thy7; |
828 val (thy9, size_thms) = |
828 val (size_thms, thy9) = |
829 if Context.exists_name "NatArith" thy8 then |
829 if Context.exists_name "NatArith" thy8 then |
830 DatatypeAbsProofs.prove_size_thms false new_type_names |
830 DatatypeAbsProofs.prove_size_thms false new_type_names |
831 [descr] sorts reccomb_names rec_thms thy8 |
831 [descr] sorts reccomb_names rec_thms thy8 |
832 else (thy8, []); |
832 else ([], thy8); |
833 |
833 |
834 val (thy10, [induction']) = thy9 |> |
834 val ([induction'], thy10) = thy9 |> |
835 (#1 o store_thmss "inject" new_type_names inject) |> |
835 store_thmss "inject" new_type_names inject |> snd |> |
836 (#1 o store_thmss "distinct" new_type_names distinct) |> |
836 store_thmss "distinct" new_type_names distinct |> snd |> |
837 Theory.add_path (space_implode "_" new_type_names) |> |
837 Theory.add_path (space_implode "_" new_type_names) |> |
838 PureThy.add_thms [(("induct", induction), [case_names_induct])]; |
838 PureThy.add_thms [(("induct", induction), [case_names_induct])] |> Library.swap; |
839 |
839 |
840 val dt_infos = map (make_dt_info descr induction' reccomb_names rec_thms) |
840 val dt_infos = map (make_dt_info descr induction' reccomb_names rec_thms) |
841 ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~ |
841 ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~ |
842 map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); |
842 map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); |
843 |
843 |
848 add_rules simps case_thms size_thms rec_thms inject distinct |
848 add_rules simps case_thms size_thms rec_thms inject distinct |
849 weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> |
849 weak_case_congs (Simplifier.change_global_ss (op addcongs)) |> |
850 put_datatypes (fold Symtab.update dt_infos dt_info) |> |
850 put_datatypes (fold Symtab.update dt_infos dt_info) |> |
851 add_cases_induct dt_infos induction' |> |
851 add_cases_induct dt_infos induction' |> |
852 Theory.parent_path |> |
852 Theory.parent_path |> |
853 (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> |
853 (snd o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |> |
854 DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos); |
854 DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos); |
855 in |
855 in |
856 ({distinct = distinct, |
856 ({distinct = distinct, |
857 inject = inject, |
857 inject = inject, |
858 exhaustion = casedist_thms, |
858 exhaustion = casedist_thms, |