Re: [isabelle] Schematic vars or universal bound vars in theorem?
On 7/18/2012 12:02 PM, John Wickerson wrote:
I think you should state the theorem without the \<forall>, because it makes it easier to use the theorem later on. For instance, you can say
... using SigmaE_is_unique[of "foo"]...
to obtain SigmaE_is_unique in the case when u is foo. You can't do this so easily when you have the \<forall> there.
That sounds like it could be the biggest reason. I was only thinking
about schematic variables being instantiated automatically. The idea of
calling theorems like in a programming language hasn't occurred to me,
So, I guess I want a schematic variable in a theorem when I know I'm
going to want to instantiate it manually. However, I now have the
question of whether automatic proof methods need the schematic variables
so that they can instantiate them.
It's my healthy paranoia kicking in here. I'm using axioms, so I'm
trying to use everything I know right now to keep from being inconsistent.
Another question I would have for a person is whether I'm protected in
any way by making a variable bound so that it doesn't become a schematic
This archive was generated by a fusion of
Pipermail (Mailman edition) and