702 val setup = [InductiveData.init]; |
702 val setup = [InductiveData.init]; |
703 |
703 |
704 |
704 |
705 (* outer syntax *) |
705 (* outer syntax *) |
706 |
706 |
707 local open OuterParse in |
707 local structure P = OuterParse and K = OuterSyntax.Keyword in |
708 |
708 |
709 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) = |
709 fun mk_ind coind (((sets, (atts, intrs)), monos), con_defs) = |
710 #1 o add_inductive true coind sets atts (map triple_swap intrs) monos con_defs; |
710 #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs; |
711 |
711 |
712 fun ind_decl coind = |
712 fun ind_decl coind = |
713 Scan.repeat1 term -- |
713 Scan.repeat1 P.term -- |
714 ($$$ "intrs" |-- !!! (opt_attribs -- Scan.repeat1 (opt_thm_name ":" -- term))) -- |
714 (P.$$$ "intrs" |-- P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term))) -- |
715 Scan.optional ($$$ "monos" |-- !!! xthms1) [] -- |
715 Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] -- |
716 Scan.optional ($$$ "con_defs" |-- !!! xthms1) [] |
716 Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] |
717 >> (Toplevel.theory o mk_ind coind); |
717 >> (Toplevel.theory o mk_ind coind); |
718 |
718 |
719 val inductiveP = OuterSyntax.command "inductive" "define inductive sets" (ind_decl false); |
719 val inductiveP = |
720 val coinductiveP = OuterSyntax.command "coinductive" "define coinductive sets" (ind_decl true); |
720 OuterSyntax.command "inductive" "define inductive sets" K.thy_decl (ind_decl false); |
|
721 |
|
722 val coinductiveP = |
|
723 OuterSyntax.command "coinductive" "define coinductive sets" K.thy_decl (ind_decl true); |
721 |
724 |
722 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; |
725 val _ = OuterSyntax.add_keywords ["intrs", "monos", "con_defs"]; |
723 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP]; |
726 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP]; |
724 |
727 |
725 end; |
728 end; |