author  wenzelm 
Sat, 17 Oct 2009 14:43:18 +0200  
changeset 32960  69916a850301 
parent 30235  58d147683393 
child 34915  7894c7dab132 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/WellForm.thy 
12854  2 
ID: $Id$ 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

3 
Author: David von Oheimb and Norbert Schirmer 
12854  4 
*) 
5 

6 
header {* Wellformedness of Java programs *} 

16417  7 
theory WellForm imports DefiniteAssignment begin 
12854  8 

9 
text {* 

10 
For static checks on expressions and statements, see WellType.thy 

11 

12 
improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1): 

13 
\begin{itemize} 

14 
\item a method implementing or overwriting another method may have a result 

15 
type that widens to the result type of the other method 

16 
(instead of identical type) 

17 
\item if a method hides another method (both methods have to be static!) 

18 
there are no restrictions to the result type 

19 
since the methods have to be static and there is no dynamic binding of 

20 
static methods 

21 
\item if an interface inherits more than one method with the same signature, the 

22 
methods need not have identical return types 

23 
\end{itemize} 

24 
simplifications: 

25 
\begin{itemize} 

26 
\item Object and standard exceptions are assumed to be declared like normal 

27 
classes 

28 
\end{itemize} 

29 
*} 

30 

31 
section "wellformed field declarations" 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

32 
text {* wellformed field declaration (common part for classes and interfaces), 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

33 
cf. 8.3 and (9.3) *} 
12854  34 

35 
constdefs 

36 
wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" 

37 
"wf_fdecl G P \<equiv> \<lambda>(fn,f). is_acc_type G P (type f)" 

38 

39 
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))" 

40 
apply (unfold wf_fdecl_def) 

41 
apply simp 

42 
done 

43 

44 

45 

46 
section "wellformed method declarations" 

47 
(*wellformed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*) 

48 
(* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *) 

49 

50 
text {* 

51 
A method head is wellformed if: 

52 
\begin{itemize} 

53 
\item the signature and the method head agree in the number of parameters 

54 
\item all types of the parameters are visible 

55 
\item the result type is visible 

56 
\item the parameter names are unique 

57 
\end{itemize} 

58 
*} 

59 
constdefs 

60 
wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" 

61 
"wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

62 
\<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
12854  63 
is_acc_type G P (resTy mh) \<and> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

64 
\<spacespace> distinct (pars mh)" 
12854  65 

66 

67 
text {* 

68 
A method declaration is wellformed if: 

69 
\begin{itemize} 

70 
\item the method head is wellformed 

71 
\item the names of the local variables are unique 

72 
\item the types of the local variables must be accessible 

73 
\item the local variables don't shadow the parameters 

74 
\item the class of the method is defined 

75 
\item the body statement is welltyped with respect to the 

76 
modified environment of local names, were the local variables, 

77 
the parameters the special result variable (Res) and This are assoziated 

78 
with there types. 

79 
\end{itemize} 

80 
*} 

81 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

82 
constdefs callee_lcl:: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

83 
"callee_lcl C sig m 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

84 
\<equiv> \<lambda> k. (case k of 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

85 
EName e 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

86 
\<Rightarrow> (case e of 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

87 
VNam v 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

88 
\<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

89 
 Res \<Rightarrow> Some (resTy m)) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

90 
 This \<Rightarrow> if is_static m then None else Some (Class C))" 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

91 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

92 
constdefs parameters :: "methd \<Rightarrow> lname set" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

93 
"parameters m \<equiv> set (map (EName \<circ> VNam) (pars m)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

94 
\<union> (if (static m) then {} else {This})" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

95 

12854  96 
constdefs 
97 
wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" 

98 
"wf_mdecl G C \<equiv> 

99 
\<lambda>(sig,m). 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

100 
wf_mhead G (pid C) sig (mhead m) \<and> 
12854  101 
unique (lcls (mbody m)) \<and> 
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 tabwidth;
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  105 
is_class G C \<and> 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

106 
\<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

107 
(\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

108 
\<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

109 
\<and> Result \<in> nrm A)" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

110 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

111 
lemma callee_lcl_VNam_simp [simp]: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

112 
"callee_lcl C sig m (EName (VNam v)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

113 
= (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

114 
by (simp add: callee_lcl_def) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

115 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

116 
lemma callee_lcl_Res_simp [simp]: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

117 
"callee_lcl C sig m (EName Res) = Some (resTy m)" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

118 
by (simp add: callee_lcl_def) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

119 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

120 
lemma callee_lcl_This_simp [simp]: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

121 
"callee_lcl C sig m (This) = (if is_static m then None else Some (Class C))" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

122 
by (simp add: callee_lcl_def) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

123 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

124 
lemma callee_lcl_This_static_simp: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

125 
"is_static m \<Longrightarrow> callee_lcl C sig m (This) = None" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

126 
by simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

127 

a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

128 
lemma callee_lcl_This_not_static_simp: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

129 
"\<not> is_static m \<Longrightarrow> callee_lcl C sig m (This) = Some (Class C)" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

130 
by simp 
12854  131 

132 
lemma wf_mheadI: 

133 
"\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T; 

12893  134 
is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow> 
12854  135 
wf_mhead G P sig m" 
136 
apply (unfold wf_mhead_def) 

137 
apply (simp (no_asm_simp)) 

138 
done 

139 

140 
lemma wf_mdeclI: "\<lbrakk> 

141 
wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m)); 

142 
(\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None); 

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  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  149 
\<rbrakk> \<Longrightarrow> 
150 
wf_mdecl G C (sig,m)" 

151 
apply (unfold wf_mdecl_def) 

152 
apply simp 

153 
done 

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  169 

170 
lemma wf_mdeclD1: 

171 
"wf_mdecl G C (sig,m) \<Longrightarrow> 

172 
wf_mhead G (pid C) sig (mhead m) \<and> unique (lcls (mbody m)) \<and> 

173 
(\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 

174 
(\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T)" 

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  177 
done 
178 

179 
lemma wf_mdecl_bodyD: 

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  183 
apply (unfold wf_mdecl_def) 
184 
apply clarify 

185 
apply (rule_tac x="(resTy m)" in exI) 

186 
apply (unfold wf_mhead_def) 

187 
apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body ) 

188 
done 

189 

190 

191 
(* 

192 
lemma static_Object_methodsE [elim!]: 

193 
"\<lbrakk>wf_mdecl G Object (sig, m);static m\<rbrakk> \<Longrightarrow> R" 

194 
apply (unfold wf_mdecl_def) 

195 
apply auto 

196 
done 

197 
*) 

198 

199 
lemma rT_is_acc_type: 

200 
"wf_mhead G P sig m \<Longrightarrow> is_acc_type G P (resTy m)" 

201 
apply (unfold wf_mhead_def) 

202 
apply auto 

203 
done 

204 

205 
section "wellformed interface declarations" 

206 
(* wellformed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *) 

207 

208 
text {* 

209 
A interface declaration is wellformed if: 

210 
\begin{itemize} 

211 
\item the interface hierarchy is wellstructured 

212 
\item there is no class with the same name 

213 
\item the method heads are wellformed and not static and have Public access 

214 
\item the methods are uniquely named 

215 
\item all superinterfaces are accessible 

216 
\item the result type of a method overriding a method of Object widens to the 

217 
result type of the overridden method. 

218 
Shadowing static methods is forbidden. 

219 
\item the result type of a method overriding a set of methods defined in the 

220 
superinterfaces widens to each of the corresponding result types 

221 
\end{itemize} 

222 
*} 

