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, until now.

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 variable.


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