Theory Expr

(*  Title:       CoreC++
    ID:          $Id: Expr.thy,v 1.7 2008-06-23 21:24:36 makarius Exp $
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
    Based on the Jinja theory J/Expr.thy by Tobias Nipkow 
*)


header {* \isaheader{Expressions} *}

theory Expr imports Value begin

section {* The expressions *}


datatype bop = Eq | Add     -- "names of binary operations"

datatype expr
  = new cname            -- "class instance creation"
  | Cast cname expr      -- "dynamic type cast"
  | StatCast cname expr  -- "static type cast"        
                                 ("(|_|)),_" [80,81] 80)
  | Val val              -- "value"
  | BinOp expr bop expr          ("_ «_» _" [80,0,81] 80)     
     -- "binary operation"
  | Var vname            -- "local variable"
  | LAss vname expr              ("_:=_" [70,70] 70)            
     -- "local assignment"
  | FAcc expr vname path         ("_•_{_}" [10,90,99] 90)      
     -- "field access"
  | FAss expr vname path expr    ("_•_{_} := _" [10,70,99,70] 70)      
     -- "field assignment"
  | Call expr "cname option" mname "expr list"
     -- "method call"
  | Block vname ty expr          ("'{_:_; _}")
  | Seq expr expr                ("_;;/ _" [61,60] 60)
  | Cond expr expr expr          ("if '(_') _/ else _" [80,79,79] 70)
  | While expr expr              ("while '(_') _" [80,79] 70)
  | throw expr

abbreviation (input)
  DynCall :: "expr => mname => expr list => expr" ("_•_'(_')" [90,99,0] 90) where
  "e•M(es) == Call e None M es"

abbreviation (input)
  StaticCall :: "expr => cname => mname => expr list => expr" 
     ("_•'(_::')_'(_')" [90,99,99,0] 90) where
  "e•(C::)M(es) == Call e (Some C) M es"


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


lemma binop_not_ref[simp]:
  "binop(bop,v1,v2) = Some (Ref r) ==> False"
by(cases bop)auto


section{*Free Variables*} 

consts
  fv  :: "expr      => vname set"
  fvs :: "expr list => vname set"
primrec
  "fv(new C) = {}"
  "fv(Cast C e) = fv e"
  "fv((|C|)),e) = fv e"
  "fv(Val v) = {}"
  "fv(e1 «bop» e2) = fv e1 ∪ fv e2"
  "fv(Var V) = {V}"
  "fv(V := e) = {V} ∪ fv e"
  "fv(e•F{Cs}) = fv e"
  "fv(e1•F{Cs}:=e2) = fv e1 ∪ fv e2"
  "fv(Call e Copt 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"

  "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