author  wenzelm 
Thu, 28 Feb 2013 13:24:51 +0100  
changeset 51304  0e71a248cacb 
parent 45133  2214ba5bdfff 
child 51686  532e0ac5a66d 
permissions  rwrr 
8011  1 
(* Title: HOL/MicroJava/J/JTypeSafe.thy 
41589  2 
Author: David von Oheimb, Technische Universitaet Muenchen 
11070  3 
*) 
8011  4 

12911  5 
header {* \isaheader{Type Safety Proof} *} 
8011  6 

16417  7 
theory JTypeSafe imports Eval Conform begin 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

8 

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

9 
declare split_beta [simp] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

10 

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

11 
lemma NewC_conforms: 
13672  12 
"[h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C] ==> 
13 
(x,(h(a\<mapsto>(C,(init_vars (fields (G,C))))), l))::\<preceq>(G, lT)" 

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

14 
apply( erule conforms_upd_obj) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

15 
apply( unfold oconf_def) 
14045  16 
apply( auto dest!: fields_is_type simp add: wf_prog_ws_prog) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

17 
done 
14045  18 

19 

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

20 
lemma Cast_conf: 
14045  21 
"[ wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>CC; G\<turnstile>CC \<preceq>? Class D; cast_ok G D h v] 
22 
==> G,h\<turnstile>v::\<preceq>Class D" 

23 
apply (case_tac "CC") 

24 
apply simp 

25 
apply (case_tac "ref_ty") 

26 
apply (clarsimp simp add: conf_def) 

27 
apply simp 

23757  28 
apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp) 
14045  29 
apply (rule conf_widen, assumption+) apply (erule widen.subcls) 
30 

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

