# HG changeset patch
# User ballarin
# Date 1520373540 -3600
# Node ID 2d3c1091527b8adf2ea7c2d89f336e9f8b296216
# Parent  44efac3d8638604b8842c2f5eb2e69d3d1d60846
Drop rewrite rule arguments of sublocale and interpretation implementations.

diff -r 44efac3d8638 -r 2d3c1091527b src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Mar 06 17:44:19 2018 +0100
+++ b/src/HOL/Statespace/state_space.ML	Tue Mar 06 22:59:00 2018 +0100
@@ -127,7 +127,7 @@
 
 fun prove_interpretation_in ctxt_tac (name, expr) thy =
    thy
-   |> Interpretation.global_sublocale_cmd (name, Position.none) (expression_no_pos expr) [] []
+   |> Interpretation.global_sublocale_cmd (name, Position.none) (expression_no_pos expr) []
    |> Proof.global_terminal_proof
          ((Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), Position.no_range), NONE)
    |> Proof_Context.theory_of
diff -r 44efac3d8638 -r 2d3c1091527b src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Tue Mar 06 17:44:19 2018 +0100
+++ b/src/Pure/Isar/interpretation.ML	Tue Mar 06 22:59:00 2018 +0100
@@ -8,39 +8,34 @@
 signature INTERPRETATION =
 sig
   type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
-  type 'a rewrites = (Attrib.binding * 'a) list
 
   (*interpretation in proofs*)
-  val interpret: Expression.expression_i -> term rewrites -> Proof.state -> Proof.state
-  val interpret_cmd: Expression.expression -> string rewrites -> Proof.state -> Proof.state
+  val interpret: Expression.expression_i -> Proof.state -> Proof.state
+  val interpret_cmd: Expression.expression -> Proof.state -> Proof.state
 
   (*interpretation in local theories*)
-  val interpretation: Expression.expression_i ->
-    term rewrites -> local_theory -> Proof.state
-  val interpretation_cmd: Expression.expression ->
-    string rewrites -> local_theory -> Proof.state
+  val interpretation: Expression.expression_i -> local_theory -> Proof.state
+  val interpretation_cmd: Expression.expression -> local_theory -> Proof.state
 
   (*interpretation into global theories*)
   val global_interpretation: Expression.expression_i ->
-    term defines -> term rewrites -> local_theory -> Proof.state
+    term defines -> local_theory -> Proof.state
   val global_interpretation_cmd: Expression.expression ->
-    string defines -> string rewrites -> local_theory -> Proof.state
+    string defines -> local_theory -> Proof.state
 
   (*interpretation between locales*)
   val sublocale: Expression.expression_i ->
-    term defines -> term rewrites -> local_theory -> Proof.state
+    term defines -> local_theory -> Proof.state
   val sublocale_cmd: Expression.expression ->
-    string defines -> string rewrites -> local_theory -> Proof.state
+    string defines -> local_theory -> Proof.state
   val global_sublocale: string -> Expression.expression_i ->
-    term defines -> term rewrites -> theory -> Proof.state
+    term defines -> theory -> Proof.state
   val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
-    string defines -> string rewrites -> theory -> Proof.state
+    string defines -> theory -> Proof.state
 
   (*mixed Isar interface*)
-  val isar_interpretation: Expression.expression_i ->
-    term rewrites -> local_theory -> Proof.state
-  val isar_interpretation_cmd: Expression.expression ->
-    string rewrites -> local_theory -> Proof.state
+  val isar_interpretation: Expression.expression_i -> local_theory -> Proof.state
+  val isar_interpretation_cmd: Expression.expression -> local_theory -> Proof.state
 end;
 
 structure Interpretation : INTERPRETATION =
@@ -49,7 +44,6 @@
 (** common interpretation machinery **)
 
 type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
-type 'a rewrites = 'a Expression.rewrites
 
 (* reading of locale expressions with rewrite morphisms *)
 
