Email Gateway (Aug 18 2022 at 19:17): Email Gateway (Aug 18 2022 at 19:17):From: filip@matf.bg.ac.rs
Hello,
I am trying to generate LaTeX-ed proof documents from my Isabelle/HOL
theories and I have several technical questions.
(1) Suppose I have a definition like
definition f where "f x == x <-> True"
When I use @{thm f_def[no_vars]}, in LaTeX, I get
f x == x = True
So, = is printed, although I used the <-> symbol. Is there a way to
persuade the system to print <-> for equality on bool type? It would be
convenient if this could be done globally, so I could be sure that <-> is
consistently used in the whole proof document.
(2) If f is an abbreviation like
abbreviation f where "f x == x <-> True"
Is there a way to print it later using some antiquotation (as I used @{thm
f_def[no_vars]}, when f was a definition).
(3) I noticed that function definitions do not allow using == but only =.
For example, I am not allowed to write:
fun f where "f (a, b) == a > b"
but only
fun f where "f (a, b) = (a > b)"
That seems a bit inconsistent with definitions made by using the
definition keyword. Is it maybe somehow possible to make @{thm
f.simps[no_vars]} print == instead of = so in LaTeX I get
f (a, b) == a > b
I prefer this notation (since it emphasizes that something holds by
definition, since it does not require additional parentheses and since it
is consistent with definitions given using the definition keyword).
Thank you very much for your answers!
Filip
Email Gateway (Aug 18 2022 at 19:18):From: Makarius <makarius@sketis.net>
On Sun, 11 Mar 2012, filip@matf.bg.ac.rs wrote:
(1) Suppose I have a definition like
definition f where "f x == x <-> True"
When I use @{thm f_def[no_vars]}, in LaTeX, I get
f x == x = True
So, = is printed, although I used the <-> symbol. Is there a way to
persuade the system to print <-> for equality on bool type?
This is controlled by the print mode "iff". So for LaTeX document
preparation, it should work via @{thm f_def [no_vars, mode = iff]}
You can also set Thy_Output.modes globally in your ROOT.ML file.
It would be convenient if this could be done globally, so I could be
sure that <-> is consistently used in the whole proof document.
It will be consistent for printing, but source text is shown as you write
it literally.
(2) If f is an abbreviation like
abbreviation f where "f x == x <-> True"
Is there a way to print it later using some antiquotation
See @{abbrev} as document antiquotation in the isar-ref manual.
(3) I noticed that function definitions do not allow using == but only =.
For example, I am not allowed to write:fun f where "f (a, b) == a > b"
but only
fun f where "f (a, b) = (a > b)"
That seems a bit inconsistent with definitions made by using the
definition keyword. Is it maybe somehow possible to make @{thm
f.simps[no_vars]} print == instead of = so in LaTeX I getf (a, b) == a > b
I prefer this notation (since it emphasizes that something holds by
definition, since it does not require additional parentheses and since
it is consistent with definitions given using the definition keyword).
Raw == from Pure is mainly for foundational purposes, it is hardly ever
used in Isabelle/HOL definitions these days.
Things like 'definition' or 'inductive' or 'function' are all some derived
form of theorems based on some primitive defs that the package
implementations produce from the user input, and then recover the
specified results by some mechanized proof. In contemporary Isabelle both
'definition' and 'theorem' are non-trivial specification mechanisms in
that sense.
Makarius
Last updated: Apr 30 2024 at 08:19 UTC