1747 |
1747 |
1748 \noindent where \isa{t} is the type constructor, \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are distinct |
1748 \noindent where \isa{t} is the type constructor, \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}} are distinct |
1749 type variables free in the local theory and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, |
1749 type variables free in the local theory and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, |
1750 \ldots, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{22}{\isachardoublequote}}} is a subsequence of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \ldots, |
1750 \ldots, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C7369676D613E}{\isasymsigma}}\isaliteral{5C3C5E697375623E}{}\isactrlisub k{\isaliteral{22}{\isachardoublequote}}} is a subsequence of \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \ldots, |
1751 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}. |
1751 \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C626574613E}{\isasymbeta}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{5C3C616C7068613E}{\isasymalpha}}\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}. |
|
1752 |
|
1753 \end{description}% |
|
1754 \end{isamarkuptext}% |
|
1755 \isamarkuptrue% |
|
1756 % |
|
1757 \isamarkupsection{Quotient types% |
|
1758 } |
|
1759 \isamarkuptrue% |
|
1760 % |
|
1761 \begin{isamarkuptext}% |
|
1762 The quotient package defines a new quotient type given a raw type |
|
1763 and a partial equivalence relation. |
|
1764 It also includes automation for transporting definitions and theorems. |
|
1765 It can automatically produce definitions and theorems on the quotient type, |
|
1766 given the corresponding constants and facts on the raw type. |
|
1767 |
|
1768 \begin{matharray}{rcl} |
|
1769 \indexdef{HOL}{command}{quotient\_type}\hypertarget{command.HOL.quotient-type}{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ |
|
1770 \indexdef{HOL}{command}{quotient\_definition}\hypertarget{command.HOL.quotient-definition}{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}local{\isaliteral{5F}{\isacharunderscore}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}\\ |
|
1771 \indexdef{HOL}{command}{print\_quotmaps}\hypertarget{command.HOL.print-quotmaps}{\hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
|
1772 \indexdef{HOL}{command}{print\_quotients}\hypertarget{command.HOL.print-quotients}{\hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
|
1773 \indexdef{HOL}{command}{print\_quotconsts}\hypertarget{command.HOL.print-quotconsts}{\hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}}\\ |
|
1774 \end{matharray} |
|
1775 |
|
1776 \begin{railoutput} |
|
1777 \rail@begin{2}{} |
|
1778 \rail@term{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}}[] |
|
1779 \rail@plus |
|
1780 \rail@nont{\isa{spec}}[] |
|
1781 \rail@nextplus{1} |
|
1782 \rail@cterm{\isa{\isakeyword{and}}}[] |
|
1783 \rail@endplus |
|
1784 \rail@end |
|
1785 \rail@begin{5}{\isa{spec}} |
|
1786 \rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[] |
|
1787 \rail@bar |
|
1788 \rail@nextbar{1} |
|
1789 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[] |
|
1790 \rail@endbar |
|
1791 \rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[] |
|
1792 \rail@cr{3} |
|
1793 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[] |
|
1794 \rail@term{\isa{{\isaliteral{2F}{\isacharslash}}}}[] |
|
1795 \rail@bar |
|
1796 \rail@nextbar{4} |
|
1797 \rail@term{\isa{partial}}[] |
|
1798 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[] |
|
1799 \rail@endbar |
|
1800 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
|
1801 \rail@end |
|
1802 \end{railoutput} |
|
1803 |
|
1804 |
|
1805 \begin{railoutput} |
|
1806 \rail@begin{4}{} |
|
1807 \rail@term{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}}[] |
|
1808 \rail@bar |
|
1809 \rail@nextbar{1} |
|
1810 \rail@nont{\isa{constdecl}}[] |
|
1811 \rail@endbar |
|
1812 \rail@bar |
|
1813 \rail@nextbar{1} |
|
1814 \rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[] |
|
1815 \rail@endbar |
|
1816 \rail@cr{3} |
|
1817 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
|
1818 \rail@term{\isa{is}}[] |
|
1819 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[] |
|
1820 \rail@end |
|
1821 \rail@begin{2}{\isa{constdecl}} |
|
1822 \rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[] |
|
1823 \rail@bar |
|
1824 \rail@nextbar{1} |
|
1825 \rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[] |
|
1826 \rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[] |
|
1827 \rail@endbar |
|
1828 \rail@bar |
|
1829 \rail@nextbar{1} |
|
1830 \rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[] |
|
1831 \rail@endbar |
|
1832 \rail@end |
|
1833 \end{railoutput} |
|
1834 |
|
1835 |
|
1836 \begin{description} |
|
1837 |
|
1838 \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. |
|
1839 |
|
1840 \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type. |
|
1841 |
|
1842 \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map functions. |
|
1843 |
|
1844 \item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints quotients. |
|
1845 |
|
1846 \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants. |
1752 |
1847 |
1753 \end{description}% |
1848 \end{description}% |
1754 \end{isamarkuptext}% |
1849 \end{isamarkuptext}% |
1755 \isamarkuptrue% |
1850 \isamarkuptrue% |
1756 % |
1851 % |