578 |
578 |
579 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) = |
579 fun mk_ind (((((doms, intrs), monos), con_defs), type_intrs), type_elims) = |
580 #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims); |
580 #1 o add_inductive doms (map Parse.triple_swap intrs) (monos, con_defs, type_intrs, type_elims); |
581 |
581 |
582 val ind_decl = |
582 val ind_decl = |
583 (Parse.$$$ "domains" |-- Parse.!!! (Parse.enum1 "+" Parse.term -- |
583 (@{keyword "domains"} |-- Parse.!!! (Parse.enum1 "+" Parse.term -- |
584 ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.term))) -- |
584 ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.term))) -- |
585 (Parse.$$$ "intros" |-- |
585 (@{keyword "intros"} |-- |
586 Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) -- |
586 Parse.!!! (Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop))) -- |
587 Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] -- |
587 Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] -- |
588 Scan.optional (Parse.$$$ "con_defs" |-- Parse.!!! Parse_Spec.xthms1) [] -- |
588 Scan.optional (@{keyword "con_defs"} |-- Parse.!!! Parse_Spec.xthms1) [] -- |
589 Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] -- |
589 Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] -- |
590 Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) [] |
590 Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) [] |
591 >> (Toplevel.theory o mk_ind); |
591 >> (Toplevel.theory o mk_ind); |
592 |
592 |
593 val _ = |
593 val _ = |
594 Outer_Syntax.command (co_prefix ^ "inductive") |
594 Outer_Syntax.command (co_prefix ^ "inductive") |
595 ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl; |
595 ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl; |