author | paulson |
Thu, 13 Aug 2009 17:19:42 +0100 | |
changeset 32367 | a508148f7c25 |
parent 32149 | ef59550a55d3 |
child 33954 | 1bc3b688548c |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/J/JTypeSafe.thy |
2 |
ID: $Id$ |
|
3 |
Author: David von Oheimb |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
11070 | 5 |
*) |
8011 | 6 |
|
12911 | 7 |
header {* \isaheader{Type Safety Proof} *} |
8011 | 8 |
|
16417 | 9 |
theory JTypeSafe imports Eval Conform begin |
11026
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 |
declare split_beta [simp] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
12 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
13 |
lemma NewC_conforms: |
13672 | 14 |
"[|h a = None; (x,(h, l))::\<preceq>(G, lT); wf_prog wf_mb G; is_class G C|] ==> |
15 |
(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
|
16 |
apply( erule conforms_upd_obj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
17 |
apply( unfold oconf_def) |
14045 | 18 |
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
|
19 |
done |
14045 | 20 |
|
21 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
22 |
lemma Cast_conf: |
14045 | 23 |
"[| wf_prog wf_mb G; G,h\<turnstile>v::\<preceq>CC; G\<turnstile>CC \<preceq>? Class D; cast_ok G D h v|] |
24 |
==> G,h\<turnstile>v::\<preceq>Class D" |
|
25 |
apply (case_tac "CC") |
|
26 |
apply simp |
|
27 |
apply (case_tac "ref_ty") |
|
28 |
apply (clarsimp simp add: conf_def) |
|
29 |
apply simp |
|
23757 | 30 |
apply (ind_cases "G \<turnstile> Class cname \<preceq>? Class D" for cname, simp) |
14045 | 31 |
apply (rule conf_widen, assumption+) apply (erule widen.subcls) |
32 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
33 |
apply (unfold cast_ok_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
34 |
apply( case_tac "v = Null") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
35 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
36 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
37 |
apply( drule (1) non_npD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
38 |
apply( auto intro!: conf_AddrI simp add: obj_ty_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
39 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
40 |
|
13672 | 41 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
42 |
lemma FAcc_type_sound: |
13672 | 43 |
"[| 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
|
44 |
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
|
45 |
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
|
46 |
apply( drule np_NoneD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
47 |
apply( erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
48 |
apply( erule (1) notE impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
49 |
apply( drule non_np_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
50 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
51 |
apply( drule conforms_heapD [THEN hconfD]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
52 |
apply( assumption) |
14045 | 53 |
apply (frule wf_prog_ws_prog) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
54 |
apply( drule (2) widen_cfs_fields) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
55 |
apply( drule (1) oconf_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
56 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
57 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
58 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
59 |
lemma FAss_type_sound: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
60 |
"[| 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
|
61 |
(G, lT)\<turnstile>v::T'; G\<turnstile>T'\<preceq>ft; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
62 |
(G, lT)\<turnstile>aa::Class C; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
63 |
field (G,C) fn = Some (fd, ft); h''\<le>|h'; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
64 |
x' = None --> G,h'\<turnstile>a'::\<preceq> Class C; h'\<le>|h; |
13672 | 65 |
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
|
66 |
h''\<le>|h(a\<mapsto>(c,(fs((fn,fd)\<mapsto>x)))) \<and> |
13672 | 67 |
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
|
68 |
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
|
69 |
apply( drule np_NoneD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
70 |
apply( erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
71 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
72 |
apply( drule non_np_objD) |
12951 | 73 |
apply( assumption) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
74 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
75 |
apply( simp (no_asm_use)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
76 |
apply( frule (1) hext_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
77 |
apply( erule exE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
78 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
79 |
apply( clarify) |
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 |
apply( fast elim: hext_trans hext_upd_obj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
82 |
apply( rule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
83 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
84 |
apply( fast elim: conf_upd_obj [THEN iffD2]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
85 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
86 |
apply( rule conforms_upd_obj) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
87 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
88 |
apply( rule_tac [2] hextI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
89 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
90 |
apply( force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
91 |
apply( rule oconf_hext) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
92 |
apply( erule_tac [2] hext_upd_obj) |
14045 | 93 |
apply (frule wf_prog_ws_prog) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
94 |
apply( drule (2) widen_cfs_fields) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
95 |
apply( rule oconf_obj [THEN iffD2]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
96 |
apply( simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
97 |
apply( intro strip) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
98 |
apply( case_tac "(aaa, b) = (fn, fd)") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
99 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
100 |
apply( fast intro: conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
101 |
apply( fast dest: conforms_heapD [THEN hconfD] oconf_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
102 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
103 |
|
13672 | 104 |
|
105 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
106 |
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
|
107 |
list_all2 (\<lambda>T T'. G\<turnstile>T\<preceq>T') pTs pTs'; wf_mhead G (mn,pTs') rT; |
12888 | 108 |
length pTs' = length pns; distinct pns; |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
109 |
Ball (set lvars) (split (\<lambda>vn. is_type G)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
110 |
|] ==> 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
|
111 |
apply (unfold wf_mhead_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
112 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
113 |
apply( rule lconf_ext_list) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
114 |
apply( rule Ball_set_table [THEN lconf_init_vars]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
115 |
apply( force) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
116 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
117 |
apply( assumption) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
118 |
apply( erule (2) conf_list_gext_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
119 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
120 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
121 |
lemma Call_type_sound: |
13672 | 122 |
"[| 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
|
123 |
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
|
124 |
list_all2 (conf G h) pvs pTsa; |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
125 |
(md, rT, pns, lvars, blk, res) = |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
126 |
the (method (G,fst (the (h (the_Addr a')))) (mn, pTs')); |
13672 | 127 |
\<forall>lT. (np a' None, h, init_vars lvars(pns[\<mapsto>]pvs)(This\<mapsto>a'))::\<preceq>(G, lT) --> |
128 |
(G, lT)\<turnstile>blk\<surd> --> h\<le>|xi \<and> (xcptb, xi, xl)::\<preceq>(G, lT); |
|
129 |
\<forall>lT. (xcptb,xi, xl)::\<preceq>(G, lT) --> (\<forall>T. (G, lT)\<turnstile>res::T --> |
|
130 |
xi\<le>|h' \<and> (x',h', xj)::\<preceq>(G, lT) \<and> (x' = None --> G,h'\<turnstile>v::\<preceq>T)); |
|
131 |
G,xh\<turnstile>a'::\<preceq> Class C |
|
132 |
|] ==> |
|
133 |
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
|
134 |
apply( drule max_spec2mheads) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
135 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
136 |
apply( drule (2) non_np_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( frule (1) hext_objD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
139 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
140 |
apply( drule (3) Call_lemma) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
141 |
apply( clarsimp simp add: wf_java_mdecl_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
142 |
apply( erule_tac V = "method ?sig ?x = ?y" in thin_rl) |
13672 | 143 |
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
|
144 |
apply( rule conformsI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
145 |
apply( erule conforms_heapD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
146 |
apply( rule lconf_ext) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
147 |
apply( force elim!: Call_lemma2) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
148 |
apply( erule conf_hext, erule (1) conf_obj_AddrI) |
13672 | 149 |
apply( erule_tac V = "?E\<turnstile>?blk\<surd>" in thin_rl) |
150 |
apply (simp add: conforms_def) |
|
151 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
152 |
apply( erule conjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
153 |
apply( drule spec, erule (1) impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
154 |
apply( drule spec, erule (1) impE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
155 |
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
|
156 |
apply( clarify) |
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( fast intro: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
159 |
apply( rule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
160 |
apply( rule_tac [2] impI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
161 |
apply( erule_tac [2] notE impE, tactic "assume_tac 2") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
162 |
apply( frule_tac [2] conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
163 |
apply( tactic "assume_tac 4") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
164 |
apply( tactic "assume_tac 2") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
165 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
166 |
apply( fast elim!: widen_trans) |
13672 | 167 |
apply (rule conforms_xcpt_change) |
168 |
apply( rule conforms_hext) apply assumption |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
169 |
apply( erule (1) hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
170 |
apply( erule conforms_heapD) |
13672 | 171 |
apply (simp add: conforms_def) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
172 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
173 |
|
13672 | 174 |
|
175 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
176 |
declare split_if [split del] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
177 |
declare fun_upd_apply [simp del] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
178 |
declare fun_upd_same [simp] |
14045 | 179 |
declare wf_prog_ws_prog [simp] |
180 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
181 |
ML{* |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
182 |
val forward_hyp_tac = ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac, |
12517 | 183 |
(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
|
184 |
*} |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23894
diff
changeset
|
185 |
|
13672 | 186 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
187 |
theorem eval_evals_exec_type_sound: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
188 |
"wf_java_prog G ==> |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
189 |
(G\<turnstile>(x,(h,l)) -e \<succ>v -> (x', (h',l')) --> |
13672 | 190 |
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>T . (G,lT)\<turnstile>e :: T --> |
191 |
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
|
192 |
(G\<turnstile>(x,(h,l)) -es[\<succ>]vs-> (x', (h',l')) --> |
13672 | 193 |
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (\<forall>Ts. (G,lT)\<turnstile>es[::]Ts --> |
194 |
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
|
195 |
(G\<turnstile>(x,(h,l)) -c -> (x', (h',l')) --> |
13672 | 196 |
(\<forall>lT. (x,(h ,l ))::\<preceq>(G,lT) --> (G,lT)\<turnstile>c \<surd> --> |
197 |
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
|
198 |
apply( rule eval_evals_exec_induct) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
199 |
apply( unfold c_hupd_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
200 |
|
12517 | 201 |
-- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
202 |
apply( simp_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
203 |
apply( tactic "ALLGOALS strip_tac") |
22271 | 204 |
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
|
205 |
THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *}) |
12517 | 206 |
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
|
207 |
|
12517 | 208 |
-- "Level 7" |
209 |
-- "15 NewC" |
|
13672 | 210 |
apply (drule sym) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
211 |
apply( drule new_AddrD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
212 |
apply( erule disjE) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
213 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
214 |
apply( simp (no_asm_simp)) |
13672 | 215 |
apply (rule conforms_xcpt_change, assumption) |
216 |
apply (simp (no_asm_simp) add: xconf_def) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
217 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
218 |
apply( rule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
219 |
apply( force elim!: NewC_conforms) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
220 |
apply( rule conf_obj_AddrI) |
23757 | 221 |
apply( rule_tac [2] rtranclp.rtrancl_refl) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
222 |
apply( simp (no_asm)) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
223 |
|
12517 | 224 |
-- "for Cast" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
225 |
defer 1 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
226 |
|
12517 | 227 |
-- "14 Lit" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
228 |
apply( erule conf_litval) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
229 |
|
12517 | 230 |
-- "13 BinOp" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
231 |
apply (tactic "forward_hyp_tac") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
232 |
apply (tactic "forward_hyp_tac") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
233 |
apply( rule conjI, erule (1) hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
234 |
apply( erule conjI) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
235 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
236 |
apply( drule eval_no_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
237 |
apply( simp split add: binop.split) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
238 |
|
12517 | 239 |
-- "12 LAcc" |
13672 | 240 |
apply simp |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
241 |
apply( fast elim: conforms_localD [THEN lconfD]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
242 |
|
12517 | 243 |
-- "for FAss" |
22271 | 244 |
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
|
245 |
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
|
246 |
|
12517 | 247 |
-- "for if" |
27215 | 248 |
apply( tactic {* (InductTacs.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
|
249 |
(asm_full_simp_tac @{simpset})) 7*}) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
250 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
251 |
apply (tactic "forward_hyp_tac") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
252 |
|
12517 | 253 |
-- "11+1 if" |
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) |
22271 | 256 |
prefer 7 |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
257 |
apply( fast intro: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
258 |
|
12517 | 259 |
-- "10 Expr" |
22271 | 260 |
prefer 6 |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
261 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
262 |
|
12517 | 263 |
-- "9 ???" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
264 |
apply( simp_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
265 |
|
12517 | 266 |
-- "8 Cast" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
267 |
prefer 8 |
13672 | 268 |
apply (rule conjI) |
269 |
apply (fast intro: conforms_xcpt_change xconf_raise_if) |
|
270 |
||
271 |
apply clarify |
|
272 |
apply (drule raise_if_NoneD) |
|
273 |
apply (clarsimp) |
|
274 |
apply (rule Cast_conf) |
|
275 |
apply assumption+ |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
276 |
|
14045 | 277 |
|
12517 | 278 |
-- "7 LAss" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
279 |
apply (fold fun_upd_def) |
22271 | 280 |
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
|
281 |
THEN_ALL_NEW (full_simp_tac @{simpset})) 1 *}) |
13672 | 282 |
apply (intro strip) |
283 |
apply (case_tac E) |
|
284 |
apply (simp) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
285 |
apply( blast intro: conforms_upd_local conf_widen) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
286 |
|
12517 | 287 |
-- "6 FAcc" |
13672 | 288 |
apply (rule conjI) |
289 |
apply (simp add: np_def) |
|
290 |
apply (fast intro: conforms_xcpt_change xconf_raise_if) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
291 |
apply( fast elim!: FAcc_type_sound) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
292 |
|
12517 | 293 |
-- "5 While" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
294 |
prefer 5 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
295 |
apply(erule_tac V = "?a \<longrightarrow> ?b" in thin_rl) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
296 |
apply(drule (1) ty_expr_ty_exprs_wt_stmt.Loop) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
297 |
apply(force elim: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
298 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
299 |
apply (tactic "forward_hyp_tac") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
300 |
|
13672 | 301 |
-- "4 Cond" |
302 |
prefer 4 |
|
303 |
apply (case_tac "the_Bool v") |
|
304 |
apply simp |
|
305 |
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
|
306 |
apply simp |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
307 |
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
|
308 |
|
12517 | 309 |
-- "3 ;;" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
310 |
prefer 3 |
13672 | 311 |
apply( fast dest: evals_no_xcpt intro: conf_hext hext_trans) |
312 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
313 |
|
12517 | 314 |
-- "2 FAss" |
22271 | 315 |
apply (subgoal_tac "(np a' x1, aa, ba) ::\<preceq> (G, lT)") |
13672 | 316 |
prefer 2 |
317 |
apply (simp add: np_def) |
|
318 |
apply (fast intro: conforms_xcpt_change xconf_raise_if) |
|
319 |
apply( case_tac "x2") |
|
320 |
-- "x2 = None" |
|
321 |
apply (simp) |
|
322 |
apply (tactic forward_hyp_tac, clarify) |
|
323 |
apply( drule eval_no_xcpt) |
|
324 |
apply( erule FAss_type_sound, rule HOL.refl, assumption+) |
|
325 |
-- "x2 = Some a" |
|
326 |
apply ( simp (no_asm_simp)) |
|
327 |
apply( fast intro: hext_trans) |
|
328 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
329 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
330 |
apply( tactic prune_params_tac) |
12517 | 331 |
-- "Level 52" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
332 |
|
12517 | 333 |
-- "1 Call" |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
334 |
apply( case_tac "x") |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
335 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
336 |
apply( clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
337 |
apply( drule exec_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( drule_tac eval_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
340 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
341 |
apply( fast elim: hext_trans) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
342 |
apply( clarify) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
343 |
apply( drule evals_no_xcpt) |
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( case_tac "a' = Null") |
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 exec_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
348 |
apply( simp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
349 |
apply( drule eval_xcpt) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
350 |
apply( simp) |
13672 | 351 |
apply (rule conjI) |
352 |
apply( fast elim: hext_trans) |
|
14045 | 353 |
apply (rule conforms_xcpt_change, assumption) |
354 |
apply (simp (no_asm_simp) add: xconf_def) |
|
13672 | 355 |
apply(clarsimp) |
356 |
||
357 |
apply( drule ty_expr_is_type, simp) |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
358 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
359 |
apply(unfold is_class_def) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
360 |
apply(clarsimp) |
13672 | 361 |
|
11644
3dfde687f0d7
Removed some unfoldings of defs after declaring wf_java_prog as syntax
streckem
parents:
11070
diff
changeset
|
362 |
apply(rule Call_type_sound); |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
363 |
prefer 11 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
364 |
apply blast |
11644
3dfde687f0d7
Removed some unfoldings of defs after declaring wf_java_prog as syntax
streckem
parents:
11070
diff
changeset
|
365 |
apply (simp (no_asm_simp))+ |
13672 | 366 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
367 |
done |
24178
4ff1dc2aa18d
turned Unify flags into configuration options (global only);
wenzelm
parents:
23894
diff
changeset
|
368 |
|
14142 | 369 |
|
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
370 |
lemma eval_type_sound: "!!E s s'. |
14142 | 371 |
[| wf_java_prog G; G\<turnstile>(x,s) -e\<succ>v -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>e::T; G=prg E |] |
372 |
==> (x',s')::\<preceq>E \<and> (x'=None --> G,heap s'\<turnstile>v::\<preceq>T) \<and> heap s \<le>| heap s'" |
|
373 |
apply (simp (no_asm_simp) only: split_tupled_all) |
|
374 |
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
|
375 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
376 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
377 |
|
14142 | 378 |
|
14045 | 379 |
lemma evals_type_sound: "!!E s s'. |
14142 | 380 |
[| wf_java_prog G; G\<turnstile>(x,s) -es[\<succ>]vs -> (x',s'); (x,s)::\<preceq>E; E\<turnstile>es[::]Ts; G=prg E |] |
381 |
==> (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'" |
|
382 |
apply (simp (no_asm_simp) only: split_tupled_all) |
|
383 |
apply (drule eval_evals_exec_type_sound [THEN conjunct2, THEN conjunct1, THEN mp, THEN spec, THEN mp]) |
|
14045 | 384 |
apply auto |
385 |
done |
|
386 |
||
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
387 |
lemma exec_type_sound: "!!E s s'. |
14142 | 388 |
\<lbrakk> wf_java_prog G; G\<turnstile>(x,s) -s0-> (x',s'); (x,s)::\<preceq>E; E\<turnstile>s0\<surd>; G=prg E \<rbrakk> |
389 |
\<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
|
390 |
apply( simp (no_asm_simp) only: split_tupled_all) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
391 |
apply (drule eval_evals_exec_type_sound |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
392 |
[THEN conjunct2, THEN conjunct2, THEN mp, THEN spec, THEN mp]) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
393 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
394 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
395 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
396 |
theorem all_methods_understood: |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
397 |
"[|G=prg E; wf_java_prog G; G\<turnstile>(x,s) -e\<succ>a'-> Norm s'; a' \<noteq> Null; |
13672 | 398 |
(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
|
399 |
method (G,fst (the (heap s' (the_Addr a')))) sig \<noteq> None" |
14142 | 400 |
apply (frule eval_type_sound, assumption+) |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
401 |
apply(clarsimp) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
402 |
apply( frule widen_methd) |
14142 | 403 |
apply assumption |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
404 |
prefer 2 |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
405 |
apply( fast) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
406 |
apply( drule non_npD) |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
407 |
apply auto |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
408 |
done |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
409 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
410 |
declare split_beta [simp del] |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
411 |
declare fun_upd_apply [simp] |
14045 | 412 |
declare wf_prog_ws_prog [simp del] |
11026
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
413 |
|
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
414 |
end |
a50365d21144
converted to Isar, simplifying recursion on class hierarchy
oheimb
parents:
8011
diff
changeset
|
415 |