author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47176  568fdc70e565 
child 51703  f2e92fc0c8aa 
permissions  rwrr 
12857  1 
(* Title: HOL/Bali/WellForm.thy 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset

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

5 
header {* Wellformedness of Java programs *} 

16417  6 
theory WellForm imports DefiniteAssignment begin 
12854  7 

8 
text {* 

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

10 

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

12 
\begin{itemize} 

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

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

15 
(instead of identical type) 

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

17 
there are no restrictions to the result type 

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

19 
static methods 

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

21 
methods need not have identical return types 

22 
\end{itemize} 

23 
simplifications: 

24 
\begin{itemize} 

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

26 
classes 

27 
\end{itemize} 

28 
*} 

29 

30 
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

31 
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

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

37956  34 
definition 
35 
wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" 

36 
where "wf_fdecl G P = (\<lambda>(fn,f). is_acc_type G P (type f))" 

12854  37 

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

39 
apply (unfold wf_fdecl_def) 

40 
apply simp 

41 
done 

42 

43 

44 

45 
section "wellformed method declarations" 

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

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

48 

49 
text {* 

50 
A method head is wellformed if: 

51 
\begin{itemize} 

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

53 
\item all types of the parameters are visible 

54 
\item the result type is visible 

55 
\item the parameter names are unique 

56 
\end{itemize} 

57 
*} 

37956  58 
definition 
59 
wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where 

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

46212  61 
( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 
12854  62 
is_acc_type G P (resTy mh) \<and> 
46212  63 
distinct (pars mh))" 
12854  64 

65 

66 
text {* 

67 
A method declaration is wellformed if: 

68 
\begin{itemize} 

69 
\item the method head is wellformed 

70 
\item the names of the local variables are unique 

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

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

73 
\item the class of the method is defined 

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

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

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

77 
with there types. 

78 
\end{itemize} 

79 
*} 

80 

37956  81 
definition 
82 
callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where 

83 
"callee_lcl C sig m = 

84 
(\<lambda>k. (case k of 

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

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

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

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

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

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

91 

37956  92 
definition 
93 
parameters :: "methd \<Rightarrow> lname set" where 

94 
"parameters m = set (map (EName \<circ> VNam) (pars m)) \<union> (if (static m) then {} else {This})" 

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

95 

37956  96 
definition 
97 
wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where 

98 
"wf_mdecl G C = 

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

110 

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

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

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

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

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

115 

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

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

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

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

119 

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

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

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

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

123 

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

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

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

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

127 

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

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

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

130 
by simp 
12854  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 
*} 

37956  223 
definition 
224 
wf_idecl :: "prog \<Rightarrow> idecl \<Rightarrow> bool" where 

225 
"wf_idecl G = 

226 
(\<lambda>(I,i). 

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

37956  325 
definition 
326 
entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20) 

327 
where "(t entails P) = (\<forall>k. \<forall> x \<in> t k: P x)" 

12854  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 

37956  336 
definition 
337 
wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where 

338 
"wf_cdecl G = 

339 
(\<lambda>(C,c). 

12854  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)))) 
37956  362 
)))" 
12854  363 

364 
(* 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35067
diff
changeset

365 
definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where 
12854  366 
"wf_cdecl G \<equiv> 
367 
\<lambda>(C,c). 

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

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

370 
(\<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

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

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

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

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

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

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

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

380 
hiding methd G (super c) 

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

382 
entails (\<lambda> new old. 

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

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

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

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

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

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

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

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

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

393 
*) 

394 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

423 

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

426 
apply (unfold wf_cdecl_def) 

427 
apply auto 

428 
done 

429 

430 
lemma wf_cdecl_fdecl: 

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

432 
apply (unfold wf_cdecl_def) 

433 
apply auto 

434 
done 

435 

436 
lemma wf_cdecl_mdecl: 

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

438 
apply (unfold wf_cdecl_def) 

439 
apply auto 

440 
done 

441 

442 
lemma wf_cdecl_impD: 

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

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

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

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

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

448 
apply (unfold wf_cdecl_def) 

449 
apply auto 

450 
done 

451 

452 
lemma wf_cdecl_supD: 

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

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

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

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

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

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

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

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

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

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

463 
is_static old))))" 

