src/HOL/Bali/WellForm.thy
author schirmer
Thu, 31 Oct 2002 18:27:10 +0100
changeset 13688 a0b16d42d489
parent 13601 fd3e3d6b37b2
child 14025 d9b155757dc8
permissions -rw-r--r--
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/WellForm.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
     3
    Author:     David von Oheimb and Norbert Schirmer
12858
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
header {* Well-formedness of Java programs *}
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
     8
theory WellForm = DefiniteAssignment:
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
For static checks on expressions and statements, see WellType.thy
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1):
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
\item a method implementing or overwriting another method may have a result 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
      type that widens to the result type of the other method 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
      (instead of identical type)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
\item if a method hides another method (both methods have to be static!)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
  there are no restrictions to the result type 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
  since the methods have to be static and there is no dynamic binding of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
  static methods
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
\item if an interface inherits more than one method with the same signature, the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
  methods need not have identical return types
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
\item Object and standard exceptions are assumed to be declared like normal 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
      classes
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
section "well-formed field declarations"
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    33
text  {* well-formed field declaration (common part for classes and interfaces),
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
    34
        cf. 8.3 and (9.3) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
  wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
 "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
apply (unfold wf_fdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
section "well-formed method declarations"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
  (*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
  (* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
A method head is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
\item the signature and the method head agree in the number of parameters
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
\item all types of the parameters are visible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
\item the result type is visible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
\item the parameter names are unique
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
\end{itemize} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
  wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    62
 "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
			    \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    64
                            is_acc_type G P (resTy mh) \<and>
12893
cbb4dc5e6478 replaced nodups by distinct;
wenzelm
parents: 12858
diff changeset
    65
			    \<spacespace> distinct (pars mh)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
A method declaration is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
\item the method head is wellformed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
\item the names of the local variables are unique
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
\item the types of the local variables must be accessible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
\item the local variables don't shadow the parameters
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
\item the class of the method is defined
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
\item the body statement is welltyped with respect to the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
      modified environment of local names, were the local variables, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
      the parameters the special result variable (Res) and This are assoziated
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
      with there types. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    82
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    83
constdefs callee_lcl:: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    84
"callee_lcl C sig m 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    85
 \<equiv> \<lambda> k. (case k of
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    86
            EName e 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    87
            \<Rightarrow> (case e of 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    88
                  VNam v 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    89
                  \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    90
                | Res \<Rightarrow> Some (resTy m))
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    91
	  | This \<Rightarrow> if is_static m then None else Some (Class C))"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    92
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    93
constdefs parameters :: "methd \<Rightarrow> lname set"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    94
"parameters m \<equiv>  set (map (EName \<circ> VNam) (pars m)) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    95
                  \<union> (if (static m) then {} else {This})"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
    96
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
  wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
 "wf_mdecl G C \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   100
      \<lambda>(sig,m).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
	  wf_mhead G (pid C) sig (mhead m) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
          unique (lcls (mbody m)) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   103
          (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   104
	  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and>
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   105
          jumpNestingOkS {Ret} (stmt (mbody m)) \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   106
          is_class G C \<and>
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   107
          \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   108
          (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   109
                \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   110
               \<and> Result \<in> nrm A)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   111
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   112
lemma callee_lcl_VNam_simp [simp]:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   113
"callee_lcl C sig m (EName (VNam v)) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   114
  = (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   115
by (simp add: callee_lcl_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   116
 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   117
lemma callee_lcl_Res_simp [simp]:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   118
"callee_lcl C sig m (EName Res) = Some (resTy m)" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   119
by (simp add: callee_lcl_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   120
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   121
lemma callee_lcl_This_simp [simp]:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   122
"callee_lcl C sig m (This) = (if is_static m then None else Some (Class C))" 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   123
by (simp add: callee_lcl_def)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   124
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   125
lemma callee_lcl_This_static_simp:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   126
"is_static m \<Longrightarrow> callee_lcl C sig m (This) = None"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   127
by simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   128
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   129
lemma callee_lcl_This_not_static_simp:
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   130
"\<not> is_static m \<Longrightarrow> callee_lcl C sig m (This) = Some (Class C)"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   131
by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
lemma wf_mheadI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   134
"\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T;
12893
cbb4dc5e6478 replaced nodups by distinct;
wenzelm
parents: 12858
diff changeset
   135
  is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow>  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
  wf_mhead G P sig m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
apply (unfold wf_mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
apply (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
lemma wf_mdeclI: "\<lbrakk>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
  wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   144
  \<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T;
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   145
  jumpNestingOkS {Ret} (stmt (mbody m));
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   146
  is_class G C;
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   147
  \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   148
  (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   149
        \<and> Result \<in> nrm A)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
  \<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
  wf_mdecl G C (sig,m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
apply (unfold wf_mdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   155
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   156
lemma wf_mdeclE [consumes 1]:  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   157
  "\<lbrakk>wf_mdecl G C (sig,m); 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   158
    \<lbrakk>wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   159
     \<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None; 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   160
     \<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   161
     jumpNestingOkS {Ret} (stmt (mbody m));
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   162
     is_class G C;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   163
     \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   164
   (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   165
        \<and> Result \<in> nrm A)
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   166
    \<rbrakk> \<Longrightarrow> P
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   167
  \<rbrakk> \<Longrightarrow> P"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   168
by (unfold wf_mdecl_def) simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   169
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
lemma wf_mdeclD1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
"wf_mdecl G C (sig,m) \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
   wf_mhead G (pid C) sig (mhead m) \<and> unique (lcls (mbody m)) \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
  (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   176
apply (unfold wf_mdecl_def)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   177
apply simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
lemma wf_mdecl_bodyD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   181
"wf_mdecl G C (sig,m) \<Longrightarrow>  
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   182
 (\<exists>T. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>Body C (stmt (mbody m))\<Colon>-T \<and> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   183
      G\<turnstile>T\<preceq>(resTy m))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
apply (unfold wf_mdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
apply (rule_tac x="(resTy m)" in exI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
apply (unfold wf_mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   190
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   191
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   192
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
lemma static_Object_methodsE [elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
 "\<lbrakk>wf_mdecl G Object (sig, m);static m\<rbrakk> \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
apply (unfold wf_mdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
lemma rT_is_acc_type: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
  "wf_mhead G P sig m \<Longrightarrow> is_acc_type G P (resTy m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
apply (unfold wf_mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
section "well-formed interface declarations"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
  (* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
A interface declaration is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
\item the interface hierarchy is wellstructured
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
\item there is no class with the same name
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
\item the method heads are wellformed and not static and have Public access
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
\item the methods are uniquely named
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
\item all superinterfaces are accessible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
\item the result type of a method overriding a method of Object widens to the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
      result type of the overridden method.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
      Shadowing static methods is forbidden.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
\item the result type of a method overriding a set of methods defined in the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
      superinterfaces widens to each of the corresponding result types
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
  wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
 "wf_idecl G \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
    \<lambda>(I,i). 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   228
        ws_idecl G I (isuperIfs i) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   229
	\<not>is_class G I \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
	(\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
                                     \<not>is_static mh \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   232
                                      accmodi mh = Public) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
	unique (imethods i) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
        (\<forall> J\<in>set (isuperIfs i). is_acc_iface G (pid I) J) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
        (table_of (imethods i)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
          hiding (methd G Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
          under  (\<lambda> new old. accmodi old \<noteq> Private)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
          entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   239
                             is_static new = is_static old)) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
        (o2s \<circ> table_of (imethods i) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   241
               hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
	       entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   244
lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
  wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
apply (unfold wf_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
lemma wf_idecl_hidings: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   251
"wf_idecl G (I, i) \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
  (\<lambda>s. o2s (table_of (imethods i) s)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
  hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
  entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
apply (unfold wf_idecl_def o_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
lemma wf_idecl_hiding:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
"wf_idecl G (I, i) \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
 (table_of (imethods i)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
           hiding (methd G Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
           under  (\<lambda> new old. accmodi old \<noteq> Private)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
           entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
                              is_static new = is_static old))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
apply (unfold wf_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
lemma wf_idecl_supD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
"\<lbrakk>wf_idecl G (I,i); J \<in> set (isuperIfs i)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
 \<Longrightarrow> is_acc_iface G (pid I) J \<and> (J, I) \<notin> (subint1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
apply (unfold wf_idecl_def ws_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
section "well-formed class declarations"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   278
  (* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   279
   class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
A class declaration is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
\item there is no interface with the same name
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
\item all superinterfaces are accessible and for all methods implementing 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
      an interface method the result type widens to the result type of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
      the interface method, the method is not static and offers at least 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
      as much access 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
      (this actually means that the method has Public access, since all 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
      interface methods have public access)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
\item all field declarations are wellformed and the field names are unique
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
\item all method declarations are wellformed and the method names are unique
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
\item the initialization statement is welltyped
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
\item the classhierarchy is wellstructured
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
\item Unless the class is Object:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
      \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
      \item the superclass is accessible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
      \item for all methods overriding another method (of a superclass )the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
            result type widens to the result type of the overridden method,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
            the access modifier of the new method provides at least as much
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
            access as the overwritten one.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
      \item for all methods hiding a method (of a superclass) the hidden 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
            method must be static and offer at least as much access rights.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
            Remark: In contrast to the Java Language Specification we don't
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
            restrict the result types of the method
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
            (as in case of overriding), because there seems to be no reason,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
            since there is no dynamic binding of static methods.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
            (cf. 8.4.6.3 vs. 15.12.1).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
            Stricly speaking the restrictions on the access rights aren't 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
            necessary to, since the static type and the access rights 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
            together determine which method is to be called statically. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
            But if a class gains more then one static method with the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
            same signature due to inheritance, it is confusing when the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
            method selection depends on the access rights only: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
            e.g.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
              Class C declares static public method foo().
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
              Class D is subclass of C and declares static method foo()
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
              with default package access.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
              D.foo() ? if this call is in the same package as D then
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
                        foo of class D is called, otherwise foo of class C.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
      \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
(* to Table *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
constdefs entails:: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
                                 ("_ entails _" 20)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
lemma entailsD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
 "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
by (simp add: entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
lemma empty_entails[simp]: "empty entails P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
by (simp add: entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
 wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
"wf_cdecl G \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
   \<lambda>(C,c).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
      \<not>is_iface G C \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
      (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   343
        (\<forall>s. \<forall> im \<in> imethds G I s.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   344
      	    (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
      	                             \<not> is_static cm \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
                                     accmodi im \<le> accmodi cm))) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   347
      (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   348
      (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   349
      jumpNestingOkS {} (init c) \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   350
      (\<exists> A. \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A) \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   351
      \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
      (C \<noteq> Object \<longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
            (is_acc_class G (pid C) (super c) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
             entails (\<lambda> new. \<forall> old sig. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
                       (G,sig\<turnstile>new overrides\<^sub>S old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
                        \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   358
                             accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
      	                     \<not>is_static old)) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
                       (G,sig\<turnstile>new hides old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   361
                         \<longrightarrow> (accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
      	                      is_static old)))) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   363
            ))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   364
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   365
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
 wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
"wf_cdecl G \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
   \<lambda>(C,c).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
      \<not>is_iface G C \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
      (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   372
        (\<forall>s. \<forall> im \<in> imethds G I s.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   373
      	    (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy (mthd cm)\<preceq>resTy (mthd im) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
      	                             \<not> is_static cm \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
                                     accmodi im \<le> accmodi cm))) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   376
      (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
      (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   378
      \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
      (C \<noteq> Object \<longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
            (is_acc_class G (pid C) (super c) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
              hiding methd G (super c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
              under (\<lambda> new old. G\<turnstile>new overrides old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
              entails (\<lambda> new old. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
                           (G\<turnstile>resTy (mthd new)\<preceq>resTy (mthd old) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   386
                            accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
      	                   \<not> is_static old)))  \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
              hiding methd G (super c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
              under (\<lambda> new old. G\<turnstile>new hides old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
              entails (\<lambda> new old. is_static old \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
                                  accmodi old \<le> accmodi new))  \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
            (table_of (cfields c) hiding accfield G C (super c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
              entails (\<lambda> newF oldF. accmodi oldF \<le> access newF))))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   396
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   397
lemma wf_cdeclE [consumes 1]: 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   398
 "\<lbrakk>wf_cdecl G (C,c);
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   399
   \<lbrakk>\<not>is_iface G C;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   400
    (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   401
        (\<forall>s. \<forall> im \<in> imethds G I s.
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   402
      	    (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   403
      	                             \<not> is_static cm \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   404
                                     accmodi im \<le> accmodi cm))); 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   405
      \<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f; unique (cfields c); 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   406
      \<forall>m\<in>set (methods c). wf_mdecl G C m; unique (methods c);
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   407
      jumpNestingOkS {} (init c);
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   408
      \<exists> A. \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A;
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   409
      \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>; 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   410
      ws_cdecl G C (super c); 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   411
      (C \<noteq> Object \<longrightarrow> 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   412
            (is_acc_class G (pid C) (super c) \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   413
            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   414
             entails (\<lambda> new. \<forall> old sig. 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   415
                       (G,sig\<turnstile>new overrides\<^sub>S old 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   416
                        \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   417
                             accmodi old \<le> accmodi new \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   418
      	                     \<not>is_static old)) \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   419
                       (G,sig\<turnstile>new hides old 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   420
                         \<longrightarrow> (accmodi old \<le> accmodi new \<and>
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   421
      	                      is_static old)))) 
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   422
            ))\<rbrakk> \<Longrightarrow> P
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   423
  \<rbrakk> \<Longrightarrow> P"
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   424
by (unfold wf_cdecl_def) simp
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   425
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
lemma wf_cdecl_unique: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
"wf_cdecl G (C,c) \<Longrightarrow> unique (cfields c) \<and> unique (methods c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
lemma wf_cdecl_fdecl: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   433
"\<lbrakk>wf_cdecl G (C,c); f\<in>set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
lemma wf_cdecl_mdecl: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   439
"\<lbrakk>wf_cdecl G (C,c); m\<in>set (methods c)\<rbrakk> \<Longrightarrow> wf_mdecl G C m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
lemma wf_cdecl_impD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
"\<lbrakk>wf_cdecl G (C,c); I\<in>set (superIfs c)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
\<Longrightarrow> is_acc_iface G (pid C) I \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
    (\<forall>s. \<forall>im \<in> imethds G I s.  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   448
        (\<exists>cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> \<not>is_static cm \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
                                   accmodi im \<le> accmodi cm))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
lemma wf_cdecl_supD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
  is_acc_class G (pid C) (super c) \<and> (super c,C) \<notin> (subcls1 G)^+ \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
   (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
    entails (\<lambda> new. \<forall> old sig. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
                 (G,sig\<turnstile>new overrides\<^sub>S old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
                  \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
                       accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
                       \<not>is_static old)) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
                 (G,sig\<turnstile>new hides old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
                   \<longrightarrow> (accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
                        is_static old))))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
apply (unfold wf_cdecl_def ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
lemma wf_cdecl_overrides_SomeD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
  G,sig\<turnstile>(C,newM) overrides\<^sub>S old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
\<rbrakk> \<Longrightarrow>  G\<turnstile>resTy newM\<preceq>resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
       accmodi old \<le> accmodi newM \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
       \<not> is_static old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
apply (drule (1) wf_cdecl_supD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
apply (clarify)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
apply (drule entailsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
apply   (blast intro: table_of_map_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
apply (drule_tac x="old" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
apply (auto dest: overrides_eq_sigD simp add: msig_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
lemma wf_cdecl_hides_SomeD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
  G,sig\<turnstile>(C,newM) hides old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
\<rbrakk> \<Longrightarrow>  accmodi old \<le> access newM \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
       is_static old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
apply (drule (1) wf_cdecl_supD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
apply (clarify)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
apply (drule entailsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
apply   (blast intro: table_of_map_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
apply (drule_tac x="old" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
apply (auto dest: hides_eq_sigD simp add: msig_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
lemma wf_cdecl_wt_init: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   499
 "wf_cdecl G (C, c) \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>init c\<Colon>\<surd>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
section "well-formed programs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
  (* well-formed program, cf. 8.1, 9.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
A program declaration is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   511
\item the class ObjectC of Object is defined
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   512
\item every method of has an access modifier distinct from Package. This is
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   513
      necessary since every interface automatically inherits from Object.  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   514
      We must know, that every time a Object method is "overriden" by an 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   515
      interface method this is also overriden by the class implementing the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   516
      the interface (see @{text "implement_dynmethd and class_mheadsD"})
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   517
\item all standard Exceptions are defined
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   518
\item all defined interfaces are wellformed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   519
\item all defined classes are wellformed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   520
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   521
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   522
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   523
  wf_prog  :: "prog \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   524
 "wf_prog G \<equiv> let is = ifaces G; cs = classes G in
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   525
	         ObjectC \<in> set cs \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   526
                (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   527
                (\<forall>xn. SXcptC xn \<in> set cs) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   528
		(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   529
		(\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   530
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   531
lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   532
apply (unfold wf_prog_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   533
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   534
apply (fast dest: map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   535
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   536
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   537
lemma wf_prog_cdecl: "\<lbrakk>class G C = Some c; wf_prog G\<rbrakk> \<Longrightarrow> wf_cdecl G (C,c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   538
apply (unfold wf_prog_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   539
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   540
apply (fast dest: map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   541
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   542
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   543
lemma wf_prog_Object_mdecls:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   544
"wf_prog G \<Longrightarrow> (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   545
apply (unfold wf_prog_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   546
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   547
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   548
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   549
lemma wf_prog_acc_superD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   550
 "\<lbrakk>wf_prog G; class G C = Some c; C \<noteq> Object \<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   551
  \<Longrightarrow> is_acc_class G (pid C) (super c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   552
by (auto dest: wf_prog_cdecl wf_cdecl_supD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   553
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   554
lemma wf_ws_prog [elim!,simp]: "wf_prog G \<Longrightarrow> ws_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   555
apply (unfold wf_prog_def Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   556
apply (rule ws_progI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   557
apply  (simp_all (no_asm))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   558
apply  (auto simp add: is_acc_class_def is_acc_iface_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   559
             dest!: wf_idecl_supD wf_cdecl_supD )+
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   560
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   561
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   562
lemma class_Object [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   563
"wf_prog G \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   564
  class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   565
                                  init=Skip,super=arbitrary,superIfs=[]\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   566
apply (unfold wf_prog_def Let_def ObjectC_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   567
apply (fast dest!: map_of_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   568
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   569
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   570
lemma methd_Object[simp]: "wf_prog G \<Longrightarrow> methd G Object =  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   571
  table_of (map (\<lambda>(s,m). (s, Object, m)) Object_mdecls)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   572
apply (subst methd_rec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   573
apply (auto simp add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   574
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   575
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   576
lemma wf_prog_Object_methd:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   577
"\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> accmodi m \<noteq> Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   578
by (auto dest!: wf_prog_Object_mdecls) (auto dest!: map_of_SomeD) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   579
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   580
lemma wf_prog_Object_is_public[intro]:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   581
 "wf_prog G \<Longrightarrow> is_public G Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   582
by (auto simp add: is_public_def dest: class_Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   583
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   584
lemma class_SXcpt [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   585
"wf_prog G \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   586
  class G (SXcpt xn) = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   587
                                   init=Skip,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   588
                                   super=if xn = Throwable then Object 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   589
                                                           else SXcpt Throwable,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   590
                                   superIfs=[]\<rparr>"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   591
apply (unfold wf_prog_def Let_def SXcptC_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   592
apply (fast dest!: map_of_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   593
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   594
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   595
lemma wf_ObjectC [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   596
	"wf_cdecl G ObjectC = (\<not>is_iface G Object \<and> Ball (set Object_mdecls)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   597
  (wf_mdecl G Object) \<and> unique Object_mdecls)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   598
apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def)
13688
a0b16d42d489 "Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents: 13601
diff changeset
   599
apply (auto intro: da.Skip)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   600
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   601
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   602
lemma Object_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   603
apply (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   604
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   605
 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   606
lemma Object_is_acc_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_acc_class G S Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   607
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   608
                               accessible_in_RefT_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   609
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   610
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   611
lemma SXcpt_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G (SXcpt xn)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   612
apply (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   613
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   614
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   615
lemma SXcpt_is_acc_class [simp,elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   616
"wf_prog G \<Longrightarrow> is_acc_class G S (SXcpt xn)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   617
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   618
                               accessible_in_RefT_simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   619
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   620
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   621
lemma fields_Object [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G Object = []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   622
by (force intro: fields_emptyI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   623
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   624
lemma accfield_Object [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   625
 "wf_prog G \<Longrightarrow> accfield G S Object = empty"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   626
apply (unfold accfield_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   627
apply (simp (no_asm_simp) add: Let_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   628
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   629
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   630
lemma fields_Throwable [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   631
 "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt Throwable) = []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   632
by (force intro: fields_emptyI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   633
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   634
lemma fields_SXcpt [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt xn) = []"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   635
apply (case_tac "xn = Throwable")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   636
apply  (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   637
by (force intro: fields_emptyI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   638
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   639
lemmas widen_trans = ws_widen_trans [OF _ _ wf_ws_prog, elim]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   640
lemma widen_trans2 [elim]: "\<lbrakk>G\<turnstile>U\<preceq>T; G\<turnstile>S\<preceq>U; wf_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   641
apply (erule (2) widen_trans)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   642
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   643
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   644
lemma Xcpt_subcls_Throwable [simp]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   645
"wf_prog G \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   646
apply (rule SXcpt_subcls_Throwable_lemma)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   647
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   648
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   649
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   650
lemma unique_fields: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   651
 "\<lbrakk>is_class G C; wf_prog G\<rbrakk> \<Longrightarrow> unique (DeclConcepts.fields G C)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   652
apply (erule ws_unique_fields)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   653
apply  (erule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   654
apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   655
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   656
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   657
lemma fields_mono: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   658
"\<lbrakk>table_of (DeclConcepts.fields G C) fn = Some f; G\<turnstile>D\<preceq>\<^sub>C C; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   659
  is_class G D; wf_prog G\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   660
   \<Longrightarrow> table_of (DeclConcepts.fields G D) fn = Some f"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   661
apply (rule map_of_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   662
apply  (erule (1) unique_fields)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   663
apply (erule (1) map_of_SomeD [THEN fields_mono_lemma])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   664
apply (erule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   665
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   666
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   667
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   668
lemma fields_is_type [elim]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   669
"\<lbrakk>table_of (DeclConcepts.fields G C) m = Some f; wf_prog G; is_class G C\<rbrakk> \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   670
      is_type G (type f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   671
apply (frule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   672
apply (force dest: fields_declC [THEN conjunct1] 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   673
                   wf_prog_cdecl [THEN wf_cdecl_fdecl]
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   674
             simp add: wf_fdecl_def2 is_acc_type_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   675
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   676
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   677
lemma imethds_wf_mhead [rule_format (no_asm)]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   678
"\<lbrakk>m \<in> imethds G I sig; wf_prog G; is_iface G I\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   679
  wf_mhead G (pid (decliface m)) sig (mthd m) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   680
  \<not> is_static m \<and> accmodi m = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   681
apply (frule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   682
apply (drule (2) imethds_declI [THEN conjunct1])
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   683
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   684
apply (frule_tac I="(decliface m)" in wf_prog_idecl,assumption)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   685
apply (drule wf_idecl_mhead)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   686
apply (erule map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   687
apply (cases m, simp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   688
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   689
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   690
lemma methd_wf_mdecl: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   691
 "\<lbrakk>methd G C sig = Some m; wf_prog G; class G C = Some y\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   692
  G\<turnstile>C\<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   693
  wf_mdecl G (declclass m) (sig,(mthd m))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   694
apply (frule wf_ws_prog)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   695
apply (drule (1) methd_declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   696
apply  fast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   697
apply clarsimp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   698
apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   699
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   700
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   701
(*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   702
This lemma doesn't hold!
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   703
lemma methd_rT_is_acc_type: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   704
"\<lbrakk>wf_prog G;methd G C C sig = Some (D,m);
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   705
    class G C = Some y\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   706
\<Longrightarrow> is_acc_type G (pid C) (resTy m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   707
The result Type is only visible in the scope of defining class D 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   708
"is_vis_type G (pid D) (resTy m)" but not necessarily in scope of class C!
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   709
(The same is true for the type of pramaters of a method)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   710
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   711
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   712
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   713
lemma methd_rT_is_type: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   714
"\<lbrakk>wf_prog G;methd G C sig = Some m;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   715
    class G C = Some y\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   716
\<Longrightarrow> is_type G (resTy m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   717
apply (drule (2) methd_wf_mdecl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   718
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   719
apply (drule wf_mdeclD1)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   720
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   721
apply (drule rT_is_acc_type)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   722
apply (cases m, simp add: is_acc_type_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   723
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   724
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   725
lemma accmethd_rT_is_type:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   726
"\<lbrakk>wf_prog G;accmethd G S C sig = Some m;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   727
    class G C = Some y\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   728
\<Longrightarrow> is_type G (resTy m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   729
by (auto simp add: accmethd_def  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   730
         intro: methd_rT_is_type)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   731
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   732
lemma methd_Object_SomeD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   733
"\<lbrakk>wf_prog G;methd G Object sig = Some m\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   734
 \<Longrightarrow> declclass m = Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   735
by (auto dest: class_Object simp add: methd_rec )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   736
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   737
lemma wf_imethdsD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
 "\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   739
 \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   741
  assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
  have "wf_prog G \<longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   743
         (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
                  \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
  proof (rule iface_rec.induct,intro allI impI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   746
    fix G I i im
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   747
    assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
                 \<longrightarrow> ?P G J"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   749
    assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   750
           im: "im \<in> imethds G I sig" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
    show "\<not>is_static im \<and> accmodi im = Public" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
    proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   753
      let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
      let ?new = "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
      from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   756
	by (simp add: imethds_rec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
      from wf if_I have 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   758
	wf_supI: "\<forall> J. J \<in> set (isuperIfs i) \<longrightarrow> (\<exists> j. iface G J = Some j)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   759
	by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
      from wf if_I have
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   761
	"\<forall> im \<in> set (imethods i). \<not> is_static im \<and> accmodi im = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
	by (auto dest!: wf_prog_idecl wf_idecl_mhead)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   763
      then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   764
                         \<longrightarrow>  \<not> is_static im \<and> accmodi im = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
	by (auto dest!: table_of_Some_in_set)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   767
	proof (cases "?new sig = {}")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
	  case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   769
	  from True wf wf_supI if_I imethds hyp 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   770
	  show ?thesis by (auto simp del:  split_paired_All)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   771
	next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   772
	  case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   773
	  from False wf wf_supI if_I imethds new_ok hyp 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   774
	  show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   775
	qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   776
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   777
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   778
  with asm show ?thesis by (auto simp del: split_paired_All)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
lemma wf_prog_hidesD:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   782
  assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   783
  shows
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   784
   "accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   785
    is_static old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   786
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
  from hides 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
  obtain c where 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   789
    clsNew: "class G (declclass new) = Some c" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   790
    neqObj: "declclass new \<noteq> Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
    by (auto dest: hidesD declared_in_classD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
  with hides obtain newM oldM where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
    newM: "table_of (methods c) (msig new) = Some newM" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
     new: "new = (declclass new,(msig new),newM)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   795
     old: "old = (declclass old,(msig old),oldM)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   796
          "msig new = msig old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
    by (cases new,cases old) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
       (auto dest: hidesD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
         simp add: cdeclaredmethd_def declared_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
  with hides 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   801
  have hides':
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
        "G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
    by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
  from clsNew wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   805
  have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   806
  note wf_cdecl_hides_SomeD [OF this neqObj newM hides']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   807
  with new old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   808
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   809
    by (cases new, cases old) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   810
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   811
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   812
text {* Compare this lemma about static  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
overriding @{term "G \<turnstile>new overrides\<^sub>S old"} with the definition of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   814
dynamic overriding @{term "G \<turnstile>new overrides old"}. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   815
Conforming result types and restrictions on the access modifiers of the old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   816
and the new method are not part of the predicate for static overriding. But
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   817
they are enshured in a wellfromed program.  Dynamic overriding has 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   818
no restrictions on the access modifiers but enforces confrom result types 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   819
as precondition. But with some efford we can guarantee the access modifier
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   820
restriction for dynamic overriding, too. See lemma 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   821
@{text wf_prog_dyn_override_prop}.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   822
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   823
lemma wf_prog_stat_overridesD:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   824
  assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   825
  shows
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   826
   "G\<turnstile>resTy new\<preceq>resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   827
    accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
    \<not> is_static old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   829
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   830
  from stat_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   831
  obtain c where 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   832
    clsNew: "class G (declclass new) = Some c" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   833
    neqObj: "declclass new \<noteq> Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   834
    by (auto dest: stat_overrides_commonD declared_in_classD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   835
  with stat_override obtain newM oldM where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   836
    newM: "table_of (methods c) (msig new) = Some newM" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   837
     new: "new = (declclass new,(msig new),newM)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   838
     old: "old = (declclass old,(msig old),oldM)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   839
          "msig new = msig old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   840
    by (cases new,cases old) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   841
       (auto dest: stat_overrides_commonD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   842
         simp add: cdeclaredmethd_def declared_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   843
  with stat_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   844
  have stat_override':
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   845
        "G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   846
    by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   847
  from clsNew wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   848
  have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   849
  note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   850
  with new old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   851
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   852
    by (cases new, cases old) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   853
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   854
    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   855
lemma static_to_dynamic_overriding: 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   856
  assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   857
  shows "G\<turnstile>new overrides old"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   858
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   859
  from stat_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   860
  show ?thesis (is "?Overrides new old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   861
  proof (induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   862
    case (Direct new old superNew)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   863
    then have stat_override:"G\<turnstile>new overrides\<^sub>S old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   864
      by (rule stat_overridesR.Direct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   865
    from stat_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   866
    have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   867
      not_static_old: "\<not> is_static old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   868
      by (auto dest: wf_prog_stat_overridesD)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   869
    have not_private_new: "accmodi new \<noteq> Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   870
    proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   871
      from stat_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   872
      have "accmodi old \<noteq> Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   873
	by (rule no_Private_stat_override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   874
      moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   875
      from stat_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   876
      have "accmodi old \<le> accmodi new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   877
	by (auto dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   878
      ultimately
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   879
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   880
	by (auto dest: acc_modi_bottom)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   881
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   882
    with Direct resTy_widen not_static_old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   883
    show "?Overrides new old" 
12962
a24ffe84a06a Cleaning up the definition of static overriding.
schirmer
parents: 12937
diff changeset
   884
      by (auto intro: overridesR.Direct stat_override_declclasses_relation) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   885
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   886
    case (Indirect inter new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   887
    then show "?Overrides new old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   888
      by (blast intro: overridesR.Indirect) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   889
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   890
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   891
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   892
lemma non_Package_instance_method_inheritance:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   893
  assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   894
              accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   895
          instance_method: "\<not> is_static old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   896
                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   897
             old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   898
                       wf: "wf_prog G"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   899
  shows "G\<turnstile>Method old member_of C \<or>
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   900
   (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   901
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   902
  from wf have ws: "ws_prog G" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   903
  from old_declared have iscls_declC_old: "is_class G (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   904
    by (auto simp add: declared_in_def cdeclaredmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   905
  from subcls have  iscls_C: "is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   906
    by (blast dest:  subcls_is_class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   907
  from iscls_C ws old_inheritable subcls 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   908
  show ?thesis (is "?P C old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   909
  proof (induct rule: ws_class_induct')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   910
    case Object
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   911
    assume "G\<turnstile>Object\<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   912
    then show "?P Object old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   913
      by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   914
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   915
    case (Subcls C c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   916
    assume cls_C: "class G C = Some c" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   917
       neq_C_Obj: "C \<noteq> Object" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   918
             hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   919
                   G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   920
     inheritable: "G \<turnstile>Method old inheritable_in pid C" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   921
         subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   922
    from cls_C neq_C_Obj  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   923
    have super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   924
      by (rule subcls1I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   925
    from wf cls_C neq_C_Obj
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   926
    have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   927
      by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   928
    {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   929
      fix old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   930
      assume    member_super: "G\<turnstile>Method old member_of (super c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   931
      assume     inheritable: "G \<turnstile>Method old inheritable_in pid C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   932
      assume instance_method: "\<not> is_static old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   933
      from member_super
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   934
      have old_declared: "G\<turnstile>Method old declared_in (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   935
       by (cases old) (auto dest: member_of_declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   936
      have "?P C old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   937
      proof (cases "G\<turnstile>mid (msig old) undeclared_in C")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   938
	case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   939
	with inheritable super accessible_super member_super
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   940
	have "G\<turnstile>Method old member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   941
	  by (cases old) (auto intro: members.Inherited)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   942
	then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   943
	  by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   944
      next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   945
	case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   946
	then obtain new_member where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   947
	     "G\<turnstile>new_member declared_in C" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   948
             "mid (msig old) = memberid new_member"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   949
          by (auto dest: not_undeclared_declared)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   950
	then obtain new where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   951
	          new: "G\<turnstile>Method new declared_in C" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   952
               eq_sig: "msig old = msig new" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   953
	    declC_new: "declclass new = C" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   954
	  by (cases new_member) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   955
	then have member_new: "G\<turnstile>Method new member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   956
	  by (cases new) (auto intro: members.Immediate)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   957
	from declC_new super member_super
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   958
	have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   959
	  by (auto dest!: member_of_subclseq_declC
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   960
	            dest: r_into_trancl intro: trancl_rtrancl_trancl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   961
	show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   962
	proof (cases "is_static new")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   963
	  case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   964
	  with eq_sig declC_new new old_declared inheritable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   965
	       super member_super subcls_new_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   966
	  have "G\<turnstile>new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   967
	    by (auto intro!: stat_overridesR.Direct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   968
	  with member_new show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   969
	    by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   970
	next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   971
	  case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   972
	  with eq_sig declC_new subcls_new_old new old_declared inheritable
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   973
	  have "G\<turnstile>new hides old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   974
	    by (auto intro: hidesI)    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   975
	  with wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   976
	  have "is_static old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   977
	    by (blast dest: wf_prog_hidesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   978
	  with instance_method
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   979
	  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   980
	    by (contradiction)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   981
	qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   982
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   983
    } note hyp_member_super = this
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   984
    from subclsC cls_C 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   985
    have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
      by (rule subcls_superD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   987
    then
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   988
    show "?P C old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   989
    proof (cases rule: subclseq_cases) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   990
      case Eq
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   991
      assume "super c = declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   992
      with old_declared 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   993
      have "G\<turnstile>Method old member_of (super c)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   994
	by (cases old) (auto intro: members.Immediate)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   995
      with inheritable instance_method 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   996
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   997
	by (blast dest: hyp_member_super)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   998
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   999
      case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1000
      assume "G\<turnstile>super c\<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1001
      moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1002
      from inheritable accmodi_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1003
      have "G \<turnstile>Method old inheritable_in pid (super c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1004
	by (cases "accmodi old") (auto simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1005
      ultimately
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1006
      have "?P (super c) old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1007
	by (blast dest: hyp)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1008
      then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1009
      proof
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1010
	assume "G \<turnstile>Method old member_of super c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1011
	with inheritable instance_method
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1012
	show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1013
	  by (blast dest: hyp_member_super)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1014
      next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1015
	assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1016
	then obtain super_new where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1017
	  super_new_override:  "G \<turnstile> super_new overrides\<^sub>S old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1018
            super_new_member:  "G \<turnstile>Method super_new member_of super c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1019
	  by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1020
	from super_new_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1021
	have "accmodi old \<le> accmodi super_new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1022
	  by (auto dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1023
	with inheritable accmodi_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1024
	have "G \<turnstile>Method super_new inheritable_in pid C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1025
	  by (auto simp add: inheritable_in_def 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1026
	              split: acc_modi.splits
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1027
                       dest: acc_modi_le_Dests)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1028
	moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1029
	from super_new_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1030
	have "\<not> is_static super_new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1031
	  by (auto dest: stat_overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1032
	moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1033
	note super_new_member
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1034
	ultimately have "?P C super_new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1035
	  by (auto dest: hyp_member_super)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1036
	then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1037
	proof 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1038
	  assume "G \<turnstile>Method super_new member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1039
	  with super_new_override
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1040
	  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1041
	    by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1042
	next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1043
	  assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1044
                  G \<turnstile>Method new member_of C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1045
	  with super_new_override show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1046
	    by (blast intro: stat_overridesR.Indirect) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1047
	qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1048
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1049
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1050
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1051
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1052
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1053
lemma non_Package_instance_method_inheritance_cases [consumes 6,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1054
         case_names Inheritance Overriding]:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1055
  assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1056
              accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1057
          instance_method: "\<not> is_static old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1058
                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1059
             old_declared: "G\<turnstile>Method old declared_in (declclass old)" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1060
                       wf: "wf_prog G" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1061
              inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1062
               overriding: "\<And> new.
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1063
                           \<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1064
                           \<Longrightarrow> P"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1065
  shows P
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1066
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1067
  from old_inheritable accmodi_old instance_method subcls old_declared wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1068
       inheritance overriding
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1069
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1070
    by (auto dest: non_Package_instance_method_inheritance)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1071
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1072
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1073
lemma dynamic_to_static_overriding:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1074
  assumes dyn_override: "G\<turnstile> new overrides old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1075
           accmodi_old: "accmodi old \<noteq> Package" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1076
                    wf: "wf_prog G"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1077
  shows "G\<turnstile> new overrides\<^sub>S old"  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1078
proof - 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1079
  from dyn_override accmodi_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1080
  show ?thesis (is "?Overrides new old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1081
  proof (induct rule: overridesR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1082
    case (Direct new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1083
    assume   new_declared: "G\<turnstile>Method new declared_in declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1084
    assume eq_sig_new_old: "msig new = msig old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1085
    assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1086
    assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1087
           "accmodi old \<noteq> Package" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1088
           "\<not> is_static old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1089
           "G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1090
           "G\<turnstile>Method old declared_in declclass old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1091
    from this wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1092
    show "?Overrides new old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1093
    proof (cases rule: non_Package_instance_method_inheritance_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1094
      case Inheritance
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1095
      assume "G \<turnstile>Method old member_of declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1096
      then have "G\<turnstile>mid (msig old) undeclared_in declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1097
      proof cases
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1098
	case Immediate 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1099
	with subcls_new_old wf show ?thesis 	
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1100
	  by (auto dest: subcls_irrefl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1101
      next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1102
	case Inherited
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1103
	then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1104
	  by (cases old) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1105
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1106
      with eq_sig_new_old new_declared
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1107
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1108
	by (cases old,cases new) (auto dest!: declared_not_undeclared)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1109
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1110
      case (Overriding new') 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1111
      assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1112
      then have "msig new' = msig old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1113
	by (auto dest: stat_overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1114
      with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1115
	by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1116
      assume "G \<turnstile>Method new' member_of declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1117
      then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1118
      proof (cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1119
	case Immediate
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1120
	then have declC_new: "declclass new' = declclass new" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1121
	  by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1122
	from Immediate 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1123
	have "G\<turnstile>Method new' declared_in declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1124
	  by (cases new') auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1125
	with new_declared eq_sig_new_new' declC_new 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1126
	have "new=new'"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1127
	  by (cases new, cases new') (auto dest: unique_declared_in) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1128
	with stat_override_new'
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1129
	show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1130
	  by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1131
      next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1132
	case Inherited
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1133
	then have "G\<turnstile>mid (msig new') undeclared_in declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1134
	  by (cases new') (auto)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1135
	with eq_sig_new_new' new_declared
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1136
	show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1137
	  by (cases new,cases new') (auto dest!: declared_not_undeclared)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1138
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1139
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1140
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1141
    case (Indirect inter new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1142
    assume accmodi_old: "accmodi old \<noteq> Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1143
    assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1144
    with accmodi_old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1145
    have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1146
      by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1147
    moreover 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1148
    assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1149
    moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1150
    have "accmodi inter \<noteq> Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1151
    proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1152
      from stat_override_inter_old wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1153
      have "accmodi old \<le> accmodi inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1154
	by (auto dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1155
      with stat_override_inter_old accmodi_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1156
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1157
	by (auto dest!: no_Private_stat_override
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1158
                 split: acc_modi.splits 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1159
	         dest: acc_modi_le_Dests)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1160
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1161
    ultimately show "?Overrides new old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1162
      by (blast intro: stat_overridesR.Indirect)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1163
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1164
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1165
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1166
lemma wf_prog_dyn_override_prop:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1167
  assumes dyn_override: "G \<turnstile> new overrides old" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1168
                    wf: "wf_prog G"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1169
  shows "accmodi old \<le> accmodi new"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1170
proof (cases "accmodi old = Package")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1171
  case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1172
  note old_Package = this
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1173
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1174
  proof (cases "accmodi old \<le> accmodi new")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1175
    case True then show ?thesis .
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1176
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1177
    case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1178
    with old_Package 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1179
    have "accmodi new = Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1180
      by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1181
    with dyn_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1182
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1183
      by (auto dest: overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1184
  qed    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1185
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1186
  case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1187
  with dyn_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1188
  have "G \<turnstile> new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1189
    by (blast intro: dynamic_to_static_overriding)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1190
  with wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1191
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1192
   by (blast dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1193
qed 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1194
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1195
lemma overrides_Package_old: 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1196
  assumes dyn_override: "G \<turnstile> new overrides old" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1197
           accmodi_new: "accmodi new = Package" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1198
                    wf: "wf_prog G "
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1199
  shows "accmodi old = Package"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1200
proof (cases "accmodi old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1201
  case Private
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1202
  with dyn_override show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1203
    by (simp add: no_Private_override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1204
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1205
  case Package
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1206
  then show ?thesis .
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1207
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1208
  case Protected
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1209
  with dyn_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1210
  have "G \<turnstile> new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1211
    by (auto intro: dynamic_to_static_overriding)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1212
  with wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1213
  have "accmodi old \<le> accmodi new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1214
    by (auto dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1215
  with Protected accmodi_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1216
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1217
    by (simp add: less_acc_def le_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1218
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1219
  case Public
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1220
  with dyn_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1221
  have "G \<turnstile> new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1222
    by (auto intro: dynamic_to_static_overriding)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1223
  with wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1224
  have "accmodi old \<le> accmodi new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1225
    by (auto dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1226
  with Public accmodi_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1227
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1228
    by (simp add: less_acc_def le_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1229
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1230
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1231
lemma dyn_override_Package:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1232
  assumes dyn_override: "G \<turnstile> new overrides old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1233
           accmodi_old: "accmodi old = Package" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1234
           accmodi_new: "accmodi new = Package" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1235
                    wf: "wf_prog G"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1236
  shows "pid (declclass old) = pid (declclass new)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1237
proof - 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1238
  from dyn_override accmodi_old accmodi_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1239
  show ?thesis (is "?EqPid old new")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1240
  proof (induct rule: overridesR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1241
    case (Direct new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1242
    assume "accmodi old = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1243
           "G \<turnstile>Method old inheritable_in pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1244
    then show "pid (declclass old) =  pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1245
      by (auto simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1246
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1247
    case (Indirect inter new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1248
    assume accmodi_old: "accmodi old = Package" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1249
           accmodi_new: "accmodi new = Package" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1250
    assume "G \<turnstile> new overrides inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1251
    with accmodi_new wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1252
    have "accmodi inter = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1253
      by  (auto intro: overrides_Package_old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1254
    with Indirect
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1255
    show "pid (declclass old) =  pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1256
      by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1257
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1258
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1259
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1260
lemma dyn_override_Package_escape:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1261
  assumes dyn_override: "G \<turnstile> new overrides old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1262
           accmodi_old: "accmodi old = Package" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1263
          outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1264
                    wf: "wf_prog G"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1265
  shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1266
             pid (declclass old) = pid (declclass inter) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1267
             Protected \<le> accmodi inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1268
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1269
  from dyn_override accmodi_old outside_pack
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1270
  show ?thesis (is "?P new old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1271
  proof (induct rule: overridesR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1272
    case (Direct new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1273
    assume accmodi_old: "accmodi old = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1274
    assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1275
    assume "G \<turnstile>Method old inheritable_in pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1276
    with accmodi_old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1277
    have "pid (declclass old) = pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1278
      by (simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1279
    with outside_pack 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1280
    show "?P new old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1281
      by (contradiction)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1282
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1283
    case (Indirect inter new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1284
    assume accmodi_old: "accmodi old = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1285
    assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1286
    assume override_new_inter: "G \<turnstile> new overrides inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1287
    assume override_inter_old: "G \<turnstile> inter overrides old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1288
    assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1289
                           pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1290
                           \<Longrightarrow> ?P new inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1291
    assume hyp_inter_old: "\<lbrakk>accmodi old = Package; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1292
                           pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1293
                           \<Longrightarrow> ?P inter old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1294
    show "?P new old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1295
    proof (cases "pid (declclass old) = pid (declclass inter)")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1296
      case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1297
      note same_pack_old_inter = this
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1298
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1299
      proof (cases "pid (declclass inter) = pid (declclass new)")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1300
	case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1301
	with same_pack_old_inter outside_pack
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1302
	show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1303
	  by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1304
      next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1305
	case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1306
	note diff_pack_inter_new = this
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1307
	show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1308
	proof (cases "accmodi inter = Package")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1309
	  case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1310
	  with diff_pack_inter_new hyp_new_inter  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1311
	  obtain newinter where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1312
	    over_new_newinter: "G \<turnstile> new overrides newinter" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1313
            over_newinter_inter: "G \<turnstile> newinter overrides inter" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1314
            eq_pid: "pid (declclass inter) = pid (declclass newinter)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1315
            accmodi_newinter: "Protected \<le> accmodi newinter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1316
	    by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1317
	  from over_newinter_inter override_inter_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1318
	  have "G\<turnstile>newinter overrides old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1319
	    by (rule overridesR.Indirect)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1320
	  moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1321
	  from eq_pid same_pack_old_inter 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1322
	  have "pid (declclass old) = pid (declclass newinter)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1323
	    by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1324
	  moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1325
	  note over_new_newinter accmodi_newinter
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1326
	  ultimately show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1327
	    by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1328
	next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1329
	  case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1330
	  with override_new_inter
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1331
	  have "Protected \<le> accmodi inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1332
	    by (cases "accmodi inter") (auto dest: no_Private_override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1333
	  with override_new_inter override_inter_old same_pack_old_inter
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1334
	  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1335
	    by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1336
	qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1337
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1338
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1339
      case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1340
      with accmodi_old hyp_inter_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1341
      obtain newinter where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1342
	over_inter_newinter: "G \<turnstile> inter overrides newinter" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1343
          over_newinter_old: "G \<turnstile> newinter overrides old" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1344
                eq_pid: "pid (declclass old) = pid (declclass newinter)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1345
	accmodi_newinter: "Protected \<le> accmodi newinter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1346
	by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1347
      from override_new_inter over_inter_newinter 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1348
      have "G \<turnstile> new overrides newinter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1349
	by (rule overridesR.Indirect)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1350
      with eq_pid over_newinter_old accmodi_newinter
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1351
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1352
	by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1353
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1354
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1355
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1356
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1357
lemma declclass_widen[rule_format]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1358
 "wf_prog G 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1359
 \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1360
 \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1361
proof (rule class_rec.induct,intro allI impI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1362
  fix G C c m
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1363
  assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1364
               \<longrightarrow> ?P G (super c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1365
  assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1366
         m:  "methd G C sig = Some m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1367
  show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1368
  proof (cases "C=Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1369
    case True 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1370
    with wf m show ?thesis by (simp add: methd_Object_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1371
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1372
    let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1373
    let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1374
    case False 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1375
    with cls_C wf m
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1376
    have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1377
      by (simp add: methd_rec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1378
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1379
    proof (cases "?table sig")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1380
      case None
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1381
      from this methd_C have "?filter (methd G (super c)) sig = Some m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1382
	by simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1383
      moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1384
      from wf cls_C False obtain sup where "class G (super c) = Some sup"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1385
	by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class)
12925
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
  1386
      moreover note wf False cls_C  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
  1387
      ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m"  
99131847fb93 Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents: 12893
diff changeset
  1388
	by (auto intro: Hyp [rule_format])
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1389
      moreover from cls_C False have  "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" by (rule subcls1I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1390
      ultimately show ?thesis by - (rule rtrancl_into_rtrancl2)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1391
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1392
      case Some
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1393
      from this wf False cls_C methd_C show ?thesis by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1394
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1395
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1396
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1397
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1398
lemma declclass_methd_Object: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1399
 "\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> declclass m = Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1400
by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1401
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1402
lemma methd_declaredD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1403
 "\<lbrakk>wf_prog G; is_class G C;methd G C sig = Some m\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1404
  \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1405
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1406
  assume    wf: "wf_prog G"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1407
  then have ws: "ws_prog G" ..
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1408
  assume  clsC: "is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1409
  from clsC ws 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1410
  show "methd G C sig = Some m 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1411
        \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1412
    (is "PROP ?P C") 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1413
  proof (induct ?P C rule: ws_class_induct')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1414
    case Object
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1415
    assume "methd G Object sig = Some m" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1416
    with wf show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1417
      by - (rule method_declared_inI, auto) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1418
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1419
    case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1420
    fix C c
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1421
    assume clsC: "class G C = Some c"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1422
    and       m: "methd G C sig = Some m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1423
    and     hyp: "methd G (super c) sig = Some m \<Longrightarrow> ?thesis" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1424
    let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1425
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1426
    proof (cases "?newMethods sig")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1427
      case None
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1428
      from None ws clsC m hyp 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1429
      show ?thesis by (auto intro: method_declared_inI simp add: methd_rec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1430
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1431
      case Some
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1432
      from Some ws clsC m 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1433
      show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1434
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1435
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1436
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1437
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1438
lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1439
  assumes methd_C: "methd G C sig = Some m" and