improved document (added headers etc)
authoroheimb
Mon Feb 05 20:14:15 2001 +0100 (2001-02-05)
changeset 11070cc421547e744
parent 11069 4f6fd393713f
child 11071 4e542a09b582
improved document (added headers etc)
src/HOL/MicroJava/J/Conform.thy
src/HOL/MicroJava/J/Decl.thy
src/HOL/MicroJava/J/Eval.thy
src/HOL/MicroJava/J/Example.thy
src/HOL/MicroJava/J/JBasis.thy
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/MicroJava/J/State.thy
src/HOL/MicroJava/J/Term.thy
src/HOL/MicroJava/J/Type.thy
src/HOL/MicroJava/J/TypeRel.thy
src/HOL/MicroJava/J/Value.thy
src/HOL/MicroJava/J/WellForm.thy
src/HOL/MicroJava/J/WellType.thy
src/HOL/MicroJava/ROOT.ML
     1.1 --- a/src/HOL/MicroJava/J/Conform.thy	Mon Feb 05 14:59:44 2001 +0100
     1.2 +++ b/src/HOL/MicroJava/J/Conform.thy	Mon Feb 05 20:14:15 2001 +0100
     1.3 @@ -2,9 +2,9 @@
     1.4      ID:         $Id$
     1.5      Author:     David von Oheimb
     1.6      Copyright   1999 Technische Universitaet Muenchen
     1.7 +*)
     1.8  
     1.9 -Conformity relations for type safety of Java
    1.10 -*)
    1.11 +header "Conformity Relations for Type Soundness Proof"
    1.12  
    1.13  theory Conform = State + WellType:
    1.14  
     2.1 --- a/src/HOL/MicroJava/J/Decl.thy	Mon Feb 05 14:59:44 2001 +0100
     2.2 +++ b/src/HOL/MicroJava/J/Decl.thy	Mon Feb 05 20:14:15 2001 +0100
     2.3 @@ -2,9 +2,9 @@
     2.4      ID:         $Id$
     2.5      Author:     David von Oheimb
     2.6      Copyright   1997 Technische Universitaet Muenchen
     2.7 +*)
     2.8  
     2.9 -Class declarations and programs
    2.10 -*)
    2.11 +header "Class Declarations and whole Programs"
    2.12  
    2.13  theory Decl = Type:
    2.14  
     3.1 --- a/src/HOL/MicroJava/J/Eval.thy	Mon Feb 05 14:59:44 2001 +0100
     3.2 +++ b/src/HOL/MicroJava/J/Eval.thy	Mon Feb 05 20:14:15 2001 +0100
     3.3 @@ -2,10 +2,9 @@
     3.4      ID:         $Id$
     3.5      Author:     David von Oheimb
     3.6      Copyright   1999 Technische Universitaet Muenchen
     3.7 +*)
     3.8  
     3.9 -Operational evaluation (big-step) semantics of the 
    3.10 -execution of Java expressions and statements
    3.11 -*)
    3.12 +header "Operational Evaluation (big-step) Semantics"
    3.13  
    3.14  theory Eval = State + WellType:
    3.15  
     4.1 --- a/src/HOL/MicroJava/J/Example.thy	Mon Feb 05 14:59:44 2001 +0100
     4.2 +++ b/src/HOL/MicroJava/J/Example.thy	Mon Feb 05 20:14:15 2001 +0100
     4.3 @@ -2,14 +2,22 @@
     4.4      ID:         $Id$
     4.5      Author:     David von Oheimb
     4.6      Copyright   1997 Technische Universitaet Muenchen
     4.7 +*)
     4.8  
     4.9 -The following example Bali program includes:
    4.10 +header "Example MicroJava Program"
    4.11 +
    4.12 +theory Example = Eval:
    4.13 +
    4.14 +text {* 
    4.15 +The following example MicroJava program includes:
    4.16   class declarations with inheritance, hiding of fields, and overriding of
    4.17    methods (with refined result type), 
    4.18   instance creation, local assignment, sequential composition,
    4.19   method call with dynamic binding, literal values,
    4.20 - expression statement, local access, type cast, field assignment (in part), skip
    4.21 + expression statement, local access, type cast, field assignment (in part), 
    4.22 + skip.
    4.23  
    4.24 +\begin{verbatim}
    4.25  class Base {
    4.26    boolean vee;
    4.27    Base foo(Base x) {return x;}
    4.28 @@ -26,9 +34,8 @@
    4.29      e.foo(null);
    4.30    }
    4.31  }
    4.32 -*)
    4.33 -
    4.34 -theory Example = Eval:
    4.35 +\end{verbatim}
    4.36 +*}
    4.37  
    4.38  datatype cnam_ = Base_ | Ext_
    4.39  datatype vnam_ = vee_ | x_ | e_
     5.1 --- a/src/HOL/MicroJava/J/JBasis.thy	Mon Feb 05 14:59:44 2001 +0100
     5.2 +++ b/src/HOL/MicroJava/J/JBasis.thy	Mon Feb 05 20:14:15 2001 +0100
     5.3 @@ -2,9 +2,9 @@
     5.4      ID:         $Id$
     5.5      Author:     David von Oheimb
     5.6      Copyright   1999 TU Muenchen
     5.7 +*)
     5.8  
     5.9 -Some auxiliary definitions.
    5.10 -*)
    5.11 +header "Some Auxiliary Definitions"
    5.12  
    5.13  theory JBasis = Main: 
    5.14  
    5.15 @@ -14,8 +14,8 @@
    5.16   
    5.17  constdefs
    5.18  
    5.19 -  unique  :: "('a \\<times> 'b) list => bool"
    5.20 - "unique  == nodups \\<circ> map fst"
    5.21 +  unique  :: "('a \<times> 'b) list => bool"
    5.22 + "unique  == nodups \<circ> map fst"
    5.23  
    5.24  
    5.25  lemma fst_in_set_lemma [rule_format (no_asm)]: 
    5.26 @@ -55,7 +55,7 @@
    5.27  done
    5.28  
    5.29  lemma Ball_set_table_: 
    5.30 -  "(\\<forall>(x,y)\\<in>set l. P x y) --> (\\<forall>x. \\<forall>y. map_of l x = Some y --> P x y)"
    5.31 +  "(\<forall>(x,y)\<in>set l. P x y) --> (\<forall>x. \<forall>y. map_of l x = Some y --> P x y)"
    5.32  apply(induct_tac "l")
    5.33  apply(simp_all (no_asm))
    5.34  apply safe
     6.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Feb 05 14:59:44 2001 +0100
     6.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Feb 05 20:14:15 2001 +0100
     6.3 @@ -2,9 +2,9 @@
     6.4      ID:         $Id$
     6.5      Author:     David von Oheimb
     6.6      Copyright   1999 Technische Universitaet Muenchen
     6.7 +*)
     6.8  
     6.9 -Type Safety Proof for MicroJava
    6.10 -*)
    6.11 +header "Type Safety Proof"
    6.12  
    6.13  theory JTypeSafe = Eval + Conform:
    6.14  
    6.15 @@ -280,7 +280,7 @@
    6.16  apply(  fast intro: hext_trans)
    6.17  apply( simp)
    6.18  apply( drule eval_no_xcpt)
    6.19 -apply( erule FAss_type_sound, simp (no_asm) (*###rule refl*), assumption+)
    6.20 +apply( erule FAss_type_sound, rule HOL.refl, assumption+)
    6.21  
    6.22  apply( tactic prune_params_tac)
    6.23  (* Level 52 *)
     7.1 --- a/src/HOL/MicroJava/J/State.thy	Mon Feb 05 14:59:44 2001 +0100
     7.2 +++ b/src/HOL/MicroJava/J/State.thy	Mon Feb 05 20:14:15 2001 +0100
     7.3 @@ -2,9 +2,9 @@
     7.4      ID:         $Id$
     7.5      Author:     David von Oheimb
     7.6      Copyright   1999 Technische Universitaet Muenchen
     7.7 +*)
     7.8  
     7.9 -State for evaluation of Java expressions and statements
    7.10 -*)
    7.11 +header "Program State"
    7.12  
    7.13  theory State = TypeRel + Value:
    7.14  
     8.1 --- a/src/HOL/MicroJava/J/Term.thy	Mon Feb 05 14:59:44 2001 +0100
     8.2 +++ b/src/HOL/MicroJava/J/Term.thy	Mon Feb 05 20:14:15 2001 +0100
     8.3 @@ -2,9 +2,9 @@
     8.4      ID:         $Id$
     8.5      Author:     David von Oheimb
     8.6      Copyright   1999 Technische Universitaet Muenchen
     8.7 +*)
     8.8  
     8.9 -Java expressions and statements
    8.10 -*)
    8.11 +header "Expressions and Statements"
    8.12  
    8.13  theory Term = Value:
    8.14  
     9.1 --- a/src/HOL/MicroJava/J/Type.thy	Mon Feb 05 14:59:44 2001 +0100
     9.2 +++ b/src/HOL/MicroJava/J/Type.thy	Mon Feb 05 20:14:15 2001 +0100
     9.3 @@ -2,9 +2,9 @@
     9.4      ID:         $Id$
     9.5      Author:     David von Oheimb
     9.6      Copyright   1999 Technische Universitaet Muenchen
     9.7 +*)
     9.8  
     9.9 -Java types
    9.10 -*)
    9.11 +header "Java types"
    9.12  
    9.13  theory Type = JBasis:
    9.14  
    10.1 --- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Feb 05 14:59:44 2001 +0100
    10.2 +++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Feb 05 20:14:15 2001 +0100
    10.3 @@ -2,9 +2,9 @@
    10.4      ID:         $Id$
    10.5      Author:     David von Oheimb
    10.6      Copyright   1999 Technische Universitaet Muenchen
    10.7 +*)
    10.8  
    10.9 -The relations between Java types
   10.10 -*)
   10.11 +header "Relations between Java Types"
   10.12  
   10.13  theory TypeRel = Decl:
   10.14  
    11.1 --- a/src/HOL/MicroJava/J/Value.thy	Mon Feb 05 14:59:44 2001 +0100
    11.2 +++ b/src/HOL/MicroJava/J/Value.thy	Mon Feb 05 20:14:15 2001 +0100
    11.3 @@ -2,9 +2,9 @@
    11.4      ID:         $Id$
    11.5      Author:     David von Oheimb
    11.6      Copyright   1999 Technische Universitaet Muenchen
    11.7 +*)
    11.8  
    11.9 -Java values
   11.10 -*)
   11.11 +header "Java Values"
   11.12  
   11.13  theory Value = Type:
   11.14  
    12.1 --- a/src/HOL/MicroJava/J/WellForm.thy	Mon Feb 05 14:59:44 2001 +0100
    12.2 +++ b/src/HOL/MicroJava/J/WellForm.thy	Mon Feb 05 20:14:15 2001 +0100
    12.3 @@ -2,20 +2,28 @@
    12.4      ID:         $Id$
    12.5      Author:     David von Oheimb
    12.6      Copyright   1999 Technische Universitaet Muenchen
    12.7 -
    12.8 -Well-formedness of Java programs
    12.9 -for static checks on expressions and statements, see WellType.thy
   12.10 +*)
   12.11  
   12.12 -improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
   12.13 -* a method implementing or overwriting another method may have a result type 
   12.14 -  that widens to the result type of the other method (instead of identical type)
   12.15 -
   12.16 -simplifications:
   12.17 -* for uniformity, Object is assumed to be declared like any other class
   12.18 -*)
   12.19 +header "Well-formedness of Java programs"
   12.20  
   12.21  theory WellForm = TypeRel:
   12.22  
   12.23 +text {*
   12.24 +for static checks on expressions and statements, see WellType.
   12.25 +
   12.26 +\begin{description}
   12.27 +\item[improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):]\ \\
   12.28 +\begin{itemize}
   12.29 +\item a method implementing or overwriting another method may have a result type
   12.30 +that widens to the result type of the other method (instead of identical type)
   12.31 +\end{itemize}
   12.32 +
   12.33 +\item[simplifications:]\ \\
   12.34 +\begin{itemize}
   12.35 +\item for uniformity, Object is assumed to be declared like any other class
   12.36 +\end{itemize}
   12.37 +\end{description}
   12.38 +*}
   12.39  types 'c wf_mb = "'c prog => cname => 'c mdecl => bool"
   12.40  
   12.41  constdefs
    13.1 --- a/src/HOL/MicroJava/J/WellType.thy	Mon Feb 05 14:59:44 2001 +0100
    13.2 +++ b/src/HOL/MicroJava/J/WellType.thy	Mon Feb 05 20:14:15 2001 +0100
    13.3 @@ -2,21 +2,25 @@
    13.4      ID:         $Id$
    13.5      Author:     David von Oheimb
    13.6      Copyright   1999 Technische Universitaet Muenchen
    13.7 +*)
    13.8  
    13.9 -Well-typedness of Java programs
   13.10 +header "Well-typedness Constraints"
   13.11  
   13.12 +theory WellType = Term + WellForm:
   13.13 +
   13.14 +text {*
   13.15  the formulation of well-typedness of method calls given below (as well as
   13.16  the Java Specification 1.0) is a little too restrictive: Is does not allow
   13.17  methods of class Object to be called upon references of interface type.
   13.18  
   13.19 -simplifications:
   13.20 -* the type rules include all static checks on expressions and statements, e.g.
   13.21 -  definedness of names (of parameters, locals, fields, methods)
   13.22 -
   13.23 -*)
   13.24 -
   13.25 -theory WellType = Term + WellForm:
   13.26 -
   13.27 +\begin{description}
   13.28 +\item[simplifications:]\ \\
   13.29 +\begin{itemize}
   13.30 +\item the type rules include all static checks on expressions and statements, 
   13.31 +  e.g.\ definedness of names (of parameters, locals, fields, methods)
   13.32 +\end{itemize}
   13.33 +\end{description}
   13.34 +*}
   13.35  types	lenv (* local variables, including method parameters and This *)
   13.36  	= "vname \<leadsto> ty"
   13.37          'c env
    14.1 --- a/src/HOL/MicroJava/ROOT.ML	Mon Feb 05 14:59:44 2001 +0100
    14.2 +++ b/src/HOL/MicroJava/ROOT.ML	Mon Feb 05 20:14:15 2001 +0100
    14.3 @@ -1,4 +1,3 @@
    14.4 -
    14.5  goals_limit := 1;
    14.6  
    14.7  add_path "J";