Email Gateway (Aug 19 2022 at 08:47): Email Gateway (Aug 19 2022 at 08:47):From: Edward Schwartz <edmcman@cmu.edu>
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
Last updated: Nov 21 2024 at 12:39 UTC