15 | "code (Right v) = S # (code v)" |
15 | "code (Right v) = S # (code v)" |
16 | "code (Seq v1 v2) = (code v1) @ (code v2)" |
16 | "code (Seq v1 v2) = (code v1) @ (code v2)" |
17 | "code (Stars []) = [S]" |
17 | "code (Stars []) = [S]" |
18 | "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)" |
18 | "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)" |
19 |
19 |
|
20 fun sz where |
|
21 "sz ZERO = 0" |
|
22 | "sz ONE = 0" |
|
23 | "sz (CH _) = 0" |
|
24 | "sz (SEQ r1 r2) = 1 + sz r1 + sz r2" |
|
25 | "sz (ALT r1 r2) = 1 + sz r1 + sz r2" |
|
26 | "sz (STAR r) = 1 + sz r" |
|
27 | "sz (NTIMES r n) = 1 + n + sz r" |
|
28 |
20 |
29 |
21 fun |
30 fun |
22 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
31 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
23 where |
32 where |
24 "Stars_add v (Stars vs) = Stars (v # vs)" |
33 "Stars_add v (Stars vs) = Stars (v # vs)" |
25 |
34 |
26 function |
35 function (sequential) |
27 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
36 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
28 where |
37 where |
29 "decode' bs ZERO = (undefined, bs)" |
38 "decode' bs ZERO = (undefined, bs)" |
30 | "decode' bs ONE = (Void, bs)" |
39 | "decode' bs ONE = (Void, bs)" |
31 | "decode' bs (CH d) = (Char d, bs)" |
40 | "decode' bs (CH d) = (Char d, bs)" |
37 | "decode' [] (STAR r) = (Void, [])" |
46 | "decode' [] (STAR r) = (Void, [])" |
38 | "decode' (S # bs) (STAR r) = (Stars [], bs)" |
47 | "decode' (S # bs) (STAR r) = (Stars [], bs)" |
39 | "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in |
48 | "decode' (Z # bs) (STAR r) = (let (v, bs') = decode' bs r in |
40 let (vs, bs'') = decode' bs' (STAR r) |
49 let (vs, bs'') = decode' bs' (STAR r) |
41 in (Stars_add v vs, bs''))" |
50 in (Stars_add v vs, bs''))" |
|
51 | "decode' [] (NTIMES r n) = (Void, [])" |
|
52 | "decode' (S # bs) (NTIMES r n) = (Stars [], bs)" |
|
53 (*| "decode' (Z # bs) (NTIMES r 0) = (undefined, bs)"*) |
|
54 | "decode' (Z # bs) (NTIMES r n) = (let (v, bs') = decode' bs r in |
|
55 let (vs, bs'') = decode' bs' (NTIMES r (n - 1)) |
|
56 in (Stars_add v vs, bs''))" |
42 by pat_completeness auto |
57 by pat_completeness auto |
43 |
58 |
44 lemma decode'_smaller: |
59 lemma decode'_smaller: |
45 assumes "decode'_dom (bs, r)" |
60 assumes "decode'_dom (bs, r)" |
46 shows "length (snd (decode' bs r)) \<le> length bs" |
61 shows "length (snd (decode' bs r)) \<le> length bs" |
47 using assms |
62 using assms |
48 apply(induct bs r) |
63 apply(induct bs r) |
49 apply(auto simp add: decode'.psimps split: prod.split) |
64 apply(auto simp add: decode'.psimps split: prod.split) |
50 using dual_order.trans apply blast |
65 using dual_order.trans apply blast |
51 by (meson dual_order.trans le_SucI) |
66 apply (meson dual_order.trans le_SucI) |
|
67 apply (meson le_SucI le_trans) |
|
68 done |
52 |
69 |
53 termination "decode'" |
70 termination "decode'" |
54 apply(relation "inv_image (measure(%cs. size cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") |
71 apply(relation "inv_image (measure(%cs. sz cs) <*lex*> measure(%s. size s)) (%(ds,r). (r,ds))") |
55 apply(auto dest!: decode'_smaller) |
72 apply(auto dest!: decode'_smaller) |
56 by (metis less_Suc_eq_le snd_conv) |
73 apply (metis less_Suc_eq_le snd_conv) |
|
74 by (metis less_Suc_eq_le snd_conv) |
57 |
75 |
58 definition |
76 definition |
59 decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option" |
77 decode :: "bit list \<Rightarrow> rexp \<Rightarrow> val option" |
60 where |
78 where |
61 "decode ds r \<equiv> (let (v, ds') = decode' ds r |
79 "decode ds r \<equiv> (let (v, ds') = decode' ds r |
66 shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)" |
84 shows "decode' (code (Stars vs) @ ds) (STAR r) = (Stars vs, ds)" |
67 using assms |
85 using assms |
68 apply(induct vs) |
86 apply(induct vs) |
69 apply(auto) |
87 apply(auto) |
70 done |
88 done |
|
89 |
|
90 lemma decode'_code_NTIMES: |
|
91 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> (\<forall>x. decode' (code v @ x) r = (v, x))" |
|
92 shows "decode' (code (Stars vs) @ ds) (NTIMES r n) = (Stars vs, ds)" |
|
93 using assms |
|
94 apply(induct vs arbitrary: n r ds) |
|
95 apply(auto) |
|
96 done |
|
97 |
71 |
98 |
72 lemma decode'_code: |
99 lemma decode'_code: |
73 assumes "\<Turnstile> v : r" |
100 assumes "\<Turnstile> v : r" |
74 shows "decode' ((code v) @ ds) r = (v, ds)" |
101 shows "decode' ((code v) @ ds) r = (v, ds)" |
75 using assms |
102 using assms |
76 apply(induct v r arbitrary: ds) |
103 apply(induct v r arbitrary: ds) |
77 apply(auto) |
104 apply(auto) |
78 using decode'_code_Stars by blast |
105 using decode'_code_Stars apply blast |
|
106 by (metis Un_iff decode'_code_NTIMES set_append) |
79 |
107 |
80 lemma decode_code: |
108 lemma decode_code: |
81 assumes "\<Turnstile> v : r" |
109 assumes "\<Turnstile> v : r" |
82 shows "decode (code v) r = Some v" |
110 shows "decode (code v) r = Some v" |
83 using assms unfolding decode_def |
111 using assms unfolding decode_def |
91 | AONE "bit list" |
119 | AONE "bit list" |
92 | ACHAR "bit list" char |
120 | ACHAR "bit list" char |
93 | ASEQ "bit list" arexp arexp |
121 | ASEQ "bit list" arexp arexp |
94 | AALTs "bit list" "arexp list" |
122 | AALTs "bit list" "arexp list" |
95 | ASTAR "bit list" arexp |
123 | ASTAR "bit list" arexp |
|
124 | ANTIMES "bit list" arexp nat |
96 |
125 |
97 abbreviation |
126 abbreviation |
98 "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]" |
127 "AALT bs r1 r2 \<equiv> AALTs bs [r1, r2]" |
99 |
128 |
100 fun asize :: "arexp \<Rightarrow> nat" where |
129 fun asize :: "arexp \<Rightarrow> nat" where |
102 | "asize (AONE cs) = 1" |
131 | "asize (AONE cs) = 1" |
103 | "asize (ACHAR cs c) = 1" |
132 | "asize (ACHAR cs c) = 1" |
104 | "asize (AALTs cs rs) = Suc (sum_list (map asize rs))" |
133 | "asize (AALTs cs rs) = Suc (sum_list (map asize rs))" |
105 | "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)" |
134 | "asize (ASEQ cs r1 r2) = Suc (asize r1 + asize r2)" |
106 | "asize (ASTAR cs r) = Suc (asize r)" |
135 | "asize (ASTAR cs r) = Suc (asize r)" |
|
136 | "asize (ANTIMES cs r n) = Suc (asize r) + n" |
107 |
137 |
108 fun |
138 fun |
109 erase :: "arexp \<Rightarrow> rexp" |
139 erase :: "arexp \<Rightarrow> rexp" |
110 where |
140 where |
111 "erase AZERO = ZERO" |
141 "erase AZERO = ZERO" |
114 | "erase (AALTs _ []) = ZERO" |
144 | "erase (AALTs _ []) = ZERO" |
115 | "erase (AALTs _ [r]) = (erase r)" |
145 | "erase (AALTs _ [r]) = (erase r)" |
116 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" |
146 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" |
117 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
147 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
118 | "erase (ASTAR _ r) = STAR (erase r)" |
148 | "erase (ASTAR _ r) = STAR (erase r)" |
|
149 | "erase (ANTIMES _ r n) = NTIMES (erase r) n" |
119 |
150 |
120 |
151 |
121 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
152 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
122 "fuse bs AZERO = AZERO" |
153 "fuse bs AZERO = AZERO" |
123 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
154 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
124 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" |
155 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" |
125 | "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs" |
156 | "fuse bs (AALTs cs rs) = AALTs (bs @ cs) rs" |
126 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" |
157 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" |
127 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
158 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
|
159 | "fuse bs (ANTIMES cs r n) = ANTIMES (bs @ cs) r n" |
128 |
160 |
129 lemma fuse_append: |
161 lemma fuse_append: |
130 shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)" |
162 shows "fuse (bs1 @ bs2) r = fuse bs1 (fuse bs2 r)" |
131 apply(induct r) |
163 apply(induct r) |
132 apply(auto) |
164 apply(auto) |
139 | "intern (CH c) = ACHAR [] c" |
171 | "intern (CH c) = ACHAR [] c" |
140 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
172 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
141 (fuse [S] (intern r2))" |
173 (fuse [S] (intern r2))" |
142 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
174 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
143 | "intern (STAR r) = ASTAR [] (intern r)" |
175 | "intern (STAR r) = ASTAR [] (intern r)" |
|
176 | "intern (NTIMES r n) = ANTIMES [] (intern r) n" |
144 |
177 |
145 |
178 |
146 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
179 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
147 "retrieve (AONE bs) Void = bs" |
180 "retrieve (AONE bs) Void = bs" |
148 | "retrieve (ACHAR bs c) (Char d) = bs" |
181 | "retrieve (ACHAR bs c) (Char d) = bs" |
151 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" |
184 | "retrieve (AALTs bs (r#rs)) (Right v) = bs @ retrieve (AALTs [] rs) v" |
152 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
185 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
153 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
186 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
154 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
187 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
155 bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" |
188 bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" |
156 |
189 | "retrieve (ANTIMES bs r 0) (Stars []) = bs @ [S]" |
|
190 | "retrieve (ANTIMES bs r (Suc n)) (Stars (v#vs)) = |
|
191 bs @ [Z] @ retrieve r v @ retrieve (ANTIMES [] r n) (Stars vs)" |
157 |
192 |
158 |
193 |
159 fun |
194 fun |
160 bnullable :: "arexp \<Rightarrow> bool" |
195 bnullable :: "arexp \<Rightarrow> bool" |
161 where |
196 where |
163 | "bnullable (AONE bs) = True" |
198 | "bnullable (AONE bs) = True" |
164 | "bnullable (ACHAR bs c) = False" |
199 | "bnullable (ACHAR bs c) = False" |
165 | "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)" |
200 | "bnullable (AALTs bs rs) = (\<exists>r \<in> set rs. bnullable r)" |
166 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)" |
201 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)" |
167 | "bnullable (ASTAR bs r) = True" |
202 | "bnullable (ASTAR bs r) = True" |
|
203 | "bnullable (ANTIMES bs r n) = (if n = 0 then True else bnullable r)" |
168 |
204 |
169 abbreviation |
205 abbreviation |
170 bnullables :: "arexp list \<Rightarrow> bool" |
206 bnullables :: "arexp list \<Rightarrow> bool" |
171 where |
207 where |
172 "bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)" |
208 "bnullables rs \<equiv> (\<exists>r \<in> set rs. bnullable r)" |
173 |
209 |
174 fun |
210 function (sequential) |
175 bmkeps :: "arexp \<Rightarrow> bit list" and |
211 bmkeps :: "arexp \<Rightarrow> bit list" |
176 bmkepss :: "arexp list \<Rightarrow> bit list" |
|
177 where |
212 where |
178 "bmkeps(AONE bs) = bs" |
213 "bmkeps(AONE bs) = bs" |
179 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
214 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
180 | "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)" |
215 | "bmkeps(AALTs bs (r#rs)) = |
|
216 (if bnullable(r) then (bs @ bmkeps r) else (bmkeps (AALTs bs rs)))" |
181 | "bmkeps(ASTAR bs r) = bs @ [S]" |
217 | "bmkeps(ASTAR bs r) = bs @ [S]" |
182 | "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))" |
218 | "bmkeps(ANTIMES bs r 0) = bs @ [S]" |
|
219 | "bmkeps(ANTIMES bs r (Suc n)) = bs @ [Z] @ (bmkeps r) @ bmkeps(ANTIMES [] r n)" |
|
220 apply(pat_completeness) |
|
221 apply(auto) |
|
222 done |
|
223 |
|
224 termination "bmkeps" |
|
225 apply(relation "measure asize") |
|
226 apply(auto) |
|
227 using asize.elims by force |
|
228 |
|
229 fun |
|
230 bmkepss :: "arexp list \<Rightarrow> bit list" |
|
231 where |
|
232 "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))" |
|
233 |
183 |
234 |
184 lemma bmkepss1: |
235 lemma bmkepss1: |
185 assumes "\<not> bnullables rs1" |
236 assumes "\<not> bnullables rs1" |
186 shows "bmkepss (rs1 @ rs2) = bmkepss rs2" |
237 shows "bmkepss (rs1 @ rs2) = bmkepss rs2" |
187 using assms |
238 using assms |
188 by (induct rs1) (auto) |
239 by(induct rs1) (auto) |
|
240 |
189 |
241 |
190 lemma bmkepss2: |
242 lemma bmkepss2: |
191 assumes "bnullables rs1" |
243 assumes "bnullables rs1" |
192 shows "bmkepss (rs1 @ rs2) = bmkepss rs1" |
244 shows "bmkepss (rs1 @ rs2) = bmkepss rs1" |
193 using assms |
245 using assms |
204 | "bder c (ASEQ bs r1 r2) = |
256 | "bder c (ASEQ bs r1 r2) = |
205 (if bnullable r1 |
257 (if bnullable r1 |
206 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
258 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
207 else ASEQ bs (bder c r1) r2)" |
259 else ASEQ bs (bder c r1) r2)" |
208 | "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)" |
260 | "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)" |
209 |
261 | "bder c (ANTIMES bs r n) = (if n = 0 then AZERO else ASEQ (bs @ [Z]) (bder c r) (ANTIMES [] r (n - 1)))" |
210 |
262 |
211 fun |
263 fun |
212 bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
264 bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
213 where |
265 where |
214 "bders r [] = r" |
266 "bders r [] = r" |
262 using assms |
314 using assms |
263 apply(induct vs) |
315 apply(induct vs) |
264 apply(simp_all) |
316 apply(simp_all) |
265 done |
317 done |
266 |
318 |
|
319 lemma retrieve_encode_NTIMES: |
|
320 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v" "length vs = n" |
|
321 shows "code (Stars vs) = retrieve (ANTIMES [] (intern r) n) (Stars vs)" |
|
322 using assms |
|
323 apply(induct vs arbitrary: n) |
|
324 apply(simp_all) |
|
325 by force |
|
326 |
|
327 |
267 lemma retrieve_fuse2: |
328 lemma retrieve_fuse2: |
268 assumes "\<Turnstile> v : (erase r)" |
329 assumes "\<Turnstile> v : (erase r)" |
269 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
330 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
270 using assms |
331 using assms |
271 apply(induct r arbitrary: v bs) |
332 apply(induct r arbitrary: v bs) |
298 lemma retrieve_code: |
365 lemma retrieve_code: |
299 assumes "\<Turnstile> v : r" |
366 assumes "\<Turnstile> v : r" |
300 shows "code v = retrieve (intern r) v" |
367 shows "code v = retrieve (intern r) v" |
301 using assms |
368 using assms |
302 apply(induct v r ) |
369 apply(induct v r ) |
303 apply(simp_all add: retrieve_fuse retrieve_encode_STARS) |
370 apply(simp_all add: retrieve_fuse retrieve_encode_STARS) |
304 done |
371 apply(subst retrieve_encode_NTIMES) |
|
372 apply(auto) |
|
373 done |
|
374 |
305 |
375 |
306 |
376 |
307 lemma retrieve_AALTs_bnullable1: |
377 lemma retrieve_AALTs_bnullable1: |
308 assumes "bnullable r" |
378 assumes "bnullable r" |
309 shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs)))) |
379 shows "retrieve (AALTs bs (r # rs)) (mkeps (erase (AALTs bs (r # rs)))) |
338 using retrieve_AALTs_bnullable1 apply presburger |
408 using retrieve_AALTs_bnullable1 apply presburger |
339 apply (metis retrieve_AALTs_bnullable2) |
409 apply (metis retrieve_AALTs_bnullable2) |
340 apply (simp add: retrieve_AALTs_bnullable1) |
410 apply (simp add: retrieve_AALTs_bnullable1) |
341 by (metis retrieve_AALTs_bnullable2) |
411 by (metis retrieve_AALTs_bnullable2) |
342 |
412 |
343 |
413 lemma bmkeps_retrieve_ANTIMES: |
|
414 assumes "if n = 0 then True else bmkeps r = retrieve r (mkeps (erase r))" |
|
415 and "bnullable (ANTIMES bs r n)" |
|
416 shows "bmkeps (ANTIMES bs r n) = retrieve (ANTIMES bs r n) (Stars (replicate n (mkeps (erase r))))" |
|
417 using assms |
|
418 apply(induct n arbitrary: r bs) |
|
419 apply(auto)[1] |
|
420 apply(simp) |
|
421 done |
|
422 |
344 lemma bmkeps_retrieve: |
423 lemma bmkeps_retrieve: |
345 assumes "bnullable r" |
424 assumes "bnullable r" |
346 shows "bmkeps r = retrieve r (mkeps (erase r))" |
425 shows "bmkeps r = retrieve r (mkeps (erase r))" |
347 using assms |
426 using assms |
348 apply(induct r) |
427 apply(induct r rule: bmkeps.induct) |
349 apply(auto) |
428 apply(auto) |
350 using bmkeps_retrieve_AALTs by auto |
429 apply (simp add: retrieve_AALTs_bnullable1) |
|
430 using retrieve_AALTs_bnullable1 apply force |
|
431 by (metis retrieve_AALTs_bnullable2) |
|
432 |
351 |
433 |
352 lemma bder_retrieve: |
434 lemma bder_retrieve: |
353 assumes "\<Turnstile> v : der c (erase r)" |
435 assumes "\<Turnstile> v : der c (erase r)" |
354 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
436 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
355 using assms |
437 using assms |
386 apply(simp) |
468 apply(simp) |
387 apply(erule Prf_elims) |
469 apply(erule Prf_elims) |
388 apply(clarify) |
470 apply(clarify) |
389 apply(erule Prf_elims) |
471 apply(erule Prf_elims) |
390 apply(clarify) |
472 apply(clarify) |
391 by (simp add: retrieve_fuse2) |
473 apply (simp add: retrieve_fuse2) |
|
474 (* ANTIMES case *) |
|
475 apply(auto) |
|
476 apply(erule Prf_elims) |
|
477 apply(erule Prf_elims) |
|
478 apply(clarify) |
|
479 apply(erule Prf_elims) |
|
480 apply(clarify) |
|
481 by (metis (full_types) Suc_pred append_assoc injval.simps(8) retrieve.simps(10) retrieve.simps(6)) |
392 |
482 |
393 |
483 |
394 lemma MAIN_decode: |
484 lemma MAIN_decode: |
395 assumes "\<Turnstile> v : ders s r" |
485 assumes "\<Turnstile> v : ders s r" |
396 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
486 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |