794 interpretations. |
794 interpretations. |
795 \end{warn} |
795 \end{warn} |
796 \<close> |
796 \<close> |
797 |
797 |
798 |
798 |
|
799 subsubsection \<open>Permanent locale interpretation\<close> |
|
800 |
|
801 text \<open> |
|
802 Permanent locale interpretation is a library extension on top |
|
803 of @{command "interpretation"} and @{command "sublocale"}. It is |
|
804 available by importing theory @{file "~~/src/Tools/Permanent_Interpretation.thy"} |
|
805 and provides |
|
806 \begin{enumerate} |
|
807 \item a unified view on arbitrary suitable local theories as interpretation target; |
|
808 \item rewrite morphisms by means of \emph{mixin definitions}. |
|
809 \end{enumerate} |
|
810 |
|
811 \begin{matharray}{rcl} |
|
812 @{command_def "permanent_interpretation"} & : & @{text "local_theory \<rightarrow> proof(prove)"} |
|
813 \end{matharray} |
|
814 |
|
815 @{rail \<open> |
|
816 @@{command permanent_interpretation} @{syntax locale_expr} \<newline> |
|
817 definitions? equations? |
|
818 ; |
|
819 |
|
820 definitions: @'defining' (@{syntax thmdecl}? @{syntax name} \<newline> |
|
821 @{syntax mixfix}? @'=' @{syntax term} + @'and'); |
|
822 equations: @'where' (@{syntax thmdecl}? @{syntax prop} + @'and') |
|
823 \<close>} |
|
824 |
|
825 \begin{description} |
|
826 |
|
827 \item @{command "permanent_interpretation"}~@{text "expr \<DEFINING> defs \<WHERE> eqns"} |
|
828 interprets @{text expr} in the current local theory. The command |
|
829 generates proof obligations for the instantiated specifications. |
|
830 Instantiated declarations (in particular, facts) are added to the |
|
831 local theory's underlying target in a post-processing phase. When |
|
832 adding declarations to locales, interpreted versions of these |
|
833 declarations are added to any target for all interpretations |
|
834 in that target as well. That is, permanent interpretations |
|
835 dynamically participate in any declarations added to |
|
836 locales. |
|
837 |
|
838 The local theory's underlying target must explicitly support |
|
839 permanent interpretations. Prominent examples are global theories |
|
840 (where @{command "permanent_interpretation"} is technically |
|
841 corresponding to @{command "interpretation"}) and locales |
|
842 (where @{command "permanent_interpretation"} is technically |
|
843 corresponding to @{command "sublocale"}). Unnamed contexts |
|
844 \secref{sec:target} are not admissible since they are |
|
845 non-permanent due to their very nature. |
|
846 |
|
847 In additions to \emph{rewrite morphisms} specified by @{text eqns}, |
|
848 also \emph{mixin definitions} may be specified. Semantically, a |
|
849 mixin definition results in a corresponding definition in |
|
850 the local theory's underlying target \emph{and} a mixin equation |
|
851 in the resulting rewrite morphisms which is symmetric to the |
|
852 original definition equation. |
|
853 |
|
854 The technical difference to a conventional definition plus |
|
855 an explicit mixin equation is that |
|
856 |
|
857 \begin{enumerate} |
|
858 |
|
859 \item definitions are parsed in the syntactic interpretation |
|
860 context, just like equations; |
|
861 |
|
862 \item the proof needs not consider the equations stemming from |
|
863 definitions -- they are proved implicitly by construction. |
|
864 |
|
865 \end{enumerate} |
|
866 |
|
867 Mixin definitions yield a pattern for introducing new explicit |
|
868 operations for existing terms after interpretation. |
|
869 |
|
870 \end{description} |
|
871 \<close> |
|
872 |
|
873 |
799 section \<open>Classes \label{sec:class}\<close> |
874 section \<open>Classes \label{sec:class}\<close> |
800 |
875 |
801 text \<open> |
876 text \<open> |
802 \begin{matharray}{rcl} |
877 \begin{matharray}{rcl} |
803 @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\ |
878 @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\ |