Theory Expr

(*
Title: Strong-Security
Authors: Sylvia Grewe, Alexander Lux, Heiko Mantel, Jens Sauer
*)
theory Expr
imports Types
begin

--"type parameters:"
--"'val: numbers, boolean constants.... "
--"'id: identifier names"

type_synonym ('val) operation = "'val list => 'val"

datatype ('id, 'val) Expr =
Const "'val" |
Var "'id" |
Op "'val operation" "(('id, 'val) Expr) list"


-- "defining a simple recursive evaluation function on this datatype"
primrec ExprEval :: "(('id, 'val) Expr, 'id, 'val) Evalfunction"
and ExprEvalL :: "(('id, 'val) Expr) list => ('id, 'val) State => 'val list"
where
"ExprEval (Const v) m = v" |
"ExprEval (Var x) m = (m x)" |
"ExprEval (Op f arglist) m = (f (ExprEvalL arglist m))" |

"ExprEvalL [] m = []" |
"ExprEvalL (e#V) m = (ExprEval e m)#(ExprEvalL V m)" 

end