1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Jul 27 19:35:00 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Jul 27 20:28:00 2011 +0200
1.3 @@ -1754,6 +1754,101 @@
1.4 \end{isamarkuptext}%
1.5 \isamarkuptrue%
1.6 %
1.7 +\isamarkupsection{Quotient types%
1.8 +}
1.9 +\isamarkuptrue%
1.10 +%
1.11 +\begin{isamarkuptext}%
1.12 +The quotient package defines a new quotient type given a raw type
1.13 + and a partial equivalence relation.
1.14 + It also includes automation for transporting definitions and theorems.
1.15 + It can automatically produce definitions and theorems on the quotient type,
1.16 + given the corresponding constants and facts on the raw type.
1.17 +
1.18 + \begin{matharray}{rcl}
1.19 + \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}}}\\
1.20 + \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}}}\\
1.21 + \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}}}\\
1.22 + \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}}}\\
1.23 + \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}}}\\
1.24 + \end{matharray}
1.25 +
1.26 + \begin{railoutput}
1.27 +\rail@begin{2}{}
1.28 +\rail@term{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
1.29 +\rail@plus
1.30 +\rail@nont{\isa{spec}}[]
1.31 +\rail@nextplus{1}
1.32 +\rail@cterm{\isa{\isakeyword{and}}}[]
1.33 +\rail@endplus
1.34 +\rail@end
1.35 +\rail@begin{5}{\isa{spec}}
1.36 +\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
1.37 +\rail@bar
1.38 +\rail@nextbar{1}
1.39 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.40 +\rail@endbar
1.41 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
1.42 +\rail@cr{3}
1.43 +\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.44 +\rail@term{\isa{{\isaliteral{2F}{\isacharslash}}}}[]
1.45 +\rail@bar
1.46 +\rail@nextbar{4}
1.47 +\rail@term{\isa{partial}}[]
1.48 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
1.49 +\rail@endbar
1.50 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.51 +\rail@end
1.52 +\end{railoutput}
1.53 +
1.54 +
1.55 + \begin{railoutput}
1.56 +\rail@begin{4}{}
1.57 +\rail@term{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}}[]
1.58 +\rail@bar
1.59 +\rail@nextbar{1}
1.60 +\rail@nont{\isa{constdecl}}[]
1.61 +\rail@endbar
1.62 +\rail@bar
1.63 +\rail@nextbar{1}
1.64 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
1.65 +\rail@endbar
1.66 +\rail@cr{3}
1.67 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.68 +\rail@term{\isa{is}}[]
1.69 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
1.70 +\rail@end
1.71 +\rail@begin{2}{\isa{constdecl}}
1.72 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
1.73 +\rail@bar
1.74 +\rail@nextbar{1}
1.75 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
1.76 +\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
1.77 +\rail@endbar
1.78 +\rail@bar
1.79 +\rail@nextbar{1}
1.80 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
1.81 +\rail@endbar
1.82 +\rail@end
1.83 +\end{railoutput}
1.84 +
1.85 +
1.86 + \begin{description}
1.87 +
1.88 + \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types.
1.89 +
1.90 + \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type.
1.91 +
1.92 + \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map functions.
1.93 +
1.94 + \item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints quotients.
1.95 +
1.96 + \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants.
1.97 +
1.98 + \end{description}%
1.99 +\end{isamarkuptext}%
1.100 +\isamarkuptrue%
1.101 +%
1.102 \isamarkupsection{Arithmetic proof support%
1.103 }
1.104 \isamarkuptrue%