rudimentary documentation of the quotient package in the isar reference manual
authorbulwahn
Wed, 27 Jul 2011 20:28:00 +0200
changeset 44864b141d7a3d4e3
parent 44863 c38c65a1bf9c
child 44865 5de4bde3ad41
rudimentary documentation of the quotient package in the isar reference manual
doc-src/IsarRef/Thy/HOL_Specific.thy
doc-src/IsarRef/Thy/document/HOL_Specific.tex
     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%