# HG changeset patch # User ballarin # Date 1519996765 -3600 # Node ID b6ce18784872e0810fbfba8b5b892c22c2df7e67 # Parent e512938b853cfe2411bcf7876ada4374b0552ca6 Proper rewrite morphisms in locale instances. diff -r e512938b853c -r b6ce18784872 NEWS --- 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 *** diff -r e512938b853c -r b6ce18784872 src/Doc/Isar_Ref/Spec.thy --- 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 \ @{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') \} 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 ``\_\'' enables to omit the instantiation for a parameter inside a positional instantiation. @@ -487,6 +490,11 @@ ``\<^verbatim>\?\''). 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. \ @@ -622,7 +630,7 @@ \ -subsection \Locale interpretation\ +subsection \Locale interpretation \label{sec:locale-interpretation}\ text \ \begin{matharray}{rcl} @@ -642,15 +650,15 @@ into locales (\<^theory_text>\sublocale\). @{rail \ - @@{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} \ - definitions? equations? + (definitions rewrites?)? ; @@{command sublocale} (@{syntax name} ('<' | '\'))? @{syntax locale_expr} \ - definitions? equations? + (definitions rewrites?)? ; @@{command print_dependencies} '!'? @{syntax locale_expr} ; @@ -659,8 +667,6 @@ definitions: @'defines' (@{syntax thmdecl}? @{syntax name} \ @{syntax mixfix}? @'=' @{syntax term} + @'and'); - - equations: @'rewrites' (@{syntax thmdecl}? @{syntax prop} + @'and') \} The core of each interpretation command is a locale expression \expr\; 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 \eqns\ amend the morphism through which \expr\ 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>\rewrites eqns\ 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 \expr\ is interpreted with + rewrite rules. This is particularly useful for interpreting concepts + introduced through definitions. The equations must be proved the user. Given definitions \defs\ produce corresponding definitions in the local - theory's underlying target \<^emph>\and\ amend the morphism with the equations + theory's underlying target \<^emph>\and\ 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>\and\ connective, \defs\ are processed sequentially without mutual recursion. - \<^descr> \<^theory_text>\interpretation expr rewrites eqns\ interprets \expr\ into a local theory + \<^descr> \<^theory_text>\interpretation expr\ interprets \expr\ 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>\interpretation\ behaves identically to \<^theory_text>\global_interpretation\ then. - \<^descr> \<^theory_text>\interpret expr rewrites eqns\ interprets \expr\ into a proof context: + \<^descr> \<^theory_text>\interpret expr\ interprets \expr\ into a proof context: the interpretation and its declarations disappear when closing the current proof block. Note that for \<^theory_text>\interpret\ the \eqns\ 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>\for\ clause. - \<^descr> \<^theory_text>\sublocale name \ defines defs expr rewrites eqns\ interprets \expr\ + \<^descr> \<^theory_text>\sublocale name \ expr defines defs rewrites eqns\ interprets \expr\ into the locale \name\. A proof that the specification of \name\ implies the specification of \expr\ is required. As in the localized version of the theorem command, the proof is in the context of \name\. After the proof @@ -737,8 +744,8 @@ adds interpretations for \expr\ as well, with the same qualifier, although only for fragments of \expr\ that are not interpreted in the theory already. - Using equations \eqns\ or rewrite definitions \defs\ can help break infinite - chains induced by circular \<^theory_text>\sublocale\ declarations. + Using rewrite rules \eqns\ or rewrite definitions \defs\ can help break + infinite chains induced by circular \<^theory_text>\sublocale\ declarations. In a named context block the \<^theory_text>\sublocale\ command may also be used, but the locale argument must be omitted. The command then refers to the locale (or diff -r e512938b853c -r b6ce18784872 src/FOL/ex/Locale_Test/Locale_Test1.thy --- 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 \Rewrite morphisms in expressions\ -interpretation y: logic_o "(\)" "Not" replaces bool_logic_o2: "logic_o.lor_o((\), Not, x, y) \ x \ y" +interpretation y: logic_o "(\)" "Not" rewrites bool_logic_o2: "logic_o.lor_o((\), Not, x, y) \ x \ y" proof - show bool_logic_o: "PROP logic_o((\), Not)" by unfold_locales fast+ show "logic_o.lor_o((\), Not, x, y) \ x \ y" unfolding logic_o.lor_o_def [OF bool_logic_o] by fast diff -r e512938b853c -r b6ce18784872 src/Pure/Isar/element.ML --- 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 diff -r e512938b853c -r b6ce18784872 src/Pure/Isar/expression.ML --- 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; diff -r e512938b853c -r b6ce18784872 src/Pure/Isar/interpretation.ML --- 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; diff -r e512938b853c -r b6ce18784872 src/Pure/Isar/parse_spec.ML --- 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 diff -r e512938b853c -r b6ce18784872 src/Pure/Pure.thy --- 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 @@ "\" "]" "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>\rewrites\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []; - val _ = Outer_Syntax.command \<^command_keyword>\interpret\ "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>\defines\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" - -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\=\ -- Parse.term))) [] -- - Scan.optional - (\<^keyword>\rewrites\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []); + -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\=\ -- Parse.term)) + -- Scan.optional (\<^keyword>\rewrites\ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" + -- Parse.prop)) []) ([], [])); val _ = Outer_Syntax.local_theory_to_proof \<^command_keyword>\global_interpretation\ @@ -649,9 +644,9 @@ val _ = Outer_Syntax.command \<^command_keyword>\interpretation\ "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\