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