464 
apply (unfold wf_cdecl_def ws_cdecl_def) 

465 
apply auto 

466 
done 

467 

468 

469 
lemma wf_cdecl_overrides_SomeD: 

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

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

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

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

474 
\<not> is_static old" 

475 
apply (drule (1) wf_cdecl_supD) 

476 
apply (clarify) 

477 
apply (drule entailsD) 

478 
apply (blast intro: table_of_map_SomeI) 

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

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

481 
done 

482 

483 
lemma wf_cdecl_hides_SomeD: 

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

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

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

487 
is_static old" 

488 
apply (drule (1) wf_cdecl_supD) 

489 
apply (clarify) 

490 
apply (drule entailsD) 

491 
apply (blast intro: table_of_map_SomeI) 

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

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

494 
done 

495 

496 
lemma wf_cdecl_wt_init: 

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

498 
apply (unfold wf_cdecl_def) 

499 
apply auto 

500 
done 

501 

502 

503 
section "wellformed programs" 

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

505 

506 
text {* 

507 
A program declaration is wellformed if: 

508 
\begin{itemize} 

509 
\item the class ObjectC of Object is defined 

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

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

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

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

516 
\item all standard Exceptions are defined 

517 
\item all defined interfaces are wellformed 

518 
\item all defined classes are wellformed 

519 
\end{itemize} 

520 
*} 

37956  521 
definition 
522 
wf_prog :: "prog \<Rightarrow> bool" where 

523 
"wf_prog G = (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

