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
  "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:›

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