documentation on last state of the art concerning interpretation
authorhaftmann
Sat Dec 19 17:03:17 2015 +0100 (2015-12-19)
changeset 6189176189756ff65
parent 61890 f6ded81f5690
child 61892 5c68d06f97b3
documentation on last state of the art concerning interpretation
CONTRIBUTORS
NEWS
src/Doc/Codegen/Further.thy
src/Doc/Isar_Ref/Spec.thy
     1.1 --- a/CONTRIBUTORS	Sat Dec 19 11:05:04 2015 +0100
     1.2 +++ b/CONTRIBUTORS	Sat Dec 19 17:03:17 2015 +0100
     1.3 @@ -6,6 +6,10 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* Autumn 2015: Florian Haftmann, TUM
     1.8 +  Rewrite definitions for global interpretations and
     1.9 +  sublocale declarations.
    1.10 +
    1.11  * Autumn 2015: Andreas Lochbihler
    1.12    Bourbaki-Witt fixpoint theorem for increasing functions on
    1.13    chain-complete partial orders.
     2.1 --- a/NEWS	Sat Dec 19 11:05:04 2015 +0100
     2.2 +++ b/NEWS	Sat Dec 19 17:03:17 2015 +0100
     2.3 @@ -346,12 +346,15 @@
     2.4      notation right.derived ("\<odot>''")
     2.5    end
     2.6  
     2.7 -* Command 'sublocale' accepts rewrite definitions after keyword
     2.8 +* Command 'global_interpreation' issues interpretations into
     2.9 +global theories, with optional rewrite definitions following keyword
    2.10  'defines'.
    2.11  
    2.12 -* Command 'permanent_interpretation' is available in Pure, without
    2.13 -need to load a separate theory.  Keyword 'defines' identifies
    2.14 -rewrite definitions, keyword 'rewrites' identifies rewrite equations.
    2.15 +* Command 'sublocale' accepts optional rewrite definitions after
    2.16 +keyword 'defines'.
    2.17 +
    2.18 +* Command 'permanent_interpretation' has been discontinued.  Use
    2.19 +'global_interpretation' or 'sublocale' instead.
    2.20  INCOMPATIBILITY.
    2.21  
    2.22  * Command 'print_definitions' prints dependencies of definitional
     3.1 --- a/src/Doc/Codegen/Further.thy	Sat Dec 19 11:05:04 2015 +0100
     3.2 +++ b/src/Doc/Codegen/Further.thy	Sat Dec 19 17:03:17 2015 +0100
     3.3 @@ -139,7 +139,8 @@
     3.4  
     3.5  text \<open>
     3.6    A technical issue comes to surface when generating code from
     3.7 -  specifications stemming from locale interpretation.
     3.8 +  specifications stemming from locale interpretation into global
     3.9 +  theories.
    3.10  
    3.11    Let us assume a locale specifying a power operation on arbitrary
    3.12    types:
    3.13 @@ -177,7 +178,7 @@
    3.14  
    3.15  text \<open>
    3.16    After an interpretation of this locale (say, @{command_def
    3.17 -  interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
    3.18 +  global_interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
    3.19    :: 'a \<Rightarrow> 'a). f ^^ n)"}), one could naively expect to have a constant @{text
    3.20    "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
    3.21    can be generated.  But this not the case: internally, the term
    3.22 @@ -185,12 +186,11 @@
    3.23    term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
    3.24    (see @{cite "isabelle-locale"} for the details behind).
    3.25  
    3.26 -  Fortunately, a succint solution is available:
    3.27 -  @{command permanent_interpretation} with a dedicated
    3.28 +  Fortunately, a succint solution is available: a dedicated
    3.29    rewrite definition:
    3.30  \<close>
    3.31  
    3.32 -permanent_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"
    3.33 +global_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"
    3.34    defines funpows = fun_power.powers
    3.35    by unfold_locales
    3.36      (simp_all add: fun_eq_iff funpow_mult mult.commute)
     4.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Dec 19 11:05:04 2015 +0100
     4.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sat Dec 19 17:03:17 2015 +0100
     4.3 @@ -607,9 +607,8 @@
     4.4    \begin{matharray}{rcl}
     4.5      @{command "interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
     4.6      @{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
     4.7 -    @{command_def "interpretation"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
     4.8 +    @{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
     4.9      @{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
    4.10 -    @{command_def "permanent_interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
    4.11      @{command_def "print_dependencies"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
    4.12      @{command_def "print_interps"}\<open>\<^sup>*\<close> & :  & \<open>context \<rightarrow>\<close> \\
    4.13    \end{matharray}
    4.14 @@ -618,24 +617,20 @@
    4.15    added to the current context. This requires proof (of the instantiated
    4.16    specification) and is called \<^emph>\<open>locale interpretation\<close>. Interpretation is
    4.17    possible within arbitrary local theories (\<^theory_text>\<open>interpretation\<close>), within proof
    4.18 -  bodies (\<^theory_text>\<open>interpret\<close>), into global theories (another variant of
    4.19 -  \<^theory_text>\<open>interpretation\<close>) and into locales (\<^theory_text>\<open>sublocale\<close>). As a generalization,
    4.20 -  interpretation into arbitrary local theories is possible, although this is
    4.21 -  only implemented by certain targets (\<^theory_text>\<open>permanent_interpretation\<close>).
    4.22 +  bodies (\<^theory_text>\<open>interpret\<close>), into global theories (\<^theory_text>\<open>global_interpretation\<close>) and
    4.23 +  into locales (\<^theory_text>\<open>sublocale\<close>).
    4.24  
    4.25    @{rail \<open>
    4.26      @@{command interpretation} @{syntax locale_expr} equations?
    4.27      ;
    4.28      @@{command interpret} @{syntax locale_expr} equations?
    4.29      ;
    4.30 -    @@{command interpretation} @{syntax locale_expr} equations?
    4.31 +    @@{command global_interpretation} @{syntax locale_expr} \<newline>
    4.32 +      definitions? equations?
    4.33      ;
    4.34      @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
    4.35        definitions? equations?
    4.36      ;
    4.37 -    @@{command permanent_interpretation} @{syntax locale_expr} \<newline>
    4.38 -      definitions? equations?
    4.39 -    ;
    4.40      @@{command print_dependencies} '!'? @{syntax locale_expr}
    4.41      ;
    4.42      @@{command print_interps} @{syntax nameref}
    4.43 @@ -666,13 +661,13 @@
    4.44  
    4.45    Given definitions \<open>defs\<close> produce corresponding definitions in the local
    4.46    theory's underlying target \<^emph>\<open>and\<close> amend the morphism with the equations
    4.47 -  stemming from the symmetric of the definitions. Hence they need not be
    4.48 +  stemming from the symmetric of those definitions. Hence these need not be
    4.49    proved explicitly the user. Such rewrite definitions are a even more useful
    4.50    device for interpreting concepts introduced through definitions, but they
    4.51    are only supported for interpretation commands operating in a local theory
    4.52    whose implementing target actually supports this.  Note that despite
    4.53    the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
    4.54 -  are parsed sequentially without mutual recursion.
    4.55 +  are processed sequentially without mutual recursion.
    4.56  
    4.57    \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory
    4.58    such that its lifetime is limited to the current context block (e.g. a
    4.59 @@ -682,17 +677,21 @@
    4.60    interpreted locale instances, as would be the case with @{command
    4.61    sublocale}.
    4.62  
    4.63 +  When used on the level of a global theory, there is no end of a current
    4.64 +  context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to
    4.65 +  \<^theory_text>\<open>global_interpretation\<close> then.
    4.66 +
    4.67    \<^descr> \<^theory_text>\<open>interpret expr rewrites eqns\<close> interprets \<open>expr\<close> into a proof context:
    4.68    the interpretation and its declarations disappear when closing the current
    4.69    proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
    4.70    universally quantified.
    4.71  
    4.72 -  \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a global
    4.73 -  theory.
    4.74 +  \<^descr> \<^theory_text>\<open>global_interpretation defines "defs" rewrites eqns\<close> interprets \<open>expr\<close>
    4.75 +  into a global theory.
    4.76  
    4.77    When adding declarations to locales, interpreted versions of these
    4.78    declarations are added to the global theory for all interpretations in the
    4.79 -  global theory as well. That is, interpretations in global theories
    4.80 +  global theory as well. That is, interpretations into global theories
    4.81    dynamically participate in any declarations added to locales.
    4.82  
    4.83    Free variables in the interpreted expression are allowed. They are turned
    4.84 @@ -724,20 +723,6 @@
    4.85    locale argument must be omitted. The command then refers to the locale (or
    4.86    class) target of the context block.
    4.87  
    4.88 -  \<^descr> \<^theory_text>\<open>permanent_interpretation defines "defs" rewrites eqns\<close> interprets \<open>expr\<close>
    4.89 -  into the target of the current local theory. When adding declarations to
    4.90 -  locales, interpreted versions of these declarations are added to any target
    4.91 -  for all interpretations in that target as well. That is, permanent
    4.92 -  interpretations dynamically participate in any declarations added to
    4.93 -  locales.
    4.94 -  
    4.95 -  The local theory's underlying target must explicitly support permanent
    4.96 -  interpretations. Prominent examples are global theories (where
    4.97 -  \<^theory_text>\<open>permanent_interpretation\<close> technically corresponds to \<^theory_text>\<open>interpretation\<close>)
    4.98 -  and locales (where \<^theory_text>\<open>permanent_interpretation\<close> technically corresponds to
    4.99 -  \<^theory_text>\<open>sublocale\<close>). Unnamed contexts (see \secref{sec:target}) are not
   4.100 -  admissible.
   4.101 -
   4.102    \<^descr> \<^theory_text>\<open>print_dependencies expr\<close> is useful for understanding the effect of an
   4.103    interpretation of \<open>expr\<close> in the current context. It lists all locale
   4.104    instances for which interpretations would be added to the current context.
   4.105 @@ -751,7 +736,6 @@
   4.106    \<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close>
   4.107    declarations.
   4.108  
   4.109 -
   4.110    \begin{warn}
   4.111      If a global theory inherits declarations (body elements) for a locale from
   4.112      one parent and an interpretation of that locale from another parent, the