(* Title: HOL/NanoJava/Term.thy ID: $Id: Term.thy,v 1.10 2005/06/17 14:13:09 haftmann Exp $ Author: David von Oheimb Copyright 2001 Technische Universitaet Muenchen *) header "Statements and expression emulations" theory Term imports Main begin typedecl cname --{* class name *} typedecl mname --{* method name *} typedecl fname --{* field name *} typedecl vname --{* variable name *} consts This :: vname --{* This pointer *} Par :: vname --{* method parameter *} Res :: vname --{* method result *} text {* Inequality axioms are not required for the meta theory. *} (* axioms This_neq_Par [simp]: "This ≠ Par" Par_neq_Res [simp]: "Par ≠ Res" Res_neq_This [simp]: "Res ≠ This" *) datatype stmt = Skip --{* empty statement *} | Comp stmt stmt ("_;; _" [91,90 ] 90) | Cond expr stmt stmt ("If '(_') _ Else _" [ 3,91,91] 91) | Loop vname stmt ("While '(_') _" [ 3,91 ] 91) | LAss vname expr ("_ :== _" [99, 95] 94) --{* local assignment *} | FAss expr fname expr ("_.._:==_" [95,99,95] 94) --{* field assignment *} | Meth "cname × mname" --{* virtual method *} | Impl "cname × mname" --{* method implementation *} and expr = NewC cname ("new _" [ 99] 95) --{* object creation *} | Cast cname expr --{* type cast *} | LAcc vname --{* local access *} | FAcc expr fname ("_.._" [95,99] 95) --{* field access *} | Call cname expr mname expr ("{_}_.._'(_')" [99,95,99,95] 95) --{* method call *} end