|
1 |
|
2 theory PosixSpec |
|
3 imports RegLangs |
|
4 begin |
|
5 |
|
6 section \<open>"Plain" Values\<close> |
|
7 |
|
8 datatype val = |
|
9 Void |
|
10 | Char char |
|
11 | Seq val val |
|
12 | Right val |
|
13 | Left val |
|
14 | Stars "val list" |
|
15 |
|
16 |
|
17 section \<open>The string behind a value\<close> |
|
18 |
|
19 fun |
|
20 flat :: "val \<Rightarrow> string" |
|
21 where |
|
22 "flat (Void) = []" |
|
23 | "flat (Char c) = [c]" |
|
24 | "flat (Left v) = flat v" |
|
25 | "flat (Right v) = flat v" |
|
26 | "flat (Seq v1 v2) = (flat v1) @ (flat v2)" |
|
27 | "flat (Stars []) = []" |
|
28 | "flat (Stars (v#vs)) = (flat v) @ (flat (Stars vs))" |
|
29 |
|
30 abbreviation |
|
31 "flats vs \<equiv> concat (map flat vs)" |
|
32 |
|
33 lemma flat_Stars [simp]: |
|
34 "flat (Stars vs) = flats vs" |
|
35 by (induct vs) (auto) |
|
36 |
|
37 |
|
38 section \<open>Lexical Values\<close> |
|
39 |
|
40 inductive |
|
41 Prf :: "val \<Rightarrow> rexp \<Rightarrow> bool" ("\<Turnstile> _ : _" [100, 100] 100) |
|
42 where |
|
43 "\<lbrakk>\<Turnstile> v1 : r1; \<Turnstile> v2 : r2\<rbrakk> \<Longrightarrow> \<Turnstile> Seq v1 v2 : SEQ r1 r2" |
|
44 | "\<Turnstile> v1 : r1 \<Longrightarrow> \<Turnstile> Left v1 : ALT r1 r2" |
|
45 | "\<Turnstile> v2 : r2 \<Longrightarrow> \<Turnstile> Right v2 : ALT r1 r2" |
|
46 | "\<Turnstile> Void : ONE" |
|
47 | "\<Turnstile> Char c : CH c" |
|
48 | "\<forall>v \<in> set vs. \<Turnstile> v : r \<and> flat v \<noteq> [] \<Longrightarrow> \<Turnstile> Stars vs : STAR r" |
|
49 | "\<lbrakk>\<forall>v \<in> set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []; |
|
50 \<forall>v \<in> set vs2. \<Turnstile> v : r \<and> flat v = []; |
|
51 length (vs1 @ vs2) = n\<rbrakk> \<Longrightarrow> \<Turnstile> Stars (vs1 @ vs2) : NTIMES r n" |
|
52 |
|
53 inductive_cases Prf_elims: |
|
54 "\<Turnstile> v : ZERO" |
|
55 "\<Turnstile> v : SEQ r1 r2" |
|
56 "\<Turnstile> v : ALT r1 r2" |
|
57 "\<Turnstile> v : ONE" |
|
58 "\<Turnstile> v : CH c" |
|
59 "\<Turnstile> vs : STAR r" |
|
60 "\<Turnstile> vs : NTIMES r n" |
|
61 |
|
62 lemma Prf_Stars_appendE: |
|
63 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
64 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
65 using assms |
|
66 by (auto intro: Prf.intros elim!: Prf_elims) |
|
67 |
|
68 lemma Pow_cstring: |
|
69 fixes A::"string set" |
|
70 assumes "s \<in> A ^^ n" |
|
71 shows "\<exists>ss1 ss2. concat (ss1 @ ss2) = s \<and> length (ss1 @ ss2) = n \<and> |
|
72 (\<forall>s \<in> set ss1. s \<in> A \<and> s \<noteq> []) \<and> (\<forall>s \<in> set ss2. s \<in> A \<and> s = [])" |
|
73 using assms |
|
74 apply(induct n arbitrary: s) |
|
75 apply(auto)[1] |
|
76 apply(auto simp add: Sequ_def) |
|
77 apply(drule_tac x="s2" in meta_spec) |
|
78 apply(simp) |
|
79 apply(erule exE)+ |
|
80 apply(clarify) |
|
81 apply(case_tac "s1 = []") |
|
82 apply(simp) |
|
83 apply(rule_tac x="ss1" in exI) |
|
84 apply(rule_tac x="s1 # ss2" in exI) |
|
85 apply(simp) |
|
86 apply(rule_tac x="s1 # ss1" in exI) |
|
87 apply(rule_tac x="ss2" in exI) |
|
88 apply(simp) |
|
89 done |
|
90 |
|
91 lemma flats_Prf_value: |
|
92 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
93 shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" |
|
94 using assms |
|
95 apply(induct ss) |
|
96 apply(auto) |
|
97 apply(rule_tac x="[]" in exI) |
|
98 apply(simp) |
|
99 apply(case_tac "flat v = []") |
|
100 apply(rule_tac x="vs" in exI) |
|
101 apply(simp) |
|
102 apply(rule_tac x="v#vs" in exI) |
|
103 apply(simp) |
|
104 done |
|
105 |
|
106 lemma Aux: |
|
107 assumes "\<forall>s\<in>set ss. s = []" |
|
108 shows "concat ss = []" |
|
109 using assms |
|
110 by (induct ss) (auto) |
|
111 |
|
112 lemma flats_cval: |
|
113 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
114 shows "\<exists>vs1 vs2. flats (vs1 @ vs2) = concat ss \<and> length (vs1 @ vs2) = length ss \<and> |
|
115 (\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []) \<and> |
|
116 (\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = [])" |
|
117 using assms |
|
118 apply(induct ss rule: rev_induct) |
|
119 apply(rule_tac x="[]" in exI)+ |
|
120 apply(simp) |
|
121 apply(simp) |
|
122 apply(clarify) |
|
123 apply(case_tac "flat v = []") |
|
124 apply(rule_tac x="vs1" in exI) |
|
125 apply(rule_tac x="v#vs2" in exI) |
|
126 apply(simp) |
|
127 apply(rule_tac x="vs1 @ [v]" in exI) |
|
128 apply(rule_tac x="vs2" in exI) |
|
129 apply(simp) |
|
130 by (simp add: Aux) |
|
131 |
|
132 lemma pow_Prf: |
|
133 assumes "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<in> A" |
|
134 shows "flats vs \<in> A ^^ (length vs)" |
|
135 using assms |
|
136 by (induct vs) (auto) |
|
137 |
|
138 lemma L_flat_Prf1: |
|
139 assumes "\<Turnstile> v : r" |
|
140 shows "flat v \<in> L r" |
|
141 using assms |
|
142 apply (induct v r rule: Prf.induct) |
|
143 apply(auto simp add: Sequ_def Star_concat lang_pow_add) |
|
144 by (metis pow_Prf) |
|
145 |
|
146 lemma L_flat_Prf2: |
|
147 assumes "s \<in> L r" |
|
148 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
|
149 using assms |
|
150 proof(induct r arbitrary: s) |
|
151 case (STAR r s) |
|
152 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
153 have "s \<in> L (STAR r)" by fact |
|
154 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" |
|
155 using Star_split by auto |
|
156 then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" |
|
157 using IH flats_Prf_value by metis |
|
158 then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s" |
|
159 using Prf.intros(6) flat_Stars by blast |
|
160 next |
|
161 case (SEQ r1 r2 s) |
|
162 then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s" |
|
163 unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) |
|
164 next |
|
165 case (ALT r1 r2 s) |
|
166 then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s" |
|
167 unfolding L.simps by (fastforce intro: Prf.intros) |
|
168 next |
|
169 case (NTIMES r n) |
|
170 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
171 have "s \<in> L (NTIMES r n)" by fact |
|
172 then obtain ss1 ss2 where "concat (ss1 @ ss2) = s" "length (ss1 @ ss2) = n" |
|
173 "\<forall>s \<in> set ss1. s \<in> L r \<and> s \<noteq> []" "\<forall>s \<in> set ss2. s \<in> L r \<and> s = []" |
|
174 using Pow_cstring by force |
|
175 then obtain vs1 vs2 where "flats (vs1 @ vs2) = s" "length (vs1 @ vs2) = n" |
|
176 "\<forall>v\<in>set vs1. \<Turnstile> v : r \<and> flat v \<noteq> []" "\<forall>v\<in>set vs2. \<Turnstile> v : r \<and> flat v = []" |
|
177 using IH flats_cval |
|
178 apply - |
|
179 apply(drule_tac x="ss1 @ ss2" in meta_spec) |
|
180 apply(drule_tac x="r" in meta_spec) |
|
181 apply(drule meta_mp) |
|
182 apply(simp) |
|
183 apply (metis Un_iff) |
|
184 apply(clarify) |
|
185 apply(drule_tac x="vs1" in meta_spec) |
|
186 apply(drule_tac x="vs2" in meta_spec) |
|
187 apply(simp) |
|
188 done |
|
189 then show "\<exists>v. \<Turnstile> v : NTIMES r n \<and> flat v = s" |
|
190 using Prf.intros(7) flat_Stars by blast |
|
191 qed (auto intro: Prf.intros) |
|
192 |
|
193 |
|
194 lemma L_flat_Prf: |
|
195 shows "L(r) = {flat v | v. \<Turnstile> v : r}" |
|
196 using L_flat_Prf1 L_flat_Prf2 by blast |
|
197 |
|
198 |
|
199 |
|
200 section \<open>Sets of Lexical Values\<close> |
|
201 |
|
202 text \<open> |
|
203 Shows that lexical values are finite for a given regex and string. |
|
204 \<close> |
|
205 |
|
206 definition |
|
207 LV :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
208 where "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}" |
|
209 |
|
210 lemma LV_simps: |
|
211 shows "LV ZERO s = {}" |
|
212 and "LV ONE s = (if s = [] then {Void} else {})" |
|
213 and "LV (CH c) s = (if s = [c] then {Char c} else {})" |
|
214 and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s" |
|
215 and "LV (NTIMES r 0) s = (if s = [] then {Stars []} else {})" |
|
216 unfolding LV_def |
|
217 apply (auto intro: Prf.intros elim: Prf.cases) |
|
218 by (metis Prf.intros(7) append.right_neutral empty_iff list.set(1) list.size(3)) |
|
219 |
|
220 |
|
221 abbreviation |
|
222 "Prefixes s \<equiv> {s'. prefix s' s}" |
|
223 |
|
224 abbreviation |
|
225 "Suffixes s \<equiv> {s'. suffix s' s}" |
|
226 |
|
227 abbreviation |
|
228 "SSuffixes s \<equiv> {s'. strict_suffix s' s}" |
|
229 |
|
230 lemma Suffixes_cons [simp]: |
|
231 shows "Suffixes (c # s) = Suffixes s \<union> {c # s}" |
|
232 by (auto simp add: suffix_def Cons_eq_append_conv) |
|
233 |
|
234 |
|
235 lemma finite_Suffixes: |
|
236 shows "finite (Suffixes s)" |
|
237 by (induct s) (simp_all) |
|
238 |
|
239 lemma finite_SSuffixes: |
|
240 shows "finite (SSuffixes s)" |
|
241 proof - |
|
242 have "SSuffixes s \<subseteq> Suffixes s" |
|
243 unfolding strict_suffix_def suffix_def by auto |
|
244 then show "finite (SSuffixes s)" |
|
245 using finite_Suffixes finite_subset by blast |
|
246 qed |
|
247 |
|
248 lemma finite_Prefixes: |
|
249 shows "finite (Prefixes s)" |
|
250 proof - |
|
251 have "finite (Suffixes (rev s))" |
|
252 by (rule finite_Suffixes) |
|
253 then have "finite (rev ` Suffixes (rev s))" by simp |
|
254 moreover |
|
255 have "rev ` (Suffixes (rev s)) = Prefixes s" |
|
256 unfolding suffix_def prefix_def image_def |
|
257 by (auto)(metis rev_append rev_rev_ident)+ |
|
258 ultimately show "finite (Prefixes s)" by simp |
|
259 qed |
|
260 |
|
261 definition |
|
262 "Stars_Append Vs1 Vs2 \<equiv> {Stars (vs1 @ vs2) | vs1 vs2. Stars vs1 \<in> Vs1 \<and> Stars vs2 \<in> Vs2}" |
|
263 |
|
264 lemma finite_Stars_Append: |
|
265 assumes "finite Vs1" "finite Vs2" |
|
266 shows "finite (Stars_Append Vs1 Vs2)" |
|
267 using assms |
|
268 proof - |
|
269 define UVs1 where "UVs1 \<equiv> Stars -` Vs1" |
|
270 define UVs2 where "UVs2 \<equiv> Stars -` Vs2" |
|
271 from assms have "finite UVs1" "finite UVs2" |
|
272 unfolding UVs1_def UVs2_def |
|
273 by(simp_all add: finite_vimageI inj_on_def) |
|
274 then have "finite ((\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2))" |
|
275 by simp |
|
276 moreover |
|
277 have "Stars_Append Vs1 Vs2 = (\<lambda>(vs1, vs2). Stars (vs1 @ vs2)) ` (UVs1 \<times> UVs2)" |
|
278 unfolding Stars_Append_def UVs1_def UVs2_def by auto |
|
279 ultimately show "finite (Stars_Append Vs1 Vs2)" |
|
280 by simp |
|
281 qed |
|
282 |
|
283 lemma LV_NTIMES_subset: |
|
284 "LV (NTIMES r n) s \<subseteq> Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) [])" |
|
285 apply(auto simp add: LV_def) |
|
286 apply(auto elim!: Prf_elims) |
|
287 apply(auto simp add: Stars_Append_def) |
|
288 apply(rule_tac x="vs1" in exI) |
|
289 apply(rule_tac x="vs2" in exI) |
|
290 apply(auto) |
|
291 using Prf.intros(6) apply(auto) |
|
292 apply(rule_tac x="length vs2" in bexI) |
|
293 thm Prf.intros |
|
294 apply(subst append.simps(1)[symmetric]) |
|
295 apply(rule Prf.intros) |
|
296 apply(auto)[1] |
|
297 apply(auto)[1] |
|
298 apply(simp) |
|
299 apply(simp) |
|
300 done |
|
301 |
|
302 lemma LV_NTIMES_Suc_empty: |
|
303 shows "LV (NTIMES r (Suc n)) [] = |
|
304 (\<lambda>(v, vs). Stars (v#vs)) ` (LV r [] \<times> (Stars -` (LV (NTIMES r n) [])))" |
|
305 unfolding LV_def |
|
306 apply(auto elim!: Prf_elims simp add: image_def) |
|
307 apply(case_tac vs1) |
|
308 apply(auto) |
|
309 apply(case_tac vs2) |
|
310 apply(auto) |
|
311 apply(subst append.simps(1)[symmetric]) |
|
312 apply(rule Prf.intros) |
|
313 apply(auto) |
|
314 apply(subst append.simps(1)[symmetric]) |
|
315 apply(rule Prf.intros) |
|
316 apply(auto) |
|
317 done |
|
318 |
|
319 lemma LV_STAR_finite: |
|
320 assumes "\<forall>s. finite (LV r s)" |
|
321 shows "finite (LV (STAR r) s)" |
|
322 proof(induct s rule: length_induct) |
|
323 fix s::"char list" |
|
324 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
|
325 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
|
326 by (force simp add: strict_suffix_def suffix_def) |
|
327 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
|
328 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'" |
|
329 define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
|
330 have "finite S1" using assms |
|
331 unfolding S1_def by (simp_all add: finite_Prefixes) |
|
332 moreover |
|
333 with IH have "finite S2" unfolding S2_def |
|
334 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
|
335 ultimately |
|
336 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
|
337 moreover |
|
338 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
|
339 unfolding S1_def S2_def f_def |
|
340 unfolding LV_def image_def prefix_def strict_suffix_def |
|
341 apply(auto) |
|
342 apply(case_tac x) |
|
343 apply(auto elim: Prf_elims) |
|
344 apply(erule Prf_elims) |
|
345 apply(auto) |
|
346 apply(case_tac vs) |
|
347 apply(auto intro: Prf.intros) |
|
348 apply(rule exI) |
|
349 apply(rule conjI) |
|
350 apply(rule_tac x="flat a" in exI) |
|
351 apply(rule conjI) |
|
352 apply(rule_tac x="flats list" in exI) |
|
353 apply(simp) |
|
354 apply(blast) |
|
355 apply(simp add: suffix_def) |
|
356 using Prf.intros(6) by blast |
|
357 ultimately |
|
358 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
|
359 qed |
|
360 |
|
361 lemma finite_NTimes_empty: |
|
362 assumes "\<And>s. finite (LV r s)" |
|
363 shows "finite (LV (NTIMES r n) [])" |
|
364 using assms |
|
365 apply(induct n) |
|
366 apply(auto simp add: LV_simps) |
|
367 apply(subst LV_NTIMES_Suc_empty) |
|
368 apply(rule finite_imageI) |
|
369 apply(rule finite_cartesian_product) |
|
370 using assms apply simp |
|
371 apply(rule finite_vimageI) |
|
372 apply(simp) |
|
373 apply(simp add: inj_on_def) |
|
374 done |
|
375 |
|
376 |
|
377 lemma LV_finite: |
|
378 shows "finite (LV r s)" |
|
379 proof(induct r arbitrary: s) |
|
380 case (ZERO s) |
|
381 show "finite (LV ZERO s)" by (simp add: LV_simps) |
|
382 next |
|
383 case (ONE s) |
|
384 show "finite (LV ONE s)" by (simp add: LV_simps) |
|
385 next |
|
386 case (CH c s) |
|
387 show "finite (LV (CH c) s)" by (simp add: LV_simps) |
|
388 next |
|
389 case (ALT r1 r2 s) |
|
390 then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) |
|
391 next |
|
392 case (SEQ r1 r2 s) |
|
393 define f where "f \<equiv> \<lambda>(v1, v2). Seq v1 v2" |
|
394 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'" |
|
395 define S2 where "S2 \<equiv> \<Union>s' \<in> Suffixes s. LV r2 s'" |
|
396 have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ |
|
397 then have "finite S1" "finite S2" unfolding S1_def S2_def |
|
398 by (simp_all add: finite_Prefixes finite_Suffixes) |
|
399 moreover |
|
400 have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
|
401 unfolding f_def S1_def S2_def |
|
402 unfolding LV_def image_def prefix_def suffix_def |
|
403 apply (auto elim!: Prf_elims) |
|
404 by (metis (mono_tags, lifting) mem_Collect_eq) |
|
405 ultimately |
|
406 show "finite (LV (SEQ r1 r2) s)" |
|
407 by (simp add: finite_subset) |
|
408 next |
|
409 case (STAR r s) |
|
410 then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) |
|
411 next |
|
412 case (NTIMES r n s) |
|
413 have "\<And>s. finite (LV r s)" by fact |
|
414 then have "finite (Stars_Append (LV (STAR r) s) (\<Union>i\<le>n. LV (NTIMES r i) []))" |
|
415 apply(rule_tac finite_Stars_Append) |
|
416 apply (simp add: LV_STAR_finite) |
|
417 using finite_NTimes_empty by blast |
|
418 then show "finite (LV (NTIMES r n) s)" |
|
419 by (metis LV_NTIMES_subset finite_subset) |
|
420 qed |
|
421 |
|
422 |
|
423 |
|
424 section \<open>Our inductive POSIX Definition\<close> |
|
425 |
|
426 inductive |
|
427 Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
|
428 where |
|
429 Posix_ONE: "[] \<in> ONE \<rightarrow> Void" |
|
430 | Posix_CH: "[c] \<in> (CH c) \<rightarrow> (Char c)" |
|
431 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
|
432 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
|
433 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
|
434 \<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> |
|
435 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
|
436 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
437 \<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> |
|
438 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
|
439 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
|
440 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs; flat v \<noteq> []; 0 < n; |
|
441 \<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 - 1)))\<rbrakk> |
|
442 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r n \<rightarrow> Stars (v # vs)" |
|
443 | Posix_NTIMES2: "\<lbrakk>\<forall>v \<in> set vs. [] \<in> r \<rightarrow> v; length vs = n\<rbrakk> |
|
444 \<Longrightarrow> [] \<in> NTIMES r n \<rightarrow> Stars vs" |
|
445 |
|
446 inductive_cases Posix_elims: |
|
447 "s \<in> ZERO \<rightarrow> v" |
|
448 "s \<in> ONE \<rightarrow> v" |
|
449 "s \<in> CH c \<rightarrow> v" |
|
450 "s \<in> ALT r1 r2 \<rightarrow> v" |
|
451 "s \<in> SEQ r1 r2 \<rightarrow> v" |
|
452 "s \<in> STAR r \<rightarrow> v" |
|
453 "s \<in> NTIMES r n \<rightarrow> v" |
|
454 |
|
455 |
|
456 lemma Posix1: |
|
457 assumes "s \<in> r \<rightarrow> v" |
|
458 shows "s \<in> L r" "flat v = s" |
|
459 using assms |
|
460 apply(induct s r v rule: Posix.induct) |
|
461 apply(auto simp add: pow_empty_iff) |
|
462 apply (metis Suc_pred concI lang_pow.simps(2)) |
|
463 by (meson ex_in_conv set_empty) |
|
464 |
|
465 |
|
466 |
|
467 lemma Posix1a: |
|
468 assumes "s \<in> r \<rightarrow> v" |
|
469 shows "\<Turnstile> v : r" |
|
470 using assms |
|
471 apply(induct s r v rule: Posix.induct) |
|
472 apply(auto intro: Prf.intros) |
|
473 apply (metis Prf.intros(6) Prf_elims(6) set_ConsD val.inject(5)) |
|
474 prefer 2 |
|
475 apply (metis Posix1(2) Prf.intros(7) append_Nil empty_iff list.set(1)) |
|
476 apply(erule Prf_elims) |
|
477 apply(auto) |
|
478 apply(subst append.simps(2)[symmetric]) |
|
479 apply(rule Prf.intros) |
|
480 apply(auto) |
|
481 done |
|
482 |
|
483 text \<open> |
|
484 For a give value and string, our Posix definition |
|
485 determines a unique value. |
|
486 \<close> |
|
487 |
|
488 lemma List_eq_zipI: |
|
489 assumes "list_all2 (\<lambda>v1 v2. v1 = v2) vs1 vs2" |
|
490 and "length vs1 = length vs2" |
|
491 shows "vs1 = vs2" |
|
492 using assms |
|
493 apply(induct vs1 vs2 rule: list_all2_induct) |
|
494 apply(auto) |
|
495 done |
|
496 |
|
497 lemma Posix_determ: |
|
498 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
499 shows "v1 = v2" |
|
500 using assms |
|
501 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
502 case (Posix_ONE v2) |
|
503 have "[] \<in> ONE \<rightarrow> v2" by fact |
|
504 then show "Void = v2" by cases auto |
|
505 next |
|
506 case (Posix_CH c v2) |
|
507 have "[c] \<in> CH c \<rightarrow> v2" by fact |
|
508 then show "Char c = v2" by cases auto |
|
509 next |
|
510 case (Posix_ALT1 s r1 v r2 v2) |
|
511 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
512 moreover |
|
513 have "s \<in> r1 \<rightarrow> v" by fact |
|
514 then have "s \<in> L r1" by (simp add: Posix1) |
|
515 ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto |
|
516 moreover |
|
517 have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
518 ultimately have "v = v'" by simp |
|
519 then show "Left v = v2" using eq by simp |
|
520 next |
|
521 case (Posix_ALT2 s r2 v r1 v2) |
|
522 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
523 moreover |
|
524 have "s \<notin> L r1" by fact |
|
525 ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" |
|
526 by cases (auto simp add: Posix1) |
|
527 moreover |
|
528 have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
529 ultimately have "v = v'" by simp |
|
530 then show "Right v = v2" using eq by simp |
|
531 next |
|
532 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v') |
|
533 have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" |
|
534 "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" |
|
535 "\<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+ |
|
536 then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" |
|
537 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
538 using Posix1(1) by fastforce+ |
|
539 moreover |
|
540 have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" |
|
541 "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ |
|
542 ultimately show "Seq v1 v2 = v'" by simp |
|
543 next |
|
544 case (Posix_STAR1 s1 r v s2 vs v2) |
|
545 have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" |
|
546 "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
547 "\<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+ |
|
548 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
549 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
550 using Posix1(1) apply fastforce |
|
551 apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2) |
|
552 using Posix1(2) by blast |
|
553 moreover |
|
554 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
555 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
556 ultimately show "Stars (v # vs) = v2" by auto |
|
557 next |
|
558 case (Posix_STAR2 r v2) |
|
559 have "[] \<in> STAR r \<rightarrow> v2" by fact |
|
560 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
561 next |
|
562 case (Posix_NTIMES2 vs r n v2) |
|
563 then show "Stars vs = v2" |
|
564 apply(erule_tac Posix_elims) |
|
565 apply(auto) |
|
566 apply (simp add: Posix1(2)) |
|
567 apply(rule List_eq_zipI) |
|
568 apply(auto simp add: list_all2_iff) |
|
569 by (meson in_set_zipE) |
|
570 next |
|
571 case (Posix_NTIMES1 s1 r v s2 n vs) |
|
572 have "(s1 @ s2) \<in> NTIMES r n \<rightarrow> v2" |
|
573 "s1 \<in> r \<rightarrow> v" "s2 \<in> NTIMES r (n - 1) \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
574 "\<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 - 1 )))" by fact+ |
|
575 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r (n - 1)) \<rightarrow> (Stars vs')" |
|
576 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
577 using Posix1(1) apply fastforce |
|
578 apply (metis One_nat_def Posix1(1) Posix_NTIMES1.hyps(7) append.right_neutral append_self_conv2) |
|
579 using Posix1(2) by blast |
|
580 moreover |
|
581 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
582 "\<And>v2. s2 \<in> NTIMES r (n - 1) \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
583 ultimately show "Stars (v # vs) = v2" by auto |
|
584 qed |
|
585 |
|
586 |
|
587 text \<open> |
|
588 Our POSIX values are lexical values. |
|
589 \<close> |
|
590 |
|
591 lemma Posix_LV: |
|
592 assumes "s \<in> r \<rightarrow> v" |
|
593 shows "v \<in> LV r s" |
|
594 using assms unfolding LV_def |
|
595 apply(induct rule: Posix.induct) |
|
596 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims Posix1a) |
|
597 apply (smt (verit, best) One_nat_def Posix1a Posix_NTIMES1 L.simps(7)) |
|
598 using Posix1a Posix_NTIMES2 by blast |
|
599 |
|
600 |
|
601 lemma longer_string_nonempty_suff: |
|
602 shows "s3 @ s4 = s1 @ s2 \<and> length s3 > length s1 \<Longrightarrow> (\<exists>s5. s3 = s1 @ s5 \<and> s5 \<noteq> [])" |
|
603 sorry |
|
604 |
|
605 |
|
606 lemma equivalent_concat_condition_aux: |
|
607 shows "(\<exists>s3 s4. s3 @ s4 = s1 @ s2 \<and> length s3 > length s1\<and> s3 \<in> L r1 \<and> s4 \<in> L r2 ) \<Longrightarrow> (\<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)" |
|
608 apply(erule exE)+ |
|
609 apply(subgoal_tac "\<exists>s5. s3 = s1 @ s5\<and> s5 \<noteq> [] ") |
|
610 apply(erule exE) |
|
611 apply auto[1] |
|
612 using longer_string_nonempty_suff by blast |
|
613 |
|
614 lemma equivalent_concat_condition: |
|
615 shows " \<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) \<Longrightarrow> \<not>(\<exists>s3 s4. s3 @ s4 = s1 @ s2 \<and> length s3 > length s1\<and> s3 \<in> L r1 \<and> s4 \<in> L r2 )" |
|
616 by (meson equivalent_concat_condition_aux) |
|
617 |
|
618 lemma seqPOSIX_altdef: |
|
619 shows "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
|
620 \<not>(\<exists>s3 s4. s3 @ s4 = s1 @ s2 \<and> length s3 > length s1\<and> s3 \<in> L r1 \<and> s4 \<in> L r2 )\<rbrakk> \<Longrightarrow> |
|
621 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
|
622 by (metis Posix_SEQ append.assoc length_append length_greater_0_conv less_add_same_cancel1) |
|
623 |
|
624 |
|
625 |
|
626 end |