Re: [isabelle] Schematic vars or universal bound vars in theorem?



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.

john

On 18 Jul 2012, at 15:10, Gottfried Barrow wrote:

> Hi,
> 
> I summarize my question first.
> 
> I have two theorems, SigmaE_is_unique and SigmaE_is_unique2. In the first, I end up with "u" as a universally quantified bound variable, because that's how I specified it in the formula. In the second, I end up with "u" as a schematic variable, because I left it as a free variable in the formula.
> 
> Which of these do I want? This question also applies to my axiom Sigma_exA.
> 
> I read this thread, "Free variables vs schematic variables":
> 
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00048.html
> 
> I've also read this email, which is an aside:
> 
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-June/msg00172.html
> 
> The context of that thread was meta-logic, so when Makarius says, "Outermost quantifiers are circumvented... there is an explicit core inference that removes the quantifiers and expresses the generality in terms of schematic variables", I conclude that he's talking about the \<And> quantifier. This is because I don't see any removal of \<forall>.
> 
> I do notice in proof steps and theorem results, that Isabelle may rearrange a \<forall> in a formula, such as taking  a \<forall> to the outside of some parentheses. That's fine with me.
> 
> Here, I use my limited knowledge to determine the difference in my two theorems mentioned above. If all the variables in the theorem are bound, then the formula in the theorem will simply be used as a fact.
> 
> If there are schematic variables in the theorem, then schematic variables will first be instantiated, and the instantiated formula of the theorem will be used as a fact.
> 
> I don't know why I need variables  to be instantiated to make it more general, or whether I don't want variables to be instantiated so that it's tighter.
> 
> This also applies to my axiom Sigma_exA. I can strip out all the universal quantifiers, and everything still works, but I end up with schematic variables being used, as shown by "thm show_info2", although it may be the proof step of show_info2 that's really a true reflection of Sigma_EeA, in which the variables are still free.
> 
> I attached the theory, where some names above are rough translations.
> 
> Thanks,
> GB
> 
> <sTs_.thy>






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