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

[Jasmin Christian Blanchette]

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.

> BTW: Whoever wrote this proof:

That would be me I guess. ;)

> The first case would be better stated as
> 
>    assume "⋀x1 x2. p = Pair x1 x2 ⟹ P" then show "P"
> 
> because meta-implication in show-statements may lead to counter-intuitive behaviour.

The first case is better written as it is because too much typing may cause arthritis and wrist pains.

Cheers,

Jasmin