author | kleing |
Tue, 16 Jan 2001 15:56:34 +0100 | |
changeset 10920 | 9b74eceea2d2 |
parent 10812 | ead84e90bfeb |
child 11085 | b830bf10bf71 |
permissions | -rw-r--r-- |
8011 | 1 |
(* Title: HOL/MicroJava/BV/Correct.thy |
2 |
ID: $Id$ |
|
3 |
Author: Cornelia Pusch |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
5 |
||
6 |
The invariant for the type safety proof. |
|
7 |
*) |
|
8 |
||
10056 | 9 |
header "BV Type Safety Invariant" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
10 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
11 |
theory Correct = BVSpec: |
8011 | 12 |
|
13 |
constdefs |
|
10056 | 14 |
approx_val :: "[jvm_prog,aheap,val,ty err] => bool" |
10496 | 15 |
"approx_val G h v any == case any of Err => True | OK T => G,h\<turnstile>v::\<preceq>T" |
8011 | 16 |
|
10056 | 17 |
approx_loc :: "[jvm_prog,aheap,val list,locvars_type] => bool" |
18 |
"approx_loc G hp loc LT == list_all2 (approx_val G hp) loc LT" |
|
19 |
||
20 |
approx_stk :: "[jvm_prog,aheap,opstack,opstack_type] => bool" |
|
10496 | 21 |
"approx_stk G hp stk ST == approx_loc G hp stk (map OK ST)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
22 |
|
10056 | 23 |
correct_frame :: "[jvm_prog,aheap,state_type,nat,bytecode] => frame => bool" |
24 |
"correct_frame G hp == \<lambda>(ST,LT) maxl ins (stk,loc,C,sig,pc). |
|
25 |
approx_stk G hp stk ST \<and> approx_loc G hp loc LT \<and> |
|
26 |
pc < length ins \<and> length loc=length(snd sig)+maxl+1" |
|
8011 | 27 |
|
10056 | 28 |
correct_frame_opt :: "[jvm_prog,aheap,state_type option,nat,bytecode] |
29 |
=> frame => bool" |
|
30 |
"correct_frame_opt G hp s == |
|
31 |
case s of None => \<lambda>maxl ins f. False | Some t => correct_frame G hp t" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
32 |
|
8011 | 33 |
|
34 |
consts |
|
10042 | 35 |
correct_frames :: "[jvm_prog,aheap,prog_type,ty,sig,frame list] => bool" |
8011 | 36 |
primrec |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
37 |
"correct_frames G hp phi rT0 sig0 [] = True" |
8011 | 38 |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
39 |
"correct_frames G hp phi rT0 sig0 (f#frs) = |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
40 |
(let (stk,loc,C,sig,pc) = f in |
10592 | 41 |
(\<exists>ST LT rT maxs maxl ins. |
10625
022c6b2bcd6b
strengthened invariant: current class must be defined
kleing
parents:
10612
diff
changeset
|
42 |
phi C sig ! pc = Some (ST,LT) \<and> is_class G C \<and> |
10592 | 43 |
method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and> |
10625
022c6b2bcd6b
strengthened invariant: current class must be defined
kleing
parents:
10612
diff
changeset
|
44 |
(\<exists>C' mn pTs k. pc = k+1 \<and> ins!k = (Invoke C' mn pTs) \<and> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
45 |
(mn,pTs) = sig0 \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
46 |
(\<exists>apTs D ST' LT'. |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
47 |
(phi C sig)!k = Some ((rev apTs) @ (Class D) # ST', LT') \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
48 |
length apTs = length pTs \<and> |
10592 | 49 |
(\<exists>D' rT' maxs' maxl' ins'. |
50 |
method (G,D) sig0 = Some(D',rT',(maxs',maxl',ins')) \<and> |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
51 |
G \<turnstile> rT0 \<preceq> rT') \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
52 |
correct_frame G hp (tl ST, LT) maxl ins f \<and> |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
53 |
correct_frames G hp phi rT sig frs))))" |
8011 | 54 |
|
55 |
||
56 |
constdefs |
|
10042 | 57 |
correct_state :: "[jvm_prog,prog_type,jvm_state] => bool" |
10060 | 58 |
("_,_ \<turnstile>JVM _ \<surd>" [51,51] 50) |
10042 | 59 |
"correct_state G phi == \<lambda>(xp,hp,frs). |
8011 | 60 |
case xp of |
10042 | 61 |
None => (case frs of |
62 |
[] => True |
|
63 |
| (f#fs) => G\<turnstile>h hp\<surd> \<and> |
|
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
64 |
(let (stk,loc,C,sig,pc) = f |
8011 | 65 |
in |
10592 | 66 |
\<exists>rT maxs maxl ins s. |
10625
022c6b2bcd6b
strengthened invariant: current class must be defined
kleing
parents:
10612
diff
changeset
|
67 |
is_class G C \<and> |
10592 | 68 |
method (G,C) sig = Some(C,rT,(maxs,maxl,ins)) \<and> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
69 |
phi C sig ! pc = Some s \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
70 |
correct_frame G hp s maxl ins f \<and> |
8045
816f566c414f
Fixed a problem with returning from the last frame.
nipkow
parents:
8034
diff
changeset
|
71 |
correct_frames G hp phi rT sig fs)) |
10042 | 72 |
| Some x => True" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
73 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
74 |
|
10060 | 75 |
syntax (HTML) |
76 |
correct_state :: "[jvm_prog,prog_type,jvm_state] => bool" |
|
77 |
("_,_ |-JVM _ [ok]" [51,51] 50) |
|
78 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
79 |
lemma sup_heap_newref: |
10920 | 80 |
"hp oref = None ==> hp \<le>| hp(oref \<mapsto> obj)" |
81 |
proof (unfold hext_def, intro strip) |
|
82 |
fix a C fs |
|
83 |
assume "hp oref = None" and hp: "hp a = Some (C, fs)" |
|
84 |
hence "a \<noteq> oref" by auto |
|
85 |
hence "(hp (oref\<mapsto>obj)) a = hp a" by (rule fun_upd_other) |
|
86 |
with hp |
|
87 |
show "\<exists>fs'. (hp(oref\<mapsto>obj)) a = Some (C, fs')" by auto |
|
88 |
qed |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
89 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
90 |
lemma sup_heap_update_value: |
10042 | 91 |
"hp a = Some (C,od') ==> hp \<le>| hp (a \<mapsto> (C,od))" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
92 |
by (simp add: hext_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
93 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
94 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
95 |
(** approx_val **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
96 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
97 |
lemma approx_val_Err: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
98 |
"approx_val G hp x Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
99 |
by (simp add: approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
100 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
101 |
lemma approx_val_Null: |
10496 | 102 |
"approx_val G hp Null (OK (RefT x))" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
103 |
by (auto intro: null simp add: approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
104 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
105 |
lemma approx_val_imp_approx_val_assConvertible [rule_format]: |
10496 | 106 |
"wf_prog wt G ==> approx_val G hp v (OK T) --> G\<turnstile> T\<preceq>T' |
107 |
--> approx_val G hp v (OK T')" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
108 |
by (cases T) (auto intro: conf_widen simp add: approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
109 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
110 |
lemma approx_val_imp_approx_val_sup_heap [rule_format]: |
10042 | 111 |
"approx_val G hp v at --> hp \<le>| hp' --> approx_val G hp' v at" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
112 |
apply (simp add: approx_val_def split: err.split) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
113 |
apply (blast intro: conf_hext) |
10056 | 114 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
115 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
116 |
lemma approx_val_imp_approx_val_heap_update: |
10042 | 117 |
"[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] |
118 |
==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
119 |
by (cases v, auto simp add: obj_ty_def conf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
120 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
121 |
lemma approx_val_imp_approx_val_sup [rule_format]: |
10056 | 122 |
"wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') |
123 |
--> (approx_val G h v us')" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
124 |
apply (simp add: sup_PTS_eq approx_val_def split: err.split) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
125 |
apply (blast intro: conf_widen) |
10056 | 126 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
127 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
128 |
lemma approx_loc_imp_approx_val_sup: |
10056 | 129 |
"[| wf_prog wt G; approx_loc G hp loc LT; idx < length LT; |
130 |
v = loc!idx; G \<turnstile> LT!idx <=o at |] |
|
10042 | 131 |
==> approx_val G hp v at" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
132 |
apply (unfold approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
133 |
apply (unfold list_all2_def) |
10056 | 134 |
apply (auto intro: approx_val_imp_approx_val_sup |
135 |
simp add: split_def all_set_conv_all_nth) |
|
136 |
done |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
137 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
138 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
139 |
(** approx_loc **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
140 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
141 |
lemma approx_loc_Cons [iff]: |
10056 | 142 |
"approx_loc G hp (s#xs) (l#ls) = |
143 |
(approx_val G hp s l \<and> approx_loc G hp xs ls)" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
144 |
by (simp add: approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
145 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
146 |
lemma assConv_approx_stk_imp_approx_loc [rule_format]: |
10042 | 147 |
"wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) |
148 |
--> length tys_n = length ts --> approx_stk G hp s tys_n --> |
|
10496 | 149 |
approx_loc G hp s (map OK ts)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
150 |
apply (unfold approx_stk_def approx_loc_def list_all2_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
151 |
apply (clarsimp simp add: all_set_conv_all_nth) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
152 |
apply (rule approx_val_imp_approx_val_assConvertible) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
153 |
apply auto |
10056 | 154 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
155 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
156 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
157 |
lemma approx_loc_imp_approx_loc_sup_heap [rule_format]: |
10056 | 158 |
"\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' |
159 |
--> approx_loc G hp' lvars lt" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
160 |
apply (unfold approx_loc_def list_all2_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
161 |
apply (cases lt) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
162 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
163 |
apply clarsimp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
164 |
apply (rule approx_val_imp_approx_val_sup_heap) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
165 |
apply auto |
10056 | 166 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
167 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
168 |
lemma approx_loc_imp_approx_loc_sup [rule_format]: |
10056 | 169 |
"wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' |
170 |
--> approx_loc G hp lvars lt'" |
|
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10625
diff
changeset
|
171 |
apply (unfold Listn.le_def lesub_def sup_loc_def approx_loc_def list_all2_def) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
172 |
apply (auto simp add: all_set_conv_all_nth) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
173 |
apply (auto elim: approx_val_imp_approx_val_sup) |
10056 | 174 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
175 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
176 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
177 |
lemma approx_loc_imp_approx_loc_subst [rule_format]: |
10042 | 178 |
"\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X) |
179 |
--> (approx_loc G hp (loc[idx:=x]) (LT[idx:=X]))" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
180 |
apply (unfold approx_loc_def list_all2_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
181 |
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update) |
10056 | 182 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
183 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
184 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
185 |
lemmas [cong] = conj_cong |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
186 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
187 |
lemma approx_loc_append [rule_format]: |
10042 | 188 |
"\<forall>L1 l2 L2. length l1=length L1 --> |
10056 | 189 |
approx_loc G hp (l1@l2) (L1@L2) = |
190 |
(approx_loc G hp l1 L1 \<and> approx_loc G hp l2 L2)" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
191 |
apply (unfold approx_loc_def list_all2_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
192 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
193 |
apply blast |
10056 | 194 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
195 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
196 |
lemmas [cong del] = conj_cong |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
197 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
198 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
199 |
(** approx_stk **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
200 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
201 |
lemma approx_stk_rev_lem: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
202 |
"approx_stk G hp (rev s) (rev t) = approx_stk G hp s t" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
203 |
apply (unfold approx_stk_def approx_loc_def list_all2_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
204 |
apply (auto simp add: zip_rev sym [OF rev_map]) |
10056 | 205 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
206 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
207 |
lemma approx_stk_rev: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
208 |
"approx_stk G hp (rev s) t = approx_stk G hp s (rev t)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
209 |
by (auto intro: subst [OF approx_stk_rev_lem]) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
210 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
211 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
212 |
lemma approx_stk_imp_approx_stk_sup_heap [rule_format]: |
10056 | 213 |
"\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' |
214 |
--> approx_stk G hp' lvars lt" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
215 |
by (auto intro: approx_loc_imp_approx_loc_sup_heap simp add: approx_stk_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
216 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
217 |
lemma approx_stk_imp_approx_stk_sup [rule_format]: |
10496 | 218 |
"wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map OK st <=l (map OK st')) |
10042 | 219 |
--> approx_stk G hp lvars st'" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
220 |
by (auto intro: approx_loc_imp_approx_loc_sup simp add: approx_stk_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
221 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
222 |
lemma approx_stk_Nil [iff]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
223 |
"approx_stk G hp [] []" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
224 |
by (simp add: approx_stk_def approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
225 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
226 |
lemma approx_stk_Cons [iff]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
227 |
"approx_stk G hp (x # stk) (S#ST) = |
10496 | 228 |
(approx_val G hp x (OK S) \<and> approx_stk G hp stk ST)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
229 |
by (simp add: approx_stk_def approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
230 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
231 |
lemma approx_stk_Cons_lemma [iff]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
232 |
"approx_stk G hp stk (S#ST') = |
10496 | 233 |
(\<exists>s stk'. stk = s#stk' \<and> approx_val G hp s (OK S) \<and> approx_stk G hp stk' ST')" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
234 |
by (simp add: list_all2_Cons2 approx_stk_def approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
235 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
236 |
lemma approx_stk_append_lemma: |
10042 | 237 |
"approx_stk G hp stk (S@ST') ==> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
238 |
(\<exists>s stk'. stk = s@stk' \<and> length s = length S \<and> length stk' = length ST' \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
239 |
approx_stk G hp s S \<and> approx_stk G hp stk' ST')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
240 |
by (simp add: list_all2_append2 approx_stk_def approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
241 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
242 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
243 |
(** oconf **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
244 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
245 |
lemma correct_init_obj: |
10042 | 246 |
"[|is_class G C; wf_prog wt G|] ==> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
247 |
G,h \<turnstile> (C, map_of (map (\<lambda>(f,fT).(f,default_val fT)) (fields(G,C)))) \<surd>" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
248 |
apply (unfold oconf_def lconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
249 |
apply (simp add: map_of_map) |
10612
779af7c58743
improved superclass entry for classes and definition status of is_class, class
oheimb
parents:
10592
diff
changeset
|
250 |
apply (force intro: defval_conf dest: map_of_SomeD fields_is_type) |
10056 | 251 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
252 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
253 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
254 |
lemma oconf_imp_oconf_field_update [rule_format]: |
10042 | 255 |
"[|map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> |] |
256 |
==> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
257 |
by (simp add: oconf_def lconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
258 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
259 |
lemma oconf_imp_oconf_heap_newref [rule_format]: |
10920 | 260 |
"hp oref = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(oref\<mapsto>obj'))\<turnstile>obj\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
261 |
apply (unfold oconf_def lconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
262 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
263 |
apply (fast intro: conf_hext sup_heap_newref) |
10056 | 264 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
265 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
266 |
lemma oconf_imp_oconf_heap_update [rule_format]: |
10042 | 267 |
"hp a = Some obj' --> obj_ty obj' = obj_ty obj'' --> G,hp\<turnstile>obj\<surd> |
268 |
--> G,hp(a\<mapsto>obj'')\<turnstile>obj\<surd>" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
269 |
apply (unfold oconf_def lconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
270 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
271 |
apply (force intro: approx_val_imp_approx_val_heap_update) |
10056 | 272 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
273 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
274 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
275 |
(** hconf **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
276 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
277 |
lemma hconf_imp_hconf_newref [rule_format]: |
10920 | 278 |
"hp oref = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(oref\<mapsto>obj)\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
279 |
apply (simp add: hconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
280 |
apply (fast intro: oconf_imp_oconf_heap_newref) |
10056 | 281 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
282 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
283 |
lemma hconf_imp_hconf_field_update [rule_format]: |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
284 |
"map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> |
10042 | 285 |
G,hp\<turnstile>v::\<preceq>T \<and> G\<turnstile>h hp\<surd> --> G\<turnstile>h hp(oloc \<mapsto> (oT, fs((F,D)\<mapsto>v)))\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
286 |
apply (simp add: hconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
287 |
apply (force intro: oconf_imp_oconf_heap_update oconf_imp_oconf_field_update |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
288 |
simp add: obj_ty_def) |
10056 | 289 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
290 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
291 |
(** correct_frames **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
292 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
293 |
lemmas [simp del] = fun_upd_apply |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
294 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
295 |
lemma correct_frames_imp_correct_frames_field_update [rule_format]: |
10042 | 296 |
"\<forall>rT C sig. correct_frames G hp phi rT sig frs --> |
297 |
hp a = Some (C,od) --> map_of (fields (G, C)) fl = Some fd --> |
|
298 |
G,hp\<turnstile>v::\<preceq>fd |
|
299 |
--> correct_frames G (hp(a \<mapsto> (C, od(fl\<mapsto>v)))) phi rT sig frs"; |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
300 |
apply (induct frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
301 |
apply simp |
10920 | 302 |
apply clarify |
303 |
apply simp |
|
304 |
apply clarify |
|
305 |
apply (unfold correct_frame_def) |
|
306 |
apply (simp (no_asm_use)) |
|
307 |
apply clarsimp |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
308 |
apply (intro exI conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
309 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
310 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
311 |
apply force |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
312 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
313 |
apply (rule approx_stk_imp_approx_stk_sup_heap) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
314 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
315 |
apply (rule sup_heap_update_value) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
316 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
317 |
apply (rule approx_loc_imp_approx_loc_sup_heap) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
318 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
319 |
apply (rule sup_heap_update_value) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
320 |
apply simp |
10056 | 321 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
322 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
323 |
lemma correct_frames_imp_correct_frames_newref [rule_format]: |
10042 | 324 |
"\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj |
10920 | 325 |
--> correct_frames G (hp(x \<mapsto> obj)) phi rT sig frs" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
326 |
apply (induct frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
327 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
328 |
apply (clarsimp simp add: correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
329 |
apply (intro exI conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
330 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
331 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
332 |
apply force |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
333 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
334 |
apply (rule approx_stk_imp_approx_stk_sup_heap) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
335 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
336 |
apply (rule sup_heap_newref) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
337 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
338 |
apply (rule approx_loc_imp_approx_loc_sup_heap) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
339 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
340 |
apply (rule sup_heap_newref) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
341 |
apply simp |
10056 | 342 |
done |
8011 | 343 |
|
344 |
end |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
345 |