223 
constdefs 

224 
wf_idecl :: "prog \<Rightarrow> idecl \<Rightarrow> bool" 

225 
"wf_idecl G \<equiv> 

226 
\<lambda>(I,i). 

227 
ws_idecl G I (isuperIfs i) \<and> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

228 
\<not>is_class G I \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

229 
(\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 
12854  230 
\<not>is_static mh \<and> 
231 
accmodi mh = Public) \<and> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

232 
unique (imethods i) \<and> 
12854  233 
(\<forall> J\<in>set (isuperIfs i). is_acc_iface G (pid I) J) \<and> 
234 
(table_of (imethods i) 

235 
hiding (methd G Object) 

236 
under (\<lambda> new old. accmodi old \<noteq> Private) 

237 
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 

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  240 
hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i)) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

241 
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old))" 
12854  242 

243 
lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow> 

244 
wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public" 

245 
apply (unfold wf_idecl_def) 

246 
apply auto 

247 
done 

248 

249 
lemma wf_idecl_hidings: 

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  252 
hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i)) 
253 
entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old" 

254 
apply (unfold wf_idecl_def o_def) 

255 
apply simp 

256 
done 

257 

258 
lemma wf_idecl_hiding: 

259 
"wf_idecl G (I, i) \<Longrightarrow> 

260 
(table_of (imethods i) 

261 
hiding (methd G Object) 

262 
under (\<lambda> new old. accmodi old \<noteq> Private) 

263 
entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 

264 
is_static new = is_static old))" 

265 
apply (unfold wf_idecl_def) 

266 
apply simp 

267 
done 

268 

269 
lemma wf_idecl_supD: 

270 
"\<lbrakk>wf_idecl G (I,i); J \<in> set (isuperIfs i)\<rbrakk> 

271 
\<Longrightarrow> is_acc_iface G (pid I) J \<and> (J, I) \<notin> (subint1 G)^+" 

272 
apply (unfold wf_idecl_def ws_idecl_def) 

273 
apply auto 

274 
done 

275 

276 
section "wellformed class declarations" 

277 
(* wellformed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and 

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 *) 

279 

280 
text {* 

281 
A class declaration is wellformed if: 

282 
\begin{itemize} 

283 
\item there is no interface with the same name 

284 
\item all superinterfaces are accessible and for all methods implementing 

285 
an interface method the result type widens to the result type of 

286 
the interface method, the method is not static and offers at least 

287 
as much access 

288 
(this actually means that the method has Public access, since all 

289 
interface methods have public access) 

290 
\item all field declarations are wellformed and the field names are unique 

291 
\item all method declarations are wellformed and the method names are unique 

292 
\item the initialization statement is welltyped 

293 
\item the classhierarchy is wellstructured 

294 
\item Unless the class is Object: 

295 
\begin{itemize} 

296 
\item the superclass is accessible 

297 
\item for all methods overriding another method (of a superclass )the 

298 
result type widens to the result type of the overridden method, 

299 
the access modifier of the new method provides at least as much 

300 
access as the overwritten one. 

301 
\item for all methods hiding a method (of a superclass) the hidden 

302 
method must be static and offer at least as much access rights. 

303 
Remark: In contrast to the Java Language Specification we don't 

304 
restrict the result types of the method 

305 
(as in case of overriding), because there seems to be no reason, 

306 
since there is no dynamic binding of static methods. 

307 
(cf. 8.4.6.3 vs. 15.12.1). 

308 
Stricly speaking the restrictions on the access rights aren't 

309 
necessary to, since the static type and the access rights 

310 
together determine which method is to be called statically. 

311 
But if a class gains more then one static method with the 

312 
same signature due to inheritance, it is confusing when the 

313 
method selection depends on the access rights only: 

314 
e.g. 

315 
Class C declares static public method foo(). 

316 
Class D is subclass of C and declares static method foo() 

317 
with default package access. 

318 
D.foo() ? if this call is in the same package as D then 

319 
foo of class D is called, otherwise foo of class C. 

320 
\end{itemize} 

321 

322 
\end{itemize} 

323 
*} 

324 
(* to Table *) 

325 
constdefs entails:: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" 

326 
("_ entails _" 20) 

327 
"t entails P \<equiv> \<forall>k. \<forall> x \<in> t k: P x" 

328 

329 
lemma entailsD: 

330 
"\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x" 

331 
by (simp add: entails_def) 

332 

333 
lemma empty_entails[simp]: "empty entails P" 

334 
by (simp add: entails_def) 

335 

336 
constdefs 

337 
wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" 

338 
"wf_cdecl G \<equiv> 

339 
\<lambda>(C,c). 

340 
\<not>is_iface G C \<and> 

341 
(\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> 

342 
(\<forall>s. \<forall> im \<in> imethds G I s. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 tabwidth;
wenzelm
parents:
30235
diff
changeset

344 
\<not> is_static cm \<and> 
12854  345 
accmodi im \<le> accmodi cm))) \<and> 
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  350 
\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and> 
351 
(C \<noteq> Object \<longrightarrow> 

352 
(is_acc_class G (pid C) (super c) \<and> 

353 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 

354 
entails (\<lambda> new. \<forall> old sig. 

355 
(G,sig\<turnstile>new overrides\<^sub>S old 

356 
\<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and> 

357 
accmodi old \<le> accmodi new \<and> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

358 
\<not>is_static old)) \<and> 
12854  359 
(G,sig\<turnstile>new hides old 
360 
\<longrightarrow> (accmodi old \<le> accmodi new \<and> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

361 
is_static old)))) 
12854  362 
))" 
363 

364 
(* 

365 
constdefs 

366 
wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" 

367 
"wf_cdecl G \<equiv> 

368 
\<lambda>(C,c). 

369 
\<not>is_iface G C \<and> 

370 
(\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> 

371 
(\<forall>s. \<forall> im \<in> imethds G I s. 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

372 
(\<exists> cm \<in> methd G C s: G\<turnstile>resTy (mthd cm)\<preceq>resTy (mthd im) \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

373 
\<not> is_static cm \<and> 
12854  374 
accmodi im \<le> accmodi cm))) \<and> 
375 
(\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 

376 
(\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 

377 
\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and> 

378 
(C \<noteq> Object \<longrightarrow> 

379 
(is_acc_class G (pid C) (super c) \<and> 

380 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 

381 
hiding methd G (super c) 

382 
under (\<lambda> new old. G\<turnstile>new overrides old) 

383 
entails (\<lambda> new old. 

384 
(G\<turnstile>resTy (mthd new)\<preceq>resTy (mthd old) \<and> 

385 
accmodi old \<le> accmodi new \<and> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

386 
\<not> is_static old))) \<and> 
12854  387 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
388 
hiding methd G (super c) 

389 
under (\<lambda> new old. G\<turnstile>new hides old) 

390 
entails (\<lambda> new old. is_static old \<and> 

391 
accmodi old \<le> accmodi new)) \<and> 

392 
(table_of (cfields c) hiding accfield G C (super c) 

393 
entails (\<lambda> newF oldF. accmodi oldF \<le> access newF))))" 

394 
*) 

