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.