author  oheimb 
Mon, 05 Feb 2001 20:14:15 +0100  
changeset 11070  cc421547e744 
parent 11026  a50365d21144 
child 11372  648795477bb5 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/WellType.thy 
2 
ID: $Id$ 

3 
Author: David von Oheimb 

4 
Copyright 1999 Technische Universitaet Muenchen 

11070  5 
*) 
8011  6 

11070  7 
header "Welltypedness Constraints" 
8011  8 

11070  9 
theory WellType = Term + WellForm: 
10 

11 
text {* 

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

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

15 

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

18 
\begin{itemize} 

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

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

21 
\end{itemize} 

22 
\end{description} 

23 
*} 

8011  24 
types lenv (* local variables, including method parameters and This *) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

25 
= "vname \<leadsto> ty" 
8011  26 
'c env 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

27 
= "'c prog \<times> lenv" 
8011  28 

29 
syntax 

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

30 
prg :: "'c env => 'c prog" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

31 
localT :: "'c env => (vname \<leadsto> ty)" 
8011  32 

33 
translations 

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

34 
"prg" => "fst" 
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

35 
"localT" => "snd" 
8011  36 

37 
consts 

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

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

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

40 
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

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

43 
defs 

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

44 
more_spec_def: "more_spec G == \<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>d\<preceq>d' \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

45 
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'" 
8011  46 

47 
(* applicable methods, cf. 15.11.2.1 *) 

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

48 
appl_methds_def: "appl_methds G C == \<lambda>(mn, pTs). 
8105
2dda3e88d23f
simplified definition of appl_methds, removing m_head
oheimb
parents:
8085
diff
changeset

