|
1 |
|
2 theory SpecExt |
|
3 imports Main "~~/src/HOL/Library/Sublist" |
|
4 begin |
|
5 |
|
6 section {* Sequential Composition of Languages *} |
|
7 |
|
8 definition |
|
9 Sequ :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
|
10 where |
|
11 "A ;; B = {s1 @ s2 | s1 s2. s1 \<in> A \<and> s2 \<in> B}" |
|
12 |
|
13 text {* Two Simple Properties about Sequential Composition *} |
|
14 |
|
15 lemma Sequ_empty_string [simp]: |
|
16 shows "A ;; {[]} = A" |
|
17 and "{[]} ;; A = A" |
|
18 by (simp_all add: Sequ_def) |
|
19 |
|
20 lemma Sequ_empty [simp]: |
|
21 shows "A ;; {} = {}" |
|
22 and "{} ;; A = {}" |
|
23 by (simp_all add: Sequ_def) |
|
24 |
|
25 lemma Sequ_assoc: |
|
26 shows "(A ;; B) ;; C = A ;; (B ;; C)" |
|
27 apply(auto simp add: Sequ_def) |
|
28 apply blast |
|
29 by (metis append_assoc) |
|
30 |
|
31 lemma Sequ_Union_in: |
|
32 shows "(A ;; (\<Union>x\<in> B. C x)) = (\<Union>x\<in> B. A ;; C x)" |
|
33 by (auto simp add: Sequ_def) |
|
34 |
|
35 section {* Semantic Derivative (Left Quotient) of Languages *} |
|
36 |
|
37 definition |
|
38 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
|
39 where |
|
40 "Der c A \<equiv> {s. c # s \<in> A}" |
|
41 |
|
42 definition |
|
43 Ders :: "string \<Rightarrow> string set \<Rightarrow> string set" |
|
44 where |
|
45 "Ders s A \<equiv> {s'. s @ s' \<in> A}" |
|
46 |
|
47 lemma Der_null [simp]: |
|
48 shows "Der c {} = {}" |
|
49 unfolding Der_def |
|
50 by auto |
|
51 |
|
52 lemma Der_empty [simp]: |
|
53 shows "Der c {[]} = {}" |
|
54 unfolding Der_def |
|
55 by auto |
|
56 |
|
57 lemma Der_char [simp]: |
|
58 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
59 unfolding Der_def |
|
60 by auto |
|
61 |
|
62 lemma Der_union [simp]: |
|
63 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
64 unfolding Der_def |
|
65 by auto |
|
66 |
|
67 lemma Der_UNION [simp]: |
|
68 shows "Der c (\<Union>x\<in>A. B x) = (\<Union>x\<in>A. Der c (B x))" |
|
69 by (auto simp add: Der_def) |
|
70 |
|
71 lemma Der_Sequ [simp]: |
|
72 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
73 unfolding Der_def Sequ_def |
|
74 by (auto simp add: Cons_eq_append_conv) |
|
75 |
|
76 |
|
77 section {* Kleene Star for Languages *} |
|
78 |
|
79 inductive_set |
|
80 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
|
81 for A :: "string set" |
|
82 where |
|
83 start[intro]: "[] \<in> A\<star>" |
|
84 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
|
85 |
|
86 (* Arden's lemma *) |
|
87 |
|
88 lemma Star_cases: |
|
89 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
|
90 unfolding Sequ_def |
|
91 by (auto) (metis Star.simps) |
|
92 |
|
93 lemma Star_decomp: |
|
94 assumes "c # x \<in> A\<star>" |
|
95 shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>" |
|
96 using assms |
|
97 by (induct x\<equiv>"c # x" rule: Star.induct) |
|
98 (auto simp add: append_eq_Cons_conv) |
|
99 |
|
100 lemma Star_Der_Sequ: |
|
101 shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>" |
|
102 unfolding Der_def Sequ_def |
|
103 by(auto simp add: Star_decomp) |
|
104 |
|
105 |
|
106 lemma Der_star [simp]: |
|
107 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
|
108 proof - |
|
109 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
|
110 by (simp only: Star_cases[symmetric]) |
|
111 also have "... = Der c (A ;; A\<star>)" |
|
112 by (simp only: Der_union Der_empty) (simp) |
|
113 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
|
114 by simp |
|
115 also have "... = (Der c A) ;; A\<star>" |
|
116 using Star_Der_Sequ by auto |
|
117 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
|
118 qed |
|
119 |
|
120 section {* Power operation for Sets *} |
|
121 |
|
122 fun |
|
123 Pow :: "string set \<Rightarrow> nat \<Rightarrow> string set" ("_ \<up> _" [101, 102] 101) |
|
124 where |
|
125 "A \<up> 0 = {[]}" |
|
126 | "A \<up> (Suc n) = A ;; (A \<up> n)" |
|
127 |
|
128 lemma Pow_empty [simp]: |
|
129 shows "[] \<in> A \<up> n \<longleftrightarrow> (n = 0 \<or> [] \<in> A)" |
|
130 by(induct n) (auto simp add: Sequ_def) |
|
131 |
|
132 lemma Pow_Suc_rev: |
|
133 "A \<up> (Suc n) = (A \<up> n) ;; A" |
|
134 apply(induct n arbitrary: A) |
|
135 apply(simp_all) |
|
136 by (metis Sequ_assoc) |
|
137 |
|
138 |
|
139 lemma Pow_decomp: |
|
140 assumes "c # x \<in> A \<up> n" |
|
141 shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A \<up> (n - 1)" |
|
142 using assms |
|
143 apply(induct n) |
|
144 apply(auto simp add: Cons_eq_append_conv Sequ_def) |
|
145 apply(case_tac n) |
|
146 apply(auto simp add: Sequ_def) |
|
147 apply(blast) |
|
148 done |
|
149 |
|
150 lemma Star_Pow: |
|
151 assumes "s \<in> A\<star>" |
|
152 shows "\<exists>n. s \<in> A \<up> n" |
|
153 using assms |
|
154 apply(induct) |
|
155 apply(auto) |
|
156 apply(rule_tac x="Suc n" in exI) |
|
157 apply(auto simp add: Sequ_def) |
|
158 done |
|
159 |
|
160 lemma Pow_Star: |
|
161 assumes "s \<in> A \<up> n" |
|
162 shows "s \<in> A\<star>" |
|
163 using assms |
|
164 apply(induct n arbitrary: s) |
|
165 apply(auto simp add: Sequ_def) |
|
166 done |
|
167 |
|
168 lemma Der_Pow_0: |
|
169 shows "Der c (A \<up> 0) = {}" |
|
170 by(simp add: Der_def) |
|
171 |
|
172 lemma Der_Pow_Suc: |
|
173 shows "Der c (A \<up> (Suc n)) = (Der c A) ;; (A \<up> n)" |
|
174 unfolding Der_def Sequ_def |
|
175 apply(auto simp add: Cons_eq_append_conv Sequ_def dest!: Pow_decomp) |
|
176 apply(case_tac n) |
|
177 apply(force simp add: Sequ_def)+ |
|
178 done |
|
179 |
|
180 lemma Der_Pow [simp]: |
|
181 shows "Der c (A \<up> n) = (if n = 0 then {} else (Der c A) ;; (A \<up> (n - 1)))" |
|
182 apply(case_tac n) |
|
183 apply(simp_all del: Pow.simps add: Der_Pow_0 Der_Pow_Suc) |
|
184 done |
|
185 |
|
186 lemma Der_Pow_Sequ [simp]: |
|
187 shows "Der c (A ;; A \<up> n) = (Der c A) ;; (A \<up> n)" |
|
188 by (simp only: Pow.simps[symmetric] Der_Pow) (simp) |
|
189 |
|
190 |
|
191 lemma Pow_Sequ_Un: |
|
192 assumes "0 < x" |
|
193 shows "(\<Union>n \<in> {..x}. (A \<up> n)) = ({[]} \<union> (\<Union>n \<in> {..x - Suc 0}. A ;; (A \<up> n)))" |
|
194 using assms |
|
195 apply(auto simp add: Sequ_def) |
|
196 apply(smt Pow.elims Sequ_def Suc_le_mono Suc_pred atMost_iff empty_iff insert_iff mem_Collect_eq) |
|
197 apply(rule_tac x="Suc xa" in bexI) |
|
198 apply(auto simp add: Sequ_def) |
|
199 done |
|
200 |
|
201 lemma Pow_Sequ_Un2: |
|
202 assumes "0 < x" |
|
203 shows "(\<Union>n \<in> {x..}. (A \<up> n)) = (\<Union>n \<in> {x - Suc 0..}. A ;; (A \<up> n))" |
|
204 using assms |
|
205 apply(auto simp add: Sequ_def) |
|
206 apply(case_tac n) |
|
207 apply(auto simp add: Sequ_def) |
|
208 apply fastforce |
|
209 apply(case_tac x) |
|
210 apply(auto) |
|
211 apply(rule_tac x="Suc xa" in bexI) |
|
212 apply(auto simp add: Sequ_def) |
|
213 done |
|
214 |
|
215 section {* Regular Expressions *} |
|
216 |
|
217 datatype rexp = |
|
218 ZERO |
|
219 | ONE |
|
220 | CHAR char |
|
221 | SEQ rexp rexp |
|
222 | ALT rexp rexp |
|
223 | STAR rexp |
|
224 | UPNTIMES rexp nat |
|
225 | NTIMES rexp nat |
|
226 | FROMNTIMES rexp nat |
|
227 | NMTIMES rexp nat nat |
|
228 |
|
229 section {* Semantics of Regular Expressions *} |
|
230 |
|
231 fun |
|
232 L :: "rexp \<Rightarrow> string set" |
|
233 where |
|
234 "L (ZERO) = {}" |
|
235 | "L (ONE) = {[]}" |
|
236 | "L (CHAR c) = {[c]}" |
|
237 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
|
238 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
|
239 | "L (STAR r) = (L r)\<star>" |
|
240 | "L (UPNTIMES r n) = (\<Union>i\<in> {..n} . (L r) \<up> i)" |
|
241 | "L (NTIMES r n) = (L r) \<up> n" |
|
242 | "L (FROMNTIMES r n) = (\<Union>i\<in> {n..} . (L r) \<up> i)" |
|
243 | "L (NMTIMES r n m) = (\<Union>i\<in>{n..m} . (L r) \<up> i)" |
|
244 |
|
245 section {* Nullable, Derivatives *} |
|
246 |
|
247 fun |
|
248 nullable :: "rexp \<Rightarrow> bool" |
|
249 where |
|
250 "nullable (ZERO) = False" |
|
251 | "nullable (ONE) = True" |
|
252 | "nullable (CHAR c) = False" |
|
253 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
|
254 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
|
255 | "nullable (STAR r) = True" |
|
256 | "nullable (UPNTIMES r n) = True" |
|
257 | "nullable (NTIMES r n) = (if n = 0 then True else nullable r)" |
|
258 | "nullable (FROMNTIMES r n) = (if n = 0 then True else nullable r)" |
|
259 | "nullable (NMTIMES r n m) = (if m < n then False else (if n = 0 then True else nullable r))" |
|
260 |
|
261 fun |
|
262 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
|
263 where |
|
264 "der c (ZERO) = ZERO" |
|
265 | "der c (ONE) = ZERO" |
|
266 | "der c (CHAR d) = (if c = d then ONE else ZERO)" |
|
267 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
|
268 | "der c (SEQ r1 r2) = |
|
269 (if nullable r1 |
|
270 then ALT (SEQ (der c r1) r2) (der c r2) |
|
271 else SEQ (der c r1) r2)" |
|
272 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
|
273 | "der c (UPNTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (UPNTIMES r (n - 1)))" |
|
274 | "der c (NTIMES r n) = (if n = 0 then ZERO else SEQ (der c r) (NTIMES r (n - 1)))" |
|
275 | "der c (FROMNTIMES r n) = SEQ (der c r) (FROMNTIMES r (n - 1))" |
|
276 | "der c (NMTIMES r n m) = |
|
277 (if m < n then ZERO |
|
278 else (if n = 0 then (if m = 0 then ZERO else |
|
279 SEQ (der c r) (UPNTIMES r (m - 1))) else |
|
280 SEQ (der c r) (NMTIMES r (n - 1) (m - 1))))" |
|
281 |
|
282 fun |
|
283 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
|
284 where |
|
285 "ders [] r = r" |
|
286 | "ders (c # s) r = ders s (der c r)" |
|
287 |
|
288 |
|
289 lemma nullable_correctness: |
|
290 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
|
291 by(induct r) (auto simp add: Sequ_def) |
|
292 |
|
293 |
|
294 lemma der_correctness: |
|
295 shows "L (der c r) = Der c (L r)" |
|
296 apply(induct r) |
|
297 apply(simp add: nullable_correctness del: Der_UNION) |
|
298 apply(simp add: nullable_correctness del: Der_UNION) |
|
299 apply(simp add: nullable_correctness del: Der_UNION) |
|
300 apply(simp add: nullable_correctness del: Der_UNION) |
|
301 apply(simp add: nullable_correctness del: Der_UNION) |
|
302 apply(simp add: nullable_correctness del: Der_UNION) |
|
303 prefer 2 |
|
304 apply(simp add: nullable_correctness del: Der_UNION) |
|
305 apply(simp add: nullable_correctness del: Der_UNION) |
|
306 apply(rule impI) |
|
307 apply(subst Sequ_Union_in) |
|
308 apply(subst Der_Pow_Sequ[symmetric]) |
|
309 apply(subst Pow.simps[symmetric]) |
|
310 apply(subst Der_UNION[symmetric]) |
|
311 apply(subst Pow_Sequ_Un) |
|
312 apply(simp) |
|
313 apply(simp only: Der_union Der_empty) |
|
314 apply(simp) |
|
315 apply(simp add: nullable_correctness del: Der_UNION) |
|
316 apply(subst Sequ_Union_in) |
|
317 apply(subst Der_Pow_Sequ[symmetric]) |
|
318 apply(subst Pow.simps[symmetric]) |
|
319 apply(case_tac x2) |
|
320 prefer 2 |
|
321 apply(subst Pow_Sequ_Un2) |
|
322 apply(simp) |
|
323 apply(simp) |
|
324 apply(auto simp add: Sequ_def Der_def)[1] |
|
325 apply(rule_tac x="Suc xa" in exI) |
|
326 apply(auto simp add: Sequ_def)[1] |
|
327 apply(drule Pow_decomp) |
|
328 apply(auto)[1] |
|
329 apply (metis append_Cons) |
|
330 apply(simp add: nullable_correctness del: Der_UNION) |
|
331 apply(rule impI) |
|
332 apply(rule conjI) |
|
333 apply(rule impI) |
|
334 apply(subst Sequ_Union_in) |
|
335 apply(subst Der_Pow_Sequ[symmetric]) |
|
336 apply(subst Pow.simps[symmetric]) |
|
337 apply(subst Der_UNION[symmetric]) |
|
338 apply(case_tac x3a) |
|
339 apply(simp) |
|
340 apply(clarify) |
|
341 apply(auto simp add: Sequ_def Der_def Cons_eq_append_conv)[1] |
|
342 apply(rule_tac x="Suc xa" in bexI) |
|
343 apply(auto simp add: Sequ_def)[2] |
|
344 apply (metis append_Cons) |
|
345 apply (metis (no_types, hide_lams) Pow_decomp atMost_iff diff_Suc_eq_diff_pred diff_is_0_eq) |
|
346 apply(rule impI)+ |
|
347 apply(subst Sequ_Union_in) |
|
348 apply(subst Der_Pow_Sequ[symmetric]) |
|
349 apply(subst Pow.simps[symmetric]) |
|
350 apply(subst Der_UNION[symmetric]) |
|
351 apply(case_tac x2) |
|
352 apply(simp) |
|
353 apply(simp del: Pow.simps) |
|
354 apply(auto simp add: Sequ_def Der_def) |
|
355 apply (metis One_nat_def Suc_le_D Suc_le_mono atLeastAtMost_iff diff_Suc_1 not_le) |
|
356 by fastforce |
|
357 |
|
358 |
|
359 |
|
360 lemma ders_correctness: |
|
361 shows "L (ders s r) = Ders s (L r)" |
|
362 by (induct s arbitrary: r) |
|
363 (simp_all add: Ders_def der_correctness Der_def) |
|
364 |
|
365 |
|
366 |
|
367 section {* Values *} |
|
368 |
|
369 datatype val = |
|
370 Void |
|
371 | Char char |
|
372 | Seq val val |
|
373 | Right val |
|
374 | Left val |
|
375 | Stars "val list" |
|
376 |
|
377 |
|
378 section {* The string behind a value *} |
|
379 |
|
380 fun |
|
381 flat :: "val \<Rightarrow> string" |
|
382 where |
|
383 "flat (Void) = []" |
|
384 | "flat (Char c) = [c]" |
|
385 | "flat (Left v) = flat v" |
|
386 | "flat (Right v) = flat v" |
|
387 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)" |
|
388 | "flat (Stars []) = []" |
|
389 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" |
|
390 |
|
391 abbreviation |
|
392 "flats vs \<equiv> concat (map flat vs)" |
|
393 |
|
394 lemma flat_Stars [simp]: |
|
395 "flat (Stars vs) = flats vs" |
|
396 by (induct vs) (auto) |
|
397 |
|
398 lemma Star_concat: |
|
399 assumes "\<forall>s \<in> set ss. s \<in> A" |
|
400 shows "concat ss \<in> A\<star>" |
|
401 using assms by (induct ss) (auto) |
|
402 |
|
403 lemma Star_cstring: |
|
404 assumes "s \<in> A\<star>" |
|
405 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])" |
|
406 using assms |
|
407 apply(induct rule: Star.induct) |
|
408 apply(auto)[1] |
|
409 apply(rule_tac x="[]" in exI) |
|
410 apply(simp) |
|
411 apply(erule exE) |
|
412 apply(clarify) |
|
413 apply(case_tac "s1 = []") |
|
414 apply(rule_tac x="ss" in exI) |
|
415 apply(simp) |
|
416 apply(rule_tac x="s1#ss" in exI) |
|
417 apply(simp) |
|
418 done |
|
419 |
|
420 lemma Aux: |
|
421 assumes "\<forall>s\<in>set ss. s = []" |
|
422 shows "concat ss = []" |
|
423 using assms |
|
424 by (induct ss) (auto) |
|
425 |
|
426 lemma Pow_cstring_nonempty: |
|
427 assumes "s \<in> A \<up> n" |
|
428 shows "\<exists>ss. concat ss = s \<and> length ss \<le> n \<and> (\<forall>s \<in> set ss. s \<in> A \<and> s \<noteq> [])" |
|
429 using assms |
|
430 apply(induct n arbitrary: s) |
|
431 apply(auto) |
|
432 apply(simp add: Sequ_def) |
|
433 apply(erule exE)+ |
|
434 apply(clarify) |
|
435 apply(drule_tac x="s2" in meta_spec) |
|
436 apply(simp) |
|
437 apply(clarify) |
|
438 apply(case_tac "s1 = []") |
|
439 apply(simp) |
|
440 apply(rule_tac x="ss" in exI) |
|
441 apply(simp) |
|
442 apply(rule_tac x="s1 # ss" in exI) |
|
443 apply(simp) |
|
444 done |
|
445 |
|
446 lemma Pow_cstring: |
|
447 assumes "s \<in> A \<up> n" |
|
448 shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and> |
|
449 (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])" |
|
450 using assms |
|
451 apply(induct n arbitrary: s) |
|
452 apply(auto)[1] |
|
453 apply(simp only: Pow_Suc_rev) |
|
454 apply(simp add: Sequ_def) |
|
455 apply(erule exE)+ |
|
456 apply(clarify) |
|
457 apply(drule_tac x="s1" in meta_spec) |
|
458 apply(simp) |
|
459 apply(erule exE)+ |
|
460 apply(clarify) |
|
461 apply(case_tac "s2 = []") |
|
462 apply(simp) |
|
463 apply(rule_tac x="ss1" in exI) |
|
464 apply(rule_tac x="s2#ss2" in exI) |
|
465 apply(simp) |
|
466 apply(rule_tac x="ss1 @ [s2]" in exI) |
|
467 apply(rule_tac x="ss2" in exI) |
|
468 apply(simp) |
|
469 apply(subst Aux) |
|
470 apply(auto)[1] |
|
471 apply(subst Aux) |
|
472 apply(auto)[1] |
|
473 apply(simp) |
|
474 done |
|
475 |
|
476 |
|
477 section {* Lexical Values *} |
|
478 |
|
479 |
|
480 |
|
481 inductive |
|
482 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100) |
|
483 where |
|
484 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" |
|
485 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
|
486 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
|
487 | "\<Turnstile> Void : ONE" |
|
488 | "\<Turnstile> Char c : CHAR c" |
|
489 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : STAR r" |
|
490 | "\<lbrakk>\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> []; length vs \<le> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars vs : UPNTIMES r n" |
|
491 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
|
492 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
|
493 length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n" |
|
494 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
|
495 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
|
496 length (vs1 @ vs2) \<ge> n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : FROMNTIMES r n" |
|
497 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
|
498 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
|
499 length (vs1 @ vs2) \<ge> n; length (vs1 @ vs2) \<le> m\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NMTIMES r n m" |
|
500 |
|
501 inductive_cases Prf_elims: |
|
502 "\<Turnstile> v : ZERO" |
|
503 "\<Turnstile> v : SEQ r1 r2" |
|
504 "\<Turnstile> v : ALT r1 r2" |
|
505 "\<Turnstile> v : ONE" |
|
506 "\<Turnstile> v : CHAR c" |
|
507 "\<Turnstile> vs : STAR r" |
|
508 "\<Turnstile> vs : UPNTIMES r n" |
|
509 "\<Turnstile> vs : NTIMES r n" |
|
510 "\<Turnstile> vs : FROMNTIMES r n" |
|
511 "\<Turnstile> vs : NMTIMES r n m" |
|
512 |
|
513 lemma Prf_Stars_appendE: |
|
514 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
515 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
516 using assms |
|
517 by (auto intro: Prf.intros elim!: Prf_elims) |
|
518 |
|
519 lemma flats_empty: |
|
520 assumes "(\<forall>v\<in>set vs. flat v = [])" |
|
521 shows "flats vs = []" |
|
522 using assms |
|
523 by(induct vs) (simp_all) |
|
524 |
|
525 lemma Star_cval: |
|
526 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
527 shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" |
|
528 using assms |
|
529 apply(induct ss) |
|
530 apply(auto) |
|
531 apply(rule_tac x="[]" in exI) |
|
532 apply(simp) |
|
533 apply(case_tac "flat v = []") |
|
534 apply(rule_tac x="vs" in exI) |
|
535 apply(simp) |
|
536 apply(rule_tac x="v#vs" in exI) |
|
537 apply(simp) |
|
538 done |
|
539 |
|
540 |
|
541 lemma flats_cval: |
|
542 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
543 shows "\<exists>vs1 vs2. flats (vs1 @ vs2) = concat ss \<and> length (vs1 @ vs2) = length ss \<and> |
|
544 (\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []) \<and> |
|
545 (\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = [])" |
|
546 using assms |
|
547 apply(induct ss rule: rev_induct) |
|
548 apply(rule_tac x="[]" in exI)+ |
|
549 apply(simp) |
|
550 apply(simp) |
|
551 apply(clarify) |
|
552 apply(case_tac "flat v = []") |
|
553 apply(rule_tac x="vs1" in exI) |
|
554 apply(rule_tac x="v#vs2" in exI) |
|
555 apply(simp) |
|
556 apply(rule_tac x="vs1 @ [v]" in exI) |
|
557 apply(rule_tac x="vs2" in exI) |
|
558 apply(simp) |
|
559 apply(subst (asm) (2) flats_empty) |
|
560 apply(simp) |
|
561 apply(simp) |
|
562 done |
|
563 |
|
564 lemma flats_cval_nonempty: |
|
565 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
566 shows "\<exists>vs. flats vs = concat ss \<and> length vs \<le> length ss \<and> |
|
567 (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" |
|
568 using assms |
|
569 apply(induct ss) |
|
570 apply(rule_tac x="[]" in exI) |
|
571 apply(simp) |
|
572 apply(simp) |
|
573 apply(clarify) |
|
574 apply(case_tac "flat v = []") |
|
575 apply(rule_tac x="vs" in exI) |
|
576 apply(simp) |
|
577 apply(rule_tac x="v # vs" in exI) |
|
578 apply(simp) |
|
579 done |
|
580 |
|
581 lemma Pow_flats: |
|
582 assumes "\<forall>v \<in> set vs. flat v \<in> A" |
|
583 shows "flats vs \<in> A \<up> length vs" |
|
584 using assms |
|
585 by(induct vs)(auto simp add: Sequ_def) |
|
586 |
|
587 lemma Pow_flats_appends: |
|
588 assumes "\<forall>v \<in> set vs1. flat v \<in> A" "\<forall>v \<in> set vs2. flat v \<in> A" |
|
589 shows "flats vs1 @ flats vs2 \<in> A \<up> (length vs1 + length vs2)" |
|
590 using assms |
|
591 apply(induct vs1) |
|
592 apply(auto simp add: Sequ_def Pow_flats) |
|
593 done |
|
594 |
|
595 lemma L_flat_Prf1: |
|
596 assumes "\<Turnstile> v : r" |
|
597 shows "flat v \<in> L r" |
|
598 using assms |
|
599 apply(induct) |
|
600 apply(auto simp add: Sequ_def Star_concat Pow_flats) |
|
601 apply(meson Pow_flats atMost_iff) |
|
602 using Pow_flats_appends apply blast |
|
603 apply(meson Pow_flats_appends atLeast_iff) |
|
604 apply(meson Pow_flats_appends atLeastAtMost_iff) |
|
605 done |
|
606 |
|
607 lemma L_flat_Prf2: |
|
608 assumes "s \<in> L r" |
|
609 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
|
610 using assms |
|
611 proof(induct r arbitrary: s) |
|
612 case (STAR r s) |
|
613 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
614 have "s \<in> L (STAR r)" by fact |
|
615 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" |
|
616 using Star_cstring by auto |
|
617 then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" |
|
618 using IH Star_cval by metis |
|
619 then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s" |
|
620 using Prf.intros(6) flat_Stars by blast |
|
621 next |
|
622 case (SEQ r1 r2 s) |
|
623 then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s" |
|
624 unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) |
|
625 next |
|
626 case (ALT r1 r2 s) |
|
627 then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s" |
|
628 unfolding L.simps by (fastforce intro: Prf.intros) |
|
629 next |
|
630 case (NTIMES r n) |
|
631 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
632 have "s \<in> L (NTIMES r n)" by fact |
|
633 then obtain ss1 ss2 where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = n" |
|
634 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
|
635 using Pow_cstring by force |
|
636 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = n" |
|
637 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
|
638 using IH flats_cval |
|
639 apply - |
|
640 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
|
641 apply(drule_tac x="r" in meta_spec) |
|
642 apply(drule meta_mp) |
|
643 apply(simp) |
|
644 apply (metis Un_iff) |
|
645 apply(clarify) |
|
646 apply(drule_tac x="vs1" in meta_spec) |
|
647 apply(drule_tac x="vs2" in meta_spec) |
|
648 apply(simp) |
|
649 done |
|
650 then show "\<exists>v. \<Turnstile> v : NTIMES r n \<and> flat v = s" |
|
651 using Prf.intros(8) flat_Stars by blast |
|
652 next |
|
653 case (FROMNTIMES r n) |
|
654 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
655 have "s \<in> L (FROMNTIMES r n)" by fact |
|
656 then obtain ss1 ss2 m where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = m" "n \<le> m" |
|
657 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
|
658 using Pow_cstring by auto blast |
|
659 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = m" "n \<le> m" |
|
660 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
|
661 using IH flats_cval |
|
662 apply - |
|
663 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
|
664 apply(drule_tac x="r" in meta_spec) |
|
665 apply(drule meta_mp) |
|
666 apply(simp) |
|
667 apply (metis Un_iff) |
|
668 apply(clarify) |
|
669 apply(drule_tac x="vs1" in meta_spec) |
|
670 apply(drule_tac x="vs2" in meta_spec) |
|
671 apply(simp) |
|
672 done |
|
673 then show "\<exists>v. \<Turnstile> v : FROMNTIMES r n \<and> flat v = s" |
|
674 using Prf.intros(9) flat_Stars by blast |
|
675 next |
|
676 case (NMTIMES r n m) |
|
677 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
678 have "s \<in> L (NMTIMES r n m)" by fact |
|
679 then obtain ss1 ss2 k where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = k" "n \<le> k" "k \<le> m" |
|
680 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
|
681 using Pow_cstring by (auto, blast) |
|
682 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = k" "n \<le> k" "k \<le> m" |
|
683 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
|
684 using IH flats_cval |
|
685 apply - |
|
686 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
|
687 apply(drule_tac x="r" in meta_spec) |
|
688 apply(drule meta_mp) |
|
689 apply(simp) |
|
690 apply (metis Un_iff) |
|
691 apply(clarify) |
|
692 apply(drule_tac x="vs1" in meta_spec) |
|
693 apply(drule_tac x="vs2" in meta_spec) |
|
694 apply(simp) |
|
695 done |
|
696 then show "\<exists>v. \<Turnstile> v : NMTIMES r n m \<and> flat v = s" |
|
697 apply(rule_tac x="Stars (vs1 @ vs2)" in exI) |
|
698 apply(simp) |
|
699 apply(rule Prf.intros) |
|
700 apply(auto) |
|
701 done |
|
702 next |
|
703 case (UPNTIMES r n s) |
|
704 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
705 have "s \<in> L (UPNTIMES r n)" by fact |
|
706 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" "length ss \<le> n" |
|
707 using Pow_cstring_nonempty by force |
|
708 then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" "length vs \<le> n" |
|
709 using IH flats_cval_nonempty by (smt order.trans) |
|
710 then show "\<exists>v. \<Turnstile> v : UPNTIMES r n \<and> flat v = s" |
|
711 using Prf.intros(7) flat_Stars by blast |
|
712 qed (auto intro: Prf.intros) |
|
713 |
|
714 |
|
715 lemma L_flat_Prf: |
|
716 shows "L(r) = {flat v | v. \<Turnstile> v : r}" |
|
717 using L_flat_Prf1 L_flat_Prf2 by blast |
|
718 |
|
719 |
|
720 |
|
721 section {* Sets of Lexical Values *} |
|
722 |
|
723 text {* |
|
724 Shows that lexical values are finite for a given regex and string. |
|
725 *} |
|
726 |
|
727 definition |
|
728 LV :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
729 where "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}" |
|
730 |
|
731 lemma LV_simps: |
|
732 shows "LV ZERO s = {}" |
|
733 and "LV ONE s = (if s = [] then {Void} else {})" |
|
734 and "LV (CHAR c) s = (if s = [c] then {Char c} else {})" |
|
735 and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s" |
|
736 unfolding LV_def |
|
737 by (auto intro: Prf.intros elim: Prf.cases) |
|
738 |
|
739 |
|
740 abbreviation |
|
741 "Prefixes s \<equiv> {s'. prefixeq s' s}" |
|
742 |
|
743 abbreviation |
|
744 "Suffixes s \<equiv> {s'. suffixeq s' s}" |
|
745 |
|
746 abbreviation |
|
747 "SSuffixes s \<equiv> {s'. suffix s' s}" |
|
748 |
|
749 lemma Suffixes_cons [simp]: |
|
750 shows "Suffixes (c # s) = Suffixes s \<union> {c # s}" |
|
751 by (auto simp add: suffixeq_def Cons_eq_append_conv) |
|
752 |
|
753 |
|
754 lemma finite_Suffixes: |
|
755 shows "finite (Suffixes s)" |
|
756 by (induct s) (simp_all) |
|
757 |
|
758 lemma finite_SSuffixes: |
|
759 shows "finite (SSuffixes s)" |
|
760 proof - |
|
761 have "SSuffixes s \<subseteq> Suffixes s" |
|
762 unfolding suffix_def suffixeq_def by auto |
|
763 then show "finite (SSuffixes s)" |
|
764 using finite_Suffixes finite_subset by blast |
|
765 qed |
|
766 |
|
767 lemma finite_Prefixes: |
|
768 shows "finite (Prefixes s)" |
|
769 proof - |
|
770 have "finite (Suffixes (rev s))" |
|
771 by (rule finite_Suffixes) |
|
772 then have "finite (rev ` Suffixes (rev s))" by simp |
|
773 moreover |
|
774 have "rev ` (Suffixes (rev s)) = Prefixes s" |
|
775 unfolding suffixeq_def prefixeq_def image_def |
|
776 by (auto)(metis rev_append rev_rev_ident)+ |
|
777 ultimately show "finite (Prefixes s)" by simp |
|
778 qed |
|
779 |
|
780 lemma LV_STAR_finite: |
|
781 assumes "\<forall>s. finite (LV r s)" |
|
782 shows "finite (LV (STAR r) s)" |
|
783 proof(induct s rule: length_induct) |
|
784 fix s::"char list" |
|
785 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
|
786 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
|
787 by (auto simp add: suffix_def) |
|
788 def f \<equiv> "\<lambda>(v, vs). Stars (v # vs)" |
|
789 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r s'" |
|
790 def S2 \<equiv> "\<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
|
791 have "finite S1" using assms |
|
792 unfolding S1_def by (simp_all add: finite_Prefixes) |
|
793 moreover |
|
794 with IH have "finite S2" unfolding S2_def |
|
795 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
|
796 ultimately |
|
797 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
|
798 moreover |
|
799 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
|
800 unfolding S1_def S2_def f_def |
|
801 unfolding LV_def image_def prefixeq_def suffix_def |
|
802 apply(auto elim: Prf_elims) |
|
803 apply(erule Prf_elims) |
|
804 apply(auto) |
|
805 apply(case_tac vs) |
|
806 apply(auto intro: Prf.intros) |
|
807 done |
|
808 ultimately |
|
809 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
|
810 qed |
|
811 |
|
812 lemma LV_UPNTIMES_STAR: |
|
813 "LV (UPNTIMES r n) s \<subseteq> LV (STAR r) s" |
|
814 by(auto simp add: LV_def intro: Prf.intros elim: Prf_elims) |
|
815 |
|
816 lemma LV_FROMNTIMES_STAR: |
|
817 "LV (FROMNTIMES r n) s \<subseteq> LV (STAR r) s" |
|
818 apply(auto simp add: LV_def intro: Prf.intros elim!: Prf_elims) |
|
819 oops |
|
820 |
|
821 lemma LV_finite: |
|
822 shows "finite (LV r s)" |
|
823 proof(induct r arbitrary: s) |
|
824 case (ZERO s) |
|
825 show "finite (LV ZERO s)" by (simp add: LV_simps) |
|
826 next |
|
827 case (ONE s) |
|
828 show "finite (LV ONE s)" by (simp add: LV_simps) |
|
829 next |
|
830 case (CHAR c s) |
|
831 show "finite (LV (CHAR c) s)" by (simp add: LV_simps) |
|
832 next |
|
833 case (ALT r1 r2 s) |
|
834 then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) |
|
835 next |
|
836 case (SEQ r1 r2 s) |
|
837 def f \<equiv> "\<lambda>(v1, v2). Seq v1 v2" |
|
838 def S1 \<equiv> "\<Union>s' \<in> Prefixes s. LV r1 s'" |
|
839 def S2 \<equiv> "\<Union>s' \<in> Suffixes s. LV r2 s'" |
|
840 have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ |
|
841 then have "finite S1" "finite S2" unfolding S1_def S2_def |
|
842 by (simp_all add: finite_Prefixes finite_Suffixes) |
|
843 moreover |
|
844 have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
|
845 unfolding f_def S1_def S2_def |
|
846 unfolding LV_def image_def prefixeq_def suffixeq_def |
|
847 by (auto elim: Prf.cases) |
|
848 ultimately |
|
849 show "finite (LV (SEQ r1 r2) s)" |
|
850 by (simp add: finite_subset) |
|
851 next |
|
852 case (STAR r s) |
|
853 then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) |
|
854 next |
|
855 case (NTIMES r n s) |
|
856 have "\<And>s. finite (LV r s)" by fact |
|
857 then show "finite (LV (NTIMES r n) s)" |
|
858 apply(simp add: LV_def) |
|
859 qed |
|
860 |
|
861 |
|
862 |
|
863 section {* Our POSIX Definition *} |
|
864 |
|
865 inductive |
|
866 Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
|
867 where |
|
868 Posix_ONE: "[] \<in> ONE \<rightarrow> Void" |
|
869 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)" |
|
870 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
|
871 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
|
872 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
|
873 \<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> |
|
874 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
|
875 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
876 \<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> |
|
877 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
|
878 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
|
879 |
|
880 inductive_cases Posix_elims: |
|
881 "s \<in> ZERO \<rightarrow> v" |
|
882 "s \<in> ONE \<rightarrow> v" |
|
883 "s \<in> CHAR c \<rightarrow> v" |
|
884 "s \<in> ALT r1 r2 \<rightarrow> v" |
|
885 "s \<in> SEQ r1 r2 \<rightarrow> v" |
|
886 "s \<in> STAR r \<rightarrow> v" |
|
887 |
|
888 lemma Posix1: |
|
889 assumes "s \<in> r \<rightarrow> v" |
|
890 shows "s \<in> L r" "flat v = s" |
|
891 using assms |
|
892 by (induct s r v rule: Posix.induct) |
|
893 (auto simp add: Sequ_def) |
|
894 |
|
895 text {* |
|
896 Our Posix definition determines a unique value. |
|
897 *} |
|
898 |
|
899 lemma Posix_determ: |
|
900 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
901 shows "v1 = v2" |
|
902 using assms |
|
903 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
904 case (Posix_ONE v2) |
|
905 have "[] \<in> ONE \<rightarrow> v2" by fact |
|
906 then show "Void = v2" by cases auto |
|
907 next |
|
908 case (Posix_CHAR c v2) |
|
909 have "[c] \<in> CHAR c \<rightarrow> v2" by fact |
|
910 then show "Char c = v2" by cases auto |
|
911 next |
|
912 case (Posix_ALT1 s r1 v r2 v2) |
|
913 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
914 moreover |
|
915 have "s \<in> r1 \<rightarrow> v" by fact |
|
916 then have "s \<in> L r1" by (simp add: Posix1) |
|
917 ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto |
|
918 moreover |
|
919 have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
920 ultimately have "v = v'" by simp |
|
921 then show "Left v = v2" using eq by simp |
|
922 next |
|
923 case (Posix_ALT2 s r2 v r1 v2) |
|
924 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
925 moreover |
|
926 have "s \<notin> L r1" by fact |
|
927 ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" |
|
928 by cases (auto simp add: Posix1) |
|
929 moreover |
|
930 have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
931 ultimately have "v = v'" by simp |
|
932 then show "Right v = v2" using eq by simp |
|
933 next |
|
934 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v') |
|
935 have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" |
|
936 "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" |
|
937 "\<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+ |
|
938 then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" |
|
939 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
940 using Posix1(1) by fastforce+ |
|
941 moreover |
|
942 have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" |
|
943 "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ |
|
944 ultimately show "Seq v1 v2 = v'" by simp |
|
945 next |
|
946 case (Posix_STAR1 s1 r v s2 vs v2) |
|
947 have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" |
|
948 "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
949 "\<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+ |
|
950 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
951 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
952 using Posix1(1) apply fastforce |
|
953 apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2) |
|
954 using Posix1(2) by blast |
|
955 moreover |
|
956 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
957 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
958 ultimately show "Stars (v # vs) = v2" by auto |
|
959 next |
|
960 case (Posix_STAR2 r v2) |
|
961 have "[] \<in> STAR r \<rightarrow> v2" by fact |
|
962 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
963 qed |
|
964 |
|
965 |
|
966 text {* |
|
967 Our POSIX value is a lexical value. |
|
968 *} |
|
969 |
|
970 lemma Posix_LV: |
|
971 assumes "s \<in> r \<rightarrow> v" |
|
972 shows "v \<in> LV r s" |
|
973 using assms unfolding LV_def |
|
974 apply(induct rule: Posix.induct) |
|
975 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) |
|
976 done |
|
977 |
|
978 end |