Email Gateway (Aug 19 2022 at 10:44): Email Gateway (Aug 19 2022 at 10:44):From: John Wickerson <jpw48@cam.ac.uk>
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
More generally, in case anybody is interested in following Isabelle-related questions on Stack Overflow, I thought I'd just point out that you might like to subscribe to the following rss feed...
http://stackoverflow.com/feeds/tag/isabelle
John
Email Gateway (Aug 19 2022 at 10:44):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi John,
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
signature.asc
Email Gateway (Aug 19 2022 at 10:44):From: John Wickerson <jpw48@cam.ac.uk>
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
Last updated: Apr 19 2024 at 08:19 UTC