[isabelle-dev] Stymied by cryptic failure in Product_type.thy
Jasmin Christian Blanchette
jasmin.blanchette at gmail.com
Tue Feb 18 09:17:12 CET 2014
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.
More information about the isabelle-dev