Drop rewrites after defines in interpretations.
authorballarin
Sun Mar 04 12:22:48 2018 +0100 (15 months ago)
changeset 677640f8cb5568b63
parent 67763 f4b1cf9e7010
child 67765 968f6891be62
Drop rewrites after defines in interpretations.
NEWS
src/Doc/Isar_Ref/Spec.thy
src/HOL/Library/FSet.thy
src/HOL/Library/Groups_Big_Fun.thy
src/Pure/Pure.thy
     1.1 --- a/NEWS	Sat Mar 03 22:33:25 2018 +0100
     1.2 +++ b/NEWS	Sun Mar 04 12:22:48 2018 +0100
     1.3 @@ -176,14 +176,14 @@
     1.4  (e.g. use 'find_theorems' or 'try' to figure this out).
     1.5  
     1.6  * Rewrites clauses (keyword 'rewrites') were moved into the locale
     1.7 -expression syntax, where they are part of locale instances.  Keyword
     1.8 -'for' now needs to occur after, not before 'rewrites'.
     1.9 -Minor INCOMPATIBILITY.
    1.10 -
    1.11 -* For rewrites clauses in locale expressions, if activating a locale
    1.12 -instance fails, fall back to reading the clause first.  This helps
    1.13 -avoiding qualified locale instances where the qualifier's sole purpose
    1.14 -is avoiding duplicate constant declarations.
    1.15 +expression syntax, where they are part of locale instances.  In
    1.16 +interpretation commands rewrites clauses now need to occur before
    1.17 +'for' and 'defines'.  Minor INCOMPATIBILITY.
    1.18 +
    1.19 +* For rewrites clauses, if activating a locale instance fails, fall
    1.20 +back to reading the clause first.  This helps avoid qualification of
    1.21 +locale instances where the qualifier's sole purpose is avoiding
    1.22 +duplicate constant declarations.
    1.23  
    1.24  
    1.25  *** Pure ***
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Sat Mar 03 22:33:25 2018 +0100
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Sun Mar 04 12:22:48 2018 +0100
     2.3 @@ -460,7 +460,8 @@
     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) rewrites?
     2.8 +    instance: (qualifier ':')? @{syntax name} (pos_insts | named_insts) \<newline>
     2.9 +      rewrites?
    2.10      ;
    2.11      qualifier: @{syntax name} ('?')?
    2.12      ;
    2.13 @@ -654,11 +655,10 @@
    2.14      ;
    2.15      @@{command interpret} @{syntax locale_expr}
    2.16      ;
    2.17 -    @@{command global_interpretation} @{syntax locale_expr} \<newline>
    2.18 -      (definitions rewrites?)?
    2.19 +    @@{command global_interpretation} @{syntax locale_expr} definitions?
    2.20      ;
    2.21      @@{command sublocale} (@{syntax name} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
    2.22 -      (definitions rewrites?)?
    2.23 +      definitions?
    2.24      ;
    2.25      @@{command print_dependencies} '!'? @{syntax locale_expr}
    2.26      ;
    2.27 @@ -681,11 +681,15 @@
    2.28    to simplify the proof obligations according to existing interpretations use
    2.29    methods @{method intro_locales} or @{method unfold_locales}.
    2.30  
    2.31 -  Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> can occur within expressions or, for
    2.32 -  some commands, as part of the command itself.  They amend the morphism
    2.33 -  through which a locale instance or expression \<open>expr\<close> is interpreted with
    2.34 -  rewrite rules. This is particularly useful for interpreting concepts
    2.35 -  introduced through definitions. The equations must be proved the user.
    2.36 +  Rewrites clauses \<^theory_text>\<open>rewrites eqns\<close> occur within expressions. They amend the
    2.37 +  morphism through which a locale instance is interpreted with rewrite rules,
    2.38 +  also called rewrite morphisms. This is particularly useful for interpreting
    2.39 +  concepts introduced through definitions. The equations must be proved the
    2.40 +  user. To enable syntax of the instantiated locale within the equation, while
    2.41 +  reading a locale expression, equations of a locale instance are read in a
    2.42 +  temporary context where the instance is already activated. If activation
    2.43 +  fails, typically due to duplicate constant declarations, processing falls
    2.44 +  back to reading the equation first.
    2.45  
    2.46    Given definitions \<open>defs\<close> produce corresponding definitions in the local
    2.47    theory's underlying target \<^emph>\<open>and\<close> amend the morphism with rewrite rules
    2.48 @@ -714,7 +718,7 @@
    2.49    proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
    2.50    universally quantified.
    2.51  
    2.52 -  \<^descr> \<^theory_text>\<open>global_interpretation defines defs rewrites eqns\<close> interprets \<open>expr\<close>
    2.53 +  \<^descr> \<^theory_text>\<open>global_interpretation defines defs\<close> interprets \<open>expr\<close>
    2.54    into a global theory.
    2.55  
    2.56    When adding declarations to locales, interpreted versions of these
    2.57 @@ -727,7 +731,7 @@
    2.58    free variable whose name is already bound in the context --- for example,
    2.59    because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
    2.60  
    2.61 -  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs rewrites eqns\<close> interprets \<open>expr\<close>
    2.62 +  \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs\<close> interprets \<open>expr\<close>
    2.63    into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the
    2.64    specification of \<open>expr\<close> is required. As in the localized version of the
    2.65    theorem command, the proof is in the context of \<open>name\<close>. After the proof
    2.66 @@ -744,7 +748,7 @@
    2.67    adds interpretations for \<open>expr\<close> as well, with the same qualifier, although
    2.68    only for fragments of \<open>expr\<close> that are not interpreted in the theory already.
    2.69  
    2.70 -  Using rewrite rules \<open>eqns\<close> or rewrite definitions \<open>defs\<close> can help break
    2.71 +  Rewrites clauses in the expression or rewrite definitions \<open>defs\<close> can help break
    2.72    infinite chains induced by circular \<^theory_text>\<open>sublocale\<close> declarations.
    2.73  
    2.74    In a named context block the \<^theory_text>\<open>sublocale\<close> command may also be used, but the
    2.75 @@ -787,13 +791,6 @@
    2.76    \end{warn}
    2.77  
    2.78    \begin{warn}
    2.79 -    Due to a technical limitation, the specific context of a interpretation
    2.80 -    given by a \<^theory_text>\<open>for\<close> clause can get lost between a \<^theory_text>\<open>defines\<close> and
    2.81 -    \<^theory_text>\<open>rewrites\<close> clause and must then be recovered manually using
    2.82 -    explicit sort constraints and quantified term variables.
    2.83 -  \end{warn}
    2.84 -
    2.85 -  \begin{warn}
    2.86      While \<^theory_text>\<open>interpretation (in c) \<dots>\<close> is admissible, it is not useful since
    2.87      its result is discarded immediately.
    2.88    \end{warn}
     3.1 --- a/src/HOL/Library/FSet.thy	Sat Mar 03 22:33:25 2018 +0100
     3.2 +++ b/src/HOL/Library/FSet.thy	Sun Mar 04 12:22:48 2018 +0100
     3.3 @@ -751,8 +751,8 @@
     3.4  context comm_monoid_add begin
     3.5  
     3.6  sublocale fsum: comm_monoid_fset plus 0
     3.7 +  rewrites "comm_monoid_set.F plus 0 = sum"
     3.8    defines fsum = fsum.F
     3.9 -  rewrites "comm_monoid_set.F plus 0 = sum"
    3.10  proof -
    3.11    show "comm_monoid_fset (+) 0" by standard
    3.12  
    3.13 @@ -797,8 +797,8 @@
    3.14  context linorder begin
    3.15  
    3.16  sublocale fMin: semilattice_order_fset min less_eq less
    3.17 +  rewrites "semilattice_set.F min = Min"
    3.18    defines fMin = fMin.F
    3.19 -  rewrites "semilattice_set.F min = Min"
    3.20  proof -
    3.21    show "semilattice_order_fset min (\<le>) (<)" by standard
    3.22  
    3.23 @@ -806,8 +806,8 @@
    3.24  qed
    3.25  
    3.26  sublocale fMax: semilattice_order_fset max greater_eq greater
    3.27 +  rewrites "semilattice_set.F max = Max"
    3.28    defines fMax = fMax.F
    3.29 -  rewrites "semilattice_set.F max = Max"
    3.30  proof -
    3.31    show "semilattice_order_fset max (\<ge>) (>)"
    3.32      by standard
     4.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Sat Mar 03 22:33:25 2018 +0100
     4.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Sun Mar 04 12:22:48 2018 +0100
     4.3 @@ -215,8 +215,8 @@
     4.4  begin
     4.5  
     4.6  sublocale Sum_any: comm_monoid_fun plus 0
     4.7 +  rewrites "comm_monoid_set.F plus 0 = sum"
     4.8    defines Sum_any = Sum_any.G
     4.9 -  rewrites "comm_monoid_set.F plus 0 = sum"
    4.10  proof -
    4.11    show "comm_monoid_fun plus 0" ..
    4.12    then interpret Sum_any: comm_monoid_fun plus 0 .
    4.13 @@ -282,8 +282,8 @@
    4.14  begin
    4.15  
    4.16  sublocale Prod_any: comm_monoid_fun times 1
    4.17 +  rewrites "comm_monoid_set.F times 1 = prod"
    4.18    defines Prod_any = Prod_any.G
    4.19 -  rewrites "comm_monoid_set.F times 1 = prod"
    4.20  proof -
    4.21    show "comm_monoid_fun times 1" ..
    4.22    then interpret Prod_any: comm_monoid_fun times 1 .
     5.1 --- a/src/Pure/Pure.thy	Sat Mar 03 22:33:25 2018 +0100
     5.2 +++ b/src/Pure/Pure.thy	Sun Mar 04 12:22:48 2018 +0100
     5.3 @@ -622,9 +622,8 @@
     5.4  val interpretation_args_with_defs =
     5.5    Parse.!!! Parse_Spec.locale_expression --
     5.6      (Scan.optional (\<^keyword>\<open>defines\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
     5.7 -      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term))
     5.8 -      -- Scan.optional (\<^keyword>\<open>rewrites\<close> |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
     5.9 -        -- Parse.prop)) []) ([], []));
    5.10 +      -- ((Parse.binding -- Parse.opt_mixfix') --| \<^keyword>\<open>=\<close> -- Parse.term)) >>
    5.11 +      (fn x => (x, []))) ([], []));
    5.12  
    5.13  val _ =
    5.14    Outer_Syntax.local_theory_to_proof \<^command_keyword>\<open>global_interpretation\<close>