1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Jul 27 19:35:00 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Wed Jul 27 20:28:00 2011 +0200
1.3 @@ -1236,6 +1236,52 @@
1.4 \end{description}
1.5 *}
1.6
1.7 +section {* Quotient types *}
1.8 +
1.9 +text {*
1.10 + The quotient package defines a new quotient type given a raw type
1.11 + and a partial equivalence relation.
1.12 + It also includes automation for transporting definitions and theorems.
1.13 + It can automatically produce definitions and theorems on the quotient type,
1.14 + given the corresponding constants and facts on the raw type.
1.15 +
1.16 + \begin{matharray}{rcl}
1.17 + @{command_def (HOL) "quotient_type"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
1.18 + @{command_def (HOL) "quotient_definition"} & : & @{text "local_theory \<rightarrow> proof(prove)"}\\
1.19 + @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
1.20 + @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
1.21 + @{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
1.22 + \end{matharray}
1.23 +
1.24 + @{rail "
1.25 + @@{command (HOL) quotient_type} (spec + @'and');
1.26 +
1.27 + spec: @{syntax typespec} @{syntax mixfix}? '=' \\
1.28 + @{syntax type} '/' ('partial' ':')? @{syntax term};
1.29 + "}
1.30 +
1.31 + @{rail "
1.32 + @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\
1.33 + @{syntax term} 'is' @{syntax term};
1.34 +
1.35 + constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
1.36 + "}
1.37 +
1.38 + \begin{description}
1.39 +
1.40 + \item @{command (HOL) "quotient_type"} defines quotient types.
1.41 +
1.42 + \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type.
1.43 +
1.44 + \item @{command (HOL) "print_quotmaps"} prints quotient map functions.
1.45 +
1.46 + \item @{command (HOL) "print_quotients"} prints quotients.
1.47 +
1.48 + \item @{command (HOL) "print_quotconsts"} prints quotient constants.
1.49 +
1.50 + \end{description}
1.51 +
1.52 +*}
1.53
1.54 section {* Arithmetic proof support *}
1.55
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Jul 27 19:35:00 2011 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Wed Jul 27 20:28:00 2011 +0200
2.3 @@ -1754,6 +1754,101 @@
2.4 \end{isamarkuptext}%
2.5 \isamarkuptrue%
2.6 %
2.7 +\isamarkupsection{Quotient types%
2.8 +}
2.9 +\isamarkuptrue%
2.10 +%
2.11 +\begin{isamarkuptext}%
2.12 +The quotient package defines a new quotient type given a raw type
2.13 + and a partial equivalence relation.
2.14 + It also includes automation for transporting definitions and theorems.
2.15 + It can automatically produce definitions and theorems on the quotient type,
2.16 + given the corresponding constants and facts on the raw type.
2.17 +
2.18 + \begin{matharray}{rcl}
2.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}}}\\
2.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}}}\\
2.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}}}\\
2.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}}}\\
2.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}}}\\
2.24 + \end{matharray}
2.25 +
2.26 + \begin{railoutput}
2.27 +\rail@begin{2}{}
2.28 +\rail@term{\hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}}}[]
2.29 +\rail@plus
2.30 +\rail@nont{\isa{spec}}[]
2.31 +\rail@nextplus{1}
2.32 +\rail@cterm{\isa{\isakeyword{and}}}[]
2.33 +\rail@endplus
2.34 +\rail@end
2.35 +\rail@begin{5}{\isa{spec}}
2.36 +\rail@nont{\hyperlink{syntax.typespec}{\mbox{\isa{typespec}}}}[]
2.37 +\rail@bar
2.38 +\rail@nextbar{1}
2.39 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
2.40 +\rail@endbar
2.41 +\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
2.42 +\rail@cr{3}
2.43 +\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
2.44 +\rail@term{\isa{{\isaliteral{2F}{\isacharslash}}}}[]
2.45 +\rail@bar
2.46 +\rail@nextbar{4}
2.47 +\rail@term{\isa{partial}}[]
2.48 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
2.49 +\rail@endbar
2.50 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2.51 +\rail@end
2.52 +\end{railoutput}
2.53 +
2.54 +
2.55 + \begin{railoutput}
2.56 +\rail@begin{4}{}
2.57 +\rail@term{\hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}}}[]
2.58 +\rail@bar
2.59 +\rail@nextbar{1}
2.60 +\rail@nont{\isa{constdecl}}[]
2.61 +\rail@endbar
2.62 +\rail@bar
2.63 +\rail@nextbar{1}
2.64 +\rail@nont{\hyperlink{syntax.thmdecl}{\mbox{\isa{thmdecl}}}}[]
2.65 +\rail@endbar
2.66 +\rail@cr{3}
2.67 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2.68 +\rail@term{\isa{is}}[]
2.69 +\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2.70 +\rail@end
2.71 +\rail@begin{2}{\isa{constdecl}}
2.72 +\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
2.73 +\rail@bar
2.74 +\rail@nextbar{1}
2.75 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
2.76 +\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
2.77 +\rail@endbar
2.78 +\rail@bar
2.79 +\rail@nextbar{1}
2.80 +\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
2.81 +\rail@endbar
2.82 +\rail@end
2.83 +\end{railoutput}
2.84 +
2.85 +
2.86 + \begin{description}
2.87 +
2.88 + \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types.
2.89 +
2.90 + \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type.
2.91 +
2.92 + \item \hyperlink{command.HOL.print-quotmaps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotmaps}}}} prints quotient map functions.
2.93 +
2.94 + \item \hyperlink{command.HOL.print-quotients}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotients}}}} prints quotients.
2.95 +
2.96 + \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants.
2.97 +
2.98 + \end{description}%
2.99 +\end{isamarkuptext}%
2.100 +\isamarkuptrue%
2.101 +%
2.102 \isamarkupsection{Arithmetic proof support%
2.103 }
2.104 \isamarkuptrue%