# HG changeset patch # User ballarin # Date 1447877913 -3600 # Node ID e89cfc004f18fc7b2307e23ff21cd2c92a5fde59 # Parent 286c1741285c190116311a20e820622f8bc141ba Refine the supression of abbreviations for morphisms that are not identities. diff -r 286c1741285c -r e89cfc004f18 NEWS --- a/NEWS Wed Nov 18 17:37:00 2015 +0000 +++ b/NEWS Wed Nov 18 21:18:33 2015 +0100 @@ -314,6 +314,28 @@ * Keyword 'rewrites' identifies rewrite morphisms in interpretation commands. Previously, the keyword was 'where'. INCOMPATIBILITY. +* More gentle suppression of syntax along locale morphisms while +printing terms. Previously 'abbreviation' and 'notation' declarations +would be suppressed for morphisms except term identity. Now +'abbreviation' is also kept for morphims that only change the involved +parameters, and only 'notation' is suppressed. This can be of great +help when working with complex locale hierarchies, because proof +states are displayed much more succinctly. It also means that only +notation needs to be redeclared if desired, as illustrated by this +example: + + locale struct = fixes composition :: "'a => 'a => 'a" (infixl "\" 65) + begin + definition derived (infixl "\" 65) where ... + end + + locale morphism = + left: struct composition + right: struct composition' + for composition (infix "\" 65) and composition' (infix "\''" 65) + begin + notation right.derived ("\''") + end + * Command 'sublocale' accepts mixin definitions after keyword 'defines'. diff -r 286c1741285c -r e89cfc004f18 src/Doc/Locales/Examples1.thy --- a/src/Doc/Locales/Examples1.thy Wed Nov 18 17:37:00 2015 +0000 +++ b/src/Doc/Locales/Examples1.thy Wed Nov 18 21:18:33 2015 +0100 @@ -70,13 +70,13 @@ The prefix @{text int} is applied to all names introduced in locale conclusions including names introduced in definitions. The qualified name @{text int.less} is short for - the interpretation of the definition, which is @{term int.less}. + the interpretation of the definition, which is @{text "partial_order.less op \"}. Qualified name and expanded form may be used almost interchangeably.% -\footnote{Since @{term "op \"} is polymorphic, for @{term int.less} a +\footnote{Since @{term "op \"} is polymorphic, for @{text "partial_order.less op \"} a more general type will be inferred than for @{text int.less} which is over type @{typ int}.} - The latter is preferred on output, as for example in the theorem + The former is preferred on output, as for example in the theorem @{thm [source] int.less_le_trans}: @{thm [display, indent=2] int.less_le_trans} Both notations for the strict order are not satisfactory. The diff -r 286c1741285c -r e89cfc004f18 src/Doc/Locales/Examples3.thy --- a/src/Doc/Locales/Examples3.thy Wed Nov 18 17:37:00 2015 +0000 +++ b/src/Doc/Locales/Examples3.thy Wed Nov 18 21:18:33 2015 +0100 @@ -223,15 +223,13 @@ \hspace*{1em}@{thm [source] le'.less_le_trans}: @{thm [display, indent=4] le'.less_le_trans} - While there is infix syntax for the strict operation associated to + While there is infix syntax for the strict operation associated with @{term "op \"}, there is none for the strict version of @{term - "op \"}. The abbreviation @{text less} with its infix syntax is only + "op \"}. The syntax @{text "\"} for @{text less} is only available for the original instance it was declared for. We may - introduce the abbreviation @{text less'} with infix syntax~@{text \} - with the following declaration:\ + introduce infix syntax for @{text le'.less} with the following declaration:\ - abbreviation (in order_preserving) - less' (infixl "\" 50) where "less' \ partial_order.less le'" + notation (in order_preserving) le'.less (infixl "\" 50) text (in order_preserving) \Now the theorem is displayed nicely as @{thm [source] le'.less_le_trans}: @@ -306,8 +304,8 @@ context lattice_hom begin - abbreviation meet' (infixl "\''" 50) where "meet' \ le'.meet" - abbreviation join' (infixl "\''" 50) where "join' \ le'.join" + notation le'.meet (infixl "\''" 50) + notation le'.join (infixl "\''" 50) end text \The next example makes radical use of the short hand diff -r 286c1741285c -r e89cfc004f18 src/FOL/ex/Locale_Test/Locale_Test1.thy --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Nov 18 17:37:00 2015 +0000 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Wed Nov 18 21:18:33 2015 +0100 @@ -126,26 +126,7 @@ thm var.test_def -text \Under which circumstances term syntax remains active.\ - -locale "syntax" = - fixes p1 :: "'a => 'b" - and p2 :: "'b => o" -begin - -definition d1 :: "'a => o" where "d1(x) \ \ p2(p1(x))" -definition d2 :: "'b => o" where "d2(x) \ \ p2(x)" - -thm d1_def d2_def - -end - -thm syntax.d1_def syntax.d2_def - -locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o" -begin - -thm d1_def d2_def (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *) +text \Under which circumstances notation remains active.\ ML \ fun check_syntax ctxt thm expected = @@ -161,9 +142,28 @@ declare [[show_hyps]] +locale "syntax" = + fixes p1 :: "'a => 'b" + and p2 :: "'b => o" +begin + +definition d1 :: "'a => o" ("D1'(_')") where "d1(x) \ \ p2(p1(x))" +definition d2 :: "'b => o" ("D2'(_')") where "d2(x) \ \ p2(x)" + +thm d1_def d2_def + +end + +thm syntax.d1_def syntax.d2_def + +locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o" +begin + +thm d1_def d2_def (* should print as "D1(?x) <-> ..." and "D2(?x) <-> ..." *) + ML \ - check_syntax @{context} @{thm d1_def} "d1(?x) \ \ p2(p1(?x))"; - check_syntax @{context} @{thm d2_def} "d2(?x) \ \ p2(?x)"; + check_syntax @{context} @{thm d1_def} "D1(?x) \ \ p2(p1(?x))"; + check_syntax @{context} @{thm d2_def} "D2(?x) \ \ p2(?x)"; \ end @@ -172,11 +172,11 @@ begin thm d1_def d2_def - (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *) + (* should print as "d1(?x) <-> ..." and "D2(?x) <-> ..." *) ML \ - check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) \ \ p2(p3(?x))"; - check_syntax @{context} @{thm d2_def} "d2(?x) \ \ p2(?x)"; + check_syntax @{context} @{thm d1_def} "d1(?x) \ \ p2(p3(?x))"; + check_syntax @{context} @{thm d2_def} "D2(?x) \ \ p2(?x)"; \ end diff -r 286c1741285c -r e89cfc004f18 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Wed Nov 18 17:37:00 2015 +0000 +++ b/src/Pure/Isar/generic_target.ML Wed Nov 18 21:18:33 2015 +0100 @@ -112,12 +112,17 @@ else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); +fun same_const (Const (c, _), Const (c', _)) = c = c' + | same_const (t $ _, t' $ _) = same_const (t, t') + | same_const (_, _) = false; + fun const_decl phi_pred prmode ((b, mx), rhs) phi context = if phi_pred phi then let val b' = Morphism.binding phi b; val rhs' = Morphism.term phi rhs; val same_shape = Term.aconv_untyped (rhs, rhs'); + val same_stem = same_shape orelse same_const (rhs, rhs'); val const_alias = if same_shape then (case rhs' of @@ -141,9 +146,9 @@ | NONE => context |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs') - |-> (fn (const as Const (c, _), _) => same_shape ? + |-> (fn (const as Const (c, _), _) => same_stem ? (Proof_Context.generic_revert_abbrev (#1 prmode) c #> - Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) + same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) end else context;