--- a/src/HOL/MicroJava/J/Decl.thy Sun Dec 16 00:17:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Sun Dec 16 00:18:17 2001 +0100
@@ -4,38 +4,28 @@
Copyright 1999 Technische Universitaet Muenchen
*)
-header "Class Declarations and whole Programs"
+header "Class Declarations and Programs"
theory Decl = Type:
-types fdecl (* field declaration, cf. 8.3 (, 9.3) *)
- = "vname \<times> ty"
+types
+ fdecl = "vname \<times> ty" -- "field declaration, cf. 8.3 (, 9.3)"
+
+ sig = "mname \<times> ty list" -- "signature of a method, cf. 8.4.2"
+
+ 'c mdecl = "sig \<times> ty \<times> 'c" -- "method declaration in a class"
+
+ 'c class = "cname \<times> fdecl list \<times> 'c mdecl list"
+ -- "class = superclass, fields, methods"
+
+ 'c cdecl = "cname \<times> 'c class" -- "class declaration, cf. 8.1"
+
+ 'c prog = "'c cdecl list" -- "program"
-types sig (* signature of a method, cf. 8.4.2 *)
- = "mname \<times> ty list"
-
- 'c mdecl (* method declaration in a class *)
- = "sig \<times> ty \<times> 'c"
-
-types 'c class (* class *)
- = "cname \<times> fdecl list \<times> 'c mdecl list"
- (* superclass, fields, methods*)
-
- 'c cdecl (* class declaration, cf. 8.1 *)
- = "cname \<times> 'c class"
-
-consts
-
- Object :: cname (* name of root class *)
- ObjectC :: "'c cdecl" (* decl of root class *)
-
-defs
-
- ObjectC_def: "ObjectC == (Object, (arbitrary, [], []))"
-
-
-types 'c prog = "'c cdecl list"
+constdefs
+ ObjectC :: "'c cdecl" -- "decl of root class"
+ "ObjectC \<equiv> (Object, (arbitrary, [], []))"
translations
@@ -46,12 +36,14 @@
"cdecl c" <= (type) "cname \<times> (c class)"
"prog c" <= (type) "(c cdecl) list"
-constdefs
- class :: "'c prog => (cname \<leadsto> 'c class)"
- "class \<equiv> map_of"
- is_class :: "'c prog => cname => bool"
- "is_class G C \<equiv> class G C \<noteq> None"
+constdefs
+ class :: "'c prog => (cname \<leadsto> 'c class)"
+ "class \<equiv> map_of"
+
+ is_class :: "'c prog => cname => bool"
+ "is_class G C \<equiv> class G C \<noteq> None"
+
lemma finite_is_class: "finite {C. is_class G C}"
apply (unfold is_class_def class_def)
@@ -60,11 +52,9 @@
done
consts
-
- is_type :: "'c prog => ty => bool"
-
+ is_type :: "'c prog => ty => bool"
primrec
-"is_type G (PrimT pt) = True"
-"is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
+ "is_type G (PrimT pt) = True"
+ "is_type G (RefT t) = (case t of NullT => True | ClassT C => is_class G C)"
end