395 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

396 
lemma wf_cdeclE [consumes 1]: 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

397 
"\<lbrakk>wf_cdecl G (C,c); 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

398 
\<lbrakk>\<not>is_iface G C; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

399 
(\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

400 
(\<forall>s. \<forall> im \<in> imethds G I s. 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

401 
(\<exists> cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

402 
\<not> is_static cm \<and> 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

403 
accmodi im \<le> accmodi cm))); 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

404 
\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f; unique (cfields c); 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

405 
\<forall>m\<in>set (methods c). wf_mdecl G C m; unique (methods c); 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

406 
jumpNestingOkS {} (init c); 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

407 
\<exists> A. \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

408 
\<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>; 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

409 
ws_cdecl G C (super c); 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

410 
(C \<noteq> Object \<longrightarrow> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

411 
(is_acc_class G (pid C) (super c) \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

412 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

413 
entails (\<lambda> new. \<forall> old sig. 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

414 
(G,sig\<turnstile>new overrides\<^sub>S old 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

415 
\<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and> 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

416 
accmodi old \<le> accmodi new \<and> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

417 
\<not>is_static old)) \<and> 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

418 
(G,sig\<turnstile>new hides old 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

419 
\<longrightarrow> (accmodi old \<le> accmodi new \<and> 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

420 
is_static old)))) 
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

421 
))\<rbrakk> \<Longrightarrow> P 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

422 
\<rbrakk> \<Longrightarrow> P" 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

423 
by (unfold wf_cdecl_def) simp 
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

424 

12854  425 
lemma wf_cdecl_unique: 
426 
"wf_cdecl G (C,c) \<Longrightarrow> unique (cfields c) \<and> unique (methods c)" 

427 
apply (unfold wf_cdecl_def) 

428 
apply auto 

429 
done 

430 

431 
lemma wf_cdecl_fdecl: 

432 
"\<lbrakk>wf_cdecl G (C,c); f\<in>set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f" 

433 
apply (unfold wf_cdecl_def) 

434 
apply auto 

435 
done 

436 

437 
lemma wf_cdecl_mdecl: 

438 
"\<lbrakk>wf_cdecl G (C,c); m\<in>set (methods c)\<rbrakk> \<Longrightarrow> wf_mdecl G C m" 

439 
apply (unfold wf_cdecl_def) 

440 
apply auto 

441 
done 

442 

443 
lemma wf_cdecl_impD: 

444 
"\<lbrakk>wf_cdecl G (C,c); I\<in>set (superIfs c)\<rbrakk> 

445 
\<Longrightarrow> is_acc_iface G (pid C) I \<and> 

446 
(\<forall>s. \<forall>im \<in> imethds G I s. 

447 
(\<exists>cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> \<not>is_static cm \<and> 

448 
accmodi im \<le> accmodi cm))" 

449 
apply (unfold wf_cdecl_def) 

450 
apply auto 

451 
done 

452 

453 
lemma wf_cdecl_supD: 

454 
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object\<rbrakk> \<Longrightarrow> 

455 
is_acc_class G (pid C) (super c) \<and> (super c,C) \<notin> (subcls1 G)^+ \<and> 

456 
(table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 

457 
entails (\<lambda> new. \<forall> old sig. 

458 
(G,sig\<turnstile>new overrides\<^sub>S old 

459 
\<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and> 

460 
accmodi old \<le> accmodi new \<and> 

461 
\<not>is_static old)) \<and> 

462 
(G,sig\<turnstile>new hides old 

463 
\<longrightarrow> (accmodi old \<le> accmodi new \<and> 

464 
is_static old))))" 

465 
apply (unfold wf_cdecl_def ws_cdecl_def) 

466 
apply auto 

467 
done 

468 

469 

470 
lemma wf_cdecl_overrides_SomeD: 

471 
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM; 

472 
G,sig\<turnstile>(C,newM) overrides\<^sub>S old 

473 
\<rbrakk> \<Longrightarrow> G\<turnstile>resTy newM\<preceq>resTy old \<and> 

474 
accmodi old \<le> accmodi newM \<and> 

475 
\<not> is_static old" 

476 
apply (drule (1) wf_cdecl_supD) 

477 
apply (clarify) 

478 
apply (drule entailsD) 

479 
apply (blast intro: table_of_map_SomeI) 

480 
apply (drule_tac x="old" in spec) 

481 
apply (auto dest: overrides_eq_sigD simp add: msig_def) 

482 
done 

483 

484 
lemma wf_cdecl_hides_SomeD: 

485 
"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM; 

486 
G,sig\<turnstile>(C,newM) hides old 

487 
\<rbrakk> \<Longrightarrow> accmodi old \<le> access newM \<and> 

488 
is_static old" 

489 
apply (drule (1) wf_cdecl_supD) 

490 
apply (clarify) 

491 
apply (drule entailsD) 

492 
apply (blast intro: table_of_map_SomeI) 

493 
apply (drule_tac x="old" in spec) 

494 
apply (auto dest: hides_eq_sigD simp add: msig_def) 

495 
done 

496 

497 
lemma wf_cdecl_wt_init: 

498 
"wf_cdecl G (C, c) \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>init c\<Colon>\<surd>" 

499 
apply (unfold wf_cdecl_def) 

500 
apply auto 

501 
done 

502 

503 

504 
section "wellformed programs" 

505 
(* wellformed program, cf. 8.1, 9.1 *) 

506 

507 
text {* 

508 
A program declaration is wellformed if: 

509 
\begin{itemize} 

510 
\item the class ObjectC of Object is defined 

14030  511 
\item every method of Object has an access modifier distinct from Package. 
512 
This is 

12854  513 
necessary since every interface automatically inherits from Object. 
514 
We must know, that every time a Object method is "overriden" by an 

515 
interface method this is also overriden by the class implementing the 

516 
the interface (see @{text "implement_dynmethd and class_mheadsD"}) 

517 
\item all standard Exceptions are defined 

518 
\item all defined interfaces are wellformed 

519 
\item all defined classes are wellformed 

520 
\end{itemize} 

521 
*} 

522 
constdefs 

523 
wf_prog :: "prog \<Rightarrow> bool" 

524 
"wf_prog G \<equiv> let is = ifaces G; cs = classes G in 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

