# HG changeset patch # User ballarin # Date 1294344377 -3600 # Node ID 710cdb9e0d17024a78019b3f252f7b64366ae185 # Parent 1b8ff770f02cfd50f886035a62f2289c125692c8 Documentation for 'interpret' and 'sublocale' with mixins. diff -r 1b8ff770f02c -r 710cdb9e0d17 NEWS --- a/NEWS Thu Jan 06 21:06:17 2011 +0100 +++ b/NEWS Thu Jan 06 21:06:17 2011 +0100 @@ -123,6 +123,11 @@ * Document antiquotation @{file} checks file/directory entries within the local file system. +* Locale interpretation commands 'interpret' and 'sublocale' accept +equations to map definitions in a locale to appropriate entities in +the context of the interpretation. The 'interpretation' command +already provided this functionality. + *** HOL *** @@ -502,8 +507,12 @@ * Theorems for additive ring operations (locale abelian_monoid and descendants) are generated by interpretation from their multiplicative -counterparts. This causes slight differences in the simp and clasets. -INCOMPATIBILITY. +counterparts. Names (in particular theorem names) have the mandatory +qualifier 'add'. Previous theorem names are redeclared for +compatibility. + +* Structure 'int_ring' is now an abbreviation (previously a +definition). This fits more natural with advanced interpretations. *** HOLCF *** diff -r 1b8ff770f02c -r 710cdb9e0d17 doc-src/IsarRef/Thy/Spec.thy --- a/doc-src/IsarRef/Thy/Spec.thy Thu Jan 06 21:06:17 2011 +0100 +++ b/doc-src/IsarRef/Thy/Spec.thy Thu Jan 06 21:06:17 2011 +0100 @@ -494,51 +494,28 @@ also within a proof body (command @{command "interpret"}). \begin{matharray}{rcl} - @{command_def "sublocale"} & : & @{text "theory \ proof(prove)"} \\ @{command_def "interpretation"} & : & @{text "theory \ proof(prove)"} \\ @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \ proof(prove)"} \\ + @{command_def "sublocale"} & : & @{text "theory \ proof(prove)"} \\ @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \"} \\ \end{matharray} \indexouternonterm{interp} \begin{rail} - 'sublocale' nameref ('<' | subseteq) localeexpr - ; - 'interpretation' localeepxr equations? + 'interpretation' localeexpr equations? ; 'interpret' localeexpr equations? ; - 'print_interps' nameref + 'sublocale' nameref ('<' | subseteq) localeexpr equations? ; equations: 'where' (thmdecl? prop + 'and') ; + 'print_interps' nameref + ; \end{rail} \begin{description} - \item @{command "sublocale"}~@{text "name \ expr"} - interprets @{text expr} in the locale @{text name}. A proof that - the specification of @{text name} implies the specification of - @{text expr} is required. As in the localized version of the - theorem command, the proof is in the context of @{text name}. After - the proof obligation has been dischared, the facts of @{text expr} - become part of locale @{text name} as \emph{derived} context - elements and are available when the context @{text name} is - subsequently entered. Note that, like import, this is dynamic: - facts added to a locale part of @{text expr} after interpretation - become also available in @{text name}. - - Only specification fragments of @{text expr} that are not already - part of @{text name} (be it imported, derived or a derived fragment - of the import) are considered in this process. This enables - circular interpretations to the extent that no infinite chains are - generated in the locale hierarchy. - - If interpretations of @{text name} exist in the current theory, the - command adds interpretations for @{text expr} as well, with the same - qualifier, although only for fragments of @{text expr} that are not - interpreted in the theory already. - \item @{command "interpretation"}~@{text "expr \ eqns"} interprets @{text expr} in the theory. The command generates proof obligations for the instantiated specifications (assumes and defines @@ -548,7 +525,7 @@ Additional equations, which are unfolded during post-processing, may be given after the keyword @{keyword "where"}. This is useful for interpreting concepts introduced through - definition specification elements. The equations must be proved. + definitions. The equations must be proved. The command is aware of interpretations already active in the theory, but does not simplify the goal automatically. In order to @@ -561,14 +538,47 @@ parts. Adding facts to locales has the effect of adding interpreted facts - to the theory for all active interpretations also. That is, + to the theory for all interpretations as well. That is, interpretations dynamically participate in any facts added to - locales. + locales. Note that if a theory inherits additional facts for a + locale through one parent and an interpretation of that locale + through another parent, the additional facts will not be + interpreted. \item @{command "interpret"}~@{text "expr \ eqns"} interprets @{text expr} in the proof context and is otherwise similar to interpretation in theories. Note that rewrite rules given to - @{command "interpret"} should be explicitly universally quantified. + @{command "interpret"} after the @{keyword "where"} keyword should be + explicitly universally quantified. + + \item @{command "sublocale"}~@{text "name \ expr \ + eqns"} + interprets @{text expr} in the locale @{text name}. A proof that + the specification of @{text name} implies the specification of + @{text expr} is required. As in the localized version of the + theorem command, the proof is in the context of @{text name}. After + the proof obligation has been discharged, the facts of @{text expr} + become part of locale @{text name} as \emph{derived} context + elements and are available when the context @{text name} is + subsequently entered. Note that, like import, this is dynamic: + facts added to a locale part of @{text expr} after interpretation + become also available in @{text name}. + + Only specification fragments of @{text expr} that are not already + part of @{text name} (be it imported, derived or a derived fragment + of the import) are considered in this process. This enables + circular interpretations provided that no infinite chains are + generated in the locale hierarchy. + + If interpretations of @{text name} exist in the current theory, the + command adds interpretations for @{text expr} as well, with the same + qualifier, although only for fragments of @{text expr} that are not + interpreted in the theory already. + + Equations given after @{keyword "where"} amend the morphism through + which @{text expr} is interpreted. This enables to map definitions + from the interpreted locales to entities of @{text name}. This + feature is experimental. \item @{command "print_interps"}~@{text "locale"} lists all interpretations of @{text "locale"} in the current theory or proof diff -r 1b8ff770f02c -r 710cdb9e0d17 doc-src/IsarRef/Thy/document/Spec.tex --- a/doc-src/IsarRef/Thy/document/Spec.tex Thu Jan 06 21:06:17 2011 +0100 +++ b/doc-src/IsarRef/Thy/document/Spec.tex Thu Jan 06 21:06:17 2011 +0100 @@ -515,51 +515,28 @@ also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}). \begin{matharray}{rcl} - \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}proof{\isaliteral{28}{\isacharparenleft}}state{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{7C}{\isacharbar}}\ proof{\isaliteral{28}{\isacharparenleft}}chain{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ + \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ proof{\isaliteral{28}{\isacharparenleft}}prove{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} \\ \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\ \end{matharray} \indexouternonterm{interp} \begin{rail} - 'sublocale' nameref ('<' | subseteq) localeexpr - ; - 'interpretation' localeepxr equations? + 'interpretation' localeexpr equations? ; 'interpret' localeexpr equations? ; - 'print_interps' nameref + 'sublocale' nameref ('<' | subseteq) localeexpr equations? ; equations: 'where' (thmdecl? prop + 'and') ; + 'print_interps' nameref + ; \end{rail} \begin{description} - \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ expr{\isaliteral{22}{\isachardoublequote}}} - interprets \isa{expr} in the locale \isa{name}. A proof that - the specification of \isa{name} implies the specification of - \isa{expr} is required. As in the localized version of the - theorem command, the proof is in the context of \isa{name}. After - the proof obligation has been dischared, the facts of \isa{expr} - become part of locale \isa{name} as \emph{derived} context - elements and are available when the context \isa{name} is - subsequently entered. Note that, like import, this is dynamic: - facts added to a locale part of \isa{expr} after interpretation - become also available in \isa{name}. - - Only specification fragments of \isa{expr} that are not already - part of \isa{name} (be it imported, derived or a derived fragment - of the import) are considered in this process. This enables - circular interpretations to the extent that no infinite chains are - generated in the locale hierarchy. - - If interpretations of \isa{name} exist in the current theory, the - command adds interpretations for \isa{expr} as well, with the same - qualifier, although only for fragments of \isa{expr} that are not - interpreted in the theory already. - \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}} interprets \isa{expr} in the theory. The command generates proof obligations for the instantiated specifications (assumes and defines @@ -569,7 +546,7 @@ Additional equations, which are unfolded during post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}. This is useful for interpreting concepts introduced through - definition specification elements. The equations must be proved. + definitions. The equations must be proved. The command is aware of interpretations already active in the theory, but does not simplify the goal automatically. In order to @@ -582,14 +559,46 @@ parts. Adding facts to locales has the effect of adding interpreted facts - to the theory for all active interpretations also. That is, + to the theory for all interpretations as well. That is, interpretations dynamically participate in any facts added to - locales. + locales. Note that if a theory inherits additional facts for a + locale through one parent and an interpretation of that locale + through another parent, the additional facts will not be + interpreted. \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}} interprets \isa{expr} in the proof context and is otherwise similar to interpretation in theories. Note that rewrite rules given to - \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} should be explicitly universally quantified. + \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} after the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} keyword should be + explicitly universally quantified. + + \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}} + interprets \isa{expr} in the locale \isa{name}. A proof that + the specification of \isa{name} implies the specification of + \isa{expr} is required. As in the localized version of the + theorem command, the proof is in the context of \isa{name}. After + the proof obligation has been discharged, the facts of \isa{expr} + become part of locale \isa{name} as \emph{derived} context + elements and are available when the context \isa{name} is + subsequently entered. Note that, like import, this is dynamic: + facts added to a locale part of \isa{expr} after interpretation + become also available in \isa{name}. + + Only specification fragments of \isa{expr} that are not already + part of \isa{name} (be it imported, derived or a derived fragment + of the import) are considered in this process. This enables + circular interpretations provided that no infinite chains are + generated in the locale hierarchy. + + If interpretations of \isa{name} exist in the current theory, the + command adds interpretations for \isa{expr} as well, with the same + qualifier, although only for fragments of \isa{expr} that are not + interpreted in the theory already. + + Equations given after \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} amend the morphism through + which \isa{expr} is interpreted. This enables to map definitions + from the interpreted locales to entities of \isa{name}. This + feature is experimental. \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} lists all interpretations of \isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} in the current theory or proof