src/Doc/Isar_Ref/Spec.thy
changeset 67764 0f8cb5568b63
parent 67740 b6ce18784872
child 68276 cbee43ff4ceb
     1.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Mar 03 22:33:25 2018 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sun Mar 04 12:22:48 2018 +0100
     1.3 @@ -460,7 +460,8 @@
     1.4    @{rail \<open>
     1.5      @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
     1.6      ;
     1.7 -    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) rewrites?
     1.8 +    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) \<newline>
     1.9 +      rewrites?
    1.10      ;
    1.11      qualifier: @{syntax name} ('?')?
    1.12      ;
    1.13 @@ -654,11 +655,10 @@
    1.14      ;
    1.15      @@{command interpret} @{syntax locale_expr}
    1.16      ;
    1.17 -    @@{command global_interpretation} @{syntax locale_expr} \<newline>
    1.18 -      (definitions rewrites?)?
    1.19 +    @@{command global_interpretation} @{syntax locale_expr} definitions?
    1.20      ;
    1.21      @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
    1.22 -      (definitions rewrites?)?
    1.23 +      definitions?
    1.24      ;
    1.25      @@{command print_dependencies} '!'? @{syntax locale_expr}
    1.26      ;
    1.27 @@ -681,11 +681,15 @@
    1.28    to simplify the proof obligations according to existing interpretations use
    1.29    methods @{method intro_locales} or @{method unfold_locales}.
    1.30  
    1.31 -  Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> can occur within expressions or, for
    1.32 -  some commands, as part of the command itself.  They amend the morphism
    1.33 -  through which a locale instance or expression \<open>expr\<close> is interpreted with
    1.34 -  rewrite rules. This is particularly useful for interpreting concepts
    1.35 -  introduced through definitions. The equations must be proved the user.
    1.36 +  Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> occur within expressions. They amend the
    1.37 +  morphism through which a locale instance is interpreted with rewrite rules,
    1.38 +  also called rewrite morphisms. This is particularly useful for interpreting
    1.39 +  concepts introduced through definitions. The equations must be proved the
    1.40 +  user. To enable syntax of the instantiated locale within the equation, while
    1.41 +  reading a locale expression, equations of a locale instance are read in a
    1.42 +  temporary context where the instance is already activated. If activation
    1.43 +  fails, typically due to duplicate constant declarations, processing falls
    1.44 +  back to reading the equation first.
    1.45  
    1.46    Given definitions \<open>defs\<close> produce corresponding definitions in the local
    1.47    theory's underlying target \<^emph>\<open>and\<close> amend the morphism with rewrite rules
    1.48 @@ -714,7 +718,7 @@
    1.49    proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
    1.50    universally quantified.
    1.51  
    1.52 -  \<^descr> \<^theory_text>\<open>global_interpretation defines defs rewrites eqns\<close> interprets \<open>expr\<close>
    1.53 +  \<^descr> \<^theory_text>\<open>global_interpretation defines defs\<close> interprets \<open>expr\<close>
    1.54    into a global theory.
    1.55  
    1.56    When adding declarations to locales, interpreted versions of these
    1.57 @@ -727,7 +731,7 @@
    1.58    free variable whose name is already bound in the context --- for example,
    1.59    because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
    1.60  
    1.61 -  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs rewrites eqns\<close> interprets \<open>expr\<close>
    1.62 +  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs\<close> interprets \<open>expr\<close>
    1.63    into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the
    1.64    specification of \<open>expr\<close> is required. As in the localized version of the
    1.65    theorem command, the proof is in the context of \<open>name\<close>. After the proof
    1.66 @@ -744,7 +748,7 @@
    1.67    adds interpretations for \<open>expr\<close> as well, with the same qualifier, although
    1.68    only for fragments of \<open>expr\<close> that are not interpreted in the theory already.
    1.69  
    1.70 -  Using rewrite rules \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can help break
    1.71 +  Rewrites clauses in the expression or rewrite definitions \<open>defs\<close> can help break
    1.72    infinite chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.
    1.73  
    1.74    In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the
    1.75 @@ -787,13 +791,6 @@
    1.76    \end{warn}
    1.77  
    1.78    \begin{warn}
    1.79 -    Due to a technical limitation, the specific context of a interpretation
    1.80 -    given by a \<^theory_text>\<open>for\<close> clause can get lost between a \<^theory_text>\<open>defines\<close> and
    1.81 -    \<^theory_text>\<open>rewrites\<close> clause and must then be recovered manually using
    1.82 -    explicit sort constraints and quantified term variables.
    1.83 -  \end{warn}
    1.84 -
    1.85 -  \begin{warn}
    1.86      While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
    1.87      its result is discarded immediately.
    1.88    \end{warn}