Proper rewrite morphisms in locale instances.
authorballarin
Fri Mar 02 14:19:25 2018 +0100 (15 months ago)
changeset 67740b6ce18784872
parent 67739 e512938b853c
child 67741 d5a7f2c54655
Proper rewrite morphisms in locale instances.
NEWS
src/Doc/Isar_Ref/Spec.thy
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/interpretation.ML
src/Pure/Isar/parse_spec.ML
src/Pure/Pure.thy
     1.1 --- a/NEWS	Thu Mar 01 20:44:38 2018 +0100
     1.2 +++ b/NEWS	Fri Mar 02 14:19:25 2018 +0100
     1.3 @@ -175,6 +175,11 @@
     1.4  Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
     1.5  (e.g. use 'find_theorems' or 'try' to figure this out).
     1.6  
     1.7 +* Rewrites clauses (keyword 'rewrites') were moved into the locale
     1.8 +expression syntax, where they are part of locale instances.  Keyword
     1.9 +'for' now needs to occur after, not before 'rewrites'.
    1.10 +Minor INCOMPATIBILITY.
    1.11 +
    1.12  
    1.13  *** Pure ***
    1.14  
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu Mar 01 20:44:38 2018 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Fri Mar 02 14:19:25 2018 +0100
     2.3 @@ -460,17 +460,20 @@
     2.4    @{rail \<open>
     2.5      @{syntax_def locale_expr}: (instance + '+') @{syntax for_fixes}
     2.6      ;
     2.7 -    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts)
     2.8 +    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) rewrites?
     2.9      ;
    2.10      qualifier: @{syntax name} ('?')?
    2.11      ;
    2.12      pos_insts: ('_' | @{syntax term})*
    2.13      ;
    2.14      named_insts: @'where' (@{syntax name} '=' @{syntax term} + @'and')
    2.15 +    ;
    2.16 +    rewrites: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
    2.17    \<close>}
    2.18  
    2.19    A locale instance consists of a reference to a locale and either positional
    2.20 -  or named parameter instantiations. Identical instantiations (that is, those
    2.21 +  or named parameter instantiations optionally followed by rewrites clauses.
    2.22 +  Identical instantiations (that is, those
    2.23    that instantiate a parameter by itself) may be omitted. The notation ``\<open>_\<close>''
    2.24    enables to omit the instantiation for a parameter inside a positional
    2.25    instantiation.
    2.26 @@ -487,6 +490,11 @@
    2.27    ``\<^verbatim>\<open>?\<close>''). Non-mandatory means that the qualifier may be omitted on input.
    2.28    Qualifiers only affect name spaces; they play no role in determining whether
    2.29    one locale instance subsumes another.
    2.30 +
    2.31 +  Rewrite clauses amend instances with equations that act as rewrite rules.
    2.32 +  This is particularly useful for changing concepts introduced through
    2.33 +  definitions. Rewrite clauses are available only in interpretation commands
    2.34 +  (see \secref{sec:locale-interpretation} below) and must be proved the user.
    2.35  \<close>
    2.36  
    2.37  
    2.38 @@ -622,7 +630,7 @@
    2.39  \<close>
    2.40  
    2.41  
    2.42 -subsection \<open>Locale interpretation\<close>
    2.43 +subsection \<open>Locale interpretation \label{sec:locale-interpretation}\<close>
    2.44  
    2.45  text \<open>
    2.46    \begin{matharray}{rcl}
    2.47 @@ -642,15 +650,15 @@
    2.48    into locales (\<^theory_text>\<open>sublocale\<close>).
    2.49  
    2.50    @{rail \<open>
    2.51 -    @@{command interpretation} @{syntax locale_expr} equations?
    2.52 +    @@{command interpretation} @{syntax locale_expr}
    2.53      ;
    2.54 -    @@{command interpret} @{syntax locale_expr} equations?
    2.55 +    @@{command interpret} @{syntax locale_expr}
    2.56      ;
    2.57      @@{command global_interpretation} @{syntax locale_expr} \<newline>
    2.58 -      definitions? equations?
    2.59 +      (definitions rewrites?)?
    2.60      ;
    2.61      @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
    2.62 -      definitions? equations?
    2.63 +      (definitions rewrites?)?
    2.64      ;
    2.65      @@{command print_dependencies} '!'? @{syntax locale_expr}
    2.66      ;
    2.67 @@ -659,8 +667,6 @@
    2.68  
    2.69      definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \<newline>
    2.70        @{syntax mixfix}? @'=' @{syntax term} + @'and');
    2.71 -
    2.72 -    equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and')
    2.73    \<close>}
    2.74  
    2.75    The core of each interpretation command is a locale expression \<open>expr\<close>; the
    2.76 @@ -675,13 +681,14 @@
    2.77    to simplify the proof obligations according to existing interpretations use
    2.78    methods @{method intro_locales} or @{method unfold_locales}.
    2.79  
    2.80 -  Given equations \<open>eqns\<close> amend the morphism through which \<open>expr\<close> is
    2.81 -  interpreted, adding rewrite rules. This is particularly useful for
    2.82 -  interpreting concepts introduced through definitions. The equations must be
    2.83 -  proved the user.
    2.84 +  Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> can occur within expressions or, for
    2.85 +  some commands, as part of the command itself.  They amend the morphism
    2.86 +  through which a locale instance or expression \<open>expr\<close> is interpreted with
    2.87 +  rewrite rules. This is particularly useful for interpreting concepts
    2.88 +  introduced through definitions. The equations must be proved the user.
    2.89  
    2.90    Given definitions \<open>defs\<close> produce corresponding definitions in the local
    2.91 -  theory's underlying target \<^emph>\<open>and\<close> amend the morphism with the equations
    2.92 +  theory's underlying target \<^emph>\<open>and\<close> amend the morphism with rewrite rules
    2.93    stemming from the symmetric of those definitions. Hence these need not be
    2.94    proved explicitly the user. Such rewrite definitions are a even more useful
    2.95    device for interpreting concepts introduced through definitions, but they
    2.96 @@ -690,7 +697,7 @@
    2.97    the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
    2.98    are processed sequentially without mutual recursion.
    2.99  
   2.100 -  \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory
   2.101 +  \<^descr> \<^theory_text>\<open>interpretation expr\<close> interprets \<open>expr\<close> into a local theory
   2.102    such that its lifetime is limited to the current context block (e.g. a
   2.103    locale or unnamed context). At the closing @{command end} of the block the
   2.104    interpretation and its declarations disappear. Hence facts based on
   2.105 @@ -702,7 +709,7 @@
   2.106    context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to
   2.107    \<^theory_text>\<open>global_interpretation\<close> then.
   2.108  
   2.109 -  \<^descr> \<^theory_text>\<open>interpret expr rewrites eqns\<close> interprets \<open>expr\<close> into a proof context:
   2.110 +  \<^descr> \<^theory_text>\<open>interpret expr\<close> interprets \<open>expr\<close> into a proof context:
   2.111    the interpretation and its declarations disappear when closing the current
   2.112    proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
   2.113    universally quantified.
   2.114 @@ -720,7 +727,7 @@
   2.115    free variable whose name is already bound in the context --- for example,
   2.116    because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
   2.117  
   2.118 -  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> defines defs expr rewrites eqns\<close> interprets \<open>expr\<close>
   2.119 +  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs rewrites eqns\<close> interprets \<open>expr\<close>
   2.120    into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the
   2.121    specification of \<open>expr\<close> is required. As in the localized version of the
   2.122    theorem command, the proof is in the context of \<open>name\<close>. After the proof
   2.123 @@ -737,8 +744,8 @@
   2.124    adds interpretations for \<open>expr\<close> as well, with the same qualifier, although
   2.125    only for fragments of \<open>expr\<close> that are not interpreted in the theory already.
   2.126  
   2.127 -  Using equations \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can help break infinite
   2.128 -  chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.
   2.129 +  Using rewrite rules \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can help break
   2.130 +  infinite chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.
   2.131  
   2.132    In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the
   2.133    locale argument must be omitted. The command then refers to the locale (or
     3.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu Mar 01 20:44:38 2018 +0100
     3.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Fri Mar 02 14:19:25 2018 +0100
     3.3 @@ -523,7 +523,7 @@
     3.4  
     3.5  subsection \<open>Rewrite morphisms in expressions\<close>
     3.6  
     3.7 -interpretation y: logic_o "(\<or>)" "Not" replaces bool_logic_o2: "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y"
     3.8 +interpretation y: logic_o "(\<or>)" "Not" rewrites bool_logic_o2: "logic_o.lor_o((\<or>), Not, x, y) \<longleftrightarrow> x \<and> y"
     3.9  proof -
    3.10    show bool_logic_o: "PROP logic_o((\<or>), Not)" by unfold_locales fast+
    3.11    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
     4.1 --- a/src/Pure/Isar/element.ML	Thu Mar 01 20:44:38 2018 +0100
     4.2 +++ b/src/Pure/Isar/element.ML	Fri Mar 02 14:19:25 2018 +0100
     4.3 @@ -50,6 +50,7 @@
     4.4    val instantiate_normalize_morphism:
     4.5      ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
     4.6    val satisfy_morphism: witness list -> morphism
     4.7 +  val eq_term_morphism: theory -> term list -> morphism option
     4.8    val eq_morphism: theory -> thm list -> morphism option
     4.9    val init: context_i -> Context.generic -> Context.generic
    4.10    val activate_i: context_i -> Proof.context -> context_i * Proof.context
    4.11 @@ -381,6 +382,26 @@
    4.12  
    4.13  (* rewriting with equalities *)
    4.14  
    4.15 +(* for activating declarations only *)
    4.16 +fun eq_term_morphism _ [] = NONE
    4.17 +  | eq_term_morphism thy props =
    4.18 +      let
    4.19 +        fun decomp_simp prop =
    4.20 +          let
    4.21 +            val ctxt = Proof_Context.init_global thy;
    4.22 +            val _ = Logic.count_prems prop = 0 orelse
    4.23 +              error ("Bad conditional rewrite rule " ^ Syntax.string_of_term ctxt prop);
    4.24 +            val lhsrhs = Logic.dest_equals prop
    4.25 +              handle TERM _ => error ("Rewrite rule not a meta-equality " ^ Syntax.string_of_term ctxt prop);
    4.26 +          in lhsrhs end;
    4.27 +        val phi =
    4.28 +          Morphism.morphism "Element.eq_term_morphism"
    4.29 +           {binding = [],
    4.30 +            typ = [],
    4.31 +            term = [Pattern.rewrite_term thy (map decomp_simp props) []],
    4.32 +            fact = [fn _ => error "Illegal application of Element.eq_term_morphism"]};
    4.33 +      in SOME phi end;
    4.34 +
    4.35  fun eq_morphism _ [] = NONE
    4.36    | eq_morphism thy thms =
    4.37        let
     5.1 --- a/src/Pure/Isar/expression.ML	Thu Mar 01 20:44:38 2018 +0100
     5.2 +++ b/src/Pure/Isar/expression.ML	Fri Mar 02 14:19:25 2018 +0100
     5.3 @@ -8,7 +8,8 @@
     5.4  sig
     5.5    (* Locale expressions *)
     5.6    datatype 'term map = Positional of 'term option list | Named of (string * 'term) list
     5.7 -  type ('name, 'term) expr = ('name * ((string * bool) * ('term map * (Attrib.binding * 'term) list))) list
     5.8 +  type 'term rewrites = (Attrib.binding * 'term) list
     5.9 +  type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list
    5.10    type expression_i = (string, term) expr * (binding * typ option * mixfix) list
    5.11    type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list
    5.12  
    5.13 @@ -58,7 +59,9 @@
    5.14    Positional of 'term option list |
    5.15    Named of (string * 'term) list;
    5.16  
    5.17 -type ('name, 'term) expr = ('name * ((string * bool) * ('term map * (Attrib.binding * 'term) list))) list;
    5.18 +type 'term rewrites = (Attrib.binding * 'term) list;
    5.19 +
    5.20 +type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list;
    5.21  
    5.22  type expression_i = (string, term) expr * (binding * typ option * mixfix) list;
    5.23  type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list;
    5.24 @@ -367,8 +370,11 @@
    5.25  
    5.26  local
    5.27  
    5.28 +fun abs_def ctxt =
    5.29 +  Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of;
    5.30 +
    5.31  fun prep_full_context_statement
    5.32 -    parse_typ parse_prop prep_obtains prep_var_elem prep_inst parse_eqn prep_var_inst prep_expr
    5.33 +    parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr
    5.34      {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 =
    5.35    let
    5.36      val thy = Proof_Context.theory_of ctxt1;
    5.37 @@ -379,23 +385,29 @@
    5.38        let
    5.39          val params = map #1 (Locale.params_of thy loc);
    5.40          val inst' = prep_inst ctxt (map #1 params) inst;
    5.41 -        val eqns' = map (apsnd (parse_eqn ctxt)) eqns;
    5.42          val parm_types' =
    5.43            params |> map (#2 #> Logic.varifyT_global #>
    5.44                Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #>
    5.45                Type_Infer.paramify_vars);
    5.46          val inst'' = map2 Type.constraint parm_types' inst';
    5.47          val insts' = insts @ [(loc, (prfx, inst''))];
    5.48 -        val eqnss' = eqnss @ [eqns'];
    5.49 -        val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt;
    5.50 -        val (inst_morph, _) = inst_morphism params (prfx, #2 (#2 (List.last insts''))) ctxt;
    5.51 -        val rewrite_morph =
    5.52 -          List.last eqnss''
    5.53 -          |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt)
    5.54 -          |> Element.eq_morphism (Proof_Context.theory_of ctxt)
    5.55 +        val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt;
    5.56 +        val inst''' = insts'' |> List.last |> snd |> snd;
    5.57 +        val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt;
    5.58 +        val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2; (* may fail *)
    5.59 +
    5.60 +        val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns;
    5.61 +        val eqns' = (prep_eqns ctxt' o map snd) eqns;
    5.62 +        val eqnss' = [attrss ~~ eqns'];
    5.63 +        val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt';
    5.64 +        val rewrite_morph = eqns'
    5.65 +          |> map (abs_def ctxt')
    5.66 +          |> Variable.export_terms ctxt' ctxt
    5.67 +          |> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
    5.68            |> the_default Morphism.identity;
    5.69 -        val ctxt' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
    5.70 -      in (i + 1, insts', eqnss', ctxt') end;
    5.71 +       val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
    5.72 +       val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
    5.73 +      in (i + 1, insts', eqnss', ctxt'') end;
    5.74  
    5.75      fun prep_elem raw_elem ctxt =
    5.76        let
    5.77 @@ -411,7 +423,7 @@
    5.78      val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2);
    5.79  
    5.80      fun prep_stmt elems ctxt =
    5.81 -      check_autofix insts' eqnss' elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
    5.82 +      check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt;
    5.83  
    5.84      val _ =
    5.85        if fixed_frees then ()
    5.86 @@ -421,7 +433,7 @@
    5.87          | frees => error ("Illegal free variables in expression: " ^
    5.88              commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees))));
    5.89  
    5.90 -    val ((insts, eqnss, elems', concl), ctxt4) = ctxt3
    5.91 +    val ((insts, _, elems', concl), ctxt4) = ctxt3
    5.92        |> init_body
    5.93        |> fold_map prep_elem raw_elems
    5.94        |-> prep_stmt;
    5.95 @@ -438,21 +450,21 @@
    5.96      val deps = map (finish_inst ctxt5) insts;
    5.97      val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems';
    5.98  
    5.99 -  in ((fixed, deps, eqnss, elems'', concl), (parms, ctxt5)) end;
   5.100 +  in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end;
   5.101  
   5.102  in
   5.103  
   5.104  fun cert_full_context_statement x =
   5.105    prep_full_context_statement (K I) (K I) Obtain.cert_obtains
   5.106 -    Proof_Context.cert_var make_inst (K I) Proof_Context.cert_var (K I) x;
   5.107 +    Proof_Context.cert_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x;
   5.108  
   5.109  fun cert_read_full_context_statement x =
   5.110    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
   5.111 -    Proof_Context.read_var make_inst (K I) Proof_Context.cert_var (K I) x;
   5.112 +    Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x;
   5.113  
   5.114  fun read_full_context_statement x =
   5.115    prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains
   5.116 -    Proof_Context.read_var parse_inst (Syntax.parse_prop) Proof_Context.read_var check_expr x;
   5.117 +    Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x;
   5.118  
   5.119  end;
   5.120  
   5.121 @@ -492,7 +504,7 @@
   5.122      val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) =
   5.123        prep {strict = false, do_close = true, fixed_frees = false}
   5.124          raw_import init_body raw_elems (Element.Shows []) ctxt;
   5.125 -    val _ = null (flat eqnss) orelse error "Illegal replaces clause(s) in declaration of locale";
   5.126 +    val _ = null (flat eqnss) orelse error "Illegal rewrites clause(s) in declaration of locale";
   5.127      (* Declare parameters and imported facts *)
   5.128      val ctxt' = ctxt
   5.129        |> fix_params fixed
   5.130 @@ -537,7 +549,7 @@
   5.131  
   5.132      val goal_ctxt = ctxt
   5.133        |> fix_params fixed
   5.134 -      |> (fold o fold) Variable.auto_fixes propss;
   5.135 +      |> (fold o fold) Variable.auto_fixes (propss @ eq_propss);
   5.136  
   5.137      val export = Variable.export_morphism goal_ctxt ctxt;
   5.138      val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
     6.1 --- a/src/Pure/Isar/interpretation.ML	Thu Mar 01 20:44:38 2018 +0100
     6.2 +++ b/src/Pure/Isar/interpretation.ML	Fri Mar 02 14:19:25 2018 +0100
     6.3 @@ -49,7 +49,7 @@
     6.4  (** common interpretation machinery **)
     6.5  
     6.6  type 'a defines = (Attrib.binding * ((binding * mixfix) * 'a)) list
     6.7 -type 'a rewrites = (Attrib.binding * 'a) list
     6.8 +type 'a rewrites = 'a Expression.rewrites
     6.9  
    6.10  (* reading of locale expressions with rewrite morphisms *)
    6.11  
    6.12 @@ -83,7 +83,7 @@
    6.13    | prep_eqns prep_props prep_attr raw_eqns deps ctxt =
    6.14        let
    6.15          (* FIXME incompatibility, creating context for parsing rewrites equation may fail in
    6.16 -           presence of replaces clause *)
    6.17 +           presence of rewrites clause in expression *)
    6.18          val ctxt' = fold Locale.activate_declarations deps ctxt;
    6.19          val eqns =
    6.20            (Variable.export_terms ctxt' ctxt o prep_props ctxt' o map snd) raw_eqns;
     7.1 --- a/src/Pure/Isar/parse_spec.ML	Thu Mar 01 20:44:38 2018 +0100
     7.2 +++ b/src/Pure/Isar/parse_spec.ML	Fri Mar 02 14:19:25 2018 +0100
     7.3 @@ -114,7 +114,7 @@
     7.4  val instance = Scan.optional (Parse.where_ |--
     7.5    Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
     7.6    Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional) (Expression.Named []) --
     7.7 -  (Scan.optional (Parse.$$$ "replaces" |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []);
     7.8 +  (Scan.optional (Parse.$$$ "rewrites" |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []);
     7.9  
    7.10  in
    7.11  
     8.1 --- a/src/Pure/Pure.thy	Thu Mar 01 20:44:38 2018 +0100
     8.2 +++ b/src/Pure/Pure.thy	Fri Mar 02 14:19:25 2018 +0100
     8.3 @@ -10,7 +10,7 @@
     8.4      "\<subseteq>" "]" "attach" "binder" "in" "infix" "infixl" "infixr" "is" "open" "output"
     8.5      "overloaded" "pervasive" "premises" "structure" "unchecked"
     8.6    and "private" "qualified" :: before_command
     8.7 -  and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "replaces" "rewrites"
     8.8 +  and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites"
     8.9      "obtains" "shows" "when" "where" "|" :: quasi_command
    8.10    and "text" "txt" :: document_body
    8.11    and "text_raw" :: document_raw
    8.12 @@ -613,23 +613,18 @@
    8.13        >> (fn elems =>
    8.14            Toplevel.begin_local_theory true (Experiment.experiment_cmd elems #> snd)));
    8.15  
    8.16 -val interpretation_args =
    8.17 -  Parse.!!! Parse_Spec.locale_expression --
    8.18 -    Scan.optional
    8.19 -      (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
    8.20 -
    8.21  val _ =
    8.22    Outer_Syntax.command \<^command_keyword>\<open>interpret\<close>
    8.23      "prove interpretation of locale expression in proof context"
    8.24 -    (interpretation_args >> (fn (expr, equations) =>
    8.25 -      Toplevel.proof (Interpretation.interpret_cmd expr equations)));
    8.26 +    (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
    8.27 +      Toplevel.proof (Interpretation.interpret_cmd expr [])));
    8.28  
    8.29  val interpretation_args_with_defs =
    8.30    Parse.!!! Parse_Spec.locale_expression --
    8.31      (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
    8.32 -      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))) [] --
    8.33 -    Scan.optional
    8.34 -      (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
    8.35 +      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))
    8.36 +      -- Scan.optional (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
    8.37 +        -- Parse.prop)) []) ([], []));
    8.38  
    8.39  val _ =
    8.40    Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>
    8.41 @@ -649,9 +644,9 @@
    8.42  val _ =
    8.43    Outer_Syntax.command \<^command_keyword>\<open>interpretation\<close>
    8.44      "prove interpretation of locale expression in local theory or into global theory"
    8.45 -    (interpretation_args >> (fn (expr, equations) =>
    8.46 +    (Parse.!!! Parse_Spec.locale_expression >> (fn expr =>
    8.47        Toplevel.local_theory_to_proof NONE NONE
    8.48 -        (Interpretation.isar_interpretation_cmd expr equations)));
    8.49 +        (Interpretation.isar_interpretation_cmd expr [])));
    8.50  
    8.51  in end\<close>
    8.52