Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] The environment function


view this post on Zulip Email Gateway (Aug 19 2022 at 16:19):

From: mahmoud abdelazim <m.abdelazim@icloud.com>
How i can define an “env” function in the theory attached here ,
in such way that if i do the following
value "evalExp (Var x ) env” i

the output will for example
“5”
:: "int"
WLG.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 16:19):

From: mahmoud abdelazim <m.abdelazim@icloud.com>
How i can define an “env” function in the theory attached here ,
in such way that if i do the following
value "evalExp (Var x ) env”

the output will for example
“5”
:: "int"
WLG.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 16:19):

From: mahmoud abdelazim <m.abdelazim@icloud.com>
How i can define an “env” function in the theory attached here ,
in such way that if i do the following
value "evalExp (Var 1 ) env”

the output will for example
“5”
:: "int"
WLG.thy

view this post on Zulip Email Gateway (Aug 19 2022 at 16:19):

From: Alfio Martini <alfio.martini@acm.org>
Hi Mahmoud,

Here are some possibilities:

definition state::"nat ⇒ int" where
"state = (λx::nat.0)(3:=5)"
value "evalExp (Var 3) ((λx::nat.0)(3:=(5::int)))"
value "evalExp (Var 3) state"

Hope it helps!

view this post on Zulip Email Gateway (Aug 19 2022 at 16:21):

From: Makarius <makarius@sketis.net>
By using the fun_upd operator in Isabelle/HOL, with its := syntax, e.g.
env(x := 5)

A potential cause of confusion is the re-use of := as notation in your
example. The included version of your WLG.thy avoids that by using bold
versions of concrete syntax everywhere (which might cause other confusion
due to visual similarity with non-bold versions).

Furthermore:

* type names are always lower case, like almost everything else

* datatype constructors are usually capitalized

* CamelCaseIsNotUsedInIsabelle

Makarius


http://stop-ttip.org


WLG.thy


Last updated: Nov 21 2024 at 12:39 UTC