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