author | wenzelm |
Sun, 02 Nov 2014 17:58:35 +0100 | |
changeset 58886 | 8a6cac7c7247 |
parent 42463 | f270e3e18be5 |
child 61361 | 8b5f00202e1a |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/Decl.thy |
2 |
Author: David von Oheimb |
|
11372 | 3 |
Copyright 1999 Technische Universitaet Muenchen |
11070 | 4 |
*) |
8011 | 5 |
|
58886 | 6 |
section {* Class Declarations and Programs *} |
8011 | 7 |
|
16417 | 8 |
theory Decl imports Type begin |
8011 | 9 |
|
42463 | 10 |
type_synonym |
12517 | 11 |
fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)" |
12 |
||
42463 | 13 |
type_synonym |
12517 | 14 |
sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2" |
15 |
||
42463 | 16 |
type_synonym |
12517 | 17 |
'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class" |
18 |
||
42463 | 19 |
type_synonym |
18551 | 20 |
'c "class" = "cname \<times> fdecl list \<times> 'c mdecl list" |
12517 | 21 |
-- "class = superclass, fields, methods" |
22 |
||
42463 | 23 |
type_synonym |
12517 | 24 |
'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1" |
25 |
||
42463 | 26 |
type_synonym |
12517 | 27 |
'c prog = "'c cdecl list" -- "program" |
8011 | 28 |
|
29 |
||
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
30 |
translations |
35431 | 31 |
(type) "fdecl" <= (type) "vname \<times> ty" |
32 |
(type) "sig" <= (type) "mname \<times> ty list" |
|
33 |
(type) "'c mdecl" <= (type) "sig \<times> ty \<times> 'c" |
|
34 |
(type) "'c class" <= (type) "cname \<times> fdecl list \<times> ('c mdecl) list" |
|
35 |
(type) "'c cdecl" <= (type) "cname \<times> ('c class)" |
|
36 |
(type) "'c prog" <= (type) "('c cdecl) list" |
|
10613
78b1d6c3ee9c
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10042
diff
changeset
|
37 |
|
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
38 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
18551
diff
changeset
|
39 |
definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where |
12517 | 40 |
"class \<equiv> map_of" |
41 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
18551
diff
changeset
|
42 |
definition is_class :: "'c prog => cname => bool" where |
12517 | 43 |
"is_class G C \<equiv> class G C \<noteq> None" |
44 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
45 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
46 |
lemma finite_is_class: "finite {C. is_class G C}" |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
47 |
apply (unfold is_class_def class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
48 |
apply (fold dom_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
49 |
apply (rule finite_dom_map_of) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10925
diff
changeset
|
50 |
done |
9346
297dcbf64526
re-structuring MicroJava; added Example; corrected := syntax; simplfied cast
oheimb
parents:
8011
diff
changeset
|
51 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
18551
diff
changeset
|
52 |
primrec is_type :: "'c prog => ty => bool" where |
12517 | 53 |
"is_type G (PrimT pt) = True" |
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
18551
diff
changeset
|
54 |
| "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
|
55 |
|
8011 | 56 |
end |