author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42463  f270e3e18be5 
child 58263  6c907aad90ba 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/WellType.thy 
2 
Author: David von Oheimb 

3 
Copyright 1999 Technische Universitaet Muenchen 

11070  4 
*) 
8011  5 

12911  6 
header {* \isaheader{Welltypedness Constraints} *} 
8011  7 

16417  8 
theory WellType imports Term WellForm begin 
11070  9 

10 
text {* 

8011  11 
the formulation of welltypedness of method calls given below (as well as 
12 
the Java Specification 1.0) is a little too restrictive: Is does not allow 

13 
methods of class Object to be called upon references of interface type. 

14 

11070  15 
\begin{description} 
16 
\item[simplifications:]\ \\ 

17 
\begin{itemize} 

18 
\item the type rules include all static checks on expressions and statements, 

19 
e.g.\ definedness of names (of parameters, locals, fields, methods) 

20 
\end{itemize} 

21 
\end{description} 

22 
*} 

12517  23 

24 
text "local variables, including method parameters and This:" 

42463  25 
type_synonym lenv = "vname \<rightharpoonup> ty" 
26 
type_synonym 'c env = "'c prog \<times> lenv" 

8011  27 

35102  28 
abbreviation (input) 
29 
prg :: "'c env => 'c prog" 

30 
where "prg == fst" 

8011  31 

35102  32 
abbreviation (input) 
33 
localT :: "'c env => (vname \<rightharpoonup> ty)" 

34 
where "localT == snd" 

8011  35 

36 
consts 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

37 
more_spec :: "'c prog => (ty \<times> 'x) \<times> ty list => 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

