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