501 \begin{railoutput} |
501 \begin{railoutput} |
502 \rail@begin{2}{\isa{}} |
502 \rail@begin{2}{\isa{}} |
503 \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[] |
503 \rail@term{\hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}}[] |
504 \rail@bar |
504 \rail@bar |
505 \rail@nextbar{1} |
505 \rail@nextbar{1} |
506 \rail@nont{\isa{prefix}}[] |
506 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
507 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[] |
507 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[] |
508 \rail@endbar |
508 \rail@endbar |
509 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
509 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
510 \rail@end |
510 \rail@end |
511 \end{railoutput} |
511 \end{railoutput} |
512 % FIXME check prefix |
512 |
513 |
513 |
514 \begin{description} |
514 \begin{description} |
515 |
515 |
516 \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} allows to prove and register |
516 \item \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}prefix{\isaliteral{3A}{\isacharcolon}}\ m{\isaliteral{22}{\isachardoublequote}}} allows to |
517 properties about the functorial structure of type constructors; |
517 prove and register properties about the functorial structure of type |
518 these properties then can be used by other packages to |
518 constructors. These properties then can be used by other packages |
519 deal with those type constructors in certain type constructions. |
519 to deal with those type constructors in certain type constructions. |
520 Characteristic theorems are noted in the current local theory; by |
520 Characteristic theorems are noted in the current local theory. By |
521 default, they are prefixed with the base name of the type constructor, |
521 default, they are prefixed with the base name of the type |
522 an explicit prefix can be given alternatively. |
522 constructor, an explicit prefix can be given alternatively. |
523 |
523 |
524 The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the |
524 The given term \isa{{\isaliteral{22}{\isachardoublequote}}m{\isaliteral{22}{\isachardoublequote}}} is considered as \emph{mapper} for the |
525 corresponding type constructor and must conform to the following |
525 corresponding type constructor and must conform to the following |
526 type pattern: |
526 type pattern: |
527 |
527 |
786 \rail@bar |
786 \rail@bar |
787 \rail@nextbar{1} |
787 \rail@nextbar{1} |
788 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[] |
788 \rail@nont{\hyperlink{syntax.target}{\mbox{\isa{target}}}}[] |
789 \rail@endbar |
789 \rail@endbar |
790 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
790 \rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[] |
791 \rail@nont{\isa{mode}}[] |
791 \rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[] |
792 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
792 \rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[] |
793 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[] |
793 \rail@nont{\hyperlink{syntax.fixes}{\mbox{\isa{fixes}}}}[] |
794 \rail@cr{3} |
794 \rail@cr{3} |
795 \rail@term{\isa{\isakeyword{where}}}[] |
795 \rail@term{\isa{\isakeyword{where}}}[] |
796 \rail@bar |
796 \rail@bar |
798 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[] |
798 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[] |
799 \rail@endbar |
799 \rail@endbar |
800 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] |
800 \rail@nont{\hyperlink{syntax.prop}{\mbox{\isa{prop}}}}[] |
801 \rail@end |
801 \rail@end |
802 \end{railoutput} |
802 \end{railoutput} |
803 % FIXME check mode |
803 |
804 |
804 |
805 \begin{description} |
805 \begin{description} |
806 |
806 |
807 \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}} defines recursive |
807 \item \hyperlink{command.HOL.partial-function}{\mbox{\isa{\isacommand{partial{\isaliteral{5F}{\isacharunderscore}}function}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}mode{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} defines |
808 functions based on fixpoints in complete partial orders. No |
808 recursive functions based on fixpoints in complete partial |
809 termination proof is required from the user or constructed |
809 orders. No termination proof is required from the user or |
810 internally. Instead, the possibility of non-termination is modelled |
810 constructed internally. Instead, the possibility of non-termination |
811 explicitly in the result type, which contains an explicit bottom |
811 is modelled explicitly in the result type, which contains an |
812 element. |
812 explicit bottom element. |
813 |
813 |
814 Pattern matching and mutual recursion are currently not supported. |
814 Pattern matching and mutual recursion are currently not supported. |
815 Thus, the specification consists of a single function described by a |
815 Thus, the specification consists of a single function described by a |
816 single recursive equation. |
816 single recursive equation. |
817 |
817 |