# Theory Expr

```(*  Title:      Jinja/J/Expr.thy
Author:     Tobias Nipkow
Copyright   2003 Technische Universitaet Muenchen
*)

section ‹Expressions›

theory Expr
imports "../Common/Exceptions"
begin

datatype bop = Eq | Add     ― ‹names of binary operations›

datatype 'a exp
= new cname      ― ‹class instance creation›
| Cast cname "('a exp)"      ― ‹type cast›
| Val val      ― ‹value›
| BinOp "('a exp)" bop "('a exp)"     ("_ «_» _" [80,0,81] 80)      ― ‹binary operation›
| Var 'a                                               ― ‹local variable (incl. parameter)›
| LAss 'a "('a exp)"     ("_:=_" [90,90]90)                    ― ‹local assignment›
| FAcc "('a exp)" vname cname     ("_∙_{_}" [10,90,99]90)      ― ‹field access›
| FAss "('a exp)" vname cname "('a exp)"     ("_∙_{_} := _" [10,90,99,90]90)      ― ‹field assignment›
| Call "('a exp)" mname "('a exp list)"     ("_∙_'(_')" [90,99,0] 90)            ― ‹method call›
| Block 'a ty "('a exp)"     ("'{_:_; _}")
| Seq "('a exp)" "('a exp)"     ("_;;/ _"             [61,60]60)
| Cond "('a exp)" "('a exp)" "('a exp)"     ("if '(_') _/ else _" [80,79,79]70)
| While "('a exp)" "('a exp)"     ("while '(_') _"     [80,79]70)
| throw "('a exp)"
| TryCatch "('a exp)" cname 'a "('a exp)"     ("try _/ catch'(_ _') _"  [0,99,80,79] 70)

type_synonym
expr = "vname exp"            ― ‹Jinja expression›
type_synonym
J_mb = "vname list × expr"    ― ‹Jinja method body: parameter names and expression›
type_synonym
J_prog = "J_mb prog"          ― ‹Jinja program›

text‹The semantics of binary operators:›

fun binop :: "bop × val × val ⇒ val option" where
"binop(Eq,v⇩1,v⇩2) = Some(Bool (v⇩1 = v⇩2))"
| "binop(Add,Intg i⇩1,Intg i⇩2) = Some(Intg(i⇩1+i⇩2))"
| "binop(bop,v⇩1,v⇩2) = None"

lemma [simp]:
"(binop(Add,v⇩1,v⇩2) = Some v) = (∃i⇩1 i⇩2. v⇩1 = Intg i⇩1 ∧ v⇩2 = Intg i⇩2 ∧ v = Intg(i⇩1+i⇩2))"
(*<*)by(cases v⇩1; cases v⇩2) auto(*>*)

subsection "Syntactic sugar"

abbreviation (input)
InitBlock:: "'a ⇒ ty ⇒ 'a exp ⇒ 'a exp ⇒ 'a exp"   ("(1'{_:_ := _;/ _})") where
"InitBlock V T e1 e2 == {V:T; V := e1;; e2}"

abbreviation unit where "unit == Val Unit"
abbreviation null where "null == Val Null"
abbreviation "true == Val(Bool True)"
abbreviation "false == Val(Bool False)"

abbreviation
Throw :: "addr ⇒ 'a exp" where
"Throw a == throw(Val(Addr a))"

abbreviation
THROW :: "cname ⇒ 'a exp" where
"THROW xc == Throw(addr_of_sys_xcpt xc)"

subsection‹Free Variables›

primrec fv :: "expr ⇒ vname set" and fvs :: "expr list ⇒ vname set" where
"fv(new C) = {}"
| "fv(Cast C e) = fv e"
| "fv(Val v) = {}"
| "fv(e⇩1 «bop» e⇩2) = fv e⇩1 ∪ fv e⇩2"
| "fv(Var V) = {V}"
| "fv(LAss V e) = {V} ∪ fv e"
| "fv(e∙F{D}) = fv e"
| "fv(e⇩1∙F{D}:=e⇩2) = fv e⇩1 ∪ fv e⇩2"
| "fv(e∙M(es)) = fv e ∪ fvs es"
| "fv({V:T; e}) = fv e - {V}"
| "fv(e⇩1;;e⇩2) = fv e⇩1 ∪ fv e⇩2"
| "fv(if (b) e⇩1 else e⇩2) = fv b ∪ fv e⇩1 ∪ fv e⇩2"
| "fv(while (b) e) = fv b ∪ fv e"
| "fv(throw e) = fv e"
| "fv(try e⇩1 catch(C V) e⇩2) = fv e⇩1 ∪ (fv e⇩2 - {V})"
| "fvs([]) = {}"
| "fvs(e#es) = fv e ∪ fvs es"

lemma [simp]: "fvs(es⇩1 @ es⇩2) = fvs es⇩1 ∪ fvs es⇩2"
(*<*)by (induct es⇩1 type:list) auto(*>*)

lemma [simp]: "fvs(map Val vs) = {}"
(*<*)by (induct vs) auto(*>*)

end
```