Re: [isabelle] typesetting compound subscripts

Peter Sewell wrote:
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>.

Dear Peter,

this could be achieved by introducing an abbreviation mapping

  x \<le>\<^bsub>R\<^esub> y


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


Dr. Stefan Berghofer               E-Mail: berghofe at
Institut fuer Informatik           Phone: +49 89 289 17328
Technische Universitaet Muenchen   Fax:   +49 89 289 17307
Boltzmannstr. 3                    Room: 01.11.059
85748 Garching, GERMANY  
theory Peter
imports Main

types t = "string"
types indexed_orders = "nat \<Rightarrow> (t*t) set"

mytest :: "indexed_orders \<Rightarrow> nat \<Rightarrow> t \<Rightarrow> t \<Rightarrow> bool"
"mytest tos n t1 t2 == (t1,t2) \<in> tos n"

  in_rel :: "'a \<Rightarrow> ('a * 'b) set \<Rightarrow> 'b \<Rightarrow> bool" ("(_/ \<le>\<^bsub>_\<^esub> _)" [51, 0, 51] 50) where
  "x \<le>\<^bsub>R\<^esub> y \<equiv> (x, y) \<in> R"

text {*
The definition of @{text mytest} is
@{thm [display] mytest_def [no_vars]}
The introduction rule @{text rtrancl_into_rtrancl} for the transitive closure is
@{thm [display] rtrancl_into_rtrancl [no_vars]}


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