Email Gateway (Aug 18 2022 at 11:20): Email Gateway (Aug 18 2022 at 11:20):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
Dear Isabelle,
How is it possible to introduce typeset syntax with compound
subscripts? For example, given an indexed family "tos" of relations,
where I currently write
(t1,t2) \<in> tos n
I'd like to write something that will be typeset roughly as the LaTeX
t1 \leq_{tos n} t2
(Here tos is a bound variable, not something introduced by a consts, if that makes any difference.)
My attempts have all failed miserably (except when the subscript is a
single-character identifier), trying various combinations of Isabelle
syntax and translations declarations, definitions of \isactrlfoo's,
and \<^bsub>...\<^esub>.
many thanks,
Peter
example:
types t = "string"
types indexed_orders = "nat \<Rightarrow> (t*t) set"
constdefs
mytest :: "indexed_orders \<Rightarrow> nat \<Rightarrow> t \<Rightarrow> t \<Rightarrow> bool"
"mytest tos n t1 t2 == (t1,t2) \<in> tos n"
Email Gateway (Aug 18 2022 at 11:23):From: Stefan Berghofer <berghofe@in.tum.de>
Peter Sewell wrote:
Dear Peter,
this could be achieved by introducing an abbreviation mapping
x \<le>\<^bsub>R\<^esub> y
to
(x, y) \<in> R
as shown in the attached theory file. Note that this abbreviation will
affect all terms of the form "(x, y) \<in> R", which for example means
that also the intoduction rules for the transitive closure are printed
using this syntax.
Greetings,
Stefan
Peter.thy
Email Gateway (Aug 18 2022 at 11:23):From: Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
Many thanks!
Part of my confusion was the difference between what happens when
Isabelle typesets constdefs at the top level of a .thy file, and what
happens when it pretty-prints quoted theorems, as in your @{thm
[display] mytest_def [no_vars]}. At present I'm using the former, to
get some control over the layout of big formulas, and to include
comments in them. Am I right in (now) guessing that to get the intended
typesetting I therefore have to use the verbose syntax explicitly,
e.g. something like this:
constdefs
mytest3 :: "indexed_orders \<Rightarrow> nat \<Rightarrow> t \<Rightarrow> t \<Rightarrow> bool"
"mytest3 tos n t1 t2 == (t1 \<le>\<^bsub> tos n \<^esub> t2)"
ie, there's no way to have the abbreviation automatically applied?
ta,
Peter
Last updated: Nov 21 2024 at 12:39 UTC