equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/J/Decl.thy |
1 (* Title: HOL/MicroJava/J/Decl.thy |
2 ID: $Id$ |
|
3 Author: David von Oheimb |
2 Author: David von Oheimb |
4 Copyright 1999 Technische Universitaet Muenchen |
3 Copyright 1999 Technische Universitaet Muenchen |
5 *) |
4 *) |
6 |
5 |
7 header {* \isaheader{Class Declarations and Programs} *} |
6 header {* \isaheader{Class Declarations and Programs} *} |
30 "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list" |
29 "class c" <= (type) "cname \<times> fdecl list \<times> (c mdecl) list" |
31 "cdecl c" <= (type) "cname \<times> (c class)" |
30 "cdecl c" <= (type) "cname \<times> (c class)" |
32 "prog c" <= (type) "(c cdecl) list" |
31 "prog c" <= (type) "(c cdecl) list" |
33 |
32 |
34 |
33 |
35 constdefs |
34 definition "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" where |
36 "class" :: "'c prog => (cname \<rightharpoonup> 'c class)" |
|
37 "class \<equiv> map_of" |
35 "class \<equiv> map_of" |
38 |
36 |
39 is_class :: "'c prog => cname => bool" |
37 definition is_class :: "'c prog => cname => bool" where |
40 "is_class G C \<equiv> class G C \<noteq> None" |
38 "is_class G C \<equiv> class G C \<noteq> None" |
41 |
39 |
42 |
40 |
43 lemma finite_is_class: "finite {C. is_class G C}" |
41 lemma finite_is_class: "finite {C. is_class G C}" |
44 apply (unfold is_class_def class_def) |
42 apply (unfold is_class_def class_def) |
45 apply (fold dom_def) |
43 apply (fold dom_def) |
46 apply (rule finite_dom_map_of) |
44 apply (rule finite_dom_map_of) |
47 done |
45 done |
48 |
46 |
49 consts |
47 primrec is_type :: "'c prog => ty => bool" where |
50 is_type :: "'c prog => ty => bool" |
|
51 primrec |
|
52 "is_type G (PrimT pt) = True" |
48 "is_type G (PrimT pt) = True" |
53 "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)" |
49 | "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)" |
54 |
50 |
55 end |
51 end |