525 
ObjectC \<in> set cs \<and> 
12854  526 
(\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and> 
527 
(\<forall>xn. SXcptC xn \<in> set cs) \<and> 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

528 
(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and> 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

529 
(\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs" 
12854  530 

531 
lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)" 

532 
apply (unfold wf_prog_def Let_def) 

533 
apply simp 

534 
apply (fast dest: map_of_SomeD) 

535 
done 

536 

537 
lemma wf_prog_cdecl: "\<lbrakk>class G C = Some c; wf_prog G\<rbrakk> \<Longrightarrow> wf_cdecl G (C,c)" 

538 
apply (unfold wf_prog_def Let_def) 

539 
apply simp 

540 
apply (fast dest: map_of_SomeD) 

541 
done 

542 

543 
lemma wf_prog_Object_mdecls: 

544 
"wf_prog G \<Longrightarrow> (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package)" 

545 
apply (unfold wf_prog_def Let_def) 

546 
apply simp 

547 
done 

548 

549 
lemma wf_prog_acc_superD: 

550 
"\<lbrakk>wf_prog G; class G C = Some c; C \<noteq> Object \<rbrakk> 

551 
\<Longrightarrow> is_acc_class G (pid C) (super c)" 

552 
by (auto dest: wf_prog_cdecl wf_cdecl_supD) 

553 

554 
lemma wf_ws_prog [elim!,simp]: "wf_prog G \<Longrightarrow> ws_prog G" 

555 
apply (unfold wf_prog_def Let_def) 

556 
apply (rule ws_progI) 

557 
apply (simp_all (no_asm)) 

558 
apply (auto simp add: is_acc_class_def is_acc_iface_def 

559 
dest!: wf_idecl_supD wf_cdecl_supD )+ 

560 
done 

561 

562 
lemma class_Object [simp]: 

563 
"wf_prog G \<Longrightarrow> 

564 
class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls, 

28524  565 
init=Skip,super=undefined,superIfs=[]\<rparr>" 
12854  566 
apply (unfold wf_prog_def Let_def ObjectC_def) 
567 
apply (fast dest!: map_of_SomeI) 

568 
done 

569 

570 
lemma methd_Object[simp]: "wf_prog G \<Longrightarrow> methd G Object = 

571 
table_of (map (\<lambda>(s,m). (s, Object, m)) Object_mdecls)" 

572 
apply (subst methd_rec) 

573 
apply (auto simp add: Let_def) 

574 
done 

575 

576 
lemma wf_prog_Object_methd: 

577 
"\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> accmodi m \<noteq> Package" 

578 
by (auto dest!: wf_prog_Object_mdecls) (auto dest!: map_of_SomeD) 

579 

580 
lemma wf_prog_Object_is_public[intro]: 

581 
"wf_prog G \<Longrightarrow> is_public G Object" 

582 
by (auto simp add: is_public_def dest: class_Object) 

583 

584 
lemma class_SXcpt [simp]: 

585 
"wf_prog G \<Longrightarrow> 

586 
class G (SXcpt xn) = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls, 

587 
init=Skip, 

588 
super=if xn = Throwable then Object 

589 
else SXcpt Throwable, 

590 
superIfs=[]\<rparr>" 

591 
apply (unfold wf_prog_def Let_def SXcptC_def) 

592 
apply (fast dest!: map_of_SomeI) 

593 
done 

594 

595 
lemma wf_ObjectC [simp]: 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

596 
"wf_cdecl G ObjectC = (\<not>is_iface G Object \<and> Ball (set Object_mdecls) 
12854  597 
(wf_mdecl G Object) \<and> unique Object_mdecls)" 
598 
apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def) 

13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset

599 
apply (auto intro: da.Skip) 
12854  600 
done 
601 

602 
lemma Object_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G Object" 

603 
apply (simp (no_asm_simp)) 

604 
done 

605 

606 
lemma Object_is_acc_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_acc_class G S Object" 

607 
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def 

608 
accessible_in_RefT_simp) 

609 
done 

610 

611 
lemma SXcpt_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G (SXcpt xn)" 

612 
apply (simp (no_asm_simp)) 

613 
done 

614 

615 
lemma SXcpt_is_acc_class [simp,elim!]: 

616 
"wf_prog G \<Longrightarrow> is_acc_class G S (SXcpt xn)" 

617 
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def 

618 
accessible_in_RefT_simp) 

619 
done 

620 

621 
lemma fields_Object [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G Object = []" 

622 
by (force intro: fields_emptyI) 

623 

624 
lemma accfield_Object [simp]: 

625 
"wf_prog G \<Longrightarrow> accfield G S Object = empty" 

626 
apply (unfold accfield_def) 

627 
apply (simp (no_asm_simp) add: Let_def) 

628 
done 

629 

630 
lemma fields_Throwable [simp]: 

631 
"wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt Throwable) = []" 

632 
by (force intro: fields_emptyI) 

633 

634 
lemma fields_SXcpt [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt xn) = []" 

635 
apply (case_tac "xn = Throwable") 

636 
apply (simp (no_asm_simp)) 

637 
by (force intro: fields_emptyI) 

638 

639 
lemmas widen_trans = ws_widen_trans [OF _ _ wf_ws_prog, elim] 

640 
lemma widen_trans2 [elim]: "\<lbrakk>G\<turnstile>U\<preceq>T; G\<turnstile>S\<preceq>U; wf_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T" 

641 
apply (erule (2) widen_trans) 

642 
done 

643 

644 
lemma Xcpt_subcls_Throwable [simp]: 

645 
"wf_prog G \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable" 

646 
apply (rule SXcpt_subcls_Throwable_lemma) 

647 
apply auto 

648 
done 

649 

650 
lemma unique_fields: 

651 
"\<lbrakk>is_class G C; wf_prog G\<rbrakk> \<Longrightarrow> unique (DeclConcepts.fields G C)" 

652 
apply (erule ws_unique_fields) 

653 
apply (erule wf_ws_prog) 

654 
apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]]) 

655 
done 

656 

657 
lemma fields_mono: 

658 
"\<lbrakk>table_of (DeclConcepts.fields G C) fn = Some f; G\<turnstile>D\<preceq>\<^sub>C C; 

659 
is_class G D; wf_prog G\<rbrakk> 

660 
\<Longrightarrow> table_of (DeclConcepts.fields G D) fn = Some f" 

661 
apply (rule map_of_SomeI) 

662 
apply (erule (1) unique_fields) 

663 
apply (erule (1) map_of_SomeD [THEN fields_mono_lemma]) 

664 
apply (erule wf_ws_prog) 

665 
done 

666 

667 

668 
lemma fields_is_type [elim]: 

669 
"\<lbrakk>table_of (DeclConcepts.fields G C) m = Some f; wf_prog G; is_class G C\<rbrakk> \<Longrightarrow> 

670 
is_type G (type f)" 

671 
apply (frule wf_ws_prog) 

672 
apply (force dest: fields_declC [THEN conjunct1] 

673 
wf_prog_cdecl [THEN wf_cdecl_fdecl] 

674 
simp add: wf_fdecl_def2 is_acc_type_def) 

675 
done 

676 

677 
lemma imethds_wf_mhead [rule_format (no_asm)]: 

678 
"\<lbrakk>m \<in> imethds G I sig; wf_prog G; is_iface G I\<rbrakk> \<Longrightarrow> 

679 
wf_mhead G (pid (decliface m)) sig (mthd m) \<and> 

680 
\<not> is_static m \<and> accmodi m = Public" 

681 
apply (frule wf_ws_prog) 

682 
apply (drule (2) imethds_declI [THEN conjunct1]) 

683 
apply clarify 

684 
apply (frule_tac I="(decliface m)" in wf_prog_idecl,assumption) 

685 
apply (drule wf_idecl_mhead) 

686 
apply (erule map_of_SomeD) 

687 
apply (cases m, simp) 

688 
done 

689 

690 
lemma methd_wf_mdecl: 

691 
"\<lbrakk>methd G C sig = Some m; wf_prog G; class G C = Some y\<rbrakk> \<Longrightarrow> 

692 
G\<turnstile>C\<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and> 

693 
wf_mdecl G (declclass m) (sig,(mthd m))" 

694 
apply (frule wf_ws_prog) 

695 
apply (drule (1) methd_declC) 

