[isabelle-dev] Stymied by cryptic failure in Product_type.thy

[Josh Tilles]

On Feb 18, 2014, at 3:17 AM, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:

> Hi Josh, Lars,
> 
> Am 18.02.2014 um 08:19 schrieb Lars Noschinski <noschinl at in.tum.de>:
> 
>> The position of the error message is a bit misleading. It is not the qed which fails. Instead, after finishing the proof, the free_constructors command tries to prove something on its own -- and fails. Probably, its internal tactics depend on the choice axiom.
> 
> No, it doesn't use choice, which is not yet available. But it probably uses "P | ~ P". The tactics are in "Tools/Ctr_Sugar/ctr_sugar_tactics.ML", should anybody feel compelled to try to make them intuitionistic.
> 
> BTW Josh: I don't know how far you plan to get with this, but I doubt you will get very far. Before you invest too much time into this, it would be useful if you told us more about your motivation.
Sure! There are some mathematical topics that I’d like to use Isabelle to study, but those topics require an intuitionistic setting. (the primary example is infinitesimal analysis) Also, the way that `src/HOL/ex/Higher_Order_Logic.thy` handles classical reasoning —by creating a locale— appeals to me aesthetically.

Thanks a bunch,
--Josh



-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140221/76c403d2/attachment.sig>