34 val get_inductive: theory -> string -> |
34 val get_inductive: theory -> string -> |
35 {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, |
35 {names: string list, coind: bool} * {defs: thm list, elims: thm list, raw_induct: thm, |
36 induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
36 induct: thm, intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
37 val print_inductives: theory -> unit |
37 val print_inductives: theory -> unit |
38 val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> |
38 val add_inductive_i: bool -> bool -> bstring -> bool -> bool -> bool -> term list -> |
39 ((bstring * term) * theory attribute list) list -> thm list -> thm list -> theory -> theory * |
39 theory attribute list -> ((bstring * term) * theory attribute list) list -> |
|
40 thm list -> thm list -> theory -> theory * |
40 {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
41 {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
41 intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
42 intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
42 val add_inductive: bool -> bool -> string list -> ((bstring * string) * Args.src list) list -> |
43 val add_inductive: bool -> bool -> string list -> Args.src list -> |
43 (xstring * Args.src list) list -> (xstring * Args.src list) list -> theory -> theory * |
44 ((bstring * string) * Args.src list) list -> (xstring * Args.src list) list -> |
|
45 (xstring * Args.src list) list -> theory -> theory * |
44 {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
46 {defs: thm list, elims: thm list, raw_induct: thm, induct: thm, |
45 intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
47 intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm} |
46 val setup: (theory -> theory) list |
48 val setup: (theory -> theory) list |
47 end; |
49 end; |
48 |
50 |
450 (*** specification of (co)inductive sets ****) |
452 (*** specification of (co)inductive sets ****) |
451 |
453 |
452 (** definitional introduction of (co)inductive sets **) |
454 (** definitional introduction of (co)inductive sets **) |
453 |
455 |
454 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs |
456 fun add_ind_def verbose declare_consts alt_name coind no_elim no_ind cs |
455 intros monos con_defs thy params paramTs cTs cnames = |
457 atts intros monos con_defs thy params paramTs cTs cnames = |
456 let |
458 let |
457 val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ |
459 val _ = if verbose then message ("Proofs for " ^ coind_prefix coind ^ "inductive set(s) " ^ |
458 commas_quote cnames) else (); |
460 commas_quote cnames) else (); |
459 |
461 |
460 val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; |
462 val sumT = fold_bal (fn (T, U) => Type ("+", [T, U])) cTs; |
537 rec_sets_defs thy'; |
539 rec_sets_defs thy'; |
538 val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct |
540 val induct = if coind orelse no_ind orelse length cs > 1 then raw_induct |
539 else standard (raw_induct RSN (2, rev_mp)); |
541 else standard (raw_induct RSN (2, rev_mp)); |
540 |
542 |
541 val thy'' = thy' |
543 val thy'' = thy' |
542 |> PureThy.add_thmss [(("intrs", intrs), [])] |
544 |> PureThy.add_thmss [(("intrs", intrs), atts)] |
543 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) |
545 |> PureThy.add_thms ((intr_names ~~ intrs) ~~ intr_atts) |
544 |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])]) |
546 |> (if no_elim then I else PureThy.add_thmss [(("elims", elims), [])]) |
545 |> (if no_ind then I else PureThy.add_thms |
547 |> (if no_ind then I else PureThy.add_thms |
546 [((coind_prefix coind ^ "induct", induct), [])]) |
548 [((coind_prefix coind ^ "induct", induct), [])]) |
547 |> Theory.parent_path; |
549 |> Theory.parent_path; |
560 |
562 |
561 |
563 |
562 (** axiomatic introduction of (co)inductive sets **) |
564 (** axiomatic introduction of (co)inductive sets **) |
563 |
565 |
564 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs |
566 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs |
565 intros monos con_defs thy params paramTs cTs cnames = |
567 atts intros monos con_defs thy params paramTs cTs cnames = |
566 let |
568 let |
567 val _ = if verbose then message ("Adding axioms for " ^ coind_prefix coind ^ |
569 val _ = if verbose then message ("Adding axioms for " ^ coind_prefix coind ^ |
568 "inductive set(s) " ^ commas_quote cnames) else (); |
570 "inductive set(s) " ^ commas_quote cnames) else (); |
569 |
571 |
570 val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; |
572 val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name; |
579 |> (if declare_consts then |
581 |> (if declare_consts then |
580 Theory.add_consts_i |
582 Theory.add_consts_i |
581 (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames)) |
583 (map (fn (c, n) => (n, paramTs ---> fastype_of c, NoSyn)) (cs ~~ cnames)) |
582 else I) |
584 else I) |
583 |> Theory.add_path rec_name |
585 |> Theory.add_path rec_name |
584 |> PureThy.add_axiomss_i [(("intrs", intr_ts), []), (("elims", elim_ts), [])] |
586 |> PureThy.add_axiomss_i [(("intrs", intr_ts), atts), (("elims", elim_ts), [])] |
585 |> (if coind then I else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]); |
587 |> (if coind then I else PureThy.add_axioms_i [(("internal_induct", ind_t), [])]); |
586 |
588 |
587 val intrs = PureThy.get_thms thy' "intrs"; |
589 val intrs = PureThy.get_thms thy' "intrs"; |
588 val elims = PureThy.get_thms thy' "elims"; |
590 val elims = PureThy.get_thms thy' "elims"; |
589 val raw_induct = if coind then TrueI else |
591 val raw_induct = if coind then TrueI else |
610 |
612 |
611 |
613 |
612 (** introduction of (co)inductive sets **) |
614 (** introduction of (co)inductive sets **) |
613 |
615 |
614 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs |
616 fun add_inductive_i verbose declare_consts alt_name coind no_elim no_ind cs |
615 intros monos con_defs thy = |
617 atts intros monos con_defs thy = |
616 let |
618 let |
617 val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); |
619 val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions"); |
618 val sign = Theory.sign_of thy; |
620 val sign = Theory.sign_of thy; |
619 |
621 |
620 (*parameters should agree for all mutually recursive components*) |
622 (*parameters should agree for all mutually recursive components*) |
633 (fn a => "Base name of recursive set not an identifier: " ^ a); |
635 (fn a => "Base name of recursive set not an identifier: " ^ a); |
634 val _ = seq (check_rule sign cs o snd o fst) intros; |
636 val _ = seq (check_rule sign cs o snd o fst) intros; |
635 |
637 |
636 val (thy1, result) = |
638 val (thy1, result) = |
637 (if ! quick_and_dirty then add_ind_axm else add_ind_def) |
639 (if ! quick_and_dirty then add_ind_axm else add_ind_def) |
638 verbose declare_consts alt_name coind no_elim no_ind cs intros monos |
640 verbose declare_consts alt_name coind no_elim no_ind cs atts intros monos |
639 con_defs thy params paramTs cTs cnames; |
641 con_defs thy params paramTs cTs cnames; |
640 val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result); |
642 val thy2 = thy1 |> put_inductives full_cnames ({names = full_cnames, coind = coind}, result); |
641 in (thy2, result) end; |
643 in (thy2, result) end; |
642 |
644 |
643 |
645 |
644 |
646 |
645 (** external interface **) |
647 (** external interface **) |
646 |
648 |
647 fun add_inductive verbose coind c_strings intro_srcs raw_monos raw_con_defs thy = |
649 fun add_inductive verbose coind c_strings srcs intro_srcs raw_monos raw_con_defs thy = |
648 let |
650 let |
649 val sign = Theory.sign_of thy; |
651 val sign = Theory.sign_of thy; |
650 val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings; |
652 val cs = map (readtm (Theory.sign_of thy) HOLogic.termTVar) c_strings; |
651 |
653 |
|
654 val atts = map (Attrib.global_attribute thy) srcs; |
652 val intr_names = map (fst o fst) intro_srcs; |
655 val intr_names = map (fst o fst) intro_srcs; |
653 val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs; |
656 val intr_ts = map (readtm (Theory.sign_of thy) propT o snd o fst) intro_srcs; |
654 val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; |
657 val intr_atts = map (map (Attrib.global_attribute thy) o snd) intro_srcs; |
655 |
658 |
656 (* the following code ensures that each recursive set *) |
659 (* the following code ensures that each recursive set *) |
684 val ((thy', con_defs), monos) = thy |
687 val ((thy', con_defs), monos) = thy |
685 |> IsarThy.apply_theorems raw_monos |
688 |> IsarThy.apply_theorems raw_monos |
686 |> apfst (IsarThy.apply_theorems raw_con_defs); |
689 |> apfst (IsarThy.apply_theorems raw_con_defs); |
687 in |
690 in |
688 add_inductive_i verbose false "" coind false false cs'' |
691 add_inductive_i verbose false "" coind false false cs'' |
689 ((intr_names ~~ intr_ts'') ~~ intr_atts) monos con_defs thy' |
692 atts ((intr_names ~~ intr_ts'') ~~ intr_atts) monos con_defs thy' |
690 end; |
693 end; |
691 |
694 |
692 |
695 |
693 |
696 |
694 (** package setup **) |
697 (** package setup **) |
700 |
703 |
701 (* outer syntax *) |
704 (* outer syntax *) |
702 |
705 |
703 local open OuterParse in |
706 local open OuterParse in |
704 |
707 |
705 fun mk_ind coind (((sets, intrs), monos), con_defs) = |
708 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) = |
706 #1 o add_inductive true coind sets (map triple_swap intrs) monos con_defs; |
709 #1 o add_inductive true coind sets atts (map triple_swap intrs) monos con_defs; |
707 |
710 |
708 fun ind_decl coind = |
711 fun ind_decl coind = |
709 Scan.repeat1 term -- |
712 Scan.repeat1 term -- |
710 ($$$ "intrs" |-- !!! (Scan.repeat1 (opt_thm_name ":" -- term))) -- |
713 ($$$ "intrs" |-- !!! (opt_attribs -- Scan.repeat1 (opt_thm_name ":" -- term))) -- |
711 Scan.optional ($$$ "monos" |-- !!! xthms1) [] -- |
714 Scan.optional ($$$ "monos" |-- !!! xthms1) [] -- |
712 Scan.optional ($$$ "con_defs" |-- !!! xthms1) [] |
715 Scan.optional ($$$ "con_defs" |-- !!! xthms1) [] |
713 >> (Toplevel.theory o mk_ind coind); |
716 >> (Toplevel.theory o mk_ind coind); |
714 |
717 |
715 val inductiveP = OuterSyntax.command "inductive" "define inductive sets" (ind_decl false); |
718 val inductiveP = OuterSyntax.command "inductive" "define inductive sets" (ind_decl false); |