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



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:
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.

--
  Peter

On Tue, 2021-04-20 at 13:03 +0200, Manuel Eberl wrote:
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


On 20/04/2021 12:59, Dominique Unruh wrote:
> 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.
>
>
>
> On 4/20/21 12:30 PM, Manuel Eberl wrote:
> > 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
> >
theory Bypass_Translations
  imports Main
begin

ML \<open>
signature BYPASS_TRANSLATIONS = sig
  val bypass_translations : bool Config.T
  val setup_bypass_translations : theory -> theory
end

structure Bypass_Translations : BYPASS_TRANSLATIONS = struct
  val bypass_prefix = "@"
  val (bypass_translations, setup_bypass_translations) = Attrib.config_bool \<^binding>\<open>bypass_translations\<close> (K false)
  fun bypass ctxt ts =
    if
      Config.get ctxt bypass_translations |> not orelse
      fold (fold_aterms (fn Const (c, _) => (fn acc => acc orelse String.isPrefix bypass_prefix c) | _ => I)) ts false
    then ts
    else
      map
        (map_aterms
          (fn t as Const (c, T)=>
                if strip_type T |> swap |-> cons |> forall (curry op <> \<^typ>\<open>prop\<close>) then
                  Const (prefix bypass_prefix c, T)
                else t
            | t => t))
        ts
   val () = Syntax_Phases.term_uncheck 101 "bypass all translations" bypass |> Context.>>

local
  open Ast
  fun detect (Constant c) = String.isPrefix bypass_prefix (perhaps (try Lexicon.unmark_const) c)
    | detect (Variable _) = false
    | detect (Appl l) = exists detect l
  fun restore (Constant c) =
        Constant (perhaps (try (Lexicon.unmark_const #> unprefix bypass_prefix #> Lexicon.mark_const)) c)
    | restore (v as Variable _) = v
    | restore (Appl l) = Appl (map restore l)
in
  val () =
    Sign.print_ast_translation
      [(\<^const_syntax>\<open>Trueprop\<close>,
        fn ctxt => fn args =>
          if Config.get ctxt bypass_translations andalso exists detect args then
            Ast.mk_appl (Ast.Constant \<^const_syntax>\<open>Trueprop\<close>) (map restore args)
          else raise Match)]
    |> Context.map_theory |> Context.>>
end
end
\<close>
setup \<open>Bypass_Translations.setup_bypass_translations\<close>

abbreviation (output) "Sum_list f xs \<equiv> sum_list (map f xs)"
print_translation \<open>[Syntax_Trans.preserve_binder_abs_tr' \<^const_syntax>\<open>Sum_list\<close> \<^const_syntax>\<open>Sum_list\<close>]\<close>
translations "\<Sum>x\<leftarrow>xs. b" \<leftharpoondown>"CONST Sum_list x b xs"

lemma "{u. P u} = {(a, b) | a b. P (a, b)}" using [[show_abbrevs=false, bypass_translations=true]] oops

prop "finite X \<Longrightarrow> (\<Sum>x\<in>X. \<Sum>y\<leftarrow>ys. f x y) = (\<Sum>y\<leftarrow>ys. \<Sum>x\<in>X. f x y)"
prop "{u. P u} = {(a, b) | a b. P (a, b)}"

declare [[show_abbrevs=false, bypass_translations=true]]

prop "finite X \<Longrightarrow> (\<Sum>x\<in>X. \<Sum>y\<leftarrow>ys. f x y) = (\<Sum>y\<leftarrow>ys. \<Sum>x\<in>X. f x y)"
prop "{u. P u} = {(a, b) | a b. P (a, b)}"

end

Attachment: goal_untranslated.png
Description: PNG image

Attachment: goal_translated.png
Description: PNG image



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.