--- a/src/HOL/MicroJava/J/Conform.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Conform.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-Conformity relations for type safety of Java
-*)
+header "Conformity Relations for Type Soundness Proof"
theory Conform = State + WellType:
--- a/src/HOL/MicroJava/J/Decl.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Decl.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
+*)
-Class declarations and programs
-*)
+header "Class Declarations and whole Programs"
theory Decl = Type:
--- a/src/HOL/MicroJava/J/Eval.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Eval.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,10 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-Operational evaluation (big-step) semantics of the
-execution of Java expressions and statements
-*)
+header "Operational Evaluation (big-step) Semantics"
theory Eval = State + WellType:
--- a/src/HOL/MicroJava/J/Example.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,14 +2,22 @@
ID: $Id$
Author: David von Oheimb
Copyright 1997 Technische Universitaet Muenchen
+*)
-The following example Bali program includes:
+header "Example MicroJava Program"
+
+theory Example = Eval:
+
+text {*
+The following example MicroJava program includes:
class declarations with inheritance, hiding of fields, and overriding of
methods (with refined result type),
instance creation, local assignment, sequential composition,
method call with dynamic binding, literal values,
- expression statement, local access, type cast, field assignment (in part), skip
+ expression statement, local access, type cast, field assignment (in part),
+ skip.
+\begin{verbatim}
class Base {
boolean vee;
Base foo(Base x) {return x;}
@@ -26,9 +34,8 @@
e.foo(null);
}
}
-*)
-
-theory Example = Eval:
+\end{verbatim}
+*}
datatype cnam_ = Base_ | Ext_
datatype vnam_ = vee_ | x_ | e_
--- a/src/HOL/MicroJava/J/JBasis.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/JBasis.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 TU Muenchen
+*)
-Some auxiliary definitions.
-*)
+header "Some Auxiliary Definitions"
theory JBasis = Main:
@@ -14,8 +14,8 @@
constdefs
- unique :: "('a \\<times> 'b) list => bool"
- "unique == nodups \\<circ> map fst"
+ unique :: "('a \<times> 'b) list => bool"
+ "unique == nodups \<circ> map fst"
lemma fst_in_set_lemma [rule_format (no_asm)]:
@@ -55,7 +55,7 @@
done
lemma Ball_set_table_:
- "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)"
+ "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
apply(induct_tac "l")
apply(simp_all (no_asm))
apply safe
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-Type Safety Proof for MicroJava
-*)
+header "Type Safety Proof"
theory JTypeSafe = Eval + Conform:
@@ -280,7 +280,7 @@
apply( fast intro: hext_trans)
apply( simp)
apply( drule eval_no_xcpt)
-apply( erule FAss_type_sound, simp (no_asm) (*###rule refl*), assumption+)
+apply( erule FAss_type_sound, rule HOL.refl, assumption+)
apply( tactic prune_params_tac)
(* Level 52 *)
--- a/src/HOL/MicroJava/J/State.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/State.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-State for evaluation of Java expressions and statements
-*)
+header "Program State"
theory State = TypeRel + Value:
--- a/src/HOL/MicroJava/J/Term.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Term.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-Java expressions and statements
-*)
+header "Expressions and Statements"
theory Term = Value:
--- a/src/HOL/MicroJava/J/Type.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Type.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-Java types
-*)
+header "Java types"
theory Type = JBasis:
--- a/src/HOL/MicroJava/J/TypeRel.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/TypeRel.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-The relations between Java types
-*)
+header "Relations between Java Types"
theory TypeRel = Decl:
--- a/src/HOL/MicroJava/J/Value.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/Value.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,9 +2,9 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-Java values
-*)
+header "Java Values"
theory Value = Type:
--- a/src/HOL/MicroJava/J/WellForm.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/WellForm.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,20 +2,28 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
-
-Well-formedness of Java programs
-for static checks on expressions and statements, see WellType.thy
+*)
-improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
-* a method implementing or overwriting another method may have a result type
- that widens to the result type of the other method (instead of identical type)
-
-simplifications:
-* for uniformity, Object is assumed to be declared like any other class
-*)
+header "Well-formedness of Java programs"
theory WellForm = TypeRel:
+text {*
+for static checks on expressions and statements, see WellType.
+
+\begin{description}
+\item[improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):]\ \\
+\begin{itemize}
+\item a method implementing or overwriting another method may have a result type
+that widens to the result type of the other method (instead of identical type)
+\end{itemize}
+
+\item[simplifications:]\ \\
+\begin{itemize}
+\item for uniformity, Object is assumed to be declared like any other class
+\end{itemize}
+\end{description}
+*}
types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
constdefs
--- a/src/HOL/MicroJava/J/WellType.thy Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/J/WellType.thy Mon Feb 05 20:14:15 2001 +0100
@@ -2,21 +2,25 @@
ID: $Id$
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
+*)
-Well-typedness of Java programs
+header "Well-typedness Constraints"
+theory WellType = Term + WellForm:
+
+text {*
the formulation of well-typedness of method calls given below (as well as
the Java Specification 1.0) is a little too restrictive: Is does not allow
methods of class Object to be called upon references of interface type.
-simplifications:
-* the type rules include all static checks on expressions and statements, e.g.
- definedness of names (of parameters, locals, fields, methods)
-
-*)
-
-theory WellType = Term + WellForm:
-
+\begin{description}
+\item[simplifications:]\ \\
+\begin{itemize}
+\item the type rules include all static checks on expressions and statements,
+ e.g.\ definedness of names (of parameters, locals, fields, methods)
+\end{itemize}
+\end{description}
+*}
types lenv (* local variables, including method parameters and This *)
= "vname \<leadsto> ty"
'c env
--- a/src/HOL/MicroJava/ROOT.ML Mon Feb 05 14:59:44 2001 +0100
+++ b/src/HOL/MicroJava/ROOT.ML Mon Feb 05 20:14:15 2001 +0100
@@ -1,4 +1,3 @@
-
goals_limit := 1;
add_path "J";