524 
ObjectC \<in> set cs \<and> 
12854  525 
(\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and> 
526 
(\<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

527 
(\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and> 
37956  528 
(\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs)" 
12854  529 

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

531 
apply (unfold wf_prog_def Let_def) 

532 
apply simp 

533 
apply (fast dest: map_of_SomeD) 

534 
done 

535 

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

537 
apply (unfold wf_prog_def Let_def) 

538 
apply simp 

539 
apply (fast dest: map_of_SomeD) 

540 
done 

541 

542 
lemma wf_prog_Object_mdecls: 

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

544 
apply (unfold wf_prog_def Let_def) 

545 
apply simp 

546 
done 

547 

548 
lemma wf_prog_acc_superD: 

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

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

551 
by (auto dest: wf_prog_cdecl wf_cdecl_supD) 

552 

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

554 
apply (unfold wf_prog_def Let_def) 

555 
apply (rule ws_progI) 

556 
apply (simp_all (no_asm)) 

557 
apply (auto simp add: is_acc_class_def is_acc_iface_def 

558 
dest!: wf_idecl_supD wf_cdecl_supD )+ 

559 
done 

560 

561 
lemma class_Object [simp]: 

562 
"wf_prog G \<Longrightarrow> 

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

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

567 
done 

568 

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

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

571 
apply (subst methd_rec) 

572 
apply (auto simp add: Let_def) 

573 
done 

574 

575 
lemma wf_prog_Object_methd: 

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

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

578 

579 
lemma wf_prog_Object_is_public[intro]: 

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

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

582 

583 
lemma class_SXcpt [simp]: 

584 
"wf_prog G \<Longrightarrow> 

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

586 
init=Skip, 

587 
super=if xn = Throwable then Object 

588 
else SXcpt Throwable, 

589 
superIfs=[]\<rparr>" 

590 
apply (unfold wf_prog_def Let_def SXcptC_def) 

591 
apply (fast dest!: map_of_SomeI) 

592 
done 

593 

594 
lemma wf_ObjectC [simp]: 

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

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

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

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

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

602 
apply (simp (no_asm_simp)) 

603 
done 

604 

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

606 
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def 

607 
accessible_in_RefT_simp) 

608 
done 

609 

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

611 
apply (simp (no_asm_simp)) 

612 
done 

613 

614 
lemma SXcpt_is_acc_class [simp,elim!]: 

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

616 
apply (simp (no_asm_simp) add: is_acc_class_def is_public_def 

617 
accessible_in_RefT_simp) 

618 
done 

619 

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

621 
by (force intro: fields_emptyI) 

622 

623 
lemma accfield_Object [simp]: 

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

625 
apply (unfold accfield_def) 

626 
apply (simp (no_asm_simp) add: Let_def) 

627 
done 

628 

629 
lemma fields_Throwable [simp]: 

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

631 
by (force intro: fields_emptyI) 

632 

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

634 
apply (case_tac "xn = Throwable") 

635 
apply (simp (no_asm_simp)) 

636 
by (force intro: fields_emptyI) 

637 

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

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

640 
apply (erule (2) widen_trans) 

641 
done 

642 

643 
lemma Xcpt_subcls_Throwable [simp]: 

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

645 
apply (rule SXcpt_subcls_Throwable_lemma) 

646 
apply auto 

647 
done 

648 

649 
lemma unique_fields: 

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

651 
apply (erule ws_unique_fields) 

652 
apply (erule wf_ws_prog) 

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

654 
done 

655 

656 
lemma fields_mono: 

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

658 
is_class G D; wf_prog G\<rbrakk> 

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

660 
apply (rule map_of_SomeI) 

661 
apply (erule (1) unique_fields) 

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

663 
apply (erule wf_ws_prog) 

664 
done 

665 

666 

667 
lemma fields_is_type [elim]: 

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

669 
is_type G (type f)" 

670 
apply (frule wf_ws_prog) 

671 
apply (force dest: fields_declC [THEN conjunct1] 

672 
wf_prog_cdecl [THEN wf_cdecl_fdecl] 

673 
simp add: wf_fdecl_def2 is_acc_type_def) 

674 
done 

675 

676 
lemma imethds_wf_mhead [rule_format (no_asm)]: 

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

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

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

680 
apply (frule wf_ws_prog) 

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

682 
apply clarify 

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

684 
apply (drule wf_idecl_mhead) 

685 
apply (erule map_of_SomeD) 

686 
apply (cases m, simp) 

687 
done 

688 

689 
lemma methd_wf_mdecl: 

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

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

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

693 
apply (frule wf_ws_prog) 

694 
apply (drule (1) methd_declC) 

695 
apply fast 

696 
apply clarsimp 

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

698 
done 

699 

700 
(* 

701 
This lemma doesn't hold! 

702 
lemma methd_rT_is_acc_type: 

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

704 
class G C = Some y\<rbrakk> 

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

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

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

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

709 
*) 

710 

711 

712 
lemma methd_rT_is_type: 

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

714 
class G C = Some y\<rbrakk> 

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

716 
apply (drule (2) methd_wf_mdecl) 

717 
apply clarify 

718 
apply (drule wf_mdeclD1) 

719 
apply clarify 

720 
apply (drule rT_is_acc_type) 

721 
apply (cases m, simp add: is_acc_type_def) 

722 
done 

723 

724 
lemma accmethd_rT_is_type: 

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

726 
class G C = Some y\<rbrakk> 

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

728 
by (auto simp add: accmethd_def 

729 
intro: methd_rT_is_type) 

730 

731 
lemma methd_Object_SomeD: 

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

733 
\<Longrightarrow> declclass m = Object" 

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

735 

45608  736 
lemmas iface_rec_induct' = iface_rec.induct [of "%x y z. P x y"] for P 
737 

12854  738 
lemma wf_imethdsD: 
739 
"\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 

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

741 
proof  

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

35440  743 

12854  744 
have "wf_prog G \<longrightarrow> 
745 
(\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig 

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

35440  747 
proof (induct G I rule: iface_rec_induct', intro allI impI) 
12854  748 
fix G I i im 
35440  749 
assume hyp: "\<And> i J. iface G I = Some i \<Longrightarrow> ws_prog G \<Longrightarrow> J \<in> set (isuperIfs i) 
750 
\<Longrightarrow> ?P G J" 

12854  751 
assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 
752 
im: "im \<in> imethds G I sig" 

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

754 
proof  

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

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

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

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

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

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

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

764 
by (auto dest!: wf_prog_idecl wf_idecl_mhead) 
12854  765 
then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 
766 
\<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

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

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

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

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

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

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

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

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

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

777 
qed 
12854  778 
qed 
779 
qed 

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

781 
qed 

782 

783 
lemma wf_prog_hidesD: 

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

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

785 
shows 
12854  786 
"accmodi old \<le> accmodi new \<and> 
787 
is_static old" 

788 
proof  

789 
from hides 

790 
obtain c where 

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

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

793 
by (auto dest: hidesD declared_in_classD) 

794 
with hides obtain newM oldM where 

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

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

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

798 
"msig new = msig old" 

799 
by (cases new,cases old) 

800 
(auto dest: hidesD 

801 
simp add: cdeclaredmethd_def declared_in_def) 

802 
with hides 

803 
have hides': 

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

805 
by auto 

806 
from clsNew wf 

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

808 
note wf_cdecl_hides_SomeD [OF this neqObj newM hides'] 

809 
with new old 

810 
show ?thesis 

811 
by (cases new, cases old) auto 

812 
qed 

813 

814 
text {* Compare this lemma about static 

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

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

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

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

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

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

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

822 
restriction for dynamic overriding, too. See lemma 

823 
@{text wf_prog_dyn_override_prop}. 

824 
*} 

825 
lemma wf_prog_stat_overridesD: 

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

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

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

830 
\<not> is_static old" 

831 
proof  

832 
from stat_override 

833 
obtain c where 

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

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

836 
by (auto dest: stat_overrides_commonD declared_in_classD) 

837 
with stat_override obtain newM oldM where 

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

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

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

841 
"msig new = msig old" 

842 
by (cases new,cases old) 

843 
(auto dest: stat_overrides_commonD 

844 
simp add: cdeclaredmethd_def declared_in_def) 

845 
with stat_override 

846 
have stat_override': 

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

848 
by auto 

849 
from clsNew wf 

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

851 
note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override'] 

852 
with new old 

853 
show ?thesis 

854 
by (cases new, cases old) auto 

855 
qed 

856 

857 
lemma static_to_dynamic_overriding: 

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

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

859 
shows "G\<turnstile>new overrides old" 
12854  860 
proof  
861 
from stat_override 

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

863 
proof (induct) 

864 
case (Direct new old superNew) 

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

866 
by (rule stat_overridesR.Direct) 

867 
from stat_override wf 

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

869 
not_static_old: "\<not> is_static old" 

870 
by (auto dest: wf_prog_stat_overridesD) 

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

872 
proof  

873 
from stat_override 

874 
have "accmodi old \<noteq> Private" 

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

875 
by (rule no_Private_stat_override) 
12854  876 
moreover 
877 
from stat_override wf 

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

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

879 
by (auto dest: wf_prog_stat_overridesD) 
12854  880 
ultimately 
881 
show ?thesis 

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

882 
by (auto dest: acc_modi_bottom) 
12854  883 
qed 
884 
with Direct resTy_widen not_static_old 

885 
show "?Overrides new old" 

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

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

891 
qed 

892 
qed 

893 

894 
lemma non_Package_instance_method_inheritance: 

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

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

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

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

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

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

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

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

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

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

906 
by (auto simp add: declared_in_def cdeclaredmethd_def) 

907 
from subcls have iscls_C: "is_class G C" 

908 
by (blast dest: subcls_is_class) 

909 
from iscls_C ws old_inheritable subcls 

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

911 
proof (induct rule: ws_class_induct') 

912 
case Object 

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

914 
then show "?P Object old" 

915 
by blast 

916 
next 

917 
case (Subcls C c) 

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

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

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

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

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

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

924 
from cls_C neq_C_Obj 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35067
diff
changeset

925 
have super: "G\<turnstile>C \<prec>\<^sub>C1 super c" 
12854  926 
by (rule subcls1I) 
927 
from wf cls_C neq_C_Obj 

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

929 
by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD) 

930 
{ 

931 
fix old 

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

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

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

935 
from member_super 

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

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

938 
have "?P C old" 

939 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

983 
qed 
12854  984 
qed 
985 
} note hyp_member_super = this 

986 
from subclsC cls_C 

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

988 
by (rule subcls_superD) 

989 
then 

990 
show "?P C old" 

991 
proof (cases rule: subclseq_cases) 

992 
case Eq 

993 
assume "super c = declclass old" 

994 
with old_declared 

995 
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

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

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

999 
by (blast dest: hyp_member_super) 
12854  1000 
next 
1001 
case Subcls 

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

1003 
moreover 

1004 
from inheritable accmodi_old 

1005 
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

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

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

1009 
by (blast dest: hyp) 
12854  1010 
then show ?thesis 
1011 
proof 

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

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

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

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

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

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

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

1019 
super_new_override: "G \<turnstile> super_new overrides\<^sub>S old" and 
12854  1020 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1049 
qed 
12854  1050 
qed 
1051 
qed 

1052 
qed 

1053 
qed 

1054 

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

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

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

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

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

1060 
old_declared: "G\<turnstile>Method old declared_in (declclass old)" and 
47176  1061 
wf: "wf_prog G" 
1062 
obtains (Inheritance) "G\<turnstile>Method old member_of C" 

1063 
 (Overriding) new where "G\<turnstile> new overrides\<^sub>S old" and "G\<turnstile>Method new member_of C" 

12854  1064 
proof  
1065 
from old_inheritable accmodi_old instance_method subcls old_declared wf 

47176  1066 
Inheritance Overriding 
1067 
show thesis 

12854  1068 
by (auto dest: non_Package_instance_method_inheritance) 
1069 
qed 

1070 

1071 
lemma dynamic_to_static_overriding: 

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

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

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

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

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

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

1079 
proof (induct rule: overridesR.induct) 

1080 
case (Direct new old) 

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

1082 
assume eq_sig_new_old: "msig new = msig old" 

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

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

1085 
"accmodi old \<noteq> Package" and 

1086 
"\<not> is_static old" and 

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

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

1089 
from this wf 

1090 
show "?Overrides new old" 

1091 
proof (cases rule: non_Package_instance_method_inheritance_cases) 

1092 
case Inheritance 

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

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

1095 
proof cases 

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

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

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

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

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

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

1102 
by (cases old) auto 
12854  1103 
qed 
1104 
with eq_sig_new_old new_declared 

1105 
show ?thesis 

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

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

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

1110 
then have "msig new' = msig old" 

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

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

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

1116 
proof (cases) 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1135 
by (cases new,cases new') (auto dest!: declared_not_undeclared) 
12854  1136 
qed 
1137 
qed 

1138 
next 

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

1142 
with accmodi_old 

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

1144 
by blast 

1145 
moreover 

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

1147 
moreover 

1148 
have "accmodi inter \<noteq> Package" 

1149 
proof  

1150 
from stat_override_inter_old wf 

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

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

1152 
by (auto dest: wf_prog_stat_overridesD) 
12854  1153 
with stat_override_inter_old accmodi_old 
1154 
show ?thesis 

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

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

1157 
dest: acc_modi_le_Dests) 
12854  1158 
qed 
1159 
ultimately show "?Overrides new old" 

1160 
by (blast intro: stat_overridesR.Indirect) 

1161 
qed 

1162 
qed 

1163 

1164 
lemma wf_prog_dyn_override_prop: 

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

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

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

1170 
note old_Package = this 

1171 
show ?thesis 

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

1173 
case True then show ?thesis . 

1174 
next 

1175 
case False 

1176 
with old_Package 

1177 
have "accmodi new = Private" 

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

1179 
with dyn_override 

1180 
show ?thesis 

1181 
by (auto dest: overrides_commonD) 

1182 
qed 

1183 
next 

1184 
case False 

1185 
with dyn_override wf 

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

1187 
by (blast intro: dynamic_to_static_overriding) 

1188 
with wf 

1189 
show ?thesis 

1190 
by (blast dest: wf_prog_stat_overridesD) 

1191 
qed 

1192 

1193 
lemma overrides_Package_old: 

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

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

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

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

1197 
shows "accmodi old = Package" 
12854  1198 
proof (cases "accmodi old") 
1199 
case Private 

1200 
with dyn_override show ?thesis 

1201 
by (simp add: no_Private_override) 

1202 
next 

1203 
case Package 

1204 
then show ?thesis . 

1205 
next 

1206 
case Protected 

1207 
with dyn_override wf 

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

1209 
by (auto intro: dynamic_to_static_overriding) 

1210 
with wf 

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

1212 
by (auto dest: wf_prog_stat_overridesD) 

1213 
with Protected accmodi_new 

1214 
show ?thesis 

1215 
by (simp add: less_acc_def le_acc_def) 

1216 
next 

1217 
case Public 

1218 
with dyn_override wf 

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

1220 
by (auto intro: dynamic_to_static_overriding) 

1221 
with wf 

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

1223 
by (auto dest: wf_prog_stat_overridesD) 

1224 
with Public accmodi_new 

1225 
show ?thesis 

1226 
by (simp add: less_acc_def le_acc_def) 

1227 
qed 

1228 

1229 
lemma dyn_override_Package: 

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

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

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

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

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

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

1238 
proof (induct rule: overridesR.induct) 

1239 
case (Direct new old) 

1240 
assume "accmodi old = Package" 

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

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

1243 
by (auto simp add: inheritable_in_def) 

1244 
next 

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

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

1249 
with accmodi_new wf 

1250 
have "accmodi inter = Package" 

1251 
by (auto intro: overrides_Package_old) 

1252 
with Indirect 

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

1254 
by auto 

1255 
qed 

1256 
qed 

1257 

1258 
lemma dyn_override_Package_escape: 

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

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

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

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

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

1266 
proof  

1267 
from dyn_override accmodi_old outside_pack 

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

1269 
proof (induct rule: overridesR.induct) 

1270 
case (Direct new old) 

1271 
assume accmodi_old: "accmodi old = Package" 

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

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

1274 
with accmodi_old 

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

1276 
by (simp add: inheritable_in_def) 

1277 
with outside_pack 

1278 
show "?P new old" 

1279 
by (contradiction) 

1280 
next 

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

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

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

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

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

1288 
\<Longrightarrow> ?P new inter" 

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

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

1291 
\<Longrightarrow> ?P inter old" 

1292 
show "?P new old" 

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

1294 
case True 

1295 
note same_pack_old_inter = this 

1296 
show ?thesis 

1297 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1334 
qed 
12854  1335 
qed 
1336 
next 

1337 
case False 

1338 
with accmodi_old hyp_inter_old 

1339 
obtain newinter where 

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

1340 
over_inter_newinter: "G \<turnstile> inter overrides newinter" and 
12854  1341 
over_newinter_old: "G \<turnstile> newinter overrides old" and 
1342 
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

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

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

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

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

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

1350 
by blast 
12854  1351 
qed 
1352 
qed 

1353 
qed 

1354 

45605  1355 
lemmas class_rec_induct' = class_rec.induct [of "%x y z w. P x y"] for P 
35440  1356 

12854  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") 

35440  1361 
proof (induct G C rule: class_rec_induct', intro allI impI) 
12854  1362 
fix G C c m 
35440  1363 
assume Hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object 
1364 
\<Longrightarrow> ?P G (super c)" 

12854  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 