author | kleing |
Mon, 07 Aug 2000 14:32:56 +0200 | |
changeset 9549 | 40d64cb4f4e6 |
parent 9376 | c32c5696ec2a |
child 9664 | 4cae97480a6d |
permissions | -rw-r--r-- |
8245 | 1 |
(* Title: HOL/MicroJava/BV/BVLightSpec.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gerwin Klein |
|
4 |
Copyright 1999 Technische Universitaet Muenchen |
|
9054 | 5 |
*) |
8245 | 6 |
|
9054 | 7 |
header {* Specification of the LBV *} |
8 |
||
8245 | 9 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
10 |
theory LBVSpec = Step : |
8245 | 11 |
|
12 |
types |
|
13 |
certificate = "state_type option list" |
|
14 |
class_certificate = "sig \\<Rightarrow> certificate" |
|
9183 | 15 |
prog_certificate = "cname \\<Rightarrow> class_certificate" |
8245 | 16 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
17 |
constdefs |
9376 | 18 |
wtl_inst :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool" |
19 |
||
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
20 |
"wtl_inst i G rT s s' cert max_pc pc \\<equiv> app (i,G,rT,s) \\<and> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
21 |
(let s'' = the (step (i,G,s)) in |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
22 |
(\\<forall> pc' \\<in> (succs i pc). pc' < max_pc \\<and> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
23 |
((pc' \\<noteq> pc+1) \\<longrightarrow> cert!pc' \\<noteq> None \\<and> G \\<turnstile> s'' <=s the (cert!pc'))) \\<and> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
24 |
(if (pc+1) \\<in> (succs i pc) then |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
25 |
s' = s'' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
26 |
else |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
27 |
cert ! (pc+1) = Some s'))" |
8245 | 28 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
29 |
lemma [simp]: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
30 |
"succs i pc = {pc+1} \\<Longrightarrow> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
31 |
wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> pc+1 < max_pc \\<and> (s' = the (step (i,G,s))))" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
32 |
by (unfold wtl_inst_def, auto) |
9376 | 33 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
34 |
lemma [simp]: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
35 |
"succs i pc = {} \\<Longrightarrow> wtl_inst i G rT s s' cert max_pc pc = (app (i,G,rT,s) \\<and> cert!(pc+1) = Some s')" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
36 |
by (unfold wtl_inst_def, auto) |
8245 | 37 |
|
38 |
||
39 |
constdefs |
|
40 |
wtl_inst_option :: "[instr,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool" |
|
41 |
"wtl_inst_option i G rT s0 s1 cert max_pc pc \\<equiv> |
|
42 |
(case cert!pc of |
|
43 |
None \\<Rightarrow> wtl_inst i G rT s0 s1 cert max_pc pc |
|
44 |
| Some s0' \\<Rightarrow> (G \\<turnstile> s0 <=s s0') \\<and> |
|
9183 | 45 |
wtl_inst i G rT s0' s1 cert max_pc pc)" |
8245 | 46 |
|
47 |
consts |
|
9183 | 48 |
wtl_inst_list :: "[instr list,jvm_prog,ty,state_type,state_type,certificate,p_count,p_count] \\<Rightarrow> bool" |
8245 | 49 |
primrec |
50 |
"wtl_inst_list [] G rT s0 s2 cert max_pc pc = (s0 = s2)" |
|
51 |
||
52 |
"wtl_inst_list (instr#is) G rT s0 s2 cert max_pc pc = |
|
53 |
(\\<exists>s1. wtl_inst_option instr G rT s0 s1 cert max_pc pc \\<and> |
|
9183 | 54 |
wtl_inst_list is G rT s1 s2 cert max_pc (pc+1))" |
8245 | 55 |
|
56 |
constdefs |
|
57 |
wtl_method :: "[jvm_prog,cname,ty list,ty,nat,instr list,certificate] \\<Rightarrow> bool" |
|
58 |
"wtl_method G C pTs rT mxl ins cert \\<equiv> |
|
59 |
let max_pc = length ins |
|
60 |
in |
|
61 |
0 < max_pc \\<and> |
|
62 |
(\\<exists>s2. wtl_inst_list ins G rT |
|
63 |
([],(Some(Class C))#((map Some pTs))@(replicate mxl None)) |
|
64 |
s2 cert max_pc 0)" |
|
65 |
||
9012 | 66 |
wtl_jvm_prog :: "[jvm_prog,prog_certificate] \\<Rightarrow> bool" |
8245 | 67 |
"wtl_jvm_prog G cert \\<equiv> |
68 |
wf_prog (\\<lambda>G C (sig,rT,maxl,b). |
|
9183 | 69 |
wtl_method G C (snd sig) rT maxl b (cert C sig)) G" |
9012 | 70 |
|
9054 | 71 |
text {* \medskip *} |
72 |
||
9183 | 73 |
lemma rev_eq: "\\<lbrakk>length a = n; length x = n; rev a @ b # c = rev x @ y # z\\<rbrakk> \\<Longrightarrow> a = x \\<and> b = y \\<and> c = z" |
74 |
by auto |
|
9012 | 75 |
|
76 |
lemma wtl_inst_unique: |
|
77 |
"wtl_inst i G rT s0 s1 cert max_pc pc \\<longrightarrow> |
|
9183 | 78 |
wtl_inst i G rT s0 s1' cert max_pc pc \\<longrightarrow> s1 = s1'" (is "?P i") |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
79 |
by (unfold wtl_inst_def, auto) |
9012 | 80 |
|
81 |
lemma wtl_inst_option_unique: |
|
82 |
"\\<lbrakk>wtl_inst_option i G rT s0 s1 cert max_pc pc; |
|
9183 | 83 |
wtl_inst_option i G rT s0 s1' cert max_pc pc\\<rbrakk> \\<Longrightarrow> s1 = s1'" |
84 |
by (cases "cert!pc") (auto simp add: wtl_inst_unique wtl_inst_option_def) |
|
9012 | 85 |
|
86 |
lemma wtl_inst_list_unique: |
|
87 |
"\\<forall> s0 pc. wtl_inst_list is G rT s0 s1 cert max_pc pc \\<longrightarrow> |
|
9183 | 88 |
wtl_inst_list is G rT s0 s1' cert max_pc pc \\<longrightarrow> s1=s1'" (is "?P is") |
89 |
proof (induct "?P" "is") |
|
90 |
case Nil |
|
91 |
show "?P []" by simp |
|
8245 | 92 |
|
9183 | 93 |
case Cons |
94 |
show "?P (a # list)" |
|
95 |
proof intro |
|
96 |
fix s0 fix pc |
|
97 |
let "?o s0 s1" = "wtl_inst_option a G rT s0 s1 cert max_pc pc" |
|
98 |
let "?l l s1 s2 pc" = "wtl_inst_list l G rT s1 s2 cert max_pc pc" |
|
99 |
assume a: "?l (a#list) s0 s1 pc" |
|
100 |
assume b: "?l (a#list) s0 s1' pc" |
|
101 |
with a |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
102 |
obtain s s' where "?o s0 s" "?o s0 s'" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
103 |
and l: "?l list s s1 (Suc pc)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
104 |
and l': "?l list s' s1' (Suc pc)" by auto |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
105 |
|
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
106 |
have "s=s'" by(rule wtl_inst_option_unique) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
107 |
with l l' Cons |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
108 |
show "s1 = s1'" by blast |
9183 | 109 |
qed |
110 |
qed |
|
9012 | 111 |
|
112 |
lemma wtl_partial: |
|
113 |
"\\<forall> pc' pc s. |
|
114 |
wtl_inst_list is G rT s s' cert mpc pc \\<longrightarrow> \ |
|
115 |
pc' < length is \\<longrightarrow> \ |
|
116 |
(\\<exists> a b s1. a @ b = is \\<and> length a = pc' \\<and> \ |
|
117 |
wtl_inst_list a G rT s s1 cert mpc pc \\<and> \ |
|
9183 | 118 |
wtl_inst_list b G rT s1 s' cert mpc (pc+length a))" (is "?P is") |
119 |
proof (induct "?P" "is") |
|
120 |
case Nil |
|
121 |
show "?P []" by auto |
|
9012 | 122 |
|
9183 | 123 |
case Cons |
124 |
show "?P (a#list)" |
|
125 |
proof (intro allI impI) |
|
126 |
fix pc' pc s |
|
127 |
assume length: "pc' < length (a # list)" |
|
128 |
assume wtl: "wtl_inst_list (a # list) G rT s s' cert mpc pc" |
|
9012 | 129 |
show "\\<exists> a' b s1. |
130 |
a' @ b = a#list \\<and> length a' = pc' \\<and> \ |
|
131 |
wtl_inst_list a' G rT s s1 cert mpc pc \\<and> \ |
|
132 |
wtl_inst_list b G rT s1 s' cert mpc (pc+length a')" |
|
9183 | 133 |
(is "\\<exists> a b s1. ?E a b s1") |
134 |
proof (cases "pc'") |
|
135 |
case 0 |
|
136 |
with wtl |
|
137 |
have "?E [] (a#list) s" by simp |
|
138 |
thus ?thesis by blast |
|
139 |
next |
|
140 |
case Suc |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
141 |
with wtl |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
142 |
obtain s0 where wtlSuc: "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
143 |
and wtlOpt: "wtl_inst_option a G rT s s0 cert mpc pc" by auto |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
144 |
from Cons |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
145 |
obtain a' b s1' |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
146 |
where "a' @ b = list" "length a' = nat" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
147 |
and w:"wtl_inst_list a' G rT s0 s1' cert mpc (Suc pc)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
148 |
and "wtl_inst_list b G rT s1' s' cert mpc (Suc pc + length a')" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
149 |
proof (elim allE impE) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
150 |
from length Suc show "nat < length list" by simp |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
151 |
from wtlSuc show "wtl_inst_list list G rT s0 s' cert mpc (Suc pc)" . |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
152 |
qed (elim exE conjE, auto) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
153 |
with Suc wtlOpt |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
154 |
have "?E (a#a') b s1'" by (auto simp del: split_paired_Ex) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
155 |
thus ?thesis by blast |
9183 | 156 |
qed |
157 |
qed |
|
158 |
qed |
|
9012 | 159 |
|
160 |
lemma "wtl_append1": |
|
161 |
"\\<lbrakk>wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0; |
|
162 |
wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)\\<rbrakk> \\<Longrightarrow> |
|
9183 | 163 |
wtl_inst_list (x@y) G rT s0 s2 cert (length (x@y)) 0" |
164 |
proof - |
|
9012 | 165 |
assume w: |
166 |
"wtl_inst_list x G rT s0 s1 cert (length (x@y)) 0" |
|
9183 | 167 |
"wtl_inst_list y G rT s1 s2 cert (length (x@y)) (length x)" |
9012 | 168 |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
169 |
have |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
170 |
"\\<forall> pc s0. |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
171 |
wtl_inst_list x G rT s0 s1 cert (pc+length (x@y)) pc \\<longrightarrow> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
172 |
wtl_inst_list y G rT s1 s2 cert (pc+length (x@y)) (pc+length x) \\<longrightarrow> |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
173 |
wtl_inst_list (x@y) G rT s0 s2 cert (pc+length (x@y)) pc" (is "?P x") |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
174 |
proof (induct "?P" "x") |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
175 |
case Nil |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
176 |
show "?P []" by simp |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
177 |
next |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
178 |
case Cons |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
179 |
show "?P (a#list)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
180 |
proof intro |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
181 |
fix pc s0 |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
182 |
assume y: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
183 |
"wtl_inst_list y G rT s1 s2 cert (pc + length ((a # list) @ y)) (pc + length (a # list))" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
184 |
assume al: |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
185 |
"wtl_inst_list (a # list) G rT s0 s1 cert (pc + length ((a # list) @ y)) pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
186 |
from this |
9012 | 187 |
obtain s' where |
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
188 |
a: "wtl_inst_option a G rT s0 s' cert (Suc pc + length (list@y)) pc" and |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
189 |
l: "wtl_inst_list list G rT s' s1 cert (Suc pc + length (list@y)) (Suc pc)" by auto |
9183 | 190 |
with y Cons |
191 |
have "wtl_inst_list (list @ y) G rT s' s2 cert (Suc pc + length (list @ y)) (Suc pc)" |
|
192 |
by (elim allE impE) (assumption, simp+) |
|
193 |
with a |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
194 |
show "wtl_inst_list ((a # list) @ y) G rT s0 s2 cert (pc + length ((a # list) @ y)) pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
195 |
by (auto simp del: split_paired_Ex) |
9183 | 196 |
qed |
197 |
qed |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
198 |
|
9183 | 199 |
with w |
200 |
show ?thesis |
|
201 |
proof (elim allE impE) |
|
202 |
from w show "wtl_inst_list x G rT s0 s1 cert (0+length (x @ y)) 0" by simp |
|
203 |
qed simp+ |
|
204 |
qed |
|
9012 | 205 |
|
206 |
lemma wtl_cons_appendl: |
|
207 |
"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; |
|
208 |
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); |
|
209 |
wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow> |
|
9183 | 210 |
wtl_inst_list (a@i#b) G rT s0 s3 cert (length (a@i#b)) 0" |
211 |
proof - |
|
212 |
assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0" |
|
9012 | 213 |
|
214 |
assume "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)" |
|
9183 | 215 |
"wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))" |
9012 | 216 |
|
9183 | 217 |
hence "wtl_inst_list (i#b) G rT s1 s3 cert (length (a@i#b)) (length a)" |
218 |
by (auto simp del: split_paired_Ex) |
|
9012 | 219 |
|
9183 | 220 |
with a |
221 |
show ?thesis by (rule wtl_append1) |
|
222 |
qed |
|
9012 | 223 |
|
224 |
lemma "wtl_append": |
|
225 |
"\\<lbrakk>wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0; |
|
226 |
wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a); |
|
227 |
wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))\\<rbrakk> \\<Longrightarrow> |
|
9183 | 228 |
wtl_inst_list (a@[i]) G rT s0 s2 cert (length (a@i#b)) 0" |
229 |
proof - |
|
230 |
assume a: "wtl_inst_list a G rT s0 s1 cert (length (a@i#b)) 0" |
|
231 |
assume i: "wtl_inst_option i G rT s1 s2 cert (length (a@i#b)) (length a)" |
|
232 |
assume b: "wtl_inst_list b G rT s2 s3 cert (length (a@i#b)) (Suc (length a))" |
|
9012 | 233 |
|
234 |
have "\\<forall> s0 pc. wtl_inst_list a G rT s0 s1 cert (pc+length (a@i#b)) pc \\<longrightarrow> |
|
235 |
wtl_inst_option i G rT s1 s2 cert (pc+length (a@i#b)) (pc + length a) \\<longrightarrow> |
|
236 |
wtl_inst_list b G rT s2 s3 cert (pc+length (a@i#b)) (Suc pc + length a) \\<longrightarrow> |
|
9183 | 237 |
wtl_inst_list (a@[i]) G rT s0 s2 cert (pc+length (a@i#b)) pc" (is "?P a") |
238 |
proof (induct "?P" "a") |
|
239 |
case Nil |
|
240 |
show "?P []" by (simp del: split_paired_Ex) |
|
241 |
case Cons |
|
242 |
show "?P (a#list)" (is "\\<forall>s0 pc. ?x s0 pc \\<longrightarrow> ?y s0 pc \\<longrightarrow> ?z s0 pc \\<longrightarrow> ?p s0 pc") |
|
243 |
proof intro |
|
244 |
fix s0 pc |
|
245 |
assume y: "?y s0 pc" |
|
246 |
assume z: "?z s0 pc" |
|
247 |
assume "?x s0 pc" |
|
9549
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
248 |
from this |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
249 |
obtain s0' where opt: "wtl_inst_option a G rT s0 s0' cert (pc + length ((a # list) @ i # b)) pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
250 |
and list: "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
251 |
by (auto simp del: split_paired_Ex) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
252 |
with y z Cons |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
253 |
have "wtl_inst_list (list @ [i]) G rT s0' s2 cert (Suc pc + length (list @ i # b)) (Suc pc)" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
254 |
proof (elim allE impE) |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
255 |
from list show "wtl_inst_list list G rT s0' s1 cert (Suc pc + length (list @ i # b)) (Suc pc)" . |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
256 |
qed auto |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
257 |
with opt |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
258 |
show "?p s0 pc" |
40d64cb4f4e6
BV and LBV specified in terms of app and step functions
kleing
parents:
9376
diff
changeset
|
259 |
by (auto simp del: split_paired_Ex) |
9183 | 260 |
qed |
261 |
qed |
|
262 |
with a i b |
|
263 |
show ?thesis |
|
264 |
proof (elim allE impE) |
|
265 |
from a show "wtl_inst_list a G rT s0 s1 cert (0+length (a@i#b)) 0" by simp |
|
266 |
qed auto |
|
267 |
qed |
|
9012 | 268 |
|
9183 | 269 |
end |