Theory Expr

(*  Title:       CoreC++
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
    Based on the Jinja theory J/Expr.thy by Tobias Nipkow 
*)

section ‹Expressions›

theory Expr imports Value begin

subsection ‹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
  "eM(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:›

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))"
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


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(Ce) = fv e"
| "fv(Val v) = {}"
| "fv(e1 «bop» e2) = fv e1  fv e2"
| "fv(Var V) = {V}"
| "fv(V := e) = {V}  fv e"
| "fv(eF{Cs}) = fv e"
| "fv(e1F{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