author | kleing |
Wed, 20 Mar 2002 13:21:07 +0100 | |
changeset 13062 | 4b1edf2f6bd2 |
parent 13006 | 51c5f3f11d16 |
child 13064 | 1f54a5fecaa6 |
permissions | -rw-r--r-- |
8388 | 1 |
(* Title: HOL/MicroJava/BV/LBVComplete.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gerwin Klein |
|
4 |
Copyright 2000 Technische Universitaet Muenchen |
|
9054 | 5 |
*) |
8388 | 6 |
|
12911 | 7 |
header {* \isaheader{Completeness of the LBV} *} |
8388 | 8 |
|
12516 | 9 |
(* This theory is currently broken. The port to exceptions |
10 |
didn't make it into the Isabelle 2001 release. It is included for |
|
11 |
documentation only. See Isabelle 99-2 for a working copy of this |
|
12 |
theory. *) |
|
13 |
||
14 |
theory LBVComplete = BVSpec + LBVSpec + EffectMono: |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
15 |
|
8388 | 16 |
constdefs |
13006 | 17 |
contains_targets :: "[instr list, certificate, method_type, p_count] \<Rightarrow> bool" |
10042 | 18 |
"contains_targets ins cert phi pc == |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
19 |
\<forall>pc' \<in> set (succs (ins!pc) pc). |
13006 | 20 |
pc' \<noteq> pc+1 \<and> pc' < length ins \<longrightarrow> cert!pc' = phi!pc'" |
8388 | 21 |
|
13006 | 22 |
fits :: "[instr list, certificate, method_type] \<Rightarrow> bool" |
23 |
"fits ins cert phi == \<forall>pc. pc < length ins \<longrightarrow> |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
24 |
contains_targets ins cert phi pc \<and> |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
25 |
(cert!pc = None \<or> cert!pc = phi!pc)" |
9012 | 26 |
|
13006 | 27 |
is_target :: "[instr list, p_count] \<Rightarrow> bool" |
10042 | 28 |
"is_target ins pc == |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
29 |
\<exists>pc'. pc \<noteq> pc'+1 \<and> pc' < length ins \<and> pc \<in> set (succs (ins!pc') pc')" |
8388 | 30 |
|
31 |
||
32 |
constdefs |
|
13006 | 33 |
make_cert :: "[instr list, method_type] \<Rightarrow> certificate" |
10042 | 34 |
"make_cert ins phi == |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
35 |
map (\<lambda>pc. if is_target ins pc then phi!pc else None) [0..length ins(]" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
36 |
|
13006 | 37 |
make_Cert :: "[jvm_prog, prog_type] \<Rightarrow> prog_certificate" |
10628 | 38 |
"make_Cert G Phi == \<lambda> C sig. let (C,rT,(maxs,maxl,b)) = the (method (G,C) sig) |
39 |
in make_cert b (Phi C sig)" |
|
8388 | 40 |
|
9559 | 41 |
lemmas [simp del] = split_paired_Ex |
42 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
43 |
lemma make_cert_target: |
13006 | 44 |
"\<lbrakk> pc < length ins; is_target ins pc \<rbrakk> \<Longrightarrow> make_cert ins phi ! pc = phi!pc" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
45 |
by (simp add: make_cert_def) |
9012 | 46 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
47 |
lemma make_cert_approx: |
13006 | 48 |
"\<lbrakk> pc < length ins; make_cert ins phi ! pc \<noteq> phi ! pc \<rbrakk> \<Longrightarrow> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
49 |
make_cert ins phi ! pc = None" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
50 |
by (auto simp add: make_cert_def) |
9012 | 51 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
52 |
lemma make_cert_contains_targets: |
13006 | 53 |
"pc < length ins \<Longrightarrow> contains_targets ins (make_cert ins phi) phi pc" |
11085 | 54 |
proof (unfold contains_targets_def, intro strip, elim conjE) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
55 |
fix pc' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
56 |
assume "pc < length ins" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
57 |
"pc' \<in> set (succs (ins ! pc) pc)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
58 |
"pc' \<noteq> pc+1" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
59 |
pc': "pc' < length ins" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
60 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
61 |
hence "is_target ins pc'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
62 |
by (auto simp add: is_target_def) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
63 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
64 |
with pc' |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
65 |
show "make_cert ins phi ! pc' = phi ! pc'" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
66 |
by (auto intro: make_cert_target) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
67 |
qed |
9012 | 68 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
69 |
theorem fits_make_cert: |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
70 |
"fits ins (make_cert ins phi) phi" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
71 |
by (auto dest: make_cert_approx simp add: fits_def make_cert_contains_targets) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
72 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
73 |
lemma fitsD: |
13006 | 74 |
"\<lbrakk> fits ins cert phi; pc' \<in> set (succs (ins!pc) pc); |
75 |
pc' \<noteq> Suc pc; pc < length ins; pc' < length ins \<rbrakk> |
|
76 |
\<Longrightarrow> cert!pc' = phi!pc'" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
77 |
by (clarsimp simp add: fits_def contains_targets_def) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
78 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
79 |
lemma fitsD2: |
13006 | 80 |
"\<lbrakk> fits ins cert phi; pc < length ins; cert!pc = Some s \<rbrakk> |
81 |
\<Longrightarrow> cert!pc = phi!pc" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
82 |
by (auto simp add: fits_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
83 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
84 |
lemma wtl_inst_mono: |
13006 | 85 |
"\<lbrakk> wtl_inst i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; |
86 |
pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow> |
|
10592 | 87 |
\<exists> s2'. wtl_inst (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
88 |
proof - |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
89 |
assume pc: "pc < length ins" "i = ins!pc" |
10592 | 90 |
assume wtl: "wtl_inst i G rT s1 cert mxs mpc pc = OK s1'" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
91 |
assume fits: "fits ins cert phi" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
92 |
assume G: "G \<turnstile> s2 <=' s1" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
93 |
|
12516 | 94 |
let "?eff s" = "eff i G s" |
9012 | 95 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
96 |
from wtl G |
10592 | 97 |
have app: "app i G mxs rT s2" by (auto simp add: wtl_inst_OK app_mono) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
98 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
99 |
from wtl G |
12516 | 100 |
have eff: "G \<turnstile> ?eff s2 <=' ?eff s1" |
101 |
by (auto intro: eff_mono simp add: wtl_inst_OK) |
|
9012 | 102 |
|
10496 | 103 |
{ also |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
104 |
fix pc' |
10496 | 105 |
assume "pc' \<in> set (succs i pc)" "pc' \<noteq> pc+1" |
106 |
with wtl |
|
12516 | 107 |
have "G \<turnstile> ?eff s1 <=' cert!pc'" |
10496 | 108 |
by (auto simp add: wtl_inst_OK) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
109 |
finally |
12516 | 110 |
have "G\<turnstile> ?eff s2 <=' cert!pc'" . |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
111 |
} note cert = this |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
112 |
|
10592 | 113 |
have "\<exists>s2'. wtl_inst i G rT s2 cert mxs mpc pc = OK s2' \<and> G \<turnstile> s2' <=' s1'" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
114 |
proof (cases "pc+1 \<in> set (succs i pc)") |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
115 |
case True |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
116 |
with wtl |
12516 | 117 |
have s1': "s1' = ?eff s1" by (simp add: wtl_inst_OK) |
9012 | 118 |
|
12516 | 119 |
have "wtl_inst i G rT s2 cert mxs mpc pc = OK (?eff s2) \<and> G \<turnstile> ?eff s2 <=' s1'" |
9580 | 120 |
(is "?wtl \<and> ?G") |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
121 |
proof |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
122 |
from True s1' |
12516 | 123 |
show ?G by (auto intro: eff) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
124 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
125 |
from True app wtl |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
126 |
show ?wtl |
10496 | 127 |
by (clarsimp intro!: cert simp add: wtl_inst_OK) |
9376 | 128 |
qed |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
129 |
thus ?thesis by blast |
9376 | 130 |
next |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
131 |
case False |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
132 |
with wtl |
10496 | 133 |
have "s1' = cert ! Suc pc" by (simp add: wtl_inst_OK) |
9012 | 134 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
135 |
with False app wtl |
10592 | 136 |
have "wtl_inst i G rT s2 cert mxs mpc pc = OK s1' \<and> G \<turnstile> s1' <=' s1'" |
10496 | 137 |
by (clarsimp intro!: cert simp add: wtl_inst_OK) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
138 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
139 |
thus ?thesis by blast |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
140 |
qed |
9012 | 141 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
142 |
with pc show ?thesis by simp |
9376 | 143 |
qed |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
144 |
|
9559 | 145 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
146 |
lemma wtl_cert_mono: |
13006 | 147 |
"\<lbrakk> wtl_cert i G rT s1 cert mxs mpc pc = OK s1'; fits ins cert phi; |
148 |
pc < length ins; G \<turnstile> s2 <=' s1; i = ins!pc \<rbrakk> \<Longrightarrow> |
|
10592 | 149 |
\<exists> s2'. wtl_cert (ins!pc) G rT s2 cert mxs mpc pc = OK s2' \<and> (G \<turnstile> s2' <=' s1')" |
9559 | 150 |
proof - |
10592 | 151 |
assume wtl: "wtl_cert i G rT s1 cert mxs mpc pc = OK s1'" and |
9559 | 152 |
fits: "fits ins cert phi" "pc < length ins" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
153 |
"G \<turnstile> s2 <=' s1" "i = ins!pc" |
9559 | 154 |
|
155 |
show ?thesis |
|
9664 | 156 |
proof (cases (open) "cert!pc") |
9559 | 157 |
case None |
9580 | 158 |
with wtl fits |
159 |
show ?thesis |
|
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
160 |
by - (rule wtl_inst_mono [elim_format], (simp add: wtl_cert_def)+) |
9559 | 161 |
next |
162 |
case Some |
|
9580 | 163 |
with wtl fits |
9559 | 164 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
165 |
have G: "G \<turnstile> s2 <=' (Some a)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
166 |
by - (rule sup_state_opt_trans, auto simp add: wtl_cert_def split: if_splits) |
9559 | 167 |
|
168 |
from Some wtl |
|
10592 | 169 |
have "wtl_inst i G rT (Some a) cert mxs mpc pc = OK s1'" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
170 |
by (simp add: wtl_cert_def split: if_splits) |
9559 | 171 |
|
172 |
with G fits |
|
10592 | 173 |
have "\<exists> s2'. wtl_inst (ins!pc) G rT (Some a) cert mxs mpc pc = OK s2' \<and> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
174 |
(G \<turnstile> s2' <=' s1')" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
175 |
by - (rule wtl_inst_mono, (simp add: wtl_cert_def)+) |
9559 | 176 |
|
9580 | 177 |
with Some G |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
178 |
show ?thesis by (simp add: wtl_cert_def) |
9559 | 179 |
qed |
180 |
qed |
|
181 |
||
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
182 |
|
9012 | 183 |
lemma wt_instr_imp_wtl_inst: |
13006 | 184 |
"\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi; |
185 |
pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> |
|
10592 | 186 |
wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
187 |
proof - |
10592 | 188 |
assume wt: "wt_instr (ins!pc) G rT phi mxs max_pc pc" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
189 |
assume fits: "fits ins cert phi" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
190 |
assume pc: "pc < length ins" "length ins = max_pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
191 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
192 |
from wt |
10592 | 193 |
have app: "app (ins!pc) G mxs rT (phi!pc)" by (simp add: wt_instr_def) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
194 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
195 |
from wt pc |
13006 | 196 |
have pc': "\<And>pc'. pc' \<in> set (succs (ins!pc) pc) \<Longrightarrow> pc' < length ins" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
197 |
by (simp add: wt_instr_def) |
9376 | 198 |
|
12516 | 199 |
let ?s' = "eff (ins!pc) G (phi!pc)" |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
200 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
201 |
from wt fits pc |
13006 | 202 |
have cert: "\<And>pc'. \<lbrakk>pc' \<in> set (succs (ins!pc) pc); pc' < max_pc; pc' \<noteq> pc+1\<rbrakk> |
203 |
\<Longrightarrow> G \<turnstile> ?s' <=' cert!pc'" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
204 |
by (auto dest: fitsD simp add: wt_instr_def) |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
205 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
206 |
from app pc cert pc' |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
207 |
show ?thesis |
10496 | 208 |
by (auto simp add: wtl_inst_OK) |
9376 | 209 |
qed |
9012 | 210 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
211 |
lemma wt_less_wtl: |
13006 | 212 |
"\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; |
10592 | 213 |
wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s; |
13006 | 214 |
fits ins cert phi; Suc pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
215 |
G \<turnstile> s <=' phi ! Suc pc" |
9376 | 216 |
proof - |
10592 | 217 |
assume wt: "wt_instr (ins!pc) G rT phi mxs max_pc pc" |
218 |
assume wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
219 |
assume fits: "fits ins cert phi" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
220 |
assume pc: "Suc pc < length ins" "length ins = max_pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
221 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
222 |
{ assume suc: "Suc pc \<in> set (succs (ins ! pc) pc)" |
12516 | 223 |
with wtl have "s = eff (ins!pc) G (phi!pc)" |
10496 | 224 |
by (simp add: wtl_inst_OK) |
13006 | 225 |
also from suc wt have "G \<turnstile> \<dots> <=' phi!Suc pc" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
226 |
by (simp add: wt_instr_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
227 |
finally have ?thesis . |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
228 |
} |
9012 | 229 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
230 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
231 |
{ assume "Suc pc \<notin> set (succs (ins ! pc) pc)" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
232 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
233 |
with wtl |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
234 |
have "s = cert!Suc pc" |
10496 | 235 |
by (simp add: wtl_inst_OK) |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
236 |
with fits pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
237 |
have ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
238 |
by - (cases "cert!Suc pc", simp, drule fitsD2, assumption+, simp) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
239 |
} |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
240 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
241 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
242 |
show ?thesis by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
243 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
244 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
245 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
246 |
lemma wt_instr_imp_wtl_cert: |
13006 | 247 |
"\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; fits ins cert phi; |
248 |
pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> |
|
10592 | 249 |
wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
250 |
proof - |
10592 | 251 |
assume "wt_instr (ins!pc) G rT phi mxs max_pc pc" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
252 |
fits: "fits ins cert phi" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
253 |
pc: "pc < length ins" and |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
254 |
"length ins = max_pc" |
9012 | 255 |
|
10592 | 256 |
hence wtl: "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc \<noteq> Err" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
257 |
by (rule wt_instr_imp_wtl_inst) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
258 |
|
13006 | 259 |
hence "cert!pc = None \<Longrightarrow> ?thesis" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
260 |
by (simp add: wtl_cert_def) |
9012 | 261 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
262 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
263 |
{ fix s |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
264 |
assume c: "cert!pc = Some s" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
265 |
with fits pc |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
266 |
have "cert!pc = phi!pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
267 |
by (rule fitsD2) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
268 |
from this c wtl |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
269 |
have ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
270 |
by (clarsimp simp add: wtl_cert_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
271 |
} |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
272 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
273 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
274 |
show ?thesis by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
275 |
qed |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
276 |
|
9012 | 277 |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
278 |
lemma wt_less_wtl_cert: |
13006 | 279 |
"\<lbrakk> wt_instr (ins!pc) G rT phi mxs max_pc pc; |
10592 | 280 |
wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s; |
13006 | 281 |
fits ins cert phi; Suc pc < length ins; length ins = max_pc \<rbrakk> \<Longrightarrow> |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
282 |
G \<turnstile> s <=' phi ! Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
283 |
proof - |
10592 | 284 |
assume wtl: "wtl_cert (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
285 |
|
10592 | 286 |
assume wti: "wt_instr (ins!pc) G rT phi mxs max_pc pc" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
287 |
"fits ins cert phi" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
288 |
"Suc pc < length ins" "length ins = max_pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
289 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
290 |
{ assume "cert!pc = None" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
291 |
with wtl |
10592 | 292 |
have "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
293 |
by (simp add: wtl_cert_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
294 |
with wti |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
295 |
have ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
296 |
by - (rule wt_less_wtl) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
297 |
} |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
298 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
299 |
{ fix t |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
300 |
assume c: "cert!pc = Some t" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
301 |
with wti |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
302 |
have "cert!pc = phi!pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
303 |
by - (rule fitsD2, simp+) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
304 |
with c wtl |
10592 | 305 |
have "wtl_inst (ins!pc) G rT (phi!pc) cert mxs max_pc pc = OK s" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
306 |
by (simp add: wtl_cert_def) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
307 |
with wti |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
308 |
have ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
309 |
by - (rule wt_less_wtl) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
310 |
} |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
311 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
312 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
313 |
show ?thesis by blast |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
314 |
qed |
9012 | 315 |
|
9559 | 316 |
text {* |
317 |
\medskip |
|
318 |
Main induction over the instruction list. |
|
319 |
*} |
|
9012 | 320 |
|
321 |
theorem wt_imp_wtl_inst_list: |
|
13006 | 322 |
"\<forall> pc. (\<forall>pc'. pc' < length all_ins \<longrightarrow> |
323 |
wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc') \<longrightarrow> |
|
324 |
fits all_ins cert phi \<longrightarrow> |
|
325 |
(\<exists>l. pc = length l \<and> all_ins = l@ins) \<longrightarrow> |
|
326 |
pc < length all_ins \<longrightarrow> |
|
327 |
(\<forall> s. (G \<turnstile> s <=' (phi!pc)) \<longrightarrow> |
|
10592 | 328 |
wtl_inst_list ins G rT cert mxs (length all_ins) pc s \<noteq> Err)" |
13006 | 329 |
(is "\<forall>pc. ?wt \<longrightarrow> ?fits \<longrightarrow> ?l pc ins \<longrightarrow> ?len pc \<longrightarrow> ?wtl pc ins" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
330 |
is "\<forall>pc. ?C pc ins" is "?P ins") |
9559 | 331 |
proof (induct "?P" "ins") |
332 |
case Nil |
|
333 |
show "?P []" by simp |
|
334 |
next |
|
335 |
fix i ins' |
|
336 |
assume Cons: "?P ins'" |
|
9012 | 337 |
|
9559 | 338 |
show "?P (i#ins')" |
339 |
proof (intro allI impI, elim exE conjE) |
|
340 |
fix pc s l |
|
13006 | 341 |
assume wt : "\<forall>pc'. pc' < length all_ins \<longrightarrow> |
10592 | 342 |
wt_instr (all_ins ! pc') G rT phi mxs (length all_ins) pc'" |
9559 | 343 |
assume fits: "fits all_ins cert phi" |
344 |
assume l : "pc < length all_ins" |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
345 |
assume G : "G \<turnstile> s <=' phi ! pc" |
9559 | 346 |
assume pc : "all_ins = l@i#ins'" "pc = length l" |
347 |
hence i : "all_ins ! pc = i" |
|
348 |
by (simp add: nth_append) |
|
9012 | 349 |
|
9559 | 350 |
from l wt |
10592 | 351 |
have wti: "wt_instr (all_ins!pc) G rT phi mxs (length all_ins) pc" by blast |
9012 | 352 |
|
9559 | 353 |
with fits l |
10592 | 354 |
have c: "wtl_cert (all_ins!pc) G rT (phi!pc) cert mxs (length all_ins) pc \<noteq> Err" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
355 |
by - (drule wt_instr_imp_wtl_cert, auto) |
9559 | 356 |
|
357 |
from Cons |
|
358 |
have "?C (Suc pc) ins'" by blast |
|
359 |
with wt fits pc |
|
13006 | 360 |
have IH: "?len (Suc pc) \<longrightarrow> ?wtl (Suc pc) ins'" by auto |
9012 | 361 |
|
10592 | 362 |
show "wtl_inst_list (i#ins') G rT cert mxs (length all_ins) pc s \<noteq> Err" |
9559 | 363 |
proof (cases "?len (Suc pc)") |
364 |
case False |
|
365 |
with pc |
|
366 |
have "ins' = []" by simp |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
367 |
with G i c fits l |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
368 |
show ?thesis by (auto dest: wtl_cert_mono) |
9559 | 369 |
next |
370 |
case True |
|
371 |
with IH |
|
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
372 |
have wtl: "?wtl (Suc pc) ins'" by blast |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
373 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
374 |
from c wti fits l True |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
375 |
obtain s'' where |
10592 | 376 |
"wtl_cert (all_ins!pc) G rT (phi!pc) cert mxs (length all_ins) pc = OK s''" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
377 |
"G \<turnstile> s'' <=' phi ! Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
378 |
by clarsimp (drule wt_less_wtl_cert, auto) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
379 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
380 |
from calculation fits G l |
9559 | 381 |
obtain s' where |
10592 | 382 |
c': "wtl_cert (all_ins!pc) G rT s cert mxs (length all_ins) pc = OK s'" and |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
383 |
"G \<turnstile> s' <=' s''" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
384 |
by - (drule wtl_cert_mono, auto) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
385 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
386 |
have G': "G \<turnstile> s' <=' phi ! Suc pc" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
387 |
by - (rule sup_state_opt_trans) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
388 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
389 |
with wtl |
10592 | 390 |
have "wtl_inst_list ins' G rT cert mxs (length all_ins) (Suc pc) s' \<noteq> Err" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
391 |
by auto |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
392 |
|
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
393 |
with i c' |
9559 | 394 |
show ?thesis by auto |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
395 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
396 |
qed |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
397 |
qed |
9559 | 398 |
|
9012 | 399 |
|
400 |
lemma fits_imp_wtl_method_complete: |
|
13006 | 401 |
"\<lbrakk> wt_method G C pTs rT mxs mxl ins phi; fits ins cert phi \<rbrakk> |
402 |
\<Longrightarrow> wtl_method G C pTs rT mxs mxl ins cert" |
|
9594 | 403 |
by (simp add: wt_method_def wtl_method_def) |
9941
fe05af7ec816
renamed atts: rulify to rule_format, elimify to elim_format;
wenzelm
parents:
9906
diff
changeset
|
404 |
(rule wt_imp_wtl_inst_list [rule_format, elim_format], auto simp add: wt_start_def) |
9012 | 405 |
|
406 |
||
407 |
lemma wtl_method_complete: |
|
10592 | 408 |
"wt_method G C pTs rT mxs mxl ins phi |
13006 | 409 |
\<Longrightarrow> wtl_method G C pTs rT mxs mxl ins (make_cert ins phi)" |
9580 | 410 |
proof - |
10592 | 411 |
assume "wt_method G C pTs rT mxs mxl ins phi" |
9757
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
412 |
moreover |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
413 |
have "fits ins (make_cert ins phi) phi" |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
414 |
by (rule fits_make_cert) |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
415 |
ultimately |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
416 |
show ?thesis |
1024a2d80ac0
functional LBV style, dead code, type safety -> Isar
kleing
parents:
9664
diff
changeset
|
417 |
by (rule fits_imp_wtl_method_complete) |
9580 | 418 |
qed |
9012 | 419 |
|
420 |
||
10628 | 421 |
theorem wtl_complete: |
13006 | 422 |
"wt_jvm_prog G Phi \<Longrightarrow> wtl_jvm_prog G (make_Cert G Phi)" |
10628 | 423 |
proof - |
424 |
assume wt: "wt_jvm_prog G Phi" |
|
425 |
||
426 |
{ fix C S fs mdecls sig rT code |
|
427 |
assume "(C,S,fs,mdecls) \<in> set G" "(sig,rT,code) \<in> set mdecls" |
|
428 |
moreover |
|
429 |
from wt obtain wf_mb where "wf_prog wf_mb G" |
|
430 |
by (blast dest: wt_jvm_progD) |
|
431 |
ultimately |
|
432 |
have "method (G,C) sig = Some (C,rT,code)" |
|
433 |
by (simp add: methd) |
|
434 |
} note this [simp] |
|
435 |
||
436 |
from wt |
|
437 |
show ?thesis |
|
438 |
apply (clarsimp simp add: wt_jvm_prog_def wtl_jvm_prog_def wf_prog_def wf_cdecl_def) |
|
439 |
apply (drule bspec, assumption) |
|
440 |
apply (clarsimp simp add: wf_mdecl_def) |
|
441 |
apply (drule bspec, assumption) |
|
442 |
apply (clarsimp simp add: make_Cert_def) |
|
443 |
apply (clarsimp dest!: wtl_method_complete) |
|
444 |
done |
|
10592 | 445 |
|
10628 | 446 |
qed |
447 |
||
9559 | 448 |
lemmas [simp] = split_paired_Ex |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
449 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
450 |
end |