theory WLG

imports Main

begin



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

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

where

  "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"

where

  "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 =

  Skip

| 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"



end