author | Andreas Lochbihler |
Fri, 05 Aug 2011 14:16:44 +0200 | |
changeset 44035 | 322d1657c40c |
parent 35102 | cc7a0b9f938c |
child 44037 | 25011c3a5c3d |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Type.thy |
2 |
Author: David von Oheimb |
|
3 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 4 |
*) |
8011 | 5 |
|
12911 | 6 |
header {* \isaheader{Java types} *} |
8011 | 7 |
|
16417 | 8 |
theory Type imports JBasis begin |
8011 | 9 |
|
12517 | 10 |
typedecl cnam |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
11 |
instantiation cnam :: equal begin |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
12 |
definition "HOL.equal (cn :: cnam) cn' \<longleftrightarrow> cn = cn'" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
13 |
instance proof qed(simp add: equal_cnam_def) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
14 |
end |
12517 | 15 |
|
16 |
-- "exceptions" |
|
17 |
datatype |
|
18 |
xcpt |
|
19 |
= NullPointer |
|
20 |
| ClassCast |
|
21 |
| OutOfMemory |
|
8011 | 22 |
|
12517 | 23 |
-- "class names" |
24 |
datatype cname |
|
25 |
= Object |
|
26 |
| Xcpt xcpt |
|
12951 | 27 |
| Cname cnam |
12517 | 28 |
|
29 |
typedecl vnam -- "variable or field name" |
|
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
30 |
instantiation vnam :: equal begin |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
31 |
definition "HOL.equal (vn :: vnam) vn' \<longleftrightarrow> vn = vn'" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
32 |
instance proof qed(simp add: equal_vnam_def) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
33 |
end |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
34 |
|
12517 | 35 |
typedecl mname -- "method name" |
44035
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
36 |
instantiation mname :: equal begin |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
37 |
definition "HOL.equal (M :: mname) M' \<longleftrightarrow> M = M'" |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
38 |
instance proof qed(simp add: equal_mname_def) |
322d1657c40c
replace old SML code generator by new code generator in MicroJava/JVM and /BV
Andreas Lochbihler
parents:
35102
diff
changeset
|
39 |
end |
12517 | 40 |
|
41 |
-- "names for @{text This} pointer and local/field variables" |
|
42 |
datatype vname |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
43 |
= This |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
44 |
| VName vnam |
8011 | 45 |
|
12517 | 46 |
-- "primitive type, cf. 4.2" |
47 |
datatype prim_ty |
|
48 |
= Void -- "'result type' of void methods" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
49 |
| Boolean |
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
50 |
| Integer |
8011 | 51 |
|
12517 | 52 |
-- "reference type, cf. 4.3" |
53 |
datatype ref_ty |
|
54 |
= NullT -- "null type, cf. 4.1" |
|
55 |
| ClassT cname -- "class type" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
56 |
|
12517 | 57 |
-- "any type, cf. 4.1" |
58 |
datatype ty |
|
59 |
= PrimT prim_ty -- "primitive type" |
|
60 |
| RefT ref_ty -- "reference type" |
|
8011 | 61 |
|
35102 | 62 |
abbreviation NT :: ty |
63 |
where "NT == RefT NullT" |
|
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset
|
64 |
|
35102 | 65 |
abbreviation Class :: "cname => ty" |
66 |
where "Class C == RefT (ClassT C)" |
|
8011 | 67 |
|
68 |
end |