Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Unexpected Behavior with Sum_Type


view this post on Zulip Email Gateway (Aug 19 2022 at 10:06):

From: Makarius <makarius@sketis.net>
Which dialog box do you mean?

The Isabelle/jEdit completions are derived from the cumulative "symbols"
specifications, notably $ISABELLE_HOME/etc/symbols and your
$ISABELLE_HOME_USER/etc/symbols (which is non-existent by default).

So if you put a line like this in the latter file it should work:

\<uplus> code: 0x00228e group: operator abbrev: <+>

This gives you physical rendering via Unicode and some input method, not
yet actual HOL notation, which is a different story.

Makarius

view this post on Zulip Email Gateway (Aug 19 2022 at 10:07):

From: Alfio Martini <alfio.martini@acm.org>
Dear Isabelle Users,

Isabelle2013-RC2 consider Projl a free variable in the following
expression:

value "Projl (Inl (3::nat))"

To get the right answer, I have to type

value "Sum_Type.Projl (Inl (3::nat))"

Even

lemma "Projl (Inl (3::nat)) = 3" by (simp add:Projl_Inl) does not work,
since Projl appears as a free variable.

Why does this happen, since Sum_Type is in Main?

I would not like to use the "Sum_Type" qualifier, if there is a workaround.

Also, if possible, I would like to have a symbol in the completion pop up
table for disjoint union of sets "<+>".
I suggest \<uplus> . I tried it myself, but I kind of got lost with the
dialog box. I wanted to add the mathematical
representation and not the internal Isabelle one.

Best!

view this post on Zulip Email Gateway (Aug 19 2022 at 10:12):

From: Christian Sternagel <c.sternagel@gmail.com>
Dear Alfio,

I don't think that the unqualified Projl was ever visible. See also

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-July/msg00118.html

for a related thread.

The reason that those constants are not openly visible is the line

hide_const (open) Suml Sumr Projl Projr

at the end of Sum_Type.thy.

As Andreas pointed out in the thread above

https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-July/msg00125.html

we can mostly replace Projl and Projr by case expressions.

cheers

chris

view this post on Zulip Email Gateway (Aug 19 2022 at 10:13):

From: Alfio Martini <alfio.martini@acm.org>
Thanks for clarifying that Christian!!

Best!


Last updated: Mar 28 2024 at 16:17 UTC