Theory FJDefs
section ‹{\tt FJDefs}: Basic Definitions›
theory FJDefs
imports Main
begin
subsection ‹Syntax›
text ‹We use a named representation for terms: variables, method
names, and class names, are all represented as {\tt nat}s. We use the
finite maps defined in {\tt Map.thy} to represent typing contexts and
the static class table. This section defines the representations of
each syntactic category (expressions, methods, constructors, classes,
class tables) and defines several constants ({\tt Object} and {\tt this}).
›
subsubsection‹Type definitions›
type_synonym varName = nat
type_synonym methodName = nat
type_synonym className = nat
record varDef =
vdName :: "varName"
vdType :: "className"
type_synonym varCtx = "varName ⇀ className"
subsubsection‹Constants›
definition
Object :: "className" where
"Object = 0"
definition
this :: "varName" where
"this == 0"
subsubsection ‹Expressions›