src/HOL/Bali/WellForm.thy
author wenzelm
Sat, 17 Oct 2009 14:43:18 +0200
changeset 32960 69916a850301
parent 30235 58d147683393
child 34915 7894c7dab132
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
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
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     4
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Well-formedness of Java programs *}
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14981
diff changeset
     7
theory WellForm imports DefiniteAssignment begin
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
For static checks on expressions and statements, see WellType.thy
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
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
    13
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
\item a method implementing or overwriting another method may have a result 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
      type that widens to the result type of the other method 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
      (instead of identical type)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
\item if a method hides another method (both methods have to be static!)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
  there are no restrictions to the result type 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
  since the methods have to be static and there is no dynamic binding of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
  static methods
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
\item if an interface inherits more than one method with the same signature, the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
  methods need not have identical return types
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
simplifications:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
\item Object and standard exceptions are assumed to be declared like normal 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
      classes
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
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
    32
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
    33
        cf. 8.3 and (9.3) *}
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
  wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
 "wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
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
    40
apply (unfold wf_fdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
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
section "well-formed method declarations"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
  (*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
    48
  (* 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
    49
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
A method head is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    52
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    53
\item the signature and the method head agree in the number of parameters
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    54
\item all types of the parameters are visible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    55
\item the result type is visible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    56
\item the parameter names are unique
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    57
\end{itemize} 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    58
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    59
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    60
  wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    61
 "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
    62
                            \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    63
                            is_acc_type G P (resTy mh) \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
    64
                            \<spacespace> distinct (pars mh)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    65
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    66
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    67
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    68
A method declaration is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    69
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    70
\item the method head is wellformed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    71
\item the names of the local variables are unique
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    72
\item the types of the local variables must be accessible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    73
\item the local variables don't shadow the parameters
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    74
\item the class of the method is defined
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    75
\item the body statement is welltyped with respect to the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    76
      modified environment of local names, were the local variables, 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    77
      the parameters the special result variable (Res) and This are assoziated
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    78
      with there types. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    79
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    80
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    81
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
    82
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
    83
"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
    84
 \<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
    85
            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
    86
            \<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
    87
                  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
    88
                  \<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
    89
                | Res \<Rightarrow> Some (resTy m))
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
    90
          | This \<Rightarrow> if is_static m then None else Some (Class 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
    91
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
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
    93
"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
    94
                  \<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
    95
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    96
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    97
  wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    98
 "wf_mdecl G C \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    99
      \<lambda>(sig,m).
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   100
          wf_mhead G (pid C) sig (mhead m) \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   101
          unique (lcls (mbody m)) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   102
          (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   103
          (\<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
   104
          jumpNestingOkS {Ret} (stmt (mbody m)) \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   105
          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
   106
          \<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
   107
          (\<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
   108
                \<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
   109
               \<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
   110
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
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
   112
"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
   113
  = (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
   114
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
   115
 
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
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
   117
"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
   118
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
   119
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
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
   121
"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
   122
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
   123
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
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
   125
"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
   126
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
   127
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
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
   129
"\<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
   130
by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   131
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   132
lemma wf_mheadI: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   133
"\<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
   134
  is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow>  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   135
  wf_mhead G P sig m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   136
apply (unfold wf_mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   137
apply (simp (no_asm_simp))
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   138
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   139
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   140
lemma wf_mdeclI: "\<lbrakk>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   141
  wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m));  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   142
  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   143
  \<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
   144
  jumpNestingOkS {Ret} (stmt (mbody m));
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   145
  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
   146
  \<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
   147
  (\<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
   148
        \<and> Result \<in> nrm A)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   149
  \<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   150
  wf_mdecl G C (sig,m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   151
apply (unfold wf_mdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   152
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   153
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   154
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
   155
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
   156
  "\<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
   157
    \<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
   158
     \<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
   159
     \<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
   160
     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
   161
     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
   162
     \<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
   163
   (\<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
   164
        \<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
   165
    \<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
   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
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
   168
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   169
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   170
lemma wf_mdeclD1: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   171
"wf_mdecl G C (sig,m) \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   172
   wf_mhead G (pid C) sig (mhead m) \<and> unique (lcls (mbody m)) \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   173
  (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   174
  (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   175
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
   176
apply simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   177
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   178
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   179
lemma wf_mdecl_bodyD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   180
"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
   181
 (\<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
   182
      G\<turnstile>T\<preceq>(resTy m))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   183
apply (unfold wf_mdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   184
apply clarify
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   185
apply (rule_tac x="(resTy m)" in exI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   186
apply (unfold wf_mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   187
apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body )
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   188
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   189
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
lemma static_Object_methodsE [elim!]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   193
 "\<lbrakk>wf_mdecl G Object (sig, m);static m\<rbrakk> \<Longrightarrow> R"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   194
apply (unfold wf_mdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   195
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   196
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   197
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   198
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   199
lemma rT_is_acc_type: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   200
  "wf_mhead G P sig m \<Longrightarrow> is_acc_type G P (resTy m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   201
apply (unfold wf_mhead_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   202
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   203
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   204
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   205
section "well-formed interface declarations"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   206
  (* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   207
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   208
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   209
A interface declaration is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   210
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   211
\item the interface hierarchy is wellstructured
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   212
\item there is no class with the same name
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   213
\item the method heads are wellformed and not static and have Public access
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   214
\item the methods are uniquely named
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   215
\item all superinterfaces are accessible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   216
\item the result type of a method overriding a method of Object widens to the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   217
      result type of the overridden method.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   218
      Shadowing static methods is forbidden.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   219
\item the result type of a method overriding a set of methods defined in the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   220
      superinterfaces widens to each of the corresponding result types
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   221
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   222
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   223
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   224
  wf_idecl :: "prog  \<Rightarrow> idecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   225
 "wf_idecl G \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   226
    \<lambda>(I,i). 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   227
        ws_idecl G I (isuperIfs i) \<and> 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   228
        \<not>is_class G I \<and>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   229
        (\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   230
                                     \<not>is_static mh \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   231
                                      accmodi mh = Public) \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   232
        unique (imethods i) \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   233
        (\<forall> J\<in>set (isuperIfs i). is_acc_iface G (pid I) J) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   234
        (table_of (imethods i)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   235
          hiding (methd G Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   236
          under  (\<lambda> new old. accmodi old \<noteq> Private)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   237
          entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   238
                             is_static new = is_static old)) \<and> 
30235
58d147683393 Made Option a separate theory and renamed option_map to Option.map
nipkow
parents: 28524
diff changeset
   239
        (Option.set \<circ> table_of (imethods i) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   240
               hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i))
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   241
               entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   242
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   243
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
   244
  wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   245
apply (unfold wf_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   246
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   247
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   248
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   249
lemma wf_idecl_hidings: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   250
"wf_idecl G (I, i) \<Longrightarrow> 
30235
58d147683393 Made Option a separate theory and renamed option_map to Option.map
nipkow
parents: 28524
diff changeset
   251
  (\<lambda>s. Option.set (table_of (imethods i) s)) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   252
  hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i))  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   253
  entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   254
apply (unfold wf_idecl_def o_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   255
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   256
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   257
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   258
lemma wf_idecl_hiding:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   259
"wf_idecl G (I, i) \<Longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   260
 (table_of (imethods i)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   261
           hiding (methd G Object)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   262
           under  (\<lambda> new old. accmodi old \<noteq> Private)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   263
           entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   264
                              is_static new = is_static old))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   265
apply (unfold wf_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   266
apply simp
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   267
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   268
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   269
lemma wf_idecl_supD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   270
"\<lbrakk>wf_idecl G (I,i); J \<in> set (isuperIfs i)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   271
 \<Longrightarrow> is_acc_iface G (pid I) J \<and> (J, I) \<notin> (subint1 G)^+"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   272
apply (unfold wf_idecl_def ws_idecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   273
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   274
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   275
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   276
section "well-formed class declarations"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   277
  (* 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
   278
   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
   279
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   280
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   281
A class declaration is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   282
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   283
\item there is no interface with the same name
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   284
\item all superinterfaces are accessible and for all methods implementing 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   285
      an interface method the result type widens to the result type of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   286
      the interface method, the method is not static and offers at least 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   287
      as much access 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   288
      (this actually means that the method has Public access, since all 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   289
      interface methods have public access)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   290
\item all field declarations are wellformed and the field names are unique
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   291
\item all method declarations are wellformed and the method names are unique
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   292
\item the initialization statement is welltyped
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   293
\item the classhierarchy is wellstructured
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   294
\item Unless the class is Object:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   295
      \begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   296
      \item the superclass is accessible
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   297
      \item for all methods overriding another method (of a superclass )the
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   298
            result type widens to the result type of the overridden method,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   299
            the access modifier of the new method provides at least as much
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   300
            access as the overwritten one.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   301
      \item for all methods hiding a method (of a superclass) the hidden 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   302
            method must be static and offer at least as much access rights.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   303
            Remark: In contrast to the Java Language Specification we don't
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   304
            restrict the result types of the method
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   305
            (as in case of overriding), because there seems to be no reason,
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   306
            since there is no dynamic binding of static methods.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   307
            (cf. 8.4.6.3 vs. 15.12.1).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   308
            Stricly speaking the restrictions on the access rights aren't 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   309
            necessary to, since the static type and the access rights 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   310
            together determine which method is to be called statically. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   311
            But if a class gains more then one static method with the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   312
            same signature due to inheritance, it is confusing when the 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   313
            method selection depends on the access rights only: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   314
            e.g.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   315
              Class C declares static public method foo().
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   316
              Class D is subclass of C and declares static method foo()
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   317
              with default package access.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   318
              D.foo() ? if this call is in the same package as D then
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   319
                        foo of class D is called, otherwise foo of class C.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   320
      \end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   321
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   322
\end{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   323
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   324
(* to Table *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   325
constdefs entails:: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   326
                                 ("_ entails _" 20)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   327
"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   328
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   329
lemma entailsD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   330
 "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   331
by (simp add: entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   332
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   333
lemma empty_entails[simp]: "empty entails P"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   334
by (simp add: entails_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   335
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   336
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   337
 wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   338
"wf_cdecl G \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   339
   \<lambda>(C,c).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   340
      \<not>is_iface G C \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   341
      (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   342
        (\<forall>s. \<forall> im \<in> imethds G I s.
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   343
            (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   344
                                     \<not> is_static cm \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   345
                                     accmodi im \<le> accmodi cm))) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   346
      (\<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
   347
      (\<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
   348
      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
   349
      (\<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
   350
      \<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
   351
      (C \<noteq> Object \<longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   352
            (is_acc_class G (pid C) (super c) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   353
            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   354
             entails (\<lambda> new. \<forall> old sig. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   355
                       (G,sig\<turnstile>new overrides\<^sub>S old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   356
                        \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   357
                             accmodi old \<le> accmodi new \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   358
                             \<not>is_static old)) \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   359
                       (G,sig\<turnstile>new hides old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   360
                         \<longrightarrow> (accmodi old \<le> accmodi new \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   361
                              is_static old)))) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   362
            ))"
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
constdefs
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   366
 wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   367
"wf_cdecl G \<equiv> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   368
   \<lambda>(C,c).
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   369
      \<not>is_iface G C \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   370
      (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   371
        (\<forall>s. \<forall> im \<in> imethds G I s.
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   372
            (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy (mthd cm)\<preceq>resTy (mthd im) \<and>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   373
                                     \<not> is_static cm \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   374
                                     accmodi im \<le> accmodi cm))) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   375
      (\<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
   376
      (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   377
      \<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
   378
      (C \<noteq> Object \<longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   379
            (is_acc_class G (pid C) (super c) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   380
            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   381
              hiding methd G (super c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   382
              under (\<lambda> new old. G\<turnstile>new overrides old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   383
              entails (\<lambda> new old. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   384
                           (G\<turnstile>resTy (mthd new)\<preceq>resTy (mthd old) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   385
                            accmodi old \<le> accmodi new \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   386
                           \<not> is_static old)))  \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   387
            (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   388
              hiding methd G (super c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   389
              under (\<lambda> new old. G\<turnstile>new hides old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   390
              entails (\<lambda> new old. is_static old \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   391
                                  accmodi old \<le> accmodi new))  \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   392
            (table_of (cfields c) hiding accfield G C (super c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   393
              entails (\<lambda> newF oldF. accmodi oldF \<le> access newF))))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   394
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   395
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
   396
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
   397
 "\<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
   398
   \<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
   399
    (\<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
   400
        (\<forall>s. \<forall> im \<in> imethds G I s.
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   401
            (\<exists> cm \<in> methd  G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   402
                                     \<not> is_static cm \<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
   403
                                     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
   404
      \<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
   405
      \<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
   406
      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
   407
      \<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
   408
      \<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
   409
      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
   410
      (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
   411
            (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
   412
            (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
   413
             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
   414
                       (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
   415
                        \<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
   416
                             accmodi old \<le> accmodi new \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   417
                             \<not>is_static old)) \<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
   418
                       (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
   419
                         \<longrightarrow> (accmodi old \<le> accmodi new \<and>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   420
                              is_static old)))) 
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
   421
            ))\<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
   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
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
   424
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   425
lemma wf_cdecl_unique: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   426
"wf_cdecl G (C,c) \<Longrightarrow> unique (cfields c) \<and> unique (methods c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   427
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   428
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   429
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   430
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   431
lemma wf_cdecl_fdecl: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   432
"\<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
   433
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   434
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   435
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   436
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   437
lemma wf_cdecl_mdecl: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   438
"\<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
   439
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   440
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   441
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   442
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   443
lemma wf_cdecl_impD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   444
"\<lbrakk>wf_cdecl G (C,c); I\<in>set (superIfs c)\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   445
\<Longrightarrow> is_acc_iface G (pid C) I \<and>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   446
    (\<forall>s. \<forall>im \<in> imethds G I s.  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   447
        (\<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
   448
                                   accmodi im \<le> accmodi cm))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   449
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   450
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   451
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   452
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   453
lemma wf_cdecl_supD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   454
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object\<rbrakk> \<Longrightarrow>  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   455
  is_acc_class G (pid C) (super c) \<and> (super c,C) \<notin> (subcls1 G)^+ \<and> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   456
   (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   457
    entails (\<lambda> new. \<forall> old sig. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   458
                 (G,sig\<turnstile>new overrides\<^sub>S old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   459
                  \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   460
                       accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   461
                       \<not>is_static old)) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   462
                 (G,sig\<turnstile>new hides old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   463
                   \<longrightarrow> (accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   464
                        is_static old))))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   465
apply (unfold wf_cdecl_def ws_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   466
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   467
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   468
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   469
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   470
lemma wf_cdecl_overrides_SomeD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   471
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   472
  G,sig\<turnstile>(C,newM) overrides\<^sub>S old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   473
\<rbrakk> \<Longrightarrow>  G\<turnstile>resTy newM\<preceq>resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   474
       accmodi old \<le> accmodi newM \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   475
       \<not> is_static old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   476
apply (drule (1) wf_cdecl_supD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   477
apply (clarify)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   478
apply (drule entailsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   479
apply   (blast intro: table_of_map_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   480
apply (drule_tac x="old" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   481
apply (auto dest: overrides_eq_sigD simp add: msig_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   482
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   483
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   484
lemma wf_cdecl_hides_SomeD:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   485
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM;
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   486
  G,sig\<turnstile>(C,newM) hides old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   487
\<rbrakk> \<Longrightarrow>  accmodi old \<le> access newM \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   488
       is_static old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   489
apply (drule (1) wf_cdecl_supD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   490
apply (clarify)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   491
apply (drule entailsD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   492
apply   (blast intro: table_of_map_SomeI)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   493
apply (drule_tac x="old" in spec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   494
apply (auto dest: hides_eq_sigD simp add: msig_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   495
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   496
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   497
lemma wf_cdecl_wt_init: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   498
 "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
   499
apply (unfold wf_cdecl_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   500
apply auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   501
done
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   502
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   503
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   504
section "well-formed programs"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   505
  (* well-formed program, cf. 8.1, 9.1 *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   506
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   507
text {*
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   508
A program declaration is wellformed if:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   509
\begin{itemize}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   510
\item the class ObjectC of Object is defined
14030
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 14025
diff changeset
   511
\item every method of Object has an access modifier distinct from Package. 
cd928c0ac225 Adapted to changes in Map.thy
schirmer
parents: 14025
diff changeset
   512
      This is
12854
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
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   525
                 ObjectC \<in> set cs \<and> 
12854
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>
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   528
                (\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and>
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   529
                (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs"
12854
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,
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 24019
diff changeset
   565
                                  init=Skip,super=undefined,superIfs=[]\<rparr>"
12854
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]: 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   596
        "wf_cdecl G ObjectC = (\<not>is_iface G Object \<and> Ball (set Object_mdecls)
12854
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))"
30235
58d147683393 Made Option a separate theory and renamed option_map to Option.map
nipkow
parents: 28524
diff changeset
   754
      let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
      from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   756
        by (simp add: imethds_rec)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   757
      from wf if_I have 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   758
        wf_supI: "\<forall> J. J \<in> set (isuperIfs i) \<longrightarrow> (\<exists> j. iface G J = Some j)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   759
        by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   760
      from wf if_I have
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   761
        "\<forall> im \<in> set (imethods i). \<not> is_static im \<and> accmodi im = Public"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   762
        by (auto dest!: wf_prog_idecl wf_idecl_mhead)
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   765
        by (auto dest!: table_of_Some_in_set)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   767
        proof (cases "?new sig = {}")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   768
          case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   769
          from True wf wf_supI if_I imethds hyp 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   770
          show ?thesis by (auto simp del:  split_paired_All)  
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   771
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   772
          case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   773
          from False wf wf_supI if_I imethds new_ok hyp 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   774
          show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   775
        qed
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   873
        by (rule no_Private_stat_override)
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   877
        by (auto dest: wf_prog_stat_overridesD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   878
      ultimately
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   879
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   880
        by (auto dest: acc_modi_bottom)
12854
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
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   886
    case (Indirect new inter old)
12854
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")
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   938
        case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   939
        with inheritable super accessible_super member_super
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   940
        have "G\<turnstile>Method old member_of C"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   941
          by (cases old) (auto intro: members.Inherited)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   942
        then show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   943
          by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   944
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   945
        case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   946
        then obtain new_member where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   947
             "G\<turnstile>new_member declared_in C" and
12854
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)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   950
        then obtain new where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   951
                  new: "G\<turnstile>Method new declared_in C" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   952
               eq_sig: "msig old = msig new" and
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   953
            declC_new: "declclass new = C" 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   954
          by (cases new_member) auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   955
        then have member_new: "G\<turnstile>Method new member_of C"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   956
          by (cases new) (auto intro: members.Immediate)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   957
        from declC_new super member_super
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   958
        have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   959
          by (auto dest!: member_of_subclseq_declC
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   960
                    dest: r_into_trancl intro: trancl_rtrancl_trancl)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   961
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   962
        proof (cases "is_static new")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   963
          case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   964
          with eq_sig declC_new new old_declared inheritable
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   965
               super member_super subcls_new_old
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   966
          have "G\<turnstile>new overrides\<^sub>S old"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   967
            by (auto intro!: stat_overridesR.Direct)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   968
          with member_new show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   969
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   970
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   971
          case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   972
          with eq_sig declC_new subcls_new_old new old_declared inheritable
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   973
          have "G\<turnstile>new hides old"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   974
            by (auto intro: hidesI)    
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   975
          with wf 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   976
          have "is_static old"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   977
            by (blast dest: wf_prog_hidesD)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   978
          with instance_method
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   979
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   980
            by (contradiction)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   981
        qed
12854
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)" 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   994
        by (cases old) (auto intro: members.Immediate)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   995
      with inheritable instance_method 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   996
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   997
        by (blast dest: hyp_member_super)
12854
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)"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1004
        by (cases "accmodi old") (auto simp add: inheritable_in_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1005
      ultimately
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1006
      have "?P (super c) old"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1007
        by (blast dest: hyp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1008
      then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1009
      proof
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1010
        assume "G \<turnstile>Method old member_of super c"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1011
        with inheritable instance_method
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1012
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1013
          by (blast dest: hyp_member_super)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1014
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1015
        assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1016
        then obtain super_new where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1017
          super_new_override:  "G \<turnstile> super_new overrides\<^sub>S old" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1018
            super_new_member:  "G \<turnstile>Method super_new member_of super c"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1019
          by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1020
        from super_new_override wf
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1021
        have "accmodi old \<le> accmodi super_new"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1022
          by (auto dest: wf_prog_stat_overridesD)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1023
        with inheritable accmodi_old
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1024
        have "G \<turnstile>Method super_new inheritable_in pid C"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1025
          by (auto simp add: inheritable_in_def 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1026
                      split: acc_modi.splits
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1027
                       dest: acc_modi_le_Dests)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1028
        moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1029
        from super_new_override 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1030
        have "\<not> is_static super_new"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1031
          by (auto dest: stat_overrides_commonD)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1032
        moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1033
        note super_new_member
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1034
        ultimately have "?P C super_new"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1035
          by (auto dest: hyp_member_super)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1036
        then show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1037
        proof 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1038
          assume "G \<turnstile>Method super_new member_of C"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1039
          with super_new_override
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1040
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1041
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1042
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1043
          assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1044
                  G \<turnstile>Method new member_of C"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1045
          with super_new_override show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1046
            by (blast intro: stat_overridesR.Indirect) 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1047
        qed
12854
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
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1098
        case Immediate 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1099
        with subcls_new_old wf show ?thesis     
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1100
          by (auto dest: subcls_irrefl)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1101
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1102
        case Inherited
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1103
        then show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1104
          by (cases old) auto
12854
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
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1108
        by (cases old,cases new) (auto dest!: declared_not_undeclared)
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1113
        by (auto dest: stat_overrides_commonD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1114
      with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1115
        by simp
12854
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)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1119
        case Immediate
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1120
        then have declC_new: "declclass new' = declclass new" 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1121
          by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1122
        from Immediate 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1123
        have "G\<turnstile>Method new' declared_in declclass new"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1124
          by (cases new') auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1125
        with new_declared eq_sig_new_new' declC_new 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1126
        have "new=new'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1127
          by (cases new, cases new') (auto dest: unique_declared_in) 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1128
        with stat_override_new'
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1129
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1130
          by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1131
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1132
        case Inherited
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1133
        then have "G\<turnstile>mid (msig new') undeclared_in declclass new"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1134
          by (cases new') (auto)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1135
        with eq_sig_new_new' new_declared
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1136
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1137
          by (cases new,cases new') (auto dest!: declared_not_undeclared)
12854
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
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
  1141
    case (Indirect new inter old)
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1154
        by (auto dest: wf_prog_stat_overridesD)
12854
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
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1157
        by (auto dest!: no_Private_stat_override
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1158
                 split: acc_modi.splits 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1159
                 dest: acc_modi_le_Dests)
12854
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
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
  1247
    case (Indirect new inter old)
12854
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
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
  1283
    case (Indirect new inter old)
12854
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)")
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1300
        case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1301
        with same_pack_old_inter outside_pack
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1302
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1303
          by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1304
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1305
        case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1306
        note diff_pack_inter_new = this
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1307
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1308
        proof (cases "accmodi inter = Package")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1309
          case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1310
          with diff_pack_inter_new hyp_new_inter  
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1311
          obtain newinter where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1312
            over_new_newinter: "G \<turnstile> new overrides newinter" and
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1316
            by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1317
          from over_newinter_inter override_inter_old
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1318
          have "G\<turnstile>newinter overrides old"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1319
            by (rule overridesR.Indirect)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1320
          moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1321
          from eq_pid same_pack_old_inter 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1322
          have "pid (declclass old) = pid (declclass newinter)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1323
            by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1324
          moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1325
          note over_new_newinter accmodi_newinter
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1326
          ultimately show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1327
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1328
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1329
          case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1330
          with override_new_inter
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1331
          have "Protected \<le> accmodi inter"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1332
            by (cases "accmodi inter") (auto dest: no_Private_override)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1333
          with override_new_inter override_inter_old same_pack_old_inter
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1334
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1335
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1336
        qed
12854
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
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1342
        over_inter_newinter: "G \<turnstile> inter overrides newinter" and
12854
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
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1345
        accmodi_newinter: "Protected \<le> accmodi newinter"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1346
        by auto
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1349
        by (rule overridesR.Indirect)
12854
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
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1352
        by blast
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1382
        by simp
12854
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"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
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