Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Printing a term without abbreviations/notation


view this post on Zulip Email Gateway (Apr 20 2021 at 09:31):

From: Manuel Eberl <eberlm@in.tum.de>
Hello,

abbreviations can sometimes make terms a bit intransparent if you don't
know what they mean, e.g.

"∀⇩F n in sequentially. ln (real n) > 0"

is internally

"eventually (λn. 0 < ln (real n)) sequentially"

but this is not so easy to find out. You cannot even ctrl+click on
anything due to the custom syntax.

So, is there an easy way to print a term

  1. without any abbreviations, but with notation (e.g. I don't want to
    see "plus x y" instead of "x + y")

  2. without abbreviations and without notation (i.e. "plus x y" instead
    of "x + y")

The closest thing I am aware of is to do something like

ML_val ‹@{term "∀⇩F n in sequentially. n > 0"}›

Manuel
smime.p7s

view this post on Zulip Email Gateway (Apr 20 2021 at 10:59):

From: Dominique Unruh <unruh@ut.ee>
You could try

ML_val ‹
Syntax.string_of_term_global \<^theory>‹Main› \<^term>‹∀⇩F n in
sequentially. n > 0› |> writeln

It's not optimal, but probably more readable that your approach. And you
can replace Main by other theories to fine-tune the amount of syntax.
(E.g., Pure for no syntactic sugar.) Main drawback are annoying question
marks in the latter case.

Best wishes,
Dominique.

view this post on Zulip Email Gateway (Apr 20 2021 at 11:04):

From: Manuel Eberl <eberlm@in.tum.de>
I think we should really strive for something more nice-to-use and
"official". Two more people have written to me privately that they would
really want to have something like this.

Manuel

view this post on Zulip Email Gateway (Apr 20 2021 at 11:11):

From: Peter Lammich <lammich@in.tum.de>
I'm also using an "inofficial" hack if the term structure is not clear
to me, and would like to see something that works better and reliably.

view this post on Zulip Email Gateway (Jul 07 2021 at 14:13):

From: Mikhail Mandrykin <mandrykin@ispras.ru>
I recently tackled with similar situations and for now implemented a
workaround/hack that works quite acceptably for me. It declares a
configuration option "bypass_translations" similar to "show_abbrevs",
and the option, when enabled, prevents print_translations and
print_ast_translations from being applied by temporarily prefixing all
constant names with a relatively uncommon symbol (e.g. '@'). Meanwhile,
it leaves alone the constants that have the type "prop" as their
argument or result types. This option is relatively convenient as it
works well for goal statements, retains trivial infix notations (but not
binders and more complex stuff) and notations from the Pure kernel (e.g.
‹⟦…⟧›). Usually it's enough to add ‹using [[show_abbrevs=false,
bypass_translations=true]]› to enable it temporarily for the current
goal. Attached the theory and a sample goal snapshot

Regards,
Mikhail

Peter Lammich писал 2021-04-20 14:11:
Bypass_Translations.thy
goal_untranslated.png
goal_translated.png


Last updated: Sep 25 2021 at 09:17 UTC