Proper rewrite morphisms in locale instances.

--- a/NEWS	Thu Mar 01 20:44:38 2018 +0100
+++ b/NEWS	Fri Mar 02 14:19:25 2018 +0100
@@ -175,6 +175,11 @@
 Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
 (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.
+
 
 *** Pure ***
 

--- a/src/Doc/Isar_Ref/Spec.thy	Thu Mar 01 20:44:38 2018 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Fri Mar 02 14:19:25 2018 +0100
@@ -460,17 +460,20 @@
   @{rail \<open>
     @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
     ;
-    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts)
+    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) rewrites?
     ;
     qualifier: @{syntax name} ('?')?
     ;
     pos_insts: ('_' | @{syntax term})*
     ;
     named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
+    ;
+    rewrites: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
   \<close>}
 
   A locale instance consists of a reference to a locale and either positional
-  or named parameter instantiations. Identical instantiations (that is, those
+  or named parameter instantiations optionally followed by rewrites clauses.
+  Identical instantiations (that is, those
   that instantiate a parameter by itself) may be omitted. The notation ``\<open>_\<close>''
   enables to omit the instantiation for a parameter inside a positional
   instantiation.
@@ -487,6 +490,11 @@
   ``\<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on input.
   Qualifiers only affect name spaces; they play no role in determining whether
   one locale instance subsumes another.
+
+  Rewrite clauses amend instances with equations that act as rewrite rules.
+  This is particularly useful for changing concepts introduced through
+  definitions. Rewrite clauses are available only in interpretation commands
+  (see \secref{sec:locale-interpretation} below) and must be proved the user.
 \<close>
 
 
@@ -622,7 +630,7 @@
 \<close>
 
 
-subsection \<open>Locale interpretation\<close>
+subsection \<open>Locale interpretation \label{sec:locale-interpretation}\<close>
 
 text \<open>
   \begin{matharray}{rcl}
@@ -642,15 +650,15 @@
   into locales (\<^theory_text>\<open>sublocale\<close>).
 
   @{rail \<open>
-    @@{command interpretation} @{syntax locale_expr} equations?
+    @@{command interpretation} @{syntax locale_expr}
     ;
-    @@{command interpret} @{syntax locale_expr} equations?
+    @@{command interpret} @{syntax locale_expr}
     ;
     @@{command global_interpretation} @{syntax locale_expr} \<newline>
-      definitions? equations?
+      (definitions rewrites?)?
     ;
     @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
-      definitions? equations?
+      (definitions rewrites?)?
     ;
     @@{command print_dependencies} '!'? @{syntax locale_expr}
     ;
@@ -659,8 +667,6 @@
 
     definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
       @{syntax mixfix}? @'=' @{syntax term} + @'and');
-
-    equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
   \<close>}
 
   The core of each interpretation command is a locale expression \<open>expr\<close>; the
@@ -675,13 +681,14 @@
   to simplify the proof obligations according to existing interpretations use
   methods @{method intro_locales} or @{method unfold_locales}.
 
-  Given equations \<open>eqns\<close> amend the morphism through which \<open>expr\<close> is
-  interpreted, adding 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> 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.
 
   Given definitions \<open>defs\<close> produce corresponding definitions in the local
-  theory's underlying target \<^emph>\<open>and\<close> amend the morphism with the equations
+  theory's underlying target \<^emph>\<open>and\<close> amend the morphism with rewrite rules
   stemming from the symmetric of those definitions. Hence these need not be
   proved explicitly the user. Such rewrite definitions are a even more useful
   device for interpreting concepts introduced through definitions, but they
@@ -690,7 +697,7 @@
   the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
   are processed sequentially without mutual recursion.
 
-  \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory
+  \<^descr> \<^theory_text>\<open>interpretation expr\<close> interprets \<open>expr\<close> into a local theory
   such that its lifetime is limited to the current context block (e.g. a
   locale or unnamed context). At the closing @{command end} of the block the
   interpretation and its declarations disappear. Hence facts based on
@@ -702,7 +709,7 @@
   context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to
   \<^theory_text>\<open>global_interpretation\<close> then.
 
-  \<^descr> \<^theory_text>\<open>interpret expr rewrites eqns\<close> interprets \<open>expr\<close> into a proof context:
+  \<^descr> \<^theory_text>\<open>interpret expr\<close> interprets \<open>expr\<close> into a proof context:
   the interpretation and its declarations disappear when closing the current
   proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
   universally quantified.
@@ -720,7 +727,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> defines defs expr rewrites eqns\<close> interprets \<open>expr\<close>
+  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs rewrites eqns\<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
@@ -737,8 +744,8 @@
   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 equations \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can help break infinite
