Re: [isabelle] "apply auto" transforms provable statement to something false?



On 25/01/16 12:02, Eugene W. Stark wrote:
For some reason, I had in my mind that auto should not produce false subgoals from
provable goals.

In my experience, this is uncommon, but it does happen, and to my knowledge, this is perfectly normal.

I did not look at your example (the definitions of Arr etc. are missing, if I see it correctly), but my guess would be that in this case, the problem is with schematic variables. Applying "existential" rules (like exI) introduces schematic variable into the goals, and at some point, you have to decide how to instantiate them. If "auto" instantiates one of these schematic variables incorrectly, you may well end up with something unprovable.


Cheers,

Manuel




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.