696 
apply fast 

697 
apply clarsimp 

698 
apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD) 

699 
done 

700 

701 
(* 

702 
This lemma doesn't hold! 

703 
lemma methd_rT_is_acc_type: 

704 
"\<lbrakk>wf_prog G;methd G C C sig = Some (D,m); 

705 
class G C = Some y\<rbrakk> 

706 
\<Longrightarrow> is_acc_type G (pid C) (resTy m)" 

707 
The result Type is only visible in the scope of defining class D 

708 
"is_vis_type G (pid D) (resTy m)" but not necessarily in scope of class C! 

709 
(The same is true for the type of pramaters of a method) 

710 
*) 

711 

712 

713 
lemma methd_rT_is_type: 

714 
"\<lbrakk>wf_prog G;methd G C sig = Some m; 

715 
class G C = Some y\<rbrakk> 

716 
\<Longrightarrow> is_type G (resTy m)" 

717 
apply (drule (2) methd_wf_mdecl) 

718 
apply clarify 

719 
apply (drule wf_mdeclD1) 

720 
apply clarify 

721 
apply (drule rT_is_acc_type) 

722 
apply (cases m, simp add: is_acc_type_def) 

723 
done 

724 

725 
lemma accmethd_rT_is_type: 

726 
"\<lbrakk>wf_prog G;accmethd G S C sig = Some m; 

727 
class G C = Some y\<rbrakk> 

728 
\<Longrightarrow> is_type G (resTy m)" 

729 
by (auto simp add: accmethd_def 

730 
intro: methd_rT_is_type) 

731 

732 
lemma methd_Object_SomeD: 

733 
"\<lbrakk>wf_prog G;methd G Object sig = Some m\<rbrakk> 

734 
\<Longrightarrow> declclass m = Object" 

735 
by (auto dest: class_Object simp add: methd_rec ) 

736 

737 
lemma wf_imethdsD: 

738 
"\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 

739 
\<Longrightarrow> \<not>is_static im \<and> accmodi im = Public" 

740 
proof  

741 
assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig" 

742 
have "wf_prog G \<longrightarrow> 

743 
(\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig 

744 
\<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I") 

745 
proof (rule iface_rec.induct,intro allI impI) 

746 
fix G I i im 

747 
assume hyp: "\<forall> J i. J \<in> set (isuperIfs i) \<and> ws_prog G \<and> iface G I = Some i 

748 
\<longrightarrow> ?P G J" 

749 
assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 

750 
im: "im \<in> imethds G I sig" 

751 
show "\<not>is_static im \<and> accmodi im = Public" 

752 
proof  

753 
let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))" 

30235
58d147683393
Made Option a separate theory and renamed option_map to Option.map
nipkow
parents:
28524
diff
changeset

754 
let ?new = "(Option.set \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))" 
12854  755 
from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

756 
by (simp add: imethds_rec) 
12854  757 
from wf if_I have 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

758 
wf_supI: "\<forall> J. J \<in> set (isuperIfs i) \<longrightarrow> (\<exists> j. iface G J = Some j)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

759 
by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD) 
12854  760 
from wf if_I have 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

761 
"\<forall> im \<in> set (imethods i). \<not> is_static im \<and> accmodi im = Public" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

762 
by (auto dest!: wf_prog_idecl wf_idecl_mhead) 
12854  763 
then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 
764 
\<longrightarrow> \<not> is_static im \<and> accmodi im = Public" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

765 
by (auto dest!: table_of_Some_in_set) 
12854  766 
show ?thesis 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

767 
proof (cases "?new sig = {}") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

768 
case True 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

769 
from True wf wf_supI if_I imethds hyp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

770 
show ?thesis by (auto simp del: split_paired_All) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

771 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

772 
case False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

773 
from False wf wf_supI if_I imethds new_ok hyp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

774 
show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

775 
qed 
12854  776 
qed 
777 
qed 

778 
with asm show ?thesis by (auto simp del: split_paired_All) 

779 
qed 

780 

781 
lemma wf_prog_hidesD: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

782 
assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

783 
shows 
12854  784 
"accmodi old \<le> accmodi new \<and> 
785 
is_static old" 

786 
proof  

787 
from hides 

788 
obtain c where 

789 
clsNew: "class G (declclass new) = Some c" and 

790 
neqObj: "declclass new \<noteq> Object" 

791 
by (auto dest: hidesD declared_in_classD) 

792 
with hides obtain newM oldM where 

793 
newM: "table_of (methods c) (msig new) = Some newM" and 

794 
new: "new = (declclass new,(msig new),newM)" and 

795 
old: "old = (declclass old,(msig old),oldM)" and 

796 
"msig new = msig old" 

797 
by (cases new,cases old) 

798 
(auto dest: hidesD 

799 
simp add: cdeclaredmethd_def declared_in_def) 

800 
with hides 

801 
have hides': 

802 
"G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)" 

803 
by auto 

804 
from clsNew wf 

805 
have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl) 

806 
note wf_cdecl_hides_SomeD [OF this neqObj newM hides'] 

807 
with new old 

808 
show ?thesis 

809 
by (cases new, cases old) auto 

810 
qed 

811 

812 
text {* Compare this lemma about static 

813 
overriding @{term "G \<turnstile>new overrides\<^sub>S old"} with the definition of 

814 
dynamic overriding @{term "G \<turnstile>new overrides old"}. 

815 
Conforming result types and restrictions on the access modifiers of the old 

816 
and the new method are not part of the predicate for static overriding. But 

817 
they are enshured in a wellfromed program. Dynamic overriding has 

818 
no restrictions on the access modifiers but enforces confrom result types 

819 
as precondition. But with some efford we can guarantee the access modifier 

820 
restriction for dynamic overriding, too. See lemma 

821 
@{text wf_prog_dyn_override_prop}. 

822 
*} 

823 
lemma wf_prog_stat_overridesD: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

824 
assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

825 
shows 
12854  826 
"G\<turnstile>resTy new\<preceq>resTy old \<and> 
827 
accmodi old \<le> accmodi new \<and> 

828 
\<not> is_static old" 

829 
proof  

830 
from stat_override 

831 
obtain c where 

832 
clsNew: "class G (declclass new) = Some c" and 

833 
neqObj: "declclass new \<noteq> Object" 

834 
by (auto dest: stat_overrides_commonD declared_in_classD) 

835 
with stat_override obtain newM oldM where 

836 
newM: "table_of (methods c) (msig new) = Some newM" and 

837 
new: "new = (declclass new,(msig new),newM)" and 

838 
old: "old = (declclass old,(msig old),oldM)" and 

839 
"msig new = msig old" 

840 
by (cases new,cases old) 

841 
(auto dest: stat_overrides_commonD 

842 
simp add: cdeclaredmethd_def declared_in_def) 

843 
with stat_override 

844 
have stat_override': 

845 
"G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)" 

846 
by auto 

847 
from clsNew wf 

848 
have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl) 

849 
note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override'] 

850 
with new old 

851 
show ?thesis 

852 
by (cases new, cases old) auto 

853 
qed 

854 

855 
lemma static_to_dynamic_overriding: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

856 
assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

857 
shows "G\<turnstile>new overrides old" 
12854  858 
proof  
859 
from stat_override 

860 
show ?thesis (is "?Overrides new old") 