-  chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.
+  Using rewrite rules \<open>eqns\<close> 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
   locale argument must be omitted. The command then refers to the locale (or

--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Mar 01 20:44:38 2018 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Mar 02 14:19:25 2018 +0100
@@ -523,7 +523,7 @@
 
 subsection \<open>Rewrite morphisms in expressions\<close>
 
-interpretation y: logic_o "(\<or>)" "Not" replaces bool_logic_o2: "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y"
+interpretation y: logic_o "(\<or>)" "Not" rewrites bool_logic_o2: "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y"
 proof -
   show bool_logic_o: "PROP logic_o((\<or>), Not)" by unfold_locales fast+
   show "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y" unfolding logic_o.lor_o_def [OF bool_logic_o] by fast

--- a/src/Pure/Isar/element.ML	Thu Mar 01 20:44:38 2018 +0100
+++ b/src/Pure/Isar/element.ML	Fri Mar 02 14:19:25 2018 +0100
@@ -50,6 +50,7 @@
   val instantiate_normalize_morphism:
     ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
   val satisfy_morphism: witness list -> morphism
+  val eq_term_morphism: theory -> term list -> morphism option
   val eq_morphism: theory -> thm list -> morphism option
   val init: context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
@@ -381,6 +382,26 @@
 
 (* rewriting with equalities *)
 
+(* for activating declarations only *)
+fun eq_term_morphism _ [] = NONE
+  | eq_term_morphism thy props =
+      let
+        fun decomp_simp prop =
+          let
+            val ctxt = Proof_Context.init_global thy;
+            val _ = Logic.count_prems prop = 0 orelse
+              error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop);
+            val lhsrhs = Logic.dest_equals prop
+              handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop);
+          in lhsrhs end;
+        val phi =
+          Morphism.morphism "Element.eq_term_morphism"
+           {binding = [],
+            typ = [],
+            term = [Pattern.rewrite_term thy (map decomp_simp props) []],
+            fact = [fn _ => error "Illegal application of Element.eq_term_morphism"]};
+      in SOME phi end;
+
 fun eq_morphism _ [] = NONE
   | eq_morphism thy thms =
       let

--- a/src/Pure/Isar/expression.ML	Thu Mar 01 20:44:38 2018 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Mar 02 14:19:25 2018 +0100
@@ -8,7 +8,8 @@
 sig
   (* Locale expressions *)
   datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
