Re: [isabelle] Unexpected Behavior with Sum_Type



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

On 02/03/2013 01:55 AM, Alfio Martini wrote:
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!







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