equal
deleted
inserted
replaced
133 |
133 |
134 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
134 definition POSIX2 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
135 where |
135 where |
136 "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')" |
136 "POSIX2 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. \<turnstile> v' : r \<longrightarrow> v \<succ>r v')" |
137 |
137 |
|
138 definition POSIX3 :: "val \<Rightarrow> rexp \<Rightarrow> bool" |
|
139 where |
|
140 "POSIX3 v r \<equiv> \<turnstile> v : r \<and> (\<forall>v'. (\<turnstile> v' : r \<and> flat v \<ge> flat v') \<longrightarrow> v \<succ>r v')" |
|
141 |
138 |
142 |
139 (* |
143 (* |
140 lemma POSIX_SEQ: |
144 lemma POSIX_SEQ: |
141 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
145 assumes "POSIX (Seq v1 v2) (SEQ r1 r2)" "\<turnstile> v1 : r1" "\<turnstile> v2 : r2" |
142 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
146 shows "POSIX v1 r1 \<and> POSIX v2 r2" |
166 |
170 |
167 apply(auto) |
171 apply(auto) |
168 done |
172 done |
169 *) |
173 *) |
170 |
174 |
|
175 |
|
176 |
|
177 |
|
178 lemma POSIX_ALT2: |
|
179 assumes "POSIX (Left v1) (ALT r1 r2)" |
|
180 shows "POSIX v1 r1" |
|
181 using assms |
|
182 unfolding POSIX_def |
|
183 apply(auto) |
|
184 apply(drule_tac x="Left v'" in spec) |
|
185 apply(simp) |
|
186 apply(drule mp) |
|
187 apply(rule Prf.intros) |
|
188 apply(auto) |
|
189 apply(erule ValOrd.cases) |
|
190 apply(simp_all) |
|
191 done |
|
192 |
|
193 lemma POSIX2_ALT: |
|
194 assumes "POSIX2 (Left v1) (ALT r1 r2)" |
|
195 shows "POSIX2 v1 r1" |
|
196 using assms |
|
197 unfolding POSIX2_def |
|
198 apply(auto) |
|
199 |
|
200 done |
|
201 |
171 lemma POSIX_ALT: |
202 lemma POSIX_ALT: |
172 assumes "POSIX (Left v1) (ALT r1 r2)" |
203 assumes "POSIX (Left v1) (ALT r1 r2)" |
173 shows "POSIX v1 r1" |
204 shows "POSIX v1 r1" |
174 using assms |
205 using assms |
175 unfolding POSIX_def |
206 unfolding POSIX_def |
181 apply(auto) |
212 apply(auto) |
182 apply(erule ValOrd.cases) |
213 apply(erule ValOrd.cases) |
183 apply(simp_all) |
214 apply(simp_all) |
184 done |
215 done |
185 |
216 |
|
217 lemma POSIX2_ALT: |
|
218 assumes "POSIX2 (Left v1) (ALT r1 r2)" |
|
219 shows "POSIX2 v1 r1" |
|
220 using assms |
|
221 apply(simp add: POSIX2_def) |
|
222 apply(auto) |
|
223 apply(erule Prf.cases) |
|
224 apply(simp_all)[5] |
|
225 apply(drule_tac x="Left v'" in spec) |
|
226 apply(drule mp) |
|
227 apply(rule Prf.intros) |
|
228 apply(auto) |
|
229 apply(erule ValOrd.cases) |
|
230 apply(simp_all) |
|
231 done |
|
232 |
|
233 |
186 lemma POSIX_ALT1a: |
234 lemma POSIX_ALT1a: |
187 assumes "POSIX (Right v2) (ALT r1 r2)" |
235 assumes "POSIX (Right v2) (ALT r1 r2)" |
188 shows "POSIX v2 r2" |
236 shows "POSIX v2 r2" |
189 using assms |
237 using assms |
190 unfolding POSIX_def |
238 unfolding POSIX_def |
196 apply(auto) |
244 apply(auto) |
197 apply(erule ValOrd.cases) |
245 apply(erule ValOrd.cases) |
198 apply(simp_all) |
246 apply(simp_all) |
199 done |
247 done |
200 |
248 |
|
249 lemma POSIX2_ALT1a: |
|
250 assumes "POSIX2 (Right v2) (ALT r1 r2)" |
|
251 shows "POSIX2 v2 r2" |
|
252 using assms |
|
253 unfolding POSIX2_def |
|
254 apply(auto) |
|
255 apply(erule Prf.cases) |
|
256 apply(simp_all)[5] |
|
257 apply(drule_tac x="Right v'" in spec) |
|
258 apply(drule mp) |
|
259 apply(rule Prf.intros) |
|
260 apply(auto) |
|
261 apply(erule ValOrd.cases) |
|
262 apply(simp_all) |
|
263 done |
|
264 |
201 |
265 |
202 lemma POSIX_ALT1b: |
266 lemma POSIX_ALT1b: |
203 assumes "POSIX (Right v2) (ALT r1 r2)" |
267 assumes "POSIX (Right v2) (ALT r1 r2)" |
204 shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')" |
268 shows "(\<forall>v'. (\<turnstile> v' : r2 \<and> flat v' = flat v2) \<longrightarrow> v2 \<succ>r2 v')" |
205 using assms |
269 using assms |
219 apply(simp_all)[5] |
283 apply(simp_all)[5] |
220 apply(auto) |
284 apply(auto) |
221 apply(rule ValOrd.intros) |
285 apply(rule ValOrd.intros) |
222 apply(auto) |
286 apply(auto) |
223 apply(rule ValOrd.intros) |
287 apply(rule ValOrd.intros) |
|
288 by simp |
|
289 |
|
290 lemma POSIX2_ALT_I1: |
|
291 assumes "POSIX2 v1 r1" |
|
292 shows "POSIX2 (Left v1) (ALT r1 r2)" |
|
293 using assms |
|
294 unfolding POSIX2_def |
|
295 apply(auto) |
|
296 apply(rule Prf.intros) |
|
297 apply(simp) |
|
298 apply(rotate_tac 2) |
|
299 apply(erule Prf.cases) |
|
300 apply(simp_all)[5] |
|
301 apply(auto) |
|
302 apply(rule ValOrd.intros) |
|
303 apply(auto) |
|
304 apply(rule ValOrd.intros) |
|
305 |
|
306 |
224 by simp |
307 by simp |
225 |
308 |
226 lemma POSIX_ALT_I2: |
309 lemma POSIX_ALT_I2: |
227 assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" |
310 assumes "POSIX v2 r2" "\<forall>v'. \<turnstile> v' : r1 \<longrightarrow> length (flat v2) > length (flat v')" |
228 shows "POSIX (Right v2) (ALT r1 r2)" |
311 shows "POSIX (Right v2) (ALT r1 r2)" |
289 text {* |
372 text {* |
290 The value mkeps returns is always the correct POSIX |
373 The value mkeps returns is always the correct POSIX |
291 value. |
374 value. |
292 *} |
375 *} |
293 |
376 |
|
377 lemma mkeps_POSIX2: |
|
378 assumes "nullable r" |
|
379 shows "POSIX2 (mkeps r) r" |
|
380 using assms |
|
381 apply(induct r) |
|
382 apply(auto)[1] |
|
383 apply(simp add: POSIX2_def) |
|
384 |
294 lemma mkeps_POSIX: |
385 lemma mkeps_POSIX: |
295 assumes "nullable r" |
386 assumes "nullable r" |
296 shows "POSIX (mkeps r) r" |
387 shows "POSIX (mkeps r) r" |
297 using assms |
388 using assms |
298 apply(induct r) |
389 apply(induct r) |
329 apply(erule Prf.cases) |
420 apply(erule Prf.cases) |
330 apply(simp_all)[5] |
421 apply(simp_all)[5] |
331 apply(auto) |
422 apply(auto) |
332 apply (metis Prf_flat_L mkeps_flat nullable_correctness) |
423 apply (metis Prf_flat_L mkeps_flat nullable_correctness) |
333 by (simp add: ValOrd.intros(5)) |
424 by (simp add: ValOrd.intros(5)) |
|
425 |
|
426 |
|
427 lemma mkeps_POSIX2: |
|
428 assumes "nullable r" |
|
429 shows "POSIX2 (mkeps r) r" |
|
430 using assms |
|
431 apply(induct r) |
|
432 apply(simp) |
|
433 apply(simp) |
|
434 apply(simp add: POSIX2_def) |
|
435 apply(rule conjI) |
|
436 apply(rule Prf.intros) |
|
437 apply(auto)[1] |
|
438 apply(erule Prf.cases) |
|
439 apply(simp_all)[5] |
|
440 apply(rule ValOrd.intros) |
|
441 apply(simp) |
|
442 apply(simp) |
|
443 apply(simp add: POSIX2_def) |
|
444 apply(rule conjI) |
|
445 apply(rule Prf.intros) |
|
446 apply(simp add: mkeps_nullable) |
|
447 apply(simp add: mkeps_nullable) |
|
448 apply(auto)[1] |
|
449 apply(rotate_tac 6) |
|
450 apply(erule Prf.cases) |
|
451 apply(simp_all)[5] |
|
452 apply(rule ValOrd.intros(2)) |
|
453 apply(simp) |
|
454 apply(simp only: nullable.simps) |
|
455 apply(erule disjE) |
|
456 apply(simp) |
|
457 thm POSIX2_ALT1a |
|
458 apply(rule POSIX2_ALT) |
|
459 apply(simp add: POSIX2_def) |
|
460 apply(rule conjI) |
|
461 apply(rule Prf.intros) |
|
462 apply(simp add: mkeps_nullable) |
|
463 apply(auto)[1] |
|
464 apply(rotate_tac 4) |
|
465 apply(erule Prf.cases) |
|
466 apply(simp_all)[5] |
|
467 apply(rule ValOrd.intros) |
|
468 apply(simp) |
|
469 apply(rule ValOrd.intros) |
334 |
470 |
335 |
471 |
336 section {* Derivatives *} |
472 section {* Derivatives *} |
337 |
473 |
338 fun |
474 fun |