# HG changeset patch
# User ballarin
# Date 1520162568 -3600
# Node ID 0f8cb5568b6369e217b9a4043abda99984b3ddb1
# Parent  f4b1cf9e70102b0203169adfd21778792e577c10
Drop rewrites after defines in interpretations.

diff -r f4b1cf9e7010 -r 0f8cb5568b63 NEWS
--- a/NEWS	Sat Mar 03 22:33:25 2018 +0100
+++ b/NEWS	Sun Mar 04 12:22:48 2018 +0100
@@ -176,14 +176,14 @@
 (e.g. use 'find_theorems' or 'try' to figure this out).
 
 * Rewrites clauses (keyword 'rewrites') were moved into the locale
-expression syntax, where they are part of locale instances.  Keyword
-'for' now needs to occur after, not before 'rewrites'.
-Minor INCOMPATIBILITY.
-
-* For rewrites clauses in locale expressions, if activating a locale
-instance fails, fall back to reading the clause first.  This helps
-avoiding qualified locale instances where the qualifier's sole purpose
-is avoiding duplicate constant declarations.
+expression syntax, where they are part of locale instances.  In
+interpretation commands rewrites clauses now need to occur before
+'for' and 'defines'.  Minor INCOMPATIBILITY.
+
+* For rewrites clauses, if activating a locale instance fails, fall
+back to reading the clause first.  This helps avoid qualification of
+locale instances where the qualifier's sole purpose is avoiding
+duplicate constant declarations.
 
 
 *** Pure ***
diff -r f4b1cf9e7010 -r 0f8cb5568b63 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sat Mar 03 22:33:25 2018 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Sun Mar 04 12:22:48 2018 +0100
@@ -460,7 +460,8 @@
   @{rail \<open>
     @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
     ;
-    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) rewrites?
+    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) \<newline>
+      rewrites?
     ;
     qualifier: @{syntax name} ('?')?
     ;
@@ -654,11 +655,10 @@
     ;
     @@{command interpret} @{syntax locale_expr}
     ;
-    @@{command global_interpretation} @{syntax locale_expr} \<newline>
-      (definitions rewrites?)?
+    @@{command global_interpretation} @{syntax locale_expr} definitions?
     ;
     @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
-      (definitions rewrites?)?
+      definitions?
     ;
     @@{command print_dependencies} '!'? @{syntax locale_expr}
     ;
@@ -681,11 +681,15 @@
   to simplify the proof obligations according to existing interpretations use
   methods @{method intro_locales} or @{method unfold_locales}.
 
-  Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> can occur within expressions or, for
-  some commands, as part of the command itself.  They amend the morphism
-  through which a locale instance or expression \<open>expr\<close> is interpreted with
-  rewrite rules. This is particularly useful for interpreting concepts
-  introduced through definitions. The equations must be proved the user.
+  Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> occur within expressions. They amend the
+  morphism through which a locale instance is interpreted with rewrite rules,
+  also called rewrite morphisms. This is particularly useful for interpreting
+  concepts introduced through definitions. The equations must be proved the
+  user. To enable syntax of the instantiated locale within the equation, while
+  reading a locale expression, equations of a locale instance are read in a
+  temporary context where the instance is already activated. If activation
+  fails, typically due to duplicate constant declarations, processing falls
+  back to reading the equation first.
 
   Given definitions \<open>defs\<close> produce corresponding definitions in the local
   theory's underlying target \<^emph>\<open>and\<close> amend the morphism with rewrite rules
@@ -714,7 +718,7 @@
   proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
   universally quantified.
 
-  \<^descr> \<^theory_text>\<open>global_interpretation defines defs rewrites eqns\<close> interprets \<open>expr\<close>
+  \<^descr> \<^theory_text>\<open>global_interpretation defines defs\<close> interprets \<open>expr\<close>
   into a global theory.
 
   When adding declarations to locales, interpreted versions of these
@@ -727,7 +731,7 @@
   free variable whose name is already bound in the context --- for example,
   because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
 