31 
apply (unfold cast_ok_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

32 
apply( case_tac "v = Null") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

33 
apply( simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

34 
apply( clarify) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

35 
apply( drule (1) non_npD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

36 
apply( auto intro!: conf_AddrI simp add: obj_ty_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

38 

13672  39 

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

40 
lemma FAcc_type_sound: 
13672  41 
"[ wf_prog wf_mb G; field (G,C) fn = Some (fd, ft); (x,(h,l))::\<preceq>(G,lT); 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

42 
x' = None > G,h\<turnstile>a'::\<preceq> Class C; np a' x' = None ] ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

43 
G,h\<turnstile>the (snd (the (h (the_Addr a'))) (fn, fd))::\<preceq>ft" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

44 
apply( drule np_NoneD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

45 
apply( erule conjE) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

46 
apply( erule (1) notE impE) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

47 
apply( drule non_np_objD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

49 
apply( drule conforms_heapD [THEN hconfD]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

50 
apply( assumption) 
14045  51 
apply (frule wf_prog_ws_prog) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

52 
apply( drule (2) widen_cfs_fields) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

53 
apply( drule (1) oconf_objD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

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

56 

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

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

58 
"[ wf_prog wf_mb G; a = the_Addr a'; (c, fs) = the (h a); 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

59 
(G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

60 
(G, lT)\<turnstile>aa::Class C; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

61 
field (G,C) fn = Some (fd, ft); h''\<le>h'; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

62 
x' = None > G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>h; 
13672  63 
Norm (h, l)::\<preceq>(G, lT); G,h\<turnstile>x::\<preceq>T'; np a' x' = None] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

64 
h''\<le>h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and> 
13672  65 
Norm(h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))), l)::\<preceq>(G, lT) \<and> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

66 
G,h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x))))\<turnstile>x::\<preceq>T'" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

67 
apply( drule np_NoneD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

68 
apply( erule conjE) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

70 
apply( drule non_np_objD) 
12951  71 
apply( assumption) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

72 
apply( clarify) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

73 
apply( simp (no_asm_use)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

74 
apply( frule (1) hext_objD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

75 
apply( erule exE) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

76 
apply( simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

77 
apply( clarify) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

78 
apply( rule conjI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

79 
apply( fast elim: hext_trans hext_upd_obj) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

80 
apply( rule conjI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

81 
prefer 2 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

82 
apply( fast elim: conf_upd_obj [THEN iffD2]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

83 

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

84 
apply( rule conforms_upd_obj) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

86 
apply( rule_tac [2] hextI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

87 
prefer 2 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

88 
apply( force) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

89 
apply( rule oconf_hext) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

90 
apply( erule_tac [2] hext_upd_obj) 
14045  91 
apply (frule wf_prog_ws_prog) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

92 
apply( drule (2) widen_cfs_fields) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

93 
apply( rule oconf_obj [THEN iffD2]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

94 
apply( simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

95 
apply( intro strip) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

96 
apply( case_tac "(aaa, b) = (fn, fd)") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

97 
apply( simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

98 
apply( fast intro: conf_widen) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

99 
apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

101 

13672  102 

103 

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

104 
lemma Call_lemma2: "[ wf_prog wf_mb G; list_all2 (conf G h) pvs pTs; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

105 
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; 
12888  106 
length pTs' = length pns; distinct pns; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

107 
Ball (set lvars) (split (\<lambda>vn. is_type G)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

108 
] ==> G,h\<turnstile>init_vars lvars(pns[\<mapsto>]pvs)[::\<preceq>]map_of lvars(pns[\<mapsto>]pTs')" 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

109 
apply (unfold wf_mhead_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

110 
apply( clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

111 
apply( rule lconf_ext_list) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

112 
apply( rule Ball_set_table [THEN lconf_init_vars]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

113 
apply( force) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

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

116 
apply( erule (2) conf_list_gext_widen) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

118 

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

119 
lemma Call_type_sound: 
13672  120 
"[ wf_java_prog G; a' \<noteq> Null; Norm (h, l)::\<preceq>(G, lT); class G C = Some y; 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

121 
max_spec G C (mn,pTsa) = {((mda,rTa),pTs')}; xc\<le>xh; xh\<le>h; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

122 
list_all2 (conf G h) pvs pTsa; 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

123 
(md, rT, pns, lvars, blk, res) = 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

124 
the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); 
13672  125 
\<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) > 
126 
(G, lT)\<turnstile>blk\<surd> > h\<le>xi \<and> (xcptb, xi, xl)::\<preceq>(G, lT); 

127 
\<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) > (\<forall>T. (G, lT)\<turnstile>res::T > 

128 
xi\<le>h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None > G,h'\<turnstile>v::\<preceq>T)); 

129 
G,xh\<turnstile>a'::\<preceq> Class C 

130 
] ==> 

131 
xc\<le>h' \<and> (x',(h', l))::\<preceq>(G, lT) \<and> (x' = None > G,h'\<turnstile>v::\<preceq>rTa)" 

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

132 
apply( drule max_spec2mheads) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

133 
apply( clarify) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

134 
apply( drule (2) non_np_objD') 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

135 
apply( clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

136 
apply( frule (1) hext_objD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

137 
apply( clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

138 
apply( drule (3) Call_lemma) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

139 
apply( clarsimp simp add: wf_java_mdecl_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

140 
apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl) 
13672  141 
apply( drule spec, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2") 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

142 
apply( rule conformsI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

143 
apply( erule conforms_heapD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

144 
apply( rule lconf_ext) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

145 
apply( force elim!: Call_lemma2) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

146 
apply( erule conf_hext, erule (1) conf_obj_AddrI) 
13672  147 
apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) 
148 
apply (simp add: conforms_def) 

149 

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

150 
apply( erule conjE) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

151 
apply( drule spec, erule (1) impE) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

152 
apply( drule spec, erule (1) impE) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

153 
apply( erule_tac V = "?E\<turnstile>res::?rT" in thin_rl) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

154 
apply( clarify) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

155 
apply( rule conjI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

156 
apply( fast intro: hext_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

157 
apply( rule conjI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

158 
apply( rule_tac [2] impI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

159 
apply( erule_tac [2] notE impE, tactic "assume_tac 2") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

160 
apply( frule_tac [2] conf_widen) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

161 
apply( tactic "assume_tac 4") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

162 
apply( tactic "assume_tac 2") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

163 
prefer 2 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

164 
apply( fast elim!: widen_trans) 
13672  165 
apply (rule conforms_xcpt_change) 
166 
apply( rule conforms_hext) apply assumption 

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

167 
apply( erule (1) hext_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

168 
apply( erule conforms_heapD) 
13672  169 
apply (simp add: conforms_def) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

171 

13672  172 

173 

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

174 
declare split_if [split del] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

175 
declare fun_upd_apply [simp del] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

176 
declare fun_upd_same [simp] 
14045  177 
declare wf_prog_ws_prog [simp] 
178 

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

179 
ML{* 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

180 
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac, 
12517  181 
(mp_tac ORELSE' (dtac spec THEN' mp_tac)), REPEAT o (etac conjE)])) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

182 
*} 
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23894
diff
changeset

183 

13672  184 

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

185 
theorem eval_evals_exec_type_sound: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

186 
"wf_java_prog G ==> 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

187 
(G\<turnstile>(x,(h,l)) e \<succ>v > (x', (h',l')) > 
13672  188 
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) > (\<forall>T . (G,lT)\<turnstile>e :: T > 
189 
h\<le>h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None > G,h'\<turnstile>v ::\<preceq> T )))) \<and> 

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

190 
(G\<turnstile>(x,(h,l)) es[\<succ>]vs> (x', (h',l')) > 
13672  191 
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) > (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts > 
192 
h\<le>h' \<and> (x',(h',l'))::\<preceq>(G,lT) \<and> (x'=None > list_all2 (\<lambda>v T. G,h'\<turnstile>v::\<preceq>T) vs Ts)))) \<and> 

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

193 
(G\<turnstile>(x,(h,l)) c > (x', (h',l')) > 
13672  194 
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) > (G,lT)\<turnstile>c \<surd> > 
195 
h\<le>h' \<and> (x',(h',l'))::\<preceq>(G,lT)))" 

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

196 
apply( rule eval_evals_exec_induct) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

197 
apply( unfold c_hupd_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

198 

12517  199 
 "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

200 
apply( simp_all) 
51304  201 
apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])") 
39159  202 
apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
32149
ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of  same for claset and clasimpset;
wenzelm
parents:
27215
diff
changeset

203 
THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *}) 
12517  204 
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

205 

12517  206 
 "Level 7" 
207 
 "15 NewC" 

13672  208 
apply (drule sym) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

209 
apply( drule new_AddrD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

210 
apply( erule disjE) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

211 
prefer 2 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

212 
apply( simp (no_asm_simp)) 
13672  213 
apply (rule conforms_xcpt_change, assumption) 
214 
apply (simp (no_asm_simp) add: xconf_def) 

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

215 
apply( clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

216 
apply( rule conjI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

217 
apply( force elim!: NewC_conforms) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

218 
apply( rule conf_obj_AddrI) 
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
32367
diff
changeset

219 
apply( rule_tac [2] rtrancl.rtrancl_refl) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

220 
apply( simp (no_asm)) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

221 

12517  222 
 "for Cast" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

223 
defer 1 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

224 

12517  225 
 "14 Lit" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

227 

12517  228 
 "13 BinOp" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

229 
apply (tactic "forward_hyp_tac") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

230 
apply (tactic "forward_hyp_tac") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

231 
apply( rule conjI, erule (1) hext_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

232 
apply( erule conjI) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

233 
apply( clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

234 
apply( drule eval_no_xcpt) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

235 
apply( simp split add: binop.split) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

236 

12517  237 
 "12 LAcc" 
13672  238 
apply simp 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

239 
apply( fast elim: conforms_localD [THEN lconfD]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

240 

12517  241 
 "for FAss" 
39159  242 
apply( tactic {* EVERY'[eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23757
diff
changeset

243 
THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*}) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

244 

12517  245 
 "for if" 
45133  246 
apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" THEN_ALL_NEW 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23757
diff
changeset

247 
(asm_full_simp_tac @{simpset})) 7*}) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

248 

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

249 
apply (tactic "forward_hyp_tac") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

250 

12517  251 
 "11+1 if" 
22271  252 
prefer 7 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

253 
apply( fast intro: hext_trans) 
22271  254 
prefer 7 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

255 
apply( fast intro: hext_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

256 

12517  257 
 "10 Expr" 
22271  258 
prefer 6 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

260 

12517  261 
 "9 ???" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

262 
apply( simp_all) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

263 

12517  264 
 "8 Cast" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

265 
prefer 8 
13672  266 
apply (rule conjI) 
267 
apply (fast intro: conforms_xcpt_change xconf_raise_if) 

268 

269 
apply clarify 

270 
apply (drule raise_if_NoneD) 

271 
apply (clarsimp) 

272 
apply (rule Cast_conf) 

273 
apply assumption+ 

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

274 

14045  275 

12517  276 
 "7 LAss" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

277 
apply (fold fun_upd_def) 
39159  278 
apply( tactic {* (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23757
diff
changeset

279 
THEN_ALL_NEW (full_simp_tac @{simpset})) 1 *}) 
13672  280 
apply (intro strip) 
281 
apply (case_tac E) 

282 
apply (simp) 

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

283 
apply( blast intro: conforms_upd_local conf_widen) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

284 

12517  285 
 "6 FAcc" 
13672  286 
apply (rule conjI) 
287 
apply (simp add: np_def) 

288 
apply (fast intro: conforms_xcpt_change xconf_raise_if) 

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

289 
apply( fast elim!: FAcc_type_sound) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

290 

12517  291 
 "5 While" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

292 
prefer 5 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

293 
apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

294 
apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

295 
apply(force elim: hext_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

296 

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

297 
apply (tactic "forward_hyp_tac") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

298 

13672  299 
 "4 Cond" 
300 
prefer 4 

301 
apply (case_tac "the_Bool v") 

302 
apply simp 

303 
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) 

304 
apply simp 

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

305 
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

306 

12517  307 
 "3 ;;" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

308 
prefer 3 
13672  309 
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) 
310 

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

311 

12517  312 
 "2 FAss" 
22271  313 
apply (subgoal_tac "(np a' x1, aa, ba) ::\<preceq> (G, lT)") 
13672  314 
prefer 2 
315 
apply (simp add: np_def) 

316 
apply (fast intro: conforms_xcpt_change xconf_raise_if) 

317 
apply( case_tac "x2") 

318 
 "x2 = None" 

319 
apply (simp) 

320 
apply (tactic forward_hyp_tac, clarify) 

321 
apply( drule eval_no_xcpt) 

322 
apply( erule FAss_type_sound, rule HOL.refl, assumption+) 

323 
 "x2 = Some a" 

324 
apply ( simp (no_asm_simp)) 

325 
apply( fast intro: hext_trans) 

326 

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

327 

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

328 
apply( tactic prune_params_tac) 
12517  329 
 "Level 52" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

330 

12517  331 
 "1 Call" 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

332 
apply( case_tac "x") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

333 
prefer 2 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

334 
apply( clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

335 
apply( drule exec_xcpt) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

336 
apply( simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

337 
apply( drule_tac eval_xcpt) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

338 
apply( simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

339 
apply( fast elim: hext_trans) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

340 
apply( clarify) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

341 
apply( drule evals_no_xcpt) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

342 
apply( simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

343 
apply( case_tac "a' = Null") 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

344 
apply( simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

345 
apply( drule exec_xcpt) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

346 
apply( simp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

347 
apply( drule eval_xcpt) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

348 
apply( simp) 
13672  349 
apply (rule conjI) 
350 
apply( fast elim: hext_trans) 

14045  351 
apply (rule conforms_xcpt_change, assumption) 
352 
apply (simp (no_asm_simp) add: xconf_def) 

13672  353 
apply(clarsimp) 
354 

355 
apply( drule ty_expr_is_type, simp) 

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

356 
apply(clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

357 
apply(unfold is_class_def) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

358 
apply(clarsimp) 
13672  359 

11644
3dfde687f0d7
Removed some unfoldings of defs after declaring wf_java_prog as syntax
streckem
parents:
11070
diff
changeset

360 
apply(rule Call_type_sound); 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

361 
prefer 11 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

362 
apply blast 
11644
3dfde687f0d7
Removed some unfoldings of defs after declaring wf_java_prog as syntax
streckem
parents:
11070
diff
changeset

363 
apply (simp (no_asm_simp))+ 
13672  364 

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

365 
done 
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23894
diff
changeset

366 

14142  367 

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

368 
lemma eval_type_sound: "!!E s s'. 
14142  369 
[ wf_java_prog G; G\<turnstile>(x,s) e\<succ>v > (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E ] 
370 
==> (x',s')::\<preceq>E \<and> (x'=None > G,heap s'\<turnstile>v::\<preceq>T) \<and> heap s \<le> heap s'" 

371 
apply (simp (no_asm_simp) only: split_tupled_all) 

372 
apply (drule eval_evals_exec_type_sound [THEN conjunct1, THEN mp, THEN spec, THEN mp]) 

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

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

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

375 

14142  376 

14045  377 
lemma evals_type_sound: "!!E s s'. 
14142  378 
[ wf_java_prog G; G\<turnstile>(x,s) es[\<succ>]vs > (x',s'); (x,s)::\<preceq>E; E\<turnstile>es[::]Ts; G=prg E ] 
379 
==> (x',s')::\<preceq>E \<and> (x'=None > (list_all2 (\<lambda>v T. G,heap s'\<turnstile>v::\<preceq>T) vs Ts)) \<and> heap s \<le> heap s'" 

380 
apply (simp (no_asm_simp) only: split_tupled_all) 

381 
apply (drule eval_evals_exec_type_sound [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp]) 

14045  382 
apply auto 
383 
done 

384 

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

385 
lemma exec_type_sound: "!!E s s'. 
14142  386 
\<lbrakk> wf_java_prog G; G\<turnstile>(x,s) s0> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd>; G=prg E \<rbrakk> 
387 
\<Longrightarrow> (x',s')::\<preceq>E \<and> heap s \<le> heap s'" 

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

388 
apply( simp (no_asm_simp) only: split_tupled_all) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

389 
apply (drule eval_evals_exec_type_sound 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

390 
[THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp]) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

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

393 

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

394 
theorem all_methods_understood: 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

395 
"[G=prg E; wf_java_prog G; G\<turnstile>(x,s) e\<succ>a'> Norm s'; a' \<noteq> Null; 
13672  396 
(x,s)::\<preceq>E; E\<turnstile>e::Class C; method (G,C) sig \<noteq> None] ==> 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

397 
method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None" 
14142  398 
apply (frule eval_type_sound, assumption+) 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

399 
apply(clarsimp) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

400 
apply( frule widen_methd) 
14142  401 
apply assumption 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

402 
prefer 2 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

404 
apply( drule non_npD) 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

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

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

407 

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

408 
declare split_beta [simp del] 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

409 
declare fun_upd_apply [simp] 
14045  410 
declare wf_prog_ws_prog [simp del] 
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

411 

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

412 
end 
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset

413 