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,v1,v2) = Some(Bool (v1 = v2))"
| "binop(Add,Intg i1,Intg i2) = Some(Intg(i1+i2))"
| "binop(bop,v1,v2) = None"

lemma [simp]:
  "(binop(Add,v1,v2) = Some v) = (∃i1 i2. v1 = Intg i1 ∧ v2 = Intg i2 ∧ v = Intg(i1+i2))"
(*<*)by(cases v1; cases v2) 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 "addr a == Val(Addr a)"
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(e1 «bop» e2) = fv e1 ∪ fv e2"
| "fv(Var V) = {V}"
| "fv(LAss V e) = {V} ∪ fv e"
| "fv(e∙F{D}) = fv e"
| "fv(e1∙F{D}:=e2) = fv e1 ∪ fv e2"
| "fv(e∙M(es)) = fv e ∪ fvs es"
| "fv({V:T; e}) = fv e - {V}"
| "fv(e1;;e2) = fv e1 ∪ fv e2"
| "fv(if (b) e1 else e2) = fv b ∪ fv e1 ∪ fv e2"
| "fv(while (b) e) = fv b ∪ fv e"
| "fv(throw e) = fv e"
| "fv(try e1 catch(C V) e2) = fv e1 ∪ (fv e2 - {V})"
| "fvs([]) = {}"
| "fvs(e#es) = fv e ∪ fvs es"

lemma [simp]: "fvs(es1 @ es2) = fvs es1 ∪ fvs es2"
(*<*)by (induct es1 type:list) auto(*>*)

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

end