# Re: [isabelle] Lifting a partial definition to a quotient type

Hi Florian,
Thanks for this. Yes, I agree, I could certainly change disj_union to be a fully defined operator. It's just that the textbook definition, to which I'm trying to be faithful, says "We write $S \uplus T$ for the union of two sets S and T known or assumed to be disjoint".
Just to make sure that I understand the totality of HOL as well as I think I do, I'll argue against your point that my disj_union is equivalent to union. I can prove "{a} union {a} = {a}", but I can't prove "{a} disj_union {a} = {a}".
john
On 12 Mar 2013, at 20:11, Florian Haftmann wrote:
> Hi John,
>
> Am 12.03.2013 15:27, schrieb John Wickerson:
>> Hi, I just wanted to alert the Quotient people to the following question that has recently appeared on Stack Overflow, on which they might have an opinion...
>>
>> http://stackoverflow.com/questions/15347913/lifting-a-partial-definition-to-a-quotient-type
>
> this is slightly off-topic, but note that HOL is total. I. e.
>
> definition "X ∩ Y = {} ⟹ disj_union X Y ≡ X ∪ Y"
>
> yields a guarded equation, but on the foundational definition level
> disj_union is equivalent to union. I'm skeptic whether such
> »partiality« is inherent to your example -- very likely in can be
> circumvented.
>
> Cheers,
> Florian
>
>
> --
>
> PGP available:
> http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
>

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