38 
(ty \<times> 'x) \<times> ty list => bool" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

39 
appl_methds :: "'c prog => cname => sig => ((ty \<times> ty) \<times> ty list) set" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

40 
max_spec :: "'c prog => cname => sig => ((ty \<times> ty) \<times> ty list) set" 
8011  41 

42 
defs 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

43 
more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and> 
12517  44 
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'" 
8011  45 

12517  46 
 "applicable methods, cf. 15.11.2.1" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

47 
appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs). 
12517  48 
{((Class md,rT),pTs') md rT mb pTs'. 
49 
method (G,C) (mn, pTs') = Some (md,rT,mb) \<and> 

50 
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'}" 

8011  51 

12517  52 
 "maximally specific methods, cf. 15.11.2.2" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

53 
max_spec_def: "max_spec G C sig == {m. m \<in>appl_methds G C sig \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

54 
(\<forall>m'\<in>appl_methds G C sig. 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

55 
more_spec G m' m > m' = m)}" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

56 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

57 
lemma max_spec2appl_meths: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

58 
"x \<in> max_spec G C sig ==> x \<in> appl_methds G C sig" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

59 
apply (unfold max_spec_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

60 
apply (fast) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

61 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

62 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

63 
lemma appl_methsD: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

64 
"((md,rT),pTs')\<in>appl_methds G C (mn, pTs) ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

65 
\<exists>D b. md = Class D \<and> method (G,C) (mn, pTs') = Some (D,rT,b) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

66 
\<and> list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

67 
apply (unfold appl_methds_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

68 
apply (fast) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

69 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

70 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

71 
lemmas max_spec2mheads = insertI1 [THEN [2] equalityD2 [THEN subsetD], 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

72 
THEN max_spec2appl_meths, THEN appl_methsD] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

73 

10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

74 

39758  75 
primrec typeof :: "(loc => ty option) => val => ty option" 
76 
where 

12517  77 
"typeof dt Unit = Some (PrimT Void)" 
39758  78 
 "typeof dt Null = Some NT" 
79 
 "typeof dt (Bool b) = Some (PrimT Boolean)" 

80 
 "typeof dt (Intg i) = Some (PrimT Integer)" 

81 
 "typeof dt (Addr a) = dt a" 

8011  82 

12517  83 
lemma is_type_typeof [rule_format (no_asm), simp]: 
84 
"(\<forall>a. v \<noteq> Addr a) > (\<exists>T. typeof t v = Some T \<and> is_type G T)" 

11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

85 
apply (rule val.induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

86 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

87 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

88 

a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

89 
lemma typeof_empty_is_type [rule_format (no_asm)]: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

90 
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

91 
apply (rule val.induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

92 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

93 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

94 

13672  95 
lemma typeof_default_val: "\<exists>T. (typeof dt (default_val ty) = Some T) \<and> G\<turnstile> T \<preceq> ty" 
96 
apply (case_tac ty) 

97 
apply (case_tac prim_ty) 

98 
apply auto 

99 
done 

100 

42463  101 
type_synonym 
12517  102 
java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr" 
103 
 "method body with parameter names, local variables, block, result expression." 

104 
 "local variables might include This, which is hidden anyway" 

8011  105 

23757  106 
inductive 
22271  107 
ty_expr :: "'c env => expr => ty => bool" ("_ \<turnstile> _ :: _" [51, 51, 51] 50) 
108 
and ty_exprs :: "'c env => expr list => ty list => bool" ("_ \<turnstile> _ [::] _" [51, 51, 51] 50) 

109 
and wt_stmt :: "'c env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51, 51] 50) 

110 
where 

12517  111 

112 
NewC: "[ is_class (prg E) C ] ==> 

113 
E\<turnstile>NewC C::Class C"  "cf. 15.8" 

8011  114 

12517  115 
 "cf. 15.15" 
22271  116 
 Cast: "[ E\<turnstile>e::C; is_class (prg E) D; 
14045  117 
prg E\<turnstile>C\<preceq>? Class D ] ==> 
118 
E\<turnstile>Cast D e:: Class D" 

8011  119 

12517  120 
 "cf. 15.7.1" 
22271  121 
 Lit: "[ typeof (\<lambda>v. None) x = Some T ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

122 
E\<turnstile>Lit x::T" 
8011  123 

9240  124 

12517  125 
 "cf. 15.13.1" 
22271  126 
 LAcc: "[ localT E v = Some T; is_type (prg E) T ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

127 
E\<turnstile>LAcc v::T" 
9240  128 

22271  129 
 BinOp:"[ E\<turnstile>e1::T; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

130 
E\<turnstile>e2::T; 
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

131 
if bop = Eq then T' = PrimT Boolean 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

132 
else T' = T \<and> T = PrimT Integer] ==> 
11645
09a1876e739b
 declared wf_java_prog as syntax (previously: definition)
streckem
parents:
11372
diff
changeset

133 
E\<turnstile>BinOp bop e1 e2::T'" 
9240  134 

12517  135 
 "cf. 15.25, 15.25.1" 
22271  136 
 LAss: "[ v ~= This; 
11645
09a1876e739b
 declared wf_java_prog as syntax (previously: definition)
streckem
parents:
11372
diff
changeset

137 
E\<turnstile>LAcc v::T; 
13672  138 
E\<turnstile>e::T'; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

139 
prg E\<turnstile>T'\<preceq>T ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

140 
E\<turnstile>v::=e::T'" 
8011  141 

12517  142 
 "cf. 15.10.1" 
22271  143 
 FAcc: "[ E\<turnstile>a::Class C; 
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

144 
field (prg E,C) fn = Some (fd,fT) ] ==> 
11645
09a1876e739b
 declared wf_java_prog as syntax (previously: definition)
streckem
parents:
11372
diff
changeset

145 
E\<turnstile>{fd}a..fn::fT" 
8011  146 

12517  147 
 "cf. 15.25, 15.25.1" 
22271  148 
 FAss: "[ E\<turnstile>{fd}a..fn::T; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

149 
E\<turnstile>v ::T'; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

150 
prg E\<turnstile>T'\<preceq>T ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

151 
E\<turnstile>{fd}a..fn:=v::T'" 
8011  152 

153 

12517  154 
 "cf. 15.11.1, 15.11.2, 15.11.3" 
22271  155 
 Call: "[ E\<turnstile>a::Class C; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

156 
E\<turnstile>ps[::]pTs; 
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

157 
max_spec (prg E) C (mn, pTs) = {((md,rT),pTs')} ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

158 
E\<turnstile>{C}a..mn({pTs'}ps)::rT" 
8011  159 

12517  160 
 "welltyped expression lists" 
8011  161 

12517  162 
 "cf. 15.11.???" 
22271  163 
 Nil: "E\<turnstile>[][::][]" 
8011  164 

12517  165 
 "cf. 15.11.???" 
22271  166 
 Cons:"[ E\<turnstile>e::T; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

167 
E\<turnstile>es[::]Ts ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

168 
E\<turnstile>e#es[::]T#Ts" 
8011  169 

12517  170 
 "welltyped statements" 
8011  171 

22271  172 
 Skip:"E\<turnstile>Skip\<surd>" 
8011  173 

22271  174 
 Expr:"[ E\<turnstile>e::T ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

175 
E\<turnstile>Expr e\<surd>" 
8011  176 

22271  177 
 Comp:"[ E\<turnstile>s1\<surd>; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

178 
E\<turnstile>s2\<surd> ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

179 
E\<turnstile>s1;; s2\<surd>" 
8011  180 

12517  181 
 "cf. 14.8" 
22271  182 
 Cond:"[ E\<turnstile>e::PrimT Boolean; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

183 
E\<turnstile>s1\<surd>; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

184 
E\<turnstile>s2\<surd> ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

185 
E\<turnstile>If(e) s1 Else s2\<surd>" 
8011  186 

12517  187 
 "cf. 14.10" 
22271  188 
 Loop:"[ E\<turnstile>e::PrimT Boolean; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

189 
E\<turnstile>s\<surd> ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

190 
E\<turnstile>While(e) s\<surd>" 
8011  191 

13672  192 

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

193 
definition wf_java_mdecl :: "'c prog => cname => java_mb mdecl => bool" where 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

194 
"wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)). 
12517  195 
length pTs = length pns \<and> 
12888  196 
distinct pns \<and> 
12517  197 
unique lvars \<and> 
11645
09a1876e739b
 declared wf_java_prog as syntax (previously: definition)
streckem
parents:
11372
diff
changeset

198 
This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> 
12517  199 
(\<forall>pn\<in>set pns. map_of lvars pn = None) \<and> 
200 
(\<forall>(vn,T)\<in>set lvars. is_type G T) & 

201 
(let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in 

202 
E\<turnstile>blk\<surd> \<and> (\<exists>T. E\<turnstile>res::T \<and> G\<turnstile>T\<preceq>rT))" 

8011  203 

35102  204 
abbreviation "wf_java_prog == wf_prog wf_java_mdecl" 
8011  205 

13672  206 
lemma wf_java_prog_wf_java_mdecl: "\<lbrakk> 
207 
wf_java_prog G; (C, D, fds, mths) \<in> set G; jmdcl \<in> set mths \<rbrakk> 

208 
\<Longrightarrow> wf_java_mdecl G C jmdcl" 

14045  209 
apply (simp only: wf_prog_def) 
13672  210 
apply (erule conjE)+ 
211 
apply (drule bspec, assumption) 

14045  212 
apply (simp add: wf_cdecl_mdecl_def split_beta) 
13672  213 
done 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

214 

14045  215 

216 
lemma wt_is_type: "(E\<turnstile>e::T \<longrightarrow> ws_prog (prg E) \<longrightarrow> is_type (prg E) T) \<and> 

217 
(E\<turnstile>es[::]Ts \<longrightarrow> ws_prog (prg E) \<longrightarrow> Ball (set Ts) (is_type (prg E))) \<and> 

13672  218 
(E\<turnstile>c \<surd> \<longrightarrow> True)" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

219 
apply (rule ty_expr_ty_exprs_wt_stmt.induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

220 
apply auto 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

221 
apply ( erule typeof_empty_is_type) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

222 
apply ( simp split add: split_if_asm) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

223 
apply ( drule field_fields) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

224 
apply ( drule (1) fields_is_type) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

225 
apply ( simp (no_asm_simp)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

226 
apply (assumption) 
14045  227 
apply (auto dest!: max_spec2mheads method_wf_mhead is_type_rTI 
12517  228 
simp add: wf_mdecl_def) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

229 
done 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

230 

13672  231 
lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, rule_format] 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

232 

14045  233 
lemma expr_class_is_class: " 
234 
\<lbrakk>ws_prog (prg E); E \<turnstile> e :: Class C\<rbrakk> \<Longrightarrow> is_class (prg E) C" 

235 
by (frule ty_expr_is_type, assumption, simp) 

236 

237 

8011  238 
end 