1 |
1 |
2 theory Sulzmann |
2 theory Sulzmann |
3 imports "Positions" |
3 imports "Lexer" |
4 begin |
4 begin |
5 |
5 |
6 |
|
7 section {* Sulzmann's "Ordering" of Values *} |
|
8 |
|
9 inductive ValOrd :: "val \<Rightarrow> val \<Rightarrow> bool" ("_ \<prec> _" [100, 100] 100) |
|
10 where |
|
11 MY0: "length (flat v2) < length (flat v1) \<Longrightarrow> v1 \<prec> v2" |
|
12 | C2: "\<lbrakk>v1 \<prec> v1'; flat (Seq v1 v2) = flat (Seq v1' v2')\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1' v2')" |
|
13 | C1: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<prec> (Seq v1 v2')" |
|
14 | A2: "flat v1 = flat v2 \<Longrightarrow> (Left v1) \<prec> (Right v2)" |
|
15 | A3: "\<lbrakk>v2 \<prec> v2'; flat v2 = flat v2'\<rbrakk> \<Longrightarrow> (Right v2) \<prec> (Right v2')" |
|
16 | A4: "\<lbrakk>v1 \<prec> v1'; flat v1 = flat v1'\<rbrakk> \<Longrightarrow> (Left v1) \<prec> (Left v1')" |
|
17 | K1: "flat (Stars (v#vs)) = [] \<Longrightarrow> (Stars []) \<prec> (Stars (v#vs))" |
|
18 | K3: "\<lbrakk>v1 \<prec> v2; flat (Stars (v1#vs1)) = flat (Stars (v2#vs2))\<rbrakk> \<Longrightarrow> (Stars (v1#vs1)) \<prec> (Stars (v2#vs2))" |
|
19 | K4: "\<lbrakk>(Stars vs1) \<prec> (Stars vs2); flat (Stars vs1) = flat (Stars vs2)\<rbrakk> \<Longrightarrow> (Stars (v#vs1)) \<prec> (Stars (v#vs2))" |
|
20 |
|
21 |
|
22 (* |
|
23 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<preceq>_ _" [100, 100, 100] 100) |
|
24 where |
|
25 C2: "v1 \<preceq>r1 v1' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1' v2')" |
|
26 | C1: "v2 \<preceq>r2 v2' \<Longrightarrow> (Seq v1 v2) \<preceq>(SEQ r1 r2) (Seq v1 v2')" |
|
27 | A1: "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Left v1)" |
|
28 | A2: "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Right v2)" |
|
29 | A3: "v2 \<preceq>r2 v2' \<Longrightarrow> (Right v2) \<preceq>(ALT r1 r2) (Right v2')" |
|
30 | A4: "v1 \<preceq>r1 v1' \<Longrightarrow> (Left v1) \<preceq>(ALT r1 r2) (Left v1')" |
|
31 | K1: "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<preceq>(STAR r) (Stars (v # vs))" |
|
32 | K2: "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<preceq>(STAR r) (Stars [])" |
|
33 | K3: "v1 \<preceq>r v2 \<Longrightarrow> (Stars (v1 # vs1)) \<preceq>(STAR r) (Stars (v2 # vs2))" |
|
34 | K4: "(Stars vs1) \<preceq>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<preceq>(STAR r) (Stars (v # vs2))" |
|
35 *) |
|
36 (*| MY1: "Void \<preceq>ONE Void" |
|
37 | MY2: "(Char c) \<preceq>(CHAR c) (Char c)" |
|
38 | MY3: "(Stars []) \<preceq>(STAR r) (Stars [])" |
|
39 *) |
|
40 |
|
41 (* |
|
42 lemma ValOrd_refl: |
|
43 assumes "\<turnstile> v : r" |
|
44 shows "v \<preceq>r v" |
|
45 using assms |
|
46 apply(induct r rule: Prf.induct) |
|
47 apply(rule ValOrd.intros) |
|
48 apply(simp) |
|
49 apply(rule ValOrd.intros) |
|
50 apply(simp) |
|
51 apply(rule ValOrd.intros) |
|
52 apply(simp) |
|
53 apply(rule ValOrd.intros) |
|
54 apply(rule ValOrd.intros) |
|
55 apply(rule ValOrd.intros) |
|
56 apply(rule ValOrd.intros) |
|
57 apply(simp) |
|
58 done |
|
59 *) |
|
60 |
|
61 lemma ValOrd_irrefl: |
|
62 assumes "\<turnstile> v : r" "v \<prec> v" |
|
63 shows "False" |
|
64 using assms |
|
65 apply(induct v r rule: Prf.induct) |
|
66 apply(erule ValOrd.cases) |
|
67 apply(simp_all) |
|
68 apply(erule ValOrd.cases) |
|
69 apply(simp_all) |
|
70 apply(erule ValOrd.cases) |
|
71 apply(simp_all) |
|
72 apply(erule ValOrd.cases) |
|
73 apply(simp_all) |
|
74 apply(erule ValOrd.cases) |
|
75 apply(simp_all) |
|
76 apply(erule ValOrd.cases) |
|
77 apply(simp_all) |
|
78 apply(erule ValOrd.cases) |
|
79 apply(simp_all) |
|
80 done |
|
81 |
|
82 lemma prefix_sprefix: |
|
83 shows "xs \<sqsubseteq>pre ys \<longleftrightarrow> (xs = ys \<or> xs \<sqsubset>spre ys)" |
|
84 apply(auto simp add: sprefix_list_def prefix_list_def) |
|
85 done |
|
86 |
|
87 |
|
88 |
|
89 lemma Posix_CPT2: |
|
90 assumes "v1 \<prec> v2" |
|
91 shows "v1 :\<sqsubset>val v2" |
|
92 using assms |
|
93 apply(induct v1 v2 arbitrary: rule: ValOrd.induct) |
|
94 apply(rule val_ord_shorterI) |
|
95 apply(simp) |
|
96 apply(rule val_ord_SeqI1) |
|
97 apply(simp) |
|
98 apply(simp) |
|
99 apply(rule val_ord_SeqI2) |
|
100 apply(simp) |
|
101 apply(simp) |
|
102 apply(simp add: val_ord_ex_def) |
|
103 apply(rule_tac x="[0]" in exI) |
|
104 apply(auto simp add: val_ord_def Pos_empty pflat_len_simps)[1] |
|
105 apply(smt inlen_bigger) |
|
106 apply(rule val_ord_RightI) |
|
107 apply(simp) |
|
108 apply(simp) |
|
109 apply(rule val_ord_LeftI) |
|
110 apply(simp) |
|
111 apply(simp) |
|
112 defer |
|
113 apply(rule val_ord_StarsI) |
|
114 apply(simp) |
|
115 apply(simp) |
|
116 apply(rule val_ord_StarsI2) |
|
117 apply(simp) |
|
118 apply(simp) |
|
119 oops |
|
120 |
|
121 lemma QQ: |
|
122 shows "x \<le> (y::nat) \<longleftrightarrow> x = y \<or> x < y" |
|
123 by auto |
|
124 |
|
125 lemma Posix_CPT2: |
|
126 assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPTpre r s" "v2 \<in> CPTpre r s" |
|
127 shows "v1 \<prec> v2" |
|
128 using assms |
|
129 apply(induct r arbitrary: v1 v2 s) |
|
130 apply(auto simp add: CPTpre_def)[1] |
|
131 apply(erule CPrf.cases) |
|
132 apply(simp_all)[7] |
|
133 apply(auto simp add: CPTpre_def)[1] |
|
134 apply(erule CPrf.cases) |
|
135 apply(simp_all)[7] |
|
136 apply(auto simp add: CPTpre_def)[1] |
|
137 apply(erule CPrf.cases) |
|
138 apply(simp_all)[7] |
|
139 apply(simp add: val_ord_ex_def) |
|
140 apply(auto simp add: val_ord_def)[1] |
|
141 apply(auto simp add: CPTpre_def)[1] |
|
142 apply(erule CPrf.cases) |
|
143 apply(simp_all)[7] |
|
144 apply(erule CPrf.cases) |
|
145 apply(simp_all)[7] |
|
146 apply(auto simp add: val_ord_ex_def val_ord_def)[1] |
|
147 (* SEQ case *) |
|
148 apply(subst (asm) (5) CPTpre_def) |
|
149 apply(subst (asm) (5) CPTpre_def) |
|
150 apply(auto)[1] |
|
151 apply(erule CPrf.cases) |
|
152 apply(simp_all)[7] |
|
153 apply(erule CPrf.cases) |
|
154 apply(simp_all)[7] |
|
155 apply(clarify) |
|
156 apply(frule val_ord_shorterE) |
|
157 apply(subst (asm) QQ) |
|
158 apply(erule disjE) |
|
159 apply(drule val_ord_SeqE) |
|
160 apply(erule disjE) |
|
161 apply(drule_tac x="v1a" in meta_spec) |
|
162 apply(rotate_tac 8) |
|
163 apply(drule_tac x="v1b" in meta_spec) |
|
164 apply(drule_tac x="flat v1a @ flat v2a @ s'" in meta_spec) |
|
165 apply(simp) |
|
166 apply(drule meta_mp) |
|
167 apply(auto simp add: CPTpre_def)[1] |
|
168 apply(drule meta_mp) |
|
169 apply(auto simp add: CPTpre_def)[1] |
|
170 apply(rule ValOrd.intros(2)) |
|
171 apply(assumption) |
|
172 apply(frule val_ord_shorterE) |
|
173 apply(subst (asm) append_eq_append_conv_if) |
|
174 apply(simp) |
|
175 apply (metis append_assoc append_eq_append_conv_if length_append) |
|
176 |
|
177 |
|
178 thm le |
|
179 apply(clarify) |
|
180 apply(rule ValOrd.intros) |
|
181 apply(simp) |
|
182 |
|
183 apply(subst (asm) (3) CPTpre_def) |
|
184 apply(subst (asm) (3) CPTpre_def) |
|
185 apply(auto)[1] |
|
186 apply(drule_tac meta_mp) |
|
187 apply(auto simp add: CPTpre_def)[1] |
|
188 apply(erule CPrf.cases) |
|
189 apply(simp_all)[7] |
|
190 apply(erule CPrf.cases) |
|
191 apply(simp_all)[7] |
|
192 apply(clarify) |
|
193 apply(drule val_ord_SeqE) |
|
194 apply(erule disjE) |
|
195 apply(simp add: append_eq_append_conv2) |
|
196 apply(auto) |
|
197 prefer 2 |
|
198 apply(rule ValOrd.intros(2)) |
|
199 prefer 2 |
|
200 apply(simp) |
|
201 thm ValOrd.intros |
|
202 apply(case_tac "flat v1b = flat v1a") |
|
203 apply(rule ValOrd.intros) |
|
204 apply(simp) |
|
205 apply(simp) |
|
206 |
|
207 |
|
208 |
|
209 |
|
210 lemma Posix_CPT: |
|
211 assumes "v1 :\<sqsubset>val v2" "v1 \<in> CPT r s" "v2 \<in> CPT r s" |
|
212 shows "v1 \<preceq>r v2" |
|
213 using assms |
|
214 apply(induct r arbitrary: v1 v2 s rule: rexp.induct) |
|
215 apply(simp add: CPT_def) |
|
216 apply(clarify) |
|
217 apply(erule CPrf.cases) |
|
218 apply(simp_all) |
|
219 apply(simp add: CPT_def) |
|
220 apply(clarify) |
|
221 apply(erule CPrf.cases) |
|
222 apply(simp_all) |
|
223 apply(erule CPrf.cases) |
|
224 apply(simp_all) |
|
225 apply(rule ValOrd.intros) |
|
226 apply(simp add: CPT_def) |
|
227 apply(clarify) |
|
228 apply(erule CPrf.cases) |
|
229 apply(simp_all) |
|
230 apply(erule CPrf.cases) |
|
231 apply(simp_all) |
|
232 apply(rule ValOrd.intros) |
|
233 (*SEQ case *) |
|
234 apply(simp add: CPT_def) |
|
235 apply(clarify) |
|
236 apply(erule CPrf.cases) |
|
237 apply(simp_all) |
|
238 apply(clarify) |
|
239 apply(erule CPrf.cases) |
|
240 apply(simp_all) |
|
241 apply(clarify) |
|
242 thm val_ord_SEQ |
|
243 apply(drule_tac r="r1a" in val_ord_SEQ) |
|
244 apply(simp) |
|
245 using Prf_CPrf apply blast |
|
246 using Prf_CPrf apply blast |
|
247 apply(erule disjE) |
|
248 apply(rule C2) |
|
249 prefer 2 |
|
250 apply(simp) |
|
251 apply(rule C1) |
|
252 apply blast |
|
253 |
|
254 apply(simp add: append_eq_append_conv2) |
|
255 apply(clarify) |
|
256 apply(auto)[1] |
|
257 apply(drule_tac x="v1a" in meta_spec) |
|
258 apply(rotate_tac 8) |
|
259 apply(drule_tac x="v1b" in meta_spec) |
|
260 apply(rotate_tac 8) |
|
261 apply(simp) |
|
262 |
|
263 (* HERE *) |
|
264 apply(subst (asm) (3) val_ord_ex_def) |
|
265 apply(clarify) |
|
266 apply(subst (asm) val_ord_def) |
|
267 apply(clarify) |
|
268 apply(rule ValOrd.intros) |
|
269 |
|
270 |
|
271 apply(simp add: val_ord_ex_def) |
|
272 oops |
|
273 |
|
274 |
|
275 lemma ValOrd_trans: |
|
276 assumes "x \<preceq>r y" "y \<preceq>r z" |
|
277 and "x \<in> CPT r s" "y \<in> CPT r s" "z \<in> CPT r s" |
|
278 shows "x \<preceq>r z" |
|
279 using assms |
|
280 apply(induct x r y arbitrary: s z rule: ValOrd.induct) |
|
281 apply(rotate_tac 2) |
|
282 apply(erule ValOrd.cases) |
|
283 apply(simp_all)[13] |
|
284 apply(rule ValOrd.intros) |
|
285 apply(drule_tac x="s" in meta_spec) |
|
286 apply(drule_tac x="v1'a" in meta_spec) |
|
287 apply(drule_tac meta_mp) |
|
288 apply(simp) |
|
289 apply(drule_tac meta_mp) |
|
290 apply(simp add: CPT_def) |
|
291 oops |
|
292 |
|
293 lemma ValOrd_preorder: |
|
294 "preorder_on (CPT r s) {(v1, v2). v1 \<preceq>r v2 \<and> v1 \<in> (CPT r s) \<and> v2 \<in> (CPT r s)}" |
|
295 apply(simp add: preorder_on_def) |
|
296 apply(rule conjI) |
|
297 apply(simp add: refl_on_def) |
|
298 apply(auto) |
|
299 apply(rule ValOrd_refl) |
|
300 apply(simp add: CPT_def) |
|
301 apply(rule Prf_CPrf) |
|
302 apply(auto)[1] |
|
303 apply(simp add: trans_def) |
|
304 apply(auto) |
|
305 |
|
306 definition ValOrdEq :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<ge>_ _" [100, 100, 100] 100) |
|
307 where |
|
308 "v\<^sub>1 \<ge>r v\<^sub>2 \<equiv> v\<^sub>1 = v\<^sub>2 \<or> (v\<^sub>1 >r v\<^sub>2 \<and> flat v\<^sub>1 = flat v\<^sub>2)" |
|
309 |
|
310 (* |
|
311 |
|
312 |
|
313 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
|
314 where |
|
315 "v2 \<succ>r2 v2' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" |
|
316 | "\<lbrakk>v1 \<succ>r1 v1'; v1 \<noteq> v1'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
|
317 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
|
318 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)" |
|
319 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
|
320 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
|
321 | "Void \<succ>EMPTY Void" |
|
322 | "(Char c) \<succ>(CHAR c) (Char c)" |
|
323 | "flat (Stars (v # vs)) = [] \<Longrightarrow> (Stars []) \<succ>(STAR r) (Stars (v # vs))" |
|
324 | "flat (Stars (v # vs)) \<noteq> [] \<Longrightarrow> (Stars (v # vs)) \<succ>(STAR r) (Stars [])" |
|
325 | "\<lbrakk>v1 \<succ>r v2; v1 \<noteq> v2\<rbrakk> \<Longrightarrow> (Stars (v1 # vs1)) \<succ>(STAR r) (Stars (v2 # vs2))" |
|
326 | "(Stars vs1) \<succ>(STAR r) (Stars vs2) \<Longrightarrow> (Stars (v # vs1)) \<succ>(STAR r) (Stars (v # vs2))" |
|
327 | "(Stars []) \<succ>(STAR r) (Stars [])" |
|
328 *) |
|
329 |
|
330 |
|
331 section {* Bit-Encodings *} |
6 section {* Bit-Encodings *} |
332 |
7 |
333 |
8 fun |
334 fun |
9 code :: "val \<Rightarrow> bool list" |
335 code :: "val \<Rightarrow> rexp \<Rightarrow> bool list" |
10 where |
336 where |
11 "code Void = []" |
337 "code Void ONE = []" |
12 | "code (Char c) = []" |
338 | "code (Char c) (CHAR d) = []" |
13 | "code (Left v) = False # (code v)" |
339 | "code (Left v) (ALT r1 r2) = False # (code v r1)" |
14 | "code (Right v) = True # (code v)" |
340 | "code (Right v) (ALT r1 r2) = True # (code v r2)" |
15 | "code (Seq v1 v2) = (code v1) @ (code v2)" |
341 | "code (Seq v1 v2) (SEQ r1 r2) = (code v1 r1) @ (code v2 r2)" |
16 | "code (Stars []) = [True]" |
342 | "code (Stars []) (STAR r) = [True]" |
17 | "code (Stars (v # vs)) = False # (code v) @ code (Stars vs)" |
343 | "code (Stars (v # vs)) (STAR r) = False # (code v r) @ code (Stars vs) (STAR r)" |
18 |
344 |
19 |
345 fun |
20 fun |
346 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
21 Stars_add :: "val \<Rightarrow> val \<Rightarrow> val" |
347 where |
22 where |
348 "Stars_add v (Stars vs) = Stars (v # vs)" |
23 "Stars_add v (Stars vs) = Stars (v # vs)" |
469 (if anullable r1 |
163 (if anullable r1 |
470 then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2)) |
164 then AALT bs (ASEQ [] (ader c r1) r2) (fuse (amkeps r1) (ader c r2)) |
471 else ASEQ bs (ader c r1) r2)" |
165 else ASEQ bs (ader c r1) r2)" |
472 | "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)" |
166 | "ader c (ASTAR bs r) = ASEQ bs (fuse [False] (ader c r)) (ASTAR [] r)" |
473 |
167 |
474 lemma |
168 |
475 assumes "\<turnstile> v : der c r" |
169 fun |
476 shows "Some (injval r c v) = decode (retrieve (ader c (internalise r)) v) r" |
170 aders :: "string \<Rightarrow> arexp \<Rightarrow> arexp" |
477 using assms |
171 where |
478 apply(induct c r arbitrary: v rule: der.induct) |
172 "aders [] r = r" |
479 apply(simp_all) |
173 | "aders (c # s) r = aders s (ader c r)" |
480 apply(erule Prf_elims) |
174 |
481 apply(erule Prf_elims) |
175 fun |
482 apply(case_tac "c = d") |
176 alex :: "arexp \<Rightarrow> string \<Rightarrow> arexp" |
483 apply(simp) |
177 where |
484 apply(erule Prf_elims) |
178 "alex r [] = r" |
485 apply(simp) |
179 | "alex r (c#s) = alex (ader c r) s" |
486 apply(simp) |
180 |
487 apply(erule Prf_elims) |
181 lemma anullable_correctness: |
488 apply(auto split: prod.splits)[1] |
182 shows "nullable (aerase r) = anullable r" |
489 oops |
183 apply(induct r) |
490 |
184 apply(simp_all) |
|
185 done |
|
186 |
|
187 lemma aerase_fuse: |
|
188 shows "aerase (fuse bs r) = aerase r" |
|
189 apply(induct r) |
|
190 apply(simp_all) |
|
191 done |
|
192 |
|
193 |
|
194 lemma aerase_ader: |
|
195 shows "aerase (ader a r) = der a (aerase r)" |
|
196 apply(induct r) |
|
197 apply(simp_all add: aerase_fuse anullable_correctness) |
|
198 done |
|
199 |
|
200 lemma aerase_internalise: |
|
201 shows "aerase (internalise r) = r" |
|
202 apply(induct r) |
|
203 apply(simp_all add: aerase_fuse) |
|
204 done |
|
205 |
|
206 |
|
207 lemma aerase_alex: |
|
208 shows "aerase (alex r s) = ders s (aerase r)" |
|
209 apply(induct s arbitrary: r ) |
|
210 apply(simp_all add: aerase_ader) |
|
211 done |
|
212 |
|
213 lemma retrieve_encode_STARS: |
|
214 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> code v = retrieve (internalise r) v" |
|
215 shows "code (Stars vs) = retrieve (ASTAR [] (internalise r)) (Stars vs)" |
|
216 using assms |
|
217 apply(induct vs) |
|
218 apply(simp) |
|
219 apply(simp) |
|
220 done |
|
221 |
|
222 lemma retrieve_afuse2: |
|
223 assumes "\<Turnstile> v : (aerase r)" |
|
224 shows "retrieve (fuse bs r) v = bs @ retrieve r v" |
|
225 using assms |
|
226 apply(induct r arbitrary: v bs) |
|
227 apply(auto) |
|
228 using Prf_elims(1) apply blast |
|
229 using Prf_elims(4) apply fastforce |
|
230 using Prf_elims(5) apply fastforce |
|
231 apply (smt Prf_elims(2) append_assoc retrieve.simps(5)) |
|
232 apply(erule Prf_elims) |
|
233 apply(simp) |
|
234 apply(simp) |
|
235 apply(erule Prf_elims) |
|
236 apply(simp) |
|
237 apply(case_tac vs) |
|
238 apply(simp) |
|
239 apply(simp) |
|
240 done |
|
241 |
|
242 lemma retrieve_afuse: |
|
243 assumes "\<Turnstile> v : r" |
|
244 shows "retrieve (fuse bs (internalise r)) v = bs @ retrieve (internalise r) v" |
|
245 using assms |
|
246 by (simp_all add: retrieve_afuse2 aerase_internalise) |
|
247 |
|
248 |
|
249 lemma retrieve_encode: |
|
250 assumes "\<Turnstile> v : r" |
|
251 shows "code v = retrieve (internalise r) v" |
|
252 using assms |
|
253 apply(induct v r) |
|
254 apply(simp_all add: retrieve_afuse retrieve_encode_STARS) |
|
255 done |
|
256 |
|
257 |
|
258 lemma alex_append: |
|
259 "alex r (s1 @ s2) = alex (alex r s1) s2" |
|
260 apply(induct s1 arbitrary: r s2) |
|
261 apply(simp_all) |
|
262 done |
|
263 |
|
264 lemma ders_append: |
|
265 shows "ders (s1 @ s2) r = ders s2 (ders s1 r)" |
|
266 apply(induct s1 arbitrary: s2 r) |
|
267 apply(auto) |
|
268 done |
|
269 |
|
270 |
|
271 |
|
272 |
|
273 lemma Q00: |
|
274 assumes "s \<in> r \<rightarrow> v" |
|
275 shows "\<Turnstile> v : r" |
|
276 using assms |
|
277 apply(induct) |
|
278 apply(auto intro: Prf.intros) |
|
279 by (metis Prf.intros(6) Prf_elims(6) insert_iff list.simps(15) val.inject(5)) |
|
280 |
|
281 lemma Qa: |
|
282 assumes "anullable r" |
|
283 shows "retrieve r (mkeps (aerase r)) = amkeps r" |
|
284 using assms |
|
285 apply(induct r) |
|
286 apply(auto) |
|
287 using anullable_correctness apply auto[1] |
|
288 apply (simp add: anullable_correctness) |
|
289 by (simp add: anullable_correctness) |
|
290 |
|
291 |
|
292 lemma Qb: |
|
293 assumes "\<Turnstile> v : der c (aerase r)" |
|
294 shows "retrieve (ader c r) v = retrieve r (injval (aerase r) c v)" |
|
295 using assms |
|
296 apply(induct r arbitrary: v c) |
|
297 apply(simp_all) |
|
298 using Prf_elims(1) apply blast |
|
299 using Prf_elims(1) apply blast |
|
300 apply(auto)[1] |
|
301 using Prf_elims(4) apply fastforce |
|
302 using Prf_elims(1) apply blast |
|
303 apply(auto split: if_splits)[1] |
|
304 apply(auto elim!: Prf_elims)[1] |
|
305 apply(rotate_tac 1) |
|
306 apply(drule_tac x="v2" in meta_spec) |
|
307 apply(drule_tac x="c" in meta_spec) |
|
308 apply(drule meta_mp) |
|
309 apply(simp) |
|
310 apply(drule sym) |
|
311 apply(simp) |
|
312 apply(subst retrieve_afuse2) |
|
313 apply (simp add: aerase_ader) |
|
314 apply (simp add: Qa) |
|
315 using anullable_correctness apply auto[1] |
|
316 apply(auto elim!: Prf_elims)[1] |
|
317 using anullable_correctness apply auto[1] |
|
318 apply(auto elim!: Prf_elims)[1] |
|
319 apply(auto elim!: Prf_elims)[1] |
|
320 apply(auto elim!: Prf_elims)[1] |
|
321 by (simp add: retrieve_afuse2 aerase_ader) |
|
322 |
|
323 |
|
324 |
|
325 |
|
326 lemma MAIN: |
|
327 assumes "\<Turnstile> v : ders s r" |
|
328 shows "code (flex r id s v) = retrieve (alex (internalise r) s) v" |
|
329 using assms |
|
330 apply(induct s arbitrary: r v rule: rev_induct) |
|
331 apply(simp) |
|
332 apply (simp add: retrieve_encode) |
|
333 apply(simp add: flex_append alex_append) |
|
334 apply(subst Qb) |
|
335 apply (simp add: aerase_internalise ders_append aerase_alex) |
|
336 apply(simp add: aerase_alex aerase_internalise) |
|
337 apply(drule_tac x="r" in meta_spec) |
|
338 apply(drule_tac x="injval (ders xs r) x v" in meta_spec) |
|
339 apply(drule meta_mp) |
|
340 apply (simp add: Prf_injval ders_append) |
|
341 apply(simp) |
|
342 done |
|
343 |
|
344 fun alexer where |
|
345 "alexer r s = (if anullable (alex (internalise r) s) then |
|
346 decode (amkeps (alex (internalise r) s)) r else None)" |
|
347 |
|
348 |
|
349 lemma FIN: |
|
350 "alexer r s = lexer r s" |
|
351 apply(auto split: prod.splits) |
|
352 apply (smt MAIN Q00 Qa aerase_alex aerase_internalise anullable_correctness decode_code lexer_correctness(1) lexer_flex mkeps_nullable) |
|
353 apply (simp add: aerase_internalise anullable_correctness[symmetric] lexer_flex aerase_alex) |
|
354 done |
|
355 |
|
356 unused_thms |
|
357 |
491 end |
358 end |