861 
proof (induct) 

862 
case (Direct new old superNew) 

863 
then have stat_override:"G\<turnstile>new overrides\<^sub>S old" 

864 
by (rule stat_overridesR.Direct) 

865 
from stat_override wf 

866 
have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and 

867 
not_static_old: "\<not> is_static old" 

868 
by (auto dest: wf_prog_stat_overridesD) 

869 
have not_private_new: "accmodi new \<noteq> Private" 

870 
proof  

871 
from stat_override 

872 
have "accmodi old \<noteq> Private" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

873 
by (rule no_Private_stat_override) 
12854  874 
moreover 
875 
from stat_override wf 

876 
have "accmodi old \<le> accmodi new" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

877 
by (auto dest: wf_prog_stat_overridesD) 
12854  878 
ultimately 
879 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

880 
by (auto dest: acc_modi_bottom) 
12854  881 
qed 
882 
with Direct resTy_widen not_static_old 

883 
show "?Overrides new old" 

12962
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset

884 
by (auto intro: overridesR.Direct stat_override_declclasses_relation) 
12854  885 
next 
21765  886 
case (Indirect new inter old) 
12854  887 
then show "?Overrides new old" 
888 
by (blast intro: overridesR.Indirect) 

889 
qed 

890 
qed 

891 

892 
lemma non_Package_instance_method_inheritance: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

893 
assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

894 
accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

895 
instance_method: "\<not> is_static old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

896 
subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

897 
old_declared: "G\<turnstile>Method old declared_in (declclass old)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

898 
wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

899 
shows "G\<turnstile>Method old member_of C \<or> 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

900 
(\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)" 
12854  901 
proof  
902 
from wf have ws: "ws_prog G" by auto 

903 
from old_declared have iscls_declC_old: "is_class G (declclass old)" 

904 
by (auto simp add: declared_in_def cdeclaredmethd_def) 

905 
from subcls have iscls_C: "is_class G C" 

906 
by (blast dest: subcls_is_class) 

907 
from iscls_C ws old_inheritable subcls 

908 
show ?thesis (is "?P C old") 

909 
proof (induct rule: ws_class_induct') 

910 
case Object 

911 
assume "G\<turnstile>Object\<prec>\<^sub>C declclass old" 

912 
then show "?P Object old" 

913 
by blast 

914 
next 

915 
case (Subcls C c) 

916 
assume cls_C: "class G C = Some c" and 

917 
neq_C_Obj: "C \<noteq> Object" and 

918 
hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); 

919 
G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and 

920 
inheritable: "G \<turnstile>Method old inheritable_in pid C" and 

921 
subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old" 

922 
from cls_C neq_C_Obj 

923 
have super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" 

924 
by (rule subcls1I) 

925 
from wf cls_C neq_C_Obj 

926 
have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 

927 
by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD) 

928 
{ 

929 
fix old 

930 
assume member_super: "G\<turnstile>Method old member_of (super c)" 

931 
assume inheritable: "G \<turnstile>Method old inheritable_in pid C" 

932 
assume instance_method: "\<not> is_static old" 

933 
from member_super 

934 
have old_declared: "G\<turnstile>Method old declared_in (declclass old)" 

935 
by (cases old) (auto dest: member_of_declC) 

936 
have "?P C old" 

937 
proof (cases "G\<turnstile>mid (msig old) undeclared_in C") 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

938 
case True 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

939 
with inheritable super accessible_super member_super 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

940 
have "G\<turnstile>Method old member_of C" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

941 
by (cases old) (auto intro: members.Inherited) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

942 
then show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

943 
by auto 
12854  944 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

945 
case False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

946 
then obtain new_member where 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

947 
"G\<turnstile>new_member declared_in C" and 
12854  948 
"mid (msig old) = memberid new_member" 
949 
by (auto dest: not_undeclared_declared) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

950 
then obtain new where 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

951 
new: "G\<turnstile>Method new declared_in C" and 
12854  952 
eq_sig: "msig old = msig new" and 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

953 
declC_new: "declclass new = C" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

954 
by (cases new_member) auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

955 
then have member_new: "G\<turnstile>Method new member_of C" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

956 
by (cases new) (auto intro: members.Immediate) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

957 
from declC_new super member_super 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

958 
have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

959 
by (auto dest!: member_of_subclseq_declC 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

960 
dest: r_into_trancl intro: trancl_rtrancl_trancl) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

961 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

962 
proof (cases "is_static new") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

963 
case False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

964 
with eq_sig declC_new new old_declared inheritable 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

965 
super member_super subcls_new_old 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

966 
have "G\<turnstile>new overrides\<^sub>S old" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

967 
by (auto intro!: stat_overridesR.Direct) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

968 
with member_new show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

969 
by blast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

970 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

971 
case True 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

972 
with eq_sig declC_new subcls_new_old new old_declared inheritable 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

973 
have "G\<turnstile>new hides old" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

974 
by (auto intro: hidesI) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

975 
with wf 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

976 
have "is_static old" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

977 
by (blast dest: wf_prog_hidesD) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

978 
with instance_method 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

979 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

980 
by (contradiction) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

981 
qed 
12854  982 
qed 
983 
} note hyp_member_super = this 

984 
from subclsC cls_C 

985 
have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old" 

986 
by (rule subcls_superD) 

987 
then 

988 
show "?P C old" 

989 
proof (cases rule: subclseq_cases) 

990 
case Eq 

991 
assume "super c = declclass old" 

992 
with old_declared 

993 
have "G\<turnstile>Method old member_of (super c)" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

994 
by (cases old) (auto intro: members.Immediate) 
12854  995 
with inheritable instance_method 
996 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

997 
by (blast dest: hyp_member_super) 
12854  998 
next 
999 
case Subcls 

1000 
assume "G\<turnstile>super c\<prec>\<^sub>C declclass old" 

1001 
moreover 

1002 
from inheritable accmodi_old 

1003 
have "G \<turnstile>Method old inheritable_in pid (super c)" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1004 
by (cases "accmodi old") (auto simp add: inheritable_in_def) 
12854  1005 
ultimately 
1006 
have "?P (super c) old" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1007 
by (blast dest: hyp) 
12854  1008 
then show ?thesis 
1009 
proof 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1010 
assume "G \<turnstile>Method old member_of super c" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1011 
with inheritable instance_method 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1012 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1013 
by (blast dest: hyp_member_super) 
12854  1014 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1015 
assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1016 
then obtain super_new where 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1017 
super_new_override: "G \<turnstile> super_new overrides\<^sub>S old" and 
12854  1018 
super_new_member: "G \<turnstile>Method super_new member_of super c" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1019 
by blast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1020 
from super_new_override wf 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1021 
have "accmodi old \<le> accmodi super_new" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1022 
by (auto dest: wf_prog_stat_overridesD) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1023 
with inheritable accmodi_old 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1024 
have "G \<turnstile>Method super_new inheritable_in pid C" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1025 
by (auto simp add: inheritable_in_def 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1026 
split: acc_modi.splits 
12854  1027 
dest: acc_modi_le_Dests) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1028 
moreover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1029 
from super_new_override 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1030 
have "\<not> is_static super_new" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1031 
by (auto dest: stat_overrides_commonD) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1032 
moreover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1033 
note super_new_member 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1034 
ultimately have "?P C super_new" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1035 
by (auto dest: hyp_member_super) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1036 
then show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1037 
proof 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1038 
assume "G \<turnstile>Method super_new member_of C" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1039 
with super_new_override 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1040 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1041 
by blast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1042 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1043 
assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 
12854  1044 
G \<turnstile>Method new member_of C" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1045 
with super_new_override show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1046 
by (blast intro: stat_overridesR.Indirect) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1047 
qed 
12854  1048 
qed 
1049 
qed 

