|
1 |
|
2 theory Spec |
|
3 imports Main |
|
4 begin |
|
5 |
|
6 |
|
7 section {* Sequential Composition of Languages *} |
|
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_string [simp]: |
|
17 shows "A ;; {[]} = A" |
|
18 and "{[]} ;; A = A" |
|
19 by (simp_all add: Sequ_def) |
|
20 |
|
21 lemma Sequ_empty [simp]: |
|
22 shows "A ;; {} = {}" |
|
23 and "{} ;; A = {}" |
|
24 by (simp_all add: Sequ_def) |
|
25 |
|
26 |
|
27 section {* Semantic Derivative (Left Quotient) of Languages *} |
|
28 |
|
29 definition |
|
30 Der :: "char \<Rightarrow> string set \<Rightarrow> string set" |
|
31 where |
|
32 "Der c A \<equiv> {s. c # s \<in> A}" |
|
33 |
|
34 definition |
|
35 Ders :: "string \<Rightarrow> string set \<Rightarrow> string set" |
|
36 where |
|
37 "Ders s A \<equiv> {s'. s @ s' \<in> A}" |
|
38 |
|
39 lemma Der_null [simp]: |
|
40 shows "Der c {} = {}" |
|
41 unfolding Der_def |
|
42 by auto |
|
43 |
|
44 lemma Der_empty [simp]: |
|
45 shows "Der c {[]} = {}" |
|
46 unfolding Der_def |
|
47 by auto |
|
48 |
|
49 lemma Der_char [simp]: |
|
50 shows "Der c {[d]} = (if c = d then {[]} else {})" |
|
51 unfolding Der_def |
|
52 by auto |
|
53 |
|
54 lemma Der_union [simp]: |
|
55 shows "Der c (A \<union> B) = Der c A \<union> Der c B" |
|
56 unfolding Der_def |
|
57 by auto |
|
58 |
|
59 lemma Der_Sequ [simp]: |
|
60 shows "Der c (A ;; B) = (Der c A) ;; B \<union> (if [] \<in> A then Der c B else {})" |
|
61 unfolding Der_def Sequ_def |
|
62 by (auto simp add: Cons_eq_append_conv) |
|
63 |
|
64 |
|
65 section {* Kleene Star for Languages *} |
|
66 |
|
67 inductive_set |
|
68 Star :: "string set \<Rightarrow> string set" ("_\<star>" [101] 102) |
|
69 for A :: "string set" |
|
70 where |
|
71 start[intro]: "[] \<in> A\<star>" |
|
72 | step[intro]: "\<lbrakk>s1 \<in> A; s2 \<in> A\<star>\<rbrakk> \<Longrightarrow> s1 @ s2 \<in> A\<star>" |
|
73 |
|
74 (* Arden's lemma *) |
|
75 |
|
76 lemma Star_cases: |
|
77 shows "A\<star> = {[]} \<union> A ;; A\<star>" |
|
78 unfolding Sequ_def |
|
79 by (auto) (metis Star.simps) |
|
80 |
|
81 lemma Star_decomp: |
|
82 assumes "c # x \<in> A\<star>" |
|
83 shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>" |
|
84 using assms |
|
85 by (induct x\<equiv>"c # x" rule: Star.induct) |
|
86 (auto simp add: append_eq_Cons_conv) |
|
87 |
|
88 lemma Star_Der_Sequ: |
|
89 shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>" |
|
90 unfolding Der_def Sequ_def |
|
91 by(auto simp add: Star_decomp) |
|
92 |
|
93 |
|
94 lemma Der_star [simp]: |
|
95 shows "Der c (A\<star>) = (Der c A) ;; A\<star>" |
|
96 proof - |
|
97 have "Der c (A\<star>) = Der c ({[]} \<union> A ;; A\<star>)" |
|
98 by (simp only: Star_cases[symmetric]) |
|
99 also have "... = Der c (A ;; A\<star>)" |
|
100 by (simp only: Der_union Der_empty) (simp) |
|
101 also have "... = (Der c A) ;; A\<star> \<union> (if [] \<in> A then Der c (A\<star>) else {})" |
|
102 by simp |
|
103 also have "... = (Der c A) ;; A\<star>" |
|
104 using Star_Der_Sequ by auto |
|
105 finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" . |
|
106 qed |
|
107 |
|
108 |
|
109 section {* Regular Expressions *} |
|
110 |
|
111 datatype rexp = |
|
112 ZERO |
|
113 | ONE |
|
114 | CHAR char |
|
115 | SEQ rexp rexp |
|
116 | ALT rexp rexp |
|
117 | STAR rexp |
|
118 |
|
119 section {* Semantics of Regular Expressions *} |
|
120 |
|
121 fun |
|
122 L :: "rexp \<Rightarrow> string set" |
|
123 where |
|
124 "L (ZERO) = {}" |
|
125 | "L (ONE) = {[]}" |
|
126 | "L (CHAR c) = {[c]}" |
|
127 | "L (SEQ r1 r2) = (L r1) ;; (L r2)" |
|
128 | "L (ALT r1 r2) = (L r1) \<union> (L r2)" |
|
129 | "L (STAR r) = (L r)\<star>" |
|
130 |
|
131 |
|
132 section {* Nullable, Derivatives *} |
|
133 |
|
134 fun |
|
135 nullable :: "rexp \<Rightarrow> bool" |
|
136 where |
|
137 "nullable (ZERO) = False" |
|
138 | "nullable (ONE) = True" |
|
139 | "nullable (CHAR c) = False" |
|
140 | "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)" |
|
141 | "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)" |
|
142 | "nullable (STAR r) = True" |
|
143 |
|
144 |
|
145 fun |
|
146 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
|
147 where |
|
148 "der c (ZERO) = ZERO" |
|
149 | "der c (ONE) = ZERO" |
|
150 | "der c (CHAR d) = (if c = d then ONE else ZERO)" |
|
151 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
|
152 | "der c (SEQ r1 r2) = |
|
153 (if nullable r1 |
|
154 then ALT (SEQ (der c r1) r2) (der c r2) |
|
155 else SEQ (der c r1) r2)" |
|
156 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
|
157 |
|
158 fun |
|
159 ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp" |
|
160 where |
|
161 "ders [] r = r" |
|
162 | "ders (c # s) r = ders s (der c r)" |
|
163 |
|
164 |
|
165 lemma nullable_correctness: |
|
166 shows "nullable r \<longleftrightarrow> [] \<in> (L r)" |
|
167 by (induct r) (auto simp add: Sequ_def) |
|
168 |
|
169 lemma der_correctness: |
|
170 shows "L (der c r) = Der c (L r)" |
|
171 by (induct r) (simp_all add: nullable_correctness) |
|
172 |
|
173 lemma ders_correctness: |
|
174 shows "L (ders s r) = Ders s (L r)" |
|
175 apply(induct s arbitrary: r) |
|
176 apply(simp_all add: Ders_def der_correctness Der_def) |
|
177 done |
|
178 |
|
179 |
|
180 section {* Lemmas about ders *} |
|
181 |
|
182 lemma ders_ZERO: |
|
183 shows "ders s (ZERO) = ZERO" |
|
184 apply(induct s) |
|
185 apply(simp_all) |
|
186 done |
|
187 |
|
188 lemma ders_ONE: |
|
189 shows "ders s (ONE) = (if s = [] then ONE else ZERO)" |
|
190 apply(induct s) |
|
191 apply(simp_all add: ders_ZERO) |
|
192 done |
|
193 |
|
194 lemma ders_CHAR: |
|
195 shows "ders s (CHAR c) = |
|
196 (if s = [c] then ONE else |
|
197 (if s = [] then (CHAR c) else ZERO))" |
|
198 apply(induct s) |
|
199 apply(simp_all add: ders_ZERO ders_ONE) |
|
200 done |
|
201 |
|
202 lemma ders_ALT: |
|
203 shows "ders s (ALT r1 r2) = ALT (ders s r1) (ders s r2)" |
|
204 apply(induct s arbitrary: r1 r2) |
|
205 apply(simp_all) |
|
206 done |
|
207 |
|
208 section {* Values *} |
|
209 |
|
210 datatype val = |
|
211 Void |
|
212 | Char char |
|
213 | Seq val val |
|
214 | Right val |
|
215 | Left val |
|
216 | Stars "val list" |
|
217 |
|
218 |
|
219 section {* The string behind a value *} |
|
220 |
|
221 fun |
|
222 flat :: "val \<Rightarrow> string" |
|
223 where |
|
224 "flat (Void) = []" |
|
225 | "flat (Char c) = [c]" |
|
226 | "flat (Left v) = flat v" |
|
227 | "flat (Right v) = flat v" |
|
228 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)" |
|
229 | "flat (Stars []) = []" |
|
230 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" |
|
231 |
|
232 lemma flat_Stars [simp]: |
|
233 "flat (Stars vs) = concat (map flat vs)" |
|
234 by (induct vs) (auto) |
|
235 |
|
236 |
|
237 section {* Relation between values and regular expressions *} |
|
238 |
|
239 inductive |
|
240 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<turnstile> _ : _" [100, 100] 100) |
|
241 where |
|
242 "\<lbrakk>\<turnstile> v1 : r1; \<turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<turnstile> Seq v1 v2 : SEQ r1 r2" |
|
243 | "\<turnstile> v1 : r1 \<Longrightarrow> \<turnstile> Left v1 : ALT r1 r2" |
|
244 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2" |
|
245 | "\<turnstile> Void : ONE" |
|
246 | "\<turnstile> Char c : CHAR c" |
|
247 | "\<forall>v \<in> set vs. \<turnstile> v : r \<Longrightarrow> \<turnstile> Stars vs : STAR r" |
|
248 |
|
249 inductive_cases Prf_elims: |
|
250 "\<turnstile> v : ZERO" |
|
251 "\<turnstile> v : SEQ r1 r2" |
|
252 "\<turnstile> v : ALT r1 r2" |
|
253 "\<turnstile> v : ONE" |
|
254 "\<turnstile> v : CHAR c" |
|
255 "\<turnstile> vs : STAR r" |
|
256 |
|
257 lemma Star_concat: |
|
258 assumes "\<forall>s \<in> set ss. s \<in> A" |
|
259 shows "concat ss \<in> A\<star>" |
|
260 using assms by (induct ss) (auto) |
|
261 |
|
262 lemma Star_string: |
|
263 assumes "s \<in> A\<star>" |
|
264 shows "\<exists>ss. concat ss = s \<and> (\<forall>s \<in> set ss. s \<in> A)" |
|
265 using assms |
|
266 apply(induct rule: Star.induct) |
|
267 apply(auto) |
|
268 apply(rule_tac x="[]" in exI) |
|
269 apply(simp) |
|
270 apply(rule_tac x="s1#ss" in exI) |
|
271 apply(simp) |
|
272 done |
|
273 |
|
274 lemma Star_val: |
|
275 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<turnstile> v : r" |
|
276 shows "\<exists>vs. concat (map flat vs) = concat ss \<and> (\<forall>v\<in>set vs. \<turnstile> v : r)" |
|
277 using assms |
|
278 apply(induct ss) |
|
279 apply(auto) |
|
280 apply(rule_tac x="[]" in exI) |
|
281 apply(simp) |
|
282 apply(rule_tac x="v#vs" in exI) |
|
283 apply(simp) |
|
284 done |
|
285 |
|
286 lemma Prf_Stars_append: |
|
287 assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r" |
|
288 shows "\<turnstile> Stars (vs1 @ vs2) : STAR r" |
|
289 using assms |
|
290 by (auto intro!: Prf.intros elim!: Prf_elims) |
|
291 |
|
292 lemma Prf_flat_L: |
|
293 assumes "\<turnstile> v : r" |
|
294 shows "flat v \<in> L r" |
|
295 using assms |
|
296 by (induct v r rule: Prf.induct) |
|
297 (auto simp add: Sequ_def Star_concat) |
|
298 |
|
299 |
|
300 lemma L_flat_Prf1: |
|
301 assumes "\<turnstile> v : r" |
|
302 shows "flat v \<in> L r" |
|
303 using assms |
|
304 by (induct) (auto simp add: Sequ_def Star_concat) |
|
305 |
|
306 lemma L_flat_Prf2: |
|
307 assumes "s \<in> L r" |
|
308 shows "\<exists>v. \<turnstile> v : r \<and> flat v = s" |
|
309 using assms |
|
310 proof(induct r arbitrary: s) |
|
311 case (STAR r s) |
|
312 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact |
|
313 have "s \<in> L (STAR r)" by fact |
|
314 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r" |
|
315 using Star_string by auto |
|
316 then obtain vs where "concat (map flat vs) = s" "\<forall>v\<in>set vs. \<turnstile> v : r" |
|
317 using IH Star_val by blast |
|
318 then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s" |
|
319 using Prf.intros(6) flat_Stars by blast |
|
320 next |
|
321 case (SEQ r1 r2 s) |
|
322 then show "\<exists>v. \<turnstile> v : SEQ r1 r2 \<and> flat v = s" |
|
323 unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) |
|
324 next |
|
325 case (ALT r1 r2 s) |
|
326 then show "\<exists>v. \<turnstile> v : ALT r1 r2 \<and> flat v = s" |
|
327 unfolding L.simps by (fastforce intro: Prf.intros) |
|
328 qed (auto intro: Prf.intros) |
|
329 |
|
330 lemma L_flat_Prf: |
|
331 shows "L(r) = {flat v | v. \<turnstile> v : r}" |
|
332 using L_flat_Prf1 L_flat_Prf2 by blast |
|
333 |
|
334 section {* CPT and CPTpre *} |
|
335 |
|
336 |
|
337 inductive |
|
338 CPrf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100) |
|
339 where |
|
340 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" |
|
341 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
|
342 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
|
343 | "\<Turnstile> Void : ONE" |
|
344 | "\<Turnstile> Char c : CHAR c" |
|
345 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r" |
|
346 |
|
347 lemma Prf_CPrf: |
|
348 assumes "\<Turnstile> v : r" |
|
349 shows "\<turnstile> v : r" |
|
350 using assms |
|
351 by (induct)(auto intro: Prf.intros) |
|
352 |
|
353 lemma CPrf_stars: |
|
354 assumes "\<Turnstile> Stars vs : STAR r" |
|
355 shows "\<forall>v \<in> set vs. flat v \<noteq> [] \<and> \<Turnstile> v : r" |
|
356 using assms |
|
357 apply(erule_tac CPrf.cases) |
|
358 apply(simp_all) |
|
359 done |
|
360 |
|
361 lemma CPrf_Stars_appendE: |
|
362 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
363 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
364 using assms |
|
365 apply(erule_tac CPrf.cases) |
|
366 apply(auto intro: CPrf.intros elim: Prf.cases) |
|
367 done |
|
368 |
|
369 definition PT :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
370 where "PT r s \<equiv> {v. flat v = s \<and> \<turnstile> v : r}" |
|
371 |
|
372 definition |
|
373 "CPT r s = {v. flat v = s \<and> \<Turnstile> v : r}" |
|
374 |
|
375 definition |
|
376 "CPTpre r s = {v. \<exists>s'. flat v @ s' = s \<and> \<Turnstile> v : r}" |
|
377 |
|
378 lemma CPT_CPTpre_subset: |
|
379 shows "CPT r s \<subseteq> CPTpre r s" |
|
380 by(auto simp add: CPT_def CPTpre_def) |
|
381 |
|
382 lemma CPT_simps: |
|
383 shows "CPT ZERO s = {}" |
|
384 and "CPT ONE s = (if s = [] then {Void} else {})" |
|
385 and "CPT (CHAR c) s = (if s = [c] then {Char c} else {})" |
|
386 and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s" |
|
387 and "CPT (SEQ r1 r2) s = |
|
388 {Seq v1 v2 | v1 v2. flat v1 @ flat v2 = s \<and> v1 \<in> CPT r1 (flat v1) \<and> v2 \<in> CPT r2 (flat v2)}" |
|
389 and "CPT (STAR r) s = |
|
390 Stars ` {vs. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. v \<in> CPT r (flat v) \<and> flat v \<noteq> [])}" |
|
391 apply - |
|
392 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
393 apply(erule CPrf.cases) |
|
394 apply(simp_all)[6] |
|
395 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
396 apply(erule CPrf.cases) |
|
397 apply(simp_all)[6] |
|
398 apply(erule CPrf.cases) |
|
399 apply(simp_all)[6] |
|
400 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
401 apply(erule CPrf.cases) |
|
402 apply(simp_all)[6] |
|
403 apply(erule CPrf.cases) |
|
404 apply(simp_all)[6] |
|
405 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
406 apply(erule CPrf.cases) |
|
407 apply(simp_all)[6] |
|
408 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
409 apply(erule CPrf.cases) |
|
410 apply(simp_all)[6] |
|
411 (* STAR case *) |
|
412 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
413 apply(erule CPrf.cases) |
|
414 apply(simp_all)[6] |
|
415 done |
|
416 |
|
417 |
|
418 |
|
419 section {* Our POSIX Definition *} |
|
420 |
|
421 inductive |
|
422 Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
|
423 where |
|
424 Posix_ONE: "[] \<in> ONE \<rightarrow> Void" |
|
425 | Posix_CHAR: "[c] \<in> (CHAR c) \<rightarrow> (Char c)" |
|
426 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
|
427 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
|
428 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
|
429 \<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> |
|
430 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
|
431 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
432 \<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> |
|
433 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
|
434 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
|
435 |
|
436 inductive_cases Posix_elims: |
|
437 "s \<in> ZERO \<rightarrow> v" |
|
438 "s \<in> ONE \<rightarrow> v" |
|
439 "s \<in> CHAR c \<rightarrow> v" |
|
440 "s \<in> ALT r1 r2 \<rightarrow> v" |
|
441 "s \<in> SEQ r1 r2 \<rightarrow> v" |
|
442 "s \<in> STAR r \<rightarrow> v" |
|
443 |
|
444 lemma Posix1: |
|
445 assumes "s \<in> r \<rightarrow> v" |
|
446 shows "s \<in> L r" "flat v = s" |
|
447 using assms |
|
448 by (induct s r v rule: Posix.induct) |
|
449 (auto simp add: Sequ_def) |
|
450 |
|
451 lemma Posix_Prf: |
|
452 assumes "s \<in> r \<rightarrow> v" |
|
453 shows "\<turnstile> v : r" |
|
454 using assms |
|
455 apply(induct s r v rule: Posix.induct) |
|
456 apply(auto intro!: Prf.intros elim!: Prf_elims) |
|
457 done |
|
458 |
|
459 text {* |
|
460 Our Posix definition determines a unique value. |
|
461 *} |
|
462 |
|
463 lemma Posix_determ: |
|
464 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
465 shows "v1 = v2" |
|
466 using assms |
|
467 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
468 case (Posix_ONE v2) |
|
469 have "[] \<in> ONE \<rightarrow> v2" by fact |
|
470 then show "Void = v2" by cases auto |
|
471 next |
|
472 case (Posix_CHAR c v2) |
|
473 have "[c] \<in> CHAR c \<rightarrow> v2" by fact |
|
474 then show "Char c = v2" by cases auto |
|
475 next |
|
476 case (Posix_ALT1 s r1 v r2 v2) |
|
477 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
478 moreover |
|
479 have "s \<in> r1 \<rightarrow> v" by fact |
|
480 then have "s \<in> L r1" by (simp add: Posix1) |
|
481 ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto |
|
482 moreover |
|
483 have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
484 ultimately have "v = v'" by simp |
|
485 then show "Left v = v2" using eq by simp |
|
486 next |
|
487 case (Posix_ALT2 s r2 v r1 v2) |
|
488 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
489 moreover |
|
490 have "s \<notin> L r1" by fact |
|
491 ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" |
|
492 by cases (auto simp add: Posix1) |
|
493 moreover |
|
494 have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
495 ultimately have "v = v'" by simp |
|
496 then show "Right v = v2" using eq by simp |
|
497 next |
|
498 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v') |
|
499 have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" |
|
500 "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" |
|
501 "\<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+ |
|
502 then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" |
|
503 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
504 using Posix1(1) by fastforce+ |
|
505 moreover |
|
506 have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" |
|
507 "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ |
|
508 ultimately show "Seq v1 v2 = v'" by simp |
|
509 next |
|
510 case (Posix_STAR1 s1 r v s2 vs v2) |
|
511 have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" |
|
512 "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
513 "\<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+ |
|
514 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
515 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
516 using Posix1(1) apply fastforce |
|
517 apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2) |
|
518 using Posix1(2) by blast |
|
519 moreover |
|
520 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
521 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
522 ultimately show "Stars (v # vs) = v2" by auto |
|
523 next |
|
524 case (Posix_STAR2 r v2) |
|
525 have "[] \<in> STAR r \<rightarrow> v2" by fact |
|
526 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
527 qed |
|
528 |
|
529 |
|
530 text {* |
|
531 Our POSIX value is a canonical value. |
|
532 *} |
|
533 |
|
534 lemma Posix_CPT: |
|
535 assumes "s \<in> r \<rightarrow> v" |
|
536 shows "v \<in> CPT r s" |
|
537 using assms |
|
538 apply(induct rule: Posix.induct) |
|
539 apply(auto simp add: CPT_def intro: CPrf.intros elim: CPrf.cases) |
|
540 apply(rotate_tac 5) |
|
541 apply(erule CPrf.cases) |
|
542 apply(simp_all) |
|
543 apply(rule CPrf.intros) |
|
544 apply(simp_all) |
|
545 done |
|
546 |
|
547 |
|
548 |
|
549 (* |
|
550 lemma CPTpre_STAR_finite: |
|
551 assumes "\<And>s. finite (CPT r s)" |
|
552 shows "finite (CPT (STAR r) s)" |
|
553 apply(induct s rule: length_induct) |
|
554 apply(case_tac xs) |
|
555 apply(simp) |
|
556 apply(simp add: CPT_simps) |
|
557 apply(auto) |
|
558 apply(rule finite_imageI) |
|
559 using assms |
|
560 thm finite_Un |
|
561 prefer 2 |
|
562 apply(simp add: CPT_simps) |
|
563 apply(rule finite_imageI) |
|
564 apply(rule finite_subset) |
|
565 apply(rule CPTpre_subsets) |
|
566 apply(simp) |
|
567 apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset) |
|
568 apply(auto)[1] |
|
569 apply(rule finite_imageI) |
|
570 apply(simp add: Collect_case_prod_Sigma) |
|
571 apply(rule finite_SigmaI) |
|
572 apply(rule assms) |
|
573 apply(case_tac "flat v = []") |
|
574 apply(simp) |
|
575 apply(drule_tac x="drop (length (flat v)) (a # list)" in spec) |
|
576 apply(simp) |
|
577 apply(auto)[1] |
|
578 apply(rule test) |
|
579 apply(simp) |
|
580 done |
|
581 |
|
582 lemma CPTpre_subsets: |
|
583 "CPTpre ZERO s = {}" |
|
584 "CPTpre ONE s \<subseteq> {Void}" |
|
585 "CPTpre (CHAR c) s \<subseteq> {Char c}" |
|
586 "CPTpre (ALT r1 r2) s \<subseteq> Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s" |
|
587 "CPTpre (SEQ r1 r2) s \<subseteq> {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" |
|
588 "CPTpre (STAR r) s \<subseteq> {Stars []} \<union> |
|
589 {Stars (v#vs) | v vs. v \<in> CPTpre r s \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) s)}" |
|
590 "CPTpre (STAR r) [] = {Stars []}" |
|
591 apply(auto simp add: CPTpre_def) |
|
592 apply(erule CPrf.cases) |
|
593 apply(simp_all) |
|
594 apply(erule CPrf.cases) |
|
595 apply(simp_all) |
|
596 apply(erule CPrf.cases) |
|
597 apply(simp_all) |
|
598 apply(erule CPrf.cases) |
|
599 apply(simp_all) |
|
600 apply(erule CPrf.cases) |
|
601 apply(simp_all) |
|
602 |
|
603 apply(erule CPrf.cases) |
|
604 apply(simp_all) |
|
605 apply(erule CPrf.cases) |
|
606 apply(simp_all) |
|
607 apply(rule CPrf.intros) |
|
608 done |
|
609 |
|
610 |
|
611 lemma CPTpre_simps: |
|
612 shows "CPTpre ONE s = {Void}" |
|
613 and "CPTpre (CHAR c) (d#s) = (if c = d then {Char c} else {})" |
|
614 and "CPTpre (ALT r1 r2) s = Left ` CPTpre r1 s \<union> Right ` CPTpre r2 s" |
|
615 and "CPTpre (SEQ r1 r2) s = |
|
616 {Seq v1 v2 | v1 v2. v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" |
|
617 apply - |
|
618 apply(rule subset_antisym) |
|
619 apply(rule CPTpre_subsets) |
|
620 apply(auto simp add: CPTpre_def intro: "CPrf.intros")[1] |
|
621 apply(case_tac "c = d") |
|
622 apply(simp) |
|
623 apply(rule subset_antisym) |
|
624 apply(rule CPTpre_subsets) |
|
625 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
626 apply(simp) |
|
627 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
628 apply(erule CPrf.cases) |
|
629 apply(simp_all) |
|
630 apply(rule subset_antisym) |
|
631 apply(rule CPTpre_subsets) |
|
632 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
633 apply(rule subset_antisym) |
|
634 apply(rule CPTpre_subsets) |
|
635 apply(auto simp add: CPTpre_def intro: CPrf.intros)[1] |
|
636 done |
|
637 |
|
638 lemma CPT_simps: |
|
639 shows "CPT ONE s = (if s = [] then {Void} else {})" |
|
640 and "CPT (CHAR c) [d] = (if c = d then {Char c} else {})" |
|
641 and "CPT (ALT r1 r2) s = Left ` CPT r1 s \<union> Right ` CPT r2 s" |
|
642 and "CPT (SEQ r1 r2) s = |
|
643 {Seq v1 v2 | v1 v2 s1 s2. s1 @ s2 = s \<and> v1 \<in> CPT r1 s1 \<and> v2 \<in> CPT r2 s2}" |
|
644 apply - |
|
645 apply(rule subset_antisym) |
|
646 apply(auto simp add: CPT_def)[1] |
|
647 apply(erule CPrf.cases) |
|
648 apply(simp_all)[7] |
|
649 apply(erule CPrf.cases) |
|
650 apply(simp_all)[7] |
|
651 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
652 apply(auto simp add: CPT_def intro: CPrf.intros)[1] |
|
653 apply(erule CPrf.cases) |
|
654 apply(simp_all)[7] |
|
655 apply(erule CPrf.cases) |
|
656 apply(simp_all)[7] |
|
657 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] |
|
658 apply(erule CPrf.cases) |
|
659 apply(simp_all)[7] |
|
660 apply(clarify) |
|
661 apply blast |
|
662 apply(auto simp add: CPT_def image_def intro: CPrf.intros)[1] |
|
663 apply(erule CPrf.cases) |
|
664 apply(simp_all)[7] |
|
665 done |
|
666 |
|
667 lemma test: |
|
668 assumes "finite A" |
|
669 shows "finite {vs. Stars vs \<in> A}" |
|
670 using assms |
|
671 apply(induct A) |
|
672 apply(simp) |
|
673 apply(auto) |
|
674 apply(case_tac x) |
|
675 apply(simp_all) |
|
676 done |
|
677 |
|
678 lemma CPTpre_STAR_finite: |
|
679 assumes "\<And>s. finite (CPTpre r s)" |
|
680 shows "finite (CPTpre (STAR r) s)" |
|
681 apply(induct s rule: length_induct) |
|
682 apply(case_tac xs) |
|
683 apply(simp) |
|
684 apply(simp add: CPTpre_subsets) |
|
685 apply(rule finite_subset) |
|
686 apply(rule CPTpre_subsets) |
|
687 apply(simp) |
|
688 apply(rule_tac B="(\<lambda>(v, vs). Stars (v#vs)) ` {(v, vs). v \<in> CPTpre r (a#list) \<and> flat v \<noteq> [] \<and> Stars vs \<in> CPTpre (STAR r) (drop (length (flat v)) (a#list))}" in finite_subset) |
|
689 apply(auto)[1] |
|
690 apply(rule finite_imageI) |
|
691 apply(simp add: Collect_case_prod_Sigma) |
|
692 apply(rule finite_SigmaI) |
|
693 apply(rule assms) |
|
694 apply(case_tac "flat v = []") |
|
695 apply(simp) |
|
696 apply(drule_tac x="drop (length (flat v)) (a # list)" in spec) |
|
697 apply(simp) |
|
698 apply(auto)[1] |
|
699 apply(rule test) |
|
700 apply(simp) |
|
701 done |
|
702 |
|
703 lemma CPTpre_finite: |
|
704 shows "finite (CPTpre r s)" |
|
705 apply(induct r arbitrary: s) |
|
706 apply(simp add: CPTpre_subsets) |
|
707 apply(rule finite_subset) |
|
708 apply(rule CPTpre_subsets) |
|
709 apply(simp) |
|
710 apply(rule finite_subset) |
|
711 apply(rule CPTpre_subsets) |
|
712 apply(simp) |
|
713 apply(rule finite_subset) |
|
714 apply(rule CPTpre_subsets) |
|
715 apply(rule_tac B="(\<lambda>(v1, v2). Seq v1 v2) ` {(v1, v2). v1 \<in> CPTpre r1 s \<and> v2 \<in> CPTpre r2 (drop (length (flat v1)) s)}" in finite_subset) |
|
716 apply(auto)[1] |
|
717 apply(rule finite_imageI) |
|
718 apply(simp add: Collect_case_prod_Sigma) |
|
719 apply(rule finite_subset) |
|
720 apply(rule CPTpre_subsets) |
|
721 apply(simp) |
|
722 by (simp add: CPTpre_STAR_finite) |
|
723 |
|
724 |
|
725 lemma CPT_finite: |
|
726 shows "finite (CPT r s)" |
|
727 apply(rule finite_subset) |
|
728 apply(rule CPT_CPTpre_subset) |
|
729 apply(rule CPTpre_finite) |
|
730 done |
|
731 *) |
|
732 |
|
733 lemma test2: |
|
734 assumes "\<forall>v \<in> set vs. flat v \<in> r \<rightarrow> v \<and> flat v \<noteq> []" |
|
735 shows "(Stars vs) \<in> CPT (STAR r) (flat (Stars vs))" |
|
736 using assms |
|
737 apply(induct vs) |
|
738 apply(auto simp add: CPT_def) |
|
739 apply(rule CPrf.intros) |
|
740 apply(simp) |
|
741 apply(rule CPrf.intros) |
|
742 apply(simp_all) |
|
743 by (metis (no_types, lifting) CPT_def Posix_CPT mem_Collect_eq) |
|
744 |
|
745 |
|
746 end |