Theory Expr

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

header {* \isaheader{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))"
(*<*)
apply(cases v⇣1)
apply auto
apply(cases v⇣2)
apply auto
done
(*>*)


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