1050 
qed 

1051 
qed 

1052 

1053 
lemma non_Package_instance_method_inheritance_cases [consumes 6, 

1054 
case_names Inheritance Overriding]: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1055 
assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1056 
accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1057 
instance_method: "\<not> is_static old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1058 
subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1059 
old_declared: "G\<turnstile>Method old declared_in (declclass old)" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1060 
wf: "wf_prog G" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1061 
inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1062 
overriding: "\<And> new. 
12854  1063 
\<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk> 
1064 
\<Longrightarrow> P" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1065 
shows P 
12854  1066 
proof  
1067 
from old_inheritable accmodi_old instance_method subcls old_declared wf 

1068 
inheritance overriding 

1069 
show ?thesis 

1070 
by (auto dest: non_Package_instance_method_inheritance) 

1071 
qed 

1072 

1073 
lemma dynamic_to_static_overriding: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1074 
assumes dyn_override: "G\<turnstile> new overrides old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1075 
accmodi_old: "accmodi old \<noteq> Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1076 
wf: "wf_prog G" 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1077 
shows "G\<turnstile> new overrides\<^sub>S old" 
12854  1078 
proof  
1079 
from dyn_override accmodi_old 

1080 
show ?thesis (is "?Overrides new old") 

1081 
proof (induct rule: overridesR.induct) 

1082 
case (Direct new old) 

1083 
assume new_declared: "G\<turnstile>Method new declared_in declclass new" 

1084 
assume eq_sig_new_old: "msig new = msig old" 

1085 
assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" 

1086 
assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and 

1087 
"accmodi old \<noteq> Package" and 

1088 
"\<not> is_static old" and 

1089 
"G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and 

1090 
"G\<turnstile>Method old declared_in declclass old" 

1091 
from this wf 

1092 
show "?Overrides new old" 

1093 
proof (cases rule: non_Package_instance_method_inheritance_cases) 

1094 
case Inheritance 

1095 
assume "G \<turnstile>Method old member_of declclass new" 

1096 
then have "G\<turnstile>mid (msig old) undeclared_in declclass new" 

1097 
proof cases 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1098 
case Immediate 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1099 
with subcls_new_old wf show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1100 
by (auto dest: subcls_irrefl) 
12854  1101 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1102 
case Inherited 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1103 
then show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1104 
by (cases old) auto 
12854  1105 
qed 
1106 
with eq_sig_new_old new_declared 

