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

[Jasmin Christian Blanchette]

Hi Josh,

Am 21.02.2014 um 07:12 schrieb Josh Tilles <merelyapseudonym at gmail.com>:

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

Otherwise, there's also the work by Stefan Berghofer, in "src/HOL/Proofs/Extraction" and partly in "src/HOL/Proofs/Lambda", where he uses an intuitinistic prover he wrote ("iprover") and carefully uses Isabelle's automation. Then he extracts code from proof terms, much like in Coq. I'm not very familiar with this work, but a successful extraction probably means that at least the computation-relevant parts are intuitionistic.

The locale might be the simplest option, but perhaps you'll find yourself wishing for the automation provided by "iprover".

Cheers,

Jasmin