Refine the supression of abbreviations for morphisms that are not identities.
authorballarin
Wed Nov 18 21:18:33 2015 +0100 (2015-11-18)
changeset 61701e89cfc004f18
parent 61700 286c1741285c
child 61702 2e89bc578935
Refine the supression of abbreviations for morphisms that are not identities.
NEWS
src/Doc/Locales/Examples1.thy
src/Doc/Locales/Examples3.thy
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/Pure/Isar/generic_target.ML
     1.1 --- a/NEWS	Wed Nov 18 17:37:00 2015 +0000
     1.2 +++ b/NEWS	Wed Nov 18 21:18:33 2015 +0100
     1.3 @@ -314,6 +314,28 @@
     1.4  * Keyword 'rewrites' identifies rewrite morphisms in interpretation
     1.5  commands.  Previously, the keyword was 'where'.  INCOMPATIBILITY.
     1.6  
     1.7 +* More gentle suppression of syntax along locale morphisms while
     1.8 +printing terms.  Previously 'abbreviation' and 'notation' declarations
     1.9 +would be suppressed for morphisms except term identity.  Now
    1.10 +'abbreviation' is also kept for morphims that only change the involved
    1.11 +parameters, and only 'notation' is suppressed.  This can be of great
    1.12 +help when working with complex locale hierarchies, because proof
    1.13 +states are displayed much more succinctly.  It also means that only
    1.14 +notation needs to be redeclared if desired, as illustrated by this
    1.15 +example:
    1.16 +
    1.17 +  locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\<cdot>" 65)
    1.18 +  begin
    1.19 +    definition derived (infixl "\<odot>" 65) where ...
    1.20 +  end
    1.21 +
    1.22 +  locale morphism =
    1.23 +    left: struct composition + right: struct composition'
    1.24 +    for composition (infix "\<cdot>" 65) and composition' (infix "\<cdot>''" 65)
    1.25 +  begin
    1.26 +    notation right.derived ("\<odot>''")
    1.27 +  end
    1.28 +
    1.29  * Command 'sublocale' accepts mixin definitions after keyword
    1.30  'defines'.
    1.31  
     2.1 --- a/src/Doc/Locales/Examples1.thy	Wed Nov 18 17:37:00 2015 +0000
     2.2 +++ b/src/Doc/Locales/Examples1.thy	Wed Nov 18 21:18:33 2015 +0100
     2.3 @@ -70,13 +70,13 @@
     2.4    The prefix @{text int} is applied to all names introduced in locale
     2.5    conclusions including names introduced in definitions.  The
     2.6    qualified name @{text int.less} is short for
     2.7 -  the interpretation of the definition, which is @{term int.less}.
     2.8 +  the interpretation of the definition, which is @{text "partial_order.less op \<le>"}.
     2.9    Qualified name and expanded form may be used almost
    2.10    interchangeably.%
    2.11 -\footnote{Since @{term "op \<le>"} is polymorphic, for @{term int.less} a
    2.12 +\footnote{Since @{term "op \<le>"} is polymorphic, for @{text "partial_order.less op \<le>"} a
    2.13    more general type will be inferred than for @{text int.less} which
    2.14    is over type @{typ int}.}
    2.15 -  The latter is preferred on output, as for example in the theorem
    2.16 +  The former is preferred on output, as for example in the theorem
    2.17    @{thm [source] int.less_le_trans}: @{thm [display, indent=2]
    2.18    int.less_le_trans}
    2.19    Both notations for the strict order are not satisfactory.  The
     3.1 --- a/src/Doc/Locales/Examples3.thy	Wed Nov 18 17:37:00 2015 +0000
     3.2 +++ b/src/Doc/Locales/Examples3.thy	Wed Nov 18 21:18:33 2015 +0100
     3.3 @@ -223,15 +223,13 @@
     3.4  
     3.5    \hspace*{1em}@{thm [source] le'.less_le_trans}:
     3.6    @{thm [display, indent=4] le'.less_le_trans}
     3.7 -  While there is infix syntax for the strict operation associated to
     3.8 +  While there is infix syntax for the strict operation associated with
     3.9    @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
    3.10 -  "op \<preceq>"}.  The abbreviation @{text less} with its infix syntax is only
    3.11 +  "op \<preceq>"}.  The syntax @{text "\<sqsubset>"} for @{text less} is only
    3.12    available for the original instance it was declared for.  We may
    3.13 -  introduce the abbreviation @{text less'} with infix syntax~@{text \<prec>}
    3.14 -  with the following declaration:\<close>
    3.15 +  introduce infix syntax for @{text le'.less} with the following declaration:\<close>
    3.16  
    3.17 -  abbreviation (in order_preserving)
    3.18 -    less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
    3.19 +  notation (in order_preserving) le'.less (infixl "\<prec>" 50)
    3.20  
    3.21  text (in order_preserving) \<open>Now the theorem is displayed nicely as
    3.22    @{thm [source]  le'.less_le_trans}:
    3.23 @@ -306,8 +304,8 @@
    3.24  
    3.25    context lattice_hom
    3.26    begin
    3.27 -  abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
    3.28 -  abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
    3.29 +  notation le'.meet (infixl "\<sqinter>''" 50)
    3.30 +  notation le'.join (infixl "\<squnion>''" 50)
    3.31    end
    3.32  
    3.33  text \<open>The next example makes radical use of the short hand
     4.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Nov 18 17:37:00 2015 +0000
     4.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed Nov 18 21:18:33 2015 +0100
     4.3 @@ -126,26 +126,7 @@
     4.4  thm var.test_def
     4.5  
     4.6  
     4.7 -text \<open>Under which circumstances term syntax remains active.\<close>
     4.8 -
     4.9 -locale "syntax" =
    4.10 -  fixes p1 :: "'a => 'b"
    4.11 -    and p2 :: "'b => o"
    4.12 -begin
    4.13 -
    4.14 -definition d1 :: "'a => o" where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
    4.15 -definition d2 :: "'b => o" where "d2(x) \<longleftrightarrow> \<not> p2(x)"
    4.16 -
    4.17 -thm d1_def d2_def
    4.18 -
    4.19 -end
    4.20 -
    4.21 -thm syntax.d1_def syntax.d2_def
    4.22 -
    4.23 -locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
    4.24 -begin
    4.25 -
    4.26 -thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
    4.27 +text \<open>Under which circumstances notation remains active.\<close>
    4.28  
    4.29  ML \<open>
    4.30    fun check_syntax ctxt thm expected =
    4.31 @@ -161,9 +142,28 @@
    4.32  
    4.33  declare [[show_hyps]]
    4.34  
    4.35 +locale "syntax" =
    4.36 +  fixes p1 :: "'a => 'b"
    4.37 +    and p2 :: "'b => o"
    4.38 +begin
    4.39 +
    4.40 +definition d1 :: "'a => o" ("D1'(_')") where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
    4.41 +definition d2 :: "'b => o" ("D2'(_')") where "d2(x) \<longleftrightarrow> \<not> p2(x)"
    4.42 +
    4.43 +thm d1_def d2_def
    4.44 +
    4.45 +end
    4.46 +
    4.47 +thm syntax.d1_def syntax.d2_def
    4.48 +
    4.49 +locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
    4.50 +begin
    4.51 +
    4.52 +thm d1_def d2_def  (* should print as "D1(?x) <-> ..." and "D2(?x) <-> ..." *)
    4.53 +
    4.54  ML \<open>
    4.55 -  check_syntax @{context} @{thm d1_def} "d1(?x) \<longleftrightarrow> \<not> p2(p1(?x))";
    4.56 -  check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)";
    4.57 +  check_syntax @{context} @{thm d1_def} "D1(?x) \<longleftrightarrow> \<not> p2(p1(?x))";
    4.58 +  check_syntax @{context} @{thm d2_def} "D2(?x) \<longleftrightarrow> \<not> p2(?x)";
    4.59  \<close>
    4.60  
    4.61  end
    4.62 @@ -172,11 +172,11 @@
    4.63  begin
    4.64  
    4.65  thm d1_def d2_def
    4.66 -  (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
    4.67 +  (* should print as "d1(?x) <-> ..." and "D2(?x) <-> ..." *)
    4.68  
    4.69  ML \<open>
    4.70 -  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) \<longleftrightarrow> \<not> p2(p3(?x))";
    4.71 -  check_syntax @{context} @{thm d2_def} "d2(?x) \<longleftrightarrow> \<not> p2(?x)";
    4.72 +  check_syntax @{context} @{thm d1_def} "d1(?x) \<longleftrightarrow> \<not> p2(p3(?x))";
    4.73 +  check_syntax @{context} @{thm d2_def} "D2(?x) \<longleftrightarrow> \<not> p2(?x)";
    4.74  \<close>
    4.75  
    4.76  end
     5.1 --- a/src/Pure/Isar/generic_target.ML	Wed Nov 18 17:37:00 2015 +0000
     5.2 +++ b/src/Pure/Isar/generic_target.ML	Wed Nov 18 21:18:33 2015 +0100
     5.3 @@ -112,12 +112,17 @@
     5.4    else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^
     5.5      Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn);
     5.6  
     5.7 +fun same_const (Const (c, _), Const (c', _)) = c = c'
     5.8 +  | same_const (t $ _, t' $ _) = same_const (t, t')
     5.9 +  | same_const (_, _) = false;
    5.10 +
    5.11  fun const_decl phi_pred prmode ((b, mx), rhs) phi context =
    5.12    if phi_pred phi then
    5.13      let
    5.14        val b' = Morphism.binding phi b;
    5.15        val rhs' = Morphism.term phi rhs;
    5.16        val same_shape = Term.aconv_untyped (rhs, rhs');
    5.17 +      val same_stem = same_shape orelse same_const (rhs, rhs');
    5.18        val const_alias =
    5.19          if same_shape then
    5.20            (case rhs' of
    5.21 @@ -141,9 +146,9 @@
    5.22        | NONE =>
    5.23            context
    5.24            |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs')
    5.25 -          |-> (fn (const as Const (c, _), _) => same_shape ?
    5.26 +          |-> (fn (const as Const (c, _), _) => same_stem ?
    5.27                  (Proof_Context.generic_revert_abbrev (#1 prmode) c #>
    5.28 -                 Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
    5.29 +                 same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)]))))
    5.30      end
    5.31    else context;
    5.32