Re: [isabelle] The environment function

On Wed, 15 Oct 2014, mahmoud abdelazim wrote:

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

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).


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

  * datatype constructors are usually capitalized

  * CamelCaseIsNotUsedInIsabelle


theory WLG

imports Main


datatype exp = K int | Var nat | Pls exp exp (infixl "\<^bold>+" 156)

primrec eval_exp :: "exp \<Rightarrow> (nat \<Rightarrow> int) \<Rightarrow> int"


  "eval_exp (K c) env = c"

| "eval_exp (Var x) env = env x"

| "eval_exp (a \<^bold>+ b) env = eval_exp a env + eval_exp b env"

datatype form = B bool | Nt form | Less_Than exp exp (infixl "\<^bold><" 100)

primrec eval_form :: "form \<Rightarrow> (nat \<Rightarrow> int) \<Rightarrow> bool"


  "eval_form (B b) env = b"

| "eval_form (Nt b) env  = (\<not> eval_form b env)"

| "eval_form (v \<^bold>< t) env = (eval_exp v env < eval_exp t env)"

datatype prog =


| Comp prog prog (infixl "\<^bold>;" 160)

| IF form prog prog

| Whil form prog

| Assign exp int (infix "\<^bold>:\<^bold>=" 200 )

value "eval_exp (K -3) env"

value "eval_exp (Var x) env"

value "eval_exp (K 2 \<^bold>+ K 3) env"

value "eval_exp (Var x) (env(x := a))"

value "eval_form (B False) env"

value "eval_form (B True) env"

value "eval_form (Nt (B False)) env"

value "eval_form (K 3 \<^bold>< K 2) env"


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