--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/Term.thy Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,46 @@
+(* Title: HOL/NanoJava/Term.thy
+ ID: $Id$
+ Author: David von Oheimb
+ Copyright 2001 Technische Universitaet Muenchen
+*)
+
+header "Statements and expression emulations"
+
+theory Term = Main:
+
+typedecl cname (* class name *)
+typedecl vnam (* variable or field name *)
+typedecl mname (* method name *)
+arities cname :: "term"
+ vnam :: "term"
+ mname :: "term"
+
+datatype vname (* variable for special names *)
+ = This (* This pointer *)
+ | Param (* method parameter *)
+ | Res (* method result *)
+ | VName vnam
+
+datatype stmt
+ = Skip (* empty statement *)
+ | Comp stmt stmt ("_;; _" [91,90] 90)
+ | Cond vname stmt stmt ("If '(_') _ Else _" [99,91,91] 91)
+ | Loop vname stmt ("While '(_') _" [99,91 ] 91)
+
+ | NewC vname cname ("_:=new _" [99, 99] 95) (* object creation *)
+ | Cast vname cname vname ("_:='(_')_" [99,99,99] 95) (* assignment, cast *)
+ | FAcc vname vname vnam ("_:=_.._" [99,99,99] 95) (* field access *)
+ | FAss vname vnam vname ("_.._:=_" [99,99,99] 95) (* field assigment *)
+ | Call vname cname vname mname vname (* method call *)
+ ("_:={_}_.._'(_')" [99,99,99,99,99] 95)
+ | Meth cname mname (* virtual method *)
+ | Impl cname mname (* method implementation *)
+
+(*###TO Product_Type_lemmas.ML*)
+lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
+apply (rule_tac x = "(a,b)" in image_eqI)
+apply auto
+done
+
+end
+