-  type ('name, 'term) expr = ('name * ((string * bool) * ('term map * (Attrib.binding * 'term) list))) list
+  type 'term rewrites = (Attrib.binding * 'term) list
+  type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list
   type expression_i = (string, term) expr * (binding * typ option * mixfix) list
   type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
 
@@ -58,7 +59,9 @@
   Positional of 'term option list |
   Named of (string * 'term) list;
 
-type ('name, 'term) expr = ('name * ((string * bool) * ('term map * (Attrib.binding * 'term) list))) list;
+type 'term rewrites = (Attrib.binding * 'term) list;
+
+type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list;
 
 type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
 type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
@@ -367,8 +370,11 @@
 
 local
 
+fun abs_def ctxt =
+  Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of;
+
 fun prep_full_context_statement
-    parse_typ parse_prop prep_obtains prep_var_elem prep_inst parse_eqn prep_var_inst prep_expr
+    parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr
     {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 =
   let
     val thy = Proof_Context.theory_of ctxt1;
@@ -379,23 +385,29 @@
       let
         val params = map #1 (Locale.params_of thy loc);
         val inst' = prep_inst ctxt (map #1 params) inst;
-        val eqns' = map (apsnd (parse_eqn ctxt)) eqns;
         val parm_types' =
           params |> map (#2 #> Logic.varifyT_global #>
               Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #>
               Type_Infer.paramify_vars);
         val inst'' = map2 Type.constraint parm_types' inst';
         val insts' = insts @ [(loc, (prfx, inst''))];
-        val eqnss' = eqnss @ [eqns'];
-        val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt;
-        val (inst_morph, _) = inst_morphism params (prfx, #2 (#2 (List.last insts''))) ctxt;
-        val rewrite_morph =
-          List.last eqnss''
-          |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt)
-          |> Element.eq_morphism (Proof_Context.theory_of ctxt)
+        val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt;
+        val inst''' = insts'' |> List.last |> snd |> snd;
+        val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt;
+        val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2; (* may fail *)
+
+        val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns;
+        val eqns' = (prep_eqns ctxt' o map snd) eqns;
+        val eqnss' = [attrss ~~ eqns'];
+        val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt';
+        val rewrite_morph = eqns'
+          |> map (abs_def ctxt')
+          |> Variable.export_terms ctxt' ctxt
+          |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
           |> the_default Morphism.identity;
-        val ctxt' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
-      in (i + 1, insts', eqnss', ctxt') end;
+       val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
+       val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
+      in (i + 1, insts', eqnss', ctxt'') end;
 
     fun prep_elem raw_elem ctxt =
       let
@@ -411,7 +423,7 @@
     val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2);
 
     fun prep_stmt elems ctxt =
-      check_autofix insts' eqnss' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
+      check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
 
     val _ =
       if fixed_frees then ()
@@ -421,7 +433,7 @@
         | frees => error ("Illegal free variables in expression: " ^
             commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
 
-    val ((insts, eqnss, elems', concl), ctxt4) = ctxt3
+    val ((insts, _, elems', concl), ctxt4) = ctxt3
       |> init_body
       |> fold_map prep_elem raw_elems
       |-> prep_stmt;
@@ -438,21 +450,21 @@
     val deps = map (finish_inst ctxt5) insts;
     val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems';
 
-  in ((fixed, deps, eqnss, elems'', concl), (parms, ctxt5)) end;
+  in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end;
 
 in
 
 fun cert_full_context_statement x =
   prep_full_context_statement (K I) (K I) Obtain.cert_obtains
-    Proof_Context.cert_var make_inst (K I) Proof_Context.cert_var (K I) x;
+    Proof_Context.cert_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x;
 
 fun cert_read_full_context_statement x =
   prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
-    Proof_Context.read_var make_inst (K I) Proof_Context.cert_var (K I) x;
+    Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x;
 
 fun read_full_context_statement x =
   prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
-    Proof_Context.read_var parse_inst (Syntax.parse_prop) Proof_Context.read_var check_expr x;
+    Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x;
 
 end;
 
@@ -492,7 +504,7 @@
     val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) =
       prep {strict = false, do_close = true, fixed_frees = false}
         raw_import init_body raw_elems (Element.Shows []) ctxt;
-    val _ = null (flat eqnss) orelse error "Illegal replaces clause(s) in declaration of locale";
+    val _ = null (flat eqnss) orelse error "Illegal rewrites clause(s) in declaration of locale";
     (* Declare parameters and imported facts *)
     val ctxt' = ctxt
       |> fix_params fixed
@@ -537,7 +549,7 @@
 
     val goal_ctxt = ctxt
       |> fix_params fixed
-      |> (fold o fold) Variable.auto_fixes propss;
+      |> (fold o fold) Variable.auto_fixes (propss @ eq_propss);
 
     val export = Variable.export_morphism goal_ctxt ctxt;
     val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;

--- a/src/Pure/Isar/interpretation.ML	Thu Mar 01 20:44:38 2018 +0100
+++ b/src/Pure/Isar/interpretation.ML	Fri Mar 02 14:19:25 2018 +0100
@@ -49,7 +49,7 @@
 (** common interpretation machinery **)
 
 type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
-type 'a rewrites = (Attrib.binding * 'a) list
+type 'a rewrites = 'a Expression.rewrites
 
 (* reading of locale expressions with rewrite morphisms *)
 
@@ -83,7 +83,7 @@
   | prep_eqns prep_props prep_attr raw_eqns deps ctxt =
       let
         (* FIXME incompatibility, creating context for parsing rewrites equation may fail in
-           presence of replaces clause *)
+           presence of rewrites clause in expression *)
         val ctxt' = fold Locale.activate_declarations deps ctxt;
         val eqns =
           (Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns;

--- a/src/Pure/Isar/parse_spec.ML	Thu Mar 01 20:44:38 2018 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Fri Mar 02 14:19:25 2018 +0100
@@ -114,7 +114,7 @@
 val instance = Scan.optional (Parse.where_ |--
   Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
   Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional) (Expression.Named []) --
-  (Scan.optional (Parse.$$$ "replaces" |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []);
+  (Scan.optional (Parse.$$$ "rewrites" |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []);
 
 in
 

--- a/src/Pure/Pure.thy	Thu Mar 01 20:44:38 2018 +0100
+++ b/src/Pure/Pure.thy	Fri Mar 02 14:19:25 2018 +0100
@@ -10,7 +10,7 @@
     "\<subseteq>" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
     "overloaded" "pervasive" "premises" "structure" "unchecked"
   and "private" "qualified" :: before_command
-  and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "replaces" "rewrites"
+  and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
     "obtains" "shows" "when" "where" "|" :: quasi_command
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
@@ -613,23 +613,18 @@
       >> (fn elems =>
           Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
 
-val interpretation_args =
-  Parse.!!! Parse_Spec.locale_expression --
-    Scan.optional
-      (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
-
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
     "prove interpretation of locale expression in proof context"
-    (interpretation_args >> (fn (expr, equations) =>
-      Toplevel.proof (Interpretation.interpret_cmd expr equations)));
+    (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
+      Toplevel.proof (Interpretation.interpret_cmd expr [])));
 
 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))
+      -- Scan.optional (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
+        -- Parse.prop)) []) ([], []));
 
 val _ =
   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
@@ -649,9 +644,9 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
     "prove interpretation of locale expression in local theory or into global theory"
-    (interpretation_args >> (fn (expr, equations) =>
+    (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
       Toplevel.local_theory_to_proof NONE NONE
-        (Interpretation.isar_interpretation_cmd expr equations)));
+        (Interpretation.isar_interpretation_cmd expr [])));
 
 in end\<close>