src/HOL/Bali/WellForm.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47176 568fdc70e565
child 51703 f2e92fc0c8aa
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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>
46212
d86ef6b96097 tuned white space;
wenzelm
parents: 45608
diff changeset
    61
                            ( \<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>
46212
d86ef6b96097 tuned white space;
wenzelm
parents: 45608
diff changeset
    63
                            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
45608
13b101cee425 eliminated obsolete "standard";
wenzelm
parents: 45605
diff changeset
   736
lemmas iface_rec_induct' = iface_rec.induct [of "%x y z. P x y"] for P
13b101cee425 eliminated obsolete "standard";
wenzelm
parents: 45605
diff changeset
   737
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   738
lemma wf_imethdsD: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   739
 "\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   740
 \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   741
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   742
  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
   743
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   744
  have "wf_prog G \<longrightarrow> 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   745
         (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   746
                  \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   747
  proof (induct G I rule: iface_rec_induct', intro allI impI)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   748
    fix G I i im
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
   749
    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
   750
                 \<Longrightarrow> ?P G J"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   751
    assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   752
           im: "im \<in> imethds G I sig" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   753
    show "\<not>is_static im \<and> accmodi im = Public" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   754
    proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   755
      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
   756
      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
   757
      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
   758
        by (simp add: imethds_rec)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   759
      from wf if_I have 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   760
        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
   761
        by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   762
      from wf if_I have
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   763
        "\<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
   764
        by (auto dest!: wf_prog_idecl wf_idecl_mhead)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   765
      then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   766
                         \<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
   767
        by (auto dest!: table_of_Some_in_set)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   768
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   769
        proof (cases "?new sig = {}")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   770
          case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   771
          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
   772
          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
   773
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   774
          case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   775
          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
   776
          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
   777
        qed
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   778
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   779
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   780
  with asm show ?thesis by (auto simp del: split_paired_All)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   781
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   782
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   783
lemma wf_prog_hidesD:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   784
  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
   785
  shows
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   786
   "accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   787
    is_static old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   788
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   789
  from hides 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   790
  obtain c where 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   791
    clsNew: "class G (declclass new) = Some c" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   792
    neqObj: "declclass new \<noteq> Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   793
    by (auto dest: hidesD declared_in_classD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   794
  with hides obtain newM oldM where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   795
    newM: "table_of (methods c) (msig new) = Some newM" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   796
     new: "new = (declclass new,(msig new),newM)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   797
     old: "old = (declclass old,(msig old),oldM)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   798
          "msig new = msig old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   799
    by (cases new,cases old) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   800
       (auto dest: hidesD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   801
         simp add: cdeclaredmethd_def declared_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   802
  with hides 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   803
  have hides':
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   804
        "G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   805
    by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   806
  from clsNew wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   807
  have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   808
  note wf_cdecl_hides_SomeD [OF this neqObj newM hides']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   809
  with new old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   810
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   811
    by (cases new, cases old) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   812
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   813
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   814
text {* Compare this lemma about static  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   815
overriding @{term "G \<turnstile>new overrides\<^sub>S old"} with the definition of 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   816
dynamic overriding @{term "G \<turnstile>new overrides old"}. 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   817
Conforming result types and restrictions on the access modifiers of the old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   818
and the new method are not part of the predicate for static overriding. But
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   819
they are enshured in a wellfromed program.  Dynamic overriding has 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   820
no restrictions on the access modifiers but enforces confrom result types 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   821
as precondition. But with some efford we can guarantee the access modifier
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   822
restriction for dynamic overriding, too. See lemma 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   823
@{text wf_prog_dyn_override_prop}.
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   824
*}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   825
lemma wf_prog_stat_overridesD:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   826
  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
   827
  shows
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   828
   "G\<turnstile>resTy new\<preceq>resTy old \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   829
    accmodi old \<le> accmodi new \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   830
    \<not> is_static old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   831
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   832
  from stat_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   833
  obtain c where 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   834
    clsNew: "class G (declclass new) = Some c" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   835
    neqObj: "declclass new \<noteq> Object"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   836
    by (auto dest: stat_overrides_commonD declared_in_classD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   837
  with stat_override obtain newM oldM where
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   838
    newM: "table_of (methods c) (msig new) = Some newM" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   839
     new: "new = (declclass new,(msig new),newM)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   840
     old: "old = (declclass old,(msig old),oldM)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   841
          "msig new = msig old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   842
    by (cases new,cases old) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   843
       (auto dest: stat_overrides_commonD 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   844
         simp add: cdeclaredmethd_def declared_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   845
  with stat_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   846
  have stat_override':
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   847
        "G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   848
    by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   849
  from clsNew wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   850
  have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   851
  note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override']
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   852
  with new old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   853
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   854
    by (cases new, cases old) auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   855
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   856
    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   857
lemma static_to_dynamic_overriding: 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   858
  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
   859
  shows "G\<turnstile>new overrides old"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   860
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   861
  from stat_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   862
  show ?thesis (is "?Overrides new old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   863
  proof (induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   864
    case (Direct new old superNew)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   865
    then have stat_override:"G\<turnstile>new overrides\<^sub>S old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   866
      by (rule stat_overridesR.Direct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   867
    from stat_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   868
    have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   869
      not_static_old: "\<not> is_static old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   870
      by (auto dest: wf_prog_stat_overridesD)  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   871
    have not_private_new: "accmodi new \<noteq> Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   872
    proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   873
      from stat_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   874
      have "accmodi old \<noteq> Private"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   875
        by (rule no_Private_stat_override)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   876
      moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   877
      from stat_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   878
      have "accmodi old \<le> accmodi new"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   879
        by (auto dest: wf_prog_stat_overridesD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   880
      ultimately
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   881
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   882
        by (auto dest: acc_modi_bottom)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   883
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   884
    with Direct resTy_widen not_static_old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   885
    show "?Overrides new old" 
12962
a24ffe84a06a Cleaning up the definition of static overriding.
schirmer
parents: 12937
diff changeset
   886
      by (auto intro: overridesR.Direct stat_override_declclasses_relation) 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   887
  next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
   888
    case (Indirect new inter old)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   889
    then show "?Overrides new old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   890
      by (blast intro: overridesR.Indirect) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   891
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   892
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   893
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   894
lemma non_Package_instance_method_inheritance:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   895
  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
   896
              accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   897
          instance_method: "\<not> is_static old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   898
                   subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   899
             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
   900
                       wf: "wf_prog G"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   901
  shows "G\<turnstile>Method old member_of C \<or>
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
   902
   (\<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
   903
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   904
  from wf have ws: "ws_prog G" by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   905
  from old_declared have iscls_declC_old: "is_class G (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   906
    by (auto simp add: declared_in_def cdeclaredmethd_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   907
  from subcls have  iscls_C: "is_class G C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   908
    by (blast dest:  subcls_is_class)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   909
  from iscls_C ws old_inheritable subcls 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   910
  show ?thesis (is "?P C old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   911
  proof (induct rule: ws_class_induct')
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   912
    case Object
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   913
    assume "G\<turnstile>Object\<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   914
    then show "?P Object old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   915
      by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   916
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   917
    case (Subcls C c)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   918
    assume cls_C: "class G C = Some c" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   919
       neq_C_Obj: "C \<noteq> Object" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   920
             hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   921
                   G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   922
     inheritable: "G \<turnstile>Method old inheritable_in pid C" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   923
         subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   924
    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
   925
    have super: "G\<turnstile>C \<prec>\<^sub>C1 super c" 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   926
      by (rule subcls1I)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   927
    from wf cls_C neq_C_Obj
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   928
    have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   929
      by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   930
    {
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   931
      fix old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   932
      assume    member_super: "G\<turnstile>Method old member_of (super c)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   933
      assume     inheritable: "G \<turnstile>Method old inheritable_in pid C"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   934
      assume instance_method: "\<not> is_static old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   935
      from member_super
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   936
      have old_declared: "G\<turnstile>Method old declared_in (declclass old)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   937
       by (cases old) (auto dest: member_of_declC)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   938
      have "?P C old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   939
      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
   940
        case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   941
        with inheritable super accessible_super member_super
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   942
        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
   943
          by (cases old) (auto intro: members.Inherited)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   944
        then show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   945
          by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   946
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   947
        case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   948
        then obtain new_member where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   949
             "G\<turnstile>new_member declared_in C" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   950
             "mid (msig old) = memberid new_member"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   951
          by (auto dest: not_undeclared_declared)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   952
        then obtain new where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   953
                  new: "G\<turnstile>Method new declared_in C" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   954
               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
   955
            declC_new: "declclass new = C" 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   956
          by (cases new_member) auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   957
        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
   958
          by (cases new) (auto intro: members.Immediate)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   959
        from declC_new super member_super
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   960
        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
   961
          by (auto dest!: member_of_subclseq_declC
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   962
                    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
   963
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   964
        proof (cases "is_static new")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   965
          case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   966
          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
   967
               super member_super subcls_new_old
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   968
          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
   969
            by (auto intro!: stat_overridesR.Direct)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   970
          with member_new show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   971
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   972
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   973
          case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   974
          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
   975
          have "G\<turnstile>new hides old"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   976
            by (auto intro: hidesI)    
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   977
          with wf 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   978
          have "is_static old"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   979
            by (blast dest: wf_prog_hidesD)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   980
          with instance_method
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   981
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   982
            by (contradiction)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   983
        qed
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   984
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   985
    } note hyp_member_super = this
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   986
    from subclsC cls_C 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   987
    have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   988
      by (rule subcls_superD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   989
    then
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   990
    show "?P C old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   991
    proof (cases rule: subclseq_cases) 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   992
      case Eq
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   993
      assume "super c = declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   994
      with old_declared 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   995
      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
   996
        by (cases old) (auto intro: members.Immediate)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   997
      with inheritable instance_method 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
   998
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
   999
        by (blast dest: hyp_member_super)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1000
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1001
      case Subcls
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1002
      assume "G\<turnstile>super c\<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1003
      moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1004
      from inheritable accmodi_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1005
      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
  1006
        by (cases "accmodi old") (auto simp add: inheritable_in_def)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1007
      ultimately
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1008
      have "?P (super c) old"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1009
        by (blast dest: hyp)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1010
      then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1011
      proof
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1012
        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
  1013
        with inheritable instance_method
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1014
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1015
          by (blast dest: hyp_member_super)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1016
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1017
        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
  1018
        then obtain super_new where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1019
          super_new_override:  "G \<turnstile> super_new overrides\<^sub>S old" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1020
            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
  1021
          by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1022
        from super_new_override wf
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1023
        have "accmodi old \<le> accmodi super_new"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1024
          by (auto dest: wf_prog_stat_overridesD)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1025
        with inheritable accmodi_old
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1026
        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
  1027
          by (auto simp add: inheritable_in_def 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1028
                      split: acc_modi.splits
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1029
                       dest: acc_modi_le_Dests)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1030
        moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1031
        from super_new_override 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1032
        have "\<not> is_static super_new"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1033
          by (auto dest: stat_overrides_commonD)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1034
        moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1035
        note super_new_member
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1036
        ultimately have "?P C super_new"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1037
          by (auto dest: hyp_member_super)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1038
        then show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1039
        proof 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1040
          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
  1041
          with super_new_override
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1042
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1043
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1044
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1045
          assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1046
                  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
  1047
          with super_new_override show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1048
            by (blast intro: stat_overridesR.Indirect) 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1049
        qed
12854
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
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1054
47176
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
  1055
lemma non_Package_instance_method_inheritance_cases:
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
47176
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
  1061
                       wf: "wf_prog G"
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
  1062
  obtains (Inheritance) "G\<turnstile>Method old member_of C"
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
  1063
    | (Overriding) new where "G\<turnstile> new overrides\<^sub>S old" and "G\<turnstile>Method new member_of C"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1064
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1065
  from old_inheritable accmodi_old instance_method subcls old_declared wf 
47176
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
  1066
       Inheritance Overriding
568fdc70e565 simplified statements and proofs;
wenzelm
parents: 46212
diff changeset
  1067
  show thesis
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1068
    by (auto dest: non_Package_instance_method_inheritance)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1069
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1070
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1071
lemma dynamic_to_static_overriding:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1072
  assumes dyn_override: "G\<turnstile> new overrides old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1073
           accmodi_old: "accmodi old \<noteq> Package" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1074
                    wf: "wf_prog G"
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1075
  shows "G\<turnstile> new overrides\<^sub>S old"  
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1076
proof - 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1077
  from dyn_override accmodi_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1078
  show ?thesis (is "?Overrides new old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1079
  proof (induct rule: overridesR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1080
    case (Direct new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1081
    assume   new_declared: "G\<turnstile>Method new declared_in declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1082
    assume eq_sig_new_old: "msig new = msig old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1083
    assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1084
    assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1085
           "accmodi old \<noteq> Package" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1086
           "\<not> is_static old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1087
           "G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1088
           "G\<turnstile>Method old declared_in declclass old" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1089
    from this wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1090
    show "?Overrides new old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1091
    proof (cases rule: non_Package_instance_method_inheritance_cases)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1092
      case Inheritance
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1093
      assume "G \<turnstile>Method old member_of declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1094
      then have "G\<turnstile>mid (msig old) undeclared_in declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1095
      proof cases
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1096
        case Immediate 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1097
        with subcls_new_old wf show ?thesis     
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1098
          by (auto dest: subcls_irrefl)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1099
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1100
        case Inherited
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1101
        then show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1102
          by (cases old) auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1103
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1104
      with eq_sig_new_old new_declared
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1105
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1106
        by (cases old,cases new) (auto dest!: declared_not_undeclared)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1107
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1108
      case (Overriding new') 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1109
      assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1110
      then have "msig new' = msig old"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1111
        by (auto dest: stat_overrides_commonD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1112
      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
  1113
        by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1114
      assume "G \<turnstile>Method new' member_of declclass new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1115
      then show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1116
      proof (cases)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1117
        case Immediate
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1118
        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
  1119
          by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1120
        from Immediate 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1121
        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
  1122
          by (cases new') auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1123
        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
  1124
        have "new=new'"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1125
          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
  1126
        with stat_override_new'
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1127
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1128
          by simp
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1129
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1130
        case Inherited
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1131
        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
  1132
          by (cases new') (auto)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1133
        with eq_sig_new_new' new_declared
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1134
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1135
          by (cases new,cases new') (auto dest!: declared_not_undeclared)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1136
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1137
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1138
  next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
  1139
    case (Indirect new inter old)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1140
    assume accmodi_old: "accmodi old \<noteq> Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1141
    assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1142
    with accmodi_old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1143
    have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1144
      by blast
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1145
    moreover 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1146
    assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1147
    moreover
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1148
    have "accmodi inter \<noteq> Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1149
    proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1150
      from stat_override_inter_old wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1151
      have "accmodi old \<le> accmodi inter"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1152
        by (auto dest: wf_prog_stat_overridesD)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1153
      with stat_override_inter_old accmodi_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1154
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1155
        by (auto dest!: no_Private_stat_override
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1156
                 split: acc_modi.splits 
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1157
                 dest: acc_modi_le_Dests)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1158
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1159
    ultimately show "?Overrides new old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1160
      by (blast intro: stat_overridesR.Indirect)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1161
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1162
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1163
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1164
lemma wf_prog_dyn_override_prop:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1165
  assumes dyn_override: "G \<turnstile> new overrides old" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1166
                    wf: "wf_prog G"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1167
  shows "accmodi old \<le> accmodi new"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1168
proof (cases "accmodi old = Package")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1169
  case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1170
  note old_Package = this
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1171
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1172
  proof (cases "accmodi old \<le> accmodi new")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1173
    case True then show ?thesis .
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1174
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1175
    case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1176
    with old_Package 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1177
    have "accmodi new = Private"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1178
      by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1179
    with dyn_override 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1180
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1181
      by (auto dest: overrides_commonD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1182
  qed    
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1183
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1184
  case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1185
  with dyn_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1186
  have "G \<turnstile> new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1187
    by (blast intro: dynamic_to_static_overriding)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1188
  with wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1189
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1190
   by (blast dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1191
qed 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1192
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1193
lemma overrides_Package_old: 
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1194
  assumes dyn_override: "G \<turnstile> new overrides old" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1195
           accmodi_new: "accmodi new = Package" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1196
                    wf: "wf_prog G "
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1197
  shows "accmodi old = Package"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1198
proof (cases "accmodi old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1199
  case Private
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1200
  with dyn_override show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1201
    by (simp add: no_Private_override)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1202
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1203
  case Package
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1204
  then show ?thesis .
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1205
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1206
  case Protected
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1207
  with dyn_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1208
  have "G \<turnstile> new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1209
    by (auto intro: dynamic_to_static_overriding)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1210
  with wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1211
  have "accmodi old \<le> accmodi new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1212
    by (auto dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1213
  with Protected accmodi_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1214
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1215
    by (simp add: less_acc_def le_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1216
next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1217
  case Public
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1218
  with dyn_override wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1219
  have "G \<turnstile> new overrides\<^sub>S old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1220
    by (auto intro: dynamic_to_static_overriding)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1221
  with wf 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1222
  have "accmodi old \<le> accmodi new"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1223
    by (auto dest: wf_prog_stat_overridesD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1224
  with Public accmodi_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1225
  show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1226
    by (simp add: less_acc_def le_acc_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1227
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1228
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1229
lemma dyn_override_Package:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1230
  assumes dyn_override: "G \<turnstile> new overrides old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1231
           accmodi_old: "accmodi old = Package" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1232
           accmodi_new: "accmodi new = Package" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1233
                    wf: "wf_prog G"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1234
  shows "pid (declclass old) = pid (declclass new)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1235
proof - 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1236
  from dyn_override accmodi_old accmodi_new
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1237
  show ?thesis (is "?EqPid old new")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1238
  proof (induct rule: overridesR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1239
    case (Direct new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1240
    assume "accmodi old = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1241
           "G \<turnstile>Method old inheritable_in pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1242
    then show "pid (declclass old) =  pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1243
      by (auto simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1244
  next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
  1245
    case (Indirect new inter old)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1246
    assume accmodi_old: "accmodi old = Package" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1247
           accmodi_new: "accmodi new = Package" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1248
    assume "G \<turnstile> new overrides inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1249
    with accmodi_new wf
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1250
    have "accmodi inter = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1251
      by  (auto intro: overrides_Package_old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1252
    with Indirect
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1253
    show "pid (declclass old) =  pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1254
      by auto
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1255
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1256
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1257
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1258
lemma dyn_override_Package_escape:
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1259
  assumes dyn_override: "G \<turnstile> new overrides old" and
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1260
           accmodi_old: "accmodi old = Package" and 
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1261
          outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1262
                    wf: "wf_prog G"
12937
0c4fd7529467 clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents: 12925
diff changeset
  1263
  shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and>
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1264
             pid (declclass old) = pid (declclass inter) \<and>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1265
             Protected \<le> accmodi inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1266
proof -
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1267
  from dyn_override accmodi_old outside_pack
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1268
  show ?thesis (is "?P new old")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1269
  proof (induct rule: overridesR.induct)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1270
    case (Direct new old)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1271
    assume accmodi_old: "accmodi old = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1272
    assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1273
    assume "G \<turnstile>Method old inheritable_in pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1274
    with accmodi_old 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1275
    have "pid (declclass old) = pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1276
      by (simp add: inheritable_in_def)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1277
    with outside_pack 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1278
    show "?P new old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1279
      by (contradiction)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1280
  next
21765
89275a3ed7be Adapted to new inductive definition package.
berghofe
parents: 17876
diff changeset
  1281
    case (Indirect new inter old)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1282
    assume accmodi_old: "accmodi old = Package"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1283
    assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1284
    assume override_new_inter: "G \<turnstile> new overrides inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1285
    assume override_inter_old: "G \<turnstile> inter overrides old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1286
    assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1287
                           pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1288
                           \<Longrightarrow> ?P new inter"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1289
    assume hyp_inter_old: "\<lbrakk>accmodi old = Package; 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1290
                           pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk>
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1291
                           \<Longrightarrow> ?P inter old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1292
    show "?P new old"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1293
    proof (cases "pid (declclass old) = pid (declclass inter)")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1294
      case True
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1295
      note same_pack_old_inter = this
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1296
      show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1297
      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
  1298
        case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1299
        with same_pack_old_inter outside_pack
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1300
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1301
          by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1302
      next
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1303
        case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1304
        note diff_pack_inter_new = this
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1305
        show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1306
        proof (cases "accmodi inter = Package")
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1307
          case True
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1308
          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
  1309
          obtain newinter where
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1310
            over_new_newinter: "G \<turnstile> new overrides newinter" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1311
            over_newinter_inter: "G \<turnstile> newinter overrides inter" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1312
            eq_pid: "pid (declclass inter) = pid (declclass newinter)" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1313
            accmodi_newinter: "Protected \<le> accmodi newinter"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1314
            by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1315
          from over_newinter_inter override_inter_old
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1316
          have "G\<turnstile>newinter overrides old"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1317
            by (rule overridesR.Indirect)
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1318
          moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1319
          from eq_pid same_pack_old_inter 
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1320
          have "pid (declclass old) = pid (declclass newinter)"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1321
            by simp
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1322
          moreover
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1323
          note over_new_newinter accmodi_newinter
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1324
          ultimately show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1325
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1326
        next
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1327
          case False
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1328
          with override_new_inter
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1329
          have "Protected \<le> accmodi inter"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1330
            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
  1331
          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
  1332
          show ?thesis
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1333
            by blast
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1334
        qed
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1335
      qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1336
    next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1337
      case False
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1338
      with accmodi_old hyp_inter_old
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1339
      obtain newinter where
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1340
        over_inter_newinter: "G \<turnstile> inter overrides newinter" and
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1341
          over_newinter_old: "G \<turnstile> newinter overrides old" and 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1342
                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
  1343
        accmodi_newinter: "Protected \<le> accmodi newinter"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1344
        by auto
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1345
      from override_new_inter over_inter_newinter 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1346
      have "G \<turnstile> new overrides newinter"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1347
        by (rule overridesR.Indirect)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1348
      with eq_pid over_newinter_old accmodi_newinter
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1349
      show ?thesis
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1350
        by blast
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1351
    qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1352
  qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1353
qed
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1354
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 44890
diff changeset
  1355
lemmas class_rec_induct' = class_rec.induct [of "%x y z w. P x y"] for P
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
  1356
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1357
lemma declclass_widen[rule_format]: 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1358
 "wf_prog G 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1359
 \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1360
 \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C")
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
  1361
proof (induct G C rule: class_rec_induct', intro allI impI)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1362
  fix G C c m
35440
bdf8ad377877 killed more recdefs
krauss
parents: 35416
diff changeset
  1363
  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
  1364
               \<Longrightarrow> ?P G (super c)"
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1365
  assume wf: "wf_prog G" and cls_C: "class G C = Some c" and
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1366
         m:  "methd G C sig = Some m"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1367
  show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1368
  proof (cases "C=Object")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1369
    case True 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1370
    with wf m show ?thesis by (simp add: methd_Object_SomeD)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1371
  next
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1372
    let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1373
    let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1374
    case False 
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1375
    with cls_C wf m
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1376
    have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m "
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1377
      by (simp add: methd_rec)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1378
    show ?thesis
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1379
    proof (cases "?table sig")
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1380
      case None
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
  1381
      from this methd_C have "?filter (methd G (super c)) sig = Some m"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 30235
diff changeset
  1382
        by simp