3 imports "Lexer" |
3 imports "Lexer" |
4 begin |
4 begin |
5 |
5 |
6 section {* Bit-Encodings *} |
6 section {* Bit-Encodings *} |
7 |
7 |
8 fun |
8 datatype bit = Z | S |
9 code :: "val \<Rightarrow> bool list" |
9 |
|
10 fun |
|
11 code :: "val \<Rightarrow> bit list" |
10 where |
12 where |
11 "code Void = []" |
13 "code Void = []" |
12 | "code (Char c) = []" |
14 | "code (Char c) = []" |
13 | "code (Left v) = False # (code v)" |
15 | "code (Left v) = Z # (code v)" |
14 | "code (Right v) = True # (code v)" |
16 | "code (Right v) = S # (code v)" |
15 | "code (Seq v1 v2) = (code v1) @ (code v2)" |
17 | "code (Seq v1 v2) = (code v1) @ (code v2)" |
16 | "code (Stars []) = [True]" |
18 | "code (Stars []) = [S]" |
17 | "code (Stars (v # vs)) = False # (code v) @ code (Stars vs)" |
19 | "code (Stars (v # vs)) = (Z # code v) @ code (Stars vs)" |
18 |
20 |
19 |
21 |
20 fun |
22 fun |
21 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
23 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
22 where |
24 where |
23 "Stars_add v (Stars vs) = Stars (v # vs)" |
25 "Stars_add v (Stars vs) = Stars (v # vs)" |
24 |
26 |
25 function |
27 function |
26 decode' :: "bool list \<Rightarrow> rexp \<Rightarrow> (val * bool list)" |
28 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
27 where |
29 where |
28 "decode' ds ZERO = (Void, [])" |
30 "decode' ds ZERO = (Void, [])" |
29 | "decode' ds ONE = (Void, ds)" |
31 | "decode' ds ONE = (Void, ds)" |
30 | "decode' ds (CHAR d) = (Char d, ds)" |
32 | "decode' ds (CHAR d) = (Char d, ds)" |
31 | "decode' [] (ALT r1 r2) = (Void, [])" |
33 | "decode' [] (ALT r1 r2) = (Void, [])" |
32 | "decode' (False # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
34 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
33 | "decode' (True # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
35 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
34 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
36 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
35 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
37 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
36 | "decode' [] (STAR r) = (Void, [])" |
38 | "decode' [] (STAR r) = (Void, [])" |
37 | "decode' (True # ds) (STAR r) = (Stars [], ds)" |
39 | "decode' (S # ds) (STAR r) = (Stars [], ds)" |
38 | "decode' (False # ds) (STAR r) = (let (v, ds') = decode' ds r in |
40 | "decode' (Z # ds) (STAR r) = (let (v, ds') = decode' ds r in |
39 let (vs, ds'') = decode' ds' (STAR r) |
41 let (vs, ds'') = decode' ds' (STAR r) |
40 in (Stars_add v vs, ds''))" |
42 in (Stars_add v vs, ds''))" |
41 by pat_completeness auto |
43 by pat_completeness auto |
42 |
44 |
43 lemma decode'_smaller: |
45 lemma decode'_smaller: |
74 using assms |
76 using assms |
75 apply(induct v r arbitrary: ds) |
77 apply(induct v r arbitrary: ds) |
76 apply(auto) |
78 apply(auto) |
77 using decode'_code_Stars by blast |
79 using decode'_code_Stars by blast |
78 |
80 |
79 |
|
80 lemma decode_code: |
81 lemma decode_code: |
81 assumes "\<Turnstile> v : r" |
82 assumes "\<Turnstile> v : r" |
82 shows "decode (code v) r = Some v" |
83 shows "decode (code v) r = Some v" |
83 using assms unfolding decode_def |
84 using assms unfolding decode_def |
84 by (smt append_Nil2 decode'_code old.prod.case) |
85 by (smt append_Nil2 decode'_code old.prod.case) |
85 |
86 |
86 |
87 |
87 datatype arexp = |
88 datatype arexp = |
88 AZERO |
89 AZERO |
89 | AONE "bool list" |
90 | AONE "bit list" |
90 | ACHAR "bool list" char |
91 | ACHAR "bit list" char |
91 | ASEQ "bool list" arexp arexp |
92 | ASEQ "bit list" arexp arexp |
92 | AALT "bool list" arexp arexp |
93 | AALT "bit list" arexp arexp |
93 | ASTAR "bool list" arexp |
94 | ASTAR "bit list" arexp |
94 |
95 |
95 fun fuse :: "bool list \<Rightarrow> arexp \<Rightarrow> arexp" where |
96 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
96 "fuse bs AZERO = AZERO" |
97 "fuse bs AZERO = AZERO" |
97 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
98 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
98 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" |
99 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" |
99 | "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2" |
100 | "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2" |
100 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" |
101 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" |
101 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
102 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
102 |
103 |
103 fun internalise :: "rexp \<Rightarrow> arexp" where |
104 fun intern :: "rexp \<Rightarrow> arexp" where |
104 "internalise ZERO = AZERO" |
105 "intern ZERO = AZERO" |
105 | "internalise ONE = AONE []" |
106 | "intern ONE = AONE []" |
106 | "internalise (CHAR c) = ACHAR [] c" |
107 | "intern (CHAR c) = ACHAR [] c" |
107 | "internalise (ALT r1 r2) = AALT [] (fuse [False] (internalise r1)) |
108 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
108 (fuse [True] (internalise r2))" |
109 (fuse [S] (intern r2))" |
109 | "internalise (SEQ r1 r2) = ASEQ [] (internalise r1) (internalise r2)" |
110 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
110 | "internalise (STAR r) = ASTAR [] (internalise r)" |
111 | "intern (STAR r) = ASTAR [] (intern r)" |
111 |
112 |
112 |
113 |
113 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bool list" where |
114 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
114 "retrieve (AONE bs) Void = bs" |
115 "retrieve (AONE bs) Void = bs" |
115 | "retrieve (ACHAR bs c) (Char d) = bs" |
116 | "retrieve (ACHAR bs c) (Char d) = bs" |
116 | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v" |
117 | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v" |
117 | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v" |
118 | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v" |
118 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
119 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
119 | "retrieve (ASTAR bs r) (Stars []) = bs @ [True]" |
120 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
120 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
121 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
121 bs @ [False] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" |
122 bs @ [Z] @ retrieve r v @ retrieve (ASTAR [] r) (Stars vs)" |
122 |
123 |
123 |
124 fun |
124 fun |
125 erase :: "arexp \<Rightarrow> rexp" |
125 aerase :: "arexp \<Rightarrow> rexp" |
126 where |
126 where |
127 "erase AZERO = ZERO" |
127 "aerase AZERO = ZERO" |
128 | "erase (AONE _) = ONE" |
128 | "aerase (AONE _) = ONE" |
129 | "erase (ACHAR _ c) = CHAR c" |
129 | "aerase (ACHAR _ c) = CHAR c" |
130 | "erase (AALT _ r1 r2) = ALT (erase r1) (erase r2)" |
130 | "aerase (AALT _ r1 r2) = ALT (aerase r1) (aerase r2)" |
131 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
131 | "aerase (ASEQ _ r1 r2) = SEQ (aerase r1) (aerase r2)" |
132 | "erase (ASTAR _ r) = STAR (erase r)" |
132 | "aerase (ASTAR _ r) = STAR (aerase r)" |
|
133 |
|
134 |
|
135 |
133 |
136 fun |
134 fun |
137 anullable :: "arexp \<Rightarrow> bool" |
135 bnullable :: "arexp \<Rightarrow> bool" |
138 where |
136 where |
139 "anullable (AZERO) = False" |
137 "bnullable (AZERO) = False" |
140 | "anullable (AONE bs) = True" |
138 | "bnullable (AONE bs) = True" |
141 | "anullable (ACHAR bs c) = False" |
139 | "bnullable (ACHAR bs c) = False" |
142 | "anullable (AALT bs r1 r2) = (anullable r1 \<or> anullable r2)" |
140 | "bnullable (AALT bs r1 r2) = (bnullable r1 \<or> bnullable r2)" |
143 | "anullable (ASEQ bs r1 r2) = (anullable r1 \<and> anullable r2)" |
141 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)" |
144 | "anullable (ASTAR bs r) = True" |
142 | "bnullable (ASTAR bs r) = True" |
145 |
143 |
146 fun |
144 fun |
147 amkeps :: "arexp \<Rightarrow> bool list" |
145 bmkeps :: "arexp \<Rightarrow> bit list" |
148 where |
146 where |
149 "amkeps(AONE bs) = bs" |
147 "bmkeps(AONE bs) = bs" |
150 | "amkeps(ASEQ bs r1 r2) = bs @ (amkeps r1) @ (amkeps r2)" |
148 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)" |
151 | "amkeps(AALT bs r1 r2) = (if anullable(r1) then bs @ (amkeps r1) else bs @ (amkeps r2))" |
149 | "bmkeps(AALT bs r1 r2) = (if bnullable(r1) then bs @ (bmkeps r1) else bs @ (bmkeps r2))" |
152 | "amkeps(ASTAR bs r) = bs @ [True]" |
150 | "bmkeps(ASTAR bs r) = bs @ [S]" |
153 |
151 |
154 |
152 |
155 fun |
153 fun |
156 ader :: "char \<Rightarrow> arexp \<Rightarrow> arexp" |
154 bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp" |
157 where |
155 where |
158 "ader c (AZERO) = AZERO" |
156 "bder c (AZERO) = AZERO" |
159 | "ader c (AONE bs) = AZERO" |
157 | "bder c (AONE bs) = AZERO" |
160 | "ader c (ACHAR bs d) = (if c = d then AONE bs else AZERO)" |
158 | "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)" |
161 | "ader c (AALT bs r1 r2) = AALT bs (ader c r1) (ader c r2)" |
159 | "bder c (AALT bs r1 r2) = AALT bs (bder c r1) (bder c r2)" |
162 | "ader c (ASEQ bs r1 r2) = |
160 | "bder c (ASEQ bs r1 r2) = |
163 (if anullable r1 |
161 (if bnullable r1 |
164 then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2)) |
162 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
165 else ASEQ bs (ader c r1) r2)" |
163 else ASEQ bs (bder c r1) r2)" |
166 | "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)" |
164 | "bder c (ASTAR bs r) = ASEQ bs (fuse [Z] (bder c r)) (ASTAR [] r)" |
167 |
165 |
168 |
166 |
169 fun |
167 fun |
170 aders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
168 bders :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
171 where |
169 where |
172 "aders r [] = r" |
170 "bders r [] = r" |
173 | "aders r (c#s) = aders (ader c r) s" |
171 | "bders r (c#s) = bders (bder c r) s" |
174 |
172 |
175 lemma aders_append: |
173 lemma bders_append: |
176 "aders r (s1 @ s2) = aders (aders r s1) s2" |
174 "bders r (s1 @ s2) = bders (bders r s1) s2" |
177 apply(induct s1 arbitrary: r s2) |
175 apply(induct s1 arbitrary: r s2) |
178 apply(simp_all) |
176 apply(simp_all) |
179 done |
177 done |
180 |
178 |
181 lemma anullable_correctness: |
179 lemma bnullable_correctness: |
182 shows "nullable (aerase r) = anullable r" |
180 shows "nullable (erase r) = bnullable r" |
183 apply(induct r) |
181 apply(induct r) |
184 apply(simp_all) |
182 apply(simp_all) |
185 done |
183 done |
186 |
184 |
187 lemma aerase_fuse: |
185 lemma erase_fuse: |
188 shows "aerase (fuse bs r) = aerase r" |
186 shows "erase (fuse bs r) = erase r" |
189 apply(induct r) |
187 apply(induct r) |
190 apply(simp_all) |
188 apply(simp_all) |
191 done |
189 done |
192 |
190 |
193 lemma aerase_internalise: |
191 lemma erase_intern[simp]: |
194 shows "aerase (internalise r) = r" |
192 shows "erase (intern r) = r" |
195 apply(induct r) |
193 apply(induct r) |
196 apply(simp_all add: aerase_fuse) |
194 apply(simp_all add: erase_fuse) |
197 done |
195 done |
198 |
196 |
199 lemma aerase_ader: |
197 lemma erase_bder[simp]: |
200 shows "aerase (ader a r) = der a (aerase r)" |
198 shows "erase (bder a r) = der a (erase r)" |
201 apply(induct r) |
199 apply(induct r) |
202 apply(simp_all add: aerase_fuse anullable_correctness) |
200 apply(simp_all add: erase_fuse bnullable_correctness) |
203 done |
201 done |
204 |
202 |
205 lemma aerase_aders: |
203 lemma erase_bders[simp]: |
206 shows "aerase (aders r s) = ders s (aerase r)" |
204 shows "erase (bders r s) = ders s (erase r)" |
207 apply(induct s arbitrary: r ) |
205 apply(induct s arbitrary: r ) |
208 apply(simp_all add: aerase_ader) |
206 apply(simp_all) |
209 done |
207 done |
210 |
208 |
211 lemma retrieve_encode_STARS: |
209 lemma retrieve_encode_STARS: |
212 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (internalise r) v" |
210 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (intern r) v" |
213 shows "code (Stars vs) = retrieve (ASTAR [] (internalise r)) (Stars vs)" |
211 shows "code (Stars vs) = retrieve (ASTAR [] (intern r)) (Stars vs)" |
214 using assms |
212 using assms |
215 apply(induct vs) |
213 apply(induct vs) |
|
214 apply(simp_all) |
|
215 done |
|
216 |
|
217 lemma retrieve_fuse2: |
|
218 assumes "\<Turnstile> v : (erase r)" |
|
219 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
|
220 using assms |
|
221 apply(induct r arbitrary: v bs) |
|
222 using retrieve_encode_STARS |
|
223 apply(auto elim!: Prf_elims) |
|
224 apply(case_tac vs) |
216 apply(simp) |
225 apply(simp) |
217 apply(simp) |
226 apply(simp) |
218 done |
227 done |
219 |
228 |
220 lemma retrieve_afuse2: |
229 lemma retrieve_fuse: |
221 assumes "\<Turnstile> v : (aerase r)" |
|
222 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
|
223 using assms |
|
224 apply(induct r arbitrary: v bs) |
|
225 apply(auto) |
|
226 using Prf_elims(1) apply blast |
|
227 using Prf_elims(4) apply fastforce |
|
228 using Prf_elims(5) apply fastforce |
|
229 apply (smt Prf_elims(2) append_assoc retrieve.simps(5)) |
|
230 apply(erule Prf_elims) |
|
231 apply(simp) |
|
232 apply(simp) |
|
233 apply(erule Prf_elims) |
|
234 apply(simp) |
|
235 apply(case_tac vs) |
|
236 apply(simp) |
|
237 apply(simp) |
|
238 done |
|
239 |
|
240 lemma retrieve_afuse: |
|
241 assumes "\<Turnstile> v : r" |
230 assumes "\<Turnstile> v : r" |
242 shows "retrieve (fuse bs (internalise r)) v = bs @ retrieve (internalise r) v" |
231 shows "retrieve (fuse bs (intern r)) v = bs @ retrieve (intern r) v" |
243 using assms |
232 using assms |
244 by (simp_all add: retrieve_afuse2 aerase_internalise) |
233 by (simp_all add: retrieve_fuse2) |
245 |
234 |
246 |
235 |
247 lemma retrieve_encode: |
236 lemma retrieve_code: |
248 assumes "\<Turnstile> v : r" |
237 assumes "\<Turnstile> v : r" |
249 shows "code v = retrieve (internalise r) v" |
238 shows "code v = retrieve (intern r) v" |
250 using assms |
239 using assms |
251 apply(induct v r) |
240 apply(induct v r) |
252 apply(simp_all add: retrieve_afuse retrieve_encode_STARS) |
241 apply(simp_all add: retrieve_fuse retrieve_encode_STARS) |
253 done |
242 done |
254 |
243 |
255 lemma Q00: |
244 |
256 assumes "s \<in> r \<rightarrow> v" |
245 lemma bmkeps_retrieve: |
257 shows "\<Turnstile> v : r" |
246 assumes "nullable (erase r)" |
258 using assms |
247 shows "bmkeps r = retrieve r (mkeps (erase r))" |
259 apply(induct) |
248 using assms |
260 apply(auto intro: Prf.intros) |
249 apply(induct r) |
261 by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5)) |
250 apply(auto simp add: bnullable_correctness) |
262 |
251 done |
263 lemma Qa: |
|
264 assumes "anullable r" |
|
265 shows "retrieve r (mkeps (aerase r)) = amkeps r" |
|
266 using assms |
|
267 apply(induct r) |
|
268 apply(auto) |
|
269 using anullable_correctness apply auto[1] |
|
270 apply (simp add: anullable_correctness) |
|
271 by (simp add: anullable_correctness) |
|
272 |
|
273 |
252 |
274 lemma Qb: |
253 lemma bder_retrieve: |
275 assumes "\<Turnstile> v : der c (aerase r)" |
254 assumes "\<Turnstile> v : der c (erase r)" |
276 shows "retrieve (ader c r) v = retrieve r (injval (aerase r) c v)" |
255 shows "retrieve (bder c r) v = retrieve r (injval (erase r) c v)" |
277 using assms |
256 using assms |
278 apply(induct r arbitrary: v c) |
257 apply(induct r arbitrary: v) |
279 apply(simp_all) |
258 apply(auto elim!: Prf_elims simp add: retrieve_fuse2 bnullable_correctness bmkeps_retrieve) |
280 using Prf_elims(1) apply blast |
259 done |
281 using Prf_elims(1) apply blast |
260 |
282 apply(auto)[1] |
261 lemma MAIN_decode: |
283 using Prf_elims(4) apply fastforce |
|
284 using Prf_elims(1) apply blast |
|
285 apply(auto split: if_splits)[1] |
|
286 apply(auto elim!: Prf_elims)[1] |
|
287 apply(rotate_tac 1) |
|
288 apply(drule_tac x="v2" in meta_spec) |
|
289 apply(drule_tac x="c" in meta_spec) |
|
290 apply(drule meta_mp) |
|
291 apply(simp) |
|
292 apply(drule sym) |
|
293 apply(simp) |
|
294 apply(subst retrieve_afuse2) |
|
295 apply (simp add: aerase_ader) |
|
296 apply (simp add: Qa) |
|
297 using anullable_correctness apply auto[1] |
|
298 apply(auto elim!: Prf_elims)[1] |
|
299 using anullable_correctness apply auto[1] |
|
300 apply(auto elim!: Prf_elims)[1] |
|
301 apply(auto elim!: Prf_elims)[1] |
|
302 apply(auto elim!: Prf_elims)[1] |
|
303 by (simp add: retrieve_afuse2 aerase_ader) |
|
304 |
|
305 lemma MAIN: |
|
306 assumes "\<Turnstile> v : ders s r" |
262 assumes "\<Turnstile> v : ders s r" |
307 shows "code (flex r id s v) = retrieve (aders (internalise r) s) v" |
263 shows "Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" |
308 using assms |
264 using assms |
309 apply(induct s arbitrary: v rule: rev_induct) |
265 proof (induct s arbitrary: v rule: rev_induct) |
310 apply(simp) |
266 case Nil |
311 apply(simp add: retrieve_encode) |
267 have "\<Turnstile> v : ders [] r" by fact |
312 apply(simp add: flex_append aders_append) |
268 then have "\<Turnstile> v : r" by simp |
313 apply(subst Qb) |
269 then have "Some v = decode (retrieve (intern r) v) r" |
314 apply(simp add: aerase_internalise ders_append aerase_aders) |
270 using decode_code retrieve_code by auto |
315 apply(simp add: aerase_aders aerase_internalise) |
271 then show "Some (flex r id [] v) = decode (retrieve (bders (intern r) []) v) r" |
316 apply(drule_tac x="injval (ders xs r) x v" in meta_spec) |
272 by simp |
317 apply(drule meta_mp) |
273 next |
318 apply(simp add: Prf_injval ders_append) |
274 case (snoc c s v) |
319 apply(simp) |
275 have IH: "\<And>v. \<Turnstile> v : ders s r \<Longrightarrow> |
320 done |
276 Some (flex r id s v) = decode (retrieve (bders (intern r) s) v) r" by fact |
321 |
277 have asm: "\<Turnstile> v : ders (s @ [c]) r" by fact |
322 fun alexer where |
278 then have asm2: "\<Turnstile> injval (ders s r) c v : ders s r" |
323 "alexer r s = (if anullable (aders (internalise r) s) then |
279 by(simp add: Prf_injval ders_append) |
324 decode (amkeps (aders (internalise r) s)) r else None)" |
280 have "Some (flex r id (s @ [c]) v) = Some (flex r id s (injval (ders s r) c v))" |
325 |
281 by (simp add: flex_append) |
326 |
282 also have "... = decode (retrieve (bders (intern r) s) (injval (ders s r) c v)) r" |
327 lemma FIN: |
283 using asm2 IH by simp |
328 "alexer r s = lexer r s" |
284 also have "... = decode (retrieve (bder c (bders (intern r) s)) v) r" |
329 apply(auto simp add: lexer_flex) |
285 using asm by(simp_all add: bder_retrieve ders_append) |
330 apply (smt MAIN Q00 Qa aerase_aders aerase_internalise decode_code lexer_correctness(1) lexer_flex mkeps_nullable) |
286 finally show "Some (flex r id (s @ [c]) v) = |
331 apply (metis aerase_aders aerase_internalise anullable_correctness) |
287 decode (retrieve (bders (intern r) (s @ [c])) v) r" by (simp add: bders_append) |
332 using aerase_aders aerase_internalise anullable_correctness by force |
288 qed |
|
289 |
|
290 |
|
291 definition blexer where |
|
292 "blexer r s \<equiv> if bnullable (bders (intern r) s) then |
|
293 decode (bmkeps (bders (intern r) s)) r else None" |
|
294 |
|
295 lemma blexer_correctness: |
|
296 shows "blexer r s = lexer r s" |
|
297 proof - |
|
298 { define bds where "bds \<equiv> bders (intern r) s" |
|
299 define ds where "ds \<equiv> ders s r" |
|
300 assume asm: "nullable ds" |
|
301 have era: "erase bds = ds" |
|
302 unfolding ds_def bds_def by simp |
|
303 have mke: "\<Turnstile> mkeps ds : ds" |
|
304 using asm by (simp add: mkeps_nullable) |
|
305 have "decode (bmkeps bds) r = decode (retrieve bds (mkeps ds)) r" |
|
306 using bmkeps_retrieve |
|
307 using asm era by (simp add: bmkeps_retrieve) |
|
308 also have "... = Some (flex r id s (mkeps ds))" |
|
309 using mke by (simp_all add: MAIN_decode ds_def bds_def) |
|
310 finally have "decode (bmkeps bds) r = Some (flex r id s (mkeps ds))" |
|
311 unfolding bds_def ds_def . |
|
312 } |
|
313 then show "blexer r s = lexer r s" |
|
314 unfolding blexer_def lexer_flex |
|
315 by(auto simp add: bnullable_correctness[symmetric]) |
|
316 qed |
333 |
317 |
334 unused_thms |
318 unused_thms |
335 |
319 |
336 end |
320 end |