author | kleing |
Sun, 07 Jan 2001 18:43:13 +0100 | |
changeset 10812 | ead84e90bfeb |
parent 10625 | 022c6b2bcd6b |
child 10920 | 9b74eceea2d2 |
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 |
||
79 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
80 |
lemma sup_heap_newref: |
10042 | 81 |
"hp x = None ==> hp \<le>| hp(newref hp \<mapsto> obj)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
82 |
apply (unfold hext_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
83 |
apply clarsimp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
84 |
apply (drule newref_None 1) back |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
85 |
apply simp |
10056 | 86 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
87 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
88 |
lemma sup_heap_update_value: |
10042 | 89 |
"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
|
90 |
by (simp add: hext_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
91 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
92 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
93 |
(** approx_val **) |
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 |
lemma approx_val_Err: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
96 |
"approx_val G hp x Err" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
97 |
by (simp add: approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
98 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
99 |
lemma approx_val_Null: |
10496 | 100 |
"approx_val G hp Null (OK (RefT x))" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
101 |
by (auto intro: null simp add: approx_val_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
102 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
103 |
lemma approx_val_imp_approx_val_assConvertible [rule_format]: |
10496 | 104 |
"wf_prog wt G ==> approx_val G hp v (OK T) --> G\<turnstile> T\<preceq>T' |
105 |
--> approx_val G hp v (OK T')" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
106 |
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
|
107 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
108 |
lemma approx_val_imp_approx_val_sup_heap [rule_format]: |
10042 | 109 |
"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
|
110 |
apply (simp add: approx_val_def split: err.split) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
111 |
apply (blast intro: conf_hext) |
10056 | 112 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
113 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
114 |
lemma approx_val_imp_approx_val_heap_update: |
10042 | 115 |
"[|hp a = Some obj'; G,hp\<turnstile> v::\<preceq>T; obj_ty obj = obj_ty obj'|] |
116 |
==> G,hp(a\<mapsto>obj)\<turnstile> v::\<preceq>T" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
117 |
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
|
118 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
119 |
lemma approx_val_imp_approx_val_sup [rule_format]: |
10056 | 120 |
"wf_prog wt G ==> (approx_val G h v us) --> (G \<turnstile> us <=o us') |
121 |
--> (approx_val G h v us')" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
122 |
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
|
123 |
apply (blast intro: conf_widen) |
10056 | 124 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
125 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
126 |
lemma approx_loc_imp_approx_val_sup: |
10056 | 127 |
"[| wf_prog wt G; approx_loc G hp loc LT; idx < length LT; |
128 |
v = loc!idx; G \<turnstile> LT!idx <=o at |] |
|
10042 | 129 |
==> approx_val G hp v at" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
130 |
apply (unfold approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
131 |
apply (unfold list_all2_def) |
10056 | 132 |
apply (auto intro: approx_val_imp_approx_val_sup |
133 |
simp add: split_def all_set_conv_all_nth) |
|
134 |
done |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
135 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
136 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
137 |
(** approx_loc **) |
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 |
lemma approx_loc_Cons [iff]: |
10056 | 140 |
"approx_loc G hp (s#xs) (l#ls) = |
141 |
(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
|
142 |
by (simp add: approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
143 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
144 |
lemma assConv_approx_stk_imp_approx_loc [rule_format]: |
10042 | 145 |
"wf_prog wt G ==> (\<forall>tt'\<in>set (zip tys_n ts). tt' \<in> widen G) |
146 |
--> length tys_n = length ts --> approx_stk G hp s tys_n --> |
|
10496 | 147 |
approx_loc G hp s (map OK ts)" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
148 |
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
|
149 |
apply (clarsimp simp add: all_set_conv_all_nth) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
150 |
apply (rule approx_val_imp_approx_val_assConvertible) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
151 |
apply auto |
10056 | 152 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
153 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
154 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
155 |
lemma approx_loc_imp_approx_loc_sup_heap [rule_format]: |
10056 | 156 |
"\<forall>lvars. approx_loc G hp lvars lt --> hp \<le>| hp' |
157 |
--> approx_loc G hp' lvars lt" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
158 |
apply (unfold approx_loc_def list_all2_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
159 |
apply (cases lt) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
160 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
161 |
apply clarsimp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
162 |
apply (rule approx_val_imp_approx_val_sup_heap) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
163 |
apply auto |
10056 | 164 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
165 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
166 |
lemma approx_loc_imp_approx_loc_sup [rule_format]: |
10056 | 167 |
"wf_prog wt G ==> approx_loc G hp lvars lt --> G \<turnstile> lt <=l lt' |
168 |
--> 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
|
169 |
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
|
170 |
apply (auto simp add: all_set_conv_all_nth) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
171 |
apply (auto elim: approx_val_imp_approx_val_sup) |
10056 | 172 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
173 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
174 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
175 |
lemma approx_loc_imp_approx_loc_subst [rule_format]: |
10042 | 176 |
"\<forall>loc idx x X. (approx_loc G hp loc LT) --> (approx_val G hp x X) |
177 |
--> (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
|
178 |
apply (unfold approx_loc_def list_all2_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
179 |
apply (auto dest: subsetD [OF set_update_subset_insert] simp add: zip_update) |
10056 | 180 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
181 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
182 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
183 |
lemmas [cong] = conj_cong |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
184 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
185 |
lemma approx_loc_append [rule_format]: |
10042 | 186 |
"\<forall>L1 l2 L2. length l1=length L1 --> |
10056 | 187 |
approx_loc G hp (l1@l2) (L1@L2) = |
188 |
(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
|
189 |
apply (unfold approx_loc_def list_all2_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
190 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
191 |
apply blast |
10056 | 192 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
193 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
194 |
lemmas [cong del] = conj_cong |
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 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
197 |
(** approx_stk **) |
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 |
lemma approx_stk_rev_lem: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
200 |
"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
|
201 |
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
|
202 |
apply (auto simp add: zip_rev sym [OF rev_map]) |
10056 | 203 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
204 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
205 |
lemma approx_stk_rev: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
206 |
"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
|
207 |
by (auto intro: subst [OF approx_stk_rev_lem]) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
208 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
209 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
210 |
lemma approx_stk_imp_approx_stk_sup_heap [rule_format]: |
10056 | 211 |
"\<forall>lvars. approx_stk G hp lvars lt --> hp \<le>| hp' |
212 |
--> approx_stk G hp' lvars lt" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
213 |
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
|
214 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
215 |
lemma approx_stk_imp_approx_stk_sup [rule_format]: |
10496 | 216 |
"wf_prog wt G ==> approx_stk G hp lvars st --> (G \<turnstile> map OK st <=l (map OK st')) |
10042 | 217 |
--> approx_stk G hp lvars st'" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
218 |
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
|
219 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
220 |
lemma approx_stk_Nil [iff]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
221 |
"approx_stk G hp [] []" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
222 |
by (simp add: approx_stk_def approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
223 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
224 |
lemma approx_stk_Cons [iff]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
225 |
"approx_stk G hp (x # stk) (S#ST) = |
10496 | 226 |
(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
|
227 |
by (simp add: approx_stk_def approx_loc_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
228 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
229 |
lemma approx_stk_Cons_lemma [iff]: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
230 |
"approx_stk G hp stk (S#ST') = |
10496 | 231 |
(\<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
|
232 |
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
|
233 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
234 |
lemma approx_stk_append_lemma: |
10042 | 235 |
"approx_stk G hp stk (S@ST') ==> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
236 |
(\<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
|
237 |
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
|
238 |
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
|
239 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
240 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
241 |
(** oconf **) |
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 |
lemma correct_init_obj: |
10042 | 244 |
"[|is_class G C; wf_prog wt G|] ==> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
245 |
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
|
246 |
apply (unfold oconf_def lconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
247 |
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
|
248 |
apply (force intro: defval_conf dest: map_of_SomeD fields_is_type) |
10056 | 249 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
250 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
251 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
252 |
lemma oconf_imp_oconf_field_update [rule_format]: |
10042 | 253 |
"[|map_of (fields (G, oT)) FD = Some T; G,hp\<turnstile>v::\<preceq>T; G,hp\<turnstile>(oT,fs)\<surd> |] |
254 |
==> G,hp\<turnstile>(oT, fs(FD\<mapsto>v))\<surd>" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
255 |
by (simp add: oconf_def lconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
256 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
257 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
258 |
lemma oconf_imp_oconf_heap_newref [rule_format]: |
10042 | 259 |
"hp x = None --> G,hp\<turnstile>obj\<surd> --> G,hp\<turnstile>obj'\<surd> --> G,(hp(newref hp\<mapsto>obj'))\<turnstile>obj\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
260 |
apply (unfold oconf_def lconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
261 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
262 |
apply (fast intro: conf_hext sup_heap_newref) |
10056 | 263 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
264 |
|
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 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
277 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
278 |
lemma hconf_imp_hconf_newref [rule_format]: |
10042 | 279 |
"hp x = None --> G\<turnstile>h hp\<surd> --> G,hp\<turnstile>obj\<surd> --> G\<turnstile>h hp(newref hp\<mapsto>obj)\<surd>" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
280 |
apply (simp add: hconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
281 |
apply (fast intro: oconf_imp_oconf_heap_newref) |
10056 | 282 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
283 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
284 |
lemma hconf_imp_hconf_field_update [rule_format]: |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
285 |
"map_of (fields (G, oT)) (F, D) = Some T \<and> hp oloc = Some(oT,fs) \<and> |
10042 | 286 |
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
|
287 |
apply (simp add: hconf_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
288 |
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
|
289 |
simp add: obj_ty_def) |
10056 | 290 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
291 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
292 |
(** correct_frames **) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
293 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
294 |
lemmas [simp del] = fun_upd_apply |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
295 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
296 |
lemma correct_frames_imp_correct_frames_field_update [rule_format]: |
10042 | 297 |
"\<forall>rT C sig. correct_frames G hp phi rT sig frs --> |
298 |
hp a = Some (C,od) --> map_of (fields (G, C)) fl = Some fd --> |
|
299 |
G,hp\<turnstile>v::\<preceq>fd |
|
300 |
--> 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
|
301 |
apply (induct frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
302 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
303 |
apply (clarsimp simp add: correct_frame_def) (*takes long*) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
304 |
apply (intro exI conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
305 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
306 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
307 |
apply force |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
308 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
309 |
apply (rule approx_stk_imp_approx_stk_sup_heap) |
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 (rule sup_heap_update_value) |
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_loc_imp_approx_loc_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 |
10056 | 317 |
done |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
318 |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
319 |
lemma correct_frames_imp_correct_frames_newref [rule_format]: |
10042 | 320 |
"\<forall>rT C sig. hp x = None --> correct_frames G hp phi rT sig frs \<and> oconf G hp obj |
321 |
--> correct_frames G (hp(newref hp \<mapsto> obj)) phi rT sig frs" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
322 |
apply (induct frs) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
323 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
324 |
apply (clarsimp simp add: correct_frame_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
325 |
apply (intro exI conjI) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
326 |
apply simp |
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 force |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
329 |
apply simp |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
330 |
apply (rule approx_stk_imp_approx_stk_sup_heap) |
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 (rule sup_heap_newref) |
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_loc_imp_approx_loc_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 |
10056 | 338 |
done |
8011 | 339 |
|
340 |
end |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9549
diff
changeset
|
341 |