Re: [isabelle] Unexpected Behavior with Sum_Type



Thanks for clarifying that Christian!!

Best!

On Sat, Feb 2, 2013 at 9:54 PM, Christian Sternagel
<c.sternagel at gmail.com>wrote:

> 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<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<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!
>>
>>
>
>


-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




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