62 | "flat(Char c) = [c]" |
62 | "flat(Char c) = [c]" |
63 | "flat(Left v) = flat(v)" |
63 | "flat(Left v) = flat(v)" |
64 | "flat(Right v) = flat(v)" |
64 | "flat(Right v) = flat(v)" |
65 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
65 | "flat(Seq v1 v2) = flat(v1) @ flat(v2)" |
66 |
66 |
|
67 (* not actually in the paper *) |
67 datatype tree = |
68 datatype tree = |
68 Leaf string |
69 Leaf string |
69 | Branch tree tree |
70 | Branch tree tree |
70 |
71 |
71 fun flats :: "val \<Rightarrow> tree" |
72 fun flats :: "val \<Rightarrow> tree" |
101 apply (metis Prf.intros(4) flat.simps(1)) |
102 apply (metis Prf.intros(4) flat.simps(1)) |
102 apply (metis Prf.intros(5) flat.simps(2)) |
103 apply (metis Prf.intros(5) flat.simps(2)) |
103 apply (metis Prf.intros(1) flat.simps(5)) |
104 apply (metis Prf.intros(1) flat.simps(5)) |
104 apply (metis Prf.intros(2) flat.simps(3)) |
105 apply (metis Prf.intros(2) flat.simps(3)) |
105 apply (metis Prf.intros(3) flat.simps(4)) |
106 apply (metis Prf.intros(3) flat.simps(4)) |
106 by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3)) |
107 sorry |
|
108 |
|
109 (*by (smt Prf.cases flat.simps(3) flat.simps(4) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.inject(3))*) |
107 |
110 |
108 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
111 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100) |
109 where |
112 where |
110 "\<lbrakk>v1 \<succ>r1 v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
113 "\<lbrakk>v1 = v1'; v2 \<succ>r2 v2'\<rbrakk> \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
|
114 | "v1 \<succ>r1 v1' \<Longrightarrow> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1' v2')" |
111 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
115 | "length (flat v1) \<ge> length (flat v2) \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Right v2)" |
112 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)" |
116 | "length (flat v2) > length (flat v1) \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Left v1)" |
113 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
117 | "v2 \<succ>r2 v2' \<Longrightarrow> (Right v2) \<succ>(ALT r1 r2) (Right v2')" |
114 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
118 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')" |
115 | "Void \<succ>EMPTY Void" |
119 | "Void \<succ>EMPTY Void" |
116 | "(Char c) \<succ>(CHAR c) (Char c)" |
120 | "(Char c) \<succ>(CHAR c) (Char c)" |
117 |
121 |
|
122 (* |
118 lemma |
123 lemma |
119 assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))" |
124 assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))" |
120 shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))" |
125 shows "(Seq (Left Void) (Right (Char c))) \<succ>r (Seq (Left Void) (Left Void))" |
121 using assms |
126 using assms |
122 apply(simp) |
127 apply(simp) |
124 apply(rule ValOrd.intros) |
129 apply(rule ValOrd.intros) |
125 apply(rule ValOrd.intros) |
130 apply(rule ValOrd.intros) |
126 apply(rule ValOrd.intros) |
131 apply(rule ValOrd.intros) |
127 apply(simp) |
132 apply(simp) |
128 done |
133 done |
129 |
134 *) |
130 |
135 |
131 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
136 definition POSIX :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
132 where |
137 where |
133 "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flats v = flats v') \<longrightarrow> v \<succ>r v')" |
138 "POSIX v r \<equiv> (\<forall>v'. (\<turnstile> v' : r \<and> flat v = flat v') \<longrightarrow> v \<succ>r v')" |
134 |
139 |
135 lemma POSIX: |
140 (* |
136 assumes "r = SEQ (ALT EMPTY EMPTY) (ALT EMPTY (CHAR c))" |
|
137 shows "POSIX (Seq (Left Void) (Right (Char c))) r" |
|
138 apply(simp add: POSIX_def assms) |
|
139 apply(auto) |
|
140 apply(erule Prf.cases) |
|
141 apply(simp_all) |
|
142 apply(rule ValOrd.intros) |
|
143 apply (smt POSIX_def Prf.cases Prf.simps ValOrd.intros(2) ValOrd.intros(5) ValOrd.intros(6) flats.simps(1) flats.simps(3) rexp.distinct(11) rexp.distinct(13) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(3) val.distinct(19) val.inject(3)) |
|
144 by (smt Prf.simps ValOrd.intros(4) ValOrd.intros(7) flats.simps(1) flats.simps(3) list.distinct(1) rexp.distinct(11) rexp.distinct(13) rexp.distinct(15) rexp.distinct(17) rexp.distinct(19) rexp.distinct(9) rexp.inject(1) rexp.inject(3) tree.inject(1)) |
|
145 |
|
146 |
|
147 lemma Exists_POSIX: "\<exists>v. POSIX v r" |
|
148 apply(induct r) |
|
149 apply(auto simp add: POSIX_def) |
|
150 apply(rule exI) |
|
151 apply(auto) |
|
152 apply(erule Prf.cases) |
|
153 apply(simp_all)[5] |
|
154 apply (smt Prf.simps ValOrd.intros(6) rexp.distinct(11) rexp.distinct(13) rexp.distinct(9)) |
|
155 apply(rule exI) |
|
156 apply(auto) |
|
157 apply(erule Prf.cases) |
|
158 apply(simp_all)[5] |
|
159 apply(rule ValOrd.intros) |
|
160 apply(rule exI) |
|
161 apply(auto) |
|
162 apply(erule Prf.cases) |
|
163 apply(simp_all)[5] |
|
164 apply(rule ValOrd.intros) |
|
165 apply(auto)[2] |
|
166 apply(rule_tac x="Left v" in exI) |
|
167 apply(auto) |
|
168 apply(erule Prf.cases) |
|
169 apply(simp_all)[5] |
|
170 apply(rule ValOrd.intros) |
|
171 apply(auto)[1] |
|
172 apply(auto) |
|
173 apply(rule ValOrd.intros) |
|
174 by (metis flats_flat order_refl) |
|
175 |
|
176 |
|
177 lemma POSIX_SEQ: |
141 lemma POSIX_SEQ: |
178 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
142 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
179 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
143 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
180 using assms |
144 using assms |
181 unfolding POSIX_def |
145 unfolding POSIX_def |
184 apply(simp) |
148 apply(simp) |
185 apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2)) |
149 apply (smt Prf.intros(1) ValOrd.simps assms(3) rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2)) |
186 apply(drule_tac x="Seq v1 v'" in spec) |
150 apply(drule_tac x="Seq v1 v'" in spec) |
187 apply(simp) |
151 apply(simp) |
188 by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2)) |
152 by (smt Prf.intros(1) ValOrd.simps rexp.inject(2) val.distinct(15) val.distinct(17) val.distinct(3) val.distinct(9) val.inject(2)) |
189 |
153 *) |
|
154 |
|
155 (* |
190 lemma POSIX_SEQ_I: |
156 lemma POSIX_SEQ_I: |
191 assumes "POSIX v1 r1" "POSIX v2 r2" |
157 assumes "POSIX v1 r1" "POSIX v2 r2" |
192 shows "POSIX (Seq v1 v2) (SEQ r1 r2)" |
158 shows "POSIX (Seq v1 v2) (SEQ r1 r2)" |
193 using assms |
159 using assms |
194 unfolding POSIX_def |
160 unfolding POSIX_def |
269 apply(rule ValOrd.intros) |
235 apply(rule ValOrd.intros) |
270 apply metis |
236 apply metis |
271 apply(rule ValOrd.intros) |
237 apply(rule ValOrd.intros) |
272 apply(auto) |
238 apply(auto) |
273 done |
239 done |
|
240 *) |
274 |
241 |
275 lemma ValOrd_refl: |
242 lemma ValOrd_refl: |
276 assumes "\<turnstile> v : r" |
243 assumes "\<turnstile> v : r" |
277 shows "v \<succ>r v" |
244 shows "v \<succ>r v" |
278 using assms |
245 using assms |
279 apply(induct) |
246 apply(induct) |
280 apply(auto intro: ValOrd.intros) |
247 apply(auto intro: ValOrd.intros) |
281 done |
248 done |
282 |
249 |
|
250 (* |
283 lemma ValOrd_length: |
251 lemma ValOrd_length: |
284 assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)" |
252 assumes "v1 \<succ>r v2" shows "length (flat v1) \<ge> length (flat v2)" |
285 using assms |
253 using assms |
286 apply(induct) |
254 apply(induct) |
287 apply(auto) |
255 apply(auto) |
288 done |
256 done |
|
257 *) |
289 |
258 |
290 section {* The Matcher *} |
259 section {* The Matcher *} |
291 |
260 |
292 fun |
261 fun |
293 nullable :: "rexp \<Rightarrow> bool" |
262 nullable :: "rexp \<Rightarrow> bool" |
335 lemma mkeps_POSIX: |
304 lemma mkeps_POSIX: |
336 assumes "nullable r" |
305 assumes "nullable r" |
337 shows "POSIX (mkeps r) r" |
306 shows "POSIX (mkeps r) r" |
338 using assms |
307 using assms |
339 apply(induct r) |
308 apply(induct r) |
340 apply(auto) |
309 apply(auto)[1] |
341 apply(simp add: POSIX_def) |
310 apply(simp add: POSIX_def) |
342 apply(auto)[1] |
311 apply(auto)[1] |
343 apply(erule Prf.cases) |
312 apply(erule Prf.cases) |
344 apply(simp_all)[5] |
313 apply(simp_all)[5] |
345 apply (metis ValOrd.intros(6)) |
314 apply (metis ValOrd.intros) |
346 apply(simp add: POSIX_def) |
315 apply(simp add: POSIX_def) |
347 apply(auto)[1] |
316 apply(auto)[1] |
348 apply(erule Prf.cases) |
317 sorry |
349 apply(simp_all)[5] |
318 |
350 apply(auto) |
|
351 apply (metis ValOrd.intros(1) append_is_Nil_conv mkeps_flat) |
|
352 apply(simp add: POSIX_def) |
|
353 apply(auto)[1] |
|
354 apply(erule Prf.cases) |
|
355 apply(simp_all)[5] |
|
356 apply(auto) |
|
357 apply (metis ValOrd.intros(5)) |
|
358 apply(rule ValOrd.intros(2)) |
|
359 apply(simp add: mkeps_flat) |
|
360 apply(simp add: flats_flat) |
|
361 apply (metis mkeps_flats) |
|
362 apply(simp add: POSIX_def) |
|
363 apply(auto)[1] |
|
364 apply(erule Prf.cases) |
|
365 apply(simp_all)[5] |
|
366 apply(auto) |
|
367 apply (metis ValOrd.intros(5)) |
|
368 apply (smt ValOrd.intros(2) flats_flat) |
|
369 apply(simp add: POSIX_def) |
|
370 apply(auto)[1] |
|
371 apply(erule Prf.cases) |
|
372 apply(simp_all)[5] |
|
373 apply (metis Prf_flat_L flats_flat mkeps_flats nullable_correctness) |
|
374 by (metis ValOrd.intros(4)) |
|
375 |
319 |
376 fun |
320 fun |
377 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
321 der :: "char \<Rightarrow> rexp \<Rightarrow> rexp" |
378 where |
322 where |
379 "der c (NULL) = NULL" |
323 "der c (NULL) = NULL" |
554 apply(induct v) |
498 apply(induct v) |
555 apply(simp_all) |
499 apply(simp_all) |
556 apply (metis Nil_is_append_conv head.elims option.distinct(1)) |
500 apply (metis Nil_is_append_conv head.elims option.distinct(1)) |
557 done |
501 done |
558 |
502 |
|
503 (* HERE *) |
559 lemma v5: |
504 lemma v5: |
560 assumes "\<turnstile> v : der c r" "POSIX v (der c r)" |
505 assumes "\<turnstile> v : der c r" "POSIX v (der c r)" |
561 shows "POSIX (injval r c v) r" |
506 shows "POSIX (injval r c v) r" |
562 using assms |
507 using assms |
|
508 apply(induct r) |
|
509 apply(simp (no_asm) only: POSIX_def) |
|
510 apply(rule allI) |
|
511 apply(rule impI) |
|
512 apply(simp) |
|
513 apply(erule Prf.cases) |
|
514 apply(simp_all)[5] |
563 apply(induct arbitrary: v rule: der.induct) |
515 apply(induct arbitrary: v rule: der.induct) |
564 apply(simp) |
516 apply(simp) |
565 apply(erule Prf.cases) |
517 apply(erule Prf.cases) |
566 apply(simp_all)[5] |
518 apply(simp_all)[5] |
567 apply(simp) |
519 apply(simp) |