|
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 |
|
50 inductive_cases Prf_elims: |
|
51 "\<Turnstile> v : ZERO" |
|
52 "\<Turnstile> v : SEQ r1 r2" |
|
53 "\<Turnstile> v : ALT r1 r2" |
|
54 "\<Turnstile> v : ONE" |
|
55 "\<Turnstile> v : CH c" |
|
56 "\<Turnstile> vs : STAR r" |
|
57 |
|
58 lemma Prf_Stars_appendE: |
|
59 assumes "\<Turnstile> Stars (vs1 @ vs2) : STAR r" |
|
60 shows "\<Turnstile> Stars vs1 : STAR r \<and> \<Turnstile> Stars vs2 : STAR r" |
|
61 using assms |
|
62 by (auto intro: Prf.intros elim!: Prf_elims) |
|
63 |
|
64 |
|
65 lemma flats_Prf_value: |
|
66 assumes "\<forall>s\<in>set ss. \<exists>v. s = flat v \<and> \<Turnstile> v : r" |
|
67 shows "\<exists>vs. flats vs = concat ss \<and> (\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> [])" |
|
68 using assms |
|
69 apply(induct ss) |
|
70 apply(auto) |
|
71 apply(rule_tac x="[]" in exI) |
|
72 apply(simp) |
|
73 apply(case_tac "flat v = []") |
|
74 apply(rule_tac x="vs" in exI) |
|
75 apply(simp) |
|
76 apply(rule_tac x="v#vs" in exI) |
|
77 apply(simp) |
|
78 done |
|
79 |
|
80 |
|
81 lemma L_flat_Prf1: |
|
82 assumes "\<Turnstile> v : r" |
|
83 shows "flat v \<in> L r" |
|
84 using assms |
|
85 by (induct) (auto simp add: Sequ_def Star_concat) |
|
86 |
|
87 lemma L_flat_Prf2: |
|
88 assumes "s \<in> L r" |
|
89 shows "\<exists>v. \<Turnstile> v : r \<and> flat v = s" |
|
90 using assms |
|
91 proof(induct r arbitrary: s) |
|
92 case (STAR r s) |
|
93 have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<Turnstile> v : r \<and> flat v = s" by fact |
|
94 have "s \<in> L (STAR r)" by fact |
|
95 then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r \<and> s \<noteq> []" |
|
96 using Star_split by auto |
|
97 then obtain vs where "flats vs = s" "\<forall>v\<in>set vs. \<Turnstile> v : r \<and> flat v \<noteq> []" |
|
98 using IH flats_Prf_value by metis |
|
99 then show "\<exists>v. \<Turnstile> v : STAR r \<and> flat v = s" |
|
100 using Prf.intros(6) flat_Stars by blast |
|
101 next |
|
102 case (SEQ r1 r2 s) |
|
103 then show "\<exists>v. \<Turnstile> v : SEQ r1 r2 \<and> flat v = s" |
|
104 unfolding Sequ_def L.simps by (fastforce intro: Prf.intros) |
|
105 next |
|
106 case (ALT r1 r2 s) |
|
107 then show "\<exists>v. \<Turnstile> v : ALT r1 r2 \<and> flat v = s" |
|
108 unfolding L.simps by (fastforce intro: Prf.intros) |
|
109 qed (auto intro: Prf.intros) |
|
110 |
|
111 |
|
112 lemma L_flat_Prf: |
|
113 shows "L(r) = {flat v | v. \<Turnstile> v : r}" |
|
114 using L_flat_Prf1 L_flat_Prf2 by blast |
|
115 |
|
116 |
|
117 |
|
118 section \<open>Sets of Lexical Values\<close> |
|
119 |
|
120 text \<open> |
|
121 Shows that lexical values are finite for a given regex and string. |
|
122 \<close> |
|
123 |
|
124 definition |
|
125 LV :: "rexp \<Rightarrow> string \<Rightarrow> val set" |
|
126 where "LV r s \<equiv> {v. \<Turnstile> v : r \<and> flat v = s}" |
|
127 |
|
128 lemma LV_simps: |
|
129 shows "LV ZERO s = {}" |
|
130 and "LV ONE s = (if s = [] then {Void} else {})" |
|
131 and "LV (CH c) s = (if s = [c] then {Char c} else {})" |
|
132 and "LV (ALT r1 r2) s = Left ` LV r1 s \<union> Right ` LV r2 s" |
|
133 unfolding LV_def |
|
134 by (auto intro: Prf.intros elim: Prf.cases) |
|
135 |
|
136 |
|
137 abbreviation |
|
138 "Prefixes s \<equiv> {s'. prefix s' s}" |
|
139 |
|
140 abbreviation |
|
141 "Suffixes s \<equiv> {s'. suffix s' s}" |
|
142 |
|
143 abbreviation |
|
144 "SSuffixes s \<equiv> {s'. strict_suffix s' s}" |
|
145 |
|
146 lemma Suffixes_cons [simp]: |
|
147 shows "Suffixes (c # s) = Suffixes s \<union> {c # s}" |
|
148 by (auto simp add: suffix_def Cons_eq_append_conv) |
|
149 |
|
150 |
|
151 lemma finite_Suffixes: |
|
152 shows "finite (Suffixes s)" |
|
153 by (induct s) (simp_all) |
|
154 |
|
155 lemma finite_SSuffixes: |
|
156 shows "finite (SSuffixes s)" |
|
157 proof - |
|
158 have "SSuffixes s \<subseteq> Suffixes s" |
|
159 unfolding strict_suffix_def suffix_def by auto |
|
160 then show "finite (SSuffixes s)" |
|
161 using finite_Suffixes finite_subset by blast |
|
162 qed |
|
163 |
|
164 lemma finite_Prefixes: |
|
165 shows "finite (Prefixes s)" |
|
166 proof - |
|
167 have "finite (Suffixes (rev s))" |
|
168 by (rule finite_Suffixes) |
|
169 then have "finite (rev ` Suffixes (rev s))" by simp |
|
170 moreover |
|
171 have "rev ` (Suffixes (rev s)) = Prefixes s" |
|
172 unfolding suffix_def prefix_def image_def |
|
173 by (auto)(metis rev_append rev_rev_ident)+ |
|
174 ultimately show "finite (Prefixes s)" by simp |
|
175 qed |
|
176 |
|
177 lemma LV_STAR_finite: |
|
178 assumes "\<forall>s. finite (LV r s)" |
|
179 shows "finite (LV (STAR r) s)" |
|
180 proof(induct s rule: length_induct) |
|
181 fix s::"char list" |
|
182 assume "\<forall>s'. length s' < length s \<longrightarrow> finite (LV (STAR r) s')" |
|
183 then have IH: "\<forall>s' \<in> SSuffixes s. finite (LV (STAR r) s')" |
|
184 by (force simp add: strict_suffix_def suffix_def) |
|
185 define f where "f \<equiv> \<lambda>(v, vs). Stars (v # vs)" |
|
186 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r s'" |
|
187 define S2 where "S2 \<equiv> \<Union>s2 \<in> SSuffixes s. Stars -` (LV (STAR r) s2)" |
|
188 have "finite S1" using assms |
|
189 unfolding S1_def by (simp_all add: finite_Prefixes) |
|
190 moreover |
|
191 with IH have "finite S2" unfolding S2_def |
|
192 by (auto simp add: finite_SSuffixes inj_on_def finite_vimageI) |
|
193 ultimately |
|
194 have "finite ({Stars []} \<union> f ` (S1 \<times> S2))" by simp |
|
195 moreover |
|
196 have "LV (STAR r) s \<subseteq> {Stars []} \<union> f ` (S1 \<times> S2)" |
|
197 unfolding S1_def S2_def f_def |
|
198 unfolding LV_def image_def prefix_def strict_suffix_def |
|
199 apply(auto) |
|
200 apply(case_tac x) |
|
201 apply(auto elim: Prf_elims) |
|
202 apply(erule Prf_elims) |
|
203 apply(auto) |
|
204 apply(case_tac vs) |
|
205 apply(auto intro: Prf.intros) |
|
206 apply(rule exI) |
|
207 apply(rule conjI) |
|
208 apply(rule_tac x="flat a" in exI) |
|
209 apply(rule conjI) |
|
210 apply(rule_tac x="flats list" in exI) |
|
211 apply(simp) |
|
212 apply(blast) |
|
213 apply(simp add: suffix_def) |
|
214 using Prf.intros(6) by blast |
|
215 ultimately |
|
216 show "finite (LV (STAR r) s)" by (simp add: finite_subset) |
|
217 qed |
|
218 |
|
219 |
|
220 lemma LV_finite: |
|
221 shows "finite (LV r s)" |
|
222 proof(induct r arbitrary: s) |
|
223 case (ZERO s) |
|
224 show "finite (LV ZERO s)" by (simp add: LV_simps) |
|
225 next |
|
226 case (ONE s) |
|
227 show "finite (LV ONE s)" by (simp add: LV_simps) |
|
228 next |
|
229 case (CH c s) |
|
230 show "finite (LV (CH c) s)" by (simp add: LV_simps) |
|
231 next |
|
232 case (ALT r1 r2 s) |
|
233 then show "finite (LV (ALT r1 r2) s)" by (simp add: LV_simps) |
|
234 next |
|
235 case (SEQ r1 r2 s) |
|
236 define f where "f \<equiv> \<lambda>(v1, v2). Seq v1 v2" |
|
237 define S1 where "S1 \<equiv> \<Union>s' \<in> Prefixes s. LV r1 s'" |
|
238 define S2 where "S2 \<equiv> \<Union>s' \<in> Suffixes s. LV r2 s'" |
|
239 have IHs: "\<And>s. finite (LV r1 s)" "\<And>s. finite (LV r2 s)" by fact+ |
|
240 then have "finite S1" "finite S2" unfolding S1_def S2_def |
|
241 by (simp_all add: finite_Prefixes finite_Suffixes) |
|
242 moreover |
|
243 have "LV (SEQ r1 r2) s \<subseteq> f ` (S1 \<times> S2)" |
|
244 unfolding f_def S1_def S2_def |
|
245 unfolding LV_def image_def prefix_def suffix_def |
|
246 apply (auto elim!: Prf_elims) |
|
247 by (metis (mono_tags, lifting) mem_Collect_eq) |
|
248 ultimately |
|
249 show "finite (LV (SEQ r1 r2) s)" |
|
250 by (simp add: finite_subset) |
|
251 next |
|
252 case (STAR r s) |
|
253 then show "finite (LV (STAR r) s)" by (simp add: LV_STAR_finite) |
|
254 qed |
|
255 |
|
256 |
|
257 |
|
258 section \<open>Our inductive POSIX Definition\<close> |
|
259 |
|
260 inductive |
|
261 Posix :: "string \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<in> _ \<rightarrow> _" [100, 100, 100] 100) |
|
262 where |
|
263 Posix_ONE: "[] \<in> ONE \<rightarrow> Void" |
|
264 | Posix_CH: "[c] \<in> (CH c) \<rightarrow> (Char c)" |
|
265 | Posix_ALT1: "s \<in> r1 \<rightarrow> v \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Left v)" |
|
266 | Posix_ALT2: "\<lbrakk>s \<in> r2 \<rightarrow> v; s \<notin> L(r1)\<rbrakk> \<Longrightarrow> s \<in> (ALT r1 r2) \<rightarrow> (Right v)" |
|
267 | Posix_SEQ: "\<lbrakk>s1 \<in> r1 \<rightarrow> v1; s2 \<in> r2 \<rightarrow> v2; |
|
268 \<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> |
|
269 (s1 @ s2) \<in> (SEQ r1 r2) \<rightarrow> (Seq v1 v2)" |
|
270 | Posix_STAR1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v \<noteq> []; |
|
271 \<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> |
|
272 \<Longrightarrow> (s1 @ s2) \<in> STAR r \<rightarrow> Stars (v # vs)" |
|
273 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
|
274 |
|
275 inductive_cases Posix_elims: |
|
276 "s \<in> ZERO \<rightarrow> v" |
|
277 "s \<in> ONE \<rightarrow> v" |
|
278 "s \<in> CH c \<rightarrow> v" |
|
279 "s \<in> ALT r1 r2 \<rightarrow> v" |
|
280 "s \<in> SEQ r1 r2 \<rightarrow> v" |
|
281 "s \<in> STAR r \<rightarrow> v" |
|
282 |
|
283 lemma Posix1: |
|
284 assumes "s \<in> r \<rightarrow> v" |
|
285 shows "s \<in> L r" "flat v = s" |
|
286 using assms |
|
287 by(induct s r v rule: Posix.induct) |
|
288 (auto simp add: Sequ_def) |
|
289 |
|
290 text \<open> |
|
291 For a give value and string, our Posix definition |
|
292 determines a unique value. |
|
293 \<close> |
|
294 |
|
295 lemma Posix_determ: |
|
296 assumes "s \<in> r \<rightarrow> v1" "s \<in> r \<rightarrow> v2" |
|
297 shows "v1 = v2" |
|
298 using assms |
|
299 proof (induct s r v1 arbitrary: v2 rule: Posix.induct) |
|
300 case (Posix_ONE v2) |
|
301 have "[] \<in> ONE \<rightarrow> v2" by fact |
|
302 then show "Void = v2" by cases auto |
|
303 next |
|
304 case (Posix_CH c v2) |
|
305 have "[c] \<in> CH c \<rightarrow> v2" by fact |
|
306 then show "Char c = v2" by cases auto |
|
307 next |
|
308 case (Posix_ALT1 s r1 v r2 v2) |
|
309 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
310 moreover |
|
311 have "s \<in> r1 \<rightarrow> v" by fact |
|
312 then have "s \<in> L r1" by (simp add: Posix1) |
|
313 ultimately obtain v' where eq: "v2 = Left v'" "s \<in> r1 \<rightarrow> v'" by cases auto |
|
314 moreover |
|
315 have IH: "\<And>v2. s \<in> r1 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
316 ultimately have "v = v'" by simp |
|
317 then show "Left v = v2" using eq by simp |
|
318 next |
|
319 case (Posix_ALT2 s r2 v r1 v2) |
|
320 have "s \<in> ALT r1 r2 \<rightarrow> v2" by fact |
|
321 moreover |
|
322 have "s \<notin> L r1" by fact |
|
323 ultimately obtain v' where eq: "v2 = Right v'" "s \<in> r2 \<rightarrow> v'" |
|
324 by cases (auto simp add: Posix1) |
|
325 moreover |
|
326 have IH: "\<And>v2. s \<in> r2 \<rightarrow> v2 \<Longrightarrow> v = v2" by fact |
|
327 ultimately have "v = v'" by simp |
|
328 then show "Right v = v2" using eq by simp |
|
329 next |
|
330 case (Posix_SEQ s1 r1 v1 s2 r2 v2 v') |
|
331 have "(s1 @ s2) \<in> SEQ r1 r2 \<rightarrow> v'" |
|
332 "s1 \<in> r1 \<rightarrow> v1" "s2 \<in> r2 \<rightarrow> v2" |
|
333 "\<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+ |
|
334 then obtain v1' v2' where "v' = Seq v1' v2'" "s1 \<in> r1 \<rightarrow> v1'" "s2 \<in> r2 \<rightarrow> v2'" |
|
335 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
336 using Posix1(1) by fastforce+ |
|
337 moreover |
|
338 have IHs: "\<And>v1'. s1 \<in> r1 \<rightarrow> v1' \<Longrightarrow> v1 = v1'" |
|
339 "\<And>v2'. s2 \<in> r2 \<rightarrow> v2' \<Longrightarrow> v2 = v2'" by fact+ |
|
340 ultimately show "Seq v1 v2 = v'" by simp |
|
341 next |
|
342 case (Posix_STAR1 s1 r v s2 vs v2) |
|
343 have "(s1 @ s2) \<in> STAR r \<rightarrow> v2" |
|
344 "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" "flat v \<noteq> []" |
|
345 "\<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+ |
|
346 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')" |
|
347 apply(cases) apply (auto simp add: append_eq_append_conv2) |
|
348 using Posix1(1) apply fastforce |
|
349 apply (metis Posix1(1) Posix_STAR1.hyps(6) append_Nil append_Nil2) |
|
350 using Posix1(2) by blast |
|
351 moreover |
|
352 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
|
353 "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
|
354 ultimately show "Stars (v # vs) = v2" by auto |
|
355 next |
|
356 case (Posix_STAR2 r v2) |
|
357 have "[] \<in> STAR r \<rightarrow> v2" by fact |
|
358 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
|
359 qed |
|
360 |
|
361 |
|
362 text \<open> |
|
363 Our POSIX values are lexical values. |
|
364 \<close> |
|
365 |
|
366 lemma Posix_LV: |
|
367 assumes "s \<in> r \<rightarrow> v" |
|
368 shows "v \<in> LV r s" |
|
369 using assms unfolding LV_def |
|
370 apply(induct rule: Posix.induct) |
|
371 apply(auto simp add: intro!: Prf.intros elim!: Prf_elims) |
|
372 done |
|
373 |
|
374 lemma Posix_Prf: |
|
375 assumes "s \<in> r \<rightarrow> v" |
|
376 shows "\<Turnstile> v : r" |
|
377 using assms Posix_LV LV_def |
|
378 by simp |
|
379 |
|
380 end |