doc-src/IsarRef/Thy/document/HOL_Specific.tex
changeset 46448 f1201fac7398
parent 46447 f37da60a8cc6
child 46457 915af80f74b3
     1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 10 09:02:51 2012 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Fri Feb 10 09:47:59 2012 +0100
     1.3 @@ -1789,6 +1789,7 @@
     1.4      \indexdef{HOL}{method}{regularize}\hypertarget{method.HOL.regularize}{\hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}}} & : & \isa{method} \\
     1.5      \indexdef{HOL}{method}{injection}\hypertarget{method.HOL.injection}{\hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}} & : & \isa{method} \\
     1.6      \indexdef{HOL}{method}{cleaning}\hypertarget{method.HOL.cleaning}{\hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}}} & : & \isa{method} \\
     1.7 +    \indexdef{HOL}{attribute}{quot\_thm}\hypertarget{attribute.HOL.quot-thm}{\hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}}} & : & \isa{attribute} \\
     1.8      \indexdef{HOL}{attribute}{quot\_lifted}\hypertarget{attribute.HOL.quot-lifted}{\hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}}} & : & \isa{attribute} \\
     1.9      \indexdef{HOL}{attribute}{quot\_respect}\hypertarget{attribute.HOL.quot-respect}{\hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}}} & : & \isa{attribute} \\
    1.10      \indexdef{HOL}{attribute}{quot\_preserve}\hypertarget{attribute.HOL.quot-preserve}{\hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}}} & : & \isa{attribute} \\
    1.11 @@ -1941,6 +1942,16 @@
    1.12      local theory store and used by the \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}
    1.13      and \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} methods respectively.
    1.14  
    1.15 +  \item \hyperlink{attribute.HOL.quot-thm}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}thm}}} declares that a certain theorem
    1.16 +    is a quotient extension theorem. Quotient extension theorems
    1.17 +    allow for quotienting inside container types. Given a polymorphic
    1.18 +    type that serves as a container, a map function defined for this
    1.19 +    container  using \hyperlink{command.HOL.enriched-type}{\mbox{\isa{\isacommand{enriched{\isaliteral{5F}{\isacharunderscore}}type}}}} and a relation
    1.20 +    map defined for for the container type, the quotient extension
    1.21 +    theorem should be \isa{{\isaliteral{22}{\isachardoublequote}}Quotient\ R\ Abs\ Rep\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Quotient\ {\isaliteral{28}{\isacharparenleft}}rel{\isaliteral{5F}{\isacharunderscore}}map\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Abs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}map\ Rep{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}}. Quotient extension theorems
    1.22 +    are stored in a database and are used all the steps of lifting
    1.23 +    theorems.
    1.24 +
    1.25    \end{description}%
    1.26  \end{isamarkuptext}%
    1.27  \isamarkuptrue%