@@ -79,37 +73,22 @@
           map (singleton (Proof_Context.export inner_lthy' lthy') o Thm.symmetric) inner_defs
       in (def_eqns, lthy') end;
 
-fun prep_eqns _ _ [] _ _ = ([], [])
-  | prep_eqns prep_props prep_attr raw_eqns deps ctxt =
-      let
-        (* FIXME incompatibility, creating context for parsing rewrites equation may fail in
-           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;
-        val attrss = map (apsnd (map (prep_attr ctxt)) o fst) raw_eqns;
-      in (eqns, attrss) end;
-
-fun prep_interpretation prep_expr prep_term prep_props prep_attr
-  expression raw_defs raw_eqns initial_ctxt =
+fun prep_interpretation prep_expr prep_term
+  expression raw_defs initial_ctxt =
   let
     val ((propss, eq_propss, deps, eqnss, export), expr_ctxt) = prep_expr expression initial_ctxt;
     val (def_eqns, def_ctxt) =
       augment_with_defs prep_term raw_defs deps expr_ctxt;
-    val (eqns, attrss) = prep_eqns prep_props prep_attr raw_eqns deps def_ctxt;
-    val goal_ctxt = fold Variable.auto_fixes eqns def_ctxt;
-    val export' = Variable.export_morphism goal_ctxt expr_ctxt;
-  in (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) end;
+    val export' = Variable.export_morphism def_ctxt expr_ctxt;
+  in (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), def_ctxt) end;
 
 in
 
 fun cert_interpretation expression =
-  prep_interpretation Expression.cert_goal_expression Syntax.check_term
-    Syntax.check_props (K I) expression;
+  prep_interpretation Expression.cert_goal_expression Syntax.check_term expression;
 
 fun read_interpretation expression =
-  prep_interpretation Expression.read_goal_expression Syntax.read_term
-    Syntax.read_props Attrib.check_src expression;
+  prep_interpretation Expression.read_goal_expression Syntax.read_term expression;
 
 end;
 
@@ -121,18 +100,15 @@
 fun meta_rewrite eqns ctxt =
   (map (Local_Defs.abs_def_rule ctxt) (maps snd eqns), ctxt);
 
-fun note_eqns_register pos note activate deps eqnss witss def_eqns thms attrss export export' ctxt =
+fun note_eqns_register pos note activate deps eqnss witss def_eqns thms export export' ctxt =
   let
-    val (thmss, thms') = split_last (unflat ((map o map) fst eqnss @ [attrss]) thms);
+    val thmss = unflat ((map o map) fst eqnss) thms;
     val factss =
       map2 (map2 (fn b => fn eq => (b, [([Morphism.thm export eq], [])]))) ((map o map) fst eqnss) thmss;
     val (eqnss', ctxt') = fold_map (fn facts => note Thm.theoremK facts #-> meta_rewrite) factss ctxt;
-    val facts =
-      (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) ::
-        map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])]))
-          attrss thms';
+    val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
     val (eqns', ctxt'') = ctxt'
-      |> note Thm.theoremK facts
+      |> note Thm.theoremK [defs]
       |-> meta_rewrite;
     val dep_morphs =
       map2 (fn (dep, morph) => fn wits =>
@@ -149,14 +125,14 @@
 in
 
 fun generic_interpretation prep_interpretation setup_proof note add_registration
-    expression raw_defs raw_eqns initial_ctxt =
+    expression raw_defs initial_ctxt =
   let
-    val (((propss, eq_propss, deps, eqnss, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) =
-      prep_interpretation expression raw_defs raw_eqns initial_ctxt;
+    val (((propss, eq_propss, deps, eqnss, export, export'), def_eqns), goal_ctxt) =
+      prep_interpretation expression raw_defs initial_ctxt;
     val pos = Position.thread_data ();
     fun after_qed witss eqns =
-      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns attrss export export';
-  in setup_proof after_qed propss (flat (eq_propss @ [eqns])) goal_ctxt end;
+      note_eqns_register pos note add_registration deps eqnss witss def_eqns eqns export export';
+  in setup_proof after_qed propss (flat eq_propss) goal_ctxt end;
 
 end;
 
@@ -167,7 +143,7 @@
 
 local
 
-fun gen_interpret prep_interpretation expression raw_eqns state =
+fun gen_interpret prep_interpretation expression state =
   let
     val _ = Proof.assert_forward_or_chain state;
     fun lift_after_qed after_qed witss eqns =
@@ -182,7 +158,7 @@
   in
     Proof.context_of state
     |> generic_interpretation prep_interpretation setup_proof
-      Attrib.local_notes add_registration expression [] raw_eqns
+      Attrib.local_notes add_registration expression []
   end;
 
 in
@@ -228,7 +204,7 @@
 local
 
 fun gen_global_sublocale prep_loc prep_interpretation
-    raw_locale expression raw_defs raw_eqns thy =
+    raw_locale expression raw_defs thy =
   let
     val lthy = Named_Target.init (prep_loc thy raw_locale) thy;
     fun setup_proof after_qed =
@@ -237,7 +213,7 @@
   in
     lthy |>
       generic_interpretation prep_interpretation setup_proof
-        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns
+        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs
   end;
 
 in
@@ -260,9 +236,9 @@
   then Local_Theory.theory_registration
   else Locale.activate_fragment;
 
-fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy =
+fun gen_isar_interpretation prep_interpretation expression lthy =
   generic_interpretation prep_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind (register_or_activate lthy) expression [] raw_eqns lthy;
+    Local_Theory.notes_kind (register_or_activate lthy) expression [] lthy;
 
 in
 
diff -r 44efac3d8638 -r 2d3c1091527b src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Mar 06 17:44:19 2018 +0100
+++ b/src/Pure/Pure.thy	Tue Mar 06 22:59:00 2018 +0100
@@ -617,35 +617,34 @@
   Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
     "prove interpretation of locale expression in proof context"
     (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
-      Toplevel.proof (Interpretation.interpret_cmd 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)) >>
-      (fn x => (x, []))) ([], []));
+      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) ([]));
 
 val _ =
   Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
     "prove interpretation of locale expression into global theory"
-    (interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
-      Interpretation.global_interpretation_cmd expr defs equations));
+    (interpretation_args_with_defs >> (fn (expr, defs) =>
+      Interpretation.global_interpretation_cmd expr defs));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>sublocale\<close>
     "prove sublocale relation between a locale and a locale expression"
     ((Parse.position Parse.name --| (\<^keyword>\<open>\<subseteq>\<close> || \<^keyword>\<open><\<close>) --
-      interpretation_args_with_defs >> (fn (loc, (expr, (defs, equations))) =>
-        Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs equations)))
-    || interpretation_args_with_defs >> (fn (expr, (defs, equations)) =>
-        Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
+      interpretation_args_with_defs >> (fn (loc, (expr, defs)) =>
+        Toplevel.theory_to_proof (Interpretation.global_sublocale_cmd loc expr defs)))
+    || interpretation_args_with_defs >> (fn (expr, defs) =>
+        Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
     "prove interpretation of locale expression in local theory or into global theory"
     (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
       Toplevel.local_theory_to_proof NONE NONE
-        (Interpretation.isar_interpretation_cmd expr [])));
+        (Interpretation.isar_interpretation_cmd expr)));
 
 in end\<close>