Email Gateway (Aug 19 2022 at 08:05): Email Gateway (Aug 19 2022 at 08:05):From: Gergely Buday <gbuday@gmail.com>
Hi,
is it possible to define a variable in Isar, like
var elem = SOME x. {x. even x}
and then use it later?
Email Gateway (Aug 19 2022 at 08:05):From: Lawrence Paulson <lp15@cam.ac.uk>
You can define constants, both globally (at the level of the theory) and local to a context. To get the meaning of such a constant, you have to refer to its defining equation explicitly. You can also create abbreviations, which are essentially macros in that there is no defining equation because the new symbol always expands to its meaning.
Globally, use keywords such as “definition" and “abbreviation". Local to a context, you can use “def" and “let". More information is available in the documentation.
Larry
Email Gateway (Aug 19 2022 at 08:05):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Dear Gergely,
let ?elem = "..."
lemma
defines "elem == ..."
assumes "..."
shows "..."
with corresponding fact "elem_def"
for a gobal definition you can use the usual "definition" command
for a non-global definition that might span several lemmas you can use
context
fixes elem
assumes "elem = ..."
begin
...
end
However, your specific example does not make sense, since it is not
well-typed. Maybe you wanted to have something like "SOME x. x : {x.
even x}" (i.e., an arbitrary element from the set "{x. even x}").
cheers
chris
Last updated: Apr 19 2024 at 20:15 UTC