-  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs rewrites eqns\<close> interprets \<open>expr\<close>
+  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs\<close> interprets \<open>expr\<close>
   into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the
   specification of \<open>expr\<close> is required. As in the localized version of the
   theorem command, the proof is in the context of \<open>name\<close>. After the proof
@@ -744,7 +748,7 @@
   adds interpretations for \<open>expr\<close> as well, with the same qualifier, although
   only for fragments of \<open>expr\<close> that are not interpreted in the theory already.
 
-  Using rewrite rules \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can help break
+  Rewrites clauses in the expression or rewrite definitions \<open>defs\<close> can help break
   infinite chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.
 
   In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the
@@ -787,13 +791,6 @@
   \end{warn}
 
   \begin{warn}
-    Due to a technical limitation, the specific context of a interpretation
-    given by a \<^theory_text>\<open>for\<close> clause can get lost between a \<^theory_text>\<open>defines\<close> and
-    \<^theory_text>\<open>rewrites\<close> clause and must then be recovered manually using
-    explicit sort constraints and quantified term variables.
-  \end{warn}
-
-  \begin{warn}
     While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
     its result is discarded immediately.
   \end{warn}
diff -r f4b1cf9e7010 -r 0f8cb5568b63 src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Sat Mar 03 22:33:25 2018 +0100
+++ b/src/HOL/Library/FSet.thy	Sun Mar 04 12:22:48 2018 +0100
@@ -751,8 +751,8 @@
 context comm_monoid_add begin
 
 sublocale fsum: comm_monoid_fset plus 0
+  rewrites "comm_monoid_set.F plus 0 = sum"
   defines fsum = fsum.F
-  rewrites "comm_monoid_set.F plus 0 = sum"
 proof -
   show "comm_monoid_fset (+) 0" by standard
 
@@ -797,8 +797,8 @@
 context linorder begin
 
 sublocale fMin: semilattice_order_fset min less_eq less
+  rewrites "semilattice_set.F min = Min"
   defines fMin = fMin.F
-  rewrites "semilattice_set.F min = Min"
 proof -
   show "semilattice_order_fset min (\<le>) (<)" by standard
 
@@ -806,8 +806,8 @@
 qed
 
 sublocale fMax: semilattice_order_fset max greater_eq greater
+  rewrites "semilattice_set.F max = Max"
   defines fMax = fMax.F
-  rewrites "semilattice_set.F max = Max"
 proof -
   show "semilattice_order_fset max (\<ge>) (>)"
     by standard
diff -r f4b1cf9e7010 -r 0f8cb5568b63 src/HOL/Library/Groups_Big_Fun.thy
--- a/src/HOL/Library/Groups_Big_Fun.thy	Sat Mar 03 22:33:25 2018 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Sun Mar 04 12:22:48 2018 +0100
@@ -215,8 +215,8 @@
 begin
 
 sublocale Sum_any: comm_monoid_fun plus 0
+  rewrites "comm_monoid_set.F plus 0 = sum"
   defines Sum_any = Sum_any.G
-  rewrites "comm_monoid_set.F plus 0 = sum"
 proof -
   show "comm_monoid_fun plus 0" ..
   then interpret Sum_any: comm_monoid_fun plus 0 .
@@ -282,8 +282,8 @@
 begin
 
 sublocale Prod_any: comm_monoid_fun times 1
+  rewrites "comm_monoid_set.F times 1 = prod"
   defines Prod_any = Prod_any.G
-  rewrites "comm_monoid_set.F times 1 = prod"
 proof -
   show "comm_monoid_fun times 1" ..
   then interpret Prod_any: comm_monoid_fun times 1 .
diff -r f4b1cf9e7010 -r 0f8cb5568b63 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sat Mar 03 22:33:25 2018 +0100
+++ b/src/Pure/Pure.thy	Sun Mar 04 12:22:48 2018 +0100
@@ -622,9 +622,8 @@
 val interpretation_args_with_defs =
   Parse.!!! Parse_Spec.locale_expression --
     (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))
-      -- Scan.optional (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-        -- Parse.prop)) []) ([], []));
+      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term)) >>
+      (fn x => (x, []))) ([], []));
 
 val _ =
   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>