|
11376
|
1 |
(* Title: HOL/NanoJava/Term.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: David von Oheimb
|
|
|
4 |
Copyright 2001 Technische Universitaet Muenchen
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
header "Statements and expression emulations"
|
|
|
8 |
|
|
|
9 |
theory Term = Main:
|
|
|
10 |
|
|
|
11 |
typedecl cname (* class name *)
|
|
|
12 |
typedecl vnam (* variable or field name *)
|
|
|
13 |
typedecl mname (* method name *)
|
|
|
14 |
arities cname :: "term"
|
|
|
15 |
vnam :: "term"
|
|
|
16 |
mname :: "term"
|
|
|
17 |
|
|
|
18 |
datatype vname (* variable for special names *)
|
|
|
19 |
= This (* This pointer *)
|
|
|
20 |
| Param (* method parameter *)
|
|
|
21 |
| Res (* method result *)
|
|
|
22 |
| VName vnam
|
|
|
23 |
|
|
|
24 |
datatype stmt
|
|
|
25 |
= Skip (* empty statement *)
|
|
|
26 |
| Comp stmt stmt ("_;; _" [91,90] 90)
|
|
|
27 |
| Cond vname stmt stmt ("If '(_') _ Else _" [99,91,91] 91)
|
|
|
28 |
| Loop vname stmt ("While '(_') _" [99,91 ] 91)
|
|
|
29 |
|
|
|
30 |
| NewC vname cname ("_:=new _" [99, 99] 95) (* object creation *)
|
|
|
31 |
| Cast vname cname vname ("_:='(_')_" [99,99,99] 95) (* assignment, cast *)
|
|
|
32 |
| FAcc vname vname vnam ("_:=_.._" [99,99,99] 95) (* field access *)
|
|
|
33 |
| FAss vname vnam vname ("_.._:=_" [99,99,99] 95) (* field assigment *)
|
|
|
34 |
| Call vname cname vname mname vname (* method call *)
|
|
|
35 |
("_:={_}_.._'(_')" [99,99,99,99,99] 95)
|
|
|
36 |
| Meth cname mname (* virtual method *)
|
|
|
37 |
| Impl cname mname (* method implementation *)
|
|
|
38 |
|
|
|
39 |
(*###TO Product_Type_lemmas.ML*)
|
|
|
40 |
lemma pair_imageI [intro]: "(a, b) \<in> A ==> f a b : (%(a, b). f a b) ` A"
|
|
|
41 |
apply (rule_tac x = "(a,b)" in image_eqI)
|
|
|
42 |
apply auto
|
|
|
43 |
done
|
|
|
44 |
|
|
|
45 |
end
|
|
|
46 |
|