49 
{((Class md,rT),pTs') md rT mb pTs'. 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

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

53 
(* maximally specific methods, cf. 15.11.2.2 *) 

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

54 
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

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

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

57 

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

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

59 
"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

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

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

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

63 

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

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

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

66 
\<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

67 
\<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

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

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

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

71 

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

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

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

74 

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

75 

8011  76 
consts 
10042  77 
typeof :: "(loc => ty option) => val => ty option" 
8011  78 

79 
primrec 

80 
"typeof dt Unit = Some (PrimT Void)" 

81 
"typeof dt Null = Some NT" 

82 
"typeof dt (Bool b) = Some (PrimT Boolean)" 

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

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

85 

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

86 
lemma is_type_typeof [rule_format (no_asm), simp]: "(\<forall>a. v \<noteq> Addr a) > (\<exists>T. typeof t v = Some T \<and> is_type G T)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

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

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

90 

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

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

92 
"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

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

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

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

96 

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

98 
java_mb = "vname list \<times> (vname \<times> ty) list \<times> stmt \<times> expr" 
8011  99 
(* method body with parameter names, local variables, block, result expression *) 
100 

101 
consts 

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

102 
ty_expr :: "java_mb env => (expr \<times> ty ) set" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

103 
ty_exprs:: "java_mb env => (expr list \<times> ty list) set" 
10042  104 
wt_stmt :: "java_mb env => stmt set" 
8011  105 

106 
syntax 

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

107 
ty_expr :: "java_mb env => [expr , ty ] => bool" ("_ \<turnstile> _ :: _" [51,51,51]50) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

108 
ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_ \<turnstile> _ [::] _" [51,51,51]50) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

109 
wt_stmt :: "java_mb env => stmt => bool" ("_ \<turnstile> _ \<surd>" [51,51 ]50) 
8011  110 

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

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

112 
ty_expr :: "java_mb env => [expr , ty ] => bool" ("_  _ :: _" [51,51,51]50) 
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

113 
ty_exprs:: "java_mb env => [expr list, ty list] => bool" ("_  _ [::] _" [51,51,51]50) 
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

114 
wt_stmt :: "java_mb env => stmt => bool" ("_  _ [ok]" [51,51 ]50) 
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

115 

8011  116 

117 
translations 

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

118 
"E\<turnstile>e :: T" == "(e,T) \<in> ty_expr E" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

119 
"E\<turnstile>e[::]T" == "(e,T) \<in> ty_exprs E" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

120 
"E\<turnstile>c \<surd>" == "c \<in> wt_stmt E" 
8011  121 

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

122 
inductive "ty_expr E" "ty_exprs E" "wt_stmt E" intros 
8011  123 

124 
(* welltyped expressions *) 

125 

126 
(* cf. 15.8 *) 

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

127 
NewC: "[ is_class (prg E) C ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

128 
E\<turnstile>NewC C::Class C" 
8011  129 

130 
(* cf. 15.15 *) 

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

131 
Cast: "[ E\<turnstile>e::Class C; is_class (prg E) D; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

132 
prg E\<turnstile>C\<preceq>? D ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

133 
E\<turnstile>Cast D e::Class D" 
8011  134 

135 
(* cf. 15.7.1 *) 

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

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

137 
E\<turnstile>Lit x::T" 
8011  138 

9240  139 

8011  140 
(* cf. 15.13.1 *) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

141 
LAcc: "[ localT E v = Some T; is_type (prg E) T ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

142 
E\<turnstile>LAcc v::T" 
9240  143 

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

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

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

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

147 
else T' = T \<and> T = PrimT Integer] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

148 
E\<turnstile>BinOp bop e1 e2::T'" 
9240  149 

8011  150 
(* cf. 15.25, 15.25.1 *) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

151 
LAss: "[ E\<turnstile>LAcc v::T; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

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

154 
E\<turnstile>v::=e::T'" 
8011  155 

156 
(* cf. 15.10.1 *) 

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

157 
FAcc: "[ E\<turnstile>a::Class C; 
10061
fe82134773dc
added HTML syntax; added spaces in normal syntax for better documents
kleing
parents:
10042
diff
changeset

158 
field (prg E,C) fn = Some (fd,fT) ] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

159 
E\<turnstile>{fd}a..fn::fT" 
8011  160 

161 
(* cf. 15.25, 15.25.1 *) 

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

162 
FAss: "[ E\<turnstile>{fd}a..fn::T; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

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

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

167 

168 
(* cf. 15.11.1, 15.11.2, 15.11.3 *) 

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

169 
Call: "[ E\<turnstile>a::Class C; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

171 
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

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

174 
(* welltyped expression lists *) 

175 

176 
(* cf. 15.11.??? *) 

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

177 
Nil: "E\<turnstile>[][::][]" 
8011  178 

179 
(* cf. 15.11.??? *) 

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

180 
Cons:"[ E\<turnstile>e::T; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

182 
E\<turnstile>e#es[::]T#Ts" 
8011  183 

184 
(* welltyped statements *) 

185 

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

186 
Skip:"E\<turnstile>Skip\<surd>" 
8011  187 

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

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

189 
E\<turnstile>Expr e\<surd>" 
8011  190 

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

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

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

193 
E\<turnstile>s1;; s2\<surd>" 
8011  194 

195 
(* cf. 14.8 *) 

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

196 
Cond:"[ E\<turnstile>e::PrimT Boolean; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

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

199 
E\<turnstile>If(e) s1 Else s2\<surd>" 
8011  200 

201 
(* cf. 14.10 *) 

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

202 
Loop:"[ E\<turnstile>e::PrimT Boolean; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

204 
E\<turnstile>While(e) s\<surd>" 
8011  205 

206 
constdefs 

207 

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

208 
wf_java_mdecl :: "java_mb prog => cname => java_mb mdecl => bool" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

209 
"wf_java_mdecl G C == \<lambda>((mn,pTs),rT,(pns,lvars,blk,res)). 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

210 
length pTs = length pns \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

211 
nodups pns \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

212 
unique lvars \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

213 
(\<forall>pn\<in>set pns. map_of lvars pn = None) \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

214 
(\<forall>(vn,T)\<in>set lvars. is_type G T) & 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

215 
(let E = (G,map_of lvars(pns[\<mapsto>]pTs)(This\<mapsto>Class C)) in 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

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

218 
wf_java_prog :: "java_mb prog => bool" 
10042  219 
"wf_java_prog G == wf_prog wf_java_mdecl G" 
8011  220 

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

221 

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

222 
lemma wt_is_type: "wf_prog wf_mb G \<Longrightarrow> ((G,L)\<turnstile>e::T \<longrightarrow> is_type G T) \<and> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

223 
((G,L)\<turnstile>es[::]Ts \<longrightarrow> Ball (set Ts) (is_type G)) \<and> ((G,L)\<turnstile>c \<surd> \<longrightarrow> True)" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

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

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

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

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

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

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

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

232 
apply (auto dest!: max_spec2mheads method_wf_mdecl is_type_rTI simp add: wf_mdecl_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

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

234 

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

235 
lemmas ty_expr_is_type = wt_is_type [THEN conjunct1,THEN mp, COMP swap_prems_rl] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
10763
diff
changeset

236 

8011  237 
end 