1.1 --- a/doc-src/IsarRef/Thy/HOL_Specific.thy Thu Feb 09 16:00:04 2012 +0100
1.2 +++ b/doc-src/IsarRef/Thy/HOL_Specific.thy Fri Feb 10 09:02:51 2012 +0100
1.3 @@ -1263,6 +1263,18 @@
1.4 @{command_def (HOL) "print_quotmaps"} & : & @{text "context \<rightarrow>"}\\
1.5 @{command_def (HOL) "print_quotients"} & : & @{text "context \<rightarrow>"}\\
1.6 @{command_def (HOL) "print_quotconsts"} & : & @{text "context \<rightarrow>"}\\
1.7 + @{method_def (HOL) "lifting"} & : & @{text method} \\
1.8 + @{method_def (HOL) "lifting_setup"} & : & @{text method} \\
1.9 + @{method_def (HOL) "descending"} & : & @{text method} \\
1.10 + @{method_def (HOL) "descending_setup"} & : & @{text method} \\
1.11 + @{method_def (HOL) "partiality_descending"} & : & @{text method} \\
1.12 + @{method_def (HOL) "partiality_descending_setup"} & : & @{text method} \\
1.13 + @{method_def (HOL) "regularize"} & : & @{text method} \\
1.14 + @{method_def (HOL) "injection"} & : & @{text method} \\
1.15 + @{method_def (HOL) "cleaning"} & : & @{text method} \\
1.16 + @{attribute_def (HOL) "quot_lifted"} & : & @{text attribute} \\
1.17 + @{attribute_def (HOL) "quot_respect"} & : & @{text attribute} \\
1.18 + @{attribute_def (HOL) "quot_preserve"} & : & @{text attribute} \\
1.19 \end{matharray}
1.20
1.21 @{rail "
1.22 @@ -1276,15 +1288,27 @@
1.23 @{rail "
1.24 @@{command (HOL) quotient_definition} constdecl? @{syntax thmdecl}? \\
1.25 @{syntax term} 'is' @{syntax term};
1.26 -
1.27 +
1.28 constdecl: @{syntax name} ('::' @{syntax type})? @{syntax mixfix}?
1.29 "}
1.30
1.31 + @{rail "
1.32 + @@{method (HOL) lifting} @{syntax thmrefs}?
1.33 + ;
1.34 +
1.35 + @@{method (HOL) lifting_setup} @{syntax thmrefs}?
1.36 + ;
1.37 + "}
1.38 +
1.39 \begin{description}
1.40 -
1.41 +
1.42 \item @{command (HOL) "quotient_type"} defines quotient types. The injection from a quotient type
1.43 to a raw type is called @{text rep_t}, its inverse @{text abs_t} unless explicit @{keyword (HOL)
1.44 - "morphisms"} specification provides alternative names.
1.45 + "morphisms"} specification provides alternative names. @{command (HOL) "quotient_type"} requires
1.46 + the user to prove that the relation is an equivalence relation (predicate @{text equivp}), unless
1.47 + the user specifies explicitely @{text partial} in which case the obligation is @{text part_equivp}.
1.48 + A quotient defined with @{text partial} is weaker in the sense that less things can be proved
1.49 + automatically.
1.50
1.51 \item @{command (HOL) "quotient_definition"} defines a constant on the quotient type.
1.52
1.53 @@ -1294,6 +1318,54 @@
1.54
1.55 \item @{command (HOL) "print_quotconsts"} prints quotient constants.
1.56
1.57 + \item @{method (HOL) "lifting"} and @{method (HOL) "lifting_setup"}
1.58 + methods match the current goal with the given raw theorem to be
1.59 + lifted producing three new subgoals: regularization, injection and
1.60 + cleaning subgoals. @{method (HOL) "lifting"} tries to apply the
1.61 + heuristics for automatically solving these three subgoals and
1.62 + leaves only the subgoals unsolved by the heuristics to the user as
1.63 + opposed to @{method (HOL) "lifting_setup"} which leaves the three
1.64 + subgoals unsolved.
1.65 +
1.66 + \item @{method (HOL) "descending"} and @{method (HOL)
1.67 + "descending_setup"} try to guess a raw statement that would lift
1.68 + to the current subgoal. Such statement is assumed as a new subgoal
1.69 + and @{method (HOL) "descending"} continues in the same way as
1.70 + @{method (HOL) "lifting"} does. @{method (HOL) "descending"} tries
1.71 + to solve the arising regularization, injection and cleaning
1.72 + subgoals with the analoguous method @{method (HOL)
1.73 + "descending_setup"} which leaves the four unsolved subgoals.
1.74 +
1.75 + \item @{method (HOL) "partiality_descending"} finds the regularized
1.76 + theorem that would lift to the current subgoal, lifts it and
1.77 + leaves as a subgoal. This method can be used with partial
1.78 + equivalence quotients where the non regularized statements would
1.79 + not be true. @{method (HOL) "partiality_descending_setup"} leaves
1.80 + the injection and cleaning subgoals unchanged.
1.81 +
1.82 + \item @{method (HOL) "regularize"} applies the regularization
1.83 + heuristics to the current subgoal.
1.84 +
1.85 + \item @{method (HOL) "injection"} applies the injection heuristics
1.86 + to the current goal using the stored quotient respectfulness
1.87 + theorems.
1.88 +
1.89 + \item @{method (HOL) "cleaning"} applies the injection cleaning
1.90 + heuristics to the current subgoal using the stored quotient
1.91 + preservation theorems.
1.92 +
1.93 + \item @{attribute (HOL) quot_lifted} attribute tries to
1.94 + automatically transport the theorem to the quotient type.
1.95 + The attribute uses all the defined quotients types and quotient
1.96 + constants often producing undesired results or theorems that
1.97 + cannot be lifted.
1.98 +
1.99 + \item @{attribute (HOL) quot_respect} and @{attribute (HOL)
1.100 + quot_preserve} attributes declare a theorem as a respectfulness
1.101 + and preservation theorem respectively. These are stored in the
1.102 + local theory store and used by the @{method (HOL) "injection"}
1.103 + and @{method (HOL) "cleaning"} methods respectively.
1.104 +
1.105 \end{description}
1.106
1.107 *}
2.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Thu Feb 09 16:00:04 2012 +0100
2.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Fri Feb 10 09:02:51 2012 +0100
2.3 @@ -1780,6 +1780,18 @@
2.4 \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.5 \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.6 \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.7 + \indexdef{HOL}{method}{lifting}\hypertarget{method.HOL.lifting}{\hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}}} & : & \isa{method} \\
2.8 + \indexdef{HOL}{method}{lifting\_setup}\hypertarget{method.HOL.lifting-setup}{\hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\
2.9 + \indexdef{HOL}{method}{descending}\hypertarget{method.HOL.descending}{\hyperlink{method.HOL.descending}{\mbox{\isa{descending}}}} & : & \isa{method} \\
2.10 + \indexdef{HOL}{method}{descending\_setup}\hypertarget{method.HOL.descending-setup}{\hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\
2.11 + \indexdef{HOL}{method}{partiality\_descending}\hypertarget{method.HOL.partiality-descending}{\hyperlink{method.HOL.partiality-descending}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending}}}} & : & \isa{method} \\
2.12 + \indexdef{HOL}{method}{partiality\_descending\_setup}\hypertarget{method.HOL.partiality-descending-setup}{\hyperlink{method.HOL.partiality-descending-setup}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending{\isaliteral{5F}{\isacharunderscore}}setup}}}} & : & \isa{method} \\
2.13 + \indexdef{HOL}{method}{regularize}\hypertarget{method.HOL.regularize}{\hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}}} & : & \isa{method} \\
2.14 + \indexdef{HOL}{method}{injection}\hypertarget{method.HOL.injection}{\hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}} & : & \isa{method} \\
2.15 + \indexdef{HOL}{method}{cleaning}\hypertarget{method.HOL.cleaning}{\hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}}} & : & \isa{method} \\
2.16 + \indexdef{HOL}{attribute}{quot\_lifted}\hypertarget{attribute.HOL.quot-lifted}{\hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}}} & : & \isa{attribute} \\
2.17 + \indexdef{HOL}{attribute}{quot\_respect}\hypertarget{attribute.HOL.quot-respect}{\hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}}} & : & \isa{attribute} \\
2.18 + \indexdef{HOL}{attribute}{quot\_preserve}\hypertarget{attribute.HOL.quot-preserve}{\hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}}} & : & \isa{attribute} \\
2.19 \end{matharray}
2.20
2.21 \begin{railoutput}
2.22 @@ -1849,10 +1861,32 @@
2.23 \end{railoutput}
2.24
2.25
2.26 + \begin{railoutput}
2.27 +\rail@begin{2}{}
2.28 +\rail@term{\hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}}}[]
2.29 +\rail@bar
2.30 +\rail@nextbar{1}
2.31 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
2.32 +\rail@endbar
2.33 +\rail@end
2.34 +\rail@begin{2}{}
2.35 +\rail@term{\hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}}[]
2.36 +\rail@bar
2.37 +\rail@nextbar{1}
2.38 +\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
2.39 +\rail@endbar
2.40 +\rail@end
2.41 +\end{railoutput}
2.42 +
2.43 +
2.44 \begin{description}
2.45 -
2.46 +
2.47 \item \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} defines quotient types. The injection from a quotient type
2.48 - to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names.
2.49 + to a raw type is called \isa{rep{\isaliteral{5F}{\isacharunderscore}}t}, its inverse \isa{abs{\isaliteral{5F}{\isacharunderscore}}t} unless explicit \hyperlink{keyword.HOL.morphisms}{\mbox{\isa{\isakeyword{morphisms}}}} specification provides alternative names. \hyperlink{command.HOL.quotient-type}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}type}}}} requires
2.50 + the user to prove that the relation is an equivalence relation (predicate \isa{equivp}), unless
2.51 + the user specifies explicitely \isa{partial} in which case the obligation is \isa{part{\isaliteral{5F}{\isacharunderscore}}equivp}.
2.52 + A quotient defined with \isa{partial} is weaker in the sense that less things can be proved
2.53 + automatically.
2.54
2.55 \item \hyperlink{command.HOL.quotient-definition}{\mbox{\isa{\isacommand{quotient{\isaliteral{5F}{\isacharunderscore}}definition}}}} defines a constant on the quotient type.
2.56
2.57 @@ -1862,6 +1896,51 @@
2.58
2.59 \item \hyperlink{command.HOL.print-quotconsts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}quotconsts}}}} prints quotient constants.
2.60
2.61 + \item \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} and \hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}}
2.62 + methods match the current goal with the given raw theorem to be
2.63 + lifted producing three new subgoals: regularization, injection and
2.64 + cleaning subgoals. \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} tries to apply the
2.65 + heuristics for automatically solving these three subgoals and
2.66 + leaves only the subgoals unsolved by the heuristics to the user as
2.67 + opposed to \hyperlink{method.HOL.lifting-setup}{\mbox{\isa{lifting{\isaliteral{5F}{\isacharunderscore}}setup}}} which leaves the three
2.68 + subgoals unsolved.
2.69 +
2.70 + \item \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} and \hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}} try to guess a raw statement that would lift
2.71 + to the current subgoal. Such statement is assumed as a new subgoal
2.72 + and \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} continues in the same way as
2.73 + \hyperlink{method.HOL.lifting}{\mbox{\isa{lifting}}} does. \hyperlink{method.HOL.descending}{\mbox{\isa{descending}}} tries
2.74 + to solve the arising regularization, injection and cleaning
2.75 + subgoals with the analoguous method \hyperlink{method.HOL.descending-setup}{\mbox{\isa{descending{\isaliteral{5F}{\isacharunderscore}}setup}}} which leaves the four unsolved subgoals.
2.76 +
2.77 + \item \hyperlink{method.HOL.partiality-descending}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending}}} finds the regularized
2.78 + theorem that would lift to the current subgoal, lifts it and
2.79 + leaves as a subgoal. This method can be used with partial
2.80 + equivalence quotients where the non regularized statements would
2.81 + not be true. \hyperlink{method.HOL.partiality-descending-setup}{\mbox{\isa{partiality{\isaliteral{5F}{\isacharunderscore}}descending{\isaliteral{5F}{\isacharunderscore}}setup}}} leaves
2.82 + the injection and cleaning subgoals unchanged.
2.83 +
2.84 + \item \hyperlink{method.HOL.regularize}{\mbox{\isa{regularize}}} applies the regularization
2.85 + heuristics to the current subgoal.
2.86 +
2.87 + \item \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}} applies the injection heuristics
2.88 + to the current goal using the stored quotient respectfulness
2.89 + theorems.
2.90 +
2.91 + \item \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} applies the injection cleaning
2.92 + heuristics to the current subgoal using the stored quotient
2.93 + preservation theorems.
2.94 +
2.95 + \item \hyperlink{attribute.HOL.quot-lifted}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}lifted}}} attribute tries to
2.96 + automatically transport the theorem to the quotient type.
2.97 + The attribute uses all the defined quotients types and quotient
2.98 + constants often producing undesired results or theorems that
2.99 + cannot be lifted.
2.100 +
2.101 + \item \hyperlink{attribute.HOL.quot-respect}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}respect}}} and \hyperlink{attribute.HOL.quot-preserve}{\mbox{\isa{quot{\isaliteral{5F}{\isacharunderscore}}preserve}}} attributes declare a theorem as a respectfulness
2.102 + and preservation theorem respectively. These are stored in the
2.103 + local theory store and used by the \hyperlink{method.HOL.injection}{\mbox{\isa{injection}}}
2.104 + and \hyperlink{method.HOL.cleaning}{\mbox{\isa{cleaning}}} methods respectively.
2.105 +
2.106 \end{description}%
2.107 \end{isamarkuptext}%
2.108 \isamarkuptrue%