Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] LaTeX output for bounded Unions

Email Gateway (Aug 22 2022 at 16:15):

From: "Urban, Christian" <christian.urban@kcl.ac.uk>
Dear All,

I have two small problems. I use the notation

U i \<in> {..n} . P i and U i \<in> {n..m} . P i

for unions where the index is drawn from an interval. If

I print them out in LaTeX, the first is displayed as

U i \<le> n . P i

I would prefer to have it uniformly displayed as interval, like

the second. What do I have to do for that? I could not find

any syntax declaration which causes the first.

My second problem is that the theorems in question

seem to be printed eta-contracted like

L(UPNTIMES r n) = UNION {..n} (SpecExt.Pow (L(r)))

even if I explicitly told Isabelle not to do it (set eta_contract = false).

How can I prevent this eta-contractions from happening?

Thanks a lot!

Christian

Email Gateway (Aug 22 2022 at 16:16):

From: Tobias Nipkow <nipkow@in.tum.de>
On 12/10/2017 15:46, Urban, Christian wrote:

Dear All,

I have two small problems. I use the notation

U i \<in> {..n} . P i and U i \<in> {n..m} . P i

for unions where the index is drawn from an interval. If

I print them out in LaTeX, the first is displayed as

U i \<le> n . P i

I would prefer to have it uniformly displayed as interval, like

the second. What do I have to do for that? I could not find

any syntax declaration which causes the first.

See Set_Interval, at the beginning.

I recommend not to use {..n::nat} because it means the same as {0..n}
but not all lemmas may exist for the former variant.

My second problem is that the theorems in question

seem to be printed eta-contracted like

L(UPNTIMES r n) = UNION {..n} (SpecExt.Pow (L(r)))

even if I explicitly told Isabelle not to do it (set eta_contract = false).

How can I prevent this eta-contractions from happening?

Are you sure the internal term is really eta-expanded? If it comes
from a fun-definition, it is likely to get eta-contracted when you
make the definition. You may have to state an explicit eta-expanded
lemma.

Tobias

Thanks a lot!

Christian

smime.p7s

Last updated: Apr 26 2024 at 16:20 UTC