1 |
1 |
2 theory LexerExt |
2 theory LexerExt |
3 imports Main |
3 imports SpecExt |
4 begin |
4 begin |
5 |
5 |
6 |
6 |
7 section {* Sequential Composition of Languages *} |
7 section {* The Lexer Functions by Sulzmann and Lu *} |
8 |
|
9 definition |
|
10 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
|
11 where |
|
12 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
|
13 |
|
14 text {* Two Simple Properties about Sequential Composition *} |
|
15 |
|
16 lemma Sequ_empty [simp]: |
|
17 shows "A ;; {[]} = A" |
|
18 and "{[]} ;; A = A" |
|
19 by (simp_all add: Sequ_def) |
|
20 |
|
21 lemma Sequ_null [simp]: |
|
22 shows "A ;; {} = {}" |
|
23 and "{} ;; A = {}" |
|
24 by (simp_all add: Sequ_def) |
|
25 |
|
26 lemma Sequ_assoc: |
|
27 shows "A ;; (B ;; C) = (A ;; B) ;; C" |
|
28 apply(auto simp add: Sequ_def) |
|
29 apply(metis append_assoc) |
|
30 apply(metis) |
|
31 done |
|
32 |
|
33 lemma Sequ_UNION: |
|
34 shows "(\<Union>x\<in>A. B ;; C x) = B ;; (\<Union>x\<in>A. C x)" |
|
35 by (auto simp add: Sequ_def) |
|
36 |
|
37 |
|
38 section {* Semantic Derivative (Left Quotient) of Languages *} |
|
39 |
|
40 definition |
|
41 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
|
42 where |
|
43 "Der c A \<equiv> {s. c # s \<in> A}" |
|
44 |
|
45 definition |
|
46 Ders :: "string \<Rightarrow> string set \<Rightarrow> string set" |
|
47 where |
|
48 "Ders s A \<equiv> {s'. s @ s' \<in> A}" |
|
49 |
|
50 lemma Der_null [simp]: |
|
51 shows "Der c {} = {}" |
|
52 unfolding Der_def |
|
53 by auto |
|
54 |
|
55 lemma Der_empty [simp]: |
|
56 shows "Der c {[]} = {}" |
|
57 unfolding Der_def |
|
58 by auto |
|
59 |
|
60 lemma Der_char [simp]: |
|
61 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
62 unfolding Der_def |
|
63 by auto |
|
64 |
|
65 lemma Der_Sequ [simp]: |
|
66 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
67 unfolding Der_def Sequ_def |
|
68 by (auto simp add: Cons_eq_append_conv) |
|
69 |
|
70 lemma Der_union [simp]: |
|
71 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
72 unfolding Der_def |
|
73 by auto |
|
74 |
|
75 lemma Der_UNION: |
|
76 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
|
77 by (auto simp add: Der_def) |
|
78 |
|
79 |
|
80 section {* Power operation for Sets *} |
|
81 |
|
82 fun |
|
83 Pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101) |
|
84 where |
|
85 "A \<up> 0 = {[]}" |
|
86 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
|
87 |
|
88 lemma Pow_empty [simp]: |
|
89 shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)" |
|
90 by(induct n) (auto simp add: Sequ_def) |
|
91 |
|
92 lemma Der_Pow [simp]: |
|
93 shows "Der c (A \<up> (Suc n)) = |
|
94 (Der c A) ;; (A \<up> n) \<union> (if [] \<in> A then Der c (A \<up> n) else {})" |
|
95 unfolding Der_def Sequ_def |
|
96 by(auto simp add: Cons_eq_append_conv Sequ_def) |
|
97 |
|
98 lemma Der_Pow_subseteq: |
|
99 assumes "[] \<in> A" |
|
100 shows "Der c (A \<up> n) \<subseteq> (Der c A) ;; (A \<up> n)" |
|
101 using assms |
|
102 apply(induct n) |
|
103 apply(simp add: Sequ_def Der_def) |
|
104 apply(simp) |
|
105 apply(rule conjI) |
|
106 apply (smt Sequ_def append_Nil2 mem_Collect_eq Sequ_assoc subsetI) |
|
107 apply(subgoal_tac "((Der c A) ;; (A \<up> n)) \<subseteq> ((Der c A) ;; (A ;; (A \<up> n)))") |
|
108 apply(auto)[1] |
|
109 by (smt Sequ_def append_Nil2 mem_Collect_eq Sequ_assoc subsetI) |
|
110 |
|
111 lemma test: |
|
112 shows "(\<Union>x\<le>Suc n. Der c (A \<up> x)) = (\<Union>x\<le>n. Der c A ;; A \<up> x)" |
|
113 apply(induct n) |
|
114 apply(simp) |
|
115 apply(auto)[1] |
|
116 apply(case_tac xa) |
|
117 apply(simp) |
|
118 apply(simp) |
|
119 apply(auto)[1] |
|
120 apply(case_tac "[] \<in> A") |
|
121 apply(simp) |
|
122 apply(simp) |
|
123 by (smt Der_Pow Der_Pow_subseteq UN_insert atMost_Suc sup.orderE sup_bot.right_neutral) |
|
124 |
|
125 lemma test2: |
|
126 shows "(\<Union>x\<in>(Suc ` A). Der c (B \<up> x)) = (\<Union>x\<in>A. Der c B ;; B \<up> x)" |
|
127 apply(auto)[1] |
|
128 apply(case_tac "[] \<in> B") |
|
129 apply(simp) |
|
130 using Der_Pow_subseteq apply blast |
|
131 apply(simp) |
|
132 done |
|
133 |
|
134 |
|
135 section {* Kleene Star for Languages *} |
|
136 |
|
137 definition |
|
138 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) where |
|
139 "A\<star> = (\<Union>n. A \<up> n)" |
|
140 |
|
141 lemma Star_empty [intro]: |
|
142 shows "[] \<in> A\<star>" |
|
143 unfolding Star_def |
|
144 by auto |
|
145 |
|
146 lemma Star_step [intro]: |
|
147 assumes "s1 \<in> A" "s2 \<in> A\<star>" |
|
148 shows "s1 @ s2 \<in> A\<star>" |
|
149 proof - |
|
150 from assms obtain n where "s1 \<in>A" "s2 \<in> A \<up> n" |
|
151 unfolding Star_def by auto |
|
152 then have "s1 @ s2 \<in> A ;; (A \<up> n)" |
|
153 by (auto simp add: Sequ_def) |
|
154 then have "s1 @ s2 \<in> A \<up> (Suc n)" |
|
155 by simp |
|
156 then show "s1 @ s2 \<in> A\<star>" |
|
157 unfolding Star_def |
|
158 by (auto simp del: Pow.simps) |
|
159 qed |
|
160 |
|
161 lemma star_cases: |
|
162 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
|
163 unfolding Star_def |
|
164 apply(simp add: Sequ_def) |
|
165 apply(auto) |
|
166 apply(case_tac xa) |
|
167 apply(auto simp add: Sequ_def) |
|
168 apply(rule_tac x="Suc xa" in exI) |
|
169 apply(auto simp add: Sequ_def) |
|
170 done |
|
171 |
|
172 lemma Der_Star1: |
|
173 shows "Der c (A ;; A\<star>) = (Der c A) ;; A\<star>" |
|
174 proof - |
|
175 have "(Der c A) ;; A\<star> = (Der c A) ;; (\<Union>n. A \<up> n)" |
|
176 unfolding Star_def by simp |
|
177 also have "... = (\<Union>n. Der c A ;; A \<up> n)" |
|
178 unfolding Sequ_UNION by simp |
|
179 also have "... = (\<Union>x\<in>(Suc ` UNIV). Der c (A \<up> x))" |
|
180 unfolding test2 by simp |
|
181 also have "... = (\<Union>n. Der c (A \<up> (Suc n)))" |
|
182 by (simp) |
|
183 also have "... = Der c (\<Union>n. A \<up> (Suc n))" |
|
184 unfolding Der_UNION by simp |
|
185 also have "... = Der c (A ;; (\<Union>n. A \<up> n))" |
|
186 by (simp only: Pow.simps Sequ_UNION) |
|
187 finally show "Der c (A ;; A\<star>) = (Der c A) ;; A\<star>" |
|
188 unfolding Star_def[symmetric] by blast |
|
189 qed |
|
190 |
|
191 lemma Der_star [simp]: |
|
192 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
|
193 proof - |
|
194 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
|
195 by (simp only: star_cases[symmetric]) |
|
196 also have "... = Der c (A ;; A\<star>)" |
|
197 by (simp only: Der_union Der_empty) (simp) |
|
198 also have "... = (Der c A) ;; A\<star>" |
|
199 using Der_Star1 by simp |
|
200 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
|
201 qed |
|
202 |
|
203 |
|
204 |
|
205 |
|
206 section {* Regular Expressions *} |
|
207 |
|
208 datatype rexp = |
|
209 ZERO |
|
210 | ONE |
|
211 | CHAR char |
|
212 | SEQ rexp rexp |
|
213 | ALT rexp rexp |
|
214 | STAR rexp |
|
215 | UPNTIMES rexp nat |
|
216 | NTIMES rexp nat |
|
217 | FROMNTIMES rexp nat |
|
218 | NMTIMES rexp nat nat |
|
219 | PLUS rexp |
|
220 |
|
221 section {* Semantics of Regular Expressions *} |
|
222 |
|
223 fun |
|
224 L :: "rexp \<Rightarrow> string set" |
|
225 where |
|
226 "L (ZERO) = {}" |
|
227 | "L (ONE) = {[]}" |
|
228 | "L (CHAR c) = {[c]}" |
|
229 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
|
230 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
|
231 | "L (STAR r) = (L r)\<star>" |
|
232 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
|
233 | "L (NTIMES r n) = (L r) \<up> n" |
|
234 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
|
235 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
|
236 | "L (PLUS r) = (\<Union>i\<in> {1..} . (L r) \<up> i)" |
|
237 |
|
238 section {* Nullable, Derivatives *} |
|
239 |
|
240 fun |
|
241 nullable :: "rexp \<Rightarrow> bool" |
|
242 where |
|
243 "nullable (ZERO) = False" |
|
244 | "nullable (ONE) = True" |
|
245 | "nullable (CHAR c) = False" |
|
246 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
|
247 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
|
248 | "nullable (STAR r) = True" |
|
249 | "nullable (UPNTIMES r n) = True" |
|
250 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
|
251 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
|
252 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
|
253 | "nullable (PLUS r) = (nullable r)" |
|
254 |
|
255 fun |
|
256 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
|
257 where |
|
258 "der c (ZERO) = ZERO" |
|
259 | "der c (ONE) = ZERO" |
|
260 | "der c (CHAR d) = (if c = d then ONE else ZERO)" |
|
261 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
|
262 | "der c (SEQ r1 r2) = |
|
263 (if nullable r1 |
|
264 then ALT (SEQ (der c r1) r2) (der c r2) |
|
265 else SEQ (der c r1) r2)" |
|
266 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
|
267 | "der c (UPNTIMES r 0) = ZERO" |
|
268 | "der c (UPNTIMES r (Suc n)) = SEQ (der c r) (UPNTIMES r n)" |
|
269 | "der c (NTIMES r 0) = ZERO" |
|
270 | "der c (NTIMES r (Suc n)) = SEQ (der c r) (NTIMES r n)" |
|
271 | "der c (FROMNTIMES r 0) = SEQ (der c r) (FROMNTIMES r 0)" |
|
272 | "der c (FROMNTIMES r (Suc n)) = SEQ (der c r) (FROMNTIMES r n)" |
|
273 | "der c (NMTIMES r n m) = |
|
274 (if m < n then ZERO |
|
275 else (if n = 0 then (if m = 0 then ZERO else |
|
276 SEQ (der c r) (UPNTIMES r (m - 1))) else |
|
277 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
|
278 | "der c (PLUS r) = SEQ (der c r) (STAR r)" |
|
279 |
|
280 fun |
|
281 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
|
282 where |
|
283 "ders [] r = r" |
|
284 | "ders (c # s) r = ders s (der c r)" |
|
285 |
|
286 |
|
287 lemma nullable_correctness: |
|
288 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
|
289 apply(induct r) |
|
290 apply(auto simp add: Sequ_def) |
|
291 done |
|
292 |
|
293 lemma Der_Pow_notin: |
|
294 assumes "[] \<notin> A" |
|
295 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" |
|
296 using assms |
|
297 by(simp) |
|
298 |
|
299 lemma der_correctness: |
|
300 shows "L (der c r) = Der c (L r)" |
|
301 apply(induct c r rule: der.induct) |
|
302 apply(simp_all add: nullable_correctness)[7] |
|
303 apply(simp only: der.simps L.simps) |
|
304 apply(simp only: Der_UNION) |
|
305 apply(simp only: Sequ_UNION[symmetric]) |
|
306 apply(simp add: test) |
|
307 apply(simp) |
|
308 (* NTIMES *) |
|
309 apply(simp only: L.simps der.simps) |
|
310 apply(simp) |
|
311 apply(rule impI) |
|
312 apply (simp add: Der_Pow_subseteq sup_absorb1) |
|
313 (* FROMNTIMES *) |
|
314 apply(simp only: der.simps) |
|
315 apply(simp only: L.simps) |
|
316 apply(simp) |
|
317 using Der_star Star_def apply auto[1] |
|
318 apply(simp only: der.simps) |
|
319 apply(simp only: L.simps) |
|
320 apply(simp add: Der_UNION) |
|
321 apply(subst Sequ_UNION[symmetric]) |
|
322 apply(subst test2[symmetric]) |
|
323 apply(subgoal_tac "(Suc ` {n..}) = {Suc n..}") |
|
324 apply simp |
|
325 apply(auto simp add: image_def)[1] |
|
326 using Suc_le_D apply blast |
|
327 (* NMTIMES *) |
|
328 apply(case_tac "n \<le> m") |
|
329 prefer 2 |
|
330 apply(simp only: der.simps if_True) |
|
331 apply(simp only: L.simps) |
|
332 apply(simp) |
|
333 apply(auto) |
|
334 apply(subst (asm) Sequ_UNION[symmetric]) |
|
335 apply(subst (asm) test[symmetric]) |
|
336 apply(auto simp add: Der_UNION)[1] |
|
337 apply(auto simp add: Der_UNION)[1] |
|
338 apply(subst Sequ_UNION[symmetric]) |
|
339 apply(subst test[symmetric]) |
|
340 apply(auto)[1] |
|
341 apply(subst (asm) Sequ_UNION[symmetric]) |
|
342 apply(subst (asm) test2[symmetric]) |
|
343 apply(auto simp add: Der_UNION)[1] |
|
344 apply(subst Sequ_UNION[symmetric]) |
|
345 apply(subst test2[symmetric]) |
|
346 apply(auto simp add: Der_UNION)[1] |
|
347 (* PLUS *) |
|
348 apply(auto simp add: Sequ_def Star_def)[1] |
|
349 apply(simp add: Der_UNION) |
|
350 apply(rule_tac x="Suc xa" in bexI) |
|
351 apply(auto simp add: Sequ_def Der_def)[2] |
|
352 apply (metis append_Cons) |
|
353 apply(simp add: Der_UNION) |
|
354 apply(erule_tac bexE) |
|
355 apply(case_tac xa) |
|
356 apply(simp) |
|
357 apply(simp) |
|
358 apply(auto) |
|
359 apply(auto simp add: Sequ_def Der_def)[1] |
|
360 using Star_def apply auto[1] |
|
361 apply(case_tac "[] \<in> L r") |
|
362 apply(auto) |
|
363 using Der_UNION Der_star Star_def by fastforce |
|
364 |
|
365 |
|
366 lemma ders_correctness: |
|
367 shows "L (ders s r) = Ders s (L r)" |
|
368 apply(induct s arbitrary: r) |
|
369 apply(simp_all add: Ders_def der_correctness Der_def) |
|
370 done |
|
371 |
|
372 lemma ders_ZERO: |
|
373 shows "ders s (ZERO) = ZERO" |
|
374 apply(induct s) |
|
375 apply(simp_all) |
|
376 done |
|
377 |
|
378 lemma ders_ONE: |
|
379 shows "ders s (ONE) = (if s = [] then ONE else ZERO)" |
|
380 apply(induct s) |
|
381 apply(simp_all add: ders_ZERO) |
|
382 done |
|
383 |
|
384 lemma ders_CHAR: |
|
385 shows "ders s (CHAR c) = (if s = [c] then ONE else |
|
386 (if s = [] then (CHAR c) else ZERO))" |
|
387 apply(induct s) |
|
388 apply(simp_all add: ders_ZERO ders_ONE) |
|
389 done |
|
390 |
|
391 lemma ders_ALT: |
|
392 shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)" |
|
393 apply(induct s arbitrary: r1 r2) |
|
394 apply(simp_all) |
|
395 done |
|
396 |
|
397 section {* Values *} |
|
398 |
|
399 datatype val = |
|
400 Void |
|
401 | Char char |
|
402 | Seq val val |
|
403 | Right val |
|
404 | Left val |
|
405 | Stars "val list" |
|
406 |
|
407 |
|
408 section {* The string behind a value *} |
|
409 |
|
410 fun |
|
411 flat :: "val \<Rightarrow> string" |
|
412 where |
|
413 "flat (Void) = []" |
|
414 | "flat (Char c) = [c]" |
|
415 | "flat (Left v) = flat v" |
|
416 | "flat (Right v) = flat v" |
|
417 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)" |
|
418 | "flat (Stars []) = []" |
|
419 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" |
|
420 |
|
421 lemma flat_Stars [simp]: |
|
422 "flat (Stars vs) = concat (map flat vs)" |
|
423 by (induct vs) (auto) |
|
424 |
|
425 |
|
426 section {* Relation between values and regular expressions *} |
|
427 |
|
428 inductive |
|
429 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
|
430 where |
|
431 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" |
|
432 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" |
|
433 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2" |
|
434 | "\<turnstile> Void : ONE" |
|
435 | "\<turnstile> Char c : CHAR c" |
|
436 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : STAR r" |
|
437 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<le> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : UPNTIMES r n" |
|
438 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs = n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NTIMES r n" |
|
439 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : FROMNTIMES r n" |
|
440 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> n; length vs \<le> m\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : NMTIMES r n m" |
|
441 | "\<lbrakk>\<forall>v \<in> set vs. \<turnstile> v : r; length vs \<ge> 1\<rbrakk> \<Longrightarrow> \<turnstile> Stars vs : PLUS r" |
|
442 |
|
443 |
|
444 inductive_cases Prf_elims: |
|
445 "\<turnstile> v : ZERO" |
|
446 "\<turnstile> v : SEQ r1 r2" |
|
447 "\<turnstile> v : ALT r1 r2" |
|
448 "\<turnstile> v : ONE" |
|
449 "\<turnstile> v : CHAR c" |
|
450 (* "\<turnstile> vs : STAR r"*) |
|
451 |
|
452 lemma Prf_STAR: |
|
453 assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r" |
|
454 shows "concat (map flat vs) \<in> L r\<star>" |
|
455 using assms |
|
456 apply(induct vs) |
|
457 apply(auto) |
|
458 done |
|
459 |
|
460 lemma Prf_Pow: |
|
461 assumes "\<forall>v\<in>set vs. \<turnstile> v : r \<and> flat v \<in> L r" |
|
462 shows "concat (map flat vs) \<in> L r \<up> length vs" |
|
463 using assms |
|
464 apply(induct vs) |
|
465 apply(auto simp add: Sequ_def) |
|
466 done |
|
467 |
|
468 lemma Prf_flat_L: |
|
469 assumes "\<turnstile> v : r" shows "flat v \<in> L r" |
|
470 using assms |
|
471 apply(induct v r rule: Prf.induct) |
|
472 apply(auto simp add: Sequ_def) |
|
473 apply(rule Prf_STAR) |
|
474 apply(simp) |
|
475 apply(rule_tac x="length vs" in bexI) |
|
476 apply(rule Prf_Pow) |
|
477 apply(simp) |
|
478 apply(simp) |
|
479 apply(rule Prf_Pow) |
|
480 apply(simp) |
|
481 apply(rule_tac x="length vs" in bexI) |
|
482 apply(rule Prf_Pow) |
|
483 apply(simp) |
|
484 apply(simp) |
|
485 apply(rule_tac x="length vs" in bexI) |
|
486 apply(rule Prf_Pow) |
|
487 apply(simp) |
|
488 apply(simp) |
|
489 using Prf_Pow by blast |
|
490 |
|
491 lemma Star_Pow: |
|
492 assumes "s \<in> A \<up> n" |
|
493 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A) \<and> (length ss = n)" |
|
494 using assms |
|
495 apply(induct n arbitrary: s) |
|
496 apply(auto simp add: Sequ_def) |
|
497 apply(drule_tac x="s2" in meta_spec) |
|
498 apply(auto) |
|
499 apply(rule_tac x="s1#ss" in exI) |
|
500 apply(simp) |
|
501 done |
|
502 |
|
503 lemma Star_string: |
|
504 assumes "s \<in> A\<star>" |
|
505 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
|
506 using assms |
|
507 apply(auto simp add: Star_def) |
|
508 using Star_Pow by blast |
|
509 |
|
510 |
|
511 lemma Star_val: |
|
512 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
|
513 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
|
514 using assms |
|
515 apply(induct ss) |
|
516 apply(auto) |
|
517 apply (metis empty_iff list.set(1)) |
|
518 by (metis concat.simps(2) list.simps(9) set_ConsD) |
|
519 |
|
520 lemma Star_val_length: |
|
521 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
|
522 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r) \<and> (length vs) = (length ss)" |
|
523 using assms |
|
524 apply(induct ss) |
|
525 apply(auto) |
|
526 by (metis List.bind_def bind_simps(2) length_Suc_conv set_ConsD) |
|
527 |
|
528 |
|
529 |
|
530 |
|
531 |
|
532 lemma L_flat_Prf2: |
|
533 assumes "s \<in> L r" shows "\<exists>v. \<turnstile> v : r \<and> flat v = s" |
|
534 using assms |
|
535 apply(induct r arbitrary: s) |
|
536 apply(auto simp add: Sequ_def intro: Prf.intros) |
|
537 using Prf.intros(1) flat.simps(5) apply blast |
|
538 using Prf.intros(2) flat.simps(3) apply blast |
|
539 using Prf.intros(3) flat.simps(4) apply blast |
|
540 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)") |
|
541 apply(auto)[1] |
|
542 apply(rule_tac x="Stars vs" in exI) |
|
543 apply(simp) |
|
544 apply(rule Prf.intros) |
|
545 apply(simp) |
|
546 using Star_string Star_val apply force |
|
547 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
548 apply(auto)[1] |
|
549 apply(rule_tac x="Stars vs" in exI) |
|
550 apply(simp) |
|
551 apply(rule Prf.intros) |
|
552 apply(simp) |
|
553 apply(simp) |
|
554 using Star_Pow Star_val_length apply blast |
|
555 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x2)") |
|
556 apply(auto)[1] |
|
557 apply(rule_tac x="Stars vs" in exI) |
|
558 apply(simp) |
|
559 apply(rule Prf.intros) |
|
560 apply(simp) |
|
561 apply(simp) |
|
562 using Star_Pow Star_val_length apply blast |
|
563 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
564 apply(auto)[1] |
|
565 apply(rule_tac x="Stars vs" in exI) |
|
566 apply(simp) |
|
567 apply(rule Prf.intros) |
|
568 apply(simp) |
|
569 apply(simp) |
|
570 using Star_Pow Star_val_length apply blast |
|
571 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
572 apply(auto)[1] |
|
573 apply(rule_tac x="Stars vs" in exI) |
|
574 apply(simp) |
|
575 apply(rule Prf.intros) |
|
576 apply(simp) |
|
577 apply(simp) |
|
578 apply(simp) |
|
579 using Star_Pow Star_val_length apply blast |
|
580 apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> (length vs = x)") |
|
581 apply(auto)[1] |
|
582 apply(rule_tac x="Stars vs" in exI) |
|
583 apply(simp) |
|
584 apply(rule Prf.intros) |
|
585 apply(simp) |
|
586 apply(simp) |
|
587 using Star_Pow Star_val_length apply blast |
|
588 done |
|
589 |
|
590 lemma L_flat_Prf: |
|
591 "L(r) = {flat v | v. \<turnstile> v : r}" |
|
592 using Prf_flat_L L_flat_Prf2 by blast |
|
593 |
|
594 |
|
595 section {* Sulzmann and Lu functions *} |
|
596 |
8 |
597 fun |
9 fun |
598 mkeps :: "rexp \<Rightarrow> val" |
10 mkeps :: "rexp \<Rightarrow> val" |
599 where |
11 where |
600 "mkeps(ONE) = Void" |
12 "mkeps(ONE) = Void" |
601 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
13 | "mkeps(SEQ r1 r2) = Seq (mkeps r1) (mkeps r2)" |
602 | "mkeps(ALT r1 r2) = (if nullable r1 then Left (mkeps r1) else Right (mkeps r2))" |
14 | "mkeps(ALT r1 r2) = (if nullable(r1) then Left (mkeps r1) else Right (mkeps r2))" |
603 | "mkeps(STAR r) = Stars []" |
15 | "mkeps(STAR r) = Stars []" |
604 | "mkeps(UPNTIMES r n) = Stars []" |
16 | "mkeps(UPNTIMES r n) = Stars []" |
605 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
17 | "mkeps(NTIMES r n) = Stars (replicate n (mkeps r))" |
606 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))" |
18 | "mkeps(FROMNTIMES r n) = Stars (replicate n (mkeps r))" |
607 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))" |
19 | "mkeps(NMTIMES r n m) = Stars (replicate n (mkeps r))" |
608 | "mkeps(PLUS r) = Stars ([mkeps r])" |
20 |
609 |
|
610 |
|
611 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
21 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val" |
612 where |
22 where |
613 "injval (CHAR d) c Void = Char d" |
23 "injval (CHAR d) c Void = Char d" |
614 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
24 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)" |
615 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
25 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)" |
616 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
26 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2" |
617 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
27 | "injval (SEQ r1 r2) c (Left (Seq v1 v2)) = Seq (injval r1 c v1) v2" |
618 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
28 | "injval (SEQ r1 r2) c (Right v2) = Seq (mkeps r1) (injval r2 c v2)" |
619 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
29 | "injval (STAR r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
620 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
30 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
621 | "injval (NTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
31 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
622 | "injval (FROMNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
32 | "injval (UPNTIMES r n) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
623 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
33 | "injval (NMTIMES r n m) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
624 | "injval (PLUS r) c (Seq v (Stars vs)) = Stars ((injval r c v) # vs)" |
34 |
625 |
35 fun |
626 section {* Mkeps, injval *} |
36 lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
627 |
37 where |
628 lemma mkeps_nullable: |
38 "lexer r [] = (if nullable r then Some(mkeps r) else None)" |
629 assumes "nullable(r)" |
39 | "lexer r (c#s) = (case (lexer (der c r) s) of |
630 shows "\<turnstile> mkeps r : r" |
40 None \<Rightarrow> None |
631 using assms |
41 | Some(v) \<Rightarrow> Some(injval r c v))" |
632 apply(induct r rule: mkeps.induct) |
42 |
633 apply(auto intro: Prf.intros) |
43 |
634 by (metis Prf.intros(10) in_set_replicate length_replicate not_le order_refl) |
44 |
|
45 section {* Mkeps, Injval Properties *} |
635 |
46 |
636 lemma mkeps_flat: |
47 lemma mkeps_flat: |
637 assumes "nullable(r)" |
48 assumes "nullable(r)" |
638 shows "flat (mkeps r) = []" |
49 shows "flat (mkeps r) = []" |
639 using assms |
50 using assms |
640 apply (induct rule: nullable.induct) |
51 apply(induct rule: nullable.induct) |
641 apply(auto) |
52 apply(auto) |
642 by meson |
53 by presburger |
643 |
54 |
644 |
55 |
645 lemma Prf_injval: |
56 lemma mkeps_nullable: |
646 assumes "\<turnstile> v : der c r" |
57 assumes "nullable(r)" |
647 shows "\<turnstile> (injval r c v) : r" |
58 shows "\<Turnstile> mkeps r : r" |
648 using assms |
59 using assms |
649 apply(induct r arbitrary: c v rule: rexp.induct) |
60 apply(induct rule: nullable.induct) |
650 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits) |
61 apply(auto intro: Prf.intros split: if_splits) |
651 (* STAR *) |
62 using Prf.intros(8) apply force |
652 apply(rotate_tac 2) |
63 apply(subst append.simps(1)[symmetric]) |
653 apply(erule Prf.cases) |
64 apply(rule Prf.intros) |
654 apply(simp_all) |
65 apply(simp) |
655 apply(auto) |
66 apply(simp) |
656 using Prf.intros(6) apply auto[1] |
67 apply (simp add: mkeps_flat) |
657 (* UPNTIMES *) |
68 apply(simp) |
658 apply(case_tac x2) |
69 using Prf.intros(9) apply force |
659 apply(simp) |
70 apply(subst append.simps(1)[symmetric]) |
660 using Prf_elims(1) apply auto[1] |
71 apply(rule Prf.intros) |
661 apply(simp) |
72 apply(simp) |
662 apply(erule Prf.cases) |
73 apply(simp) |
663 apply(simp_all) |
74 apply (simp add: mkeps_flat) |
664 apply(clarify) |
75 apply(simp) |
665 apply(rotate_tac 2) |
76 using Prf.intros(11) apply force |
666 apply(erule Prf.cases) |
77 apply(subst append.simps(1)[symmetric]) |
667 apply(simp_all) |
78 apply(rule Prf.intros) |
668 apply(clarify) |
79 apply(simp) |
669 using Prf.intros(7) apply auto[1] |
80 apply(simp) |
670 (* NTIMES *) |
81 apply (simp add: mkeps_flat) |
671 apply(case_tac x2) |
82 apply(simp) |
672 apply(simp) |
83 apply(simp) |
673 using Prf_elims(1) apply auto[1] |
|
674 apply(simp) |
|
675 apply(erule Prf.cases) |
|
676 apply(simp_all) |
|
677 apply(clarify) |
|
678 apply(rotate_tac 2) |
|
679 apply(erule Prf.cases) |
|
680 apply(simp_all) |
|
681 apply(clarify) |
|
682 using Prf.intros(8) apply auto[1] |
|
683 (* FROMNTIMES *) |
|
684 apply(case_tac x2) |
|
685 apply(simp) |
|
686 apply(erule Prf.cases) |
|
687 apply(simp_all) |
|
688 apply(clarify) |
|
689 apply(rotate_tac 2) |
|
690 apply(erule Prf.cases) |
|
691 apply(simp_all) |
|
692 apply(clarify) |
|
693 using Prf.intros(9) apply auto[1] |
|
694 apply(rotate_tac 1) |
|
695 apply(erule Prf.cases) |
|
696 apply(simp_all) |
|
697 apply(clarify) |
|
698 apply(rotate_tac 2) |
|
699 apply(erule Prf.cases) |
|
700 apply(simp_all) |
|
701 apply(clarify) |
|
702 using Prf.intros(9) apply auto |
|
703 (* NMTIMES *) |
|
704 apply(rotate_tac 3) |
|
705 apply(erule Prf.cases) |
|
706 apply(simp_all) |
|
707 apply(clarify) |
|
708 apply(rule Prf.intros) |
|
709 apply(auto)[2] |
|
710 apply simp |
|
711 apply(rotate_tac 4) |
|
712 apply(erule Prf.cases) |
|
713 apply(simp_all) |
|
714 apply(clarify) |
|
715 apply(rule Prf.intros) |
|
716 apply(auto)[2] |
|
717 apply simp |
|
718 (* PLUS *) |
|
719 apply(rotate_tac 2) |
|
720 apply(erule Prf.cases) |
|
721 apply(simp_all) |
|
722 apply(auto) |
|
723 using Prf.intros apply auto[1] |
|
724 done |
84 done |
725 |
85 |
726 |
86 |
727 lemma Prf_injval_flat: |
87 lemma Prf_injval_flat: |
728 assumes "\<turnstile> v : der c r" |
88 assumes "\<Turnstile> v : der c r" |
729 shows "flat (injval r c v) = c # (flat v)" |
89 shows "flat (injval r c v) = c # (flat v)" |
730 using assms |
90 using assms |
731 apply(induct arbitrary: v rule: der.induct) |
91 apply(induct arbitrary: v rule: der.induct) |
732 apply(auto elim!: Prf_elims split: if_splits) |
92 apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits) |
733 apply(metis mkeps_flat) |
|
734 apply(rotate_tac 2) |
|
735 apply(erule Prf.cases) |
|
736 apply(simp_all) |
|
737 apply(rotate_tac 2) |
|
738 apply(erule Prf.cases) |
|
739 apply(simp_all) |
|
740 apply(rotate_tac 2) |
|
741 apply(erule Prf.cases) |
|
742 apply(simp_all) |
|
743 apply(rotate_tac 2) |
|
744 apply(erule Prf.cases) |
|
745 apply(simp_all) |
|
746 apply(rotate_tac 2) |
|
747 apply(erule Prf.cases) |
|
748 apply(simp_all) |
|
749 apply(rotate_tac 3) |
|
750 apply(erule Prf.cases) |
|
751 apply(simp_all) |
|
752 apply(rotate_tac 4) |
|
753 apply(erule Prf.cases) |
|
754 apply(simp_all) |
|
755 apply(rotate_tac 2) |
|
756 apply(erule Prf.cases) |
|
757 apply(simp_all) |
|
758 done |
93 done |
759 |
94 |
760 |
95 lemma Prf_injval: |
761 section {* Our Alternative Posix definition *} |
96 assumes "\<Turnstile> v : der c r" |
762 |
97 shows "\<Turnstile> (injval r c v) : r" |
763 inductive |
|
764 Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
|
765 where |
|
766 Posix_ONE: "[] \<in> ONE \<rightarrow> Void" |
|
767 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)" |
|
768 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
|
769 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
|
770 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
|
771 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r1 \<and> s\<^sub>4 \<in> L r2)\<rbrakk> \<Longrightarrow> |
|
772 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
|
773 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
774 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> |
|
775 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
|
776 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
|
777 | Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r n \<rightarrow> Stars vs; flat v \<noteq> []; |
|
778 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r n))\<rbrakk> |
|
779 \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
|
780 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []" |
|
781 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
|
782 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r n))\<rbrakk> |
|
783 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
|
784 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
|
785 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
|
786 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r n))\<rbrakk> |
|
787 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
|
788 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
|
789 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
|
790 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))\<rbrakk> |
|
791 \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)" |
|
792 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow> s \<in> NMTIMES r 0 m \<rightarrow> Stars vs" |
|
793 | Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
|
794 \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk> |
|
795 \<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)" |
|
796 |
|
797 inductive_cases Posix_elims: |
|
798 "s \<in> ZERO \<rightarrow> v" |
|
799 "s \<in> ONE \<rightarrow> v" |
|
800 "s \<in> CHAR c \<rightarrow> v" |
|
801 "s \<in> ALT r1 r2 \<rightarrow> v" |
|
802 "s \<in> SEQ r1 r2 \<rightarrow> v" |
|
803 "s \<in> STAR r \<rightarrow> v" |
|
804 |
|
805 lemma Posix1: |
|
806 assumes "s \<in> r \<rightarrow> v" |
|
807 shows "s \<in> L r" "flat v = s" |
|
808 using assms |
98 using assms |
809 apply (induct s r v rule: Posix.induct) |
99 apply(induct r arbitrary: c v rule: rexp.induct) |
810 apply(auto simp add: Sequ_def) |
100 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)[6] |
811 apply(rule_tac x="Suc x" in bexI) |
101 apply(simp add: Prf_injval_flat) |
812 apply(auto simp add: Sequ_def) |
102 apply(simp) |
813 apply(rule_tac x="Suc x" in bexI) |
103 apply(case_tac x2) |
814 using Sequ_def apply auto[2] |
104 apply(simp) |
815 apply(simp add: Star_def) |
105 apply(erule Prf_elims) |
816 apply(rule_tac x="Suc x" in bexI) |
106 apply(simp) |
817 apply(auto simp add: Sequ_def) |
107 apply(erule Prf_elims) |
818 apply(simp add: Star_def) |
108 apply(simp) |
819 apply(clarify) |
109 apply(erule Prf_elims) |
820 apply(rule_tac x="Suc x" in bexI) |
110 apply(simp) |
821 apply(auto simp add: Sequ_def) |
111 using Prf.intros(7) Prf_injval_flat apply auto[1] |
|
112 apply(simp) |
|
113 apply(case_tac x2) |
|
114 apply(simp) |
|
115 apply(erule Prf_elims) |
|
116 apply(simp) |
|
117 apply(erule Prf_elims) |
|
118 apply(simp) |
|
119 apply(erule Prf_elims) |
|
120 apply(simp) |
|
121 apply(subst append.simps(2)[symmetric]) |
|
122 apply(rule Prf.intros) |
|
123 apply(simp add: Prf_injval_flat) |
|
124 apply(simp) |
|
125 apply(simp) |
|
126 prefer 2 |
|
127 apply(simp) |
|
128 apply(case_tac "x3a < x2") |
|
129 apply(simp) |
|
130 apply(erule Prf_elims) |
|
131 apply(simp) |
|
132 apply(case_tac x2) |
|
133 apply(simp) |
|
134 apply(case_tac x3a) |
|
135 apply(simp) |
|
136 apply(erule Prf_elims) |
|
137 apply(simp) |
|
138 apply(erule Prf_elims) |
|
139 apply(simp) |
|
140 apply(erule Prf_elims) |
|
141 apply(simp) |
|
142 using Prf.intros(12) Prf_injval_flat apply auto[1] |
|
143 apply(simp) |
|
144 apply(erule Prf_elims) |
|
145 apply(simp) |
|
146 apply(erule Prf_elims) |
|
147 apply(simp) |
|
148 apply(subst append.simps(2)[symmetric]) |
|
149 apply(rule Prf.intros) |
|
150 apply(simp add: Prf_injval_flat) |
|
151 apply(simp) |
|
152 apply(simp) |
|
153 apply(simp) |
|
154 apply(simp) |
|
155 using Prf.intros(12) Prf_injval_flat apply auto[1] |
|
156 apply(case_tac x2) |
|
157 apply(simp) |
|
158 apply(erule Prf_elims) |
|
159 apply(simp) |
|
160 apply(erule Prf_elims) |
|
161 apply(simp_all) |
|
162 apply (simp add: Prf.intros(10) Prf_injval_flat) |
|
163 using Prf.intros(10) Prf_injval_flat apply auto[1] |
|
164 apply(erule Prf_elims) |
|
165 apply(simp) |
|
166 apply(erule Prf_elims) |
|
167 apply(simp_all) |
|
168 apply(subst append.simps(2)[symmetric]) |
|
169 apply(rule Prf.intros) |
|
170 apply(simp add: Prf_injval_flat) |
|
171 apply(simp) |
|
172 apply(simp) |
|
173 using Prf.intros(10) Prf_injval_flat apply auto |
822 done |
174 done |
823 |
175 |
824 |
176 |
825 lemma |
177 |
826 "([] @ []) \<in> PLUS (ONE) \<rightarrow> Stars ([Void])" |
178 text {* |
827 apply(rule Posix_PLUS1) |
179 Mkeps and injval produce, or preserve, Posix values. |
828 apply(rule Posix.intros) |
180 *} |
829 apply(rule Posix.intros) |
|
830 apply(simp) |
|
831 apply(simp) |
|
832 done |
|
833 |
|
834 lemma |
|
835 assumes "s \<in> r \<rightarrow> v" "flat v \<noteq> []" "\<forall>s' \<in> L r. length s' < length s" |
|
836 shows "([] @ (s @ [])) \<in> PLUS (ALT ONE r) \<rightarrow> Stars ([Left Void, Right v])" |
|
837 using assms |
|
838 oops |
|
839 |
|
840 lemma |
|
841 "([] @ ([] @ [])) \<in> FROMNTIMES (ONE) (Suc (Suc 0)) \<rightarrow> Stars ([Void, Void])" |
|
842 apply(rule Posix.intros) |
|
843 apply(rule Posix.intros) |
|
844 apply(rule Posix.intros) |
|
845 apply(rule Posix.intros) |
|
846 apply(rule Posix.intros) |
|
847 apply(rule Posix.intros) |
|
848 apply(auto) |
|
849 done |
|
850 |
|
851 |
|
852 lemma |
|
853 assumes "s \<in> r \<rightarrow> v" "flat v \<noteq> []" |
|
854 "s \<in> PLUS (ALT ONE r) \<rightarrow> Stars ([Left(Void), Right(v)])" |
|
855 shows "False" |
|
856 using assms |
|
857 apply(rotate_tac 2) |
|
858 apply(erule_tac Posix.cases) |
|
859 apply(simp_all) |
|
860 apply(auto) |
|
861 oops |
|
862 |
|
863 |
|
864 |
|
865 |
|
866 |
|
867 lemma Posix1a: |
|
868 assumes "s \<in> r \<rightarrow> v" |
|
869 shows "\<turnstile> v : r" |
|
870 using assms |
|
871 apply(induct s r v rule: Posix.induct) |
|
872 apply(auto intro: Prf.intros) |
|
873 apply(rule Prf.intros) |
|
874 apply(auto)[1] |
|
875 apply(rotate_tac 3) |
|
876 apply(erule Prf.cases) |
|
877 apply(simp_all) |
|
878 apply(rule Prf.intros) |
|
879 apply(auto)[1] |
|
880 apply(rotate_tac 3) |
|
881 apply(erule Prf.cases) |
|
882 apply(simp_all) |
|
883 apply(rotate_tac 3) |
|
884 apply(erule Prf.cases) |
|
885 apply(simp_all) |
|
886 apply(rule Prf.intros) |
|
887 apply(auto)[1] |
|
888 apply(rotate_tac 3) |
|
889 apply(erule Prf.cases) |
|
890 apply(simp_all) |
|
891 apply(rotate_tac 3) |
|
892 apply(erule Prf.cases) |
|
893 apply(simp_all) |
|
894 apply(rule Prf.intros) |
|
895 apply(auto)[1] |
|
896 apply(rotate_tac 3) |
|
897 apply(erule Prf.cases) |
|
898 apply(simp_all) |
|
899 apply(rotate_tac 3) |
|
900 apply(erule Prf.cases) |
|
901 apply(simp_all) |
|
902 apply(rule Prf.intros) |
|
903 apply(auto)[2] |
|
904 apply(rotate_tac 3) |
|
905 apply(erule Prf.cases) |
|
906 apply(simp_all) |
|
907 apply(rule Prf.intros) |
|
908 apply(auto)[3] |
|
909 apply(rotate_tac 3) |
|
910 apply(erule Prf.cases) |
|
911 apply(simp_all) |
|
912 apply(rotate_tac 3) |
|
913 apply(erule Prf.cases) |
|
914 apply(simp_all) |
|
915 apply(rotate_tac 3) |
|
916 apply(erule Prf.cases) |
|
917 apply(simp_all) |
|
918 apply(rule Prf.intros) |
|
919 apply(auto)[3] |
|
920 apply(rotate_tac 3) |
|
921 apply(erule Prf.cases) |
|
922 apply(simp_all) |
|
923 apply(erule Prf.cases) |
|
924 apply(simp_all) |
|
925 apply(rotate_tac 3) |
|
926 apply(erule Prf.cases) |
|
927 apply(simp_all) |
|
928 apply(rule Prf.intros) |
|
929 apply(auto) |
|
930 done |
|
931 |
|
932 |
|
933 lemma Posix_NTIMES_mkeps: |
|
934 assumes "[] \<in> r \<rightarrow> mkeps r" |
|
935 shows "[] \<in> NTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
|
936 apply(induct n) |
|
937 apply(simp) |
|
938 apply (rule Posix_NTIMES2) |
|
939 apply(simp) |
|
940 apply(subst append_Nil[symmetric]) |
|
941 apply (rule Posix_NTIMES1) |
|
942 apply(auto) |
|
943 apply(rule assms) |
|
944 done |
|
945 |
|
946 lemma Posix_FROMNTIMES_mkeps: |
|
947 assumes "[] \<in> r \<rightarrow> mkeps r" |
|
948 shows "[] \<in> FROMNTIMES r n \<rightarrow> Stars (replicate n (mkeps r))" |
|
949 apply(induct n) |
|
950 apply(simp) |
|
951 apply (rule Posix_FROMNTIMES2) |
|
952 apply (rule Posix.intros) |
|
953 apply(simp) |
|
954 apply(subst append_Nil[symmetric]) |
|
955 apply (rule Posix_FROMNTIMES1) |
|
956 apply(auto) |
|
957 apply(rule assms) |
|
958 done |
|
959 |
|
960 lemma Posix_NMTIMES_mkeps: |
|
961 assumes "[] \<in> r \<rightarrow> mkeps r" "n \<le> m" |
|
962 shows "[] \<in> NMTIMES r n m \<rightarrow> Stars (replicate n (mkeps r))" |
|
963 using assms(2) |
|
964 apply(induct n arbitrary: m) |
|
965 apply(simp) |
|
966 apply(rule Posix.intros) |
|
967 apply(rule Posix.intros) |
|
968 apply(case_tac m) |
|
969 apply(simp) |
|
970 apply(simp) |
|
971 apply(subst append_Nil[symmetric]) |
|
972 apply(rule Posix.intros) |
|
973 apply(auto) |
|
974 apply(rule assms) |
|
975 done |
|
976 |
|
977 |
|
978 |
181 |
979 lemma Posix_mkeps: |
182 lemma Posix_mkeps: |
980 assumes "nullable r" |
183 assumes "nullable r" |
981 shows "[] \<in> r \<rightarrow> mkeps r" |
184 shows "[] \<in> r \<rightarrow> mkeps r" |
982 using assms |
185 using assms |
983 apply(induct r rule: nullable.induct) |
186 apply(induct r rule: nullable.induct) |
984 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def) |
187 apply(auto intro: Posix.intros simp add: nullable_correctness Sequ_def) |
985 apply(subst append.simps(1)[symmetric]) |
188 apply(subst append.simps(1)[symmetric]) |
986 apply(rule Posix.intros) |
189 apply(rule Posix.intros) |
987 apply(auto) |
190 apply(auto) |
988 apply(case_tac n) |
191 done |
989 apply(simp) |
192 |
990 apply (simp add: Posix_NTIMES2) |
193 lemma test: |
991 apply(simp) |
194 assumes "s \<in> der c (FROMNTIMES r 0) \<rightarrow> v" |
992 apply(subst append.simps(1)[symmetric]) |
195 shows "XXX" |
993 apply(rule Posix.intros) |
196 using assms |
994 apply(auto) |
197 apply(simp) |
995 apply(rule Posix_NTIMES_mkeps) |
198 apply(erule Posix_elims) |
996 apply(simp) |
199 apply(drule FROMNTIMES_0) |
997 apply(rule Posix.intros) |
|
998 apply(rule Posix.intros) |
|
999 apply(case_tac n) |
|
1000 apply(simp) |
|
1001 apply(rule Posix.intros) |
|
1002 apply(rule Posix.intros) |
|
1003 apply(simp) |
|
1004 apply(subst append.simps(1)[symmetric]) |
|
1005 apply(rule Posix.intros) |
|
1006 apply(auto) |
|
1007 apply(rule Posix_FROMNTIMES_mkeps) |
|
1008 apply(simp) |
|
1009 apply(rule Posix.intros) |
|
1010 apply(rule Posix.intros) |
|
1011 apply(case_tac n) |
|
1012 apply(simp) |
|
1013 apply(rule Posix.intros) |
|
1014 apply(rule Posix.intros) |
|
1015 apply(simp) |
|
1016 apply(case_tac m) |
|
1017 apply(simp) |
|
1018 apply(simp) |
|
1019 apply(subst append_Nil[symmetric]) |
|
1020 apply(rule Posix.intros) |
|
1021 apply(auto) |
|
1022 apply(rule Posix_NMTIMES_mkeps) |
|
1023 apply(auto) |
|
1024 apply(subst append_Nil[symmetric]) |
|
1025 apply(rule Posix.intros) |
|
1026 apply(auto) |
|
1027 apply(rule Posix.intros) |
|
1028 done |
|
1029 |
|
1030 |
|
1031 lemma Posix_determ: |
|
1032 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
1033 shows "v1 = v2" |
|
1034 using assms |
|
1035 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
1036 case (Posix_ONE v2) |
|
1037 have "[] \<in> ONE \<rightarrow> v2" by fact |
|
1038 then show "Void = v2" by cases auto |
|
1039 next |
|
1040 case (Posix_CHAR c v2) |
|
1041 have "[c] \<in> CHAR c \<rightarrow> v2" by fact |
|
1042 then show "Char c = v2" by cases auto |
|
1043 next |
|
1044 case (Posix_ALT1 s r1 v r2 v2) |
|
1045 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
1046 moreover |
|
1047 have "s \<in> r1 \<rightarrow> v" by fact |
|
1048 then have "s \<in> L r1" by (simp add: Posix1) |
|
1049 ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto |
|
1050 moreover |
|
1051 have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
1052 ultimately have "v = v'" by simp |
|
1053 then show "Left v = v2" using eq by simp |
|
1054 next |
|
1055 case (Posix_ALT2 s r2 v r1 v2) |
|
1056 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
1057 moreover |
|
1058 have "s \<notin> L r1" by fact |
|
1059 ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" |
|
1060 by cases (auto simp add: Posix1) |
|
1061 moreover |
|
1062 have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
1063 ultimately have "v = v'" by simp |
|
1064 then show "Right v = v2" using eq by simp |
|
1065 next |
|
1066 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v') |
|
1067 have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" |
|
1068 "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" |
|
1069 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r1 \<and> s\<^sub>4 \<in> L r2)" by fact+ |
|
1070 then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" |
|
1071 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1072 using Posix1(1) by fastforce+ |
|
1073 moreover |
|
1074 have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" |
|
1075 "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ |
|
1076 ultimately show "Seq v1 v2 = v'" by simp |
|
1077 next |
|
1078 case (Posix_STAR1 s1 r v s2 vs v2) |
|
1079 have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" |
|
1080 "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
1081 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+ |
|
1082 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
1083 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1084 using Posix1(1) apply fastforce |
|
1085 apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2) |
|
1086 using Posix1(2) by blast |
|
1087 moreover |
|
1088 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1089 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1090 ultimately show "Stars (v # vs) = v2" by auto |
|
1091 next |
|
1092 case (Posix_STAR2 r v2) |
|
1093 have "[] \<in> STAR r \<rightarrow> v2" by fact |
|
1094 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
1095 next |
|
1096 case (Posix_UPNTIMES1 s1 r v s2 n vs v2) |
|
1097 have "(s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> v2" |
|
1098 "s1 \<in> r \<rightarrow> v" "s2 \<in> (UPNTIMES r n) \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
1099 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r n))" by fact+ |
|
1100 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (UPNTIMES r n) \<rightarrow> (Stars vs')" |
|
1101 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1102 using Posix1(1) apply fastforce |
|
1103 apply (metis Posix1(1) Posix_UPNTIMES1.hyps(6) append_Nil append_Nil2) |
|
1104 using Posix1(2) by blast |
|
1105 moreover |
|
1106 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1107 "\<And>v2. s2 \<in> UPNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1108 ultimately show "Stars (v # vs) = v2" by auto |
|
1109 next |
|
1110 case (Posix_UPNTIMES2 r n v2) |
|
1111 have "[] \<in> UPNTIMES r n \<rightarrow> v2" by fact |
|
1112 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
1113 next |
|
1114 case (Posix_NTIMES2 r v2) |
|
1115 have "[] \<in> NTIMES r 0 \<rightarrow> v2" by fact |
|
1116 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
1117 next |
|
1118 case (Posix_NTIMES1 s1 r v s2 n vs v2) |
|
1119 have "(s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> v2" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
|
1120 "s1 \<in> r \<rightarrow> v" "s2 \<in> (NTIMES r n) \<rightarrow> Stars vs" |
|
1121 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r n))" by fact+ |
|
1122 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r n) \<rightarrow> (Stars vs')" |
|
1123 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1124 using Posix1(1) apply fastforce |
|
1125 by (metis Posix1(1) Posix_NTIMES1.hyps(6) append_Nil append_Nil2) |
|
1126 moreover |
|
1127 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1128 "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1129 ultimately show "Stars (v # vs) = v2" by auto |
|
1130 next |
|
1131 case (Posix_FROMNTIMES2 s r v1 v2) |
|
1132 have "s \<in> FROMNTIMES r 0 \<rightarrow> v2" "s \<in> STAR r \<rightarrow> Stars v1" |
|
1133 "\<And>v3. s \<in> STAR r \<rightarrow> v3 \<Longrightarrow> Stars v1 = v3" by fact+ |
|
1134 then show ?case |
|
1135 apply(cases) |
|
1136 apply(auto) |
200 apply(auto) |
1137 done |
201 oops |
1138 next |
|
1139 case (Posix_FROMNTIMES1 s1 r v s2 n vs v2) |
|
1140 have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2" |
|
1141 "s1 \<in> r \<rightarrow> v" "s2 \<in> (FROMNTIMES r n) \<rightarrow> Stars vs" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
|
1142 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r n))" by fact+ |
|
1143 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r n) \<rightarrow> (Stars vs')" |
|
1144 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1145 using Posix1(1) apply fastforce |
|
1146 by (metis Posix1(1) Posix_FROMNTIMES1.hyps(6) append_Nil append_Nil2) |
|
1147 moreover |
|
1148 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1149 "\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1150 ultimately show "Stars (v # vs) = v2" by auto |
|
1151 next |
|
1152 case (Posix_NMTIMES2 s r m v1 v2) |
|
1153 have "s \<in> NMTIMES r 0 m \<rightarrow> v2" "s \<in> UPNTIMES r m \<rightarrow> Stars v1" |
|
1154 "\<And>v3. s \<in> UPNTIMES r m \<rightarrow> v3 \<Longrightarrow> Stars v1 = v3" by fact+ |
|
1155 then show ?case |
|
1156 apply(cases) |
|
1157 apply(auto) |
|
1158 done |
|
1159 next |
|
1160 case (Posix_NMTIMES1 s1 r v s2 n m vs v2) |
|
1161 have "(s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> v2" |
|
1162 "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n m) \<rightarrow> Stars vs" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
|
1163 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))" by fact+ |
|
1164 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NMTIMES r n m) \<rightarrow> (Stars vs')" |
|
1165 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1166 using Posix1(1) apply fastforce |
|
1167 by (metis Posix1(1) Posix_NMTIMES1.hyps(6) self_append_conv self_append_conv2) |
|
1168 moreover |
|
1169 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1170 "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1171 ultimately show "Stars (v # vs) = v2" by auto |
|
1172 next |
|
1173 case (Posix_PLUS1 s1 r v s2 vs v2) |
|
1174 have "(s1 @ s2) \<in> PLUS r \<rightarrow> v2" |
|
1175 "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<rightarrow> Stars vs" (*"flat v = [] \<Longrightarrow> flat (Stars vs) = []"*) |
|
1176 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+ |
|
1177 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
1178 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
1179 using Posix1(1) apply fastforce |
|
1180 by (metis Posix1(1) Posix_PLUS1.hyps(6) append_self_conv append_self_conv2) |
|
1181 moreover |
|
1182 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
1183 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
1184 ultimately show "Stars (v # vs) = v2" by auto |
|
1185 qed |
|
1186 |
|
1187 lemma NTIMES_Stars: |
|
1188 assumes "\<turnstile> v : NTIMES r n" |
|
1189 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs = n" |
|
1190 using assms |
|
1191 apply(induct n arbitrary: v) |
|
1192 apply(erule Prf.cases) |
|
1193 apply(simp_all) |
|
1194 apply(erule Prf.cases) |
|
1195 apply(simp_all) |
|
1196 done |
|
1197 |
|
1198 lemma UPNTIMES_Stars: |
|
1199 assumes "\<turnstile> v : UPNTIMES r n" |
|
1200 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> length vs \<le> n" |
|
1201 using assms |
|
1202 apply(induct n arbitrary: v) |
|
1203 apply(erule Prf.cases) |
|
1204 apply(simp_all) |
|
1205 apply(erule Prf.cases) |
|
1206 apply(simp_all) |
|
1207 done |
|
1208 |
|
1209 lemma FROMNTIMES_Stars: |
|
1210 assumes "\<turnstile> v : FROMNTIMES r n" |
|
1211 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs" |
|
1212 using assms |
|
1213 apply(induct n arbitrary: v) |
|
1214 apply(erule Prf.cases) |
|
1215 apply(simp_all) |
|
1216 apply(erule Prf.cases) |
|
1217 apply(simp_all) |
|
1218 done |
|
1219 |
|
1220 lemma PLUS_Stars: |
|
1221 assumes "\<turnstile> v : PLUS r" |
|
1222 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> 1 \<le> length vs" |
|
1223 using assms |
|
1224 apply(erule_tac Prf.cases) |
|
1225 apply(simp_all) |
|
1226 done |
|
1227 |
|
1228 lemma NMTIMES_Stars: |
|
1229 assumes "\<turnstile> v : NMTIMES r n m" |
|
1230 shows "\<exists>vs. v = Stars vs \<and> (\<forall>v \<in> set vs. \<turnstile> v : r) \<and> n \<le> length vs \<and> length vs \<le> m" |
|
1231 using assms |
|
1232 apply(induct n arbitrary: m v) |
|
1233 apply(erule Prf.cases) |
|
1234 apply(simp_all) |
|
1235 apply(erule Prf.cases) |
|
1236 apply(simp_all) |
|
1237 done |
|
1238 |
|
1239 |
202 |
1240 lemma Posix_injval: |
203 lemma Posix_injval: |
1241 assumes "s \<in> (der c r) \<rightarrow> v" |
204 assumes "s \<in> (der c r) \<rightarrow> v" |
1242 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
205 shows "(c # s) \<in> r \<rightarrow> (injval r c v)" |
1243 using assms |
206 using assms |
1244 proof(induct r arbitrary: s v rule: rexp.induct) |
207 proof(induct r arbitrary: s v rule: rexp.induct) |
1245 case ZERO |
208 case ZERO |
1246 have "s \<in> der c ZERO \<rightarrow> v" by fact |
209 have "s \<in> der c ZERO \<rightarrow> v" by fact |
1382 by (simp add: der_correctness Der_def) |
395 by (simp add: der_correctness Der_def) |
1383 ultimately |
396 ultimately |
1384 have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros) |
397 have "((c # s1) @ s2) \<in> STAR r \<rightarrow> Stars (injval r c v1 # vs)" by (rule Posix.intros) |
1385 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp) |
398 then show "(c # s) \<in> STAR r \<rightarrow> injval (STAR r) c v" using cons by(simp) |
1386 qed |
399 qed |
1387 next |
400 next |
1388 case (UPNTIMES r n) |
401 case (NTIMES r n s v) |
1389 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
402 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1390 have "s \<in> der c (UPNTIMES r n) \<rightarrow> v" by fact |
403 have "s \<in> der c (NTIMES r n) \<rightarrow> v" by fact |
1391 then consider |
404 then consider |
1392 (cons) m v1 vs s1 s2 where |
405 (cons) v1 vs s1 s2 where |
1393 "n = Suc m" |
|
1394 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
406 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1395 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (UPNTIMES r m) \<rightarrow> (Stars vs)" |
407 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n" |
1396 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r m))" |
408 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" |
1397 apply(case_tac n) |
409 apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits) |
1398 apply(simp) |
410 apply(erule Posix_elims) |
1399 using Posix_elims(1) apply blast |
411 apply(simp) |
1400 apply(simp) |
412 apply(subgoal_tac "\<exists>vss. v2 = Stars vss") |
1401 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
413 apply(clarify) |
1402 by (metis Posix1a UPNTIMES_Stars) |
414 apply(drule_tac x="v1" in meta_spec) |
1403 then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" |
415 apply(drule_tac x="vss" in meta_spec) |
|
416 apply(drule_tac x="s1" in meta_spec) |
|
417 apply(drule_tac x="s2" in meta_spec) |
|
418 apply(simp add: der_correctness Der_def) |
|
419 apply(erule Posix_elims) |
|
420 apply(auto) |
|
421 done |
|
422 then show "(c # s) \<in> (NTIMES r n) \<rightarrow> injval (NTIMES r n) c v" |
1404 proof (cases) |
423 proof (cases) |
1405 case cons |
424 case cons |
1406 have "n = Suc m" by fact |
|
1407 moreover |
|
1408 have "s1 \<in> der c r \<rightarrow> v1" by fact |
425 have "s1 \<in> der c r \<rightarrow> v1" by fact |
1409 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
426 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
1410 moreover |
427 moreover |
1411 have "s2 \<in> UPNTIMES r m \<rightarrow> Stars vs" by fact |
428 have "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> Stars vs" by fact |
1412 moreover |
429 moreover |
1413 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact |
430 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact |
1414 then have "flat (injval r c v1) = (c # s1)" by (rule Posix1) |
431 then have "flat (injval r c v1) = (c # s1)" by (rule Posix1) |
1415 then have "flat (injval r c v1) \<noteq> []" by simp |
432 then have "flat (injval r c v1) \<noteq> []" by simp |
1416 moreover |
433 moreover |
1417 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (UPNTIMES r m))" by fact |
434 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" by fact |
1418 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (UPNTIMES r m))" |
435 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r (n - 1)))" |
1419 by (simp add: der_correctness Der_def) |
436 by (simp add: der_correctness Der_def) |
1420 ultimately |
437 ultimately |
1421 have "((c # s1) @ s2) \<in> UPNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
438 have "((c # s1) @ s2) \<in> NTIMES r n \<rightarrow> Stars (injval r c v1 # vs)" |
1422 apply(rule_tac Posix.intros(8)) |
439 apply (rule_tac Posix.intros) |
1423 apply(simp_all) |
440 apply(simp_all) |
1424 done |
441 apply(case_tac n) |
1425 then show "(c # s) \<in> UPNTIMES r n \<rightarrow> injval (UPNTIMES r n) c v" using cons by(simp) |
442 apply(simp) |
1426 qed |
443 using Posix_elims(1) NTIMES.prems apply auto[1] |
1427 next |
444 apply(simp) |
1428 case (NTIMES r n) |
445 done |
|
446 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp) |
|
447 qed |
|
448 next |
|
449 case (FROMNTIMES r n s v) |
1429 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
450 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1430 have "s \<in> der c (NTIMES r n) \<rightarrow> v" by fact |
451 have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact |
1431 then consider |
452 then consider |
1432 (cons) m v1 vs s1 s2 where |
453 (cons) v1 vs s1 s2 where |
1433 "n = Suc m" |
454 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1434 "v = Seq v1 (Stars vs)" "s = s1 @ s2" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
455 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> (Stars vs)" "0 < n" |
1435 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r m) \<rightarrow> (Stars vs)" |
456 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))" |
1436 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r m))" |
457 | (null) v1 where |
1437 apply(case_tac n) |
458 "v = Seq v1 (Stars [])" |
1438 apply(simp) |
459 "s \<in> der c r \<rightarrow> v1" "[] \<in> (FROMNTIMES r 0) \<rightarrow> (Stars [])" "n = 0" |
1439 using Posix_elims(1) apply blast |
460 (* here *) |
1440 apply(simp) |
461 apply(auto elim: Posix_elims simp add: der_correctness Der_def intro: Posix.intros split: if_splits) |
1441 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
462 apply(erule Posix_elims) |
1442 by (metis NTIMES_Stars Posix1a) |
463 apply(simp) |
1443 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" |
464 apply(case_tac "n = 0") |
|
465 apply(simp) |
|
466 apply(drule FROMNTIMES_0) |
|
467 apply(simp) |
|
468 using FROMNTIMES_0 Posix_mkeps apply force |
|
469 apply(subgoal_tac "\<exists>vss. v2 = Stars vss") |
|
470 apply(clarify) |
|
471 apply(drule_tac x="v1" in meta_spec) |
|
472 apply(drule_tac x="vss" in meta_spec) |
|
473 apply(drule_tac x="s1" in meta_spec) |
|
474 apply(drule_tac x="s2" in meta_spec) |
|
475 apply(simp add: der_correctness Der_def) |
|
476 apply(case_tac "n = 0") |
|
477 apply(simp) |
|
478 apply(simp) |
|
479 apply(rotate_tac 4) |
|
480 apply(erule Posix_elims) |
|
481 apply(auto)[2] |
|
482 done |
|
483 then show "(c # s) \<in> (FROMNTIMES r n) \<rightarrow> injval (FROMNTIMES r n) c v" |
1444 proof (cases) |
484 proof (cases) |
1445 case cons |
485 case cons |
1446 have "n = Suc m" by fact |
|
1447 moreover |
|
1448 have "s1 \<in> der c r \<rightarrow> v1" by fact |
486 have "s1 \<in> der c r \<rightarrow> v1" by fact |
1449 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
487 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
1450 moreover |
488 moreover |
1451 have "flat v = [] \<Longrightarrow> flat (Stars vs) = []" by fact |
489 have "s2 \<in> (FROMNTIMES r (n - 1)) \<rightarrow> Stars vs" by fact |
1452 moreover |
490 moreover |
1453 have "s2 \<in> NTIMES r m \<rightarrow> Stars vs" by fact |
491 have "(c # s1) \<in> r \<rightarrow> injval r c v1" by fact |
1454 moreover |
492 then have "flat (injval r c v1) = (c # s1)" by (rule Posix1) |
1455 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r m))" by fact |
493 then have "flat (injval r c v1) \<noteq> []" by simp |
1456 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r m))" |
494 moreover |
|
495 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))" by fact |
|
496 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r (n - 1)))" |
1457 by (simp add: der_correctness Der_def) |
497 by (simp add: der_correctness Der_def) |
1458 ultimately |
498 ultimately |
1459 have "((c # s1) @ s2) \<in> NTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
499 have "((c # s1) @ s2) \<in> FROMNTIMES r n \<rightarrow> Stars (injval r c v1 # vs)" |
1460 apply(rule_tac Posix.intros(10)) |
500 apply (rule_tac Posix.intros) |
1461 apply(simp_all) |
501 apply(simp_all) |
1462 by (simp add: Posix1(2)) |
502 apply(case_tac n) |
1463 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp) |
503 apply(simp) |
1464 qed |
504 using Posix_elims(1) FROMNTIMES.prems apply auto[1] |
1465 next |
505 using cons(5) apply blast |
1466 case (FROMNTIMES r n) |
506 apply(simp) |
1467 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
507 done |
1468 have "s \<in> der c (FROMNTIMES r n) \<rightarrow> v" by fact |
508 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
1469 then consider |
509 next |
1470 (null) v1 vs s1 s2 where |
510 case null |
1471 "n = 0" |
511 have "s \<in> der c r \<rightarrow> v1" by fact |
1472 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
512 then have "(c # s) \<in> r \<rightarrow> injval r c v1" using IH by simp |
1473 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r 0) \<rightarrow> (Stars vs)" |
|
1474 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r 0))" |
|
1475 | (cons) m v1 vs s1 s2 where |
|
1476 "n = Suc m" |
|
1477 "v = Seq v1 (Stars vs)" "s = s1 @ s2" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
|
1478 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<rightarrow> (Stars vs)" |
|
1479 "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" |
|
1480 apply(case_tac n) |
|
1481 apply(simp) |
|
1482 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
|
1483 defer |
|
1484 apply (metis FROMNTIMES_Stars Posix1a) |
|
1485 apply(rotate_tac 5) |
|
1486 apply(erule Posix.cases) |
|
1487 apply(simp_all) |
|
1488 apply(clarify) |
|
1489 by (simp add: Posix_FROMNTIMES2) |
|
1490 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" |
|
1491 proof (cases) |
|
1492 case cons |
|
1493 have "n = Suc m" by fact |
|
1494 moreover |
513 moreover |
1495 have "s1 \<in> der c r \<rightarrow> v1" by fact |
514 have "[] \<in> (FROMNTIMES r 0) \<rightarrow> Stars []" by fact |
1496 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
515 moreover |
1497 moreover |
516 have "(c # s) \<in> r \<rightarrow> injval r c v1" by fact |
1498 have "s2 \<in> FROMNTIMES r m \<rightarrow> Stars vs" by fact |
517 then have "flat (injval r c v1) = (c # s)" by (rule Posix1) |
1499 moreover |
518 then have "flat (injval r c v1) \<noteq> []" by simp |
1500 have "flat v = [] \<Longrightarrow> flat (Stars vs) = []" by fact |
|
1501 moreover |
|
1502 have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" by fact |
|
1503 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" |
|
1504 by (simp add: der_correctness Der_def) |
|
1505 ultimately |
519 ultimately |
1506 have "((c # s1) @ s2) \<in> FROMNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
520 have "((c # s) @ []) \<in> FROMNTIMES r 1 \<rightarrow> Stars [injval r c v1]" |
1507 apply(rule_tac Posix.intros(12)) |
521 apply (rule_tac Posix.intros) |
1508 apply(simp_all) |
522 apply(simp_all) |
1509 by (simp add: Posix1(2)) |
523 done |
1510 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
524 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null |
1511 next |
525 apply(simp) |
1512 case null |
526 apply(erule Posix_elims) |
1513 then have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)" |
527 apply(auto) |
1514 apply(rule_tac Posix.intros) |
528 apply(rotate_tac 6) |
1515 apply(rule_tac Posix.intros) |
529 apply(drule FROMNTIMES_0) |
1516 apply(rule IH) |
530 apply(simp) |
1517 apply(simp) |
531 sorry |
1518 apply(rotate_tac 4) |
532 qed |
1519 apply(erule Posix.cases) |
533 next |
1520 apply(simp_all) |
534 case (NMTIMES x1 x2 m s v) |
1521 apply (simp add: Posix1a Prf_injval_flat) |
535 then show ?case sorry |
1522 apply(simp only: Star_def) |
|
1523 apply(simp only: der_correctness Der_def) |
|
1524 apply(simp) |
|
1525 done |
|
1526 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using null by simp |
|
1527 qed |
|
1528 next |
|
1529 case (NMTIMES r n m) |
|
1530 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
|
1531 have "s \<in> der c (NMTIMES r n m) \<rightarrow> v" by fact |
|
1532 then show "(c # s) \<in> (NMTIMES r n m) \<rightarrow> injval (NMTIMES r n m) c v" |
|
1533 apply(case_tac "m < n") |
|
1534 apply(simp) |
|
1535 using Posix_elims(1) apply blast |
|
1536 apply(case_tac n) |
|
1537 apply(simp_all) |
|
1538 apply(case_tac m) |
|
1539 apply(simp) |
|
1540 apply(erule Posix_elims(1)) |
|
1541 apply(simp) |
|
1542 apply(erule Posix.cases) |
|
1543 apply(simp_all) |
|
1544 apply(clarify) |
|
1545 apply(rotate_tac 5) |
|
1546 apply(frule Posix1a) |
|
1547 apply(drule UPNTIMES_Stars) |
|
1548 apply(clarify) |
|
1549 apply(simp) |
|
1550 apply(subst append_Cons[symmetric]) |
|
1551 apply(rule Posix.intros) |
|
1552 apply(rule Posix.intros) |
|
1553 apply(auto) |
|
1554 apply(rule IH) |
|
1555 apply blast |
|
1556 using Posix1a Prf_injval_flat apply auto[1] |
|
1557 apply(simp add: der_correctness Der_def) |
|
1558 apply blast |
|
1559 apply(case_tac m) |
|
1560 apply(simp) |
|
1561 apply(simp) |
|
1562 apply(erule Posix.cases) |
|
1563 apply(simp_all) |
|
1564 apply(clarify) |
|
1565 apply(rotate_tac 6) |
|
1566 apply(frule Posix1a) |
|
1567 apply(drule NMTIMES_Stars) |
|
1568 apply(clarify) |
|
1569 apply(simp) |
|
1570 apply(subst append_Cons[symmetric]) |
|
1571 apply(rule Posix.intros) |
|
1572 apply(rule IH) |
|
1573 apply(blast) |
|
1574 apply(simp) |
|
1575 apply(simp add: der_correctness Der_def) |
|
1576 using Posix1a Prf_injval_flat list.distinct(1) apply auto[1] |
|
1577 apply(simp add: der_correctness Der_def) |
|
1578 done |
|
1579 next |
|
1580 case (PLUS r) |
|
1581 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
|
1582 have "s \<in> der c (PLUS r) \<rightarrow> v" by fact |
|
1583 then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" |
|
1584 apply - |
|
1585 apply(erule Posix.cases) |
|
1586 apply(simp_all) |
|
1587 apply(auto) |
|
1588 apply(rotate_tac 3) |
|
1589 apply(erule Posix.cases) |
|
1590 apply(simp_all) |
|
1591 apply(subst append_Cons[symmetric]) |
|
1592 apply(rule Posix.intros) |
|
1593 using PLUS.hyps apply auto[1] |
|
1594 apply(rule Posix.intros) |
|
1595 apply(simp) |
|
1596 apply(simp) |
|
1597 apply(simp) |
|
1598 apply(simp) |
|
1599 apply(simp) |
|
1600 using Posix1a Prf_injval_flat apply auto[1] |
|
1601 apply(simp add: der_correctness Der_def) |
|
1602 apply(subst append_Nil2[symmetric]) |
|
1603 apply(rule Posix.intros) |
|
1604 using PLUS.hyps apply auto[1] |
|
1605 apply(rule Posix.intros) |
|
1606 apply(simp) |
|
1607 apply(simp) |
|
1608 done |
|
1609 qed |
536 qed |
1610 |
537 |
1611 |
538 |
1612 |
539 section {* Lexer Correctness *} |
1613 section {* The Lexer by Sulzmann and Lu *} |
|
1614 |
|
1615 fun |
|
1616 lexer :: "rexp \<Rightarrow> string \<Rightarrow> val option" |
|
1617 where |
|
1618 "lexer r [] = (if nullable r then Some(mkeps r) else None)" |
|
1619 | "lexer r (c#s) = (case (lexer (der c r) s) of |
|
1620 None \<Rightarrow> None |
|
1621 | Some(v) \<Rightarrow> Some(injval r c v))" |
|
1622 |
|
1623 |
540 |
1624 lemma lexer_correct_None: |
541 lemma lexer_correct_None: |
1625 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
542 shows "s \<notin> L r \<longleftrightarrow> lexer r s = None" |
1626 apply(induct s arbitrary: r) |
543 apply(induct s arbitrary: r) |
1627 apply(simp add: nullable_correctness) |
544 apply(simp add: nullable_correctness) |