Theory Expr

(*  Title:      Jinja/J/Expr.thy
    ID:         $Id: Expr.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Tobias Nipkow
    Copyright   2003 Technische Universitaet Muenchen
*)

header {* \isaheader{Expressions} *}

theory Expr = Exceptions:

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     ("_\<bullet>_{_}" [10,90,99]90)      -- "field access"
  | FAss "('a exp)" vname cname "('a exp)"     ("_\<bullet>_{_} := _" [10,90,99,90]90)      -- "field assignment"
  | Call "('a exp)" mname "('a exp list)"     ("_\<bullet>_'(_')" [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)

types
  expr = "vname exp"            -- "Jinja expression"
  J_mb = "vname list × expr"    -- "Jinja method body: parameter names and expression"
  J_prog = "J_mb prog"          -- "Jinja program"

text{*The semantics of binary operators: *}

consts
  binop :: "bop × val × val => val option"
recdef binop "{}"
  "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))"
(*<*)
apply(cases v1)
apply auto
apply(cases v2)
apply auto
done
(*>*)


subsection "Syntactic sugar"

syntax
  InitBlock:: "vname => ty => 'a exp => 'a exp => 'a exp"   ("(1'{_:_ := _;/ _})")
translations
  "InitBlock V T e1 e2" => "{V:T; V := e1;; e2}"

syntax
 unit :: "'a exp"
 null :: "'a exp"
 addr :: "addr => 'a exp"
 true :: "'a exp"
 false :: "'a exp"
translations
 "unit" == "Val Unit"
 "null" == "Val Null"
 "addr a" == "Val(Addr a)"
 "true" == "Val(Bool True)"
 "false" == "Val(Bool False)"

syntax
  Throw :: "addr => 'a exp"
  THROW :: "cname => 'a exp"
translations
  "Throw a" == "throw(Val(Addr a))"
  "THROW xc" == "Throw(addr_of_sys_xcpt xc)"


subsection{*Free Variables*}

consts
  fv  :: "expr      => vname set"
  fvs :: "expr list => vname set"
primrec
  "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\<bullet>F{D}) = fv e"
  "fv(e1\<bullet>F{D}:=e2) = fv e1 ∪ fv e2"
  "fv(e\<bullet>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