[isabelle] Creating fresh logical variables



Hi all,

I am a new user of Isabelle, and my first project using it seems to be
non-standard.  Any help would be greatly appreciated.

My main question is: Is it possible to create new fresh logical
variables inside a theory?

I am trying to model a function F that takes a program as input, and
produces a quantified formula.  Each assignment v := e in the program
corresponds to a quantifier \<exists> v ... in the formula, which is
why it is important to be able to create a new (logical) variable
corresponding to each program variable to quantify over.

So, for instance, the program "v := e; assert v=5" would produce a
formula like \<exists> v. v=e /\ v=5.  Here, e is a free variable.

Is it possible to model the function F such that it returns a term of
type bool?  If this isn't possible, is there any other way to model
this inside of Isabelle?

Thanks for your help,
Edward Schwartz





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