1107 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1108 
by (cases old,cases new) (auto dest!: declared_not_undeclared) 
12854  1109 
next 
1110 
case (Overriding new') 

1111 
assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old" 

1112 
then have "msig new' = msig old" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1113 
by (auto dest: stat_overrides_commonD) 
12854  1114 
with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1115 
by simp 
12854  1116 
assume "G \<turnstile>Method new' member_of declclass new" 
1117 
then show ?thesis 

1118 
proof (cases) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1119 
case Immediate 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1120 
then have declC_new: "declclass new' = declclass new" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1121 
by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1122 
from Immediate 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1123 
have "G\<turnstile>Method new' declared_in declclass new" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1124 
by (cases new') auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1125 
with new_declared eq_sig_new_new' declC_new 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1126 
have "new=new'" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1127 
by (cases new, cases new') (auto dest: unique_declared_in) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1128 
with stat_override_new' 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1129 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1130 
by simp 
12854  1131 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1132 
case Inherited 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1133 
then have "G\<turnstile>mid (msig new') undeclared_in declclass new" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1134 
by (cases new') (auto) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1135 
with eq_sig_new_new' new_declared 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1136 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1137 
by (cases new,cases new') (auto dest!: declared_not_undeclared) 
12854  1138 
qed 
1139 
qed 

1140 
next 

21765  1141 
case (Indirect new inter old) 
12854  1142 
assume accmodi_old: "accmodi old \<noteq> Package" 
1143 
assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old" 

1144 
with accmodi_old 

1145 
have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old" 

1146 
by blast 

1147 
moreover 

1148 
assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter" 

1149 
moreover 

1150 
have "accmodi inter \<noteq> Package" 

1151 
proof  

1152 
from stat_override_inter_old wf 

1153 
have "accmodi old \<le> accmodi inter" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1154 
by (auto dest: wf_prog_stat_overridesD) 
12854  1155 
with stat_override_inter_old accmodi_old 
1156 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1157 
by (auto dest!: no_Private_stat_override 
12854  1158 
split: acc_modi.splits 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1159 
dest: acc_modi_le_Dests) 
12854  1160 
qed 
1161 
ultimately show "?Overrides new old" 

1162 
by (blast intro: stat_overridesR.Indirect) 

1163 
qed 

1164 
qed 

1165 

1166 
lemma wf_prog_dyn_override_prop: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1167 
assumes dyn_override: "G \<turnstile> new overrides old" and 
12854  1168 
wf: "wf_prog G" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1169 
shows "accmodi old \<le> accmodi new" 
12854  1170 
proof (cases "accmodi old = Package") 
1171 
case True 

1172 
note old_Package = this 

1173 
show ?thesis 

1174 
proof (cases "accmodi old \<le> accmodi new") 

1175 
case True then show ?thesis . 

1176 
next 

1177 
case False 

1178 
with old_Package 

1179 
have "accmodi new = Private" 

1180 
by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def) 

1181 
with dyn_override 

1182 
show ?thesis 

1183 
by (auto dest: overrides_commonD) 

1184 
qed 

1185 
next 

1186 
case False 

1187 
with dyn_override wf 

1188 
have "G \<turnstile> new overrides\<^sub>S old" 

1189 
by (blast intro: dynamic_to_static_overriding) 

1190 
with wf 

1191 
show ?thesis 

1192 
by (blast dest: wf_prog_stat_overridesD) 

1193 
qed 

1194 

1195 
lemma overrides_Package_old: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1196 
assumes dyn_override: "G \<turnstile> new overrides old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1197 
accmodi_new: "accmodi new = Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1198 
wf: "wf_prog G " 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1199 
shows "accmodi old = Package" 
12854  1200 
proof (cases "accmodi old") 
1201 
case Private 

1202 
with dyn_override show ?thesis 

1203 
by (simp add: no_Private_override) 

1204 
next 

1205 
case Package 

1206 
then show ?thesis . 

1207 
next 

1208 
case Protected 

1209 
with dyn_override wf 

1210 
have "G \<turnstile> new overrides\<^sub>S old" 

1211 
by (auto intro: dynamic_to_static_overriding) 

1212 
with wf 

1213 
have "accmodi old \<le> accmodi new" 

1214 
by (auto dest: wf_prog_stat_overridesD) 

1215 
with Protected accmodi_new 

1216 
show ?thesis 

1217 
by (simp add: less_acc_def le_acc_def) 

1218 
next 

1219 
case Public 

1220 
with dyn_override wf 

1221 
have "G \<turnstile> new overrides\<^sub>S old" 

1222 
by (auto intro: dynamic_to_static_overriding) 

1223 
with wf 

1224 
have "accmodi old \<le> accmodi new" 

1225 
by (auto dest: wf_prog_stat_overridesD) 

1226 
with Public accmodi_new 

1227 
show ?thesis 

1228 
by (simp add: less_acc_def le_acc_def) 

1229 
qed 

1230 

1231 
lemma dyn_override_Package: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1232 
assumes dyn_override: "G \<turnstile> new overrides old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1233 
accmodi_old: "accmodi old = Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1234 
accmodi_new: "accmodi new = Package" and 
12854  1235 
wf: "wf_prog G" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1236 
shows "pid (declclass old) = pid (declclass new)" 
12854  1237 
proof  
1238 
from dyn_override accmodi_old accmodi_new 

1239 
show ?thesis (is "?EqPid old new") 

1240 
proof (induct rule: overridesR.induct) 

1241 
case (Direct new old) 

1242 
assume "accmodi old = Package" 

1243 
"G \<turnstile>Method old inheritable_in pid (declclass new)" 

1244 
then show "pid (declclass old) = pid (declclass new)" 

1245 
by (auto simp add: inheritable_in_def) 

1246 
next 

21765  1247 
case (Indirect new inter old) 
12854  1248 
assume accmodi_old: "accmodi old = Package" and 
1249 
accmodi_new: "accmodi new = Package" 

1250 
assume "G \<turnstile> new overrides inter" 

1251 
with accmodi_new wf 

1252 
have "accmodi inter = Package" 

1253 
by (auto intro: overrides_Package_old) 

1254 
with Indirect 

1255 
show "pid (declclass old) = pid (declclass new)" 

1256 
by auto 

1257 
qed 

1258 
qed 

1259 

1260 
lemma dyn_override_Package_escape: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1261 
assumes dyn_override: "G \<turnstile> new overrides old" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1262 
accmodi_old: "accmodi old = Package" and 
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1263 
outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and 
12854  1264 
wf: "wf_prog G" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1265 
shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and> 
12854  1266 
pid (declclass old) = pid (declclass inter) \<and> 
1267 
Protected \<le> accmodi inter" 

1268 
proof  

1269 
from dyn_override accmodi_old outside_pack 

1270 
show ?thesis (is "?P new old") 

1271 
proof (induct rule: overridesR.induct) 

1272 
case (Direct new old) 

1273 
assume accmodi_old: "accmodi old = Package" 

1274 
assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" 

1275 
assume "G \<turnstile>Method old inheritable_in pid (declclass new)" 

1276 
with accmodi_old 

1277 
have "pid (declclass old) = pid (declclass new)" 

1278 
by (simp add: inheritable_in_def) 

1279 
with outside_pack 

1280 
show "?P new old" 

1281 
by (contradiction) 

1282 
next 

21765  1283 
case (Indirect new inter old) 
12854  1284 
assume accmodi_old: "accmodi old = Package" 
1285 
assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" 

1286 
assume override_new_inter: "G \<turnstile> new overrides inter" 

1287 
assume override_inter_old: "G \<turnstile> inter overrides old" 

1288 
assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; 

1289 
pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk> 

1290 
\<Longrightarrow> ?P new inter" 

1291 
assume hyp_inter_old: "\<lbrakk>accmodi old = Package; 

1292 
pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk> 

1293 
\<Longrightarrow> ?P inter old" 

1294 
show "?P new old" 

1295 
proof (cases "pid (declclass old) = pid (declclass inter)") 

1296 
case True 

1297 
note same_pack_old_inter = this 

1298 
show ?thesis 

1299 
proof (cases "pid (declclass inter) = pid (declclass new)") 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1300 
case True 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1301 
with same_pack_old_inter outside_pack 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1302 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1303 
by auto 
12854  1304 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1305 
case False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1306 
note diff_pack_inter_new = this 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1307 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1308 
proof (cases "accmodi inter = Package") 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1309 
case True 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1310 
with diff_pack_inter_new hyp_new_inter 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1311 
obtain newinter where 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1312 
over_new_newinter: "G \<turnstile> new overrides newinter" and 
12854  1313 
over_newinter_inter: "G \<turnstile> newinter overrides inter" and 
1314 
eq_pid: "pid (declclass inter) = pid (declclass newinter)" and 

1315 
accmodi_newinter: "Protected \<le> accmodi newinter" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1316 
by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1317 
from over_newinter_inter override_inter_old 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1318 
have "G\<turnstile>newinter overrides old" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1319 
by (rule overridesR.Indirect) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1320 
moreover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1321 
from eq_pid same_pack_old_inter 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1322 
have "pid (declclass old) = pid (declclass newinter)" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1323 
by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1324 
moreover 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1325 
note over_new_newinter accmodi_newinter 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1326 
ultimately show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1327 
by blast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1328 
next 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1329 
case False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1330 
with override_new_inter 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1331 
have "Protected \<le> accmodi inter" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1332 
by (cases "accmodi inter") (auto dest: no_Private_override) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1333 
with override_new_inter override_inter_old same_pack_old_inter 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1334 
show ?thesis 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1335 
by blast 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1336 
qed 
12854  1337 
qed 
1338 
next 

1339 
case False 

1340 
with accmodi_old hyp_inter_old 

1341 
obtain newinter where 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1342 
over_inter_newinter: "G \<turnstile> inter overrides newinter" and 
12854  1343 
over_newinter_old: "G \<turnstile> newinter overrides old" and 
1344 
eq_pid: "pid (declclass old) = pid (declclass newinter)" and 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1345 
accmodi_newinter: "Protected \<le> accmodi newinter" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1346 
by auto 
12854  1347 
from override_new_inter over_inter_newinter 
1348 
have "G \<turnstile> new overrides newinter" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1349 
by (rule overridesR.Indirect) 
12854  1350 
with eq_pid over_newinter_old accmodi_newinter 
1351 
show ?thesis 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1352 
by blast 
12854  1353 
qed 
1354 
qed 

1355 
qed 

1356 

1357 
lemma declclass_widen[rule_format]: 

1358 
"wf_prog G 

1359 
\<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 

1360 
\<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C") 

1361 
proof (rule class_rec.induct,intro allI impI) 

1362 
fix G C c m 

1363 
assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c 

1364 
\<longrightarrow> ?P G (super c)" 

1365 
assume wf: "wf_prog G" and cls_C: "class G C = Some c" and 

1366 
m: "methd G C sig = Some m" 

1367 
show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 

1368 
proof (cases "C=Object") 

1369 
case True 

1370 
with wf m show ?thesis by (simp add: methd_Object_SomeD) 

1371 
next 

1372 
let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)" 

1373 
let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" 

1374 
case False 

1375 
with cls_C wf m 

1376 
have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m " 

1377 
by (simp add: methd_rec) 

1378 
show ?thesis 

1379 
proof (cases "?table sig") 

1380 
case None 

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 tabwidth;
wenzelm
parents:
30235
diff
changeset

1382 
by simp 
12854  1383 
moreover 
1384 
from wf cls_C False obtain sup where "class G (super c) = Some sup" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30235
diff
changeset

1385 
by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
