Documentation for 'interpret' and 'sublocale' with mixins.
authorballarin
Thu Jan 06 21:06:17 2011 +0100 (2011-01-06)
changeset 41434710cdb9e0d17
parent 41433 1b8ff770f02c
child 41435 12585dfb86fe
Documentation for 'interpret' and 'sublocale' with mixins.
NEWS
doc-src/IsarRef/Thy/Spec.thy
doc-src/IsarRef/Thy/document/Spec.tex
     1.1 --- a/NEWS	Thu Jan 06 21:06:17 2011 +0100
     1.2 +++ b/NEWS	Thu Jan 06 21:06:17 2011 +0100
     1.3 @@ -123,6 +123,11 @@
     1.4  * Document antiquotation @{file} checks file/directory entries within
     1.5  the local file system.
     1.6  
     1.7 +* Locale interpretation commands 'interpret' and 'sublocale' accept
     1.8 +equations to map definitions in a locale to appropriate entities in
     1.9 +the context of the interpretation.  The 'interpretation' command
    1.10 +already provided this functionality.
    1.11 +
    1.12  
    1.13  *** HOL ***
    1.14  
    1.15 @@ -502,8 +507,12 @@
    1.16  
    1.17  * Theorems for additive ring operations (locale abelian_monoid and
    1.18  descendants) are generated by interpretation from their multiplicative
    1.19 -counterparts.  This causes slight differences in the simp and clasets.
    1.20 -INCOMPATIBILITY.
    1.21 +counterparts.  Names (in particular theorem names) have the mandatory
    1.22 +qualifier 'add'.  Previous theorem names are redeclared for
    1.23 +compatibility.
    1.24 +
    1.25 +* Structure 'int_ring' is now an abbreviation (previously a
    1.26 +definition).  This fits more natural with advanced interpretations.
    1.27  
    1.28  
    1.29  *** HOLCF ***
     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Jan 06 21:06:17 2011 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Jan 06 21:06:17 2011 +0100
     2.3 @@ -494,51 +494,28 @@
     2.4    also within a proof body (command @{command "interpret"}).
     2.5  
     2.6    \begin{matharray}{rcl}
     2.7 -    @{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     2.8      @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     2.9      @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
    2.10 +    @{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
    2.11      @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    2.12    \end{matharray}
    2.13  
    2.14    \indexouternonterm{interp}
    2.15    \begin{rail}
    2.16 -    'sublocale' nameref ('<' | subseteq) localeexpr
    2.17 -    ;
    2.18 -    'interpretation' localeepxr equations?
    2.19 +    'interpretation' localeexpr equations?
    2.20      ;
    2.21      'interpret' localeexpr equations?
    2.22      ;
    2.23 -    'print_interps' nameref
    2.24 +    'sublocale' nameref ('<' | subseteq) localeexpr equations?
    2.25      ;
    2.26      equations: 'where' (thmdecl? prop + 'and')
    2.27      ;
    2.28 +    'print_interps' nameref
    2.29 +    ;
    2.30    \end{rail}
    2.31  
    2.32    \begin{description}
    2.33  
    2.34 -  \item @{command "sublocale"}~@{text "name \<subseteq> expr"}
    2.35 -  interprets @{text expr} in the locale @{text name}.  A proof that
    2.36 -  the specification of @{text name} implies the specification of
    2.37 -  @{text expr} is required.  As in the localized version of the
    2.38 -  theorem command, the proof is in the context of @{text name}.  After
    2.39 -  the proof obligation has been dischared, the facts of @{text expr}
    2.40 -  become part of locale @{text name} as \emph{derived} context
    2.41 -  elements and are available when the context @{text name} is
    2.42 -  subsequently entered.  Note that, like import, this is dynamic:
    2.43 -  facts added to a locale part of @{text expr} after interpretation
    2.44 -  become also available in @{text name}.
    2.45 -
    2.46 -  Only specification fragments of @{text expr} that are not already
    2.47 -  part of @{text name} (be it imported, derived or a derived fragment
    2.48 -  of the import) are considered in this process.  This enables
    2.49 -  circular interpretations to the extent that no infinite chains are
    2.50 -  generated in the locale hierarchy.
    2.51 -
    2.52 -  If interpretations of @{text name} exist in the current theory, the
    2.53 -  command adds interpretations for @{text expr} as well, with the same
    2.54 -  qualifier, although only for fragments of @{text expr} that are not
    2.55 -  interpreted in the theory already.
    2.56 -
    2.57    \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
    2.58    interprets @{text expr} in the theory.  The command generates proof
    2.59    obligations for the instantiated specifications (assumes and defines
    2.60 @@ -548,7 +525,7 @@
    2.61    Additional equations, which are unfolded during
    2.62    post-processing, may be given after the keyword @{keyword "where"}.
    2.63    This is useful for interpreting concepts introduced through
    2.64 -  definition specification elements.  The equations must be proved.
    2.65 +  definitions.  The equations must be proved.
    2.66  
    2.67    The command is aware of interpretations already active in the
    2.68    theory, but does not simplify the goal automatically.  In order to
    2.69 @@ -561,14 +538,47 @@
    2.70    parts.
    2.71  
    2.72    Adding facts to locales has the effect of adding interpreted facts
    2.73 -  to the theory for all active interpretations also.  That is,
    2.74 +  to the theory for all interpretations as well.  That is,
    2.75    interpretations dynamically participate in any facts added to
    2.76 -  locales.
    2.77 +  locales.  Note that if a theory inherits additional facts for a
    2.78 +  locale through one parent and an interpretation of that locale
    2.79 +  through another parent, the additional facts will not be
    2.80 +  interpreted.
    2.81  
    2.82    \item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
    2.83    @{text expr} in the proof context and is otherwise similar to
    2.84    interpretation in theories.  Note that rewrite rules given to
    2.85 -  @{command "interpret"} should be explicitly universally quantified.
    2.86 +  @{command "interpret"} after the @{keyword "where"} keyword should be
    2.87 +  explicitly universally quantified.
    2.88 +
    2.89 +  \item @{command "sublocale"}~@{text "name \<subseteq> expr \<WHERE>
    2.90 +  eqns"}
    2.91 +  interprets @{text expr} in the locale @{text name}.  A proof that
    2.92 +  the specification of @{text name} implies the specification of
    2.93 +  @{text expr} is required.  As in the localized version of the
    2.94 +  theorem command, the proof is in the context of @{text name}.  After
    2.95 +  the proof obligation has been discharged, the facts of @{text expr}
    2.96 +  become part of locale @{text name} as \emph{derived} context
    2.97 +  elements and are available when the context @{text name} is
    2.98 +  subsequently entered.  Note that, like import, this is dynamic:
    2.99 +  facts added to a locale part of @{text expr} after interpretation
   2.100 +  become also available in @{text name}.
   2.101 +
   2.102 +  Only specification fragments of @{text expr} that are not already
   2.103 +  part of @{text name} (be it imported, derived or a derived fragment
   2.104 +  of the import) are considered in this process.  This enables
   2.105 +  circular interpretations provided that no infinite chains are
   2.106 +  generated in the locale hierarchy.
   2.107 +
   2.108 +  If interpretations of @{text name} exist in the current theory, the
   2.109 +  command adds interpretations for @{text expr} as well, with the same
   2.110 +  qualifier, although only for fragments of @{text expr} that are not
   2.111 +  interpreted in the theory already.
   2.112 +
   2.113 +  Equations given after @{keyword "where"} amend the morphism through
   2.114 +  which @{text expr} is interpreted.  This enables to map definitions
   2.115 +  from the interpreted locales to entities of @{text name}.  This
   2.116 +  feature is experimental.
   2.117  
   2.118    \item @{command "print_interps"}~@{text "locale"} lists all
   2.119    interpretations of @{text "locale"} in the current theory or proof
     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Jan 06 21:06:17 2011 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Thu Jan 06 21:06:17 2011 +0100
     3.3 @@ -515,51 +515,28 @@
     3.4    also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
     3.5  
     3.6    \begin{matharray}{rcl}
     3.7 -    \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}}} \\
     3.8      \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}}} \\
     3.9      \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}}} \\
    3.10 +    \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}}} \\
    3.11      \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}}} \\
    3.12    \end{matharray}
    3.13  
    3.14    \indexouternonterm{interp}
    3.15    \begin{rail}
    3.16 -    'sublocale' nameref ('<' | subseteq) localeexpr
    3.17 -    ;
    3.18 -    'interpretation' localeepxr equations?
    3.19 +    'interpretation' localeexpr equations?
    3.20      ;
    3.21      'interpret' localeexpr equations?
    3.22      ;
    3.23 -    'print_interps' nameref
    3.24 +    'sublocale' nameref ('<' | subseteq) localeexpr equations?
    3.25      ;
    3.26      equations: 'where' (thmdecl? prop + 'and')
    3.27      ;
    3.28 +    'print_interps' nameref
    3.29 +    ;
    3.30    \end{rail}
    3.31  
    3.32    \begin{description}
    3.33  
    3.34 -  \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ expr{\isaliteral{22}{\isachardoublequote}}}
    3.35 -  interprets \isa{expr} in the locale \isa{name}.  A proof that
    3.36 -  the specification of \isa{name} implies the specification of
    3.37 -  \isa{expr} is required.  As in the localized version of the
    3.38 -  theorem command, the proof is in the context of \isa{name}.  After
    3.39 -  the proof obligation has been dischared, the facts of \isa{expr}
    3.40 -  become part of locale \isa{name} as \emph{derived} context
    3.41 -  elements and are available when the context \isa{name} is
    3.42 -  subsequently entered.  Note that, like import, this is dynamic:
    3.43 -  facts added to a locale part of \isa{expr} after interpretation
    3.44 -  become also available in \isa{name}.
    3.45 -
    3.46 -  Only specification fragments of \isa{expr} that are not already
    3.47 -  part of \isa{name} (be it imported, derived or a derived fragment
    3.48 -  of the import) are considered in this process.  This enables
    3.49 -  circular interpretations to the extent that no infinite chains are
    3.50 -  generated in the locale hierarchy.
    3.51 -
    3.52 -  If interpretations of \isa{name} exist in the current theory, the
    3.53 -  command adds interpretations for \isa{expr} as well, with the same
    3.54 -  qualifier, although only for fragments of \isa{expr} that are not
    3.55 -  interpreted in the theory already.
    3.56 -
    3.57    \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}}
    3.58    interprets \isa{expr} in the theory.  The command generates proof
    3.59    obligations for the instantiated specifications (assumes and defines
    3.60 @@ -569,7 +546,7 @@
    3.61    Additional equations, which are unfolded during
    3.62    post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
    3.63    This is useful for interpreting concepts introduced through
    3.64 -  definition specification elements.  The equations must be proved.
    3.65 +  definitions.  The equations must be proved.
    3.66  
    3.67    The command is aware of interpretations already active in the
    3.68    theory, but does not simplify the goal automatically.  In order to
    3.69 @@ -582,14 +559,46 @@
    3.70    parts.
    3.71  
    3.72    Adding facts to locales has the effect of adding interpreted facts
    3.73 -  to the theory for all active interpretations also.  That is,
    3.74 +  to the theory for all interpretations as well.  That is,
    3.75    interpretations dynamically participate in any facts added to
    3.76 -  locales.
    3.77 +  locales.  Note that if a theory inherits additional facts for a
    3.78 +  locale through one parent and an interpretation of that locale
    3.79 +  through another parent, the additional facts will not be
    3.80 +  interpreted.
    3.81  
    3.82    \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}} interprets
    3.83    \isa{expr} in the proof context and is otherwise similar to
    3.84    interpretation in theories.  Note that rewrite rules given to
    3.85 -  \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} should be explicitly universally quantified.
    3.86 +  \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}} after the \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} keyword should be
    3.87 +  explicitly universally quantified.
    3.88 +
    3.89 +  \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}name\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ expr\ {\isaliteral{5C3C57484552453E}{\isasymWHERE}}\ eqns{\isaliteral{22}{\isachardoublequote}}}
    3.90 +  interprets \isa{expr} in the locale \isa{name}.  A proof that
    3.91 +  the specification of \isa{name} implies the specification of
    3.92 +  \isa{expr} is required.  As in the localized version of the
    3.93 +  theorem command, the proof is in the context of \isa{name}.  After
    3.94 +  the proof obligation has been discharged, the facts of \isa{expr}
    3.95 +  become part of locale \isa{name} as \emph{derived} context
    3.96 +  elements and are available when the context \isa{name} is
    3.97 +  subsequently entered.  Note that, like import, this is dynamic:
    3.98 +  facts added to a locale part of \isa{expr} after interpretation
    3.99 +  become also available in \isa{name}.
   3.100 +
   3.101 +  Only specification fragments of \isa{expr} that are not already
   3.102 +  part of \isa{name} (be it imported, derived or a derived fragment
   3.103 +  of the import) are considered in this process.  This enables
   3.104 +  circular interpretations provided that no infinite chains are
   3.105 +  generated in the locale hierarchy.
   3.106 +
   3.107 +  If interpretations of \isa{name} exist in the current theory, the
   3.108 +  command adds interpretations for \isa{expr} as well, with the same
   3.109 +  qualifier, although only for fragments of \isa{expr} that are not
   3.110 +  interpreted in the theory already.
   3.111 +
   3.112 +  Equations given after \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}} amend the morphism through
   3.113 +  which \isa{expr} is interpreted.  This enables to map definitions
   3.114 +  from the interpreted locales to entities of \isa{name}.  This
   3.115 +  feature is experimental.
   3.116  
   3.117    \item \hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}interps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} lists all
   3.118    interpretations of \isa{{\isaliteral{22}{\isachardoublequote}}locale{\isaliteral{22}{\isachardoublequote}}} in the current theory or proof