author | oheimb |
Tue, 12 Jun 2001 14:11:00 +0200 | |
changeset 11372 | 648795477bb5 |
parent 11070 | cc421547e744 |
child 12517 | 360e3215f029 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Decl.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
11372 | 4 |
Copyright 1999 Technische Universitaet Muenchen |
11070 | 5 |
*) |
8011 | 6 |
|
11070 | 7 |
header "Class Declarations and whole Programs" |
8011 | 8 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
9 |
theory Decl = Type: |
8011 | 10 |
|
11 |
types fdecl (* field declaration, cf. 8.3 (, 9.3) *) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
12 |
= "vname \<times> ty" |
8011 | 13 |
|
14 |
||
15 |
types sig (* signature of a method, cf. 8.4.2 *) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
16 |
= "mname \<times> ty list" |
8011 | 17 |
|
18 |
'c mdecl (* method declaration in a class *) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
19 |
= "sig \<times> ty \<times> 'c" |
8011 | 20 |
|
21 |
types 'c class (* class *) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
22 |
= "cname \<times> fdecl list \<times> 'c mdecl list" |
8011 | 23 |
(* superclass, fields, methods*) |
24 |
||
25 |
'c cdecl (* class declaration, cf. 8.1 *) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
26 |
= "cname \<times> 'c class" |
8011 | 27 |
|
28 |
consts |
|
29 |
||
30 |
Object :: cname (* name of root class *) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
31 |
ObjectC :: "'c cdecl" (* decl of root class *) |
8011 | 32 |
|
33 |
defs |
|
34 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
35 |
ObjectC_def: "ObjectC == (Object, (arbitrary, [], []))" |
8011 | 36 |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
37 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
38 |
types 'c prog = "'c cdecl list" |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
39 |
|
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
40 |
|
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
41 |
translations |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
42 |
"fdecl" <= (type) "vname \<times> ty" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
43 |
"sig" <= (type) "mname \<times> ty list" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
44 |
"mdecl c" <= (type) "sig \<times> ty \<times> c" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
45 |
"class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
46 |
"cdecl c" <= (type) "cname \<times> (c class)" |
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
47 |
"prog c" <= (type) "(c cdecl) list" |
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
48 |
|
10925
5ffe7ed8899a
is_class and class now as defs (rather than translations); corrected Digest.thy
oheimb
parents:
10613
diff
changeset
|
49 |
constdefs |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
50 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
51 |
class :: "'c prog => (cname \<leadsto> 'c class)" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
52 |
"class \<equiv> map_of" |
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
53 |
is_class :: "'c prog => cname => bool" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
54 |
"is_class G C \<equiv> class G C \<noteq> None" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
55 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
56 |
lemma finite_is_class: "finite {C. is_class G C}" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
57 |
apply (unfold is_class_def class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
58 |
apply (fold dom_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
59 |
apply (rule finite_dom_map_of) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
60 |
done |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
61 |
|
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
62 |
consts |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
63 |
|
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
64 |
is_type :: "'c prog => ty => bool" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
65 |
|
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
66 |
primrec |
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
67 |
"is_type G (PrimT pt) = True" |
10042 | 68 |
"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)" |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
69 |
|
8011 | 70 |
end |