Re: [isabelle] Presenting theories - equality symbols and abbreviations



On Sun, 11 Mar 2012, filip at 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 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).

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





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