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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and